diff options
39 files changed, 466 insertions, 603 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 0b6ec899e..7db5b5cb9 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -47,7 +47,8 @@ Cbytecodes Copcodes Cemitcodes Nativevalues -Declarations +Lazyconstr +Declareops Retroknowledge Pre_env Nativelambda diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 0dc09f9ba..db895fc0f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -49,7 +49,7 @@ let rawdebug = ref false let ppconstr x = pp (Termops.print_constr x) let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) let ppterm = ppconstr -let ppsconstr x = ppconstr (Declarations.force x) +let ppsconstr x = ppconstr (Lazyconstr.force x) let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr x)) let pppattern = (fun x -> pp(pr_constr_pattern x)) 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* This file is a late renaming in May 2000 of constant.ml which - itself was made for V7.0 in Aug 1999 out of a dispatch by - Jean-Christophe Filliâtre of Chet Murthy's constants.ml in V5.10.5 - into cooking.ml, declare.ml and constant.ml, ...; renaming done - because the new contents exceeded in extent what the name - suggested *) -(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *) -(* Declarations for the module systems added by Jacek Chrzaszcz, Aug 2002 *) -(* Miscellaneous extensions, cleaning or restructurations by Bruno - Barras, Hugo Herbelin, Jean-Christophe Filliâtre, Pierre Letouzey *) - -(* This module defines the types of global declarations. This includes - global constants/axioms, mutual inductive definitions and the - module system *) - -open Util -open Names -open Univ -open Term -open Sign -open Mod_subst - -type engagement = ImpredicativeSet - -(*s Constants (internal representation) (Definition/Axiom) *) - -type polymorphic_arity = { - poly_param_levels : universe option list; - poly_level : universe; -} - -type constant_type = - | NonPolymorphicType of types - | PolymorphicArity of rel_context * polymorphic_arity - -type constr_substituted = constr substituted - -let from_val = from_val - -let force = force subst_mps - -let subst_constr_subst = subst_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. The ['a substituted] type isn't really great - here, so we store "manually" a substitution list, the younger one at top. -*) - -type lazy_constr = constr_substituted Lazy.t * substitution list - -let force_lazy_constr (c,l) = - List.fold_right subst_constr_subst l (Lazy.force c) - -let lazy_constr_is_val (c,_) = Lazy.lazy_is_val c - -let make_lazy_constr c = (c, []) - -let force_opaque lc = force (force_lazy_constr lc) - -let opaque_from_val c = (Lazy.lazy_from_val (from_val c), []) - -let subst_lazy_constr sub (c,l) = (c,sub::l) - -(** Inlining level of parameters at functor applications. - None means no inlining *) - -type inline = int option - -(** A constant can have no body (axiom/parameter), or a - transparent body, or an opaque one *) - -type constant_def = - | Undef of inline - | Def of constr_substituted - | OpaqueDef of lazy_constr - -type native_name = - | Linked of string - | LinkedLazy of string - | LinkedInteractive of string - | NotLinked - -type constant_body = { - const_hyps : section_context; (* New: younger hyp at top *) - const_body : constant_def; - const_type : constant_type; - const_body_code : Cemitcodes.to_patch_substituted; - const_constraints : constraints; - const_native_name : native_name ref; - const_inline_code : bool } - -let body_of_constant cb = match cb.const_body with - | Undef _ -> 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 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Declarations +open Mod_subst +open Lazyconstr +open Util + +(** Operations concernings types in [Declarations] : + [constant_body], [mutual_inductive_body], [module_body] ... *) + +(** Constants *) + +let body_of_constant cb = match cb.const_body with + | Undef _ -> 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 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Declarations +open Mod_subst +open Lazyconstr + +(** Operations concerning types in [Declarations] : + [constant_body], [mutual_inductive_body], [module_body] ... *) + +(** {6 Constants} *) + +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 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 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Term +open Mod_subst + +(** [constr_substituted] are [constr] with possibly pending + substitutions of kernel names. *) + +type constr_substituted = constr substituted + +let from_val = from_val + +let force = force subst_mps + +let subst_constr_subst = subst_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. The ['a substituted] type isn't really great + here, so we store "manually" a substitution list, the younger one at top. +*) + +type lazy_constr = constr_substituted Lazy.t * substitution list + +let force_lazy_constr (c,l) = + List.fold_right subst_constr_subst l (Lazy.force c) + +let lazy_constr_is_val (c,_) = Lazy.lazy_is_val c + +let make_lazy_constr c = (c, []) + +let force_opaque lc = force (force_lazy_constr lc) + +let opaque_from_val c = (Lazy.lazy_from_val (from_val c), []) + +let subst_lazy_constr sub (c,l) = (c,sub::l) + diff --git a/kernel/lazyconstr.mli b/kernel/lazyconstr.mli new file mode 100644 index 000000000..17c9bcc76 --- /dev/null +++ b/kernel/lazyconstr.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Term +open Mod_subst + +(** [constr_substituted] are [constr] with possibly pending + substitutions of kernel names. *) + +type constr_substituted + +val from_val : constr -> 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 diff --git a/library/assumptions.ml b/library/assumptions.ml index ee916c237..2d99aca8c 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -151,7 +151,7 @@ let lookup_constant_in_impl cst fallback = let lookup_constant cst = try let cb = Global.lookup_constant cst in - if constant_has_body cb then cb + if Declareops.constant_has_body cb then cb else lookup_constant_in_impl cst (Some cb) with Not_found -> lookup_constant_in_impl cst None @@ -227,8 +227,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = (s,ContextObjectMap.add cst ctype acc) in let (s,acc) = - if Declarations.constant_has_body cb then - if Declarations.is_opaque cb || not (Cpred.mem kn knst) then + if Declareops.constant_has_body cb then + if Declareops.is_opaque cb || not (Cpred.mem kn knst) then (** it is opaque *) if add_opaque then do_type (Opaque kn) else (s, acc) @@ -237,9 +237,9 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = else (s, acc) else (s, acc) in - match Declarations.body_of_constant cb with + match Declareops.body_of_constant cb with | None -> do_type (Axiom kn) - | Some body -> do_constr (Declarations.force body) s acc + | Some body -> do_constr (Lazyconstr.force body) s acc and do_memoize_kn kn = try_and_go (Axiom kn) (add_kn kn) diff --git a/library/declaremods.ml b/library/declaremods.ml index 591567fea..c30b2099f 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -524,7 +524,7 @@ let rec seb2mse = function | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp)) | SEBwith (s,With_definition_body(l,cb)) -> (match cb.const_body with - | Def c -> MSEwith(seb2mse s,With_Definition(l,Declarations.force c)) + | Def c -> MSEwith(seb2mse s,With_Definition(l,Lazyconstr.force c)) | _ -> assert false) | _ -> failwith "seb2mse: received a non-atomic seb" diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 5aee45dcc..ae60259e9 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -136,7 +136,7 @@ let check_arity env cb = let check_fix env cb i = match cb.const_body with | Def lbody -> - (match kind_of_term (Declarations.force lbody) with + (match kind_of_term (Lazyconstr.force lbody) with | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd) | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd) | _ -> raise Impossible) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index c8f376565..035f8e3bb 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -11,6 +11,7 @@ open Util open Names open Term open Declarations +open Declareops open Environ open Reduction open Reductionops @@ -277,7 +278,7 @@ let rec extract_type env db j c args = | Undef _ | OpaqueDef _ -> mlt | Def _ when is_custom r -> mlt | Def lbody -> - let newc = applist (Declarations.force lbody, args) in + let newc = applist (Lazyconstr.force lbody, args) in let mlt' = extract_type env db j newc [] in (* ML type abbreviations interact badly with Coq *) (* reduction, so [mlt] and [mlt'] might be different: *) @@ -291,7 +292,7 @@ let rec extract_type env db j c args = | Undef _ | OpaqueDef _ -> Tunknown (* Brutal approx ... *) | Def lbody -> (* We try to reduce. *) - let newc = applist (Declarations.force lbody, args) in + let newc = applist (Lazyconstr.force lbody, args) in extract_type env db j newc [])) | Ind (kn,i) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in @@ -515,7 +516,7 @@ and mlt_env env r = match r with | Def l_body -> (match flag_of_type env typ with | Info,TypeScheme -> - let body = Declarations.force l_body in + let body = Lazyconstr.force l_body in let s,vl = type_sign_vl env typ in let db = db_from_sign s in let t = extract_type_scheme env db body (List.length s) @@ -986,17 +987,21 @@ let extract_constant env kn cb = | (Info,TypeScheme) -> (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () - | Def c -> mk_typ (force c) + | Def c -> mk_typ (Lazyconstr.force c) | OpaqueDef c -> add_opaque r; - if access_opaque () then mk_typ (force_opaque c) else mk_typ_ax ()) + if access_opaque () then + mk_typ (Lazyconstr.force_opaque c) + else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with | Undef _ -> warn_info (); mk_ax () - | Def c -> mk_def (force c) + | Def c -> mk_def (Lazyconstr.force c) | OpaqueDef c -> add_opaque r; - if access_opaque () then mk_def (force_opaque c) else mk_ax ()) + if access_opaque () then + mk_def (Lazyconstr.force_opaque c) + else mk_ax ()) let extract_constant_spec env kn cb = let r = ConstRef kn in @@ -1010,7 +1015,8 @@ let extract_constant_spec env kn cb = | Undef _ | OpaqueDef _ -> Stype (r, vl, None) | Def body -> let db = db_from_sign s in - let t = extract_type_scheme env db (force body) (List.length s) + let body = Lazyconstr.force body in + let t = extract_type_scheme env db body (List.length s) in Stype (r, vl, Some t)) | (Info, Default) -> let t = snd (record_constant_type env kn (Some typ)) in @@ -1023,7 +1029,7 @@ let extract_with_type env cb = let s,vl = type_sign_vl env typ in let db = db_from_sign s in let c = match cb.const_body with - | Def body -> force body + | Def body -> Lazyconstr.force body (* A "with Definition ..." is necessarily transparent *) | Undef _ | OpaqueDef _ -> assert false in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 8ecd8cd7c..4407c6798 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1289,6 +1289,7 @@ let is_not_strict t = *) open Declarations +open Declareops let inline_test r t = if not (auto_inline ()) then false diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 450b3ef40..3c92bb5bd 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -5,6 +5,7 @@ open Term open Namegen open Names open Declarations +open Declareops open Pp open Hiddentac open Tacmach @@ -947,7 +948,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let f_def = Global.lookup_constant (destConst f) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in let f_body = - force (Option.get (body_of_constant f_def)) + Lazyconstr.force (Option.get (body_of_constant f_def)) in let params,f_body_with_params = decompose_lam_n nb_params f_body in let (_,num),(_,_,bodies) = destFix f_body_with_params in @@ -1065,7 +1066,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let get_body const = match body_of_constant (Global.lookup_constant const) with | Some b -> - let body = force b in + let body = Lazyconstr.force b in Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) (Global.env ()) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 9916ed95a..debf96345 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -5,6 +5,7 @@ open Term open Namegen open Names open Declarations +open Declareops open Pp open Entries open Tactics @@ -404,7 +405,7 @@ let get_funs_constant mp dp = let find_constant_body const = match body_of_constant (Global.lookup_constant const) with | Some b -> - let body = force b in + let body = Lazyconstr.force b in let body = Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) (Global.env ()) @@ -539,7 +540,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis let finfos = find_Function_infos this_block_funs.(0) in try let equation = Option.get finfos.equation_lemma in - Declarations.is_opaque (Global.lookup_constant equation) + Declareops.is_opaque (Global.lookup_constant equation) with Option.IsNone -> (* non recursive definition *) false in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 99bf66d1f..fd4e23de7 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -8,6 +8,7 @@ open Libnames open Globnames open Glob_term open Declarations +open Declareops open Misctypes open Decl_kinds @@ -770,7 +771,7 @@ let make_graph (f_ref:global_reference) = | None -> error "Cannot build a graph over an axiom !" | Some b -> let env = Global.env () in - let body = (force b) in + let body = Lazyconstr.force b in let extern_body,extern_type = with_full_print (fun () -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 92d2fe680..9879f08a0 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -121,8 +121,8 @@ let const_of_id id = let def_of_const t = match (Term.kind_of_term t) with Term.Const sp -> - (try (match Declarations.body_of_constant (Global.lookup_constant sp) with - | Some c -> Declarations.force c + (try (match Declareops.body_of_constant (Global.lookup_constant sp) with + | Some c -> Lazyconstr.force c | _ -> assert false) with _ -> assert false) |_ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d5e1ee53a..bea019259 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -10,6 +10,7 @@ open Term open Namegen open Environ open Declarations +open Declareops open Entries open Pp open Names @@ -68,7 +69,7 @@ let def_of_const t = match (kind_of_term t) with Const sp -> (try (match body_of_constant (Global.lookup_constant sp) with - | Some c -> Declarations.force c + | Some c -> Lazyconstr.force c | _ -> assert false) with _ -> anomaly (str "Cannot find definition of constant " ++ diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 033c84691..4d9541ebc 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -229,12 +229,11 @@ let mk_constant_obj id bo ty variables hyps = Acic.Constant (Names.Id.to_string id,None,ty,params) | Some c -> Acic.Constant - (Names.Id.to_string id, Some (Unshare.unshare (Declarations.force c)), + (Names.Id.to_string id, Some (Unshare.unshare (Lazyconstr.force c)), ty,params) ;; let mk_inductive_obj sp mib packs variables nparams hyps finite = - let module D = Declarations in let hyps = string_list_of_named_context_list hyps in let params = filter_params variables hyps in (* let nparams = extract_nparams packs in *) @@ -243,8 +242,8 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite = Array.fold_right (fun p i -> decr tyno ; - let {D.mind_consnames=consnames ; - D.mind_typename=typename } = p + let {Declarations.mind_consnames=consnames ; + Declarations.mind_typename=typename } = p in let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in @@ -368,7 +367,7 @@ let print_object_kind uri (xmltag,variation) = (* form of the definition (all the parameters are *) (* lambda-abstracted, but the object can still refer to variables) *) let print internal glob_ref kind xml_library_root = - let module D = Declarations in + let module D = Declareops in let module De = Declare in let module G = Global in let module N = Names in @@ -392,16 +391,16 @@ let print internal glob_ref kind xml_library_root = let id = N.Label.to_id (N.con_label kn) in let cb = G.lookup_constant kn in let val0 = D.body_of_constant cb in - let typ = cb.D.const_type in - let hyps = cb.D.const_hyps in + let typ = cb.Declarations.const_type in + let hyps = cb.Declarations.const_hyps in let typ = Typeops.type_of_constant_type (Global.env()) typ in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Gn.IndRef (kn,_) -> let mib = G.lookup_mind kn in - let {D.mind_nparams=nparams; - D.mind_packets=packs ; - D.mind_hyps=hyps; - D.mind_finite=finite} = mib in + let {Declarations.mind_nparams=nparams; + Declarations.mind_packets=packs ; + Declarations.mind_hyps=hyps; + Declarations.mind_finite=finite} = mib in Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite | Gn.ConstructRef _ -> Errors.error ("a single constructor cannot be printed in XML") diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index bf166f128..a5c4ecd3b 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -20,6 +20,7 @@ open Nameops open Term open Namegen open Declarations +open Declareops open Inductive open Inductiveops open Environ diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 3880dfd4e..0017fee78 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -14,6 +14,7 @@ open Term open Termops open Namegen open Declarations +open Declareops open Environ open Reductionops diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 732903af9..18bfeb6d6 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -399,7 +399,7 @@ let gallina_print_section_variable id = with_line_skip (print_name_infos (VarRef id)) let print_body = function - | Some lc -> pr_lconstr (Declarations.force lc) + | Some lc -> pr_lconstr (Lazyconstr.force lc) | None -> (str"<no body>") let print_typed_body (val_0,typ) = @@ -411,7 +411,7 @@ let ungeneralized_type_of_constant_type = function let print_constant with_values sep sp = let cb = Global.lookup_constant sp in - let val_0 = body_of_constant cb in + let val_0 = Declareops.body_of_constant cb in let typ = ungeneralized_type_of_constant_type cb.const_type in hov 0 ( match val_0 with @@ -566,11 +566,11 @@ let print_full_pure_context () = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr (Declarations.force_opaque lc) + str "Proof " ++ pr_lconstr (Lazyconstr.force_opaque lc) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ - pr_lconstr (Declarations.force c)) + pr_lconstr (Lazyconstr.force c)) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> let mind = Global.mind_of_delta_kn kn in @@ -654,7 +654,7 @@ let print_opaque_name qid = match global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in - if constant_has_body cb then + if Declareops.constant_has_body cb then print_constant_with_infos cst else error "Not a defined constant." diff --git a/printing/printmod.ml b/printing/printmod.ml index 07a5d954c..57d990b86 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -120,7 +120,7 @@ let print_body is_impl env mp (l,body) = | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env (Declarations.force l)) + Printer.pr_lconstr_env env (Lazyconstr.force l)) | _ -> mt ()) ++ str ".") | SFBmind mib -> diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f7a8a787c..b2d39b57a 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -201,7 +201,7 @@ let compute_construtor_signatures isrec (_,k as ity) = let rec analrec c recargs = match kind_of_term c, recargs with | Prod (_,_,c), recarg::rest -> - let b = match dest_recarg recarg with + let b = match Declareops.dest_recarg recarg with | Norec | Imbr _ -> false | Mrec (_,j) -> isrec && Int.equal j k in b :: (analrec c rest) @@ -213,7 +213,7 @@ let compute_construtor_signatures isrec (_,k as ity) = let n = mib.mind_nparams in let lc = Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in - let lrecargs = dest_subterms mip.mind_recargs in + let lrecargs = Declareops.dest_subterms mip.mind_recargs in Array.map2 analrec lc lrecargs let elimination_sort_of_goal gl = diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 65655ed90..bf8cbcc25 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -16,6 +16,7 @@ open Pp open Names open Term open Declarations +open Declareops open Entries open Environ open Nameops @@ -40,7 +41,7 @@ let retrieve_first_recthm = function (pi2 (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - (Option.map Declarations.force (body_of_constant cb), is_opaque cb) + (Option.map Lazyconstr.force (body_of_constant cb), is_opaque cb) | _ -> assert false let adjust_guardness_conditions const = function |