package logtk

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

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
type t = private {
  1. id : int;
  2. name : string;
  3. mutable payload : exn list;
    (*

    Use exn as an open type for user-defined payload

    *)
}
val make : string -> t

Makes a fresh ID

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

Copy with a new ID

val id : t -> int
val name : t -> string
val payload : t -> exn list
val dummy_of_int : int -> t
val payload_find : f:(exn -> 'a option) -> t -> 'a option
val payload_pred : f:(exn -> bool) -> t -> bool
val 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
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
val compare : t -> t -> int
include Interfaces.PRINT with type t := t
val to_string : t -> string

NOTE: default printer does not display the id field

val pp_full : t CCFormat.printer

Prints the ID with its internal number

val pp_fullc : t CCFormat.printer

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

val pp_tstp : t CCFormat.printer
val pp_zf : t CCFormat.printer
val gensym : unit -> t

Generate a new ID with a new, unique name

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

Infix name for pretty-printing

exception Attr_prefix of string

Prefix name for pretty-printing

exception Attr_parameter of int

Parameter, used for HO unif

type skolem_kind =
  1. | K_normal
  2. | K_ind
exception Attr_skolem of skolem_kind
exception Attr_distinct
val as_infix : t -> string option
val is_infix : t -> bool
val as_prefix : t -> string option
val is_prefix : t -> bool
val as_parameter : t -> int option
val is_parameter : t -> bool
val is_skolem : t -> bool

is_skolem id returns true iff id is a Skolem symbol

val as_skolem : t -> skolem_kind option
val is_distinct_object : t -> bool

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