Extend the dialect of for statement in Typescript

Strata/DL/CallHeap/CallHeapEvaluator.lean

@@ -169,8 +169,19 @@ partial def evalStatementWithContext (stmt : CallHeapStrataStatement) (ctx : Cal
       ctx
     | .goto _ _ =>
       ctx
-    | .loop _ _ _ _ _ =>
-      ctx
+    | .loop guard _ _ body _ =>
+      let rec loop (ctx : CallHeapEvalContext) : CallHeapEvalContext :=
+      let (newState, condVal) := Heap.evalHExpr ctx.hstate guard
+      let conditionIsTrue := match condVal with
+        | .lambda (.const "true" _) => true
+        | _ => false
+      let newCtx := { ctx with hstate := newState }
+      if conditionIsTrue then
+        let afterBody := evalProgramWithContext body.ss newCtx
+        loop afterBody
+      else
+        newCtx
+    loop ctx
     | _ =>
       ctx
 
@@ -194,7 +205,9 @@ def evalCallHeapTranslatedProgram (transCtx : CallHeapTranslationContext) (stmts
   evalProgramWithContext stmts evalCtx
 
 -- JSON output function with TranslationContext (matching MIDI pattern)
-def runCallHeapAndShowJSONWithTranslation (transCtx : CallHeapTranslationContext) (stmts : List CallHeapStrataStatement) : IO Unit := do
+def runCallHeapAndShowJSONWithTranslation (transCtx : CallHeapTranslationContext)
+    (stmts : List CallHeapStrataStatement)
+    (visibleVars : Option (Std.HashSet String) := none) : IO Unit := do
   let finalContext := evalCallHeapTranslatedProgram transCtx stmts
   let finalState := finalContext.hstate
 
@@ -221,8 +234,12 @@ def runCallHeapAndShowJSONWithTranslation (transCtx : CallHeapTranslationContext
       | none => continue
     | none => continue
 
+  -- Optionally filter the visible variables to match a provided allowlist
   -- Create JSON object and output (sorted for consistency)
-  let sortedFields := jsonFields.toArray.qsort (fun a b => a.1 < b.1) |>.toList
+  let filteredFields : List (String × Lean.Json) := match visibleVars with
+    | some allowed => jsonFields.filter (fun (name, _) => allowed.contains name)
+    | none => jsonFields
+  let sortedFields := filteredFields.toArray.qsort (fun a b => a.1 < b.1) |>.toList
   let jsonObj := Lean.Json.mkObj sortedFields
   IO.println jsonObj.compress  -- Use compress for compact output like {"x": 5, "y": 15}
 

Strata/Languages/TypeScript/TS_to_Strata.lean

@@ -108,6 +108,7 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr :=
     Heap.HExpr.deferredIte guard consequent alternate
 
   | .TS_NumericLiteral n =>
+    dbg_trace s!"[DEBUG] Translating numeric literal value={n.value}, raw={n.extra.raw}, rawValue={n.extra.rawValue}"
     Heap.HExpr.int n.extra.raw.toInt!
 
   | .TS_BooleanLiteral b =>
@@ -200,7 +201,7 @@ partial def translate_statement (s: TS_Statement) (ctx : TranslationContext) : T
       (ctx, [.cmd (.set "return_value" (Heap.HExpr.int 1))])
 
   | .TS_VariableDeclaration decl =>
-    match decl.declarations.get? 0 with
+    match decl.declarations[0]? with
     | .none => panic! "VariableDeclarations should have at least one declaration"
     | .some d =>
       -- Check if this is a function call assignment
@@ -233,6 +234,7 @@ partial def translate_statement (s: TS_Statement) (ctx : TranslationContext) : T
       | .TS_Identifier id =>
         -- Handle identifier assignment: x = value
         let value := translate_expr assgn.right
+        dbg_trace s!"[DEBUG] Assignment: {id.name} = {repr value}"
         (ctx, [.cmd (.set id.name value)])
       | .TS_MemberExpression member =>
         -- Handle field assignment: obj[field] = value
@@ -280,6 +282,31 @@ partial def translate_statement (s: TS_Statement) (ctx : TranslationContext) : T
     -- For now, we'll use the then context (could be more sophisticated)
     (thenCtx, [.ite testExpr thenBlock elseBlock])
 
+  | .TS_ForStatement forStmt =>
+    -- init phase
+    let (_, initStmts) := translate_statement (.TS_VariableDeclaration forStmt.init) ctx
+    -- guard (test)
+    let guard := translate_expr forStmt.test
+    -- body (first translate loop body)
+    let (ctx1, bodyStmts) := translate_statement forStmt.body ctx
+    -- update (translate expression into statements following ExpressionStatement style)
+    let (_, updateStmts) :=
+      translate_statement (.TS_ExpressionStatement { expression := .TS_AssignmentExpression forStmt.update, start_loc := forStmt.start_loc, end_loc := forStmt.end_loc, loc:= forStmt.loc, type := "TS_AssignmentExpression" }) ctx1
+    -- assemble loop body (body + update)
+    let loopBody : Imperative.Block TSStrataExpression TSStrataCommand :=
+      { ss := bodyStmts ++ updateStmts }
+
+    -- output: init statements first, then a loop statement
+    (ctx1, initStmts ++ [.loop guard none none loopBody])
+
+  | .TS_WhileStatement whileStmt =>
+    dbg_trace s!"[DEBUG] Translating while statement at loc {whileStmt.start_loc}-{whileStmt.end_loc}"
+    dbg_trace s!"[DEBUG] While test: {repr whileStmt.test}"
+    dbg_trace s!"[DEBUG] While body: {repr whileStmt.body}"
+    let testExpr := translate_expr whileStmt.test
+    let (bodyCtx, bodyStmts) := translate_statement whileStmt.body ctx
+    let bodyBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := bodyStmts }
+    (bodyCtx, [.loop testExpr none none bodyBlock])
   | _ => panic! s!"Unimplemented statement: {repr s}"
 
 -- Translate list of TypeScript statements with context

Strata/Languages/TypeScript/js_ast.lean

@@ -203,6 +203,19 @@ mutual
     body : TS_Statement
   deriving Repr, Lean.FromJson, Lean.ToJson
 
+  structure TS_WhileStatement extends BaseNode where
+    test: TS_Expression
+    body: TS_Statement
+  deriving Repr, Lean.FromJson, Lean.ToJson
+
+  /- TODO: Add support for for(let a=0, b=0;a!=0 and b!=0;a++,b++) -/
+  structure TS_ForStatement extends BaseNode where
+    init: TS_VariableDeclaration
+    test: TS_Expression
+    update: TS_AssignmentExpression
+    body: TS_Statement
+  deriving Repr, Lean.FromJson, Lean.ToJson
+
   inductive TS_Statement where
     | TS_IfStatement : TS_IfStatement → TS_Statement
     | TS_VariableDeclaration : TS_VariableDeclaration → TS_Statement
@@ -211,6 +224,8 @@ mutual
     | TS_ThrowStatement : TS_ThrowStatement → TS_Statement
     | TS_ReturnStatement : TS_ReturnStatement → TS_Statement
     | TS_FunctionDeclaration : TS_FunctionDeclaration → TS_Statement
+    | TS_ForStatement : TS_ForStatement → TS_Statement
+    | TS_WhileStatement: TS_WhileStatement -> TS_Statement
   deriving Repr, Lean.FromJson, Lean.ToJson
 end
 

StrataTest/Languages/TypeScript/test_for.ts

@@ -0,0 +1,4 @@
+let forCounter:number = 0
+for(let i = 0; i < 5; i = i + 1) {
+    forCounter = forCounter + 1
+}

StrataTest/Languages/TypeScript/test_while.ts

@@ -0,0 +1,4 @@
+let i:number = 0;
+while (i < 1) {
+    i = 3;
+}

conformance_testing/babel_to_lean.py

@@ -241,6 +241,26 @@ def parse_throw_statement(j):
     add_missing_node_info(j, target_j)
     return target_j
 
+def parse_while_statement(j):
+    target_body = parse_statement(j['body'])
+    target_j = {
+        "test": parse_expression(j['test']),
+        "body": target_body
+    }
+    add_missing_node_info(j, target_j)
+    return target_j
+
+def parse_for_statement(j):
+    target_body = parse_statement(j['body'])
+    target_j = {
+        "init": parse_variable_declaration(j['init']),
+        "test": parse_expression(j['test']),
+        "update": parse_assignment_expression(j['update']),
+        "body": target_body
+    }
+    add_missing_node_info(j, target_j)
+    return target_j
+
 def parse_statement(j):
     match j['type']:
         case "ExpressionStatement":
@@ -265,9 +285,11 @@ def parse_statement(j):
         # case "ContinueStatement":
         # case "SwitchStatement":
         # case "TryStatement":
-        # case "WhileStatement":
+        case "WhileStatement":
+            return {"TS_WhileStatement": parse_while_statement(j)}
         # case "DoWhileStatement":
-        # case "ForStatement":
+        case "ForStatement":
+            return {"TS_ForStatement": parse_for_statement(j)}
         # case "ForInStatement":
         # case "ForOfStatement":
         # case "ClassDeclaration":

conformance_testing/failures/Languages/TypeScript/test_while.ts

@@ -0,0 +1,4 @@
+let i: number = 0;
+while (i < 5) {
+    i = i + 1;
+}