hermit-0.6.0.0: Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone
LanguageHaskell2010

HERMIT.Dictionary.Unfold

Synopsis

Documentation

betaReducePlusR :: MonadCatch m => Rewrite c m CoreExpr Source

Perform one or more beta reductions.

rememberR :: RememberedName -> Rewrite c HermitM Core Source

Stash a binding with a name for later use. Allows us to look at past definitions.

unfoldR :: forall c m. (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr Source

A more powerful inline. Matches two cases: Var ==> inlines App ==> inlines the head of the function call for the app tree

unfoldStashR :: ReadBindings c => RememberedName -> Rewrite c HermitM CoreExpr Source

Stash a binding with a name for later use. Allows us to look at past definitions. rememberR :: String -> Transform c m Core () rememberR label = contextfreeT $ core -> case core of DefCore def -> saveDef label def BindCore (NonRec i e) -> saveDef label (Def i e) _ -> fail "remember: not a binding"

Apply a stashed definition (like inline, but looks in stash instead of context).