diff options
40 files changed, 218 insertions, 160 deletions
@@ -20,6 +20,16 @@ Vernacular commands - The undocumented and obsolete option "Set/Unset Boxed Definitions" has been removed, as well as syntaxes like "Boxed Fixpoint foo". +Module System + +- The inlining done during application of functors can now be controlled + more precisely. In addition to the "!F G" syntax preventing any inlining, + we can now use a priority level to select parameters to inline : + "<30>F X" means "only inline in F the parameters whose levels are <= 30". + The level of a parameter can be fixed by "Parameter Inline(30) foo". + When levels aren't given, the default value is 100. One can also use + the flag "Set Inline Level ..." to set a level. TODO: DOC! + Libraries - Creation of PArith, a subdirectory containing files about the positive type, diff --git a/checker/declarations.ml b/checker/declarations.ml index 664712dd5..190e14eb1 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -553,6 +553,8 @@ let val_cstr_subst = val_substituted val_constr let subst_constr_subst = subst_substituted +type inline = int option (* inlining level, None for no inlining *) + type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) const_body : constr_substituted option; @@ -561,7 +563,7 @@ type constant_body = { (* const_type_code : Cemitcodes.to_patch; *) const_constraints : Univ.constraints; const_opaque : bool; - const_inline : bool} + const_inline : inline } let val_cb = val_tuple ~name:"constant_body" [|val_nctxt; diff --git a/checker/declarations.mli b/checker/declarations.mli index ee44c8d5f..b5038996c 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -29,6 +29,8 @@ type constr_substituted val force_constr : constr_substituted -> constr val from_val : constr -> constr_substituted +type inline = int option (* inlining level, None for no inlining *) + type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) const_body : constr_substituted option; @@ -36,7 +38,7 @@ type constant_body = { const_body_code : to_patch_substituted; const_constraints : Univ.constraints; const_opaque : bool; - const_inline : bool} + const_inline : inline } (* Mutual inductives *) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index f8c0aeb87..81b4e8e94 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -1218,7 +1218,12 @@ type module_ast = | CMapply of module_ast * module_ast | CMwith of module_ast * with_declaration_ast -type module_ast_inl = module_ast * bool (* honor the inline annotations or not *) +(* Which inline annotations should we honor, either None or the ones + whose level is less or equal to the given integer *) + +type inline = int option + +type module_ast_inl = module_ast * inline type 'a module_signature = | Enforce of 'a (* ... : T *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 405db2d17..b7bac17bd 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -264,7 +264,12 @@ type module_ast = | CMapply of module_ast * module_ast | CMwith of module_ast * with_declaration_ast -type module_ast_inl = module_ast * bool (** honor the inline annotations or not *) +(* Which inline annotations should we honor, either None or the ones + whose level is less or equal to the given integer *) + +type inline = int option + +type module_ast_inl = module_ast * inline type 'a module_signature = | Enforce of 'a (** ... : T *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index d01398841..87474b863 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -137,4 +137,4 @@ let cook_constant env r = let j = make_judge (force (Option.get body)) typ in Typeops.make_polymorphic_if_constant_for_ind env j in - (body, typ, cb.const_constraints, cb.const_opaque, false) + (body, typ, cb.const_constraints, cb.const_opaque, None) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 09b42d0b1..4b8b4537c 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -23,7 +23,7 @@ type recipe = { val cook_constant : env -> recipe -> - constr_substituted option * constant_type * constraints * bool * bool + constr_substituted option * constant_type * constraints * bool * inline (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 4308f9c1a..282dad0da 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -49,6 +49,8 @@ let force = force subst_mps let subst_constr_subst = subst_substituted +type inline = int option (* inlining level, None for no inlining *) + type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) const_body : constr_substituted option; @@ -57,7 +59,7 @@ type constant_body = { (* const_type_code : Cemitcodes.to_patch; *) const_constraints : constraints; const_opaque : bool; - const_inline : bool} + const_inline : inline } (*s Inductive types (internal representation with redundant information). *) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index a92cb2cb4..d4c86fb35 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -35,6 +35,8 @@ type constr_substituted val from_val : constr -> constr_substituted val force : constr_substituted -> constr +type inline = int option (* inlining level, None for no inlining *) + type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constr_substituted option; @@ -43,7 +45,7 @@ type constant_body = { (* const_type_code : to_patch;*) const_constraints : constraints; const_opaque : bool; - const_inline : bool} + const_inline : inline } val subst_const_body : substitution -> constant_body -> constant_body diff --git a/kernel/entries.ml b/kernel/entries.ml index dbf802bb1..28f11c9af 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -59,8 +59,9 @@ type definition_entry = { const_entry_type : types option; const_entry_opaque : bool } -(* type and the inlining flag *) -type parameter_entry = types * bool +type inline = int option (* inlining level, None for no inlining *) + +type parameter_entry = types * inline type constant_entry = | DefinitionEntry of definition_entry diff --git a/kernel/entries.mli b/kernel/entries.mli index d45e2bbdb..08740afae 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -55,7 +55,9 @@ type definition_entry = { const_entry_type : types option; const_entry_opaque : bool } -type parameter_entry = types * bool (*inline flag*) +type inline = int option (* inlining level, None for no inlining *) + +type parameter_entry = types * inline type constant_entry = | DefinitionEntry of definition_entry diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 452c2e69a..9e8ce3fe5 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -18,9 +18,11 @@ open Util open Names open Term +(* For Inline, the int is an inlining level, and the constr (if present) + is the term into which we should inline *) type delta_hint = - Inline of constr option + Inline of int * constr option | Equiv of kernel_name | Prefix_equiv of module_path @@ -63,11 +65,11 @@ let add_mp mp1 mp2 resolve = let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst -let add_inline_delta_resolver con = - Deltamap.add (KN(user_con con)) (Inline None) - -let add_inline_constr_delta_resolver con cstr = - Deltamap.add (KN(user_con con)) (Inline (Some cstr)) +let add_inline_delta_resolver con lev = + Deltamap.add (KN(user_con con)) (Inline (lev,None)) + +let add_inline_constr_delta_resolver con lev cstr = + Deltamap.add (KN(user_con con)) (Inline (lev, Some cstr)) let add_constant_delta_resolver con = Deltamap.add (KN(user_con con)) (Equiv (canonical_con con)) @@ -131,15 +133,15 @@ let rec find_prefix resolve mp = with Not_found -> mp -exception Change_equiv_to_inline of constr +exception Change_equiv_to_inline of (int * constr) let solve_delta_kn resolve kn = try match Deltamap.find (KN kn) resolve with | Equiv kn1 -> kn1 - | Inline (Some c) -> - raise (Change_equiv_to_inline c) - | Inline None -> raise Inline_kn + | Inline (lev, Some c) -> + raise (Change_equiv_to_inline (lev,c)) + | Inline (_, None) -> raise Inline_kn | _ -> anomaly "mod_subst: bad association in delta_resolver" with @@ -199,13 +201,16 @@ let mind_of_delta2 resolve mind = _ -> mind -let inline_of_delta resolver = - let extract key hint l = - match key,hint with - |KN kn, Inline _ -> kn::l - | _,_ -> l - in - Deltamap.fold extract resolver [] +let inline_of_delta inline resolver = + match inline with + | None -> [] + | Some inl_lev -> + let extract key hint l = + match key,hint with + |KN kn, Inline (lev,_) -> if lev <= inl_lev then (lev,kn)::l else l + | _,_ -> l + in + Deltamap.fold extract resolver [] exception Not_inline @@ -213,14 +218,12 @@ let constant_of_delta_with_inline resolve con = let kn1,kn2 = canonical_con con,user_con con in try match Deltamap.find (KN kn2) resolve with - | Inline None -> None - | Inline (Some const) -> Some const + | Inline (_,o) -> o | _ -> raise Not_inline with Not_found | Not_inline -> try match Deltamap.find (KN kn1) resolve with - | Inline None -> None - | Inline (Some const) -> Some const + | Inline (_,o) -> o | _ -> raise Not_inline with Not_found | Not_inline -> None @@ -575,12 +578,12 @@ let subst_codom_delta_resolver subst resolver = (try Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver with - Change_equiv_to_inline c -> - Deltamap.add key (Inline (Some c)) resolver) - | Inline None -> + Change_equiv_to_inline (lev,c) -> + Deltamap.add key (Inline (lev,Some c)) resolver) + | Inline (_,None) -> Deltamap.add key hint resolver - | Inline (Some t) -> - Deltamap.add key (Inline (Some (subst_mps subst t))) resolver + | Inline (lev,Some t) -> + Deltamap.add key (Inline (lev,Some (subst_mps subst t))) resolver in Deltamap.fold apply_subst resolver empty_delta_resolver @@ -597,14 +600,14 @@ let subst_dom_codom_delta_resolver subst resolver = (try Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver with - Change_equiv_to_inline c -> - Deltamap.add key (Inline (Some c)) resolver) - | (KN kn),Inline None -> + Change_equiv_to_inline (lev,c) -> + Deltamap.add key (Inline (lev,Some c)) resolver) + | (KN kn),Inline (_,None) -> let key = KN (subst_kn subst kn) in Deltamap.add key hint resolver - | (KN kn),Inline (Some t) -> + | (KN kn),Inline (lev,Some t) -> let key = KN (subst_kn subst kn) in - Deltamap.add key (Inline (Some (subst_mps subst t))) resolver + Deltamap.add key (Inline (lev,Some (subst_mps subst t))) resolver | _,_ -> anomaly "Mod_subst: Bad association in resolver" in Deltamap.fold apply_subst resolver empty_delta_resolver @@ -625,8 +628,8 @@ let update_delta_resolver resolver1 resolver2 = Equiv (solve_delta_kn resolver2 kn) in Deltamap.add key new_hint res with - Change_equiv_to_inline c -> - Deltamap.add key (Inline (Some c)) res) + Change_equiv_to_inline (lev,c) -> + Deltamap.add key (Inline (lev,Some c)) res) | _ -> Deltamap.add key hint res with Not_found -> Deltamap.add key hint res diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 7164d1162..91139985b 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -19,10 +19,11 @@ type substitution val empty_delta_resolver : delta_resolver -val add_inline_delta_resolver : constant -> delta_resolver -> delta_resolver +val add_inline_delta_resolver : + constant -> int -> delta_resolver -> delta_resolver -val add_inline_constr_delta_resolver : constant -> constr -> delta_resolver - -> delta_resolver +val add_inline_constr_delta_resolver : + constant -> int -> constr -> delta_resolver -> delta_resolver val add_constant_delta_resolver : constant -> delta_resolver -> delta_resolver @@ -50,7 +51,7 @@ val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive val delta_of_mp : delta_resolver -> module_path -> module_path (** Extract the set of inlined constant in the resolver *) -val inline_of_delta : delta_resolver -> kernel_name list +val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list (** remove_mp is used for the computation of a resolver induced by Include P *) val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 407ae73ca..13ac21437 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -294,11 +294,11 @@ and translate_struct_module_entry env mp inl mse = match mse with (* place for nondep_supertype *) in let cst = check_subtypes env mtb farg_b in let mp_delta = discr_resolver env mtb in - let mp_delta = if not inl then mp_delta else - complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta + let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in - let subst = map_mbid farg_id mp1 mp_delta in - (subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst), + let subst = map_mbid farg_id mp1 mp_delta + in + (subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst), (subst_codom_delta_resolver subst resolver), Univ.union_constraints cst1 cst | MSEwith(mte, with_decl) -> @@ -333,12 +333,13 @@ and translate_struct_type_entry env inl mse = match mse with (* place for nondep_supertype *) in let cst2 = check_subtypes env mtb farg_b in let mp_delta = discr_resolver env mtb in - let mp_delta = if not inl then mp_delta else - complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta + let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta + in + let subst = map_mbid farg_id mp1 mp_delta in - let subst = map_mbid farg_id mp1 mp_delta in - (subst_struct_expr subst fbody_b),None, - (subst_codom_delta_resolver subst resolve),mp_from,Univ.union_constraints cst1 cst2 + (subst_struct_expr subst fbody_b),None, + (subst_codom_delta_resolver subst resolve),mp_from, + Univ.union_constraints cst1 cst2 | MSEwith(mte, with_decl) -> let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in let sign,alg,resolve,cst1 = @@ -375,11 +376,11 @@ let rec translate_struct_include_module_entry env mp inl mse = match mse with (* place for nondep_supertype *) in let cst = check_subtypes env mtb farg_b in let mp_delta = discr_resolver env mtb in - let mp_delta = if not inl then mp_delta else - complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta + let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta + in + let subst = map_mbid farg_id mp1 mp_delta in - let subst = map_mbid farg_id mp1 mp_delta in - (subst_struct_expr subst fbody_b), + (subst_struct_expr subst fbody_b), (subst_codom_delta_resolver subst resolver), Univ.union_constraints cst1 cst | _ -> error ("You cannot Include a high-order structure.") diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index f14d63be9..81974edfa 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -13,20 +13,20 @@ open Mod_subst open Names -val translate_module : env -> module_path -> bool -> module_entry +val translate_module : env -> module_path -> inline -> module_entry -> module_body -val translate_module_type : env -> module_path -> bool -> module_struct_entry -> +val translate_module_type : env -> module_path -> inline -> module_struct_entry -> module_type_body -val translate_struct_module_entry : env -> module_path -> bool -> module_struct_entry -> +val translate_struct_module_entry : env -> module_path -> inline -> module_struct_entry -> struct_expr_body * struct_expr_body * delta_resolver * Univ.constraints -val translate_struct_type_entry : env -> bool -> module_struct_entry -> +val translate_struct_type_entry : env -> inline -> module_struct_entry -> struct_expr_body * struct_expr_body option * delta_resolver * module_path * Univ.constraints -val translate_struct_include_module_entry : env -> module_path - -> bool -> module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints +val translate_struct_include_module_entry : env -> module_path -> inline -> + module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints val add_modtype_constraints : env -> module_type_body -> env diff --git a/kernel/modops.ml b/kernel/modops.ml index ce968b40e..2bcfada96 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -364,31 +364,28 @@ let module_type_of_module env mp mb = typ_constraints = mb.mod_constraints; typ_delta = mb.mod_delta} -let complete_inline_delta_resolver env mp mbid mtb delta = - let constants = inline_of_delta mtb.typ_delta in +let inline_delta_resolver env inl mp mbid mtb delta = + let constants = inline_of_delta inl mtb.typ_delta in let rec make_inline delta = function | [] -> delta - | kn::r -> + | (lev,kn)::r -> let kn = replace_mp_in_kn (MPbound mbid) mp kn in let con = constant_of_kn kn in let con' = constant_of_delta delta con in - try - let constant = lookup_constant con' env in - if (not constant.Declarations.const_opaque) then - let constr = Option.map Declarations.force - constant.Declarations.const_body in - if constr = None then - (make_inline delta r) - else - add_inline_constr_delta_resolver con (Option.get constr) - (make_inline delta r) - else - (make_inline delta r) - with - Not_found -> error_no_such_label_sub (con_label con) - (string_of_mp (con_modpath con)) + try + let constant = lookup_constant con' env in + let l = make_inline delta r in + if constant.Declarations.const_opaque then l + else match constant.Declarations.const_body with + | None -> l + | Some body -> + let constr = Declarations.force body in + add_inline_constr_delta_resolver con lev constr l + with Not_found -> + error_no_such_label_sub (con_label con) + (string_of_mp (con_modpath con)) in - make_inline delta constants + make_inline delta constants let rec strengthen_and_subst_mod mb subst env mp_from mp_to env resolver = diff --git a/kernel/modops.mli b/kernel/modops.mli index 9c00b8194..f34fa88c4 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -39,8 +39,8 @@ val check_modpath_equiv : env -> module_path -> module_path -> unit val strengthen : env -> module_type_body -> module_path -> module_type_body -val complete_inline_delta_resolver : - env -> module_path -> mod_bound_id -> module_type_body -> +val inline_delta_resolver : + env -> inline -> module_path -> mod_bound_id -> module_type_body -> delta_resolver -> delta_resolver val strengthen_and_subst_mb : module_body -> module_path -> env -> bool diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 2bed2bb48..41ec0c6a6 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -262,11 +262,9 @@ let add_constant dir l decl senv = in let senv' = add_constraints cb.const_constraints senv in let env'' = Environ.add_constant kn cb senv'.env in - let resolver = - if cb.const_inline then - add_inline_delta_resolver kn senv'.modinfo.resolver - else - senv'.modinfo.resolver + let resolver = match cb.const_inline with + | None -> senv'.modinfo.resolver + | Some lev -> add_inline_delta_resolver kn lev senv'.modinfo.resolver in kn, { old = senv'.old; env = env''; @@ -492,8 +490,9 @@ let end_module l restype senv = | SEBfunctor(mbid,mtb,str) -> let cst_sub = check_subtypes senv.env mb mtb in let senv = add_constraints cst_sub senv in - let mpsup_delta = if not inl then mb.typ_delta else - complete_inline_delta_resolver senv.env mp_sup mbid mtb mb.typ_delta in + let mpsup_delta = + inline_delta_resolver senv.env inl mp_sup mbid mtb mb.typ_delta + in let subst = map_mbid mbid mp_sup mpsup_delta in let resolver = subst_codom_delta_resolver subst resolver in (compute_sign diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 406727664..0ab70b69e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -53,12 +53,12 @@ val add_mind : (** Adding a module *) val add_module : - label -> module_entry -> bool -> safe_environment + label -> module_entry -> inline -> safe_environment -> module_path * delta_resolver * safe_environment (** Adding a module type *) val add_modtype : - label -> module_struct_entry -> bool -> safe_environment + label -> module_struct_entry -> inline -> safe_environment -> module_path * safe_environment (** Adding universe constraints *) @@ -75,11 +75,11 @@ val start_module : label -> safe_environment -> module_path * safe_environment val end_module : - label -> (module_struct_entry * bool) option + label -> (module_struct_entry * inline) option -> safe_environment -> module_path * delta_resolver * safe_environment val add_module_parameter : - mod_bound_id -> module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment + mod_bound_id -> module_struct_entry -> inline -> safe_environment -> delta_resolver * safe_environment val start_modtype : label -> safe_environment -> module_path * safe_environment @@ -88,7 +88,7 @@ val end_modtype : label -> safe_environment -> module_path * safe_environment val add_include : - module_struct_entry -> bool -> bool -> safe_environment -> + module_struct_entry -> bool -> inline -> safe_environment -> delta_resolver * safe_environment val pack_module : safe_environment -> module_body diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 432460d7d..801bd6c80 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -94,7 +94,7 @@ let infer_declaration env dcl = let (j,cst) = infer env c.const_entry_body in let (typ,cst) = constrain_type env j cst c.const_entry_type in Some (Declarations.from_val j.uj_val), typ, cst, - c.const_entry_opaque, false + c.const_entry_opaque, None | ParameterEntry (t,nl) -> let (j,cst) = infer env t in None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst, diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 500858a59..8b48fc3cf 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -22,10 +22,10 @@ val translate_local_assum : env -> types -> types * Univ.constraints val infer_declaration : env -> constant_entry -> - constr_substituted option * constant_type * constraints * bool * bool + constr_substituted option * constant_type * constraints * bool * inline val build_constant_declaration : env -> 'a -> - constr_substituted option * constant_type * constraints * bool * bool -> + constr_substituted option * constant_type * constraints * bool * inline -> constant_body val translate_constant : env -> constant -> constant_entry -> constant_body diff --git a/lib/flags.ml b/lib/flags.ml index 13f540379..6d1fb7fae 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -124,3 +124,9 @@ let camlbin = ref Coq_config.camlbin let camlp4bin_spec = ref false let camlp4bin = ref Coq_config.camlp4bin +(* Level of inlining during a functor application *) + +let default_inline_level = 100 +let inline_level = ref default_inline_level +let set_inline_level = (:=) inline_level +let get_inline_level () = !inline_level diff --git a/lib/flags.mli b/lib/flags.mli index ecb4d6dd6..20e3a7819 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -84,3 +84,8 @@ val camlbin_spec : bool ref val camlbin : string ref val camlp4bin_spec : bool ref val camlp4bin : string ref + +(** Level of inlining during a functor application *) +val set_inline_level : int -> unit +val get_inline_level : unit -> int +val default_inline_level : int diff --git a/library/declare.ml b/library/declare.ml index fa95fe313..c566cedfd 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -139,7 +139,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) = Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind) (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false)) +let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,None)) let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk diff --git a/library/declaremods.ml b/library/declaremods.ml index 58b0d6a46..b6b3a766f 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -78,7 +78,7 @@ let modtab_objects = let openmod_info = ref ((MPfile(initial_dir),[],None,[]) : module_path * mod_bound_id list * - (module_struct_entry * bool) option * module_type_body list) + (module_struct_entry * inline) option * module_type_body list) (* The library_cache here is needed to avoid recalculations of substituted modules object during "reloading" of libraries *) @@ -425,24 +425,20 @@ let rec get_objs_modtype_application env = function Modops.error_application_to_not_path mexpr | _ -> error "Application of a non-functor." -let rec compute_subst env mbids sign mp_l inline = +let rec compute_subst env mbids sign mp_l inl = match mbids,mp_l with | _,[] -> mbids,empty_subst | [],r -> error "Application of a functor with too few arguments." | mbid::mbids,mp::mp_l -> let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in let mb = Environ.lookup_module mp env in - let mbid_left,subst = compute_subst env mbids fbody_b mp_l inline in - match discr_resolver mb with - | None -> - mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst + let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in + let resolver = match discr_resolver mb with + | None -> empty_delta_resolver | Some mp_delta -> - let mp_delta = - if not inline then mp_delta else - Modops.complete_inline_delta_resolver env mp - farg_id farg_b mp_delta - in - mbid_left,join (map_mbid mbid mp mp_delta) subst + Modops.inline_delta_resolver env inl mp farg_id farg_b mp_delta + in + mbid_left,join (map_mbid mbid mp resolver) subst let rec get_modtype_substobjs env mp_from inline = function MSEident ln -> @@ -748,15 +744,16 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = let funct f m = funct_entry arg_entries (f (Global.env ()) m) in let env = Global.env() in + let default_inl = Some (Flags.get_inline_level ()) in (* PLTODO *) let mty_entry_o, subs, inl_res = match res with | Topconstr.Enforce (mty,inl) -> Some (funct interp_modtype mty), [], inl | Topconstr.Check mtys -> - None, build_subtypes interp_modtype mmp arg_entries mtys, true + None, build_subtypes interp_modtype mmp arg_entries mtys, default_inl in (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in *) let mexpr_entry_o, inl_expr = match mexpr_o with - | None -> None, true + | None -> None, default_inl | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl in let entry = @@ -775,7 +772,8 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = (* and declare the module as a whole *) Summary.unfreeze_summaries fs; let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in - let mp_env,resolver = Global.add_module id entry (inl_expr&&inl_res) in + let inl = if inl_expr = None then None else inl_res in (*PLTODO *) + let mp_env,resolver = Global.add_module id entry inl in if mp_env <> mp then anomaly "Kernel and Library names do not match"; @@ -853,8 +851,8 @@ let rec include_subst env mb mbids sign inline = | mbid::mbids -> let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in let subst = include_subst env mb mbids fbody_b inline in - let mp_delta = if not inline then mb.mod_delta else - Modops.complete_inline_delta_resolver env mb.mod_mp + let mp_delta = + Modops.inline_delta_resolver env inline mb.mod_mp farg_id farg_b mb.mod_delta in join (map_mbid mbid mb.mod_mp mp_delta) subst diff --git a/library/declaremods.mli b/library/declaremods.mli index 83c6b2bb6..b1978c282 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -37,13 +37,13 @@ val declare_module : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> identifier -> - (identifier located list * ('modast * bool)) list -> - ('modast * bool) Topconstr.module_signature -> - ('modast * bool) list -> module_path + (identifier located list * ('modast * inline)) list -> + ('modast * inline) Topconstr.module_signature -> + ('modast * inline) list -> module_path val start_module : (env -> 'modast -> module_struct_entry) -> - bool option -> identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) Topconstr.module_signature -> module_path + bool option -> identifier -> (identifier located list * ('modast * inline)) list -> + ('modast * inline) Topconstr.module_signature -> module_path val end_module : unit -> module_path @@ -53,12 +53,12 @@ val end_module : unit -> module_path val declare_modtype : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> - identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) list -> ('modast * bool) list -> module_path + identifier -> (identifier located list * ('modast * inline)) list -> + ('modast * inline) list -> ('modast * inline) list -> module_path val start_modtype : (env -> 'modast -> module_struct_entry) -> - identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) list -> module_path + identifier -> (identifier located list * ('modast * inline)) list -> + ('modast * inline) list -> module_path val end_modtype : unit -> module_path @@ -103,7 +103,7 @@ val import_module : bool -> module_path -> unit (** Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> - ('struct_expr * bool) list -> unit + ('struct_expr * inline) list -> unit (** {6 ... } *) (** [iter_all_segments] iterate over all segments, the modules' @@ -120,5 +120,5 @@ val debug_print_modtab : unit -> Pp.std_ppcmds (** For translator *) val process_module_bindings : module_ident list -> - (mod_bound_id * (module_struct_entry * bool)) list -> unit + (mod_bound_id * (module_struct_entry * inline)) list -> unit diff --git a/library/global.mli b/library/global.mli index eb58fd86e..9beb535d5 100644 --- a/library/global.mli +++ b/library/global.mli @@ -48,11 +48,11 @@ val add_mind : dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive val add_module : - identifier -> module_entry -> bool -> module_path * delta_resolver + identifier -> module_entry -> inline -> module_path * delta_resolver val add_modtype : - identifier -> module_struct_entry -> bool -> module_path + identifier -> module_struct_entry -> inline -> module_path val add_include : - module_struct_entry -> bool -> bool -> delta_resolver + module_struct_entry -> bool -> inline -> delta_resolver val add_constraints : constraints -> unit @@ -68,10 +68,10 @@ val set_engagement : engagement -> unit val start_module : identifier -> module_path val end_module : Summary.frozen ->identifier -> - (module_struct_entry * bool) option -> module_path * delta_resolver + (module_struct_entry * inline) option -> module_path * delta_resolver val add_module_parameter : - mod_bound_id -> module_struct_entry -> bool -> delta_resolver + mod_bound_id -> module_struct_entry -> inline -> delta_resolver val start_modtype : identifier -> module_path val end_modtype : Summary.frozen -> identifier -> module_path diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f6943871c..0c7dbeeb0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -215,7 +215,9 @@ GEXTEND Gram | IDENT "Parameters" -> (Global, Definitional) ] ] ; inline: - [ ["Inline" -> true | -> false] ] + [ [ IDENT "Inline"; "("; i = INT; ")" -> Some (int_of_string i) + | IDENT "Inline" -> Some (Flags.get_inline_level()) + | -> None] ] ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) @@ -443,12 +445,14 @@ GEXTEND Gram | -> [] ] ] ; module_expr_inl: - [ [ "!"; me = module_expr -> (me,false) - | me = module_expr -> (me,true) ] ] + [ [ "!"; me = module_expr -> (me,None) + | "<"; i = INT; ">"; me = module_expr -> (me,Some (int_of_string i)) + | me = module_expr -> (me,Some (Flags.get_inline_level())) ] ] ; module_type_inl: - [ [ "!"; me = module_type -> (me,false) - | me = module_type -> (me,true) ] ] + [ [ "!"; me = module_type -> (me,None) + | "<"; i = INT; ">"; me = module_type -> (me,Some (int_of_string i)) + | me = module_type -> (me,Some (Flags.get_inline_level())) ] ] ; (* Module binder *) module_binder: diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 21281f6e4..42007e4b0 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -227,8 +227,8 @@ let rec pr_module_ast pr_c = function pr_module_ast pr_c me1 ++ spc() ++ hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")") -let pr_module_ast_inl pr_c (mast,b) = - (if b then mt () else str "!") ++ pr_module_ast pr_c mast +let pr_module_ast_inl pr_c (mast,o) = + (if o=None then str "!" else mt ()) ++ pr_module_ast pr_c mast let pr_of_module_type prc = function | Enforce mty -> str ":" ++ pr_module_ast_inl prc mty diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 30c88602d..1218dd80c 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -153,7 +153,8 @@ let rec seb2mse = function let expand_seb env mp seb = let seb,_,_,_ = - Mod_typing.translate_struct_module_entry env mp true (seb2mse seb) + let inl = Some (Flags.get_inline_level()) in + Mod_typing.translate_struct_module_entry env mp inl (seb2mse seb) in seb (** When possible, we use the nicer, shorter, algebraic type structures diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 3d1e836a7..e8e1fc25f 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -603,7 +603,7 @@ let admit_obligations n = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false), + let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,None), IsAssumption Conjectural) in assumption_message x.obl_name; diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index a6a36672b..9e017bbd8 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1410,7 +1410,7 @@ let add_morphism_infer glob m n = let instance = build_morphism_signature m in if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id - (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) + (Entries.ParameterEntry (instance,None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 11bb6b436..ab04ebaf6 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3417,7 +3417,7 @@ let admit_as_an_axiom gl = let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in if occur_existential concl then error"\"admit\" cannot handle existentials."; let axiom = - let cd = Entries.ParameterEntry (concl,false) in + let cd = Entries.ParameterEntry (concl,None) in let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in constr_of_global (ConstRef con) in diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 8d56772ac..4dedcfe32 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -18,7 +18,7 @@ Require Export Equalities Orders NumPrelude GenericMinMax. *) Module Type ZeroSuccPred (Import T:Typ). - Parameter Inline zero : t. + Parameter Inline(20) zero : t. Parameters Inline succ pred : t -> t. End ZeroSuccPred. @@ -47,7 +47,7 @@ End IsNZDomain. *) Module Type OneTwo (Import T:Typ). - Parameter Inline one two : t. + Parameter Inline(20) one two : t. End OneTwo. Module Type OneTwoNotation (T:Typ)(Import NZ:OneTwo T). diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 8e72bd611..2fbdff624 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -21,13 +21,13 @@ End Nop. (** * Structure with just a base type [t] *) Module Type Typ. - Parameter Inline t : Type. + Parameter Inline(10) t : Type. End Typ. (** * Structure with an equality relation [eq] *) Module Type HasEq (Import T:Typ). - Parameter Inline eq : t -> t -> Prop. + Parameter Inline(30) eq : t -> t -> Prop. End HasEq. Module Type Eq := Typ <+ HasEq. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index f11bdb4a8..9b6c74398 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -179,7 +179,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props in Evarutil.check_evars env Evd.empty !evars termtype; let cst = Declare.declare_constant ~internal:Declare.KernelSilent id - (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical) + (Entries.ParameterEntry (termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical) in instance_hook k None false imps ?hook (ConstRef cst); id end else @@ -286,7 +286,7 @@ let context ?(hook=fun _ -> ()) l = let fn (id, _, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then let cst = Declare.declare_constant ~internal:Declare.KernelSilent id - (ParameterEntry (t,false), IsAssumption Logical) + (ParameterEntry (t,None), IsAssumption Logical) in match class_of_constr t with | Some tc -> @@ -299,7 +299,7 @@ let context ?(hook=fun _ -> ()) l = match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls in Command.declare_assumption false (Local (* global *), Definitional) t - [] impl (* implicit *) false (* inline *) (dummy_loc, id); + [] impl (* implicit *) None (* inline *) (dummy_loc, id); match class_of_constr t with | None -> () | Some tc -> hook (VarRef id)) diff --git a/toplevel/command.mli b/toplevel/command.mli index 163f68fd0..b12479b45 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -44,11 +44,11 @@ val interp_assumption : val declare_assumption : coercion_flag -> assumption_kind -> types -> manual_implicits -> - bool (** implicit *) -> bool (* inline *) -> variable located -> unit + bool (** implicit *) -> inline -> variable located -> unit val declare_assumptions : variable located list -> coercion_flag -> assumption_kind -> types -> manual_implicits -> - bool -> bool -> unit + bool -> inline -> unit (** {6 Inductive and coinductive types} *) diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 847278b07..c0ce16cea 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -199,7 +199,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) = (Local,VarRef id,imps) | Global -> let k = IsAssumption Conjectural in - let kn = declare_constant id (ParameterEntry (t_i,false), k) in + let kn = declare_constant id (ParameterEntry (t_i,None), k) in (Global,ConstRef kn,imps)) | Some body -> let k = logical_kind_of_goal_kind kind in @@ -330,7 +330,7 @@ let start_proof_com kind thms hook = let admit () = let (id,k,typ,hook) = Pfedit.current_proof_statement () in let kn = - declare_constant id (ParameterEntry (typ,false),IsAssumption Conjectural) in + declare_constant id (ParameterEntry (typ,None),IsAssumption Conjectural) in Pfedit.delete_current_proof (); assumption_message id; hook Global (ConstRef kn) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a18340e90..f4fc8714b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -941,6 +941,16 @@ let _ = optwrite = (fun b -> Vconv.set_use_vm b) } let _ = + declare_int_option + { optsync = true; + optname = "level of inling duging functor application"; + optkey = ["Inline";"Level"]; + optread = (fun () -> Some (Flags.get_inline_level ())); + optwrite = (fun o -> + let lev = Option.default Flags.default_inline_level o in + Flags.set_inline_level lev) } + +let _ = declare_bool_option { optsync = true; optname = "use of boxed values"; diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 80191b8fd..3091f10c5 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -196,6 +196,8 @@ type scheme = | CaseScheme of bool * reference or_by_notation * sort_expr | EqualityScheme of reference or_by_notation +type inline = int option (* inlining level, none for no inlining *) + type vernac_expr = (* Control *) | VernacList of located_vernac_expr list @@ -226,7 +228,7 @@ type vernac_expr = bool * declaration_hook | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list + | VernacAssumption of assumption_kind * inline * simple_binder with_coercion list | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list |