module DDC.Core.Transform.Beta
( Config (..)
, configZero
, Info (..)
, betaReduce)
where
import DDC.Base.Pretty
import DDC.Core.Exp.Annot
import DDC.Core.Fragment
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.Typeable (Typeable)
import DDC.Type.Env (KindEnv, TypeEnv)
import qualified DDC.Type.Env as Env
import Prelude hiding ((<$>))
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
in case xx of
XApp _a (XLAM _ b11 x12) (XType _a2 t2)
| isRegionKind $ typeOfBind b11
-> ret mempty { infoTypes = 1}
$ substituteTX b11 t2 x12
XApp _a (XLAM _ b11 x12) (XType _ t2)
-> ret mempty { infoTypes = 1 }
$ substituteTX b11 t2 x12
XApp _a (XLam _ b11 x12) (XWitness _a2 w2)
-> ret mempty { infoWits = 1 }
$ substituteWX b11 w2 x12
XApp a (XLam _ b11 x12) x2
| canBetaSubstX x2
-> ret mempty { infoValues = 1 }
$ 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