diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean index 9ff3ab2ed..f6bf6d26c 100644 --- a/Strata/DL/Heap/HEval.lean +++ b/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 diff --git a/Strata/DL/Heap/HState.lean b/Strata/DL/Heap/HState.lean index 4935049fc..9395804df 100644 --- a/Strata/DL/Heap/HState.lean +++ b/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 diff --git a/Strata/DL/Heap/HeapStrataEval.lean b/Strata/DL/Heap/HeapStrataEval.lean index ba2642eab..117ec1315 100644 --- a/Strata/DL/Heap/HeapStrataEval.lean +++ b/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 := diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean index 8d82e3776..7d3cd0682 100644 --- a/Strata/Languages/TypeScript/TS_to_Strata.lean +++ b/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 diff --git a/StrataTest/Languages/TypeScript/test_obj_string_prop.ts b/StrataTest/Languages/TypeScript/test_obj_string_prop.ts new file mode 100644 index 000000000..aa8163c1a --- /dev/null +++ b/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" +} \ No newline at end of file