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

Author: Ex10si0n

Strata/DL/Heap/HEval.lean

@@ -156,6 +156,20 @@ 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'
+
   | .deferredOp op _ =>
     -- First application to a deferred operation - return partially applied
     (state2, .app (.deferredOp op none) e2')
@@ -219,6 +233,57 @@ 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 :=
+  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

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