package logtk

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

First-order terms

Terms use LogtkScopedTerm with kind "LogtkFOTerm".

type symbol = LogtkSymbol.t

Term

type t = private LogtkScopedTerm.t
type term = t
type view = private
  1. | Var of int
    (*

    Term variable

    *)
  2. | BVar of int
    (*

    Bound variable (De Bruijn index)

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

    LogtkTyped constant

    *)
  4. | TyApp of t * LogtkType.t
    (*

    Application to type

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

    Application to a list of terms (cannot be left-nested)

    *)
val view : t -> view
val open_app : t -> t * LogtkType.t list * t list

Open application recursively so as to gather all type arguments

module Classic : sig ... end

LogtkComparison, equality, containers

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

checks whether sub is a (non-strict) subterm of t

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 ty : t -> LogtkType.t

Obtain the type of a term..

module Tbl : sig ... end
module Set : Sequence.Set.S with type elt = t
module Map : Sequence.Map.S with type key = t
module TLogtkCache : LogtkCache.S with type key = t
module T2LogtkCache : LogtkCache.S2 with type key1 = t and type key2 = t

Constructors

val var : ty:LogtkType.t -> int -> t

Create a variable. Providing a type is mandatory.

val bvar : ty:LogtkType.t -> int -> t

Create a bound variable. Providing a type is mandatory. Warning: be careful and try not to use this function directly.

val const : ty:LogtkType.t -> symbol -> t

Create a typed constant

val tyapp : t -> LogtkType.t -> t

Apply a term to a type

val app : t -> t list -> t

Apply a term to a list of terms

val app_full : t -> LogtkType.t list -> t list -> t

Apply the term to types, then to terms

val cast : ty:LogtkType.t -> t -> t

Change the type. Only works for variables and bound variables.

val of_term : LogtkScopedTerm.t -> t option
val of_term_exn : LogtkScopedTerm.t -> t
val is_term : LogtkScopedTerm.t -> bool
val is_var : t -> bool
val is_bvar : t -> bool
val is_tyapp : t -> bool
val is_app : t -> bool
val is_const : t -> bool

Sequences

module Seq : sig ... end
val var_occurs : var:t -> t -> bool

var_occurs ~var t true iff var in t

val is_ground : t -> bool

var_occurs ~var t true iff var in t

is the term ground? (no free vars)

val monomorphic : t -> bool

is the term ground? (no free vars)

true if the term contains no type var

val max_var : Set.t -> int

true if the term contains no type var

find the maximum variable index, or 0

val min_var : Set.t -> int

find the maximum variable index, or 0

minimum variable, or 0 if ground

val add_vars : unit Tbl.t -> t -> unit

minimum variable, or 0 if ground

add variables of the term to the set

val vars : t Sequence.t -> Set.t

add variables of the term to the set

compute variables of the terms

val vars_prefix_order : t -> t list

compute variables of the terms

variables in prefix traversal order

val depth : t -> int

variables in prefix traversal order

depth of the term

val head : t -> LogtkSymbol.t option

depth of the term

head symbol

val head_exn : t -> LogtkSymbol.t

head symbol

head symbol (or Invalid_argument)

val size : t -> int

head symbol (or Invalid_argument)

Size (number of nodes)

val weight : ?var:int -> ?sym:(LogtkSymbol.t -> int) -> t -> int

Compute the weight of a term, given a weight for variables and one for symbols.

  • parameter var

    unique weight for every variable (default 1)

  • parameter sym

    function from symbols to their weight (default const 1)

  • since 0.5.3
val ty_vars : t -> LogtkType.Set.t

Set of free type variables

Subterms and LogtkPositions

module Pos : sig ... end
val replace : t -> old:t -> by:t -> t

replace t ~old ~by syntactically replaces all occurrences of old in t by the term by.

High-level operations

val symbols : ?init:LogtkSymbol.Set.t -> t -> LogtkSymbol.Set.t

LogtkSymbols of the term (keys of signature)

val contains_symbol : LogtkSymbol.t -> t -> bool

Does the term contain this given symbol?

Fold

High level fold-like combinators

val all_positions : ?vars:bool -> ?pos:LogtkPosition.t -> t -> 'a -> ('a -> t -> LogtkPosition.t -> 'a) -> 'a

apply f to all non-variable positions in t, accumulating the results along. vars specifies whether variables are folded on (default true).

Some AC-utils

module type AC_SPEC = sig ... end
module AC (A : AC_SPEC) : sig ... end

Conversions

val to_prolog : ?depth:int -> t -> LogtkPrologTerm.t

Printing/parsing

val print_all_types : bool Pervasives.ref

If true, pp will print the types of all annotated terms

include LogtkInterfaces.PRINT with type t := t
val pp : Buffer.t -> t -> unit
val to_string : t -> string
val fmt : Format.formatter -> t -> unit
include LogtkInterfaces.PRINT_DE_BRUIJN with type t := t and type term := t
type print_hook = int -> (Buffer.t -> t -> unit) -> Buffer.t -> t -> bool

User-provided hook that can be used to print terms (for composite cases) before the default printing occurs. The int argument is the De Bruijn depth in the term. A hook takes as arguments the depth and the recursive printing function that it can use to print subterms. A hook should return true if it fired, false to fall back on the default printing.

val pp_depth : ?hooks:print_hook list -> int -> Buffer.t -> t -> unit
val add_hook : print_hook -> unit

Hook used by default for printing

val default_hooks : unit -> print_hook list

List of default hooks

val debug : Format.formatter -> t -> unit

debug printing, with sorts

TPTP

module TPTP : sig ... end