aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml4
-rw-r--r--checker/check_stat.ml1
-rw-r--r--checker/checker.ml2
-rw-r--r--checker/cic.mli331
-rw-r--r--checker/closure.ml3
-rw-r--r--checker/closure.mli2
-rw-r--r--checker/declarations.ml206
-rw-r--r--checker/declarations.mli191
-rw-r--r--checker/environ.ml1
-rw-r--r--checker/environ.mli33
-rw-r--r--checker/indtypes.ml1
-rw-r--r--checker/indtypes.mli3
-rw-r--r--checker/inductive.ml1
-rw-r--r--checker/inductive.mli3
-rw-r--r--checker/mod_checking.ml1
-rw-r--r--checker/mod_checking.mli2
-rw-r--r--checker/modops.ml1
-rw-r--r--checker/modops.mli3
-rw-r--r--checker/reduction.ml1
-rw-r--r--checker/reduction.mli1
-rw-r--r--checker/safe_typing.ml1
-rw-r--r--checker/safe_typing.mli4
-rw-r--r--checker/subtyping.ml1
-rw-r--r--checker/subtyping.mli4
-rw-r--r--checker/term.ml70
-rw-r--r--checker/term.mli52
-rw-r--r--checker/type_errors.ml1
-rw-r--r--checker/type_errors.mli2
-rw-r--r--checker/typeops.ml1
-rw-r--r--checker/typeops.mli3
-rw-r--r--kernel/term.mli4
31 files changed, 387 insertions, 547 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*)
diff --git a/kernel/term.mli b/kernel/term.mli
index c5f23ae9c..e585e66b7 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -95,7 +95,7 @@ val mkSet : types
val mkType : Univ.universe -> types
-(* This defines the strategy to use for verifiying a Cast *)
+(** This defines the strategy to use for verifiying a Cast *)
type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the
@@ -331,7 +331,7 @@ val destFix : constr -> fixpoint
val destCoFix : constr -> cofixpoint
-(** {6 Local } *)
+(** {6 Local context} *)
(** A {e declaration} has the form [(name,body,type)]. It is either an
{e assumption} if [body=None] or a {e definition} if
[body=Some actualbody]. It is referred by {e name} if [na] is an
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 22:15:39 +0000