Safe Haskell | None |
---|---|
Language | Haskell98 |
defunctionalize
traverses the query to:
1. "normalize" lambda terms by renaming binders,
2. generate alpha- and beta-equality axioms for
The lambdas and redexes found in the query.
NOTE: defunctionalize
should happen **BEFORE**
elaborate
as the latter converts all actual EApp
into the (uninterpreted) smt_apply
.
We cannot elaborate prior to defunc
as we need the
EApp
and ELam
to determine the lambdas and redexes.
Documentation
Containers defunctionalization --------------------------------------------
Defunc Sort Source # | |
Defunc SortedReft Source # | |
Defunc Reft Source # | |
Defunc Expr Source # | |
Defunc BindEnv Source # | |
Defunc a => Defunc [a] Source # | |
Defunc a => Defunc (SEnv a) Source # | |
Defunc a => Defunc (Triggered a) Source # | |
Defunc (SimpC a) Source # | |
Defunc (WfC a) Source # | |
Defunc (Symbol, Sort) Source # | |
Defunc (Symbol, SortedReft) Source # | |
(Defunc a, Eq k, Hashable k) => Defunc (HashMap k a) Source # | |
(Defunc (c a), TaggedC c a) => Defunc (GInfo c a) Source # | |