From 25704298c2e32da28d2c21bca2f57d9d8086de62 Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Wed, 24 Sep 2025 23:01:39 -0700 Subject: [PATCH 01/11] array: array initial support --- Strata/Languages/TypeScript/js_ast.lean | 5 ----- conformance_testing/babel_to_lean.py | 3 --- 2 files changed, 8 deletions(-) diff --git a/Strata/Languages/TypeScript/js_ast.lean b/Strata/Languages/TypeScript/js_ast.lean index 73568e381..fc6af2b79 100644 --- a/Strata/Languages/TypeScript/js_ast.lean +++ b/Strata/Languages/TypeScript/js_ast.lean @@ -51,11 +51,6 @@ mutual structure TS_TSArrayType extends BaseNode where elementType : TS_TSTypeKeyword deriving Repr, Lean.FromJson, Lean.ToJson - - -- TODO: Array not as a type? - -- structure TS_TSArrayType extends BaseNode where - -- elementType : TS_TSTypeKeyword - -- deriving Repr, Lean.FromJson, Lean.ToJson end structure TS_TSTypeAnnotation extends BaseNode where diff --git a/conformance_testing/babel_to_lean.py b/conformance_testing/babel_to_lean.py index eeae71e76..53793d9f3 100644 --- a/conformance_testing/babel_to_lean.py +++ b/conformance_testing/babel_to_lean.py @@ -133,9 +133,6 @@ def parse_member_expression(j): add_missing_node_info(j, target_j) return target_j - add_missing_node_info(j, target_j) - return target_j - def parse_array_expression(j): # Normalize Babel ArrayExpression: keep only non-null elements and parse each elems = [] From 9b0852fb445df3b386cf41a5d5e1c728368607fa Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Tue, 30 Sep 2025 13:42:28 -0700 Subject: [PATCH 02/11] array: add array length test, implemented array length calculations --- Strata/DL/Heap/HEval.lean | 31 +++++++++++++++++++ Strata/Languages/TypeScript/TS_to_Strata.lean | 4 +-- .../TypeScript/test_arrays_length.ts | 5 +++ 3 files changed, 38 insertions(+), 2 deletions(-) create mode 100644 StrataTest/Languages/TypeScript/test_arrays_length.ts diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index 9ff3ab2ed..89a323f29 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -156,6 +156,12 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE -- Second application to StringFieldAccess - return partially applied -- This handles str.fieldName where fieldName is a string literal evalStringFieldAccess state2 objExpr e2' + | .deferredOp "LengthAccess" _ => + -- First application to LengthAccess - return partially applied + (state2, .app (.deferredOp "LengthAccess" none) e2') + | .app (.deferredOp "LengthAccess" _) objExpr => + -- Second application to LengthAccess - evaluate + evalLengthAccess state2 objExpr e2' | .deferredOp op _ => -- First application to a deferred operation - return partially applied (state2, .app (.deferredOp op none) e2') @@ -219,6 +225,31 @@ partial def evalStringFieldAccess (state : HState) (objExpr fieldExpr : HExpr) : -- Field is not a string literal (state, .lambda (LExpr.const "error_non_literal_string_field" none)) +-- Handle length access for both strings and arrays +partial def evalLengthAccess (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr := + match fieldExpr with + | .lambda (LExpr.const key _) => + if key == "length" then + match objExpr with + | .lambda (LExpr.const s _) => + -- String length + let len := s.length + (state, .lambda (LExpr.const (toString len) (some Lambda.LMonoTy.int))) + | .address addr => + -- Array length + match state.heap.get? addr with + | some obj => + let len := obj.size + (state, .lambda (LExpr.const (toString len) (some Lambda.LMonoTy.int))) + | none => + (state, .lambda (LExpr.const "error_invalid_address" none)) + | _ => + (state, .lambda (LExpr.const "error_not_string_or_array" none)) + else + (state, .lambda (LExpr.const "error_unknown_length_property" none)) + | _ => + (state, .lambda (LExpr.const "error_non_literal_field" none)) + -- Extract a numeric field index from an expression partial def extractFieldIndex (expr : HExpr) : Option Nat := match expr with diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index 404c91635..14fd5051f 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -177,9 +177,9 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := | .TS_IdExpression id => let keyName := id.name if !e.computed && keyName == "length" then - -- String dot access: str.length + -- .length property access - use unified operation that handles both strings and arrays let keyExpr := Heap.HExpr.string keyName - Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "StringFieldAccess" none) objExpr) keyExpr + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) keyExpr else -- Dynamic field access: obj[variable] let varExpr := translate_expr (.TS_IdExpression id) diff --git a/StrataTest/Languages/TypeScript/test_arrays_length.ts b/StrataTest/Languages/TypeScript/test_arrays_length.ts new file mode 100644 index 000000000..1acf63db3 --- /dev/null +++ b/StrataTest/Languages/TypeScript/test_arrays_length.ts @@ -0,0 +1,5 @@ +let numbers: number[] = [1, 2, 3, 4, 5]; +let strings: string[] = ["hello", "world"]; + +const numLen: number = numbers.length; +const strLen: number = strings.length; \ No newline at end of file From c76048ca72a7b971a0b63eef9da310f129777c15 Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Tue, 7 Oct 2025 20:21:14 -0700 Subject: [PATCH 03/11] array: implemented field deletion and enhance call expression parsing,supported array `.push()` and `.pop()` --- Strata/DL/Heap/HEval.lean | 33 +++++ Strata/DL/Heap/HState.lean | 12 ++ Strata/Languages/TypeScript/TS_to_Strata.lean | 131 ++++++++++++++---- Strata/Languages/TypeScript/js_ast.lean | 121 ++++++++-------- .../Languages/TypeScript/test_arrays.ts | 9 +- conformance_testing/babel_to_lean.py | 2 +- 6 files changed, 220 insertions(+), 88 deletions(-) diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index 89a323f29..900148971 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -162,6 +162,13 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE | .app (.deferredOp "LengthAccess" _) objExpr => -- Second application to LengthAccess - evaluate evalLengthAccess state2 objExpr e2' + | .deferredOp "FieldDelete" _ => + -- First application to FieldDelete - return partially applied + (state2, .app (.deferredOp "FieldDelete" none) e2') + | .app (.deferredOp "FieldDelete" _) objExpr => + -- Second application to FieldDelete - now we can evaluate + -- This handles delete obj[field] where field is dynamic + evalFieldDelete state2 objExpr e2' | .deferredOp op _ => -- First application to a deferred operation - return partially applied (state2, .app (.deferredOp op none) e2') @@ -225,6 +232,32 @@ partial def evalStringFieldAccess (state : HState) (objExpr fieldExpr : HExpr) : -- Field is not a string literal (state, .lambda (LExpr.const "error_non_literal_string_field" none)) +-- Handle field deletion: delete obj[field] +partial def evalFieldDelete (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr := + -- First try to extract a numeric field index from the field expression + match extractFieldIndex fieldExpr with + | some fieldIndex => + -- We have a numeric field index, delete the field + match objExpr with + | .address addr => + -- Delete field from the object at this address + match state.deleteField addr fieldIndex with + | some newState => (newState, objExpr) -- Return the object address + | none => (state, .lambda (LExpr.const s!"error_cannot_delete_field_{fieldIndex}" none)) + | _ => + -- First evaluate the object expression to get an address + let (state1, objVal) := evalHExpr state objExpr + match objVal with + | .address addr => + match state1.deleteField addr fieldIndex with + | some newState => (newState, objVal) + | none => (state1, .lambda (LExpr.const s!"error_cannot_delete_field_{fieldIndex}" none)) + | _ => + (state1, .lambda (LExpr.const "error_invalid_address_for_delete" none)) + | none => + -- Can't extract a numeric field index, return error + (state, .lambda (LExpr.const "error_field_delete_failed" none)) + -- Handle length access for both strings and arrays partial def evalLengthAccess (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr := match fieldExpr with diff --git a/Strata/DL/Heap/HState.lean b/Strata/DL/Heap/HState.lean index 4935049fc..9bd07ebf5 100644 --- a/Strata/DL/Heap/HState.lean +++ b/Strata/DL/Heap/HState.lean @@ -161,6 +161,18 @@ def setField (state : HState) (addr : Address) (field : Nat) (value : HExpr) : O some { state with heap := newHeap } | none => none +def deleteField (state : HState) (addr : Address) (field : Nat) : Option HState := + -- Remove the field from the object's fields + -- As an example: + -- before array deletion {'0': 1, '1': 5} (delete arr[1]) + -- after array deletion {'0': 1} instead of {'0': 1, '1': None} + match state.getObject addr with + | some obj => + let newObj := obj.erase field + let newHeap := state.heap.insert addr newObj + some { state with heap := newHeap } + | none => none + -- Check if an address is valid (exists in heap) def isValidAddr (state : HState) (addr : Address) : Bool := state.heap.contains addr diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index 14fd5051f..aa5fbdd4f 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -202,9 +202,32 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := Heap.HExpr.allocSimple fields | .TS_CallExpression call => - -- Handle function calls - translate to expressions for now - -- For now, create a placeholder that will be handled during call statement processing - Heap.HExpr.lambda (.fvar s!"call_{call.callee.name}" none) + match call.callee with + | .TS_MemberExpression member => + -- Handle method calls like arr.push(x) or arr.pop() + let objExpr := translate_expr member.object + match member.property with + | .TS_IdExpression id => + match id.name with + | "push" => + -- arr.push(value) - use DynamicFieldAssign with length as index + let valueExpr := translate_expr call.arguments[0]! + let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) lengthExpr) valueExpr + | "pop" => + -- arr.pop() - read arr[arr.length - 1] + let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") + let lastIndexExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) lengthExpr) (Heap.HExpr.int 1) + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) lastIndexExpr + | methodName => + Heap.HExpr.lambda (.fvar s!"call_{methodName}" none) + | _ => + Heap.HExpr.lambda (.fvar "call_unknown_method" none) + | .TS_IdExpression id => + -- Handle function calls - translate to expressions for now + Heap.HExpr.lambda (.fvar s!"call_{id.name}" none) + | _ => + panic! s!"Unsupported call expression callee: {repr call.callee}" | .TS_FunctionExpression e => -- Translate function definition @@ -273,12 +296,47 @@ partial def translate_statement_core -- Check if this is a function call assignment match d.init with | .TS_CallExpression call => - -- Handle function call assignment: let x = func(args) - dbg_trace s!"[DEBUG] Translating TypeScript function call assignment: {d.id.name} = {call.callee.name}(...)" - let args := call.arguments.toList.map translate_expr - dbg_trace s!"[DEBUG] Function call has {args.length} arguments" - let lhs := [d.id.name] -- Left-hand side variables to store result - (ctx, [.cmd (.directCall lhs call.callee.name args)]) + match call.callee with + | .TS_IdExpression id => + dbg_trace s!"[DEBUG] Translating TypeScript function call assignment: {d.id.name} = {id.name}(...)" + let args := call.arguments.toList.map translate_expr + dbg_trace s!"[DEBUG] Function call has {args.length} arguments" + let lhs := [d.id.name] + (ctx, [.cmd (.directCall lhs id.name args)]) + | .TS_MemberExpression member => + -- Handle method call assignments like x = arr.pop() + let objExpr := translate_expr member.object + match member.property with + | .TS_IdExpression id => + match id.name with + | "pop" => + -- x = arr.pop() - read and delete + let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") + let lastIndexExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) lengthExpr) (Heap.HExpr.int 1) + let tempIndexInit := .cmd (.init "temp_pop_index" Heap.HMonoTy.int lastIndexExpr) + let tempIndexVar := Heap.HExpr.lambda (.fvar "temp_pop_index" none) + -- Read the value + let popExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) tempIndexVar + let ty := get_var_type d.id.typeAnnotation d.init + let readStmt := .cmd (.init d.id.name ty popExpr) + -- Delete the element + let deleteExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) tempIndexVar) Heap.HExpr.null + let deleteStmt := .cmd (.set "temp_delete_result" deleteExpr) + (ctx, [tempIndexInit, readStmt, deleteStmt]) + | methodName => + dbg_trace s!"[DEBUG] Translating method call assignment: {d.id.name} = obj.{methodName}(...)" + let value := translate_expr d.init + let ty := get_var_type d.id.typeAnnotation d.init + (ctx, [.cmd (.init d.id.name ty value)]) + | _ => + let value := translate_expr d.init + let ty := get_var_type d.id.typeAnnotation d.init + (ctx, [.cmd (.init d.id.name ty value)]) + | _ => + -- Fallback for other call expressions + let value := translate_expr d.init + let ty := get_var_type d.id.typeAnnotation d.init + (ctx, [.cmd (.init d.id.name ty value)]) | .TS_FunctionExpression funcExpr => -- Handle function expression assignment: let x = function(...) { ... } let funcName := d.id.name @@ -291,11 +349,10 @@ partial def translate_statement_core name := funcName, params := funcExpr.params.toList.map (·.name), body := funcBody, - returnType := none -- We'll infer this later if needed + returnType := none } let newCtx := ctx.addFunction strataFunc dbg_trace s!"[DEBUG] Added function '{funcName}' to context" - -- Initialize variable to the function reference let ty := get_var_type d.id.typeAnnotation d.init let funcRef := Heap.HExpr.lambda (.fvar funcName none) (newCtx, [.cmd (.init d.id.name ty funcRef)]) @@ -311,11 +368,10 @@ partial def translate_statement_core name := funcName, params := funcExpr.params.toList.map (·.name), body := funcBody, - returnType := none -- We'll infer this later if needed + returnType := none } let newCtx := ctx.addFunction strataFunc dbg_trace s!"[DEBUG] Added arrow function '{funcName}' to context" - -- Initialize variable to the function reference let ty := get_var_type d.id.typeAnnotation d.init let funcRef := Heap.HExpr.lambda (.fvar funcName none) (newCtx, [.cmd (.init d.id.name ty funcRef)]) @@ -328,12 +384,44 @@ partial def translate_statement_core | .TS_ExpressionStatement expr => match expr.expression with | .TS_CallExpression call => - -- Handle standalone function call - dbg_trace s!"[DEBUG] Translating TypeScript standalone function call: {call.callee.name}(...)" - let args := call.arguments.toList.map translate_expr - dbg_trace s!"[DEBUG] Function call has {args.length} arguments" - let lhs := [] -- No left-hand side for standalone calls - (ctx, [.cmd (.directCall lhs call.callee.name args)]) + match call.callee with + | .TS_MemberExpression member => + -- Handle method calls like arr.push(x) or arr.pop() + let objExpr := translate_expr member.object + match member.property with + | .TS_IdExpression id => + match id.name with + | "push" => + -- arr.push(value) - use DynamicFieldAssign + let valueExpr := translate_expr call.arguments[0]! + let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") + let pushExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) lengthExpr) valueExpr + (ctx, [.cmd (.set "temp_push_result" pushExpr)]) + | "pop" => + -- arr.pop() standalone - read and delete + let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") + let lastIndexExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) lengthExpr) (Heap.HExpr.int 1) + let tempIndexInit := .cmd (.init "temp_pop_index" Heap.HMonoTy.int lastIndexExpr) + let tempIndexVar := Heap.HExpr.lambda (.fvar "temp_pop_index" none) + -- Read the value + let popExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) tempIndexVar + let readStmt := .cmd (.set "temp_pop_result" popExpr) + -- Delete the element + let deleteExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) tempIndexVar) Heap.HExpr.null + let deleteStmt := .cmd (.set "temp_delete_result" deleteExpr) + (ctx, [tempIndexInit, readStmt, deleteStmt]) + | methodName => + dbg_trace s!"[DEBUG] Translating method call: {methodName}(...)" + (ctx, []) + | _ => (ctx, []) + | .TS_IdExpression id => + -- Handle standalone function call + dbg_trace s!"[DEBUG] Translating TypeScript standalone function call: {id.name}(...)" + let args := call.arguments.toList.map translate_expr + dbg_trace s!"[DEBUG] Function call has {args.length} arguments" + let lhs := [] -- No left-hand side for standalone calls + (ctx, [.cmd (.directCall lhs id.name args)]) + | _ => (ctx, []) | .TS_AssignmentExpression assgn => assert! assgn.operator == "=" match assgn.left with @@ -415,7 +503,6 @@ partial def translate_statement_core let fieldExpr := translate_expr member.property let assignExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) fieldExpr) valueExpr (ctx, [.cmd (.set "temp_assign_result" assignExpr)]) - --| _ => panic! s!"Unsupported assignment target: {repr assgn.left}" | .TS_FunctionExpression funcExpr => -- Handle standalone function expression (immediately invoked function expression - IIFE) let funcName := s!"__anon_func_{funcExpr.start_loc}_{funcExpr.end_loc}" @@ -714,8 +801,4 @@ def describeTSStrataStatement (stmt: TSStrataStatement) : String := | .goto label _ => s!"goto {label}" - - ---#eval translate_expr (.NumericLiteral {value := 42, extra := {raw := "42", rawValue := 42}, type := "NumericLiteral"}) - end TSStrata diff --git a/Strata/Languages/TypeScript/js_ast.lean b/Strata/Languages/TypeScript/js_ast.lean index fc6af2b79..0e7f50963 100644 --- a/Strata/Languages/TypeScript/js_ast.lean +++ b/Strata/Languages/TypeScript/js_ast.lean @@ -62,7 +62,6 @@ structure TS_Identifier extends BaseNode where typeAnnotation : Option TS_TSTypeAnnotation deriving Repr, Lean.FromJson, Lean.ToJson - structure TS_Parameter extends BaseNode where name : String typeAnnotation : TS_TSTypeAnnotation @@ -90,7 +89,49 @@ deriving Repr, Lean.FromJson, Lean.ToJson structure TS_NullLiteral extends BaseNode where deriving Repr, Lean.FromJson, Lean.ToJson +structure TS_Comment extends BaseNode where +deriving Repr, Lean.FromJson, Lean.ToJson + mutual + inductive TS_Expression where + | TS_BinaryExpression : TS_BinaryExpression → TS_Expression + | TS_ConditionalExpression : TS_ConditionalExpression → TS_Expression + | TS_LogicalExpression : TS_LogicalExpression → TS_Expression + | TS_AssignmentExpression : TS_AssignmentExpression → TS_Expression + | TS_NumericLiteral : TS_NumericLiteral → TS_Expression + | TS_BooleanLiteral : TS_BooleanLiteral → TS_Expression + | TS_StringLiteral : TS_StringLiteral → TS_Expression + | TS_NullLiteral : TS_NullLiteral → TS_Expression + | TS_IdExpression : TS_Identifier → TS_Expression + | TS_UnaryExpression: TS_UnaryExpression → TS_Expression + | TS_ObjectExpression: TS_ObjectExpression → TS_Expression + | TS_ArrayExpression: TS_ArrayExpression → TS_Expression + | TS_MemberExpression: TS_MemberExpression → TS_Expression + | TS_CallExpression: TS_CallExpression → TS_Expression + | TS_FunctionExpression: TS_FunctionExpression → TS_Expression + | TS_ArrowFunctionExpression: TS_ArrowFunctionExpression → TS_Expression + deriving Repr, Lean.FromJson, Lean.ToJson + + inductive TS_Statement where + | TS_IfStatement : TS_IfStatement → TS_Statement + | TS_VariableDeclaration : TS_VariableDeclaration → TS_Statement + | TS_ExpressionStatement : TS_ExpressionStatement → TS_Statement + | TS_BlockStatement : TS_BlockStatement → TS_Statement + | 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 + | TS_BreakStatement : TS_BreakStatement → TS_Statement + | TS_SwitchStatement : TS_SwitchStatement → TS_Statement + | TS_ContinueStatement: TS_ContinueStatement → TS_Statement + deriving Repr, Lean.FromJson, Lean.ToJson + + inductive TS_AssignmentIdentifier where + | TS_Identifier : TS_Identifier → TS_AssignmentIdentifier + | TS_MemberExpression: TS_MemberExpression → TS_AssignmentIdentifier + deriving Repr, Lean.FromJson, Lean.ToJson + structure TS_MemberExpression extends BaseNode where object: TS_Expression property: TS_Expression @@ -104,9 +145,9 @@ mutual deriving Repr, Lean.FromJson, Lean.ToJson structure TS_ConditionalExpression extends BaseNode where - test : TS_Expression - consequent : TS_Expression - alternate : TS_Expression + test : TS_Expression + consequent : TS_Expression + alternate : TS_Expression deriving Repr, Lean.FromJson, Lean.ToJson structure TS_LogicalExpression extends BaseNode where @@ -115,10 +156,6 @@ mutual right : TS_Expression deriving Repr, Lean.FromJson, Lean.ToJson - inductive TS_AssignmentIdentifier where - | TS_Identifier : TS_Identifier → TS_AssignmentIdentifier - | TS_MemberExpression: TS_MemberExpression → TS_AssignmentIdentifier - structure TS_AssignmentExpression extends BaseNode where operator: String left: TS_AssignmentIdentifier @@ -132,7 +169,6 @@ mutual structure TS_ObjectProperty extends BaseNode where method: Bool - -- Key can be any expression (NumericLiteral, StringLiteral, etc.) key: TS_Expression computed: Bool shorthand: Bool @@ -148,15 +184,11 @@ mutual deriving Repr, Lean.FromJson, Lean.ToJson structure TS_CallExpression extends BaseNode where - callee : TS_Identifier + callee : TS_Expression arguments : Array TS_Expression deriving Repr, Lean.FromJson, Lean.ToJson structure TS_FunctionExpression extends BaseNode where - -- id : TS_Identifier - -- expression : Bool - -- generator : Bool - -- async : Bool params : Array TS_Identifier body: TS_Statement deriving Repr, Lean.FromJson, Lean.ToJson @@ -166,26 +198,6 @@ mutual body: TS_Statement deriving Repr, Lean.FromJson, Lean.ToJson - inductive TS_Expression where - | TS_BinaryExpression : TS_BinaryExpression → TS_Expression - | TS_ConditionalExpression : TS_ConditionalExpression → TS_Expression - | TS_LogicalExpression : TS_LogicalExpression → TS_Expression - | TS_AssignmentExpression : TS_AssignmentExpression → TS_Expression - | TS_NumericLiteral : TS_NumericLiteral → TS_Expression - | TS_BooleanLiteral : TS_BooleanLiteral → TS_Expression - | TS_StringLiteral : TS_StringLiteral → TS_Expression - | TS_NullLiteral : TS_NullLiteral → TS_Expression - | TS_IdExpression : TS_Identifier → TS_Expression - | TS_UnaryExpression: TS_UnaryExpression → TS_Expression - | TS_ObjectExpression: TS_ObjectExpression → TS_Expression - | TS_ArrayExpression: TS_ArrayExpression → TS_Expression - | TS_MemberExpression: TS_MemberExpression → TS_Expression - | TS_CallExpression: TS_CallExpression → TS_Expression - | TS_FunctionExpression: TS_FunctionExpression → TS_Expression - | TS_ArrowFunctionExpression: TS_ArrowFunctionExpression → TS_Expression - deriving Repr, Lean.FromJson, Lean.ToJson - - structure TS_VariableDeclarator extends BaseNode where id : TS_Identifier init: TS_Expression @@ -207,11 +219,9 @@ mutual argument: TS_Expression deriving Repr, Lean.FromJson, Lean.ToJson - structure TS_BlockStatement extends BaseNode where body : Array TS_Statement directives : Array String := #[] - -- innerComments is an array of comments deriving Repr, Lean.FromJson, Lean.ToJson structure TS_IfStatement extends BaseNode where @@ -220,11 +230,8 @@ mutual alternate : Option TS_Statement deriving Repr, Lean.FromJson, Lean.ToJson - /-- A single `case` (or `default` when `test = none`) inside a switch. -/ structure TS_SwitchCase extends BaseNode where - /-- `some expr` for `case expr:`, `none` for `default:` --/ test : Option TS_Expression - /-- statements executed for this case (often end with a BreakStatement) --/ consequent : Array TS_Statement deriving Repr, Lean.FromJson, Lean.ToJson @@ -248,7 +255,6 @@ mutual label: Option TS_Identifier 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 @@ -256,36 +262,29 @@ mutual body: TS_Statement deriving Repr, Lean.FromJson, Lean.ToJson - /-- `break;` (labels optional; ESTree uses null when absent) -/ structure TS_BreakStatement extends BaseNode where label : Option TS_Identifier := none deriving Repr, Lean.FromJson, Lean.ToJson - /-- `switch (discriminant) { cases... }` -/ structure TS_SwitchStatement extends BaseNode where discriminant : TS_Expression cases : Array TS_SwitchCase deriving Repr, Lean.FromJson, Lean.ToJson - - inductive TS_Statement where - | TS_IfStatement : TS_IfStatement → TS_Statement - | TS_VariableDeclaration : TS_VariableDeclaration → TS_Statement - | TS_ExpressionStatement : TS_ExpressionStatement → TS_Statement - | TS_BlockStatement : TS_BlockStatement → TS_Statement - | 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 - | TS_BreakStatement : TS_BreakStatement → TS_Statement - | TS_SwitchStatement : TS_SwitchStatement → TS_Statement - | TS_ContinueStatement: TS_ContinueStatement -> TS_Statement - deriving Repr, Lean.FromJson, Lean.ToJson end -structure TS_Comment extends BaseNode where -deriving Repr, Lean.FromJson, Lean.ToJson - +instance : Inhabited TS_Expression where + default := .TS_NumericLiteral { + value := 0, + extra := { rawValue := 0, raw := "0" }, + type := "NumericLiteral", + start_loc := 0, + end_loc := 0, + loc := { + start_loc := { line := 0, column := 0, index := 0 }, + end_loc := { line := 0, column := 0, index := 0 }, + identifierName := none + } + } structure TS_Program extends BaseNode where sourceType : String @@ -306,8 +305,6 @@ def test_json_to_x (x: Lean.Json) : IO Unit := let e: Except String TS_Expression := Lean.FromJson.fromJson? x IO.println s!"{repr e}" --- #eval test_json_to_x example_expression - def loadJsonFile (path : System.FilePath) : IO TS_File := do let contents ← IO.FS.readFile path let json ← match Lean.Json.parse contents with diff --git a/StrataTest/Languages/TypeScript/test_arrays.ts b/StrataTest/Languages/TypeScript/test_arrays.ts index 5d1409023..071110e07 100644 --- a/StrataTest/Languages/TypeScript/test_arrays.ts +++ b/StrataTest/Languages/TypeScript/test_arrays.ts @@ -26,4 +26,11 @@ let isEqual: boolean = numbers[2] == 3 // let obj = {0: data[0], 1: data[1], 2: data[2]}; // Nested arrays -// let matrix: number[][] = [[1, 2], [3, 4]]; \ No newline at end of file +// let matrix: number[][] = [[1, 2], [3, 4]]; + +// Array Push and Pop +numbers.push(6); +let popped: number | undefined = numbers.pop(); + +// Pop empty array +empty.pop(); \ No newline at end of file diff --git a/conformance_testing/babel_to_lean.py b/conformance_testing/babel_to_lean.py index 53793d9f3..e630a3e28 100644 --- a/conformance_testing/babel_to_lean.py +++ b/conformance_testing/babel_to_lean.py @@ -78,7 +78,7 @@ def parse_conditional_expression(j): def parse_call_expression(j): target_j = { - "callee": parse_identifier(j['callee']), + "callee": parse_expression(j['callee']), "arguments": [parse_expression(arg) for arg in j['arguments']] } add_missing_node_info(j, target_j) From 0d18258e395535fbb52b6ec99a9b48c55d75f1bc Mon Sep 17 00:00:00 2001 From: ygrx532 Date: Thu, 30 Oct 2025 10:46:47 -0700 Subject: [PATCH 04/11] array: implement array slice and add unary expression support --- Strata/DL/Heap/HEval.lean | 59 +++++++++++++++++++ Strata/Languages/TypeScript/TS_to_Strata.lean | 21 +++++++ .../Languages/TypeScript/test_array_slice.ts | 5 ++ test_single_file.sh | 50 ++++++++++++++++ 4 files changed, 135 insertions(+) create mode 100644 StrataTest/Languages/TypeScript/test_array_slice.ts create mode 100644 test_single_file.sh diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index 900148971..51726c4ea 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -169,6 +169,18 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE -- Second application to FieldDelete - now we can evaluate -- This handles delete obj[field] where field is dynamic evalFieldDelete state2 objExpr e2' + + -- ArraySlice(obj, start?, end?) handling + | .deferredOp "ArraySlice" _ => + -- First application: capture the array object + (state2, .app (.deferredOp "ArraySlice" none) e2') + | .app (.deferredOp "ArraySlice" _) objExpr => + -- Second application: capture start + (state2, .app (.app (.deferredOp "ArraySlice" none) objExpr) e2') + | .app (.app (.deferredOp "ArraySlice" _) objExpr) startExpr => + -- Third application: we have obj, start, and end -> evaluate + evalArraySlice state2 objExpr startExpr e2' + | .deferredOp op _ => -- First application to a deferred operation - return partially applied (state2, .app (.deferredOp op none) e2') @@ -258,6 +270,53 @@ partial def evalFieldDelete (state : HState) (objExpr fieldExpr : HExpr) : HStat -- Can't extract a numeric field index, return error (state, .lambda (LExpr.const "error_field_delete_failed" none)) +-- Handle Array.prototype.slice semantics +partial def evalArraySlice (state : HState) (objExpr startExpr endExpr : HExpr) : HState × HExpr := + -- Ensure we have an address for the array object + let (state1, objVal) := evalHExpr state objExpr + -- Evaluate start/end arguments to simplify (handle negatives, computed exprs) + let (state2, startVal) := evalHExpr state1 startExpr + let (state3, endVal) := evalHExpr state2 endExpr + let someAddr? : Option Nat := match objVal with + | .address addr => some addr + | _ => none + match someAddr? with + | none => (state3, .lambda (LExpr.const "error_array_slice_invalid_object" none)) + | some addr => + match state3.heap.get? addr with + | none => (state3, .lambda (LExpr.const "error_array_slice_invalid_address" none)) + | some obj => + let len : Nat := obj.size + -- Helper to extract integer from Lambda const + let extractInt : HExpr → Option Int := fun e => + match e with + | .lambda (LExpr.const s _) => s.toInt? + | _ => none + let resolveIndex (arg : HExpr) (defaultVal : Int) : Nat := + let i : Int := match arg with + | .null => defaultVal + | _ => (extractInt arg).getD defaultVal + let i' : Int := if i < 0 then i + Int.ofNat len else i + let clamped : Int := + if i' < 0 then 0 + else if i' > Int.ofNat len then Int.ofNat len + else i' + Int.toNat clamped + let startIdx : Nat := resolveIndex startVal 0 + let endIdx : Nat := resolveIndex endVal (Int.ofNat len) + let finalStart := startIdx + let finalEnd := if endIdx < startIdx then startIdx else endIdx + -- Collect values in [finalStart, finalEnd) and reindex from 0 + let rec collect (j : Nat) (i : Nat) (acc : List (Nat × HExpr)) : List (Nat × HExpr) := + if i ≥ finalEnd then acc.reverse + else + match state3.getField addr i with + | some v => collect (j+1) (i+1) ((j, v) :: acc) + | none => collect j (i+1) acc + let outFields := collect 0 finalStart [] + -- Allocate a new array with these fields + evalHExpr state3 (.alloc (HMonoTy.mkObj outFields.length HMonoTy.int) outFields) + -- Handle length access for both strings and arrays partial def evalLengthAccess (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr := match fieldExpr with diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index aa5fbdd4f..4c38d6f5c 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -142,6 +142,18 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := -- Use deferred conditional instead of toLambda? checks Heap.HExpr.deferredIte guard consequent alternate + | .TS_UnaryExpression e => + match e.operator with + | "-" => + -- Numeric negation: translate as 0 - arg + let arg := translate_expr e.argument + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) (Heap.HExpr.int 0)) arg + | "!" => + -- Logical not: use Bool.Not deferred op + let arg := translate_expr e.argument + Heap.HExpr.app (Heap.HExpr.deferredOp "Bool.Not" none) arg + | op => panic! s!"Unsupported unary operator: {op}" + | .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! @@ -209,6 +221,15 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := match member.property with | .TS_IdExpression id => match id.name with + | "slice" => + -- arr.slice(start?, end?) - return a new array (deferred op) + let startArg := match call.arguments[0]? with + | some a => translate_expr a + | none => Heap.HExpr.null + let endArg := match call.arguments[1]? with + | some a => translate_expr a + | none => Heap.HExpr.null + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArraySlice" none) objExpr) startArg) endArg | "push" => -- arr.push(value) - use DynamicFieldAssign with length as index let valueExpr := translate_expr call.arguments[0]! diff --git a/StrataTest/Languages/TypeScript/test_array_slice.ts b/StrataTest/Languages/TypeScript/test_array_slice.ts new file mode 100644 index 000000000..845120a35 --- /dev/null +++ b/StrataTest/Languages/TypeScript/test_array_slice.ts @@ -0,0 +1,5 @@ +let arr: number[] = [10, 20, 30, 40, 50]; +let slicedArr1: number[] = arr.slice(1, 4); +let slicedArr2: number[] = arr.slice(2); +let slicedArr3: number[] = arr.slice(); +let slicedArr4: number[] = arr.slice(-3, -1); \ No newline at end of file diff --git a/test_single_file.sh b/test_single_file.sh new file mode 100644 index 000000000..9156acf62 --- /dev/null +++ b/test_single_file.sh @@ -0,0 +1,50 @@ +#!/bin/bash +# Complete pipeline for testing single TypeScript file with debug output +# Usage: ./test_single_file.sh + +set -e + +if [ $# -ne 1 ]; then + echo "Usage: $0 " + echo "Example: $0 StrataTest/Languages/TypeScript/test_debug_break.ts" + exit 1 +fi + +TS_FILE="$1" +BASE_NAME=$(basename "$TS_FILE" .ts) +AST_FILE="${BASE_NAME}_ast.json" +LEAN_FILE="${BASE_NAME}_lean.json" + +echo "🔍 Testing TypeScript file: $TS_FILE" +echo "📁 Working directory: $(pwd)" +echo "" + +echo "Step 1: Converting TypeScript to AST JSON..." +node conformance_testing/js_to_ast.js "$TS_FILE" > "$AST_FILE" +echo "✅ Generated: $AST_FILE" + +echo "" +echo "Step 2: Converting AST JSON to Lean-compatible JSON..." +python3 conformance_testing/babel_to_lean.py "$AST_FILE" > "$LEAN_FILE" +echo "✅ Generated: $LEAN_FILE" + +echo "" +echo "Step 3: Running through StrataTypeScriptRunner with debug output..." +echo "🔍 Debug output:" +echo "----------------------------------------" + +# Run with debug output and capture both stdout and stderr +lake exe StrataTypeScriptRunner "$LEAN_FILE" 2>&1 | grep "DEBUG" || echo "No DEBUG output found" + +echo "----------------------------------------" +echo "" +echo "Step 4: Final execution result..." +lake exe StrataTypeScriptRunner "$LEAN_FILE" 2>&1 | tail -1 + +echo "" +echo "🧹 Cleaning up temporary files..." +rm -f "$AST_FILE" "$LEAN_FILE" +echo "✅ Cleanup complete" + +echo "" +echo "🎯 Pipeline complete!" From e0a92ce1c6f89bad43482bea0fd0bb244cbda526 Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Sun, 26 Oct 2025 20:32:14 -0700 Subject: [PATCH 05/11] array: implemented `shift()` and `unshift()` with single param supported --- Strata/DL/Heap/HEval.lean | 115 ++++++++++++++---- Strata/DL/Heap/HState.lean | 21 +++- Strata/Languages/TypeScript/TS_to_Strata.lean | 92 ++++++++------ .../Languages/TypeScript/test_array_shift.ts | 20 +++ .../Languages/TypeScript/test_arrays.ts | 9 +- .../TypeScript/test_arrays_length.ts | 5 - 6 files changed, 189 insertions(+), 73 deletions(-) create mode 100644 StrataTest/Languages/TypeScript/test_array_shift.ts delete mode 100644 StrataTest/Languages/TypeScript/test_arrays_length.ts diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index 51726c4ea..7c6948420 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -181,6 +181,15 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE -- Third application: we have obj, start, and end -> evaluate evalArraySlice state2 objExpr startExpr e2' + | .deferredOp "ArrayShift" _ => + -- ArrayShift applied once - now we can evaluate + evalArrayShift state2 e2' + | .deferredOp "ArrayUnshift" _ => + -- First application to ArrayUnshift - return partially applied + (state2, .app (.deferredOp "ArrayUnshift" none) e2') + | .app (.deferredOp "ArrayUnshift" _) objExpr => + -- Second application to ArrayUnshift - now we can evaluate + evalArrayUnshift state2 objExpr e2' | .deferredOp op _ => -- First application to a deferred operation - return partially applied (state2, .app (.deferredOp op none) e2') @@ -244,6 +253,32 @@ partial def evalStringFieldAccess (state : HState) (objExpr fieldExpr : HExpr) : -- Field is not a string literal (state, .lambda (LExpr.const "error_non_literal_string_field" none)) + +-- Handle length access for both strings and arrays +partial def evalLengthAccess (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr := + match fieldExpr with + | .lambda (LExpr.const key _) => + if key == "length" then + match objExpr with + | .lambda (LExpr.const s _) => + -- String length + let len := s.length + (state, .lambda (LExpr.const (toString len) (some Lambda.LMonoTy.int))) + | .address addr => + -- Array length + match state.heap.get? addr with + | some obj => + let len := obj.size + (state, .lambda (LExpr.const (toString len) (some Lambda.LMonoTy.int))) + | none => + (state, .lambda (LExpr.const "error_invalid_address" none)) + | _ => + (state, .lambda (LExpr.const "error_not_string_or_array" none)) + else + (state, .lambda (LExpr.const "error_unknown_length_property" none)) + | _ => + (state, .lambda (LExpr.const "error_non_literal_field" none)) + -- Handle field deletion: delete obj[field] partial def evalFieldDelete (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr := -- First try to extract a numeric field index from the field expression @@ -317,30 +352,62 @@ partial def evalArraySlice (state : HState) (objExpr startExpr endExpr : HExpr) -- Allocate a new array with these fields evalHExpr state3 (.alloc (HMonoTy.mkObj outFields.length HMonoTy.int) outFields) --- Handle length access for both strings and arrays -partial def evalLengthAccess (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr := - match fieldExpr with - | .lambda (LExpr.const key _) => - if key == "length" then - match objExpr with - | .lambda (LExpr.const s _) => - -- String length - let len := s.length - (state, .lambda (LExpr.const (toString len) (some Lambda.LMonoTy.int))) - | .address addr => - -- Array length - match state.heap.get? addr with - | some obj => - let len := obj.size - (state, .lambda (LExpr.const (toString len) (some Lambda.LMonoTy.int))) - | none => - (state, .lambda (LExpr.const "error_invalid_address" none)) - | _ => - (state, .lambda (LExpr.const "error_not_string_or_array" none)) - else - (state, .lambda (LExpr.const "error_unknown_length_property" none)) + +-- Handle array shift: arr.shift() - removes first element and reindexes +partial def evalArrayShift (state : HState) (objExpr : HExpr) : HState × HExpr := + match objExpr with + | .address addr => + match state.getObject addr with + | some obj => + -- Get the value at index 0 + let firstValue := obj.get? 0 |>.getD (.lambda (LExpr.const "undefined" none)) + + -- Get all fields and shift them down by 1 + let fields := obj.toList + let shiftedFields := fields.filterMap fun (idx, value) => + if idx > 0 then some (idx - 1, value) else none + + -- Create new object with shifted fields + let newObj := Std.HashMap.ofList shiftedFields + let newHeap := state.heap.insert addr newObj + let newState := { state with heap := newHeap } + + (newState, firstValue) + | none => (state, .lambda (LExpr.const "error_invalid_address" none)) | _ => - (state, .lambda (LExpr.const "error_non_literal_field" none)) + -- Evaluate object expression first + let (state1, objVal) := evalHExpr state objExpr + evalArrayShift state1 objVal + +-- Handle array unshift: arr.unshift(value) - adds element at beginning and reindexes +partial def evalArrayUnshift (state : HState) (objExpr valueExpr : HExpr) : HState × HExpr := + match objExpr with + | .address addr => + match state.getObject addr with + | some obj => + -- First evaluate the value expression + let (state1, evaluatedValue) := evalHExpr state valueExpr + + -- Get all fields and shift them up by 1 + let fields := obj.toList + let shiftedFields := fields.map fun (idx, value) => (idx + 1, value) + + -- Add new value at index 0 + let newFields := (0, evaluatedValue) :: shiftedFields + + -- Create new object with all fields + let newObj := Std.HashMap.ofList newFields + let newHeap := state1.heap.insert addr newObj + let newState := { state1 with heap := newHeap } + + -- Return the new length + let newLength := newObj.size + (newState, .lambda (LExpr.const (toString newLength) (some Lambda.LMonoTy.int))) + | none => (state, .lambda (LExpr.const "error_invalid_address" none)) + | _ => + -- Evaluate object expression first + let (state1, objVal) := evalHExpr state objExpr + evalArrayUnshift state1 objVal valueExpr -- Extract a numeric field index from an expression partial def extractFieldIndex (expr : HExpr) : Option Nat := @@ -378,4 +445,4 @@ def allocSimple (fields : List (Nat × HExpr)) : HExpr := end HExpr -end Heap +end Heap \ No newline at end of file diff --git a/Strata/DL/Heap/HState.lean b/Strata/DL/Heap/HState.lean index 9bd07ebf5..c3a7fdee8 100644 --- a/Strata/DL/Heap/HState.lean +++ b/Strata/DL/Heap/HState.lean @@ -137,7 +137,7 @@ def getHeapVarNames (state : HState) : List String := -- Allocate a new object in the heap def alloc (state : HState) (fields : List (Nat × HExpr)) : HState × Address := let addr := state.nextAddr - let obj := Std.HashMap.ofList fields -- I think the fields need to be evaluated + let obj := Std.HashMap.ofList fields let newHeap := state.heap.insert addr obj let newState := { state with heap := newHeap, nextAddr := addr + 1 } (newState, addr) @@ -161,13 +161,11 @@ def setField (state : HState) (addr : Address) (field : Nat) (value : HExpr) : O some { state with heap := newHeap } | none => none +-- Delete a field from an object in the heap def deleteField (state : HState) (addr : Address) (field : Nat) : Option HState := - -- Remove the field from the object's fields - -- As an example: - -- before array deletion {'0': 1, '1': 5} (delete arr[1]) - -- after array deletion {'0': 1} instead of {'0': 1, '1': None} match state.getObject addr with | some obj => + -- Remove the field from the object (obj is a HashMap, use erase) let newObj := obj.erase field let newHeap := state.heap.insert addr newObj some { state with heap := newHeap } @@ -181,6 +179,17 @@ def isValidAddr (state : HState) (addr : Address) : Bool := def getAllAddrs (state : HState) : List Address := state.heap.toList.map (·.1) +-- Get the logical length of an array (highest index + 1, ignoring gaps) +def getArrayLength (state : HState) (addr : Address) : Nat := + match state.getObject addr with + | some obj => + let indices := obj.toList.map (·.1) + if indices.isEmpty then + 0 + else + indices.foldl Nat.max 0 + 1 + | none => 0 + -- Pretty printing helpers def heapToString (state : HState) : String := let entries := state.heap.toList @@ -200,4 +209,4 @@ def toString (state : HState) : String := end HState -end Heap +end Heap \ No newline at end of file diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index 4c38d6f5c..e28e5c17e 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -240,6 +240,13 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") let lastIndexExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) lengthExpr) (Heap.HExpr.int 1) Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) lastIndexExpr + | "shift" => + -- arr.shift() - deferred operation that removes first element and reindexes + Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr + | "unshift" => + -- arr.unshift(value) - deferred operation that adds to beginning and reindexes + let valueExpr := translate_expr call.arguments[0]! + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) valueExpr | methodName => Heap.HExpr.lambda (.fvar s!"call_{methodName}" none) | _ => @@ -344,6 +351,10 @@ partial def translate_statement_core let deleteExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) tempIndexVar) Heap.HExpr.null let deleteStmt := .cmd (.set "temp_delete_result" deleteExpr) (ctx, [tempIndexInit, readStmt, deleteStmt]) + | "shift" => + let shiftExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr + let ty := get_var_type d.id.typeAnnotation d.init + (ctx, [.cmd (.init d.id.name ty shiftExpr)]) | methodName => dbg_trace s!"[DEBUG] Translating method call assignment: {d.id.name} = obj.{methodName}(...)" let value := translate_expr d.init @@ -406,43 +417,52 @@ partial def translate_statement_core match expr.expression with | .TS_CallExpression call => match call.callee with - | .TS_MemberExpression member => - -- Handle method calls like arr.push(x) or arr.pop() - let objExpr := translate_expr member.object - match member.property with - | .TS_IdExpression id => - match id.name with - | "push" => - -- arr.push(value) - use DynamicFieldAssign - let valueExpr := translate_expr call.arguments[0]! - let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") - let pushExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) lengthExpr) valueExpr - (ctx, [.cmd (.set "temp_push_result" pushExpr)]) - | "pop" => - -- arr.pop() standalone - read and delete - let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") - let lastIndexExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) lengthExpr) (Heap.HExpr.int 1) - let tempIndexInit := .cmd (.init "temp_pop_index" Heap.HMonoTy.int lastIndexExpr) - let tempIndexVar := Heap.HExpr.lambda (.fvar "temp_pop_index" none) - -- Read the value - let popExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) tempIndexVar - let readStmt := .cmd (.set "temp_pop_result" popExpr) - -- Delete the element - let deleteExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) tempIndexVar) Heap.HExpr.null - let deleteStmt := .cmd (.set "temp_delete_result" deleteExpr) - (ctx, [tempIndexInit, readStmt, deleteStmt]) - | methodName => - dbg_trace s!"[DEBUG] Translating method call: {methodName}(...)" - (ctx, []) - | _ => (ctx, []) + | .TS_MemberExpression member => + -- Handle method calls like arr.push(x), arr.pop(), arr.shift(), arr.unshift(x) + let objExpr := translate_expr member.object + match member.property with | .TS_IdExpression id => - -- Handle standalone function call - dbg_trace s!"[DEBUG] Translating TypeScript standalone function call: {id.name}(...)" - let args := call.arguments.toList.map translate_expr - dbg_trace s!"[DEBUG] Function call has {args.length} arguments" - let lhs := [] -- No left-hand side for standalone calls - (ctx, [.cmd (.directCall lhs id.name args)]) + match id.name with + | "push" => + -- arr.push(value) - use DynamicFieldAssign + let valueExpr := translate_expr call.arguments[0]! + let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") + let pushExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) lengthExpr) valueExpr + (ctx, [.cmd (.set "temp_push_result" pushExpr)]) + | "pop" => + -- arr.pop() standalone - read and delete + let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") + let lastIndexExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) lengthExpr) (Heap.HExpr.int 1) + let tempIndexInit := .cmd (.init "temp_pop_index" Heap.HMonoTy.int lastIndexExpr) + let tempIndexVar := Heap.HExpr.lambda (.fvar "temp_pop_index" none) + -- Read the value + let popExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) tempIndexVar + let readStmt := .cmd (.set "temp_pop_result" popExpr) + -- Delete the element + let deleteExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "FieldDelete" none) objExpr) tempIndexVar + let deleteStmt := .cmd (.set "temp_delete_result" deleteExpr) + (ctx, [tempIndexInit, readStmt, deleteStmt]) + | "shift" => + -- arr.shift() standalone + let shiftExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr + (ctx, [.cmd (.set "temp_shift_result" shiftExpr)]) + | "unshift" => + -- arr.unshift(value) standalone + let valueExpr := translate_expr call.arguments[0]! + let unshiftExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) valueExpr + (ctx, [.cmd (.set "temp_unshift_result" unshiftExpr)]) + | methodName => + dbg_trace s!"[DEBUG] Translating method call: {methodName}(...)" + (ctx, []) | _ => (ctx, []) + | .TS_IdExpression id => + -- Handle standalone function call + dbg_trace s!"[DEBUG] Translating TypeScript standalone function call: {id.name}(...)" + let args := call.arguments.toList.map translate_expr + dbg_trace s!"[DEBUG] Function call has {args.length} arguments" + let lhs := [] -- No left-hand side for standalone calls + (ctx, [.cmd (.directCall lhs id.name args)]) + | _ => (ctx, []) | .TS_AssignmentExpression assgn => assert! assgn.operator == "=" match assgn.left with @@ -822,4 +842,4 @@ def describeTSStrataStatement (stmt: TSStrataStatement) : String := | .goto label _ => s!"goto {label}" -end TSStrata +end TSStrata \ No newline at end of file diff --git a/StrataTest/Languages/TypeScript/test_array_shift.ts b/StrataTest/Languages/TypeScript/test_array_shift.ts new file mode 100644 index 000000000..f71745617 --- /dev/null +++ b/StrataTest/Languages/TypeScript/test_array_shift.ts @@ -0,0 +1,20 @@ +let numbers1: number[] = [1, 2, 3, 4]; + +// Shift removes the first element +let shifted: number | undefined = numbers1.shift(); + +// Array after shift +// nums = [2, 3, 4] + +// Shift on empty array +let emptyArr: number[] = []; +let shiftedEmpty: number | undefined = emptyArr.shift(); + +// Unshift adds an element to the beginning +let newLen: number = numbers1.unshift(0); + +// Array after unshift +// nums = [0, 2, 3, 4] + +// Unshift multiple elements +let moreLen: number = numbers1.unshift(-2, -1); diff --git a/StrataTest/Languages/TypeScript/test_arrays.ts b/StrataTest/Languages/TypeScript/test_arrays.ts index 071110e07..b9a473da7 100644 --- a/StrataTest/Languages/TypeScript/test_arrays.ts +++ b/StrataTest/Languages/TypeScript/test_arrays.ts @@ -1,6 +1,6 @@ // Basic array literal // TODO: add assertion tests AST test + verification test (as a user) pre/post-condi -let numbers: number[] = [1, 2, 3, 4, 5]; +let numbers: number[] = [1, 2, 3, 4]; // Empty array initialization let empty: number[] = []; @@ -21,6 +21,11 @@ numbers[index] = 30; let sum: number = numbers[0] + numbers[1]; let isEqual: boolean = numbers[2] == 3 +let strings: string[] = ["hello", "world"]; + +const numLen: number = numbers.length; +const strLen: number = strings.length; + // Mixed with objects // let data: number[] = [100, 200, 300]; // let obj = {0: data[0], 1: data[1], 2: data[2]}; @@ -33,4 +38,4 @@ numbers.push(6); let popped: number | undefined = numbers.pop(); // Pop empty array -empty.pop(); \ No newline at end of file +empty.pop(); diff --git a/StrataTest/Languages/TypeScript/test_arrays_length.ts b/StrataTest/Languages/TypeScript/test_arrays_length.ts deleted file mode 100644 index 1acf63db3..000000000 --- a/StrataTest/Languages/TypeScript/test_arrays_length.ts +++ /dev/null @@ -1,5 +0,0 @@ -let numbers: number[] = [1, 2, 3, 4, 5]; -let strings: string[] = ["hello", "world"]; - -const numLen: number = numbers.length; -const strLen: number = strings.length; \ No newline at end of file From e2cc197322cec805c96dff68f10f33648f3d19c0 Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Thu, 30 Oct 2025 11:17:43 -0700 Subject: [PATCH 06/11] array: `shift()` and `unshift()` supported multiple params now --- Strata/DL/Heap/HEval.lean | 1 - Strata/Languages/TypeScript/TS_to_Strata.lean | 59 +++++++++++++------ .../Languages/TypeScript/test_array_shift.ts | 2 +- 3 files changed, 42 insertions(+), 20 deletions(-) diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index 7c6948420..54f3c5add 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -409,7 +409,6 @@ partial def evalArrayUnshift (state : HState) (objExpr valueExpr : HExpr) : HSta let (state1, objVal) := evalHExpr state objExpr evalArrayUnshift state1 objVal valueExpr --- Extract a numeric field index from an expression partial def extractFieldIndex (expr : HExpr) : Option Nat := match expr with | .lambda (LExpr.const s _) => diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index e28e5c17e..1ac13471f 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -244,9 +244,12 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := -- arr.shift() - deferred operation that removes first element and reindexes Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr | "unshift" => - -- arr.unshift(value) - deferred operation that adds to beginning and reindexes - let valueExpr := translate_expr call.arguments[0]! - Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) valueExpr + -- arr.unshift(value) - single value only in expression context + if call.arguments.size != 1 then + panic! s!"unshift with multiple arguments in expression context not supported" + else + let valueExpr := translate_expr call.arguments[0]! + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) valueExpr | methodName => Heap.HExpr.lambda (.fvar s!"call_{methodName}" none) | _ => @@ -321,40 +324,55 @@ partial def translate_statement_core match decl.declarations[0]? with | .none => panic! "VariableDeclarations should have at least one declaration" | .some d => - -- Check if this is a function call assignment match d.init with | .TS_CallExpression call => match call.callee with | .TS_IdExpression id => dbg_trace s!"[DEBUG] Translating TypeScript function call assignment: {d.id.name} = {id.name}(...)" let args := call.arguments.toList.map translate_expr - dbg_trace s!"[DEBUG] Function call has {args.length} arguments" let lhs := [d.id.name] (ctx, [.cmd (.directCall lhs id.name args)]) | .TS_MemberExpression member => - -- Handle method call assignments like x = arr.pop() let objExpr := translate_expr member.object match member.property with | .TS_IdExpression id => match id.name with | "pop" => - -- x = arr.pop() - read and delete + -- Handle Array.pop() method let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") let lastIndexExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) lengthExpr) (Heap.HExpr.int 1) let tempIndexInit := .cmd (.init "temp_pop_index" Heap.HMonoTy.int lastIndexExpr) let tempIndexVar := Heap.HExpr.lambda (.fvar "temp_pop_index" none) - -- Read the value - let popExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) tempIndexVar + let valueExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) tempIndexVar let ty := get_var_type d.id.typeAnnotation d.init - let readStmt := .cmd (.init d.id.name ty popExpr) - -- Delete the element - let deleteExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) tempIndexVar) Heap.HExpr.null + let initStmt := .cmd (.init d.id.name ty valueExpr) + let deleteExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "FieldDelete" none) objExpr) tempIndexVar) Heap.HExpr.null let deleteStmt := .cmd (.set "temp_delete_result" deleteExpr) - (ctx, [tempIndexInit, readStmt, deleteStmt]) + (ctx, [tempIndexInit, initStmt, deleteStmt]) | "shift" => + -- Handle Array.shift() method let shiftExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr let ty := get_var_type d.id.typeAnnotation d.init (ctx, [.cmd (.init d.id.name ty shiftExpr)]) + | "unshift" => + -- Handle Array.unshift() with multiple arguments + let valueExprs := call.arguments.toList.map translate_expr + if valueExprs.isEmpty then + let value := translate_expr d.init + let ty := get_var_type d.id.typeAnnotation d.init + (ctx, [.cmd (.init d.id.name ty value)]) + else + let reversed := valueExprs.reverse + let allButLast := reversed.dropLast + let lastValue := reversed.getLast! + let tempStmts := allButLast.map (fun valueExpr => + let unshiftExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) valueExpr + (.cmd (.set "temp_unshift_result" unshiftExpr) : TSStrataStatement) + ) + let lastUnshiftExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) lastValue + let ty := Heap.HMonoTy.int + let initStmt := .cmd (.init d.id.name ty lastUnshiftExpr) + (ctx, tempStmts ++ [initStmt]) | methodName => dbg_trace s!"[DEBUG] Translating method call assignment: {d.id.name} = obj.{methodName}(...)" let value := translate_expr d.init @@ -365,10 +383,10 @@ partial def translate_statement_core let ty := get_var_type d.id.typeAnnotation d.init (ctx, [.cmd (.init d.id.name ty value)]) | _ => - -- Fallback for other call expressions let value := translate_expr d.init let ty := get_var_type d.id.typeAnnotation d.init (ctx, [.cmd (.init d.id.name ty value)]) + | .TS_FunctionExpression funcExpr => -- Handle function expression assignment: let x = function(...) { ... } let funcName := d.id.name @@ -388,6 +406,7 @@ partial def translate_statement_core let ty := get_var_type d.id.typeAnnotation d.init let funcRef := Heap.HExpr.lambda (.fvar funcName none) (newCtx, [.cmd (.init d.id.name ty funcRef)]) + | .TS_ArrowFunctionExpression funcExpr => -- Handle arrow function assignment: let x = (args) => { ... } let funcName := d.id.name @@ -407,6 +426,7 @@ partial def translate_statement_core let ty := get_var_type d.id.typeAnnotation d.init let funcRef := Heap.HExpr.lambda (.fvar funcName none) (newCtx, [.cmd (.init d.id.name ty funcRef)]) + | _ => -- Handle simple variable declaration: let x = value let value := translate_expr d.init @@ -447,10 +467,13 @@ partial def translate_statement_core let shiftExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr (ctx, [.cmd (.set "temp_shift_result" shiftExpr)]) | "unshift" => - -- arr.unshift(value) standalone - let valueExpr := translate_expr call.arguments[0]! - let unshiftExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) valueExpr - (ctx, [.cmd (.set "temp_unshift_result" unshiftExpr)]) + -- arr.unshift(val1, val2, ...) - expand to multiple single unshift statements + let valueExprs := call.arguments.toList.map translate_expr + let statements := valueExprs.reverse.map (fun valueExpr => + let unshiftExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) valueExpr + (.cmd (.set "temp_unshift_result" unshiftExpr) : TSStrataStatement) + ) + (ctx, statements) | methodName => dbg_trace s!"[DEBUG] Translating method call: {methodName}(...)" (ctx, []) diff --git a/StrataTest/Languages/TypeScript/test_array_shift.ts b/StrataTest/Languages/TypeScript/test_array_shift.ts index f71745617..cc761cd7d 100644 --- a/StrataTest/Languages/TypeScript/test_array_shift.ts +++ b/StrataTest/Languages/TypeScript/test_array_shift.ts @@ -17,4 +17,4 @@ let newLen: number = numbers1.unshift(0); // nums = [0, 2, 3, 4] // Unshift multiple elements -let moreLen: number = numbers1.unshift(-2, -1); +let moreLen: number = numbers1.unshift(2, 1) From a97e0ff0536cc004617d15c2a02a01822b492e8c Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Mon, 3 Nov 2025 00:13:31 -0800 Subject: [PATCH 07/11] misc: added support for unary operators in expression parsing --- Strata/Languages/TypeScript/TS_to_Strata.lean | 14 ++++++ .../Languages/TypeScript/test_array_shift.ts | 2 +- test_single_file.sh | 50 ------------------- 3 files changed, 15 insertions(+), 51 deletions(-) delete mode 100644 test_single_file.sh diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index 1ac13471f..647cee850 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -213,6 +213,20 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := -- Use allocSimple which handles the object type automatically Heap.HExpr.allocSimple fields + | .TS_UnaryExpression e => + let arg := translate_expr e.argument + match e.operator with + | "-" => + -- Unary minus: -x + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) (Heap.HExpr.int 0)) arg + | "+" => + -- Unary plus: +x (just return the argument) + arg + | "!" => + -- Logical NOT: !x + Heap.HExpr.app (Heap.HExpr.deferredOp "Bool.Not" none) arg + | _ => panic! s!"Unsupported unary operator: {e.operator}" + | .TS_CallExpression call => match call.callee with | .TS_MemberExpression member => diff --git a/StrataTest/Languages/TypeScript/test_array_shift.ts b/StrataTest/Languages/TypeScript/test_array_shift.ts index cc761cd7d..532df7f1f 100644 --- a/StrataTest/Languages/TypeScript/test_array_shift.ts +++ b/StrataTest/Languages/TypeScript/test_array_shift.ts @@ -17,4 +17,4 @@ let newLen: number = numbers1.unshift(0); // nums = [0, 2, 3, 4] // Unshift multiple elements -let moreLen: number = numbers1.unshift(2, 1) +let moreLen: number = numbers1.unshift(-2, 1) diff --git a/test_single_file.sh b/test_single_file.sh deleted file mode 100644 index 9156acf62..000000000 --- a/test_single_file.sh +++ /dev/null @@ -1,50 +0,0 @@ -#!/bin/bash -# Complete pipeline for testing single TypeScript file with debug output -# Usage: ./test_single_file.sh - -set -e - -if [ $# -ne 1 ]; then - echo "Usage: $0 " - echo "Example: $0 StrataTest/Languages/TypeScript/test_debug_break.ts" - exit 1 -fi - -TS_FILE="$1" -BASE_NAME=$(basename "$TS_FILE" .ts) -AST_FILE="${BASE_NAME}_ast.json" -LEAN_FILE="${BASE_NAME}_lean.json" - -echo "🔍 Testing TypeScript file: $TS_FILE" -echo "📁 Working directory: $(pwd)" -echo "" - -echo "Step 1: Converting TypeScript to AST JSON..." -node conformance_testing/js_to_ast.js "$TS_FILE" > "$AST_FILE" -echo "✅ Generated: $AST_FILE" - -echo "" -echo "Step 2: Converting AST JSON to Lean-compatible JSON..." -python3 conformance_testing/babel_to_lean.py "$AST_FILE" > "$LEAN_FILE" -echo "✅ Generated: $LEAN_FILE" - -echo "" -echo "Step 3: Running through StrataTypeScriptRunner with debug output..." -echo "🔍 Debug output:" -echo "----------------------------------------" - -# Run with debug output and capture both stdout and stderr -lake exe StrataTypeScriptRunner "$LEAN_FILE" 2>&1 | grep "DEBUG" || echo "No DEBUG output found" - -echo "----------------------------------------" -echo "" -echo "Step 4: Final execution result..." -lake exe StrataTypeScriptRunner "$LEAN_FILE" 2>&1 | tail -1 - -echo "" -echo "🧹 Cleaning up temporary files..." -rm -f "$AST_FILE" "$LEAN_FILE" -echo "✅ Cleanup complete" - -echo "" -echo "🎯 Pipeline complete!" From 703ac69f04a7a21c849fa82197a7f1ecf0a4423b Mon Sep 17 00:00:00 2001 From: ygrx532 Date: Thu, 6 Nov 2025 00:16:58 -0800 Subject: [PATCH 08/11] array: support array `concat()` --- Strata/DL/Heap/HEval.lean | 38 +++++++++++++++++++ Strata/Languages/TypeScript/TS_to_Strata.lean | 11 ++++++ .../Languages/TypeScript/test_array_concat.ts | 4 ++ 3 files changed, 53 insertions(+) create mode 100644 StrataTest/Languages/TypeScript/test_array_concat.ts diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index 54f3c5add..cd761d16c 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -190,6 +190,12 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE | .app (.deferredOp "ArrayUnshift" _) objExpr => -- Second application to ArrayUnshift - now we can evaluate evalArrayUnshift state2 objExpr e2' + | .deferredOp "ArrayConcat" _ => + -- First application to ArrayConcat - return partially applied + (state2, .app (.deferredOp "ArrayConcat" none) e2') + | .app (.deferredOp "ArrayConcat" _) arr1Expr => + -- Second application to ArrayConcat - now we can evaluate + evalArrayConcat state2 arr1Expr e2' | .deferredOp op _ => -- First application to a deferred operation - return partially applied (state2, .app (.deferredOp op none) e2') @@ -409,6 +415,38 @@ partial def evalArrayUnshift (state : HState) (objExpr valueExpr : HExpr) : HSta let (state1, objVal) := evalHExpr state objExpr evalArrayUnshift state1 objVal valueExpr +-- Handle array concat: arr1.concat(arr2) - concatenates two arrays, returns new array +partial def evalArrayConcat (state : HState) (arr1Expr arr2Expr : HExpr) : HState × HExpr := + -- First evaluate both array expressions to get addresses + let (state1, arr1Val) := evalHExpr state arr1Expr + let (state2, arr2Val) := evalHExpr state1 arr2Expr + + match arr1Val, arr2Val with + | .address addr1, .address addr2 => + match state2.getObject addr1, state2.getObject addr2 with + | some obj1, some obj2 => + -- Get all fields from arr1 + let arr1Fields := obj1.toList + + -- Calculate the length of arr1 (highest index + 1) + let arr1Length := if arr1Fields.isEmpty then 0 else + (arr1Fields.map (·.1)).foldl Nat.max 0 + 1 + + -- Get all fields from arr2 and shift their indices by arr1Length + let arr2Fields := obj2.toList.map fun (idx, value) => (idx + arr1Length, value) + + -- Combine all fields: arr1's fields followed by shifted arr2's fields + let combinedFields := arr1Fields ++ arr2Fields + + -- Allocate a new array with the combined fields + let (newState, newAddr) := state2.alloc combinedFields + + (newState, .address newAddr) + | _, _ => (state2, .lambda (LExpr.const "error_invalid_address" none)) + | _, _ => + -- One or both expressions didn't evaluate to addresses + (state2, .lambda (LExpr.const "error_invalid_array_for_concat" none)) + partial def extractFieldIndex (expr : HExpr) : Option Nat := match expr with | .lambda (LExpr.const s _) => diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index 647cee850..a44aaedf9 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -264,6 +264,17 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := else let valueExpr := translate_expr call.arguments[0]! Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) valueExpr + | "concat" => + -- arr.concat(arr2, arr3, ...) - concatenate arrays, returns new array + let argExprs := call.arguments.toList.map translate_expr + if argExprs.isEmpty then + -- concat() with no arguments returns a copy of the original array + objExpr + else + -- Chain concat operations: concat(arr1, arr2, arr3) = concat(concat(arr1, arr2), arr3) + argExprs.foldl (fun acc argExpr => + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayConcat" none) acc) argExpr + ) objExpr | methodName => Heap.HExpr.lambda (.fvar s!"call_{methodName}" none) | _ => diff --git a/StrataTest/Languages/TypeScript/test_array_concat.ts b/StrataTest/Languages/TypeScript/test_array_concat.ts new file mode 100644 index 000000000..7221bc310 --- /dev/null +++ b/StrataTest/Languages/TypeScript/test_array_concat.ts @@ -0,0 +1,4 @@ +let arr1 = [1, 2, 3]; +let arr2 = [4, 5, 6]; + +let combinedArr = arr1.concat(arr2); \ No newline at end of file From f9c58d3eaf3ab5b5b9ce0f04e4b68d967fdfb614 Mon Sep 17 00:00:00 2001 From: ygrx532 Date: Sun, 9 Nov 2025 21:57:59 -0800 Subject: [PATCH 09/11] array: supported array `join()` --- Strata/DL/Heap/HEval.lean | 52 +++++++++++++++++++ Strata/Languages/TypeScript/TS_to_Strata.lean | 21 +++----- .../Languages/TypeScript/test_array_join.ts | 7 +++ 3 files changed, 66 insertions(+), 14 deletions(-) create mode 100644 StrataTest/Languages/TypeScript/test_array_join.ts diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index cd761d16c..b712c0c7f 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -196,6 +196,12 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE | .app (.deferredOp "ArrayConcat" _) arr1Expr => -- Second application to ArrayConcat - now we can evaluate evalArrayConcat state2 arr1Expr e2' + | .deferredOp "ArrayJoin" _ => + -- First application to ArrayJoin - return partially applied + (state2, .app (.deferredOp "ArrayJoin" none) e2') + | .app (.deferredOp "ArrayJoin" _) arrExpr => + -- Second application to ArrayJoin - now we can evaluate + evalArrayJoin state2 arrExpr e2' | .deferredOp op _ => -- First application to a deferred operation - return partially applied (state2, .app (.deferredOp op none) e2') @@ -447,6 +453,52 @@ partial def evalArrayConcat (state : HState) (arr1Expr arr2Expr : HExpr) : HStat -- One or both expressions didn't evaluate to addresses (state2, .lambda (LExpr.const "error_invalid_array_for_concat" none)) +-- Handle array join: arr.join(separator?) - joins elements into a string +partial def evalArrayJoin (state : HState) (arrExpr sepExpr : HExpr) : HState × HExpr := + let (state1, arrVal) := evalHExpr state arrExpr + let (state2, sepVal) := evalHExpr state1 sepExpr + let formatToString : Std.Format → String := fun fmt => fmt.pretty 80 + let separator : String := + match sepVal with + | .null => "," + | .lambda (LExpr.const s _) => s + | _ => + match sepVal.toLambda? with + | some (LExpr.const s _) => s + | _ => formatToString (repr sepVal) + match arrVal with + | .address addr => + match state2.getObject addr with + | some _ => + let len := state2.getArrayLength addr + let stringOf : HExpr → String := fun value => + match value with + | .lambda (LExpr.const s _) => s + | .lambda _ => formatToString (repr value) + | .address _ => "[object Object]" + | .null => "" + | _ => formatToString (repr value) + let rec collect (idx : Nat) (st : HState) (acc : List String) : HState × List String := + if idx ≥ len then (st, acc.reverse) + else + match st.getField addr idx with + | some rawVal => + let (st1, evaluated) := evalHExpr st rawVal + let str := stringOf evaluated + collect (idx + 1) st1 (str :: acc) + | none => + -- Sparse slot - treated as empty string but still contributes separator + collect (idx + 1) st ("" :: acc) + let (stateFinal, parts) := collect 0 state2 [] + let resultString := + match parts with + | [] => "" + | _ => String.intercalate separator parts + (stateFinal, Heap.HExpr.string resultString) + | none => (state2, .lambda (LExpr.const "error_invalid_address" none)) + | _ => + (state2, .lambda (LExpr.const "error_invalid_array_for_join" none)) + partial def extractFieldIndex (expr : HExpr) : Option Nat := match expr with | .lambda (LExpr.const s _) => diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index a44aaedf9..9fa6a4c70 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -213,20 +213,6 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := -- Use allocSimple which handles the object type automatically Heap.HExpr.allocSimple fields - | .TS_UnaryExpression e => - let arg := translate_expr e.argument - match e.operator with - | "-" => - -- Unary minus: -x - Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) (Heap.HExpr.int 0)) arg - | "+" => - -- Unary plus: +x (just return the argument) - arg - | "!" => - -- Logical NOT: !x - Heap.HExpr.app (Heap.HExpr.deferredOp "Bool.Not" none) arg - | _ => panic! s!"Unsupported unary operator: {e.operator}" - | .TS_CallExpression call => match call.callee with | .TS_MemberExpression member => @@ -275,6 +261,13 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := argExprs.foldl (fun acc argExpr => Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayConcat" none) acc) argExpr ) objExpr + | "join" => + -- arr.join(separator?) - join elements into a string + let separator := + match call.arguments[0]? with + | some sepExpr => translate_expr sepExpr + | none => Heap.HExpr.string "," + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayJoin" none) objExpr) separator | methodName => Heap.HExpr.lambda (.fvar s!"call_{methodName}" none) | _ => diff --git a/StrataTest/Languages/TypeScript/test_array_join.ts b/StrataTest/Languages/TypeScript/test_array_join.ts new file mode 100644 index 000000000..a6795887a --- /dev/null +++ b/StrataTest/Languages/TypeScript/test_array_join.ts @@ -0,0 +1,7 @@ +let arr_to_join: string[] = ["Hello", "world", "from", "Strata"]; +let joined_str1: string = arr_to_join.join(); +let joined_str2: string = arr_to_join.join(" "); + +let number_arr: number[] = [1, 2, 3, 4, 5]; +let joined_numbers: string = number_arr.join(); +let joined_numbers_with_dash: string = number_arr.join("-"); From bb2dfaf3ea0eecab1dc24c6f41c9fb21520935ca Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Mon, 17 Nov 2025 01:23:26 -0800 Subject: [PATCH 10/11] support for-in, added test --- Strata/DL/Heap/HEval.lean | 24 ++ Strata/Languages/TypeScript/TS_to_Strata.lean | 260 +++++++++++------- Strata/Languages/TypeScript/js_ast.lean | 7 + .../Languages/TypeScript/test_for_in.ts | 5 + conformance_testing/babel_to_lean.py | 39 ++- 5 files changed, 229 insertions(+), 106 deletions(-) create mode 100644 StrataTest/Languages/TypeScript/test_for_in.ts diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index b712c0c7f..9a61b9d4f 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -184,6 +184,9 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE | .deferredOp "ArrayShift" _ => -- ArrayShift applied once - now we can evaluate evalArrayShift state2 e2' + | .deferredOp "ObjectKeys" _ => + -- ObjectKeys applied once - now we can evaluate + evalObjectKeys state2 e2' | .deferredOp "ArrayUnshift" _ => -- First application to ArrayUnshift - return partially applied (state2, .app (.deferredOp "ArrayUnshift" none) e2') @@ -391,6 +394,27 @@ partial def evalArrayShift (state : HState) (objExpr : HExpr) : HState × HExpr let (state1, objVal) := evalHExpr state objExpr evalArrayShift state1 objVal +partial def evalObjectKeys (state : HState) (objExpr : HExpr) : HState × HExpr := + match objExpr with + | .address addr => + match state.getObject addr with + | some obj => + -- Get all field indices and sort them + let indices := obj.toList.map (·.1) |>.toArray.qsort (· < ·) + + -- Create array with indices as integer values + let keyFields := indices.toList.mapIdx fun arrayIdx fieldIdx => + (arrayIdx, .lambda (LExpr.const (toString fieldIdx) (some Lambda.LMonoTy.int))) + + -- Allocate new array with the keys + let (newState, newAddr) := state.alloc keyFields + (newState, .address newAddr) + | none => (state, .lambda (LExpr.const "error_invalid_address" none)) + | _ => + -- Evaluate object expression first + let (state1, objVal) := evalHExpr state objExpr + evalObjectKeys state1 objVal + -- Handle array unshift: arr.unshift(value) - adds element at beginning and reindexes partial def evalArrayUnshift (state : HState) (objExpr valueExpr : HExpr) : HState × HExpr := match objExpr with diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index 9fa6a4c70..b8c193e53 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -726,115 +726,165 @@ partial def translate_statement_core let bodyBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := bodyStmts } (bodyCtx, [ initBreakFlag, .loop combinedCondition none none bodyBlock ]) - | .TS_ForStatement forStmt => - dbg_trace s!"[DEBUG] Translating for statement at loc {forStmt.start_loc}-{forStmt.end_loc}" - - let continueLabel := s!"for_continue_{forStmt.start_loc}" - let breakLabel := s!"for_break_{forStmt.start_loc}" - let breakFlagVar := s!"for_break_flag_{forStmt.start_loc}" - - -- Initialize break flag to false - let initBreakFlag : TSStrataStatement := .cmd (.init breakFlagVar Heap.HMonoTy.bool Heap.HExpr.false) - - -- init phase - let (_, initStmts) := translate_statement_core (.TS_VariableDeclaration forStmt.init) ctx - -- guard (test) - let guard := translate_expr forStmt.test - -- body (first translate loop body with break support) - let (ctx1, bodyStmts) := - translate_statement_core forStmt.body ctx - { continueLabel? := some continueLabel, breakLabel? := some breakLabel, breakFlagVar? := some breakFlagVar } - -- update (translate expression into statements following ExpressionStatement style) - let (_, updateStmts) := - translate_statement_core - (.TS_ExpressionStatement { - expression := .TS_AssignmentExpression forStmt.update, - start_loc := forStmt.start_loc, - end_loc := forStmt.end_loc, - loc := forStmt.loc, - type := "TS_AssignmentExpression" - }) ctx1 - - -- Modify loop condition to include break flag check: (original_condition && !break_flag) - let breakFlagExpr := Heap.HExpr.lambda (.fvar breakFlagVar none) - let combinedCondition := Heap.HExpr.deferredIte breakFlagExpr Heap.HExpr.false guard - - -- assemble loop body (body + update) - let loopBody : Imperative.Block TSStrataExpression TSStrataCommand := - { ss := bodyStmts ++ updateStmts } - - -- output: init break flag, init statements, then a loop statement - (ctx1, [initBreakFlag] ++ initStmts ++ [ .loop combinedCondition none none loopBody]) - - | .TS_SwitchStatement switchStmt => - -- Handle switch statement: switch discriminant { cases } - - -- Process all cases in their original order, separating regular from default - let allCases := switchStmt.cases.toList - let (regularCaseStmts, defaultStmts) := allCases.foldl (fun (regCases, defStmts) case => - match case.test with - | some expr => - -- Regular case - let discrimExpr := translate_expr switchStmt.discriminant - let caseValue := translate_expr expr - let testExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Eq" none) discrimExpr) caseValue - let (caseCtx, stmts) := case.consequent.foldl (fun (accCtx, accStmts) stmt => - let (newCtx, newStmts) := translate_statement_core stmt accCtx - (newCtx, accStmts ++ newStmts)) (ctx, []) - (regCases ++ [(testExpr, stmts)], defStmts) - | none => - -- Default case - let (defaultCtx, stmts) := case.consequent.foldl (fun (accCtx, accStmts) stmt => - let (newCtx, newStmts) := translate_statement_core stmt accCtx - (newCtx, accStmts ++ newStmts)) (ctx, []) - (regCases, stmts) - ) ([], []) - - -- Build nested if-then-else structure for regular cases - let rec build_cases (cases: List (Heap.HExpr × List TSStrataStatement)) (defaultStmts: List TSStrataStatement) : TSStrataStatement := - match cases with - | [] => - -- No regular cases, just execute default if it exists - let defaultBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := defaultStmts } - .block "default" defaultBlock - | [(test, stmts)] => - let thenBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := stmts } - let elseBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := defaultStmts } - .ite test thenBlock elseBlock - | (test, stmts) :: rest => - let thenBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := stmts } - let elseBlock := build_cases rest defaultStmts - let elseBlockWrapped : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [elseBlock] } - .ite test thenBlock elseBlockWrapped - - let switchStructure := build_cases regularCaseStmts defaultStmts - (ctx, [switchStructure]) - - | .TS_ContinueStatement cont => + | .TS_ForInStatement forInStmt => + dbg_trace s!"[DEBUG] Translating for-in statement at loc {forInStmt.start_loc}-{forInStmt.end_loc}" + + let continueLabel := s!"forin_continue_{forInStmt.start_loc}" + let breakLabel := s!"forin_break_{forInStmt.start_loc}" + let breakFlagVar := s!"forin_break_flag_{forInStmt.start_loc}" + + let keyVarName := match forInStmt.left.declarations[0]? with + | some decl => decl.id.name + | none => panic! "for-in must have loop variable" + + let objExpr := translate_expr forInStmt.right + + let keysVar := s!"__keys_{forInStmt.start_loc}" + let indexVar := s!"__index_{forInStmt.start_loc}" + let lengthVar := s!"__length_{forInStmt.start_loc}" + + let keysExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ObjectKeys" none) objExpr + let initKeys := .cmd (.init keysVar Heap.HMonoTy.addr keysExpr) + + let keysVarExpr := Heap.HExpr.lambda (.fvar keysVar none) + let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) keysVarExpr) (Heap.HExpr.string "length") + let initLength := .cmd (.init lengthVar Heap.HMonoTy.int lengthExpr) + + let initIndex := .cmd (.init indexVar Heap.HMonoTy.int (Heap.HExpr.int 0)) + + let initBreakFlag := .cmd (.init breakFlagVar Heap.HMonoTy.bool Heap.HExpr.false) + + let indexVarExpr := Heap.HExpr.lambda (.fvar indexVar none) + let lengthVarExpr := Heap.HExpr.lambda (.fvar lengthVar none) + let indexCheck := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Lt" none) indexVarExpr) lengthVarExpr + let breakFlagExpr := Heap.HExpr.lambda (.fvar breakFlagVar none) + let guard := Heap.HExpr.deferredIte breakFlagExpr Heap.HExpr.false indexCheck + + let getCurrentKey := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) keysVarExpr) indexVarExpr + let setKeyVar := .cmd (.init keyVarName Heap.HMonoTy.int getCurrentKey) + + let (bodyCtx, userBodyStmts) := translate_statement_core forInStmt.body ctx + { continueLabel? := some continueLabel, + breakLabel? := some breakLabel, + breakFlagVar? := some breakFlagVar } + + let incrementExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) indexVarExpr) (Heap.HExpr.int 1) + let incrementIndex := .cmd (.set indexVar incrementExpr) + + let loopBodyStmts := [setKeyVar] ++ userBodyStmts ++ [incrementIndex] + let bodyBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := loopBodyStmts } + + (bodyCtx, [initBreakFlag, initKeys, initLength, initIndex, .loop guard none none bodyBlock]) + + | .TS_ForStatement forStmt => + dbg_trace s!"[DEBUG] Translating for statement at loc {forStmt.start_loc}-{forStmt.end_loc}" + + let continueLabel := s!"for_continue_{forStmt.start_loc}" + let breakLabel := s!"for_break_{forStmt.start_loc}" + let breakFlagVar := s!"for_break_flag_{forStmt.start_loc}" + + -- Initialize break flag to false + let initBreakFlag : TSStrataStatement := .cmd (.init breakFlagVar Heap.HMonoTy.bool Heap.HExpr.false) + + -- init phase + let (_, initStmts) := translate_statement_core (.TS_VariableDeclaration forStmt.init) ctx + -- guard (test) + let guard := translate_expr forStmt.test + -- body (first translate loop body with break support) + let (ctx1, bodyStmts) := + translate_statement_core forStmt.body ctx + { continueLabel? := some continueLabel, breakLabel? := some breakLabel, breakFlagVar? := some breakFlagVar } + -- update (translate expression into statements following ExpressionStatement style) + let (_, updateStmts) := + translate_statement_core + (.TS_ExpressionStatement { + expression := .TS_AssignmentExpression forStmt.update, + start_loc := forStmt.start_loc, + end_loc := forStmt.end_loc, + loc := forStmt.loc, + type := "TS_AssignmentExpression" + }) ctx1 + + -- Modify loop condition to include break flag check: (original_condition && !break_flag) + let breakFlagExpr := Heap.HExpr.lambda (.fvar breakFlagVar none) + let combinedCondition := Heap.HExpr.deferredIte breakFlagExpr Heap.HExpr.false guard + + -- assemble loop body (body + update) + let loopBody : Imperative.Block TSStrataExpression TSStrataCommand := + { ss := bodyStmts ++ updateStmts } + + -- output: init break flag, init statements, then a loop statement + (ctx1, [initBreakFlag] ++ initStmts ++ [ .loop combinedCondition none none loopBody]) + + | .TS_SwitchStatement switchStmt => + -- Handle switch statement: switch discriminant { cases } + + -- Process all cases in their original order, separating regular from default + let allCases := switchStmt.cases.toList + let (regularCaseStmts, defaultStmts) := allCases.foldl (fun (regCases, defStmts) case => + match case.test with + | some expr => + -- Regular case + let discrimExpr := translate_expr switchStmt.discriminant + let caseValue := translate_expr expr + let testExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Eq" none) discrimExpr) caseValue + let (caseCtx, stmts) := case.consequent.foldl (fun (accCtx, accStmts) stmt => + let (newCtx, newStmts) := translate_statement_core stmt accCtx + (newCtx, accStmts ++ newStmts)) (ctx, []) + (regCases ++ [(testExpr, stmts)], defStmts) + | none => + -- Default case + let (defaultCtx, stmts) := case.consequent.foldl (fun (accCtx, accStmts) stmt => + let (newCtx, newStmts) := translate_statement_core stmt accCtx + (newCtx, accStmts ++ newStmts)) (ctx, []) + (regCases, stmts) + ) ([], []) + + -- Build nested if-then-else structure for regular cases + let rec build_cases (cases: List (Heap.HExpr × List TSStrataStatement)) (defaultStmts: List TSStrataStatement) : TSStrataStatement := + match cases with + | [] => + -- No regular cases, just execute default if it exists + let defaultBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := defaultStmts } + .block "default" defaultBlock + | [(test, stmts)] => + let thenBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := stmts } + let elseBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := defaultStmts } + .ite test thenBlock elseBlock + | (test, stmts) :: rest => + let thenBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := stmts } + let elseBlock := build_cases rest defaultStmts + let elseBlockWrapped : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [elseBlock] } + .ite test thenBlock elseBlockWrapped + + let switchStructure := build_cases regularCaseStmts defaultStmts + (ctx, [switchStructure]) + + | .TS_ContinueStatement cont => + let tgt := + match ct.continueLabel? with + | some lab => lab + | none => + dbg_trace "[WARN] `continue` encountered outside of a loop; emitting goto to __unbound_continue"; + "__unbound_continue" + (ctx, [ .goto tgt ]) + + | .TS_BreakStatement brk => + -- Handle break statement if loop context fails to handle it + dbg_trace "[WARN] `break` statement not handled by pattern matching"; + match ct.breakFlagVar? with + | some flagVar => + -- Set break flag to true as fallback + (ctx, [ .cmd (.set flagVar Heap.HExpr.true) ]) + | none => + dbg_trace "[WARN] `break` encountered outside of a loop; using fallback goto"; let tgt := - match ct.continueLabel? with + match ct.breakLabel? with | some lab => lab - | none => - dbg_trace "[WARN] `continue` encountered outside of a loop; emitting goto to __unbound_continue"; - "__unbound_continue" + | none => "__unbound_break" (ctx, [ .goto tgt ]) - | .TS_BreakStatement brk => - -- Handle break statement if loop context fails to handle it - dbg_trace "[WARN] `break` statement not handled by pattern matching"; - match ct.breakFlagVar? with - | some flagVar => - -- Set break flag to true as fallback - (ctx, [ .cmd (.set flagVar Heap.HExpr.true) ]) - | none => - dbg_trace "[WARN] `break` encountered outside of a loop; using fallback goto"; - let tgt := - match ct.breakLabel? with - | some lab => lab - | none => "__unbound_break" - (ctx, [ .goto tgt ]) - - | _ => panic! s!"Unimplemented statement: {repr s}" + | _ => panic! s!"Unimplemented statement: {repr s}" -- Translate TypeScript statements to TypeScript-Strata statements partial def translate_statement (s: TS_Statement) (ctx : TranslationContext) : TranslationContext × List TSStrataStatement := diff --git a/Strata/Languages/TypeScript/js_ast.lean b/Strata/Languages/TypeScript/js_ast.lean index 0e7f50963..4e39a9369 100644 --- a/Strata/Languages/TypeScript/js_ast.lean +++ b/Strata/Languages/TypeScript/js_ast.lean @@ -125,6 +125,7 @@ mutual | TS_BreakStatement : TS_BreakStatement → TS_Statement | TS_SwitchStatement : TS_SwitchStatement → TS_Statement | TS_ContinueStatement: TS_ContinueStatement → TS_Statement + | TS_ForInStatement : TS_ForInStatement → TS_Statement deriving Repr, Lean.FromJson, Lean.ToJson inductive TS_AssignmentIdentifier where @@ -270,6 +271,12 @@ mutual discriminant : TS_Expression cases : Array TS_SwitchCase deriving Repr, Lean.FromJson, Lean.ToJson + + structure TS_ForInStatement extends BaseNode where + left: TS_VariableDeclaration + right: TS_Expression + body: TS_Statement + deriving Repr, Lean.FromJson, Lean.ToJson end instance : Inhabited TS_Expression where diff --git a/StrataTest/Languages/TypeScript/test_for_in.ts b/StrataTest/Languages/TypeScript/test_for_in.ts new file mode 100644 index 000000000..4abc2b766 --- /dev/null +++ b/StrataTest/Languages/TypeScript/test_for_in.ts @@ -0,0 +1,5 @@ +let obj = {0: 10, 1: 20, 2: 30}; +let sum = 0; +for (let key in obj) { + sum = sum + obj[key]; +} \ No newline at end of file diff --git a/conformance_testing/babel_to_lean.py b/conformance_testing/babel_to_lean.py index e630a3e28..a323cb5f4 100644 --- a/conformance_testing/babel_to_lean.py +++ b/conformance_testing/babel_to_lean.py @@ -316,6 +316,42 @@ def parse_for_statement(j): add_missing_node_info(j, target_j) return target_j +def parse_for_in_statement(j): + target_body = parse_statement(j['body']) + + left_decl = j['left'] + + # For-in declarators don't have init, so provide a null literal + declarators = [] + for d in left_decl.get('declarations', []): + decl_dict = { + "id": parse_identifier(d['id']), + "init": {"TS_NullLiteral": { + "type": "NullLiteral", + "start": d.get('start', 0), + "end": d.get('end', 0), + "loc": d.get('loc', {}) + }} # Provide dummy null expression + } + add_missing_node_info(d, decl_dict) + declarators.append(decl_dict) + + target_left = { + "type": "VariableDeclaration", + "declarations": declarators, + "kind": left_decl.get('kind') + } + add_missing_node_info(left_decl, target_left) + + target_j = { + "left": target_left, + "right": parse_expression(j['right']), + "body": target_body + } + add_missing_node_info(j, target_j) + + return target_j + def parse_switch_statement(j): target_j = { "discriminant": parse_expression(j['discriminant']), @@ -376,7 +412,8 @@ def parse_statement(j): # case "DoWhileStatement": case "ForStatement": return {"TS_ForStatement": parse_for_statement(j)} - # case "ForInStatement": + case "ForInStatement": + return {"TS_ForInStatement": parse_for_in_statement(j)} # case "ForOfStatement": # case "ClassDeclaration": case _: From 3532c8f06e0d455b99032b343ba1d74810887afe Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Mon, 24 Nov 2025 13:07:38 -0800 Subject: [PATCH 11/11] support for-of, added test --- Strata/Languages/TypeScript/TS_to_Strata.lean | 53 +++++++++++++++++++ Strata/Languages/TypeScript/js_ast.lean | 7 +++ .../Languages/TypeScript/test_for_of.ts | 5 ++ conformance_testing/babel_to_lean.py | 39 +++++++++++++- 4 files changed, 103 insertions(+), 1 deletion(-) create mode 100644 StrataTest/Languages/TypeScript/test_for_of.ts diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index b8c193e53..0bb9a3980 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -776,6 +776,59 @@ partial def translate_statement_core (bodyCtx, [initBreakFlag, initKeys, initLength, initIndex, .loop guard none none bodyBlock]) + | .TS_ForOfStatement forOfStmt => + dbg_trace s!"[DEBUG] Translating for-of statement at loc {forOfStmt.start_loc}-{forOfStmt.end_loc}" + + let continueLabel := s!"forof_continue_{forOfStmt.start_loc}" + let breakLabel := s!"forof_break_{forOfStmt.start_loc}" + let breakFlagVar := s!"forof_break_flag_{forOfStmt.start_loc}" + + -- Extract loop variable name + let valueVarName := match forOfStmt.left.declarations[0]? with + | some decl => decl.id.name + | none => panic! "for-of must have loop variable" + + -- Array to iterate over + let arrExpr := translate_expr forOfStmt.right + + -- Create temporary variables for iteration + let indexVar := s!"__index_{forOfStmt.start_loc}" + let lengthVar := s!"__length_{forOfStmt.start_loc}" + + -- Get length of array + let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) arrExpr) (Heap.HExpr.string "length") + let initLength := .cmd (.init lengthVar Heap.HMonoTy.int lengthExpr) + + -- Initialize index to 0 + let initIndex := .cmd (.init indexVar Heap.HMonoTy.int (Heap.HExpr.int 0)) + + -- Initialize break flag + let initBreakFlag := .cmd (.init breakFlagVar Heap.HMonoTy.bool Heap.HExpr.false) + + -- Loop guard: index < length && !breakFlag + let indexVarExpr := Heap.HExpr.lambda (.fvar indexVar none) + let lengthVarExpr := Heap.HExpr.lambda (.fvar lengthVar none) + let indexCheck := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Lt" none) indexVarExpr) lengthVarExpr + let breakFlagExpr := Heap.HExpr.lambda (.fvar breakFlagVar none) + let guard := Heap.HExpr.deferredIte breakFlagExpr Heap.HExpr.false indexCheck + + let getCurrentValue := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) arrExpr) indexVarExpr + let setValueVar := .cmd (.set valueVarName getCurrentValue) + + let (bodyCtx, userBodyStmts) := translate_statement_core forOfStmt.body ctx + { continueLabel? := some continueLabel, + breakLabel? := some breakLabel, + breakFlagVar? := some breakFlagVar } + + let incrementExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) indexVarExpr) (Heap.HExpr.int 1) + let incrementIndex := .cmd (.set indexVar incrementExpr) + + let initValueVar := .cmd (.init valueVarName Heap.HMonoTy.int (Heap.HExpr.int 0)) + + let loopBodyStmts := [setValueVar] ++ userBodyStmts ++ [incrementIndex] + let bodyBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := loopBodyStmts } + + (bodyCtx, [initBreakFlag, initLength, initIndex, initValueVar, .loop guard none none bodyBlock]) | .TS_ForStatement forStmt => dbg_trace s!"[DEBUG] Translating for statement at loc {forStmt.start_loc}-{forStmt.end_loc}" diff --git a/Strata/Languages/TypeScript/js_ast.lean b/Strata/Languages/TypeScript/js_ast.lean index 4e39a9369..9861150c4 100644 --- a/Strata/Languages/TypeScript/js_ast.lean +++ b/Strata/Languages/TypeScript/js_ast.lean @@ -126,6 +126,7 @@ mutual | TS_SwitchStatement : TS_SwitchStatement → TS_Statement | TS_ContinueStatement: TS_ContinueStatement → TS_Statement | TS_ForInStatement : TS_ForInStatement → TS_Statement + | TS_ForOfStatement : TS_ForOfStatement → TS_Statement deriving Repr, Lean.FromJson, Lean.ToJson inductive TS_AssignmentIdentifier where @@ -277,6 +278,12 @@ mutual right: TS_Expression body: TS_Statement deriving Repr, Lean.FromJson, Lean.ToJson + + structure TS_ForOfStatement extends BaseNode where + left: TS_VariableDeclaration + right: TS_Expression + body: TS_Statement + deriving Repr, Lean.FromJson, Lean.ToJson end instance : Inhabited TS_Expression where diff --git a/StrataTest/Languages/TypeScript/test_for_of.ts b/StrataTest/Languages/TypeScript/test_for_of.ts new file mode 100644 index 000000000..742789823 --- /dev/null +++ b/StrataTest/Languages/TypeScript/test_for_of.ts @@ -0,0 +1,5 @@ +let arr = [10, 20, 30]; +let sum = 0; +for (let value of arr) { + sum = sum + value; +} \ No newline at end of file diff --git a/conformance_testing/babel_to_lean.py b/conformance_testing/babel_to_lean.py index a323cb5f4..a04dbd190 100644 --- a/conformance_testing/babel_to_lean.py +++ b/conformance_testing/babel_to_lean.py @@ -352,6 +352,42 @@ def parse_for_in_statement(j): return target_j +def parse_for_of_statement(j): + target_body = parse_statement(j['body']) + + # Parse left as bare TS_VariableDeclaration structure + left_decl = j['left'] + + declarators = [] + for d in left_decl.get('declarations', []): + decl_dict = { + "id": parse_identifier(d['id']), + "init": {"TS_NullLiteral": { + "type": "NullLiteral", + "start": d.get('start', 0), + "end": d.get('end', 0), + "loc": d.get('loc', {}) + }} + } + add_missing_node_info(d, decl_dict) + declarators.append(decl_dict) + + target_left = { + "type": "VariableDeclaration", + "declarations": declarators, + "kind": left_decl.get('kind') + } + add_missing_node_info(left_decl, target_left) + + target_j = { + "left": target_left, + "right": parse_expression(j['right']), + "body": target_body + } + add_missing_node_info(j, target_j) + + return target_j + def parse_switch_statement(j): target_j = { "discriminant": parse_expression(j['discriminant']), @@ -414,7 +450,8 @@ def parse_statement(j): return {"TS_ForStatement": parse_for_statement(j)} case "ForInStatement": return {"TS_ForInStatement": parse_for_in_statement(j)} - # case "ForOfStatement": + case "ForOfStatement": + return {"TS_ForOfStatement": parse_for_of_statement(j)} # case "ClassDeclaration": case _: print("Unsupported statement type: " + j['type'], file=sys.stderr)