Add support to type guards

Strata/DL/Heap/HEval.lean

@@ -149,6 +149,15 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE
     -- Third application to DynamicFieldAssign - now we can evaluate
     -- This handles obj[field] = value where field is dynamic
     evalDynamicFieldAssign state2 objExpr fieldExpr e2'
+  | .deferredOp "DynamicFieldAssignReturnObj" _ =>
+    -- First application to DynamicFieldAssignReturnObj - return partially applied
+    (state2, .app (.deferredOp "DynamicFieldAssignReturnObj" none) e2')
+  | .app (.deferredOp "DynamicFieldAssignReturnObj" _) objExpr =>
+    -- Second application to DynamicFieldAssignReturnObj - return partially applied
+    (state2, .app (.app (.deferredOp "DynamicFieldAssignReturnObj" none) objExpr) e2')
+  | .app (.app (.deferredOp "DynamicFieldAssignReturnObj" _) objExpr) fieldExpr =>
+    -- Third application to DynamicFieldAssignReturnObj - now we can evaluate
+    evalDynamicFieldAssignReturnObj state2 objExpr fieldExpr e2'
   | .deferredOp "StringFieldAccess" _ =>
     -- First application to StringFieldAccess - return partially applied
     (state2, .app (.deferredOp "StringFieldAccess" none) e2')
@@ -170,6 +179,31 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE
     -- This handles delete obj[field] where field is dynamic
     evalFieldDelete state2 objExpr e2'
 
+  | .deferredOp "TypeOf" _ =>
+    -- Unary typeof operator
+    let result : HExpr :=
+      match e2' with
+      | .address _ =>
+        HExpr.string "object"
+      | .null =>
+        HExpr.string "object"
+      | .lambda (LExpr.const _ (some Lambda.LMonoTy.int)) =>
+        HExpr.string "number"
+      | .lambda (LExpr.const _ (some Lambda.LMonoTy.bool)) =>
+        HExpr.string "boolean"
+      | .lambda (LExpr.const _ (some Lambda.LMonoTy.string)) =>
+        HExpr.string "string"
+      | .lambda (LExpr.const _ _) =>
+        HExpr.string "undefined"
+      | _ =>
+        HExpr.string "undefined"
+    (state2, result)
+
+  | .deferredOp "InstanceOf" _ =>
+    (state2, .app (.deferredOp "InstanceOf" none) e2')
+  | .app (.deferredOp "InstanceOf" _) lhsExpr =>
+    evalInstanceOf state2 lhsExpr e2'
+
   | .deferredOp op _ =>
     -- First application to a deferred operation - return partially applied
     (state2, .app (.deferredOp op none) e2')
@@ -193,25 +227,69 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE
 
 -- Handle dynamic field access: obj[field] where field is dynamic
 partial def evalDynamicFieldAccess (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, use regular deref
-    evalHExpr state (.deref objExpr fieldIndex)
-  | none =>
-    -- Can't extract a numeric field index, return error
-    (state, .lambda (LExpr.const "error_dynamic_field_access_failed" none))
+  let (s1, objVal) := evalHExpr state objExpr
+  let (s2, keyVal) := evalHExpr s1 fieldExpr
+  match objVal with
+  | .address addr =>
+    match keyVal with
+    | .lambda (LExpr.const k _) =>
+      match k.toNat? with
+      | some n =>
+        match s2.getField addr n with
+        | some v => (s2, v)
+        | none   => (s2, .lambda (LExpr.const s!"error_field_{n}_not_found" none))
+      | none =>
+        match s2.getStringField addr k with
+        | some v => (s2, v)
+        | none   => (s2, .lambda (LExpr.const s!"error_string_field_{k}_not_found" none))
+    | _ => (s2, .lambda (LExpr.const "error_invalid_field_key" none))
+  | .null => (s2, .lambda (LExpr.const "error_null_dereference" none))
+  | _     => (s2, .lambda (LExpr.const "error_invalid_address" none))
 
 -- Handle dynamic field assignment: obj[field] = value where field is dynamic
 partial def evalDynamicFieldAssign (state : HState) (objExpr fieldExpr valueExpr : 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, use regular assign
-    evalHExpr state (.assign objExpr fieldIndex valueExpr)
-  | none =>
-    -- Can't extract a numeric field index, return error
-    (state, .lambda (LExpr.const "error_dynamic_field_assign_failed" none))
+  let (s1, objVal) := evalHExpr state objExpr
+  let (s2, keyVal) := evalHExpr s1 fieldExpr
+  let (s3, valVal) := evalHExpr s2 valueExpr
+  match objVal with
+  | .address addr =>
+    match keyVal with
+    | .lambda (LExpr.const k _) =>
+      match k.toNat? with
+      | some n =>
+        match s3.setField addr n valVal with
+        | some s' => (s', valVal)
+        | none    => (s3, .lambda (LExpr.const s!"error_cannot_update_field_{n}" none))
+      | none =>
+        match s3.setStringField addr k valVal with
+        | some s' => (s', valVal)
+        | none    => (s3, .lambda (LExpr.const s!"error_cannot_update_string_field_{k}" none))
+    | _ => (s3, .lambda (LExpr.const "error_invalid_field_key" none))
+  | .null => (s3, .lambda (LExpr.const "error_null_assignment" none))
+  | _     => (s3, .lambda (LExpr.const "error_invalid_address_assignment" none))
+
+-- Handle dynamic field assignment but return the *object address* to allow chaining
+partial def evalDynamicFieldAssignReturnObj (state : HState) (objExpr fieldExpr valueExpr : HExpr) : HState × HExpr :=
+  let (s1, objVal) := evalHExpr state objExpr
+  let (s2, keyVal) := evalHExpr s1 fieldExpr
+  let (s3, valVal) := evalHExpr s2 valueExpr
+  match objVal with
+  | .address addr =>
+    match keyVal with
+    | .lambda (LExpr.const k _) =>
+      match k.toNat? with
+      | some n =>
+        match s3.setField addr n valVal with
+        | some s' => (s', .address addr)
+        | none    => (s3, .lambda (LExpr.const s!"error_cannot_update_field_{n}" none))
+      | none =>
+        match s3.setStringField addr k valVal with
+        | some s' => (s', .address addr)
+        | none    => (s3, .lambda (LExpr.const s!"error_cannot_update_string_field_{k}" none))
+    | _ => (s3, .lambda (LExpr.const "error_invalid_field_key" none))
+  | .null => (s3, .lambda (LExpr.const "error_null_assignment" none))
+  | _     => (s3, .lambda (LExpr.const "error_invalid_address_assignment" none))
+
 
 -- Handle string field access: str.fieldName where fieldName is a string literal
 partial def evalStringFieldAccess (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr :=
@@ -288,7 +366,6 @@ partial def evalLengthAccess (state : HState) (objExpr fieldExpr : HExpr) : HSta
 partial def extractFieldIndex (expr : HExpr) : Option Nat :=
   match expr with
   | .lambda (LExpr.const s _) =>
-    -- Try to parse the string as a natural number
     s.toNat?
   | _ => none
 
@@ -305,6 +382,18 @@ partial def evalBinaryOp (state : HState) (op : String) (arg1 arg2 : HExpr) : HS
     -- Partial evaluation - keep as deferred operation
     (state, .app (.app (.deferredOp op none) arg1) arg2)
 
+partial def evalInstanceOf (state : HState) (lhs rhs : HExpr) : HState × HExpr :=
+  let (s1, v)   := evalHExpr state lhs
+  let (s2, _) := evalHExpr s1 rhs
+
+  let result : HExpr :=
+    match v with
+    | .address _ => Heap.HExpr.true
+    | .null      => Heap.HExpr.false
+    | _          => Heap.HExpr.false
+
+  (s2, result)
+
 end
 
 -- Convenience function for evaluation
@@ -318,6 +407,25 @@ namespace HExpr
 def allocSimple (fields : List (Nat × HExpr)) : HExpr :=
   .alloc (HMonoTy.mkObj fields.length HMonoTy.int) fields
 
+def dynamicAssign (obj : HExpr) (key : HExpr) (val : HExpr) : HExpr :=
+  HExpr.app
+    (HExpr.app
+      (HExpr.app (HExpr.deferredOp "DynamicFieldAssign" none) obj)
+      key)
+    val
+
+/-- Like `dynamicAssign`, but evaluates to the *object* so it can be chained. --/
+def dynamicAssignReturnObj (obj : HExpr) (key : HExpr) (val : HExpr) : HExpr :=
+  HExpr.app
+    (HExpr.app
+      (HExpr.app (HExpr.deferredOp "DynamicFieldAssignReturnObj" none) obj)
+      key)
+    val
+
+def dynamicAlloc (numFields : List (Nat × HExpr)) (dynFields : List (HExpr × HExpr)) : HExpr :=
+  let obj0 := allocSimple numFields
+  dynFields.foldl (fun acc (k, v) => dynamicAssignReturnObj acc k v) obj0
+
 end HExpr
 
 end Heap

Strata/DL/Heap/HState.lean

@@ -34,6 +34,10 @@ abbrev HeapMemory := Std.HashMap Address HeapObject
 -- Heap variable environment - maps variable names to (type, value) pairs
 abbrev HeapVarEnv := Std.HashMap String (HMonoTy × HExpr)
 
+-- String-keyed fields for objects
+abbrev StringFieldMap := Std.HashMap String HExpr
+abbrev StringFields := Std.HashMap Nat StringFieldMap
+
 /--
 Heap State extending Lambda state with heap memory and heap variable environment.
 -/
@@ -46,9 +50,11 @@ structure HState where
   nextAddr : Address
   -- Heap variable environment (parallel to Lambda's variable environment)
   heapVars : HeapVarEnv
+  -- String-keyed fields: address -> (key -> value)
+  stringFields : StringFields
 
 instance : Repr HState where
-  reprPrec s _ := s!"HState(nextAddr: {s.nextAddr}, heap: <{s.heap.size} objects>, heapVars: <{s.heapVars.size} vars>)"
+  reprPrec s _ := s!"HState(nextAddr: {s.nextAddr}, heap: <{s.heap.size} objects>, heapVars: <{s.heapVars.size} vars>, stringFields: <{s.stringFields.size} props>)"
 
 namespace HState
 
@@ -81,9 +87,10 @@ def empty : HState :=
     | .ok state => state
     | .error _ => lambdaState  -- Fallback to basic state if factory addition fails
   { lambdaState := lambdaStateWithFactory,
-    heap := Std.HashMap.empty,
+    heap := Std.HashMap.emptyWithCapacity,
     nextAddr := 1,  -- Start addresses from 1 (0 can represent null)
-    heapVars := Std.HashMap.empty }
+    heapVars := Std.HashMap.emptyWithCapacity,
+    stringFields := Std.HashMap.emptyWithCapacity }
 
 -- Heap Variable Environment Operations
 
@@ -173,6 +180,19 @@ def deleteField (state : HState) (addr : Address) (field : Nat) : Option HState
     some { state with heap := newHeap }
   | none => none
 
+-- String field operations (for objects with string-keyed fields)
+def getStringField (s : HState) (addr : Nat) (key : String) : Option HExpr :=
+  match s.stringFields.get? addr with
+  | some m => m.get? key
+  | none => none
+
+-- Set a string field in an object
+def setStringField (s : HState) (addr : Nat) (key : String) (val : HExpr) : Option HState :=
+  let existing : StringFieldMap := (s.stringFields.get? addr).getD (Std.HashMap.emptyWithCapacity)
+  let updated := existing.insert key val
+  some { s with stringFields := s.stringFields.insert addr updated }
+
+
 -- Check if an address is valid (exists in heap)
 def isValidAddr (state : HState) (addr : Address) : Bool :=
   state.heap.contains addr
@@ -198,6 +218,29 @@ def heapVarsToString (state : HState) : String :=
 def toString (state : HState) : String :=
   s!"{state.heapToString}\n{state.heapVarsToString}"
 
+-- Return all string-keyed fields for an address as an association list
+def getAllStringFields (s : HState) (addr : Nat) : List (String × HExpr) :=
+  match s.stringFields.get? addr with
+  | some m => m.toList
+  | none => []
+
+-- Return all fields (numeric and string) as string-keyed pairs
+def getAllFieldsAsStringPairs (s : HState) (addr : Nat) : List (String × HExpr) :=
+  let numeric : List (String × HExpr) :=
+    match s.getObject addr with
+    | some obj => obj.toList.map (fun (i, v) => (s!"{i}", v))
+    | none => []
+  let strk   : List (String × HExpr) := s.getAllStringFields addr
+  -- string keys should override numeric if the same string exists
+  let merged := Id.run do
+    let mut map : Std.HashMap String HExpr := Std.HashMap.emptyWithCapacity
+    for (k, v) in numeric do
+      map := map.insert k v
+    for (k, v) in strk do
+      map := map.insert k v
+    pure map
+  merged.toList
+
 end HState
 
 end Heap

Strata/DL/Heap/HeapStrataEval.lean

@@ -151,21 +151,16 @@ mutual
     | _ => none  -- Other expressions not supported yet
 
   partial def extractObjectAsJson (state : HState) (addr : Address) : Option Lean.Json :=
-    match state.getObject addr with
-    | some obj =>
-      -- Convert heap object (field index -> HExpr) to JSON object
-      let fields := obj.toList
-      let jsonFields := fields.filterMap fun (fieldIndex, fieldExpr) =>
-        match extractConcreteValueWithState state fieldExpr with
-        | some fieldJson =>
-          -- Use field index as string key for now
-          some (toString fieldIndex, fieldJson)
-        | none => none
-
-      -- Sort fields by key for consistency
-      let sortedFields := jsonFields.toArray.qsort (fun a b => a.1 < b.1) |>.toList
-      some (Lean.Json.mkObj sortedFields)
-    | none => none
+    -- Merge numeric fields and string-keyed fields from the heap
+    let pairs : List (String × HExpr) := state.getAllFieldsAsStringPairs addr
+    -- Encode each field value recursively
+    let jsonFields : List (String × Lean.Json) := pairs.filterMap fun (k, v) =>
+      match extractConcreteValueWithState state v with
+      | some j => some (k, j)
+      | none   => none
+    -- Sort for stable output
+    let sortedFields := jsonFields.toArray.qsort (fun a b => a.1 < b.1) |>.toList
+    some (Lean.Json.mkObj sortedFields)
 
   -- Legacy function for backward compatibility
   partial def extractConcreteValue (expr : HExpr) : Option String :=