summaryrefslogtreecommitdiff
path: root/kernel/inductive.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /kernel/inductive.mli
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'kernel/inductive.mli')
-rw-r--r--kernel/inductive.mli46
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