[feat] Add support to object string properties

Author: zhiyuuuu

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')
@@ -179,25 +188,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 :=
@@ -223,7 +276,6 @@ partial def evalStringFieldAccess (state : HState) (objExpr fieldExpr : HExpr) :
 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
 
@@ -253,6 +305,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
 
@@ -161,6 +168,18 @@ def setField (state : HState) (addr : Address) (field : Nat) (value : HExpr) : O
     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
@@ -186,6 +205,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 :=

Strata/Languages/TypeScript/TS_to_Strata.lean

@@ -191,15 +191,25 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr :=
       Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) fieldExpr
 
   | .TS_ObjectExpression e =>
-    -- Translate {1: value1, 5: value5} to heap allocation
-    let fields := e.properties.toList.map (fun prop =>
-      let key := match prop.key with
-        | .TS_NumericLiteral numLit => Float.floor numLit.value |>.toUInt64.toNat
-        | _ => panic! s!"Expected numeric literal as object key, got: {repr prop.key}"
-      let value := translate_expr prop.value
-      (key, value))
-    -- Use allocSimple which handles the object type automatically
-    Heap.HExpr.allocSimple fields
+    -- Collect numeric props for allocSimple, and *one* list of dynamic (keyExpr,valueExpr)
+    let (numProps, dynProps) :=
+      e.properties.toList.foldl
+        (fun (ns, ds) prop =>
+          let v := translate_expr prop.value
+          match prop.key with
+          | .TS_NumericLiteral numLit =>
+              let idx := Float.floor numLit.value |>.toUInt64.toNat
+              ((idx, v) :: ns, ds)
+          | .TS_StringLiteral strLit =>
+              -- unify: string-literal key becomes a constant string expression
+              (ns, (Heap.HExpr.string strLit.value, v) :: ds)
+          | other =>
+              -- computed or identifier: translate to an expr
+              (ns, (translate_expr other, v) :: ds))
+        ([], [])
+
+    let obj := Heap.HExpr.dynamicAlloc (numProps.reverse) (dynProps.reverse)
+    obj
 
   | .TS_CallExpression call =>
     -- Handle function calls - translate to expressions for now

StrataTest/Languages/TypeScript/test_obj_string_prop.ts

@@ -0,0 +1,6 @@
+// Test objects with string key-value
+let str_obj = {
+    "name": "Strata",
+    "type": "Testing",
+    "version": "1.0"
+}