diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 16:04:56 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 16:04:56 +0000 |
commit | 56c88d763b0cf636a740f531bd7d734426769d7d (patch) | |
tree | 720ad9b125abc6d1d2faaf65d218e365fcd64a06 /checker | |
parent | 6a05c7e546a9dd2065f35b788b35e7a85866dfc8 (diff) |
Checker: regroup all vo-related types in cic.mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker')
-rw-r--r-- | checker/check.ml | 4 | ||||
-rw-r--r-- | checker/check_stat.ml | 1 | ||||
-rw-r--r-- | checker/checker.ml | 2 | ||||
-rw-r--r-- | checker/cic.mli | 331 | ||||
-rw-r--r-- | checker/closure.ml | 3 | ||||
-rw-r--r-- | checker/closure.mli | 2 | ||||
-rw-r--r-- | checker/declarations.ml | 206 | ||||
-rw-r--r-- | checker/declarations.mli | 191 | ||||
-rw-r--r-- | checker/environ.ml | 1 | ||||
-rw-r--r-- | checker/environ.mli | 33 | ||||
-rw-r--r-- | checker/indtypes.ml | 1 | ||||
-rw-r--r-- | checker/indtypes.mli | 3 | ||||
-rw-r--r-- | checker/inductive.ml | 1 | ||||
-rw-r--r-- | checker/inductive.mli | 3 | ||||
-rw-r--r-- | checker/mod_checking.ml | 1 | ||||
-rw-r--r-- | checker/mod_checking.mli | 2 | ||||
-rw-r--r-- | checker/modops.ml | 1 | ||||
-rw-r--r-- | checker/modops.mli | 3 | ||||
-rw-r--r-- | checker/reduction.ml | 1 | ||||
-rw-r--r-- | checker/reduction.mli | 1 | ||||
-rw-r--r-- | checker/safe_typing.ml | 1 | ||||
-rw-r--r-- | checker/safe_typing.mli | 4 | ||||
-rw-r--r-- | checker/subtyping.ml | 1 | ||||
-rw-r--r-- | checker/subtyping.mli | 4 | ||||
-rw-r--r-- | checker/term.ml | 70 | ||||
-rw-r--r-- | checker/term.mli | 52 | ||||
-rw-r--r-- | checker/type_errors.ml | 1 | ||||
-rw-r--r-- | checker/type_errors.mli | 2 | ||||
-rw-r--r-- | checker/typeops.ml | 1 | ||||
-rw-r--r-- | checker/typeops.mli | 3 |
30 files changed, 385 insertions, 545 deletions
diff --git a/checker/check.ml b/checker/check.ml index 1b9fd0701..7ac15393a 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -56,7 +56,7 @@ type library_t = { library_name : compilation_unit_name; library_filename : CUnix.physical_path; library_compiled : Safe_typing.compiled_library; - library_opaques : Term.constr array; + library_opaques : Cic.constr array; library_deps : (compilation_unit_name * Digest.t) array; library_digest : Digest.t } @@ -314,7 +314,7 @@ let intern_from_file (dir, f) = let ch = with_magic_number_check raw_intern_library f in let (md:library_disk) = System.marshal_in f ch in let (digest:Digest.t) = System.marshal_in f ch in - let (table:Term.constr array) = System.marshal_in f ch in + let (table:Cic.constr array) = System.marshal_in f ch in (* Verification of the final checksum *) let pos = pos_in ch in let (checksum:Digest.t) = System.marshal_in f ch in diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 3176a4307..62d5ac064 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -8,6 +8,7 @@ open Pp open Names +open Cic open Declarations open Environ diff --git a/checker/checker.ml b/checker/checker.ml index 6b76b6b32..e981cf8fe 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -284,7 +284,7 @@ let parse_args argv = let rec parse = function | [] -> () | "-impredicative-set" :: rem -> - set_engagement Declarations.ImpredicativeSet; parse rem + set_engagement Cic.ImpredicativeSet; parse rem | "-coqlib" :: s :: rem -> if not (exists_dir s) then diff --git a/checker/cic.mli b/checker/cic.mli new file mode 100644 index 000000000..5c1345ba0 --- /dev/null +++ b/checker/cic.mli @@ -0,0 +1,331 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Type definitions for the Calculus of Inductive Constructions *) + +(** We regroup here the type definitions for structures of the Coq kernel + that are present in .vo files. Here is everything the Checker needs + to know about these structures for verifying a .vo. Note that this + isn't an exact copy of the kernel code : + + - there isn't any abstraction here (see e.g. [constr] or [lazy_constr]) + - some types are left undefined when they aren't used by the Checker + - some types have less constructors when the final constructors aren't + supposed to appear in .vo (see [REVERTcast] and [Direct]). + + The following types are also described in a reified manner in values.ml, + for validating the layout of structures after de-marshalling. So: + + IF YOU ADAPT THIS FILE, PLEASE MODIFY ACCORDINGLY values.ml ! +*) + +open Names + +(*************************************************************************) +(** {4 From term.ml} *) + +(** {6 The sorts of CCI. } *) + +type contents = Pos | Null + +type sorts = + | Prop of contents (** Prop and Set *) + | Type of Univ.universe (** Type *) + +(** {6 The sorts family of CCI. } *) + +type sorts_family = InProp | InSet | InType + +(** {6 Useful types } *) + +(** {6 Existential variables } *) +type existential_key = int + +(** {6 Existential variables } *) +type metavariable = int + +(** {6 Case annotation } *) +type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle + | RegularStyle (** infer printing form from number of constructor *) +type case_printing = + { ind_nargs : int; (** length of the arity of the inductive type *) + style : case_style } + +(** the integer is the number of real args, needed for reduction *) +type case_info = + { ci_ind : inductive; + ci_npar : int; + ci_cstr_ndecls : int array; (** number of real args of each constructor *) + ci_pp_info : case_printing (** not interpreted by the kernel *) + } + +(** This defines the strategy to use for verifiying a Cast. *) +type cast_kind = VMcast | NATIVEcast | DEFAULTcast (* | REVERTcast *) + +(** {6 The type of constructions } *) + +(** [constr array] is an instance matching definitional [named_context] in + the same order (i.e. last argument first) *) +type 'constr pexistential = existential_key * 'constr array +type 'constr prec_declaration = + Name.t array * 'constr array * 'constr array +type 'constr pfixpoint = + (int array * int) * 'constr prec_declaration +type 'constr pcofixpoint = + int * 'constr prec_declaration + +type constr = + | Rel of int + | Var of Id.t + | Meta of metavariable + | Evar of constr pexistential + | Sort of sorts + | Cast of constr * cast_kind * constr + | Prod of Name.t * constr * constr + | Lambda of Name.t * constr * constr + | LetIn of Name.t * constr * constr * constr + | App of constr * constr array + | Const of constant + | Ind of inductive + | Construct of constructor + | Case of case_info * constr * constr * constr array + | Fix of constr pfixpoint + | CoFix of constr pcofixpoint + +type existential = constr pexistential +type rec_declaration = constr prec_declaration +type fixpoint = constr pfixpoint +type cofixpoint = constr pcofixpoint + +(** {6 Type of assumptions and contexts} *) + +type named_declaration = Id.t * constr option * constr +type rel_declaration = Name.t * constr option * constr + +type rel_context = rel_declaration list + + +(*************************************************************************) +(** {4 From sign.ml} *) + +type named_context = named_declaration list +type section_context = named_context + + +(*************************************************************************) +(** {4 From mod_susbt.ml and lazyconstr.ml} *) + +(** {6 Substitutions} *) + +type delta_hint = + | Inline of int * constr option + | Equiv of kernel_name + +type delta_resolver = module_path MPmap.t * delta_hint KNmap.t + +type 'a umap_t = 'a MPmap.t * 'a MBImap.t +type substitution = (module_path * delta_resolver) umap_t + +(** {6 Delayed constr} *) + +type 'a lazy_subst = + | LSval of 'a + | LSlazy of substitution list * 'a + +type constr_substituted = constr lazy_subst ref + +(** Nota : in coqtop, the [lazy_constr] type also have a [Direct] + constructor, but it shouldn't occur inside a .vo, so we ignore it *) + +type lazy_constr = + | Indirect of substitution list * DirPath.t * int +(* | Direct of constr_substituted *) + + +(*************************************************************************) +(** {4 From declarations.mli} *) + +(** Some types unused in the checker, hence left undefined *) + +(** Bytecode *) +type reloc_table +type to_patch_substituted +(** Native code *) +type native_name +(** Retroknowledge *) +type action + +(** Engagements *) + +type engagement = ImpredicativeSet + +(** {6 Representation of constants (Definition/Axiom) } *) + +type polymorphic_arity = { + poly_param_levels : Univ.universe option list; + poly_level : Univ.universe; +} + +type constant_type = + | NonPolymorphicType of constr + | PolymorphicArity of rel_context * polymorphic_arity + +(** Inlining level of parameters at functor applications. + This is ignored by the checker. *) + +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 constant_body = { + const_hyps : section_context; (** New: younger hyp at top *) + const_body : constant_def; + const_type : constant_type; + const_body_code : to_patch_substituted; + const_constraints : Univ.constraints; + const_native_name : native_name ref; + const_inline_code : bool } + +(** {6 Representation of mutual inductive types } *) + +type recarg = + | Norec + | Mrec of inductive + | Imbr of inductive + +type wf_paths = recarg Rtree.t + +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 = { +(** {8 Primitive datas } *) + + mind_typename : Id.t; (** Name of the type: [Ii] *) + + mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) + + mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *) + + mind_consnames : Id.t array; (** Names of the constructors: [cij] *) + + mind_user_lc : constr 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 *) + +(** {8 Derived datas } *) + + mind_nrealargs : int; (** Number of expected real arguments of the type (no let, no params) *) + + mind_nrealargs_ctxt : int; (** Length of realargs context (with let, no params) *) + + mind_kelim : sorts_family list; (** List of allowed elimination sorts *) + + mind_nf_lc : constr array; (** Head normalized constructor types so that their conclusion is atomic *) + + mind_consnrealdecls : int array; + (** Length of the signature of the constructors (with let, w/o params) + (not used in the kernel) *) + + mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *) + +(** {8 Datas for bytecode compilation } *) + + mind_nb_constant : int; (** number of constant constructor *) + + mind_nb_args : int; (** number of no constant constructor *) + + mind_reloc_tbl : reloc_table; + } + +type mutual_inductive_body = { + + mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) + + mind_record : bool; (** Whether the inductive type has been declared as a record *) + + mind_finite : bool; (** Whether the type is inductive or coinductive *) + + mind_ntypes : int; (** Number of types in the block *) + + mind_hyps : section_context; (** Section hypotheses on which the block depends *) + + mind_nparams : int; (** Number of expected parameters *) + + mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *) + + mind_params_ctxt : rel_context; (** The context of parameters (includes let-in declaration) *) + + mind_constraints : Univ.constraints; (** Universes constraints enforced by the inductive declaration *) + +(** {8 Data for native compilation } *) + + mind_native_name : native_name ref; (** status of the code (linked or not, and where) *) + } + +(** {6 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 * 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 * Univ.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 = + { (** absolute path of the module *) + mod_mp : module_path; + (** Implementation *) + mod_expr : struct_expr_body option; + (** Signature *) + mod_type : struct_expr_body; + (** algebraic structure expression is kept + if it's relevant for extraction *) + mod_type_alg : struct_expr_body option; + (** set of all constraint in the module *) + mod_constraints : Univ.constraints; + (** quotiented set of equivalent constant and inductive name *) + mod_delta : delta_resolver; + mod_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 + if it's relevant for extraction *) + typ_expr_alg : struct_expr_body option ; + typ_constraints : Univ.constraints; + (** quotiented set of equivalent constant and inductive name *) + typ_delta : delta_resolver} diff --git a/checker/closure.ml b/checker/closure.ml index 9677680e6..45452874e 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -8,8 +8,9 @@ open Util open Pp -open Term open Names +open Cic +open Term open Esubst open Environ diff --git a/checker/closure.mli b/checker/closure.mli index 443eeb6aa..bee6b1bb8 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -9,7 +9,7 @@ (*i*) open Pp open Names -open Term +open Cic open Esubst open Environ (*i*) diff --git a/checker/declarations.ml b/checker/declarations.ml index cfaa2f5f7..42d49e83b 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -1,45 +1,21 @@ open Util open Names +open Cic open Term open Validate -(* Bytecode *) -type values -type reloc_table -type to_patch_substituted -(* Native code *) -type native_name -(*Retroknowledge *) -type action -type retroknowledge - -type engagement = ImpredicativeSet let val_eng = val_enum "eng" 1 - -type polymorphic_arity = { - poly_param_levels : Univ.universe option list; - poly_level : Univ.universe; -} let val_pol_arity = val_tuple ~name:"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|] -type constant_type = - | NonPolymorphicType of constr - | PolymorphicArity of rel_context * polymorphic_arity - let val_cst_type = val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|] (** Substitutions, code imported from kernel/mod_subst *) -type delta_hint = - | Inline of int * constr option - | Equiv of kernel_name - - module Deltamap = struct - type t = module_path MPmap.t * delta_hint KNmap.t + type t = delta_resolver let empty = MPmap.empty, KNmap.empty let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km) @@ -55,12 +31,10 @@ module Deltamap = struct let join map1 map2 = fold add_mp add_kn map1 map2 end -type delta_resolver = Deltamap.t - let empty_delta_resolver = Deltamap.empty module Umap = struct - type 'a t = 'a MPmap.t * 'a MBImap.t + type 'a t = 'a umap_t let empty = MPmap.empty, MBImap.empty let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2 let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2) @@ -75,7 +49,6 @@ module Umap = struct let join map1 map2 = fold add_mp add_mbi map1 map2 end -type substitution = (module_path * delta_resolver) Umap.t type 'a subst_fun = substitution -> 'a -> 'a let empty_subst = Umap.empty @@ -324,13 +297,6 @@ let subst_mps sub c = if is_empty_subst sub then c else map_kn (subst_ind sub) (subst_con0 sub) c - -type 'a lazy_subst = - | LSval of 'a - | LSlazy of substitution list * 'a - -type 'a substituted = 'a lazy_subst ref - let val_substituted val_a = val_ref (val_sum "constr_substituted" 0 @@ -482,19 +448,10 @@ let force_constr = force subst_mps let from_val c = ref (LSval c) -type constr_substituted = constr substituted - let val_cstr_subst = val_substituted val_constr let subst_constr_subst = subst_substituted -(* Nota : in coqtop, the [lazy_constr] type also have a [Direct] - constructor, but it shouldn't occur inside a .vo, so we ignore it *) - -type lazy_constr = - | Indirect of substitution list * DirPath.t * int -(* | Direct of constr_substituted *) - let subst_lazy_constr sub = function | Indirect (l,dp,i) -> Indirect (sub::l,dp,i) @@ -509,19 +466,6 @@ let force_lazy_constr = function let val_lazy_constr = val_sum "lazy_constr" 0 [|[|val_list val_subst;val_dp;val_int|]|] -(** Inlining level of parameters at functor applications. - This is ignored by the checker. *) - -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 - let val_cst_def = val_sum "constant_def" 0 [|[|val_opt val_int|]; [|val_cstr_subst|]; [|val_lazy_constr|]|] @@ -531,15 +475,6 @@ let subst_constant_def sub = function | Def c -> Def (subst_constr_subst sub c) | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc) -type constant_body = { - const_hyps : section_context; (* New: younger hyp at top *) - const_body : constant_def; - const_type : constant_type; - const_body_code : to_patch_substituted; - const_constraints : Univ.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 (force_constr c) @@ -569,10 +504,6 @@ let subst_rel_declaration sub (id,copt,t as x) = let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) -type recarg = - | Norec - | Mrec of inductive - | Imbr of inductive let val_recarg = val_sum "recarg" 1 (* Norec *) [|[|val_ind|] (* Mrec *);[|val_ind|] (* Imbr *)|] @@ -581,7 +512,6 @@ let subst_recarg sub r = match r with | (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 val_wfp = val_rec_sum "wf_paths" 0 (fun val_wfp -> [|[|val_int;val_int|]; (* Rtree.Param *) @@ -611,110 +541,17 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn *) -type monomorphic_inductive_arity = { - mind_user_arity : constr; - mind_sort : sorts; -} let val_mono_ind_arity = val_tuple ~name:"monomorphic_inductive_arity"[|val_constr;val_sort|] -type inductive_arity = -| Monomorphic of monomorphic_inductive_arity -| Polymorphic of polymorphic_arity let val_ind_arity = val_sum "inductive_arity" 0 [|[|val_mono_ind_arity|];[|val_pol_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 : constr 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 : constr 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 : reloc_table; - } - let val_one_ind = val_tuple ~name:"one_inductive_body" [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr; val_int;val_int;val_list val_sortfam;val_array val_constr;val_array val_int; val_wfp;val_int;val_int;no_val|] - -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 : Univ.constraints; - - (* Data for native compilation *) - mind_native_name : native_name ref; - - } let val_ind_pack = val_tuple ~name:"mutual_inductive_body" [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt; val_int; val_int; val_rctxt;val_cstrs;no_val|] @@ -772,43 +609,6 @@ let subst_mind sub mib = (* Modules *) -(* Whenever you change these types, please do update the validation - functions below *) -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 * 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 * Univ.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 : Univ.constraints; - mod_delta : delta_resolver; - mod_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 : Univ.constraints; - typ_delta :delta_resolver} - (* the validation functions: *) let rec val_sfb o = val_sum "struct_field_body" 0 [|[|val_cb|]; (* SFBconst *) diff --git a/checker/declarations.mli b/checker/declarations.mli index cc3123ca7..af38ab0fb 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -1,60 +1,12 @@ open Names -open Term +open Cic -(* Bytecode *) -type values -type reloc_table -type to_patch_substituted -(* Native code *) -type native_name -(*Retroknowledge *) -type action -type retroknowledge - -(* Engagements *) - -type engagement = ImpredicativeSet - -(* Constants *) - -type polymorphic_arity = { - poly_param_levels : Univ.universe option list; - poly_level : Univ.universe; -} - -type constant_type = - | NonPolymorphicType of constr - | PolymorphicArity of rel_context * polymorphic_arity - -type constr_substituted val force_constr : constr_substituted -> constr val from_val : constr -> constr_substituted -type lazy_constr - val indirect_opaque_access : (DirPath.t -> int -> constr) ref -(** Inlining level of parameters at functor applications. - This is ignored by the checker. *) - -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 constant_body = { - const_hyps : section_context; (* New: younger hyp at top *) - const_body : constant_def; - const_type : constant_type; - const_body_code : to_patch_substituted; - const_constraints : Univ.constraints; - const_native_name : native_name ref; - const_inline_code : bool } +(** Constant_body *) val body_of_constant : constant_body -> constr option val constant_has_body : constant_body -> bool @@ -62,154 +14,15 @@ val is_opaque : constant_body -> bool (* Mutual inductives *) -type recarg = - | Norec - | Mrec of inductive - | Imbr of inductive - -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 -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 : constr 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 : constr 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 : 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 : Univ.constraints; - - (* Data for native compilation *) - mind_native_name : native_name ref; - - } - (* Modules *) -type substitution -type delta_resolver val empty_delta_resolver : delta_resolver -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 * 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 * Univ.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 : Univ.constraints; - mod_delta : delta_resolver; - mod_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 : Univ.constraints; - typ_delta :delta_resolver} - (* Substitutions *) type 'a subst_fun = substitution -> 'a -> 'a diff --git a/checker/environ.ml b/checker/environ.ml index 0b475ad49..c64495d41 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -2,6 +2,7 @@ open Errors open Util open Names open Univ +open Cic open Term open Declarations diff --git a/checker/environ.mli b/checker/environ.mli index 095d93ae5..4165f0bcf 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -1,17 +1,18 @@ open Names -open Term +open Cic + (* Environments *) type globals = { - env_constants : Declarations.constant_body Cmap_env.t; - env_inductives : Declarations.mutual_inductive_body Mindmap_env.t; + env_constants : constant_body Cmap_env.t; + env_inductives : mutual_inductive_body Mindmap_env.t; env_inductives_eq : kernel_name KNmap.t; - env_modules : Declarations.module_body MPmap.t; - env_modtypes : Declarations.module_type_body MPmap.t} + env_modules : module_body MPmap.t; + env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : Univ.universes; - env_engagement : Declarations.engagement option; + env_engagement : engagement option; } type env = { env_globals : globals; @@ -23,8 +24,8 @@ type env = { val empty_env : env (* Engagement *) -val engagement : env -> Declarations.engagement option -val set_engagement : Declarations.engagement -> env -> env +val engagement : env -> Cic.engagement option +val set_engagement : Cic.engagement -> env -> env (* Digests *) val add_digest : env -> DirPath.t -> Digest.t -> env @@ -48,8 +49,8 @@ val universes : env -> Univ.universes val add_constraints : Univ.constraints -> env -> env (* Constants *) -val lookup_constant : constant -> env -> Declarations.constant_body -val add_constant : constant -> Declarations.constant_body -> env -> env +val lookup_constant : constant -> env -> Cic.constant_body +val add_constant : constant -> Cic.constant_body -> env -> env type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant -> constr @@ -59,16 +60,16 @@ val evaluable_constant : constant -> env -> bool val mind_equiv : env -> inductive -> inductive -> bool val lookup_mind : - mutual_inductive -> env -> Declarations.mutual_inductive_body + mutual_inductive -> env -> Cic.mutual_inductive_body val add_mind : - mutual_inductive -> Declarations.mutual_inductive_body -> env -> env + mutual_inductive -> Cic.mutual_inductive_body -> env -> env (* Modules *) val add_modtype : - module_path -> Declarations.module_type_body -> env -> env + module_path -> Cic.module_type_body -> env -> env val shallow_add_module : - module_path -> Declarations.module_body -> env -> env + module_path -> Cic.module_body -> env -> env val shallow_remove_module : module_path -> env -> env -val lookup_module : module_path -> env -> Declarations.module_body -val lookup_modtype : module_path -> env -> Declarations.module_type_body +val lookup_module : module_path -> env -> Cic.module_body +val lookup_modtype : module_path -> env -> Cic.module_type_body diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 8f93ff0be..69e16386e 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -10,6 +10,7 @@ open Errors open Util open Names open Univ +open Cic open Term open Inductive open Reduction diff --git a/checker/indtypes.mli b/checker/indtypes.mli index 5c032a0ca..0029eb652 100644 --- a/checker/indtypes.mli +++ b/checker/indtypes.mli @@ -9,9 +9,8 @@ (*i*) open Names open Univ -open Term +open Cic open Typeops -open Declarations open Environ (*i*) diff --git a/checker/inductive.ml b/checker/inductive.ml index 5fdca0fab..ac9bf415c 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -10,6 +10,7 @@ open Errors open Util open Names open Univ +open Cic open Term open Reduction open Type_errors diff --git a/checker/inductive.mli b/checker/inductive.mli index d0040e3db..0e9b9ccf3 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -8,8 +8,7 @@ (*i*) open Names -open Term -open Declarations +open Cic open Environ (*i*) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index ebe44997d..089414f63 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -3,6 +3,7 @@ open Pp open Errors open Util open Names +open Cic open Term open Reduction open Typeops diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli index a88afd7b3..9425a6e3a 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -6,4 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -val check_module : Environ.env -> Names.module_path -> Declarations.module_body -> unit +val check_module : Environ.env -> Names.module_path -> Cic.module_body -> unit diff --git a/checker/modops.ml b/checker/modops.ml index 13e436a5e..20f330812 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -11,6 +11,7 @@ open Errors open Util open Pp open Names +open Cic open Term open Declarations (*i*) diff --git a/checker/modops.mli b/checker/modops.mli index ef3bb6fd2..0b94edb54 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -9,8 +9,7 @@ (*i*) open Names open Univ -open Term -open Declarations +open Cic open Environ (*i*) diff --git a/checker/reduction.ml b/checker/reduction.ml index 57e39f9ce..53a12295e 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -8,6 +8,7 @@ open Errors open Util +open Cic open Term open Univ open Closure diff --git a/checker/reduction.mli b/checker/reduction.mli index 2f6e5c3b7..915805d26 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Cic open Term open Environ (*i*) diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 492f5bc20..2ccaad3e9 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -9,6 +9,7 @@ open Pp open Errors open Util +open Cic open Names open Declarations open Environ diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index a5f014935..6a7708971 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -8,7 +8,7 @@ (*i*) open Names -open Term +open Cic open Environ (*i*) @@ -17,7 +17,7 @@ val get_env : unit -> env (* exporting and importing modules *) type compiled_library -val set_engagement : Declarations.engagement -> unit +val set_engagement : engagement -> unit val import : CUnix.physical_path -> compiled_library -> constr array -> Digest.t -> unit val unsafe_import : diff --git a/checker/subtyping.ml b/checker/subtyping.ml index d0d18c68c..609918495 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -11,6 +11,7 @@ open Errors open Util open Names open Univ +open Cic open Term open Declarations open Environ diff --git a/checker/subtyping.mli b/checker/subtyping.mli index 121e37542..e0ca4a507 100644 --- a/checker/subtyping.mli +++ b/checker/subtyping.mli @@ -7,9 +7,7 @@ (************************************************************************) (*i*) -open Univ -open Term -open Declarations +open Cic open Environ (*i*) diff --git a/checker/term.ml b/checker/term.ml index bdbc7f8ec..937b27ca0 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -15,25 +15,8 @@ open Univ open Esubst open Validate -(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *) - -type existential_key = int -type metavariable = int - -(* This defines the strategy to use for verifiying a Cast *) - -(* This defines Cases annotations *) -type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | - RegularStyle -type case_printing = - { ind_nargs : int; (* length of the arity of the inductive type *) - style : case_style } -type case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; (* number of pattern var of each constructor *) - ci_pp_info : case_printing (* not interpreted by the kernel *) - } +open Cic + let val_ci = let val_cstyle = val_enum "case_style" 5 in let val_cprint = val_tuple ~name:"case_printing" [|val_int;val_cstyle|] in @@ -41,14 +24,6 @@ let val_ci = (* Sorts. *) -type contents = Pos | Null - -type sorts = - | Prop of contents (* proposition types *) - | Type of universe - -type sorts_family = InProp | InSet | InType - let family_of_sort = function | Prop Null -> InProp | Prop Pos -> InSet @@ -61,16 +36,6 @@ let val_sortfam = val_enum "sorts_family" 3 (* Constructions as implemented *) (********************************************************************) -(* [constr array] is an instance matching definitional [named_context] in - the same order (i.e. last argument first) *) -type 'constr pexistential = existential_key * 'constr array -type 'constr prec_declaration = - name array * 'constr array * 'constr array -type 'constr pfixpoint = - (int array * int) * 'constr prec_declaration -type 'constr pcofixpoint = - int * 'constr prec_declaration - let val_evar f = val_tuple ~name:"pexistential" [|val_int;val_array f|] let val_prec f = val_tuple ~name:"prec_declaration" @@ -80,30 +45,11 @@ let val_fix f = [|val_tuple~name:"fix2"[|val_array val_int;val_int|];val_prec f|] let val_cofix f = val_tuple ~name:"pcofixpoint"[|val_int;val_prec f|] -type cast_kind = VMcast | NATIVEcast | DEFAULTcast let val_cast = val_enum "cast_kind" 3 (*s*******************************************************************) (* The type of constructions *) -type constr = - | Rel of int - | Var of Id.t - | Meta of metavariable - | Evar of constr pexistential - | Sort of sorts - | Cast of constr * cast_kind * constr - | Prod of name * constr * constr - | Lambda of name * constr * constr - | LetIn of name * constr * constr * constr - | App of constr * constr array - | Const of constant - | Ind of inductive - | Construct of constructor - | Case of case_info * constr * constr * constr array - | Fix of constr pfixpoint - | CoFix of constr pcofixpoint - let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [| [|val_int|]; (* Rel *) [|val_id|]; (* Var *) @@ -123,11 +69,6 @@ let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [| [|val_cofix val_constr|] (* CoFix *) |]) -type existential = constr pexistential -type rec_declaration = constr prec_declaration -type fixpoint = constr pfixpoint -type cofixpoint = constr pcofixpoint - let rec strip_outer_cast c = match c with | Cast (c,_,_) -> strip_outer_cast c @@ -318,16 +259,9 @@ let val_rdecl = let val_nctxt = val_list val_ndecl let val_rctxt = val_list val_rdecl -type named_declaration = Id.t * constr option * constr -type rel_declaration = name * constr option * constr - -type named_context = named_declaration list let empty_named_context = [] let fold_named_context f l ~init = List.fold_right f l init -type section_context = named_context - -type rel_context = rel_declaration list let empty_rel_context = [] let rel_context_length = List.length let rel_context_nhyps hyps = diff --git a/checker/term.mli b/checker/term.mli index cc9d5cf97..4993e0718 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -1,50 +1,8 @@ open Names +open Cic -type existential_key = int -type metavariable = int -type case_style = - LetStyle - | IfStyle - | LetPatternStyle - | MatchStyle - | RegularStyle -type case_printing = { ind_nargs : int; style : case_style; } -type case_info = { - ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; - ci_pp_info : case_printing; -} -type contents = Pos | Null -type sorts = Prop of contents | Type of Univ.universe -type sorts_family = InProp | InSet | InType val family_of_sort : sorts -> sorts_family -type 'a pexistential = existential_key * 'a array -type 'a prec_declaration = name array * 'a array * 'a array -type 'a pfixpoint = (int array * int) * 'a prec_declaration -type 'a pcofixpoint = int * 'a prec_declaration -type cast_kind = VMcast | NATIVEcast | DEFAULTcast -type constr = - Rel of int - | Var of Id.t - | Meta of metavariable - | Evar of constr pexistential - | Sort of sorts - | Cast of constr * cast_kind * constr - | Prod of name * constr * constr - | Lambda of name * constr * constr - | LetIn of name * constr * constr * constr - | App of constr * constr array - | Const of constant - | Ind of inductive - | Construct of constructor - | Case of case_info * constr * constr * constr array - | Fix of constr pfixpoint - | CoFix of constr pcofixpoint -type existential = constr pexistential -type rec_declaration = constr prec_declaration -type fixpoint = constr pfixpoint -type cofixpoint = constr pcofixpoint + val strip_outer_cast : constr -> constr val collapse_appl : constr -> constr val decompose_app : constr -> constr * constr list @@ -71,14 +29,9 @@ val substnl : constr list -> int -> constr -> constr val substl : constr list -> constr -> constr val subst1 : constr -> constr -> constr -type named_declaration = Id.t * constr option * constr -type rel_declaration = name * constr option * constr -type named_context = named_declaration list val empty_named_context : named_context val fold_named_context : (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a -type section_context = named_context -type rel_context = rel_declaration list val empty_rel_context : rel_context val rel_context_length : rel_context -> int val rel_context_nhyps : rel_context -> int @@ -96,6 +49,7 @@ val decompose_prod_assum : constr -> rel_context * constr val decompose_prod_n_assum : int -> constr -> rel_context * constr type arity = rel_context * sorts + val mkArity : arity -> constr val destArity : constr -> arity val isArity : constr -> bool diff --git a/checker/type_errors.ml b/checker/type_errors.ml index bcfc31c6f..6cf814dce 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -7,6 +7,7 @@ (************************************************************************) open Names +open Cic open Term open Environ diff --git a/checker/type_errors.mli b/checker/type_errors.mli index c57b1556a..bcd4360b3 100644 --- a/checker/type_errors.mli +++ b/checker/type_errors.mli @@ -8,7 +8,7 @@ (*i*) open Names -open Term +open Cic open Environ (*i*) diff --git a/checker/typeops.ml b/checker/typeops.ml index a5b110f9b..3c6fa7c04 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -10,6 +10,7 @@ open Errors open Util open Names open Univ +open Cic open Term open Reduction open Type_errors diff --git a/checker/typeops.mli b/checker/typeops.mli index fc16c9ed0..5e71ec77f 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -8,8 +8,7 @@ (*i*) open Names -open Term -open Declarations +open Cic open Environ (*i*) |