package logtk

  1. Overview
  2. Docs
On This Page
  1. Signature
    1. IO

Module Logtk.Signature

Signature

A signature is a finite mapping from identifiers to types and a property sym_in_conjecture.

type t = private {
  1. sym_map : (Type.t * bool) ID.Map.t;
  2. ty_map : ID.Set.t Type.Map.t;
}

A signature maps symbols to types, and there is a map in the backwards direction

val empty : t

Empty signature

val is_empty : t -> bool
val mem : t -> ID.t -> bool

Is the symbol declared?

exception AlreadyDeclared of ID.t * Type.t * Type.t
val declare : t -> ID.t -> Type.t -> t

Declare the symbol, or

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

Lookup the type of a symbol

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

Lookup the type of a symbol

  • raises Not_found

    if the symbol is not in the signature

val find_by_type : t -> Type.t -> ID.Set.t

Reverse lookup -- given a type return all IDs with that type

val sym_in_conj : ID.t -> t -> bool
val set_sym_in_conj : ID.t -> t -> t
val 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

val cardinal : t -> int

Number of symbols

val is_ground : t -> bool

Only ground types?

val merge : t -> t -> t

Merge two signatures together.

  • raises Type.Error

    if they share some symbols with distinct types

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 -> ID.Set.t

Set of symbols of the signature

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

Has the symbol a boolean return sort?

  • raises Not_found

    if the symbol is not in the signature

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

IO

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