package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

LogtkSignature

module SMap : module type of LogtkSymbol.Map
type t = private LogtkType.t SMap.t

A signature maps symbols to types

val empty : t

Empty signature

val is_empty : t -> bool
val singleton : LogtkSymbol.t -> LogtkType.t -> t
val mem : t -> LogtkSymbol.t -> bool

Is the symbol declared?

val declare : t -> LogtkSymbol.t -> LogtkType.t -> t

Declare the symbol, or

  • raises LogtkType.Error

    if the symbol is already defined with a different type

  • raises Invalid_argument

    if the type has free variables

val find : t -> LogtkSymbol.t -> LogtkType.t option

Lookup the type of a symbol

val find_exn : t -> LogtkSymbol.t -> LogtkType.t

Lookup the type of a symbol

  • raises Not_found

    if the symbol is not in the signature

val arity : t -> LogtkSymbol.t -> int * int

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

  • raises Not_found

    if the symbol is not in the signature

val cardinal : t -> int

Number of symbols

val is_ground : t -> bool

Only ground types?

val merge : t -> t -> t

Merge two signatures together.

val filter : t -> (LogtkSymbol.t -> LogtkType.t -> bool) -> t

Only keep part of the signature

val diff : t -> t -> t

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

val 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

module Seq : sig ... end
val to_set : t -> LogtkSymbol.Set.t

Set of symbols of the signature

val to_list : t -> (LogtkSymbol.t * LogtkType.t) list
val of_list : (LogtkSymbol.t * LogtkType.t) list -> t
val iter : t -> (LogtkSymbol.t -> LogtkType.t -> unit) -> unit
val fold : t -> 'a -> ('a -> LogtkSymbol.t -> LogtkType.t -> 'a) -> 'a

IO

include LogtkInterfaces.PRINT with type t := t
val pp : Buffer.t -> t -> unit
val to_string : t -> string
val fmt : Format.formatter -> t -> unit

Pre-defined signature in TPTP

module TPTP : sig ... end