diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index b3dd2dc1..1d0ddf8c 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/Strata/Languages/TypeScript/TS_to_Strata.lean @@ -409,6 +409,84 @@ partial def translate_statement_core let loopBody : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [callCb, writeStmt, incIdx] } (ctxAfterCb, [initDst, initIdx, initLen, .loop guard none none loopBody]) + else if methodId.name == "filter" then + -- Handle Array.filter() + let objExpr := translate_expr member.object + let (cbName, ctxAfterCb) := + match call.arguments[0]? with + | some (.TS_FunctionExpression fexpr) => + let funcName := s!"__anon_filter_func_{fexpr.start_loc}_{fexpr.end_loc}" + let funcBody := match fexpr.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 fexpr.body}" + let strataFunc : CallHeapStrataFunction := { + name := funcName, + params := fexpr.params.toList.map (·.name), + body := funcBody, + returnType := none + } + let newCtx := ctx.addFunction strataFunc + (funcName, newCtx) + | some (.TS_ArrowFunctionExpression aexpr) => + let funcName := s!"__anon_filter_arrow_{aexpr.start_loc}_{aexpr.end_loc}" + let funcBody := match aexpr.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 aexpr.body}" + let strataFunc : CallHeapStrataFunction := { + name := funcName, + params := aexpr.params.toList.map (·.name), + body := funcBody, + returnType := none + } + let newCtx := ctx.addFunction strataFunc + (funcName, newCtx) + | some (.TS_IdExpression fid) => + (fid.name, ctx) + | _ => panic! "filter(callback) expects a function or identifier as the first argument" + + -- Initialize destination array variable (bind to declared identifier) + let dstVar := d.id.name + let initDst : TSStrataStatement := .cmd (.init dstVar Heap.HMonoTy.addr (Heap.HExpr.allocSimple [])) + + -- idx/len + let idxVar := s!"temp_filter_idx_{member.start_loc}" + let lenVar := s!"temp_filter_len_{member.start_loc}" + let outIdxVar := s!"temp_filter_outidx_{member.start_loc}" + let initIdx : TSStrataStatement := .cmd (.init idxVar Heap.HMonoTy.int (Heap.HExpr.int 0)) + let initOutIdx : TSStrataStatement := .cmd (.init outIdxVar Heap.HMonoTy.int (Heap.HExpr.int 0)) + let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") + let initLen : TSStrataStatement := .cmd (.init lenVar Heap.HMonoTy.int lengthExpr) + + -- guard idx < len + let idxRef := Heap.HExpr.lambda (.fvar idxVar none) + let lenRef := Heap.HExpr.lambda (.fvar lenVar none) + let outIdxRef := Heap.HExpr.lambda (.fvar outIdxVar none) + let guard := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Lt" none) idxRef) lenRef + + -- value = obj[idx]; cond = cb(value, idx, obj); if cond then dst[outIdx] = value; outIdx++; idx++ + let valueExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) idxRef + let condVar := s!"temp_filter_cond_{member.start_loc}" + let callCb : TSStrataStatement := .cmd (.directCall [condVar] cbName [valueExpr, idxRef, objExpr]) + let dstRef := Heap.HExpr.lambda (.fvar dstVar none) + let assignExpr := + Heap.HExpr.app + (Heap.HExpr.app + (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) dstRef) + outIdxRef) + valueExpr + let writeStmt : TSStrataStatement := .cmd (.set "temp_filter_assign_result" assignExpr) + let incOutIdx := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) outIdxRef) (Heap.HExpr.int 1) + let incOutIdxStmt : TSStrataStatement := .cmd (.set outIdxVar incOutIdx) + let condRef := Heap.HExpr.lambda (.fvar condVar none) + let thenBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [writeStmt, incOutIdxStmt] } + let elseBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [] } + let iteStmt : TSStrataStatement := .ite condRef thenBlk elseBlk + let nextIdx := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) idxRef) (Heap.HExpr.int 1) + let incIdx : TSStrataStatement := .cmd (.set idxVar nextIdx) + let loopBody : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [callCb, iteStmt, incIdx] } + (ctxAfterCb, [initDst, initIdx, initOutIdx, initLen, .loop guard none none loopBody]) else defaultInit | _ => defaultInit @@ -615,6 +693,83 @@ partial def translate_statement_core { ss := [callCb, writeStmt, incIdx] } (ctxAfterCb, [initDst, initIdx, initLen, .loop guard none none loopBody]) + | "filter" => + -- arr.filter(callback) + dbg_trace s!"[DEBUG] Translating arr.filter(callback) method call" + let (cbName, ctxAfterCb) := + match call.arguments[0]? with + | some (.TS_FunctionExpression fexpr) => + let funcName := s!"__anon_filter_func_{fexpr.start_loc}_{fexpr.end_loc}" + let funcBody := match fexpr.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 fexpr.body}" + let strataFunc : CallHeapStrataFunction := { + name := funcName, + params := fexpr.params.toList.map (·.name), + body := funcBody, + returnType := none + } + let newCtx := ctx.addFunction strataFunc + (funcName, newCtx) + | some (.TS_ArrowFunctionExpression aexpr) => + let funcName := s!"__anon_filter_arrow_{aexpr.start_loc}_{aexpr.end_loc}" + let funcBody := match aexpr.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 aexpr.body}" + let strataFunc : CallHeapStrataFunction := { + name := funcName, + params := aexpr.params.toList.map (·.name), + body := funcBody, + returnType := none + } + let newCtx := ctx.addFunction strataFunc + (funcName, newCtx) + | some (.TS_IdExpression fid) => + (fid.name, ctx) + | _ => panic! "filter(callback) expects a function or identifier as the first argument" + + -- Prepare destination array to hold filtered values + let dstVar := s!"temp_filter_arr_{member.start_loc}" + let initDst : TSStrataStatement := + .cmd (.init dstVar Heap.HMonoTy.addr (Heap.HExpr.allocSimple [])) + -- idx/len and output idx + let idxVar := s!"temp_filter_idx_{member.start_loc}" + let lenVar := s!"temp_filter_len_{member.start_loc}" + let outIdxVar := s!"temp_filter_outidx_{member.start_loc}" + let initIdx : TSStrataStatement := .cmd (.init idxVar Heap.HMonoTy.int (Heap.HExpr.int 0)) + let initOutIdx : TSStrataStatement := .cmd (.init outIdxVar Heap.HMonoTy.int (Heap.HExpr.int 0)) + let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length") + let initLen : TSStrataStatement := .cmd (.init lenVar Heap.HMonoTy.int lengthExpr) + -- Build guard: idx < len + let idxRef := Heap.HExpr.lambda (.fvar idxVar none) + let lenRef := Heap.HExpr.lambda (.fvar lenVar none) + let outIdxRef := Heap.HExpr.lambda (.fvar outIdxVar none) + let guard := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Lt" none) idxRef) lenRef + -- Loop body: value = obj[idx], cond = cb(value, idx, obj), if cond then dst[outIdx] = value; outIdx++; idx++ + let valueExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) idxRef + let condVar := s!"temp_filter_cond_{member.start_loc}" + let callCb : TSStrataStatement := .cmd (.directCall [condVar] cbName [valueExpr, idxRef, objExpr]) + let dstRef := Heap.HExpr.lambda (.fvar dstVar none) + let assignExpr := + Heap.HExpr.app + (Heap.HExpr.app + (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) dstRef) + outIdxRef) + valueExpr + let writeStmt : TSStrataStatement := .cmd (.set "temp_filter_assign_result" assignExpr) + let incOutIdx := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) outIdxRef) (Heap.HExpr.int 1) + let incOutIdxStmt : TSStrataStatement := .cmd (.set outIdxVar incOutIdx) + let condRef := Heap.HExpr.lambda (.fvar condVar none) + let thenBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [writeStmt, incOutIdxStmt] } + let elseBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [] } + let iteStmt : TSStrataStatement := .ite condRef thenBlk elseBlk + let nextIdx := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) idxRef) (Heap.HExpr.int 1) + let incIdx : TSStrataStatement := .cmd (.set idxVar nextIdx) + let loopBody : Imperative.Block TSStrataExpression TSStrataCommand := + { ss := [callCb, iteStmt, incIdx] } + (ctxAfterCb, [initDst, initIdx, initOutIdx, initLen, .loop guard none none loopBody]) | methodName => dbg_trace s!"[DEBUG] Translating method call: {methodName}(...)" (ctx, []) @@ -850,26 +1005,26 @@ 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) := + | .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, @@ -879,16 +1034,16 @@ partial def translate_statement_core 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 + -- 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 } + -- 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]) + -- output: init break flag, init statements, then a loop statement + (ctx1, [initBreakFlag] ++ initStmts ++ [ .loop combinedCondition none none loopBody]) | .TS_ContinueStatement cont => let tgt := diff --git a/StrataTest/Languages/TypeScript/test_arrays_iterations.ts b/StrataTest/Languages/TypeScript/test_arrays_iterations.ts index 4724e7b7..70aba5ee 100644 --- a/StrataTest/Languages/TypeScript/test_arrays_iterations.ts +++ b/StrataTest/Languages/TypeScript/test_arrays_iterations.ts @@ -6,4 +6,9 @@ arr.forEach((value: number, index: number) => { }); // map -let mappedArr = arr.map((value: number) => {return value + 1}); \ No newline at end of file +let mappedArr = arr.map((value: number) => {return value + 1}); + +// filter +let filteredArr = arr.filter((value: number) => { + return value > 5; +});