diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index 7183bfcf..ac915719 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -206,6 +206,16 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr := -- For now, create a placeholder that will be handled during call statement processing Heap.HExpr.lambda (.fvar s!"call_{call.callee.name}" none) + | .TS_FunctionExpression e => + -- Translate function definition + dbg_trace s!"[DEBUG] Translating TypeScript function expression at loc {e.start_loc}-{e.end_loc}" + let funcName := s!"__anon_func_{e.start_loc}_{e.end_loc}" + -- just return a heap lambda placeholder + Heap.HExpr.lambda (.fvar funcName none) + + | .TS_ArrowFunctionExpression e => + Heap.HExpr.lambda (.fvar s!"__arrow_func_{e.start_loc}_{e.end_loc}" none) + | _ => panic! s!"Unimplemented expression: {repr e}" partial def translate_statement_core @@ -219,10 +229,10 @@ partial def translate_statement_core dbg_trace s!"[DEBUG] Function parameters: {funcDecl.params.toList.map (·.name)}" dbg_trace s!"[DEBUG] Function body has statements" - let funcBody := match funcDecl.body with - | .TS_BlockStatement blockStmt => - (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten - | _ => panic! s!"Expected block statement as function body, got: {repr funcDecl.body}" + let funcBody := match funcDecl.body with + | .TS_BlockStatement blockStmt => + (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten + | _ => panic! s!"Expected block statement as function body, got: {repr funcDecl.body}" dbg_trace s!"[DEBUG] Translated function body to {funcBody.length} Strata statements" @@ -263,6 +273,46 @@ partial def translate_statement_core 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)]) + | .TS_FunctionExpression funcExpr => + -- Handle function expression assignment: let x = function(...) { ... } + let funcName := d.id.name + let funcBody := match funcExpr.body with + | .TS_BlockStatement blockStmt => + (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten + | _ => panic! s!"Expected block statement as function body, got: {repr funcExpr.body}" + dbg_trace s!"[DEBUG] Translating TypeScript function expression assignment: {d.id.name} = function(...)" + let strataFunc : CallHeapStrataFunction := { + name := funcName, + params := funcExpr.params.toList.map (·.name), + body := funcBody, + returnType := none -- We'll infer this later if needed + } + 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)]) + | .TS_ArrowFunctionExpression funcExpr => + -- Handle arrow function assignment: let x = (args) => { ... } + let funcName := d.id.name + let funcBody := match funcExpr.body with + | .TS_BlockStatement blockStmt => + (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten + | _ => panic! s!"Expected block statement as function body, got: {repr funcExpr.body}" + dbg_trace s!"[DEBUG] Translating TypeScript arrow function assignment: {d.id.name} = (args) => function(...)" + let strataFunc : CallHeapStrataFunction := { + name := funcName, + params := funcExpr.params.toList.map (·.name), + body := funcBody, + returnType := none -- We'll infer this later if needed + } + 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)]) | _ => -- Handle simple variable declaration: let x = value let value := translate_expr d.init @@ -283,119 +333,187 @@ partial def translate_statement_core match assgn.left with | .TS_Identifier id => -- Handle identifier assignment: x = value - let value := translate_expr assgn.right - dbg_trace s!"[DEBUG] Assignment: {id.name} = {repr value}" - (ctx, [.cmd (.set id.name value)]) + match assgn.right with + | .TS_FunctionExpression funcExpr => + -- Capture parameters and body here (since translate_expr is kept pure) + let funcName := id.name + let funcBody := match funcExpr.body with + | .TS_BlockStatement blockStmt => + (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten + | _ => panic! s!"Expected block statement as function body, got: {repr funcExpr.body}" + let strataFunc : CallHeapStrataFunction := { + name := funcName, + params := funcExpr.params.toList.map (·.name), + body := funcBody, + returnType := none + } + let newCtx := ctx.addFunction strataFunc + dbg_trace s!"[DEBUG] Added anonymous function '{funcName}' to context (assignment to identifier)" + let funcRef := Heap.HExpr.lambda (.fvar funcName none) + (newCtx, [.cmd (.set id.name funcRef)]) + | otherExpr => + let value := translate_expr otherExpr + dbg_trace s!"[DEBUG] Assignment: {id.name} = {repr value}" + (ctx, [.cmd (.set id.name value)]) | .TS_MemberExpression member => -- Handle field assignment: obj[field] = value let objExpr := translate_expr member.object - let valueExpr := translate_expr assgn.right - - -- Handle both static and dynamic field assignment - match member.property with - | .TS_NumericLiteral numLit => - -- Static field assignment: obj[5] = value - let fieldIndex := Float.floor numLit.value |>.toUInt64.toNat - let assignExpr := Heap.HExpr.assign objExpr fieldIndex valueExpr - (ctx, [.cmd (.set "temp_assign_result" assignExpr)]) - | .TS_IdExpression id => - -- Dynamic field assignment: obj[variable] = value - let fieldExpr := translate_expr (.TS_IdExpression id) - 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)]) - | _ => - -- Other dynamic field assignment: obj[expr] = value - 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)]) + + -- If RHS is a function expression, capture params/body now and bind funcRef + match assgn.right with + | .TS_FunctionExpression funcExpr => + let funcName := s!"__anon_func_{funcExpr.start_loc}_{funcExpr.end_loc}" + let funcBody := match funcExpr.body with + | .TS_BlockStatement blockStmt => + (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten + | _ => panic! s!"Expected block statement as function body, got: {repr funcExpr.body}" + let strataFunc : CallHeapStrataFunction := { + name := funcName, + params := funcExpr.params.toList.map (·.name), + body := funcBody, + returnType := none + } + let newCtx := ctx.addFunction strataFunc + dbg_trace s!"[DEBUG] Added anonymous function '{funcName}' to context (assignment to member)" + let funcRef := Heap.HExpr.lambda (.fvar funcName none) + -- Handle both static and dynamic field assignment using funcRef + match member.property with + | .TS_NumericLiteral numLit => + let fieldIndex := Float.floor numLit.value |>.toUInt64.toNat + let assignExpr := Heap.HExpr.assign objExpr fieldIndex funcRef + (newCtx, [.cmd (.set "temp_assign_result" assignExpr)]) + | .TS_IdExpression id => + let fieldExpr := translate_expr (.TS_IdExpression id) + let assignExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) fieldExpr) funcRef + (newCtx, [.cmd (.set "temp_assign_result" assignExpr)]) + | _ => + let fieldExpr := translate_expr member.property + let assignExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) fieldExpr) funcRef + (newCtx, [.cmd (.set "temp_assign_result" assignExpr)]) + | otherExpr => + let valueExpr := translate_expr otherExpr + -- Handle both static and dynamic field assignment with normal RHS + match member.property with + | .TS_NumericLiteral numLit => + -- Static field assignment: obj[5] = value + let fieldIndex := Float.floor numLit.value |>.toUInt64.toNat + let assignExpr := Heap.HExpr.assign objExpr fieldIndex valueExpr + (ctx, [.cmd (.set "temp_assign_result" assignExpr)]) + | .TS_IdExpression id => + -- Dynamic field assignment: obj[variable] = value + let fieldExpr := translate_expr (.TS_IdExpression id) + 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)]) + | _ => + -- Other dynamic field assignment: obj[expr] = value + 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}" + let funcBody := match funcExpr.body with + | .TS_BlockStatement blockStmt => + (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten + | _ => panic! s!"Expected block statement as function body, got: {repr funcExpr.body}" + let strataFunc : CallHeapStrataFunction := { + name := funcName, + params := funcExpr.params.toList.map (·.name), + body := funcBody, + returnType := none -- We'll infer this later if needed + } + let newCtx := ctx.addFunction strataFunc + dbg_trace s!"[DEBUG] Added anonymous function '{funcName}' to context" + -- For now, we don't execute the function; just define it + (newCtx, []) | _ => -- Other expression statements - ignore for now (ctx, []) - | .TS_BlockStatement block => - -- lower inside loops: if (cond) { continue; } ==> if (cond) { } else { } - -- lower inside loops: if (cond) { break; } ==> if (cond) { } else { } - let stmts := block.body.toList - - -- consequent is exactly a bare `continue` - let isBareContinueStmt : TS_Statement → Bool - | .TS_ContinueStatement _ => true - | _ => false - - -- consequent is exactly a bare `break` - let isBareBreakStmt : TS_Statement → Bool - | .TS_BreakStatement _ => true - | _ => false - - let isIfWithBareContinue : TS_Statement → Option TS_IfStatement - | .TS_IfStatement ifs => - let conseqIsBare := - match ifs.consequent with - | .TS_ContinueStatement _ => true - | .TS_BlockStatement b => - match b.body.toList with - | [one] => isBareContinueStmt one - | _ => false - | _ => false - if conseqIsBare && ifs.alternate.isNone then some ifs else none - | _ => none - - let isIfWithBareBreak : TS_Statement → Option TS_IfStatement - | .TS_IfStatement ifs => - let conseqIsBare := - match ifs.consequent with - | .TS_BreakStatement _ => true - | .TS_BlockStatement b => - match b.body.toList with - | [one] => isBareBreakStmt one - | _ => false - | _ => false - if conseqIsBare && ifs.alternate.isNone then some ifs else none - | _ => none - - -- when we hit the pattern (in a loop), guard the tail with `else` - let rec go (accCtx : TranslationContext) (acc : List TSStrataStatement) (rest : List TS_Statement) - : TranslationContext × List TSStrataStatement := - match rest with - | [] => (accCtx, acc) - | s :: tail => - let continueMatch := isIfWithBareContinue s - let breakMatch := isIfWithBareBreak s - dbg_trace s!"[DEBUG] Block statement processing: continueMatch={continueMatch.isSome}, breakMatch={breakMatch.isSome}, ct.continueLabel?={ct.continueLabel?}, ct.breakLabel?={ct.breakLabel?}" - match ct.continueLabel?, ct.breakFlagVar?, continueMatch, breakMatch with - | some _, _, some ifs, _ => - -- Continue case: Translate the tail (everything after the `if`) under the `else` branch - let (tailCtx, tailStmts) := - tail.foldl - (fun (p, accS) stmt => + | .TS_BlockStatement block => + -- lower inside loops: if (cond) { continue; } ==> if (cond) { } else { } + -- lower inside loops: if (cond) { break; } ==> if (cond) { } else { } + let stmts := block.body.toList + + -- consequent is exactly a bare `continue` + let isBareContinueStmt : TS_Statement → Bool + | .TS_ContinueStatement _ => true + | _ => false + + -- consequent is exactly a bare `break` + let isBareBreakStmt : TS_Statement → Bool + | .TS_BreakStatement _ => true + | _ => false + + let isIfWithBareContinue : TS_Statement → Option TS_IfStatement + | .TS_IfStatement ifs => + let conseqIsBare := + match ifs.consequent with + | .TS_ContinueStatement _ => true + | .TS_BlockStatement b => + match b.body.toList with + | [one] => isBareContinueStmt one + | _ => false + | _ => false + if conseqIsBare && ifs.alternate.isNone then some ifs else none + | _ => none + + let isIfWithBareBreak : TS_Statement → Option TS_IfStatement + | .TS_IfStatement ifs => + let conseqIsBare := + match ifs.consequent with + | .TS_BreakStatement _ => true + | .TS_BlockStatement b => + match b.body.toList with + | [one] => isBareBreakStmt one + | _ => false + | _ => false + if conseqIsBare && ifs.alternate.isNone then some ifs else none + | _ => none + + -- when we hit the pattern (in a loop), guard the tail with `else` + let rec go (accCtx : TranslationContext) (acc : List TSStrataStatement) (rest : List TS_Statement) + : TranslationContext × List TSStrataStatement := + match rest with + | [] => (accCtx, acc) + | s :: tail => + let continueMatch := isIfWithBareContinue s + let breakMatch := isIfWithBareBreak s + dbg_trace s!"[DEBUG] Block statement processing: continueMatch={continueMatch.isSome}, breakMatch={breakMatch.isSome}, ct.continueLabel?={ct.continueLabel?}, ct.breakLabel?={ct.breakLabel?}" + match ct.continueLabel?, ct.breakFlagVar?, continueMatch, breakMatch with + | some _, _, some ifs, _ => + -- Continue case: Translate the tail (everything after the `if`) under the `else` branch + let (tailCtx, tailStmts) := + tail.foldl + (fun (p, accS) stmt => let (p2, ss2) := translate_statement_core stmt p ct (p2, accS ++ ss2)) - (accCtx, []) - let cond := translate_expr ifs.test - let thenBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [] } - let elseBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := tailStmts } - -- Emit one conditional and STOP - (tailCtx, acc ++ [ .ite cond thenBlk elseBlk ]) - | _, some breakFlagVar, _, some ifs => - -- Break case: Set break flag in then branch, execute tail in else branch - let (tailCtx, tailStmts) := - tail.foldl - (fun (p, accS) stmt => + (accCtx, []) + let cond := translate_expr ifs.test + let thenBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [] } + let elseBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := tailStmts } + -- Emit one conditional and STOP + (tailCtx, acc ++ [ .ite cond thenBlk elseBlk ]) + | _, some breakFlagVar, _, some ifs => + -- Break case: Set break flag in then branch, execute tail in else branch + let (tailCtx, tailStmts) := + tail.foldl + (fun (p, accS) stmt => let (p2, ss2) := translate_statement_core stmt p ct (p2, accS ++ ss2)) - (accCtx, []) - let cond := translate_expr ifs.test - let setBreakFlag : TSStrataStatement := .cmd (.set breakFlagVar Heap.HExpr.true) - let thenBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [setBreakFlag] } - let elseBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := tailStmts } - -- Emit conditional: if condition then set break flag, else execute remaining statements - (tailCtx, acc ++ [ .ite cond thenBlk elseBlk ]) - | _, _, _, _ => - let (newCtx, ss) := translate_statement_core s accCtx ct - go newCtx (acc ++ ss) tail - - go ctx [] stmts + (accCtx, []) + let cond := translate_expr ifs.test + let setBreakFlag : TSStrataStatement := .cmd (.set breakFlagVar Heap.HExpr.true) + let thenBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [setBreakFlag] } + let elseBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := tailStmts } + -- Emit conditional: if condition then set break flag, else execute remaining statements + (tailCtx, acc ++ [ .ite cond thenBlk elseBlk ]) + | _, _, _, _ => + let (newCtx, ss) := translate_statement_core s accCtx ct + go newCtx (acc ++ ss) tail + + go ctx [] stmts | .TS_IfStatement ifStmt => -- Handle if statement: if test then consequent else alternate diff --git a/Strata/Languages/TypeScript/js_ast.lean b/Strata/Languages/TypeScript/js_ast.lean index 18efab8b..6635b89d 100644 --- a/Strata/Languages/TypeScript/js_ast.lean +++ b/Strata/Languages/TypeScript/js_ast.lean @@ -153,6 +153,20 @@ mutual 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 + + structure TS_ArrowFunctionExpression extends BaseNode where + params : Array TS_Identifier + 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 @@ -168,31 +182,33 @@ mutual | 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 -end -structure TS_VariableDeclarator extends BaseNode where - id : TS_Identifier - init: TS_Expression -deriving Repr, Lean.FromJson, Lean.ToJson -structure TS_VariableDeclaration extends BaseNode where - declarations : Array TS_VariableDeclarator := #[] - kind : Option String -deriving Repr, Lean.FromJson, Lean.ToJson + structure TS_VariableDeclarator extends BaseNode where + id : TS_Identifier + init: TS_Expression + deriving Repr, Lean.FromJson, Lean.ToJson -structure TS_EmptyStatement extends BaseNode where -deriving Repr, Lean.FromJson, Lean.ToJson + structure TS_VariableDeclaration extends BaseNode where + declarations : Array TS_VariableDeclarator := #[] + kind : Option String + deriving Repr, Lean.FromJson, Lean.ToJson -structure TS_ExpressionStatement extends BaseNode where - expression : TS_Expression -deriving Repr, Lean.FromJson, Lean.ToJson + structure TS_EmptyStatement extends BaseNode where + deriving Repr, Lean.FromJson, Lean.ToJson + + structure TS_ExpressionStatement extends BaseNode where + expression : TS_Expression + deriving Repr, Lean.FromJson, Lean.ToJson + + structure TS_ThrowStatement extends BaseNode where + argument: TS_Expression + deriving Repr, Lean.FromJson, Lean.ToJson -structure TS_ThrowStatement extends BaseNode where - argument: TS_Expression -deriving Repr, Lean.FromJson, Lean.ToJson -mutual structure TS_BlockStatement extends BaseNode where body : Array TS_Statement directives : Array String := #[] diff --git a/StrataTest/Languages/TypeScript/test_arrow_func.ts b/StrataTest/Languages/TypeScript/test_arrow_func.ts new file mode 100644 index 00000000..fdbd7f4e --- /dev/null +++ b/StrataTest/Languages/TypeScript/test_arrow_func.ts @@ -0,0 +1,7 @@ +// Example: Arrow function that adds two numbers +const add = (x: number, y: number): number => { + return x + y; +}; + +// Usage +let result = add(3, 5); // Output: 8 \ No newline at end of file diff --git a/StrataTest/Languages/TypeScript/test_function_expr.ts b/StrataTest/Languages/TypeScript/test_function_expr.ts new file mode 100644 index 00000000..7e398a17 --- /dev/null +++ b/StrataTest/Languages/TypeScript/test_function_expr.ts @@ -0,0 +1,8 @@ +// Test function expression +let f = function() { + let x: number = 1; + let y: number = 2; + return x + y; +}; + +let result: number = f(); \ No newline at end of file diff --git a/conformance_testing/babel_to_lean.py b/conformance_testing/babel_to_lean.py index d0cbb08e..72de1114 100644 --- a/conformance_testing/babel_to_lean.py +++ b/conformance_testing/babel_to_lean.py @@ -133,6 +133,19 @@ def parse_member_expression(j): add_missing_node_info(j, target_j) return target_j +def parse_function_expression(j): + target_j = { + 'params': [parse_identifier(ji) for ji in j['params']], + 'body': parse_statement(j['body']) + } + add_missing_node_info(j, target_j) + return target_j + +def parse_arrow_function_expression(j): + target_j = { + 'params': [parse_identifier(ji) for ji in j['params']], + 'body': parse_statement(j['body']) + } def parse_array_expression(j): # Normalize Babel ArrayExpression: keep only non-null elements and parse each elems = [] @@ -173,14 +186,16 @@ def parse_expression(j): return {"TS_MemberExpression": parse_member_expression(j)} # case "ThisExpression": - # case "ArrowFunctionExpression": + case "ArrowFunctionExpression": + return {"TS_ArrowFunctionExpression": parse_function_expression(j)} # case "YieldExpression": # case "AwaitExpression": case "ArrayExpression": return {"TS_ArrayExpression": parse_array_expression(j)} # case "RecordExpression": # case "TupleExpression": - # case "FunctionExpression": + case "FunctionExpression": + return {"TS_FunctionExpression": parse_function_expression(j)} # case "UnaryExpression": # case "UpdateExpression": # case "BindExpression":