Prefix the ty variants with "T" in Charon-ML

charon-ml/src/GAstOfJson.ml

@@ -222,8 +222,8 @@ let type_id_of_json (js : json) : (T.type_id, string) result =
     (match js with
     | `Assoc [ ("Adt", id) ] ->
         let* id = T.TypeDeclId.id_of_json id in
-        Ok (T.AdtId id)
-    | `String "Tuple" -> Ok T.Tuple
+        Ok (T.TAdtId id)
+    | `String "Tuple" -> Ok T.TTuple
     | `Assoc [ ("Assumed", aty) ] ->
         let* aty = assumed_ty_of_json aty in
         Ok (T.TAssumed aty)
@@ -329,34 +329,34 @@ let rec ty_of_json (js : json) : (T.ty, string) result =
         let* generics = generic_args_of_json generics in
         (* Sanity check *)
         (match id with
-        | T.Tuple ->
+        | T.TTuple ->
             assert (generics.T.regions = [] && generics.T.trait_refs = [])
         | _ -> ());
         Ok (T.TAdt (id, generics))
     | `Assoc [ ("TypeVar", id) ] ->
         let* id = T.TypeVarId.id_of_json id in
-        Ok (T.TypeVar id)
+        Ok (T.TVar id)
     | `Assoc [ ("Literal", ty) ] ->
         let* ty = literal_type_of_json ty in
         Ok (T.TLiteral ty)
     | `Assoc [ ("Ref", `List [ region; ty; ref_kind ]) ] ->
         let* region = region_of_json region in
         let* ty = ty_of_json ty in
         let* ref_kind = ref_kind_of_json ref_kind in
-        Ok (T.Ref (region, ty, ref_kind))
+        Ok (T.TRef (region, ty, ref_kind))
     | `Assoc [ ("RawPtr", `List [ ty; ref_kind ]) ] ->
         let* ty = ty_of_json ty in
         let* ref_kind = ref_kind_of_json ref_kind in
-        Ok (T.RawPtr (ty, ref_kind))
+        Ok (T.TRawPtr (ty, ref_kind))
     | `Assoc [ ("TraitType", `List [ trait_ref; generics; item_name ]) ] ->
         let* trait_ref = trait_ref_of_json trait_ref in
         let* generics = generic_args_of_json generics in
         let* item_name = string_of_json item_name in
-        Ok (T.TraitType (trait_ref, generics, item_name))
+        Ok (T.TTraitType (trait_ref, generics, item_name))
     | `Assoc [ ("Arrow", `List [ inputs; output ]) ] ->
         let* inputs = list_of_json ty_of_json inputs in
         let* output = ty_of_json output in
-        Ok (T.Arrow (inputs, output))
+        Ok (T.TArrow (inputs, output))
     | _ -> Error "")
 
 and trait_ref_of_json (js : json) : (T.trait_ref, string) result =

charon-ml/src/PrintExpressions.ml

@@ -176,8 +176,8 @@ let rvalue_to_string (fmt : expr_formatter) (rv : E.rvalue) : string =
       match akind with
       | E.AggregatedAdt (type_id, opt_variant_id, _generics) -> (
           match type_id with
-          | Tuple -> "(" ^ String.concat ", " ops ^ ")"
-          | AdtId def_id ->
+          | TTuple -> "(" ^ String.concat ", " ops ^ ")"
+          | TAdtId def_id ->
               let adt_name = fmt.type_decl_id_to_string def_id in
               let variant_name =
                 match opt_variant_id with

charon-ml/src/PrintTypes.ml

@@ -54,8 +54,8 @@ let region_to_string (fmt : type_formatter) (r : T.region) : string =
 
 let type_id_to_string (fmt : type_formatter) (id : T.type_id) : string =
   match id with
-  | T.AdtId id -> fmt.type_decl_id_to_string id
-  | T.Tuple -> ""
+  | T.TAdtId id -> fmt.type_decl_id_to_string id
+  | T.TTuple -> ""
   | T.TAssumed aty -> (
       match aty with
       | TBox -> "alloc::boxed::Box"
@@ -73,27 +73,27 @@ let const_generic_to_string (fmt : type_formatter) (cg : T.const_generic) :
 let rec ty_to_string (fmt : type_formatter) (ty : T.ty) : string =
   match ty with
   | T.TAdt (id, generics) ->
-      let is_tuple = match id with T.Tuple -> true | _ -> false in
+      let is_tuple = match id with T.TTuple -> true | _ -> false in
       let params = params_to_string fmt is_tuple generics in
       type_id_to_string fmt id ^ params
-  | T.TypeVar tv -> fmt.type_var_id_to_string tv
-  | T.Never -> "!"
+  | T.TVar tv -> fmt.type_var_id_to_string tv
+  | T.TNever -> "!"
   | T.TLiteral lit_ty -> literal_type_to_string lit_ty
-  | T.TraitType (trait_ref, generics, type_name) ->
+  | T.TTraitType (trait_ref, generics, type_name) ->
       let trait_ref = trait_ref_to_string fmt trait_ref in
       let generics = generic_args_to_string fmt generics in
       trait_ref ^ generics ^ "::" ^ type_name
-  | T.Ref (r, rty, ref_kind) -> (
+  | T.TRef (r, rty, ref_kind) -> (
       match ref_kind with
       | T.Mut ->
           "&" ^ region_to_string fmt r ^ " mut (" ^ ty_to_string fmt rty ^ ")"
       | T.Shared ->
           "&" ^ region_to_string fmt r ^ " (" ^ ty_to_string fmt rty ^ ")")
-  | T.RawPtr (rty, ref_kind) -> (
+  | T.TRawPtr (rty, ref_kind) -> (
       match ref_kind with
       | T.Mut -> "*mut " ^ ty_to_string fmt rty
       | T.Shared -> "*const " ^ ty_to_string fmt rty)
-  | T.Arrow (inputs, output) ->
+  | T.TArrow (inputs, output) ->
       let inputs =
         "(" ^ String.concat ", " (List.map (ty_to_string fmt) inputs) ^ ") -> "
       in

charon-ml/src/Types.ml

@@ -235,20 +235,20 @@ type assumed_ty = TBox | TArray | TSlice | TStr
     ADTs are very general in our encoding: they account for "regular" ADTs,
     tuples and also assumed types.
 *)
-and type_id = AdtId of type_decl_id | Tuple | TAssumed of assumed_ty
+and type_id = TAdtId of type_decl_id | TTuple | TAssumed of assumed_ty
 
 (* TODO: we should prefix the type variants with "T", this would avoid collisions *)
 and ty =
   | TAdt of type_id * generic_args
       (** {!Types.ty.TAdt} encodes ADTs, tuples and assumed types *)
-  | TypeVar of type_var_id
+  | TVar of type_var_id
   | TLiteral of literal_type
-  | Never
-  | Ref of region * ty * ref_kind
-  | RawPtr of ty * ref_kind
-  | TraitType of trait_ref * generic_args * string
+  | TNever
+  | TRef of region * ty * ref_kind
+  | TRawPtr of ty * ref_kind
+  | TTraitType of trait_ref * generic_args * string
       (** The string is for the name of the associated type *)
-  | Arrow of ty list * ty
+  | TArrow of ty list * ty
 
 and trait_ref = {
   trait_id : trait_instance_id;

charon-ml/src/TypesUtils.ml

@@ -31,7 +31,7 @@ let type_decl_is_enum (def : type_decl) : bool =
 let ty_is_unit (ty : ty) : bool =
   match ty with
   | TAdt
-      (Tuple, { regions = []; types = []; const_generics = []; trait_refs = _ })
+      (TTuple, { regions = []; types = []; const_generics = []; trait_refs = _ })
     ->
       true
   | _ -> false
@@ -46,15 +46,15 @@ let ty_as_adt (ty : ty) : type_id * generic_args =
 
 let ty_as_ref (ty : ty) : region * ty * ref_kind =
   match ty with
-  | Ref (r, ref_ty, kind) -> (r, ref_ty, kind)
+  | TRef (r, ref_ty, kind) -> (r, ref_ty, kind)
   | _ -> raise (Failure "Unreachable")
 
 let ty_is_custom_adt (ty : ty) : bool =
-  match ty with TAdt (AdtId _, _) -> true | _ -> false
+  match ty with TAdt (TAdtId _, _) -> true | _ -> false
 
 let ty_as_custom_adt (ty : ty) : TypeDeclId.id * generic_args =
   match ty with
-  | TAdt (AdtId id, generics) -> (id, generics)
+  | TAdt (TAdtId id, generics) -> (id, generics)
   | _ -> raise (Failure "Unreachable")
 
 let ty_as_literal (ty : ty) : literal_type =
@@ -98,7 +98,7 @@ let merge_generic_args (g1 : generic_args) (g2 : generic_args) : generic_args =
   }
 
 (** The unit type *)
-let mk_unit_ty : ty = TAdt (Tuple, mk_empty_generic_args)
+let mk_unit_ty : ty = TAdt (TTuple, mk_empty_generic_args)
 
 (** The usize type *)
 let mk_usize_ty : ty = TLiteral (TInteger Usize)
@@ -114,11 +114,11 @@ let ty_get_box (box_ty : ty) : ty =
  *)
 let ty_get_ref (ty : ty) : region * ty * ref_kind =
   match ty with
-  | Ref (r, ty, ref_kind) -> (r, ty, ref_kind)
+  | TRef (r, ty, ref_kind) -> (r, ty, ref_kind)
   | _ -> raise (Failure "Not a ref type")
 
 let mk_ref_ty (r : region) (ty : ty) (ref_kind : ref_kind) : ty =
-  Ref (r, ty, ref_kind)
+  TRef (r, ty, ref_kind)
 
 (** Make a box type *)
 let mk_box_ty (ty : ty) : ty =
@@ -192,16 +192,16 @@ let ty_has_regions_in_set (rset : RegionId.Set.t) (ty : ty) : bool =
   *)
 let rec ty_is_primitively_copyable (ty : ty) : bool =
   match ty with
-  | TAdt (AdtId _, generics) ->
+  | TAdt (TAdtId _, generics) ->
       List.for_all ty_is_primitively_copyable generics.types
   | TAdt (TAssumed (TBox | TStr | TSlice), _) -> false
-  | TAdt ((Tuple | TAssumed TArray), generics) ->
+  | TAdt ((TTuple | TAssumed TArray), generics) ->
       List.for_all ty_is_primitively_copyable generics.types
-  | TypeVar _ | Never -> false
+  | TVar _ | TNever -> false
   | TLiteral (TBool | TChar | TInteger _) -> true
-  | TraitType _ | Arrow (_, _) -> false
-  | Ref (_, _, Mut) -> false
-  | Ref (_, _, Shared) -> true
-  | RawPtr (_, _) ->
+  | TTraitType _ | TArrow (_, _) -> false
+  | TRef (_, _, Mut) -> false
+  | TRef (_, _, Shared) -> true
+  | TRawPtr (_, _) ->
       (* Not sure what to do here, so being conservative *)
       false