Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 34 insertions, 12 deletions

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index e60f909e..d81904cc 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: inductive.mli 8673 2006-03-29 21:21:52Z herbelin $ i*)
+(*i $Id: inductive.mli 8871 2006-05-28 16:46:48Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -38,6 +38,8 @@ val lookup_mind_specif : env -> inductive -> mind_specif
 
 val type_of_inductive : mind_specif -> types
 
+val elim_sorts : mind_specif -> sorts_family list
+
 (* Return type as quoted by the user *)
 val type_of_constructor : constructor -> mind_specif -> types
 
@@ -58,28 +60,48 @@ val type_case_branches :
   env -> inductive * constr list -> unsafe_judgment -> constr
     -> types array * types * constraints
 
+(* Return the arity of an inductive type *)
+val mind_arity : one_inductive_body -> Sign.rel_context * sorts_family
+
+val inductive_sort_family : one_inductive_body -> sorts_family
+
 (* Check a [case_info] actually correspond to a Case expression on the
    given inductive type. *)
 val check_case_info : env -> inductive -> case_info -> unit
 
-(* Find the ultimate inductive in the [mind_equiv] chain *)
-
-val scrape_mind : env -> mutual_inductive -> mutual_inductive
-
 (*s Guard conditions for fix and cofix-points. *)
 val check_fix : env -> fixpoint -> unit
 val check_cofix : env -> cofixpoint -> unit
 
 (*s Support for sort-polymorphic inductive types *)
 
-val constructor_instances : env -> mind_specif -> inductive -> 
-  constr array -> env * types array array * universe array
+val type_of_inductive_knowing_parameters :
+  env -> one_inductive_body -> types array -> types
 
 val set_inductive_level : env -> sorts -> types -> types
 
-val find_inductive_level : env -> mind_specif -> inductive -> 
-  universe array -> universe array -> sorts
-
-val is_small_inductive : mind_specif -> bool
-
 val max_inductive_sort : sorts array -> universe
+
+(***************************************************************)
+(* Debug *)
+
+type size = Large | Strict
+type subterm_spec =
+    Subterm of (size * wf_paths)
+  | Dead_code
+  | Not_subterm
+type guard_env =
+  { env     : env;
+    (* dB of last fixpoint *)
+    rel_min : int;
+    (* inductive of recarg of each fixpoint *)
+    inds    : inductive array;
+    (* the recarg information of inductive family *)
+    recvec  : wf_paths array;
+    (* dB of variables denoting subterms *)
+    genv    : subterm_spec list;
+  }
+
+val subterm_specif : guard_env -> constr -> subterm_spec
+val case_branches_specif : guard_env -> constr -> inductive ->
+  constr array -> (guard_env * constr) array