package logtk

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

Module Logtk.IDSource

Unique Identifiers

An ID.t is a unique identifier (an integer) with a human-readable name. We use those to give names to variables that are not hashconsed (the hashconsing does not play nice with names).

An identifier is primarily determined by its id (a unique number for this identifier), and contains a string name for readability. Sometimes we display identifiers as "name/id".

Identifiers are generative: you can easily create new ones or copy them.

Identifiers can carry some payload (values, of type exn because it's extensible). It is useful to remember easily some information about the identifier (e.g. special sugar notation, whether it's a skolem, etc.)

  • since 1.5
Sourcetype t = private {
  1. id : int;
  2. name : string;
  3. mutable payload : exn list;
    (*

    Use exn as an open type for user-defined payload

    *)
}
Sourceval make : string -> t

Makes a fresh ID

Sourceval makef : ('a, Format.formatter, unit, t) format4 -> 'a
Sourceval copy : t -> t

Copy with a new ID

Sourceval id : t -> int
Sourceval name : t -> string
Sourceval payload : t -> exn list
Sourceval payload_find : f:(exn -> 'a option) -> t -> 'a option
Sourceval payload_pred : f:(exn -> bool) -> t -> bool
Sourceval set_payload : ?can_erase:(exn -> bool) -> t -> exn -> unit

Set given exception as payload.

  • parameter can_erase

    if provided, checks whether an existing value is to be replaced instead of adding a new entry

include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
include Interfaces.ORD with type t := t
Sourceval compare : t -> t -> int
include Interfaces.PRINT with type t := t
Sourceval to_string : t -> string

NOTE: default printer does not display the id field

Prints the ID with its internal number

Sourceval pp_fullc : t CCFormat.printer

Prints the ID with its internal number colored in gray (better for readability). Only use for debugging.

Sourceval gensym : unit -> t

Generate a new ID with a new, unique name

Sourcemodule Map : CCMap.S with type key = t
Sourcemodule Set : CCSet.S with type elt = t
Sourcemodule Tbl : CCHashtbl.S with type key = t
Sourceexception Attr_infix of string

Infix name for pretty-printing

Sourceexception Attr_prefix of string

Prefix name for pretty-printing

Sourceexception Attr_parameter of int

Parameter, used for HO unif

Sourcetype skolem_kind =
  1. | K_normal
  2. | K_ind
Sourceexception Attr_skolem of skolem_kind * int
Sourceexception Attr_distinct
Sourceval as_infix : t -> string option
Sourceval is_infix : t -> bool
Sourceval as_prefix : t -> string option
Sourceval is_prefix : t -> bool
Sourceval as_parameter : t -> int option
Sourceval is_parameter : t -> bool
Sourceval is_skolem : t -> bool

is_skolem id returns true iff id is a Skolem symbol

Sourceval as_skolem : t -> skolem_kind option
Sourceval num_mandatory_args : t -> int

number of mandatory arguments of a skolem constant or 0 otherwise

Sourceval is_distinct_object : t -> bool

whether the identifier is a distinct object (as defined in TPTP syntax)