aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-26 18:52:24 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-26 18:52:24 +0000
commit60de53d159c85b8300226a61aa502a7e0dd2f04b (patch)
treee542ed90d58872a75816d451ae26e38fa7b1d9f9 /kernel
parent7dd28b4772251af6ae3641ec63a8251153915e21 (diff)
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
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytegen.ml2
-rw-r--r--kernel/cooking.ml8
-rw-r--r--kernel/declarations.ml430
-rw-r--r--kernel/declarations.mli100
-rw-r--r--kernel/declareops.ml201
-rw-r--r--kernel/declareops.mli56
-rw-r--r--kernel/entries.mli8
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/indtypes.ml1
-rw-r--r--kernel/inductive.ml9
-rw-r--r--kernel/kernel.mllib3
-rw-r--r--kernel/lazyconstr.ml43
-rw-r--r--kernel/lazyconstr.mli34
-rw-r--r--kernel/mod_typing.ml6
-rw-r--r--kernel/modops.ml5
-rw-r--r--kernel/nativecode.ml6
-rw-r--r--kernel/nativelambda.ml6
-rw-r--r--kernel/safe_typing.ml19
-rw-r--r--kernel/subtyping.ml16
-rw-r--r--kernel/term_typing.ml8
20 files changed, 406 insertions, 557 deletions
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