Rename some variants

AeneasVerif · Nov 12, 2023 · 61b6a72 · 61b6a72
1 parent b7d6ba6
commit 61b6a72
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 14 deletions.
diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml
@@ -312,13 +312,13 @@ let const_generic_of_json (js : json) : (T.const_generic, string) result =
     (match js with
     | `Assoc [ ("Global", id) ] ->
         let* id = E.GlobalDeclId.id_of_json id in
-        Ok (T.ConstGenericGlobal id)
+        Ok (T.CGGlobal id)
     | `Assoc [ ("Var", id) ] ->
         let* id = T.ConstGenericVarId.id_of_json id in
-        Ok (T.ConstGenericVar id)
+        Ok (T.CGVar id)
     | `Assoc [ ("Value", lit) ] ->
         let* lit = literal_of_json lit in
-        Ok (T.ConstGenericValue lit)
+        Ok (T.CGValue lit)
     | _ -> Error "")
 
 let rec ty_of_json (js : json) : (T.ty, string) result =

diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml
@@ -66,9 +66,9 @@ let type_id_to_string (fmt : type_formatter) (id : T.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) (ty : T.ty) : string =
   match ty with

diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml
@@ -140,14 +140,11 @@ class virtual ['self] mapreduce_const_generic_base =
   end
 
 (** Remark: we have to use long names because otherwise we have collisions in
-    the functions derived for the visitors.
-
-    TODO: change the prefix to "CG"
- *)
+    the functions derived for the visitors. *)
 type const_generic =
-  | ConstGenericGlobal of global_decl_id
-  | ConstGenericVar of const_generic_var_id
-  | ConstGenericValue of literal
+  | CGGlobal of global_decl_id
+  | CGVar of const_generic_var_id
+  | CGValue of literal
 [@@deriving
   show,
     ord,

diff --git a/charon-ml/src/TypesUtils.ml b/charon-ml/src/TypesUtils.ml
@@ -61,7 +61,7 @@ let ty_as_literal (ty : ty) : literal_type =
   match ty with TLiteral lty -> lty | _ -> raise (Failure "Unreachable")
 
 let const_generic_as_literal (cg : const_generic) : PrimitiveValues.literal =
-  match cg with ConstGenericValue v -> v | _ -> raise (Failure "Unreachable")
+  match cg with CGValue v -> v | _ -> raise (Failure "Unreachable")
 
 let trait_instance_id_as_trait_impl (id : trait_instance_id) : trait_impl_id =
   match id with TraitImpl id -> id | _ -> raise (Failure "Unreachable")