Module M_with_make.Adt

Constructor Definition

module Cons : sig ... end

This module defines the interface for creating ADT constructors.

type t

The abstract type representing a defined Algebraic Data Type, encapsulating its sort and associated functions (constructors, selectors, and testers).

val make : string -> Cons.t list -> t

make name constructors defines a new ADT with the given name and a list of constructors (of type Cons.t). This returns the ADT definition t.

val ty : t -> ty

ty adt retrieves the SMT sort (ty) of the defined ADT adt.

val constructor : string -> t -> func_decl option

constructor name adt retrieves the constructor function declaration (e.g., Cons) with the given name from the ADT adt, if it exists.

val selector : string -> t -> func_decl option

selector name adt retrieves the selector function declaration (e.g., field_a) with the given name from the ADT adt, if it exists.

val tester : string -> t -> func_decl option

tester name adt retrieves the tester function declaration (e.g., "is-Cons") with the given name from the ADT adt, if it exists.