Merge the switches over integers and the matches over enumerations in

the pure AST

6 files changed, 36 insertions, 97 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 8746b8af..919a5b05 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -665,6 +665,9 @@ let extract_adt_g_value
 let rec extract_typed_lvalue (ctx : extraction_ctx) (fmt : F.formatter)
     (inside : bool) (v : typed_lvalue) : extraction_ctx =
   match v.value with
+  | LvConcrete cv ->
+      ctx.fmt.extract_constant_value fmt inside cv;
+      ctx
   | LvVar (Var (v, _)) ->
       let vname =
         ctx.fmt.var_basename ctx.names_map.names_set v.basename v.ty
@@ -832,56 +835,6 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
           extract_branch false e_else;
           (* Close the box for the whole `if ... then ... else ...` *)
           F.pp_close_box fmt ()
-      | SwitchInt (_, branches, otherwise) ->
-          (* Open a box for the whole match *)
-          F.pp_open_hvbox fmt 0;
-          (* Open a box for the `match ... with` *)
-          F.pp_open_hovbox fmt ctx.indent_incr;
-          (* Print the `match ... with` *)
-          F.pp_print_string fmt "begin match";
-          F.pp_print_space fmt ();
-          extract_texpression ctx fmt false scrut;
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt "with";
-          (* Close the box for the `match ... with` *)
-          F.pp_close_box fmt ();
-
-          (* Extract the branches *)
-          let extract_branch (sv : scalar_value option) (e_branch : texpression)
-              : unit =
-            F.pp_print_space fmt ();
-            (* Open a box for the pattern+branch *)
-            F.pp_open_hovbox fmt ctx.indent_incr;
-            F.pp_print_string fmt "|";
-            (* Print the pattern *)
-            F.pp_print_space fmt ();
-            (match sv with
-            | Some sv -> ctx.fmt.extract_constant_value fmt false (V.Scalar sv)
-            | None -> F.pp_print_string fmt "_");
-            F.pp_print_space fmt ();
-            F.pp_print_string fmt "->";
-            F.pp_print_space fmt ();
-            (* Open a box for the branch *)
-            F.pp_open_hvbox fmt 0;
-            (* Print the branch itself *)
-            extract_texpression ctx fmt false e_branch;
-            (* Close the box for the branch *)
-            F.pp_close_box fmt ();
-            (* Close the box for the pattern+branch *)
-            F.pp_close_box fmt ()
-          in
-
-          let all_branches =
-            List.map (fun (sv, br) -> (Some sv, br)) branches
-          in
-          let all_branches = List.append all_branches [ (None, otherwise) ] in
-          List.iter (fun (sv, br) -> extract_branch sv br) all_branches;
-
-          (* End the match *)
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt "end";
-          (* Close the box for the whole match *)
-          F.pp_close_box fmt ()
       | Match branches ->
           (* Open a box for the whole match *)
           F.pp_open_hvbox fmt 0;
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 0325e60c..81ebcc7e 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -267,6 +267,7 @@ let adt_g_value_to_string (fmt : value_formatter)
 let rec typed_lvalue_to_string (fmt : value_formatter) (v : typed_lvalue) :
     string =
   match v.value with
+  | LvConcrete cv -> Print.Values.constant_value_to_string cv
   | LvVar var -> var_or_dummy_to_string fmt var
   | LvAdt av ->
       adt_g_value_to_string fmt
@@ -415,20 +416,6 @@ and switch_to_string (fmt : ast_formatter) (indent : string)
       let e_false = texpression_to_string fmt indent1 indent_incr e_false in
       "if " ^ scrut ^ "\n" ^ indent ^ "then\n" ^ indent ^ e_true ^ "\n" ^ indent
       ^ "else\n" ^ indent ^ e_false
-  | SwitchInt (_, branches, otherwise) ->
-      let branches =
-        List.map
-          (fun (v, be) ->
-            indent ^ "| " ^ scalar_value_to_string v ^ " ->\n" ^ indent1
-            ^ texpression_to_string fmt indent1 indent_incr be)
-          branches
-      in
-      let otherwise =
-        indent ^ "| _ ->\n" ^ indent1
-        ^ texpression_to_string fmt indent1 indent_incr otherwise
-      in
-      let all_branches = List.append branches [ otherwise ] in
-      "switch " ^ scrut ^ " with\n" ^ String.concat "\n" all_branches
   | Match branches ->
       let val_fmt = ast_to_value_formatter fmt in
       let branch_to_string (b : match_branch) : string =
diff --git a/src/Pure.ml b/src/Pure.ml
index 428246dd..c773d613 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -264,7 +264,12 @@ type var_or_dummy =
       }]
 
 (** A left value (which appears on the left of assignments *)
-type lvalue = LvVar of var_or_dummy | LvAdt of adt_lvalue
+type lvalue =
+  | LvConcrete of constant_value
+      (** [LvConcrete] is necessary because we merge the switches over integer
+        values and the matches over enumerations *)
+  | LvVar of var_or_dummy
+  | LvAdt of adt_lvalue
 
 and adt_lvalue = {
   variant_id : (VariantId.id option[@opaque]);
@@ -505,12 +510,7 @@ and call = {
        *)
 }
 
-and switch_body =
-  | If of texpression * texpression
-  | SwitchInt of integer_type * (scalar_value * texpression) list * texpression
-  | Match of match_branch list
-(* TODO: merge SwitchInt and Match. In order to do that,
- * we need to add constants to lvalues. *)
+and switch_body = If of texpression * texpression | Match of match_branch list
 
 and match_branch = { pat : typed_lvalue; branch : texpression }
 
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 6b42e328..d8bfe4cd 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -240,19 +240,6 @@ let compute_pretty_names (def : fun_def) : fun_def =
           let ctx2, e_false = update_texpression e_false ctx in
           let ctx = merge_ctxs ctx1 ctx2 in
           (ctx, If (e_true, e_false))
-      | SwitchInt (int_ty, branches, otherwise) ->
-          let ctx_branches_ls =
-            List.map
-              (fun (v, br) ->
-                let ctx, br = update_texpression br ctx in
-                (ctx, (v, br)))
-              branches
-          in
-          let ctx, otherwise = update_texpression otherwise ctx in
-          let ctxs, branches = List.split ctx_branches_ls in
-          let ctxs = merge_ctxs_ls ctxs in
-          let ctx = merge_ctxs ctx ctxs in
-          (ctx, SwitchInt (int_ty, branches, otherwise))
       | Match branches ->
           let ctx_branches_ls =
             List.map
@@ -478,12 +465,6 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) (call0 : call)
             fun () ->
               self#visit_texpression env e1 ()
               && self#visit_texpression env e2 ()
-        | SwitchInt (_, branches, otherwise) ->
-            fun () ->
-              List.for_all
-                (fun (_, br) -> self#visit_texpression env br ())
-                branches
-              && self#visit_texpression env otherwise ()
         | Match branches ->
             fun () ->
               List.for_all
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index c19d7914..f12ed87b 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -127,6 +127,17 @@ let mk_result_return_lvalue (v : typed_lvalue) : typed_lvalue =
 
 let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ])
 
+let compute_constant_value_ty (cv : constant_value) : ty =
+  match cv with
+  | V.Scalar sv -> Integer sv.V.int_ty
+  | Bool _ -> Bool
+  | Char _ -> Char
+  | String _ -> Str
+
+let mk_typed_lvalue_from_constant_value (cv : constant_value) : typed_lvalue =
+  let ty = compute_constant_value_ty cv in
+  { value = LvConcrete cv; ty }
+
 let mk_value_expression (v : typed_rvalue) (mp : mplace option) : texpression =
   let e = Value (v, mp) in
   let ty = v.ty in
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 9a611899..a1208f92 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1305,21 +1305,28 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
       { e; ty }
   | ExpandInt (int_ty, branches, otherwise) ->
       let translate_branch ((v, branch_e) : V.scalar_value * S.expression) :
-          scalar_value * texpression =
+          match_branch =
         (* We don't need to update the context: we don't introduce any
          * new values/variables *)
-        let branch_e = translate_expression branch_e ctx in
-        (v, branch_e)
+        let branch = translate_expression branch_e ctx in
+        let pat = mk_typed_lvalue_from_constant_value (V.Scalar v) in
+        { pat; branch }
       in
       let branches = List.map translate_branch branches in
       let otherwise = translate_expression otherwise ctx in
+      let pat_ty = Integer int_ty in
+      let otherwise_pat : typed_lvalue = { value = LvVar Dummy; ty = pat_ty } in
+      let otherwise : match_branch =
+        { pat = otherwise_pat; branch = otherwise }
+      in
+      let all_branches = List.append branches [ otherwise ] in
       let e =
         Switch
-          ( mk_value_expression scrutinee scrutinee_mplace,
-            SwitchInt (int_ty, branches, otherwise) )
+          (mk_value_expression scrutinee scrutinee_mplace, Match all_branches)
       in
-      let ty = otherwise.ty in
-      assert (List.for_all (fun (_, br) -> br.ty = ty) branches);
+      let ty = otherwise.branch.ty in
+      assert (
+        List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches);
       { e; ty }
 
 and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :