package logtk

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

Higher Order Terms

Both higher order formulas and terms are represented by terms.

Term

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

    variable

    *)
  2. | BVar of int
    (*

    bound variable (De Bruijn index)

    *)
  3. | Lambda of LogtkType.t * t
    (*

    lambda abstraction over one variable.

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

    Forall quantifier (commutes with other forall)

    *)
  5. | Exists of LogtkType.t * t
    (*

    Exists quantifier (commutes with other exists)

    *)
  6. | Const of symbol
    (*

    LogtkTyped constant

    *)
  7. | At of t * t
    (*

    Curried application

    *)
  8. | TyLift of LogtkType.t
    (*

    Lift a type to a term

    *)
  9. | Multiset of LogtkType.t * t list
    (*

    a multiset of terms, and their common type

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

    Record of terms

    *)
val view : t -> view
val ty : t -> LogtkType.t
val of_term : LogtkScopedTerm.t -> t option
val of_term_exn : LogtkScopedTerm.t -> t
val is_term : LogtkScopedTerm.t -> bool

LogtkComparison, equality, containers

val open_at : t -> t * LogtkType.t list * t list

Open application recursively so as to gather all type arguments

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

Only on lambda terms: returns the type of the function argument.

  • raises Invalid_argument

    otherwise.

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

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

module Tbl : sig ... end
module Set : Sequence.Set.S with type elt = t
module Map : Sequence.Map.S with type key = t
module LogtkCache : LogtkCache.S with type key = t

Constructors

The constructors take care of type-checking. They may raise LogtkType.Error in case of type error.

Use lambda rather than __mk_lambda, and try not to create bound variables by yourself.

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

Create a variable. Providing a type is mandatory. The index must be non-negative,

  • raises Invalid_argument

    otherwise.

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 at : t -> t -> t

Curried application. The first term must have a function type with the same argument as the type of the second term. Note that at t1 t2 and app t1 [t2] are not the same term.

val at_list : t -> t list -> t

Curried application to several terms, left-parenthesing.

val tylift : LogtkType.t -> t

tylift ty makes a term out of ty. It has type ty

val tyat : t -> LogtkType.t -> t

tyat t ty is the same as at t (tylift ty)

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

Application to a list of types

val at_full : ?tyargs:LogtkType.t list -> t -> t list -> t

Combination of at_list and tyat_list

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

Create a typed constant.

val record : (string * t) list -> rest:t option -> t

Build a record. All terms in the list must have the same type, and the rest (if present) must have a record() type.

  • parameter rest

    if present, must be either a variable, or a record.

val multiset : ty:LogtkType.t -> t list -> t

Build a multiset. The ty argument is the type of the elements, in case the multiset is empty.

val __mk_lambda : varty:LogtkType.t -> t -> t

not documented

val __mk_forall : varty:LogtkType.t -> t -> t

not documented

val __mk_exists : varty:LogtkType.t -> t -> t

constructors with free variables. The first argument is the list of variables that is bound, then the quantified/abstracted term.

val lambda : t list -> t -> t

(lambda v1,...,vn. t).

val forall : t list -> t -> t
val exists : t list -> t -> t
val is_var : t -> bool
val is_bvar : t -> bool
val is_at : t -> bool
val is_tylift : t -> bool
val is_const : t -> bool
val is_lambda : t -> bool
val is_forall : t -> bool
val is_exists : t -> bool
val is_multiset : t -> bool
val is_record : 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

depth of the term

head symbol (or Invalid_argument)

val size : t -> int

head symbol (or Invalid_argument)

Size (number of nodes)

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?

Visitor

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

Visitor that maps the subterms into themselves

Conversion with LogtkFOTerm

val curry : LogtkFOTerm.t -> t

Curry all subterms

val uncurry : t -> LogtkFOTerm.t option

Un-curry all subterms. If some subterms are not convertible to first-order * terms then None is returned.

val is_fo : t -> bool

Check whether the term is convertible to a first-order term (no binders, no variable applied to something...)

Various operations

val close_forall : t -> t

Universally quantify all free variables

  • since 0.8
val close_exists : t -> t

Existentially quantify all free variables

  • since 0.8
val open_forall : ?offset:int -> t -> t

open_forall t removes all prenex "forall" quantifiers with fresh variables

  • parameter offset

    use this offset to generate fresh free variables

  • since 0.8

IO

First, full functions with the amount of surrounding binders; then helpers in the case this amount is 0 (for instance in clauses)

val print_all_types : bool Pervasives.ref
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

TPTP

module TPTP : sig ... end
val debug : Format.formatter -> t -> unit

debug printing, with sorts