summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/AssociatedTypes.ml22
-rw-r--r--compiler/Assumed.ml12
-rw-r--r--compiler/Extract.ml14
-rw-r--r--compiler/ExtractBase.ml27
-rw-r--r--compiler/ExtractTypes.ml142
-rw-r--r--compiler/Interpreter.ml2
-rw-r--r--compiler/InterpreterBorrows.ml4
-rw-r--r--compiler/InterpreterBorrowsCore.ml10
-rw-r--r--compiler/InterpreterExpansion.ml16
-rw-r--r--compiler/InterpreterExpressions.ml16
-rw-r--r--compiler/InterpreterLoopsFixedPoint.ml2
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml10
-rw-r--r--compiler/InterpreterPaths.ml12
-rw-r--r--compiler/InterpreterProjectors.ml8
-rw-r--r--compiler/InterpreterStatements.ml8
-rw-r--r--compiler/Invariants.ml12
-rw-r--r--compiler/PrePasses.ml2
-rw-r--r--compiler/Print.ml8
-rw-r--r--compiler/PrintPure.ml70
-rw-r--r--compiler/Pure.ml24
-rw-r--r--compiler/PureMicroPasses.ml12
-rw-r--r--compiler/PureTypeCheck.ml18
-rw-r--r--compiler/PureUtils.ml58
-rw-r--r--compiler/Substitute.ml8
-rw-r--r--compiler/SymbolicToPure.ml104
-rw-r--r--compiler/SynthesizeSymbolic.ml6
-rw-r--r--compiler/TypesAnalysis.ml14
27 files changed, 320 insertions, 321 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index c76af138..d5c9596e 100644
--- a/compiler/AssociatedTypes.ml
+++ b/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 *)
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index 5622ef26..cf81502c 100644
--- a/compiler/Assumed.ml
+++ b/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
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 24999c7d..04f6c2c3 100644
--- a/compiler/Extract.ml
+++ b/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,7 +966,7 @@ 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
@@ -974,7 +974,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
(* 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 (";
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 272e6396..d5eac6f4 100644
--- a/compiler/ExtractBase.ml
+++ b/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
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 902b7e25..553d5863 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -226,69 +226,69 @@ let assumed_adts () : (assumed_ty * string) list =
match !backend with
| Lean ->
[
- (State, "State");
- (Result, "Result");
- (Error, "Error");
- (Fuel, "Nat");
- (Array, "Array");
- (Slice, "Slice");
- (Str, "Str");
- (RawPtr Mut, "MutRawPtr");
- (RawPtr Const, "ConstRawPtr");
+ (TState, "State");
+ (TResult, "Result");
+ (TError, "Error");
+ (TFuel, "Nat");
+ (TArray, "Array");
+ (TSlice, "Slice");
+ (TStr, "Str");
+ (TRawPtr Mut, "MutRawPtr");
+ (TRawPtr Const, "ConstRawPtr");
]
| Coq | FStar | HOL4 ->
[
- (State, "state");
- (Result, "result");
- (Error, "error");
- (Fuel, if !backend = HOL4 then "num" else "nat");
- (Array, "array");
- (Slice, "slice");
- (Str, "str");
- (RawPtr Mut, "mut_raw_ptr");
- (RawPtr Const, "const_raw_ptr");
+ (TState, "state");
+ (TResult, "result");
+ (TError, "error");
+ (TFuel, if !backend = HOL4 then "num" else "nat");
+ (TArray, "array");
+ (TSlice, "slice");
+ (TStr, "str");
+ (TRawPtr Mut, "mut_raw_ptr");
+ (TRawPtr Const, "const_raw_ptr");
]
let assumed_struct_constructors () : (assumed_ty * string) list =
match !backend with
- | Lean -> [ (Array, "Array.make") ]
- | Coq -> [ (Array, "mk_array") ]
- | FStar -> [ (Array, "mk_array") ]
- | HOL4 -> [ (Array, "mk_array") ]
+ | Lean -> [ (TArray, "Array.make") ]
+ | Coq -> [ (TArray, "mk_array") ]
+ | FStar -> [ (TArray, "mk_array") ]
+ | HOL4 -> [ (TArray, "mk_array") ]
let assumed_variants () : (assumed_ty * VariantId.id * string) list =
match !backend with
| FStar ->
[
- (Result, result_return_id, "Return");
- (Result, result_fail_id, "Fail");
- (Error, error_failure_id, "Failure");
- (Error, error_out_of_fuel_id, "OutOfFuel");
+ (TResult, result_return_id, "Return");
+ (TResult, result_fail_id, "Fail");
+ (TError, error_failure_id, "Failure");
+ (TError, error_out_of_fuel_id, "OutOfFuel");
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
]
| Coq ->
[
- (Result, result_return_id, "Return");
- (Result, result_fail_id, "Fail_");
- (Error, error_failure_id, "Failure");
- (Error, error_out_of_fuel_id, "OutOfFuel");
- (Fuel, fuel_zero_id, "O");
- (Fuel, fuel_succ_id, "S");
+ (TResult, result_return_id, "Return");
+ (TResult, result_fail_id, "Fail_");
+ (TError, error_failure_id, "Failure");
+ (TError, error_out_of_fuel_id, "OutOfFuel");
+ (TFuel, fuel_zero_id, "O");
+ (TFuel, fuel_succ_id, "S");
]
| Lean ->
[
- (Result, result_return_id, "ret");
- (Result, result_fail_id, "fail");
- (Error, error_failure_id, "panic");
+ (TResult, result_return_id, "ret");
+ (TResult, result_fail_id, "fail");
+ (TError, error_failure_id, "panic");
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
]
| HOL4 ->
[
- (Result, result_return_id, "Return");
- (Result, result_fail_id, "Fail");
- (Error, error_failure_id, "Failure");
+ (TResult, result_return_id, "Return");
+ (TResult, result_fail_id, "Fail");
+ (TError, error_failure_id, "Failure");
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
]
@@ -801,18 +801,18 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
match ty with
| TAdt (type_id, generics) -> (
match type_id with
- | Tuple ->
+ | TTuple ->
(* The "pair" case is frequent enough to have its special treatment *)
if List.length generics.types = 2 then "p" else "t"
- | TAssumed Result -> "r"
- | TAssumed Error -> ConstStrings.error_basename
- | TAssumed Fuel -> ConstStrings.fuel_basename
- | TAssumed Array -> "a"
- | TAssumed Slice -> "s"
- | TAssumed Str -> "s"
- | TAssumed State -> ConstStrings.state_basename
- | TAssumed (RawPtr _) -> "p"
- | AdtId adt_id ->
+ | TAssumed TResult -> "r"
+ | TAssumed TError -> ConstStrings.error_basename
+ | TAssumed TFuel -> ConstStrings.fuel_basename
+ | TAssumed TArray -> "a"
+ | TAssumed TSlice -> "s"
+ | TAssumed TStr -> "s"
+ | TAssumed TState -> ConstStrings.state_basename
+ | TAssumed (TRawPtr _) -> "p"
+ | TAdtId adt_id ->
let def = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in
(* Derive the var name from the last ident of the type name
* Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm"
@@ -821,15 +821,15 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
* be an ident *)
let cl = List.nth def.name (List.length def.name - 1) in
name_from_type_ident (Names.as_ident cl))
- | TypeVar _ -> (
+ | TVar _ -> (
(* TODO: use "t" also for F* *)
match !backend with
| FStar -> "x" (* lacking inspiration here... *)
| Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
| TLiteral lty -> (
match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
- | Arrow _ -> "f"
- | TraitType (_, _, name) -> name_from_type_ident name)
+ | TArrow _ -> "f"
+ | TTraitType (_, _, name) -> name_from_type_ident name)
in
let type_var_basename (_varset : StringSet.t) (basename : string) : string =
(* Rust type variables are snake-case and start with a capital letter *)
@@ -1161,7 +1161,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
| TAdt (type_id, generics) -> (
let has_params = generics <> empty_generic_args in
match type_id with
- | Tuple ->
+ | TTuple ->
(* This is a bit annoying, but in F*/Coq/HOL4 [()] is not the unit type:
* we have to write [unit]... *)
if generics.types = [] then F.pp_print_string fmt (unit_name ())
@@ -1181,7 +1181,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ())
(extract_rec true) generics.types;
F.pp_print_string fmt ")")
- | AdtId _ | TAssumed _ -> (
+ | TAdtId _ | TAssumed _ -> (
(* HOL4 behaves differently. Where in Coq/FStar/Lean we would write:
`tree a b`
@@ -1200,7 +1200,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
argument for `Vec`). *)
let generics =
match type_id with
- | AdtId id -> (
+ | TAdtId id -> (
match
TypeDeclId.Map.find_opt id ctx.types_filter_type_args_map
with
@@ -1223,7 +1223,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
assert (const_generics = []);
let print_tys =
match type_id with
- | AdtId id -> not (TypeDeclId.Set.mem id no_params_tys)
+ | TAdtId id -> not (TypeDeclId.Set.mem id no_params_tys)
| TAssumed _ -> true
| _ -> raise (Failure "Unreachable")
in
@@ -1243,9 +1243,9 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
Collections.List.iter_link (F.pp_print_space fmt)
(extract_trait_ref ctx fmt no_params_tys true)
trait_refs)))
- | TypeVar vid -> F.pp_print_string fmt (ctx_get_type_var vid ctx)
+ | TVar vid -> F.pp_print_string fmt (ctx_get_type_var vid ctx)
| TLiteral lty -> extract_literal_type ctx fmt lty
- | Arrow (arg_ty, ret_ty) ->
+ | TArrow (arg_ty, ret_ty) ->
if inside then F.pp_print_string fmt "(";
extract_rec false arg_ty;
F.pp_print_space fmt ();
@@ -1253,7 +1253,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
extract_rec false ret_ty;
if inside then F.pp_print_string fmt ")"
- | TraitType (trait_ref, generics, type_name) -> (
+ | TTraitType (trait_ref, generics, type_name) -> (
if !parameterize_trait_types then raise (Failure "Unimplemented")
else
let type_name =
@@ -1445,7 +1445,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
| None -> ctx.fmt.type_name def.name
| Some info -> info.extract_name
in
- let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in
+ let ctx = ctx_add (TypeId (TAdtId def.def_id)) def_name ctx in
(* Compute and register:
* - the variant names, if this is an enumeration
* - the field names, if this is a structure
@@ -1487,11 +1487,11 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
let ctx =
List.fold_left
(fun ctx (fid, name) ->
- ctx_add (FieldId (AdtId def.def_id, fid)) name ctx)
+ ctx_add (FieldId (TAdtId def.def_id, fid)) name ctx)
ctx field_names
in
(* Add the constructor name *)
- ctx_add (StructId (AdtId def.def_id)) cons_name ctx
+ ctx_add (StructId (TAdtId def.def_id)) cons_name ctx
| Enum variants ->
let variant_names =
match info with
@@ -1527,7 +1527,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
in
List.fold_left
(fun ctx (vid, vname) ->
- ctx_add (VariantId (AdtId def.def_id, vid)) vname ctx)
+ ctx_add (VariantId (TAdtId def.def_id, vid)) vname ctx)
ctx variant_names
| Opaque ->
(* Nothing to do *)
@@ -1730,7 +1730,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(* If Coq: print the constructor name *)
(* TODO: remove superfluous test not is_rec below *)
if !backend = Coq && not is_rec then (
- F.pp_print_string fmt (ctx_get_struct (AdtId def.def_id) ctx);
+ F.pp_print_string fmt (ctx_get_struct (TAdtId def.def_id) ctx);
F.pp_print_string fmt " ");
(match !backend with
| Lean -> ()
@@ -1744,7 +1744,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
| Lean -> F.pp_open_vbox fmt 0);
(* Print the fields *)
let print_field (field_id : FieldId.id) (f : field) : unit =
- let field_name = ctx_get_field (AdtId def.def_id) field_id ctx in
+ let field_name = ctx_get_field (TAdtId def.def_id) field_id ctx in
(* Open a box for the field *)
F.pp_open_box fmt ctx.indent_incr;
F.pp_print_string fmt field_name;
@@ -1779,7 +1779,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq
we generate `inductive Foo := | mk ... *)
let cons_name =
- if !backend = Lean then "mk" else ctx_get_struct (AdtId def.def_id) ctx
+ if !backend = Lean then "mk" else ctx_get_struct (TAdtId def.def_id) ctx
in
let def_name = ctx_get_local_type def.def_id ctx in
extract_type_decl_variant ctx fmt type_decl_group def_name type_params
@@ -2223,7 +2223,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
match decl.kind with
| Opaque -> ()
| Struct fields ->
- let adt_id = AdtId decl.def_id in
+ let adt_id = TAdtId decl.def_id in
(* Generate the instruction for the record constructor *)
let cons_name = ctx_get_struct adt_id ctx in
extract_coq_arguments_instruction ctx fmt cons_name num_params;
@@ -2241,7 +2241,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
(* Generate the instructions *)
VariantId.iteri
(fun vid (_ : variant) ->
- let cons_name = ctx_get_variant (AdtId decl.def_id) vid ctx in
+ let cons_name = ctx_get_variant (TAdtId decl.def_id) vid ctx in
extract_coq_arguments_instruction ctx fmt cons_name num_params)
variants;
(* Add breaks to insert new lines between definitions *)
@@ -2270,7 +2270,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
let ctx, record_var = ctx_add_var "x" (VarId.of_int 0) ctx in
let ctx, field_var = ctx_add_var "x" (VarId.of_int 1) ctx in
let def_name = ctx_get_local_type decl.def_id ctx in
- let cons_name = ctx_get_struct (AdtId decl.def_id) ctx in
+ let cons_name = ctx_get_struct (TAdtId decl.def_id) ctx in
let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
F.pp_print_space fmt ();
(* Outer box for the projector definition *)
@@ -2281,7 +2281,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
F.pp_open_hovbox fmt ctx.indent_incr;
F.pp_print_string fmt "Definition";
F.pp_print_space fmt ();
- let field_name = ctx_get_field (AdtId decl.def_id) field_id ctx in
+ let field_name = ctx_get_field (TAdtId decl.def_id) field_id ctx in
F.pp_print_string fmt field_name;
(* Print the generics *)
let as_implicits = true in
@@ -2364,7 +2364,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
let ctx, record_var = ctx_add_var "x" (VarId.of_int 0) ctx in
F.pp_print_string fmt "Notation";
F.pp_print_space fmt ();
- let field_name = ctx_get_field (AdtId decl.def_id) field_id ctx in
+ let field_name = ctx_get_field (TAdtId decl.def_id) field_id ctx in
F.pp_print_string fmt ("\"" ^ record_var ^ " .(" ^ field_name ^ ")\"");
F.pp_print_space fmt ();
F.pp_print_string fmt ":=";
@@ -2421,7 +2421,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
* one line *)
F.pp_open_hvbox fmt 0;
(* Retrieve the name *)
- let state_name = ctx_get_assumed_type State ctx in
+ let state_name = ctx_get_assumed_type TState ctx in
(* The syntax for Lean and Coq is almost identical. *)
let print_axiom () =
let axiom =
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index b1178aa7..395c0c80 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -71,7 +71,7 @@ let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (sg : A.fun_sig)
let generics =
let { T.regions; types; const_generics; trait_clauses } = sg.generics in
let regions = List.map (fun _ -> T.RErased) regions in
- let types = List.map (fun (v : T.type_var) -> T.TypeVar v.T.index) types in
+ let types = List.map (fun (v : T.type_var) -> T.TVar v.T.index) types in
let const_generics =
List.map
(fun (v : T.const_generic_var) -> T.CGVar v.T.index)
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index d4dbf80a..c54d55d4 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1889,7 +1889,7 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
match bc with
| SharedBorrow bid ->
assert (ty_no_regions ref_ty);
- let ty = T.Ref (T.RVar r_id, ref_ty, kind) in
+ let ty = T.TRef (T.RVar r_id, ref_ty, kind) in
let value = V.ABorrow (V.ASharedBorrow bid) in
([ { V.value; ty } ], v)
| MutBorrow (bid, bv) ->
@@ -1897,7 +1897,7 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
(* We don't support nested borrows for now *)
assert (not (value_has_borrows ctx bv.V.value));
(* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
- let ty = T.Ref (T.RVar r_id, ref_ty, kind) in
+ let ty = T.TRef (T.RVar r_id, ref_ty, kind) in
let ignored = mk_aignored ref_ty in
let av = V.ABorrow (V.AMutBorrow (bid, ignored)) in
let av = { V.value = av; ty } in
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index cf8e5994..8807f3ef 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -107,10 +107,10 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool)
assert (ty_is_rty ty1 && ty_is_rty ty2);
(* Normalize the associated types *)
match (ty1, ty2) with
- | T.TLiteral lit1, T.TLiteral lit2 ->
+ | TLiteral lit1, TLiteral lit2 ->
assert (lit1 = lit2);
default
- | T.TAdt (id1, generics1), T.TAdt (id2, generics2) ->
+ | TAdt (id1, generics1), TAdt (id2, generics2) ->
assert (id1 = id2);
(* There are no regions in the const generics, so we ignore them,
but we still check they are the same, for sanity *)
@@ -146,7 +146,7 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool)
in
(* Combine *)
combine params_b tys_b
- | T.Ref (r1, ty1, kind1), T.Ref (r2, ty2, kind2) ->
+ | TRef (r1, ty1, kind1), TRef (r2, ty2, kind2) ->
(* Sanity check *)
assert (kind1 = kind2);
(* Explanation for the case where we check if projections intersect:
@@ -155,10 +155,10 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool)
let regions_b = compare_regions r1 r2 in
let tys_b = compare ty1 ty2 in
combine regions_b tys_b
- | T.TypeVar id1, T.TypeVar id2 ->
+ | TVar id1, TVar id2 ->
assert (id1 = id2);
default
- | T.TraitType _, T.TraitType _ ->
+ | TTraitType _, TTraitType _ ->
(* The types should have been normalized. If after normalization we
get trait types, we can consider them as variables *)
assert (ty1 = ty2);
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 48688893..b07f2629 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -272,10 +272,10 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
(kind : V.sv_kind) (adt_id : T.type_id) (generics : T.generic_args)
(ctx : C.eval_ctx) : V.symbolic_expansion list =
match (adt_id, generics.regions, generics.types) with
- | T.AdtId def_id, _, _ ->
+ | T.TAdtId def_id, _, _ ->
compute_expanded_symbolic_non_assumed_adt_value expand_enumerations kind
def_id generics ctx
- | T.Tuple, [], _ ->
+ | T.TTuple, [], _ ->
[ compute_expanded_symbolic_tuple_value kind generics.types ]
| T.TAssumed T.TBox, [], [ boxed_ty ] ->
[ compute_expanded_symbolic_box_value kind boxed_ty ]
@@ -306,7 +306,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
V.abstract_shared_borrows option =
if same_symbolic_id sv original_sv then
match proj_ty with
- | T.Ref (r, ref_ty, T.Shared) ->
+ | T.TRef (r, ref_ty, T.Shared) ->
(* Projector over the shared value *)
let shared_asb = V.AsbProjReborrows (sv, ref_ty) in
(* Check if the region is in the set of projected regions *)
@@ -548,7 +548,7 @@ let expand_symbolic_value_no_branching (config : C.config)
S.synthesize_symbolic_expansion_no_branching original_sv
original_sv_place see expr
(* Borrows *)
- | T.Ref (region, ref_ty, rkind) ->
+ | T.TRef (region, ref_ty, rkind) ->
expand_symbolic_value_borrow config original_sv original_sv_place region
ref_ty rkind cf ctx
| _ ->
@@ -665,7 +665,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
^ symbolic_value_to_string ctx sv));
let cc : cm_fun =
match sv.V.sv_ty with
- | T.TAdt (AdtId def_id, _) ->
+ | T.TAdt (TAdtId def_id, _) ->
(* {!expand_symbolic_value_no_branching} checks if there are branchings,
* but we prefer to also check it here - this leads to cleaner messages
* and debugging *)
@@ -690,7 +690,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
[config]): "
^ Print.name_to_string def.name))
else expand_symbolic_value_no_branching config sv None
- | T.TAdt ((Tuple | TAssumed TBox), _) | T.Ref (_, _, _) ->
+ | T.TAdt ((TTuple | TAssumed TBox), _) | T.TRef (_, _, _) ->
(* Ok *)
expand_symbolic_value_no_branching config sv None
| T.TAdt (TAssumed (TArray | TSlice | TStr), _) ->
@@ -698,8 +698,8 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
raise
(Failure
"Attempted to greedily expand an ADT which can't be expanded ")
- | T.TypeVar _ | T.TLiteral _ | Never | T.TraitType _ | T.Arrow _
- | T.RawPtr _ ->
+ | T.TVar _ | T.TLiteral _ | TNever | T.TTraitType _ | T.TArrow _
+ | T.TRawPtr _ ->
raise (Failure "Unreachable")
in
(* Compose and continue *)
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index c7fcc1af..7865d7be 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -144,9 +144,9 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
(match v.V.ty with
| T.TAdt (T.TAssumed T.TBox, _) ->
raise (Failure "Can't copy an assumed value other than Option")
- | T.TAdt (T.AdtId _, _) as ty ->
+ | T.TAdt (T.TAdtId _, _) as ty ->
assert (allow_adt_copy || ty_is_primitively_copyable ty)
- | T.TAdt (T.Tuple, _) -> () (* Ok *)
+ | T.TAdt (T.TTuple, _) -> () (* Ok *)
| T.TAdt
( T.TAssumed (TSlice | T.TArray),
{
@@ -670,7 +670,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
| E.TwoPhaseMut -> T.Mut
| _ -> raise (Failure "Unreachable")
in
- let rv_ty = T.Ref (T.RErased, v.ty, ref_kind) in
+ let rv_ty = T.TRef (T.RErased, v.ty, ref_kind) in
let bc =
match bkind with
| E.Shared | E.Shallow ->
@@ -698,7 +698,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
fun ctx ->
(* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
let bid = C.fresh_borrow_id () in
- let rv_ty = T.Ref (T.RErased, v.ty, Mut) in
+ let rv_ty = T.TRef (T.RErased, v.ty, Mut) in
let rv : V.typed_value =
{ V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty }
in
@@ -725,15 +725,15 @@ let eval_rvalue_aggregate (config : C.config)
match aggregate_kind with
| E.AggregatedAdt (type_id, opt_variant_id, generics) -> (
match type_id with
- | Tuple ->
+ | TTuple ->
let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
let v = V.VAdt { variant_id = None; field_values = values } in
let generics = TypesUtils.mk_generic_args [] tys [] [] in
- let ty = T.TAdt (T.Tuple, generics) in
+ let ty = T.TAdt (T.TTuple, generics) in
let aggregated : V.typed_value = { V.value = v; ty } in
(* Call the continuation *)
cf aggregated ctx
- | AdtId def_id ->
+ | TAdtId def_id ->
(* Sanity checks *)
let type_decl = C.ctx_lookup_type_decl ctx def_id in
assert (
@@ -750,7 +750,7 @@ let eval_rvalue_aggregate (config : C.config)
let av : V.adt_value =
{ V.variant_id = opt_variant_id; V.field_values = values }
in
- let aty = T.TAdt (T.AdtId def_id, generics) in
+ let aty = T.TAdt (T.TAdtId def_id, generics) in
let aggregated : V.typed_value = { V.value = VAdt av; ty = aty } in
(* Call the continuation *)
cf aggregated ctx
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 3447131c..2f7e8f3d 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -170,7 +170,7 @@ let prepare_ashared_loans (loop_id : V.LoopId.id option) : cm_fun =
let child_av = mk_aignored child_rty in
(* Create the shared loan *)
- let loan_rty = T.Ref (T.RVar nrid, rty, T.Shared) in
+ let loan_rty = T.TRef (T.RVar nrid, rty, T.Shared) in
let loan_value =
V.ALoan (V.ASharedLoan (V.BorrowId.Set.singleton nlid, nsv, child_av))
in
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 9bc25626..27020efb 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -172,20 +172,20 @@ let rec match_types (match_distinct_types : T.ty -> T.ty -> T.ty)
in
let generics = { T.regions; types; const_generics; trait_refs } in
TAdt (id, generics)
- | TypeVar vid0, TypeVar vid1 ->
+ | TVar vid0, TVar vid1 ->
assert (vid0 = vid1);
let vid = vid0 in
- TypeVar vid
+ TVar vid
| TLiteral lty0, TLiteral lty1 ->
assert (lty0 = lty1);
ty0
- | Never, Never -> ty0
- | Ref (r0, ty0, k0), Ref (r1, ty1, k1) ->
+ | TNever, TNever -> ty0
+ | TRef (r0, ty0, k0), TRef (r1, ty1, k1) ->
let r = match_regions r0 r1 in
let ty = match_rec ty0 ty1 in
assert (k0 = k1);
let k = k0 in
- Ref (r, ty, k)
+ TRef (r, ty, k)
| _ -> match_distinct_types ty0 ty1
module MakeMatcher (M : PrimMatcher) : Matcher = struct
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 728e5226..36af1db4 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -101,7 +101,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
T.TAdt (type_id, _) ) -> (
(* Check consistency *)
(match (proj_kind, type_id) with
- | ProjAdt (def_id, opt_variant_id), T.AdtId def_id' ->
+ | ProjAdt (def_id, opt_variant_id), T.TAdtId def_id' ->
assert (def_id = def_id');
assert (opt_variant_id = adt.variant_id)
| _ -> raise (Failure "Unreachable"));
@@ -118,7 +118,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
let updated = { v with value = nadt } in
Ok (ctx, { res with updated }))
(* Tuples *)
- | Field (ProjTuple arity, field_id), V.VAdt adt, T.TAdt (T.Tuple, _) -> (
+ | Field (ProjTuple arity, field_id), V.VAdt adt, T.TAdt (T.TTuple, _) -> (
assert (arity = List.length adt.field_values);
let fv = T.FieldId.nth adt.field_values field_id in
(* Project *)
@@ -372,7 +372,7 @@ let compute_expanded_bottom_adt_value (ctx : C.eval_ctx)
(* Initialize the expanded value *)
let fields = List.map mk_bottom field_types in
let av = V.VAdt { variant_id = opt_variant_id; field_values = fields } in
- let ty = T.TAdt (T.AdtId def_id, generics) in
+ let ty = T.TAdt (TAdtId def_id, generics) in
{ V.value = av; V.ty }
let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
@@ -381,7 +381,7 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
let fields = List.map mk_bottom field_types in
let v = V.VAdt { variant_id = None; field_values = fields } in
let generics = TypesUtils.mk_generic_args [] field_types [] [] in
- let ty = T.TAdt (T.Tuple, generics) in
+ let ty = T.TAdt (TTuple, generics) in
{ V.value = v; V.ty }
(** Auxiliary helper to expand {!V.Bottom} values.
@@ -433,13 +433,13 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place)
match (pe, ty) with
(* "Regular" ADTs *)
| ( Field (ProjAdt (def_id, opt_variant_id), _),
- T.TAdt (T.AdtId def_id', generics) ) ->
+ T.TAdt (TAdtId def_id', generics) ) ->
assert (def_id = def_id');
compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics
(* Tuples *)
| ( Field (ProjTuple arity, _),
T.TAdt
- ( T.Tuple,
+ ( TTuple,
{ T.regions = []; types; const_generics = []; trait_refs = [] } ) )
->
assert (arity = List.length types);
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 70a77be5..e47886ec 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -43,7 +43,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
in
List.concat proj_fields
| V.Bottom, _ -> raise (Failure "Unreachable")
- | V.Borrow bc, T.Ref (r, ref_ty, kind) ->
+ | V.Borrow bc, TRef (r, ref_ty, kind) ->
(* Retrieve the bid of the borrow and the asb of the projected borrowed value *)
let bid, asb =
(* Not in the set: dive *)
@@ -121,7 +121,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
in
V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields }
| V.Bottom, _ -> raise (Failure "Unreachable")
- | V.Borrow bc, T.Ref (r, ref_ty, kind) ->
+ | V.Borrow bc, TRef (r, ref_ty, kind) ->
if
(* Check if the region is in the set of projected regions (note that
* we never project over static regions) *)
@@ -277,7 +277,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
field_values
in
(V.AAdt { V.variant_id; field_values }, original_sv_ty)
- | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) ->
+ | SeMutRef (bid, spc), TRef (r, ref_ty, T.Mut) ->
(* Sanity check *)
assert (spc.V.sv_ty = ref_ty);
(* Apply the projector to the borrowed value *)
@@ -295,7 +295,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
if region_in_set r ancestors_regions then Some bid else None
in
(V.ALoan (V.AIgnoredMutLoan (opt_bid, child_av)), ref_ty)
- | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) ->
+ | SeSharedRef (bids, spc), TRef (r, ref_ty, T.Shared) ->
(* Sanity check *)
assert (spc.V.sv_ty = ref_ty);
(* Apply the projector to the borrowed value *)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index cdcea2cc..cf9b840b 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -232,7 +232,7 @@ let set_discriminant (config : C.config) (p : E.place)
let update_value cf (v : V.typed_value) : m_fun =
fun ctx ->
match (v.V.ty, v.V.value) with
- | T.TAdt ((T.AdtId _ as type_id), generics), V.VAdt av -> (
+ | T.TAdt ((T.TAdtId _ as type_id), generics), V.VAdt av -> (
(* There are two situations:
- either the discriminant is already the proper one (in which case we
don't do anything)
@@ -248,16 +248,16 @@ let set_discriminant (config : C.config) (p : E.place)
(* Replace the value *)
let bottom_v =
match type_id with
- | T.AdtId def_id ->
+ | T.TAdtId def_id ->
compute_expanded_bottom_adt_value ctx def_id
(Some variant_id) generics
| _ -> raise (Failure "Unreachable")
in
assign_to_place config bottom_v p (cf Unit) ctx)
- | T.TAdt ((T.AdtId _ as type_id), generics), V.Bottom ->
+ | T.TAdt ((T.TAdtId _ as type_id), generics), V.Bottom ->
let bottom_v =
match type_id with
- | T.AdtId def_id ->
+ | T.TAdtId def_id ->
compute_expanded_bottom_adt_value ctx def_id (Some variant_id)
generics
| _ -> raise (Failure "Unreachable")
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 01de6fd0..8895bd8e 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -419,7 +419,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
(match (tv.V.value, tv.V.ty) with
| V.VLiteral cv, T.TLiteral ty -> check_literal_type cv ty
(* ADT case *)
- | V.VAdt av, T.TAdt (T.AdtId def_id, generics) ->
+ | V.VAdt av, T.TAdt (T.TAdtId def_id, generics) ->
(* Retrieve the definition to check the variant id, the number of
* parameters, etc. *)
let def = C.ctx_lookup_type_decl ctx def_id in
@@ -445,7 +445,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
(fun ((v, ty) : V.typed_value * T.ty) -> assert (v.V.ty = ty))
fields_with_types
(* Tuple case *)
- | V.VAdt av, T.TAdt (T.Tuple, generics) ->
+ | V.VAdt av, T.TAdt (T.TTuple, generics) ->
assert (generics.regions = []);
assert (generics.const_generics = []);
assert (av.V.variant_id = None);
@@ -486,7 +486,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| (T.TSlice | T.TStr), _, _, _, _ -> raise (Failure "Unexpected")
| _ -> raise (Failure "Erroneous type"))
| V.Bottom, _ -> (* Nothing to check *) ()
- | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
+ | V.Borrow bc, T.TRef (_, ref_ty, rkind) -> (
match (bc, rkind) with
| V.SharedBorrow bid, T.Shared | V.ReservedMutBorrow bid, T.Mut -> (
(* Lookup the borrowed value to check it has the proper type *)
@@ -533,7 +533,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
(* Check the current pair (value, type) *)
(match (atv.V.value, atv.V.ty) with
(* ADT case *)
- | V.AAdt av, T.TAdt (T.AdtId def_id, generics) ->
+ | V.AAdt av, T.TAdt (T.TAdtId def_id, generics) ->
(* Retrieve the definition to check the variant id, the number of
* parameters, etc. *)
let def = C.ctx_lookup_type_decl ctx def_id in
@@ -562,7 +562,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
(fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.V.ty = ty))
fields_with_types
(* Tuple case *)
- | V.AAdt av, T.TAdt (T.Tuple, generics) ->
+ | V.AAdt av, T.TAdt (T.TTuple, generics) ->
assert (generics.regions = []);
assert (generics.const_generics = []);
assert (av.V.variant_id = None);
@@ -589,7 +589,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
assert (boxed_value.V.ty = boxed_ty)
| _ -> raise (Failure "Erroneous type"))
| V.ABottom, _ -> (* Nothing to check *) ()
- | V.ABorrow bc, T.Ref (_, ref_ty, rkind) -> (
+ | V.ABorrow bc, T.TRef (_, ref_ty, rkind) -> (
match (bc, rkind) with
| V.AMutBorrow (_, av), T.Mut ->
(* Check that the child value has the proper type *)
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index ee06fa07..67063af9 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -108,7 +108,7 @@ let remove_useless_cf_merges (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
| Assign (_, rv) -> (
match rv with
| Use _ | RvRef _ -> not must_end_with_exit
- | Aggregate (AggregatedAdt (Tuple, _, _), []) -> not must_end_with_exit
+ | Aggregate (AggregatedAdt (TTuple, _, _), []) -> not must_end_with_exit
| _ -> false)
| FakeRead _ | Drop _ | Nop -> not must_end_with_exit
| Panic | Return -> true
diff --git a/compiler/Print.ml b/compiler/Print.ml
index dd24767e..7494dc2a 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -73,10 +73,10 @@ module Values = struct
List.map (typed_value_to_string fmt) av.field_values
in
match v.ty with
- | T.TAdt (T.Tuple, _) ->
+ | T.TAdt (T.TTuple, _) ->
(* Tuple *)
"(" ^ String.concat ", " field_values ^ ")"
- | T.TAdt (T.AdtId def_id, _) ->
+ | T.TAdt (T.TAdtId def_id, _) ->
(* "Regular" ADT *)
let adt_ident =
match av.variant_id with
@@ -177,10 +177,10 @@ module Values = struct
List.map (typed_avalue_to_string fmt) av.field_values
in
match v.ty with
- | T.TAdt (T.Tuple, _) ->
+ | T.TAdt (T.TTuple, _) ->
(* Tuple *)
"(" ^ String.concat ", " field_values ^ ")"
- | T.TAdt (T.AdtId def_id, _) ->
+ | T.TAdt (T.TAdtId def_id, _) ->
(* "Regular" ADT *)
let adt_ident =
match av.variant_id with
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 7c52c423..8b737cb5 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -191,20 +191,20 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
let assumed_ty_to_string (aty : assumed_ty) : string =
match aty with
- | State -> "State"
- | Result -> "Result"
- | Error -> "Error"
- | Fuel -> "Fuel"
- | Array -> "Array"
- | Slice -> "Slice"
- | Str -> "Str"
- | RawPtr Mut -> "MutRawPtr"
- | RawPtr Const -> "ConstRawPtr"
+ | TState -> "State"
+ | TResult -> "Result"
+ | TError -> "Error"
+ | TFuel -> "Fuel"
+ | TArray -> "Array"
+ | TSlice -> "Slice"
+ | TStr -> "Str"
+ | TRawPtr Mut -> "MutRawPtr"
+ | TRawPtr Const -> "ConstRawPtr"
let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
match id with
- | AdtId id -> fmt.type_decl_id_to_string id
- | Tuple -> ""
+ | TAdtId id -> fmt.type_decl_id_to_string id
+ | TTuple -> ""
| TAssumed aty -> assumed_ty_to_string aty
(* TODO: duplicates Charon.PrintTypes.const_generic_to_string *)
@@ -219,24 +219,24 @@ let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string =
match ty with
| TAdt (id, generics) -> (
match id with
- | Tuple ->
+ | TTuple ->
let generics = generic_args_to_strings fmt false generics in
"(" ^ String.concat " * " generics ^ ")"
- | AdtId _ | TAssumed _ ->
+ | TAdtId _ | TAssumed _ ->
let generics = generic_args_to_strings fmt true generics in
let generics_s =
if generics = [] then "" else " " ^ String.concat " " generics
in
let ty_s = type_id_to_string fmt id ^ generics_s in
if generics <> [] && inside then "(" ^ ty_s ^ ")" else ty_s)
- | TypeVar tv -> fmt.type_var_id_to_string tv
+ | TVar tv -> fmt.type_var_id_to_string tv
| TLiteral lty -> literal_type_to_string lty
- | Arrow (arg_ty, ret_ty) ->
+ | TArrow (arg_ty, ret_ty) ->
let ty =
ty_to_string fmt true arg_ty ^ " -> " ^ ty_to_string fmt false ret_ty
in
if inside then "(" ^ ty ^ ")" else ty
- | TraitType (trait_ref, generics, type_name) ->
+ | TTraitType (trait_ref, generics, type_name) ->
let trait_ref = trait_ref_to_string fmt false trait_ref in
let s =
if generics = empty_generic_args then trait_ref ^ "::" ^ type_name
@@ -378,8 +378,8 @@ let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
(variant_id : VariantId.id option) : string =
match adt_id with
- | Tuple -> "Tuple"
- | AdtId def_id -> (
+ | TTuple -> "Tuple"
+ | TAdtId def_id -> (
(* "Regular" ADT *)
match variant_id with
| Some vid -> fmt.adt_variant_to_string def_id vid
@@ -387,21 +387,21 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
| TAssumed aty -> (
(* Assumed type *)
match aty with
- | State | Array | Slice | Str | RawPtr _ ->
+ | TState | TArray | TSlice | TStr | TRawPtr _ ->
(* Those types are opaque: we can't get there *)
raise (Failure "Unreachable")
- | Result ->
+ | TResult ->
let variant_id = Option.get variant_id in
if variant_id = result_return_id then "@Result::Return"
else if variant_id = result_fail_id then "@Result::Fail"
else
raise (Failure "Unreachable: improper variant id for result type")
- | Error ->
+ | TError ->
let variant_id = Option.get variant_id in
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: improper variant id for error type")
- | Fuel ->
+ | TFuel ->
let variant_id = Option.get variant_id in
if variant_id = fuel_zero_id then "@Fuel::Zero"
else if variant_id = fuel_succ_id then "@Fuel::Succ"
@@ -410,10 +410,10 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
(field_id : FieldId.id) : string =
match adt_id with
- | Tuple ->
+ | TTuple ->
raise (Failure "Unreachable")
(* Tuples don't use the opaque field id for the field indices, but [int] *)
- | AdtId def_id -> (
+ | TAdtId def_id -> (
(* "Regular" ADT *)
let fields = fmt.adt_field_names def_id None in
match fields with
@@ -422,10 +422,10 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
| TAssumed aty -> (
(* Assumed type *)
match aty with
- | State | Fuel | Array | Slice | Str ->
+ | TState | TFuel | TArray | TSlice | TStr ->
(* Opaque types: we can't get there *)
raise (Failure "Unreachable")
- | Result | Error | RawPtr _ ->
+ | TResult | TError | TRawPtr _ ->
(* Enumerations: we can't get there *)
raise (Failure "Unreachable"))
@@ -437,10 +437,10 @@ let adt_g_value_to_string (fmt : value_formatter)
(field_values : 'v list) (ty : ty) : string =
let field_values = List.map value_to_string field_values in
match ty with
- | TAdt (Tuple, _) ->
+ | TAdt (TTuple, _) ->
(* Tuple *)
"(" ^ String.concat ", " field_values ^ ")"
- | TAdt (AdtId def_id, _) ->
+ | TAdt (TAdtId def_id, _) ->
(* "Regular" ADT *)
let adt_ident =
match variant_id with
@@ -465,10 +465,10 @@ let adt_g_value_to_string (fmt : value_formatter)
| TAdt (TAssumed aty, _) -> (
(* Assumed type *)
match aty with
- | State | RawPtr _ ->
+ | TState | TRawPtr _ ->
(* This type is opaque: we can't get there *)
raise (Failure "Unreachable")
- | Result ->
+ | TResult ->
let variant_id = Option.get variant_id in
if variant_id = result_return_id then
match field_values with
@@ -480,13 +480,13 @@ let adt_g_value_to_string (fmt : value_formatter)
| _ -> raise (Failure "Result::Fail takes exactly one value")
else
raise (Failure "Unreachable: improper variant id for result type")
- | Error ->
+ | TError ->
assert (field_values = []);
let variant_id = Option.get variant_id in
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: improper variant id for error type")
- | Fuel ->
+ | TFuel ->
let variant_id = Option.get variant_id in
if variant_id = fuel_zero_id then (
assert (field_values = []);
@@ -496,7 +496,7 @@ let adt_g_value_to_string (fmt : value_formatter)
| [ v ] -> "@Fuel::Succ " ^ v
| _ -> raise (Failure "@Fuel::Succ takes exactly one value")
else raise (Failure "Unreachable: improper variant id for fuel type")
- | Array | Slice | Str ->
+ | TArray | TSlice | TStr ->
assert (variant_id = None);
let field_values =
List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
@@ -650,7 +650,7 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
let indent2 = indent1 ^ indent_incr in
(* The id should be a custom type decl id or an array *)
match supd.struct_id with
- | AdtId aid ->
+ | TAdtId aid ->
let field_names = Option.get (fmt.adt_field_names aid None) in
let fields =
List.map
@@ -664,7 +664,7 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
in
let bl = if fields = [] then "" else "\n" ^ indent in
"{" ^ s ^ String.concat "" fields ^ bl ^ "}"
- | TAssumed Array ->
+ | TAssumed TArray ->
let fields =
List.map
(fun (_, fe) ->
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index ffbd1f09..72a6400e 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -68,14 +68,14 @@ type mutability = Mut | Const [@@deriving show, ord]
TODO: add a prefix "T"
*)
type assumed_ty =
- | State
- | Result
- | Error
- | Fuel
- | Array
- | Slice
- | Str
- | RawPtr of mutability
+ | TState
+ | TResult
+ | TError
+ | TFuel
+ | TArray
+ | TSlice
+ | TStr
+ | TRawPtr of mutability
(** The bool
Raw pointers don't make sense in the pure world, but we don't know
how to translate them yet and we have to handle some functions which
@@ -146,7 +146,7 @@ class virtual ['self] mapreduce_type_id_base =
fun _ x -> (x, self#zero)
end
-type type_id = AdtId of type_decl_id | Tuple | TAssumed of assumed_ty
+type type_id = TAdtId of type_decl_id | TTuple | TAssumed of assumed_ty
[@@deriving
show,
ord,
@@ -276,10 +276,10 @@ type ty =
be able to only give back part of the ADT. We need a way to encode
such "partial" ADTs.
*)
- | TypeVar of type_var_id
+ | TVar of type_var_id
| TLiteral of literal_type
- | Arrow of ty * ty
- | TraitType of trait_ref * generic_args * string
+ | TArrow of ty * ty
+ | TTraitType of trait_ref * generic_args * string
(** The string is for the name of the associated type *)
and trait_ref = {
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index d62a028e..8872571f 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -582,7 +582,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
match app.e with
| Qualif
{
- id = AdtCons { adt_id = AdtId adt_id; variant_id = None };
+ id = AdtCons { adt_id = TAdtId adt_id; variant_id = None };
generics = _;
} ->
(* Lookup the def *)
@@ -606,7 +606,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
(!Config.backend <> Lean && !Config.backend <> Coq)
|| not is_rec
then
- let struct_id = AdtId adt_id in
+ let struct_id = TAdtId adt_id in
let init = None in
let updates =
FieldId.mapi
@@ -1085,7 +1085,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
match app.e with
| Qualif
{
- id = AdtCons { adt_id = AdtId adt_id; variant_id = None };
+ id = AdtCons { adt_id = TAdtId adt_id; variant_id = None };
generics;
} ->
(* This is a struct *)
@@ -1114,7 +1114,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
| ( Qualif
{
id =
- Proj { adt_id = AdtId proj_adt_id; field_id };
+ Proj { adt_id = TAdtId proj_adt_id; field_id };
generics = proj_generics;
},
Var v ) ->
@@ -1157,13 +1157,13 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
match (proj.e, x.e) with
| ( Qualif
{
- id = Proj { adt_id = AdtId proj_adt_id; field_id };
+ id = Proj { adt_id = TAdtId proj_adt_id; field_id };
generics = _;
},
Var v ) ->
(* We check that this is the proper ADT, and the proper field *)
if
- AdtId proj_adt_id = struct_id
+ TAdtId proj_adt_id = struct_id
&& field_id = fid && x.ty = adt_ty
then Some v
else None
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index f8b5de6a..ea1851f0 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -12,41 +12,41 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
(type_id : type_id) (variant_id : VariantId.id option)
(generics : generic_args) : ty list =
match type_id with
- | Tuple ->
+ | TTuple ->
(* Tuple *)
assert (generics.const_generics = []);
assert (generics.trait_refs = []);
assert (variant_id = None);
generics.types
- | AdtId def_id ->
+ | TAdtId def_id ->
(* "Regular" ADT *)
let def = TypeDeclId.Map.find def_id type_decls in
type_decl_get_instantiated_fields_types def variant_id generics
| TAssumed aty -> (
(* Assumed type *)
match aty with
- | State ->
+ | TState ->
(* This type is opaque *)
raise (Failure "Unreachable: opaque type")
- | Result ->
+ | TResult ->
let ty = Collections.List.to_cons_nil generics.types in
let variant_id = Option.get variant_id in
if variant_id = result_return_id then [ ty ]
else if variant_id = result_fail_id then [ mk_error_ty ]
else
raise (Failure "Unreachable: improper variant id for result type")
- | Error ->
+ | TError ->
assert (generics = empty_generic_args);
let variant_id = Option.get variant_id in
assert (
variant_id = error_failure_id || variant_id = error_out_of_fuel_id);
[]
- | Fuel ->
+ | TFuel ->
let variant_id = Option.get variant_id in
if variant_id = fuel_zero_id then []
else if variant_id = fuel_succ_id then [ mk_fuel_ty ]
else raise (Failure "Unreachable: improper variant id for fuel type")
- | Array | Slice | Str | RawPtr _ ->
+ | TArray | TSlice | TStr | TRawPtr _ ->
(* Array: when not symbolic values (for instance, because of aggregates),
the array expressions are introduced as struct updates *)
raise (Failure "Attempting to access the fields of an opaque type"))
@@ -208,7 +208,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
assert (adt_id = supd.struct_id);
(* The id can only be: a custom type decl or an array *)
match adt_id with
- | AdtId _ ->
+ | TAdtId _ ->
let variant_id = None in
let expected_field_tys =
get_adt_field_types ctx.type_decls adt_id variant_id adt_generics
@@ -219,7 +219,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
assert (expected_field_ty = fe.ty);
check_texpression ctx fe)
supd.updates
- | TAssumed Array ->
+ | TAssumed TArray ->
let expected_field_ty =
Collections.List.to_cons_nil adt_generics.types
in
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 49c8dd70..4cc7ef91 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -59,7 +59,7 @@ module FunLoopIdSet = Collections.MakeSet (FunLoopIdOrderedType)
let dest_arrow_ty (ty : ty) : ty * ty =
match ty with
- | Arrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
+ | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
| _ -> raise (Failure "Unreachable")
let compute_literal_type (cv : literal) : literal_type =
@@ -110,7 +110,7 @@ let ty_substitute (subst : subst) (ty : ty) : ty =
let obj =
object
inherit [_] map_ty
- method! visit_TypeVar _ var_id = subst.ty_subst var_id
+ method! visit_TVar _ var_id = subst.ty_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
@@ -249,12 +249,12 @@ let remove_meta (e : texpression) : texpression =
in
obj#visit_texpression () e
-let mk_arrow (ty0 : ty) (ty1 : ty) : ty = Arrow (ty0, ty1)
+let mk_arrow (ty0 : ty) (ty1 : ty) : ty = TArrow (ty0, ty1)
(** Construct a type as a list of arrows: ty1 -> ... tyn *)
let mk_arrows (inputs : ty list) (output : ty) =
let rec aux (tys : ty list) : ty =
- match tys with [] -> output | ty :: tys' -> Arrow (ty, aux tys')
+ match tys with [] -> output | ty :: tys' -> TArrow (ty, aux tys')
in
aux inputs
@@ -305,7 +305,7 @@ let destruct_apps (e : texpression) : texpression * texpression list =
(** Make an [App (app, arg)] expression *)
let mk_app (app : texpression) (arg : texpression) : texpression =
match app.ty with
- | Arrow (ty0, ty1) ->
+ | TArrow (ty0, ty1) ->
(* Sanity check *)
assert (ty0 = arg.ty);
let e = App (app, arg) in
@@ -340,7 +340,7 @@ let opt_destruct_function_call (e : texpression) :
let opt_destruct_result (ty : ty) : ty option =
match ty with
- | TAdt (TAssumed Result, generics) ->
+ | TAdt (TAssumed TResult, generics) ->
assert (generics.const_generics = []);
assert (generics.trait_refs = []);
Some (Collections.List.to_cons_nil generics.types)
@@ -350,14 +350,14 @@ let destruct_result (ty : ty) : ty = Option.get (opt_destruct_result ty)
let opt_destruct_tuple (ty : ty) : ty list option =
match ty with
- | TAdt (Tuple, generics) ->
+ | TAdt (TTuple, generics) ->
assert (generics.const_generics = []);
assert (generics.trait_refs = []);
Some generics.types
| _ -> None
let mk_abs (x : typed_pattern) (e : texpression) : texpression =
- let ty = Arrow (x.ty, e.ty) in
+ let ty = TArrow (x.ty, e.ty) in
let e = Abs (x, e) in
{ e; ty }
@@ -370,12 +370,12 @@ let rec destruct_abs_list (e : texpression) : typed_pattern list * texpression =
let destruct_arrow (ty : ty) : ty * ty =
match ty with
- | Arrow (ty0, ty1) -> (ty0, ty1)
+ | TArrow (ty0, ty1) -> (ty0, ty1)
| _ -> raise (Failure "Not an arrow type")
let rec destruct_arrows (ty : ty) : ty list * ty =
match ty with
- | Arrow (ty0, ty1) ->
+ | TArrow (ty0, ty1) ->
let tys, out_ty = destruct_arrows ty1 in
(ty0 :: tys, out_ty)
| _ -> ([], ty)
@@ -427,13 +427,13 @@ let mk_switch (scrut : texpression) (sb : switch_body) : texpression =
let mk_simpl_tuple_ty (tys : ty list) : ty =
match tys with
| [ ty ] -> ty
- | _ -> TAdt (Tuple, mk_generic_args_from_types tys)
+ | _ -> TAdt (TTuple, mk_generic_args_from_types tys)
let mk_bool_ty : ty = TLiteral TBool
-let mk_unit_ty : ty = TAdt (Tuple, empty_generic_args)
+let mk_unit_ty : ty = TAdt (TTuple, empty_generic_args)
let mk_unit_rvalue : texpression =
- let id = AdtCons { adt_id = Tuple; variant_id = None } in
+ let id = AdtCons { adt_id = TTuple; variant_id = None } in
let qualif = { id; generics = empty_generic_args } in
let e = Qualif qualif in
let ty = mk_unit_ty in
@@ -474,7 +474,7 @@ let mk_simpl_tuple_pattern (vl : typed_pattern list) : typed_pattern =
| [ v ] -> v
| _ ->
let tys = List.map (fun (v : typed_pattern) -> v.ty) vl in
- let ty = TAdt (Tuple, mk_generic_args_from_types tys) in
+ let ty = TAdt (TTuple, mk_generic_args_from_types tys) in
let value = PatAdt { variant_id = None; field_values = vl } in
{ value; ty }
@@ -485,10 +485,10 @@ let mk_simpl_tuple_texpression (vl : texpression list) : texpression =
| _ ->
(* Compute the types of the fields, and the type of the tuple constructor *)
let tys = List.map (fun (v : texpression) -> v.ty) vl in
- let ty = TAdt (Tuple, mk_generic_args_from_types tys) in
+ let ty = TAdt (TTuple, mk_generic_args_from_types tys) in
let ty = mk_arrows tys ty in
(* Construct the tuple constructor qualifier *)
- let id = AdtCons { adt_id = Tuple; variant_id = None } in
+ let id = AdtCons { adt_id = TTuple; variant_id = None } in
let qualif = { id; generics = mk_generic_args_from_types tys } in
(* Put everything together *)
let cons = { e = Qualif qualif; ty } in
@@ -507,17 +507,17 @@ let ty_as_integer (t : ty) : T.integer_type =
let ty_as_literal (t : ty) : T.literal_type =
match t with TLiteral ty -> ty | _ -> raise (Failure "Unreachable")
-let mk_state_ty : ty = TAdt (TAssumed State, empty_generic_args)
+let mk_state_ty : ty = TAdt (TAssumed TState, empty_generic_args)
let mk_result_ty (ty : ty) : ty =
- TAdt (TAssumed Result, mk_generic_args_from_types [ ty ])
+ TAdt (TAssumed TResult, mk_generic_args_from_types [ ty ])
-let mk_error_ty : ty = TAdt (TAssumed Error, empty_generic_args)
-let mk_fuel_ty : ty = TAdt (TAssumed Fuel, empty_generic_args)
+let mk_error_ty : ty = TAdt (TAssumed TError, empty_generic_args)
+let mk_fuel_ty : ty = TAdt (TAssumed TFuel, empty_generic_args)
let mk_error (error : VariantId.id) : texpression =
let ty = mk_error_ty in
- let id = AdtCons { adt_id = TAssumed Error; variant_id = Some error } in
+ let id = AdtCons { adt_id = TAssumed TError; variant_id = Some error } in
let qualif = { id; generics = empty_generic_args } in
let e = Qualif qualif in
{ e; ty }
@@ -525,16 +525,16 @@ let mk_error (error : VariantId.id) : texpression =
let unwrap_result_ty (ty : ty) : ty =
match ty with
| TAdt
- (TAssumed Result, { types = [ ty ]; const_generics = []; trait_refs = [] })
- ->
+ ( TAssumed TResult,
+ { types = [ ty ]; const_generics = []; trait_refs = [] } ) ->
ty
| _ -> raise (Failure "not a result type")
let mk_result_fail_texpression (error : texpression) (ty : ty) : texpression =
let type_args = [ ty ] in
- let ty = TAdt (TAssumed Result, mk_generic_args_from_types type_args) in
+ let ty = TAdt (TAssumed TResult, mk_generic_args_from_types type_args) in
let id =
- AdtCons { adt_id = TAssumed Result; variant_id = Some result_fail_id }
+ AdtCons { adt_id = TAssumed TResult; variant_id = Some result_fail_id }
in
let qualif = { id; generics = mk_generic_args_from_types type_args } in
let cons_e = Qualif qualif in
@@ -549,9 +549,9 @@ let mk_result_fail_texpression_with_error_id (error : VariantId.id) (ty : ty) :
let mk_result_return_texpression (v : texpression) : texpression =
let type_args = [ v.ty ] in
- let ty = TAdt (TAssumed Result, mk_generic_args_from_types type_args) in
+ let ty = TAdt (TAssumed TResult, mk_generic_args_from_types type_args) in
let id =
- AdtCons { adt_id = TAssumed Result; variant_id = Some result_return_id }
+ AdtCons { adt_id = TAssumed TResult; variant_id = Some result_return_id }
in
let qualif = { id; generics = mk_generic_args_from_types type_args } in
let cons_e = Qualif qualif in
@@ -562,7 +562,7 @@ let mk_result_return_texpression (v : texpression) : texpression =
(** Create a [Fail err] pattern which captures the error *)
let mk_result_fail_pattern (error_pat : pattern) (ty : ty) : typed_pattern =
let error_pat : typed_pattern = { value = error_pat; ty = mk_error_ty } in
- let ty = TAdt (TAssumed Result, mk_generic_args_from_types [ ty ]) in
+ let ty = TAdt (TAssumed TResult, mk_generic_args_from_types [ ty ]) in
let value =
PatAdt { variant_id = Some result_fail_id; field_values = [ error_pat ] }
in
@@ -574,7 +574,7 @@ let mk_result_fail_pattern_ignore_error (ty : ty) : typed_pattern =
mk_result_fail_pattern error_pat ty
let mk_result_return_pattern (v : typed_pattern) : typed_pattern =
- let ty = TAdt (TAssumed Result, mk_generic_args_from_types [ v.ty ]) in
+ let ty = TAdt (TAssumed TResult, mk_generic_args_from_types [ v.ty ]) in
let value =
PatAdt { variant_id = Some result_return_id; field_values = [ v ] }
in
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 490574a2..166c237a 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -23,7 +23,7 @@ let st_substitute_visitor (subst : subst) =
object
inherit [_] A.map_statement
method! visit_region _ r = subst.r_subst r
- method! visit_TypeVar _ id = subst.ty_subst id
+ method! visit_TVar _ id = subst.ty_subst id
method! visit_type_var_id _ _ =
(* We should never get here because we reimplemented [visit_TypeVar] *)
@@ -67,7 +67,7 @@ let generic_args_substitute (subst : subst) (g : T.generic_args) :
let erase_regions_subst : subst =
{
r_subst = (fun _ -> T.RErased);
- ty_subst = (fun vid -> T.TypeVar vid);
+ ty_subst = (fun vid -> T.TVar vid);
cg_subst = (fun id -> T.CGVar id);
tr_subst = (fun id -> T.Clause id);
tr_self = T.Self;
@@ -288,10 +288,10 @@ let ctx_adt_value_get_instantiated_field_types (ctx : C.eval_ctx)
(adt : V.adt_value) (id : T.type_id) (generics : T.generic_args) : T.ty list
=
match id with
- | T.AdtId id ->
+ | T.TAdtId id ->
(* Retrieve the types of the fields *)
ctx_adt_get_instantiated_field_types ctx id adt.V.variant_id generics
- | T.Tuple ->
+ | T.TTuple ->
assert (generics.regions = []);
generics.types
| T.TAssumed aty -> (
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 91edbf04..60020d9a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -397,8 +397,8 @@ let rec translate_sty (ty : T.ty) : ty =
| T.TAdt (type_id, generics) -> (
let generics = translate_sgeneric_args generics in
match type_id with
- | T.AdtId adt_id -> TAdt (AdtId adt_id, generics)
- | T.Tuple ->
+ | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics)
+ | T.TTuple ->
assert (generics.const_generics = []);
mk_simpl_tuple_ty generics.types
| T.TAssumed aty -> (
@@ -412,23 +412,23 @@ let rec translate_sty (ty : T.ty) : ty =
(Failure
"Box/vec/option type with incorrect number of arguments")
)
- | T.TArray -> TAdt (TAssumed Array, generics)
- | T.TSlice -> TAdt (TAssumed Slice, generics)
- | T.TStr -> TAdt (TAssumed Str, generics)))
- | TypeVar vid -> TypeVar vid
+ | T.TArray -> TAdt (TAssumed TArray, generics)
+ | T.TSlice -> TAdt (TAssumed TSlice, generics)
+ | T.TStr -> TAdt (TAssumed TStr, generics)))
+ | TVar vid -> TVar vid
| TLiteral ty -> TLiteral ty
- | Never -> raise (Failure "Unreachable")
- | Ref (_, rty, _) -> translate rty
- | RawPtr (ty, rkind) ->
+ | TNever -> raise (Failure "Unreachable")
+ | TRef (_, rty, _) -> translate rty
+ | TRawPtr (ty, rkind) ->
let mut = match rkind with Mut -> Mut | Shared -> Const in
let ty = translate ty in
let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
- TAdt (TAssumed (RawPtr mut), generics)
- | TraitType (trait_ref, generics, type_name) ->
+ TAdt (TAssumed (TRawPtr mut), generics)
+ | TTraitType (trait_ref, generics, type_name) ->
let trait_ref = translate_strait_ref trait_ref in
let generics = translate_sgeneric_args generics in
- TraitType (trait_ref, generics, type_name)
- | Arrow _ -> raise (Failure "TODO")
+ TTraitType (trait_ref, generics, type_name)
+ | TArrow _ -> raise (Failure "TODO")
and translate_sgeneric_args (generics : T.generic_args) : generic_args =
translate_generic_args translate_sty generics
@@ -506,20 +506,20 @@ let translate_type_decl (def : T.type_decl) : type_decl =
let translate_type_id (id : T.type_id) : type_id =
match id with
- | AdtId adt_id -> AdtId adt_id
- | T.TAssumed aty ->
+ | TAdtId adt_id -> TAdtId adt_id
+ | TAssumed aty ->
let aty =
match aty with
- | T.TArray -> Array
- | T.TSlice -> Slice
- | T.TStr -> Str
+ | T.TArray -> TArray
+ | T.TSlice -> TSlice
+ | T.TStr -> TStr
| T.TBox ->
(* Boxes have to be eliminated: this type id shouldn't
be translated *)
raise (Failure "Unreachable")
in
TAssumed aty
- | T.Tuple -> Tuple
+ | TTuple -> TTuple
(** Translate a type, seen as an input/output of a forward function
(preserve all borrows, etc.).
@@ -536,14 +536,14 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
let t_generics = translate_fwd_generic_args type_infos generics in
(* Eliminate boxes and simplify tuples *)
match type_id with
- | AdtId _ | T.TAssumed (T.TArray | T.TSlice | T.TStr) ->
+ | TAdtId _ | TAssumed (TArray | TSlice | TStr) ->
let type_id = translate_type_id type_id in
TAdt (type_id, t_generics)
- | Tuple ->
+ | TTuple ->
(* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the
identity *)
mk_simpl_tuple_ty t_generics.types
- | T.TAssumed T.TBox -> (
+ | TAssumed TBox -> (
(* We eliminate boxes *)
(* No general parametricity for now *)
assert (
@@ -558,20 +558,20 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
(Failure
"Unreachable: box/vec/option receives exactly one type \
parameter")))
- | TypeVar vid -> TypeVar vid
- | Never -> raise (Failure "Unreachable")
+ | TVar vid -> TVar vid
+ | TNever -> raise (Failure "Unreachable")
| TLiteral lty -> TLiteral lty
- | Ref (_, rty, _) -> translate rty
- | RawPtr (ty, rkind) ->
+ | TRef (_, rty, _) -> translate rty
+ | TRawPtr (ty, rkind) ->
let mut = match rkind with Mut -> Mut | Shared -> Const in
let ty = translate ty in
let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
- TAdt (TAssumed (RawPtr mut), generics)
- | TraitType (trait_ref, generics, type_name) ->
+ TAdt (TAssumed (TRawPtr mut), generics)
+ | TTraitType (trait_ref, generics, type_name) ->
let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
let generics = translate_fwd_generic_args type_infos generics in
- TraitType (trait_ref, generics, type_name)
- | Arrow _ -> raise (Failure "TODO")
+ TTraitType (trait_ref, generics, type_name)
+ | TArrow _ -> raise (Failure "TODO")
and translate_fwd_generic_args (type_infos : TA.type_infos)
(generics : T.generic_args) : generic_args =
@@ -611,7 +611,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
match ty with
| T.TAdt (type_id, generics) -> (
match type_id with
- | T.AdtId _ | TAssumed (T.TArray | T.TSlice | T.TStr) ->
+ | TAdtId _ | TAssumed (TArray | TSlice | TStr) ->
let type_id = translate_type_id type_id in
if inside_mut then
(* We do not want to filter anything, so we translate the generics
@@ -630,7 +630,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
let generics = translate_fwd_generic_args type_infos generics in
Some (TAdt (type_id, generics))
else None
- | TAssumed T.TBox -> (
+ | TAssumed TBox -> (
(* Don't accept ADTs (which are not tuples) with borrows for now *)
assert (not (TypesUtils.ty_has_borrows type_infos ty));
(* Eliminate the box *)
@@ -640,7 +640,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
raise
(Failure "Unreachable: boxes receive exactly one type parameter")
)
- | T.Tuple -> (
+ | TTuple -> (
(* Tuples can contain borrows (which we eliminate) *)
let tys_t = List.filter_map translate generics.types in
match tys_t with
@@ -649,10 +649,10 @@ let rec translate_back_ty (type_infos : TA.type_infos)
(* Note that if there is exactly one type, [mk_simpl_tuple_ty]
* is the identity *)
Some (mk_simpl_tuple_ty tys_t)))
- | TypeVar vid -> wrap (TypeVar vid)
- | Never -> raise (Failure "Unreachable")
+ | TVar vid -> wrap (TVar vid)
+ | TNever -> raise (Failure "Unreachable")
| TLiteral lty -> wrap (TLiteral lty)
- | Ref (r, rty, rkind) -> (
+ | TRef (r, rty, rkind) -> (
match rkind with
| T.Shared ->
(* Ignore shared references, unless we are below a mutable borrow *)
@@ -663,17 +663,17 @@ let rec translate_back_ty (type_infos : TA.type_infos)
if keep_region r then
translate_back_ty type_infos keep_region inside_mut rty
else None)
- | RawPtr _ ->
+ | TRawPtr _ ->
(* TODO: not sure what to do here *)
None
- | TraitType (trait_ref, generics, type_name) ->
+ | TTraitType (trait_ref, generics, type_name) ->
assert (generics.regions = []);
(* Translate the trait ref and the generics as "forward" generics -
we do not want to filter any type *)
let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
let generics = translate_fwd_generic_args type_infos generics in
- Some (TraitType (trait_ref, generics, type_name))
- | Arrow _ -> raise (Failure "TODO")
+ Some (TTraitType (trait_ref, generics, type_name))
+ | TArrow _ -> raise (Failure "TODO")
(** Simply calls [translate_back_ty] *)
let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
@@ -1155,7 +1155,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
let field_values = List.map translate av.field_values in
(* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
match v.ty with
- | T.TAdt (T.Tuple, _) ->
+ | TAdt (TTuple, _) ->
assert (variant_id = None);
mk_simpl_tuple_texpression field_values
| _ ->
@@ -1233,10 +1233,10 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
(* For now, only tuples can contain borrows *)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
- | T.AdtId _ | T.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
+ | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
assert (field_values = []);
None
- | T.Tuple ->
+ | TTuple ->
(* Return *)
if field_values = [] then None
else
@@ -1378,10 +1378,10 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
* vector value upon visiting the "abstraction borrow" node *)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
- | T.AdtId _ | T.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
+ | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
assert (field_values = []);
(ctx, None)
- | T.Tuple ->
+ | TTuple ->
(* Return *)
let variant_id = adt_v.variant_id in
assert (variant_id = None);
@@ -2386,7 +2386,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
let branch = translate_expression branch ctx in
match type_id with
- | T.AdtId adt_id ->
+ | TAdtId adt_id ->
(* Detect if this is an enumeration or not *)
let tdef = bs_ctx_lookup_llbc_type_decl adt_id ctx in
let is_enum = TypesUtils.type_decl_is_enum tdef in
@@ -2433,14 +2433,14 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
let field_proj = gen_field_proj fid var in
mk_let monadic (mk_typed_pattern_from_var var None) field_proj e)
id_var_pairs branch
- | T.Tuple ->
+ | TTuple ->
let vars = List.map (fun x -> mk_typed_pattern_from_var x None) vars in
let monadic = false in
mk_let monadic
(mk_simpl_tuple_pattern vars)
(mk_opt_mplace_texpression scrutinee_mplace scrutinee)
branch
- | T.TAssumed T.TBox ->
+ | TAssumed TBox ->
(* There should be exactly one variable *)
let var =
match vars with [ v ] -> v | _ -> raise (Failure "Unreachable")
@@ -2452,7 +2452,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
(mk_typed_pattern_from_var var None)
(mk_opt_mplace_texpression scrutinee_mplace scrutinee)
branch
- | T.TAssumed (T.TArray | T.TSlice | T.TStr) ->
+ | TAssumed (TArray | TSlice | TStr) ->
(* We can't expand those values: we can access the fields only
* through the functions provided by the API (note that we don't
* know how to expand values like vectors or arrays, because they have a variable number
@@ -2484,7 +2484,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
let values = List.map (typed_value_to_texpression ctx ectx) values in
let values = FieldId.mapi (fun fid v -> (fid, v)) values in
let su : struct_update =
- { struct_id = TAssumed Array; init = None; updates = values }
+ { struct_id = TAssumed TArray; init = None; updates = values }
in
{ e = StructUpdate su; ty = var.ty }
| VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty }
@@ -2735,9 +2735,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
call to the loop forward function) *)
let generics =
let { types; const_generics; trait_clauses } = ctx.sg.generics in
- let types =
- List.map (fun (ty : T.type_var) -> TypeVar ty.T.index) types
- in
+ let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in
let const_generics =
List.map
(fun (cg : T.const_generic_var) -> T.CGVar cg.T.index)
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index edd67749..ddb9d681 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -80,14 +80,14 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
ls
in
ExpandAdt exp
- | T.Ref (_, _, _) -> (
+ | T.TRef (_, _, _) -> (
(* Reference expansion: there should be one branch *)
match ls with
| [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
| _ -> raise (Failure "Ill-formed borrow expansion"))
- | T.TypeVar _
+ | T.TVar _
| T.TLiteral TChar
- | Never | T.TraitType _ | T.Arrow _ | T.RawPtr _ ->
+ | TNever | T.TTraitType _ | T.TArrow _ | T.TRawPtr _ ->
raise (Failure "Ill-formed symbolic expansion")
in
Some (Expansion (place, sv, expansion))
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 6318c624..eddc1e42 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -121,8 +121,8 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
let rec analyze (expl_info : expl_info) (ty_info : partial_type_info)
(ty : ty) : partial_type_info =
match ty with
- | TLiteral _ | Never | TraitType _ -> ty_info
- | TypeVar var_id -> (
+ | TLiteral _ | TNever | TTraitType _ -> ty_info
+ | TVar var_id -> (
(* Update the information for the proper parameter, if necessary *)
match ty_info.param_infos with
| None -> ty_info
@@ -144,7 +144,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
in
let param_infos = Some param_infos in
{ ty_info with param_infos })
- | Ref (r, rty, rkind) ->
+ | TRef (r, rty, rkind) ->
(* Update the type info *)
let contains_static = r_is_static r in
let contains_borrow = true in
@@ -168,15 +168,15 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
in
(* Continue exploring *)
analyze expl_info ty_info rty
- | RawPtr (rty, _) ->
+ | TRawPtr (rty, _) ->
(* TODO: not sure what to do here *)
analyze expl_info ty_info rty
- | TAdt ((Tuple | TAssumed (TBox | TSlice | TArray | TStr)), generics) ->
+ | TAdt ((TTuple | TAssumed (TBox | TSlice | TArray | TStr)), generics) ->
(* Nothing to update: just explore the type parameters *)
List.fold_left
(fun ty_info ty -> analyze expl_info ty_info ty)
ty_info generics.types
- | TAdt (AdtId adt_id, generics) ->
+ | TAdt (TAdtId adt_id, generics) ->
(* Lookup the information for this type definition *)
let adt_info = TypeDeclId.Map.find adt_id infos in
(* Update the type info with the information from the adt *)
@@ -233,7 +233,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
in
(* Return *)
ty_info
- | Arrow (inputs, output) ->
+ | TArrow (inputs, output) ->
(* Just dive into the arrow *)
let ty_info =
List.fold_left