Update following the introduction of ConstantExpr

16 files changed, 220 insertions, 143 deletions

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 2ca5653d..14b5d559 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -263,6 +263,10 @@ type eval_ctx = {
   region_groups : RegionGroupId.id list;
   type_vars : type_var list;
   const_generic_vars : const_generic_var list;
+  const_generic_vars_map : typed_value Types.ConstGenericVarId.Map.t;
+      (** The map from const generic vars to their values. Those values
+          can be symbolic values or concrete values (in the latter case:
+          if we run in interpreter mode) *)
   env : env;
   ended_regions : RegionId.Set.t;
 }
@@ -312,6 +316,11 @@ let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
 let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value =
   env_lookup_var_value ctx.env vid
 
+(** Retrieve a const generic value in an evaluation context *)
+let ctx_lookup_const_generic_value (ctx : eval_ctx) (vid : ConstGenericVarId.id)
+    : typed_value =
+  Types.ConstGenericVarId.Map.find vid ctx.const_generic_vars_map
+
 (** Update a variable's value in the current frame.
 
     This is a helper function: it can break invariants and doesn't perform
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index c4238d83..7daec16f 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2249,6 +2249,9 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
   | Var var_id ->
       let var_name = ctx_get_var var_id ctx in
       F.pp_print_string fmt var_name
+  | CVar var_id ->
+      let var_name = ctx_get_const_generic_var var_id ctx in
+      F.pp_print_string fmt var_name
   | Const cv -> ctx.fmt.extract_literal fmt inside cv
   | App _ ->
       let app, args = destruct_apps e in
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 154c5a21..37eeb333 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -34,6 +34,15 @@ let initialize_eval_context (type_context : C.type_context)
     (region_groups : T.RegionGroupId.id list) (type_vars : T.type_var list)
     (const_generic_vars : T.const_generic_var list) : C.eval_ctx =
   C.reset_global_counters ();
+  let const_generic_vars_map =
+    T.ConstGenericVarId.Map.of_list
+      (List.map
+         (fun (cg : T.const_generic_var) ->
+           let ty = TypesUtils.ety_no_regions_to_rty (T.Literal cg.ty) in
+           let cv = mk_fresh_symbolic_typed_value V.ConstGeneric ty in
+           (cg.index, cv))
+         const_generic_vars)
+  in
   {
     C.type_context;
     C.fun_context;
@@ -41,6 +50,7 @@ let initialize_eval_context (type_context : C.type_context)
     C.region_groups;
     C.type_vars;
     C.const_generic_vars;
+    C.const_generic_vars_map;
     C.env = [ C.Frame ];
     C.ended_regions = T.RegionId.Set.empty;
   }
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 4d67a4e4..f908d060 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -452,7 +452,8 @@ let give_back_symbolic_value (_config : C.config)
   | V.SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
     ->
       ()
-  | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate ->
+  | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate
+  | ConstGeneric ->
       raise (Failure "Unreachable"));
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 8b2070c6..2f6a7b49 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -230,17 +230,16 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
   let prepare : cm_fun =
    fun cf ctx ->
     match op with
-    | Expressions.Constant (ty, cv) ->
+    | E.Constant _ ->
         (* No need to reorganize the context *)
-        literal_to_typed_value (TypesUtils.ty_as_literal ty) cv |> ignore;
         cf ctx
-    | Expressions.Copy p ->
+    | E.Copy p ->
         (* Access the value *)
         let access = Read in
         (* Expand the symbolic values, if necessary *)
         let expand_prim_copy = true in
         access_rplace_reorganize config expand_prim_copy access p cf ctx
-    | Expressions.Move p ->
+    | E.Move p ->
         (* Access the value *)
         let access = Move in
         let expand_prim_copy = false in
@@ -260,9 +259,35 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
      ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n"));
   (* Evaluate *)
   match op with
-  | Expressions.Constant (ty, cv) ->
-      cf (literal_to_typed_value (TypesUtils.ty_as_literal ty) cv) ctx
-  | Expressions.Copy p ->
+  | E.Constant cv -> (
+      match cv.value with
+      | E.CLiteral lit ->
+          cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx
+      | E.CVar vid -> (
+          let ctx0 = ctx in
+          (* Lookup the const generic value *)
+          let cv = C.ctx_lookup_const_generic_value ctx vid in
+          (* Copy the value *)
+          let allow_adt_copy = false in
+          let ctx, v = copy_value allow_adt_copy config ctx cv in
+          (* Continue *)
+          let e = cf v ctx in
+          (* We have to wrap the expression to introduce *)
+          match e with
+          | None -> None
+          | Some e ->
+              (* If we are synthesizing a symbolic AST, it means that we are in symbolic
+                 mode: the value of the const generic is necessarily symbolic. *)
+              assert (is_symbolic cv.V.value);
+              (* *)
+              Some
+                (SymbolicAst.IntroSymbolic
+                   ( ctx0,
+                     None,
+                     value_as_symbolic v.value,
+                     SymbolicAst.ConstGenericValue vid,
+                     e ))))
+  | E.Copy p ->
       (* Access the value *)
       let access = Read in
       let cc = read_place access p in
@@ -283,7 +308,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
       in
       (* Compose and apply *)
       comp cc copy cf ctx
-  | Expressions.Move p ->
+  | E.Move p ->
       (* Access the value *)
       let access = Move in
       let cc = read_place access p in
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index bf88e055..10205c27 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -557,6 +557,7 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
       region_groups;
       type_vars;
       const_generic_vars;
+      const_generic_vars_map;
       env = _;
       ended_regions = ended_regions0;
     } =
@@ -569,6 +570,7 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
       region_groups = _;
       type_vars = _;
       const_generic_vars = _;
+      const_generic_vars_map = _;
       env = _;
       ended_regions = ended_regions1;
     } =
@@ -583,6 +585,7 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
         region_groups;
         type_vars;
         const_generic_vars;
+        const_generic_vars_map;
         env;
         ended_regions;
       }
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 045c4484..6d520059 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -421,16 +421,16 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
 (** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_replace_concrete (_config : C.config)
     (_region_params : T.erased_region list) (_type_params : T.ety list)
-    (_cg_params : T.const_generic list) : cm_fun =
+    (_cg_args : T.const_generic list) : cm_fun =
  fun _cf _ctx -> raise Unimplemented
 
 (** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_box_new_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_params : T.const_generic list) : cm_fun =
+    (cg_args : T.const_generic list) : cm_fun =
  fun cf ctx ->
   (* Check and retrieve the arguments *)
-  match (region_params, type_params, cg_params, ctx.env) with
+  match (region_params, type_params, cg_args, ctx.env) with
   | ( [],
       [ boxed_ty ],
       [],
@@ -470,10 +470,10 @@ let eval_box_new_concrete (config : C.config)
     and [std::DerefMut::deref_mut] - see {!eval_non_local_function_call} *)
 let eval_box_deref_mut_or_shared_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_params : T.const_generic list) (is_mut : bool) : cm_fun =
+    (cg_args : T.const_generic list) (is_mut : bool) : cm_fun =
  fun cf ctx ->
   (* Check the arguments *)
-  match (region_params, type_params, cg_params, ctx.env) with
+  match (region_params, type_params, cg_args, ctx.env) with
   | ( [],
       [ boxed_ty ],
       [],
@@ -517,18 +517,18 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config)
 (** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_box_deref_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_params : T.const_generic list) : cm_fun =
+    (cg_args : T.const_generic list) : cm_fun =
   let is_mut = false in
-  eval_box_deref_mut_or_shared_concrete config region_params type_params
-    cg_params is_mut
+  eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args
+    is_mut
 
 (** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_box_deref_mut_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_params : T.const_generic list) : cm_fun =
+    (cg_args : T.const_generic list) : cm_fun =
   let is_mut = true in
-  eval_box_deref_mut_or_shared_concrete config region_params type_params
-    cg_params is_mut
+  eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args
+    is_mut
 
 (** Auxiliary function - see {!eval_non_local_function_call}.
 
@@ -550,10 +550,10 @@ let eval_box_deref_mut_concrete (config : C.config)
     the destination (by setting it to [()]).
 *)
 let eval_box_free (config : C.config) (region_params : T.erased_region list)
-    (type_params : T.ety list) (cg_params : T.const_generic list)
+    (type_params : T.ety list) (cg_args : T.const_generic list)
     (args : E.operand list) (dest : E.place) : cm_fun =
  fun cf ctx ->
-  match (region_params, type_params, cg_params, args) with
+  match (region_params, type_params, cg_args, args) with
   | [], [ boxed_ty ], [], [ E.Move input_box_place ] ->
       (* Required type checking *)
       let input_box = InterpreterPaths.read_place Write input_box_place ctx in
@@ -573,14 +573,17 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
 (** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id)
     (_region_params : T.erased_region list) (_type_params : T.ety list)
-    (_cg_params : T.const_generic list) : cm_fun =
+    (_cg_args : T.const_generic list) : cm_fun =
  fun _cf _ctx -> raise Unimplemented
 
 (** Evaluate a non-local function call in concrete mode *)
 let eval_non_local_function_call_concrete (config : C.config)
     (fid : A.assumed_fun_id) (region_params : T.erased_region list)
-    (type_params : T.ety list) (cg_params : T.const_generic list)
+    (type_params : T.ety list) (cg_args : T.const_generic list)
     (args : E.operand list) (dest : E.place) : cm_fun =
+  (* Sanity check: we don't fully handle the const generic vars environment
+     in concrete mode yet *)
+  assert (cg_args = []);
   (* There are two cases (and this is extremely annoying):
      - the function is not box_free
      - the function is box_free
@@ -589,7 +592,7 @@ let eval_non_local_function_call_concrete (config : C.config)
   match fid with
   | A.BoxFree ->
       (* Degenerate case: box_free *)
-      eval_box_free config region_params type_params cg_params args dest
+      eval_box_free config region_params type_params cg_args args dest
   | _ ->
       (* "Normal" case: not box_free *)
       (* Evaluate the operands *)
@@ -612,7 +615,7 @@ let eval_non_local_function_call_concrete (config : C.config)
         let ret_vid = E.VarId.zero in
         let ret_ty =
           get_non_local_function_return_type fid region_params type_params
-            cg_params
+            cg_args
         in
         let ret_var = mk_var ret_vid (Some "@return") ret_ty in
         let cc = comp cc (push_uninitialized_var ret_var) in
@@ -631,19 +634,19 @@ let eval_non_local_function_call_concrete (config : C.config)
         let cf_eval_body : cm_fun =
           match fid with
           | A.Replace ->
-              eval_replace_concrete config region_params type_params cg_params
+              eval_replace_concrete config region_params type_params cg_args
           | BoxNew ->
-              eval_box_new_concrete config region_params type_params cg_params
+              eval_box_new_concrete config region_params type_params cg_args
           | BoxDeref ->
-              eval_box_deref_concrete config region_params type_params cg_params
+              eval_box_deref_concrete config region_params type_params cg_args
           | BoxDerefMut ->
               eval_box_deref_mut_concrete config region_params type_params
-                cg_params
+                cg_args
           | BoxFree ->
               (* Should have been treated above *) raise (Failure "Unreachable")
           | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut ->
               eval_vec_function_concrete config fid region_params type_params
-                cg_params
+                cg_args
           | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
           | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut
           | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
@@ -663,7 +666,7 @@ let eval_non_local_function_call_concrete (config : C.config)
       comp cf_eval_ops cf_eval_call
 
 let instantiate_fun_sig (type_params : T.ety list)
-    (cg_params : T.const_generic list) (sg : A.fun_sig) : A.inst_fun_sig =
+    (cg_args : T.const_generic list) (sg : A.fun_sig) : A.inst_fun_sig =
   (* Generate fresh abstraction ids and create a substitution from region
    * group ids to abstraction ids *)
   let rg_abs_ids_bindings =
@@ -694,7 +697,7 @@ let instantiate_fun_sig (type_params : T.ety list)
   let rtype_params = List.map ety_no_regions_to_rty type_params in
   let tsubst = Subst.make_type_subst_from_vars sg.type_params rtype_params in
   let cgsubst =
-    Subst.make_const_generic_subst_from_vars sg.const_generic_params cg_params
+    Subst.make_const_generic_subst_from_vars sg.const_generic_params cg_args
   in
   (* Substitute the signature *)
   let inst_sig = Subst.substitute_signature asubst rsubst tsubst cgsubst sg in
@@ -1054,81 +1057,86 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
     (_region_args : T.erased_region list) (type_args : T.ety list)
     (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
     st_cm_fun =
- fun cf ctx ->
-  (* Retrieve the (correctly instantiated) body *)
-  let def = C.ctx_lookup_fun_decl ctx fid in
-  (* We can evaluate the function call only if it is not opaque *)
-  let body =
-    match def.body with
-    | None ->
-        raise
-          (Failure
-             ("Can't evaluate a call to an opaque function: "
-             ^ Print.name_to_string def.name))
-    | Some body -> body
-  in
-  let tsubst =
-    Subst.make_type_subst_from_vars def.A.signature.type_params type_args
-  in
-  let cgsubst =
-    Subst.make_const_generic_subst_from_vars
-      def.A.signature.const_generic_params cg_args
-  in
-  let locals, body_st = Subst.fun_body_substitute_in_body tsubst cgsubst body in
-
-  (* Evaluate the input operands *)
-  assert (List.length args = body.A.arg_count);
-  let cc = eval_operands config args in
-
-  (* Push a frame delimiter - we use {!comp_transmit} to transmit the result
-   * of the operands evaluation from above to the functions afterwards, while
-   * ignoring it in this function *)
-  let cc = comp_transmit cc push_frame in
-
-  (* Compute the initial values for the local variables *)
-  (* 1. Push the return value *)
-  let ret_var, locals =
-    match locals with
-    | ret_ty :: locals -> (ret_ty, locals)
-    | _ -> raise (Failure "Unreachable")
-  in
-  let input_locals, locals =
-    Collections.List.split_at locals body.A.arg_count
-  in
-
-  let cc = comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty)) in
-
-  (* 2. Push the input values *)
-  let cf_push_inputs cf args =
-    let inputs = List.combine input_locals args in
-    (* Note that this function checks that the variables and their values
-     * have the same type (this is important) *)
-    push_vars inputs cf
-  in
-  let cc = comp cc cf_push_inputs in
+  (* Sanity check: we don't fully handle the const generic vars environment
+     in concrete mode yet *)
+  assert (cg_args = []);
+  fun cf ctx ->
+    (* Retrieve the (correctly instantiated) body *)
+    let def = C.ctx_lookup_fun_decl ctx fid in
+    (* We can evaluate the function call only if it is not opaque *)
+    let body =
+      match def.body with
+      | None ->
+          raise
+            (Failure
+               ("Can't evaluate a call to an opaque function: "
+               ^ Print.name_to_string def.name))
+      | Some body -> body
+    in
+    let tsubst =
+      Subst.make_type_subst_from_vars def.A.signature.type_params type_args
+    in
+    let cgsubst =
+      Subst.make_const_generic_subst_from_vars
+        def.A.signature.const_generic_params cg_args
+    in
+    let locals, body_st =
+      Subst.fun_body_substitute_in_body tsubst cgsubst body
+    in
 
-  (* 3. Push the remaining local variables (initialized as {!Bottom}) *)
-  let cc = comp cc (push_uninitialized_vars locals) in
+    (* Evaluate the input operands *)
+    assert (List.length args = body.A.arg_count);
+    let cc = eval_operands config args in
+
+    (* Push a frame delimiter - we use {!comp_transmit} to transmit the result
+     * of the operands evaluation from above to the functions afterwards, while
+     * ignoring it in this function *)
+    let cc = comp_transmit cc push_frame in
+
+    (* Compute the initial values for the local variables *)
+    (* 1. Push the return value *)
+    let ret_var, locals =
+      match locals with
+      | ret_ty :: locals -> (ret_ty, locals)
+      | _ -> raise (Failure "Unreachable")
+    in
+    let input_locals, locals =
+      Collections.List.split_at locals body.A.arg_count
+    in
 
-  (* Execute the function body *)
-  let cc = comp cc (eval_function_body config body_st) in
+    let cc = comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty)) in
 
-  (* Pop the stack frame and move the return value to its destination *)
-  let cf_finish cf res =
-    match res with
-    | Panic -> cf Panic
-    | Return ->
-        (* Pop the stack frame, retrieve the return value, move it to
-         * its destination and continue *)
-        pop_frame_assign config dest (cf Unit)
-    | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _
-    | EndContinue _ ->
-        raise (Failure "Unreachable")
-  in
-  let cc = comp cc cf_finish in
+    (* 2. Push the input values *)
+    let cf_push_inputs cf args =
+      let inputs = List.combine input_locals args in
+      (* Note that this function checks that the variables and their values
+       * have the same type (this is important) *)
+      push_vars inputs cf
+    in
+    let cc = comp cc cf_push_inputs in
+
+    (* 3. Push the remaining local variables (initialized as {!Bottom}) *)
+    let cc = comp cc (push_uninitialized_vars locals) in
+
+    (* Execute the function body *)
+    let cc = comp cc (eval_function_body config body_st) in
+
+    (* Pop the stack frame and move the return value to its destination *)
+    let cf_finish cf res =
+      match res with
+      | Panic -> cf Panic
+      | Return ->
+          (* Pop the stack frame, retrieve the return value, move it to
+           * its destination and continue *)
+          pop_frame_assign config dest (cf Unit)
+      | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _
+      | EndContinue _ ->
+          raise (Failure "Unreachable")
+    in
+    let cc = comp cc cf_finish in
 
-  (* Continue *)
-  cc cf ctx
+    (* Continue *)
+    cc cf ctx
 
 (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
 and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 7bd37550..637f1b1e 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -255,7 +255,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
               raise Found
             else ()
         | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
-        | V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate ->
+        | V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate
+        | V.ConstGeneric ->
             ()
     end
   in
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index cfb63ec2..dfb2c9fd 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -559,9 +559,8 @@ let fun_or_op_id_to_string (fmt : ast_formatter) (fun_id : fun_or_op_id) :
 let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
     (indent : string) (indent_incr : string) (e : texpression) : string =
   match e.e with
-  | Var var_id ->
-      let s = fmt.var_id_to_string var_id in
-      if inside then "(" ^ s ^ ")" else s
+  | Var var_id -> fmt.var_id_to_string var_id
+  | CVar cg_id -> fmt.const_generic_var_id_to_string cg_id
   | Const cv -> literal_to_string cv
   | App _ ->
       (* Recursively destruct the app, to have a pair (app, arguments list) *)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index ac4ca081..55513cc2 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -37,6 +37,7 @@ module ConstGenericVarId = T.ConstGenericVarId
 type integer_type = T.integer_type [@@deriving show, ord]
 type const_generic_var = T.const_generic_var [@@deriving show, ord]
 type const_generic = T.const_generic [@@deriving show, ord]
+type const_generic_var_id = T.const_generic_var_id [@@deriving show, ord]
 
 (** The assumed types for the pure AST.
 
@@ -536,6 +537,7 @@ class virtual ['self] mapreduce_expression_base =
  *)
 type expression =
   | Var of var_id  (** a variable *)
+  | CVar of const_generic_var_id  (** a const generic var *)
   | Const of literal
   | App of texpression * texpression
       (** Application of a function to an argument.
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index b6025df4..65dc7ff2 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -376,8 +376,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     let ty = e.ty in
     let ctx, e =
       match e.e with
-      | Var _ -> (* Nothing to do *) (ctx, e.e)
-      | Const _ -> (* Nothing to do *) (ctx, e.e)
+      | Var _ | CVar _ | Const _ -> (* Nothing to do *) (ctx, e.e)
       | App (app, arg) ->
           let ctx, app = update_texpression app ctx in
           let ctx, arg = update_texpression arg ctx in
@@ -834,7 +833,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
 
       method! visit_texpression env e =
         match e.e with
-        | Var _ | Const _ -> fun _ -> false
+        | Var _ | CVar _ | Const _ -> fun _ -> false
         | StructUpdate _ ->
             (* There shouldn't be monadic calls in structure updates - also
                note that by returning [false] we are conservative: we might
@@ -930,7 +929,7 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
 
       method! visit_expression env e =
         match e with
-        | Var _ | Const _ | App _ | Qualif _
+        | Var _ | CVar _ | Const _ | App _ | Qualif _
         | Switch (_, _)
         | Meta (_, _)
         | StructUpdate _ | Abs _ ->
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 8d28bb8a..d145ce93 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -65,6 +65,8 @@ type tc_ctx = {
   global_decls : A.global_decl A.GlobalDeclId.Map.t;
       (** The global declarations *)
   env : ty VarId.Map.t;  (** Environment from variables to types *)
+  const_generics : ty T.ConstGenericVarId.Map.t;
+      (** The types of the const generics *)
 }
 
 let check_literal (v : literal) (ty : literal_type) : unit =
@@ -115,6 +117,9 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
       match VarId.Map.find_opt var_id ctx.env with
       | None -> ()
       | Some ty -> assert (ty = e.ty))
+  | CVar cg_id ->
+      let ty = T.ConstGenericVarId.Map.find cg_id ctx.const_generics in
+      assert (ty = e.ty)
   | Const cv -> check_literal cv (ty_as_literal e.ty)
   | App (app, arg) ->
       let input_ty, output_ty = destruct_arrow app.ty in
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 1c8d8921..461098f2 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -164,7 +164,8 @@ let fun_sig_substitute (tsubst : TypeVarId.id -> ty)
  *)
 let rec let_group_requires_parentheses (e : texpression) : bool =
   match e.e with
-  | Var _ | Const _ | App _ | Abs _ | Qualif _ | StructUpdate _ -> false
+  | Var _ | CVar _ | Const _ | App _ | Abs _ | Qualif _ | StructUpdate _ ->
+      false
   | Let (monadic, _, _, next_e) ->
       if monadic then true else let_group_requires_parentheses next_e
   | Switch (_, _) -> false
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 7dc94dcd..17cdcabc 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -79,6 +79,9 @@ class ['self] iter_expression_base =
     method visit_loop_id : 'env -> V.loop_id -> unit = fun _ _ -> ()
     method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
 
+    method visit_const_generic_var_id : 'env -> T.const_generic_var_id -> unit =
+      fun _ _ -> ()
+
     method visit_symbolic_value_id : 'env -> V.symbolic_value_id -> unit =
       fun _ _ -> ()
 
@@ -171,14 +174,14 @@ type expression =
       * expression
       (** We introduce a new symbolic value, equal to some other value.
 
-        This is used for instance when reorganizing the environment to compute
-        fixed points: we duplicate some shared symbolic values to destructure
-        the shared values, in order to make the environment a bit more general
-        (while losing precision of course).
+          This is used for instance when reorganizing the environment to compute
+          fixed points: we duplicate some shared symbolic values to destructure
+          the shared values, in order to make the environment a bit more general
+          (while losing precision of course).
 
-        The context is the evaluation context from before introducing the new
-        value. It has the same purpose as for the {!Return} case.
-      *)
+          The context is the evaluation context from before introducing the new
+          value. It has the same purpose as for the {!Return} case.
+       *)
   | ForwardEnd of
       Contexts.eval_ctx
       * V.typed_value symbolic_value_id_map option
@@ -253,6 +256,9 @@ and value_aggregate =
   | SingleValue of V.typed_value  (** Regular case *)
   | Array of V.typed_value list
       (** This is used when introducing array aggregates *)
+  | ConstGenericValue of T.const_generic_var_id
+      (** This is used when evaluating a const generic value: in the interpreter,
+          we introduce a fresh symbolic value. *)
 [@@deriving
   show,
     visitors
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 3512270a..7dda1f22 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -201,29 +201,6 @@ type bs_ctx = {
 }
 [@@deriving show]
 
-let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
-  let env = VarId.Map.empty in
-  let ctx =
-    {
-      PureTypeCheck.type_decls = ctx.type_context.type_decls;
-      global_decls = ctx.global_context.llbc_global_decls;
-      env;
-    }
-  in
-  let _ = PureTypeCheck.check_typed_pattern ctx v in
-  ()
-
-let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
-  let env = VarId.Map.empty in
-  let ctx =
-    {
-      PureTypeCheck.type_decls = ctx.type_context.type_decls;
-      global_decls = ctx.global_context.llbc_global_decls;
-      env;
-    }
-  in
-  PureTypeCheck.check_texpression ctx e
-
 (* TODO: move *)
 let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
   Print.Ast.decls_and_fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls
@@ -589,6 +566,31 @@ let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
   let type_infos = ctx.type_context.type_infos in
   translate_back_ty type_infos keep_region inside_mut ty
 
+let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
+  let const_generics =
+    T.ConstGenericVarId.Map.of_list
+      (List.map
+         (fun (cg : T.const_generic_var) ->
+           (cg.index, ctx_translate_fwd_ty ctx (T.Literal cg.ty)))
+         ctx.sg.const_generic_params)
+  in
+  let env = VarId.Map.empty in
+  {
+    PureTypeCheck.type_decls = ctx.type_context.type_decls;
+    global_decls = ctx.global_context.llbc_global_decls;
+    env;
+    const_generics;
+  }
+
+let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
+  let ctx = mk_type_check_ctx ctx in
+  let _ = PureTypeCheck.check_typed_pattern ctx v in
+  ()
+
+let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
+  let ctx = mk_type_check_ctx ctx in
+  PureTypeCheck.check_texpression ctx e
+
 (** List the ancestors of an abstraction *)
 let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs)
     (call_id : V.FunCallId.id) : V.AbstractionId.id list =
@@ -2298,6 +2300,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
           { struct_id = Assumed Array; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
+    | ConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
   in
 
   (* Make the let-binding *)
diff --git a/compiler/Values.ml b/compiler/Values.ml
index d884c319..58737557 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -52,6 +52,8 @@ type sv_kind =
       (** The result of a loop join (when computing loop fixed points) *)
   | Aggregate
       (** A symbolic value we introduce in place of an aggregate value *)
+  | ConstGeneric
+      (** A symbolic value we introduce when using a const generic as a value *)
 [@@deriving show, ord]
 
 (** Ancestor for {!symbolic_value} iter visitor *)