Add Typescript Basic features (#141)

*Issue #, if available:*

*Description of changes:*
Batch of changes from CMU Practicum students to support TS.

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Signed-off-by: YingZhu <yingzhu3@andrew.cmu.edu>
Co-authored-by: YingZhu <yingzhu3@andrew.cmu.edu>
Co-authored-by: ygrx532 <xiayuyang_1506@outlook.com>
Co-authored-by: ex10si0n <me@aspires.cc>

Author: 4 people

.gitignore

@@ -5,3 +5,10 @@
 vcs/*.smt2
 
 Strata.code-workspace
+
+conformance_testing/failures/*
+package.json
+package-lock.json
+
+conformance_testing/__pycache__
+conformance_testing/failures

Strata/DL/CallHeap/CallHeapEvaluator.lean

@@ -169,8 +169,19 @@ partial def evalStatementWithContext (stmt : CallHeapStrataStatement) (ctx : Cal
       ctx
     | .goto _ _ =>
       ctx
-    | .loop _ _ _ _ _ =>
-      ctx
+    | .loop guard _ _ body _ =>
+      let rec loop (ctx : CallHeapEvalContext) : CallHeapEvalContext :=
+      let (newState, condVal) := Heap.evalHExpr ctx.hstate guard
+      let conditionIsTrue := match condVal with
+        | .lambda (.const "true" _) => true
+        | _ => false
+      let newCtx := { ctx with hstate := newState }
+      if conditionIsTrue then
+        let afterBody := evalProgramWithContext body.ss newCtx
+        loop afterBody
+      else
+        newCtx
+    loop ctx
     | _ =>
       ctx
 
@@ -194,7 +205,9 @@ def evalCallHeapTranslatedProgram (transCtx : CallHeapTranslationContext) (stmts
   evalProgramWithContext stmts evalCtx
 
 -- JSON output function with TranslationContext (matching MIDI pattern)
-def runCallHeapAndShowJSONWithTranslation (transCtx : CallHeapTranslationContext) (stmts : List CallHeapStrataStatement) : IO Unit := do
+def runCallHeapAndShowJSONWithTranslation (transCtx : CallHeapTranslationContext)
+    (stmts : List CallHeapStrataStatement)
+    (visibleVars : Option (Std.HashSet String) := none) : IO Unit := do
   let finalContext := evalCallHeapTranslatedProgram transCtx stmts
   let finalState := finalContext.hstate
 
@@ -221,8 +234,12 @@ def runCallHeapAndShowJSONWithTranslation (transCtx : CallHeapTranslationContext
       | none => continue
     | none => continue
 
+  -- Optionally filter the visible variables to match a provided allowlist
   -- Create JSON object and output (sorted for consistency)
-  let sortedFields := jsonFields.toArray.qsort (fun a b => a.1 < b.1) |>.toList
+  let filteredFields : List (String × Lean.Json) := match visibleVars with
+    | some allowed => jsonFields.filter (fun (name, _) => allowed.contains name)
+    | none => jsonFields
+  let sortedFields := filteredFields.toArray.qsort (fun a b => a.1 < b.1) |>.toList
   let jsonObj := Lean.Json.mkObj sortedFields
   IO.println jsonObj.compress  -- Use compress for compact output like {"x": 5, "y": 15}
 

Strata/DL/Heap/HEval.lean

@@ -149,6 +149,13 @@ 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 "StringFieldAccess" _ =>
+    -- First application to StringFieldAccess - return partially applied
+    (state2, .app (.deferredOp "StringFieldAccess" none) e2')
+  | .app (.deferredOp "StringFieldAccess" _) objExpr =>
+    -- Second application to StringFieldAccess - return partially applied
+    -- This handles str.fieldName where fieldName is a string literal
+    evalStringFieldAccess state2 objExpr e2'
   | .deferredOp op _ =>
     -- First application to a deferred operation - return partially applied
     (state2, .app (.deferredOp op none) e2')
@@ -192,6 +199,26 @@ partial def evalDynamicFieldAssign (state : HState) (objExpr fieldExpr valueExpr
     -- Can't extract a numeric field index, return error
     (state, .lambda (LExpr.const "error_dynamic_field_assign_failed" none))
 
+-- Handle string field access: str.fieldName where fieldName is a string literal
+partial def evalStringFieldAccess (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr :=
+  match fieldExpr with
+  | .lambda (LExpr.const key _) =>
+    if key == "length" then
+      -- Handle string length property
+      match objExpr with
+      | .lambda (LExpr.const s _) =>
+        let len := s.length
+        (state, .lambda (LExpr.const (toString len) (some Lambda.LMonoTy.int)))
+      | _ =>
+        -- Not a string value
+        (state, .lambda (LExpr.const "error_not_a_string" none))
+    else
+      -- Unknown string property
+      (state, .lambda (LExpr.const "error_unknown_string_property" none))
+  | _ =>
+    -- Field is not a string literal
+    (state, .lambda (LExpr.const "error_non_literal_string_field" none))
+
 -- Extract a numeric field index from an expression
 partial def extractFieldIndex (expr : HExpr) : Option Nat :=
   match expr with

Strata/DL/Lambda/IntBoolFactory.lean

@@ -139,6 +139,10 @@ def intGeFunc [Coe String Ident] : LFunc Ident :=
   binaryPredicate "Int.Ge" .int
   (some (binOpCeval Int Bool LExpr.denoteInt (fun x y => x >= y) .bool))
 
+def intEqFunc [Coe String Ident] : LFunc Ident :=
+  binaryPredicate "Int.Eq" .int
+  (some (binOpCeval Int Bool LExpr.denoteInt (fun x y => x == y) .bool))
+
 /- Boolean Operations -/
 def boolAndFunc [Coe String Ident] : LFunc Ident :=
   binaryOp "Bool.And" .bool
@@ -172,6 +176,7 @@ def IntBoolFactory : @Factory String :=
     intLeFunc,
     intGtFunc,
     intGeFunc,
+    intEqFunc,
 
     boolAndFunc,
     boolOrFunc,