package smtml

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

Module Make.AdtSource

Constructor Definition

Sourcemodule Cons : sig ... end

This module defines the interface for creating ADT constructors.

Sourcetype t

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

Sourceval 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.

Sourceval ty : t -> ty

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

Sourceval 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.

Sourceval 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.

Sourceval 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.