Module `Logtk.Term`Source

Terms

Those terms provide a direct presentation of higher-order terms with lambdas in the sense that they make currying possible (as well as applying functions to other terms).

This is as if terms had an `apply` symbol everywhere, but more lightweight.

Types and terms are mixed because it makes application much easier (applying to a type and to a term are the same thing). It might also make dependent typing possible some day.

Term

Sourcetype t = private InnerTerm.t

Sourcetype term = t

Sourcetype var = Type.t HVar.t

Variables are typed with Type.t

Sourcetype 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
*)

Sourceval view : t -> view

Sourcemodule Classic : sig ... end

Sourceval 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 with type t := t

Sourceval equal : t -> t -> bool

Sourceval hash : t -> int

include Interfaces.ORD with type t := t

Sourceval compare : t -> t -> int

Sourceval ty : t -> Type.t

Obtain the type of a term..

Sourcemodule Set : CCSet.S with type elt = t

Sourcemodule Map : CCMap.S with type key = t

Sourcemodule Tbl : CCHashtbl.S with type key = t

Sourceval hash_mod_alpha : t -> int

Hash invariant w.r.t variable renaming

Sourceval 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

Sourceval var : var -> t

Sourceval var_of_int : ty:Type.t -> int -> t

Sourceval 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

Sourceval builtin : ty:Type.t -> Builtin.t -> t

Sourceval app_builtin : ty:Type.t -> Builtin.t -> t list -> t

Sourceval const : ty:Type.t -> ID.t -> t

Create a typed constant

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

Apply a term to types

raises Type.Error
if types do not match.

Sourceval app : t -> t list -> t

Apply a term to a list of terms

raises Type.ApplyError
if types do not match.

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

Apply the term to types, then to terms

Sourceval true_ : t

Sourceval false_ : t

Sourceval fun_ : Type.t -> t -> t

Sourceval fun_l : Type.t list -> t -> t

Sourceval 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.

Sourceval open_fun : t -> Type.t list * t

Sourceval 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

Sourceval grounding : Type.t -> t

grounding ty is a unique constant of type ty

Sourceval is_var : t -> bool

Sourceval is_bvar : t -> bool

Sourceval is_app : t -> bool

Sourceval is_const : t -> bool

Sourceval is_fun : t -> bool

Sourceval is_type : t -> bool

Does it have type tType?

Sourceval as_const : t -> ID.t option

Sourceval as_const_exn : t -> ID.t

Sourceval as_var : t -> var option

Sourceval as_var_exn : t -> var

Sourceval 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

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

Open functions

Sourceval head_term : t -> t

head_term t = fst (as_app t)

Sourceval head_term_mono : t -> t

head term, but still with type arguments

Sourceval args : t -> t list

args t = snd (as_app t)

Sourceval of_term_unsafe : InnerTerm.t -> t

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

Sourceval of_term_unsafe_l : InnerTerm.t list -> t list

Sourceval of_ty : Type.t -> t

Upcast from type

Sourcemodule VarSet : CCSet.S with type elt = var

Sourcemodule VarMap : CCMap.S with type key = var

Sourcemodule VarTbl : CCHashtbl.S with type key = var

Iters

Sourcemodule Seq : sig ... end

Sourceval var_occurs : var:var -> t -> bool

var_occurs ~var t true iff var in t

Sourceval is_ground : t -> bool

is the term ground? (no free vars)

Sourceval monomorphic : t -> bool

true if the term contains no type var

Sourceval max_var : VarSet.t -> int

find the maximum variable

Sourceval min_var : VarSet.t -> int

minimum variable

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

add variables of the term to the set

Sourceval vars : t -> VarSet.t

compute variables of the terms

Sourceval vars_prefix_order : t -> var list

variables in prefix traversal order

Sourceval depth : t -> int

depth of the term

Sourceval head : t -> ID.t option

head ID.t

Sourceval head_exn : t -> ID.t

head ID.t (or Invalid_argument)

Sourceval size : t -> int

Size (number of nodes)

Sourceval 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

Sourceval ty_vars : t -> Type.VarSet.t

Set of free type variables

Sourceval is_ho_var : t -> bool

Sourceval is_ho_app : t -> bool

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

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

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

Sourceval is_ho_pred : t -> bool

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

Sourceval 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

Sourcemodule Pos : sig ... end

Sourceval replace : t -> old:t -> by:t -> t

replace t ~old ~by syntactically replaces all occurrences of old in t by the term by.

Sourceval 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

Sourceval symbols : ?init:ID.Set.t -> t -> ID.Set.t

Symbols of the term (keys of signature)

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

Does the term contain this given ID.t?

Fold

High level fold-like combinators

Source

val all_positions : 
  ?vars:bool ->
  ?ty_args:bool ->
  ?pos:Position.t ->
  t ->
  t Position.With.t Iter.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

Sourcemodule type AC_SPEC = sig ... end

Sourcemodule AC (A : AC_SPEC) : sig ... end

Printing/parsing

Sourceval print_all_types : bool ref

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

include Interfaces.PRINT with type t := t

Sourceval pp : t CCFormat.printer

Sourceval to_string : t -> string

include Interfaces.PRINT_DE_BRUIJN with type t := t and type term := t

Sourcetype print_hook = int -> t CCFormat.printer -> Format.formatter -> 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.

Sourceval pp_depth : ?hooks:print_hook list -> int -> t CCFormat.printer

Sourceval pp_var : Type.t HVar.t CCFormat.printer

Sourceval add_hook : print_hook -> unit

Hook used by default for printing

Sourceval default_hooks : unit -> print_hook list

List of default hooks

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

debugf printing, with sorts

Formulas

Sourcemodule Form : sig ... end

Arith

Sourcemodule Arith : sig ... end

Sourcemodule DB : sig ... end

TPTP

Sourcemodule TPTP : sig ... end

Sourcemodule ZF : sig ... end

Sourceval pp_in : Output_format.t -> t CCFormat.printer

Sourcemodule Conv : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/logtk/Logtk/Term/index.html

Module `Logtk.Term`Source

Terms

Term

Constructors

Iters

Subterms and Positions

High-level operations

Fold

Some AC-utils

Printing/parsing

Formulas

Arith

TPTP

package logtk

Install

Dune Dependency

Authors

Maintainers

Sources

doc/logtk/Logtk/Term/index.html

Module Logtk.TermSource

Terms

Term

Constructors

Iters

Subterms and Positions

High-level operations

Fold

Some AC-utils

Printing/parsing

Formulas

Arith

TPTP

Module `Logtk.Term`Source