module HERMIT.Dictionary.Composite
( externals
, unfoldBasicCombinatorR
, simplifyR
, bashUsingR
, bashR
, bashExtendedWithR
, bashDebugR
)
where
import Control.Arrow
import HERMIT.Context
import HERMIT.Core
import HERMIT.GHC
import HERMIT.Monad
import HERMIT.Kure
import HERMIT.External
import HERMIT.Dictionary.Debug hiding (externals)
import HERMIT.Dictionary.GHC hiding (externals)
import HERMIT.Dictionary.Inline hiding (externals)
import HERMIT.Dictionary.Local hiding (externals)
import HERMIT.Dictionary.Unfold hiding (externals)
externals :: [External]
externals =
[ external "unfold-basic-combinator" (promoteExprR unfoldBasicCombinatorR :: RewriteH Core)
[ "Unfold the current expression if it is one of the basic combinators: ($), (.), id, flip, const, fst or snd." ]
, external "simplify" (simplifyR :: RewriteH Core)
[ "innermost (unfold-basic-combinator <+ beta-reduce-plus <+ safe-let-subst <+ case-reduce <+ let-elim)" ]
, external "bash" (bashR :: RewriteH Core)
bashHelp .+ Eval .+ Deep .+ Loop
, external "smash" (smashR :: RewriteH Core)
smashHelp .+ Eval .+ Deep .+ Loop .+ Experiment
, external "bash-extended-with" (bashExtendedWithR :: [RewriteH Core] -> RewriteH Core)
[ "Run \"bash\" extended with additional rewrites.",
"Note: be sure that the new rewrite either fails or makes progress, else this may loop."
] .+ Eval .+ Deep .+ Loop
, external "smash-extended-with" (smashExtendedWithR :: [RewriteH Core] -> RewriteH Core)
[ "Run \"smash\" extended with additional rewrites.",
"Note: be sure that the new rewrite either fails or makes progress, else this may loop."
] .+ Eval .+ Deep .+ Loop
, external "bash-debug" (bashDebugR :: RewriteH Core)
[ "verbose bash - most useful with set-auto-corelint True" ] .+ Eval .+ Deep .+ Loop
]
basicCombinators :: [String]
basicCombinators = ["$",".","id","flip","const","fst","snd","curry","uncurry"]
unfoldBasicCombinatorR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c) => Rewrite c HermitM CoreExpr
unfoldBasicCombinatorR = setFailMsg "unfold-basic-combinator failed." $
unfoldNamesR basicCombinators
simplifyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c) => Rewrite c HermitM Core
simplifyR = setFailMsg "Simplify failed: nothing to simplify." $
innermostR ( promoteBindR recToNonrecR
<+ promoteExprR ( unfoldBasicCombinatorR
<+ betaReducePlusR
<+ letNonRecSubstSafeR
<+ caseReduceR False
<+ letElimR )
)
bashR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c) => Rewrite c HermitM Core
bashR = bashExtendedWithR []
bashExtendedWithR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c) => [Rewrite c HermitM Core] -> Rewrite c HermitM Core
bashExtendedWithR rs = bashUsingR (rs ++ map fst bashComponents)
smashR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c) => Rewrite c HermitM Core
smashR = smashExtendedWithR []
smashExtendedWithR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c) => [Rewrite c HermitM Core] -> Rewrite c HermitM Core
smashExtendedWithR rs = smashUsingR (rs ++ map fst smashComponents1) (map fst smashComponents2)
bashDebugR :: RewriteH Core
bashDebugR = bashUsingR [ idR >>= \e -> r >>> traceR nm >>> (catchM (promoteT lintExprT >> idR)
(\s -> do _ <- return e >>> observeR "[before]"
observeR ("[" ++ nm ++ "]\n" ++ s)))
| (r,nm) <- bashComponents ]
bashUsingR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, HasEmptyContext c, MonadCatch m) => [Rewrite c m Core] -> Rewrite c m Core
bashUsingR rs =
setFailMsg "bash failed: nothing to do." $
repeatR (occurAnalyseR >>> onetdR (catchesT rs)) >+> anytdR (promoteExprR dezombifyR) >+> occurAnalyseChangedR
smashUsingR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, HasEmptyContext c, MonadCatch m) => [Rewrite c m Core] -> [Rewrite c m Core] -> Rewrite c m Core
smashUsingR rs1 rs2 =
setFailMsg "smash failed: nothing to do." $
repeatR (occurAnalyseR >>> (onetdR (catchesT rs1) <+ onetdR (catchesT rs2))) >+> anytdR (promoteExprR dezombifyR) >+> occurAnalyseChangedR
bashHelp :: [String]
bashHelp = "Iteratively apply the following rewrites until nothing changes:" : map snd (bashComponents
:: [(RewriteH Core,String)]
)
bashComponents :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c) => [(Rewrite c HermitM Core, String)]
bashComponents =
[
(promoteExprR betaReduceR, "beta-reduce")
, (promoteExprR (caseReduceR True), "case-reduce")
, (promoteExprR (caseReduceIdR True), "case-reduce-id")
, (promoteExprR caseElimSeqR, "case-elim-seq")
, (promoteExprR unfoldBasicCombinatorR, "unfold-basic-combinator")
, (promoteExprR inlineCaseAlternativeR, "inline-case-alternative")
, (promoteExprR etaReduceR, "eta-reduce")
, (promoteExprR letNonRecSubstSafeR, "let-nonrec-subst-safe")
, (promoteExprR caseFloatAppR, "case-float-app")
, (promoteExprR caseFloatCaseR, "case-float-case")
, (promoteExprR caseFloatLetR, "case-float-let")
, (promoteExprR caseFloatCastR, "case-float-cast")
, (promoteExprR letFloatAppR, "let-float-app")
, (promoteExprR letFloatArgR, "let-float-arg")
, (promoteExprR letFloatLamR, "let-float-lam")
, (promoteExprR letFloatLetR, "let-float-let")
, (promoteExprR letFloatCaseR, "let-float-case")
, (promoteExprR letFloatCastR, "let-float-cast")
, (promoteProgR letFloatTopR, "let-float-top")
, (promoteExprR castElimReflR, "cast-elim-refl")
, (promoteExprR castElimSymR, "cast-elim-sym")
]
smashHelp :: [String]
smashHelp = "A more powerful but less efficient version of \"bash\", intended for use while proving lemmas. Iteratively apply the following rewrites until nothing changes:" : map snd (smashComponents1 ++ smashComponents2
:: [(RewriteH Core,String)]
)
smashComponents1 :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c) => [(Rewrite c HermitM Core, String)]
smashComponents1 =
[
(promoteExprR betaReduceR, "beta-reduce")
, (promoteExprR (caseReduceR True), "case-reduce")
, (promoteExprR (caseReduceIdR True), "case-reduce-id")
, (promoteExprR caseElimSeqR, "case-elim-seq")
, (promoteExprR unfoldBasicCombinatorR, "unfold-basic-combinator")
, (promoteExprR inlineCaseAlternativeR, "inline-case-alternative")
, (promoteExprR etaReduceR, "eta-reduce")
, (promoteExprR letNonRecSubstR, "let-nonrec-subst")
, (promoteExprR caseFloatAppR, "case-float-app")
, (promoteExprR caseFloatCaseR, "case-float-case")
, (promoteExprR caseFloatLetR, "case-float-let")
, (promoteExprR caseFloatCastR, "case-float-cast")
, (promoteExprR letFloatAppR, "let-float-app")
, (promoteExprR letFloatArgR, "let-float-arg")
, (promoteExprR letFloatLamR, "let-float-lam")
, (promoteExprR letFloatLetR, "let-float-let")
, (promoteExprR letFloatCaseR, "let-float-case")
, (promoteExprR letFloatCastR, "let-float-cast")
, (promoteProgR letFloatTopR, "let-float-top")
, (promoteExprR castElimReflR, "cast-elim-refl")
, (promoteExprR castElimSymR, "cast-elim-sym")
]
smashComponents2 :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c) => [(Rewrite c HermitM Core, String)]
smashComponents2 =
[
(promoteExprR caseElimMergeAltsR, "case-elim-merge-alts")
]