Skip to content

[feat] Add support to arr.filter() (including foreach, map) #192

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
andrewmwells-amazon merged 2 commits into from
Dec 5, 2025
Merged

[feat] Add support to arr.filter() (including foreach, map) #192

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b836477
[feat] Add support to arr.filter() (including foreach, map)
Ex10si0n Oct 8, 2025
fe2f4cb
Merge branch 'typescript-frontend' into array-filter
zhiyuuuu Dec 2, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
211 changes: 183 additions & 28 deletions Strata/Languages/TypeScript/TS_to_Strata.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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, [])
Expand Down Expand Up @@ -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,
Expand All @@ -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 :=
Expand Down
7 changes: 6 additions & 1 deletion StrataTest/Languages/TypeScript/test_arrays_iterations.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,9 @@ arr.forEach((value: number, index: number) => {
});

// map
let mappedArr = arr.map((value: number) => {return value + 1});
let mappedArr = arr.map((value: number) => {return value + 1});

// filter
let filteredArr = arr.filter((value: number) => {
return value > 5;
});
Loading