HERMIT.Dictionary.Fold

Fold/Unfold Transformation

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

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

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

Compile a list of Equality's into a single fold matcher.

runFold :: BoundVars c => CompiledFold -> c -> CoreExpr -> Maybe CoreExpr

Attempt to fold an expression using a matcher in a given context.

runFoldMatches :: BoundVars c => CompiledFold -> c -> CoreExpr -> Maybe (CoreExpr, VarEnv CoreExpr)

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

proves :: Clause -> Clause -> Bool

Determine if the left Clause proves the right Clause. Here, proves means that the clause is a substitution instance of the left one, where the top-level binders of the left clause are the holes.

lemmaMatch :: [Var] -> Clause -> Clause -> Maybe (VarEnv CoreExpr)

Determine if the right Clause is a substitution instance of the left Clause (which is a pattern with a given set of holes).

Equality

data Equality

An equality is represented as a set of universally quantified binders, and the LHS and RHS of the equality.

Constructors

Equality [CoreBndr] CoreExpr CoreExpr

Instances

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]

flipEquality :: Equality -> Equality

Flip the LHS and RHS of a Equality.

freeVarsEquality :: Equality -> VarSet

ppEqualityT :: PrettyPrinter -> PrettyH Equality