package logtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.Ind_tySource

Inductive Types

An inductive datatype, defined by a list of constructors (and associated projectors that are defined as partial functions). Inductive types can be mutually recursive.

Sourceval section : Util.Section.t
Sourcetype constructor = private {
  1. cstor_name : ID.t;
  2. cstor_ty : Type.t;
  3. cstor_args : (Type.t * projector) list;
}

Constructor for an inductive type

Sourceand projector = private {
  1. p_id : ID.t;
  2. p_ty : Type.t;
  3. p_index : int;
  4. p_cstor : constructor lazy_t;
}

A projector for a given constructor and argument position

Inductive Types
Sourcetype t = private {
  1. ty_id : ID.t;
  2. ty_vars : Type.t HVar.t list;
  3. ty_pattern : Type.t;
  4. ty_constructors : constructor list;
  5. ty_is_rec : bool lazy_t;
  6. ty_proof : Proof.t;
}

An inductive type, along with its set of constructors

Sourceexception InvalidDecl of string
Sourceexception NotAnInductiveType of ID.t
Sourceexception NotAnInductiveConstructor of ID.t
Sourceval declare_ty : ID.t -> ty_vars:Type.t HVar.t list -> constructor list -> proof:Proof.t -> t

Declare the given inductive type.

  • raises InvalidDecl

    if the type is already declared, or the list of constructors is empty

Sourceval as_inductive_ty : ID.t -> t option
Sourceval as_inductive_ty_exn : ID.t -> t

Unsafe version of as_inductive_ty

Sourceval is_inductive_ty : ID.t -> bool
Sourceval as_inductive_type : Type.t -> (t * Type.t list) option

as_inductive_ty (list int) will return list, [int] as an inductive type applied to some arguments

Sourceval as_inductive_type_exn : Type.t -> t * Type.t list
Sourceval is_inductive_type : Type.t -> bool

is_inductive_type ty holds iff ty is an instance of some registered type (registered with declare_ty).

Sourceval is_inductive_simple_type : TypedSTerm.t -> bool
Sourceval is_recursive : t -> bool
Sourceval proof : t -> Proof.t
Constructors
Sourceval mk_constructor : ID.t -> Type.t -> (Type.t * (ID.t * Type.t)) list -> constructor
Sourceval is_constructor : ID.t -> bool

true if the symbol is an inductive constructor (zero, successor...)

Sourceval as_constructor : ID.t -> (constructor * t) option

if id is a constructor of ity, then as_constructor id returns Some (cstor, ity)

Sourceval as_constructor_exn : ID.t -> constructor * t

Unsafe version of as_constructor

Sourceval contains_inductive_types : Term.t -> bool

true iff the term contains at least one subterm with an inductive type

Projectors
Sourceval projector_id : projector -> ID.t
Sourceval projector_ty : projector -> Type.t
Sourceval projector_idx : projector -> int
Sourceval projector_cstor : projector -> constructor
Sourceval as_projector : ID.t -> projector option
OCaml

Innovation. Community. Security.