diff options
Diffstat (limited to '')
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 |