Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

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