Safe Haskell | None |
---|---|
Language | Haskell2010 |
- externals :: [External]
- foldR :: (ReadBindings c, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => HermitName -> Rewrite c m CoreExpr
- foldVarR :: (ReadBindings c, MonadCatch m, MonadUnique m) => Maybe BindingDepth -> Var -> Rewrite c m CoreExpr
- foldVarConfigR :: (ReadBindings c, MonadCatch m, MonadUnique m) => InlineConfig -> Maybe BindingDepth -> Var -> Rewrite c m CoreExpr
- runFoldR :: (BoundVars c, Monad m) => CompiledFold -> Rewrite c m CoreExpr
- fold :: BoundVars c => [Equality] -> c -> CoreExpr -> Maybe CoreExpr
- compileFold :: [Equality] -> CompiledFold
- runFold :: BoundVars c => CompiledFold -> c -> CoreExpr -> Maybe CoreExpr
- runFoldMatches :: BoundVars c => CompiledFold -> c -> CoreExpr -> Maybe (CoreExpr, VarEnv CoreExpr)
- data CompiledFold
- proves :: Clause -> Clause -> Bool
- lemmaMatch :: [Var] -> Clause -> Clause -> Maybe (VarEnv CoreExpr)
- data Equality = Equality [CoreBndr] CoreExpr CoreExpr
- toEqualities :: Clause -> [Equality]
- flipEquality :: Equality -> Equality
- freeVarsEquality :: Equality -> VarSet
- ppEqualityT :: PrettyPrinter -> PrettyH Equality
Fold/Unfold Transformation
foldR :: (ReadBindings c, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => HermitName -> Rewrite c m CoreExpr Source
foldVarR :: (ReadBindings c, MonadCatch m, MonadUnique m) => Maybe BindingDepth -> Var -> Rewrite c m CoreExpr Source
foldVarConfigR :: (ReadBindings c, MonadCatch m, MonadUnique m) => InlineConfig -> Maybe BindingDepth -> Var -> Rewrite c m CoreExpr Source
runFoldR :: (BoundVars c, Monad m) => CompiledFold -> Rewrite c m CoreExpr Source
Rewrite using a compiled fold. Useful inside traversal strategies like anytdR, because you can compile the fold once outside the traversal, then apply it everywhere in the tree.
Unlifted fold interface
fold :: BoundVars c => [Equality] -> c -> CoreExpr -> Maybe CoreExpr Source
Attempt to apply a list of Equalitys to the given expression, folding the
left-hand side into an application of the right-hand side. This
implementation depends on Equality
being well-formed. That is, both the
LHS and RHS are NOT lambda expressions. Always use mkEquality
to ensure
this is the case.
compileFold :: [Equality] -> CompiledFold Source
Compile a list of Equality's into a single fold matcher.
runFold :: BoundVars c => CompiledFold -> c -> CoreExpr -> Maybe CoreExpr Source
Attempt to fold an expression using a matcher in a given context.
runFoldMatches :: BoundVars c => CompiledFold -> c -> CoreExpr -> Maybe (CoreExpr, VarEnv CoreExpr) Source
Attempt to fold an expression using a matcher in a given context. Return resulting expression and a map of what when in the holes in the pattern.
data CompiledFold Source
lemmaMatch :: [Var] -> Clause -> Clause -> Maybe (VarEnv CoreExpr) Source
Determine if the right Clause is a substitution instance of the left Clause (which is a pattern with a given set of holes).
Equality
An equality is represented as a set of universally quantified binders, and the LHS and RHS of the equality.
Extern (RewriteH Equality) | |
Extern (TransformH Equality String) | |
Extern (TransformH Equality ()) | |
type Box (RewriteH Equality) | |
type Box (TransformH Equality String) | |
type Box (TransformH Equality ()) |
toEqualities :: Clause -> [Equality] Source
flipEquality :: Equality -> Equality Source
Flip the LHS and RHS of a Equality
.
freeVarsEquality :: Equality -> VarSet Source