Module Logtk.HOTerm (.ml)

module HOTerm: LogtkHOTerm


type symbol = LogtkSymbol.t 
type t = private LogtkScopedTerm.t 
type term = t 
type view = private 
| Var of int (*
| RigidVar of int (*
rigid variable, only targets other variables
| BVar of int (*
bound variable (De Bruijn index)
| Lambda of LogtkType.t * t (*
lambda abstraction over one variable.
| Const of symbol (*
LogtkTyped constant
| At of t * t (*
Curried application
| TyAt of t * LogtkType.t (*
Curried application to a type
| Multiset of LogtkType.t * t list (*
a multiset of terms, and their common type
| Record of (string * t) list * t option (*
Record of terms
val view : t -> view
val ty : t -> LogtkType.t
val kind : LogtkScopedTerm.Kind.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
include LogtkInterfaces.ORD
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


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

Use lambda rather than LogtkHOTerm.__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 rigid_var : ty:LogtkType.t -> int -> t
Rigid variable.
Raises Invalid_argument if the index is negative
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.
Raises LogtkType.Error if types do not match.
val at_list : t -> t list -> t
Curried application to several terms, left-parenthesing.
Raises LogtkType.Error of types do not match.
val tyat : t -> LogtkType.t -> t
Curried type application.
Raises LogtkType.Error if types do not match.
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 LogtkHOTerm.at_list and LogtkHOTerm.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.
Raises LogtkType.Error if types mismatch
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.
Raises LogtkType.Error if types mismatch
val __mk_lambda : varty:LogtkType.t -> t -> t
not documented

constructors with free variables. The first argument is the list of variables that is bound, then the quantified/abstracted term.
val mk_lambda : t list -> t -> t
(lambda v1,...,vn. t).
val is_var : t -> bool
val is_bvar : t -> bool
val is_at : t -> bool
val is_tyat : t -> bool
val is_const : t -> bool
val is_lambda : t -> bool
val is_multiset : t -> bool
val is_record : t -> bool


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
is the term ground? (no free vars)
val monomorphic : t -> bool
true if the term contains no type var
val max_var : Set.t -> int
find the maximum variable index, or 0
val min_var : Set.t -> int
minimum variable, or 0 if ground
val add_vars : unit Tbl.t -> t -> unit
add variables of the term to the set
val vars : t Sequence.t -> Set.t
compute variables of the terms
val vars_prefix_order : t -> t list
variables in prefix traversal order
val depth : t -> int
depth of the term
val head : t -> LogtkSymbol.t
head symbol (or Invalid_argument)
val size : t -> int
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?


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 rigidify : t -> t
Replace Var occurrences with RigidVar ones.
val unrigidify : t -> t
Converse of LogtkHOTerm.rigidify


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
include LogtkInterfaces.PRINT_DE_BRUIJN
val add_hook : print_hook -> unit


module TPTP: sig .. end
val debug : Format.formatter -> t -> unit
debug printing, with sorts