diff options
Diffstat (limited to 'checker/declarations.mli')
| -rw-r--r-- | checker/declarations.mli | 212 |
1 files changed, 212 insertions, 0 deletions
diff --git a/checker/declarations.mli b/checker/declarations.mli new file mode 100644 index 00000000..fdea3383 --- /dev/null +++ b/checker/declarations.mli @@ -0,0 +1,212 @@ +open Util +open Names +open Term + +(* Bytecode *) +type values +type reloc_table +type to_patch_substituted +(*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 constant_body = { + const_hyps : section_context; (* New: younger hyp at top *) + const_body : constr_substituted option; + const_type : constant_type; + const_body_code : to_patch_substituted; + const_constraints : Univ.constraints; + const_opaque : bool; + const_inline : bool} + +(* Mutual inductives *) + +type recarg = + | Norec + | Mrec of int + | 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_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 : identifier; + + (* 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 : identifier 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; + + (* 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; + + (* Source of the inductive block when aliased in a module *) + mind_equiv : kernel_name option + } + +(* Modules *) + +type substitution + +type structure_field_body = + | SFBconst of constant_body + | SFBmind of mutual_inductive_body + | SFBmodule of module_body + | SFBalias of module_path * Univ.constraints option + | SFBmodtype of module_type_body + +and structure_body = (label * structure_field_body) list + +and struct_expr_body = + | SEBident of module_path + | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body + | SEBstruct of mod_self_id * structure_body + | SEBapply of struct_expr_body * struct_expr_body + * Univ.constraints + | SEBwith of struct_expr_body * with_declaration_body + +and with_declaration_body = + With_module_body of identifier list * module_path * Univ.constraints + | With_definition_body of identifier list * constant_body + +and module_body = + { mod_expr : struct_expr_body option; + mod_type : struct_expr_body option; + mod_constraints : Univ.constraints; + mod_alias : substitution; + mod_retroknowledge : action list} + +and module_type_body = + { typ_expr : struct_expr_body; + typ_strength : module_path option; + typ_alias : substitution} + +(* Substitutions *) + +val fold_subst : + (mod_self_id -> module_path -> 'a -> 'a) -> + (mod_bound_id -> module_path -> 'a -> 'a) -> + (module_path -> module_path -> 'a -> 'a) -> + substitution -> 'a -> 'a + +type 'a subst_fun = substitution -> 'a -> 'a + +val empty_subst : substitution +val add_msid : mod_self_id -> module_path -> substitution -> substitution +val add_mbid : mod_bound_id -> module_path -> substitution -> substitution +val add_mp : module_path -> module_path -> substitution -> substitution +val map_msid : mod_self_id -> module_path -> substitution +val map_mbid : mod_bound_id -> module_path -> substitution +val map_mp : module_path -> module_path -> substitution + +val subst_const_body : constant_body subst_fun +val subst_mind : mutual_inductive_body subst_fun +val subst_modtype : substitution -> module_type_body -> module_type_body +val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body +val subst_structure : substitution -> structure_body -> structure_body +val subst_signature_msid : + mod_self_id -> module_path -> structure_body -> structure_body + +val join : substitution -> substitution -> substitution +val join_alias : substitution -> substitution -> substitution +val update_subst_alias : substitution -> substitution -> substitution +val update_subst : substitution -> substitution -> substitution +val subst_key : substitution -> substitution -> substitution |