Module Logtk.FOTerm (.ml)

module FOTerm: LogtkFOTerm

type symbol = LogtkSymbol.t 


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
Classic view

LogtkComparison, equality, containers

val subterm : sub:t -> t -> bool
checks whether sub is a (non-strict) subterm of t
include LogtkInterfaces.HASH
include LogtkInterfaces.ORD
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


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


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 option
head symbol
val head_exn : t -> LogtkSymbol.t
head symbol (or Invalid_argument)
val size : t -> int
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.
Since 0.5.3
var : unique weight for every variable (default 1)
sym : function from symbols to their weight (default const 1)
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?


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


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


val print_all_types : bool Pervasives.ref
If true, pp will print the types of all annotated terms
include LogtkInterfaces.PRINT
include LogtkInterfaces.PRINT_DE_BRUIJN
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


module TPTP: sig .. end