Module Logtk.Signature (.ml)

module Signature: 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
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.
Raises LogtkType.Error if they share some symbols with distinct types
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

Pre-defined signature in TPTP


module TPTP: sig .. end