Fix pretty-printing of switch-cases

Weird bug, cf. test/pattern.sail.

3 files changed, 29 insertions, 3 deletions

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 4a27d523..285dc56c 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -547,17 +547,18 @@ and pp_lem_exp ppf (E_aux(e,_)) =
       kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps 
   | E_field(fexp,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id
   | E_case(exp,pexps) -> 
-    fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_lem_case pp_lem_case) pexps
+    fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps
   | E_let(leb,exp) -> fprintf ppf "@[<0>(%a %a %a) @]" kwd "E_let" pp_lem_let leb pp_lem_exp exp
   | E_assign(lexp,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp
 
 and pp_semi_lem_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_lem_exp e kwd ";"
 
 and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),_)) = fprintf ppf "@[<1>(%a %a %a)@]" kwd "FE_Fexp" pp_lem_id id pp_lem_exp exp
-and pp_semi_lem_fexp ppf fexp = fprintf ppf "@[<1>(%a %a)@]" pp_lem_fexp fexp kwd ";"
+and pp_semi_lem_fexp ppf fexp = fprintf ppf "@[<1>%a %a@]" pp_lem_fexp fexp kwd ";"
 
 and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),_)) = 
-  fprintf ppf "@[<1>(%a %a@ %a)@]" kwd "Pat_exp" pp_lem_pat pat pp_lem_exp exp 
+  fprintf ppf "@[<1>(%a %a@ %a)@]" kwd "Pat_exp" pp_lem_pat pat pp_lem_exp exp
+and pp_semi_lem_case ppf case = fprintf ppf "@[<1>%a %a@]" pp_lem_case case kwd ";"
 
 and pp_lem_lexp ppf (LEXP_aux(lexp,_)) =
   match lexp with
diff --git a/src/test/pattern.sail b/src/test/pattern.sail
new file mode 100644
index 00000000..35a6b632
--- /dev/null
+++ b/src/test/pattern.sail
@@ -0,0 +1,24 @@
+
+register nat n
+register nat x
+register nat y
+
+function unit main _ = {
+
+  (* works - x and y are set to 42 *)
+  n := 1;
+  y :=
+  (switch n {
+    case 0 -> { x := 21; x }
+    case 1 -> { x := 42; x } 
+    case x -> { x := 99; x }
+  });
+
+  (* doesn't work - main returns 1 instead of 42 *)
+  n := 1;
+  switch n {
+    case 0 -> { 21 }
+    case 1 -> { 42 } 
+    case x -> { 99 }
+  }
+}
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index a86e3d1c..df5598dc 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -2,6 +2,7 @@ let tests = [
   "test1", Test1.defs;
   "test2", Test2.defs;
   "test3", Test3.defs;
+  "pattern", Pattern.defs;
   "vectors", Vectors.defs;
 ] ;;