package logtk

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

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
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