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.Fragment
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 (KindEnv, TypeEnv)
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)
=> Profile n
-> Config
-> c a n
-> TransformResult (c a n)
betaReduce profile config x
=
let (x', info) = runWriter
$ transformUpMX (betaReduce1 profile 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
=> Profile n
-> Config
-> KindEnv n
-> TypeEnv n
-> Exp a n
-> Writer Info (Exp a n)
betaReduce1 profile config _kenv tenv xx
= let ret info x = tell info >> return x
weakenClosure a usesBind fvs2 xWeak x
| featuresTrackedClosures $ profileFeatures profile
, not (usesBind || Set.null fvs2)
= XCast a (CastWeakenClosure [xWeak]) x
| otherwise
= x
in case xx of
XApp a (XLAM _ b11 x12) (XType a2 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}
$ weakenClosure a usesBind fvs2 (XType a2 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 a2 w2)
-> let usesBind = any (flip boundMatchesBind b11)
$ Set.toList $ freeX tenv x12
fvs2 = freeX Env.empty w2
in ret mempty { infoWits = 1 }
$ weakenClosure a usesBind fvs2 (XWitness a2 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 }
$ weakenClosure a usesBind fvs2 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