From 60de53d159c85b8300226a61aa502a7e0dd2f04b Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 26 Feb 2013 18:52:24 +0000 Subject: kernel/declarations becomes a pure mli - constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml - the functions that were in declarations.ml (mostly substitution utilities and hashcons) are now in kernel/declareops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/cbytegen.ml | 2 +- kernel/cooking.ml | 8 +- kernel/declarations.ml | 430 ------------------------------------------------ kernel/declarations.mli | 100 +++-------- kernel/declareops.ml | 201 ++++++++++++++++++++++ kernel/declareops.mli | 56 +++++++ kernel/entries.mli | 8 +- kernel/environ.ml | 2 +- kernel/indtypes.ml | 1 + kernel/inductive.ml | 9 +- kernel/kernel.mllib | 3 +- kernel/lazyconstr.ml | 43 +++++ kernel/lazyconstr.mli | 34 ++++ kernel/mod_typing.ml | 6 +- kernel/modops.ml | 5 +- kernel/nativecode.ml | 6 +- kernel/nativelambda.ml | 6 +- kernel/safe_typing.ml | 19 ++- kernel/subtyping.ml | 16 +- kernel/term_typing.ml | 8 +- 20 files changed, 406 insertions(+), 557 deletions(-) delete mode 100644 kernel/declarations.ml create mode 100644 kernel/declareops.ml create mode 100644 kernel/declareops.mli create mode 100644 kernel/lazyconstr.ml create mode 100644 kernel/lazyconstr.mli (limited to 'kernel') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index d0751475b..0f3636632 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -719,7 +719,7 @@ let compile env c = let compile_constant_body env = function | Undef _ | OpaqueDef _ -> BCconstant | Def sb -> - let body = Declarations.force sb in + let body = Lazyconstr.force sb in match kind_of_term body with | Const kn' -> (* we use the canonical name of the constant*) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index fb3303687..e8e35ee85 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -121,14 +121,14 @@ type recipe = { let on_body f = function | Undef inl -> Undef inl - | Def cs -> Def (Declarations.from_val (f (Declarations.force cs))) + | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs))) | OpaqueDef lc -> - OpaqueDef (Declarations.opaque_from_val (f (Declarations.force_opaque lc))) + OpaqueDef (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc))) let constr_of_def = function | Undef _ -> assert false - | Def cs -> Declarations.force cs - | OpaqueDef lc -> Declarations.force_opaque lc + | Def cs -> Lazyconstr.force cs + | OpaqueDef lc -> Lazyconstr.force_opaque lc let cook_constant env r = let cb = r.d_from in diff --git a/kernel/declarations.ml b/kernel/declarations.ml deleted file mode 100644 index 62a3170f2..000000000 --- a/kernel/declarations.ml +++ /dev/null @@ -1,430 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* None - | Def c -> Some c - | OpaqueDef lc -> Some (force_lazy_constr lc) - -let constant_has_body cb = match cb.const_body with - | Undef _ -> false - | Def _ | OpaqueDef _ -> true - -let is_opaque cb = match cb.const_body with - | OpaqueDef _ -> true - | Undef _ | Def _ -> false - -(* Substitutions of [constant_body] *) - -let subst_rel_declaration sub (id,copt,t as x) = - let copt' = Option.smartmap (subst_mps sub) copt in - let t' = subst_mps sub t in - if copt == copt' & t == t' then x else (id,copt',t') - -let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) - -(* TODO: these substitution functions could avoid duplicating things - when the substitution have preserved all the fields *) - -let subst_const_type sub arity = - if is_empty_subst sub then arity - else match arity with - | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) - | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) - -let subst_const_def sub = function - | Undef inl -> Undef inl - | Def c -> Def (subst_constr_subst sub c) - | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc) - -let subst_const_body sub cb = { - const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false); - const_body = subst_const_def sub cb.const_body; - const_type = subst_const_type sub cb.const_type; - const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; - const_constraints = cb.const_constraints; - const_native_name = ref NotLinked; - const_inline_code = cb.const_inline_code } - -(* Hash-consing of [constant_body] *) - -let hcons_rel_decl ((n,oc,t) as d) = - let n' = Name.hcons n - and oc' = Option.smartmap hcons_constr oc - and t' = hcons_types t - in if n' == n && oc' == oc && t' == t then d else (n',oc',t') - -let hcons_rel_context l = List.smartmap hcons_rel_decl l - -let hcons_polyarity ar = - { poly_param_levels = - List.smartmap (Option.smartmap hcons_univ) ar.poly_param_levels; - poly_level = hcons_univ ar.poly_level } - -let hcons_const_type = function - | NonPolymorphicType t -> - NonPolymorphicType (hcons_constr t) - | PolymorphicArity (ctx,s) -> - PolymorphicArity (hcons_rel_context ctx, hcons_polyarity s) - -let hcons_const_def = function - | Undef inl -> Undef inl - | Def l_constr -> - let constr = force l_constr in - Def (from_val (hcons_constr constr)) - | OpaqueDef lc -> - if lazy_constr_is_val lc then - let constr = force_opaque lc in - OpaqueDef (opaque_from_val (hcons_constr constr)) - else OpaqueDef lc - -let hcons_const_body cb = - { cb with - const_body = hcons_const_def cb.const_body; - const_type = hcons_const_type cb.const_type; - const_constraints = hcons_constraints cb.const_constraints } - - -(*s Inductive types (internal representation with redundant - information). *) - -type recarg = - | Norec - | Mrec of inductive - | Imbr of inductive - -let eq_recarg r1 r2 = match r1, r2 with -| Norec, Norec -> true -| Mrec i1, Mrec i2 -> eq_ind i1 i2 -| Imbr i1, Imbr i2 -> eq_ind i1 i2 -| _ -> false - -let subst_recarg sub r = match r with - | Norec -> r - | Mrec (kn,i) -> let kn' = subst_ind sub kn in - if kn==kn' then r else Mrec (kn',i) - | Imbr (kn,i) -> let kn' = subst_ind sub kn in - if kn==kn' then r else Imbr (kn',i) - -type wf_paths = recarg Rtree.t - -let mk_norec = Rtree.mk_node Norec [||] - -let mk_paths r recargs = - Rtree.mk_node r - (Array.map (fun l -> Rtree.mk_node Norec (Array.of_list l)) recargs) - -let dest_recarg p = fst (Rtree.dest_node p) - -(* dest_subterms returns the sizes of each argument of each constructor of - an inductive object of size [p]. This should never be done for Norec, - because the number of sons does not correspond to the number of - constructors. - *) -let dest_subterms p = - let (ra,cstrs) = Rtree.dest_node p in - assert (match ra with Norec -> false | _ -> true); - Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs - -let recarg_length p j = - let (_,cstrs) = Rtree.dest_node p in - Array.length (snd (Rtree.dest_node cstrs.(j-1))) - -let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p - -(**********************************************************************) -(* Representation of mutual inductive types in the kernel *) -(* - Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1 - ... - with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn -*) - -type monomorphic_inductive_arity = { - mind_user_arity : constr; - mind_sort : sorts; -} - -type inductive_arity = -| Monomorphic of monomorphic_inductive_arity -| Polymorphic of polymorphic_arity - -type one_inductive_body = { - -(* Primitive datas *) - - (* Name of the type: [Ii] *) - mind_typename : Id.t; - - (* Arity context of [Ii] with parameters: [forall params, Ui] *) - mind_arity_ctxt : rel_context; - - (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *) - mind_arity : inductive_arity; - - (* Names of the constructors: [cij] *) - mind_consnames : Id.t array; - - (* Types of the constructors with parameters: [forall params, Tij], - where the Ik are replaced by de Bruijn index in the context - I1:forall params, U1 .. In:forall params, Un *) - mind_user_lc : types array; - -(* Derived datas *) - - (* Number of expected real arguments of the type (no let, no params) *) - mind_nrealargs : int; - - (* Length of realargs context (with let, no params) *) - mind_nrealargs_ctxt : int; - - (* List of allowed elimination sorts *) - mind_kelim : sorts_family list; - - (* Head normalized constructor types so that their conclusion is atomic *) - mind_nf_lc : types array; - - (* Length of the signature of the constructors (with let, w/o params) *) - mind_consnrealdecls : int array; - - (* Signature of recursive arguments in the constructors *) - mind_recargs : wf_paths; - -(* Datas for bytecode compilation *) - - (* number of constant constructor *) - mind_nb_constant : int; - - (* number of no constant constructor *) - mind_nb_args : int; - - mind_reloc_tbl : Cbytecodes.reloc_table; - } - -type mutual_inductive_body = { - - (* The component of the mutual inductive block *) - mind_packets : one_inductive_body array; - - (* Whether the inductive type has been declared as a record *) - mind_record : bool; - - (* Whether the type is inductive or coinductive *) - mind_finite : bool; - - (* Number of types in the block *) - mind_ntypes : int; - - (* Section hypotheses on which the block depends *) - mind_hyps : section_context; - - (* Number of expected parameters *) - mind_nparams : int; - - (* Number of recursively uniform (i.e. ordinary) parameters *) - mind_nparams_rec : int; - - (* The context of parameters (includes let-in declaration) *) - mind_params_ctxt : rel_context; - - (* Universes constraints enforced by the inductive declaration *) - mind_constraints : constraints; - - (* Data for native compilation *) - (* Status of the code (linked or not, and where) *) - mind_native_name : native_name ref; - - } - -let subst_indarity sub = function -| Monomorphic s -> - Monomorphic { - mind_user_arity = subst_mps sub s.mind_user_arity; - mind_sort = s.mind_sort; - } -| Polymorphic s as x -> x - -let subst_mind_packet sub mbp = - { mind_consnames = mbp.mind_consnames; - mind_consnrealdecls = mbp.mind_consnrealdecls; - mind_typename = mbp.mind_typename; - mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; - mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; - mind_arity = subst_indarity sub mbp.mind_arity; - mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; - mind_nrealargs = mbp.mind_nrealargs; - mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; - mind_kelim = mbp.mind_kelim; - mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); - mind_nb_constant = mbp.mind_nb_constant; - mind_nb_args = mbp.mind_nb_args; - mind_reloc_tbl = mbp.mind_reloc_tbl } - -let subst_mind sub mib = - { mind_record = mib.mind_record ; - mind_finite = mib.mind_finite ; - mind_ntypes = mib.mind_ntypes ; - mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); - mind_nparams = mib.mind_nparams; - mind_nparams_rec = mib.mind_nparams_rec; - mind_params_ctxt = - map_rel_context (subst_mps sub) mib.mind_params_ctxt; - mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_constraints = mib.mind_constraints; - mind_native_name = ref NotLinked } - -let hcons_indarity = function - | Monomorphic a -> - Monomorphic { mind_user_arity = hcons_constr a.mind_user_arity; - mind_sort = hcons_sorts a.mind_sort } - | Polymorphic a -> Polymorphic (hcons_polyarity a) - -let hcons_mind_packet oib = - { oib with - mind_typename = Id.hcons oib.mind_typename; - mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; - mind_arity = hcons_indarity oib.mind_arity; - mind_consnames = Array.smartmap Id.hcons oib.mind_consnames; - mind_user_lc = Array.smartmap hcons_types oib.mind_user_lc; - mind_nf_lc = Array.smartmap hcons_types oib.mind_nf_lc } - -let hcons_mind mib = - { mib with - mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; - mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; - mind_constraints = hcons_constraints mib.mind_constraints } - -(*s Modules: signature component specifications, module types, and - module declarations *) - -type structure_field_body = - | SFBconst of constant_body - | SFBmind of mutual_inductive_body - | SFBmodule of module_body - | SFBmodtype of module_type_body - -and structure_body = (Label.t * structure_field_body) list - -and struct_expr_body = - | SEBident of module_path - | SEBfunctor of MBId.t * module_type_body * struct_expr_body - | SEBapply of struct_expr_body * struct_expr_body * constraints - | SEBstruct of structure_body - | SEBwith of struct_expr_body * with_declaration_body - -and with_declaration_body = - With_module_body of Id.t list * module_path - | With_definition_body of Id.t list * constant_body - -and module_body = - { mod_mp : module_path; - mod_expr : struct_expr_body option; - mod_type : struct_expr_body; - mod_type_alg : struct_expr_body option; - mod_constraints : constraints; - mod_delta : delta_resolver; - mod_retroknowledge : Retroknowledge.action list} - -and module_type_body = - { typ_mp : module_path; - typ_expr : struct_expr_body; - typ_expr_alg : struct_expr_body option ; - typ_constraints : constraints; - typ_delta :delta_resolver} diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 5b5e1750c..3a05f9309 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -7,11 +7,7 @@ (************************************************************************) open Names -open Univ open Term -open Cemitcodes -open Sign -open Mod_subst (** This module defines the internal representation of global declarations. This includes global constants/axioms, mutual @@ -22,33 +18,14 @@ type engagement = ImpredicativeSet (** {6 Representation of constants (Definition/Axiom) } *) type polymorphic_arity = { - poly_param_levels : universe option list; - poly_level : universe; + poly_param_levels : Univ.universe option list; + poly_level : Univ.universe; } type constant_type = | NonPolymorphicType of types | PolymorphicArity of rel_context * polymorphic_arity -type constr_substituted - -val from_val : constr -> constr_substituted -val force : constr_substituted -> constr - -(** Opaque proof terms are not loaded immediately, but are there - in a lazy form. Forcing this lazy may trigger some unmarshal of - the necessary structure. *) - -type lazy_constr - -val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr -val force_lazy_constr : lazy_constr -> constr_substituted -val make_lazy_constr : constr_substituted Lazy.t -> lazy_constr -val lazy_constr_is_val : lazy_constr -> bool - -val force_opaque : lazy_constr -> constr -val opaque_from_val : constr -> lazy_constr - (** Inlining level of parameters at functor applications. None means no inlining *) @@ -59,8 +36,8 @@ type inline = int option type constant_def = | Undef of inline - | Def of constr_substituted - | OpaqueDef of lazy_constr + | Def of Lazyconstr.constr_substituted + | OpaqueDef of Lazyconstr.lazy_constr type native_name = | Linked of string @@ -69,27 +46,14 @@ type native_name = | NotLinked type constant_body = { - const_hyps : section_context; (** New: younger hyp at top *) + const_hyps : Sign.section_context; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; - const_body_code : to_patch_substituted; - const_constraints : constraints; + const_body_code : Cemitcodes.to_patch_substituted; + const_constraints : Univ.constraints; const_native_name : native_name ref; const_inline_code : bool } -val subst_const_def : substitution -> constant_def -> constant_def -val subst_const_body : substitution -> constant_body -> constant_body - -(** Is there a actual body in const_body or const_body_opaque ? *) - -val constant_has_body : constant_body -> bool - -(** Accessing const_body_opaque or const_body *) - -val body_of_constant : constant_body -> constr_substituted option - -val is_opaque : constant_body -> bool - (** {6 Representation of mutual inductive types in the kernel } *) type recarg = @@ -97,20 +61,8 @@ type recarg = | Mrec of inductive | Imbr of inductive -val eq_recarg : recarg -> recarg -> bool - -val subst_recarg : substitution -> recarg -> recarg - type wf_paths = recarg Rtree.t -val mk_norec : wf_paths -val mk_paths : recarg -> wf_paths list array -> wf_paths -val dest_recarg : wf_paths -> recarg -val dest_subterms : wf_paths -> wf_paths list array -val recarg_length : wf_paths -> int -> int - -val subst_wf_paths : substitution -> wf_paths -> wf_paths - (** {v Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1 @@ -179,7 +131,7 @@ type mutual_inductive_body = { mind_ntypes : int; (** Number of types in the block *) - mind_hyps : section_context; (** Section hypotheses on which the block depends *) + mind_hyps : Sign.section_context; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters *) @@ -187,7 +139,7 @@ type mutual_inductive_body = { mind_params_ctxt : rel_context; (** The context of parameters (includes let-in declaration) *) - mind_constraints : constraints; (** Universes constraints enforced by the inductive declaration *) + mind_constraints : Univ.constraints; (** Universes constraints enforced by the inductive declaration *) (** {8 Data for native compilation } *) @@ -196,8 +148,6 @@ type mutual_inductive_body = { } -val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body - (** {6 Modules: signature component specifications, module types, and module declarations } *) @@ -216,7 +166,7 @@ and structure_body = (Label.t * structure_field_body) list and struct_expr_body = | SEBident of module_path | SEBfunctor of MBId.t * module_type_body * struct_expr_body - | SEBapply of struct_expr_body * struct_expr_body * constraints + | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints | SEBstruct of structure_body | SEBwith of struct_expr_body * with_declaration_body @@ -228,36 +178,26 @@ and module_body = { (** absolute path of the module *) mod_mp : module_path; (** Implementation *) - mod_expr : struct_expr_body option; + mod_expr : struct_expr_body option; (** Signature *) mod_type : struct_expr_body; - (** algebraic structure expression is kept + (** algebraic structure expression is kept if it's relevant for extraction *) - mod_type_alg : struct_expr_body option; + mod_type_alg : struct_expr_body option; (** set of all constraint in the module *) - mod_constraints : constraints; + mod_constraints : Univ.constraints; (** quotiented set of equivalent constant and inductive name *) - mod_delta : delta_resolver; + mod_delta : Mod_subst.delta_resolver; mod_retroknowledge : Retroknowledge.action list} - + and module_type_body = - { + { (** Path of the module type *) typ_mp : module_path; typ_expr : struct_expr_body; - (** algebraic structure expression is kept + (** algebraic structure expression is kept if it's relevant for extraction *) typ_expr_alg : struct_expr_body option ; - typ_constraints : constraints; + typ_constraints : Univ.constraints; (** quotiented set of equivalent constant and inductive name *) - typ_delta :delta_resolver} - - -(** Hash-consing *) - -(** Here, strictly speaking, we don't perform true hash-consing - of the structure, but simply hash-cons all inner constr - and other known elements *) - -val hcons_const_body : constant_body -> constant_body -val hcons_mind : mutual_inductive_body -> mutual_inductive_body + typ_delta : Mod_subst.delta_resolver} diff --git a/kernel/declareops.ml b/kernel/declareops.ml new file mode 100644 index 000000000..90327da6c --- /dev/null +++ b/kernel/declareops.ml @@ -0,0 +1,201 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* None + | Def c -> Some c + | OpaqueDef lc -> Some (force_lazy_constr lc) + +let constant_has_body cb = match cb.const_body with + | Undef _ -> false + | Def _ | OpaqueDef _ -> true + +let is_opaque cb = match cb.const_body with + | OpaqueDef _ -> true + | Undef _ | Def _ -> false + +(** Constant substitutions *) + +let subst_rel_declaration sub (id,copt,t as x) = + let copt' = Option.smartmap (subst_mps sub) copt in + let t' = subst_mps sub t in + if copt == copt' & t == t' then x else (id,copt',t') + +let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) + +(* TODO: these substitution functions could avoid duplicating things + when the substitution have preserved all the fields *) + +let subst_const_type sub arity = + if is_empty_subst sub then arity + else match arity with + | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) + | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) + +let subst_const_def sub = function + | Undef inl -> Undef inl + | Def c -> Def (subst_constr_subst sub c) + | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc) + +let subst_const_body sub cb = { + const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false); + const_body = subst_const_def sub cb.const_body; + const_type = subst_const_type sub cb.const_type; + const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; + const_constraints = cb.const_constraints; + const_native_name = ref NotLinked; + const_inline_code = cb.const_inline_code } + +(** Hash-consing of constants *) + +let hcons_rel_decl ((n,oc,t) as d) = + let n' = Names.Name.hcons n + and oc' = Option.smartmap Term.hcons_constr oc + and t' = Term.hcons_types t + in if n' == n && oc' == oc && t' == t then d else (n',oc',t') + +let hcons_rel_context l = List.smartmap hcons_rel_decl l + +let hcons_polyarity ar = + { poly_param_levels = + List.smartmap (Option.smartmap Univ.hcons_univ) ar.poly_param_levels; + poly_level = Univ.hcons_univ ar.poly_level } + +let hcons_const_type = function + | NonPolymorphicType t -> + NonPolymorphicType (Term.hcons_constr t) + | PolymorphicArity (ctx,s) -> + PolymorphicArity (hcons_rel_context ctx, hcons_polyarity s) + +let hcons_const_def = function + | Undef inl -> Undef inl + | Def l_constr -> + let constr = force l_constr in + Def (from_val (Term.hcons_constr constr)) + | OpaqueDef lc -> + if lazy_constr_is_val lc then + let constr = force_opaque lc in + OpaqueDef (opaque_from_val (Term.hcons_constr constr)) + else OpaqueDef lc + +let hcons_const_body cb = + { cb with + const_body = hcons_const_def cb.const_body; + const_type = hcons_const_type cb.const_type; + const_constraints = Univ.hcons_constraints cb.const_constraints } + +(** Inductive types *) + +let eq_recarg r1 r2 = match r1, r2 with +| Norec, Norec -> true +| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 +| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 +| _ -> false + +let subst_recarg sub r = match r with + | Norec -> r + | Mrec (kn,i) -> let kn' = subst_ind sub kn in + if kn==kn' then r else Mrec (kn',i) + | Imbr (kn,i) -> let kn' = subst_ind sub kn in + if kn==kn' then r else Imbr (kn',i) + +let mk_norec = Rtree.mk_node Norec [||] + +let mk_paths r recargs = + Rtree.mk_node r + (Array.map (fun l -> Rtree.mk_node Norec (Array.of_list l)) recargs) + +let dest_recarg p = fst (Rtree.dest_node p) + +(* dest_subterms returns the sizes of each argument of each constructor of + an inductive object of size [p]. This should never be done for Norec, + because the number of sons does not correspond to the number of + constructors. + *) +let dest_subterms p = + let (ra,cstrs) = Rtree.dest_node p in + assert (match ra with Norec -> false | _ -> true); + Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs + +let recarg_length p j = + let (_,cstrs) = Rtree.dest_node p in + Array.length (snd (Rtree.dest_node cstrs.(j-1))) + +let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p + +(** Substitution of inductive declarations *) + +let subst_indarity sub = function +| Monomorphic s -> + Monomorphic { + mind_user_arity = subst_mps sub s.mind_user_arity; + mind_sort = s.mind_sort; + } +| Polymorphic s as x -> x + +let subst_mind_packet sub mbp = + { mind_consnames = mbp.mind_consnames; + mind_consnrealdecls = mbp.mind_consnrealdecls; + mind_typename = mbp.mind_typename; + mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; + mind_arity = subst_indarity sub mbp.mind_arity; + mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; + mind_nrealargs = mbp.mind_nrealargs; + mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; + mind_kelim = mbp.mind_kelim; + mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); + mind_nb_constant = mbp.mind_nb_constant; + mind_nb_args = mbp.mind_nb_args; + mind_reloc_tbl = mbp.mind_reloc_tbl } + +let subst_mind sub mib = + { mind_record = mib.mind_record ; + mind_finite = mib.mind_finite ; + mind_ntypes = mib.mind_ntypes ; + mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); + mind_nparams = mib.mind_nparams; + mind_nparams_rec = mib.mind_nparams_rec; + mind_params_ctxt = + Sign.map_rel_context (subst_mps sub) mib.mind_params_ctxt; + mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; + mind_constraints = mib.mind_constraints; + mind_native_name = ref NotLinked } + +(** Hash-consing of inductive declarations *) + +let hcons_indarity = function + | Monomorphic a -> + Monomorphic { mind_user_arity = Term.hcons_constr a.mind_user_arity; + mind_sort = Term.hcons_sorts a.mind_sort } + | Polymorphic a -> Polymorphic (hcons_polyarity a) + +let hcons_mind_packet oib = + { oib with + mind_typename = Names.Id.hcons oib.mind_typename; + mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; + mind_arity = hcons_indarity oib.mind_arity; + mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames; + mind_user_lc = Array.smartmap Term.hcons_types oib.mind_user_lc; + mind_nf_lc = Array.smartmap Term.hcons_types oib.mind_nf_lc } + +let hcons_mind mib = + { mib with + mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; + mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; + mind_constraints = Univ.hcons_constraints mib.mind_constraints } diff --git a/kernel/declareops.mli b/kernel/declareops.mli new file mode 100644 index 000000000..1616e4639 --- /dev/null +++ b/kernel/declareops.mli @@ -0,0 +1,56 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constant_def -> constant_def +val subst_const_body : substitution -> constant_body -> constant_body + +(** Is there a actual body in const_body or const_body_opaque ? *) + +val constant_has_body : constant_body -> bool + +(** Accessing const_body_opaque or const_body *) + +val body_of_constant : constant_body -> constr_substituted option + +val is_opaque : constant_body -> bool + + +(** {6 Inductive types} *) + +val eq_recarg : recarg -> recarg -> bool + +val subst_recarg : substitution -> recarg -> recarg + +val mk_norec : wf_paths +val mk_paths : recarg -> wf_paths list array -> wf_paths +val dest_recarg : wf_paths -> recarg +val dest_subterms : wf_paths -> wf_paths list array +val recarg_length : wf_paths -> int -> int + +val subst_wf_paths : substitution -> wf_paths -> wf_paths + +val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body + + +(** {6 Hash-consing} *) + +(** Here, strictly speaking, we don't perform true hash-consing + of the structure, but simply hash-cons all inner constr + and other known elements *) + +val hcons_const_body : constant_body -> constant_body +val hcons_mind : mutual_inductive_body -> mutual_inductive_body diff --git a/kernel/entries.mli b/kernel/entries.mli index 20742d341..650c3566d 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -7,9 +7,7 @@ (************************************************************************) open Names -open Univ open Term -open Sign (** This module defines the entry types for global declarations. This information is entered in the environments. This includes global @@ -52,14 +50,14 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; - const_entry_secctx : section_context option; + const_entry_secctx : Sign.section_context option; const_entry_type : types option; const_entry_opaque : bool; const_entry_inline_code : bool } type inline = int option (* inlining level, None for no inlining *) -type parameter_entry = section_context option * types * inline +type parameter_entry = Sign.section_context option * types * inline type constant_entry = | DefinitionEntry of definition_entry @@ -80,5 +78,3 @@ and with_declaration = and module_entry = { mod_entry_type : module_struct_entry option; mod_entry_expr : module_struct_entry option} - - diff --git a/kernel/environ.ml b/kernel/environ.ml index a36e2dcf6..0063aa6f2 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -174,7 +174,7 @@ exception NotEvaluableConst of const_evaluation_result let constant_value env kn = let cb = lookup_constant kn env in match cb.const_body with - | Def l_body -> Declarations.force l_body + | Def l_body -> Lazyconstr.force l_body | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index d80c69bee..e6faaaa85 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -12,6 +12,7 @@ open Names open Univ open Term open Declarations +open Declareops open Inductive open Environ open Reduction diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 31d9f48ac..3132b7e79 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -12,6 +12,7 @@ open Names open Univ open Term open Declarations +open Declareops open Environ open Reduction open Type_errors @@ -414,8 +415,10 @@ type subterm_spec = | Dead_code | Not_subterm +let eq_wf_paths = Rtree.eq_rtree Declareops.eq_recarg + let spec_of_tree t = lazy - (if Rtree.eq_rtree eq_recarg (Lazy.force t) mk_norec + (if eq_wf_paths (Lazy.force t) mk_norec then Not_subterm else Subterm(Strict,Lazy.force t)) @@ -427,7 +430,7 @@ let subterm_spec_glb = | Not_subterm, _ -> Not_subterm | _, Not_subterm -> Not_subterm | Subterm (a1,t1), Subterm (a2,t2) -> - if Rtree.eq_rtree eq_recarg t1 t2 then Subterm (size_glb a1 a2, t1) + if eq_wf_paths t1 t2 then Subterm (size_glb a1 a2, t1) (* branches do not return objects with same spec *) else Not_subterm in Array.fold_left glb2 Dead_code @@ -877,7 +880,7 @@ let check_one_cofix env nbfix def deftype = let realargs = List.skipn mib.mind_nparams args in let rec process_args_of_constr = function | (t::lr), (rar::lrar) -> - if Rtree.eq_rtree eq_recarg rar mk_norec then + if eq_wf_paths rar mk_norec then if noccur_with_meta n nbfix t then process_args_of_constr (lr, lrar) else raise (CoFixGuardError diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 07f24583e..ef3ef6d94 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -8,7 +8,8 @@ Cbytecodes Copcodes Cemitcodes Nativevalues -Declarations +Lazyconstr +Declareops Retroknowledge Pre_env Cbytegen diff --git a/kernel/lazyconstr.ml b/kernel/lazyconstr.ml new file mode 100644 index 000000000..31cb76575 --- /dev/null +++ b/kernel/lazyconstr.ml @@ -0,0 +1,43 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr_substituted +val force : constr_substituted -> constr +val subst_constr_subst : + substitution -> constr_substituted -> constr_substituted + +(** Opaque proof terms are not loaded immediately, but are there + in a lazy form. Forcing this lazy may trigger some unmarshal of + the necessary structure. *) + +type lazy_constr + +val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr +val force_lazy_constr : lazy_constr -> constr_substituted +val make_lazy_constr : constr_substituted Lazy.t -> lazy_constr +val lazy_constr_is_val : lazy_constr -> bool + +val force_opaque : lazy_constr -> constr +val opaque_from_val : constr -> lazy_constr diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index b566dd8af..b24deb0dc 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -105,12 +105,12 @@ and check_with_def env sign (idl,c) mp equiv = (union_constraints cb.const_constraints cst1) cst2 in - let def = Def (Declarations.from_val j.uj_val) in + let def = Def (Lazyconstr.from_val j.uj_val) in def,cst | Def cs -> - let cst1 = Reduction.conv env' c (Declarations.force cs) in + let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in let cst = union_constraints cb.const_constraints cst1 in - let def = Def (Declarations.from_val c) in + let def = Def (Lazyconstr.from_val c) in def,cst in let cb' = diff --git a/kernel/modops.ml b/kernel/modops.ml index 986118655..c1b5d788d 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -20,6 +20,7 @@ open Util open Names open Term open Declarations +open Declareops open Environ open Entries open Mod_subst @@ -287,7 +288,7 @@ let strengthen_const mp_from l cb resolver = let kn = KerName.make2 mp_from l in let con = constant_of_delta_kn resolver kn in { cb with - const_body = Def (Declarations.from_val (mkConst con)); + const_body = Def (Lazyconstr.from_val (mkConst con)); const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) } @@ -377,7 +378,7 @@ let inline_delta_resolver env inl mp mbid mtb delta = match constant.const_body with | Undef _ | OpaqueDef _ -> l | Def body -> - let constr = Declarations.force body in + let constr = Lazyconstr.force body in add_inline_delta_resolver kn (lev, Some constr) l with Not_found -> error_no_such_label_sub (con_label con) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 7b878c53e..932b490e3 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1319,7 +1319,7 @@ and compile_named env auxdefs id = let compile_constant env prefix con body = match body with | Def t -> - let t = Declarations.force t in + let t = Lazyconstr.force t in let code = lambda_of_constr env t in let code, name = if is_lazy t then mk_lazy code, LinkedLazy prefix @@ -1414,7 +1414,7 @@ let rec compile_deps env prefix ~interactive init t = then init else let comp_stack, (mind_updates, const_updates) = match cb.const_body with - | Def t -> compile_deps env prefix ~interactive init (Declarations.force t) + | Def t -> compile_deps env prefix ~interactive init (Lazyconstr.force t) | _ -> init in let code, name = compile_constant env prefix c cb.const_body in @@ -1429,7 +1429,7 @@ let compile_constant_field env prefix con (code, symb, (mupds, cupds)) cb = let acc = (code, (mupds, cupds)) in match cb.const_body with | Def t -> - let t = Declarations.force t in + let t = Lazyconstr.force t in let (code, (mupds, cupds)) = compile_deps env prefix ~interactive:false acc t in let (gl, name) = compile_constant env prefix con cb.const_body in let cupds = Cmap_env.add con (cb.const_native_name, name) cupds in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index f530f6e2e..9c400e4c0 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -631,11 +631,13 @@ and lambda_of_app env f args = let cb = lookup_constant kn !global_env in begin match cb.const_body with | Def csubst -> - if cb.const_inline_code then lambda_of_app env (force csubst) args + if cb.const_inline_code then + lambda_of_app env (Lazyconstr.force csubst) args else let prefix = get_const_prefix !global_env kn in let t = - if is_lazy (force csubst) then mkLapp Lforce [|Lconst (prefix, kn)|] + if is_lazy (Lazyconstr.force csubst) then + mkLapp Lforce [|Lconst (prefix, kn)|] else Lconst (prefix, kn) in mkLapp t (lambda_of_args env 0 args) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8a9822b18..932e43163 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -271,7 +271,7 @@ let add_constant dir l decl senv = | ConstantEntry ce -> translate_constant senv.env kn ce | GlobalRecipe r -> let cb = translate_recipe senv.env kn r in - if DirPath.is_empty dir then hcons_const_body cb else cb + if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb in let senv' = add_field (l,SFBconst cb) (C kn) senv in let senv'' = match cb.const_body with @@ -296,7 +296,8 @@ let add_mind dir l mie senv = type do not match"); let kn = make_mind senv.modinfo.modpath dir l in let mib = translate_mind senv.env kn mie in - let mib = match mib.mind_hyps with [] -> hcons_mind mib | _ -> mib in + let mib = match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib + in let senv' = add_field (l,SFBmind mib) (I kn) senv in kn, senv' @@ -780,9 +781,9 @@ end = struct [lightened_compiled_library] is abstract and only meant for writing to .vo via Marshal (which doesn't care about types). *) - type table = constr_substituted array - let key_as_lazy_constr (i:int) = (Obj.magic i : lazy_constr) - let key_of_lazy_constr (c:lazy_constr) = (Obj.magic c : int) + type table = Lazyconstr.constr_substituted array + let key_as_lazy_constr (i:int) = (Obj.magic i : Lazyconstr.lazy_constr) + let key_of_lazy_constr (c:Lazyconstr.lazy_constr) = (Obj.magic c : int) (* To avoid any future misuse of the lightened library that could interpret encoded keys as real [constr_substituted], we hide @@ -812,7 +813,7 @@ end = struct } and traverse_struct struc = let traverse_body (l,body) = (l,match body with - | SFBconst cb when is_opaque cb -> + | SFBconst cb when Declareops.is_opaque cb -> SFBconst {cb with const_body = on_opaque_const_body cb.const_body} | (SFBconst _ | SFBmind _ ) as x -> x @@ -855,7 +856,7 @@ end = struct ((* Insert inside the table. *) (fun def -> let opaque_definition = match def with - | OpaqueDef lc -> force_lazy_constr lc + | OpaqueDef lc -> Lazyconstr.force_lazy_constr lc | _ -> assert false in incr counter; @@ -886,10 +887,10 @@ end = struct match load_proof with | Flags.Force -> let lc = Lazy.lazy_from_val (access k) in - OpaqueDef (make_lazy_constr lc) + OpaqueDef (Lazyconstr.make_lazy_constr lc) | Flags.Lazy -> let lc = lazy (access k) in - OpaqueDef (make_lazy_constr lc) + OpaqueDef (Lazyconstr.make_lazy_constr lc) | Flags.Dont -> Undef None in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 8f46831b8..e5b81c72f 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -94,10 +94,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let check_conv why cst f = check_conv_error error why cst f in let mib1 = match info1 with - | IndType ((_,0), mib) -> subst_mind subst1 mib + | IndType ((_,0), mib) -> Declareops.subst_mind subst1 mib | _ -> error (InductiveFieldExpected mib2) in - let mib2 = subst_mind subst2 mib2 in + let mib2 = Declareops.subst_mind subst2 mib2 in let check_inductive_type cst name env t1 t2 = (* Due to sort-polymorphism in inductive types, the conclusions of @@ -270,8 +270,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = match info1 with | Constant cb1 -> let () = assert (List.is_empty cb1.const_hyps && List.is_empty cb2.const_hyps) in - let cb1 = subst_const_body subst1 cb1 in - let cb2 = subst_const_body subst2 cb2 in + let cb1 = Declareops.subst_const_body subst1 cb1 in + let cb2 = Declareops.subst_const_body subst2 cb2 in (* Start by checking types*) let typ1 = Typeops.type_of_constant_type env cb1.const_type in let typ2 = Typeops.type_of_constant_type env cb2.const_type in @@ -290,8 +290,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = | Def lc1 -> (* NB: cb1 might have been strengthened and appear as transparent. Anyway [check_conv] will handle that afterwards. *) - let c1 = Declarations.force lc1 in - let c2 = Declarations.force lc2 in + let c1 = Lazyconstr.force lc1 in + let c2 = Lazyconstr.force lc2 in check_conv NotConvertibleBodyField cst conv env c1 c2)) | IndType ((kn,i),mind1) -> ignore (Errors.error ( @@ -300,7 +300,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "inductive type and give a definition to map the old name to the new " ^ "name.")); let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in - if constant_has_body cb2 then error DefinitionFieldExpected; + if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in let error = NotConvertibleTypeField (arity1, typ2) in @@ -312,7 +312,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "constructor and give a definition to map the old name to the new " ^ "name.")); let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in - if constant_has_body cb2 then error DefinitionFieldExpected; + if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in let error = NotConvertibleTypeField (ty1, ty2) in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 1cd006f25..3ec0da457 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -96,8 +96,8 @@ let infer_declaration env dcl = let (typ,cst) = constrain_type env j cst c.const_entry_type in let def = if c.const_entry_opaque - then OpaqueDef (Declarations.opaque_from_val j.uj_val) - else Def (Declarations.from_val j.uj_val) + then OpaqueDef (Lazyconstr.opaque_from_val j.uj_val) + else Def (Lazyconstr.from_val j.uj_val) in def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx | ParameterEntry (ctx,t,nl) -> @@ -119,9 +119,9 @@ let build_constant_declaration env kn (def,typ,cst,inline_code,ctx) = let ids_typ = global_vars_set_constant_type env typ in let ids_def = match def with | Undef _ -> Id.Set.empty - | Def cs -> global_vars_set env (Declarations.force cs) + | Def cs -> global_vars_set env (Lazyconstr.force cs) | OpaqueDef lc -> - global_vars_set env (Declarations.force_opaque lc) in + global_vars_set env (Lazyconstr.force_opaque lc) in keep_hyps env (Id.Set.union ids_typ ids_def) in let declared = match ctx with | None -> inferred -- cgit v1.2.3