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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct