Yuyang/switch (#21) (#182)

This pull request modifies the compiler support for switch statements.

Modifications

- Introduces complete translation logic for switch statements,
preserving fallthrough, break, and default behaviors.

- Initializes control variables: switch_discriminant_,
switch_fallthrough_, and switch_break_*.

- Defines helpers for splitting at break, translating case bodies, and
building conditional chains.

- Ensures each case conditionally executes based on the discriminant,
fallthrough, and break flags, with deferred evaluation of break to
maintain semantic correctness.

Author: ygrx532

.gitignore

@@ -7,4 +7,6 @@ vcs/*.smt2
 Strata.code-workspace
 
 conformance_testing/__pycache__
-conformance_testing/failures
+conformance_testing/failures
+
+test_single_file.sh

Strata/Languages/TypeScript/TS_to_Strata.lean

@@ -890,50 +890,6 @@ partial def translate_statement_core
           -- output: init break flag, init statements, then a loop statement
           (ctx1, [initBreakFlag] ++ initStmts ++ [ .loop combinedCondition none none loopBody])
 
-        | .TS_SwitchStatement switchStmt =>
-          -- Handle switch statement: switch discriminant { cases }
-
-          -- Process all cases in their original order, separating regular from default
-          let allCases := switchStmt.cases.toList
-          let (regularCaseStmts, defaultStmts) := allCases.foldl (fun (regCases, defStmts) case =>
-            match case.test with
-            | some expr =>
-              -- Regular case
-              let discrimExpr := translate_expr switchStmt.discriminant
-              let caseValue := translate_expr expr
-              let testExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Eq" none) discrimExpr) caseValue
-              let (caseCtx, stmts) := case.consequent.foldl (fun (accCtx, accStmts) stmt =>
-                let (newCtx, newStmts) := translate_statement_core stmt accCtx
-                (newCtx, accStmts ++ newStmts)) (ctx, [])
-              (regCases ++ [(testExpr, stmts)], defStmts)
-            | none =>
-              -- Default case
-              let (defaultCtx, stmts) := case.consequent.foldl (fun (accCtx, accStmts) stmt =>
-                let (newCtx, newStmts) := translate_statement_core stmt accCtx
-                (newCtx, accStmts ++ newStmts)) (ctx, [])
-              (regCases, stmts)
-          ) ([], [])
-
-          -- Build nested if-then-else structure for regular cases
-          let rec build_cases (cases: List (Heap.HExpr × List TSStrataStatement)) (defaultStmts: List TSStrataStatement) : TSStrataStatement :=
-            match cases with
-            | [] =>
-              -- No regular cases, just execute default if it exists
-              let defaultBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := defaultStmts }
-              .block "default" defaultBlock
-            | [(test, stmts)] =>
-              let thenBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := stmts }
-              let elseBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := defaultStmts }
-              .ite test thenBlock elseBlock
-            | (test, stmts) :: rest =>
-              let thenBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := stmts }
-              let elseBlock := build_cases rest defaultStmts
-              let elseBlockWrapped : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [elseBlock] }
-              .ite test thenBlock elseBlockWrapped
-
-          let switchStructure := build_cases regularCaseStmts defaultStmts
-          (ctx, [switchStructure])
-
         | .TS_ContinueStatement cont =>
           let tgt :=
             match ct.continueLabel? with
@@ -958,7 +914,98 @@ partial def translate_statement_core
               | none     => "__unbound_break"
             (ctx, [ .goto tgt ])
 
-        | _ => panic! s!"Unimplemented statement: {repr s}"
+        | .TS_SwitchStatement switchStmt =>
+        -- Handle switch statement with fallthrough and break semantics
+        dbg_trace s!"[DEBUG] Translating switch statement at loc {switchStmt.start_loc}-{switchStmt.end_loc}"
+
+        -- Variables for storing control variables
+        let loc := switchStmt.start_loc
+        let discriminantVar := s!"switch_discriminant_{loc}" -- Stores the switch expression value
+        let fallthroughVar := s!"switch_fallthrough_{loc}" -- Stores fallthrough state
+        let breakFlagVar := s!"switch_break_{loc}" -- Stores break state
+
+        -- Initialize control variables
+        let initDiscriminant : TSStrataStatement := .cmd (.init discriminantVar (infer_type_from_expr switchStmt.discriminant) (translate_expr switchStmt.discriminant))
+        let initFallthrough : TSStrataStatement := .cmd (.init fallthroughVar Heap.HMonoTy.bool Heap.HExpr.false)
+        let initBreakFlag : TSStrataStatement := .cmd (.init breakFlagVar Heap.HMonoTy.bool Heap.HExpr.false)
+
+        -- Helper: split statements at break
+        let splitAtBreak (stmts : List TS_Statement) : List TS_Statement × Bool :=
+          let rec loop acc rest :=
+            match rest with
+            | [] => (acc.reverse, false)
+            | .TS_BreakStatement _ :: _ => (acc.reverse, true)
+            | s :: tail => loop (s :: acc) tail
+          loop [] stmts
+
+        -- Helper: translate case body
+        let translateCaseBody (stmts : List TS_Statement) (caseCtx : TranslationContext) : TranslationContext × List TSStrataStatement :=
+          stmts.foldl (fun (c, acc) stmt =>
+            let (c2, ss) := translate_statement_core stmt c ct
+            (c2, acc ++ ss)) (caseCtx, [])
+
+        -- Helper: build case statements with optional break and fallthrough
+        let buildCaseStmts (caseStmts : List TSStrataStatement) (hasBreak : Bool) (isDefault : Bool) : List TSStrataStatement :=
+          let setFallthrough := .cmd (.set fallthroughVar Heap.HExpr.true)
+          let setBreak := .cmd (.set breakFlagVar Heap.HExpr.true)
+          let stmts := if isDefault then caseStmts else setFallthrough :: caseStmts
+          if hasBreak then stmts ++ [setBreak] else stmts
+
+        -- Flag references
+        let breakFlagRef := Heap.HExpr.lambda (.fvar breakFlagVar none)
+        let discriminantRef := Heap.HExpr.lambda (.fvar discriminantVar none)
+        let fallthroughRef := Heap.HExpr.lambda (.fvar fallthroughVar none)
+
+        -- Helper: create condition (if break then false else baseCondition)
+        let mkCondition (baseCondition : Heap.HExpr) : Heap.HExpr :=
+          Heap.HExpr.deferredIte breakFlagRef Heap.HExpr.false baseCondition
+
+        -- Helper: build case condition for regular case
+        let mkCaseCondition (testExpr : TS_Expression) : Heap.HExpr :=
+          let testVal := translate_expr testExpr
+          let matchCond := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Eq" none) discriminantRef) testVal
+          let matchOrFallthrough := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Bool.Or" none) fallthroughRef) matchCond
+          mkCondition matchOrFallthrough
+
+        -- Recursive case builder
+        let rec buildCases (remainingCases : List TS_SwitchCase) (accCtx : TranslationContext) : TranslationContext × TSStrataStatement :=
+          let emptyBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [] }
+
+          match remainingCases with
+          | [] => (accCtx, .ite Heap.HExpr.false emptyBlock emptyBlock)
+
+          | [singleCase] =>
+            -- Last case: no rest to chain
+            let (stmtsBeforeBreak, hasBreak) := splitAtBreak singleCase.consequent.toList
+            let (caseCtx, caseStmts) := translateCaseBody stmtsBeforeBreak accCtx
+            let isDefault := singleCase.test.isNone
+            let finalStmts := buildCaseStmts caseStmts hasBreak isDefault
+
+            let condition := match singleCase.test with
+              | none => mkCondition Heap.HExpr.true  -- Default: if !break then true
+              | some testExpr => mkCaseCondition testExpr
+
+            (caseCtx, .ite condition { ss := finalStmts } emptyBlock)
+
+          | currentCase :: restCases =>
+            -- Non-last case: chain with rest
+            let (stmtsBeforeBreak, hasBreak) := splitAtBreak currentCase.consequent.toList
+            let (caseCtx, caseStmts) := translateCaseBody stmtsBeforeBreak accCtx
+            let isDefault := currentCase.test.isNone
+            let finalStmts := buildCaseStmts caseStmts hasBreak isDefault
+            let (restCtx, restStmt) := buildCases restCases caseCtx
+
+            let condition := match currentCase.test with
+              | none => mkCondition Heap.HExpr.true  -- Default: if !break then true
+              | some testExpr => mkCaseCondition testExpr
+
+            (restCtx, .ite condition { ss := finalStmts ++ [restStmt] } { ss := [restStmt] })
+
+        let (finalCtx, switchBody) := buildCases switchStmt.cases.toList ctx
+        dbg_trace s!"[DEBUG] Switch statement translated with {switchStmt.cases.size} cases (with break support)"
+        (finalCtx, [initDiscriminant, initFallthrough, initBreakFlag, switchBody])
+
+      | _ => panic! s!"Unimplemented statement: {repr s}"
 
 -- Translate TypeScript statements to TypeScript-Strata statements
 partial def translate_statement (s: TS_Statement) (ctx : TranslationContext) : TranslationContext × List TSStrataStatement :=

StrataTest/Languages/TypeScript/test_switch.ts

@@ -1,11 +1,14 @@
-function getWeekendName(date: number): string | undefined {
-    switch (date) {
-        case 0:
-            return "Sunday";
-        case 6:
-            return "Saturday";
-    }
-}
+// Test switch statement with fallthrough
+let x: number = 2;
+let result: number = 0;
 
-let day: number = 6;
-let weekendName: string | undefined = getWeekendName(day);
+switch (x) {
+  case 1:
+    result = 10;
+  case 2:
+    result = 20;
+  case 3:
+    result = 30;
+  default:
+    result = 40;
+}

StrataTest/Languages/TypeScript/test_switch_break_simple.ts

@@ -0,0 +1,12 @@
+// Simple switch with break
+let x: number = 1;
+let r: number = 0;
+
+switch (x) {
+  case 1:
+    r = 10;
+    break;
+  case 2:
+    r = 20;
+}
+

StrataTest/Languages/TypeScript/test_switch_mixed.ts

@@ -0,0 +1,19 @@
+// Test switch with mixed break and fallthrough
+let x: number = 2;
+let result: number = 0;
+
+switch (x) {
+  case 1:
+    result = 10;
+  case 2:
+    result = 20;
+  case 3:
+    result = 30;
+    break;
+  default:
+    result = 40;
+}
+
+result;
+
+

conformance_testing/babel_to_lean.py

@@ -307,18 +307,7 @@ def parse_continue_statement(j):
     }
     add_missing_node_info(j, target_j)
     return target_j
-
-def parse_for_statement(j):
-    target_body = parse_statement(j['body'])
-    target_j = {
-        "init": parse_variable_declaration(j['init']),
-        "test": parse_expression(j['test']),
-        "update": parse_assignment_expression(j['update']),
-        "body": target_body
-    }
-    add_missing_node_info(j, target_j)
-    return target_j
-
+    
 def parse_switch_statement(j):
     target_j = {
         "discriminant": parse_expression(j['discriminant']),
@@ -340,12 +329,24 @@ def parse_switch_case(j):
     add_missing_node_info(j, target_j)
     return target_j
 
+
 def parse_break_statement(j):
     target_j = {
         "label": parse_identifier(j['label']) if j.get('label') else None
     }
     add_missing_node_info(j, target_j)
     return target_j
+    
+def parse_for_statement(j):
+    target_body = parse_statement(j['body'])
+    target_j = {
+        "init": parse_variable_declaration(j['init']),
+        "test": parse_expression(j['test']),
+        "update": parse_assignment_expression(j['update']),
+        "body": target_body
+    }
+    add_missing_node_info(j, target_j)
+    return target_j
 
 def parse_statement(j):
     match j['type']: