lambdapi
Library
Module
Module type
Parameter
Class
Class type
val eta_equality : bool Timed.ref
Flag indicating whether eta-reduction should be used or not.
type rw_tag = [
| `NoBeta | (* If true, no beta-reduction is performed. *) |
| `NoRw | (* If true, no user-defined rewrite rule is used. *) |
| `NoExpand | (* If true, definitions are not expanded. *) |
]
Tags for rewriting configuration.
Functions that use the rewriting engine and accept an optional argument tags
of type rw_tag list
have the following behaviour.
- If the argument is not given, then no tag is active and the rewrite engine is not constrained: it uses user defined reduction rules, it expands variable definitions (that are stored in the
ctxt
) and performs beta reductions. - Each tag if present disables some functionality of the rewrite engine. The descriptions of the functionalities are given in the documentation of
rw_tag
.
Reduction functions also accept an optional problem
that is used to store metavariables that may be created while rewriting. Such metavariables may be created by particular rewrite rules (such as unification rules), but not by rules declared with rule t ↪ u;
.
NOTE that all reduction functions, and eq_modulo
, may reduce in-place some subterms of the reduced term.
val whnf :
?problem:Term.problem ->
?tags:rw_tag list ->
Term.ctxt ->
Term.term ->
Term.term
whnf ?problem ?tags c t
computes a whnf of the term t
in context c
.
eq_modulo c a b
tests the convertibility of a
and b
in context c
.
pure_eq_modulo c a b
tests the convertibility of a
and b
in context c
with no side effects.
val snf :
?problem:Term.problem ->
?tags:rw_tag list ->
Term.ctxt ->
Term.term ->
Term.term
snf ?problem ?tags c t
computes the strong normal form of the term t
in the context c
.
val hnf :
?problem:Term.problem ->
?tags:rw_tag list ->
Term.ctxt ->
Term.term ->
Term.term
hnf ?problem ?tags c t
computes a head-normal form of the term t
in context c
.
simplify t
computes a beta whnf of t
belonging to the set S such that:
- terms of S are in beta whnf normal format
- if
t
is a product, then both its domain and codomain are in S.
If s
is a non-opaque symbol having a definition, unfold_sym s t
replaces in t
all the occurrences of s
by its definition.
type strategy =
| WHNF | (* Reduce to weak head-normal form. *) |
| HNF | (* Reduce to head-normal form. *) |
| SNF | (* Reduce to strong normal form. *) |
| NONE | (* Do nothing. *) |
Dedukti evaluation strategies.
type strat = {
strategy : strategy; | (* Evaluation strategy. *) |
steps : int option; | (* Max number of steps if given. *) |
}