Module Ind_ty

module Ind_ty: sig .. end

Inductive Types



val section : Util.Section.t
type constructor = {
   cstor_name : ID.t;
   cstor_ty : Type.t;
}
Constructor for an inductive type

Inductive Types

type t = private {
   ty_id : ID.t;
   ty_vars : Type.t HVar.t list;
   ty_pattern : Type.t;
   ty_constructors : constructor list;
}
An inductive type, along with its set of constructors
exception InvalidDecl of string
exception NotAnInductiveType of ID.t
exception NotAnInductiveConstructor of ID.t
val declare_ty : ID.t -> ty_vars:Type.t HVar.t list -> constructor list -> t
Declare the given inductive type.
Raises InvalidDecl if the type is already declared, or the list of constructors is empty
val as_inductive_ty : ID.t -> t option
val as_inductive_ty_exn : ID.t -> t
Unsafe version of Ind_ty.as_inductive_ty
Raises NotAnInductiveType if the ID is not an inductive type
val is_inductive_ty : ID.t -> bool
val as_inductive_type : Type.t -> t option
val is_inductive_type : Type.t -> bool
is_inductive_type ty holds iff ty is an instance of some registered type (registered with Ind_ty.declare_ty).

Constructors

val is_constructor : ID.t -> bool
true if the symbol is an inductive constructor (zero, successor...)
val as_constructor : ID.t -> (constructor * t) option
if id is a constructor of ity, then as_constructor id returns Some (cstor, ity)
val as_constructor_exn : ID.t -> constructor * t
Unsafe version of Ind_ty.as_constructor
Raises NotAnInductiveConstructor if it fails
val contains_inductive_types : FOTerm.t -> bool
true iff the term contains at least one subterm with an inductive type

Constants with Inductive Type

val is_inductive_constant : ID.t -> bool
An ID whose type is inductive; nothing more
val declare_inductive_constant : ID.t -> unit
Make the ID satisfy Ind_ty.is_inductive_constant
val scan_for_constant : ID.t -> Type.t -> unit
Check whether id : ty has an inductive type; if yes, then call Ind_ty.declare_inductive_constant

Scan Declarations

val scan_stmt : ('a, 'b, Type.t, 'c) Statement.t -> unit
scan_stmt stmt examines stmt, and, if the statement is a declaration of inductive types or constants, it declares them using Ind_ty.declare_ty or Ind_ty.declare_inductive_constant.

Exceptions used to store information in IDs
exception Payload_ind_type of t
exception Payload_ind_cstor of constructor * t
exception Payload_ind_constant
exception Payload_ind_projector of ID.t