module HERMIT.Dictionary.Local
(
HERMIT.Dictionary.Local.externals
, module HERMIT.Dictionary.Local.Bind
, module HERMIT.Dictionary.Local.Case
, module HERMIT.Dictionary.Local.Cast
, module HERMIT.Dictionary.Local.Let
, abstractR
, pushR
, betaReduceR
, betaReducePlusR
, betaExpandR
, etaReduceR
, etaExpandR
, multiEtaExpandR
, flattenModuleR
, flattenProgramR
, flattenProgramT
)
where
import HERMIT.Core
import HERMIT.Context
import HERMIT.Kure
import HERMIT.Monad
import HERMIT.External
import HERMIT.GHC
import HERMIT.Utilities
import HERMIT.Dictionary.Common
import HERMIT.Dictionary.GHC (substCoreExpr)
import HERMIT.Dictionary.Local.Bind hiding (externals)
import qualified HERMIT.Dictionary.Local.Bind as Bind
import HERMIT.Dictionary.Local.Case hiding (externals)
import qualified HERMIT.Dictionary.Local.Case as Case
import HERMIT.Dictionary.Local.Cast hiding (externals)
import qualified HERMIT.Dictionary.Local.Cast as Cast
import HERMIT.Dictionary.Local.Let hiding (externals)
import qualified HERMIT.Dictionary.Local.Let as Let
import qualified Language.Haskell.TH as TH
import Control.Arrow
externals :: [External]
externals =
[ external "beta-reduce" (promoteExprR betaReduceR :: RewriteH Core)
[ "((\\ v -> E1) E2) ==> let v = E2 in E1"
, "This form of beta-reduction is safe if E2 is an arbitrary expression"
, "(won't duplicate work)." ] .+ Eval .+ Shallow
, external "beta-reduce-plus" (promoteExprR betaReducePlusR :: RewriteH Core)
[ "Perform one or more beta-reductions."] .+ Eval .+ Shallow
, external "beta-expand" (promoteExprR betaExpandR :: RewriteH Core)
[ "(let v = e1 in e2) ==> (\\ v -> e2) e1" ] .+ Shallow
, external "eta-reduce" (promoteExprR etaReduceR :: RewriteH Core)
[ "(\\ v -> e1 v) ==> e1" ] .+ Eval .+ Shallow
, external "eta-expand" (promoteExprR . etaExpandR . show :: TH.Name -> RewriteH Core)
[ "\"eta-expand 'v\" performs e1 ==> (\\ v -> e1 v)" ] .+ Shallow .+ Introduce
, external "flatten-module" (promoteModGutsR flattenModuleR :: RewriteH Core)
[ "Flatten all the top-level binding groups in the module to a single recursive binding group."
, "This can be useful if you intend to appply GHC RULES." ]
, external "flatten-program" (promoteProgR flattenProgramR :: RewriteH Core)
[ "Flatten all the top-level binding groups in a program (list of binding groups) to a single"
, "recursive binding group. This can be useful if you intend to apply GHC RULES." ]
, external "abstract" (promoteExprR . abstractR :: TH.Name -> RewriteH Core)
[ "Abstract over a variable using a lambda."
, "e ==> (\\ x -> e) x" ] .+ Shallow .+ Introduce .+ Context
, external "push" ((\ nm strictf -> push (Just strictf) (cmpTHName2Var nm)) :: TH.Name -> RewriteH Core -> RewriteH Core)
[ "Push a function 'f into a case-expression or let-expression argument,"
, "given a proof that f (fully saturated with type arguments) is strict." ] .+ Shallow .+ Commute
, external "push-unsafe" (push Nothing . cmpTHName2Var :: TH.Name -> RewriteH Core)
[ "Push a function 'f into a case-expression or let-expression argument."
, "Requires 'f to be strict." ] .+ Shallow .+ Commute .+ PreCondition
]
++ Bind.externals
++ Case.externals
++ Cast.externals
++ Let.externals
betaReduceR :: MonadCatch m => Rewrite c m CoreExpr
betaReduceR = setFailMsg ("Beta-reduction failed: " ++ wrongExprForm "App (Lam v e1) e2") $
do App (Lam v e1) e2 <- idR
return $ Let (NonRec v e2) e1
multiBetaReduceR :: MonadCatch m => (Int -> Bool) -> Rewrite c m CoreExpr
multiBetaReduceR p = prefixFailMsg "Multi-Beta-Reduce failed: " $
do
e <- idR
let (f,xs) = collectArgs e
guardMsg (p (length xs)) "incorrect number of arguments."
let (vs,e0) = collectBinders f
guardMsg (length vs >= length xs) "insufficent lambdas."
let (vs1,vs2) = splitAt (length xs) vs
return
$ mkLets (zipWith NonRec vs1 xs)
$ mkLams vs2 e0
betaReducePlusR :: MonadCatch m => Rewrite c m CoreExpr
betaReducePlusR = multiBetaReduceR (> 0)
betaExpandR :: MonadCatch m => Rewrite c m CoreExpr
betaExpandR = setFailMsg ("Beta-expansion failed: " ++ wrongExprForm "Let (NonRec v e1) e2") $
do Let (NonRec v e1) e2 <- idR
return $ App (Lam v e2) e1
etaReduceR :: MonadCatch m => Rewrite c m CoreExpr
etaReduceR = prefixFailMsg "Eta-reduction failed: " $
withPatFailMsg (wrongExprForm "Lam v (App f (Var v))") $
do Lam v1 (App f e) <- idR
case e of
Var v2 -> guardMsg (v1 == v2) "the expression has the right form, but the variables are not equal."
Type ty -> case getTyVar_maybe ty of
Nothing -> fail "the argument expression is not a type variable."
Just v2 -> guardMsg (v1 == v2) "type variables are not equal."
_ -> fail "the argument expression is not a variable."
guardMsg (v1 `notElemVarSet` freeVarsExpr f) $ var2String v1 ++ " is free in the function being applied."
return f
etaExpandR :: String -> Rewrite c HermitM CoreExpr
etaExpandR nm = prefixFailMsg "Eta-expansion failed: " $
contextfreeT $ \ e -> let ty = exprKindOrType e in
case splitFunTy_maybe ty of
Just (argTy, _) -> do v <- newIdH nm argTy
return $ Lam v (App e (varToCoreExpr v))
Nothing -> case splitForAllTy_maybe ty of
Just (tv,_) -> do v <- newTyVarH nm (tyVarKind tv)
return $ Lam v (App e (varToCoreExpr v))
Nothing -> fail "type of expression is not a function or a forall."
multiEtaExpandR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c) => [String] -> Rewrite c HermitM CoreExpr
multiEtaExpandR [] = idR
multiEtaExpandR (nm:nms) = etaExpandR nm >>> lamAllR idR (multiEtaExpandR nms)
flattenModuleR :: (ExtendPath c Crumb, Monad m) => Rewrite c m ModGuts
flattenModuleR = modGutsR flattenProgramR
flattenProgramR :: Monad m => Rewrite c m CoreProg
flattenProgramR = do bnd <- flattenProgramT
return (bindsToProg [bnd])
flattenProgramT :: Monad m => Translate c m CoreProg CoreBind
flattenProgramT = do bds <- arr (concatMap bindToVarExprs . progToBinds)
guardMsg (nodups $ map fst bds) "Top-level bindings contain multiple occurrences of a name."
return (Rec bds)
abstractR :: (ReadBindings c) => TH.Name -> Rewrite c HermitM CoreExpr
abstractR nm = prefixFailMsg "abstraction failed: " $
do v <- findBoundVarT nm
v' <- constT (cloneVarH id v)
e <- arr (substCoreExpr v (varToCoreExpr v'))
return $ App (Lam v' e) (varToCoreExpr v)
push :: Maybe (RewriteH Core)
-> (Id -> Bool)
-> RewriteH Core
push mstrict p = promoteExprR (pushR (extractR `fmap` mstrict) p)
pushR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasGlobalRdrEnv c)
=> Maybe (Rewrite c HermitM CoreExpr)
-> (Id -> Bool)
-> Rewrite c HermitM CoreExpr
pushR strictf p = prefixFailMsg "push failed: " $
withPatFailMsg (wrongExprForm "App f e") $
do App f e <- idR
case collectArgs f of
(Var i,args) -> do
guardMsg (p i) $ "identifier not matched."
guardMsg (all isTypeArg args) $ "initial arguments are not all type arguments."
case e of
Case {} -> caseFloatArgR (Just (f,strictf))
Let {} -> letFloatArgR
_ -> fail "argument is not a Case or Let."
_ -> fail "no identifier to match."