Prefix variants related to types with "T"

compiler/AssociatedTypes.ml

@@ -55,7 +55,7 @@ let compute_norm_trait_types_from_preds
        that it would be enough to only visit the field [ty] of the trait type
        constraint, but for safety we visit all the fields *)
     assert (TU.trait_type_constraint_no_regions c);
-    let trait_ty = T.TraitType (c.trait_ref, c.generics, c.type_name) in
+    let trait_ty = T.TTraitType (c.trait_ref, c.generics, c.type_name) in
     let trait_ty_ref = get_ref trait_ty in
     let ty_ref = get_ref c.ty in
     let new_repr = UF.get ty_ref in
@@ -76,7 +76,7 @@ let compute_norm_trait_types_from_preds
     List.filter_map
       (fun (k, v) ->
         match k with
-        | T.TraitType (trait_ref, generics, type_name) ->
+        | T.TTraitType (trait_ref, generics, type_name) ->
             assert (generics = TypesUtils.mk_empty_generic_args);
             Some ({ C.trait_ref; type_name }, v)
         | _ -> None)
@@ -182,18 +182,18 @@ let rec ctx_normalize_ty (ctx : norm_ctx) (ty : T.ty) : T.ty =
   log#ldebug (lazy ("ctx_normalize_ty: " ^ ty_to_string ctx ty));
   match ty with
   | T.TAdt (id, generics) -> TAdt (id, ctx_normalize_generic_args ctx generics)
-  | TypeVar _ | TLiteral _ | Never -> ty
-  | Ref (r, ty, rkind) ->
+  | TVar _ | TLiteral _ | TNever -> ty
+  | TRef (r, ty, rkind) ->
       let ty = ctx_normalize_ty ctx ty in
-      T.Ref (r, ty, rkind)
-  | RawPtr (ty, rkind) ->
+      T.TRef (r, ty, rkind)
+  | TRawPtr (ty, rkind) ->
       let ty = ctx_normalize_ty ctx ty in
-      RawPtr (ty, rkind)
-  | Arrow (inputs, output) ->
+      TRawPtr (ty, rkind)
+  | TArrow (inputs, output) ->
       let inputs = List.map (ctx_normalize_ty ctx) inputs in
       let output = ctx_normalize_ty ctx output in
-      Arrow (inputs, output)
-  | TraitType (trait_ref, generics, type_name) -> (
+      TArrow (inputs, output)
+  | TTraitType (trait_ref, generics, type_name) -> (
       log#ldebug
         (lazy
           ("ctx_normalize_ty:\n- trait type: " ^ ty_to_string ctx ty
@@ -250,7 +250,7 @@ let rec ctx_normalize_ty (ctx : norm_ctx) (ty : T.ty) : T.ty =
                 ^ "\n- raw trait ref:\n" ^ T.show_trait_ref trait_ref));
             (* We can't project *)
             assert (trait_instance_id_is_local_clause trait_ref.trait_id);
-            T.TraitType (trait_ref, generics, type_name)
+            T.TTraitType (trait_ref, generics, type_name)
       in
       let tr : C.trait_type_ref = { C.trait_ref; type_name } in
       (* Lookup the representative, if there is *)

compiler/Assumed.ml

@@ -41,7 +41,7 @@ module Sig = struct
   let rvar_0 : T.region = T.RVar rvar_id_0
   let rg_id_0 = T.RegionGroupId.of_int 0
   let tvar_id_0 = T.TypeVarId.of_int 0
-  let tvar_0 : T.ty = T.TypeVar tvar_id_0
+  let tvar_0 : T.ty = T.TVar tvar_id_0
   let cgvar_id_0 = T.ConstGenericVarId.of_int 0
   let cgvar_0 : T.const_generic = T.CGVar cgvar_id_0
 
@@ -150,13 +150,13 @@ module Sig = struct
   let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : A.fun_sig =
     (* Array<T, N> *)
     let input_ty id =
-      if is_array then mk_array_ty (T.TypeVar id) cgvar_0
-      else mk_slice_ty (T.TypeVar id)
+      if is_array then mk_array_ty (T.TVar id) cgvar_0
+      else mk_slice_ty (T.TVar id)
     in
     (* usize *)
     let index_ty = usize_ty in
     (* T *)
-    let output_ty id = T.TypeVar id in
+    let output_ty id = T.TVar id in
     let cgs = if is_array then [ cg_param_0 ] else [] in
     mk_array_slice_borrow_sig cgs input_ty (Some index_ty) output_ty is_mut
 
@@ -165,9 +165,9 @@ module Sig = struct
 
   let array_to_slice_sig (is_mut : bool) : A.fun_sig =
     (* Array<T, N> *)
-    let input_ty id = mk_array_ty (T.TypeVar id) cgvar_0 in
+    let input_ty id = mk_array_ty (T.TVar id) cgvar_0 in
     (* Slice<T> *)
-    let output_ty id = mk_slice_ty (T.TypeVar id) in
+    let output_ty id = mk_slice_ty (T.TVar id) in
     let cgs = [ cg_param_0 ] in
     mk_array_slice_borrow_sig cgs input_ty None output_ty is_mut
 

compiler/Extract.ml

@@ -124,7 +124,7 @@ let extract_adt_g_value
     (inside : bool) (variant_id : VariantId.id option) (field_values : 'v list)
     (ty : ty) : extraction_ctx =
   match ty with
-  | TAdt (Tuple, generics) ->
+  | TAdt (TTuple, generics) ->
       (* Tuple *)
       (* For now, we only support fully applied tuple constructors *)
       assert (List.length generics.types = List.length field_values);
@@ -871,7 +871,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
      thus extracted to unit. We need to check that by looking up the definition *)
   let extract_as_unit =
     match (!backend, supd.struct_id) with
-    | HOL4, AdtId adt_id ->
+    | HOL4, TAdtId adt_id ->
         let d = TypeDeclId.Map.find adt_id ctx.trans_ctx.type_ctx.type_decls in
         d.kind = Struct []
     | _ -> false
@@ -885,7 +885,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
        - this is an array
     *)
     match supd.struct_id with
-    | AdtId _ ->
+    | TAdtId _ ->
         F.pp_open_hvbox fmt 0;
         F.pp_open_hvbox fmt ctx.indent_incr;
         (* Inner/outer brackets: there are several syntaxes for the field updates.
@@ -966,15 +966,15 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
         if need_paren then F.pp_print_string fmt ")";
         print_bracket false orb;
         F.pp_close_box fmt ()
-    | TAssumed Array ->
+    | TAssumed TArray ->
         (* Open the boxes *)
         F.pp_open_hvbox fmt ctx.indent_incr;
         let need_paren = inside in
         if need_paren then F.pp_print_string fmt "(";
         (* Open the box for `Array.replicate T N [` *)
         F.pp_open_hovbox fmt ctx.indent_incr;
         (* Print the array constructor *)
-        let cs = ctx_get_struct (TAssumed Array) ctx in
+        let cs = ctx_get_struct (TAssumed TArray) ctx in
         F.pp_print_string fmt cs;
         (* Print the parameters *)
         let _, generics = ty_as_adt e_ty in
@@ -2662,7 +2662,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_space fmt ();
         F.pp_print_string fmt "=";
         F.pp_print_space fmt ();
-        let success = ctx_get_variant (TAssumed Result) result_return_id ctx in
+        let success = ctx_get_variant (TAssumed TResult) result_return_id ctx in
         F.pp_print_string fmt (success ^ " ())")
     | Coq ->
         F.pp_print_string fmt "Check";
@@ -2691,7 +2691,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_space fmt ();
         F.pp_print_string fmt "==";
         F.pp_print_space fmt ();
-        let success = ctx_get_variant (TAssumed Result) result_return_id ctx in
+        let success = ctx_get_variant (TAssumed TResult) result_return_id ctx in
         F.pp_print_string fmt ("." ^ success ^ " ())")
     | HOL4 ->
         F.pp_print_string fmt "val _ = assert_return (";

compiler/ExtractBase.ml

@@ -672,11 +672,11 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
   (* TODO: factorize the pretty-printing with what is in PrintPure *)
   let get_type_name (id : type_id) : string =
     match id with
-    | AdtId id ->
+    | TAdtId id ->
         let def = TypeDeclId.Map.find id type_decls in
         Print.name_to_string def.name
     | TAssumed aty -> show_assumed_ty aty
-    | Tuple -> raise (Failure "Unreachable")
+    | TTuple -> raise (Failure "Unreachable")
   in
   match id with
   | GlobalId gid ->
@@ -744,26 +744,26 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
   | VariantId (id, variant_id) ->
       let variant_name =
         match id with
-        | Tuple -> raise (Failure "Unreachable")
-        | TAssumed Result ->
+        | TTuple -> raise (Failure "Unreachable")
+        | TAssumed TResult ->
             if variant_id = result_return_id then "@result::Return"
             else if variant_id = result_fail_id then "@result::Fail"
             else raise (Failure "Unreachable")
-        | TAssumed Error ->
+        | TAssumed TError ->
             if variant_id = error_failure_id then "@error::Failure"
             else if variant_id = error_out_of_fuel_id then "@error::OutOfFuel"
             else raise (Failure "Unreachable")
-        | TAssumed Fuel ->
+        | TAssumed TFuel ->
             if variant_id = fuel_zero_id then "@fuel::0"
             else if variant_id = fuel_succ_id then "@fuel::Succ"
             else raise (Failure "Unreachable")
-        | TAssumed (State | Array | Slice | Str | RawPtr _) ->
+        | TAssumed (TState | TArray | TSlice | TStr | TRawPtr _) ->
             raise
               (Failure
                  ("Unreachable: variant id ("
                  ^ VariantId.to_string variant_id
                  ^ ") for " ^ show_type_id id))
-        | AdtId id -> (
+        | TAdtId id -> (
             let def = TypeDeclId.Map.find id type_decls in
             match def.kind with
             | Struct _ | Opaque -> raise (Failure "Unreachable")
@@ -775,12 +775,13 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
   | FieldId (id, field_id) ->
       let field_name =
         match id with
-        | Tuple -> raise (Failure "Unreachable")
+        | TTuple -> raise (Failure "Unreachable")
         | TAssumed
-            (State | Result | Error | Fuel | Array | Slice | Str | RawPtr _) ->
+            ( TState | TResult | TError | TFuel | TArray | TSlice | TStr
+            | TRawPtr _ ) ->
             (* We can't directly have access to the fields of those types *)
             raise (Failure "Unreachable")
-        | AdtId id -> (
+        | TAdtId id -> (
             let def = TypeDeclId.Map.find id type_decls in
             match def.kind with
             | Enum _ | Opaque -> raise (Failure "Unreachable")
@@ -954,11 +955,11 @@ let ctx_get_local_function (id : A.FunDeclId.id) (lp : LoopId.id option)
   ctx_get_function (FromLlbc (FunId (FRegular id), lp, rg)) ctx
 
 let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string =
-  assert (id <> Tuple);
+  assert (id <> TTuple);
   ctx_get (TypeId id) ctx
 
 let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string =
-  ctx_get_type (AdtId id) ctx
+  ctx_get_type (TAdtId id) ctx
 
 let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string =
   ctx_get_type (TAssumed id) ctx