From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 19:28:56 +0100 Subject: Remove the 'r type variable from the ty type definition --- compiler/PureMicroPasses.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index f3e6cbe2..d62a028e 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -791,7 +791,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) let id0 = match id0 with | FunId fun_id -> fun_id - | TraitMethod (_, _, fun_decl_id) -> Regular fun_decl_id + | TraitMethod (_, _, fun_decl_id) -> FRegular fun_decl_id in LlbcAstUtils.lookup_fun_sig id0 ctx.fun_ctx.fun_decls in @@ -1527,7 +1527,7 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = * could have: [box_new f x]) * *) match fun_id with - | Fun (FromLlbc (FunId (Assumed aid), _lp_id, rg_id)) -> ( + | Fun (FromLlbc (FunId (FAssumed aid), _lp_id, rg_id)) -> ( match (aid, rg_id) with | BoxNew, _ -> assert (rg_id = None); @@ -1541,7 +1541,7 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = | ArrayRepeat | SliceLen ), _ ) -> super#visit_texpression env e) - | Fun (FromLlbc (FunId (Regular fid), _lp_id, rg_id)) -> ( + | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> ( (* Lookup the function name *) let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in match @@ -2050,7 +2050,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) : let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in assert (Option.is_some decl.loop_id); - let fun_id = (E.Regular decl.def_id, decl.loop_id) in + let fun_id = (E.FRegular decl.def_id, decl.loop_id) in let set_used vid = used := List.map (fun (vid', b) -> (vid', b || vid = vid')) !used @@ -2134,7 +2134,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) : (* We then apply the filtering to all the function definitions at once *) let filter_in_one (decl : fun_decl) : fun_decl = (* Filter the function signature *) - let fun_id = (E.Regular decl.def_id, decl.loop_id) in + let fun_id = (E.FRegular decl.def_id, decl.loop_id) in let decl = match FunLoopIdMap.find_opt fun_id !used_map with | None -> (* Nothing to filter *) decl -- cgit v1.3.1 From 6ef68fa9ffd4caec09677ee2800a778080d6da34 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 20:04:11 +0100 Subject: Prefix variants related to types with "T" --- compiler/AssociatedTypes.ml | 22 ++--- compiler/Assumed.ml | 12 +-- compiler/Extract.ml | 14 ++-- compiler/ExtractBase.ml | 27 ++++--- compiler/ExtractTypes.ml | 142 ++++++++++++++++----------------- compiler/Interpreter.ml | 2 +- compiler/InterpreterBorrows.ml | 4 +- compiler/InterpreterBorrowsCore.ml | 10 +-- compiler/InterpreterExpansion.ml | 16 ++-- compiler/InterpreterExpressions.ml | 16 ++-- compiler/InterpreterLoopsFixedPoint.ml | 2 +- compiler/InterpreterLoopsMatchCtxs.ml | 10 +-- compiler/InterpreterPaths.ml | 12 +-- compiler/InterpreterProjectors.ml | 8 +- compiler/InterpreterStatements.ml | 8 +- compiler/Invariants.ml | 12 +-- compiler/PrePasses.ml | 2 +- compiler/Print.ml | 8 +- compiler/PrintPure.ml | 70 ++++++++-------- compiler/Pure.ml | 24 +++--- compiler/PureMicroPasses.ml | 12 +-- compiler/PureTypeCheck.ml | 18 ++--- compiler/PureUtils.ml | 58 +++++++------- compiler/Substitute.ml | 8 +- compiler/SymbolicToPure.ml | 104 ++++++++++++------------ compiler/SynthesizeSymbolic.ml | 6 +- compiler/TypesAnalysis.ml | 14 ++-- 27 files changed, 320 insertions(+), 321 deletions(-) (limited to 'compiler/PureMicroPasses.ml') 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 *) 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 *) - 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 *) - 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 -- cgit v1.3.1 From 6c88d30031255c0ac612b67bb5b3c20c2f07e563 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 13 Nov 2023 13:27:02 +0100 Subject: Add RegionsHierarchy.ml --- compiler/AssociatedTypes.ml | 5 +- compiler/Assumed.ml | 18 +-- compiler/Contexts.ml | 2 + compiler/ExtractBase.ml | 8 +- compiler/Interpreter.ml | 28 +++-- compiler/InterpreterStatements.ml | 2 +- compiler/InterpreterUtils.ml | 9 +- compiler/LlbcAstUtils.ml | 13 ++ compiler/PureMicroPasses.ml | 9 +- compiler/RegionsHierarchy.ml | 243 ++++++++++++++++++++++++++++++++++++++ compiler/ReorderDecls.ml | 97 +-------------- compiler/SCC.ml | 121 +++++++++++++++++-- compiler/Substitute.ml | 12 +- compiler/SymbolicToPure.ml | 25 ++-- compiler/Translate.ml | 7 +- compiler/dune | 1 + 16 files changed, 453 insertions(+), 147 deletions(-) create mode 100644 compiler/RegionsHierarchy.ml (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index d5c9596e..27e08495 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -521,10 +521,11 @@ let ctx_subst_norm_signature (ctx : C.eval_ctx) (ty_subst : T.TypeVarId.id -> T.ty) (cg_subst : T.ConstGenericVarId.id -> T.const_generic) (tr_subst : T.TraitClauseId.id -> T.trait_instance_id) - (tr_self : T.trait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig = + (tr_self : T.trait_instance_id) (sg : A.fun_sig) + (regions_hierarchy : T.region_groups) : A.inst_fun_sig = let sg = Subst.substitute_signature asubst r_subst ty_subst cg_subst tr_subst tr_self - sg + sg regions_hierarchy in let { A.regions_hierarchy; inputs; output; trait_type_constraints } = sg in let inputs = List.map (ctx_normalize_ty ctx) inputs in diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index cf81502c..aa0cfccf 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -79,7 +79,7 @@ module Sig = struct let mk_slice_ty (ty : T.ty) : T.ty = TAdt (TAssumed TSlice, mk_generic_args [] [ ty ] []) - let mk_sig generics regions_hierarchy inputs output : A.fun_sig = + let mk_sig generics inputs output : A.fun_sig = let preds : T.predicates = { regions_outlive = []; types_outlive = []; trait_type_constraints = [] } in @@ -88,7 +88,6 @@ module Sig = struct generics; preds; parent_params_info = None; - regions_hierarchy; inputs; output; } @@ -96,18 +95,16 @@ module Sig = struct (** [fn(T) -> Box] *) let box_new_sig : A.fun_sig = let generics = mk_generic_params [] [ type_param_0 ] [] (* *) in - let regions_hierarchy = [] in let inputs = [ tvar_0 (* T *) ] in let output = mk_box_ty tvar_0 (* Box *) in - mk_sig generics regions_hierarchy inputs output + mk_sig generics inputs output (** [fn(Box) -> ()] *) let box_free_sig : A.fun_sig = let generics = mk_generic_params [] [ type_param_0 ] [] (* *) in - let regions_hierarchy = [] in let inputs = [ mk_box_ty tvar_0 (* Box *) ] in let output = mk_unit_ty (* () *) in - mk_sig generics regions_hierarchy inputs output + mk_sig generics inputs output (** Array/slice functions *) @@ -129,7 +126,6 @@ module Sig = struct let generics = mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *) in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in let inputs = [ mk_ref_ty rvar_0 @@ -145,7 +141,7 @@ module Sig = struct (output_ty type_param_0.index) is_mut (* &'a (mut) output_ty *) in - mk_sig generics regions_hierarchy inputs output + mk_sig generics inputs output let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : A.fun_sig = (* Array *) @@ -176,13 +172,12 @@ module Sig = struct (* *) mk_generic_params [] [ type_param_0 ] [ cg_param_0 ] in - let regions_hierarchy = [] (* <> *) in let inputs = [ tvar_0 (* T *) ] in let output = (* [T; N] *) mk_array_ty tvar_0 cgvar_0 in - mk_sig generics regions_hierarchy inputs output + mk_sig generics inputs output (** Helper: [fn(&'a [T]) -> usize] @@ -191,12 +186,11 @@ module Sig = struct let generics = mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in let inputs = [ mk_ref_ty rvar_0 (mk_slice_ty tvar_0) false (* &'a [T] *) ] in let output = mk_usize_ty (* usize *) in - mk_sig generics regions_hierarchy inputs output + mk_sig generics inputs output end type raw_assumed_fun_info = diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index 9a20a6cc..12927aab 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -2,6 +2,7 @@ open Types open Expressions open Values open LlbcAst +open LlbcAstUtils module V = Values open ValuesUtils open Identifiers @@ -190,6 +191,7 @@ type type_context = { type fun_context = { fun_decls : fun_decl FunDeclId.Map.t; fun_infos : FunsAnalysis.fun_info FunDeclId.Map.t; + regions_hierarchies : T.region_groups FunIdMap.t; } [@@deriving show] diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index d5eac6f4..4ce1e9f1 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1188,14 +1188,18 @@ let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl) let def_id = def.def_id in let llbc_def = A.FunDeclId.Map.find def_id ctx.trans_ctx.fun_ctx.fun_decls in let sg = llbc_def.signature in - let num_rgs = List.length sg.regions_hierarchy in + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FRegular def_id) + ctx.trans_ctx.fun_ctx.regions_hierarchies + in + let num_rgs = List.length regions_hierarchy in let { keep_fwd; fwd = _; backs } = trans_group in let num_backs = List.length backs in let rg_info = match def.back_id with | None -> None | Some rg_id -> - let rg = T.RegionGroupId.nth sg.regions_hierarchy rg_id in + let rg = T.RegionGroupId.nth regions_hierarchy rg_id in let region_names = List.map (fun rid -> (T.RegionId.nth sg.generics.regions rid).name) diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 395c0c80..69c9af62 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -29,7 +29,10 @@ let compute_contexts (m : A.crate) : C.decls_ctx = let fun_infos = FunsAnalysis.analyze_module m fun_decls global_decls !Config.use_state in - let fun_ctx = { C.fun_decls; fun_infos } in + let regions_hierarchies = + RegionsHierarchy.compute_regions_hierarchies type_decls fun_decls + in + let fun_ctx = { C.fun_decls; fun_infos; regions_hierarchies } in let global_ctx = { C.global_decls } in let trait_decls_ctx = { C.trait_decls } in let trait_impls_ctx = { C.trait_impls } in @@ -124,8 +127,8 @@ let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (sg : A.fun_sig) List.fold_left_map (fun tr_map (c : T.trait_clause) -> let subst = mk_subst tr_map in - let { T.trait_id = trait_decl_id; generics; _ } = c in - let generics = Subst.generic_args_substitute subst generics in + let { T.trait_id = trait_decl_id; clause_generics; _ } = c in + let generics = Subst.generic_args_substitute subst clause_generics in let trait_decl_ref = { T.trait_decl_id; decl_generics = generics } in (* Note that because we directly refer to the clause, we give it empty generics *) @@ -183,8 +186,11 @@ let initialize_symbolic_context_for_fun (ctx : C.decls_ctx) (fdef : A.fun_decl) * *) let sg = fdef.signature in (* Create the context *) + let regions_hierarchy = + FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies + in let region_groups = - List.map (fun (g : T.region_group) -> g.id) sg.regions_hierarchy + List.map (fun (g : T.region_group) -> g.id) regions_hierarchy in let ctx = initialize_eval_context ctx region_groups sg.generics.types @@ -269,7 +275,6 @@ let evaluate_function_symbolic_synthesize_backward_from_return * the return type. Note that it is important to re-generate * an instantiation of the signature, so that we use fresh * region ids for the return abstractions. *) - let sg = fdef.signature in let _, ret_inst_sg = symbolic_instantiate_fun_sig ctx fdef.signature fdef.kind in @@ -282,7 +287,10 @@ let evaluate_function_symbolic_synthesize_backward_from_return * will end - this will allow us to, first, mark the other return * regions as non-endable, and, second, end those parent regions in * proper order. *) - let parent_rgs = list_ancestor_region_groups sg back_id in + let regions_hierarchy = + FunIdMap.find (FRegular fdef.def_id) ctx.fun_context.regions_hierarchies + in + let parent_rgs = list_ancestor_region_groups regions_hierarchy back_id in let parent_input_abs_ids = T.RegionGroupId.mapi (fun rg_id rg -> @@ -455,6 +463,10 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : C.decls_ctx) (* Create the evaluation context *) let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun ctx fdef in + let regions_hierarchy = + FunIdMap.find (FRegular fdef.def_id) ctx.fun_context.regions_hierarchies + in + (* Create the continuation to finish the evaluation *) let config = C.mk_config C.SymbolicMode in let cf_finish res ctx = @@ -511,7 +523,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : C.decls_ctx) let back_el = T.RegionGroupId.mapi (fun gid _ -> (gid, finish_back_eval gid)) - fdef.signature.regions_hierarchy + regions_hierarchy in let back_el = T.RegionGroupId.Map.of_list back_el in (* Put everything together *) @@ -555,7 +567,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : C.decls_ctx) let back_el = T.RegionGroupId.mapi (fun gid _ -> (gid, finish_back_eval gid)) - fdef.signature.regions_hierarchy + regions_hierarchy in let back_el = T.RegionGroupId.Map.of_list back_el in (* Put everything together *) diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index cbc09c29..3627490d 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1434,7 +1434,7 @@ and eval_assumed_function_call_symbolic (config : C.config) let inst_sig = match fid with | BoxFree -> - (* should have been treated above *) + (* Should have been treated above *) raise (Failure "Unreachable") | _ -> (* There shouldn't be any reference to Self *) diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 60747b2a..5e2746c5 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -474,6 +474,11 @@ let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args) (* Erase the regions in the generics we use for the instantiation *) let generics = Subst.generic_args_erase_regions generics in let tr_self = Subst.trait_instance_id_erase_regions tr_self in + (* Compute the regions hierarchy *) + let regions_hierarchy = + RegionsHierarchy.compute_regions_hierarchy_for_sig + ctx.type_context.type_decls sg + in (* Generate fresh abstraction ids and create a substitution from region * group ids to abstraction ids *) let rg_abs_ids_bindings = @@ -481,7 +486,7 @@ let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args) (fun rg -> let abs_id = C.fresh_abstraction_id () in (rg.T.id, abs_id)) - sg.regions_hierarchy + regions_hierarchy in let asubst_map : V.AbstractionId.id T.RegionGroupId.Map.t = List.fold_left @@ -512,7 +517,7 @@ let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.generic_args) (* Substitute the signature *) let inst_sig = AssociatedTypes.ctx_subst_norm_signature ctx asubst rsubst tsubst cgsubst - tr_subst tr_self sg + tr_subst tr_self sg regions_hierarchy in (* Return *) inst_sig diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 46b36851..de46320b 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -1,5 +1,18 @@ open LlbcAst include Charon.LlbcAstUtils +open Collections + +module FunIdOrderedType : OrderedType with type t = fun_id = struct + type t = fun_id + + let compare = compare_fun_id + let to_string = show_fun_id + let pp_t = pp_fun_id + let show_t = show_fun_id +end + +module FunIdMap = Collections.MakeMap (FunIdOrderedType) +module FunIdSet = Collections.MakeSet (FunIdOrderedType) let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : fun_sig = diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 8872571f..d2747a4b 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -786,18 +786,19 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) if rg_id0 = rg_id1 then true else (* We need to use the regions hierarchy *) - (* First, lookup the signature of the LLBC function *) - let sg = + let regions_hierarchy = let id0 = match id0 with | FunId fun_id -> fun_id | TraitMethod (_, _, fun_decl_id) -> FRegular fun_decl_id in - LlbcAstUtils.lookup_fun_sig id0 ctx.fun_ctx.fun_decls + LlbcAstUtils.FunIdMap.find id0 + ctx.fun_ctx.regions_hierarchies in (* Compute the set of ancestors of the function in call1 *) let call1_ancestors = - LlbcAstUtils.list_ancestor_region_groups sg rg_id1 + LlbcAstUtils.list_ancestor_region_groups regions_hierarchy + rg_id1 in (* Check if the function used in call0 is inside *) T.RegionGroupId.Set.mem rg_id0 call1_ancestors diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml new file mode 100644 index 00000000..dd566426 --- /dev/null +++ b/compiler/RegionsHierarchy.ml @@ -0,0 +1,243 @@ +(** This module analyzes function signatures to compute the + hierarchy between regions. + + Note that we don't need to analyze the types: when there is a non-trivial + relation between lifetimes in a type definition, the Rust compiler will + automatically introduce the relevant where clauses. For instance, in the + definition below: + + {[ + struct Wrapper<'a, 'b, T> { + x : &'a mut &'b mut T, + } + ]} + + the Rust compiler will introduce the where clauses: + {[ + 'b : 'a + T : 'b + ]} + + However, it doesn't do so for the function signatures, which means we have + to compute the constraints between the lifetimes ourselves, then that we + have to compute the SCCs of the lifetimes (two lifetimes 'a and 'b may + satisfy 'a : 'b and 'b : 'a, meaning they are actually equal and should + be grouped together). + *) + +open Types +open TypesUtils +open Expressions +open LlbcAst +open LlbcAstUtils +open Assumed +open SCC +module Subst = Substitute + +let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) + (sg : fun_sig) : region_groups = + (* Create the dependency graph. + + An edge from 'short to 'long means that 'long outlives 'short (that is + we have 'long : 'short, using Rust notations). + *) + (* First initialize the regions map. + + We add: + - the region variables + - the static region + - edges from the region variables to the static region + *) + let g : RegionSet.t RegionMap.t ref = + let s_set = RegionSet.singleton RStatic in + let m = + List.map + (fun (r : region_var) -> (RVar r.index, s_set)) + sg.generics.regions + in + let s = (RStatic, RegionSet.empty) in + ref (RegionMap.of_list (s :: m)) + in + + let add_edge ~(short : region) ~(long : region) = + let m = !g in + let s = RegionMap.find short !g in + let s = RegionSet.add long s in + g := RegionMap.add short s m + in + + let add_edge_from_region_constraint ((long, short) : region_outlives) = + add_edge ~short ~long + in + + let add_edges ~(long : region) ~(shorts : region list) = + List.iter (fun short -> add_edge ~short ~long) shorts + in + + (* Explore the clauses - we only explore the "region outlives" clause, + not the "type outlives" clauses *) + List.iter add_edge_from_region_constraint sg.preds.regions_outlive; + + (* Explore the types in the signature to add the edges *) + let rec explore_ty (outer : region list) (ty : ty) = + match ty with + | TAdt (id, generics) -> + (* Add constraints coming from the type clauses *) + (match id with + | TAdtId id -> + (* Lookup the type declaration *) + let decl = TypeDeclId.Map.find id type_decls in + (* Instantiate the predicates *) + let tr_self = + UnknownTrait ("Unexpected, introduced by " ^ __FUNCTION__) + in + let subst = + Subst.make_subst_from_generics decl.generics generics tr_self + in + let predicates = Subst.predicates_substitute subst decl.preds in + (* Note that because we also explore the generics below, we may + explore several times the same type - this is ok *) + List.iter + (fun (long, short) -> add_edges ~long ~shorts:(short :: outer)) + predicates.regions_outlive; + List.iter + (fun (ty, short) -> explore_ty (short :: outer) ty) + predicates.types_outlive + | TTuple -> (* No clauses for tuples *) () + | TAssumed aid -> ( + match aid with + | TBox | TArray | TSlice | TStr -> (* No clauses for those *) ())); + (* Explore the generics *) + explore_generics outer generics + | TVar _ | TLiteral _ | TNever -> () + | TRef (r, ty, _) -> + (* Add the constraints for r *) + add_edges ~long:r ~shorts:outer; + (* Add r to the outer regions *) + let outer = r :: outer in + (* Continue *) + explore_ty outer ty + | TRawPtr (ty, _) -> explore_ty outer ty + | TTraitType (trait_ref, _generic_args, _) -> + (* The trait should reference a clause, and not an implementation + (otherwise it should have been normalized) *) + assert ( + AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id); + (* We have nothing to do *) + () + | TArrow (inputs, output) -> + (* TODO: this may be too constraining *) + List.iter (explore_ty outer) (output :: inputs) + and explore_generics (outer : region list) (generics : generic_args) = + let { regions; types; const_generics = _; trait_refs = _ } = generics in + List.iter (fun long -> add_edges ~long ~shorts:outer) regions; + List.iter (explore_ty outer) types + in + + List.iter (explore_ty []) (sg.output :: sg.inputs); + + (* Compute the ordered SCCs *) + let module Scc = SCC.Make (RegionOrderedType) in + let sccs = Scc.compute (RegionMap.bindings !g) in + + (* Remove the SCC containing the static region. + + For now, we don't handle cases where regions different from 'static + can live as long as 'static, so we check that if the group contains + 'static then it is the only region it contains, and then we filter + the group. + TODO: general support for 'static + *) + let sccs = + (* Find the SCC which contains the static region *) + let static_gr_id, static_scc = + List.find + (fun (_, scc) -> List.mem RStatic scc) + (SccId.Map.bindings sccs.sccs) + in + (* The SCC should only contain the 'static *) + assert (static_scc = [ RStatic ]); + (* Remove the group as well as references to this group from the + other SCCs *) + let { sccs; scc_deps } = sccs in + (* We have to change the indexing: + - if id < static_gr_id: we leave the id as it is + - if id = static_gr_id: we remove id + - if id > static_gr_id: we decrement it by one + *) + let static_i = SccId.to_int static_gr_id in + let convert_id (id : SccId.id) : SccId.id option = + let i = SccId.to_int id in + if i < static_i then Some id + else if i = static_i then None + else Some (SccId.of_int (i - 1)) + in + let sccs = + SccId.Map.of_list + (List.filter_map + (fun (id, rg_ids) -> + match convert_id id with + | None -> None + | Some id -> Some (id, rg_ids)) + (SccId.Map.bindings sccs)) + in + + let scc_deps = + List.filter_map + (fun (id, deps) -> + match convert_id id with + | None -> None + | Some id -> + let deps = List.filter_map convert_id (SccId.Set.elements deps) in + Some (id, SccId.Set.of_list deps)) + (SccId.Map.bindings scc_deps) + in + let scc_deps = SccId.Map.of_list scc_deps in + + { sccs; scc_deps } + in + + (* + * Compute the regions hierarchy + *) + List.filter_map + (fun (scc_id, scc) -> + (* The region id *) + let i = SccId.to_int scc_id in + let id = RegionGroupId.of_int i in + + (* Retrieve the set of regions in the group *) + let regions = + List.map + (fun r -> + match r with RVar r -> r | _ -> raise (Failure "Unreachable")) + scc + in + + (* Compute the set of parent region groups *) + let parents = + List.map + (fun id -> RegionGroupId.of_int (SccId.to_int id)) + (SccId.Set.elements (SccId.Map.find scc_id sccs.scc_deps)) + in + + (* Put together *) + Some { id; regions; parents }) + (SccId.Map.bindings sccs.sccs) + +let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) + (fun_decls : fun_decl FunDeclId.Map.t) : region_groups FunIdMap.t = + let regular = + List.map + (fun (fid, d) -> (FRegular fid, d.signature)) + (FunDeclId.Map.bindings fun_decls) + in + let assumed = + List.map + (fun (info : assumed_fun_info) -> (FAssumed info.fun_id, info.fun_sig)) + assumed_fun_infos + in + FunIdMap.of_list + (List.map + (fun (fid, sg) -> (fid, compute_regions_hierarchy_for_sig type_decls sg)) + (regular @ assumed)) diff --git a/compiler/ReorderDecls.ml b/compiler/ReorderDecls.ml index c82d625f..53c94ff4 100644 --- a/compiler/ReorderDecls.ml +++ b/compiler/ReorderDecls.ml @@ -1,4 +1,3 @@ -open Graph open Collections open SCC open Pure @@ -99,99 +98,9 @@ let group_reorder_fun_decls (decls : fun_decl list) : decls in - (* - * Create the dependency graph - *) - (* Convert the ids to vertices (i.e., injectively map ids to integers, and create - vertices labeled with those integers). - - Rem.: [Graph.create] is *imperative*: it generates a new vertex every time - it is called (!!). - *) - let module Graph = Pack.Digraph in - let id_to_vertex : Graph.V.t FunIdMap.t = - let cnt = ref 0 in - FunIdMap.of_list - (List.map - (fun id -> - let lbl = !cnt in - cnt := !cnt + 1; - (* We create a vertex *) - let v = Graph.V.create lbl in - (id, v)) - idl) - in - let vertex_to_id : fun_id IntMap.t = - IntMap.of_list - (List.map - (fun (fid, v) -> (Graph.V.label v, fid)) - (FunIdMap.bindings id_to_vertex)) - in - - let to_v id = FunIdMap.find id id_to_vertex in - let to_id v = IntMap.find (Graph.V.label v) vertex_to_id in - - let g = Graph.create () in - - (* Add the edges, first from the vertices to themselves, then between vertices *) - List.iter - (fun (fun_id, deps) -> - let v = to_v fun_id in - Graph.add_edge g v v; - FunIdSet.iter (fun dep_id -> Graph.add_edge g v (to_v dep_id)) deps) - deps; - - (* Compute the SCCs *) - let module Comp = Components.Make (Graph) in - let sccs = Comp.scc_list g in - - (* Convert the vertices to ids *) - let sccs = List.map (List.map to_id) sccs in - - log#ldebug - (lazy - ("group_reorder_fun_decls: SCCs:\n" - ^ Print.list_to_string (Print.list_to_string FunIdOrderedType.show_t) sccs - )); - - (* Sanity check *) - let _ = - (* Check that the SCCs are pairwise disjoint *) - assert (FunIdSet.pairwise_disjoint (List.map FunIdSet.of_list sccs)); - (* Check that all the ids are in the sccs *) - let scc_ids = FunIdSet.of_list (List.concat sccs) in - - log#ldebug - (lazy - ("group_reorder_fun_decls: sanity check:" ^ "\n- ids : " - ^ FunIdSet.show ids ^ "\n- scc_ids: " ^ FunIdSet.show scc_ids)); - - assert (FunIdSet.equal scc_ids ids) - in - - log#ldebug - (lazy - ("group_reorder_fun_decls: reordered SCCs:\n" - ^ Print.list_to_string (Print.list_to_string FunIdOrderedType.show_t) sccs - )); - - (* Reorder *) - let module Reorder = SCC.Make (FunIdOrderedType) in - let id_deps = - FunIdMap.of_list - (List.map (fun (fid, deps) -> (fid, FunIdSet.elements deps)) deps) - in - let sccs = Reorder.reorder_sccs id_deps idl sccs in - - (* Sanity check *) - let _ = - (* Check that the SCCs are pairwise disjoint *) - let sccs = List.map snd (SccId.Map.bindings sccs.sccs) in - assert (FunIdSet.pairwise_disjoint (List.map FunIdSet.of_list sccs)); - (* Check that all the ids are in the sccs *) - let scc_ids = FunIdSet.of_list (List.concat sccs) in - assert (FunIdSet.equal scc_ids ids) - in + (* Compute the ordered SCCs *) + let module Scc = SCC.Make (FunIdOrderedType) in + let sccs = Scc.compute deps in (* Group the declarations *) let deps = FunIdMap.of_list deps in diff --git a/compiler/SCC.ml b/compiler/SCC.ml index d9a4cd3e..150821ad 100644 --- a/compiler/SCC.ml +++ b/compiler/SCC.ml @@ -6,8 +6,15 @@ module SccId = Identifiers.IdGen () (** The local logger *) let log = Logging.scc_log +(** A structure containing information about SCCs (strongly connected components) *) +type 'id sccs = { + sccs : 'id list SccId.Map.t; + scc_deps : SccId.Set.t SccId.Map.t; (** The dependencies between sccs *) +} +[@@deriving show] + (** A functor which provides functions to work on strongly connected components *) -module Make (Id : OrderedType) = struct +module MakeReorder (Id : OrderedType) = struct module IdMap = MakeMap (Id) module IdSet = MakeSet (Id) @@ -15,13 +22,6 @@ module Make (Id : OrderedType) = struct let pp_id = Id.pp_t - (** A structure containing information about SCCs (strongly connected components) *) - type sccs = { - sccs : id list SccId.Map.t; - scc_deps : SccId.Set.t SccId.Map.t; (** The dependencies between sccs *) - } - [@@deriving show] - (** The order in which Tarjan's algorithm generates the SCCs is arbitrary, while we want to keep as much as possible the original order (the order in which the user generated the ids). For this, we iterate through @@ -93,7 +93,7 @@ module Make (Id : OrderedType) = struct Charon project. *) let reorder_sccs (id_deps : Id.t list IdMap.t) (ids : Id.t list) - (sccs : Id.t list list) : sccs = + (sccs : Id.t list list) : id sccs = (* Map the identifiers to the SCC indices *) let id_to_scc = IdMap.of_list @@ -168,13 +168,114 @@ module Make (Id : OrderedType) = struct { sccs = tgt_sccs; scc_deps = tgt_deps } end +module Make (Id : OrderedType) = struct + module M = MakeMap (Id) + module S = MakeSet (Id) + + (** Compute the ordered SCC components for a graph, which is a map + from identifier to set of identifiers (which represent the set + of edges starting from an identifier). + *) + let compute (m : (Id.t * S.t) list) : Id.t sccs = + (* + * Create the dependency graph + *) + (* Compute the list/set of identifiers *) + let idl = List.map fst m in + let ids = S.of_list idl in + + (* Convert the ids to vertices (i.e., injectively map ids to integers, + and create vertices labeled with those integers). + + Rem.: [Graph.create] is *imperative*: it generates a new vertex every + time it is called (!!). For this reason, we first add all the vertices + we need, then add the edges. + *) + let open Graph in + let module IntMap = MakeMap (OrderedInt) in + let module Graph = Pack.Digraph in + let id_to_vertex : Graph.V.t M.t = + let cnt = ref 0 in + M.of_list + (List.map + (fun id -> + let lbl = !cnt in + cnt := !cnt + 1; + (* We create a vertex *) + let v = Graph.V.create lbl in + (id, v)) + idl) + in + let vertex_to_id : Id.t IntMap.t = + IntMap.of_list + (List.map + (fun (fid, v) -> (Graph.V.label v, fid)) + (M.bindings id_to_vertex)) + in + + let to_v id = M.find id id_to_vertex in + let to_id v = IntMap.find (Graph.V.label v) vertex_to_id in + + let g = Graph.create () in + + (* Add the edges, first from the vertices to themselves, then between + vertices. *) + List.iter + (fun (id, deps) -> + let v = to_v id in + Graph.add_edge g v v; + S.iter (fun dep_id -> Graph.add_edge g v (to_v dep_id)) deps) + m; + + (* Compute the SCCs *) + let module Comp = Components.Make (Graph) in + let sccs = Comp.scc_list g in + + (* Convert the vertices to ids *) + let sccs = List.map (List.map to_id) sccs in + + (* Sanity check *) + let _ = + (* Check that the SCCs are pairwise disjoint *) + assert (S.pairwise_disjoint (List.map S.of_list sccs)); + (* Check that all the ids are in the sccs *) + let scc_ids = S.of_list (List.concat sccs) in + + log#ldebug + (lazy + ("group_reorder_fun_decls: sanity check:" ^ "\n- ids : " + ^ S.show ids ^ "\n- scc_ids: " ^ S.show scc_ids)); + + assert (S.equal scc_ids ids) + in + + (* Reorder *) + let module Reorder = MakeReorder (Id) in + let id_deps = + M.of_list (List.map (fun (fid, deps) -> (fid, S.elements deps)) m) + in + let sccs = Reorder.reorder_sccs id_deps idl sccs in + + (* Sanity check *) + let _ = + (* Check that the SCCs are pairwise disjoint *) + let sccs = List.map snd (SccId.Map.bindings sccs.sccs) in + assert (S.pairwise_disjoint (List.map S.of_list sccs)); + (* Check that all the ids are in the sccs *) + let scc_ids = S.of_list (List.concat sccs) in + assert (S.equal scc_ids ids) + in + + sccs +end + (** Test - TODO: make "real" unit tests *) let _ = (* Check that some SCCs are correctly reordered *) let check_sccs (id_deps : (int * int list) list) (ids : int list) (sccs : int list list) (tgt_sccs : int list list) : unit = let module Ord = OrderedInt in - let module Reorder = Make (Ord) in + let module Reorder = MakeReorder (Ord) in let module Map = MakeMap (Ord) in let id_deps = Map.of_list id_deps in diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index 166c237a..45edc602 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -64,6 +64,10 @@ let generic_args_substitute (subst : subst) (g : T.generic_args) : let visitor = st_substitute_visitor subst in visitor#visit_generic_args () g +let predicates_substitute (subst : subst) (p : T.predicates) : T.predicates = + let visitor = st_substitute_visitor subst in + visitor#visit_predicates () p + let erase_regions_subst : subst = { r_subst = (fun _ -> T.RErased); @@ -351,7 +355,8 @@ let trait_type_constraint_substitute (subst : subst) let ty = visitor#visit_ty () ty in { T.trait_ref; generics; type_name; ty } -(** Substitute a function signature. +(** Substitute a function signature, together with the regions hierarchy + associated to that signature. **IMPORTANT:** this function doesn't normalize the types. *) @@ -360,7 +365,8 @@ let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id) (ty_subst : T.TypeVarId.id -> T.ty) (cg_subst : T.ConstGenericVarId.id -> T.const_generic) (tr_subst : T.TraitClauseId.id -> T.trait_instance_id) - (tr_self : T.trait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig = + (tr_self : T.trait_instance_id) (sg : A.fun_sig) + (regions_hierarchy : T.region_groups) : A.inst_fun_sig = let r_subst' (r : T.region) : T.region = match r with | T.RStatic | T.RErased -> r @@ -375,7 +381,7 @@ let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id) let parents = List.map asubst rg.parents in ({ id; regions; parents } : A.abs_region_group) in - let regions_hierarchy = List.map subst_region_group sg.A.regions_hierarchy in + let regions_hierarchy = List.map subst_region_group regions_hierarchy in let trait_type_constraints = List.map (trait_type_constraint_substitute subst) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 258b1cf2..922aa307 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -47,6 +47,7 @@ type fun_context = { llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t; fun_sigs : fun_sig_named_outputs RegularFunIdNotLoopMap.t; (** *) fun_infos : FA.fun_info A.FunDeclId.Map.t; + regions_hierarchies : T.region_groups FunIdMap.t; } [@@deriving show] @@ -441,8 +442,8 @@ and translate_strait_instance_id (id : T.trait_instance_id) : trait_instance_id translate_trait_instance_id translate_sty id let translate_trait_clause (clause : T.trait_clause) : trait_clause = - let { T.clause_id; meta = _; trait_id; generics } = clause in - let generics = translate_sgeneric_args generics in + let { T.clause_id; meta = _; trait_id; clause_generics } = clause in + let generics = translate_sgeneric_args clause_generics in { clause_id; trait_id; generics } let translate_strait_type_constraint (ttc : T.trait_type_constraint) : @@ -848,11 +849,14 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id) let fun_infos = decls_ctx.fun_ctx.fun_infos in let type_infos = decls_ctx.type_ctx.type_infos in (* Retrieve the list of parent backward functions *) + let regions_hierarchy = + FunIdMap.find fun_id decls_ctx.fun_ctx.regions_hierarchies + in let gid, parents = match bid with | None -> (None, T.RegionGroupId.Set.empty) | Some bid -> - let parents = list_ancestor_region_groups sg bid in + let parents = list_ancestor_region_groups regions_hierarchy bid in (Some bid, parents) in (* Is the function stateful, and can it fail? *) @@ -865,7 +869,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id) (* Create the context *) let ctx = let region_groups = - List.map (fun (g : T.region_group) -> g.id) sg.regions_hierarchy + List.map (fun (g : T.region_group) -> g.id) regions_hierarchy in let ctx = InterpreterUtils.initialize_eval_context decls_ctx region_groups @@ -898,7 +902,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id) assert (T.RegionGroupId.Set.is_empty parents); (* Small helper to translate types for backward functions *) let translate_back_ty_for_gid (gid : T.RegionGroupId.id) : T.ty -> ty option = - let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in + let rg = T.RegionGroupId.nth regions_hierarchy gid in let regions = T.RegionId.Set.of_list rg.regions in let keep_region r = match r with @@ -2924,6 +2928,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = let basename = def.name in (* Retrieve the signature *) let signature = ctx.sg in + let regions_hierarchy = + FunIdMap.find (FRegular def_id) ctx.fun_context.regions_hierarchies + in (* Translate the body, if there is *) let body = match body with @@ -2965,7 +2972,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = | None -> [] | Some back_id -> let parents_ids = - list_ordered_ancestor_region_groups def.signature back_id + list_ordered_ancestor_region_groups regions_hierarchy back_id in let backward_ids = List.append parents_ids [ back_id ] in List.concat @@ -3069,6 +3076,10 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx) let translate_one (fun_id : A.fun_id) (input_names : string option list) (sg : A.fun_sig) : (regular_fun_id_not_loop * fun_sig_named_outputs) list = + (* Retrieve the regions hierarchy *) + let regions_hierarchy = + FunIdMap.find fun_id decls_ctx.fun_ctx.regions_hierarchies + in (* The forward function *) let fwd_sg = translate_fun_sig decls_ctx fun_id sg input_names None in let fwd_id = (fun_id, None) in @@ -3081,7 +3092,7 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx) in let id = (fun_id, Some rg.id) in (id, tsg)) - sg.regions_hierarchy + regions_hierarchy in (* Return *) (fwd_id, fwd_sg) :: back_sgs diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 9a6addee..2aedb544 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -91,6 +91,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) SymbolicToPure.llbc_fun_decls = trans_ctx.fun_ctx.fun_decls; fun_sigs; fun_infos = trans_ctx.fun_ctx.fun_infos; + regions_hierarchies = trans_ctx.fun_ctx.regions_hierarchies; } in let global_context = @@ -263,9 +264,11 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Translate *) SymbolicToPure.translate_fun_decl ctx (Some symbolic) in - let pure_backwards = - List.map translate_backward fdef.signature.regions_hierarchy + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FRegular fdef.def_id) + fun_context.regions_hierarchies in + let pure_backwards = List.map translate_backward regions_hierarchy in (* Return *) (pure_forward, pure_backwards) diff --git a/compiler/dune b/compiler/dune index 648c7325..bc3cc718 100644 --- a/compiler/dune +++ b/compiler/dune @@ -57,6 +57,7 @@ Pure PureTypeCheck PureUtils + RegionsHierarchy ReorderDecls SCC Scalars -- cgit v1.3.1 From a27efd1ed08bc9583752445d9eda7a693c0c7379 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 16 Nov 2023 10:13:28 +0100 Subject: Finish propagating the changes to the names and cleaning --- compiler/Contexts.ml | 2 +- compiler/Driver.ml | 21 +++--- compiler/Extract.ml | 40 +++++------ compiler/ExtractTypes.ml | 155 +++++++++++++++++++++++++++++------------- compiler/FunsAnalysis.ml | 4 +- compiler/Print.ml | 1 - compiler/Pure.ml | 1 + compiler/PureMicroPasses.ml | 29 ++++---- compiler/SymbolicToPure.ml | 6 +- compiler/Translate.ml | 159 ++++++++++++++++++++++---------------------- compiler/TranslateCore.ml | 3 + compiler/TypesAnalysis.ml | 2 +- 12 files changed, 244 insertions(+), 179 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index 41c84141..a2ae4f16 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -525,7 +525,7 @@ let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id) let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool = let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in - match decl_group with Rec _ -> true | NonRec _ -> false + match decl_group with RecGroup _ -> true | NonRecGroup _ -> false (** Visitor to iterate over the values in the *current* frame *) class ['self] iter_frame = diff --git a/compiler/Driver.ml b/compiler/Driver.ml index aa293469..94e50a08 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -1,15 +1,10 @@ open Aeneas.LlbcOfJson open Aeneas.Logging -module T = Aeneas.Types -module A = Aeneas.LlbcAst -module I = Aeneas.Interpreter +open Aeneas.LlbcAst +open Aeneas.Interpreter module EL = Easy_logging.Logging -module TA = Aeneas.TypesAnalysis -module Micro = Aeneas.PureMicroPasses -module Print = Aeneas.Print -module PrePasses = Aeneas.PrePasses -module Translate = Aeneas.Translate open Aeneas.Config +open Aeneas (** The local logger *) let log = main_log @@ -227,7 +222,9 @@ let () = if !backend = Lean && !extract_decreases_clauses && List.exists - (function Aeneas.LlbcAst.Fun (Rec (_ :: _)) -> true | _ -> false) + (function + | Aeneas.LlbcAst.FunGroup (RecGroup (_ :: _)) -> true + | _ -> false) m.declarations then ( log#error @@ -237,15 +234,15 @@ let () = fail ()); (* Apply the pre-passes *) - let m = PrePasses.apply_passes m in + let m = Aeneas.PrePasses.apply_passes m in (* Some options for the execution *) (* Test the unit functions with the concrete interpreter *) - if !test_unit_functions then I.Test.test_unit_functions m; + if !test_unit_functions then Test.test_unit_functions m; (* Translate the functions *) - Translate.translate_crate filename dest_dir m; + Aeneas.Translate.translate_crate filename dest_dir m; (* Print total elapsed time *) log#linfo diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 04f6c2c3..cd62c15c 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -27,7 +27,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) let builtin = let open ExtractBuiltin in let funs_map = builtin_funs_map () in - let sname = name_to_simple_name def.fwd.f.basename in + let sname = name_to_simple_name def.fwd.f.llbc_name in SimpleNameMap.find_opt sname funs_map in (* Use the builtin names if necessary *) @@ -65,7 +65,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) raise (Failure ("Not found: " - ^ Names.name_to_string f.basename + ^ name_to_string ctx f.llbc_name ^ ", " ^ Print.option_to_string Pure.show_loop_id f.loop_id ^ Print.option_to_string Pure.show_region_group_id @@ -212,7 +212,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list) let decl = FunDeclId.Map.find id ctx.trans_funs in let err = "Ill-formed builtin information for function " - ^ Names.name_to_string decl.fwd.f.basename + ^ name_to_string ctx decl.fwd.f.llbc_name ^ ": " ^ string_of_int (List.length filter) ^ " filtering arguments provided for " @@ -1137,7 +1137,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) extract_comment fmt - [ "[" ^ Print.fun_name_to_string def.basename ^ "]: decreases clause" ]; + [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]; F.pp_print_space fmt (); (* Open a box for the definition, so that whenever possible it gets printed on * one line *) @@ -1199,7 +1199,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) extract_comment fmt - [ "[" ^ Print.fun_name_to_string def.basename ^ "]: termination measure" ]; + [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]; F.pp_print_space fmt (); (* Open a box for the definition, so that whenever possible it gets printed on * one line *) @@ -1253,7 +1253,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) (* syntax term ... term : tactic *) F.pp_print_break fmt 0 0; extract_comment fmt - [ "[" ^ Print.fun_name_to_string def.basename ^ "]: decreases_by tactic" ]; + [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]; F.pp_print_space fmt (); F.pp_open_hvbox fmt 0; F.pp_print_string fmt "syntax \""; @@ -1289,7 +1289,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter) (Pure.FunId (FRegular def.def_id), def.loop_id, def.back_id) ctx.fun_name_info in - let comment_pre = "[" ^ Print.fun_name_to_string def.basename ^ "]: " in + let comment_pre = "[" ^ name_to_string ctx def.llbc_name ^ "]: " in let comment = let loop_comment = match def.loop_id with @@ -1766,13 +1766,13 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; - extract_comment fmt [ "[" ^ Print.global_name_to_string global.name ^ "]" ]; + extract_comment fmt [ "[" ^ name_to_string ctx global.name ^ "]" ]; F.pp_print_space fmt (); let decl_name = ctx_get_global global.def_id ctx in let body_name = ctx_get_function - (FromLlbc (Pure.FunId (FRegular global.body_id), None, None)) + (FromLlbc (Pure.FunId (FRegular global.body), None, None)) ctx in @@ -1958,8 +1958,10 @@ let extract_trait_decl_method_names (ctx : extraction_ctx) = (* We do something special to reuse the [ctx_compute_fun_decl] function. TODO: make it cleaner. *) - let basename : name = [ Ident item_name ] in - let f = { f with basename } in + let llbc_name : Types.name = + [ Types.PeIdent (item_name, Disambiguator.zero) ] + in + let f = { f with llbc_name } in let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in let name = ctx_compute_fun_name trans f ctx in (* Add a prefix if necessary *) @@ -1991,7 +1993,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx) | None -> let err = "Ill-formed builtin information for trait decl \"" - ^ Names.name_to_string trait_decl.name + ^ name_to_string ctx trait_decl.llbc_name ^ "\", method \"" ^ item_name ^ "\": could not find name for region " ^ Print.option_to_string Pure.show_region_group_id @@ -2022,7 +2024,7 @@ let extract_trait_decl_register_names (ctx : extraction_ctx) (trait_decl : trait_decl) : extraction_ctx = (* Lookup the information if this is a builtin trait *) let open ExtractBuiltin in - let sname = name_to_simple_name trait_decl.name in + let sname = name_to_simple_name trait_decl.llbc_name in let builtin_info = SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) in @@ -2059,8 +2061,8 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) (* Check if the trait implementation is builtin *) let builtin_info = let open ExtractBuiltin in - let type_sname = name_to_simple_name trait_impl.name in - let trait_sname = name_to_simple_name trait_decl.name in + let type_sname = name_to_simple_name trait_impl.llbc_name in + let trait_sname = name_to_simple_name trait_decl.llbc_name in SimpleNamePairMap.find_opt (type_sname, trait_sname) (builtin_trait_impls_map ()) in @@ -2185,7 +2187,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) extract_comment fmt - [ "Trait declaration: [" ^ Print.name_to_string decl.name ^ "]" ]; + [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]; F.pp_print_break fmt 0 0; (* Open two outer boxes for the definition, so that whenever possible it gets printed on one line and indents are correct. @@ -2466,14 +2468,14 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) (** Extract a trait implementation *) let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (impl : trait_impl) : unit = - log#ldebug (lazy ("extract_trait_impl: " ^ Names.name_to_string impl.name)); + log#ldebug (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.llbc_name)); (* Retrieve the impl name *) let impl_name = ctx_get_trait_impl impl.def_id ctx in (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) extract_comment fmt - [ "Trait implementation: [" ^ Print.name_to_string impl.name ^ "]" ]; + [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]; F.pp_print_break fmt 0 0; (* Open two outer boxes for the definition, so that whenever possible it gets printed on @@ -2640,7 +2642,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_break fmt 0 0; (* Print a comment *) extract_comment fmt - [ "Unit test for [" ^ Print.fun_name_to_string def.basename ^ "]" ]; + [ "Unit test for [" ^ name_to_string ctx def.llbc_name ^ "]" ]; F.pp_print_space fmt (); (* Open a box for the test *) F.pp_open_hovbox fmt ctx.indent_incr; diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 553d5863..e4617d2c 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -309,7 +309,6 @@ let assumed_llbc_functions () : (SliceIndexShared, None, "slice_index_usize"); (SliceIndexMut, None, "slice_index_usize"); (SliceIndexMut, rg0, "slice_update_usize"); - (SliceLen, None, "slice_len"); ] | Lean -> [ @@ -323,7 +322,6 @@ let assumed_llbc_functions () : (SliceIndexShared, None, "Slice.index_usize"); (SliceIndexMut, None, "Slice.index_usize"); (SliceIndexMut, rg0, "Slice.update_usize"); - (SliceLen, None, "Slice.len"); ] let assumed_pure_functions () : (pure_assumed_fun_id * string) list = @@ -538,6 +536,11 @@ let type_keyword () = | Coq | Lean -> "Type" | HOL4 -> raise (Failure "Unexpected") +let name_last_elem_as_ident (n : llbc_name) : string = + match Collections.List.last n with + | PeIdent (s, _) -> s + | PeImpl _ -> raise (Failure "Unexpected") + (** [ctx]: we use the context to lookup type definitions, to retrieve type names. This is used to compute variable names, when they have no basenames: in this @@ -579,34 +582,90 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) let int_name = int_name in (* Prepare a name. - * The first id elem is always the crate: if it is the local crate, - * we remove it. - * We also remove all the disambiguators, then convert everything to strings. - * **Rmk:** because we remove the disambiguators, there may be name collisions - * (which is ok, because we check for name collisions and fail if there is any). - *) - let get_name (name : name) : string list = + The first id elem is always the crate: if it is the local crate, + we remove it. We ignore disambiguators (there may be collisions, but we + check if there are). + *) + let rec name_to_simple_name (name : llbc_name) : string list = (* Rmk.: initially we only filtered the disambiguators equal to 0 *) - let name = Names.filter_disambiguators name in match name with - | Ident crate :: name -> - let name = if crate = crate_name then name else Ident crate :: name in + | (PeIdent (crate, _) as id) :: name -> + let name = if crate = crate_name then name else id :: name in + let open Types in let name = List.map (function - | Names.Ident s -> s - | Disambiguator d -> Names.Disambiguator.to_string d) + | PeIdent (s, _) -> s + | PeImpl impl -> impl_elem_to_simple_name impl) name in name | _ -> - raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name)) + raise + (Failure + ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name)) + and impl_elem_to_simple_name (impl : Types.impl_elem) : string = + (* We do something simple for now. + TODO: we might want to do something different for impl elements which are + actually trait implementations, in order to prevent name collisions (it + is possible to define several times the same trait for the same type, + but with different instantiations of the type, or different trait + requirements *) + ty_to_simple_name impl.generics impl.ty + and ty_to_simple_name (generics : Types.generic_params) (ty : Types.ty) : + string = + (* We do something simple for now. + TODO: find a more principled way of converting types to names. + In particular, we might want to do something different for impl elements which are + actually trait implementations, in order to prevent name collisions (it + is possible to define several times the same trait for the same type, + but with different instantiations of the type, or different trait + requirements *) + match ty with + | TAdt (id, args) -> ( + match id with + | TAdtId id -> + let def = TypeDeclId.Map.find id ctx.type_ctx.type_decls in + name_last_elem_as_ident def.name + | TTuple -> + (* TODO *) + "Tuple" + ^ String.concat "" + (List.map (ty_to_simple_name generics) args.types) + | TAssumed id -> Types.show_assumed_ty id) + | TVar vid -> + (* Use the variable name *) + (List.find (fun (v : type_var) -> v.index = vid) generics.types).name + | TLiteral lty -> + StringUtils.capitalize_first_letter + (Print.Types.literal_type_to_string lty) + | TNever -> raise (Failure "Unreachable") + | TRef (_, rty, rk) -> ( + let rty = ty_to_simple_name generics rty in + match rk with + | RMut -> "MutBorrow" ^ rty + | RShared -> "SharedBorrow" ^ rty) + | TRawPtr (rty, rk) -> ( + let rty = ty_to_simple_name generics rty in + match rk with RMut -> "MutPtr" ^ rty | RShared -> "ConstPtr" ^ rty) + | TTraitType (tr, _, name) -> + (* TODO: this is way too simple *) + let trait_decl = + TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id + ctx.trait_decls_ctx.trait_decls + in + name_last_elem_as_ident trait_decl.name ^ name + | TArrow (inputs, output) -> + "Arrow" + ^ String.concat "" + (List.map (ty_to_simple_name generics) (inputs @ [ output ])) in let flatten_name (name : string list) : string = match !backend with | FStar | Coq | HOL4 -> String.concat "_" name | Lean -> String.concat "." name in + let get_name name : string list = name_to_simple_name name in let get_type_name = get_name in let get_type_name_no_suffix name = match !backend with @@ -620,7 +679,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | Coq | HOL4 -> get_type_name_no_suffix name ^ "_t" | Lean -> get_type_name_no_suffix name in - let field_name (def_name : name) (field_id : FieldId.id) + let field_name (def_name : llbc_name) (field_id : FieldId.id) (field_name : string option) : string = let field_name_s = match field_name with @@ -639,7 +698,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | Lean | HOL4 -> def_name | Coq | FStar -> StringUtils.lowercase_first_letter def_name in - let variant_name (def_name : name) (variant : string) : string = + let variant_name (def_name : llbc_name) (variant : string) : string = match !backend with | FStar | Coq | HOL4 -> let variant = to_camel_case variant in @@ -649,7 +708,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) else variant | Lean -> variant in - let struct_constructor (basename : name) : string = + let struct_constructor (basename : llbc_name) : string = let tname = type_name basename in ExtractBuiltin.mk_struct_constructor tname in @@ -661,15 +720,15 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname | Lean -> fname in - let global_name (name : global_name) : string = + let global_name (name : llbc_name) : string = (* Converting to snake case also lowercases the letters (in Rust, global * names are written in capital letters). *) let parts = List.map to_snake_case (get_name name) in String.concat "_" parts in - let fun_name (fname : fun_name) (num_loops : int) (loop_id : LoopId.id option) - (num_rgs : int) (rg : region_group_info option) (filter_info : bool * int) - : string = + let fun_name (fname : llbc_name) (num_loops : int) + (loop_id : LoopId.id option) (num_rgs : int) + (rg : region_group_info option) (filter_info : bool * int) : string = let fname = get_fun_name fname in (* Compute the suffix *) let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in @@ -678,7 +737,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) in let trait_decl_name (trait_decl : trait_decl) : string = - type_name trait_decl.name + type_name trait_decl.llbc_name in let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) : @@ -686,12 +745,14 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) (* TODO: provisional: we concatenate the trait impl name (which is its type) with the trait decl name *) let trait_decl = - let name = trait_decl.name in + let name = trait_decl.llbc_name in let name = get_type_name_no_suffix name ^ "Inst" in (* Remove the occurrences of '.' *) String.concat "" (String.split_on_char '.' name) in - let name = flatten_name (get_type_name trait_impl.name @ [ trait_decl ]) in + let name = + flatten_name (get_type_name trait_impl.llbc_name @ [ trait_decl ]) + in match !backend with | FStar -> StringUtils.lowercase_first_letter name | Coq | HOL4 | Lean -> name @@ -745,7 +806,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) ^ TraitClauseId.to_string clause.clause_id in - let termination_measure_name (_fid : A.FunDeclId.id) (fname : fun_name) + let termination_measure_name (_fid : A.FunDeclId.id) (fname : llbc_name) (num_loops : int) (loop_id : LoopId.id option) : string = let fname = get_fun_name fname in let lp_suffix = default_fun_loop_suffix num_loops loop_id in @@ -760,7 +821,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) fname ^ lp_suffix ^ suffix in - let decreases_proof_name (_fid : A.FunDeclId.id) (fname : fun_name) + let decreases_proof_name (_fid : A.FunDeclId.id) (fname : llbc_name) (num_loops : int) (loop_id : LoopId.id option) : string = let fname = get_fun_name fname in let lp_suffix = default_fun_loop_suffix num_loops loop_id in @@ -815,12 +876,12 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | 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" - *) + Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm" + *) (* The name shouldn't be empty, and its last element should * be an ident *) - let cl = List.nth def.name (List.length def.name - 1) in - name_from_type_ident (Names.as_ident cl)) + let cl = Collections.List.last def.name in + name_from_type_ident (TypesUtils.as_ident cl)) | TVar _ -> ( (* TODO: use "t" also for F* *) match !backend with @@ -866,31 +927,31 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) match cv with | VScalar sv -> ( match !backend with - | FStar -> F.pp_print_string fmt (Z.to_string sv.PV.value) + | FStar -> F.pp_print_string fmt (Z.to_string sv.value) | Coq | HOL4 | Lean -> let print_brackets = inside && !backend = HOL4 in if print_brackets then F.pp_print_string fmt "("; (match !backend with | Coq | Lean -> () | HOL4 -> - F.pp_print_string fmt ("int_to_" ^ int_name sv.PV.int_ty); + F.pp_print_string fmt ("int_to_" ^ int_name sv.int_ty); F.pp_print_space fmt () | _ -> raise (Failure "Unreachable")); (* We need to add parentheses if the value is negative *) - if sv.PV.value >= Z.of_int 0 then - F.pp_print_string fmt (Z.to_string sv.PV.value) + if sv.value >= Z.of_int 0 then + F.pp_print_string fmt (Z.to_string sv.value) else if !backend = Lean then (* TODO: parsing issues with Lean because there are ambiguous interpretations between int values and nat values *) F.pp_print_string fmt - ("(-(" ^ Z.to_string (Z.neg sv.PV.value) ^ ":Int))") - else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")"); + ("(-(" ^ Z.to_string (Z.neg sv.value) ^ ":Int))") + else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")"); (match !backend with | Coq -> - let iname = int_name sv.PV.int_ty in + let iname = int_name sv.int_ty in F.pp_print_string fmt ("%" ^ iname) | Lean -> - let iname = String.lowercase_ascii (int_name sv.PV.int_ty) in + let iname = String.lowercase_ascii (int_name sv.int_ty) in F.pp_print_string fmt ("#" ^ iname) | HOL4 -> () | _ -> raise (Failure "Unreachable")); @@ -1426,7 +1487,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : extraction_ctx = (* Lookup the builtin information, if there is *) let open ExtractBuiltin in - let sname = name_to_simple_name def.name in + let sname = name_to_simple_name def.llbc_name in let info = SimpleNameMap.find_opt sname (builtin_types_map ()) in (* Register the filtering information, if there is *) let ctx = @@ -1442,7 +1503,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : (* Compute and register the type def name *) let def_name = match info with - | None -> ctx.fmt.type_name def.name + | None -> ctx.fmt.type_name def.llbc_name | Some info -> info.extract_name in let ctx = ctx_add (TypeId (TAdtId def.def_id)) def_name ctx in @@ -1460,10 +1521,10 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : let field_names = FieldId.mapi (fun fid (field : field) -> - (fid, ctx.fmt.field_name def.name fid field.field_name)) + (fid, ctx.fmt.field_name def.llbc_name fid field.field_name)) fields in - let cons_name = ctx.fmt.struct_constructor def.name in + let cons_name = ctx.fmt.struct_constructor def.llbc_name in (field_names, cons_name) | Some { body_info = Some (Struct (cons_name, field_names)); _ } -> let field_names = @@ -1499,12 +1560,12 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : VariantId.mapi (fun variant_id (variant : variant) -> let name = - ctx.fmt.variant_name def.name variant.variant_name + ctx.fmt.variant_name def.llbc_name variant.variant_name in (* Add the type name prefix for Lean *) let name = if !Config.backend = Lean then - let type_name = ctx.fmt.type_name def.name in + let type_name = ctx.fmt.type_name def.llbc_name in type_name ^ "." ^ name else name in @@ -1648,7 +1709,7 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter) let print_variant _variant_id (v : variant) = (* We don't lookup the name, because it may have a prefix for the type id (in the case of Lean) *) - let cons_name = ctx.fmt.variant_name def.name v.variant_name in + let cons_name = ctx.fmt.variant_name def.llbc_name v.variant_name in let fields = v.fields in extract_type_decl_variant ctx fmt type_decl_group def_name type_params cg_params cons_name fields @@ -2030,7 +2091,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) if !backend <> HOL4 || not (decl_is_first_from_group kind) then F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment fmt [ "[" ^ Print.name_to_string def.name ^ "]" ]; + extract_comment fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]; F.pp_print_break fmt 0 0; (* Open a box for the definition, so that whenever possible it gets printed on * one line. Note however that in the case of Lean line breaks are important diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 57aa9e12..a07ad35a 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -164,7 +164,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let analyze_fun_decl_group (d : fun_declaration_group) : unit = (* Retrieve the function declarations *) - let funs = match d with NonRec id -> [ id ] | Rec ids -> ids in + let funs = match d with NonRecGroup id -> [ id ] | RecGroup ids -> ids in let funs = List.map (fun id -> FunDeclId.Map.find id funs_map) funs in let fun_ids = List.map (fun (d : fun_decl) -> d.def_id) funs in let fun_ids = FunDeclId.Set.of_list fun_ids in @@ -183,7 +183,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) | GlobalGroup id :: decls' -> (* Analyze a global by analyzing its body function *) let global = GlobalDeclId.Map.find id globals_map in - analyze_fun_decl_group (NonRec global.body); + analyze_fun_decl_group (NonRecGroup global.body); analyze_decl_groups decls' in diff --git a/compiler/Print.ml b/compiler/Print.ml index cd83a589..48a5a20b 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -1,6 +1,5 @@ include Charon.PrintUtils include Charon.PrintLlbcAst -open Charon.PrintPrimitiveValues open Charon.PrintTypes open Charon.PrintExpressions open Charon.PrintLlbcAst.Ast diff --git a/compiler/Pure.ml b/compiler/Pure.ml index fa059499..40711e53 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -14,6 +14,7 @@ module GlobalDeclId = A.GlobalDeclId module TraitDeclId = T.TraitDeclId module TraitImplId = T.TraitImplId module TraitClauseId = T.TraitClauseId +module Disambiguator = T.Disambiguator (** We redefine identifiers for loop: in {!Values}, the identifiers are global (they monotonically increase across functions) while in {!module:Pure} we want diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index d2747a4b..2106c206 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -3,10 +3,13 @@ open Pure open PureUtils open TranslateCore -module V = Values (** The local logger *) -let log = L.pure_micro_passes_log +let log = Logging.pure_micro_passes_log + +let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = + let fmt = trans_ctx_to_pure_fmt_env ctx in + PrintPure.fun_decl_to_string fmt def (** Small utility. @@ -597,8 +600,8 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl = match TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls_groups with - | NonRec _ -> false - | Rec _ -> true + | NonRecGroup _ -> false + | RecGroup _ -> true in (* Convert, if possible - note that for now for Lean and Coq we don't support the structure syntax on recursive structures *) @@ -1420,14 +1423,15 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = let loop_body = { inputs; inputs_lvs; body = loop_body } in - let loop_def = + let loop_def : fun_decl = { def_id = def.def_id; kind = def.kind; num_loops; loop_id = Some loop.loop_id; back_id = def.back_id; - basename = def.basename; + llbc_name = def.llbc_name; + name = def.name; signature = loop_sig; is_global_decl_body = def.is_global_decl_body; body = Some loop_body; @@ -1539,10 +1543,12 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = mk_unit_rvalue | ( ( SliceIndexShared | SliceIndexMut | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut - | ArrayRepeat | SliceLen ), + | ArrayRepeat ), _ ) -> super#visit_texpression env e) - | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> ( + | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> + failwith "TODO" + (* (* Lookup the function name *) let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in match @@ -1570,7 +1576,8 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = | _ -> raise (Failure "Unreachable") in mk_apps arg args - | _ -> super#visit_texpression env e) + | _ -> super#visit_texpression env e + *) | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e end @@ -1918,9 +1925,7 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : (* Debug *) log#ldebug (lazy - ("PureMicroPasses.apply_passes_to_def: " - ^ Print.fun_name_to_string def.basename - ^ " (" + ("PureMicroPasses.apply_passes_to_def: " ^ def.name ^ " (" ^ Print.option_to_string T.RegionGroupId.to_string def.back_id ^ ")")); diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 2460e040..4e12d31e 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3036,9 +3036,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = (* return *) def -let translate_type_decls (ctx : Contexts.decls_ctx) - (type_decls : T.type_decl list) : type_decl list = - List.map (translate_type_decl ctx) type_decls +let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = + List.map (translate_type_decl ctx) + (TypeDeclId.Map.values ctx.type_ctx.type_decls) (** Translates function signatures. diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 2aedb544..cf23fd44 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -1,11 +1,11 @@ -open InterpreterStatements open Interpreter -module L = Logging -module T = Types -module A = LlbcAst +open Expressions +open Types +open Values +open LlbcAst +open Contexts module SA = SymbolicAst module Micro = PureMicroPasses -module C = Contexts open PureUtils open TranslateCore @@ -16,18 +16,17 @@ let log = TranslateCore.log - the list of symbolic values used for the input values - the generated symbolic AST *) -type symbolic_fun_translation = V.symbolic_value list * SA.expression +type symbolic_fun_translation = symbolic_value list * SA.expression (** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs, for the forward function and the backward functions. *) -let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl) - : symbolic_fun_translation option = +let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : + symbolic_fun_translation option = (* Debug *) log#ldebug (lazy - ("translate_function_to_symbolics: " - ^ Print.fun_name_to_string fdef.A.name)); + ("translate_function_to_symbolics: " ^ name_to_string trans_ctx fdef.name)); match fdef.body with | None -> None @@ -45,12 +44,11 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl) *) let translate_function_to_pure (trans_ctx : trans_ctx) (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdNotLoopMap.t) - (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl) - : pure_fun_translation_no_loops = + (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : fun_decl) : + pure_fun_translation_no_loops = (* Debug *) log#ldebug - (lazy - ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name)); + (lazy ("translate_function_to_pure: " ^ name_to_string trans_ctx fdef.name)); let def_id = fdef.def_id in @@ -61,22 +59,24 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Initialize the context *) let forward_sig = - RegularFunIdNotLoopMap.find (E.FRegular def_id, None) fun_sigs + RegularFunIdNotLoopMap.find (FRegular def_id, None) fun_sigs in - let sv_to_var = V.SymbolicValueId.Map.empty in + let sv_to_var = SymbolicValueId.Map.empty in let var_counter = Pure.VarId.generator_zero in let state_var, var_counter = Pure.VarId.fresh var_counter in let back_state_var, var_counter = Pure.VarId.fresh var_counter in let fuel0, var_counter = Pure.VarId.fresh var_counter in let fuel, var_counter = Pure.VarId.fresh var_counter in - let calls = V.FunCallId.Map.empty in - let abstractions = V.AbstractionId.Map.empty in + let calls = FunCallId.Map.empty in + let abstractions = AbstractionId.Map.empty in let recursive_type_decls = - T.TypeDeclId.Set.of_list + TypeDeclId.Set.of_list (List.filter_map (fun (tid, g) -> - match g with Charon.GAst.NonRec _ -> None | Rec _ -> Some tid) - (T.TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups)) + match g with + | Charon.GAst.NonRecGroup _ -> None + | RecGroup _ -> Some tid) + (TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups)) in let type_context = { @@ -104,9 +104,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx) *) let loop_ids_map = match symbolic_trans with - | None -> V.LoopId.Map.empty + | None -> LoopId.Map.empty | Some (_, ast) -> - let m = ref V.LoopId.Map.empty in + let m = ref LoopId.Map.empty in let _, fresh_loop_id = Pure.LoopId.fresh_stateful_generator () in let visitor = @@ -115,10 +115,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx) method! visit_loop env loop = let _ = - match V.LoopId.Map.find_opt loop.loop_id !m with + match LoopId.Map.find_opt loop.loop_id !m with | Some _ -> () - | None -> - m := V.LoopId.Map.add loop.loop_id (fresh_loop_id ()) !m + | None -> m := LoopId.Map.add loop.loop_id (fresh_loop_id ()) !m in super#visit_loop env loop end @@ -148,9 +147,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx) fun_decl = fdef; forward_inputs = []; (* Empty for now *) - backward_inputs = T.RegionGroupId.Map.empty; + backward_inputs = RegionGroupId.Map.empty; (* Empty for now *) - backward_outputs = T.RegionGroupId.Map.empty; + backward_outputs = RegionGroupId.Map.empty; loop_backward_outputs = None; (* Empty for now *) calls; @@ -171,7 +170,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) | Some body, Some (input_svs, _) -> let forward_input_vars = LlbcAstUtils.fun_body_get_input_vars body in let forward_input_varnames = - List.map (fun (v : A.var) -> v.name) forward_input_vars + List.map (fun (v : var) -> v.name) forward_input_vars in let input_svs = List.combine forward_input_varnames input_svs in let ctx, forward_inputs = @@ -189,7 +188,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) in (* Translate the backward functions *) - let translate_backward (rg : T.region_group) : Pure.fun_decl = + let translate_backward (rg : region_group) : Pure.fun_decl = (* For the backward inputs/outputs initialization: we use the fact that * there are no nested borrows for now, and so that the region groups * can't have parents *) @@ -244,10 +243,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx) SymbolicToPure.fresh_vars backward_outputs ctx in let backward_inputs = - T.RegionGroupId.Map.singleton back_id backward_inputs + RegionGroupId.Map.singleton back_id backward_inputs in let backward_outputs = - T.RegionGroupId.Map.singleton back_id backward_outputs + RegionGroupId.Map.singleton back_id backward_outputs in (* Put everything in the context *) @@ -274,7 +273,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (pure_forward, pure_backwards) (* TODO: factor out the return type *) -let translate_crate_to_pure (crate : A.crate) : +let translate_crate_to_pure (crate : crate) : trans_ctx * Pure.type_decl list * pure_fun_translation list @@ -287,9 +286,7 @@ let translate_crate_to_pure (crate : A.crate) : let trans_ctx = compute_contexts crate in (* Translate all the type definitions *) - let type_decls = - SymbolicToPure.translate_type_decls (T.TypeDeclId.Map.values crate.types) - in + let type_decls = SymbolicToPure.translate_type_decls trans_ctx in (* Compute the type definition map *) let type_decls_map = @@ -301,24 +298,24 @@ let translate_crate_to_pure (crate : A.crate) : let assumed_sigs = List.map (fun (info : Assumed.assumed_fun_info) -> - ( E.FAssumed info.fun_id, + ( FAssumed info.fun_id, List.map (fun _ -> None) info.fun_sig.inputs, info.fun_sig )) Assumed.assumed_fun_infos in let local_sigs = List.map - (fun (fdef : A.fun_decl) -> + (fun (fdef : fun_decl) -> let input_names = match fdef.body with | None -> List.map (fun _ -> None) fdef.signature.inputs | Some body -> List.map - (fun (v : A.var) -> v.name) + (fun (v : var) -> v.name) (LlbcAstUtils.fun_body_get_input_vars body) in - (E.FRegular fdef.def_id, input_names, fdef.signature)) - (A.FunDeclId.Map.values crate.functions) + (FRegular fdef.def_id, input_names, fdef.signature)) + (FunDeclId.Map.values crate.fun_decls) in let sigs = List.append assumed_sigs local_sigs in let fun_sigs = SymbolicToPure.translate_fun_signatures trans_ctx sigs in @@ -327,22 +324,21 @@ let translate_crate_to_pure (crate : A.crate) : let pure_translations = List.map (translate_function_to_pure trans_ctx fun_sigs type_decls_map) - (A.FunDeclId.Map.values crate.functions) + (FunDeclId.Map.values crate.fun_decls) in (* Translate the trait declarations *) - let type_infos = trans_ctx.type_ctx.type_infos in let trait_decls = List.map - (SymbolicToPure.translate_trait_decl type_infos) - (T.TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) + (SymbolicToPure.translate_trait_decl trans_ctx) + (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) in (* Translate the trait implementations *) let trait_impls = List.map - (SymbolicToPure.translate_trait_impl type_infos) - (T.TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) + (SymbolicToPure.translate_trait_impl trans_ctx) + (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) in (* Apply the micro-passes *) @@ -401,9 +397,9 @@ let crate_has_opaque_non_builtin_decls (ctx : gen_ctx) (filter_assumed : bool) : log#ldebug (lazy ("Opaque decls:" ^ "\n- types:\n" - ^ String.concat ",\n" (List.map T.show_type_decl types) + ^ String.concat ",\n" (List.map show_type_decl types) ^ "\n- functions:\n" - ^ String.concat ",\n" (List.map A.show_fun_decl funs))); + ^ String.concat ",\n" (List.map show_fun_decl funs))); (types <> [], funs <> []) (** Export a type declaration. @@ -481,7 +477,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) let types_map = builtin_types_map () in List.map (fun (def : Pure.type_decl) -> - let sname = name_to_simple_name def.name in + let sname = name_to_simple_name def.llbc_name in SimpleNameMap.find_opt sname types_map <> None) defs in @@ -531,10 +527,10 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) TODO: check correct behavior with opaque globals. *) let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) - (id : A.GlobalDeclId.id) : unit = + (id : GlobalDeclId.id) : unit = let global_decls = ctx.trans_ctx.global_ctx.global_decls in - let global = A.GlobalDeclId.Map.find id global_decls in - let trans = A.FunDeclId.Map.find global.body_id ctx.trans_funs in + let global = GlobalDeclId.Map.find id global_decls in + let trans = FunDeclId.Map.find global.body ctx.trans_funs in assert (trans.fwd.loops = []); assert (trans.backs = []); let body = trans.fwd.f in @@ -665,7 +661,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let funs_map = builtin_funs_map () in List.map (fun (trans : pure_fun_translation) -> - let sname = name_to_simple_name trans.fwd.f.basename in + let sname = name_to_simple_name trans.fwd.f.llbc_name in SimpleNameMap.find_opt sname funs_map <> None) pure_ls in @@ -756,10 +752,10 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let export_trait_decl (fmt : Format.formatter) (_config : gen_config) (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) (extract_decl : bool) (extract_extra_info : bool) : unit = - let trait_decl = T.TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in + let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in (* Check if the trait declaration is builtin, in which case we ignore it *) let open ExtractBuiltin in - let sname = name_to_simple_name trait_decl.name in + let sname = name_to_simple_name trait_decl.llbc_name in if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then ( let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in if extract_decl then Extract.extract_trait_decl ctx fmt trait_decl; @@ -771,7 +767,7 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config) let export_trait_impl (fmt : Format.formatter) (_config : gen_config) (ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit = (* Lookup the definition *) - let trait_impl = T.TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in + let trait_impl = TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in let trait_decl = Pure.TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id ctx.trans_trait_decls @@ -779,8 +775,8 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config) (* Check if the trait implementation is builtin *) let builtin_info = let open ExtractBuiltin in - let type_sname = name_to_simple_name trait_impl.name in - let trait_sname = name_to_simple_name trait_decl.name in + let type_sname = name_to_simple_name trait_impl.llbc_name in + let trait_sname = name_to_simple_name trait_decl.llbc_name in SimpleNamePairMap.find_opt (type_sname, trait_sname) (builtin_trait_impls_map ()) in @@ -817,14 +813,15 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) Extract.extract_state_type fmt ctx kind in - let export_decl_group (dg : A.declaration_group) : unit = + let export_decl_group (dg : declaration_group) : unit = match dg with - | Type (NonRec id) -> + | TypeGroup (NonRecGroup id) -> if config.extract_types then export_types_group false [ id ] - | Type (Rec ids) -> if config.extract_types then export_types_group true ids - | Fun (NonRec id) -> ( + | TypeGroup (RecGroup ids) -> + if config.extract_types then export_types_group true ids + | FunGroup (NonRecGroup id) -> ( (* Lookup *) - let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in + let pure_fun = FunDeclId.Map.find id ctx.trans_funs in (* Special case: we skip trait method *declarations* (we will extract their type directly in the records we generate for the trait declarations themselves, there is no point in having @@ -834,21 +831,21 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) | _ -> (* Translate *) export_functions_group [ pure_fun ]) - | Fun (Rec ids) -> + | FunGroup (RecGroup ids) -> (* General case of mutually recursive functions *) (* Lookup *) let pure_funs = - List.map (fun id -> A.FunDeclId.Map.find id ctx.trans_funs) ids + List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids in (* Translate *) export_functions_group pure_funs - | Global id -> export_global id - | TraitDecl id -> + | GlobalGroup id -> export_global id + | TraitDeclGroup id -> (* TODO: update to extract groups *) if config.extract_trait_decls && config.extract_transparent then ( export_trait_decl_group id; export_trait_decl_group_extra_info id) - | TraitImpl id -> + | TraitImplGroup id -> if config.extract_trait_impls && config.extract_transparent then export_trait_impl id in @@ -986,7 +983,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) close_out out (** Translate a crate and write the synthesized code to an output file. *) -let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : +let translate_crate (filename : string) (dest_dir : string) (crate : crate) : unit = (* Translate the module to the pure AST *) let trans_ctx, trans_types, trans_funs, trans_trait_decls, trans_trait_impls = @@ -1036,8 +1033,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : Pure.TypeDeclId.Map.of_list (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types) in - let trans_funs : pure_fun_translation A.FunDeclId.Map.t = - A.FunDeclId.Map.of_list + let trans_funs : pure_fun_translation FunDeclId.Map.t = + FunDeclId.Map.of_list (List.map (fun (trans : pure_fun_translation) -> (trans.fwd.f.def_id, trans)) trans_funs) @@ -1046,13 +1043,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (* Put everything in the context *) let ctx = let trans_trait_decls = - T.TraitDeclId.Map.of_list + TraitDeclId.Map.of_list (List.map (fun (d : Pure.trait_decl) -> (d.def_id, d)) trans_trait_decls) in let trans_trait_impls = - T.TraitImplId.Map.of_list + TraitImplId.Map.of_list (List.map (fun (d : Pure.trait_impl) -> (d.def_id, d)) trans_trait_impls) @@ -1107,12 +1104,12 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : if is_global then ctx else Extract.extract_fun_decl_register_names ctx gen_decr_clause trans) ctx - (A.FunDeclId.Map.values trans_funs) + (FunDeclId.Map.values trans_funs) in let ctx = List.fold_left Extract.extract_global_decl_register_names ctx - (A.GlobalDeclId.Map.values crate.globals) + (GlobalDeclId.Map.values crate.global_decls) in let ctx = @@ -1291,7 +1288,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : namespace; in_namespace = true; crate_name; - rust_module_name = crate.A.name; + rust_module_name = crate.name; module_name = types_module; custom_msg = ": type definitions"; custom_imports = []; @@ -1319,7 +1316,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : namespace; in_namespace = true; crate_name; - rust_module_name = crate.A.name; + rust_module_name = crate.name; module_name = template_clauses_module; custom_msg = ": templates for the decreases clauses"; custom_imports = [ types_module ]; @@ -1369,7 +1366,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : namespace; in_namespace = false; crate_name; - rust_module_name = crate.A.name; + rust_module_name = crate.name; module_name = opaque_module; custom_msg; custom_imports = []; @@ -1408,7 +1405,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : namespace; in_namespace = true; crate_name; - rust_module_name = crate.A.name; + rust_module_name = crate.name; module_name = fun_module; custom_msg = ": function definitions"; custom_imports = []; @@ -1441,7 +1438,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : namespace; in_namespace = true; crate_name; - rust_module_name = crate.A.name; + rust_module_name = crate.name; module_name = crate_name; custom_msg = ""; custom_imports = []; diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml index a148175d..a974cdee 100644 --- a/compiler/TranslateCore.ml +++ b/compiler/TranslateCore.ml @@ -26,3 +26,6 @@ let trans_ctx_to_fmt_env (ctx : trans_ctx) : Print.fmt_env = let trans_ctx_to_pure_fmt_env (ctx : trans_ctx) : PrintPure.fmt_env = PrintPure.decls_ctx_to_fmt_env ctx + +let name_to_string (ctx : trans_ctx) = + Print.Types.name_to_string (trans_ctx_to_fmt_env ctx) diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml index 659eac59..5371a3d7 100644 --- a/compiler/TypesAnalysis.ml +++ b/compiler/TypesAnalysis.ml @@ -283,7 +283,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos) let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t) (infos : type_infos) (decl : A.type_declaration_group) : type_infos = (* Collect the identifiers used in the declaration group *) - let ids = match decl with NonRec id -> [ id ] | Rec ids -> ids in + let ids = match decl with NonRecGroup id -> [ id ] | RecGroup ids -> ids in (* Retrieve the type definitions *) let decl_defs = List.map (fun id -> TypeDeclId.Map.find id type_decls) ids in (* Initialize the type information for the current definitions *) -- cgit v1.3.1 From 9ab6a034aaadacac62d241474af3cf28bf6ac928 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 16 Nov 2023 10:52:28 +0100 Subject: Update SymbolicToPure.eliminate_box_functions --- compiler/PureMicroPasses.ml | 75 +++++++++++++++++++++++++++------------------ 1 file changed, 45 insertions(+), 30 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 2106c206..50a50815 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1546,38 +1546,53 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = | ArrayRepeat ), _ ) -> super#visit_texpression env e) - | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> - failwith "TODO" - (* + | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> ( + (* TODO: use a more general matching mechanism *) (* Lookup the function name *) let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in - match - (Names.name_no_disambiguators_to_string def.name, rg_id) - with - | "alloc::boxed::Box::deref", None -> - (* [Box::deref] forward is the identity *) - let arg, args = Collections.List.pop args in - mk_apps arg args - | "alloc::boxed::Box::deref", Some _ -> - (* [Box::deref] backward is [()] (doesn't give back anything) *) - assert (args = []); - mk_unit_rvalue - | "alloc::boxed::Box::deref_mut", None -> - (* [Box::deref_mut] forward is the identity *) - let arg, args = Collections.List.pop args in - mk_apps arg args - | "alloc::boxed::Box::deref_mut", Some _ -> - (* [Box::deref_mut] back is almost the identity: - * let box_deref_mut (x_init : t) (x_back : t) : t = x_back - * *) - let arg, args = - match args with - | _ :: given_back :: args -> (given_back, args) - | _ -> raise (Failure "Unreachable") - in - mk_apps arg args - | _ -> super#visit_texpression env e - *) + (* We first need to check if the name is "alloc::boxed::Box::_" *) + match def.name with + | [ + PeIdent ("alloc", _); + PeIdent ("boxed", _); + PeImpl impl; + PeIdent (fname, _); + ] -> ( + match impl.ty with + | TAdt + ( TAssumed TBox, + { + regions = []; + types = [ TVar _ ]; + const_generics = []; + trait_refs = []; + } ) -> ( + match (fname, rg_id) with + | "deref", None -> + (* [Box::deref] forward is the identity *) + let arg, args = Collections.List.pop args in + mk_apps arg args + | "deref", Some _ -> + (* [Box::deref] backward is [()] (doesn't give back anything) *) + assert (args = []); + mk_unit_rvalue + | "deref_mut", None -> + (* [Box::deref_mut] forward is the identity *) + let arg, args = Collections.List.pop args in + mk_apps arg args + | "deref_mut", Some _ -> + (* [Box::deref_mut] back is almost the identity: + * let box_deref_mut (x_init : t) (x_back : t) : t = x_back + * *) + let arg, args = + match args with + | _ :: given_back :: args -> (given_back, args) + | _ -> raise (Failure "Unreachable") + in + mk_apps arg args + | _ -> super#visit_texpression env e) + | _ -> super#visit_texpression env e) + | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e end -- cgit v1.3.1 From 5aa37b3a0a539f9ae37a119b9ce7c8dee504125e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Nov 2023 22:38:58 +0100 Subject: Fix minor issues --- compiler/ExtractBuiltin.ml | 2 -- compiler/PureMicroPasses.ml | 66 +++++++++------------------------------------ 2 files changed, 13 insertions(+), 55 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index d15905a2..106451cc 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -331,8 +331,6 @@ let builtin_fun_effects = (* TODO: redundancy with the funs information below *) "alloc::vec::{alloc::vec::Vec<@T>}::new"; "alloc::vec::{alloc::vec::Vec<@T>}::len"; - "alloc::boxed::{Box<@T>}::deref"; - "alloc::boxed::{Box<@T>}::deref_mut"; "core::mem::replace"; "core::mem::take"; ] diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 50a50815..96421925 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1250,6 +1250,7 @@ let filter_if_backward_with_no_outputs (def : fun_decl) : fun_decl option = !Config.filter_useless_functions && Option.is_some def.back_id && def.signature.output = mk_result_ty mk_unit_ty + || def.signature.output = mk_unit_ty then None else Some def @@ -1508,8 +1509,8 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl = let body = Some { body with body = body_exp; inputs_lvs } in { def with body } -(** Eliminate the box functions like [Box::new], [Box::deref], etc. Most of them - are translated to identity, and [Box::free] is translated to [()]. +(** Eliminate the box functions like [Box::new] (which is translated to the + identity) and [Box::free] (which is translated to [()]). Note that the box types have already been eliminated during the translation from symbolic to pure. @@ -1518,7 +1519,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl = function calls, and when translating end abstractions. Here, we can do something simpler, in one micro-pass. *) -let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = +let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = (* The map visitor *) let obj = object @@ -1546,53 +1547,6 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = | ArrayRepeat ), _ ) -> super#visit_texpression env e) - | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> ( - (* TODO: use a more general matching mechanism *) - (* Lookup the function name *) - let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in - (* We first need to check if the name is "alloc::boxed::Box::_" *) - match def.name with - | [ - PeIdent ("alloc", _); - PeIdent ("boxed", _); - PeImpl impl; - PeIdent (fname, _); - ] -> ( - match impl.ty with - | TAdt - ( TAssumed TBox, - { - regions = []; - types = [ TVar _ ]; - const_generics = []; - trait_refs = []; - } ) -> ( - match (fname, rg_id) with - | "deref", None -> - (* [Box::deref] forward is the identity *) - let arg, args = Collections.List.pop args in - mk_apps arg args - | "deref", Some _ -> - (* [Box::deref] backward is [()] (doesn't give back anything) *) - assert (args = []); - mk_unit_rvalue - | "deref_mut", None -> - (* [Box::deref_mut] forward is the identity *) - let arg, args = Collections.List.pop args in - mk_apps arg args - | "deref_mut", Some _ -> - (* [Box::deref_mut] back is almost the identity: - * let box_deref_mut (x_init : t) (x_back : t) : t = x_back - * *) - let arg, args = - match args with - | _ :: given_back :: args -> (given_back, args) - | _ -> raise (Failure "Unreachable") - in - mk_apps arg args - | _ -> super#visit_texpression env e) - | _ -> super#visit_texpression env e) - | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e end @@ -1966,11 +1920,17 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : * Note that the calls to those functions should already have been removed, * when translating from symbolic to pure. Here, we remove the definitions * altogether, because they are now useless *) - let def = filter_if_backward_with_no_outputs def in + let name = def.name ^ PrintPure.fun_suffix def.loop_id def.back_id in + let opt_def = filter_if_backward_with_no_outputs def in - match def with - | None -> None + match opt_def with + | None -> + log#ldebug (lazy ("filtered (backward with no outputs): " ^ name ^ "\n")); + None | Some def -> + log#ldebug + (lazy ("not filtered (not backward with no outputs): " ^ name ^ "\n")); + (* Extract the loop definitions by removing the {!Loop} node *) let def, loops = decompose_loops def in -- cgit v1.3.1 From e94cd72ffa63dbc5fc40c7c1a422c1a70ba4a7e5 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 13:55:46 +0100 Subject: Add an `is_local` field to declarations --- compiler/Pure.ml | 4 ++++ compiler/PureMicroPasses.ml | 1 + compiler/PureUtils.ml | 2 ++ compiler/SymbolicToPure.ml | 8 +++++++- compiler/dune | 4 ++-- 5 files changed, 16 insertions(+), 3 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 40711e53..ebcaa68d 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -381,6 +381,7 @@ type predicates = { trait_type_constraints : trait_type_constraint list } type type_decl = { def_id : TypeDeclId.id; + is_local : bool; llbc_name : llbc_name; (** The original name coming from the LLBC declaration *) name : string; @@ -991,6 +992,7 @@ type fun_kind = A.fun_kind [@@deriving show] type fun_decl = { def_id : FunDeclId.id; + is_local : bool; kind : fun_kind; num_loops : int; (** The number of loops in the parent forward function (basically the number @@ -1014,6 +1016,7 @@ type fun_decl = { type trait_decl = { def_id : trait_decl_id; + is_local : bool; llbc_name : llbc_name; name : string; generics : generic_params; @@ -1028,6 +1031,7 @@ type trait_decl = { type trait_impl = { def_id : trait_impl_id; + is_local : bool; llbc_name : llbc_name; name : string; impl_trait : trait_decl_ref; diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 96421925..1565f252 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1427,6 +1427,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = let loop_def : fun_decl = { def_id = def.def_id; + is_local = def.is_local; kind = def.kind; num_loops; loop_id = Some loop.loop_id; diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 06270621..d410abdc 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -646,6 +646,7 @@ let trait_decl_get_method (trait_decl : trait_decl) (method_name : string) : let trait_decl_is_empty (trait_decl : trait_decl) : bool = let { def_id = _; + is_local = _; name = _; llbc_name = _; generics = _; @@ -664,6 +665,7 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool = let trait_impl_is_empty (trait_impl : trait_impl) : bool = let { def_id = _; + is_local = _; name = _; llbc_name = _; impl_trait = _; diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index f25ff2f6..9899a0c6 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -495,7 +495,8 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : let generics = { types; const_generics; trait_clauses } in let kind = translate_type_decl_kind def.T.kind in let preds = translate_predicates def.preds in - { def_id; llbc_name; name; generics; kind; preds } + let is_local = def.is_local in + { def_id; is_local; llbc_name; name; generics; kind; preds } let translate_type_id (id : T.type_id) : type_id = match id with @@ -3026,6 +3027,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = let def : fun_decl = { def_id; + is_local = def.is_local; kind = def.kind; num_loops; loop_id; @@ -3104,6 +3106,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) : trait_decl = let { def_id; + is_local; name = llbc_name; generics; preds; @@ -3139,6 +3142,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) in { def_id; + is_local; llbc_name; name; generics; @@ -3154,6 +3158,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) : trait_impl = let { A.def_id; + is_local; name = llbc_name; impl_trait; generics; @@ -3193,6 +3198,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) in { def_id; + is_local; llbc_name; name; impl_trait; diff --git a/compiler/dune b/compiler/dune index 4bba6a08..0d0a8017 100644 --- a/compiler/dune +++ b/compiler/dune @@ -84,7 +84,7 @@ -g ;-dsource -warn-error - -5@8-9-11-14-33-20-21-26-27-39)) + -5@8-11-14-33-20-21-26-27-39)) (release (flags :standard @@ -92,4 +92,4 @@ -g ;-dsource -warn-error - -5@8-9-11-14-33-20-21-26-27-39))) + -5@8-11-14-33-20-21-26-27-39))) -- cgit v1.3.1 From 77ba13b371cccbe8098e432ebd287108d5373666 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 14:43:12 +0100 Subject: Add span information to the generated code --- compiler/Extract.ml | 31 +++++++++++++++++++------------ compiler/ExtractTypes.ml | 15 ++++++++++++++- compiler/InterpreterLoops.ml | 12 +++++++----- compiler/InterpreterLoops.mli | 3 ++- compiler/InterpreterStatements.ml | 2 +- compiler/PrintPure.ml | 4 ++-- compiler/Pure.ml | 13 +++++++++++-- compiler/PureMicroPasses.ml | 9 ++++++--- compiler/PureUtils.ml | 6 ++++-- compiler/SymbolicAst.ml | 13 +++++++------ compiler/SymbolicToPure.ml | 21 ++++++++++++++------- compiler/SynthesizeSymbolic.ml | 7 ++++--- 12 files changed, 91 insertions(+), 45 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index fb3364f4..d7b4c152 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1135,8 +1135,9 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment fmt - [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]; + extract_comment_with_span fmt + [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ] + def.meta.span; F.pp_print_space fmt (); (* Open a box for the definition, so that whenever possible it gets printed on * one line *) @@ -1197,8 +1198,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment fmt - [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]; + extract_comment_with_span fmt + [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ] + def.meta.span; F.pp_print_space fmt (); (* Open a box for the definition, so that whenever possible it gets printed on * one line *) @@ -1251,8 +1253,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) let def_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in (* syntax term ... term : tactic *) F.pp_print_break fmt 0 0; - extract_comment fmt - [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]; + extract_comment_with_span fmt + [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ] + def.meta.span; F.pp_print_space fmt (); F.pp_open_hvbox fmt 0; F.pp_print_string fmt "syntax \""; @@ -1313,7 +1316,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter) | [ s ] -> [ comment_pre ^ loop_comment ^ s ] | s :: sl -> (comment_pre ^ loop_comment ^ s) :: sl in - extract_comment fmt comment + extract_comment_with_span fmt comment def.meta.span (** Extract a function declaration. @@ -1765,7 +1768,9 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; - extract_comment fmt [ "[" ^ name_to_string ctx global.name ^ "]" ]; + extract_comment_with_span fmt + [ "[" ^ name_to_string ctx global.name ^ "]" ] + global.meta.span; F.pp_print_space fmt (); let decl_name = ctx_get_global global.def_id ctx in @@ -2190,8 +2195,9 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment fmt - [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]; + extract_comment_with_span fmt + [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ] + decl.meta.span; F.pp_print_break fmt 0 0; (* Open two outer boxes for the definition, so that whenever possible it gets printed on one line and indents are correct. @@ -2478,8 +2484,9 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment fmt - [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]; + extract_comment_with_span fmt + [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ] + impl.meta.span; F.pp_print_break fmt 0 0; (* Open two outer boxes for the definition, so that whenever possible it gets printed on diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index a74bd532..4dcefabc 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -1813,6 +1813,17 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit = F.pp_print_string fmt rd; F.pp_close_box fmt () +let extract_comment_with_span (fmt : F.formatter) (sl : string list) + (span : Meta.span) : unit = + let file = match span.file with Virtual s | Local s -> s in + let span = + "Source: '" ^ file ^ "': lines " + ^ string_of_int span.beg_loc.line + ^ "-" + ^ string_of_int span.end_loc.line + in + extract_comment fmt (sl @ [ span ]) + let extract_trait_clause_type (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit = let trait_name = ctx_get_trait_decl clause.trait_id ctx in @@ -2034,7 +2045,9 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) if !backend <> HOL4 || not (decl_is_first_from_group kind) then F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]; + extract_comment_with_span fmt + [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ] + def.meta.span; F.pp_print_break fmt 0 0; (* Open a box for the definition, so that whenever possible it gets printed on * one line. Note however that in the case of Lean line breaks are important diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index f88fc977..ed2a9587 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -2,6 +2,7 @@ open Types open Values open Contexts open ValuesUtils +open Meta module S = SynthesizeSymbolic open Cps open InterpreterUtils @@ -60,8 +61,8 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun = eval_loop_body reeval_loop_body ctx (** Evaluate a loop in symbolic mode *) -let eval_loop_symbolic (config : config) (eval_loop_body : st_cm_fun) : - st_cm_fun = +let eval_loop_symbolic (config : config) (meta : meta) + (eval_loop_body : st_cm_fun) : st_cm_fun = fun cf ctx -> (* Debug *) log#ldebug @@ -205,9 +206,10 @@ let eval_loop_symbolic (config : config) (eval_loop_body : st_cm_fun) : (* Put together *) S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back end_expr - loop_expr + loop_expr meta -let eval_loop (config : config) (eval_loop_body : st_cm_fun) : st_cm_fun = +let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) : + st_cm_fun = fun cf ctx -> match config.mode with | ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx @@ -231,4 +233,4 @@ let eval_loop (config : config) (eval_loop_body : st_cm_fun) : st_cm_fun = *non-fixed* abstractions. *) let cc = prepare_ashared_loans None in - comp cc (eval_loop_symbolic config eval_loop_body) cf ctx + comp cc (eval_loop_symbolic config meta eval_loop_body) cf ctx diff --git a/compiler/InterpreterLoops.mli b/compiler/InterpreterLoops.mli index 320e4bcb..03633861 100644 --- a/compiler/InterpreterLoops.mli +++ b/compiler/InterpreterLoops.mli @@ -58,6 +58,7 @@ open Contexts open Cps +open Meta (** Evaluate a loop *) -val eval_loop : config -> st_cm_fun -> st_cm_fun +val eval_loop : config -> meta -> st_cm_fun -> st_cm_fun diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index e8069e31..9ea5387f 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -739,7 +739,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = (* Compose and apply *) comp cf_st1 cf_st2 cf ctx | Loop loop_body -> - InterpreterLoops.eval_loop config + InterpreterLoops.eval_loop config st.meta (eval_statement config loop_body) cf ctx | Switch switch -> eval_switch config switch cf ctx diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 49e74b6c..5d8297d3 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -590,7 +590,7 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string) "[ " ^ String.concat ", " fields ^ " ]" | _ -> raise (Failure "Unexpected")) | Meta (meta, e) -> ( - let meta_s = meta_to_string env meta in + let meta_s = emeta_to_string env meta in let e = texpression_to_string env inside indent indent_incr e in match meta with | Assignment _ | SymbolicAssignment _ | Tag _ -> @@ -724,7 +724,7 @@ and loop_to_string (env : fmt_env) (indent : string) (indent_incr : string) ^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1 ^ "}\n" ^ indent ^ "}" -and meta_to_string (env : fmt_env) (meta : meta) : string = +and emeta_to_string (env : fmt_env) (meta : emeta) : string = let meta = match meta with | Assignment (lp, rv, rp) -> diff --git a/compiler/Pure.ml b/compiler/Pure.ml index ebcaa68d..42f51075 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -48,6 +48,10 @@ type fun_decl_id = A.fun_decl_id [@@deriving show, ord] type loop_id = LoopId.id [@@deriving show, ord] type region_group_id = T.region_group_id [@@deriving show, ord] type mutability = Mut | Const [@@deriving show, ord] +type loc = Meta.loc [@@deriving show, ord] +type file_name = Meta.file_name [@@deriving show, ord] +type span = Meta.span [@@deriving show, ord] +type meta = Meta.meta [@@deriving show, ord] (** The assumed types for the pure AST. @@ -389,6 +393,7 @@ type type_decl = { the name used at extraction time will be derived from the llbc_name. *) + meta : meta; generics : generic_params; kind : type_decl_kind; preds : predicates; @@ -717,7 +722,7 @@ type expression = | Switch of texpression * switch_body | Loop of loop (** See the comments for {!loop} *) | StructUpdate of struct_update (** See the comments for {!struct_update} *) - | Meta of (meta[@opaque]) * texpression (** Meta-information *) + | Meta of (emeta[@opaque]) * texpression (** Meta-information *) and switch_body = If of texpression * texpression | Match of match_branch list and match_branch = { pat : typed_pattern; branch : texpression } @@ -736,6 +741,7 @@ and match_branch = { pat : typed_pattern; branch : texpression } and loop = { fun_end : texpression; loop_id : loop_id; + meta : meta; [@opaque] fuel0 : var_id; fuel : var_id; input_state : var_id option; @@ -791,7 +797,7 @@ and texpression = { e : expression; ty : ty } and mvalue = (texpression[@opaque]) (** Meta-information stored in the AST *) -and meta = +and emeta = | Assignment of mplace * mvalue * mplace option (** Information about an assignment which occured in LLBC. We use this to guide the heuristics which derive pretty names. @@ -993,6 +999,7 @@ type fun_kind = A.fun_kind [@@deriving show] type fun_decl = { def_id : FunDeclId.id; is_local : bool; + meta : meta; kind : fun_kind; num_loops : int; (** The number of loops in the parent forward function (basically the number @@ -1019,6 +1026,7 @@ type trait_decl = { is_local : bool; llbc_name : llbc_name; name : string; + meta : meta; generics : generic_params; preds : predicates; parent_clauses : trait_clause list; @@ -1034,6 +1042,7 @@ type trait_impl = { is_local : bool; llbc_name : llbc_name; name : string; + meta : meta; impl_trait : trait_decl_ref; generics : generic_params; preds : predicates; diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 1565f252..8463f56c 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -391,7 +391,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = | Switch (scrut, body) -> update_switch_body scrut body ctx | Loop loop -> update_loop loop ctx | StructUpdate supd -> update_struct_update supd ctx - | Meta (meta, e) -> update_meta meta e ctx + | Meta (meta, e) -> update_emeta meta e ctx in (ctx, { e; ty }) (* *) @@ -449,6 +449,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = let { fun_end; loop_id; + meta; fuel0; fuel; input_state; @@ -467,6 +468,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = { fun_end; loop_id; + meta; fuel0; fuel; input_state; @@ -490,7 +492,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = let supd = { struct_id; init; updates } in (ctx, StructUpdate supd) (* *) - and update_meta (meta : meta) (e : texpression) (ctx : pn_ctx) : + and update_emeta (meta : emeta) (e : texpression) (ctx : pn_ctx) : pn_ctx * expression = let ctx = match meta with @@ -516,7 +518,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = | Tag _ -> ctx in let ctx, e = update_texpression e ctx in - let e = mk_meta meta e in + let e = mk_emeta meta e in (ctx, e.e) in @@ -1428,6 +1430,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = { def_id = def.def_id; is_local = def.is_local; + meta = loop.meta; kind = def.kind; num_loops; loop_id = Some loop.loop_id; diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index d410abdc..992ea499 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -453,13 +453,13 @@ let mk_dummy_pattern (ty : ty) : typed_pattern = let value = PatDummy in { value; ty } -let mk_meta (m : meta) (e : texpression) : texpression = +let mk_emeta (m : emeta) (e : texpression) : texpression = let ty = e.ty in let e = Meta (m, e) in { e; ty } let mk_mplace_texpression (mp : mplace) (e : texpression) : texpression = - mk_meta (MPlace mp) e + mk_emeta (MPlace mp) e let mk_opt_mplace_texpression (mp : mplace option) (e : texpression) : texpression = @@ -649,6 +649,7 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool = is_local = _; name = _; llbc_name = _; + meta = _; generics = _; preds = _; parent_clauses; @@ -668,6 +669,7 @@ let trait_impl_is_empty (trait_impl : trait_impl) : bool = is_local = _; name = _; llbc_name = _; + meta = _; impl_trait = _; generics = _; preds = _; diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index c9820ba5..a9f45926 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -51,11 +51,10 @@ type call = { } [@@deriving show] -(** Meta information, not necessary for synthesis but useful to guide it to - generate a pretty output. +(** Meta information for expressions, not necessary for synthesis but useful to + guide it to generate a pretty output. *) - -type meta = +type emeta = | Assignment of Contexts.eval_ctx * mplace * typed_value * mplace option (** We generated an assignment (destination, assigned value, src) *) [@@deriving show] @@ -82,7 +81,8 @@ class ['self] iter_expression_base = fun _ _ -> () method visit_mplace : 'env -> mplace -> unit = fun _ _ -> () - method visit_meta : 'env -> meta -> unit = fun _ _ -> () + method visit_emeta : 'env -> emeta -> unit = fun _ _ -> () + method visit_meta : 'env -> Meta.meta -> unit = fun _ _ -> () method visit_region_group_id_map : 'a. ('env -> 'a -> unit) -> 'env -> 'a region_group_id_map -> unit = @@ -200,7 +200,7 @@ type expression = The boolean is [is_continue]. *) - | Meta of meta * expression (** Meta information *) + | Meta of emeta * expression (** Meta information *) and loop = { loop_id : loop_id; @@ -215,6 +215,7 @@ and loop = { end_expr : expression; (** The end of the function (upon the moment it enters the loop) *) loop_expr : expression; (** The symbolically executed loop body *) + meta : Meta.meta; (** Information about where the origin of the loop body *) } and expansion = diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 9899a0c6..5dee23db 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -496,7 +496,8 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : let kind = translate_type_decl_kind def.T.kind in let preds = translate_predicates def.preds in let is_local = def.is_local in - { def_id; is_local; llbc_name; name; generics; kind; preds } + let meta = def.meta in + { def_id; is_local; llbc_name; name; meta; generics; kind; preds } let translate_type_id (id : T.type_id) : type_id = match id with @@ -1489,11 +1490,11 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) : (call_info.forward, abs_ancestors) (** Add meta-information to an expression *) -let mk_meta_symbolic_assignments (vars : var list) (values : texpression list) +let mk_emeta_symbolic_assignments (vars : var list) (values : texpression list) (e : texpression) : texpression = let var_values = List.combine vars values in List.fold_right - (fun (var, arg) e -> mk_meta (SymbolicAssignment (var_get_id var, arg)) e) + (fun (var, arg) e -> mk_emeta (SymbolicAssignment (var_get_id var, arg)) e) var_values e let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = @@ -1509,7 +1510,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx | IntroSymbolic (ectx, p, sv, v, e) -> translate_intro_symbolic ectx p sv v e ctx - | Meta (meta, e) -> translate_meta meta e ctx + | Meta (meta, e) -> translate_emeta meta e ctx | ForwardEnd (ectx, loop_input_values, e, back_e) -> translate_forward_end ectx loop_input_values e back_e ctx | Loop loop -> translate_loop loop ctx @@ -2206,7 +2207,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) var_values in let vars, values = List.split var_values in - mk_meta_symbolic_assignments vars values next_e + mk_emeta_symbolic_assignments vars values next_e else next_e in @@ -2637,7 +2638,7 @@ and translate_forward_end (ectx : C.eval_ctx) We then remove all the meta information from the body *before* calling {!PureMicroPasses.decompose_loops}. *) - mk_meta_symbolic_assignments loop_info.input_vars org_args e + mk_emeta_symbolic_assignments loop_info.input_vars org_args e and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = let loop_id = V.LoopId.Map.find loop.loop_id ctx.loop_ids_map in @@ -2795,6 +2796,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = { fun_end; loop_id; + meta = loop.meta; fuel0 = ctx.fuel0; fuel = ctx.fuel; input_state; @@ -2810,7 +2812,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = let ty = fun_end.ty in { e = loop; ty } -and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) : +and translate_emeta (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) : texpression = let next_e = translate_expression e ctx in let meta = @@ -3028,6 +3030,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = { def_id; is_local = def.is_local; + meta = def.meta; kind = def.kind; num_loops; loop_id; @@ -3108,6 +3111,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) def_id; is_local; name = llbc_name; + meta; generics; preds; parent_clauses; @@ -3145,6 +3149,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) is_local; llbc_name; name; + meta; generics; preds; parent_clauses; @@ -3160,6 +3165,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) A.def_id; is_local; name = llbc_name; + meta; impl_trait; generics; preds; @@ -3201,6 +3207,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) is_local; llbc_name; name; + meta; impl_trait; generics; preds; diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 9e14a4d6..efcf001a 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -15,7 +15,7 @@ let mk_opt_place_from_op (op : operand) (ctx : Contexts.eval_ctx) : mplace option = match op with Copy p | Move p -> Some (mk_mplace p ctx) | Constant _ -> None -let mk_meta (m : meta) (e : expression) : expression = Meta (m, e) +let mk_emeta (m : emeta) (e : expression) : expression = Meta (m, e) let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option) (seel : symbolic_expansion option list) (el : expression list option) : @@ -163,8 +163,8 @@ let synthesize_forward_end (ctx : Contexts.eval_ctx) let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list) (fresh_svalues : SymbolicValueId.Set.t) (rg_to_given_back_tys : (RegionId.Set.t * ty list) RegionGroupId.Map.t) - (end_expr : expression option) (loop_expr : expression option) : - expression option = + (end_expr : expression option) (loop_expr : expression option) + (meta : Meta.meta) : expression option = match (end_expr, loop_expr) with | None, None -> None | Some end_expr, Some loop_expr -> @@ -177,5 +177,6 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list) rg_to_given_back_tys; end_expr; loop_expr; + meta; }) | _ -> raise (Failure "Unreachable") -- cgit v1.3.1 From ba66f35a0e196c17757e06187cf2563abec253e5 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 22 Nov 2023 09:09:46 +0100 Subject: Improve further the generation of parent clause/trait clause names --- compiler/Extract.ml | 33 +++++++++++--- compiler/ExtractBase.ml | 102 ++++++++++++++++++++++++++++++++------------ compiler/ExtractName.ml | 2 + compiler/ExtractTypes.ml | 5 ++- compiler/Pure.ml | 27 ++++++++++++ compiler/PureMicroPasses.ml | 8 +++- compiler/PureUtils.ml | 4 ++ compiler/SymbolicToPure.ml | 44 ++++++++++++++----- 8 files changed, 177 insertions(+), 48 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 16262c91..c8c16c08 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1044,7 +1044,8 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx) (* Add the type parameters - note that we need those bindings only for the * body translation (they are not top-level) *) let ctx, type_params, cg_params, trait_clauses = - ctx_add_generic_params def.signature.generics ctx + ctx_add_generic_params def.llbc_name def.signature.llbc_generics + def.signature.generics ctx in (* Print the generics *) (* Open a box for the generics *) @@ -1578,7 +1579,10 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) assert (def.signature.generics.const_generics = []); (* Add the type/const gen parameters - note that we need those bindings only for the generation of the type (they are not top-level) *) - let ctx, _, _, _ = ctx_add_generic_params def.signature.generics ctx in + let ctx, _, _, _ = + ctx_add_generic_params def.llbc_name def.signature.llbc_generics + def.signature.generics ctx + in (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0; (* Open a box for the whole definition *) @@ -2164,8 +2168,14 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) generic_params_drop_prefix ~drop_trait_clauses decl.generics f.signature.generics in + (* Note that we do not filter the LLBC generic parameters. + This is ok because: + - we only use them to find meaningful names for the trait clauses + - we only generate trait clauses for the clauses we find in the + pure generics *) let ctx, type_params, cg_params, trait_clauses = - ctx_add_generic_params generics ctx + ctx_add_generic_params f.llbc_name f.signature.llbc_generics generics + ctx in let backend_uses_forall = match !backend with Coq | Lean -> true | FStar | HOL4 -> false @@ -2229,7 +2239,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add the type and const generic params - note that we need those bindings only for the * body translation (they are not top-level) *) let ctx, type_params, cg_params, trait_clauses = - ctx_add_generic_params generics ctx + ctx_add_generic_params decl.llbc_name decl.llbc_generics generics ctx in extract_generic_params ctx fmt TypeDeclId.Set.empty generics type_params cg_params trait_clauses; @@ -2448,8 +2458,17 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) { impl.generics with types = impl_types } f_generics in - (* Register and print the quantified generics *) - let ctx, f_tys, f_cgs, f_tcs = ctx_add_generic_params f_generics ctx in + (* Register and print the quantified generics. + + Note that we do not filter the LLBC generic parameters. + This is ok because: + - we only use them to find meaningful names for the trait clauses + - we only generate trait clauses for the clauses we find in the + pure generics *) + let ctx, f_tys, f_cgs, f_tcs = + ctx_add_generic_params f.llbc_name f.signature.llbc_generics f_generics + ctx + in let use_forall = f_generics <> empty_generic_params in extract_generic_params ctx fmt TypeDeclId.Set.empty ~use_forall f_generics f_tys f_cgs f_tcs; @@ -2515,7 +2534,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (* Add the type and const generic params - note that we need those bindings only for the * body translation (they are not top-level) *) let ctx, type_params, cg_params, trait_clauses = - ctx_add_generic_params impl.generics ctx + ctx_add_generic_params impl.llbc_name impl.llbc_generics impl.generics ctx in let all_generics = (type_params, cg_params, trait_clauses) in extract_generic_params ctx fmt TypeDeclId.Set.empty impl.generics type_params diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index cfba7324..c6158847 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1488,13 +1488,8 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl) where the instance has been defined (it is indepedent of the file, etc.). *) let name = - (* We need to lookup the LLBC definitions, to have the original instantiation *) - let trait_impl = - TraitImplId.Map.find trait_impl.def_id - ctx.trans_ctx.trait_impls_ctx.trait_impls - in - let params = trait_impl.generics in - let args = trait_impl.impl_trait.decl_generics in + let params = trait_impl.llbc_generics in + let args = trait_impl.llbc_impl_trait.decl_generics in trait_name_with_generics_to_simple_name ctx.trans_ctx trait_decl.llbc_name params args in @@ -1508,15 +1503,29 @@ let ctx_compute_trait_decl_constructor (ctx : extraction_ctx) let name = ctx_compute_trait_decl_name ctx trait_decl in ExtractBuiltin.mk_struct_constructor name -let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx) - (trait_decl : trait_decl) (clause : trait_clause) : string = +(** Helper to derive names for parent trait clauses and for variables + for trait instances. + + We derive the name from the type of the clause (i.e., the trait ref + the clause implements). + For instance, if a trait clause is for the trait ref "Trait", + we generate a name like "traitBoxUsizeInst". This is more meaningful + that giving it a generic name with an index (such as "parent_clause_1" + or "inst3"). + + Because we want to be precise when deriving the name, we use the + original LLBC types, that is the types from before the translation + to pure, which simplifies types like boxes and references. + *) +let ctx_compute_trait_clause_name (ctx : extraction_ctx) + (current_def_name : Types.name) (params : Types.generic_params) + (clauses : Types.trait_clause list) (clause_id : trait_clause_id) : string = (* We derive the name of the clause from the trait instance. For instance, if the clause gives us an instance of `Foo`, we generate a name along the lines of "fooU32Inst". *) - (* We need to lookup the LLBC definitions, to have the original instantiation *) let clause = - (* If the current trait decl and the trait decl referenced by the clause + (* If the current def and the trait decl referenced by the clause are in the same namespace, we try to simplify the names. We do so by removing the common prefixes in their names. @@ -1530,23 +1539,33 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx) For the parent clause of trait [Child] we would like to generate the name: "ParentInst", rather than "traitParentInst". *) - let prefix = Some trait_decl.llbc_name in - let trait_decl = - TraitDeclId.Map.find trait_decl.def_id ctx.crate.trait_decls - in + let prefix = Some current_def_name in let clause = List.find - (fun (c : Types.trait_clause) -> c.clause_id = clause.clause_id) - trait_decl.parent_clauses + (fun (c : Types.trait_clause) -> c.clause_id = clause_id) + clauses in let trait_id = clause.trait_id in let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in - let params = trait_decl.generics in let args = clause.clause_generics in trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix impl_trait_decl.name params args in - let clause = String.concat "" clause in + String.concat "" clause + +let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx) + (trait_decl : trait_decl) (clause : trait_clause) : string = + (* We derive the name of the clause from the trait instance. + For instance, if the clause gives us an instance of `Foo`, + we generate a name along the lines of "fooU32Inst". + *) + (* We need to lookup the LLBC definitions, to have the original instantiation *) + let clause = + let current_def_name = trait_decl.llbc_name in + let params = trait_decl.llbc_generics in + ctx_compute_trait_clause_name ctx current_def_name params + trait_decl.llbc_parent_clauses clause.clause_id + in let clause = if !Config.record_fields_short_names then clause else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause @@ -1751,10 +1770,18 @@ let ctx_compute_const_generic_var_basename (_ctx : extraction_ctx) In the traduction we explicitely manipulate the trait clause instances, that is we introduce one input variable for each trait clause. *) -let ctx_compute_trait_clause_basename (_ctx : extraction_ctx) - (_clause : trait_clause) : string = - (* TODO: actually use the clause to derive the name *) - "inst" +let ctx_compute_trait_clause_basename (ctx : extraction_ctx) + (current_def_name : Types.name) (params : Types.generic_params) + (clause_id : trait_clause_id) : string = + (* This is similar to {!ctx_compute_trait_parent_clause_name}: we + derive the name from the trait reference (i.e., from the type) *) + let clause = + ctx_compute_trait_clause_name ctx current_def_name params + params.trait_clauses clause_id + in + match !backend with + | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter clause + | Lean -> clause let trait_self_clause_basename = "self_clause" @@ -1845,11 +1872,24 @@ let ctx_add_const_generic_params (vars : const_generic_var list) ctx_add_const_generic_var var.name var.index ctx) ctx vars -let ctx_add_local_trait_clauses (clauses : trait_clause list) +(** Returns the lists of names for: + - the type variables + - the const generic variables + - the trait clauses + + For the [current_name_def] and the [llbc_generics]: we use them to derive + pretty names for the trait clauses. See {!ctx_compute_trait_clause_name} + for additional information. + *) +let ctx_add_local_trait_clauses (current_def_name : Types.name) + (llbc_generics : Types.generic_params) (clauses : trait_clause list) (ctx : extraction_ctx) : extraction_ctx * string list = List.fold_left_map (fun ctx (c : trait_clause) -> - let basename = ctx_compute_trait_clause_basename ctx c in + let basename = + ctx_compute_trait_clause_basename ctx current_def_name llbc_generics + c.clause_id + in ctx_add_local_trait_clause basename c.clause_id ctx) ctx clauses @@ -1857,13 +1897,21 @@ let ctx_add_local_trait_clauses (clauses : trait_clause list) - the type variables - the const generic variables - the trait clauses + + For the [current_name_def] and the [llbc_generics]: we use them to derive + pretty names for the trait clauses. See {!ctx_compute_trait_clause_name} + for additional information. *) -let ctx_add_generic_params (generics : generic_params) (ctx : extraction_ctx) : +let ctx_add_generic_params (current_def_name : Types.name) + (llbc_generics : Types.generic_params) (generics : generic_params) + (ctx : extraction_ctx) : extraction_ctx * string list * string list * string list = let { types; const_generics; trait_clauses } = generics in let ctx, tys = ctx_add_type_params types ctx in let ctx, cgs = ctx_add_const_generic_params const_generics ctx in - let ctx, tcs = ctx_add_local_trait_clauses trait_clauses ctx in + let ctx, tcs = + ctx_add_local_trait_clauses current_def_name llbc_generics trait_clauses ctx + in (ctx, tys, cgs, tcs) let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) : diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml index f7177223..0943aefe 100644 --- a/compiler/ExtractName.ml +++ b/compiler/ExtractName.ml @@ -2,6 +2,8 @@ open Charon.NameMatcher +let log = Logging.extract_log + module NameMatcherMap = struct type 'a t = (pattern * 'a) list diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index c9be5abe..c6212d31 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -1272,7 +1272,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* Add the type and const generic params - note that we need those bindings only for the * body translation (they are not top-level) *) let ctx_body, type_params, cg_params, trait_clauses = - ctx_add_generic_params def.generics ctx + ctx_add_generic_params def.llbc_name def.llbc_generics def.generics ctx in (* Add a break before *) if !backend <> HOL4 || not (decl_is_first_from_group kind) then @@ -1515,7 +1515,8 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) if is_rec then (* Add the type params *) let ctx, type_params, cg_params, trait_clauses = - ctx_add_generic_params decl.generics ctx + ctx_add_generic_params decl.llbc_name decl.llbc_generics decl.generics + ctx in 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 diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 42f51075..50849df9 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -395,6 +395,12 @@ type type_decl = { *) meta : meta; generics : generic_params; + llbc_generics : Types.generic_params; + (** We use the LLBC generics to generate "pretty" names, for instance + for the variables we introduce for the trait clauses: we derive + those names from the types, and when doing so it is more meaningful + to derive them from the original LLBC types from before the + simplification of types like boxes and references. *) kind : type_decl_kind; preds : predicates; } @@ -922,6 +928,12 @@ type fun_sig_info = { type fun_sig = { generics : generic_params; (** TODO: we should analyse the signature to make the type parameters implicit whenever possible *) + llbc_generics : Types.generic_params; + (** We use the LLBC generics to generate "pretty" names, for instance + for the variables we introduce for the trait clauses: we derive + those names from the types, and when doing so it is more meaningful + to derive them from the original LLBC types from before the + simplification of types like boxes and references. *) preds : predicates; inputs : ty list; (** The types of the inputs. @@ -1028,8 +1040,15 @@ type trait_decl = { name : string; meta : meta; generics : generic_params; + llbc_generics : Types.generic_params; + (** We use the LLBC generics to generate "pretty" names, for instance + for the variables we introduce for the trait clauses: we derive + those names from the types, and when doing so it is more meaningful + to derive them from the original LLBC types from before the + simplification of types like boxes and references. *) preds : predicates; parent_clauses : trait_clause list; + llbc_parent_clauses : Types.trait_clause list; consts : (trait_item_name * (ty * global_decl_id option)) list; types : (trait_item_name * (trait_clause list * ty option)) list; required_methods : (trait_item_name * fun_decl_id) list; @@ -1044,7 +1063,15 @@ type trait_impl = { name : string; meta : meta; impl_trait : trait_decl_ref; + llbc_impl_trait : Types.trait_decl_ref; + (** Same remark as for {llbc_generics}. *) generics : generic_params; + llbc_generics : Types.generic_params; + (** We use the LLBC generics to generate "pretty" names, for instance + for the variables we introduce for the trait clauses: we derive + those names from the types, and when doing so it is more meaningful + to derive them from the original LLBC types from before the + simplification of types like boxes and references. *) preds : predicates; parent_trait_refs : trait_ref list; consts : (trait_item_name * (ty * global_decl_id)) list; diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 8463f56c..d0741b29 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1364,6 +1364,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = let loop_sig = { generics = fun_sig.generics; + llbc_generics = fun_sig.llbc_generics; preds = fun_sig.preds; inputs = inputs_tys; output; @@ -2127,7 +2128,8 @@ let filter_loop_inputs (transl : pure_fun_translation list) : let num_filtered = List.length (List.filter (fun b -> not b) used_info) in - let { generics; preds; inputs; output; doutputs; info } = + let { generics; llbc_generics; preds; inputs; output; doutputs; info } + = decl.signature in let { @@ -2155,7 +2157,9 @@ let filter_loop_inputs (transl : pure_fun_translation list) : effect_info; } in - let signature = { generics; preds; inputs; output; doutputs; info } in + let signature = + { generics; llbc_generics; preds; inputs; output; doutputs; info } + in { decl with signature } in diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 992ea499..6b0deb73 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -651,8 +651,10 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool = llbc_name = _; meta = _; generics = _; + llbc_generics = _; preds = _; parent_clauses; + llbc_parent_clauses = _; consts; types; required_methods; @@ -671,7 +673,9 @@ let trait_impl_is_empty (trait_impl : trait_impl) : bool = llbc_name = _; meta = _; impl_trait = _; + llbc_impl_trait = _; generics = _; + llbc_generics = _; preds = _; parent_trait_refs; consts; diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 5dee23db..4df3ee73 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -497,7 +497,17 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : let preds = translate_predicates def.preds in let is_local = def.is_local in let meta = def.meta in - { def_id; is_local; llbc_name; name; meta; generics; kind; preds } + { + def_id; + is_local; + llbc_name; + name; + meta; + generics; + llbc_generics = def.generics; + kind; + preds; + } let translate_type_id (id : T.type_id) : type_id = match id with @@ -1029,7 +1039,17 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id) } in let preds = translate_predicates sg.preds in - let sg = { generics; preds; inputs; output; doutputs; info } in + let sg = + { + generics; + llbc_generics = sg.generics; + preds; + inputs; + output; + doutputs; + info; + } + in { sg; output_names } let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern = @@ -3112,9 +3132,9 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) is_local; name = llbc_name; meta; - generics; + generics = llbc_generics; preds; - parent_clauses; + parent_clauses = llbc_parent_clauses; consts; types; required_methods; @@ -3128,9 +3148,9 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in - let generics = translate_generic_params generics in + let generics = translate_generic_params llbc_generics in let preds = translate_predicates preds in - let parent_clauses = List.map translate_trait_clause parent_clauses in + let parent_clauses = List.map translate_trait_clause llbc_parent_clauses in let consts = List.map (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id))) @@ -3151,8 +3171,10 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) name; meta; generics; + llbc_generics; preds; parent_clauses; + llbc_parent_clauses; consts; types; required_methods; @@ -3166,8 +3188,8 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) is_local; name = llbc_name; meta; - impl_trait; - generics; + impl_trait = llbc_impl_trait; + generics = llbc_generics; preds; parent_trait_refs; consts; @@ -3179,14 +3201,14 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) in let type_infos = ctx.type_ctx.type_infos in let impl_trait = - translate_trait_decl_ref (translate_fwd_ty type_infos) impl_trait + translate_trait_decl_ref (translate_fwd_ty type_infos) llbc_impl_trait in let name = Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in - let generics = translate_generic_params generics in + let generics = translate_generic_params llbc_generics in let preds = translate_predicates preds in let parent_trait_refs = List.map translate_strait_ref parent_trait_refs in let consts = @@ -3209,7 +3231,9 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) name; meta; impl_trait; + llbc_impl_trait; generics; + llbc_generics; preds; parent_trait_refs; consts; -- cgit v1.3.1