package logtk

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

Prolog-like Terms

.

Those terms are not hashconsed, nor do they use De Bruijn indices. Their simplicity make them good for heavy AST transformations, output of parsing, etc.

Terms are only compared, hashsed, etc. by their "term" component (the algebraic variant). Additional fields (location...) are ignored for almost every operation.

type location = LogtkParseLocation.t
type t = private {
  1. term : view;
  2. loc : location option;
}
and view = private
  1. | Var of string
    (*

    variable

    *)
  2. | Int of Z.t
    (*

    integer

    *)
  3. | Rat of Q.t
    (*

    rational

    *)
  4. | Const of LogtkSymbol.t
    (*

    constant

    *)
  5. | Syntactic of LogtkSymbol.t * t list
    (*

    syntactic construct (operator...)

    *)
  6. | App of t * t list
    (*

    apply term

    *)
  7. | Bind of LogtkSymbol.t * t list * t
    (*

    bind n variables

    *)
  8. | List of t list
    (*

    special constructor for lists

    *)
  9. | Record of (string * t) list * t option
    (*

    extensible record

    *)
  10. | Column of t * t
    (*

    t:t (useful for typing, e.g.)

    *)
type term = t
val view : t -> view
val loc : t -> location option
include LogtkInterfaces.HASH with type t := t
include LogtkInterfaces.EQ with type t := t
val eq : t -> t -> bool
val hash_fun : t CCHash.hash_fun
val hash : t -> int
include LogtkInterfaces.ORD with type t := t
val cmp : t -> t -> int
val var : ?loc:location -> ?ty:t -> string -> t
val int_ : Z.t -> t
val of_int : int -> t
val rat : Q.t -> t
val app : ?loc:location -> t -> t list -> t
val syntactic : ?loc:location -> LogtkSymbol.t -> t list -> t
val const : ?loc:location -> LogtkSymbol.t -> t
val bind : ?loc:location -> LogtkSymbol.t -> t list -> t -> t
val list_ : ?loc:location -> t list -> t
val nil : t
val column : ?loc:location -> t -> t -> t
val record : ?loc:location -> (string * t) list -> rest:t option -> t
val at_loc : loc:location -> t -> t
val wildcard : t
val is_app : t -> bool
val is_var : t -> bool
module Set : Sequence.Set.S with type elt = term
module Map : Sequence.Map.S with type key = term
module Tbl : Hashtbl.S with type key = term
module Seq : sig ... end
val ground : t -> bool
val close_all : LogtkSymbol.t -> t -> t

Bind all free vars with the symbol

val subterm : strict:bool -> t -> sub:t -> bool

Bind all free vars with the symbol

is sub a (strict?) subterm of the other arg?

include LogtkInterfaces.PRINT with type t := t
val pp : Buffer.t -> t -> unit
val to_string : t -> string
val fmt : Format.formatter -> t -> unit

Visitor

class virtual 'a visitor : object ... end
class id_visitor : object ... end

Visitor that maps the subterms into themselves

module TPTP : sig ... end