package logtk

  1. Overview
  2. Docs
On This Page
  1. Signature
    1. IO
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.SignatureSource

Signature

A signature is a finite mapping from identifiers to types.

A signature maps symbols to types

Sourceval empty : t

Empty signature

Sourceval is_empty : t -> bool
Sourceval singleton : ID.t -> Type.t -> t
Sourceval mem : t -> ID.t -> bool

Is the symbol declared?

Sourceexception AlreadyDeclared of ID.t * Type.t * Type.t
Sourceval declare : t -> ID.t -> Type.t -> t

Declare the symbol, or

Sourceval find : t -> ID.t -> Type.t option

Lookup the type of a symbol

Sourceval find_exn : t -> ID.t -> Type.t

Lookup the type of a symbol

  • raises Not_found

    if the symbol is not in the signature

Sourceval arity : t -> ID.t -> int * int

Arity of the given symbol, or failure. see Type.arity for more details about the returned value.

  • raises Not_found

    if the symbol is not in the signature

Sourceval cardinal : t -> int

Number of symbols

Sourceval is_ground : t -> bool

Only ground types?

Sourceval merge : t -> t -> t

Merge two signatures together.

  • raises Type.Error

    if they share some symbols with distinct types

Sourceval diff : t -> t -> t

diff s1 s2 contains the symbols of s1 that do not appear in s2. Useful to remove base symbols.

Sourceval well_founded : t -> bool

Are there some symbols of arity 0 in the signature?

  • returns

    true iff the Herbrand term universe of this signature is non empty

Sourcemodule Seq : sig ... end
Sourceval to_set : t -> ID.Set.t

Set of symbols of the signature

Sourceval to_list : t -> (ID.t * Type.t) list
Sourceval add_list : t -> (ID.t * Type.t) list -> t
Sourceval of_list : (ID.t * Type.t) list -> t
Sourceval iter : t -> (ID.t -> Type.t -> unit) -> unit
Sourceval fold : t -> 'a -> ('a -> ID.t -> Type.t -> 'a) -> 'a
Sourceval is_bool : t -> ID.t -> bool

Has the symbol a boolean return sort?

  • raises Not_found

    if the symbol is not in the signature

Sourceval is_not_bool : t -> ID.t -> bool

IO

include Interfaces.PRINT with type t := t
Sourceval to_string : t -> string
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct