package logtk

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

First-order terms

package logtk

logtk
- Logtk
- LogtkCache
  - Dummy
    
    X
  - Dummy2
    
    X
    
    Y
  - EQ
  - HASH
  - LRU
    
    X
  - Linear
    
    X
  - Linear2
    
    X
    
    Y
  - Replacing
    
    X
  - Replacing2
    
    X
    
    Y
  - S
  - S2
- LogtkCnf
- LogtkComparison
  - PARTIAL_ORD
- LogtkCongruence
  - FO
  - HO
  - Make
    
    T
  - S
  - TERM
- LogtkDBEnv
- LogtkDtree
  - Default
  - Make
    
    E
- LogtkFOTerm
  - AC
    
    A
  - AC_SPEC
  - Classic
  - Map
  - Pos
  - Seq
  - Set
  - T2LogtkCache
  - TLogtkCache
  - TPTP
    
    Arith
  - Tbl
- LogtkFastFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFeatureVector
  - Make
    
    C
    
    Feature
- LogtkFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFormula
  - FO
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Make
    
    Base
    
    Map
    
    MyT
    
    Seq
    
    Set
    
    TPTP
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Map
    
    From
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
    
    To
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - S
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - TERM
    
    Seq
    
    Set
    
    TPTP
- LogtkFormulaShape
- LogtkHORewriting
  - Seq
- LogtkHOTerm
  - LogtkCache
  - Map
  - Pos
  - Seq
  - Set
  - TPTP
  - Tbl
  - any_visitor
  - id_visitor
- LogtkHashcons
  - HashedLogtkType
  - Make
    
    H
    
    X
  - S
    
    H
- LogtkIArray
  - Seq
- LogtkIndex
  - BasicEquation
  - CLAUSE
  - EQUATION
  - LEAF
  - MakeLeaf
    
    X
  - SUBSUMPTION_IDX
    
    C
  - TERM_IDX
    
    Leaf
  - UNIT_IDX
    
    E
- LogtkInterfaces
  - EQ
  - GROUP
  - HASH
  - ITER
  - MONOID
  - ORD
  - PRINT
  - PRINT1
  - PRINT_DE_BRUIJN
  - PRINT_OVERLOAD
- LogtkLambda
- LogtkLazyGraph
  - Dot
  - Full
  - Heap
  - Infix
  - Mutable
- LogtkLazyList
- LogtkMultiset
  - Make
    
    Seq
    
    X
  - S
    
    Seq
- LogtkNPDtree
  - Make
    
    E
  - MakeTerm
    
    Leaf
    
    X
- LogtkOptions
- LogtkOrdering
  - Default
  - Make
    
    P
    
    Constr
    
    Seq
- LogtkOrdering_intf
  - S
    
    Prec
    
    Constr
    
    Seq
- LogtkParseLocation
- LogtkPartialOrder
  - ELEMENT
  - Make
    
    E
- LogtkPartialOrder_intf
  - S
- LogtkPosition
  - Build
- LogtkPrecedence
  - Constr
  - Default
    
    Constr
    
    Seq
  - Make
    
    Constr
    
    Seq
    
    Sym
  - SYMBOL
  - Seq
- LogtkPrecedence_intf
  - S
    
    Constr
    
    Seq
- LogtkPrologTerm
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
  - id_visitor
  - visitor
- LogtkRewriting
  - FormRW
  - MakeOrdered
    
    E
  - MakeTRS
    
    I
    
    E
  - ORDERED
    
    E
  - SIG_TRS
  - TRS
- LogtkScopedTerm
  - DB
  - Kind
  - Map
  - Pos
  - Seq
  - Set
  - Tbl
- LogtkSignature
  - SMap
  - Seq
  - TPTP
    
    Arith
- LogtkSkolem
- LogtkSourced
- LogtkSubsts
  - FO
  - Form
  - HO
  - Renaming
  - SPECIALIZED
  - Ty
- LogtkSymbol
  - ArithOp
  - Base
  - Map
  - Seq
  - Set
  - TPTP
    
    Arith
  - Tbl
- LogtkTransform
  - DAG
    
    Form
  - FORM
  - FormDag
    
    Form
  - MakeDAG
    
    Form
- LogtkType
  - Conv
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
- LogtkTypeInference
  - Closure
  - Ctx
  - FO
  - HO
  - S
- LogtkTypedPrologTerm
  - Map
  - Seq
  - Set
  - Subst
  - Tbl
  - Visitor
- LogtkUnif
  - FO
  - Form
  - HO
  - NARY
  - Nary
  - Ty
  - UNARY
  - Unary
- LogtkUtil
  - Exn
  - Flag
  - Section

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

| Var of int
(*
Term variable
*)
| BVar of int
(*
Bound variable (De Bruijn index)
*)
| Const of LogtkSymbol.t
(*
LogtkTyped constant
*)
| TyApp of t * LogtkType.t
(*
Application to type
*)
| App of t * t list
(*
Application to a list of terms (cannot be left-nested)
*)

val view : t -> view

val kind : LogtkScopedTerm.Kind.t

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.

raises LogtkScopedTerm.IllFormedTerm
if the index is < 0

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.

raises LogtkScopedTerm.IllFormedTerm
if the index is < 0

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

Create a typed constant

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

Apply a term to a type

raises LogtkType.Error
if types do not match.

val app : t -> t list -> t

Apply a term to a list of terms

raises LogtkType.Error
if types do not match.

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