Module Logtk.Term

Lambda-free Terms

Term

type t = private InnerTerm.t
type term = t
type var = Type.t HVar.t

Variables are typed with Type.t

type view = private
| AppBuiltin of Builtin.t * t list
| DB of int

Bound variable (De Bruijn index)

| Var of var

Term variable

| Const of ID.t

Typed constant

| App of t * t list

Application to a list of terms (cannot be left-nested)

| Fun of Type.t * t

Lambda abstraction

val view : t -> view
module Classic : sig ... end
val subterm : sub:t -> t -> bool

checks whether sub is a (non-strict) subterm of t

include Interfaces.HASH with type t := t
include Interfaces.EQ
type t
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
type t
val compare : t -> t -> int
val ty : t -> Type.t

Obtain the type of a term..

module Set : CCSet.S with type Set.elt = t
module Map : CCMap.S with type Map.key = t
module Tbl : CCHashtbl.S with type Tbl.key = t
val hash_mod_alpha : t -> int

Hash invariant w.r.t variable renaming

val same_l : t list -> t list -> bool

same_l l1 l2 returns true if terms of l1 and l2 are pairwise equal, false otherwise. Precondition: both lists have the same length

raises Assert_failure

if lists have not the same length

Constructors

val var : var -> t
val var_of_int : ty:Type.t -> int -> t
val bvar : ty:Type.t -> int -> t

Create a bound variable. Providing a type is mandatory. Warning: be careful and try not to use this function directly.

raises InnerTerm.IllFormedTerm

if the index is < 0

val builtin : ty:Type.t -> Builtin.t -> t
val app_builtin : ty:Type.t -> Builtin.t -> t list -> t
val const : ty:Type.t -> ID.t -> t

Create a typed constant

val tyapp : t -> Type.t list -> t

Apply a term to types

raises Type.Error

if types do not match.

val app : t -> t list -> t

Apply a term to a list of terms

raises Type.ApplyError

if types do not match.

val app_full : t -> Type.t list -> t list -> t

Apply the term to types, then to terms

val true_ : t
val false_ : t
val fun_ : Type.t -> t -> t
val fun_l : Type.t list -> t -> t
val fun_of_fvars : var list -> t -> t

Build a function from a list of free vars + the body. This performs the De Bruijn transformation, and shifts the body.

val open_fun : t -> Type.t list * t
val open_fun_offset : offset:int -> t -> var list * t * int

open_fun ~offset (λxy. F) returns [v1,v2], F[v1/x,v2/y], offset+2 where v1 and v2 are fresh variables starting from offset

val grounding : Type.t -> t

grounding ty is a unique constant of type ty

val is_var : t -> bool
val is_bvar : t -> bool
val is_app : t -> bool
val is_const : t -> bool
val is_fun : t -> bool
val is_type : t -> bool

Does it have type tType?

val as_const : t -> ID.t option
val as_const_exn : t -> ID.t
val as_var : t -> var option
val as_var_exn : t -> var
val as_app : t -> t * t list

as_app t decomposes t into a head (non-application) and arguments, such as (let f,l = as_app t in app f l) = t

val as_fun : t -> Type.t list * t

Open functions

val head_term : t -> t

head_term t = fst (as_app t)

val head_term_mono : t -> t

head term, but still with type arguments

val args : t -> t list

args t = snd (as_app t)

val of_term_unsafe : InnerTerm.t -> t

NOTE: this can break the invariants and make view fail. Only apply with caution.

val of_term_unsafe_l : InnerTerm.t list -> t list
val of_ty : Type.t -> t

Upcast from type

module VarSet : CCSet.S with type VarSet.elt = var
module VarMap : CCMap.S with type VarMap.key = var
module VarTbl : CCHashtbl.S with type VarTbl.key = var

Sequences

module Seq : sig ... end
val var_occurs : var:var -> 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 : VarSet.t -> int

true if the term contains no type var

find the maximum variable

val min_var : VarSet.t -> int

find the maximum variable

minimum variable

val add_vars : unit VarTbl.t -> t -> unit

minimum variable

add variables of the term to the set

val vars : t -> VarSet.t

add variables of the term to the set

compute variables of the terms

val vars_prefix_order : t -> var 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 -> ID.t option

depth of the term

head ID.t

val head_exn : t -> ID.t

head ID.t

head ID.t (or Invalid_argument)

val size : t -> int

head ID.t (or Invalid_argument)

Size (number of nodes)

val weight : ?⁠var:int -> ?⁠sym:(ID.t -> int) -> t -> int

Compute the weight of a term, given a weight for variables and one for ID.ts.

parameter var

unique weight for every variable (default 1)

parameter sym

function from ID.ts to their weight (default const 1)

since
0.5.3
val ty_vars : t -> Logtk.Type.VarSet.t

Set of free type variables

val is_ho_var : t -> bool
val is_ho_app : t -> bool

is_ho_app (F t1…tn) is true, when F is a variable (of any function type)

val as_ho_app : t -> (Type.t HVar.t * t list) option

as_ho_app (F t1…tn) = Some (F, [t1…tn])

val is_ho_pred : t -> bool

is_ho_pred (F t1…tn) is true, when F is a predicate variable

val is_ho_at_root : t -> bool

is_ho_at_root t returns true if the term t is a higher-order variable, possibly applied (i.e. is_ho_var t || is_ho_app t)

Subterms and Positions

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.

val replace_m : t -> t Map.t -> t

replace t m syntactically replaces all occurrences of bindings of the map in t, starting from the root

High-level operations

val symbols : ?⁠init:Logtk.ID.Set.t -> t -> Logtk.ID.Set.t

Symbols of the term (keys of signature)

val contains_symbol : ID.t -> t -> bool

Does the term contain this given ID.t?

Fold

val all_positions : ?⁠vars:bool -> ?⁠ty_args:bool -> ?⁠pos:Position.t -> t -> t Position.With.t Sequence.t

Iterate on all sub-terms with their position.

parameter vars

specifies whether variables are folded on (default false).

parameter ty_args

specifies whether type arguments are folded on (default true).

parameter pos

the initial position (default empty)

Some AC-utils

module type AC_SPEC = sig ... end
module AC : functor (A : AC_SPEC) -> sig ... end

Printing/parsing

val print_all_types : bool Pervasives.ref

If true, pp will print the types of all annotated terms

include Interfaces.PRINT with type t := t
type t
val pp : t CCFormat.printer
val to_string : t -> string
include Interfaces.PRINT_DE_BRUIJN with type t := t and type term := t
type t
type term
type print_hook = int -> term CCFormat.printer -> Format.formatter -> term -> 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 -> t CCFormat.printer
val pp_var : Type.t HVar.t CCFormat.printer
val add_hook : print_hook -> unit

Hook used by default for printing

val default_hooks : unit -> print_hook list

List of default hooks

val debugf : Format.formatter -> t -> unit

debugf printing, with sorts

Formulas

module Form : sig ... end

Arith

module Arith : sig ... end
module DB : sig ... end

TPTP

module TPTP : sig ... end
module ZF : sig ... end
val pp_in : Output_format.t -> t CCFormat.printer
module Conv : sig ... end