HERMIT.Dictionary.Composite

Documentation

externals :: [External]

unfoldBasicCombinatorR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr

Unfold the current expression if it is one of the basic combinators: ($), (.), id, flip, const, fst, snd, curry, and uncurry. This is intended to be used as a component of simplification traversals such as simplifyR or bashR.

simplifyR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadBindings c, ReadPath c Crumb, MonadCatch m, MonadUnique m) => Rewrite c m LCore

bashUsingR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, MonadCatch m) => [Rewrite c m LCore] -> Rewrite c m LCore

Perform the bash algorithm with a given list of rewrites.

bashR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadBindings c, ReadPath c Crumb, MonadCatch m, MonadUnique m) => Rewrite c m LCore

Bash is intended as a general-purpose cleanup/simplification command. It performs rewrites such as let floating, case floating, and case elimination, when safe. It also performs dead binding elimination and case reduction, and unfolds a number of basic combinators. See bashComponents for a list of rewrites performed. Bash also performs occurrence analysis and de-zombification on the result, to update IdInfo attributes relied-upon by GHC.

bashExtendedWithR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadBindings c, ReadPath c Crumb, MonadCatch m, MonadUnique m) => [Rewrite c m LCore] -> Rewrite c m LCore

An extensible bash. Given rewrites are performed before normal bash rewrites.

bashDebugR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasDynFlags m, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m, MonadUnique m) => Rewrite c m LCore

Like bashR, but outputs name of each successful sub-rewrite, providing a log. Also performs core lint on the result of a successful sub-rewrite. If core lint fails, shows core fragment before and after the sub-rewrite which introduced the problem. Note: core fragment which fails linting is still returned! Otherwise would behave differently than bashR. Useful for debugging the bash command itself.

smashR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasDynFlags m, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Rewrite c m LCore

Smash is a more powerful but less efficient version of bash. Unlike bash, smash is not concerned with whether it duplicates work, and is intended for use during proving tasks.

smashUsingR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, HasEmptyContext c, LemmaContext c, MonadCatch m) => [Rewrite c m LCore] -> [Rewrite c m LCore] -> Rewrite c m LCore

smashExtendedWithR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasDynFlags m, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => [Rewrite c m LCore] -> Rewrite c m LCore