Ex10si0n/array

Strata/Languages/TypeScript/TS_to_Strata.lean

@@ -65,7 +65,7 @@ def TS_type_to_HMonoTy (ty: String) : Heap.HMonoTy :=
   | "TS_TSNumberKeyword" => Heap.HMonoTy.int
   | "TS_TSBooleanKeyword" => Heap.HMonoTy.bool
   | "TS_TSStringKeyword" => Heap.HMonoTy.string
-  -- | "TS_TSArrayType" => Heap.HMonoTy.addr
+  | "TS_TSArrayType" => Heap.HMonoTy.addr
   | _ => panic! s!"Unsupported type: {ty}"
 
 def Option_TS_TSTypeKeyword_to_str (i: Option TS_TSTypeKeyword) : String :=
@@ -74,7 +74,7 @@ def Option_TS_TSTypeKeyword_to_str (i: Option TS_TSTypeKeyword) : String :=
     | .TS_TSNumberKeyword _ => "TS_TSNumberKeyword"
     | .TS_TSBooleanKeyword _ => "TS_TSBooleanKeyword"
     | .TS_TSStringKeyword _ => "TS_TSStringKeyword"
-    -- | .TS_TSArrayType _ => "TS_TSArrayType"
+    | .TS_TSArrayType _ => "TS_TSArrayType"
   | .none => panic! "Unimplemented"
 
 -- Helper to extract type from optional type annotation
@@ -87,7 +87,7 @@ def extract_type_from_annotation (ann: Option TS_TSTypeAnnotation) : String :=
 partial def infer_type_from_expr (expr: TS_Expression) : Heap.HMonoTy :=
   match expr with
   | .TS_ObjectExpression _ => Heap.HMonoTy.addr  -- Objects are addresses
-  -- | .TS_ArrayExpression _ => Heap.HMonoTy.addr   -- Arrays are addresses
+  | .TS_ArrayExpression _ => Heap.HMonoTy.addr   -- Arrays are addresses
   | .TS_NumericLiteral _ => Heap.HMonoTy.int
   | .TS_BooleanLiteral _ => Heap.HMonoTy.bool
   | .TS_BinaryExpression e =>
@@ -159,12 +159,12 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr :=
   | .TS_NullLiteral _ =>
     Heap.HExpr.null
 
-  -- | .TS_ArrayExpression arr =>
-    -- -- Translate [value1, value2, value3] to heap allocation with numeric indices
-    -- let fields := arr.elements.toList.mapIdx (fun idx elem =>
-      -- (idx, translate_expr elem))
-    -- -- Arrays store elements at numeric indices: 0->value1, 1->value2, etc.
-    -- Heap.HExpr.allocSimple fields
+  | .TS_ArrayExpression arr =>
+    -- Translate [value1, value2, value3] to heap allocation with numeric indices
+    let fields := arr.elements.toList.mapIdx (fun idx elem =>
+      (idx, translate_expr elem))
+    -- Arrays store elements at numeric indices: 0->value1, 1->value2, etc.
+    Heap.HExpr.allocSimple fields
 
   | .TS_MemberExpression e =>
     -- Translate obj[index] to heap dereference

Strata/Languages/TypeScript/js_ast.lean

@@ -45,13 +45,13 @@ mutual
     | TS_TSNumberKeyword : TS_TSNumberKeyword → TS_TSTypeKeyword
     | TS_TSBooleanKeyword : TS_TSBooleanKeyword → TS_TSTypeKeyword
     | TS_TSStringKeyword : TS_TSStringKeyword → TS_TSTypeKeyword
-    -- | TS_TSArrayType : TS_TSArrayType → TS_TSTypeKeyword
+    | TS_TSArrayType : TS_TSArrayType → TS_TSTypeKeyword
   deriving Repr, Lean.FromJson, Lean.ToJson
 
   -- TODO: Array not as a type?
-  -- structure TS_TSArrayType extends BaseNode where
-    -- elementType : TS_TSTypeKeyword
-  -- deriving Repr, Lean.FromJson, Lean.ToJson
+  structure TS_TSArrayType extends BaseNode where
+    elementType : TS_TSTypeKeyword
+  deriving Repr, Lean.FromJson, Lean.ToJson
 end
 
 structure TS_TSTypeAnnotation extends BaseNode where
@@ -144,9 +144,9 @@ mutual
     properties: Array TS_ObjectProperty
   deriving Repr, Lean.FromJson, Lean.ToJson
 
-  -- structure TS_ArrayExpression extends BaseNode where
-    -- elements : Array TS_Expression
-  -- deriving Repr, Lean.FromJson, Lean.ToJson
+  structure TS_ArrayExpression extends BaseNode where
+    elements : Array TS_Expression
+  deriving Repr, Lean.FromJson, Lean.ToJson
 
   structure TS_CallExpression extends BaseNode where
     callee : TS_Identifier
@@ -165,7 +165,7 @@ mutual
     | TS_IdExpression : TS_Identifier → TS_Expression
     | TS_UnaryExpression: TS_UnaryExpression → TS_Expression
     | TS_ObjectExpression: TS_ObjectExpression → TS_Expression
-    -- | TS_ArrayExpression: TS_ArrayExpression → TS_Expression
+    | TS_ArrayExpression: TS_ArrayExpression → TS_Expression
     | TS_MemberExpression: TS_MemberExpression → TS_Expression
     | TS_CallExpression: TS_CallExpression → TS_Expression
   deriving Repr, Lean.FromJson, Lean.ToJson

StrataTest/Languages/TypeScript/test_arrays.ts

@@ -0,0 +1,29 @@
+// Basic array literal
+// TODO: add assertion tests AST test + verification test (as a user) pre/post-condi
+let numbers: number[] = [1, 2, 3, 4, 5];
+
+// Empty array initialization
+let empty: number[] = [];
+
+// Array element access
+let first: number = numbers[0];
+let last: number = numbers[4];
+
+// Dynamic array indexing
+let index: number = 2;
+let element: number = numbers[index];
+
+// Array element assignment
+numbers[0] = 10;
+numbers[index] = 30;
+
+// Array in expressions
+let sum: number = numbers[0] + numbers[1];
+let isEqual: boolean = numbers[2] == 3
+
+// Mixed with objects
+// let data: number[] = [100, 200, 300];
+// let obj = {0: data[0], 1: data[1], 2: data[2]};
+
+// Nested arrays
+// let matrix: number[][] = [[1, 2], [3, 4]];

conformance_testing/babel_to_lean.py

@@ -13,26 +13,44 @@ def add_missing_node_info(source_j, target_j):
         if source_key not in target_j:
             target_j[source_key] = source_j[source_key]
 
+
+def parse_ts_type(j):
+    """
+    Parse a Babel TS type node into the tagged union Lean expects.
+    Returns either a tagged dict (e.g. {"TS_TSNumberKeyword": {...}})
+    or None (for TSAnyKeyword / missing).
+    """
+    if j is None:
+        return None
+    t = j.get('type')
+    if t == "TSNumberKeyword":
+        return {"TS_TSNumberKeyword": j}
+    elif t == "TSBooleanKeyword":
+        return {"TS_TSBooleanKeyword": j}
+    elif t == "TSStringKeyword":
+        return {"TS_TSStringKeyword": j}
+    elif t == "TSArrayType":
+        # Recursively tag the elementType
+        elem = j.get('elementType')
+        tagged_elem = parse_ts_type(elem) if elem is not None else None
+        inner = {"elementType": tagged_elem}
+        add_missing_node_info(j, inner)
+        return {"TS_TSArrayType": inner}
+    elif t == "TSAnyKeyword" or t is None:
+        return None
+    else:
+        print("Unsupported type annotation type: " + str(t), file=sys.stderr)
+        return None
+
+
 def parse_type_annotation(j):
-    innerTypeAnnotation = None
-    match j['typeAnnotation'].get('type'):
-        case "TSNumberKeyword":
-            innerTypeAnnotation = {"TS_TSNumberKeyword": j['typeAnnotation']}
-        case "TSBooleanKeyword":
-            innerTypeAnnotation = {"TS_TSBooleanKeyword": j['typeAnnotation']}
-        case "TSAnyKeyword":
-            # TODO: Is TSAnyKeyword different than not stating any type?
-            innerTypeAnnotation = None
-        case None:
-            innerTypeAnnotation = None
-        case _:
-            print("Unsupported type annotation type: " + j['typeAnnotation'].get('type'), file=sys.stderr)
-    target_j = {
-        "typeAnnotation": innerTypeAnnotation
-    }
+    # j is a TSTypeAnnotation node; its 'typeAnnotation' holds the inner TS* node
+    inner = j.get('typeAnnotation')
+    tagged = parse_ts_type(inner) if inner is not None else None
+    target_j = {"typeAnnotation": tagged}
     add_missing_node_info(j, target_j)
     return target_j
-    
+
 
 def parse_binary_expression(j):
     target_j = {
@@ -115,6 +133,16 @@ def parse_member_expression(j):
     add_missing_node_info(j, target_j)
     return target_j
 
+def parse_array_expression(j):
+    # Normalize Babel ArrayExpression: keep only non-null elements and parse each
+    elems = []
+    for e in j.get('elements', []):
+        if e is not None:
+            elems.append(parse_expression(e))
+    target_j = {"elements": elems}
+    add_missing_node_info(j, target_j)
+    return target_j
+
 def parse_expression(j):
     match j['type']:
         case "Identifier":
@@ -148,7 +176,8 @@ def parse_expression(j):
         # case "ArrowFunctionExpression":
         # case "YieldExpression":
         # case "AwaitExpression":
-        # case "ArrayExpression":
+        case "ArrayExpression":
+            return {"TS_ArrayExpression": parse_array_expression(j)}
         # case "RecordExpression":
         # case "TupleExpression":
         # case "FunctionExpression":

conformance_testing/unified_conformance.py

@@ -19,6 +19,12 @@
 
 from language_processor import get_language_processor, LanguageProcessor
 
+def _to_strata_heap_value(v):
+    if isinstance(v, list):
+        return {str(i): _to_strata_heap_value(x) for i, x in enumerate(v)}
+    if isinstance(v, dict):
+        return {k: _to_strata_heap_value(x) for k, x in v.items()}
+    return v
 
 class ConformanceTestRunner:
     """Language-neutral conformance test runner."""
@@ -55,6 +61,8 @@ def compare_outputs(self, native_json: str, strata_json: str) -> Tuple[bool, str
             print("strata json", strata_json)
             native_data = json.loads(native_json.strip())
             strata_data = json.loads(strata_json.strip())
+
+            native_data = {k: _to_strata_heap_value(v) for k, v in native_data.items()}
 
             mismatches = []
             missing_keys = []