(* $Id$ *)

(*i*)
open Names
open Univ
open Term
open Declarations
open Environ
(*i*)


(*s The different kinds of errors that may result of a malformed inductive
  definition. *)

type inductive_error =
  (* These are errors related to inductive constructions in this module *)
  | NonPos of env * constr * constr
  | NotEnoughArgs of env * constr * constr
  | NotConstructor of env * constr * constr
  | NonPar of env * constr * int * constr * constr
  | SameNamesTypes of identifier
  | SameNamesConstructors of identifier * identifier
  | NotAnArity of identifier
  | BadEntry
  (* These are errors related to recursors building in Indrec *)
  | NotAllowedCaseAnalysis of bool * sorts * inductive
  | BadInduction of bool * identifier * sorts
  | NotMutualInScheme

exception InductiveError of inductive_error

(*s The following functions are utility functions to check and to
  decompose a declaration. *)

(* [mind_check_names] checks the names of an inductive types declaration
   i.e. that all the types and constructors names are distinct. 
   It raises an exception [InductiveError _] if it is not the case. *)

val mind_check_names : mutual_inductive_entry -> unit

(* [mind_extract_and_check_params] extracts the parameters of an inductive
   types declaration. It raises an exception [InductiveError _] if there is
   not enough abstractions in any of the terms of the field 
   [mind_entry_inds]. *)

val mind_extract_and_check_params : 
  mutual_inductive_entry -> Sign.rel_context

val mind_extract_params : int -> constr -> Sign.rel_context * constr

val mind_check_lc : Sign.rel_context -> mutual_inductive_entry -> unit

(* [mind_check_arities] checks that the types declared for all the
   inductive types are some arities. *)

val mind_check_arities : env -> mutual_inductive_entry -> unit

(* [cci_inductive] checks positivity and builds an inductive body *)

val cci_inductive : 
  env -> env -> path_kind -> int -> bool -> 
   (identifier * types * identifier list * bool * bool * types array)
      list ->
      constraints ->
      	mutual_inductive_body