Rename some variants

compiler/Assumed.ml

@@ -43,7 +43,7 @@ module Sig = struct
   let tvar_id_0 = T.TypeVarId.of_int 0
   let tvar_0 : T.ty = T.TypeVar tvar_id_0
   let cgvar_id_0 = T.ConstGenericVarId.of_int 0
-  let cgvar_0 : T.const_generic = T.ConstGenericVar cgvar_id_0
+  let cgvar_0 : T.const_generic = T.CGVar cgvar_id_0
 
   (** Region 'a of id 0 *)
   let region_param_0 : T.region_var = { T.index = rvar_id_0; name = Some "'a" }

compiler/ExtractTypes.ml

@@ -1119,11 +1119,11 @@ let extract_arrow (fmt : F.formatter) () : unit =
 let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter)
     (inside : bool) (cg : const_generic) : unit =
   match cg with
-  | ConstGenericGlobal id ->
+  | CGGlobal id ->
       let s = ctx_get_global id ctx in
       F.pp_print_string fmt s
-  | ConstGenericValue v -> ctx.fmt.extract_literal fmt inside v
-  | ConstGenericVar id ->
+  | CGValue v -> ctx.fmt.extract_literal fmt inside v
+  | CGVar id ->
       let s = ctx_get_const_generic_var id ctx in
       F.pp_print_string fmt s
 

compiler/Interpreter.ml

@@ -74,7 +74,7 @@ let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (sg : A.fun_sig)
     let types = List.map (fun (v : T.type_var) -> T.TypeVar v.T.index) types in
     let const_generics =
       List.map
-        (fun (v : T.const_generic_var) -> T.ConstGenericVar v.T.index)
+        (fun (v : T.const_generic_var) -> T.CGVar v.T.index)
         const_generics
     in
     (* Annoying that we have to generate this substitution here *)

compiler/InterpreterExpressions.ml

@@ -329,7 +329,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
                    ( ctx0,
                      None,
                      value_as_symbolic v.value,
-                     SymbolicAst.VaConstGenericValue vid,
+                     SymbolicAst.VaCGValue vid,
                      e )))
       | E.CFnPtr _ -> raise (Failure "TODO"))
   | E.Copy p ->

compiler/PrintPure.ml

@@ -211,9 +211,9 @@ let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
 let const_generic_to_string (fmt : type_formatter) (cg : T.const_generic) :
     string =
   match cg with
-  | ConstGenericGlobal id -> fmt.global_decl_id_to_string id
-  | ConstGenericVar id -> fmt.const_generic_var_id_to_string id
-  | ConstGenericValue lit -> literal_to_string lit
+  | CGGlobal id -> fmt.global_decl_id_to_string id
+  | CGVar id -> fmt.const_generic_var_id_to_string id
+  | CGValue lit -> literal_to_string lit
 
 let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string =
   match ty with

compiler/PureUtils.ml

@@ -111,7 +111,7 @@ let ty_substitute (subst : subst) (ty : ty) : ty =
     object
       inherit [_] map_ty
       method! visit_TypeVar _ var_id = subst.ty_subst var_id
-      method! visit_ConstGenericVar _ var_id = subst.cg_subst var_id
+      method! visit_CGVar _ var_id = subst.cg_subst var_id
       method! visit_Clause _ id = subst.tr_subst id
       method! visit_Self _ = subst.tr_self
     end

compiler/Substitute.ml

@@ -29,7 +29,7 @@ let st_substitute_visitor (subst : subst) =
       (* We should never get here because we reimplemented [visit_TypeVar] *)
       raise (Failure "Unexpected")
 
-    method! visit_ConstGenericVar _ id = subst.cg_subst id
+    method! visit_CGVar _ id = subst.cg_subst id
 
     method! visit_const_generic_var_id _ _ =
       (* We should never get here because we reimplemented [visit_Var] *)
@@ -68,7 +68,7 @@ let erase_regions_subst : subst =
   {
     r_subst = (fun _ -> T.RErased);
     ty_subst = (fun vid -> T.TypeVar vid);
-    cg_subst = (fun id -> T.ConstGenericVar id);
+    cg_subst = (fun id -> T.CGVar id);
     tr_subst = (fun id -> T.Clause id);
     tr_self = T.Self;
   }

compiler/SymbolicAst.ml

@@ -243,7 +243,7 @@ and value_aggregate =
   | VaSingleValue of V.typed_value  (** Regular case *)
   | VaArray of V.typed_value list
       (** This is used when introducing array aggregates *)
-  | VaConstGenericValue of T.const_generic_var_id
+  | VaCGValue of T.const_generic_var_id
       (** This is used when evaluating a const generic value: in the interpreter,
           we introduce a fresh symbolic value. *)
   | VaTraitConstValue of T.trait_ref * T.generic_args * string

compiler/SymbolicToPure.ml

@@ -2487,7 +2487,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
           { struct_id = TAssumed Array; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
-    | VaConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
+    | VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty }
     | VaTraitConstValue (trait_ref, generics, const_name) ->
         let type_infos = ctx.type_context.type_infos in
         let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
@@ -2740,7 +2740,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       in
       let const_generics =
         List.map
-          (fun (cg : T.const_generic_var) -> T.ConstGenericVar cg.T.index)
+          (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index)
           const_generics
       in
       let trait_refs =