diff options
Diffstat (limited to 'checker/cic.mli')
-rw-r--r-- | checker/cic.mli | 444 |
1 files changed, 444 insertions, 0 deletions
diff --git a/checker/cic.mli b/checker/cic.mli new file mode 100644 index 00000000..a793fefa --- /dev/null +++ b/checker/cic.mli @@ -0,0 +1,444 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \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, YOU SHOULD MODIFY values.ml ACCORDINGLY ! +*) + +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_tags : bool list; (* tell whether letin or lambda in the arity of the inductive type *) + cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *) + 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 pattern vars of each constructor (with let's)*) + ci_cstr_nargs : int array; (* number of pattern vars of each constructor (w/o let's) *) + 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 'a puniverses = 'a Univ.puniverses +type pconstant = constant puniverses +type pinductive = inductive puniverses +type pconstructor = constructor puniverses + +type constr = + | Rel of int + | Var of Id.t (** Shouldn't occur in a .vo *) + | Meta of metavariable (** Shouldn't occur in a .vo *) + | Evar of constr pexistential (** Shouldn't occur in a .vo *) + | 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 pconstant + | Ind of pinductive + | Construct of pconstructor + | Case of case_info * constr * constr * constr array + | Fix of constr pfixpoint + | CoFix of constr pcofixpoint + | Proj of constant * constr + +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 rel_declaration = Name.t * constr option * constr +type rel_context = rel_declaration list + +(** The declarations below in .vo should be outside sections, + so we expect there a value compatible with an empty list *) +type section_context = unit + + +(*************************************************************************) +(** {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 substituted = { + mutable subst_value : 'a; + mutable subst_subst : substitution list; +} + +type constr_substituted = constr 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 *) + + +(*************************************************************************) +(** {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 template_arity = { + template_param_levels : Univ.universe_level option list; + template_level : Univ.universe; +} + +type ('a, 'b) declaration_arity = + | RegularArity of 'a + | TemplateArity of 'b + +type constant_type = (constr, rel_context * template_arity) declaration_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 *) + +(** Projections are a particular kind of constant: + always transparent. *) + +type projection_body = { + proj_ind : mutual_inductive; + proj_npars : int; + proj_arg : int; + proj_type : constr; (* Type under params *) + proj_eta : constr * constr; (* Eta-expanded term and type *) + proj_body : constr; (* For compatibility, the match version *) +} + +type constant_def = + | Undef of inline + | Def of constr_substituted + | OpaqueDef of lazy_constr + +type constant_universes = Univ.universe_context + +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_polymorphic : bool; (** Is it polymorphic or not *) + const_universes : constant_universes; + const_proj : projection_body option; + 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 record_body = (Id.t * constant array * projection_body array) option + (* The body is empty for non-primitive records, otherwise we get its + binder name in projections and list of projections if it is primitive. *) + +type regular_inductive_arity = { + mind_user_arity : constr; + mind_sort : sorts; +} + +type recursivity_kind = + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) + +type inductive_arity = (regular_inductive_arity, template_arity) declaration_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_nrealdecls : 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_consnrealargs : int array; + (** Length of the signature of the constructors (w/o let, w/o params) + (not used in the kernel) *) + + 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 : record_body option; (** Whether the inductive type has been declared as a record. *) + + mind_finite : recursivity_kind; (** 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_polymorphic : bool; (** Is it polymorphic or not *) + + mind_universes : Univ.universe_context; (** Local universe variables and constraints *) + + mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) + +(** {8 Data for native compilation } *) + + mind_native_name : native_name ref; (** status of the code (linked or not, and where) *) + } + +(** {6 Module declarations } *) + +(** Functor expressions are forced to be on top of other expressions *) + +type ('ty,'a) functorize = + | NoFunctor of 'a + | MoreFunctor of MBId.t * 'ty * ('ty,'a) functorize + +(** The fully-algebraic module expressions : names, applications, 'with ...'. + They correspond to the user entries of non-interactive modules. + They will be later expanded into module structures in [Mod_typing], + and won't play any role into the kernel after that : they are kept + only for short module printing and for extraction. *) + +type with_declaration = + | WithMod of Id.t list * module_path + | WithDef of Id.t list * constr + +type module_alg_expr = + | MEident of module_path + | MEapply of module_alg_expr * module_path + | MEwith of module_alg_expr * with_declaration + +(** A component of a module structure *) + +type structure_field_body = + | SFBconst of constant_body + | SFBmind of mutual_inductive_body + | SFBmodule of module_body + | SFBmodtype of module_type_body + +(** A module structure is a list of labeled components. + + Note : we may encounter now (at most) twice the same label in + a [structure_body], once for a module ([SFBmodule] or [SFBmodtype]) + and once for an object ([SFBconst] or [SFBmind]) *) + +and structure_body = (Label.t * structure_field_body) list + +(** A module signature is a structure, with possibly functors on top of it *) + +and module_signature = (module_type_body,structure_body) functorize + +(** A module expression is an algebraic expression, possibly functorized. *) + +and module_expression = (module_type_body,module_alg_expr) functorize + +and module_implementation = + | Abstract (** no accessible implementation (keep this constructor first!) *) + | Algebraic of module_expression (** non-interactive algebraic expression *) + | Struct of module_signature (** interactive body *) + | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) + +and module_body = + { mod_mp : module_path; (** absolute path of the module *) + mod_expr : module_implementation; (** implementation *) + mod_type : module_signature; (** expanded type *) + (** algebraic type, kept if it's relevant for extraction *) + mod_type_alg : module_expression option; + (** set of all constraints in the module *) + mod_constraints : Univ.constraints; + (** quotiented set of equivalent constants and inductive names *) + mod_delta : delta_resolver; + mod_retroknowledge : action list } + +(** A [module_type_body] is just a [module_body] with no + implementation ([mod_expr] always [Abstract]) and also + an empty [mod_retroknowledge] *) + +and module_type_body = module_body + +(*************************************************************************) +(** {4 From safe_typing.ml} *) + +type nativecode_symb_array + +type compilation_unit_name = DirPath.t + +type vodigest = + | Dvo of Digest.t (* The digest of the seg_lib part *) + | Dviovo of Digest.t * Digest.t (* The digest of the seg_lib+seg_univ part *) + +type library_info = compilation_unit_name * vodigest + +type library_deps = library_info array + +type compiled_library = { + comp_name : compilation_unit_name; + comp_mod : module_body; + comp_deps : library_deps; + comp_enga : engagement option; + comp_natsymbs : nativecode_symb_array +} + + +(*************************************************************************) +(** {4 From library.ml} *) + +type library_objects + +type library_disk = { + md_name : compilation_unit_name; + md_compiled : compiled_library; + md_objects : library_objects; + md_deps : library_deps; + md_imports : compilation_unit_name array } + +type opaque_table = constr Future.computation array +type univ_table = + (Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool) option + +(** A .vo file is currently made of : + + 1) a magic number (4 bytes, cf output_binary_int) + 2) a marshalled [library_disk] structure + 3) a [Digest.t] string (16 bytes) + 4) a marshalled [univ_table] (* Some if vo was obtained from vi *) + 5) a [Digest.t] string (16 bytes) + 6) a marshalled [None] discharge_table (* Some in vi files *) + 7) a [Digest.t] string (16 bytes) + 8) a marshalled [None] todo_table (* Some in vi files *) + 9) a [Digest.t] string (16 bytes) + 10) a marshalled [opaque_table] + 11) a [Digest.t] string (16 bytes) +*) |