summaryrefslogtreecommitdiff
path: root/checker/declarations.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /checker/declarations.mli
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'checker/declarations.mli')
-rw-r--r--checker/declarations.mli212
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