diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 2 | ||||
| -rw-r--r-- | kernel/cooking.mli | 2 | ||||
| -rw-r--r-- | kernel/declarations.ml | 4 | ||||
| -rw-r--r-- | kernel/declarations.mli | 4 | ||||
| -rw-r--r-- | kernel/entries.ml | 5 | ||||
| -rw-r--r-- | kernel/entries.mli | 4 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 69 | ||||
| -rw-r--r-- | kernel/mod_subst.mli | 9 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 27 | ||||
| -rw-r--r-- | kernel/mod_typing.mli | 12 | ||||
| -rw-r--r-- | kernel/modops.ml | 35 | ||||
| -rw-r--r-- | kernel/modops.mli | 4 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 13 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 10 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 4 |
16 files changed, 107 insertions, 99 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index d01398841c..87474b863f 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 09b42d0b12..4b8b4537cb 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 4308f9c1a4..282dad0da1 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 a92cb2cb49..d4c86fb353 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 dbf802bb12..28f11c9af4 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 d45e2bbdb8..08740afae7 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 452c2e69ad..9e8ce3fe5d 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 7164d1162b..91139985bb 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 407ae73ca7..13ac214370 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 f14d63be90..81974edfab 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 ce968b40ef..2bcfada964 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 9c00b8194e..f34fa88c4c 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 2bed2bb484..41ec0c6a6a 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 406727664c..0ab70b69e8 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 432460d7d5..801bd6c807 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 500858a59c..8b48fc3cf7 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 |