Cleanup

6 files changed, 47 insertions, 106 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 0bcf66bd..0a06ef73 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -817,14 +817,14 @@ let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
   | PatConcrete cv ->
       ctx.fmt.extract_constant_value fmt inside cv;
       ctx
-  | PatVar (Var (v, _)) ->
+  | PatVar (v, _) ->
       let vname =
         ctx.fmt.var_basename ctx.names_map.names_set v.basename v.ty
       in
       let ctx, vname = ctx_add_var vname v.id ctx in
       F.pp_print_string fmt vname;
       ctx
-  | PatVar Dummy ->
+  | PatDummy ->
       F.pp_print_string fmt "_";
       ctx
   | PatAdt av ->
@@ -845,7 +845,7 @@ let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
 let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
     (inside : bool) (e : texpression) : unit =
   match e.e with
-  | Local var_id ->
+  | Var var_id ->
       let var_name = ctx_get_var var_id ctx in
       F.pp_print_string fmt var_name
   | Const cv -> ctx.fmt.extract_constant_value fmt inside cv
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 2da653bb..f21329ed 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -362,21 +362,17 @@ let adt_g_value_to_string (fmt : value_formatter)
           ^ "\n- ty: " ^ ty_to_string fmt ty ^ "\n- variant_id: "
            ^ Print.option_to_string VariantId.to_string variant_id))
 
-let var_or_dummy_to_string (fmt : ast_formatter) (v : var_or_dummy) : string =
-  match v with
-  | Var (v, None) -> var_to_string (ast_to_type_formatter fmt) v
-  | Var (v, Some mp) ->
-      let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in
-      "(" ^ var_to_varname v ^ " " ^ mp ^ " : "
-      ^ ty_to_string (ast_to_type_formatter fmt) v.ty
-      ^ ")"
-  | Dummy -> "_"
-
 let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) :
     string =
   match v.value with
   | PatConcrete cv -> Print.Values.constant_value_to_string cv
-  | PatVar var -> var_or_dummy_to_string fmt var
+  | PatVar (v, None) -> var_to_string (ast_to_type_formatter fmt) v
+  | PatVar (v, Some mp) ->
+      let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in
+      "(" ^ var_to_varname v ^ " " ^ mp ^ " : "
+      ^ ty_to_string (ast_to_type_formatter fmt) v.ty
+      ^ ")"
+  | PatDummy -> "_"
   | PatAdt av ->
       adt_g_value_to_string
         (ast_to_value_formatter fmt)
@@ -455,7 +451,7 @@ let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string =
 let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
     (indent : string) (indent_incr : string) (e : texpression) : string =
   match e.e with
-  | Local var_id ->
+  | Var var_id ->
       let s = fmt.var_id_to_string var_id in
       if inside then "(" ^ s ^ ")" else s
   | Const cv -> Print.Values.constant_value_to_string cv
diff --git a/src/Pure.ml b/src/Pure.ml
index 9cf7a077..e2362338 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -172,7 +172,7 @@ type mplace = {
 
 type variant_id = VariantId.id [@@deriving show]
 
-(** Ancestor for [iter_var_or_dummy] visitor *)
+(** Ancestor for [iter_pat_var_or_dummy] visitor *)
 class ['self] iter_value_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
@@ -242,57 +242,13 @@ class virtual ['self] mapreduce_value_base =
       fun _ x -> (x, self#zero)
   end
 
-type var_or_dummy =
-  | Var of var * mplace option
-      (** Rk.: the mdplace is actually always a variable (i.e.: there are no projections).
-
-          We use [mplace] because it leads to a more uniform treatment of the meta
-          information.
-       *)
-  | Dummy  (** Ignored value: `_`. *)
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_var_or_dummy";
-        variety = "iter";
-        ancestors = [ "iter_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
-        concrete = true;
-        polymorphic = false;
-      },
-    visitors
-      {
-        name = "map_var_or_dummy";
-        variety = "map";
-        ancestors = [ "map_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.map] *);
-        concrete = true;
-        polymorphic = false;
-      },
-    visitors
-      {
-        name = "reduce_var_or_dummy";
-        variety = "reduce";
-        ancestors = [ "reduce_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.reduce] *);
-        polymorphic = false;
-      },
-    visitors
-      {
-        name = "mapreduce_var_or_dummy";
-        variety = "mapreduce";
-        ancestors = [ "mapreduce_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.reduce] *);
-        polymorphic = false;
-      }]
-
 (** A pattern (which appears on the left of assignments, in matches, etc.). *)
 type pattern =
   | PatConcrete of constant_value
       (** [PatConcrete] is necessary because we merge the switches over integer
           values and the matches over enumerations *)
-  | PatVar of var_or_dummy
+  | PatVar of var * mplace option
+  | PatDummy  (** Ignored value: `_`. *)
   | PatAdt of adt_pattern
 
 and adt_pattern = {
@@ -307,7 +263,7 @@ and typed_pattern = { value : pattern; ty : ty }
       {
         name = "iter_typed_pattern";
         variety = "iter";
-        ancestors = [ "iter_var_or_dummy" ];
+        ancestors = [ "iter_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
         polymorphic = false;
@@ -316,7 +272,7 @@ and typed_pattern = { value : pattern; ty : ty }
       {
         name = "map_typed_pattern";
         variety = "map";
-        ancestors = [ "map_var_or_dummy" ];
+        ancestors = [ "map_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
         polymorphic = false;
@@ -325,7 +281,7 @@ and typed_pattern = { value : pattern; ty : ty }
       {
         name = "reduce_typed_pattern";
         variety = "reduce";
-        ancestors = [ "reduce_var_or_dummy" ];
+        ancestors = [ "reduce_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         polymorphic = false;
       },
@@ -333,7 +289,7 @@ and typed_pattern = { value : pattern; ty : ty }
       {
         name = "mapreduce_typed_pattern";
         variety = "mapreduce";
-        ancestors = [ "mapreduce_var_or_dummy" ];
+        ancestors = [ "mapreduce_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         polymorphic = false;
       }]
@@ -439,11 +395,7 @@ class virtual ['self] mapreduce_expression_base =
     more general than the LLBC statements, in a sense.
  *)
 type expression =
-  | Local of var_id
-      (** Local variable - TODO: we name it "Local" because "Var" is used
-          in [var_or_dummy]: change the name. Maybe rename `Var` and `Dummy`
-          in `var_or_dummy` to `PatVar` and `PatDummy`.
-       *)
+  | Var of var_id  (** a variable *)
   | Const of constant_value
   | App of texpression * texpression
       (** Application of a function to an argument.
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index c84bf7cd..bd7d7766 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -95,7 +95,7 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator =
       method! visit_var _ v _ = v.id
       (** For the patterns *)
 
-      method! visit_Local _ vid _ = vid
+      method! visit_Var _ vid _ = vid
       (** For the rvalues *)
     end
   in
@@ -296,7 +296,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       object
         inherit [_] map_typed_pattern
 
-        method! visit_Var _ v mp = Var (update_var ctx v mp, mp)
+        method! visit_PatVar _ v mp = PatVar (update_var ctx v mp, mp)
       end
     in
     obj#visit_typed_pattern () lv
@@ -350,7 +350,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     (* Register the place *)
     let ctx = register_mplace mp ctx in
     (* Add the constraint *)
-    match (unmeta rv).e with Local vid -> add_constraint mp vid ctx | _ -> ctx
+    match (unmeta rv).e with Var vid -> add_constraint mp vid ctx | _ -> ctx
   in
   (* Specific case of constraint on left values *)
   let add_left_constraint (lv : typed_pattern) (ctx : pn_ctx) : pn_ctx =
@@ -362,7 +362,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
 
         method plus ctx0 ctx1 _ = merge_ctxs (ctx0 ()) (ctx1 ())
 
-        method! visit_Var _ v mp () =
+        method! visit_PatVar _ v mp () =
           (* Register the variable *)
           let ctx = register_var (self#zero ()) v in
           (* Register the mplace information if there is such information *)
@@ -381,7 +381,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     (* We propagate constraints across variable reassignments: `^0 = x`,
      * if the destination doesn't have naming information *)
     match lv.value with
-    | PatVar (Var (({ id = _; basename = None; ty = _ } as lvar), lmp)) ->
+    | PatVar (({ id = _; basename = None; ty = _ } as lvar), lmp) ->
         if
           (* Check that there is not already a name for the variable *)
           VarId.Map.mem lvar.id ctx.pure_vars
@@ -413,7 +413,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
           (* We try to use the rvalue information, if it is a variable *)
           let ctx =
             match (unmeta re).e with
-            | Local rvar_id -> (
+            | Var rvar_id -> (
                 match VarId.Map.find_opt rvar_id ctx.pure_vars with
                 | None -> ctx
                 | Some name -> add name ctx)
@@ -429,7 +429,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     let ty = e.ty in
     let ctx, e =
       match e.e with
-      | Local _ -> (* Nothing to do *) (ctx, e.e)
+      | Var _ -> (* Nothing to do *) (ctx, e.e)
       | Const _ -> (* Nothing to do *) (ctx, e.e)
       | App (app, arg) ->
           let ctx, app = update_texpression app ctx in
@@ -590,7 +590,7 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
          * - the left-value is a variable
          *)
         match (monadic, lv.value) with
-        | false, PatVar (Var (lv_var, _)) ->
+        | false, PatVar (lv_var, _) ->
             (* We can filter if: *)
             let filter = false in
             (* 1. Either:
@@ -610,7 +610,7 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
               if inline_pure then
                 let app, _ = destruct_apps re in
                 match app.e with
-                | Const _ | Local _ -> true (* constant or variable *)
+                | Const _ | Var _ -> true (* constant or variable *)
                 | Qualif qualif -> (
                     match qualif.id with
                     | AdtCons _ | Proj _ -> true (* ADT constructor *)
@@ -635,9 +635,9 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
       (** Visit the let-bindings to filter the useless ones (and update
           the substitution map while doing so *)
 
-      method! visit_Local (env : texpression VarId.Map.t) (vid : VarId.id) =
+      method! visit_Var (env : texpression VarId.Map.t) (vid : VarId.id) =
         match VarId.Map.find_opt vid env with
-        | None -> (* No substitution *) super#visit_Local env vid
+        | None -> (* No substitution *) super#visit_Var env vid
         | Some ne ->
             (* Substitute - note that we need to reexplore, because
              * there may be stacked substitutions, if we have:
@@ -750,7 +750,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
 
       method! visit_texpression env e =
         match e.e with
-        | Local _ | Const _ -> fun _ -> false
+        | Var _ | Const _ -> fun _ -> false
         | Let (_, _, re, e) -> (
             match opt_destruct_function_call re with
             | None -> fun () -> self#visit_texpression env e ()
@@ -812,12 +812,9 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
 
       method plus b0 b1 _ = b0 () && b1 ()
 
-      method! visit_var_or_dummy env v =
-        match v with
-        | Dummy -> (Dummy, fun _ -> true)
-        | Var (v, mp) ->
-            if VarId.Set.mem v.id env then (Var (v, mp), fun _ -> false)
-            else (Dummy, fun _ -> true)
+      method! visit_PatVar env v mp =
+        if VarId.Set.mem v.id env then (PatVar (v, mp), fun _ -> false)
+        else (PatDummy, fun _ -> true)
     end
   in
   let filter_typed_pattern (used_vars : VarId.Set.t) (lv : typed_pattern) :
@@ -839,12 +836,12 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
 
       method plus s0 s1 _ = VarId.Set.union (s0 ()) (s1 ())
 
-      method! visit_Local _ vid = (Local vid, fun _ -> VarId.Set.singleton vid)
+      method! visit_Var _ vid = (Var vid, fun _ -> VarId.Set.singleton vid)
       (** Whenever we visit a variable, we need to register the used variable *)
 
       method! visit_expression env e =
         match e with
-        | Local _ | Const _ | App _ | Qualif _
+        | Var _ | Const _ | App _ | Qualif _
         | Switch (_, _)
         | Meta (_, _)
         | Abs _ ->
@@ -970,10 +967,8 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
     object
       inherit [_] map_expression as super
 
-      method! visit_var_or_dummy _ v =
-        match v with
-        | Dummy -> Dummy
-        | Var (v, mp) -> if v.ty = unit_ty then Dummy else Var (v, mp)
+      method! visit_PatVar _ v mp =
+        if v.ty = unit_ty then PatDummy else PatVar (v, mp)
       (** Replace in patterns *)
 
       method! visit_texpression env e =
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 96d84fb1..fe71b3b2 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -180,17 +180,17 @@ let functions_not_mutually_recursive (funs : fun_decl list) : bool =
  *)
 let rec let_group_requires_parentheses (e : texpression) : bool =
   match e.e with
-  | Local _ | Const _ | App _ | Abs _ | Qualif _ -> false
+  | Var _ | Const _ | App _ | Abs _ | Qualif _ -> false
   | Let (monadic, _, _, next_e) ->
       if monadic then true else let_group_requires_parentheses next_e
   | Switch (_, _) -> false
   | Meta (_, next_e) -> let_group_requires_parentheses next_e
 
 let is_var (e : texpression) : bool =
-  match e.e with Local _ -> true | _ -> false
+  match e.e with Var _ -> true | _ -> false
 
 let as_var (e : texpression) : VarId.id =
-  match e.e with Local v -> v | _ -> raise (Failure "Unreachable")
+  match e.e with Var v -> v | _ -> raise (Failure "Unreachable")
 
 (** Remove the external occurrences of [Meta] *)
 let rec unmeta (e : texpression) : texpression =
@@ -350,12 +350,12 @@ let unit_rvalue : texpression =
   { e; ty }
 
 let mk_texpression_from_var (v : var) : texpression =
-  let e = Local v.id in
+  let e = Var v.id in
   let ty = v.ty in
   { e; ty }
 
 let mk_typed_pattern_from_var (v : var) (mp : mplace option) : typed_pattern =
-  let value = PatVar (Var (v, mp)) in
+  let value = PatVar (v, mp) in
   let ty = v.ty in
   { value; ty }
 
@@ -535,8 +535,8 @@ module TypeCheck = struct
     | PatConcrete cv ->
         check_constant_value cv v.ty;
         ctx
-    | PatVar Dummy -> ctx
-    | PatVar (Var (var, _)) ->
+    | PatDummy -> ctx
+    | PatVar (var, _) ->
         assert (var.ty = v.ty);
         let env = VarId.Map.add var.id var.ty ctx.env in
         { ctx with env }
@@ -567,7 +567,7 @@ module TypeCheck = struct
 
   let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
     match e.e with
-    | Local var_id -> (
+    | Var var_id -> (
         (* Lookup the variable - note that the variable may not be there,
          * if we type-check a subexpression (i.e.: if the variable is introduced
          * "outside" of the expression) - TODO: this won't happen once
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 14a844a1..c0e47ca7 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1512,9 +1512,7 @@ and translate_expansion (config : config) (p : S.mplace option)
       let branches = List.map translate_branch branches in
       let otherwise = translate_expression config otherwise ctx in
       let pat_ty = Integer int_ty in
-      let otherwise_pat : typed_pattern =
-        { value = PatVar Dummy; ty = pat_ty }
-      in
+      let otherwise_pat : typed_pattern = { value = PatDummy; ty = pat_ty } in
       let otherwise : match_branch =
         { pat = otherwise_pat; branch = otherwise }
       in