package logtk
Install
Dune Dependency
Authors
Maintainers
Sources
md5=cc320f66f10555c54822da624419e003
sha512=f8d5f7a5ae790bf0388d74261673803cf375f91f92f7b413b70db1ce5841ef55343a208f98727c8551d66f1840ab892f1c0c943a34861d14d79ce469b235a2f2
doc/logtk/Logtk/Term/index.html
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
same_l l1 l2
returns true
if terms of l1
and l2
are pairwise equal, false
otherwise. Precondition: both lists have the same length
Constructors
Create a bound variable. Providing a type is mandatory. Warning: be careful and try not to use this function directly.
Build a function from a list of free vars + the body. This performs the De Bruijn transformation, and shifts the body.
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
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
NOTE: this can break the invariants and make view
fail. Only apply with caution.
Iters
Compute the weight of a term, given a weight for variables and one for ID.ts.
Set of free type variables
is_ho_app (F t1…tn)
is true, when F
is a variable (of any function type)
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
replace t ~old ~by
syntactically replaces all occurrences of old
in t
by the term by
.
replace t m
syntactically replaces all occurrences of bindings of the map in t
, starting from the root
High-level operations
Fold
High level fold-like combinators
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.
Some AC-utils
Printing/parsing
include Interfaces.PRINT with type t := t
include Interfaces.PRINT_DE_BRUIJN with type t := t and type term := t
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.
Hook used by default for printing
List of default hooks
debugf printing, with sorts