module HERMIT.Dictionary.Composite
( externals
, unfoldBasicCombinatorR
, simplifyR
, bashUsingR
, bashR
, bashExtendedWithR
, bashDebugR
, smashR
, smashUsingR
, smashExtendedWithR
) where
import Control.Arrow
import Control.Monad
import Control.Monad.IO.Class
import Data.String (fromString)
import HERMIT.Context
import HERMIT.Core
import HERMIT.External
import HERMIT.GHC
import HERMIT.Kure
import HERMIT.Monad
import HERMIT.Name
import HERMIT.Dictionary.Common
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.Reasoning hiding (externals)
import HERMIT.Dictionary.Undefined hiding (externals)
import HERMIT.Dictionary.Unfold hiding (externals)
externals :: [External]
externals =
[ external "unfold-basic-combinator" (promoteExprR unfoldBasicCombinatorR :: RewriteH LCore)
[ "Unfold the current expression if it is one of the basic combinators:"
, "($), (.), id, flip, const, fst, snd, curry, and uncurry." ]
, external "simplify" (simplifyR :: RewriteH LCore)
[ "innermost (unfold-basic-combinator <+ beta-reduce-plus <+ safe-let-subst <+ case-reduce <+ let-elim)" ]
, external "bash" (bashR :: RewriteH LCore)
bashHelp .+ Eval .+ Deep .+ Loop
, external "smash" (smashR :: RewriteH LCore)
smashHelp .+ Eval .+ Deep .+ Loop .+ Experiment
, external "bash-extended-with" (bashExtendedWithR :: [RewriteH LCore] -> RewriteH LCore)
[ "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 LCore] -> RewriteH LCore)
[ "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 LCore)
[ "verbose bash - most useful with set-auto-corelint True" ] .+ Eval .+ Deep .+ Loop
]
basicCombinators :: [HermitName]
basicCombinators = map fromString ["$",".","id","flip","const","fst","snd","curry","uncurry"]
unfoldBasicCombinatorR :: ( AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb
, MonadCatch m )
=> Rewrite c m CoreExpr
unfoldBasicCombinatorR = setFailMsg "unfold-basic-combinator failed." $ orR (map f basicCombinators)
where f nm = voidM (callNameT nm) >> voidM callSaturatedT >> unfoldR
voidM = liftM (const ())
simplifyR :: ( AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadBindings c, ReadPath c Crumb
, MonadCatch m, MonadUnique m )
=> Rewrite c m LCore
simplifyR = setFailMsg "Simplify failed: nothing to simplify." $
innermostR ( promoteBindR recToNonrecR
<+ promoteExprR ( unfoldBasicCombinatorR
<+ betaReducePlusR
<+ letNonRecSubstSafeR
<+ caseReduceR False
<+ letElimR )
)
bashR :: ( AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadBindings c, ReadPath c Crumb
, MonadCatch m, MonadUnique m )
=> Rewrite c m LCore
bashR = bashExtendedWithR []
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
bashExtendedWithR rs = bashUsingR (rs ++ map fst bashComponents)
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
bashDebugR = bashUsingR [ bracketR nm r >>> catchM (promoteT lintExprT >> idR) traceR
| (r,nm) <- bashComponents ]
bashUsingR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, MonadCatch m)
=> [Rewrite c m LCore] -> Rewrite c m LCore
bashUsingR rs = setFailMsg "bash failed: nothing to do." $
repeatR (occurAnalyseR >>> onetdR (catchesT rs)) >+> anytdR (promoteExprR dezombifyR) >+> occurAnalyseChangedR
bashHelp :: [String]
bashHelp = "Iteratively apply the following rewrites until nothing changes:"
: map snd (bashComponents :: [(RewriteH LCore,String)]
)
bashComponents :: ( AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb
, MonadCatch m, MonadUnique m )
=> [(Rewrite c m LCore, String)]
bashComponents =
[
(promoteExprR betaReduceR, "beta-reduce")
, (promoteExprR (caseReduceR True), "case-reduce")
, (promoteExprR (caseReduceUnfoldR True), "case-reduce-unfold")
, (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")
]
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
smashR = smashExtendedWithR []
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
smashExtendedWithR rs = smashUsingR (rs ++ map fst smashComponents1) (map fst smashComponents2)
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
smashUsingR rs1 rs2 =
setFailMsg "smash failed: nothing to do." $
repeatR (occurAnalyseR >>> (onetdR (catchesT rs1) <+ onetdR (catchesT rs2))) >+> anytdR (promoteExprR dezombifyR) >+> occurAnalyseChangedR
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 LCore,String)]
)
smashComponents1 :: ( AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb
, HasDynFlags m, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m )
=> [(Rewrite c m LCore, String)]
smashComponents1 =
[
(promoteExprR betaReduceR, "beta-reduce")
, (promoteExprR (caseReduceR True), "case-reduce")
, (promoteExprR (caseReduceUnfoldR True), "case-reduce-unfold")
, (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")
, (promoteExprR castFloatAppR, "cast-float-app")
, (promoteExprR castFloatLamR, "cast-float-lam")
, (promoteExprR undefinedExprR, "undefined-expr")
]
smashComponents2 :: ( ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasEmptyContext c
, MonadCatch m, MonadUnique m )
=> [(Rewrite c m LCore, String)]
smashComponents2 =
[ (promoteExprR caseElimMergeAltsR, "case-elim-merge-alts")
, (promoteClauseR quantIdentitiesR, "quant-indentities")
, (promoteClauseR reflexivityR, "reflexivity")
]