module Signature: sig
.. end
Signature
type
t = private Type.t ID.Map.t
A signature maps symbols to types
val empty : t
Empty signature
val is_empty : t -> bool
val singleton : ID.t -> Type.t -> t
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
RaisesAlreadyDeclared
if the symbol is already defined
Invalid_argument
if the type has free variables
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 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 filter : t -> (ID.t -> Type.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 -> ID.Set.t
Set of symbols of the signature
val to_list : t -> (ID.t * Type.t) list
val add_list : t -> (ID.t * Type.t) list -> t
val of_list : (ID.t * Type.t) list -> t
val iter : t -> (ID.t -> Type.t -> unit) -> unit
val fold : t -> 'a -> ('a -> ID.t -> Type.t -> '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