From 1a1f7b4ce567da11c05650f17234cb4543f082c0 Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Tue, 30 Sep 2025 13:42:28 -0700 Subject: [PATCH 01/13] [feat] add test for array length calculation --- StrataTest/Languages/TypeScript/test_arrays_length.ts | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 StrataTest/Languages/TypeScript/test_arrays_length.ts diff --git a/StrataTest/Languages/TypeScript/test_arrays_length.ts b/StrataTest/Languages/TypeScript/test_arrays_length.ts new file mode 100644 index 000000000..6610d9494 --- /dev/null +++ b/StrataTest/Languages/TypeScript/test_arrays_length.ts @@ -0,0 +1,3 @@ +let numbers: number[] = [1, 2, 3, 4, 5]; + +let len: number = numbers.length; \ No newline at end of file From df7fcc69087745ec37f3b3212bfce996af5eb119 Mon Sep 17 00:00:00 2001 From: YingZhu Date: Sun, 28 Sep 2025 21:12:11 -0700 Subject: [PATCH 02/13] feat(str.length): add support for translation of str.length and corresponding test Signed-off-by: YingZhu --- Strata/DL/Heap/HEval.lean | 27 +++++++++++++++++++ Strata/Languages/TypeScript/TS_to_Strata.lean | 16 +++++++---- .../TypeScript/test_str_properties.ts | 2 ++ 3 files changed, 40 insertions(+), 5 deletions(-) create mode 100644 StrataTest/Languages/TypeScript/test_str_properties.ts diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index ba01057f3..9ff3ab2ed 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -149,6 +149,13 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE -- Third application to DynamicFieldAssign - now we can evaluate -- This handles obj[field] = value where field is dynamic evalDynamicFieldAssign state2 objExpr fieldExpr e2' + | .deferredOp "StringFieldAccess" _ => + -- First application to StringFieldAccess - return partially applied + (state2, .app (.deferredOp "StringFieldAccess" none) e2') + | .app (.deferredOp "StringFieldAccess" _) objExpr => + -- Second application to StringFieldAccess - return partially applied + -- This handles str.fieldName where fieldName is a string literal + evalStringFieldAccess state2 objExpr e2' | .deferredOp op _ => -- First application to a deferred operation - return partially applied (state2, .app (.deferredOp op none) e2') @@ -192,6 +199,26 @@ partial def evalDynamicFieldAssign (state : HState) (objExpr fieldExpr valueExpr -- Can't extract a numeric field index, return error (state, .lambda (LExpr.const "error_dynamic_field_assign_failed" none)) +-- Handle string field access: str.fieldName where fieldName is a string literal +partial def evalStringFieldAccess (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr := + match fieldExpr with + | .lambda (LExpr.const key _) => + if key == "length" then + -- Handle string length property + match objExpr with + | .lambda (LExpr.const s _) => + let len := s.length + (state, .lambda (LExpr.const (toString len) (some Lambda.LMonoTy.int))) + | _ => + -- Not a string value + (state, .lambda (LExpr.const "error_not_a_string" none)) + else + -- Unknown string property + (state, .lambda (LExpr.const "error_unknown_string_property" none)) + | _ => + -- Field is not a string literal + (state, .lambda (LExpr.const "error_non_literal_string_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 e164ac4b3..7183bfcfc 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -167,18 +167,24 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := Heap.HExpr.allocSimple fields | .TS_MemberExpression e => - -- Translate obj[index] to heap dereference + -- Translate str.length/obj[index] to heap dereference let objExpr := translate_expr e.object - -- Handle both static and dynamic field access match e.property with | .TS_NumericLiteral numLit => -- Static field access: obj[5] let field := Float.floor numLit.value |>.toUInt64.toNat Heap.HExpr.deref objExpr field | .TS_IdExpression id => - -- Dynamic field access: obj[variable] - let varExpr := translate_expr (.TS_IdExpression id) - Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) varExpr + let keyName := id.name + if !e.computed && keyName == "length" then + -- String dot access: str.length + let keyExpr := Heap.HExpr.string keyName + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "StringFieldAccess" none) objExpr) keyExpr + else + -- Dynamic field access: obj[variable] + let varExpr := translate_expr (.TS_IdExpression id) + Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) varExpr + | _ => -- Other dynamic expressions: obj[expr] let fieldExpr := translate_expr e.property diff --git a/StrataTest/Languages/TypeScript/test_str_properties.ts b/StrataTest/Languages/TypeScript/test_str_properties.ts new file mode 100644 index 000000000..1da3c9fb4 --- /dev/null +++ b/StrataTest/Languages/TypeScript/test_str_properties.ts @@ -0,0 +1,2 @@ +let s = "abcd" +let l = s.length \ No newline at end of file From f7d9c8dc698eb9a707e74b2f97da155cb2a16148 Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Thu, 2 Oct 2025 11:22:21 -0700 Subject: [PATCH 03/13] [feat] implemented array length calculation --- Strata/DL/Heap/HEval.lean | 45 ++++++++++++++++--- Strata/Languages/TypeScript/TS_to_Strata.lean | 4 +- 2 files changed, 40 insertions(+), 9 deletions(-) diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index 9ff3ab2ed..b4e770831 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -149,13 +149,19 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE -- Third application to DynamicFieldAssign - now we can evaluate -- This handles obj[field] = value where field is dynamic evalDynamicFieldAssign state2 objExpr fieldExpr e2' - | .deferredOp "StringFieldAccess" _ => - -- First application to StringFieldAccess - return partially applied - (state2, .app (.deferredOp "StringFieldAccess" none) e2') - | .app (.deferredOp "StringFieldAccess" _) objExpr => - -- Second application to StringFieldAccess - return partially applied - -- This handles str.fieldName where fieldName is a string literal - evalStringFieldAccess state2 objExpr e2' + -- | .deferredOp "StringFieldAccess" _ => + -- -- First application to StringFieldAccess - return partially applied + -- (state2, .app (.deferredOp "StringFieldAccess" none) e2') + -- | .app (.deferredOp "StringFieldAccess" _) objExpr => + -- -- 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 7183bfcfc..ba3a9201d 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) From 88736e4d82bdf141660e66aff699eef482b13f18 Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Thu, 2 Oct 2025 11:28:00 -0700 Subject: [PATCH 04/13] [feat] uncomment `StringFieldAccess` --- Strata/DL/Heap/HEval.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index b4e770831..89a323f29 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -149,13 +149,13 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE -- Third application to DynamicFieldAssign - now we can evaluate -- This handles obj[field] = value where field is dynamic evalDynamicFieldAssign state2 objExpr fieldExpr e2' - -- | .deferredOp "StringFieldAccess" _ => - -- -- First application to StringFieldAccess - return partially applied - -- (state2, .app (.deferredOp "StringFieldAccess" none) e2') - -- | .app (.deferredOp "StringFieldAccess" _) objExpr => - -- -- Second application to StringFieldAccess - return partially applied - -- -- This handles str.fieldName where fieldName is a string literal - -- evalStringFieldAccess state2 objExpr e2' + | .deferredOp "StringFieldAccess" _ => + -- First application to StringFieldAccess - return partially applied + (state2, .app (.deferredOp "StringFieldAccess" none) e2') + | .app (.deferredOp "StringFieldAccess" _) objExpr => + -- 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') From 9d7cac1790810de79d5779629567a62bc68b1bfe Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Sat, 4 Oct 2025 22:49:29 -0700 Subject: [PATCH 05/13] [feat] more array length test --- StrataTest/Languages/TypeScript/test_arrays_length.ts | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/StrataTest/Languages/TypeScript/test_arrays_length.ts b/StrataTest/Languages/TypeScript/test_arrays_length.ts index 6610d9494..1acf63db3 100644 --- a/StrataTest/Languages/TypeScript/test_arrays_length.ts +++ b/StrataTest/Languages/TypeScript/test_arrays_length.ts @@ -1,3 +1,5 @@ let numbers: number[] = [1, 2, 3, 4, 5]; +let strings: string[] = ["hello", "world"]; -let len: number = numbers.length; \ No newline at end of file +const numLen: number = numbers.length; +const strLen: number = strings.length; \ No newline at end of file From 5fe89901a284fb5dfc5a6893ab7e2f62274d33f2 Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Tue, 7 Oct 2025 20:21:14 -0700 Subject: [PATCH 06/13] [feat] implement field deletion and enhance call expression parsing, implement implmented array `.push()` and `.pop()` --- Strata/DL/Heap/HEval.lean | 33 +++++ Strata/DL/Heap/HState.lean | 12 ++ Strata/Languages/TypeScript/TS_to_Strata.lean | 115 +++++++++++++++--- Strata/Languages/TypeScript/js_ast.lean | 16 ++- .../Languages/TypeScript/test_arrays.ts | 9 +- conformance_testing/babel_to_lean.py | 2 +- 6 files changed, 164 insertions(+), 23 deletions(-) diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index 936da4386..7901e602b 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -162,6 +162,14 @@ 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 +233,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 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 := 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 ba3a9201d..8cb6e1c9e 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}" | _ => panic! s!"Unimplemented expression: {repr e}" @@ -254,30 +277,82 @@ 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 => - -- 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)]) - | _ => - -- Handle simple variable declaration: let x = value + let defaultInit := let value := translate_expr d.init let ty := get_var_type d.id.typeAnnotation d.init (ctx, [.cmd (.init d.id.name ty value)]) + 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 + let lhs := [d.id.name] + (ctx, [.cmd (.directCall lhs id.name args)]) + | .TS_MemberExpression member => + match member.property with + | .TS_IdExpression methodId => + if methodId.name == "pop" then + -- Handle Array.pop() method + let objExpr := translate_expr member.object + 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) + let valueExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) tempIndexVar + let ty := infer_type_from_expr d.init + 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, initStmt, deleteStmt]) + else + defaultInit + | _ => defaultInit + | _ => defaultInit + | _ => defaultInit + | .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 diff --git a/Strata/Languages/TypeScript/js_ast.lean b/Strata/Languages/TypeScript/js_ast.lean index 18efab8b3..64ef40c63 100644 --- a/Strata/Languages/TypeScript/js_ast.lean +++ b/Strata/Languages/TypeScript/js_ast.lean @@ -149,7 +149,7 @@ 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 @@ -171,6 +171,20 @@ mutual deriving Repr, Lean.FromJson, Lean.ToJson end +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_VariableDeclarator extends BaseNode where id : TS_Identifier init: TS_Expression 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 d0cbb08ec..6c92c54bc 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 d499427f27e0a9ebe5d15cc189b44f1fb48307c1 Mon Sep 17 00:00:00 2001 From: ygrx532 Date: Thu, 30 Oct 2025 10:46:47 -0700 Subject: [PATCH 07/13] [feat] implement array slice and add unary expression support --- Strata/DL/Heap/HEval.lean | 58 +++++++++++++++++++ Strata/Languages/TypeScript/TS_to_Strata.lean | 21 +++++++ .../Languages/TypeScript/test_array_slice.ts | 5 ++ test_single_file.sh | 50 ++++++++++++++++ 4 files changed, 134 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 7901e602b..51726c4ea 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -170,6 +170,17 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE -- 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') @@ -259,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 8cb6e1c9e..42f0ae5e0 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 bbe6d1e7a253dc4c93bf928908ff35ff731c1c1a Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Sun, 26 Oct 2025 20:32:14 -0700 Subject: [PATCH 08/13] 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 | 93 ++++++++------ .../Languages/TypeScript/test_array_shift.ts | 20 +++ .../Languages/TypeScript/test_arrays.ts | 9 +- .../TypeScript/test_arrays_length.ts | 5 - 6 files changed, 189 insertions(+), 74 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 7901e602b..ab7e34bae 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -169,7 +169,15 @@ 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' - + | .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') @@ -233,6 +241,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 @@ -259,30 +293,61 @@ 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 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 := @@ -320,4 +385,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 8cb6e1c9e..3ebf58a0e 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -219,6 +219,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) | _ => @@ -306,6 +313,11 @@ partial def translate_statement_core 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, initStmt, deleteStmt]) + else if methodId.name == "shift" then + let objExpr := translate_expr member.object + let shiftExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr + let ty := infer_type_from_expr d.init + (ctx, [.cmd (.init d.id.name ty shiftExpr)]) else defaultInit | _ => defaultInit @@ -316,43 +328,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 @@ -602,4 +623,4 @@ def describeTSStrataStatement (stmt: TSStrataStatement) : String := --#eval translate_expr (.NumericLiteral {value := 42, extra := {raw := "42", rawValue := 42}, type := "NumericLiteral"}) -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 a832fa3b43ec23d5e908662cf0a7a0ff49f39614 Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Thu, 30 Oct 2025 11:17:43 -0700 Subject: [PATCH 09/13] array: `shift()` and `unshift()` supported multiple params now --- Strata/DL/Heap/HEval.lean | 1 - Strata/Languages/TypeScript/TS_to_Strata.lean | 49 ++++++++++++++++--- .../Languages/TypeScript/test_array_shift.ts | 2 +- 3 files changed, 43 insertions(+), 9 deletions(-) diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index ab7e34bae..cdeacbdd9 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -349,7 +349,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 3ebf58a0e..10207ded5 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -223,9 +223,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) | _ => @@ -318,6 +321,35 @@ partial def translate_statement_core let shiftExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr let ty := infer_type_from_expr d.init (ctx, [.cmd (.init d.id.name ty shiftExpr)]) + else if methodId.name == "shift" then + let objExpr := translate_expr member.object + let shiftExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr + let ty := infer_type_from_expr d.init + (ctx, [.cmd (.init d.id.name ty shiftExpr)]) + else if methodId.name == "unshift" then + -- Handle Array.unshift() with multiple arguments + let objExpr := translate_expr member.object + let valueExprs := call.arguments.toList.map translate_expr + if valueExprs.isEmpty then + defaultInit + else + -- Process all unshifts in reverse order + -- valueExprs = [2, 1], reverse = [1, 2] + -- We want to execute: unshift(1), then unshift(2) + 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) + ) + -- Last unshift assigns to the variable + 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]) + else defaultInit | _ => defaultInit @@ -358,10 +390,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 e40d23a1547d477aaaf7c4225d3be79c36b86edc Mon Sep 17 00:00:00 2001 From: ex10si0n Date: Mon, 3 Nov 2025 00:13:31 -0800 Subject: [PATCH 10/13] misc: added support for unary operators in expression parsing --- Strata/Languages/TypeScript/TS_to_Strata.lean | 14 ++++++++++++++ .../Languages/TypeScript/test_array_shift.ts | 2 +- 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index 10207ded5..d5938c8f8 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -201,6 +201,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) From 1123316ab284bdb8949248cd908484a17a6dcb85 Mon Sep 17 00:00:00 2001 From: ygrx532 Date: Mon, 3 Nov 2025 10:01:49 -0800 Subject: [PATCH 11/13] [chore] remove single test script --- test_single_file.sh | 50 --------------------------------------------- 1 file changed, 50 deletions(-) delete mode 100644 test_single_file.sh 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 47944b0a47631a2c4c9e04002a8033db3fd3ea8e Mon Sep 17 00:00:00 2001 From: ygrx532 Date: Thu, 6 Nov 2025 00:16:58 -0800 Subject: [PATCH 12/13] feat: 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 cdeacbdd9..9ff11bdb9 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -178,6 +178,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') @@ -349,6 +355,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 d5938c8f8..c1b96ab74 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -243,6 +243,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 3facaa6bf92ed7eb339e9aa03ea40e1a938a9c35 Mon Sep 17 00:00:00 2001 From: ygrx532 Date: Sun, 9 Nov 2025 21:57:59 -0800 Subject: [PATCH 13/13] feat: support array join --- Strata/DL/Heap/HEval.lean | 52 +++++++++++++++++++ Strata/Languages/TypeScript/TS_to_Strata.lean | 7 +++ .../Languages/TypeScript/test_array_join.ts | 7 +++ 3 files changed, 66 insertions(+) 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 f4814341d..0bc80df72 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/Strata/DL/Heap/HEval.lean @@ -195,6 +195,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') @@ -445,6 +451,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 2afeb3a60..d307a7b24 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -263,6 +263,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("-");