diff options
| -rw-r--r-- | compiler/Extract.ml | 33 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 102 | ||||
| -rw-r--r-- | compiler/ExtractName.ml | 2 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 5 | ||||
| -rw-r--r-- | compiler/Pure.ml | 27 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 8 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 4 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 44 |
8 files changed, 177 insertions, 48 deletions
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<Box<usize>", + 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<u32>`, 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<u32>`, + 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; |