liquid-fixpoint-0.7.0.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Defunctionalize

Description

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.

Synopsis

Documentation

class Defunc a where Source #

Containers defunctionalization --------------------------------------------

Minimal complete definition

defunc

Methods

defunc :: a -> DF a Source #

Instances

Defunc Sort Source # 

Methods

defunc :: Sort -> DF Sort Source #

Defunc SortedReft Source # 
Defunc Reft Source # 

Methods

defunc :: Reft -> DF Reft Source #

Defunc Expr Source # 

Methods

defunc :: Expr -> DF Expr Source #

Defunc BindEnv Source # 

Methods

defunc :: BindEnv -> DF BindEnv Source #

Defunc a => Defunc [a] Source # 

Methods

defunc :: [a] -> DF [a] Source #

Defunc a => Defunc (SEnv a) Source # 

Methods

defunc :: SEnv a -> DF (SEnv a) Source #

Defunc a => Defunc (Triggered a) Source # 

Methods

defunc :: Triggered a -> DF (Triggered a) Source #

Defunc (SimpC a) Source # 

Methods

defunc :: SimpC a -> DF (SimpC a) Source #

Defunc (WfC a) Source # 

Methods

defunc :: WfC a -> DF (WfC a) Source #

Defunc (Symbol, Sort) Source # 

Methods

defunc :: (Symbol, Sort) -> DF (Symbol, Sort) Source #

Defunc (Symbol, SortedReft) Source # 
(Defunc a, Eq k, Hashable k) => Defunc (HashMap k a) Source # 

Methods

defunc :: HashMap k a -> DF (HashMap k a) Source #

(Defunc (c a), TaggedC c a) => Defunc (GInfo c a) Source # 

Methods

defunc :: GInfo c a -> DF (GInfo c a) Source #

defuncAny :: Defunc a => Config -> SymEnv -> a -> a Source #