Rename "lvalue" to "pattern"

6 files changed, 159 insertions, 160 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 357b49b5..19e17260 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -758,7 +758,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
 
 (** The following function factorizes the extraction of ADT values.
 
-    Note that lvalues can introduce new variables: we thus return an extraction
+    Note that patterns can introduce new variables: we thus return an extraction
     context updated with new bindings.
     
     TODO: we don't need something very generic anymore
@@ -808,27 +808,27 @@ let extract_adt_g_value
 
 (** [inside]: see [extract_ty].
 
-    As an lvalue can introduce new variables, we return an extraction context
+    As an pattern can introduce new variables, we return an extraction context
     updated with new bindings.
  *)
-let rec extract_typed_lvalue (ctx : extraction_ctx) (fmt : F.formatter)
-    (inside : bool) (v : typed_lvalue) : extraction_ctx =
+let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
+    (inside : bool) (v : typed_pattern) : extraction_ctx =
   match v.value with
-  | LvConcrete cv ->
+  | PatConcrete cv ->
       ctx.fmt.extract_constant_value fmt inside cv;
       ctx
-  | LvVar (Var (v, _)) ->
+  | PatVar (Var (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
-  | LvVar Dummy ->
+  | PatVar Dummy ->
       F.pp_print_string fmt "_";
       ctx
-  | LvAdt av ->
-      let extract_value ctx inside v = extract_typed_lvalue ctx fmt inside v in
+  | PatAdt av ->
+      let extract_value ctx inside v = extract_typed_pattern ctx fmt inside v in
       extract_adt_g_value extract_value fmt ctx inside av.variant_id
         av.field_values v.ty
 
@@ -1014,7 +1014,7 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
       raise (Failure "Unreachable")
 
 and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
-    (xl : typed_lvalue list) (e : texpression) : unit =
+    (xl : typed_pattern list) (e : texpression) : unit =
   (* Open a box for the abs expression *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* Open parentheses *)
@@ -1026,7 +1026,7 @@ and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     List.fold_left
       (fun ctx x ->
         F.pp_print_space fmt ();
-        extract_typed_lvalue ctx fmt true x)
+        extract_typed_pattern ctx fmt true x)
       ctx xl
   in
   F.pp_print_space fmt ();
@@ -1040,7 +1040,7 @@ and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   F.pp_close_box fmt ()
 
 and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
-    (monadic : bool) (lv : typed_lvalue) (re : texpression)
+    (monadic : bool) (lv : typed_pattern) (re : texpression)
     (next_e : texpression) : unit =
   (* Open a box for the whole expression *)
   F.pp_open_hvbox fmt 0;
@@ -1052,7 +1052,7 @@ and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     if monadic then (
       (* Note that in F*, the left value of a monadic let-binding can only be
        * a variable *)
-      let ctx = extract_typed_lvalue ctx fmt true lv in
+      let ctx = extract_typed_pattern ctx fmt true lv in
       F.pp_print_space fmt ();
       F.pp_print_string fmt "<--";
       F.pp_print_space fmt ();
@@ -1062,7 +1062,7 @@ and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     else (
       F.pp_print_string fmt "let";
       F.pp_print_space fmt ();
-      let ctx = extract_typed_lvalue ctx fmt true lv in
+      let ctx = extract_typed_pattern ctx fmt true lv in
       F.pp_print_space fmt ();
       F.pp_print_string fmt "=";
       F.pp_print_space fmt ();
@@ -1148,7 +1148,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         F.pp_print_string fmt "|";
         (* Print the pattern *)
         F.pp_print_space fmt ();
-        let ctx = extract_typed_lvalue ctx fmt false br.pat in
+        let ctx = extract_typed_pattern ctx fmt false br.pat in
         F.pp_print_space fmt ();
         F.pp_print_string fmt "->";
         F.pp_print_space fmt ();
@@ -1208,11 +1208,11 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
     | None -> ctx
     | Some body ->
         List.fold_left
-          (fun ctx (lv : typed_lvalue) ->
+          (fun ctx (lv : typed_pattern) ->
             (* Open a box for the input parameter *)
             F.pp_open_hovbox fmt 0;
             F.pp_print_string fmt "(";
-            let ctx = extract_typed_lvalue ctx fmt false lv in
+            let ctx = extract_typed_pattern ctx fmt false lv in
             F.pp_print_space fmt ();
             F.pp_print_string fmt ":";
             F.pp_print_space fmt ();
@@ -1427,9 +1427,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
       in
       let _ =
         List.fold_left
-          (fun ctx (lv : typed_lvalue) ->
+          (fun ctx (lv : typed_pattern) ->
             F.pp_print_space fmt ();
-            let ctx = extract_typed_lvalue ctx fmt false lv in
+            let ctx = extract_typed_pattern ctx fmt false lv in
             ctx)
           ctx inputs_lvs
       in
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 3adf4eee..e40a7b8b 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -288,7 +288,7 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
           raise (Failure "Unreachable"))
 
 (** TODO: we don't need a general function anymore (it is now only used for
-    lvalues (i.e., patterns)
+    patterns (i.e., patterns)
  *)
 let adt_g_value_to_string (fmt : value_formatter)
     (value_to_string : 'v -> string) (variant_id : VariantId.id option)
@@ -372,15 +372,15 @@ let var_or_dummy_to_string (fmt : ast_formatter) (v : var_or_dummy) : string =
       ^ ")"
   | Dummy -> "_"
 
-let rec typed_lvalue_to_string (fmt : ast_formatter) (v : typed_lvalue) : string
-    =
+let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) :
+    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 ->
+  | PatConcrete cv -> Print.Values.constant_value_to_string cv
+  | PatVar var -> var_or_dummy_to_string fmt var
+  | PatAdt av ->
       adt_g_value_to_string
         (ast_to_value_formatter fmt)
-        (typed_lvalue_to_string fmt)
+        (typed_pattern_to_string fmt)
         av.variant_id av.field_values v.ty
 
 let fun_sig_to_string (fmt : ast_formatter) (sg : fun_sig) : string =
@@ -542,19 +542,19 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
   if all_args <> [] && inside then "(" ^ e ^ ")" else e
 
 and abs_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string)
-    (xl : typed_lvalue list) (e : texpression) : string =
-  let xl = List.map (typed_lvalue_to_string fmt) xl in
+    (xl : typed_pattern list) (e : texpression) : string =
+  let xl = List.map (typed_pattern_to_string fmt) xl in
   let e = texpression_to_string fmt false indent indent_incr e in
   "λ " ^ String.concat " " xl ^ ". " ^ e
 
 and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string)
-    (monadic : bool) (lv : typed_lvalue) (re : texpression) (e : texpression) :
+    (monadic : bool) (lv : typed_pattern) (re : texpression) (e : texpression) :
     string =
   let indent1 = indent ^ indent_incr in
   let inside = false in
   let re = texpression_to_string fmt inside indent1 indent_incr re in
   let e = texpression_to_string fmt inside indent indent_incr e in
-  let lv = typed_lvalue_to_string fmt lv in
+  let lv = typed_pattern_to_string fmt lv in
   if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e
   else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e
 
@@ -575,7 +575,7 @@ and switch_to_string (fmt : ast_formatter) (indent : string)
       ^ indent ^ "else\n" ^ indent1 ^ e_false
   | Match branches ->
       let branch_to_string (b : match_branch) : string =
-        let pat = typed_lvalue_to_string fmt b.pat in
+        let pat = typed_pattern_to_string fmt b.pat in
         indent ^ "| " ^ pat ^ " ->\n" ^ indent1 ^ e_to_string b.branch
       in
       let branches = List.map branch_to_string branches in
diff --git a/src/Pure.ml b/src/Pure.ml
index 243b493e..05f7e199 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -287,28 +287,25 @@ type var_or_dummy =
         polymorphic = false;
       }]
 
-(** A left value (which appears on the left of assignments.
- 
-    TODO: rename to "pattern"
- *)
-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 = {
+(** 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
+  | PatAdt of adt_pattern
+
+and adt_pattern = {
   variant_id : variant_id option;
-  field_values : typed_lvalue list;
+  field_values : typed_pattern list;
 }
 
-and typed_lvalue = { value : lvalue; ty : ty }
+and typed_pattern = { value : pattern; ty : ty }
 [@@deriving
   show,
     visitors
       {
-        name = "iter_typed_lvalue";
+        name = "iter_typed_pattern";
         variety = "iter";
         ancestors = [ "iter_var_or_dummy" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -317,7 +314,7 @@ and typed_lvalue = { value : lvalue; ty : ty }
       },
     visitors
       {
-        name = "map_typed_lvalue";
+        name = "map_typed_pattern";
         variety = "map";
         ancestors = [ "map_var_or_dummy" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -326,7 +323,7 @@ and typed_lvalue = { value : lvalue; ty : ty }
       },
     visitors
       {
-        name = "reduce_typed_lvalue";
+        name = "reduce_typed_pattern";
         variety = "reduce";
         ancestors = [ "reduce_var_or_dummy" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -334,7 +331,7 @@ and typed_lvalue = { value : lvalue; ty : ty }
       },
     visitors
       {
-        name = "mapreduce_typed_lvalue";
+        name = "mapreduce_typed_pattern";
         variety = "mapreduce";
         ancestors = [ "mapreduce_var_or_dummy" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -393,7 +390,7 @@ type var_id = VarId.id [@@deriving show]
 (** Ancestor for [iter_expression] visitor *)
 class ['self] iter_expression_base =
   object (_self : 'self)
-    inherit [_] iter_typed_lvalue
+    inherit [_] iter_typed_pattern
 
     method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
 
@@ -405,7 +402,7 @@ class ['self] iter_expression_base =
 (** Ancestor for [map_expression] visitor *)
 class ['self] map_expression_base =
   object (_self : 'self)
-    inherit [_] map_typed_lvalue
+    inherit [_] map_typed_pattern
 
     method visit_integer_type : 'env -> integer_type -> integer_type =
       fun _ x -> x
@@ -418,7 +415,7 @@ class ['self] map_expression_base =
 (** Ancestor for [reduce_expression] visitor *)
 class virtual ['self] reduce_expression_base =
   object (self : 'self)
-    inherit [_] reduce_typed_lvalue
+    inherit [_] reduce_typed_pattern
 
     method visit_integer_type : 'env -> integer_type -> 'a =
       fun _ _ -> self#zero
@@ -431,7 +428,7 @@ class virtual ['self] reduce_expression_base =
 (** Ancestor for [mapreduce_expression] visitor *)
 class virtual ['self] mapreduce_expression_base =
   object (self : 'self)
-    inherit [_] mapreduce_typed_lvalue
+    inherit [_] mapreduce_typed_pattern
 
     method visit_integer_type : 'env -> integer_type -> integer_type * 'a =
       fun _ x -> (x, self#zero)
@@ -463,9 +460,9 @@ type expression =
           field accesses with calls to projectors over fields (when there
           are clashes of field names, some provers like F* get pretty bad...)
        *)
-  | Abs of typed_lvalue * texpression  (** Lambda abstraction: `fun x -> e` *)
+  | Abs of typed_pattern * texpression  (** Lambda abstraction: `fun x -> e` *)
   | Qualif of qualif  (** A top-level qualifier *)
-  | Let of bool * typed_lvalue * texpression * texpression
+  | Let of bool * typed_pattern * texpression * texpression
       (** Let binding.
       
           TODO: the boolean should be replaced by an enum: sometimes we use
@@ -509,7 +506,7 @@ type expression =
 
 and switch_body = If of texpression * texpression | Match of match_branch list
 
-and match_branch = { pat : typed_lvalue; branch : texpression }
+and match_branch = { pat : typed_pattern; branch : texpression }
 
 and texpression = { e : expression; ty : ty }
 
@@ -587,8 +584,8 @@ type inst_fun_sig = { inputs : ty list; outputs : ty list }
 
 type fun_body = {
   inputs : var list;
-  inputs_lvs : typed_lvalue list;
-      (** The inputs seen as lvalues. Allows to make transformations, for example
+  inputs_lvs : typed_pattern list;
+      (** The inputs seen as patterns. Allows to make transformations, for example
           to replace unused variables by `_` *)
   body : texpression;
 }
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index b4f4462b..c84bf7cd 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -93,7 +93,7 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator =
       (* Get the maximum *)
 
       method! visit_var _ v _ = v.id
-      (** For the lvalues *)
+      (** For the patterns *)
 
       method! visit_Local _ vid _ = vid
       (** For the rvalues *)
@@ -117,7 +117,7 @@ type pn_ctx = {
     
     The way it works is as follows:
     - we only modify the names of the unnamed variables
-    - whenever we see an rvalue/lvalue which is exactly an unnamed variable,
+    - whenever we see an rvalue/pattern which is exactly an unnamed variable,
       and this value is linked to some meta-place information which contains
       a name and an empty path, we consider we should use this name
     - we try to propagate naming constraints on the pure variables use in the
@@ -290,16 +290,16 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
               | Some basename -> { v with basename = Some basename }
             else v)
   in
-  (* Update an lvalue - used to update an expression after we computed constraints *)
-  let update_typed_lvalue ctx (lv : typed_lvalue) : typed_lvalue =
+  (* Update an pattern - used to update an expression after we computed constraints *)
+  let update_typed_pattern ctx (lv : typed_pattern) : typed_pattern =
     let obj =
       object
-        inherit [_] map_typed_lvalue
+        inherit [_] map_typed_pattern
 
         method! visit_Var _ v mp = Var (update_var ctx v mp, mp)
       end
     in
-    obj#visit_typed_lvalue () lv
+    obj#visit_typed_pattern () lv
   in
 
   (* Register an mplace the first time we find one *)
@@ -353,10 +353,10 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     match (unmeta rv).e with Local vid -> add_constraint mp vid ctx | _ -> ctx
   in
   (* Specific case of constraint on left values *)
-  let add_left_constraint (lv : typed_lvalue) (ctx : pn_ctx) : pn_ctx =
+  let add_left_constraint (lv : typed_pattern) (ctx : pn_ctx) : pn_ctx =
     let obj =
       object (self)
-        inherit [_] reduce_typed_lvalue
+        inherit [_] reduce_typed_pattern
 
         method zero _ = empty_ctx
 
@@ -369,19 +369,19 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
           match mp with Some mp -> add_constraint mp v.id ctx | None -> ctx
       end
     in
-    let ctx1 = obj#visit_typed_lvalue () lv () in
+    let ctx1 = obj#visit_typed_pattern () lv () in
     merge_ctxs ctx ctx1
   in
 
   (* This is used to propagate constraint information about places in case of
    * variable reassignments: we try to propagate the information from the
    * rvalue to the left *)
-  let add_left_right_constraint (lv : typed_lvalue) (re : texpression)
+  let add_left_right_constraint (lv : typed_pattern) (re : texpression)
       (ctx : pn_ctx) : pn_ctx =
     (* We propagate constraints across variable reassignments: `^0 = x`,
      * if the destination doesn't have naming information *)
     match lv.value with
-    | LvVar (Var (({ id = _; basename = None; ty = _ } as lvar), lmp)) ->
+    | PatVar (Var (({ 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
@@ -444,18 +444,18 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     in
     (ctx, { e; ty })
   (* *)
-  and update_abs (x : typed_lvalue) (e : texpression) (ctx : pn_ctx) :
+  and update_abs (x : typed_pattern) (e : texpression) (ctx : pn_ctx) :
       pn_ctx * expression =
     (* We first add the left-constraint *)
     let ctx = add_left_constraint x ctx in
     (* Update the expression, and add additional constraints *)
     let ctx, e = update_texpression e ctx in
     (* Update the abstracted value *)
-    let x = update_typed_lvalue ctx x in
+    let x = update_typed_pattern ctx x in
     (* Put together *)
     (ctx, Abs (x, e))
   (* *)
-  and update_let (monadic : bool) (lv : typed_lvalue) (re : texpression)
+  and update_let (monadic : bool) (lv : typed_pattern) (re : texpression)
       (e : texpression) (ctx : pn_ctx) : pn_ctx * expression =
     (* We first add the left-constraint *)
     let ctx = add_left_constraint lv ctx in
@@ -464,7 +464,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     let ctx = add_left_right_constraint lv re ctx in
     let ctx, re = update_texpression re ctx in
     let ctx, e = update_texpression e ctx in
-    let lv = update_typed_lvalue ctx lv in
+    let lv = update_typed_pattern ctx lv in
     (ctx, Let (monadic, lv, re, e))
   (* *)
   and update_switch_body (scrut : texpression) (body : switch_body)
@@ -484,7 +484,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
               (fun br ->
                 let ctx = add_left_constraint br.pat ctx in
                 let ctx, branch = update_texpression br.branch ctx in
-                let pat = update_typed_lvalue ctx br.pat in
+                let pat = update_typed_pattern ctx br.pat in
                 (ctx, { pat; branch }))
               branches
           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, LvVar (Var (lv_var, _)) ->
+        | false, PatVar (Var (lv_var, _)) ->
             (* We can filter if: *)
             let filter = false in
             (* 1. Either:
@@ -806,7 +806,7 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
    *)
   let lv_visitor =
     object
-      inherit [_] mapreduce_typed_lvalue
+      inherit [_] mapreduce_typed_pattern
 
       method zero _ = true
 
@@ -820,9 +820,9 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
             else (Dummy, fun _ -> true)
     end
   in
-  let filter_typed_lvalue (used_vars : VarId.Set.t) (lv : typed_lvalue) :
-      typed_lvalue * bool =
-    let lv, all_dummies = lv_visitor#visit_typed_lvalue used_vars lv in
+  let filter_typed_pattern (used_vars : VarId.Set.t) (lv : typed_pattern) :
+      typed_pattern * bool =
+    let lv, all_dummies = lv_visitor#visit_typed_pattern used_vars lv in
     (lv, all_dummies ())
   in
 
@@ -854,7 +854,7 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
             let e, used = self#visit_texpression env e in
             let used = used () in
             (* Filter the left values *)
-            let lv, all_dummies = filter_typed_lvalue used lv in
+            let lv, all_dummies = filter_typed_pattern used lv in
             (* Small utility - called if we can't filter the let-binding *)
             let dont_filter () =
               let re, used_re = self#visit_texpression env re in
@@ -906,7 +906,7 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
       let inputs_lvs =
         if false then
           List.map
-            (fun lv -> fst (filter_typed_lvalue used_vars lv))
+            (fun lv -> fst (filter_typed_pattern used_vars lv))
             body.inputs_lvs
         else body.inputs_lvs
       in
@@ -974,7 +974,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
         match v with
         | Dummy -> Dummy
         | Var (v, mp) -> if v.ty = unit_ty then Dummy else Var (v, mp)
-      (** Replace in lvalues *)
+      (** Replace in patterns *)
 
       method! visit_texpression env e =
         if e.ty = unit_ty then unit_rvalue else super#visit_texpression env e
@@ -989,7 +989,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
   | Some body ->
       let body_exp = obj#visit_texpression () body.body in
       (* Update the input parameters *)
-      let inputs_lvs = List.map (obj#visit_typed_lvalue ()) body.inputs_lvs in
+      let inputs_lvs = List.map (obj#visit_typed_pattern ()) body.inputs_lvs in
       (* Return *)
       let body = Some { body with body = body_exp; inputs_lvs } in
       { def with body }
@@ -1089,7 +1089,7 @@ let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
                * - if not, make the decomposition in two steps
                *)
               match lv.value with
-              | LvVar _ ->
+              | PatVar _ ->
                   (* Variable: nothing to do *)
                   super#visit_Let env monadic lv re next_e
               | _ ->
@@ -1098,7 +1098,7 @@ let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
                    * monadic binding *)
                   let vid = fresh_id () in
                   let tmp : var = { id = vid; basename = None; ty = lv.ty } in
-                  let ltmp = mk_typed_lvalue_from_var tmp None in
+                  let ltmp = mk_typed_pattern_from_var tmp None in
                   let rtmp = mk_texpression_from_var tmp in
                   (* Visit the next expression *)
                   let next_e = self#visit_texpression env next_e in
@@ -1155,7 +1155,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
               (* Generate a fresh state variable *)
               let state_var = fresh_state_var () in
               let state_value = mk_texpression_from_var state_var in
-              let state_lvar = mk_typed_lvalue_from_var state_var None in
+              let state_lvar = mk_typed_pattern_from_var state_var None in
               (* Apply in all the branches and reconstruct the switch *)
               let mk_app e = mk_app e state_value in
               let switch_body = map_switch_body_branches mk_app switch_body in
@@ -1219,17 +1219,17 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
                   mk_app re state_value
                 in
                 (* Create the match *)
-                let fail_pat = mk_result_fail_lvalue re_no_monad_ty in
+                let fail_pat = mk_result_fail_pattern re_no_monad_ty in
                 let fail_value = mk_result_fail_rvalue e_no_monad_ty in
                 let fail_branch = { pat = fail_pat; branch = fail_value } in
                 (* The `Success` branch introduces a fresh state variable *)
                 let pat_state_var = fresh_state_var () in
-                let pat_state_lvalue =
-                  mk_typed_lvalue_from_var pat_state_var None
+                let pat_state_pattern =
+                  mk_typed_pattern_from_var pat_state_var None
                 in
                 let success_pat =
-                  mk_result_return_lvalue
-                    (mk_simpl_tuple_lvalue [ pat_state_lvalue; lv ])
+                  mk_result_return_pattern
+                    (mk_simpl_tuple_pattern [ pat_state_pattern; lv ])
                 in
                 let pat_state_rvalue = mk_texpression_from_var pat_state_var in
                 (* TODO: write a utility to create matches (and perform
@@ -1241,7 +1241,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
                 let e = Switch (re, switch_body) in
                 let e = { e; ty = e_no_arrow_ty } in
                 (* Add the lambda to introduce the state variable *)
-                let e = mk_abs (mk_typed_lvalue_from_var state_var None) e in
+                let e = mk_abs (mk_typed_pattern_from_var state_var None) e in
                 (* Sanity check *)
                 assert (e0.ty = e.ty);
                 assert (fail_branch.branch.ty = success_branch.branch.ty);
@@ -1250,10 +1250,10 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
               else
                 let re_ty = Option.get (opt_destruct_result re.ty) in
                 assert (lv.ty = re_ty);
-                let fail_pat = mk_result_fail_lvalue lv.ty in
+                let fail_pat = mk_result_fail_pattern lv.ty in
                 let fail_value = mk_result_fail_rvalue e.ty in
                 let fail_branch = { pat = fail_pat; branch = fail_value } in
-                let success_pat = mk_result_return_lvalue lv in
+                let success_pat = mk_result_return_pattern lv in
                 let success_branch = { pat = success_pat; branch = e } in
                 let switch_body = Match [ fail_branch; success_branch ] in
                 let e = Switch (re, switch_body) in
@@ -1282,7 +1282,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
           let sg = { sg with inputs = sg_inputs; outputs = sg_outputs } in
           (* Input list *)
           let inputs = body.inputs @ [ state_var ] in
-          let input_lv = mk_typed_lvalue_from_var state_var None in
+          let input_lv = mk_typed_pattern_from_var state_var None in
           let inputs_lvs = body.inputs_lvs @ [ input_lv ] in
           let body = { body = body_e; inputs; inputs_lvs } in
           (body, sg)
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index aaae94ca..0d941079 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -57,16 +57,16 @@ let compute_constant_value_ty (cv : constant_value) : ty =
   | Char _ -> Char
   | String _ -> Str
 
-let mk_typed_lvalue_from_constant_value (cv : constant_value) : typed_lvalue =
+let mk_typed_pattern_from_constant_value (cv : constant_value) : typed_pattern =
   let ty = compute_constant_value_ty cv in
-  { value = LvConcrete cv; ty }
+  { value = PatConcrete cv; ty }
 
 (*let mk_value_expression (v : typed_rvalue) (mp : mplace option) : texpression =
     let e = Value (v, mp) in
     let ty = v.ty in
   { e; ty }*)
 
-let mk_let (monadic : bool) (lv : typed_lvalue) (re : texpression)
+let mk_let (monadic : bool) (lv : typed_pattern) (re : texpression)
     (next_e : texpression) : texpression =
   let e = Let (monadic, lv, re, next_e) in
   let ty = next_e.ty in
@@ -273,12 +273,12 @@ let destruct_result (ty : ty) : ty = Option.get (opt_destruct_result ty)
 let opt_destruct_tuple (ty : ty) : ty list option =
   match ty with Adt (Tuple, tys) -> Some tys | _ -> None
 
-let mk_abs (x : typed_lvalue) (e : texpression) : texpression =
+let mk_abs (x : typed_pattern) (e : texpression) : texpression =
   let ty = Arrow (x.ty, e.ty) in
   let e = Abs (x, e) in
   { e; ty }
 
-let rec destruct_abs_list (e : texpression) : typed_lvalue list * texpression =
+let rec destruct_abs_list (e : texpression) : typed_pattern list * texpression =
   match e.e with
   | Abs (x, e') ->
       let xl, e'' = destruct_abs_list e' in
@@ -354,8 +354,8 @@ let mk_texpression_from_var (v : var) : texpression =
   let ty = v.ty in
   { e; ty }
 
-let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue =
-  let value = LvVar (Var (v, mp)) in
+let mk_typed_pattern_from_var (v : var) (mp : mplace option) : typed_pattern =
+  let value = PatVar (Var (v, mp)) in
   let ty = v.ty in
   { value; ty }
 
@@ -375,16 +375,16 @@ let mk_opt_mplace_texpression (mp : mplace option) (e : texpression) :
     - if there is exactly one value, just return it
     - if there is > one value: wrap them in a tuple
  *)
-let mk_simpl_tuple_lvalue (vl : typed_lvalue list) : typed_lvalue =
+let mk_simpl_tuple_pattern (vl : typed_pattern list) : typed_pattern =
   match vl with
   | [ v ] -> v
   | _ ->
-      let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in
+      let tys = List.map (fun (v : typed_pattern) -> v.ty) vl in
       let ty = Adt (Tuple, tys) in
-      let value = LvAdt { variant_id = None; field_values = vl } in
+      let value = PatAdt { variant_id = None; field_values = vl } in
       { value; ty }
 
-(** Similar to [mk_simpl_tuple_lvalue] *)
+(** Similar to [mk_simpl_tuple_pattern] *)
 let mk_simpl_tuple_texpression (vl : texpression list) : texpression =
   match vl with
   | [ v ] -> v
@@ -400,9 +400,9 @@ let mk_simpl_tuple_texpression (vl : texpression list) : texpression =
       let cons = { e = Qualif qualif; ty } in
       mk_apps cons vl
 
-let mk_adt_lvalue (adt_ty : ty) (variant_id : VariantId.id)
-    (vl : typed_lvalue list) : typed_lvalue =
-  let value = LvAdt { variant_id = Some variant_id; field_values = vl } in
+let mk_adt_pattern (adt_ty : ty) (variant_id : VariantId.id)
+    (vl : typed_pattern list) : typed_pattern =
+  let value = PatAdt { variant_id = Some variant_id; field_values = vl } in
   { value; ty = adt_ty }
 
 let ty_as_integer (t : ty) : T.integer_type =
@@ -442,15 +442,15 @@ let mk_result_return_rvalue (v : texpression) : texpression =
   let cons = { e = cons_e; ty = cons_ty } in
   mk_app cons v
 
-let mk_result_fail_lvalue (ty : ty) : typed_lvalue =
+let mk_result_fail_pattern (ty : ty) : typed_pattern =
   let ty = Adt (Assumed Result, [ ty ]) in
-  let value = LvAdt { variant_id = Some result_fail_id; field_values = [] } in
+  let value = PatAdt { variant_id = Some result_fail_id; field_values = [] } in
   { value; ty }
 
-let mk_result_return_lvalue (v : typed_lvalue) : typed_lvalue =
+let mk_result_return_pattern (v : typed_pattern) : typed_pattern =
   let ty = Adt (Assumed Result, [ v.ty ]) in
   let value =
-    LvAdt { variant_id = Some result_return_id; field_values = [ v ] }
+    PatAdt { variant_id = Some result_return_id; field_values = [ v ] }
   in
   { value; ty }
 
@@ -529,18 +529,18 @@ module TypeCheck = struct
     | Bool, Bool _ | Char, Char _ | Str, String _ -> ()
     | _ -> raise (Failure "Inconsistent type")
 
-  let rec check_typed_lvalue (ctx : tc_ctx) (v : typed_lvalue) : tc_ctx =
-    log#ldebug (lazy ("check_typed_lvalue: " ^ show_typed_lvalue v));
+  let rec check_typed_pattern (ctx : tc_ctx) (v : typed_pattern) : tc_ctx =
+    log#ldebug (lazy ("check_typed_pattern: " ^ show_typed_pattern v));
     match v.value with
-    | LvConcrete cv ->
+    | PatConcrete cv ->
         check_constant_value cv v.ty;
         ctx
-    | LvVar Dummy -> ctx
-    | LvVar (Var (var, _)) ->
+    | PatVar Dummy -> ctx
+    | PatVar (Var (var, _)) ->
         assert (var.ty = v.ty);
         let env = VarId.Map.add var.id var.ty ctx.env in
         { ctx with env }
-    | LvAdt av ->
+    | PatAdt av ->
         (* Compute the field types *)
         let type_id, tys =
           match v.ty with
@@ -550,13 +550,13 @@ module TypeCheck = struct
         let field_tys =
           get_adt_field_types ctx.type_decls type_id av.variant_id tys
         in
-        let check_value (ctx : tc_ctx) (ty : ty) (v : typed_lvalue) : tc_ctx =
+        let check_value (ctx : tc_ctx) (ty : ty) (v : typed_pattern) : tc_ctx =
           if ty <> v.ty then (
             log#serror
-              ("check_typed_lvalue: not the same types:" ^ "\n- ty: "
+              ("check_typed_pattern: not the same types:" ^ "\n- ty: "
              ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty);
             raise (Failure "Inconsistent types"));
-          check_typed_lvalue ctx v
+          check_typed_pattern ctx v
         in
         (* Check the field types - TODO: we might also want to check that the
          * type of the applied constructor is correct *)
@@ -587,7 +587,7 @@ module TypeCheck = struct
         assert (pat.ty = pat_ty);
         assert (body.ty = body_ty);
         (* Check the pattern and register the introduced variables at the same time *)
-        let ctx = check_typed_lvalue ctx pat in
+        let ctx = check_typed_pattern ctx pat in
         check_texpression ctx body
     | Qualif qualif -> (
         match qualif.id with
@@ -620,7 +620,7 @@ module TypeCheck = struct
         (* Check the right-expression *)
         check_texpression ctx re;
         (* Check the pattern and register the introduced variables at the same time *)
-        let ctx = check_typed_lvalue ctx pat in
+        let ctx = check_typed_pattern ctx pat in
         (* Check the next expression *)
         check_texpression ctx e_next
     | Switch (scrut, switch_body) -> (
@@ -635,7 +635,7 @@ module TypeCheck = struct
         | Match branches ->
             let check_branch (br : match_branch) : unit =
               assert (br.pat.ty = scrut.ty);
-              let ctx = check_typed_lvalue ctx br.pat in
+              let ctx = check_typed_pattern ctx br.pat in
               check_texpression ctx br.branch
             in
             List.iter check_branch branches)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 3a61784c..e8f37f1e 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -111,10 +111,10 @@ type bs_ctx = {
 }
 (** Body synthesis context *)
 
-let type_check_lvalue (ctx : bs_ctx) (v : typed_lvalue) : unit =
+let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
   let env = VarId.Map.empty in
   let ctx = { TypeCheck.type_decls = ctx.type_context.type_decls; env } in
-  let _ = TypeCheck.check_typed_lvalue ctx v in
+  let _ = TypeCheck.check_typed_pattern ctx v in
   ()
 
 let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
@@ -830,7 +830,7 @@ let translate_opt_mplace (p : S.mplace option) : mplace option =
 (** Explore an abstraction value and convert it to a given back value
     by collecting all the meta-values from the ended *borrows*.
 
-    Given back values are lvalues, because when an abstraction ends, we
+    Given back values are patterns, because when an abstraction ends, we
     introduce a call to a backward function in the synthesized program,
     which introduces new values:
     ```
@@ -842,7 +842,7 @@ let translate_opt_mplace (p : S.mplace option) : mplace option =
     the heuristics which later find pretty names for the variables.
  *)
 let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
-    (ctx : bs_ctx) : bs_ctx * typed_lvalue option =
+    (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   let ctx, value =
     match av.value with
     | AConcrete _ -> raise (Failure "Unreachable")
@@ -872,9 +872,9 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
             assert (variant_id = None);
             if field_values = [] then (ctx, None)
             else
-              (* Note that if there is exactly one field value, [mk_simpl_tuple_lvalue]
+              (* Note that if there is exactly one field value, [mk_simpl_tuple_pattern]
                * is the identity *)
-              let lv = mk_simpl_tuple_lvalue field_values in
+              let lv = mk_simpl_tuple_pattern field_values in
               (ctx, Some lv))
     | ABottom -> raise (Failure "Unreachable")
     | ALoan lc -> aloan_content_to_given_back mp lc ctx
@@ -884,12 +884,12 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
   in
   (* Sanity check - Rk.: we do this at every recursive call, which is a bit
    * expansive... *)
-  (match value with None -> () | Some value -> type_check_lvalue ctx value);
+  (match value with None -> () | Some value -> type_check_pattern ctx value);
   (* Return *)
   (ctx, value)
 
 and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content)
-    (ctx : bs_ctx) : bs_ctx * typed_lvalue option =
+    (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   match lc with
   | AMutLoan (_, _) | ASharedLoan (_, _, _) -> raise (Failure "Unreachable")
   | AEndedMutLoan { child = _; given_back = _; given_back_meta = _ }
@@ -907,14 +907,14 @@ and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content)
       (ctx, None)
 
 and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content)
-    (ctx : bs_ctx) : bs_ctx * typed_lvalue option =
+    (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   match bc with
   | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
       raise (Failure "Unreachable")
   | AEndedMutBorrow (msv, _) ->
       (* Return the meta-symbolic-value *)
       let ctx, var = fresh_var_for_symbolic_value msv ctx in
-      (ctx, Some (mk_typed_lvalue_from_var var mp))
+      (ctx, Some (mk_typed_pattern_from_var var mp))
   | AEndedIgnoredMutBorrow _ ->
       (* This happens with nested borrows: we need to dive in *)
       raise Unimplemented
@@ -923,7 +923,7 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content)
       (ctx, None)
 
 and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) :
-    bs_ctx * typed_lvalue option =
+    bs_ctx * typed_pattern option =
   match aproj with
   | V.AEndedProjLoans (_, child_projs) ->
       (* There may be children borrow projections in case of nested borrows,
@@ -936,7 +936,7 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) :
   | AEndedProjBorrows mv ->
       (* Return the meta-value *)
       let ctx, var = fresh_var_for_symbolic_value mv ctx in
-      (ctx, Some (mk_typed_lvalue_from_var var mp))
+      (ctx, Some (mk_typed_pattern_from_var var mp))
   | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
       raise (Failure "Unreachable")
 
@@ -945,7 +945,7 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) :
     See [typed_avalue_to_given_back].
  *)
 let abs_to_given_back (mpl : mplace option list) (abs : V.abs) (ctx : bs_ctx) :
-    bs_ctx * typed_lvalue list =
+    bs_ctx * typed_pattern list =
   let avalues = List.combine mpl abs.avalues in
   let ctx, values =
     List.fold_left_map
@@ -957,7 +957,7 @@ let abs_to_given_back (mpl : mplace option list) (abs : V.abs) (ctx : bs_ctx) :
 
 (** Simply calls [abs_to_given_back] *)
 let abs_to_given_back_no_mp (abs : V.abs) (ctx : bs_ctx) :
-    bs_ctx * typed_lvalue list =
+    bs_ctx * typed_pattern list =
   let mpl = List.map (fun _ -> None) abs.avalues in
   abs_to_given_back mpl abs ctx
 
@@ -1024,8 +1024,8 @@ and translate_panic (config : config) (ctx : bs_ctx) : texpression =
     let _, state_var =
       fresh_var (Some ConstStrings.state_basename) mk_state_ty ctx
     in
-    let state_lvalue = mk_typed_lvalue_from_var state_var None in
-    mk_abs state_lvalue ret_v
+    let state_pattern = mk_typed_pattern_from_var state_var None in
+    mk_abs state_pattern ret_v
   else mk_result_fail_rvalue ctx.ret_ty
 
 and translate_return (config : config) (opt_v : V.typed_value option)
@@ -1054,7 +1054,7 @@ and translate_return (config : config) (opt_v : V.typed_value option)
           mk_result_return_rvalue
             (mk_simpl_tuple_texpression [ state_rvalue; v ])
         in
-        let state_var = mk_typed_lvalue_from_var state_var None in
+        let state_var = mk_typed_pattern_from_var state_var None in
         mk_abs state_var ret_v
       else mk_result_return_rvalue v
   | Some bid ->
@@ -1078,7 +1078,7 @@ and translate_return (config : config) (opt_v : V.typed_value option)
           mk_result_return_rvalue
             (mk_simpl_tuple_texpression [ state_rvalue; ret_value ])
         in
-        let state_var = mk_typed_lvalue_from_var state_var None in
+        let state_var = mk_typed_pattern_from_var state_var None in
         mk_abs state_var ret_value
       else
         let ret_value = mk_simpl_tuple_texpression field_values in
@@ -1126,7 +1126,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
       (fun (arg, mp) -> mk_opt_mplace_texpression mp arg)
       (List.combine args args_mplaces)
   in
-  let dest_v = mk_typed_lvalue_from_var dest dest_mplace in
+  let dest_v = mk_typed_pattern_from_var dest dest_mplace in
   let func = { id = Func fun_id; type_params } in
   let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
   let ret_ty = mk_function_ret_ty config monadic state_monad dest_v.ty in
@@ -1192,7 +1192,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
       let monadic = false in
       List.fold_right
         (fun (var, value) (e : texpression) ->
-          mk_let monadic (mk_typed_lvalue_from_var var None) value e)
+          mk_let monadic (mk_typed_pattern_from_var var None) value e)
         variables_values next_e
   | V.FunCall ->
       let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in
@@ -1221,7 +1221,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
         List.append (List.map translate_opt_mplace call.args_places) [ None ]
       in
       let ctx, outputs = abs_to_given_back output_mpl abs ctx in
-      let output = mk_simpl_tuple_lvalue outputs in
+      let output = mk_simpl_tuple_pattern outputs in
       (* Sanity check: the inputs and outputs have the proper number and the proper type *)
       let fun_id =
         match call.call_id with
@@ -1244,7 +1244,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
           ^ "\n- expected outputs: "
           ^ string_of_int (List.length inst_sg.outputs)));
       List.iter
-        (fun (x, ty) -> assert ((x : typed_lvalue).ty = ty))
+        (fun (x, ty) -> assert ((x : typed_pattern).ty = ty))
         (List.combine outputs inst_sg.outputs);
       (* Retrieve the function id, and register the function call in the context
        * if necessary *)
@@ -1326,7 +1326,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
       let given_back_inputs = List.combine given_back inputs in
       (* Sanity check *)
       List.iter
-        (fun ((given_back, input) : typed_lvalue * var) ->
+        (fun ((given_back, input) : typed_pattern * var) ->
           log#ldebug
             (lazy
               ("\n- given_back ty: "
@@ -1364,7 +1364,7 @@ and translate_expansion (config : config) (p : S.mplace option)
           let next_e = translate_expression config e ctx in
           let monadic = false in
           mk_let monadic
-            (mk_typed_lvalue_from_var var None)
+            (mk_typed_pattern_from_var var None)
             (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
             next_e
       | SeAdt _ ->
@@ -1388,9 +1388,9 @@ and translate_expansion (config : config) (p : S.mplace option)
                 (* This is an enumeration: introduce an [ExpandEnum] let-binding *)
                 let variant_id = Option.get variant_id in
                 let lvars =
-                  List.map (fun v -> mk_typed_lvalue_from_var v None) vars
+                  List.map (fun v -> mk_typed_pattern_from_var v None) vars
                 in
-                let lv = mk_adt_lvalue scrutinee.ty variant_id lvars in
+                let lv = mk_adt_pattern scrutinee.ty variant_id lvars in
                 let monadic = false in
 
                 mk_let monadic lv
@@ -1421,16 +1421,16 @@ and translate_expansion (config : config) (p : S.mplace option)
                   (fun (fid, var) e ->
                     let field_proj = gen_field_proj fid var in
                     mk_let monadic
-                      (mk_typed_lvalue_from_var var None)
+                      (mk_typed_pattern_from_var var None)
                       field_proj e)
                   id_var_pairs branch
           | T.Tuple ->
               let vars =
-                List.map (fun x -> mk_typed_lvalue_from_var x None) vars
+                List.map (fun x -> mk_typed_pattern_from_var x None) vars
               in
               let monadic = false in
               mk_let monadic
-                (mk_simpl_tuple_lvalue vars)
+                (mk_simpl_tuple_pattern vars)
                 (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
                 branch
           | T.Assumed T.Box ->
@@ -1444,7 +1444,7 @@ and translate_expansion (config : config) (p : S.mplace option)
                * identity when extracted (`box a == a`) *)
               let monadic = false in
               mk_let monadic
-                (mk_typed_lvalue_from_var var None)
+                (mk_typed_pattern_from_var var None)
                 (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
                 branch
           | T.Assumed T.Vec ->
@@ -1465,10 +1465,10 @@ and translate_expansion (config : config) (p : S.mplace option)
             let variant_id = Option.get variant_id in
             let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
             let vars =
-              List.map (fun x -> mk_typed_lvalue_from_var x None) vars
+              List.map (fun x -> mk_typed_pattern_from_var x None) vars
             in
             let pat_ty = scrutinee.ty in
-            let pat = mk_adt_lvalue pat_ty variant_id vars in
+            let pat = mk_adt_pattern pat_ty variant_id vars in
             let branch = translate_expression config branch ctx in
             { pat; branch }
           in
@@ -1506,13 +1506,15 @@ and translate_expansion (config : config) (p : S.mplace option)
         (* We don't need to update the context: we don't introduce any
          * new values/variables *)
         let branch = translate_expression config branch_e ctx in
-        let pat = mk_typed_lvalue_from_constant_value (V.Scalar v) in
+        let pat = mk_typed_pattern_from_constant_value (V.Scalar v) in
         { pat; branch }
       in
       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_lvalue = { value = LvVar Dummy; ty = pat_ty } in
+      let otherwise_pat : typed_pattern =
+        { value = PatVar Dummy; ty = pat_ty }
+      in
       let otherwise : match_branch =
         { pat = otherwise_pat; branch = otherwise }
       in
@@ -1584,7 +1586,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
         in
         let inputs = List.append ctx.forward_inputs backward_inputs in
         let inputs_lvs =
-          List.map (fun v -> mk_typed_lvalue_from_var v None) inputs
+          List.map (fun v -> mk_typed_pattern_from_var v None) inputs
         in
         (* Sanity check *)
         assert (