Safe Haskell	None
Language	Haskell98

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

defunctionalize :: Fixpoint a => Config -> SInfo a -> SInfo a
class Defunc a where
- defunc :: a -> DF a
defuncAny :: Defunc a => Config -> SymEnv -> a -> a

Documentation

defunctionalize :: Fixpoint a => Config -> SInfo a -> SInfo a Source #

class Defunc a where Source #

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

Methods

defunc :: a -> DF a Source #

Instances

Instances details

Defunc Sort Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: Sort -> DF Sort Source #
Defunc SortedReft Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: SortedReft -> DF SortedReft Source #
Defunc Reft Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: Reft -> DF Reft Source #
Defunc Expr Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: Expr -> DF Expr Source #
Defunc BindEnv Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: BindEnv -> DF BindEnv Source #
Defunc a => Defunc [a] Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: [a] -> DF [a] Source #
Defunc a => Defunc (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: Triggered a -> DF (Triggered a) Source #
Defunc a => Defunc (SEnv a) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: SEnv a -> DF (SEnv a) Source #
Defunc (SimpC a) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: SimpC a -> DF (SimpC a) Source #
Defunc (WfC a) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: WfC a -> DF (WfC a) Source #
Defunc (Symbol, Sort) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: (Symbol, Sort) -> DF (Symbol, Sort) Source #
Defunc (Symbol, SortedReft) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: (Symbol, SortedReft) -> DF (Symbol, SortedReft) Source #
(Defunc a, Eq k, Hashable k) => Defunc (HashMap k a) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: HashMap k a -> DF (HashMap k a) Source #
(Defunc (c a), TaggedC c a) => Defunc (GInfo c a) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: GInfo c a -> DF (GInfo c a) Source #

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