Merge the rvalues with the expressions

5 files changed, 497 insertions, 371 deletions

diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 1a38e504..cf8c3f57 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -234,11 +234,62 @@ let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
   let name = name ^ "^" ^ V.VarId.to_string p.var_id ^ "llbc" in
   projection_to_string fmt name p.projection
 
-let place_to_string (fmt : ast_formatter) (p : place) : string =
-  (* TODO: improve that *)
-  let var = fmt.var_id_to_string p.var in
-  projection_to_string fmt var p.projection
+let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
+    (variant_id : VariantId.id option) : string =
+  match adt_id with
+  | Tuple -> "Tuple"
+  | AdtId def_id -> (
+      (* "Regular" ADT *)
+      match variant_id with
+      | Some vid -> fmt.adt_variant_to_string def_id vid
+      | None -> fmt.type_decl_id_to_string def_id)
+  | Assumed aty -> (
+      (* Assumed type *)
+      match aty with
+      | State ->
+          (* The `State` type is opaque: we can't get there *)
+          raise (Failure "Unreachable")
+      | Result ->
+          let variant_id = Option.get variant_id in
+          if variant_id = result_return_id then "@Result::Return"
+          else if variant_id = result_fail_id then "@Result::Fail"
+          else
+            raise (Failure "Unreachable: improper variant id for result type")
+      | Option ->
+          let variant_id = Option.get variant_id in
+          if variant_id = option_some_id then "@Option::Some "
+          else if variant_id = option_none_id then "@Option::None"
+          else
+            raise (Failure "Unreachable: improper variant id for result type")
+      | Vec ->
+          assert (variant_id = None);
+          "Vec")
+
+let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
+    (field_id : FieldId.id) : string =
+  match adt_id with
+  | Tuple ->
+      raise (Failure "Unreachable")
+      (* Tuples don't use the opaque field id for the field indices, but `int` *)
+  | AdtId def_id -> (
+      (* "Regular" ADT *)
+      let fields = fmt.adt_field_names def_id None in
+      match fields with
+      | None -> FieldId.to_string field_id
+      | Some fields -> FieldId.nth fields field_id)
+  | Assumed aty -> (
+      (* Assumed type *)
+      match aty with
+      | State | Vec ->
+          (* Opaque types: we can't get there *)
+          raise (Failure "Unreachable")
+      | Result | Option ->
+          (* Enumerations: we can't get there *)
+          raise (Failure "Unreachable"))
 
+(** TODO: we don't need a general function anymore (it is now only used for
+    lvalues (i.e., patterns)
+ *)
 let adt_g_value_to_string (fmt : value_formatter)
     (value_to_string : 'v -> string) (variant_id : VariantId.id option)
     (field_values : 'v list) (ty : ty) : string =
@@ -311,17 +362,6 @@ 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 rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string
-    =
-  match v.value with
-  | RvConcrete cv -> Print.Values.constant_value_to_string cv
-  | RvPlace p -> place_to_string fmt p
-  | RvAdt av ->
-      adt_g_value_to_string
-        (ast_to_value_formatter fmt)
-        (typed_rvalue_to_string fmt)
-        av.variant_id av.field_values v.ty
-
 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
@@ -411,33 +451,19 @@ let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string =
   | Binop (binop, int_ty) ->
       binop_to_string binop ^ "<" ^ integer_type_to_string int_ty ^ ">"
 
-let meta_to_string (fmt : ast_formatter) (meta : meta) : string =
-  let meta =
-    match meta with
-    | Assignment (lp, rv, rp) ->
-        let rp =
-          match rp with
-          | None -> ""
-          | Some rp -> " [@src=" ^ mplace_to_string fmt rp ^ "]"
-        in
-        "@assign(" ^ mplace_to_string fmt lp ^ " := "
-        ^ typed_rvalue_to_string fmt rv
-        ^ rp ^ ")"
-  in
-  "@meta[" ^ meta ^ "]"
-
 (** [inside]: controls the introduction of parentheses *)
 let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
     (indent : string) (indent_incr : string) (e : texpression) : string =
   match e.e with
-  | Value (v, mp) ->
+  | Local (var_id, mp) ->
       let mp =
         match mp with
         | None -> ""
         | Some mp -> " [@mplace=" ^ mplace_to_string fmt mp ^ "]"
       in
-      let e = typed_rvalue_to_string fmt v ^ mp in
-      if inside then "(" ^ e ^ ")" else e
+      let s = fmt.var_id_to_string var_id ^ mp in
+      if inside then "(" ^ s ^ ")" else s
+  | Const cv -> Print.Values.constant_value_to_string cv
   | App _ ->
       (* Recursively destruct the app, to have a pair (app, arguments list) *)
       let app, args = destruct_apps e in
@@ -447,8 +473,8 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
       let xl, e = destruct_abs_list e in
       let e = abs_to_string fmt indent indent_incr xl e in
       if inside then "(" ^ e ^ ")" else e
-  | Func _ ->
-      (* Func without arguments *)
+  | Qualif _ ->
+      (* Qualifier without arguments *)
       app_to_string fmt inside indent indent_incr e []
   | Let (monadic, lv, re, e) ->
       let e = let_to_string fmt indent indent_incr monadic lv re e in
@@ -466,18 +492,36 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
     (indent_incr : string) (app : texpression) (args : texpression list) :
     string =
   (* There are two possibilities: either the `app` is an instantiated,
-   * top-level function, or it is a "regular" expression *)
+   * top-level qualifier (function, ADT constructore...), or it is a "regular"
+   * expression *)
   let app, tys =
     match app.e with
-    | Func func ->
-        (* Function case *)
-        (* Convert the function identifier *)
-        let fun_id = fun_id_to_string fmt func.func in
+    | Qualif qualif ->
+        (* Qualifier case *)
+        (* Convert the qualifier identifier *)
+        let qualif_s =
+          match qualif.id with
+          | Func fun_id -> fun_id_to_string fmt fun_id
+          | AdtCons adt_cons_id ->
+              let variant_s =
+                adt_variant_to_string
+                  (ast_to_value_formatter fmt)
+                  adt_cons_id.adt_id adt_cons_id.variant_id
+              in
+              ConstStrings.constructor_prefix ^ variant_s
+          | Proj (ProjField (adt_id, field_id)) ->
+              let value_fmt = ast_to_value_formatter fmt in
+              let adt_s = adt_variant_to_string value_fmt adt_id None in
+              let field_s = adt_field_to_string value_fmt adt_id field_id in
+              (* Adopting an F*-like syntax *)
+              ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s
+          | Proj (ProjTuple field_id) -> "MkTuple?." ^ string_of_int field_id
+        in
         (* Convert the type instantiation *)
         let ty_fmt = ast_to_type_formatter fmt in
-        let tys = List.map (ty_to_string ty_fmt) func.type_params in
+        let tys = List.map (ty_to_string ty_fmt) qualif.type_params in
         (* *)
-        (fun_id, tys)
+        (qualif_s, tys)
     | _ ->
         (* "Regular" expression case *)
         let inside = args <> [] || (args = [] && inside) in
@@ -540,6 +584,21 @@ and switch_to_string (fmt : ast_formatter) (indent : string)
       let branches = List.map branch_to_string branches in
       "match " ^ scrut ^ " with\n" ^ String.concat "\n" branches
 
+and meta_to_string (fmt : ast_formatter) (meta : meta) : string =
+  let meta =
+    match meta with
+    | Assignment (lp, rv, rp) ->
+        let rp =
+          match rp with
+          | None -> ""
+          | Some rp -> " [@src=" ^ mplace_to_string fmt rp ^ "]"
+        in
+        "@assign(" ^ mplace_to_string fmt lp ^ " := "
+        ^ texpression_to_string fmt false "" "" rv
+        ^ rp ^ ")"
+  in
+  "@meta[" ^ meta ^ "]"
+
 let fun_decl_to_string (fmt : ast_formatter) (def : fun_decl) : string =
   let type_fmt = ast_to_type_formatter fmt in
   let name = fun_name_to_string def.basename ^ fun_suffix def.back_id in
diff --git a/src/Pure.ml b/src/Pure.ml
index cd28b035..c72f9dd0 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -149,7 +149,9 @@ type var = {
 
 (* TODO: we might want to redefine field_proj_kind here, to prevent field accesses
  * on enumerations.
- * Also: tuples... *)
+ * Also: tuples...
+ * Rmk: projections are actually only used as meta-data.
+ * *)
 type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id }
 [@@deriving show]
 
@@ -168,9 +170,6 @@ type mplace = {
     we introduce.
  *)
 
-(* TODO: there shouldn't be places *)
-type place = { var : VarId.id; projection : projection } [@@deriving show]
-
 type variant_id = VariantId.id [@@deriving show]
 
 (** Ancestor for [iter_var_or_dummy] visitor *)
@@ -182,8 +181,6 @@ class ['self] iter_value_base =
 
     method visit_var : 'env -> var -> unit = fun _ _ -> ()
 
-    method visit_place : 'env -> place -> unit = fun _ _ -> ()
-
     method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
 
     method visit_ty : 'env -> ty -> unit = fun _ _ -> ()
@@ -201,8 +198,6 @@ class ['self] map_value_base =
 
     method visit_var : 'env -> var -> var = fun _ x -> x
 
-    method visit_place : 'env -> place -> place = fun _ x -> x
-
     method visit_mplace : 'env -> mplace -> mplace = fun _ x -> x
 
     method visit_ty : 'env -> ty -> ty = fun _ x -> x
@@ -220,8 +215,6 @@ class virtual ['self] reduce_value_base =
 
     method visit_var : 'env -> var -> 'a = fun _ _ -> self#zero
 
-    method visit_place : 'env -> place -> 'a = fun _ _ -> self#zero
-
     method visit_mplace : 'env -> mplace -> 'a = fun _ _ -> self#zero
 
     method visit_ty : 'env -> ty -> 'a = fun _ _ -> self#zero
@@ -240,8 +233,6 @@ class virtual ['self] mapreduce_value_base =
 
     method visit_var : 'env -> var -> var * 'a = fun _ x -> (x, self#zero)
 
-    method visit_place : 'env -> place -> place * 'a = fun _ x -> (x, self#zero)
-
     method visit_mplace : 'env -> mplace -> mplace * 'a =
       fun _ x -> (x, self#zero)
 
@@ -251,57 +242,6 @@ class virtual ['self] mapreduce_value_base =
       fun _ x -> (x, self#zero)
   end
 
-(* TODO: merge with expressions *)
-type rvalue =
-  | RvConcrete of constant_value
-  | RvPlace of place (* TODO: field projectors should be expressions *)
-  | RvAdt of adt_rvalue
-
-and adt_rvalue = {
-  variant_id : variant_id option;
-  (* TODO: variant constructors should be expressions, treated in a manner
-   * similar to functions *)
-  field_values : typed_rvalue list;
-}
-
-and typed_rvalue = { value : rvalue; ty : ty }
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_typed_rvalue";
-        variety = "iter";
-        ancestors = [ "iter_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
-        concrete = true;
-        polymorphic = false;
-      },
-    visitors
-      {
-        name = "map_typed_rvalue";
-        variety = "map";
-        ancestors = [ "map_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
-        concrete = true;
-        polymorphic = false;
-      },
-    visitors
-      {
-        name = "reduce_typed_rvalue";
-        variety = "reduce";
-        ancestors = [ "reduce_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
-        polymorphic = false;
-      },
-    visitors
-      {
-        name = "mapreduce_typed_rvalue";
-        variety = "mapreduce";
-        ancestors = [ "mapreduce_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
-        polymorphic = false;
-      }]
-
 type var_or_dummy =
   | Var of var * mplace option
       (** Rk.: the mdplace is actually always a variable (i.e.: there are no projections).
@@ -316,7 +256,7 @@ type var_or_dummy =
       {
         name = "iter_var_or_dummy";
         variety = "iter";
-        ancestors = [ "iter_typed_rvalue" ];
+        ancestors = [ "iter_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
         polymorphic = false;
@@ -325,7 +265,7 @@ type var_or_dummy =
       {
         name = "map_var_or_dummy";
         variety = "map";
-        ancestors = [ "map_typed_rvalue" ];
+        ancestors = [ "map_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.map] *);
         concrete = true;
         polymorphic = false;
@@ -334,7 +274,7 @@ type var_or_dummy =
       {
         name = "reduce_var_or_dummy";
         variety = "reduce";
-        ancestors = [ "reduce_typed_rvalue" ];
+        ancestors = [ "reduce_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.reduce] *);
         polymorphic = false;
       },
@@ -342,7 +282,7 @@ type var_or_dummy =
       {
         name = "mapreduce_var_or_dummy";
         variety = "mapreduce";
-        ancestors = [ "mapreduce_typed_rvalue" ];
+        ancestors = [ "mapreduce_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.reduce] *);
         polymorphic = false;
       }]
@@ -419,30 +359,43 @@ type fun_id =
   | Binop of E.binop * integer_type
 [@@deriving show, ord]
 
-(** Meta-information stored in the AST *)
-type meta = Assignment of mplace * typed_rvalue * mplace option
+type adt_cons_id = { adt_id : type_id; variant_id : variant_id option }
+[@@deriving show]
+(** An identifier for an ADT constructor *)
+
+type proj_kind = ProjField of type_id * FieldId.id | ProjTuple of int
 [@@deriving show]
 
-type func = { func : fun_id; type_params : ty list } [@@deriving show]
-(** A function.
+type qualif_id =
+  | Func of fun_id
+  | AdtCons of adt_cons_id  (** A function or ADT constructor identifier *)
+  | Proj of proj_kind  (** Field projector *)
+[@@deriving show]
+
+type qualif = {
+  id : qualif_id;
+  type_params : ty list; (* TODO: rename to type_args *)
+}
+[@@deriving show]
+(** An instantiated qualified.
 
     Note that for now we have a clear separation between types and expressions,
-    which explains why we have the `type_params` field: a function is always
-    fully instantiated.
+    which explains why we have the `type_params` field: a function or ADT
+    constructor is always fully instantiated.
  *)
 
+type var_id = VarId.id [@@deriving show]
+
 (** Ancestor for [iter_expression] visitor *)
 class ['self] iter_expression_base =
   object (_self : 'self)
     inherit [_] iter_typed_lvalue
 
-    method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
-
     method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
 
-    method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> ()
+    method visit_var_id : 'env -> var_id -> unit = fun _ _ -> ()
 
-    method visit_func : 'env -> func -> unit = fun _ _ -> ()
+    method visit_qualif : 'env -> qualif -> unit = fun _ _ -> ()
   end
 
 (** Ancestor for [map_expression] visitor *)
@@ -450,15 +403,12 @@ class ['self] map_expression_base =
   object (_self : 'self)
     inherit [_] map_typed_lvalue
 
-    method visit_meta : 'env -> meta -> meta = fun _ x -> x
-
     method visit_integer_type : 'env -> integer_type -> integer_type =
       fun _ x -> x
 
-    method visit_scalar_value : 'env -> scalar_value -> scalar_value =
-      fun _ x -> x
+    method visit_var_id : 'env -> var_id -> var_id = fun _ x -> x
 
-    method visit_func : 'env -> func -> func = fun _ x -> x
+    method visit_qualif : 'env -> qualif -> qualif = fun _ x -> x
   end
 
 (** Ancestor for [reduce_expression] visitor *)
@@ -466,15 +416,12 @@ class virtual ['self] reduce_expression_base =
   object (self : 'self)
     inherit [_] reduce_typed_lvalue
 
-    method visit_meta : 'env -> meta -> 'a = fun _ _ -> self#zero
-
     method visit_integer_type : 'env -> integer_type -> 'a =
       fun _ _ -> self#zero
 
-    method visit_scalar_value : 'env -> scalar_value -> 'a =
-      fun _ _ -> self#zero
+    method visit_var_id : 'env -> var_id -> 'a = fun _ _ -> self#zero
 
-    method visit_func : 'env -> func -> 'a = fun _ _ -> self#zero
+    method visit_qualif : 'env -> qualif -> 'a = fun _ _ -> self#zero
   end
 
 (** Ancestor for [mapreduce_expression] visitor *)
@@ -482,15 +429,14 @@ class virtual ['self] mapreduce_expression_base =
   object (self : 'self)
     inherit [_] mapreduce_typed_lvalue
 
-    method visit_meta : 'env -> meta -> meta * 'a = fun _ x -> (x, self#zero)
-
     method visit_integer_type : 'env -> integer_type -> integer_type * 'a =
       fun _ x -> (x, self#zero)
 
-    method visit_scalar_value : 'env -> scalar_value -> scalar_value * 'a =
+    method visit_var_id : 'env -> var_id -> var_id * 'a =
       fun _ x -> (x, self#zero)
 
-    method visit_func : 'env -> func -> func * 'a = fun _ x -> (x, self#zero)
+    method visit_qualif : 'env -> qualif -> qualif * 'a =
+      fun _ x -> (x, self#zero)
   end
 
 (** **Rk.:** here, [expression] is not at all equivalent to the expressions
@@ -498,7 +444,12 @@ class virtual ['self] mapreduce_expression_base =
     more general than the LLBC statements, in a sense.
  *)
 type expression =
-  | Value of typed_rvalue * mplace option
+  | Local of var_id * mplace option
+      (** 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`.
+       *)
+  | Const of constant_value
   | App of texpression * texpression
       (** Application of a function to an argument.
 
@@ -509,7 +460,7 @@ type expression =
           are clashes of field names, some provers like F* get pretty bad...)
        *)
   | Abs of typed_lvalue * texpression  (** Lambda abstraction: `fun x -> e` *)
-  | Func of func  (** A function - TODO: change to Qualifier *)
+  | Qualif of qualif  (** A top-level qualifier *)
   | Let of bool * typed_lvalue * texpression * texpression
       (** Let binding.
       
@@ -550,13 +501,25 @@ type expression =
           ```
        *)
   | Switch of texpression * switch_body
-  | Meta of meta * texpression  (** Meta-information *)
+  | Meta of (meta[@opaque]) * texpression  (** Meta-information *)
 
 and switch_body = If of texpression * texpression | Match of match_branch list
 
 and match_branch = { pat : typed_lvalue; branch : texpression }
 
 and texpression = { e : expression; ty : ty }
+
+and mvalue = (texpression[@opaque])
+(** Meta-value (converted to an expression) *)
+
+and meta =
+  | Assignment of mplace * mvalue * mplace option
+      (** Meta-information stored in the AST.
+
+          The first mplace stores the destination.
+          The mvalue stores the value which is put in the destination
+          The second (optional) mplace stores the origin.
+        *)
 [@@deriving
   show,
     visitors
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 9ddc71ab..3c25e7b6 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -1160,7 +1160,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
       in
       let fresh_state_var () =
         let id = fresh_var_id () in
-        { id; basename = Some "st"; ty = mk_state_ty }
+        { id; basename = Some ConstStrings.state_basename; ty = mk_state_ty }
       in
       (* It is a very simple map *)
       let obj =
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 873931be..c01dd5c9 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -43,96 +43,7 @@ let binop_can_fail (binop : E.binop) : bool =
   | Div | Rem | Add | Sub | Mul -> true
   | Shl | Shr -> raise Errors.Unimplemented
 
-let mk_place_from_var (v : var) : place = { var = v.id; projection = [] }
-
-(** Make a "simplified" tuple type from a list of types:
-    - if there is exactly one type, just return it
-    - if there is > one type: wrap them in a tuple
- *)
-let mk_simpl_tuple_ty (tys : ty list) : ty =
-  match tys with [ ty ] -> ty | _ -> Adt (Tuple, tys)
-
-let unit_ty : ty = Adt (Tuple, [])
-
-let unit_rvalue : typed_rvalue =
-  let value = RvAdt { variant_id = None; field_values = [] } in
-  let ty = unit_ty in
-  { value; ty }
-
-let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
-  let value = RvPlace (mk_place_from_var v) in
-  let ty = v.ty in
-  { value; ty }
-
-let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue =
-  let value = LvVar (Var (v, mp)) in
-  let ty = v.ty in
-  { value; ty }
-
-(** Make a "simplified" tuple value from a list of values:
-    - 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 =
-  match vl with
-  | [ v ] -> v
-  | _ ->
-      let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in
-      let ty = Adt (Tuple, tys) in
-      let value = LvAdt { variant_id = None; field_values = vl } in
-      { value; ty }
-
-(** Similar to [mk_simpl_tuple_lvalue] *)
-let mk_simpl_tuple_rvalue (vl : typed_rvalue list) : typed_rvalue =
-  match vl with
-  | [ v ] -> v
-  | _ ->
-      let tys = List.map (fun (v : typed_rvalue) -> v.ty) vl in
-      let ty = Adt (Tuple, tys) in
-      let value = RvAdt { variant_id = None; field_values = vl } in
-      { value; ty }
-
-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
-  { value; ty = adt_ty }
-
-let ty_as_integer (t : ty) : T.integer_type =
-  match t with Integer int_ty -> int_ty | _ -> raise (Failure "Unreachable")
-
-(* TODO: move *)
-let type_decl_is_enum (def : T.type_decl) : bool =
-  match def.kind with T.Struct _ -> false | Enum _ -> true | Opaque -> false
-
-let mk_state_ty : ty = Adt (Assumed State, [])
-
-let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ])
-
-let mk_result_fail_rvalue (ty : ty) : typed_rvalue =
-  let ty = Adt (Assumed Result, [ ty ]) in
-  let value = RvAdt { variant_id = Some result_fail_id; field_values = [] } in
-  { value; ty }
-
-let mk_result_return_rvalue (v : typed_rvalue) : typed_rvalue =
-  let ty = Adt (Assumed Result, [ v.ty ]) in
-  let value =
-    RvAdt { variant_id = Some result_return_id; field_values = [ v ] }
-  in
-  { value; ty }
-
-let mk_result_fail_lvalue (ty : ty) : typed_lvalue =
-  let ty = Adt (Assumed Result, [ ty ]) in
-  let value = LvAdt { variant_id = Some result_fail_id; field_values = [] } in
-  { value; ty }
-
-let mk_result_return_lvalue (v : typed_lvalue) : typed_lvalue =
-  let ty = Adt (Assumed Result, [ v.ty ]) in
-  let value =
-    LvAdt { variant_id = Some result_return_id; field_values = [ v ] }
-  in
-  { value; ty }
-
-let mk_arrow_ty (arg_ty : ty) (ret_ty : ty) : ty = Arrow (arg_ty, ret_ty)
+(*let mk_arrow_ty (arg_ty : ty) (ret_ty : ty) : ty = Arrow (arg_ty, ret_ty)*)
 
 let dest_arrow_ty (ty : ty) : ty * ty =
   match ty with
@@ -150,10 +61,10 @@ 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
-  { e; 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)
     (next_e : texpression) : texpression =
@@ -244,9 +155,12 @@ let functions_not_mutually_recursive (funs : fun_decl list) : bool =
       object
         inherit [_] iter_expression as super
 
-        method! visit_func env func =
-          if FunIdSet.mem func.func !ids then raise Utils.Found
-          else super#visit_func env func
+        method! visit_qualif env qualif =
+          match qualif.id with
+          | Func fun_id ->
+              if FunIdSet.mem fun_id !ids then raise Utils.Found
+              else super#visit_qualif env qualif
+          | _ -> super#visit_qualif env qualif
       end
     in
 
@@ -266,126 +180,24 @@ let functions_not_mutually_recursive (funs : fun_decl list) : bool =
  *)
 let rec let_group_requires_parentheses (e : texpression) : bool =
   match e.e with
-  | Value _ | App _ | Func _ | Abs _ -> false
+  | Local _ | 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
 
-(** Module to perform type checking - we use this for sanity checks only *)
-module TypeCheck = struct
-  type tc_ctx = { type_decls : type_decl TypeDeclId.Map.t }
-
-  let check_constant_value (ty : ty) (v : constant_value) : unit =
-    match (ty, v) with
-    | Integer int_ty, V.Scalar sv -> assert (int_ty = sv.V.int_ty)
-    | Bool, Bool _ | Char, Char _ | Str, String _ -> ()
-    | _ -> raise (Failure "Inconsistent type")
-
-  let check_adt_g_value (ctx : tc_ctx) (check_value : ty -> 'v -> unit)
-      (variant_id : VariantId.id option) (field_values : 'v list) (ty : ty) :
-      unit =
-    (* Retrieve the field types *)
-    let field_tys =
-      match ty with
-      | Adt (Tuple, tys) ->
-          (* Tuple *)
-          tys
-      | Adt (AdtId def_id, tys) ->
-          (* "Regular" ADT *)
-          let def = TypeDeclId.Map.find def_id ctx.type_decls in
-          type_decl_get_instantiated_fields_types def variant_id tys
-      | Adt (Assumed aty, tys) -> (
-          (* Assumed type *)
-          match aty with
-          | State ->
-              (* `State` is opaque *)
-              raise (Failure "Unreachable: `State` values are opaque")
-          | Result ->
-              let ty = Collections.List.to_cons_nil tys in
-              let variant_id = Option.get variant_id in
-              if variant_id = result_return_id then [ ty ]
-              else if variant_id = result_fail_id then []
-              else
-                raise
-                  (Failure "Unreachable: improper variant id for result type")
-          | Option ->
-              let ty = Collections.List.to_cons_nil tys in
-              let variant_id = Option.get variant_id in
-              if variant_id = option_some_id then [ ty ]
-              else if variant_id = option_none_id then []
-              else
-                raise
-                  (Failure "Unreachable: improper variant id for result type")
-          | Vec ->
-              assert (variant_id = None);
-              let ty = Collections.List.to_cons_nil tys in
-              List.map (fun _ -> ty) field_values)
-      | _ -> raise (Failure "Inconsistently typed value")
-    in
-    (* Check that the field values have the expected types *)
-    List.iter
-      (fun (ty, v) -> check_value ty v)
-      (List.combine field_tys field_values)
-
-  let rec check_typed_lvalue (ctx : tc_ctx) (v : typed_lvalue) : unit =
-    log#ldebug (lazy ("check_typed_lvalue: " ^ show_typed_lvalue v));
-    match v.value with
-    | LvConcrete cv -> check_constant_value v.ty cv
-    | LvVar _ -> ()
-    | LvAdt av ->
-        check_adt_g_value ctx
-          (fun ty (v : typed_lvalue) ->
-            if ty <> v.ty then (
-              log#serror
-                ("check_typed_lvalue: 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)
-          av.variant_id av.field_values v.ty
-
-  let rec check_typed_rvalue (ctx : tc_ctx) (v : typed_rvalue) : unit =
-    log#ldebug (lazy ("check_typed_rvalue: " ^ show_typed_rvalue v));
-    match v.value with
-    | RvConcrete cv -> check_constant_value v.ty cv
-    | RvPlace _ ->
-        (* TODO: *)
-        ()
-    | RvAdt av ->
-        check_adt_g_value ctx
-          (fun ty (v : typed_rvalue) ->
-            if ty <> v.ty then (
-              log#serror
-                ("check_typed_rvalue: not the same types:" ^ "\n- ty: "
-               ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty);
-              raise (Failure "Inconsistent types"));
-            check_typed_rvalue ctx v)
-          av.variant_id av.field_values v.ty
-end
-
-let is_value (e : texpression) : bool =
-  match e.e with Value _ -> true | _ -> false
-
 let is_var (e : texpression) : bool =
-  match e.e with
-  | Value (v, _) -> (
-      match v.value with
-      | RvPlace { var = _; projection = [] } -> true
-      | _ -> false)
-  | _ -> false
+  match e.e with Local _ -> true | _ -> false
 
 let as_var (e : texpression) : VarId.id =
-  match e.e with
-  | Value (v, _) -> (
-      match v.value with
-      | RvPlace { var; projection = [] } -> var
-      | _ -> raise (Failure "Unreachable"))
-  | _ -> raise (Failure "Unreachable")
+  match e.e with Local (v, _) -> v | _ -> raise (Failure "Unreachable")
 
 (** Remove the external occurrences of [Meta] *)
 let rec unmeta (e : texpression) : texpression =
   match e.e with Meta (_, e) -> unmeta e | _ -> e
 
+let mk_arrow (ty0 : ty) (ty1 : ty) : ty = Arrow (ty0, ty1)
+
 (** Construct a type as a list of arrows: ty1 -> ... tyn  *)
 let mk_arrows (inputs : ty list) (output : ty) =
   let rec aux (tys : ty list) : ty =
@@ -419,16 +231,16 @@ let mk_app (app : texpression) (arg : texpression) : texpression =
 let mk_apps (app : texpression) (args : texpression list) : texpression =
   List.fold_left (fun app arg -> mk_app app arg) app args
 
-(** Destruct an expression into a function identifier and a list of arguments,
+(** Destruct an expression into a qualif identifier and a list of arguments,
  *  if possible *)
-let opt_destruct_function_call (e : texpression) :
-    (func * texpression list) option =
+let opt_destruct_qualif_app (e : texpression) :
+    (qualif * texpression list) option =
   let app, args = destruct_apps e in
-  match app.e with Func func -> Some (func, args) | _ -> None
+  match app.e with Qualif qualif -> Some (qualif, args) | _ -> None
 
 (** Destruct an expression into a function identifier and a list of arguments *)
-let destruct_function_call (e : texpression) : func * texpression list =
-  Option.get (opt_destruct_function_call e)
+let destruct_qualif_app (e : texpression) : qualif * texpression list =
+  Option.get (opt_destruct_qualif_app e)
 
 let opt_destruct_result (ty : ty) : ty option =
   match ty with
@@ -440,26 +252,6 @@ 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 opt_destruct_state_monad_result (ty : ty) : ty option =
-  (* Checking:
-   * ty == state -> result (state & _) ? *)
-  match ty with
-  | Arrow (ty0, ty1) ->
-      (* ty == ty0 -> ty1
-       * Checking: ty0 == state ?
-       * *)
-      if ty0 = mk_state_ty then
-        (* Checking: ty1 == result (state & _) *)
-        match opt_destruct_result ty1 with
-        | None -> None
-        | Some ty2 -> (
-            (* Checking: ty2 == state & _ *)
-            match opt_destruct_tuple ty2 with
-            | Some [ ty3; ty4 ] -> if ty3 = mk_state_ty then Some ty4 else None
-            | _ -> None)
-      else None
-  | _ -> None
-
 let mk_abs (x : typed_lvalue) (e : texpression) : texpression =
   let ty = Arrow (x.ty, e.ty) in
   let e = Abs (x, e) in
@@ -475,9 +267,14 @@ let rec destruct_abs_list (e : texpression) : typed_lvalue list * texpression =
 let destruct_arrow (ty : ty) : ty * ty =
   match ty with
   | Arrow (ty0, ty1) -> (ty0, ty1)
-  | _ -> raise (Failure "Unreachable")
+  | _ -> raise (Failure "Not an arrow type")
 
-let mk_arrow (ty0 : ty) (ty1 : ty) : ty = Arrow (ty0, ty1)
+let rec destruct_arrows (ty : ty) : ty list * ty =
+  match ty with
+  | Arrow (ty0, ty1) ->
+      let tys, out_ty = destruct_arrows ty1 in
+      (ty0 :: tys, out_ty)
+  | _ -> ([], ty)
 
 let get_switch_body_ty (sb : switch_body) : ty =
   match sb with
@@ -512,3 +309,306 @@ let mk_switch (scrut : texpression) (sb : switch_body) : texpression =
   (* Put together *)
   let e = Switch (scrut, sb) in
   { e; ty }
+
+(** Make a "simplified" tuple type from a list of types:
+    - if there is exactly one type, just return it
+    - if there is > one type: wrap them in a tuple
+ *)
+let mk_simpl_tuple_ty (tys : ty list) : ty =
+  match tys with [ ty ] -> ty | _ -> Adt (Tuple, tys)
+
+(** TODO: rename to "mk_..." *)
+let unit_ty : ty = Adt (Tuple, [])
+
+(** TODO: rename to "mk_..." *)
+let unit_rvalue : texpression =
+  let id = AdtCons { adt_id = Tuple; variant_id = None } in
+  let qualif = { id; type_params = [] } in
+  let e = Qualif qualif in
+  let ty = unit_ty in
+  { e; ty }
+
+let mk_texpression_from_var (v : var) (mp : mplace option) : texpression =
+  let e = Local (v.id, mp) in
+  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 ty = v.ty in
+  { value; ty }
+
+(** Make a "simplified" tuple value from a list of values:
+    - 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 =
+  match vl with
+  | [ v ] -> v
+  | _ ->
+      let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in
+      let ty = Adt (Tuple, tys) in
+      let value = LvAdt { variant_id = None; field_values = vl } in
+      { value; ty }
+
+(** Similar to [mk_simpl_tuple_lvalue] *)
+let mk_simpl_tuple_texpression (vl : texpression list) : texpression =
+  match vl with
+  | [ v ] -> v
+  | _ ->
+      (* Compute the types of the fields, and the type of the tuple constructor *)
+      let tys = List.map (fun (v : texpression) -> v.ty) vl in
+      let ty = Adt (Tuple, tys) in
+      let ty = mk_arrows tys ty in
+      (* Construct the tuple constructor qualifier *)
+      let id = AdtCons { adt_id = Tuple; variant_id = None } in
+      let qualif = { id; type_params = tys } in
+      (* Put everything together *)
+      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
+  { value; ty = adt_ty }
+
+let ty_as_integer (t : ty) : T.integer_type =
+  match t with Integer int_ty -> int_ty | _ -> raise (Failure "Unreachable")
+
+(* TODO: move *)
+let type_decl_is_enum (def : T.type_decl) : bool =
+  match def.kind with T.Struct _ -> false | Enum _ -> true | Opaque -> false
+
+let mk_state_ty : ty = Adt (Assumed State, [])
+
+let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ])
+
+let mk_result_fail_rvalue (ty : ty) : texpression =
+  let type_args = [ ty ] in
+  let ty = Adt (Assumed Result, type_args) in
+  let id =
+    AdtCons { adt_id = Assumed Result; variant_id = Some result_fail_id }
+  in
+  let qualif = { id; type_params = type_args } in
+  let cons_e = Qualif qualif in
+  let cons_ty = ty in
+  let cons = { e = cons_e; ty = cons_ty } in
+  cons
+
+let mk_result_return_rvalue (v : texpression) : texpression =
+  let type_args = [ v.ty ] in
+  let ty = Adt (Assumed Result, type_args) in
+  let id =
+    AdtCons { adt_id = Assumed Result; variant_id = Some result_return_id }
+  in
+  let qualif = { id; type_params = type_args } in
+  let cons_e = Qualif qualif in
+  let cons_ty = mk_arrow v.ty ty in
+  let cons = { e = cons_e; ty = cons_ty } in
+  mk_app cons v
+
+let mk_result_fail_lvalue (ty : ty) : typed_lvalue =
+  let ty = Adt (Assumed Result, [ ty ]) in
+  let value = LvAdt { variant_id = Some result_fail_id; field_values = [] } in
+  { value; ty }
+
+let mk_result_return_lvalue (v : typed_lvalue) : typed_lvalue =
+  let ty = Adt (Assumed Result, [ v.ty ]) in
+  let value =
+    LvAdt { variant_id = Some result_return_id; field_values = [ v ] }
+  in
+  { value; ty }
+
+let opt_destruct_state_monad_result (ty : ty) : ty option =
+  (* Checking:
+   * ty == state -> result (state & _) ? *)
+  match ty with
+  | Arrow (ty0, ty1) ->
+      (* ty == ty0 -> ty1
+       * Checking: ty0 == state ?
+       * *)
+      if ty0 = mk_state_ty then
+        (* Checking: ty1 == result (state & _) *)
+        match opt_destruct_result ty1 with
+        | None -> None
+        | Some ty2 -> (
+            (* Checking: ty2 == state & _ *)
+            match opt_destruct_tuple ty2 with
+            | Some [ ty3; ty4 ] -> if ty3 = mk_state_ty then Some ty4 else None
+            | _ -> None)
+      else None
+  | _ -> None
+
+(** Utility function, used for type checking - TODO: move *)
+let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
+    (type_id : type_id) (variant_id : VariantId.id option) (tys : ty list) :
+    ty list =
+  match type_id with
+  | Tuple ->
+      (* Tuple *)
+      assert (variant_id = None);
+      tys
+  | AdtId def_id ->
+      (* "Regular" ADT *)
+      let def = TypeDeclId.Map.find def_id type_decls in
+      type_decl_get_instantiated_fields_types def variant_id tys
+  | Assumed aty -> (
+      (* Assumed type *)
+      match aty with
+      | State ->
+          (* `State` is opaque *)
+          raise (Failure "Unreachable: `State` values are opaque")
+      | Result ->
+          let ty = Collections.List.to_cons_nil tys in
+          let variant_id = Option.get variant_id in
+          if variant_id = result_return_id then [ ty ]
+          else if variant_id = result_fail_id then []
+          else
+            raise (Failure "Unreachable: improper variant id for result type")
+      | Option ->
+          let ty = Collections.List.to_cons_nil tys in
+          let variant_id = Option.get variant_id in
+          if variant_id = option_some_id then [ ty ]
+          else if variant_id = option_none_id then []
+          else
+            raise (Failure "Unreachable: improper variant id for result type")
+      | Vec -> raise (Failure "Unreachable: `Vector` values are opaque"))
+
+(** Module to perform type checking - we use this for sanity checks only
+
+    TODO: move to a special file (so that we can also use PrintPure for
+    debugging)
+ *)
+module TypeCheck = struct
+  type tc_ctx = {
+    type_decls : type_decl TypeDeclId.Map.t;  (** The type declarations *)
+    env : ty VarId.Map.t;  (** Environment from variables to types *)
+  }
+
+  let check_constant_value (v : constant_value) (ty : ty) : unit =
+    match (ty, v) with
+    | Integer int_ty, V.Scalar sv -> assert (int_ty = sv.V.int_ty)
+    | 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));
+    match v.value with
+    | LvConcrete cv ->
+        check_constant_value cv v.ty;
+        ctx
+    | LvVar Dummy -> ctx
+    | LvVar (Var (var, _)) ->
+        assert (var.ty = v.ty);
+        let env = VarId.Map.add var.id var.ty ctx.env in
+        { ctx with env }
+    | LvAdt av ->
+        (* Compute the field types *)
+        let type_id, tys =
+          match v.ty with
+          | Adt (type_id, tys) -> (type_id, tys)
+          | _ -> raise (Failure "Inconsistently typed value")
+        in
+        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 =
+          if ty <> v.ty then (
+            log#serror
+              ("check_typed_lvalue: 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
+        in
+        (* Check the field types - TODO: we might also want to check that the
+         * type of the applied constructor is correct *)
+        List.fold_left
+          (fun ctx (ty, v) -> check_value ctx ty v)
+          ctx
+          (List.combine field_tys av.field_values)
+
+  let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
+    match e.e with
+    | Local (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
+         * we use a locally nameless representation *)
+        match VarId.Map.find_opt var_id ctx.env with
+        | None -> ()
+        | Some ty -> assert (ty = e.ty))
+    | Const cv -> check_constant_value cv e.ty
+    | App (app, arg) ->
+        let input_ty, output_ty = destruct_arrow app.ty in
+        assert (input_ty = arg.ty);
+        assert (output_ty = e.ty);
+        check_texpression ctx app;
+        check_texpression ctx arg
+    | Abs (pat, body) ->
+        let pat_ty, body_ty = destruct_arrow e.ty in
+        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
+        check_texpression ctx body
+    | Qualif qualif -> (
+        match qualif.id with
+        | Func _ -> () (* TODO *)
+        | Proj (ProjField (type_id, field_id)) ->
+            (* Note we can only project fields of structurs (not enumerations) *)
+            let variant_id = None in
+            let expected_field_tys =
+              get_adt_field_types ctx.type_decls type_id variant_id
+                qualif.type_params
+            in
+            let expected_field_ty = FieldId.nth expected_field_tys field_id in
+            let _adt_ty, field_ty = destruct_arrow e.ty in
+            (* TODO: check the adt_ty *)
+            assert (expected_field_ty = field_ty)
+        | Proj (ProjTuple field_id) -> (
+            let tuple_ty, field_ty = destruct_arrow e.ty in
+            match tuple_ty with
+            | Adt (Tuple, tys) ->
+                let expected_field_ty = List.nth tys field_id in
+                assert (field_ty = expected_field_ty)
+            | _ -> raise (Failure "Inconsistently typed projector"))
+        | AdtCons id ->
+            (* TODO: we might also want to check the out type *)
+            let expected_field_tys =
+              get_adt_field_types ctx.type_decls id.adt_id id.variant_id
+                qualif.type_params
+            in
+            let field_tys, _ = destruct_arrows e.ty in
+            assert (expected_field_tys = field_tys))
+    | Let (monadic, pat, re, e_next) ->
+        let expected_pat_ty =
+          if monadic then destruct_result re.ty else re.ty
+        in
+        assert (pat.ty = expected_pat_ty);
+        assert (e.ty = e_next.ty);
+        (* 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
+        (* Check the next expression *)
+        check_texpression ctx e_next
+    | Switch (scrut, switch_body) -> (
+        check_texpression ctx scrut;
+        match switch_body with
+        | If (e_then, e_else) ->
+            assert (scrut.ty = Bool);
+            assert (e_then.ty = e.ty);
+            assert (e_else.ty = e.ty);
+            check_texpression ctx e_then;
+            check_texpression ctx e_else
+        | Match branches ->
+            let check_branch (br : match_branch) : unit =
+              assert (br.pat.ty = scrut.ty);
+              let ctx = check_typed_lvalue ctx br.pat in
+              check_texpression ctx br.branch
+            in
+            List.iter check_branch branches)
+    | Meta (_, e_next) ->
+        assert (e_next.ty = e.ty);
+        check_texpression ctx e_next
+end
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 64f8f481..6606ca25 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -999,7 +999,9 @@ and translate_panic (config : config) (ctx : bs_ctx) : texpression =
     let ty = v.ty in
     let e = { e; ty } in
     (* Add the lambda *)
-    let _, state_var = fresh_var (Some "st") mk_state_ty ctx in
+    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 e
   else
@@ -1026,7 +1028,9 @@ and translate_return (config : config) (opt_v : V.typed_value option)
        * *)
       (* TODO: we should use a `return` function, it would be cleaner *)
       if config.use_state_monad then
-        let _, state_var = fresh_var (Some "st") mk_state_ty ctx in
+        let _, state_var =
+          fresh_var (Some ConstStrings.state_basename) mk_state_ty ctx
+        in
         let state_rvalue = mk_typed_rvalue_from_var state_var in
         let v =
           mk_result_return_rvalue (mk_simpl_tuple_rvalue [ state_rvalue; v ])