module DDC.Core.Transform.Beta
( Config (..)
, configZero
, Info (..)
, betaReduce)
where
import DDC.Base.Pretty
import DDC.Core.Collect
import DDC.Core.Exp
import DDC.Core.Predicates
import DDC.Core.Transform.TransformUpX
import DDC.Core.Transform.SubstituteTX
import DDC.Core.Transform.SubstituteWX
import DDC.Core.Transform.SubstituteXX
import DDC.Core.Simplifier.Result
import Control.Monad.Writer (Writer, runWriter, tell)
import Data.Monoid (Monoid, mempty, mappend)
import Data.Typeable (Typeable)
import DDC.Type.Env (Env)
import DDC.Type.Compounds
import qualified DDC.Type.Env as Env
import qualified Data.Set as Set
data Config
= Config
{
configBindRedexes :: Bool }
deriving Show
configZero :: Config
configZero
= Config
{ configBindRedexes = False }
data Info
= Info
{
infoTypes :: Int
, infoWits :: Int
, infoValues :: Int
, infoValuesLetted :: Int
, infoValuesSkipped :: Int }
deriving Typeable
instance Pretty Info where
ppr (Info ty wit val lets skip)
= text "Beta reduction:"
<$> indent 4 (vcat
[ text "Types: " <> int ty
, text "Witnesses: " <> int wit
, text "Values: " <> int val
, text "Values letted: " <> int lets
, text "Values skipped: " <> int skip ])
instance Monoid Info where
mempty = Info 0 0 0 0 0
mappend (Info ty1 wit1 val1 lets1 skip1)
(Info ty2 wit2 val2 lets2 skip2)
= Info
(ty1 + ty2) (wit1 + wit2) (val1 + val2)
(lets1 + lets2) (skip1 + skip2)
betaReduce
:: forall (c :: * -> * -> *) a n
. (Ord n, TransformUpMX (Writer Info) c)
=> Config
-> c a n
-> TransformResult (c a n)
betaReduce config x
=
let (x', info) = runWriter
$ transformUpMX (betaReduce1 config) Env.empty Env.empty x
progress
= case info of
Info ty wit val lets' _
-> (ty + wit + val + lets') > 0
in TransformResult
{ result = x'
, resultAgain = progress
, resultProgress = progress
, resultInfo = TransformInfo info }
betaReduce1
:: Ord n
=> Config
-> Env n
-> Env n
-> Exp a n
-> Writer Info (Exp a n)
betaReduce1 config _kenv tenv xx
= let ret info x = tell info >> return x
in case xx of
XApp a (XLAM _ b11 x12) (XType t2)
| isRegionKind $ typeOfBind b11
-> let sup = support Env.empty Env.empty x12
usUsed = Set.unions
[ supportTyConXArg sup
, supportSpVarXArg sup ]
usesBind = any (flip boundMatchesBind b11)
$ Set.toList usUsed
fvs2 = freeT Env.empty t2
in ret mempty { infoTypes = 1}
$ if usesBind || Set.null fvs2
then substituteTX b11 t2 x12
else XCast a (CastWeakenClosure [XType t2])
$ substituteTX b11 t2 x12
XApp _ (XLAM _ b11 x12) (XType t2)
-> ret mempty { infoTypes = 1 }
$ substituteTX b11 t2 x12
XApp a (XLam _ b11 x12) (XWitness w2)
-> let usesBind = any (flip boundMatchesBind b11)
$ Set.toList $ freeX tenv x12
fvs2 = freeX Env.empty w2
in ret mempty { infoWits = 1 }
$ if usesBind || Set.null fvs2
then substituteWX b11 w2 x12
else XCast a (CastWeakenClosure [XWitness w2])
$ substituteWX b11 w2 x12
XApp a (XLam _ b11 x12) x2
| canBetaSubstX x2
-> let usesBind = any (flip boundMatchesBind b11)
$ Set.toList $ freeX tenv x12
fvs2 = freeX Env.empty x2
in ret mempty { infoValues = 1 }
$ if usesBind || Set.null fvs2
then substituteXX b11 x2 x12
else XCast a (CastWeakenClosure [x2])
$ substituteXX b11 x2 x12
| configBindRedexes config
-> ret mempty { infoValuesLetted = 1 }
$ XLet a (LLet b11 x2) x12
| otherwise
-> ret mempty { infoValuesSkipped = 1 }
$ xx
_ -> return xx
canBetaSubstX :: Exp a n -> Bool
canBetaSubstX xx
= case xx of
XVar{} -> True
XCon{} -> True
XLam{} -> True
XLAM{} -> True
XApp _ x1 (XType _)
-> canBetaSubstX x1
XApp _ x1 (XWitness _)
-> canBetaSubstX x1
_ -> False