add for-in for-of support

Strata/DL/Heap/HEval.lean

@@ -156,6 +156,55 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE
     -- Second application to StringFieldAccess - return partially applied
     -- This handles str.fieldName where fieldName is a string literal
     evalStringFieldAccess state2 objExpr e2'
+  | .deferredOp "LengthAccess" _ =>
+    -- First application to LengthAccess - return partially applied
+    (state2, .app (.deferredOp "LengthAccess" none) e2')
+  | .app (.deferredOp "LengthAccess" _) objExpr =>
+    -- Second application to LengthAccess - evaluate
+    evalLengthAccess state2 objExpr e2'
+  | .deferredOp "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'
+
+  -- 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 "ArrayShift" _ =>
+    -- ArrayShift applied once - now we can evaluate
+    evalArrayShift state2 e2'
+  | .deferredOp "ObjectKeys" _ =>
+    -- ObjectKeys applied once - now we can evaluate
+    evalObjectKeys state2 e2'
+  | .deferredOp "ArrayUnshift" _ =>
+    -- First application to ArrayUnshift - return partially applied
+    (state2, .app (.deferredOp "ArrayUnshift" none) e2')
+  | .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 "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')
@@ -219,7 +268,261 @@ partial def evalStringFieldAccess (state : HState) (objExpr fieldExpr : HExpr) :
     -- Field is not a string literal
     (state, .lambda (LExpr.const "error_non_literal_string_field" none))
 
--- Extract a numeric field index from an expression
+
+-- 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
+  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 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 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))
+  | _ =>
+    -- Evaluate object expression first
+    let (state1, objVal) := evalHExpr state objExpr
+    evalArrayShift state1 objVal
+
+partial def evalObjectKeys (state : HState) (objExpr : HExpr) : HState × HExpr :=
+  match objExpr with
+  | .address addr =>
+    match state.getObject addr with
+    | some obj =>
+      -- Get all field indices and sort them
+      let indices := obj.toList.map (·.1) |>.toArray.qsort (· < ·)
+
+      -- Create array with indices as integer values
+      let keyFields := indices.toList.mapIdx fun arrayIdx fieldIdx =>
+        (arrayIdx, .lambda (LExpr.const (toString fieldIdx) (some Lambda.LMonoTy.int)))
+
+      -- Allocate new array with the keys
+      let (newState, newAddr) := state.alloc keyFields
+      (newState, .address newAddr)
+    | none => (state, .lambda (LExpr.const "error_invalid_address" none))
+  | _ =>
+    -- Evaluate object expression first
+    let (state1, objVal) := evalHExpr state objExpr
+    evalObjectKeys state1 objVal
+
+-- Handle array unshift: arr.unshift(value) - adds element at beginning and reindexes
+partial def evalArrayUnshift (state : HState) (objExpr valueExpr : HExpr) : HState × HExpr :=
+  match objExpr with
+  | .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
+
+-- 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))
+
+-- 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 _) =>
@@ -255,4 +558,4 @@ def allocSimple (fields : List (Nat × HExpr)) : HExpr :=
 
 end HExpr
 
-end Heap
+end Heap

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,6 +161,16 @@ 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 :=
+  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 }
+  | none => none
+
 -- Check if an address is valid (exists in heap)
 def isValidAddr (state : HState) (addr : Address) : Bool :=
   state.heap.contains addr
@@ -169,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
@@ -188,4 +209,4 @@ def toString (state : HState) : String :=
 
 end HState
 
-end Heap
+end Heap