diff --git a/DDC/Core/Analysis/Arity.hs b/DDC/Core/Analysis/Arity.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Analysis/Arity.hs @@ -0,0 +1,141 @@ + +-- | Slurp out arities of function bindings. +-- and infer arities for primitives based on their types. +-- +-- For function bindings the arity is the number of outer-most lambdas +-- in the definition. +-- +-- For primitives, the arity is the number of function +-- constructors in its type. +-- +module DDC.Core.Analysis.Arity + ( -- * Arities map + Arities + , emptyArities + , extendsArities + , getArity + + -- * Arity analysis + , aritiesOfModule + , aritiesOfLets + , aritiesOfPat + , arityFromType + , arityOfExp) +where +import DDC.Core.Module +import DDC.Core.Exp.Annot +import DDC.Data.ListUtils +import Control.Monad +import Data.Maybe +import qualified Data.Map as Map + + +-- | Arities of named and anonymous bindings. +type Arities n = (Map.Map n Int, [Int]) + + +-- | Empty arities context. +emptyArities :: Arities n +emptyArities = (Map.empty, []) + + +-- | Extend map with some binders and their arities. +extendsArities :: Ord n => Arities n -> [(Bind n, Int)] -> Arities n +extendsArities arity exts = foldl go arity exts + where go (named, anon) (BNone _t, _) = (named,anon) + go (named, anon) (BAnon _t, a) = (named, a:anon) + go (named, anon) (BName n _t, a) = (Map.insert n a named, anon) + + +-- | Look up a binder's arity from the arity map +-- or determine it from its type in the case of primops. +getArity :: Ord n => Arities n -> Bound n -> Maybe Int +getArity (named, anon) u + = case u of + -- Get arities of anonymous things from the stack. + UIx ix + -> let Just x = index anon ix + in Just x + + -- Lookup arities of named things from the stack. + UName n -> Map.lookup n named + + -- Get a primitive's arity from its type. + -- The arities of primitives always match their types, so this is ok. + UPrim _ t -> arityFromType t + + +-- Slurp ---------------------------------------------------------------------- +-- | Slurp out arities of imports and top-level bindings from a module. +aritiesOfModule :: Ord n => Module a n -> Arities n +aritiesOfModule mm + = let (lts, _) = splitXLets $ moduleBody mm + + aritiesLets + = concat $ catMaybes $ map aritiesOfLets lts + + aritiesImports + = catMaybes + $ [ case arityFromType (typeOfImportValue isrc) of + Just a -> Just (BName n (typeOfImportValue isrc), a) + Nothing -> Nothing + | (n, isrc) <- moduleImportValues mm ] + + in emptyArities + `extendsArities` aritiesImports + `extendsArities` aritiesLets + + +-- | Get the arities of a `Lets` +aritiesOfLets :: Ord n => Lets a n -> Maybe [(Bind n, Int)] +aritiesOfLets ll + = let get (b, x) + = case arityOfExp x of + Nothing -> Nothing + Just a -> Just (b, a) + in case ll of + LLet b x -> sequence $ map get [(b, x)] + LRec bxs -> sequence $ map get bxs + _ -> Just [] + + +-- | Retrieve binders from case pattern, so we can extend the arity context. +-- We don't know anything about their values, so record as 0. +aritiesOfPat :: Pat n -> [(Bind n, Int)] +aritiesOfPat p + = case p of + PDefault -> [] + (PData _b bs) -> zip bs (repeat 0) + + +-- | Get the arity of an expression. +arityOfExp :: Ord n => Exp a n -> Maybe Int +arityOfExp xx + = case xx of + -- Counting all binders, because they all correspond to XApps. + XLam _ _ e -> liftM (+ 1) $ arityOfExp e + XLAM _ _ e -> liftM (+ 1) $ arityOfExp e + + -- Determine a data constructor's arity from its type. + XCon _ (DaConPrim _ t) + -> arityFromType t + + -- Anything else we'll need to apply one at a time + _ -> Just 0 + + +-- | Determine the arity of an expression by looking at its type. +-- Count all the function arrows, and foralls. +arityFromType :: Ord n => Type n -> Maybe Int +arityFromType tt + | TForall _ t <- tt + = case arityFromType t of + Nothing -> Nothing + Just a -> Just (1 + a) + + | isBot tt + = Nothing + + | (args, _) <- takeTFunArgResult tt + = Just (length args) + diff --git a/DDC/Core/Analysis/Usage.hs b/DDC/Core/Analysis/Usage.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Analysis/Usage.hs @@ -0,0 +1,292 @@ + +-- | Annotate let bindings with how their bound variables are used. +module DDC.Core.Analysis.Usage + ( -- * Usage map + Used (..) + , UsedMap (..) + + -- * Usage analysis + , usageModule + , usageX) +where +import DDC.Core.Module +import DDC.Core.Exp.Annot +import Data.List +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Maybe (mapMaybe) + + +-- Used ----------------------------------------------------------------------- +-- | Tracks how a bound variable is used. +data Used + -- | Bound variable is used as the function in an application. + = UsedFunction + + -- | Bound variable is destructed by a case-expression. + | UsedDestruct + + -- | Bound variable is used inside a @weakclo@ cast. + | UsedInCast + + -- | Bound variable has an occurrence that is not one of the above. + | UsedOcc + + -- | Usage is inside a Lambda abstraction (either type or value) + | UsedInLambda Used + + -- | Usage is inside a case alternative. + | UsedInAlt Used + deriving (Eq, Show) + + +-- UsedMap -------------------------------------------------------------------- +-- | Map of bound name to how the variable is used. +data UsedMap n + = UsedMap (Map n [Used]) + deriving Show + + +-- | An empty usage map. +empty :: UsedMap n +empty = UsedMap (Map.empty) + + +-- | Add a single usage to a usage map. +accUsed :: Ord n => Bound n -> Used -> UsedMap n -> UsedMap n +accUsed u used um@(UsedMap m) + = case u of + UName n -> UsedMap $ Map.insertWith (++) n [used] m + _ -> um + +-- | Combine two usage maps. +plusUsedMap :: Ord n => UsedMap n -> UsedMap n -> UsedMap n +plusUsedMap (UsedMap map1) (UsedMap map2) + = UsedMap $ Map.unionWith (++) map1 map2 + + +-- | Combine a list of usage maps into a single one. +sumUsedMap :: Ord n => [UsedMap n] -> UsedMap n +sumUsedMap [] = UsedMap Map.empty +sumUsedMap (m:ms) + = foldl' plusUsedMap m ms + + +-- | Remove some binds from a usage map +removeUsedMap :: Ord n => UsedMap n -> [Bind n] -> UsedMap n +removeUsedMap (UsedMap m) bs + = UsedMap + $ foldr Map.delete m + $ mapMaybe takeNameOfBind bs + + +-- Module --------------------------------------------------------------------- +-- | Annotate all binding occurrences of variables in an expression +-- with how they are used. +usageModule + :: Ord n + => Module a n + -> Module (UsedMap n, a) n +usageModule + (ModuleCore + { moduleName = name + , moduleIsHeader = isHeader + , moduleExportTypes = exportTypes + , moduleExportValues = exportValues + , moduleImportTypes = importTypes + , moduleImportCaps = importCaps + , moduleImportValues = importValues + , moduleImportDataDefs = importDataDefs + , moduleImportTypeDefs = importTypeDefs + , moduleDataDefsLocal = dataDefsLocal + , moduleTypeDefsLocal = typeDefsLocal + , moduleBody = body }) + + = ModuleCore + { moduleName = name + , moduleIsHeader = isHeader + , moduleExportTypes = exportTypes + , moduleExportValues = exportValues + , moduleImportTypes = importTypes + , moduleImportCaps = importCaps + , moduleImportValues = importValues + , moduleImportDataDefs = importDataDefs + , moduleImportTypeDefs = importTypeDefs + , moduleDataDefsLocal = dataDefsLocal + , moduleTypeDefsLocal = typeDefsLocal + , moduleBody = usageX body } + + +-- Exp ------------------------------------------------------------------------ +-- | Annotate all binding occurrences of variables in an expression +-- with how they are used. +usageX :: Ord n + => Exp a n + -> Exp (UsedMap n, a) n +usageX xx = snd $ usageX' xx + + +usageX' :: Ord n + => Exp a n + -> (UsedMap n, Exp (UsedMap n, a) n) + +usageX' xx + = case xx of + XVar a u + | used <- accUsed u UsedOcc empty + -> ( used + , XVar (used, a) u) + + XCon a u + -> ( empty + , XCon (empty, a) u) + + -- Wrap usages from the body in UsedInLambda to singla that if we move + -- the definition here then it might not be demanded at runtime. + XLAM a b1 x2 + | ( used2, x2') <- usageX' x2 + , UsedMap us2 <- used2 + , used2' <- UsedMap (Map.map (map UsedInLambda) us2) + , cleared <- removeUsedMap used2' [b1] + -> ( cleared + , XLAM (used2', a) b1 x2') + + -- Wrap usages from the body in UsedInLambda to signal that if we move + -- the definition here then it might not be demanded at runtime. + XLam a b1 x2 + | ( used2, x2') <- usageX' x2 + , UsedMap us2 <- used2 + , used2' <- UsedMap (Map.map (map UsedInLambda) us2) + , cleared <- removeUsedMap used2' [b1] + -> ( cleared + , XLam (used2', a) b1 x2') + + XApp a x1 x2 + -- application of a function variable. + | XVar a1 u <- x1 + , used1 <- accUsed u UsedFunction empty + , (used2, x2') <- usageX' x2 + , used' <- used1 `plusUsedMap` used2 + -> ( used' + , XApp (used', a) (XVar (used1, a1) u) x2') + + -- General application. + | ( used1, x1') <- usageX' x1 + , ( used2, x2') <- usageX' x2 + , used' <- used1 `plusUsedMap` used2 + -> ( used' + , XApp (used', a) x1' x2') + + XLet a lts x2 + | ( used1, lts') <- usageLets lts + , ( used2, x2') <- usageX' x2 + , used' <- used1 `plusUsedMap` used2 + , cleared <- removeUsedMap used' + $ uncurry (++) (bindsOfLets lts) + -> ( cleared + , XLet (used', a) lts' x2') + + -- Wrap usages in the Alts in UsedInAlt to signal that if we move + -- the definition here then it might not be demanded at runtime. + XCase a x1 alts + | ( used1, x1') <- usageX' x1 + , ( usedA, alts') <- unzip $ map usageAlt alts + , UsedMap usA <- sumUsedMap usedA + , usedA' <- UsedMap (Map.map (map UsedInAlt) usA) + , used' <- plusUsedMap used1 usedA' + -> ( used' + , XCase (used', a) x1' alts' ) + + XCast a c x1 + | (used1, x1') <- usageX' x1 + , (used2, c') <- usageCast c + , used' <- plusUsedMap used1 used2 + -> ( used' + , XCast (used', a) c' x1') + + XType a t + -> ( empty + , XType (empty, a) t) + + XWitness a w + | (used', w') <- usageWitness w + -> ( used' + , XWitness (used', a) w') + + +-- | Annotate binding occurences of named variables with usage information. +usageLets + :: Ord n + => Lets a n + -> (UsedMap n, Lets (UsedMap n, a) n) + +usageLets lts + = case lts of + LLet b x + | (used1', x') <- usageX' x + -> (used1', LLet b x') + + LRec bxs + | (bs, xs) <- unzip bxs + , (useds', xs') <- unzip $ map usageX' xs + , used' <- sumUsedMap useds' + -> (used', LRec $ zip bs xs') + + LPrivate b mt bs + -> (empty, LPrivate b mt bs) + + +-- | Annotate binding occurrences of named value variables with +-- usage information. +usageCast + :: Ord n + => Cast a n + -> (UsedMap n, Cast (UsedMap n, a) n) +usageCast cc + = case cc of + CastWeakenEffect eff + -> (empty, CastWeakenEffect eff) + + CastPurify w + | (used, w') <- usageWitness w + -> (used, CastPurify w') + + CastBox -> (empty, CastBox) + CastRun -> (empty, CastRun) + + +-- | Annotate binding occurrences of named level-0 variables with +-- usage information. +usageAlt + :: Ord n + => Alt a n + -> (UsedMap n, Alt (UsedMap n, a) n) + +usageAlt (AAlt p x) + = let (used, x') = usageX' x + in (used, AAlt p x') + + +-- | Annotate binding occurrences of named level-0 variables with +-- usage information. +usageWitness + :: Ord n + => Witness a n + -> (UsedMap n, Witness (UsedMap n, a) n) + +usageWitness ww + = case ww of + WVar a u + -> (empty, WVar (empty, a) u) + + WCon a c + -> (empty, WCon (empty, a) c) + + WApp a w1 w2 + | (used1, w1') <- usageWitness w1 + , (used2, w2') <- usageWitness w2 + , used' <- plusUsedMap used1 used2 + -> (empty, WApp (used', a) w1' w2') + + WType a t + -> (empty, WType (empty, a) t) diff --git a/DDC/Core/Simplifier.hs b/DDC/Core/Simplifier.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Simplifier.hs @@ -0,0 +1,21 @@ + +module DDC.Core.Simplifier + ( -- * Simplifier Specifications + Simplifier(..) + + -- * Transform Specifications + , Transform(..) + , InlinerTemplates + , NamedRewriteRules + + -- * Transform Results + , TransformResult(..) + , TransformInfo(..) + , resultDone + + -- * Application + , applySimplifier + , applySimplifierX) +where +import DDC.Core.Simplifier.Apply +import DDC.Core.Simplifier.Base diff --git a/DDC/Core/Simplifier/Apply.hs b/DDC/Core/Simplifier/Apply.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Simplifier/Apply.hs @@ -0,0 +1,322 @@ + +-- | Application of simplifiers to modules and expressions. +module DDC.Core.Simplifier.Apply + ( applySimplifier + , applyTransform + , applySimplifierX + , applyTransformX) +where +import DDC.Data.Pretty +import DDC.Core.Module +import DDC.Core.Exp +import DDC.Core.Fragment +import DDC.Core.Simplifier.Base +import DDC.Core.Transform.AnonymizeX +import DDC.Core.Transform.Beta +import DDC.Core.Transform.Bubble +import DDC.Core.Transform.Elaborate +import DDC.Core.Transform.Eta as Eta +import DDC.Core.Transform.Flatten +import DDC.Core.Transform.Forward as Forward +import DDC.Core.Transform.Inline +import DDC.Core.Transform.Namify +import DDC.Core.Transform.Prune +import DDC.Core.Transform.Rewrite +import qualified DDC.Core.Transform.Lambdas as Lambdas +import qualified DDC.Core.Transform.Snip as Snip +import qualified DDC.Core.Transform.FoldCase as FoldCase + +import DDC.Data.Name +import DDC.Type.Env (KindEnv, TypeEnv) +import Data.Typeable (Typeable) +import Control.Monad.State.Strict +import qualified DDC.Data.Pretty as P +import qualified DDC.Core.Env.EnvX as EnvX +import qualified Data.Set as Set +import Prelude hiding ((<$>)) + + +-- Modules -------------------------------------------------------------------- +-- | Apply a simplifier to a module. +-- +-- The state monad can be used by `Namifier` functions to generate fresh names. +-- +applySimplifier + :: (Show a, Pretty a, Ord n, Show n, Pretty n, CompoundName n) + => Profile n -- ^ Profile of language we're working in + -> KindEnv n -- ^ Kind environment + -> TypeEnv n -- ^ Type environment + -> Simplifier s a n -- ^ Simplifier to apply + -> Module a n -- ^ Module to simplify + -> State s (TransformResult (Module a n)) + +applySimplifier !profile !kenv !tenv !spec !mm + = let down = applySimplifier profile kenv tenv + in case spec of + Seq t1 t2 + -> do tm <- down t1 mm + tm' <- down t2 (result tm) + + let info = + case (resultInfo tm, resultInfo tm') of + (TransformInfo i1, TransformInfo i2) -> SeqInfo i1 i2 + + let again = resultAgain tm || resultAgain tm' + let progress = resultProgress tm || resultProgress tm' + + return TransformResult + { result = result tm' + , resultAgain = again + , resultProgress = progress + , resultInfo = TransformInfo info } + + Fix i s + -> do tm <- applyFixpoint profile kenv tenv i s mm + let info = + case resultInfo tm of + TransformInfo info1 -> FixInfo i info1 + + return TransformResult + { result = result tm + , resultAgain = resultAgain tm + , resultProgress = resultProgress tm + , resultInfo = TransformInfo info } + + Trans t1 + -> applyTransform profile kenv tenv t1 mm + + +-- | Apply a transform until it stops progressing, or a maximum number of times +applyFixpoint + :: (Show a, Pretty a, Ord n, Show n, Pretty n, CompoundName n) + => Profile n -- ^ Profile of language we're working in + -> KindEnv n -- ^ Kind environment + -> TypeEnv n -- ^ Type environment + -> Int -- ^ Maximum number of times to apply + -> Simplifier s a n -- ^ Transform to apply. + -> Module a n -- ^ Module to simplify. + -> State s (TransformResult (Module a n)) + +applyFixpoint !profile !kenv !tenv !i' !spec !mm' + = go i' mm' False + where + simp = applySimplifier profile kenv tenv spec + + go 0 mm progress + = do tm <- simp mm + return tm { resultProgress = progress } + + go i mm progress + = do tm <- simp mm + case resultAgain tm of + False + -> return tm { resultProgress = progress } + + True + -> do tm' <- go (i-1) (result tm) True + + let info + = case (resultInfo tm, resultInfo tm') of + (TransformInfo i1, TransformInfo i2) + -> SeqInfo i1 i2 + + return TransformResult + { result = result tm' + , resultAgain = resultProgress tm' + , resultProgress = resultProgress tm' + , resultInfo = TransformInfo info } + +-- | Apply a transform to a module. +applyTransform + :: (Show a, Pretty a, Ord n, Show n, Pretty n, CompoundName n) + => Profile n -- ^ Profile of language we're working in + -> KindEnv n -- ^ Kind environment + -> TypeEnv n -- ^ Type environment + -> Transform s a n -- ^ Transform to apply. + -> Module a n -- ^ Module to simplify. + -> State s (TransformResult (Module a n)) + +applyTransform !profile !_kenv !_tenv !spec !mm + = let res x = return $ resultDone (show $ ppr spec) x + in case spec of + Id -> res mm + Anonymize -> res $ anonymizeX mm + Beta config -> return $ betaReduce profile config mm + Bubble -> res $ bubbleModule mm + Elaborate -> res $ elaborateModule mm + Eta config -> return $ Eta.etaModule profile config mm + Flatten -> res $ flatten mm + + Forward + -> let config = Forward.Config (const FloatAllow) False + in return $ forwardModule profile config mm + + FoldCase config -> res $ FoldCase.foldCase config mm + Inline getDef -> res $ inline getDef Set.empty mm + + Lambdas + -> res + $ Lambdas.evalState "l" + $ Lambdas.lambdasModule profile mm + + Namify namK namT -> namifyUnique namK namT mm >>= res + Prune -> res $ pruneModule profile mm + Rewrite rules -> res $ rewriteModule rules mm + Snip config -> res $ Snip.snip config mm + + +-- Expressions ---------------------------------------------------------------- +-- | Apply a simplifier to an expression. +-- +-- The state monad can be used by `Namifier` functions to generate fresh names. +-- +applySimplifierX + :: (Show a, Pretty a, Show n, Ord n, Pretty n, CompoundName n) + => Profile n -- ^ Profile of language we're working in + -> KindEnv n -- ^ Kind environment + -> TypeEnv n -- ^ Type environment + -> Simplifier s a n -- ^ Simplifier to apply + -> Exp a n -- ^ Expression to simplify + -> State s (TransformResult (Exp a n)) + +applySimplifierX !profile !kenv !tenv !spec !xx + = let down = applySimplifierX profile kenv tenv + in case spec of + Seq t1 t2 + -> do tx <- down t1 xx + tx' <- down t2 (result tx) + + let info = + case (resultInfo tx, resultInfo tx') of + (TransformInfo i1, TransformInfo i2) -> SeqInfo i1 i2 + + let again = resultAgain tx || resultAgain tx' + let progress = resultProgress tx || resultProgress tx' + + return TransformResult + { result = result tx' + , resultAgain = again + , resultProgress = progress + , resultInfo = TransformInfo info } + + Fix i s + -> do tx <- applyFixpointX profile kenv tenv i s xx + let info = + case resultInfo tx of + TransformInfo info1 -> FixInfo i info1 + + return TransformResult + { result = result tx + , resultAgain = resultAgain tx + , resultProgress = resultProgress tx + , resultInfo = TransformInfo info } + + Trans t1 + -> applyTransformX profile kenv tenv t1 xx + + +-- | Apply a simplifier until it stops progressing, or a maximum number of times +applyFixpointX + :: (Show a, Pretty a, Show n, Ord n, Pretty n, CompoundName n) + => Profile n -- ^ Profile of language we're working in + -> KindEnv n -- ^ Kind environment + -> TypeEnv n -- ^ Type environment + -> Int -- ^ Maximum number of times to apply + -> Simplifier s a n -- ^ Simplifier to apply. + -> Exp a n -- ^ Exp to simplify. + -> State s (TransformResult (Exp a n)) + +applyFixpointX !profile !kenv !tenv !i' !s !xx' + = go i' xx' False + where + simp = applySimplifierX profile kenv tenv s + + go 0 xx progress + = do tx <- simp xx + return tx { resultProgress = progress } + + go i xx progress + = do tx <- simp xx + case resultAgain tx of + False + -> return tx { resultProgress = progress } + + True + -> do tx' <- go (i-1) (result tx) True + + let info + = case (resultInfo tx, resultInfo tx') of + (TransformInfo i1, TransformInfo i2) + -> SeqInfo i1 i2 + + return TransformResult + { result = result tx' + , resultAgain = resultProgress tx' + , resultProgress = resultProgress tx' + , resultInfo = TransformInfo info } + + +-- | Result of applying two simplifiers in sequence. +data SeqInfo + = forall i1 i2 + . (Typeable i1, Typeable i2, Pretty i1, Pretty i2) + => SeqInfo i1 i2 + deriving Typeable + + +instance Pretty SeqInfo where + ppr (SeqInfo i1 i2) = ppr i1 P.<> text ";" <$> ppr i2 + + +-- | Result of applying a simplifier until we reach a fixpoint. +data FixInfo + = forall i1 + . (Typeable i1, Pretty i1) + => FixInfo Int i1 + deriving Typeable + + +instance Pretty FixInfo where + ppr (FixInfo num i1) + = text "fix" <+> int num P.<> text ":" + <$> indent 4 (ppr i1) + + +-- | Apply a single transform to an expression. +applyTransformX + :: (Show a, Show n, Ord n, Pretty n) + => Profile n -- ^ Profile of language we're working in + -> KindEnv n -- ^ Kind environment + -> TypeEnv n -- ^ Type environment + -> Transform s a n -- ^ Transform to apply. + -> Exp a n -- ^ Exp to transform. + -> State s (TransformResult (Exp a n)) + +applyTransformX !profile !kenv !tenv !spec !xx + = let res x = return $ resultDone (show $ ppr spec) x + env = EnvX.fromPrimEnvs + (profilePrimKinds profile) + (profilePrimTypes profile) + (profilePrimDataDefs profile) + in case spec of + Id -> res xx + Anonymize -> res $ anonymizeX xx + Beta config -> return $ betaReduce profile config xx + Bubble -> res $ bubbleX kenv tenv xx + Elaborate{} -> res $ elaborateX xx + Eta config -> return $ Eta.etaX profile config env xx + Flatten -> res $ flatten xx + + Forward + -> let config = Forward.Config (const FloatAllow) False + in return $ forwardX profile config xx + + Inline getDef -> res $ inline getDef Set.empty xx + FoldCase config -> res $ FoldCase.foldCase config xx + Lambdas -> res $ xx + Namify namK namT -> namifyUnique namK namT xx >>= res + Prune -> return $ pruneX profile env xx + Rewrite rules -> return $ rewriteX rules xx + Snip config -> res $ Snip.snip config xx + + diff --git a/DDC/Core/Simplifier/Base.hs b/DDC/Core/Simplifier/Base.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Simplifier/Base.hs @@ -0,0 +1,153 @@ + +module DDC.Core.Simplifier.Base + ( -- * Simplifier Specifications + Simplifier(..) + + -- * Transform Specifications + , Transform(..) + , InlinerTemplates + , NamedRewriteRules + + -- * Transform Results + , TransformResult(..) + , TransformInfo(..) + , NoInformation + , resultDone) +where +import DDC.Core.Simplifier.Result +import DDC.Core.Transform.Rewrite.Rule +import DDC.Core.Transform.Namify +import DDC.Core.Exp +import DDC.Type.Env +import DDC.Data.Pretty +import qualified DDC.Core.Transform.Snip as Snip +import qualified DDC.Core.Transform.Eta as Eta +import qualified DDC.Core.Transform.Beta as Beta +import qualified DDC.Core.Transform.FoldCase as FoldCase + + +-- Simplifier ----------------------------------------------------------------- +-- | Specification of how to simplify a core program. +data Simplifier s a n + -- | Apply a single transform. + = Trans (Transform s a n) + + -- | Apply two simplifiers in sequence. + | Seq (Simplifier s a n) (Simplifier s a n) + + -- | Keep applying a transform until it reports that further + -- applications won't be helpful, bailing out after a maximum number + -- of applications. + | Fix Int (Simplifier s a n) + + +instance Monoid (Simplifier s a n) where + mempty = Trans Id + mappend = Seq + + +instance Pretty (Simplifier s a n) where + ppr ss + = case ss of + Seq s1 s2 + -> ppr s1 <+> text ";" <+> ppr s2 + + Fix i s + -> text "fix" <+> int i <+> ppr s + + Trans t1 + -> ppr t1 + + +-- Transform ------------------------------------------------------------------ +-- | Individual transforms to apply during simplification. +data Transform s a n + -- | The Identity transform returns the original program unharmed. + = Id + + -- | Rewrite named binders to anonymous deBruijn binders. + | Anonymize + + -- | Perform beta reduction when the argument is not a redex. + | Beta Beta.Config + + -- | Float casts outwards. + | Bubble + + -- | Elaborate possible Const and Distinct witnesses that aren't + -- otherwise in the program. + | Elaborate + + -- | Perform eta expansion and reduction. + | Eta Eta.Config + + -- | Flatten nested let and case expressions. + | Flatten + + -- | Float single-use bindings forward into their use sites. + | Forward + + -- | Fold case expressions. + | FoldCase FoldCase.Config + + -- | Inline definitions into their use sites. + | Inline + { -- | Get the unfolding for a named variable. + transInlineDef :: InlinerTemplates a n } + + -- | Perform lambda lifting. + | Lambdas + + -- | Rewrite anonymous binders to fresh named binders. + | Namify + { -- | Create a namifier to make fresh type (level-1) + -- names that don't conflict with any already in this + -- environment. + transMkNamifierT :: Env n -> Namifier s n + + -- | Create a namifier to make fresh value or witness (level-0) + -- names that don't conflict with any already in this + -- environment. + , transMkNamifierX :: Env n -> Namifier s n } + + -- | Remove unused, pure let bindings. + | Prune + + -- | Apply general rule-based rewrites. + | Rewrite + { -- | List of rewrite rules along with their names. + transRules :: NamedRewriteRules a n } + + -- | Introduce let-bindings for nested applications. + | Snip Snip.Config + + +-- | Function to get the inliner template (unfolding) for the given name. +type InlinerTemplates a n + = (n -> Maybe (Exp a n)) + +-- | Rewrite rules along with their names. +type NamedRewriteRules a n + = [(String, RewriteRule a n)] + + +instance Pretty (Transform s a n) where + ppr ss + = case ss of + Id -> text "Id" + Anonymize -> text "Anonymize" + Beta{} -> text "Beta" + Bubble -> text "Bubble" + Elaborate -> text "Elaborate" + Eta{} -> text "Eta" + Flatten -> text "Flatten" + Forward -> text "Forward" + FoldCase{} -> text "FoldCase" + Inline{} -> text "Inline" + Lambdas{} -> text "Lambdas" + Namify{} -> text "Namify" + Prune -> text "Prune" + Rewrite{} -> text "Rewrite" + Snip{} -> text "Snip" + + diff --git a/DDC/Core/Simplifier/Lexer.hs b/DDC/Core/Simplifier/Lexer.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Simplifier/Lexer.hs @@ -0,0 +1,84 @@ + +module DDC.Core.Simplifier.Lexer + ( Tok(..) + , lexSimplifier) +where +import DDC.Data.SourcePos +import Data.Char + + +lexSimplifier + :: (String -> Maybe n) -- ^ Function to read a name. + -> String -- ^ String to parse. + -> [Located (Tok n)] + +lexSimplifier readName str + = map (\t -> Located (SourcePos "" 0 0) t) + $ lexer readName str + + +-- Lexer ---------------------------------------------------------------------- +-- | Lex a transform specification. +lexer :: (String -> Maybe n) -- ^ Function to read a name. + -> String -- ^ String to parse. + -> [Tok n] + +lexer readName ss + = let down = lexer readName + in case ss of + [] -> [] + + (';' : cs) -> KSemiColon : down cs + (',' : cs) -> KComma : down cs + ('-' : cs) -> KMinus : down cs + ('+' : cs) -> KPlus : down cs + ('{' : cs) -> KBraceBra : down cs + ('}' : cs) -> KBraceKet : down cs + ('[' : cs) -> KSquareBra : down cs + (']' : cs) -> KSquareKet : down cs + + 'f' : 'i' : 'x' : s : cs + | isSpace s -> KFix : down cs + + (c : cs) + | isSpace c + -> down cs + + (c : cs) + | isUpper c + , (body, rest) <- span isAlpha cs + -> KCon (c : body) : down rest + + (c : cs) + | isLower c + , (body, rest) <- span isAlpha cs + , Just n <- readName (c : body) + -> KVar n : down rest + + (c : cs) + | isDigit c + , (digits, rest) <- span isDigit cs + -> KInt (read (c:digits)) : down rest + + _ -> [KJunk ss] + + +-- | Tokens for transform specification. +data Tok n + = KEnd + | KJunk String + | KCon String + | KVar n + | KInt Int + + | KFix + + | KSemiColon + | KComma + | KMinus + | KPlus + | KBraceBra + | KBraceKet + | KSquareBra + | KSquareKet + deriving (Eq, Show) diff --git a/DDC/Core/Simplifier/Parser.hs b/DDC/Core/Simplifier/Parser.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Simplifier/Parser.hs @@ -0,0 +1,235 @@ + +module DDC.Core.Simplifier.Parser + ( SimplifierDetails (..) + , parseSimplifier) +where +import DDC.Core.Transform.Namify +import DDC.Core.Transform.Inline +import DDC.Core.Simplifier.Base +import DDC.Core.Module +import DDC.Type.Env +import DDC.Core.Simplifier.Lexer +import DDC.Data.SourcePos +import DDC.Control.Parser (pTok) +import Data.Set (Set) +import qualified DDC.Core.Transform.Snip as Snip +import qualified DDC.Core.Transform.Beta as Beta +import qualified DDC.Core.Transform.Eta as Eta +import qualified DDC.Core.Transform.FoldCase as FoldCase +import qualified DDC.Control.Parser as P +import qualified Data.Map as Map +import qualified Data.Set as Set + + +--------------------------------------------------------------------------------------------------- +-- | Auxilliary information that may be used by a simplifier. +data SimplifierDetails s a n + = SimplifierDetails + { -- | Create a namifier to make fresh type (level-1) + -- names that don't conflict with any already in this environment. + simplifierMkNamifierT :: Env n -> Namifier s n + + -- | Create a namifier to make fresh value or witness (level-0) + -- names that don't conflict with any already in this environment. + , simplifierMkNamifierX :: Env n -> Namifier s n + + -- | Rewrite rules along with their names. + , simplifierRules :: NamedRewriteRules a n + + -- | Modules available for inlining. + , simplifierTemplates :: [Module a n] } + + +--------------------------------------------------------------------------------------------------- +-- | A parser of simplifier specifications. +type Parser n a + = P.Parser (Tok n) a + +-- | Parse a simplifier from a string. +parseSimplifier + :: (Ord n, Show n) + => (String -> Maybe n) -- Function to read a name. + -> SimplifierDetails s a n + -> String + -> Either P.ParseError (Simplifier s a n) + +parseSimplifier readName details str + = let kend = Located (SourcePos "" 0 0) KEnd + toks = lexSimplifier readName str ++ [kend] + in P.runTokenParser show "" + (pSimplifier details) + toks + + +-- | Parse a simplifier. +pSimplifier + :: (Ord n, Show n) + => SimplifierDetails s a n + -> Parser n (Simplifier s a n) + +pSimplifier details + = do simpl <- pSimplifierSeq details + pTok KEnd + return simpl + + +-- | Parse a simplifier sequence. +pSimplifierSeq + :: (Ord n, Show n) + => SimplifierDetails s a n + -> Parser n (Simplifier s a n) + +pSimplifierSeq details + = P.choice + [ do -- Single Transform or Sequence. + simpl0 <- pSimplifier0 details + + P.choice + [ do pTok KSemiColon + simpl1 <- pSimplifierSeq details + return $ Seq simpl0 simpl1 + + , do return simpl0 ] + ] + + +pSimplifier0 + :: (Ord n, Show n) + => SimplifierDetails s a n + -> Parser n (Simplifier s a n) + +pSimplifier0 details + = P.choice + [ -- Fixpoint transform. + -- fix INT SIMP + do pTok KFix + maxIters <- pInt + simp <- pSimplifier0 details + return $ Fix maxIters simp + + , do -- Atomic transform. + trans <- pTransform details + return $ Trans trans + + , do -- Simplifier in braces + -- { SIMP } + pTok KBraceBra + simpl <- pSimplifierSeq details + pTok KBraceKet + return simpl + ] + + +-- | Parse a single transform. +pTransform + :: (Ord n, Show n) + => SimplifierDetails s a n + -> Parser n (Transform s a n) + +pTransform details + = P.choice + [ -- Single transforms with no parameters. + do trans <- P.pTokMaybe readTransformAtomic + return trans + + -- Namifier + , do pTok (KCon "Namify") + return $ Namify (simplifierMkNamifierT details) + (simplifierMkNamifierX details) + + -- Rewrite + , do pTok (KCon "Rewrite") + return $ Rewrite (simplifierRules details) + + -- Inline + , do pTok (KCon "Inline") + let modules = simplifierTemplates details + specs <- P.many pInlinerSpec + let specsMap = Map.fromList specs + return $ Inline (lookupTemplateFromModules specsMap modules) ] + + +-- | Parse an inlining specification. +pInlinerSpec + :: Ord n + => Parser n (ModuleName, InlineSpec n) + +pInlinerSpec + = P.choice + [ do modname <- pModuleName + P.choice + [ pInlinerSpecIncludeList modname + , pInlinerSpecExcludeList modname + , return (modname, InlineSpecAll modname (Set.empty :: Set n)) ] + ] + +-- Inline all bindings in a module, except particulars. +-- Inline MODULENAME +[VAR1, VAR2, ... VARn] +-- Inline MODULENAME [VAR1, VAR2, ... VARn] +pInlinerSpecIncludeList modname + = do P.choice [ pTok KPlus, return () ] + pTok KSquareBra + ns <- P.sepEndBy pVar (pTok KComma) + pTok KSquareKet + return $ (modname, InlineSpecNone modname (Set.fromList ns)) + + +-- Inline no bindings in a module by default, +-- but include some particulars. +-- Inline MODULENAME -[VAR1, VAR2, ... VARn] +pInlinerSpecExcludeList modname + = do pTok KMinus + pTok KSquareBra + ns <- P.sepEndBy pVar (pTok KComma) + pTok KSquareKet + return $ (modname, InlineSpecAll modname (Set.fromList ns)) + + +-- | Read an atomic transform name. +readTransformAtomic :: Tok n -> Maybe (Transform s a n) +readTransformAtomic kk + | KCon name <- kk + = case name of + "Id" -> Just Id + "Anonymize" -> Just Anonymize + "Beta" -> Just (Beta Beta.configZero) + "BetaLets" -> Just (Beta Beta.configZero { Beta.configBindRedexes = True }) + "Bubble" -> Just Bubble + "Elaborate" -> Just Elaborate + "Eta" -> Just (Eta Eta.configZero { Eta.configExpand = True }) + "Flatten" -> Just Flatten + "Forward" -> Just Forward + "FoldCase" -> Just (FoldCase FoldCase.configZero + { FoldCase.configCaseOfConstructor = True + , FoldCase.configCaseOfCase = True }) + "Lambdas" -> Just Lambdas + "Prune" -> Just Prune + "Snip" -> Just (Snip Snip.configZero) + "SnipOver" -> Just (Snip Snip.configZero { Snip.configSnipOverApplied = True }) + "SnipBody" -> Just (Snip Snip.configZero { Snip.configSnipLetBody = True }) + _ -> Nothing + + | otherwise + = Nothing + + +-- | Parse a variable name +pVar :: Parser n n +pVar = P.pTokMaybe f + where f (KVar n) = Just n + f _ = Nothing + + +-- | Parse an integer. +pInt :: Parser n Int +pInt = P.pTokMaybe f + where f (KInt i) = Just i + f _ = Nothing + + +-- | Parse a module name. +pModuleName :: Parser n ModuleName +pModuleName = P.pTokMaybe f + where f (KCon n) = Just $ ModuleName [n] + f _ = Nothing + diff --git a/DDC/Core/Simplifier/Recipe.hs b/DDC/Core/Simplifier/Recipe.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Simplifier/Recipe.hs @@ -0,0 +1,118 @@ + +-- | Common simplifier recipes that combine multiple transforms. +module DDC.Core.Simplifier.Recipe + ( -- * Atomic recipies + idsimp + , anonymize + , beta + , betaLets + , bubble + , elaborate + , flatten + , forward + , lambdas + , snip + , snipOver + , prune + + -- * Compound recipies + , anormalize + , rewriteSimp) +where +import DDC.Core.Simplifier.Base +import DDC.Core.Transform.Namify +import qualified DDC.Core.Transform.Snip as Snip +import qualified DDC.Core.Transform.Beta as Beta +import DDC.Type.Env +import Data.Monoid + + +-- Atomic --------------------------------------------------------------------- +-- These are short names for single transforms. + +-- | The identity simplifier returns the code unharmed. +idsimp :: Simplifier s a n +idsimp = Trans Id + + +-- | Rewrite named binders to anonymous debruijn binders. +anonymize :: Simplifier s a n +anonymize = Trans Anonymize + + +-- | Perform beta reduction +beta :: Simplifier s a n +beta = Trans (Beta Beta.configZero) + + +-- | Perform beta reduction, introducing let-expressions for compound arguments. +betaLets :: Simplifier s a n +betaLets = Trans (Beta Beta.configZero { Beta.configBindRedexes = True }) + + +-- | Float casts outwards. +bubble :: Simplifier s a n +bubble = Trans Bubble + + +-- | Elaborate possible Const and Distinct witnesses that aren't +-- otherwise in the program. +elaborate :: Simplifier s a n +elaborate = Trans Elaborate + + +-- | Flatten nested let and case expressions. +flatten :: Simplifier s a n +flatten = Trans Flatten + + +-- | Float single-use bindings forward into their use sites. +forward :: Simplifier s a n +forward = Trans Forward + + +-- | Lift out nested lambda expressions to top-level. +lambdas :: Simplifier s a n +lambdas = Trans Lambdas + + +-- | Remove unused, pure let bindings. +prune :: Simplifier s a n +prune = Trans Prune + + +-- | Introduce let-bindings for nested applications. +snip :: Simplifier s a n +snip = Trans (Snip Snip.configZero) + + +-- | Introduce let-bindings for nested applications. +snipOver :: Simplifier s a n +snipOver = Trans (Snip Snip.configZero { Snip.configSnipOverApplied = True }) + + +-- Compound ------------------------------------------------------------------- +-- | Conversion to administrative normal-form. +anormalize + :: (KindEnv n -> Namifier s n) + -- ^ Make a namifier to create fresh level-1 names. + -> (TypeEnv n -> Namifier s n) + -- ^ Make a namifier to create fresh level-0 names. + -> Simplifier s a n + +anormalize namK namT + = snip + <> Trans Flatten + <> Trans (Namify namK namT) + + +-- | Intersperse rewrites and beta reduction +rewriteSimp + :: Int -- ^ Maximum number of iterations. + -> NamedRewriteRules a n -- ^ Rewrite rules to apply. + -> Simplifier s a n + +rewriteSimp maxIters rules + = let rewrite = Trans $ Rewrite rules + in Fix maxIters (rewrite <> bubble <> betaLets) + diff --git a/DDC/Core/Simplifier/Result.hs b/DDC/Core/Simplifier/Result.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Simplifier/Result.hs @@ -0,0 +1,70 @@ + +module DDC.Core.Simplifier.Result + ( TransformResult (..) + , TransformInfo (..) + , NoInformation + , resultDone) +where +import DDC.Data.Pretty +import Data.Typeable +import qualified DDC.Data.Pretty as P + + +-- TransformResult ------------------------------------------------------------ +-- | Package up the result of applying a single transform. +data TransformResult r + = TransformResult + { -- | Transform result proper (eg the new module) + result :: r + + -- | Whether this transform made any progess. + -- + -- If `False` then the result program must be the same as the + -- input program, and a simplifer fixpoint won't apply this + -- transform again to the result program. + , resultProgress :: Bool + + -- | Whether it might help to run the same transform again. + -- + -- If `False` then a simplifier fixpoint won't apply this transform + -- again to the result program. + , resultAgain :: Bool + + -- | Transform specific log. This might contain a count of what rules + -- fired, or information about what parts of the program couldn't + -- be processed. + , resultInfo :: TransformInfo } + + +-- | Existential package for a typeable thing, +-- used in `TransformResult`. +data TransformInfo + = forall i + . (Typeable i, Pretty i) + => TransformInfo i + + +-- | Place-holder type to use when there is no real `TransformResult`. +data NoInformation + = NoInformation String + deriving Typeable + + +instance Pretty NoInformation where + ppr (NoInformation name) = text name P.<> text ": No information" + + +instance Pretty (TransformResult r) where + ppr (TransformResult _ _ _ (TransformInfo i)) + = ppr i + + +-- | Create a default result with no transform again. +-- +-- We'll say we made progress, but set `resultAgain` to False +-- so to stop any simplifier fixpoints. +resultDone :: String -> r -> TransformResult r +resultDone name r + = TransformResult r True False + $ TransformInfo + $ NoInformation name diff --git a/DDC/Core/Transform/ANormal.hs b/DDC/Core/Transform/ANormal.hs deleted file mode 100644 --- a/DDC/Core/Transform/ANormal.hs +++ /dev/null @@ -1,253 +0,0 @@ - -module DDC.Core.Transform.ANormal - (anormalise) -where -import DDC.Core.Exp -import qualified DDC.Type.Exp as T -import qualified DDC.Type.Compounds as T -import qualified DDC.Core.Transform.AnonymizeX as A -import qualified DDC.Core.Transform.LiftX as L - -import qualified Data.Map as Map - --- **** Recording arities of known values --- So we can try to create apps to fully apply - --- | Arities of known bound variables. --- We need to track everything even if it's not a function to keep indices correct. --- Just use zero for unknown/irrelevant -type Arities n = (Map.Map n Int, [Int]) - --- | Empty arities context -arEmpty :: Ord n => Arities n -arEmpty = (Map.empty, []) - --- | Extend map with multiple bindings and their arities -arExtends :: Ord n => Arities n -> [(Bind n, Int)] -> Arities n -arExtends arity exts = foldl go arity exts - where go (named,anon) (BNone _t, _) = (named,anon) - go (named,anon) (BAnon _t, a) = (named, a:anon) - go (named,anon) (BName n _t, a) = (Map.insert n a named, anon) - --- | Look up a binder's arity -arGet :: Ord n => Arities n -> Bound n -> Int -arGet (_named, anon) (UIx ix _) = anon !! ix -arGet (named, _anon) (UName n _) = named Map.! n --- Get a primitive's arity from its type -arGet (_named,_anon) (UPrim _ t) = arityOfType t - --- **** Finding arities of expressions etc - --- | Count all the arrows and foralls, ignoring any effects --- We can be sure that primitives don't effect until they're fully applied -arityOfType :: Ord n => Type n -> Int -arityOfType (T.TForall _ t) - = 1 + arityOfType t -arityOfType t - = let (args, _) = T.takeTFunArgResult t in - length args - --- | Find arity of an expression. Count lambdas, use type for primitives -arityOfExp :: Ord n => Exp a n -> Int --- Counting all binders, because they all correspond to XApps. -arityOfExp (XLam _ _ e) - = 1 + arityOfExp e -arityOfExp (XLAM _ _ e) - = 1 + arityOfExp e --- Find primitive's constructor's arities from type, --- we might need to do this for user defined constructors too. -arityOfExp (XCon _ (UPrim _ t)) - = arityOfType t --- Anything else we'll need to apply one at a time -arityOfExp _ - = 0 - --- | Retrieve binders from case pattern, so we can extend the arity context. --- We don't know anything about their values, so record as 0. -aritiesOfPat :: Ord n => Pat n -> [(Bind n, Int)] -aritiesOfPat PDefault = [] -aritiesOfPat (PData _b bs) = zip bs (repeat 0) - - --- **** Actually converting to a-normal form - --- | Recursively transform expression into a-normal -anormal :: Ord n - => Arities n -- ^ environment, arities of bound variables - -> Exp a n -- ^ expression to transform - -> [(Exp a n,a)]-- ^ arguments being applied to current expression - -> Exp a n - --- Application: just record argument and descend into function -anormal ar (XApp a lhs rhs) args - = -- normalise rhs and add to arguments - let args' = (anormal ar rhs [], a) : args in - -- descend into lhs, remembering all args - anormal ar lhs args' - --- Anything other than application: if we're applied to arguments add bindings, --- otherwise just recurse. -anormal ar x args - = let x' = go x in - case args of - -- if there are no args, we're done - [] -> x' - -- there are arguments. we must apply them. - _ -> flattenLets $ makeLets ar x' args - where - -- helper for descent - down ars e = anormal (arExtends ar ars) e [] - - -- we know x isn't an app. - go (XApp{}) = error "DDC.Core.Transform.ANormal.anormal: impossible XApp!" - - -- leafy ones - go (XVar{}) = x - go (XCon{}) = x - go (XType{}) = x - go (XWitness{}) = x - - -- lambdas - go (XLAM a b e) = - XLAM a b (down [(b,0)] e) - go (XLam a b e) = - XLam a b (down [(b,0)] e) - - -- non-recursive let - go (XLet a (LLet m b le) re) = - let le' = down [] le in - let re' = down [(b, arityOfExp le')] re in - XLet a (LLet m b le') re' - - -- recursive let - go (XLet a (LRec lets) re) = - let bs = map fst lets in - let es = map snd lets in - let ars= zip bs (map arityOfExp es) in - let es'= map (down ars) es in - let re'= down ars re in - XLet a (LRec $ zip bs es') re' - - -- letregion, just make sure we record bindings with dummy val - go (XLet a (LLetRegion b bs) re) = - let ars = zip bs (repeat 0) in - XLet a (LLetRegion b bs) (down ars re) - - -- withregion: I don't think this should ever show up. - go (XLet a (LWithRegion b) re) = - XLet a (LWithRegion b) (down [] re) - - -- case - go (XCase a e alts) = - let e' = down [] e in - let alts' = map (\(AAlt pat ae) -> AAlt pat (down (aritiesOfPat pat) ae)) alts in - XCase a e' alts' - - -- cast - go (XCast a c e) = - XCast a c (down [] e) - - --- | Convert an expression into a-normal form -anormalise :: Ord n => Exp a n -> Exp a n -anormalise x = anormal arEmpty x [] - --- | Check if an expression needs a binding, or if it's simple enough to be applied as-is -isNormal :: Ord n => Exp a n -> Bool --- Trivial expressions -isNormal (XVar{}) = True -isNormal (XCon{}) = True -isNormal (XType{}) = True -isNormal (XWitness{}) = True --- Casts are ignored by code generator, so we can leave them in if their subexpression is normal -isNormal (XCast _ _ x) = isNormal x -isNormal _ = False - --- | Create lets for any non-trivial arguments -makeLets :: Ord n - => Arities n -- ^ environment, arities of bound variables - -> Exp a n -- ^ function - -> [(Exp a n,a)]-- ^ arguments being applied to current expression - -> Exp a n -makeLets _ f0 [] = f0 -makeLets ar f0 args@((_,annot):_) = go 0 (findArity f0) ((f0,annot):args) [] - where - tBot = T.tBot T.kData - - -- out of arguments, create XApps out of leftovers - go i _arf [] acc = mkApps i 0 acc - -- f is fully applied and we have arguments left to add: - -- create let for intermediate result - go i arf ((x,a):xs) acc | length acc > arf - = XLet a (LLet LetStrict (BAnon tBot) (mkApps i 0 acc)) - (go i 1 ((x,a):xs) [(XVar a $ UIx 0 tBot,a)]) - -- application to variable, don't bother binding - go i arf ((x,a):xs) acc | isNormal x - = go i arf xs ((x,a):acc) - -- non-trivial argument, create binding - go i arf ((x,a):xs) acc - = XLet a (LLet LetStrict (BAnon tBot) (L.liftX i x)) - (go (i+1) arf xs ((x,a):acc)) - - -- fold list into applications - -- can't create empty app - mkApps _ _ [] - = error "DDC.Core.Transform.ANormal.makeLets.mkApps: impossible empty list" - - -- single element - this is the function - mkApps l _ [(x,_)] | isNormal x - = L.liftX l x - mkApps _ i [(_,a)] - = XVar a $ UIx i tBot - - -- apply this argument and recurse - mkApps l i ((x,a):xs) | isNormal x - = XApp a (mkApps l i xs) (L.liftX l x) - mkApps l i ((_,a):xs) - = XApp a (mkApps l (i+1) xs) (XVar a $ UIx i tBot) - - findArity (XVar _ b) = max (arGet ar b) 1 - findArity x = max (arityOfExp x) 1 - --- | Perform let-floating on strict non-recursive lets --- Only does the top level, to clean up the ones directly produced by makeLets. --- let b1 = (let b2 = def2 in x2) --- in x1 --- ==> --- let b2 = def2 --- in let b1 = x2 --- in x1 -flattenLets :: Ord n - => Exp a n - -> Exp a n - --- We only do this if b2 is anonymous (ones generated by makeLets are). --- If we tried to wrap x1 in b2 when b2's name is already used, --- we'd be in trouble. -flattenLets - (XLet a1 - (LLet LetStrict b1 - (XLet a2 (LLet LetStrict b2@(BAnon _) def2) x2)) - x1) - = -- If b1 is anon, we don't want to lift references to it - let liftDepth = case b1 of { BAnon _ -> 1; _ -> 0 } in - let x1' = L.liftAtDepthX 1 liftDepth x1 in - XLet a2 (LLet LetStrict b2 def2) $ - flattenLets $ XLet a1 (LLet LetStrict b1 x2) x1' - --- Same as above but b2 isn't anonymous - anonymize inner let & re-flatten. -flattenLets - (XLet a1 - (LLet LetStrict b1 inner@(XLet _ (LLet LetStrict _ _) _)) - x1) - = flattenLets $ - XLet a1 - (LLet LetStrict b1 (A.anonymizeX inner)) - x1 - --- Any let, its bound expression doesn't contain a strict non-recursive let so just flatten the body -flattenLets (XLet a1 llet1 x1) - = XLet a1 llet1 (flattenLets x1) - --- Anything else we can ignore. We don't need to recurse, because this is always called immediately after makeLets. -flattenLets x = x diff --git a/DDC/Core/Transform/AnonymizeX.hs b/DDC/Core/Transform/AnonymizeX.hs --- a/DDC/Core/Transform/AnonymizeX.hs +++ b/DDC/Core/Transform/AnonymizeX.hs @@ -1,19 +1,23 @@ +-- | Rewrite all binders to anonymous deBruijn form. module DDC.Core.Transform.AnonymizeX ( anonymizeX - , AnonymizeX(..)) + , AnonymizeX(..) + , pushAnonymizeBindX) where +import DDC.Core.Module import DDC.Core.Exp import DDC.Type.Transform.AnonymizeT -import DDC.Type.Compounds -import Control.Monad +import DDC.Type.Exp.Simple import Data.List +import Data.Set (Set) +import qualified Data.Set as Set --- | Rewrite all binders in a thing to be of anonymous form. +-- | Rewrite all binders in a thing to anonymous form. anonymizeX :: (Ord n, AnonymizeX c) => c n -> c n anonymizeX xx - = anonymizeWithX [] [] xx + = anonymizeWithX Set.empty [] [] xx ------------------------------------------------------------------------------- @@ -23,153 +27,175 @@ -- The stacks contains existing anonymous binders that we have entered into, -- and named binders that we have rewritten. All bound occurrences of variables -- will be replaced by references into these stacks. - anonymizeWithX - :: forall n. Ord n - => [Bind n] -- ^ Stack for Spec binders (level-1). + anonymizeWithX + :: forall n. Ord n + => Set n -- ^ Don't anonymize level-0 binders with these names. + -> [Bind n] -- ^ Stack for Spec binders (level-1). -> [Bind n] -- ^ Stack for Data and Witness binders (level-0). -> c n -> c n +instance AnonymizeX (Module a) where + anonymizeWithX keep kstack tstack mm@ModuleCore{} + = let + -- We need to keep exported names, + -- because the export list can't deal with anonymous binders. + keep' = Set.union keep + $ Set.fromList + $ map fst $ moduleExportTypes mm + x' = anonymizeWithX keep' kstack tstack (moduleBody mm) + + in mm { moduleBody = x' } + + instance AnonymizeX (Exp a) where - anonymizeWithX kstack tstack xx - = let down = anonymizeWithX kstack tstack + anonymizeWithX keep kstack tstack xx + = {-# SCC anonymizeWithX #-} + let down = anonymizeWithX keep kstack tstack in case xx of - XVar a u -> XVar a (down u) - XCon a u -> XCon a (down u) + XVar _ UPrim{} -> xx + XCon{} -> xx + + XVar a u@(UName{}) + | Just ix <- findIndex (boundMatchesBind u) tstack + -> XVar a (UIx ix) + + XVar a u + -> XVar a u + XApp a x1 x2 -> XApp a (down x1) (down x2) XLAM a b x -> let (kstack', b') = pushAnonymizeBindT kstack b - in XLAM a b' (anonymizeWithX kstack' tstack x) + in XLAM a b' (anonymizeWithX keep kstack' tstack x) XLam a b x - -> let (tstack', b') = pushAnonymizeBindX kstack tstack b - in XLam a b' (anonymizeWithX kstack tstack' x) + -> let (tstack', b') = pushAnonymizeBindX keep kstack tstack b + in XLam a b' (anonymizeWithX keep kstack tstack' x) XLet a lts x - -> let (kstack', tstack', lts') - = pushAnonymizeLets kstack tstack lts - in XLet a lts' (anonymizeWithX kstack' tstack' x) + -> let (kstack', tstack', lts') + = pushAnonymizeLets keep kstack tstack lts + in XLet a lts' (anonymizeWithX keep kstack' tstack' x) - XCase a x alts -> XCase a (down x) (map down alts) - XCast a c x -> XCast a (down c) (down x) - XType t -> XType (anonymizeWithT kstack t) - XWitness w -> XWitness (down w) + XCase a x alts -> XCase a (down x) (map down alts) + XCast a c x -> XCast a (down c) (down x) + XType a t -> XType a (anonymizeWithT kstack t) + XWitness a w -> XWitness a (down w) -instance AnonymizeX Cast where - anonymizeWithX kstack tstack cc - = case cc of +instance AnonymizeX (Cast a) where + anonymizeWithX keep kstack tstack cc + = let down = anonymizeWithX keep kstack tstack + in case cc of CastWeakenEffect eff -> CastWeakenEffect (anonymizeWithT kstack eff) - CastWeakenClosure clo -> CastWeakenClosure (anonymizeWithT kstack clo) - CastPurify w -> CastPurify (anonymizeWithX kstack tstack w) - CastForget w -> CastForget (anonymizeWithX kstack tstack w) - - -instance AnonymizeX LetMode where - anonymizeWithX kstack tstack lm - = case lm of - LetStrict -> lm - LetLazy mw -> LetLazy $ liftM (anonymizeWithX kstack tstack) mw + CastPurify w -> CastPurify (down w) + CastBox -> CastBox + CastRun -> CastRun instance AnonymizeX (Alt a) where - anonymizeWithX kstack tstack alt - = case alt of + anonymizeWithX keep kstack tstack alt + = let down = anonymizeWithX keep kstack tstack + in case alt of AAlt PDefault x - -> AAlt PDefault (anonymizeWithX kstack tstack x) + -> AAlt PDefault (down x) AAlt (PData uCon bs) x - -> let (tstack', bs') = pushAnonymizeBindXs kstack tstack bs - x' = anonymizeWithX kstack tstack' x + -> let (tstack', bs') = pushAnonymizeBindXs keep kstack tstack bs + x' = anonymizeWithX keep kstack tstack' x in AAlt (PData uCon bs') x' -instance AnonymizeX Witness where - anonymizeWithX kstack tstack ww - = let down = anonymizeWithX kstack tstack +instance AnonymizeX (Witness a) where + anonymizeWithX keep kstack tstack ww + = let down = anonymizeWithX keep kstack tstack in case ww of - WVar u -> WVar (down u) - WCon c -> WCon c - WApp w1 w2 -> WApp (down w1) (down w2) - WJoin w1 w2 -> WJoin (down w1) (down w2) - WType t -> WType (anonymizeWithT kstack t) + WVar a u@(UName _) + | Just ix <- findIndex (boundMatchesBind u) tstack + -> WVar a (UIx ix) + WVar a u -> WVar a u + WCon a c -> WCon a c + WApp a w1 w2 -> WApp a (down w1) (down w2) + WType a t -> WType a (anonymizeWithT kstack t) + instance AnonymizeX Bind where - anonymizeWithX kstack _tstack bb + anonymizeWithX _keep kstack _tstack bb = let t' = anonymizeWithT kstack $ typeOfBind bb - in replaceTypeOfBind t' bb - - -instance AnonymizeX Bound where - anonymizeWithX kstack tstack bb - = case bb of - UName _ t - | Just ix <- findIndex (boundMatchesBind bb) tstack - -> UIx ix (anonymizeWithT kstack t) - - _ -> bb + in replaceTypeOfBind t' bb -- Push ---------------------------------------------------------------------- --- Push a binding occurrence of a type variable on the stack, --- returning the anonyized binding occurrence and the new stack. -pushAnonymizeBindX - :: Ord n - => [Bind n] -- ^ Stack for Spec binders (kind environment) - -> [Bind n] -- ^ Stack for Value and Witness binders (type environment) - -> Bind n +-- | Push a binding occurrence of a level-0 on the stack, +-- returning the anonyized binding occurrence and the new stack. +pushAnonymizeBindX + :: Ord n + => Set n -- ^ Don't anonymize binders with these names. + -> [Bind n] -- ^ Stack for Spec binders (level-1) + -> [Bind n] -- ^ Stack for Value and Witness binders (level-0) + -> Bind n -> ([Bind n], Bind n) -pushAnonymizeBindX kstack tstack b - = let b' = anonymizeWithX kstack tstack b +pushAnonymizeBindX keep kstack tstack b@(BName n _) + | Set.member n keep + = let b' = anonymizeWithX keep kstack tstack b + in (tstack, b') + +pushAnonymizeBindX keep kstack tstack b@BNone{} + = let b' = anonymizeWithX keep kstack tstack b t' = typeOfBind b' + in (tstack, BNone t') + +pushAnonymizeBindX keep kstack tstack b + = let b' = anonymizeWithX keep kstack tstack b + t' = typeOfBind b' tstack' = b' : tstack in (tstack', BAnon t') --- Push a binding occurrence on the stack, --- returning the anonyized binding occurrence and the new stack. --- Used in the definition of `anonymize`. -pushAnonymizeBindXs - :: Ord n - => [Bind n] -- ^ Stack for Spec binders (kind environment) - -> [Bind n] -- ^ Stack for Value and Witness binders (type environment) - -> [Bind n] +-- | Push a binding occurrence on the stack, +-- returning the anonyized binding occurrence and the new stack. +-- Used in the definition of `anonymize`. +pushAnonymizeBindXs + :: Ord n + => Set n -- ^ Don't anonymize binders with these names. + -> [Bind n] -- ^ Stack for Spec binders (level-1) + -> [Bind n] -- ^ Stack for Value and Witness binders (level-0) + -> [Bind n] -> ([Bind n], [Bind n]) -pushAnonymizeBindXs kstack tstack bs - = mapAccumL (\tstack' b -> pushAnonymizeBindX kstack tstack' b) - tstack bs +pushAnonymizeBindXs keep kstack tstack bs + = mapAccumL + (\tstack' b -> pushAnonymizeBindX keep kstack tstack' b) + tstack bs -pushAnonymizeLets - :: Ord n - => [Bind n] -> [Bind n] - -> Lets a n +pushAnonymizeLets + :: Ord n + => Set n + -> [Bind n] + -> [Bind n] + -> Lets a n -> ([Bind n], [Bind n], Lets a n) -pushAnonymizeLets kstack tstack lts +pushAnonymizeLets keep kstack tstack lts = case lts of - LLet mode b x - -> let mode' = anonymizeWithX kstack tstack mode - x' = anonymizeWithX kstack tstack x - (tstack', b') = pushAnonymizeBindX kstack tstack b - in (kstack, tstack', LLet mode' b' x') + LLet b x + -> let x' = anonymizeWithX keep kstack tstack x + (tstack', b') = pushAnonymizeBindX keep kstack tstack b + in (kstack, tstack', LLet b' x') - LRec bxs + LRec bxs -> let (bs, xs) = unzip bxs - (tstack', bs') = pushAnonymizeBindXs kstack tstack bs - xs' = map (anonymizeWithX kstack tstack') xs + (tstack', bs') = pushAnonymizeBindXs keep kstack tstack bs + xs' = map (anonymizeWithX keep kstack tstack') xs bxs' = zip bs' xs' in (kstack, tstack', LRec bxs') - LLetRegion b bs - -> let (kstack', b') = pushAnonymizeBindT kstack b - (tstack', bs') = pushAnonymizeBindXs kstack' tstack bs - in (kstack', tstack', LLetRegion b' bs') - - LWithRegion{} - -> (kstack, tstack, lts) + LPrivate b mt bs + -> let (kstack', b') = mapAccumL pushAnonymizeBindT kstack b + (tstack', bs') = pushAnonymizeBindXs keep kstack' tstack bs + in (kstack', tstack', LPrivate b' mt bs') diff --git a/DDC/Core/Transform/Beta.hs b/DDC/Core/Transform/Beta.hs --- a/DDC/Core/Transform/Beta.hs +++ b/DDC/Core/Transform/Beta.hs @@ -1,40 +1,174 @@ +-- | Beta-reduce applications of a explicit lambda abstractions +-- to variables and values. module DDC.Core.Transform.Beta - (betaReduce) + ( Config (..) + , configZero + , Info (..) + , betaReduce) where -import DDC.Core.Exp -import DDC.Core.Transform.TransformX +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.Type.Env (Env) -import qualified DDC.Type.Env as Env +import DDC.Core.Simplifier.Result +import DDC.Data.Pretty +import DDC.Core.Env.EnvX (EnvX) +import Control.Monad.Writer (Writer, runWriter, tell) +import Data.Typeable (Typeable) +import Prelude hiding ((<$>)) +import qualified DDC.Core.Env.EnvX as EnvX + +------------------------------------------------------------------------------- +data Config + = Config + { -- | If we find a lambda abstraction applied to a redex then let-bind + -- the redex and substitute the new variable instead. + configBindRedexes :: Bool } + deriving Show + + +-- | Empty beta configuration with all flags set to False. +configZero :: Config +configZero + = Config + { configBindRedexes = False } + + +------------------------------------------------------------------------------- +-- | A summary of what the beta reduction transform did. +data Info + = Info + { -- | Number of type applications reduced. + infoTypes :: Int + + -- | Number of witness applications reduced. + , infoWits :: Int + + -- | Number of value applications reduced. + , infoValues :: Int + + -- | Number of redexes let-bound. + , infoValuesLetted :: Int + + -- | Number of applications that we couldn't reduce. + , 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) + + +------------------------------------------------------------------------------- -- | Beta-reduce applications of a explicit lambda abstractions -- to variables and values. -betaReduce :: Ord n => Exp a n -> Exp a n -betaReduce - = transformUpX betaReduce1 Env.empty Env.empty +-- +-- If the flag is set then if we find a lambda abstraction that is applied +-- to a redex then let-bind the redex and substitute the new variable +-- instead. +betaReduce + :: forall (c :: * -> * -> *) a n + . (Ord n, TransformUpMX (Writer Info) c) + => Profile n -- ^ Language profile. + -> Config -- ^ Beta transform config. + -> c a n -- ^ Thing to transform. + -> TransformResult (c a n) +betaReduce profile config x + = {-# SCC betaReduce #-} + let (x', info) = runWriter + $ transformUpMX (betaReduce1 profile config) EnvX.empty x -betaReduce1 :: Ord n => Env n -> Env n -> Exp a n -> Exp a n -betaReduce1 _ _ xx - = case xx of - XApp _ (XLAM _ b11 x12) (XType t2) - -> substituteTX b11 t2 x12 + -- Check if any actual work was performed + progress + = case info of + Info ty wit val lets' _ + -> (ty + wit + val + lets') > 0 - XApp _ (XLam _ b11 x12) (XWitness w2) - -> substituteWX b11 w2 x12 + in TransformResult + { result = x' + , resultAgain = progress + , resultProgress = progress + , resultInfo = TransformInfo info } - XApp _ (XLam _ b11 x12) x2 - | canBetaSubstX x2 - -> substituteXX b11 x2 x12 +-- | Do a single beta reduction for this application. +-- +-- To avoid duplicating work, we only reduce value applications when the +-- the argument is not a redex. +-- +-- If needed, we also insert 'weakclo' to ensure the result has the same +-- closure as the original expression. +-- +betaReduce1 + :: Ord n + => Profile n -- ^ Language profile. + -> Config -- ^ Beta tranform config. + -> EnvX n -- ^ Current environment + -> Exp a n -- ^ Expression to transform. + -> Writer Info (Exp a n) + +betaReduce1 _profile config _env xx + = let ret info x = tell info >> return x + + in case xx of + + -- Substitute type arguments into type abstractions. + -- If the type argument of the redex does not appear as an + -- argument of the result then we need to add a closure weakening + -- for the case where t2 was a region variable or handle. + XApp _a (XLAM _ b11 x12) (XType _a2 t2) + | isRegionKind $ typeOfBind b11 + -> ret mempty { infoTypes = 1} + $ substituteTX b11 t2 x12 + + -- Substitute type arguments into type abstractions, + -- Where the argument is not a region type. + XApp _a (XLAM _ b11 x12) (XType _ t2) + -> ret mempty { infoTypes = 1 } + $ substituteTX b11 t2 x12 + + -- Substitute witness arguments into witness abstractions. + XApp _a (XLam _ b11 x12) (XWitness _a2 w2) + -> ret mempty { infoWits = 1 } + $ substituteWX b11 w2 x12 + + -- Substitute value arguments into value abstractions. + 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 - -> xx + -> ret mempty { infoValuesSkipped = 1 } + $ xx - _ -> xx + _ -> return xx -- | Check whether we can safely substitute this expression during beta @@ -43,6 +177,7 @@ -- We allow variables, abstractions, type and witness applications. -- Duplicating these expressions is guaranteed not to duplicate work -- at runtime, +-- canBetaSubstX :: Exp a n -> Bool canBetaSubstX xx = case xx of @@ -51,10 +186,10 @@ XLam{} -> True XLAM{} -> True - XApp _ x1 (XType _) + XApp _ x1 XType{} -> canBetaSubstX x1 - XApp _ x1 (XWitness _) + XApp _ x1 XWitness{} -> canBetaSubstX x1 _ -> False diff --git a/DDC/Core/Transform/Boxing.hs b/DDC/Core/Transform/Boxing.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Boxing.hs @@ -0,0 +1,390 @@ +-- | Manage representation of numeric values in a module. +-- +-- [Note: Boxing and Partial Application] +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-- Unlike in Haskell, we do not allow explictly unboxed types in the source +-- program because we don't want to deal with partial applications of +-- functions to unboxed values. With our current setup we always have a version +-- of each function that accepts boxed values, so we never need to do generic +-- application involving unboxed values. Fast-path function specialisations +-- that take unboxed parameters should be created separately, and not replace +-- the existing slow-path, fully boxed version. Taking this approach is possible +-- in a strict language because the boxed and unboxed values have the same +-- semantic meaning. Boxing of values does not imply "lifting" of the associated +-- semantic domain. +-- +module DDC.Core.Transform.Boxing + ( Rep (..) + , Config (..) + , boxingModule) +where +import DDC.Core.Module +import DDC.Core.Exp.Annot +import DDC.Type.Transform.Instantiate +import Data.Maybe + + +--------------------------------------------------------------------------------------------------- +-- | Representation of the values of some type. +data Rep + -- | These types don't contain any values. + = RepNone + + -- | Values of this type are uncomitted to a particular representation, + -- they just describe a set of logical values. + | RepBoxed + + -- | Values of this type are represented in unboxed form. + | RepUnboxed + deriving (Eq, Ord, Show) + + +data Config a n + = Config + { -- | Get the representation of this type. + configRepOfType :: Type n -> Maybe Rep + + -- | Get the type for a different representation of the given one. + , configConvertRepType :: Rep -> Type n -> Maybe (Type n) + + -- | Convert a value between representations. + , configConvertRepExp :: Rep -> a -> Type n -> Exp a n -> Maybe (Exp a n) + + -- | Take the type of a literal name, if there is one. + , configValueTypeOfLitName :: n -> Maybe (Type n) + + -- | Take the type of a primitive operator name, if it is one. + -- The primops can be polytypic, but must have prenex rank-1 types. + , configValueTypeOfPrimOpName :: n -> Maybe (Type n) + + -- | Take the type of a foreign function name, if it is one. + -- The function can be polymorphic, but must have a prenex rank-1 type. + , configValueTypeOfForeignName :: n -> Maybe (Type n) + + -- | Convert a literal name to its unboxed version. + , configUnboxLitName :: n -> Maybe n + + -- | Covnert a primop name to its unboxed version. + , configUnboxPrimOpName :: n -> Maybe n + } + + +-- Module ----------------------------------------------------------------------------------------- +-- | Manage boxing in a module. +boxingModule + :: Ord n + => Config a n -> Module a n -> Module a n + +boxingModule config mm + = let + -- Use explicitly unboxed types when importing foreign sea functions. + boxingImport imp + = case imp of + ImportValueSea v t + -> ImportValueSea v $ boxingForeignSeaType config t + _ -> imp + + -- Use explicitly unboxed types when exporting foreign sea functions. + nsImportSea = [ n | (n, ImportValueSea _ _) <- moduleImportValues mm] + boxingExport expt + = case expt of + ExportSourceLocal n t + | elem n nsImportSea + -> ExportSourceLocal n $ boxingForeignSeaType config t + _ -> expt + + in mm { moduleBody + = boxingX config (moduleBody mm) + + , moduleExportValues + = [(n, boxingExport expt) | (n, expt) <- moduleExportValues mm ] + + , moduleImportValues + = [(n, boxingImport impt) | (n, impt) <- moduleImportValues mm ] } + + +boxingX config xx + = case xx of + + -- Convert literals to their unboxed form, followed by a boxing conversion. + XCon a (DaConPrim n tLit) + | Just RepBoxed <- configRepOfType config tLit + , Just tLitU <- configConvertRepType config RepUnboxed tLit + , Just nU <- configUnboxLitName config n + + , Just xLit <- configConvertRepExp config RepBoxed a tLitU + $ XCon a (DaConPrim nU tLitU) + -> xLit + + -- Use unboxed versions of primops by unboxing their arguments then + -- reboxing their results. + XCast _ CastRun xx'@(XApp a _ _) + | Just (n, xsArgsAll) <- takeXPrimApps xx' + , Just n' <- configUnboxPrimOpName config n + -> let Just tPrimBoxed = configValueTypeOfPrimOpName config n + Just tPrimUnboxed = configValueTypeOfPrimOpName config n' + xsArgsAll' = map (boxingX config) xsArgsAll + in boxingPrimitive config a True xx' (XVar a (UPrim n' tPrimUnboxed)) + tPrimBoxed tPrimUnboxed + xsArgsAll' + + -- Unbox primitive applications. + XApp a _ _ + | Just (n, xsArgsAll) <- takeXPrimApps xx + , Just n' <- configUnboxPrimOpName config n + -> let Just tPrimBoxed = configValueTypeOfPrimOpName config n + Just tPrimUnboxed = configValueTypeOfPrimOpName config n' + xsArgsAll' = map (boxingX config) xsArgsAll + in boxingPrimitive config a False xx (XVar a (UPrim n' tPrimUnboxed)) + tPrimBoxed tPrimUnboxed + xsArgsAll' + + -- Foreign calls + XApp a _ _ + | Just (xFn@(XVar _ (UName n)), xsArgsAll) + <- takeXApps xx + , Just tForeign <- configValueTypeOfForeignName config n + -> let xsArgsAll' = map (boxingX config) xsArgsAll + in boxingForeignSea config a xx xFn tForeign xsArgsAll' + + -- Unbox literal patterns in alternatives. + XCase a xScrut alts + | p : _ <- [ p | AAlt (PData p@DaConPrim{} []) _ <- alts] + , Just tLit1 <- configValueTypeOfLitName config (daConName p) + , Just RepBoxed <- configRepOfType config tLit1 + -> let alts' = map (boxingAlt config) alts + in boxingCase config a tLit1 xScrut alts' + + -- Boilerplate. + XVar{} -> xx + XCon{} -> xx + XLAM a b x -> XLAM a b (boxingX config x) + XLam a b x -> XLam a b (boxingX config x) + XApp a x1 x2 -> XApp a (boxingX config x1) (boxingX config x2) + XLet a lts x -> XLet a (boxingLts config lts) (boxingX config x) + XCase a x alts -> XCase a (boxingX config x) (map (boxingAlt config) alts) + XCast a c x -> XCast a c (boxingX config x) + XType{} -> xx + XWitness{} -> xx + +boxingLts config lts + = case lts of + LLet b x -> LLet b (boxingX config x) + LRec bxs -> LRec [(b, boxingX config x) | (b, x) <- bxs] + LPrivate{} -> lts + +boxingAlt config alt + = case alt of + AAlt p x -> AAlt p (boxingX config x) + + +--------------------------------------------------------------------------------------------------- +-- | Marshall arguments and return values of primitive operations. +-- If something goes wrong then just return the original expression and leave it to +-- follow on transforms to report the error. The code generator won't be able to +-- convert the original expression. +-- +-- * Assumes that the type of the primitive is in prenex form. +-- +boxingPrimitive + :: Ord n + => Config a n -> a + -> Bool -- ^ Primitive is being run at the call site. + -> Exp a n -- ^ Whole primitive application, for debugging. + -> Exp a n -- ^ Functional expression. + -> Type n -- ^ Type of the boxed version of the primitive. + -> Type n -- ^ Type of the unboxed version of the primitive. + -> [Exp a n] -- ^ Arguments to the primitive. + -> Exp a n + +boxingPrimitive config a bRun xx xFn tPrimBoxed tPrimUnboxed xsArgsAll + = fromMaybe xx go + where + go = do + -- Split off the type args. + let (asArgs, tsArgs) = unzip [(a', t) | XType a' t <- xsArgsAll] + let xsArgs = drop (length tsArgs) xsArgsAll + + -- Get the boxed version of the types of parameters and return value. + tPrimBoxedInst <- instantiateTs tPrimBoxed tsArgs + let (tsParamBoxed, _tResultBoxed) + = takeTFunArgResult tPrimBoxedInst + + -- Get the unboxed version of the types of parameters and return value. + tPrimUnboxedInst <- instantiateTs tPrimUnboxed tsArgs + let (_tsParamUnboxed, tResultUnboxed) + = takeTFunArgResult tPrimUnboxedInst + + -- If the primitive is being run at the call site then we need to + -- re-box the result AFTER it has been run, not before. + let tResultUnboxed' + | not bRun = tResultUnboxed + | otherwise = case takeTSusp tResultUnboxed of + Just (_, t) -> t + Nothing -> tResultUnboxed + + -- We must end up with a type of each argument. + -- If not then the primop is partially applied or something else is wrong. + -- The Tetra to Salt conversion will give a proper error message + -- if the primop is indeed partially applied. +-- (if not ( length xsArgs == length tsParamBoxed +-- && length xsArgs == length tsParamUnboxed) +-- then Nothing +-- else Just ()) + + -- We got a type for each argument, so the primop is fully applied + -- and we can do the boxing/unboxing transform. + let xsArgs' = [ (let t = fromMaybe xArg + $ configConvertRepExp config RepUnboxed a tArgInst xArg + in t) + | xArg <- xsArgs + | tArgInst <- tsParamBoxed ] + + -- Construct the result expression, running it if necessary. + let xtsArgsU = [ XType a' t | t <- tsArgs | a' <- asArgs ] + let xResultU = xApps a xFn (xtsArgsU ++ xsArgs') + let xResultRunU + | not bRun = xResultU + | otherwise = XCast a CastRun xResultU + + let xResultV = fromMaybe xResultRunU + $ configConvertRepExp config RepBoxed a tResultUnboxed' xResultRunU + + return xResultV + + +--------------------------------------------------------------------------------------------------- +-- Marshall arguments and return values of foreign imported functions. +-- +-- * Assumes that the type of the imported thing is in prenex form. +-- +boxingForeignSea + :: Ord n + => Config a n -> a + -> Exp a n -- ^ Whole function application, for debugging. + -> Exp a n -- ^ Functional expression. + -> Type n -- ^ Type of the foreign function. + -> [Exp a n] -- ^ Arguments to the foreign function. + -> Exp a n + +boxingForeignSea config a xx xFn tF xsArg + = fromMaybe xx go + where go = do + -- Split off the type args. + let (_asArg, tsArgType) = unzip [(a', t) | XType a' t <- xsArg] + let xsArgVal = drop (length tsArgType) xsArg + + -- Get the argument and return types of the function. + -- Unlike primitives, foreign functions are not polytypic, so we can + -- just erase any outer foralls to reveal the types of the args. + let (tsArgVal, tResult) + = takeTFunArgResult + $ eraseTForalls tF + + -- We must end up with a type for each argument. + (if not (length xsArgVal == length tsArgVal) + then Nothing + else Just ()) + + -- For each argument, if it has an unboxed representation then unbox it. + let unboxArg xArg tArg + = fromMaybe xArg + $ configConvertRepExp config RepUnboxed a tArg xArg + + let xsArgValU = zipWith unboxArg xsArgVal tsArgVal + let xExpU = xApps a xFn ([XType a t | t <- tsArgType] ++ xsArgValU) + + -- If the result has a boxed representation then box it. + let boxResult tRes xRes + = fromMaybe xRes + $ do tResU <- configConvertRepType config RepUnboxed tRes + configConvertRepExp config RepBoxed a tResU xExpU + + return $ boxResult tResult xExpU + + +-- | Marshall arguments and return values for function imported from Sea land. +boxingForeignSeaType + :: Config a n -> Type n -> Type n + +boxingForeignSeaType config tForeign + = let + -- Split the type into quantifiers, parameter and result types. + (bsForall, tBody) + = fromMaybe ([], tForeign) + $ takeTForalls tForeign + + (tsParam, tResult) + = takeTFunArgResult tBody + + -- If there is an unboxed representation of each parameter and result + -- type, then use that. + unboxType tThing + = fromMaybe tThing + $ configConvertRepType config RepUnboxed tThing + + tsParamU = map unboxType tsParam + tResultU = unboxType tResult + + -- Build the converted type back out of its parts. + Just tBodyU = tFunOfList (tsParamU ++ [tResultU]) + tForeignU = foldr TForall tBodyU bsForall + + in tForeignU + + +--------------------------------------------------------------------------------------------------- +-- For case expressions that match against literals, like +-- +-- case e1 of +-- { 5# -> e2; _ -> e3 } +-- +-- Unbox the scrutinee and convert the alternatives to match against +-- unboxed literals. +-- +-- case convert# [Nat] [Nat#] e1 of +-- { 5## -> e2; _ -> e3 } +-- +boxingCase + :: Config a n + -> a -> Type n + -> Exp a n + -> [Alt a n] + -> Exp a n + +boxingCase config a tLit1 xScrut alts + = let + unboxAlt (AAlt (PData (DaConPrim n tLit) []) x) + | Just RepBoxed <- configRepOfType config tLit + , Just nU <- configUnboxLitName config n + , Just tLitU <- configConvertRepType config RepUnboxed tLit + = Just (AAlt (PData (DaConPrim nU tLitU) []) x) + + unboxAlt alt@(AAlt PDefault _) = Just alt + unboxAlt _ = Nothing + + Just alts_unboxed + = sequence $ map unboxAlt alts + + Just xScrut' = configConvertRepExp config RepUnboxed a tLit1 xScrut + alts_default = ensureDefault alts_unboxed + + in XCase a xScrut' $ alts_default + + +-- | Ensure that there is a default alternative in this list, +-- if not then make the last one the default. +-- We need do this to handle the case when the unboxed type does not have +-- all its constructors listed in the data defs. If it doesn't then the +-- case exhaustiveness checker will compilain when checking the result code. +ensureDefault :: [Alt a n] -> [Alt a n] +ensureDefault alts + | _ : _ <- [alt | alt@(AAlt PDefault _) <- alts] + = alts + + | AAlt (PData _ []) x : rest <- reverse alts + = reverse rest ++ [AAlt PDefault x] + + | otherwise + = alts + diff --git a/DDC/Core/Transform/Bubble.hs b/DDC/Core/Transform/Bubble.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Bubble.hs @@ -0,0 +1,285 @@ + +-- | Bubble casts outwards. +-- We float casts up and outwards so they are just inside the inner-most +-- enclosing let. This way the functions still have the same effect and +-- closure, but the casts don't get in the way of subsequent transforms. +-- +module DDC.Core.Transform.Bubble + ( bubbleModule + , bubbleX) +where +import DDC.Core.Collect +import DDC.Core.Transform.BoundX +import DDC.Core.Module +import DDC.Core.Exp.Annot +import DDC.Type.Env (KindEnv, TypeEnv) +import qualified DDC.Type.Env as Env +import qualified DDC.Type.Sum as Sum +import qualified Data.Set as Set +import Data.Set (Set) +import Data.List + + +-- | Bubble casts outwards in a `Module`. +bubbleModule + :: Ord n + => Module a n -> Module a n + +bubbleModule mm@ModuleCore{} + = let kenv = moduleKindEnv mm + tenv = moduleTypeEnv mm + in mm { moduleBody = bubbleX kenv tenv (moduleBody mm) } + + +-- | Bubble casts outwards in an `Exp`. +bubbleX :: Ord n + => KindEnv n -> TypeEnv n -> Exp a n -> Exp a n +bubbleX kenv tenv x + = let + -- Bubble the expression, yielding any casts that floated out + -- to top-level. + (cs, x') = bubble kenv tenv x + a = annotOfExp x' + + -- Reattach top-level casts. + in dropAllCasts kenv tenv a cs x' + + +------------------------------------------------------------------------------- +-- | Bubble casts outwards in some thing. +class Bubble (c :: * -> * -> *) where + bubble :: Ord n + => KindEnv n + -> TypeEnv n + -> c a n + -> ([FvsCast a n], c a n) + + +instance Bubble Exp where + bubble kenv tenv xx + = {-# SCC bubble #-} + case xx of + XVar{} -> ([], xx) + XCon{} -> ([], xx) + + -- Drop casts before we leave lambda abstractions, because the + -- function type depends on the effect and closure of the body. + -- The cast could also reference the bound variable. + XLAM a b x + -> let kenv' = Env.extend b kenv + (cs, x') = bubble kenv' tenv x + in ([], XLAM a b (dropAllCasts kenv' tenv a cs x')) + + XLam a b x + -> let tenv' = Env.extend b tenv + (cs, x') = bubble kenv tenv' x + in ([], XLam a b (dropAllCasts kenv tenv' a cs x')) + + -- Decend into applications. + XApp a x1 x2 + -> let (cs1, x1') = bubble kenv tenv x1 + (cs2, x2') = bubble kenv tenv x2 + in (cs1 ++ cs2, XApp a x1' x2') + + -- After decending into let-expressions, make sure to drop + -- any casts that mention variables bound here. + XLet a lts x2 + -> let (cs1, lts') = bubble kenv tenv lts + (bs1, bs0) = bindsOfLets lts + kenv' = Env.extends bs1 kenv + tenv' = Env.extends bs0 tenv + (cs2, x2') = bubble kenv' tenv' x2 + (cs2', x2'') = dropCasts kenv' tenv' a bs1 bs0 cs2 x2' + in ( cs1 ++ cs2' + , XLet a lts' x2'') + + -- Decent into case-expressions. + -- Casts that depend on bound variables are dropped + -- in the corresponding alternatives. + XCase a x alts + -> let (cs, x') = bubble kenv tenv x + (css, alts') = unzip $ map (bubble kenv tenv) alts + in ( cs ++ concat css + , XCase a x' alts') + + -- Strip of cast and pass it up. + XCast _ c x + -> let (cs, x') = bubble kenv tenv x + fvsT = freeT Env.empty c + fvsX = freeX Env.empty c + fc = FvsCast c fvsT fvsX + in (fc : cs, x') + + XType{} -> ([], xx) + XWitness{} -> ([], xx) + + +instance Bubble Lets where + bubble kenv tenv lts + = case lts of + + -- Drop casts that mention the bound variable here, + -- but we can float the others further outwards. + LLet b x + -> let (cs, x') = bubble kenv tenv x + a = annotOfExp x' + (cs', xc') = dropCasts kenv tenv a [] [b] cs x' + in (cs', LLet b xc') + + -- ISSUE #299: Bubble casts out of recursive lets. + LRec bxs + -> let bs = map fst bxs + tenv' = Env.extends bs tenv + + bubbleRec (b, x) + = let (cs, x') = bubble kenv tenv' x + a = annotOfExp x' + in (b, dropAllCasts kenv tenv' a cs x') + + bxs' = map bubbleRec bxs + + in ([], LRec bxs') + + LPrivate{} + -> ([], lts) + + +instance Bubble Alt where + + -- Default patterns don't bind variables, + -- so there is no problem floating casts outwards. + bubble kenv tenv (AAlt PDefault x) + = let (cs, x') = bubble kenv tenv x + in (cs, AAlt PDefault x') + + -- Drop casts before we leave the alt because they could contain + -- variables bound by the pattern. + bubble kenv tenv (AAlt p x) + = let bs = bindsOfPat p + a = annotOfExp x' + tenv' = Env.extends bs tenv + (cs, x') = bubble kenv tenv' x + (csUp, xcHere) = dropCasts kenv tenv' a [] bs cs x' + in (csUp, AAlt p xcHere) + + +-- FvsCast -------------------------------------------------------------------- +-- | A Cast along with its free level-1 and level-0 vars. +-- When we first build a `FvsCast` we record its free variables, +-- so that we don't have to keep recomputing them. +data FvsCast a n + = FvsCast (Cast a n) + (Set (Bound n)) -- Free level-1 variables. + (Set (Bound n)) -- Free level-0 variables. + +instance Ord n => MapBoundX (FvsCast a) n where + mapBoundAtDepthX f d (FvsCast c fvs1 fvs0) + = FvsCast (mapBoundAtDepthX f d c) + fvs1 + (Set.fromList + $ map (mapBoundAtDepthX f d) + $ Set.toList fvs0) + + +packFvsCasts + :: Ord n + => KindEnv n -> TypeEnv n + -> a -> [FvsCast a n] -> [Cast a n] + +packFvsCasts kenv tenv a fvsCasts + = packCasts kenv tenv a [ c | FvsCast c _ _ <- fvsCasts ] + + +-- | Pack down casts by combining multiple 'weakclo' and 'weakeff' casts +-- together. We pack casts just before we drop them, so that the resulting +-- code is easier to read. +packCasts :: Ord n + => KindEnv n -> TypeEnv n -> a -> [Cast a n] -> [Cast a n] +packCasts _kenv _tenv _a vs + = let + -- Sort casts into weakeff, weakclo and any others. + -- We'll collect the weakeff and weakclo casts together. + collect weakEffs weakClos others cc + = case cc of + [] + -> (reverse weakEffs, reverse weakClos, reverse others) + + CastWeakenEffect eff : cs + -> collect (eff : weakEffs) weakClos others cs + + c : cs + -> collect weakEffs weakClos (c : others) cs + + + (effs, csOthers, _) + = collect [] [] [] vs + + in (if null effs + then [] + else [CastWeakenEffect (TSum $ Sum.fromList kEffect effs)]) + ++ csOthers + + +-- Dropping ------------------------------------------------------------------- +-- | Wrap the provided expression with these casts. +dropAllCasts + :: Ord n + => KindEnv n + -> TypeEnv n + -> a + -> [FvsCast a n] -> Exp a n + -> Exp a n + +dropAllCasts kenv tenv a cs x + = let cs' = packFvsCasts kenv tenv a cs + in foldr (XCast a) x cs' + + +-- | Split the provided casts into ones that contain variables +-- bound by these binders. The casts that do are used to wrap +-- the provided expression, and the casts that don't are returned +-- seprately so we can keep bubbling them up the tree. +dropCasts + :: Ord n + => KindEnv n -> TypeEnv n + -> a + -> [Bind n] -- ^ Level-1 binders. + -> [Bind n] -- ^ Level-0 binders. + -> [FvsCast a n] + -> Exp a n + -> ([FvsCast a n], Exp a n) + +dropCasts kenv tenv a bs1 bs0 cs x + = let (csHere1, cs1) = partition (fvsCastUsesBinds1 bs1) cs + (csHere0, csUp) = partition (fvsCastUsesBinds0 bs0) cs1 + csHere = packFvsCasts kenv tenv a $ csHere1 ++ csHere0 + in ( map (lowerX 1) csUp + , foldr (XCast a) x csHere) + + +-- | Check if a `FvsCast` mentions any of these level-0 variables. +fvsCastUsesBinds0 :: Ord n => [Bind n] -> FvsCast a n -> Bool +fvsCastUsesBinds0 bb (FvsCast _ _ fvs0) + = bindsMatchBoundSet bb fvs0 + + +-- | Check if a `FvsCast` mentions any of these level-1 variables. +fvsCastUsesBinds1 :: Ord n => [Bind n] -> FvsCast a n -> Bool +fvsCastUsesBinds1 bb (FvsCast _ fvs1 _) + = bindsMatchBoundSet bb fvs1 + + +-- | Check if a set of bound variables matches any of the given binders. +bindsMatchBoundSet :: Ord n => [Bind n] -> Set (Bound n) -> Bool +bindsMatchBoundSet bb fvs + = go bb + where go [] = False + go (b : bs) + | Just u <- takeSubstBoundOfBind b + = if Set.member u fvs + then True + else go bs + + | otherwise + = go bs + diff --git a/DDC/Core/Transform/Elaborate.hs b/DDC/Core/Transform/Elaborate.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Elaborate.hs @@ -0,0 +1,110 @@ + +-- | Add possible Const and Distinct witnesses that aren't +-- otherwise in the program. +module DDC.Core.Transform.Elaborate + ( elaborateModule + , elaborateX ) +where +import DDC.Core.Exp +import DDC.Core.Module +import DDC.Type.Exp.Simple +import DDC.Data.ListUtils +import Control.Monad +import Control.Arrow +import Data.Maybe +import Data.List + + +-- | Elaborate witnesses in a module. +elaborateModule :: Eq n => Module a n -> Module a n +elaborateModule mm + = mm { moduleBody = elaborate [] $ moduleBody mm } + + +-- | Elaborate witnesses in an expression. +elaborateX :: Eq n => Exp a n -> Exp a n +elaborateX xx + = elaborate [] xx + + +------------------------------------------------------------------------------- +class Elaborate (c :: * -> *) where + elaborate :: Eq n => [Bound n] -> c n -> c n + + +instance Elaborate (Exp a) where + elaborate us xx + = {-# SCC elaborate #-} + let down = elaborate us + in case xx of + XVar{} -> xx + XCon{} -> xx + XLAM a b x -> XLAM a b (down x) + XLam a b x -> XLam a b (down x) + XApp a x1 x2 -> XApp a (down x1) (down x2) + + XLet a lts x2 + -> let (us', lts') = elaborateLets us lts + in XLet a lts' (elaborate us' x2) + + XCase a x alts -> XCase a (down x) (map down alts) + XCast a cst x2 -> XCast a (down cst) (down x2) + XType{} -> xx + XWitness{} -> xx + + +instance Elaborate (Cast a) where + elaborate _us cst = cst + + +instance Elaborate (Alt a) where + elaborate us (AAlt p x) = AAlt p (elaborate us x) + + +-- | Elaborate witnesses in some let-bindings. +elaborateLets + :: Eq n + => [Bound n] -- ^ Witness bindings in the environment. + -> Lets a n -- ^ Elaborate these let bindings. + -> ([Bound n], Lets a n) + +elaborateLets us lts + = let down = elaborate us + in case lts of + LLet b x -> (us, LLet b (down x)) + LRec bs -> (us, LRec $ map (second down) bs) + + LPrivate brs mt bws + | urs@(_:_) <- takeSubstBoundsOfBinds brs + -> let + -- Mutable regions bound here. + rsMutable = catMaybes + $ map (takeMutableRegion . typeOfBind) bws + + -- Make a new const witness for all non-mutable regions. + constWits = map makeConstWit + $ urs \\ rsMutable + + -- Make a new distinct witness against all regions + -- in the environment. + Just ursTail = takeTail urs + distinctWits = map makeDistinctWit + $ liftM2 (,) us urs + ++ zip urs ursTail + + in ( us ++ urs + , LPrivate brs mt $ bws ++ distinctWits ++ constWits ) + + _ -> (us, lts) + +makeConstWit u + = BNone $ tConst (TVar u) + +makeDistinctWit (u1,u2) + = BNone $ tDistinct 2 [TVar u1, TVar u2] + +takeMutableRegion tt + = case takeTyConApps tt of + Just (TyConWitness TwConMutable, [TVar u]) -> Just u + _ -> Nothing + diff --git a/DDC/Core/Transform/Eta.hs b/DDC/Core/Transform/Eta.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Eta.hs @@ -0,0 +1,306 @@ + +-- Eta-expand functional values. +--- +-- NOTE: This is module currently just does eta-expansion, but in future +-- we should expand the config to also make it do expansion/contraction +-- based on the real arity of bindings. +-- +module DDC.Core.Transform.Eta + ( Config(..) + , configZero + , Info (..) + , etaModule + , etaX) +where +import qualified DDC.Core.Check as Check +import DDC.Core.Module +import DDC.Core.Exp.Annot +import DDC.Core.Fragment +import DDC.Core.Transform.BoundX +import DDC.Core.Transform.BoundT +import DDC.Core.Simplifier.Result +import DDC.Core.Pretty +import DDC.Type.Transform.AnonymizeT +import Control.Monad.Writer (Writer, tell, runWriter) +import Data.Typeable +import DDC.Core.Env.EnvX (EnvX) +import qualified DDC.Core.Env.EnvX as EnvX +import Prelude hiding ((<$>)) + + +------------------------------------------------------------------------------- +data Config + = Config + { configExpand :: Bool } + deriving Show + + +-- | Empty eta configuration with all flags set to False. +configZero :: Config +configZero + = Config + { configExpand = False } + + +------------------------------------------------------------------------------- +data Info + = Info + { -- | Number of level-1 lambdas added. + infoExpandedXLAMs :: Int + + -- | Number of level-0 lambdas added. + , infoExpandedXLams :: Int } + deriving Typeable + + +instance Pretty Info where + ppr (Info ex1 ex0) + = text "Eta Transform" + <$> indent 4 (vcat + [ text "level-1 lambdas added: " <> int ex1 + , text "level-0 lambdas added: " <> int ex0 ]) + + +instance Monoid Info where + mempty = Info 0 0 + mappend (Info ex1 ex0) + (Info ex1' ex0') + = Info (ex1 + ex1') (ex0 + ex0') + + +-- Module --------------------------------------------------------------------- +-- | Eta-transform expressions in a module. +etaModule + :: (Ord n, Show n, Pretty n, Show a) + => Profile n + -> Config + -> Module a n + -> TransformResult (Module a n) + +etaModule profile config mm + = let + -- Slurp type checker config. + cconfig = Check.configOfProfile profile + + -- Slurp the top level environment. + env = moduleEnvX + (profilePrimKinds profile) + (profilePrimTypes profile) + (profilePrimDataDefs profile) + mm + + -- Run the eta transform. + (mm', info) = runWriter $ etaM config cconfig env mm + + -- Check if any actual work was performed + progress + = case info of + Info ex1 ex0 + -> ex1 + ex0 > 0 + + in TransformResult + { result = mm' + , resultAgain = False + , resultProgress = progress + , resultInfo = TransformInfo info } + + +-- | Eta-transform an expression. +etaX :: (Ord n, Show n, Show a, Pretty n) + => Profile n -- ^ Language profile. + -> Config -- ^ Eta-transform config. + -> EnvX n -- ^ Type checker environment. + -> Exp a n -- ^ Expression to transform. + -> TransformResult (Exp a n) + +etaX profile config env xx + = let cconfig = Check.configOfProfile profile + + -- Run the eta transform. + (xx', info) + = runWriter + $ etaM config cconfig env xx + + -- Check if any actual work was performed + progress + = case info of + Info ex1 ex0 + -> ex1 + ex0 > 0 + + in TransformResult + { result = xx' + , resultAgain = False + , resultProgress = progress + , resultInfo = TransformInfo info } + + +------------------------------------------------------------------------------- +class Eta (c :: * -> * -> *) where + etaM :: (Show a, Ord n, Pretty n, Show n) + => Config -- ^ Eta-transform config. + -> Check.Config n -- ^ Type checker config. + -> EnvX n -- ^ Type checker environment. + -> c a n -- ^ Do eta-expansion in this thing. + -> Writer Info (c a n) + + +instance Eta Module where + etaM config cconfig envx mm + = do -- The top level environment of the module is added + -- by the etaModule wrapper, so we don't need to do it again. + xx' <- etaM config cconfig envx (moduleBody mm) + return $ mm { moduleBody = xx' } + + +instance Eta Exp where + etaM config cconfig env xx + = let down = etaM config cconfig env + in case xx of + + XVar a _ + | configExpand config + , Right tX <- Check.typeOfExp cconfig env xx + -> do etaExpand a tX xx + + XApp a _ _ + | configExpand config + , Right tX <- Check.typeOfExp cconfig env xx + -> do + -- Decend into the arguments first. + -- We don't need to decend into the function part because + -- we're eta-expanding that here. + let (x : xs) = takeXAppsAsList xx + xs_eta <- mapM down xs + + -- Now eta expand the result. + etaExpand a tX $ xApps a x xs_eta + + XLAM a b x + -> do let env' = EnvX.extendT b env + x' <- etaM config cconfig env' x + return $ XLAM a b x' + + XLam a b x + -> do let env' = EnvX.extendX b env + x' <- etaM config cconfig env' x + return $ XLam a b x' + + XLet a lts x2 + -> do lts' <- down lts + let (bs1, bs0) = bindsOfLets lts + + let env' = EnvX.extendsT bs1 + $ EnvX.extendsX bs0 env + + x2' <- etaM config cconfig env' x2 + return $ XLet a lts' x2' + + XCase a x alts + -> do x' <- down x + alts' <- mapM (etaM config cconfig env) alts + return $ XCase a x' alts' + + XCast a cc x + -> do x' <- down x + return $ XCast a cc x' + + _ -> return xx + + +instance Eta Lets where + etaM config cconfig env lts + = let down = etaM config cconfig env + in case lts of + LLet b x + -> do x' <- down x + return $ LLet b x' + + LRec bxs + -> do let bs = map fst bxs + let env' = EnvX.extendsX bs env + xs' <- mapM (etaM config cconfig env') + $ map snd bxs + return $ LRec (zip bs xs') + + LPrivate{} + -> return lts + + +instance Eta Alt where + etaM config cconfig env alt + = case alt of + AAlt p x + -> do let bs = bindsOfPat p + let env' = EnvX.extendsX bs env + x' <- etaM config cconfig env' x + return $ AAlt p x' + + +-- Expand --------------------------------------------------------------------- +-- | Eta expand an expression. +etaExpand + :: Ord n + => a -- ^ Annotation to use for new AST nodes. + -> Type n -- ^ Type of the expression. + -> Exp a n -- ^ Inner expression to wrap. + -> Writer Info (Exp a n) + +etaExpand a tX xx + -- Anonymize the type, so any references to foralls will become anonymous. + -- Then, when we add the anonymous bindings, it will work out. + = do let btsMore = expandableArgs $ anonymizeT tX + xx' <- etaExpand' a 0 0 [] btsMore xx + return xx' + + +-- | Decide what type arguments need to be eta-expanded. +expandableArgs :: Type n -> [(Bool, Type n)] +expandableArgs tt + | TForall b t' <- tt + = (True, typeOfBind b) : expandableArgs t' + + | Just (t1, t2) <- takeTFun tt + = (False, t1) : expandableArgs t2 + + | otherwise + = [] + + +-- | Eta-expand an expression. +etaExpand' + :: Ord n + => a -- ^ Annotation to use for the new AST nodes. + -> Int -- ^ Number of level-1 lambdas we've added so far. + -> Int -- ^ Number of level-0 lambdas we've added so far. + -> [Exp a n] -- ^ Accumulate arguments we need to add to the + -- inner expression. + -> [(Bool, Type n)] -- ^ Types of bindings we need to add, along with + -- a flag to indicate level-1 or level-0 binder + -> Exp a n -- ^ Inner expression that is being applied. + -> Writer Info (Exp a n) + +etaExpand' a levels1 levels0 args [] xx + = do let xx' = liftT levels1 $ liftX levels0 xx + return $ xApps a xx' args + +etaExpand' a levels1 levels0 args ((True, t) : ts) xx + = do let depth1 = length $ filter ((== True) . fst) ts + xx' <- etaExpand' a (levels1 + 1) levels0 + (args ++ [XType a (TVar (UIx depth1))]) + ts + xx + + tell mempty { infoExpandedXLAMs = 1 } + return $ XLAM a (BAnon t) xx' + +etaExpand' a levels1 levels0 args ((False, t) : ts) xx + = do let depth0 = length $ filter ((== False) . fst) ts + xx' <- etaExpand' a + levels1 (levels0 + 1) + (args ++ [XVar a (UIx depth0)]) + ts + xx + + tell mempty { infoExpandedXLams = 1 } + return $ XLam a (BAnon t) xx' + diff --git a/DDC/Core/Transform/Flatten.hs b/DDC/Core/Transform/Flatten.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Flatten.hs @@ -0,0 +1,134 @@ + +-- | Flattening nested let and case expressions. +module DDC.Core.Transform.Flatten + (flatten) +where +import DDC.Core.Transform.TransformUpX +import DDC.Core.Transform.AnonymizeX +import DDC.Core.Transform.BoundX +import DDC.Core.Exp.Annot +import Data.Functor.Identity + + +-- | Flatten binding structure in a thing. +-- +-- Flattens nested let-expressions, +-- and single alternative let-case expressions. +-- +flatten :: Ord n + => (TransformUpMX Identity c) + => c a n -> c a n +flatten + = {-# SCC flatten #-} + transformUpX' flatten1 + + +-- | Flatten a single nested let-expression. +flatten1 + :: Ord n + => Exp a n + -> Exp a n + +-- Run ---------------------------------------------------- +flatten1 (XCast a1 CastRun (XLet a2 lts x2)) + = XLet a2 lts $ flatten1 (XCast a1 CastRun x2) + + +-- Let ---------------------------------------------------- +-- Special case when nested let is (let b = x in b): +-- @ +-- let b1 = (let ^ = def2 in ^0) in +-- x1 +-- +-- ==> let b1 = def2 in +-- x1 +-- @ +-- +flatten1 (XLet a1 (LLet b1 + (XLet _ (LLet (BAnon _) def2) (XVar _ (UIx 0)))) + x1) + = flatten1 + $ XLet a1 (LLet b1 def2) + x1 + +-- Let ---------------------------------------------------- +-- Flatten Nested Lets. +-- @ +-- let b1 = (let b2 = def2 in x2) in +-- x1 +-- +-- ==> let b2 = def2 in +-- let b1 = x2 in +-- x1 +-- @ +-- +flatten1 (XLet a1 (LLet b1 + inner@(XLet a2 (LLet b2 def2) x2)) + x1) + + | isBName b2 + = flatten1 + $ XLet a1 (LLet b1 + (anonymizeX inner)) + x1 + + | otherwise + = let x1' = liftAcrossX [b1] [b2] x1 + in XLet a2 (LLet b2 def2) + $ flatten1 + $ XLet a1 (LLet b1 x2) + x1' + + +-- Flatten single-alt case expressions. +-- @ +-- let b1 = case x1 of +-- P -> x2 +-- in x3 +-- +-- => case x1 of +-- P -> let b1 = x2 +-- in x3 +-- @ +-- +-- * binding must be strict because we force evaluation of x1. +-- +flatten1 (XLet a1 (LLet b1 + inner@(XCase a2 x1 [AAlt p x2])) + x3) + | any isBName $ bindsOfPat p + = flatten1 + $ XLet a1 (LLet b1 + (anonymizeX inner)) + x3 + + | otherwise + = let x3' = liftAcrossX [b1] (bindsOfPat p) x3 + in XCase a2 x1 + [AAlt p ( flatten1 + $ XLet a1 (LLet b1 x2) + (anonymizeX x3'))] + + +-- Any let, its bound expression doesn't contain a strict non-recursive +-- let so just flatten the body +flatten1 (XLet a1 llet1 x1) + = XLet a1 llet1 (flatten1 x1) + + +-- Case --------------------------------------------------- +-- Flatten all the alternatives in a case-expression. +flatten1 (XCase a x1 alts) + = XCase a (flatten1 x1) + [AAlt p (flatten1 x) | AAlt p x <- alts ] + +flatten1 x = x + + +liftAcrossX :: [Bind n] -> [Bind n] -> Exp a n -> Exp a n +liftAcrossX bsDepth bsLevels x + = let depth = length [b | b@(BAnon _) <- bsDepth] + levels = length [b | b@(BAnon _) <- bsLevels] + in liftAtDepthX levels depth x + + diff --git a/DDC/Core/Transform/FoldCase.hs b/DDC/Core/Transform/FoldCase.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/FoldCase.hs @@ -0,0 +1,84 @@ + +module DDC.Core.Transform.FoldCase + ( Config (..) + , configZero + , foldCase + , foldCaseX ) +where +import DDC.Core.Exp.Annot +import DDC.Core.Transform.TransformDownX +import Control.Monad.State.Strict +import qualified Data.Map.Strict as M +import qualified DDC.Type.Env as Env + +data Config + = Config + { -- | Perform the case-of-constructor transformation. + configCaseOfConstructor :: Bool + + -- | Perform the case-of-case transformation. + -- Not implemented yet. + , configCaseOfCase :: Bool } + +configZero :: Config +configZero + = Config + { configCaseOfConstructor = False + , configCaseOfCase = False } + + +--------------------------------------------------------------------------------------------------- +type FoldCase a n = State (M.Map n (DaCon n (Type n), [Exp a n])) + +foldCase :: (Ord n, TransformDownMX (FoldCase a n) c) + => Config + -> c a n + -> c a n + +foldCase config xx + = {-# SCC foldCase #-} + evalState (transformDownMX (\_ _ -> foldCaseX config) Env.empty Env.empty xx) M.empty + +foldCaseX :: Ord n + => Config + -> Exp a n + -> FoldCase a n (Exp a n) + + +-- Collect ---------------------------------------------------------------------------------------- +foldCaseX _ + x@(XLet _ (LLet (BName b _) ex) _) + | Just (dc, args) <- takeXConApps ex + = do + modify (M.insert b (dc, args)) + return x + + +-- Case of Constructor ---------------------------------------------------------------------------- +-- @ +-- let x = Con y z in +-- case x of +-- Con a b -> x1 +-- +-- ==> let x = Con y z in +-- let a = y in +-- let b = z in +-- x1 +-- @ +-- +foldCaseX config + x@(XCase _ (XVar _ (UName n)) [alt]) + | configCaseOfConstructor config + , AAlt (PData dc binds) rest <- alt + = do + seen <- gets (M.lookup n) + return $ case seen of + Just (dc', args') | dc == dc' + -> foldr (\(x', bnd) next -> XLet (annotOfExp x') (LLet bnd x') next) + rest (zip (filter (not . isXType) args') binds) + + _ -> x + + +-- Default case. +foldCaseX _ x = return x diff --git a/DDC/Core/Transform/Forward.hs b/DDC/Core/Transform/Forward.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Forward.hs @@ -0,0 +1,302 @@ + +-- | Float let-bindings with a single use forward into their use-sites. +module DDC.Core.Transform.Forward + ( ForwardInfo (..) + , FloatControl (..) + , Config(..) + , forwardModule + , forwardX) +where +import DDC.Data.Pretty +import DDC.Core.Analysis.Usage +import DDC.Core.Exp.Annot +import DDC.Core.Module +import DDC.Core.Simplifier.Base +import DDC.Core.Transform.Reannotate +import DDC.Core.Fragment +import Data.Map (Map) +import Control.Monad +import Control.Monad.Writer (Writer, runWriter, tell) +import Data.Typeable +import qualified Data.Map as Map +import qualified DDC.Core.Transform.SubstituteXX as S +import Prelude hiding ((<$>)) + + +------------------------------------------------------------------------------- +-- | Summary of number of bindings floated. +data ForwardInfo + = ForwardInfo + { -- | Number of bindings inspected. + infoInspected :: !Int + + -- | Number of trivial @v1 = v2@ bindings inlined. + , infoSubsts :: !Int + + -- | Number of bindings floated forwards. + , infoBindings :: !Int } + deriving Typeable + + +instance Pretty ForwardInfo where + ppr (ForwardInfo inspected substs bindings) + = text "Forward:" + <$> indent 4 (vcat + [ text "Total bindings inspected: " <> int inspected + , text " Trivial substitutions made: " <> int substs + , text " Bindings moved forward: " <> int bindings ]) + + +instance Monoid ForwardInfo where + mempty = ForwardInfo 0 0 0 + mappend (ForwardInfo i1 s1 b1)(ForwardInfo i2 s2 b2) + = ForwardInfo (i1 + i2) (s1 + s2) (b1 + b2) + + +------------------------------------------------------------------------------- +-- | Fine control over what should be floated. +data FloatControl + = FloatAllow -- ^ Allow binding to be floated, but don't require it. + | FloatDeny -- ^ Prevent a binding being floated, at all times. + | FloatForce -- ^ Force a binding to be floated, at all times. + | FloatForceUsedOnce -- ^ Force a binding to be floated if it's only used once. + deriving (Eq, Show) + +data Config a n + = Config + { configFloatControl :: Lets a n -> FloatControl + , configFloatLetBody :: Bool } + +------------------------------------------------------------------------------- +-- | Float let-bindings in a module with a single use forward into +-- their use sites. +forwardModule + :: Ord n + => Profile n -- ^ Language profile + -> Config a n + -> Module a n + -> TransformResult (Module a n) + +forwardModule profile config mm + = let (mm', info) + = runWriter + $ forwardWith profile config Map.empty + $ usageModule mm + + progress (ForwardInfo _ s f) + = s + f > 0 + + in TransformResult + { result = mm' + , resultProgress = progress info + , resultAgain = False + , resultInfo = TransformInfo info } + + +-- | Float let-bindings in an expression with a single use forward into +-- their use-sites. +forwardX :: Ord n + => Profile n -- ^ Language profile. + -> Config a n + -> Exp a n + -> TransformResult (Exp a n) + +forwardX profile config xx + = let (x',info) = runWriter + $ forwardWith profile config Map.empty + $ usageX xx + + progress (ForwardInfo _ s f) + = s + f > 0 + + in TransformResult + { result = x' + , resultProgress = progress info + , resultAgain = False + , resultInfo = TransformInfo info } + + +------------------------------------------------------------------------------- +class Forward (c :: * -> * -> *) where + -- | Carry bindings forward and downward into their use-sites. + forwardWith + :: Ord n + => Profile n -- ^ Language profile. + -> Config a n + -> Map n (Exp a n) -- ^ Bindings currently being carried forward. + -> c (UsedMap n, a) n + -> Writer ForwardInfo (c a n) + +instance Forward Module where + forwardWith profile config bindings + (ModuleCore + { moduleName = name + , moduleIsHeader = isHeader + , moduleExportTypes = exportTypes + , moduleExportValues = exportValues + , moduleImportTypes = importTypes + , moduleImportCaps = importCaps + , moduleImportValues = importValues + , moduleImportDataDefs = importDataDefs + , moduleImportTypeDefs = importTypeDefs + , moduleDataDefsLocal = dataDefsLocal + , moduleTypeDefsLocal = typeDefsLocal + , moduleBody = body }) + + = do body' <- forwardWith profile config bindings body + return ModuleCore + { moduleName = name + , moduleIsHeader = isHeader + , moduleExportTypes = exportTypes + , moduleExportValues = exportValues + , moduleImportTypes = importTypes + , moduleImportCaps = importCaps + , moduleImportValues = importValues + , moduleImportDataDefs = importDataDefs + , moduleImportTypeDefs = importTypeDefs + , moduleDataDefsLocal = dataDefsLocal + , moduleTypeDefsLocal = typeDefsLocal + , moduleBody = body' } + + +instance Forward Exp where + forwardWith profile config bindings xx + = {-# SCC forwardWith #-} + let down = forwardWith profile config bindings + in case xx of + XVar a u@(UName n) + -> case Map.lookup n bindings of + Just xx' -> do + tell mempty { infoSubsts = 1 } + return xx' + Nothing -> + return $ XVar (snd a) u + + XVar a u -> return $ XVar (snd a) u + XCon a u -> return $ XCon (snd a) u + XLAM a b x -> liftM (XLAM (snd a) b) (down x) + XLam a b x -> liftM (XLam (snd a) b) (down x) + XApp a x1 x2 -> liftM2 (XApp (snd a)) (down x1) (down x2) + + -- Always float last let-binding into its use. + -- let x = exp in x => exp + XLet _ (LLet b x1) (XVar _ u) + | boundMatchesBind u b + , configFloatLetBody config + -> down x1 + + -- A special case for atomic anonymous bindings. + -- Always float atomic bindings (variables, constructors), + -- but only if they're still atomic after forwarding them: + -- if x1 is a variable to be replaced with a function, then + -- substituting x1 into x2 could duplicate that. + XLet (_, a) (LLet b@(BAnon _) x1) x2 + | isAtomX x1 + -> do + x1' <- down x1 + if isAtomX x1' + then do + -- Record that we've moved this binding. + tell mempty { infoInspected = 1 + , infoBindings = 1 } + + -- Slower, but handles anonymous binders and shadowing + down $ S.substituteXX b x1 x2 + + else do + tell mempty { infoInspected = 1} + liftM (XLet a $ LLet b x1') (down x2) + + XLet (UsedMap um, a') lts@(LLet (BName n t) x1) x2 + -> do + let control = configFloatControl config + $ reannotate snd lts + + let isFun = isXLam x1 || isXLAM x1 + + let isApplied + | Just usage <- Map.lookup n um + , [UsedFunction] <- filterUsedInCasts usage + = True + | otherwise = False + + let shouldFloat + = case control of + FloatDeny -> False + FloatForce -> True + FloatAllow -> isFun && isApplied + + FloatForceUsedOnce + | Just usage <- Map.lookup n um + , length usage == 1 + -> True + | otherwise + -> False + + -- Always float atomic bindings (variables, constructors). + x1' <- down x1 + + if shouldFloat || isAtomX x1' + then do + -- Record that we've moved this binding. + tell mempty { infoInspected = 1 + , infoBindings = 1 } + + let bindings' = Map.insert n x1' bindings + forwardWith profile config bindings' x2 + + else do + tell mempty { infoInspected = 1} + + -- Note that @n@ has been shadowed + let bindings' = Map.delete n bindings + x2' <- forwardWith profile config bindings' x2 + + return $ XLet a' (LLet (BName n t) x1') x2' + + XLet (_, a') lts x + -> liftM2 (XLet a') (down lts) (down x) + + XCase a x alts -> liftM2 (XCase (snd a)) (down x) (mapM down alts) + XCast a c x -> liftM2 (XCast (snd a)) (down c) (down x) + XType a t -> return (XType (snd a) t) + XWitness a w -> return (XWitness (snd a) (reannotate snd w)) + + +filterUsedInCasts :: [Used] -> [Used] +filterUsedInCasts = filter notCast + where notCast UsedInCast = False + notCast _ = True + + +instance Forward Cast where + forwardWith _profile _config _bindings xx + = case xx of + CastWeakenEffect eff -> return $ CastWeakenEffect eff + CastPurify w -> return $ CastPurify (reannotate snd w) + CastBox -> return $ CastBox + CastRun -> return $ CastRun + + +instance Forward Lets where + forwardWith profile config bindings lts + = let down = forwardWith profile config bindings + in case lts of + LLet b x + -> liftM (LLet b) (down x) + + LRec bxs + -> liftM LRec + $ mapM (\(b,x) + -> do x' <- down x + return (b, x')) + bxs + + LPrivate b mt bs + -> return $ LPrivate b mt bs + + +instance Forward Alt where + forwardWith profile config bindings (AAlt p x) + = liftM (AAlt p) (forwardWith profile config bindings x) + diff --git a/DDC/Core/Transform/Inline.hs b/DDC/Core/Transform/Inline.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Inline.hs @@ -0,0 +1,75 @@ + +-- | Inlining definitions into their use sites. +module DDC.Core.Transform.Inline + ( inline + , InlineSpec (..) + , lookupTemplateFromModules) +where +import DDC.Core.Exp +import DDC.Core.Module +import DDC.Core.Transform.Inline.Templates +import qualified Data.Set as Set +import Data.Set (Set) + + +class Inline (c :: * -> * -> *) where + inline :: Ord n + => (n -> Maybe (Exp a n)) + -- ^ Get the template for a named variable. + -> Set n -- ^ Don't inline definitions for these names. + -> c a n + -> c a n + + +instance Inline Module where + inline get inside mm + = mm { moduleBody = inline get inside (moduleBody mm) } + + +instance Inline Exp where + inline get inside xx + = let down x = inline get inside x + in case xx of + XVar _ (UName n) + -- Don't inline a recursive definition into itself. + | Set.member n inside + -> xx + + -- If there is a template for this variable then inline it, + -- but remember that we're now inside the body so we don't inline + -- recursive functions forever. + | Just xx' <- get n + -> let !inside' = Set.insert n inside + in inline get inside' xx' + + XVar{} -> xx + XCon{} -> xx + XLAM a b x -> XLAM a b (down x) + XLam a b x -> XLam a b (down x) + XApp a x1 x2 -> XApp a (down x1) (down x2) + XLet a lts x2 -> XLet a (down lts) (down x2) + XCase a x alts -> XCase a (down x) (map down alts) + XCast a c x -> XCast a c (down x) + XType{} -> xx + XWitness{} -> xx + + +instance Inline Lets where + inline get inside lts + = let enter b x + = case b of + BName n _ -> inline get (Set.insert n inside) x + _ -> inline get inside x + + in case lts of + LLet b x -> LLet b (enter b x) + LRec bxs -> LRec [(b, enter b x) | (b, x) <- bxs] + LPrivate{} -> lts + + +instance Inline Alt where + inline get inside alt + = case alt of + AAlt p x -> AAlt p (inline get inside x) + + diff --git a/DDC/Core/Transform/Inline/Templates.hs b/DDC/Core/Transform/Inline/Templates.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Inline/Templates.hs @@ -0,0 +1,96 @@ + +-- | Retrieving inliner templates from a list of modules. +module DDC.Core.Transform.Inline.Templates + ( InlineSpec(..) + , lookupTemplateFromModules + , lookupTemplateFromModule ) +where +import DDC.Core.Exp +import DDC.Core.Module +import DDC.Core.Transform.AnonymizeX +import Data.List +import Data.Set (Set) +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Data.Set as Set + + +-- | Inlining specification says what bindings we should inline +-- from a particular module. +data InlineSpec n + -- | Inline all bindings from a module, + -- but exclude some particulars. + = InlineSpecAll + { inlineSpecModuleName :: ModuleName + , inlineSpecExclude :: Set n } + + -- | Inline no bindings from a module, + -- but include some particulars. + | InlineSpecNone + { inlineSpecModuleName :: ModuleName + , inlineSpecInclude :: Set n } + deriving Show + + +-- | Lookup an inliner template from a list of modules. +--- +-- This just does a linear search through all the modules. +-- As we only inline functions defined at top level, we don't need to worry +-- about lifting indices in templates when we go under binders. +-- +lookupTemplateFromModules + :: (Ord n, Show n) + => Map ModuleName (InlineSpec n) + -- ^ Inliner specifications for the modules. + -> [Module a n] -- ^ Modules to use for inliner templates. + -> n + -> Maybe (Exp a n) + +lookupTemplateFromModules specs mm n + | m : ms <- mm + = let -- If there is no inliner spec then don't inline anything. + spec = case Map.lookup (moduleName m) specs of + Just s -> s + Nothing -> InlineSpecNone (moduleName m) Set.empty + + in case lookupTemplateFromModule spec m n of + Nothing -> lookupTemplateFromModules specs ms n + Just x -> Just x + + | otherwise + = Nothing + + +lookupTemplateFromModule + :: Ord n + => InlineSpec n -- ^ Inliner specification for this module. + -> Module a n -- ^ Module to use for inliner templates. + -> n + -> Maybe (Exp a n) + +lookupTemplateFromModule spec mm n + | shouldInline spec n + , XLet _ (LRec bxs) _ <- moduleBody mm + , Just (_,x) <- find (\(BName n' _, _) -> n == n') bxs + = Just $ anonymizeX x + + | otherwise + = Nothing + + +-- | Decide whether we should inline the binding with this name based on the +-- provided inliner specification. +shouldInline + :: Ord n + => InlineSpec n -> n -> Bool + +shouldInline spec n + = case spec of + InlineSpecAll _ except + | Set.member n except -> False + | otherwise -> True + + InlineSpecNone _ include + | Set.member n include -> True + | otherwise -> False + diff --git a/DDC/Core/Transform/Lambdas.hs b/DDC/Core/Transform/Lambdas.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Lambdas.hs @@ -0,0 +1,481 @@ + +module DDC.Core.Transform.Lambdas + ( lambdasModule + , evalState + , newVar) +where +import DDC.Core.Transform.Lambdas.Lift +import DDC.Core.Transform.Lambdas.Base +import DDC.Core.Fragment +import DDC.Core.Collect.Support +import DDC.Core.Transform.SubstituteXX +import DDC.Core.Module +import DDC.Core.Exp.Annot.Context +import DDC.Core.Exp.Annot.Ctx +import DDC.Core.Exp.Annot +import DDC.Type.Transform.SubstituteT +import DDC.Data.Pretty +import DDC.Data.Name +import qualified DDC.Type.Env as Env +import qualified DDC.Type.DataDef as DataDef +import qualified DDC.Core.Env.EnvX as EnvX +import qualified Data.Set as Set +import qualified Data.Map as Map +import Data.Maybe + + +--------------------------------------------------------------------------------------------------- +-- | Perform lambda lifting in a module. +lambdasModule + :: ( Show a, Pretty a + , Show n, Pretty n, Ord n, CompoundName n) + => Profile n + -> Module a n + -> S (Module a n) + +lambdasModule profile mm + = do + -- Take the top-level environment of the module. + let env = moduleEnvX + (profilePrimKinds profile) + (profilePrimTypes profile) + (profilePrimDataDefs profile) + mm + + let c = Context env (CtxTop env) + x' <- lambdasLoopX profile c $ moduleBody mm + + return + $ mm { moduleBody = x' } + + +-- Exp -------------------------------------------------------------------------------------------- +lambdasLoopX + :: (Show n, Show a, Pretty n, Pretty a, CompoundName n, Ord n) + => Profile n -- ^ Language profile. + -> Context a n -- ^ Enclosing context. + -> Exp a n -- ^ Expression to perform lambda lifting on. + -> S (Exp a n) -- Replacement expression. + +lambdasLoopX p c xx + = do (xx1, Result progress _) + <- lambdasTopX p c xx + + if progress + then lambdasLoopX p c xx1 + else return xx1 + +-- | Handle the expression that defines the body of the module +-- separately. The body is a letrec that contains the top level +-- bindings, and we don't want to lift them out further. +lambdasTopX p c xx + = case xx of + XLet a lts xBody + -> do (lts', r1) <- lambdasTopLets p c a xBody lts + (x', r2) <- enterLetBody c a lts xBody (lambdasTopX p) + return ( foldr (XLet a) x' lts' + , mappend r1 r2) + + _ -> lambdasX p c xx + + +-- | Handle the top-level group of bindings. +lambdasTopLets p c a xBody lts + = case lts of + LRec bxs + -> do (bxs', r) <- lambdasLetRec p c a [] bxs xBody + return ([LRec bxs'], r) + + _ -> lambdasLets p c a xBody lts + + +--------------------------------------------------------------------------------------------------- +-- | Perform a single pass of lambda lifting in an expression. +lambdasX :: (Show n, Show a, Pretty n, Pretty a, CompoundName n, Ord n) + => Profile n -- ^ Language profile. + -> Context a n -- ^ Enclosing context. + -> Exp a n -- ^ Expression to perform lambda lifting on. + -> S ( Exp a n -- Replacement expression + , Result a n) -- Lifter result. + +lambdasX p c xx + = case xx of + XVar{} + -> return (xx, mempty) + + XCon a (DaConBound nCon) + -> do mResult <- etaXConApp p c a xx nCon [] + case mResult of + Nothing -> return (xx, mempty) + Just result -> return result + + XCon{} + -> return (xx, mempty) + + -- Lift type lambdas to top-level. + XLAM a b x0 + -> enterLAM c a b x0 $ \c' x + -> do (x', r) <- lambdasX p c' x + let xx' = XLAM a b x' + let Result _ bxs = r + + -- Decide whether to lift this lambda to top-level. + -- If there are multiple nested lambdas then we want to lift + -- the whole group at once, rather than lifting each one + -- individually. + let liftMe = isLiftyContext (contextCtx c) && null bxs + if liftMe + then do + let us' = supportEnvFlags + $ support Env.empty Env.empty xx' + + (xCall, bLifted, xLifted) + <- liftLambda p c us' a [(True, b)] x' + + return ( xCall + , Result True (bxs ++ [(bLifted, xLifted)])) + + else return (xx', r) + + + -- Lift value lambdas to top-level. + XLam a b x0 + -> enterLam c a b x0 $ \c' x + -> do (x', r) <- lambdasX p c' x + let xx' = XLam a b x' + let Result _ bxs = r + + -- Decide whether to lift this lambda to top-level. + let liftMe = isLiftyContext (contextCtx c) && null bxs + + if liftMe + then do + let us' = supportEnvFlags + $ support Env.empty Env.empty xx' + + (xCall, bLifted, xLifted) + <- liftLambda p c us' a [(False, b)] x' + + return ( xCall + , Result True (bxs ++ [(bLifted, xLifted)])) + + else return (xx', r) + + + -- Lift suspensions to top-level. + -- These behave like zero-arity lambda expressions, + -- they suspend evaluation but do not abstract over a value. + XCast a cc@CastBox x0 + -> enterCastBody c a cc x0 $ \c' x + -> do (x', r) <- lambdasX p c' x + let xx' = XCast a CastBox x' + let Result _ bxs = r + + -- Decide whether to lift this box to top-level. + let liftMe = isLiftyContext (contextCtx c) && null bxs + + if liftMe + then do + let us' = supportEnvFlags + $ support Env.empty Env.empty xx' + + (xCall, bLifted, xLifted) + <- liftLambda p c us' a [] (XCast a CastBox x') + + return ( xCall + , Result True (bxs ++ [(bLifted, xLifted)])) + + else return (xx', r) + + + -- Eta-expand partially applied data contructors. + XApp a x1 x2 + | (XCon _a (DaConBound nCon), xsArg) <- takeXApps1 x1 x2 + -> do + mResult <- etaXConApp p c a x1 nCon xsArg + case mResult of + Just result + -> return result + + _ -> do (x1', r1) <- enterAppLeft c a x1 x2 (lambdasX p) + (x2', r2) <- enterAppRight c a x1 x2 (lambdasX p) + return ( XApp a x1' x2' + , mappend r1 r2) + + + -- Boilerplate. + XApp a x1 x2 + -> do (x1', r1) <- enterAppLeft c a x1 x2 (lambdasX p) + (x2', r2) <- enterAppRight c a x1 x2 (lambdasX p) + return ( XApp a x1' x2' + , mappend r1 r2) + + XLet a lts x + -> do (lts', r1) <- lambdasLets p c a x lts + (x', r2) <- enterLetBody c a lts x (lambdasX p) + return ( foldr (XLet a) x' lts' + , mappend r1 r2) + + XCase a x alts + -> do (x', r1) <- enterCaseScrut c a x alts (lambdasX p) + (alts', r2) <- lambdasAlts p c a x [] alts + return ( XCase a x' alts' + , mappend r1 r2) + + XCast a cc x + -> lambdasCast p c a cc x + + XType{} + -> return (xx, mempty) + + XWitness{} + -> return (xx, mempty) + + +-- Lets ------------------------------------------------------------------------------------------- +-- | Perform lambda lifting in some let-bindings. +lambdasLets + :: (Show a, Show n, Ord n, Pretty n, Pretty a, CompoundName n) + => Profile n -> Context a n + -> a -> Exp a n + -> Lets a n + -> S ([Lets a n], Result a n) + +lambdasLets p c a xBody lts + = case lts of + LLet b x + -> do (x', r) <- enterLetLLet c a b x xBody (lambdasX p) + return ([LLet b x'], r) + + LRec bxs + -> do (bxs', r) <- lambdasLetRecLiftAll p c a bxs + return (map (uncurry LLet) bxs', r) + + LPrivate{} + -> return ([lts], mempty) + + +-- LetRec ----------------------------------------------------------------------------------------- +-- | Perform lambda lifting in the right of a single let-rec binding. +lambdasLetRec + :: (Show a, Show n, Ord n, Pretty n, Pretty a, CompoundName n) + => Profile n -> Context a n + -> a -> [(Bind n, Exp a n)] -> [(Bind n, Exp a n)] -> Exp a n + -> S ([(Bind n, Exp a n)], Result a n) + +lambdasLetRec _ _ _ _ [] _ + = return ([], mempty) + +lambdasLetRec p c a bxsAcc ((b, x) : bxsMore) xBody + = do (x', r1) + <- enterLetLRec c a bxsAcc b x bxsMore xBody (lambdasX p) + + case contextCtx c of + + -- If we're at top-level then drop lifted bindings here. + CtxTop{} + -> do (bxs', Result p2 bxs2) + <- lambdasLetRec p c a ((b, x') : bxsAcc) bxsMore xBody + let Result p1 bxsLifted = r1 + return ( bxsLifted ++ ((b, x') : bxs') + , Result (p1 || p2) bxs2 ) + + _ + -> do (bxs', r2) + <- lambdasLetRec p c a ((b, x') : bxsAcc) bxsMore xBody + return ( (b, x') : bxs' + , mappend r1 r2 ) + + +-- | When all the bindings in a letrec are lambdas, lift them all together. +lambdasLetRecLiftAll + :: (Show a, Show n, Ord n, Pretty n, Pretty a, CompoundName n) + => Profile n -> Context a n + -> a + -> [(Bind n, Exp a n)] + -> S ([(Bind n, Exp a n)], Result a n) + +lambdasLetRecLiftAll p c a bxs + = let -- Wrap the context in the letrec + ctx before b x after + = enterLetLRec c a before b x after x (\c' _ -> c') + in do + + -- The union of free variables of all the mutually recursive bindings must be used, + -- as any lifted function may call the other lifted functions. + let us = Set.unions + $ map (supportEnvFlags . support Env.empty Env.empty) + $ map snd bxs + + -- However, the functions we are lifting should not be treated as free variables + let us' = Set.filter + (\(_, bo) -> not $ any (boundMatchesBind bo . fst) bxs) + $ us + + -- Lift each of the bindings in its own context. + -- We allow the group of bindings to contain ones with outer lambda + -- abstractions that need to be lifted, along with non-functional + -- bindings that stay in place. + let lift _before [] + = return [] + + lift before ((b, x) : after) + = case takeXLamFlags x of + -- The right of this binding has an outer abstraction, + -- so we need to lift it to top-level. + Just (lams, xx) + -> do let c' = ctx before b x after + l' <- liftLambda p c' us' a lams xx + ls <- lift (before ++ [(b,x)]) after + return $ Right (b, l') : ls + + -- The right of this binding does not have any outer + -- abstractions, so we can leave it in place. + Nothing + -> do ls <- lift (before ++ [(b, x)]) after + return $ Left (b, x) : ls + + ls <- lift [] bxs + + -- The call to each lifted function + let stripCall (Left (b, x)) = (b, x) + stripCall (Right (b, (xC, _, _))) = (b, xC) + let calls = map stripCall ls + + -- Substitute the original name of the recursive function with a call to its new name, + -- including passing along any free variables. + -- Here, we need to unwrap the newly-created lambdas for the free variables, + -- as capture-avoiding substitution would rename them - the opposite of what we want. + let sub x = case takeXLamFlags x of + Just (lams, xx) -> makeXLamFlags a lams (substituteXXs calls xx) + Nothing -> substituteXXs calls x + + -- The result bindings to add at the top-level, with all the new names substituted in + let stripResult (Left _) = Nothing + stripResult (Right (_, (_, bL, xL))) = Just (bL, sub xL) + + let res = mapMaybe stripResult ls + + return (calls, Result True res) + + + +-- Alts ------------------------------------------------------------------------------------------- +-- | Perform lambda lifting in the right of a single alternative. +lambdasAlts + :: (Show a, Show n, Ord n, Pretty n, Pretty a, CompoundName n) + => Profile n -> Context a n + -> a -> Exp a n -> [Alt a n] -> [Alt a n] + -> S ([Alt a n], Result a n) + +lambdasAlts _ _ _ _ _ [] + = return ([], mempty) + +lambdasAlts p c a xScrut altsAcc (AAlt w x : altsMore) + = do (x', r1) <- enterCaseAlt c a xScrut altsAcc w x altsMore (lambdasX p) + (alts', r2) <- lambdasAlts p c a xScrut (AAlt w x' : altsAcc) altsMore + return ( AAlt w x' : alts' + , mappend r1 r2) + + +-- Cast ------------------------------------------------------------------------------------------- +-- | Perform lambda lifting in the body of a Cast expression. +lambdasCast + :: (Show a, Show n, Ord n, Pretty n, Pretty a, CompoundName n) + => Profile n -> Context a n + -> a -> Cast a n -> Exp a n + -> S (Exp a n, Result a n) + +lambdasCast p c a cc x + = case cc of + CastWeakenEffect{} + -> do (x', r) <- enterCastBody c a cc x (lambdasX p) + return ( XCast a cc x', r) + + CastPurify{} + -> do (x', r) <- enterCastBody c a cc x (lambdasX p) + return (XCast a cc x', r) + + CastBox + -> do (x', r) <- enterCastBody c a cc x (lambdasX p) + return (XCast a cc x', r) + + CastRun + -> do (x', r) <- enterCastBody c a cc x (lambdasX p) + return (XCast a cc x', r) + + +------------------------------------------------------------------------------- +-- | Eta-expand partially applied data constructors. +-- The code generator only handles fully applied data constructors, +-- so we eta-expand partially applied ones so that they get turned +-- into thunks. +etaXConApp + :: (Show a, Pretty a, Pretty n, Ord n, Show n, CompoundName n) + => Profile n -- ^ Language Profile. + -> Context a n -- ^ Current context of transform. + -> a -- ^ Annotation from constructor applicatin onde. + -> Exp a n -- ^ Expression holding constructor. + -> n -- ^ Name of constructor. + -> [Exp a n] -- ^ Arguments to constructor. + -> S (Maybe ( Exp a n + , Result a n)) + +etaXConApp !p !c !a !x1 !nCon !xsArg + -- Lookup the type of the constructor. + | ctx <- contextCtx c + , case ctx of + CtxAppLeft{} -> False + _ -> True + + , envX <- topOfCtx ctx + , defs <- EnvX.envxDataDefs envX + , Just dataCtor <- Map.lookup nCon (DataDef.dataDefsCtors defs) + + -- We're expecting an argument for each of the type and term parameters. + , arityT <- length $ DataDef.dataCtorTypeParams dataCtor + , arityX <- length $ DataDef.dataCtorFieldTypes dataCtor + , arity <- arityT + arityX + + -- Check if the constructor is partially applied. + , arityX >= 1 + , args <- length xsArg + , args /= arity + = do + -- Make binders for the new type parameters. + (bsT, usT) + <- fmap unzip + $ mapM (\(i, t) -> newVar (show i) t) + $ [ (i, typeOfBind b) + | i <- [0..arityT - 1] + | b <- DataDef.dataCtorTypeParams dataCtor ] + + let sub = zip (DataDef.dataCtorTypeParams dataCtor) + (map TVar usT) + + -- Make binders for the new term parameters. + (bsX, usX) + <- fmap unzip + $ mapM (\(i, t) -> newVar (show i) (substituteTs sub t)) + $ [ (i, t) + | i <- [0 .. arityX - 1] + | t <- DataDef.dataCtorFieldTypes dataCtor ] + + -- Transform all the arguments. + let downArg xArg = enterAppRight c a x1 xArg (lambdasX p) + (xsArg', rs) <- fmap unzip $ mapM downArg xsArg + + -- Build application of our new abstraction. + return $ Just + $ ( xApps a + ( xLAMs a bsT $ xLams a bsX + $ xApps a (XCon a (DaConBound nCon)) + $ [ XType a (TVar u) | u <- usT] + ++ [ XVar a u | u <- usX]) + xsArg' + + , mconcat (Result True [] : rs)) + + | otherwise + = return Nothing + diff --git a/DDC/Core/Transform/Lambdas/Base.hs b/DDC/Core/Transform/Lambdas/Base.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Lambdas/Base.hs @@ -0,0 +1,103 @@ + +module DDC.Core.Transform.Lambdas.Base + ( S, evalState + , newVar + , newVarExtend + , Result (..) + , isLiftyContext) +where +import DDC.Core.Exp.Annot.Ctx +import DDC.Core.Exp.Annot +import DDC.Data.Name +import qualified Control.Monad.State.Strict as S + + +--------------------------------------------------------------------------------------------------- +-- | State holding a variable name prefix and counter to +-- create fresh variable names. +type S = S.State (String, Int) + + +-- | Evaluate a desguaring computation, +-- using the given prefix for freshly introduced variables. +evalState :: String -> S a -> a +evalState n c + = S.evalState c (n, 0) + + +-- | Allocate a new named variable, yielding its associated bind and bound. +newVar + :: CompoundName n + => String -- ^ Informational name to add. + -> Type n -- ^ Type of the new binder. + -> S (Bind n, Bound n) + +newVar prefix t + = do (n, i) <- S.get + let name' = newVarName (n ++ "$" ++ prefix ++ "$" ++ show i) + S.put (n, i + 1) + return (BName name' t, UName name') + + +-- | Allocate a new named variable, yielding its associated bind and bound. +newVarExtend + :: CompoundName n + => n -- ^ Base name. + -> String -- ^ Informational name to ad. + -> Type n -- ^ Type of the new binder. + -> S (Bind n, Bound n) + +newVarExtend name prefix t + = do (n, i) <- S.get + let name' = extendName name (n ++ "$" ++ prefix ++ "$" ++ show i) + S.put (n, i + 1) + return (BName name' t, UName name') + + + +--------------------------------------------------------------------------------------------------- +-- | Result of lambda lifter recursion. +data Result a n + = Result + { -- | Whether we've made any progress in this pass. + _resultProgress :: Bool + + -- | Bindings that we've already lifted out, + -- and should be added at top-level. + , _resultBindings :: [(Bind n, Exp a n)] + } + + +instance Monoid (Result a n) where + mempty + = Result False [] + + mappend (Result p1 lts1) (Result p2 lts2) + = Result (p1 || p2) (lts1 ++ lts2) + + +--------------------------------------------------------------------------------------------------- +-- | Check if this is a context that we should lift lambda abstractions out of. +isLiftyContext :: Ctx a n -> Bool +isLiftyContext ctx + = case ctx of + -- Don't lift out of the top-level context. + -- There's nowhere else to lift to. + CtxTop{} -> False + CtxLetLLet{} -> not $ isTopLetCtx ctx + CtxLetLRec{} -> not $ isTopLetCtx ctx + + -- Don't lift if we're inside more lambdas. + -- We want to lift the whole binding group together. + CtxLAM{} -> False + CtxLam{} -> False + + -- We can't do code generation for abstractions in these contexts, + -- so they need to be lifted. + CtxAppLeft{} -> True + CtxAppRight{} -> True + CtxLetBody{} -> True + CtxCaseScrut{} -> True + CtxCaseAlt{} -> True + CtxCastBody{} -> True + diff --git a/DDC/Core/Transform/Lambdas/Lift.hs b/DDC/Core/Transform/Lambdas/Lift.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Lambdas/Lift.hs @@ -0,0 +1,184 @@ + +module DDC.Core.Transform.Lambdas.Lift + (liftLambda) +where +import DDC.Core.Transform.Lambdas.Base +import DDC.Core.Fragment +import DDC.Core.Exp.Annot.Context +import DDC.Core.Exp.Annot.Ctx +import DDC.Core.Exp.Annot +import DDC.Core.Collect +import DDC.Data.Pretty +import DDC.Data.Name +import Data.Function +import Data.List +import Data.Set (Set) +import qualified DDC.Core.Check as Check +import qualified DDC.Type.Env as Env +import qualified DDC.Core.Env.EnvX as EnvX +import qualified Data.Set as Set +import qualified Data.Map as Map + + +--------------------------------------------------------------------------------------------------- +-- | Construct the call site, and new lifted binding for a lambda lifted +-- abstraction. +liftLambda + :: (Show a, Show n, Pretty n, Ord n, CompoundName n, Pretty a) + => Profile n -- ^ Language profile. + -> Context a n -- ^ Context of the original abstraction. + -> Set (Bool, Bound n) -- ^ Free variables in the body of the abstraction. + -> a + -> [(Bool, Bind n)] -- ^ Parameters of the current lambda abstraction. + -> Exp a n -- ^ Body of the current lambda abstraction. + -> S ( Exp a n + , Bind n, Exp a n) + +liftLambda p c fusFree a bfsParam xBody + = do + -- Name of the enclosing top-level binding. + let Just nTop = takeTopNameOfCtx (contextCtx c) + + -- Names of other supers bound at top-level. + let nsSuper = takeTopLetEnvNamesOfCtx (contextCtx c) + + -- The complete abstraction that we're lifting out. + let xLambda = makeXLamFlags a bfsParam xBody + + -- Get the list of new parameters we need to add to our super. + -- These bind all the variables that were free in the abstraction + -- group that we're lifting out. + let fusFree_filtered + = filter (needParamForFreeBound nsSuper bfsParam) + $ Set.toList fusFree + + + -- Lookup the types of those variables from the context, + -- so we can add the correct types for the parameters of the new super. + let joinType (f@True, u) + | Just t <- EnvX.lookupT u (contextEnv c) + = ((f, u), t) + + joinType (f@False, u) + | Just t <- EnvX.lookupX u (contextEnv c) + = ((f, u), t) + + joinType (f, u) + = error $ unlines + [ "ddc-core-simpl.liftLambda: cannot find type of free variable." + , show (f, u) + , show (Map.keys $ EnvX.envxMap (contextEnv c)) ] + + let futsFree_types + = map joinType fusFree_filtered + + + -- Add in type variables that are free in the types of free + -- value variables. We need to bind these as well in the new super. + let expandFree ((f@True, u), _) + = [(f, u)] + + expandFree ((f@False, u), t) + = [(f, u)] + ++ [(True, ut) | ut <- Set.toList + $ freeVarsT Env.empty t] + + let fusFree_body + = [(True, ut) | ut <- Set.toList + $ freeVarsT Env.empty $ typeOfExp p c xLambda] + + let futsFree_expandFree + = map joinType + $ Set.toList $ Set.fromList + $ (concatMap expandFree $ futsFree_types) + ++ fusFree_body + + + -- Sort free vars so the type variables come out the front. + let futsFree + = sortBy (compare `on` (not . fst . fst)) + $ futsFree_expandFree + + + -- Make the new super. + -- For the lifted abstraction, wrap it in new lambdas to bind all of + -- its free variables. + -- ISSUE #330: Lambda lifter doesn't work with anonymous binders. + let makeBind ((True, (UName n)), t) = (True, BName n t) + makeBind ((False, (UName n)), t) = (False, BName n t) + makeBind fut + = error $ "ddc-core-simpl.liftLamba: unhandled binder " ++ show fut + + let bsParam = map makeBind futsFree + let xLifted = makeXLamFlags a bsParam xLambda + + -- Make a binder for the new super. + (bLifted, uLifted) + <- newVarExtend nTop "L" + $ typeOfExp p c xLifted + + -- At the point where the original abstraction group was, + -- call our new lifted super instead. + let makeArg (True, u) = XType a (TVar u) + makeArg (False, u) = XVar a u + + let xCall = xApps a (XVar a uLifted) + $ map makeArg $ map fst futsFree + + -- All done. + return ( xCall + , bLifted, xLifted) + + +--------------------------------------------------------------------------------------------------- +-- | Decide whether we need to bind the given variable as a new parameter +-- on the lifted super. +needParamForFreeBound + :: (Ord n) + => Set n -- ^ Names of supers at top level. + -> [(Bool, Bind n)] -- ^ Parameters of the current lambda abstraction. + -> (Bool, Bound n) -- ^ Bound variable, and whether it is a type (True) or not. + -> Bool + +needParamForFreeBound nsSuper bfsParam (bType, u) + -- We don't need new parameters for supers that are already + -- at top level, as we can reference those directly. + | not bType + , UName n <- u + = not $ Set.member n nsSuper + + -- We don't need new parameters for primitives, + -- as we can reference those directly. + | UPrim{} <- u + = False + + -- We don't need new paramters for variables that + -- are already bound by the abstractions that we're lifting. + | any (boundMatchesBind u . snd) bfsParam + = False + + -- We need a new parameter for this free variable. + | otherwise + = True + + +-- Function to get the type of an expression in the given context. +typeOfExp + :: (Pretty a, Show a, Show n, Pretty n, Eq n, Ord n) + => Profile n -- ^ Language profile. + -> Context a n -- ^ Current context. + -> Exp a n -- ^ Expression we want the type for. + -> Type n + +typeOfExp p c x + = case Check.typeOfExp + (Check.configOfProfile p) + (contextEnv c) x + of Left err + -> error $ renderIndent $ vcat + [ text "ddc-core-simpl.liftLambda: type error in lifted expression" + , ppr err] + + Right t + -> t + diff --git a/DDC/Core/Transform/Namify.hs b/DDC/Core/Transform/Namify.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Namify.hs @@ -0,0 +1,285 @@ + +-- | Rewriting of anonymous binders to named binders. +module DDC.Core.Transform.Namify + ( Namify (..) + , Namifier (..) + , makeNamifier + , namifyUnique) +where +import DDC.Core.Module +import DDC.Core.Exp +import DDC.Core.Collect +import DDC.Type.Exp.Simple +import Control.Monad +import DDC.Type.Env (Env, KindEnv, TypeEnv) +import qualified DDC.Type.Sum as Sum +import qualified DDC.Type.Env as Env +import Control.Monad.State.Strict + + +-- | Holds a function to rename binders, +-- and the state of the renamer as we decend into the tree. +data Namifier s n + = Namifier + { -- | Create a new name for this bind that is not in the given + -- environment. + namifierNew :: Env n -> Bind n -> State s n + + -- | Holds the current environment during namification. + , namifierEnv :: Env n + + -- | Stack of debruijn binders that have been rewritten during + -- namification. + , namifierStack :: [Bind n] } + + +-- | Construct a new namifier. +makeNamifier + :: (Env n -> Bind n -> State s n) + -- ^ Function to rename binders. + -- The name chosen cannot be a member of the given + --- environment. + -> Env n -- ^ Starting environment of names we cannot use. + -> Namifier s n + +makeNamifier new env + = Namifier new env [] + + +-- | Namify a thing, +-- not reusing names already in the program. +namifyUnique + :: (Ord n, Namify c, BindStruct (c n) n) + => (KindEnv n -> Namifier s n) -- ^ Make a namifier for level-1 names. + -> (TypeEnv n -> Namifier s n) -- ^ Make a namifier for level-0 names. + -> c n + -> State s (c n) + +namifyUnique mkNamK mkNamT xx + = let (tbinds, xbinds) = collectBinds xx + namK = mkNamK (Env.fromList tbinds) + namT = mkNamT (Env.fromList xbinds) + in namify namK namT xx + + +-- Namify --------------------------------------------------------------------- +class Namify (c :: * -> *) where + -- | Rewrite anonymous binders to named binders in a thing. + namify :: Ord n + => Namifier s n -- ^ Namifier for type names (level-1) + -> Namifier s n -- ^ Namifier for exp names (level-0) + -> c n -- ^ Rewrite binders in this thing. + -> State s (c n) + + +instance Namify Type where + namify tnam xnam tt + = let down = namify tnam xnam + in case tt of + TVar u + -> liftM TVar (rewriteT tnam u) + + TCon{} + -> return tt + + TAbs b t + -> do (tnam', b') <- pushT tnam b + t' <- namify tnam' xnam t + return $ TAbs b' t' + + TApp t1 t2 + -> liftM2 TApp (down t1) (down t2) + + TForall b t + -> do (tnam', b') <- pushT tnam b + t' <- namify tnam' xnam t + return $ TForall b' t' + + TSum ts + -> do ts' <- mapM down $ Sum.toList ts + return $ TSum $ Sum.fromList (Sum.kindOfSum ts) ts' + + +instance Namify (Module a) where + namify tnam xnam mm + = do body' <- namify tnam xnam $ moduleBody mm + return $ mm { moduleBody = body' } + + +instance Namify (Witness a) where + namify tnam xnam ww + = let down = namify tnam xnam + in case ww of + WVar a u -> liftM (WVar a) (rewriteX tnam xnam u) + WCon{} -> return ww + WApp a w1 w2 -> liftM2 (WApp a) (down w1) (down w2) + WType a t -> liftM (WType a) (down t) + + +instance Namify (Exp a) where + namify tnam xnam xx + = {-# SCC namify #-} + let down = namify tnam xnam + in case xx of + XVar a u -> liftM2 XVar (return a) (rewriteX tnam xnam u) + XCon{} -> return xx + + XLAM a b x + -> do (tnam', b') <- pushT tnam b + x' <- namify tnam' xnam x + return $ XLAM a b' x' + + XLam a b x + -> do (xnam', b') <- pushX tnam xnam b + x' <- namify tnam xnam' x + return $ XLam a b' x' + + XApp a x1 x2 + -> liftM3 XApp (return a) (down x1) (down x2) + + XLet a (LLet b x1) x2 + -> do x1' <- namify tnam xnam x1 + (xnam', b') <- pushX tnam xnam b + x2' <- namify tnam xnam' x2 + return $ XLet a (LLet b' x1') x2' + + XLet a (LRec bxs) x2 + -> do let (bs, xs) = unzip bxs + (xnam', bs') <- pushXs tnam xnam bs + xs' <- mapM (namify tnam xnam') xs + x2' <- namify tnam xnam' x2 + return $ XLet a (LRec (zip bs' xs')) x2' + + XLet a (LPrivate b mt bs) x2 + -> do (tnam', b') <- pushTs tnam b + (xnam', bs') <- pushXs tnam' xnam bs + x2' <- namify tnam' xnam' x2 + return $ XLet a (LPrivate b' mt bs') x2' + + XCase a x1 alts -> liftM2 (XCase a) (down x1) (mapM down alts) + XCast a c x -> liftM2 (XCast a) (down c) (down x) + XType a t -> liftM (XType a) (down t) + XWitness a w -> liftM (XWitness a) (down w) + + +instance Namify (Alt a) where + namify tnam xnam (AAlt PDefault x) + = liftM (AAlt PDefault) (namify tnam xnam x) + + namify tnam xnam (AAlt (PData u bs) x) + = do (xnam', bs') <- pushXs tnam xnam bs + x' <- namify tnam xnam' x + return $ AAlt (PData u bs') x' + + +instance Namify (Cast a) where + namify tnam xnam cc + = let down = namify tnam xnam + in case cc of + CastWeakenEffect eff -> liftM CastWeakenEffect (down eff) + CastPurify w -> liftM CastPurify (down w) + CastBox -> return CastBox + CastRun -> return CastRun + + +-- | Rewrite level-1 anonymous binders. +rewriteT :: Namifier s n + -> Bound n + -> State s (Bound n) + +rewriteT tnam u + = case u of + UIx i + -> case lookup i (zip [0..] (namifierStack tnam)) of + Just (BName n _) -> return $ UName n + _ -> return u + + _ -> return u + + +-- | Rewrite level-0 anonymous binders. +rewriteX :: Namifier s n + -> Namifier s n + -> Bound n + -> State s (Bound n) + +rewriteX _tnam xnam u + = case u of + UIx i + -> case lookup i (zip [0..] (namifierStack xnam)) of + Just (BName n _) + -> do return $ UName n + _ -> return u + + _ -> return u + + +-- Push ----------------------------------------------------------------------- +-- Chosing new names for anonymous binders and pushing them on the stack. + +-- | Push a level-0 binder on the stack. +-- When we do this we also rewrite any indices in its type annotation. +pushX :: Ord n + => Namifier s n + -> Namifier s n + -> Bind n + -> State s (Namifier s n, Bind n) + +pushX tnam xnam b + = do t' <- namify tnam xnam (typeOfBind b) + let b' = replaceTypeOfBind t' b + push xnam b' + + +-- | Push some level-0 binders on the stack. +-- When we do this we also rewrite their type annotations. +pushXs :: Ord n + => Namifier s n + -> Namifier s n + -> [Bind n] + -> State s (Namifier s n, [Bind n]) + +pushXs _tnam xnam [] + = return (xnam, []) + +pushXs tnam xnam (b:bs) + = do (xnam1, b') <- pushX tnam xnam b + (xnam2, bs') <- pushXs tnam xnam1 bs + return (xnam2, b' : bs') + + +-- | Push a level-1 binder on the stack. +pushT :: Ord n + => Namifier s n + -> Bind n + -> State s (Namifier s n, Bind n) +pushT = push + + +pushTs :: Ord n + => Namifier s n + -> [Bind n] + -> State s (Namifier s n, [Bind n]) +pushTs tnam [] = return (tnam, []) +pushTs tnam (b:bs) + = do (tnam1, b') <- pushT tnam b + (tnam2, bs') <- pushTs tnam1 bs + return (tnam2, b' : bs') + + +-- | Rewrite an anonymous binder and push it on the stack. +push :: Ord n + => Namifier s n + -> Bind n + -> State s (Namifier s n, Bind n) + +push nam b + = case b of + BAnon t + -> do n <- namifierNew nam (namifierEnv nam) b + let b' = BName n t + return ( nam { namifierStack = b' : namifierStack nam + , namifierEnv = Env.extend b (namifierEnv nam) } + , b' ) + _ -> return ( nam { namifierEnv = Env.extend b (namifierEnv nam) } + , b) diff --git a/DDC/Core/Transform/Prune.hs b/DDC/Core/Transform/Prune.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Prune.hs @@ -0,0 +1,213 @@ + +-- | Erase contained let-bindings that have no uses. +-- +-- Contained bindings are ones that do not perform effects that are +-- visible to anything in the calling context. This includes allocation +-- and read effects, but not writes or any globally visible effects. +-- +module DDC.Core.Transform.Prune + ( PruneInfo (..) + , pruneModule + , pruneX) +where +import DDC.Core.Analysis.Usage +import DDC.Core.Simplifier.Base +import DDC.Core.Transform.Reannotate +import DDC.Core.Transform.TransformUpX +import DDC.Core.Fragment +import DDC.Core.Check +import DDC.Core.Module +import DDC.Core.Exp +import DDC.Data.Pretty +import Data.Typeable +import Control.Monad.Writer (Writer, runWriter, tell) +import DDC.Core.Env.EnvX (EnvX) +import qualified Data.Map as Map +import qualified DDC.Core.Transform.SubstituteXX as S +import qualified DDC.Type.Exp.Simple as T +import qualified DDC.Type.Sum as TS +import qualified DDC.Core.Env.EnvT as EnvT +import Prelude hiding ((<$>)) + + +------------------------------------------------------------------------------- +-- | A summary of what the prune transform did. +data PruneInfo + = PruneInfo + { -- | How many let-bindings we erased. + infoBindingsErased :: Int } + deriving Typeable + + +instance Pretty PruneInfo where + ppr (PruneInfo remo) + = text "Prune:" + <$> indent 4 (vcat + [ text "Removed: " <> int remo]) + + +instance Monoid PruneInfo where + mempty = PruneInfo 0 + + mappend (PruneInfo r1) (PruneInfo r2) + = PruneInfo (r1 + r2) + + +------------------------------------------------------------------------------- +-- | Erase pure let-bindings in a module that have no uses. +pruneModule + :: (Show a, Show n, Ord n, Pretty n) + => Profile n -- ^ Profile of the language we're in + -> Module a n + -> Module a n + +pruneModule profile mm + -- If the language fragment has untracked effects then we can't do + -- the prune transform because we risk dropping statements with global + -- effects. + | not $ featuresTrackedEffects + $ profileFeatures profile + = mm + + | otherwise + = let env = moduleEnvX + (profilePrimKinds profile) + (profilePrimTypes profile) + (profilePrimDataDefs profile) + mm + in mm { moduleBody + = result $ pruneX profile env + $ moduleBody mm } + + +-- | Erase pure let-bindings in an expression that have no uses. +pruneX + :: (Show a, Show n, Ord n, Pretty n) + => Profile n -- ^ Profile of the language we're in + -> EnvX n -- ^ Type checker environment. + -> Exp a n + -> TransformResult (Exp a n) + +pruneX profile env xx + = {-# SCC pruneX #-} + let + (xx', info) + = transformTypeUsage profile env + (transformUpMX pruneTrans env) + xx + + progress (PruneInfo r) + = r > 0 + + in TransformResult + { result = xx' + , resultAgain = progress info + , resultProgress = progress info + , resultInfo = TransformInfo info } + + +-- The prune transform proper needs to have every expression annotated +-- with its type an effect, as well the variable usage map. +-- +-- We generate these annotations here then pass the result off to +-- deadCodeTrans to actually erase dead bindings. +-- +transformTypeUsage profile env trans xx + = let config = configOfProfile profile + rr = checkExp config env Recon DemandNone xx + in case fst rr of + Right (xx1, _, _) + -> let xx2 = usageX xx1 + (x', info) = runWriter (trans xx2) + x'' = reannotate (\(_, AnTEC { annotTail = a }) -> a) x' + in (x'', info) + + Left _ + -> error $ renderIndent + $ vcat [ text "ddc-core-simpl.Prune: core type error" ] + + +------------------------------------------------------------------------------- +-- | Annotations used by the dead-code trasnform. +type Annot a n + = (UsedMap n, AnTEC a n) + + +-- | Apply the dead-code transform to an annotated expression. +pruneTrans + :: Ord n + => EnvX n -- ^ Type checker environment. + -> Exp (Annot a n) n -- ^ Expression to transform. + -> Writer PruneInfo + (Exp (Annot a n) n) + +pruneTrans _ xx + = case xx of + XLet a@(usedMap, antec) (LLet b x1) x2 + | isUnusedBind b usedMap + , isContainedEffect $ annotEffect antec + -> do + -- We still need to substitute value into casts + let x2' = S.substituteXX b x1 x2 + + -- Record that we've erased a binding. + tell mempty {infoBindingsErased = 1} + + -- + return $ XCast a (weakEff antec) + $ x2' + + _ -> return xx + + where + weakEff antec + = CastWeakenEffect + $ T.crushEffect EnvT.empty + $ annotEffect antec + + +-- | Check whether this binder has no uses, +-- not including weakclo casts, beause we'll substitute the bound +-- expression directly into those. +isUnusedBind :: Ord n => Bind n -> UsedMap n -> Bool +isUnusedBind bb (UsedMap um) + = case bb of + BName n _ + -> case Map.lookup n um of + Just useds -> filterUsedInCasts useds == [] + Nothing -> True + + BNone _ -> True + _ -> False + + +filterUsedInCasts :: [Used] -> [Used] +filterUsedInCasts = filter notCast + where notCast UsedInCast = False + notCast _ = True + + +-- | A contained effect is one that is not visible to anything else +-- in the context. This is allocation and read effects, which are +-- not visible from outside the computation performing the effect. +isContainedEffect :: Ord n => Effect n -> Bool +isContainedEffect eff + = all contained + $ map T.takeTApps + $ sumList + $ T.crushEffect EnvT.empty eff + where + contained (c : _args) + = case c of + TCon (TyConSpec TcConAlloc) -> True + TCon (TyConSpec TcConDeepAlloc) -> True + TCon (TyConSpec TcConRead) -> True + TCon (TyConSpec TcConHeadRead) -> True + TCon (TyConSpec TcConDeepRead) -> True + _ -> False + + contained [] = False + + sumList (TSum ts) = TS.toList ts + sumList tt = [tt] + diff --git a/DDC/Core/Transform/Rewrite.hs b/DDC/Core/Transform/Rewrite.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Rewrite.hs @@ -0,0 +1,546 @@ + +-- | Apply rewrite rules. +module DDC.Core.Transform.Rewrite + ( RewriteRule(..) + , rewriteModule + , rewriteX) +where +import DDC.Data.Pretty +import DDC.Core.Exp.Annot as X +import DDC.Core.Module +import Data.Map (Map) +import DDC.Core.Simplifier.Base (TransformResult(..), TransformInfo(..)) +import qualified DDC.Core.Transform.AnonymizeX as A +import qualified DDC.Core.Transform.Rewrite.Disjoint as RD +import qualified DDC.Core.Transform.Rewrite.Env as RE +import qualified DDC.Core.Transform.Rewrite.Match as RM +import DDC.Core.Transform.Rewrite.Rule +import qualified DDC.Core.Transform.SubstituteXX as S +import qualified DDC.Type.Transform.SubstituteT as S +import qualified DDC.Core.Transform.BoundX as L +import qualified DDC.Type.Exp.Simple as T +import qualified Data.Map as Map +import qualified Data.Set as Set +import Data.Maybe +import Control.Monad +import Control.Monad.Writer (tell, runWriter) +import Data.List +import Data.Typeable +import Prelude hiding ((<$>)) + + +-- Log ------------------------------------------------------------------------ +-- | Tracks which rewrite rules fired. +data RewriteInfo + = RewriteInfo [RewriteLog] + deriving Typeable + +data RewriteLog + = LogRewrite String + | LogUnfold String + deriving Typeable + + +instance Pretty RewriteInfo where + ppr (RewriteInfo rules) + = text "Rules fired:" + <$> indent 4 (vcat $ map ppr rules) + + +instance Pretty RewriteLog where + ppr (LogRewrite name) = text "Rewrite: " <> text name + ppr (LogUnfold name) = text "Unfold: " <> text name + +isProgress = not . null + + +-- Rewrite -------------------------------------------------------------------- +-- | Apply rewrite rules to a module. +rewriteModule + :: (Show a, Show n, Ord n, Pretty n) + => [NamedRewriteRule a n] -- ^ Rewrite rule database. + -> Module a n -- ^ Rewrite in this module. + -> Module a n + +rewriteModule rules mm + = mm { moduleBody = result $ rewriteX' True rules $ moduleBody mm } + + +-- | Perform rewrites top-down, repeatedly. +rewriteX + :: (Show a, Show n, Ord n, Pretty n) + => [NamedRewriteRule a n] -- ^ Rewrite rules database. + -> Exp a n -- ^ Rewrite in this expression. + -> TransformResult (Exp a n) +rewriteX = rewriteX' False + + +-- | Repeatedly perform rewrites top-down. +-- Usually any names bound in @letrec@s disable rules, because the +-- new binding makes the old rule meaningless. +-- For modules we do not want to do this, since the rules for that module +-- are probably about the functions exported from the module. +-- In this case, we ignore the top-level bindings when checking for rule shadowing. +rewriteX' + :: (Show a, Show n, Ord n, Pretty n) + => Bool -- ^ Ignore top-level bindings when checking for shadowing? + -> [NamedRewriteRule a n] -- ^ Rewrite rules database. + -> Exp a n -- ^ Rewrite in this expression. + -> TransformResult (Exp a n) + +rewriteX' ignore_toplevel rules x0 + = {-# SCC rewriteX #-} + let (x,info) = runWriter $ go RE.empty x0 [] ignore_toplevel + in TransformResult + { result = x + , resultAgain = isProgress info + , resultProgress = isProgress info + , resultInfo = TransformInfo (RewriteInfo info) } + where + -- ISSUE #280: Rewrites should be done with the most specific rule. + -- The rewrite engine should apply the most specific rule, instead + -- of the first one that it finds that matches. If not, then we + -- should give some warning about overlapping rules. + -- + -- Look for rules in the list that match the given expression, + -- and apply the first one that matches. + rewrites env f args + = rewrites' rules env f args + + rewrites' [] _ f args + = return $ X.makeXAppsWithAnnots f args + + rewrites' ((n, rule) : rs) env f args + = case rewriteWithX rule env f args of + Nothing -> rewrites' rs env f args + Just x -> tell [LogRewrite n] >> go env x [] False + + + down env x + = go env x [] False + + + -- Decend into the expression, looking for applications that we + -- might be able to apply rewrites to. + go env (XApp a f arg) args _toplevel + = do arg' <- down env arg + go env f ((arg',a):args) False + + go env x@XVar{} args _toplevel + = rewrites env x args + + go env x@XCon{} args _toplevel + = rewrites env x args + + go env (XLAM a b e) args _toplevel + = do e' <- down (RE.lift b env) e + rewrites env (XLAM a b e') args + + go env (XLam a b e) args _toplevel + = do e' <- down (RE.extend b env) e + rewrites env (XLam a b e') args + + go env (XLet a l@(LRec _) e) args toplevel + = do -- Don't add the @letrec@'s bindings to the rule shadow list if we're at the top-level + let env' = if toplevel + then env + else RE.extendLets l env + l' <- goLets l env' + e' <- down env' e + rewrites env' (XLet a l' e') args + + go env (XLet a l e) args _toplevel + = do l' <- goLets l env + dh <- goDefHoles rules a l' e env down + rewrites env dh args + + go env (XCase a e alts) args _toplevel + = do e' <- down env e + alts' <- mapM (goAlts env) alts + rewrites env (XCase a e' alts') args + + go env (XCast a c e) args _toplevel + = do e' <- down env e + rewrites env (XCast a c e') args + + go env x@(XType{}) args _toplevel + = rewrites env x args + + go env x@(XWitness{}) args _toplevel + = rewrites env x args + + + goLets (LLet b e) ws + = do e' <- down ws e + return $ LLet b e' + + goLets (LRec bs) ws + = do bs' <- mapM (down ws) $ map snd bs + return $ LRec $ zip (map fst bs) bs' + + + goLets l _ + = return $ l + + goAlts ws (AAlt p e) + = do e' <- down ws e + return $ AAlt p e' + + +-- If definitions match the holes of any rules, +-- clean it up and record it for later. +-- Eg with this rule, +-- RULE unbox {box s} = s +-- +-- this expression: +-- let x = box (some expensive op) +-- in ... +-- +-- will be transformed to +-- let ^ = some expensive op +-- x = box ^0 +-- in ... +-- +goDefHoles rules a l@(LLet let_bind def) e env down + | (((sub, []), name, RewriteRule { ruleBinds = bs, ruleLeft = hole }):_) + <- checkHoles rules def env + + = let -- only get value-level bindings + bs' = filter (isBMValue . fst) bs + bas' = lookupFromSubst a bs' sub + + -- check if it looks like something has already been unfolded + isUIx x = case x of + XVar _ (UIx _) -> True + XVar _ (UPrim _ _) -> True + _ -> False + + already_done + = all isUIx $ map snd bas' + + -- find kind-values and sub those in as well + bsK' = filter ((== BMSpec) . fst) bs + basK = lookupFromSubst a bsK' sub + + basK' = concatMap (\(b,x) -> case X.takeXType x of + Just t -> [(b,t)] + Nothing-> []) basK + + -- surround whole expression with anon lets from sub + values = map (\(b,v) -> (BAnon (S.substituteTs basK' $ T.typeOfBind b), v)) + (reverse bas') + + -- replace 'def' with LHS-HOLE[sub => ^n] + anons = zipWith (\(b,_) i -> (b, XVar a (UIx i))) bas' [0..] + lets = map (\(b,v) -> LLet b v) values + + def' = S.substituteXArgs basK + $ S.substituteXArgs anons hole + + let_bind' = S.substituteTs basK' let_bind + lets' = lets ++ [LLet let_bind' def'] + + -- lift e by (length bas) + depth = case let_bind of + BAnon _ -> 1 + _ -> 0 + + e' = L.liftAtDepthX (length bas') depth e + + -- SAVE in wit env + env' = foldl (flip RE.extendLets) env lets' + + in if already_done + then do + e'' <- down (RE.extendLets l env) e + return $ XLet a l e'' + + else do + tell [LogUnfold name] + e'' <- down env' e' + return $ X.xLets a lets' e'' + + | otherwise + = do e' <- down (RE.extendLets l env) e + return $ XLet a l e' + +goDefHoles _rules a l e env down + = do e' <- down (RE.extendLets l env) e + return $ XLet a l e' + + +-- Match a let-definition against the holes in all the rules +checkHoles + :: (Show n, Show a, Ord n, Pretty n) + => [NamedRewriteRule a n] + -> Exp a n + -> RE.RewriteEnv a n + -> [ ( (RM.SubstInfo a n, [(Exp a n, a)]) + , String + , RewriteRule a n) ] + +checkHoles rules def ws + = let rules' = catMaybes $ map holeRule rules + (f,args) = X.takeXAppsWithAnnots def + + in catMaybes + $ map (\(name,r) -> fmap (\s -> (s,name,r)) + $ matchWithRule r ws f args RM.emptySubstInfo) + rules' + + +holeRule (name, rule@RewriteRule { ruleLeftHole = Just hole }) + = Just ( name + , rule { ruleLeft = hole + , ruleLeftHole = Nothing }) + +holeRule _ = Nothing + + +------------------------------------------------------------------------------- +-- | Perform rewrite rule on expression if a valid substitution exists, +-- and constraints are satisfied. +rewriteWithX + :: (Show n, Show a, Ord n, Pretty n) + => RewriteRule a n + -> RE.RewriteEnv a n + -> Exp a n + -> [(Exp a n, a)] + -> Maybe (Exp a n) + +rewriteWithX rule env f args + = do + let RewriteRule + { ruleBinds = binds + , ruleConstraints = constrs + , ruleRight = rhs + , ruleWeakEff = eff + , ruleWeakClo = _clo } + = rule + + -- Try to find a substitution for the left of the rule. + (m, rest) <- matchWithRule rule env f args RM.emptySubstInfo + + -- Check constraints, perform substitution and add weakens if necessary. + let a = X.annotOfExp f + + let bas2 = lookupFromSubst a binds m + let rhs2 = A.anonymizeX rhs + let (bas3,lets) = wrapLets a binds bas2 + let rhs3 = L.liftX (length lets) rhs2 + + -- Substitute bindings into the effect of the right of the rule. + let eff' = liftM (substT bas3) eff + + -- Substitute bindings into rule constraints and + -- check that they are all satisfied by the environment. + let constrs' = map (substT bas3) constrs + when (not $ all (satisfiedContraint env) constrs') + $ Nothing + + -- Build the rewritten expression. + let x' = X.xLets a lets + $ weakeff a eff' + $ S.substituteXArgs bas3 rhs3 + + -- Add the remaining arguments from the original expression + -- that weren't matched by rule + return $ X.makeXAppsWithAnnots x' rest + + +-- | Check whether we can satisfy this constraint using witnesses +-- in the rewrite nevironment. +satisfiedContraint :: Ord n => RE.RewriteEnv a n -> Type n -> Bool +satisfiedContraint env c + = RE.containsWitness c env + || RD.checkDisjoint c env + || RD.checkDistinct c env + + +-- | Wrap an expression in an effect weakning. +weakeff :: a -> Maybe (Effect n) + -> Exp a n -> Exp a n + +weakeff a meff x + = maybe x (\e -> XCast a (CastWeakenEffect e) x) meff + + +wrapLets + :: Ord n + => a + -> [(BindMode, Bind n)] -- ^ Variables bound by the rule. + -> [(Bind n, Exp a n)] -- ^ Substitution for the left of the rule. + -> ( [(Bind n, Exp a n)] + , [Lets a n]) + +wrapLets a binds bas + = let isMkLet (_, (BMValue i, _)) = i /= 1 + isMkLet _ = False + + (as, bs'') = partition isMkLet (bas `zip` binds) + as' = map fst as + bs' = map fst bs'' + + anons = zipWith (\(b,_) i -> (b, XVar a (UIx i))) as' [0..] + values = map (\(b,v) -> (BAnon (substT bs' $ T.typeOfBind b), v)) + (reverse as') + lets = map (\(b,v) -> LLet b v) values + + in (bs' ++ anons, lets) + + +-- | Substitute type bindings into a type. +substT :: Ord n => [(Bind n, Exp a n)] -> Type n -> Type n +substT bas x + = let sub = [(b, t) | (b, XType _ t) <- bas ] + in S.substituteTs sub x + + +------------------------------------------------------------------------------- +-- | Attempt to find a rewrite substitution to match expression against rule. +-- Returns substitution and the left-over arguments that weren't matched +-- against. +-- +-- matchWithRule +-- (RULE mapMapId [a b : *] (f : a -> b) (xs : List a). +-- map [:a b:] f (map [:a a:] id xs) +-- = map [:a b:] f xs) +-- map +-- [ [Int], [Int], (\x -> f), (map [:Int Int:] id [1,2,3]) ] +-- +-- env +-- +-- emptySubstInfo +-- ==> +-- Just ({a |-> Int, b |-> Int, f |-> (\x -> f), xs |-> [1,2,3] }, []) +-- +-- However if we had passed a substitution such as {a |-> Float} instead of +-- emptySubstInfo, it would not have matched. +-- +-- The environment is used for 'hole' rules, that can look up bound definitions +-- and match if inlining would let them, even when inlining won't occur. +-- +matchWithRule + :: (Show n, Show a, Ord n, Pretty n) + => RewriteRule a n -- ^ Rule to unify with. + -> RE.RewriteEnv a n -- ^ Environment to rewrite in, contains witnesses + -- for the constraints on rules. + -> Exp a n -- ^ Function-part of the expression to rewrite. + -> [(Exp a n, a)] -- ^ Arguments of expression to rewrite, with the + -- annotations we took from the XApp nodes. + -> RM.SubstInfo a n -- ^ Existing substitution to match with + + -> Maybe ( RM.SubstInfo a n + , [(Exp a n, a)]) + -- ^ Substitution map and remaining (unmatched) args + +-- Handle a rule without a hole. +matchWithRule + RewriteRule + { ruleBinds = binds + , ruleLeft = lhs + , ruleLeftHole = Nothing + , ruleFreeVars = free } + env f args sub + = do + -- Check that none of the free variables have been rebound. + when (any (flip RE.hasDef env) free) + $ Nothing + + -- Get names of all the variables bound by the rule. + -- This should always match because checked rules are guaranteed not to + -- have `BAnon` or `BNone` binders. + let Just vs + = liftM Set.fromList + $ sequence + $ map T.takeNameOfBind + $ map snd binds + + -- Split the left part of the rule in to the function part and its + -- arguments. + l:ls <- return $ X.takeXAppsAsList lhs + + -- Match the function part of the expression against + -- the function part of the rule. + sub' <- RM.match sub vs l f + + -- Match each of the expression arguments against + -- the arguments of the rule. + let go m [] rest + = do return $ (m, rest) + + go m (l':ls') ((r,_):rs) + = do m' <- RM.match m vs l' r + go m' ls' rs + + go _ _ _ + = Nothing + + go sub' ls args + + +-- Handle a rule with a hole. +-- An example rule with a holes is: +-- RULE (i : Int). unbox {box i} = i +matchWithRule + rule@(RewriteRule { ruleLeftHole = Just hole }) + env f args sub + + -- Try to match against entire rule with no inlining. + -- Eg (unbox (box 5)) + | a <- X.annotOfExp f + , lhs_full <- XApp a (ruleLeft rule) hole + , rule_full <- rule { ruleLeft = lhs_full, ruleLeftHole = Nothing} + , Just subst <- matchWithRule rule_full env f args sub + = Just subst + + -- Try to match against the part without the hole. + -- eg unifyWithRule (RULE (i : Int). unbox) (unbox x) + -- which will return a substitution (empty here), + -- and the leftover argument 'x'. + | rule_some <- rule { ruleLeftHole = Nothing } + , Just (sub', (XVar _ b, _) : as) + <- matchWithRule rule_some env f args sub + + -- See if the 'x' variable is let-bound in an outer scope + , Just d' <- RE.getDef b env + , (fd, ad) <- X.takeXAppsWithAnnots d' + + -- Match the hole part with the right of the 'x' binding. + -- This completes the match, so we merge this new substitution + -- with the one for the outer part of the rule. + , rule_hole <- rule { ruleLeft = hole, ruleLeftHole = Nothing } + , Just (subd, asd) <- matchWithRule rule_hole env fd ad sub' + = Just (subd, asd ++ as) + + -- rule_some didn't match properly: failure + | otherwise + = Nothing + + +------------------------------------------------------------------------------- +-- | Lookup a binding from a rewrite rule substitution. +-- +-- Eg: RULE [x : %] (x : Int x). ... +-- +lookupFromSubst + :: Ord n + => a + -> [(BindMode,Bind n)] + -> (Map n (Exp a n), Map n (Type n)) + -> [(Bind n, Exp a n)] + +lookupFromSubst a1 bs m + = let bas = catMaybes $ map (lookupX m) bs + in map (\(b, a) -> (A.anonymizeX b, A.anonymizeX a)) bas + + where lookupX (xs,_) (BMValue _, b@(BName n _)) + | Just x <- Map.lookup n xs + = Just (b, x) + + lookupX (_,tys) (BMSpec, b@(BName n _)) + | Just t <- Map.lookup n tys + = Just (b, XType a1 t) + + lookupX _ _ = Nothing + diff --git a/DDC/Core/Transform/Rewrite/Disjoint.hs b/DDC/Core/Transform/Rewrite/Disjoint.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Rewrite/Disjoint.hs @@ -0,0 +1,202 @@ +-- | Check whether two effects are non-interfering +module DDC.Core.Transform.Rewrite.Disjoint + ( checkDisjoint + , checkDistinct ) +where +import DDC.Core.Exp +import DDC.Type.Exp.Simple as T +import qualified DDC.Core.Transform.Rewrite.Env as RE +import qualified DDC.Type.Sum as Sum +import qualified DDC.Core.Env.EnvT as EnvT + + +-- | Check whether a disjointness property is true in the given +-- rewrite environment. +-- +-- Disjointness means that two effects do not interfere. +-- +-- Context is important because if two regions are known to be +-- distinct, reading from one and writing to another is valid. +-- If they have different names they may not be distinct. +-- +-- All read effects are disjoint with other reads. +-- +-- > Disjoint (Read r1) (Read r2) +-- > Disjoint (Read r1) (DeepRead a) +-- +-- Allocation effects are disjoint with everything. +-- +-- > Disjoint (Alloc r) (_) +-- +-- Atomic reads and write effects are disjoint if they are to distinct regions. +-- +-- > Distinct r1 r2 +-- > ----------------------------- +-- > Disjoint (Read r1) (Write r2) +-- +-- @DeepWrite@ effects are only disjoint with allocation effects, because +-- we don't know what regions it will write to. +-- +-- An effect sum is disjoint from some other effect if all its components are. +-- +-- > Disjoint f1 g /\ Disjoint f2 g +-- > ----------------------------- +-- > Disjoint (f1 + f2) g +-- +-- Disjointness is commutative. +-- +-- > Disjoint f g +-- > ------------ +-- > Disjoint g f +-- +-- Example: +-- +-- > checkDisjoint +-- > (Disjoint (Read r1 + Read r2) (Write r3)) +-- > [Distinct r1 r3, Distinct r2 r3] +-- > = True +-- +checkDisjoint + :: Ord n + => Type n -- ^ Type of property we want + -- eg @Disjoint e1 e2@ + -> RE.RewriteEnv a n -- ^ Environment we're rewriting in. + -> Bool + +checkDisjoint c env + -- The type must have the form "Disjoint e1 e2" + | [TCon (TyConWitness TwConDisjoint), fs, gs] <- takeTApps c + = and [ areDisjoint env g f + | f <- sumList $ T.crushEffect EnvT.empty fs + , g <- sumList $ T.crushEffect EnvT.empty gs ] + + | otherwise + = False + where sumList (TSum ts) = Sum.toList ts + sumList tt = [tt] + + +-- | Check whether two atomic effects are disjoint. +areDisjoint + :: Ord n + => RE.RewriteEnv a n + -> Effect n + -> Effect n + -> Bool + +areDisjoint env t1 t2 + -- Allocations are disjoint with everything. + | isSomeAllocEffect t1 + || isSomeAllocEffect t2 + = True + + -- All the read effects are disjoint with each other. + | isSomeReadEffect t1 + , isSomeReadEffect t2 + = True + + -- Combinations of reads and writes are disjoint + -- if the regions are distinct. + | TApp _ tR1 <- t1 + , TApp _ tR2 <- t2 + , (isReadEffect t1 && isWriteEffect t2) + || (isWriteEffect t1 && isReadEffect t2) + || (isWriteEffect t1 && isWriteEffect t2) + = areDistinct env tR1 tR2 + + -- All other effects are assumed to be interfering. + | otherwise = False + + +-- Distinct ------------------------------------------------------------------- +-- | Check whether a distintness property is true in the given +-- rewrite environment. +-- +-- Distinctness means that two regions do not alias. +-- +checkDistinct + :: Ord n + => Type n -- ^ Type of the property we want, + -- eg @Distinct r1 r2@ + -> RE.RewriteEnv a n -- ^ Environment we're rewriting in. + -> Bool + +checkDistinct c env + -- It's of the form "Distinct r q" + | (TCon (TyConWitness (TwConDistinct _)) : args) + <- takeTApps c + = all (uncurry $ areDistinct env) (combinations args) + + | otherwise + = False + + where combinations [] = [] + combinations (x:xs) = repeat x `zip` xs ++ combinations xs + + +-- | Check if two regions are distinct. +areDistinct + :: Ord n + => RE.RewriteEnv a n + -> Type n -> Type n -> Bool + +areDistinct env t1 t2 + | Just u1 <- takeBound t1 + , Just u2 <- takeBound t2 + = areDistinctBound env u1 u2 + + | otherwise + = False + where takeBound (TVar u) = Just u + takeBound (TCon (TyConBound u _)) = Just u + takeBound _ = Nothing + + +-- | Check whether two regions are distinct. +-- This version takes `Bounds` so we don't need to worry about +-- region constructors like R0# directly. +areDistinctBound + :: Ord n + => RE.RewriteEnv a n + -> Bound n -> Bound n -> Bool + +areDistinctBound env p q + -- If they are the same, they can't possibly be different + | p == q + = False + + -- If they're both named primitives (eg R0#, R1#) + -- we can just check name-equality, since can't be bound in lambdas + -- Or if they're both bound in letregions, we can check by name + -- (and we know names are different because that's an insta-fail) + | concrete p && concrete q + = True + + -- Check witness map for "Distinct p q" and vice versa + | any check $ RE.getWitnesses env + = True + + -- Otherwise not. + | otherwise + = False + + where -- Check if region is 'concrete' either a region handle (R0#) + -- or bound by a letregion in a higher scope. + concrete r + = case r of + UPrim _ _ -> True + _ -> RE.containsRegion r env + + check w + | (TCon (TyConWitness (TwConDistinct _)) : args) + <- takeTApps w + = rgn p `elem` args && rgn q `elem` args + + | otherwise + = False + + rgn b + = case b of + UPrim _ t -> TCon (TyConBound b t) + _ -> TVar b + diff --git a/DDC/Core/Transform/Rewrite/Env.hs b/DDC/Core/Transform/Rewrite/Env.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Rewrite/Env.hs @@ -0,0 +1,215 @@ +module DDC.Core.Transform.Rewrite.Env + ( RewriteEnv + , empty + , extend + , extendLets + , containsRegion + , containsWitness + , getWitnesses + , insertDef + , getDef + , hasDef + , lift + , liftValue) +where +import DDC.Core.Exp +import qualified DDC.Type.Exp.Simple as T +import qualified DDC.Type.Transform.BoundT as L +import qualified DDC.Core.Transform.BoundX as L +import Data.Maybe (fromMaybe, listToMaybe, isJust) + + +-- | A summary of the environment that we perform a rewrite in. +-- +-- As we decend into the program looking for expressions to rewrite, +-- we keep track of what information as been defined in the environment +-- in a `RewriteEnv`. +-- +-- When we go under an anonymous binder then we push a new outermost +-- list instead of lifting every element on the environment eagerly. +-- +data RewriteEnv a n + = RewriteEnv + { -- | Types of all witnesses in scope. + -- We use these to satisfy constraints on rewrite rules like Const r. + witnesses :: [[T.Type n]] + + -- | Names of letregion-bound regions: + -- this is interesting because they must be distinct. + , letregions :: [[Bind n]] + + -- | Assoc of known values + -- If going to inline them, they must only reference de bruijn binds + -- these are value-level bindings, so be careful lifting. + , defs :: [[RewriteDef a n]] } + deriving (Show,Eq) + + +type RewriteDef a n + = (Bind n, Maybe (Exp a n)) + + +-- | An empty environment. +empty :: RewriteEnv a n +empty = RewriteEnv [] [] [] + + +-- | Extend an environment with some lambda-bound binder (XLam) +-- Might be a witness. Don't count if it's a region. +extend :: Ord n => Bind n -> RewriteEnv a n -> RewriteEnv a n +extend b env + | T.isWitnessType (T.typeOfBind b) + = let ty = T.typeOfBind b + extend' (w:ws') = (ty:w) : ws' + extend' [] = [[ty]] + in liftValue b $ env { witnesses = extend' (witnesses env) } + + | otherwise + = insertDef b Nothing (liftValue b env) + + +-- | Extend an environment with the variables bount by these let-bindings. +-- +-- If it's a letregion, remember the region's name and any witnesses. +-- +extendLets :: Ord n => Lets a n -> RewriteEnv a n -> RewriteEnv a n +extendLets (LPrivate bs _mt cs) renv + = foldl (flip extend) (foldl extendB renv bs) cs + where + extendB (env@RewriteEnv{witnesses = ws, letregions = rs}) b + = case b of + BAnon{} + -> env { witnesses = [] : ws + , letregions = [b] : rs } + + BName{} + -> env { letregions = extend' b rs } + + BNone{} + -> env + + extend' b (r:rs') = (b:r) : rs' + extend' b [] = [[b]] + +extendLets (LLet b def) env + = insertDef b (Just def') (liftValue b env) + where def' = case b of + BAnon{} -> L.liftX 1 def + _ -> def + +extendLets (LRec bs) env + = foldl lift' env (map fst bs) + where lift' e b = insertDef b Nothing (liftValue b e) + + + +-- Witnesses ------------------------------------------------------------------ +-- | Check if the witness map in the given environment. +--- +-- This tries each set in turn, lowering the indices in c by 1 after each +-- unsuccessful match. If nothing matches then 'c' may end up with negative +-- indices, which will definiately not match anything else. +-- +containsWitness :: Ord n => Type n -> RewriteEnv a n -> Bool +containsWitness c env + = go c (witnesses env) + where go _ [] = False + go c' (w:ws) = c' `elem` w || go (L.liftT (-1) c') ws + + +-- | Get a list of all the witness types in an environment, +-- normalising their indices. +getWitnesses :: Ord n => RewriteEnv a n -> [Type n] +getWitnesses env + = go (witnesses env) 0 + where go [] _ = [] + go (w:ws) i = map (L.liftT i) w ++ go ws (i+1) + + +-- Regions -------------------------------------------------------------------- +-- | Check whether an environment contains the given region, +-- bound by a letregion. +containsRegion :: Ord n => Bound n -> RewriteEnv a n -> Bool +containsRegion r env + = go r (letregions env) + where + go _ [] + = False + + go (UIx 0) (w:_) + = any (T.boundMatchesBind (UIx 0)) w + + go (UIx n) (_:ws) + = go (UIx (n-1)) ws + + go (UName n) (w:ws) + = any (T.boundMatchesBind (UName n)) w || go r ws + + go (UPrim _ _) _ + = False + + +-- Defs ----------------------------------------------------------------------- +-- | Insert a rewrite definition into the environment. +insertDef :: Bind n -> Maybe (Exp a n) -> RewriteEnv a n -> RewriteEnv a n +insertDef b def env + = env { defs = extend' $ defs env } + where + extend' (r:rs') = ((b,def):r) : rs' + extend' [] = [[(b,def)]] + + +hasDef :: (Ord n, L.MapBoundX (Exp a) n) + => Bound n -> RewriteEnv a n -> Bool + +hasDef b env + = isJust $ getDef' b env + + +-- | Lookup the definition of some let-bound variable from the environment. +getDef :: (Ord n, L.MapBoundX (Exp a) n) + => Bound n + -> RewriteEnv a n + -> Maybe (Exp a n) +getDef b env + = fromMaybe Nothing $ getDef' b env + + +getDef' :: (Ord n, L.MapBoundX (Exp a) n) + => Bound n + -> RewriteEnv a n + -> Maybe (Maybe (Exp a n)) + +getDef' b env + = go b 0 (defs env) + where + go _ _ [] = Nothing + go b' i (w:ws) = match b' i w `orM` go (L.liftX (-1) b') (i+1) ws + + match b' i ds + = fmap (fmap $ L.liftX i) + $ listToMaybe + $ map snd + $ filter (T.boundMatchesBind b' . fst) ds + + orM (Just x) _ = Just x + orM Nothing y = y + + +-- | Raise all elements in witness map if binder is anonymous. +-- Only call with type binders: ie XLAM, not XLam +lift :: Bind n -> RewriteEnv a n -> RewriteEnv a n +lift b env@(RewriteEnv ws rs is) + = case b of + BAnon{} -> RewriteEnv ([]:ws) ([]:rs) is + _ -> env + + +-- | Raise all elements in definitions map if binder is anonymous +-- Use for *value* binders, not type binders. +liftValue :: Bind n -> RewriteEnv a n -> RewriteEnv a n +liftValue b env@(RewriteEnv ws rs is) + = case b of + BAnon{} -> RewriteEnv ws rs ([]:is) + _ -> env + diff --git a/DDC/Core/Transform/Rewrite/Error.hs b/DDC/Core/Transform/Rewrite/Error.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Rewrite/Error.hs @@ -0,0 +1,81 @@ +module DDC.Core.Transform.Rewrite.Error + ( Error (..) + , Side (..)) +where +import DDC.Core.Exp +import DDC.Core.Check () +import DDC.Core.Pretty +import qualified DDC.Core.Check as C + + +-- | What can go wrong when checking a rewrite rule. +data Error a n + -- | Error typechecking one of the expressions + = ErrorTypeCheck + { -- | What side of the rule the error was on. + errorSide :: Side + , errorExp :: Exp a n + , errorCheckError :: C.Error a n } + + -- | Error typechecking one of the expressions + | ErrorBadConstraint + { errorConstraint :: Type n } + + -- | Types don't match... + | ErrorTypeConflict + { errorTypeLhs :: (Type n, Effect n, Closure n) + , errorTypeRhs :: (Type n, Effect n, Closure n) } + + -- | No binders allowed in left-hand side (right is fine, eg @let@s) + | ErrorNotFirstOrder + { errorExp :: Exp a n } + + -- | All variables must be mentioned in left-hand side, + -- otherwise they won't get bound. + | ErrorVarUnmentioned + + -- | I don't want to deal with anonymous variables. + | ErrorAnonymousBinder + { errorBinder :: Bind n } + + +-- | What side of a rewrite rule we're talking about. +data Side + = Lhs | Rhs + + +instance Pretty Side where + ppr Lhs = text "lhs" + ppr Rhs = text "rhs" + + +instance (Pretty a, Pretty n, Show n, Eq n) + => Pretty (Error a n) where + ppr err + = case err of + ErrorTypeCheck s x e + -> vcat [ text "Can't typecheck " <> ppr s <> text ": " <> ppr e + , text "While checking " <> ppr x ] + + ErrorBadConstraint c + -> text "Bad constraint: " <> ppr c + + ErrorTypeConflict (tl,el,cl) (tr,er,cr) + -> vcat [ text "LHS and RHS have different types:" + , text "Type L: " <> ppr tl + , text "Type R: " <> ppr tr + , text "Eff L: " <> ppr el + , text "Eff R: " <> ppr er + , text "Clo L: " <> ppr cl + , text "Clo R: " <> ppr cr ] + + ErrorNotFirstOrder x + -> vcat [ text "No binders allowed in left-hand side." + , text "While checking " <> ppr x ] + + ErrorVarUnmentioned + -> text "All variables in rule should be mentioned in left-hand side." + + ErrorAnonymousBinder b + -> text "Anonymous binders, just give it a name: " <> ppr b + diff --git a/DDC/Core/Transform/Rewrite/Match.hs b/DDC/Core/Transform/Rewrite/Match.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Rewrite/Match.hs @@ -0,0 +1,213 @@ +-- | Create substitution to make (subst template) == target +module DDC.Core.Transform.Rewrite.Match + ( -- * Substitutions + SubstInfo + , emptySubstInfo + + -- * Matching + , match) +where +import DDC.Core.Exp +import Data.Set (Set) +import Data.Map (Map) +import qualified DDC.Type.Sum as Sum +import qualified DDC.Type.Transform.AnonymizeT as T +import qualified DDC.Core.Transform.AnonymizeX as T +import qualified DDC.Core.Transform.Reannotate as T +import qualified DDC.Type.Exp.Simple as T +import qualified Data.Map as Map +import qualified Data.Set as Set +import qualified DDC.Core.Env.EnvT as EnvT + + +------------------------------------------------------------------------------- +-- | Value and type substition. +type SubstInfo a n + = (Map n (Exp a n), Map n (Type n)) + +-- | An empty substition info. +emptySubstInfo :: SubstInfo a n +emptySubstInfo + = (Map.empty, Map.empty) + +lookupx n (xs,_) + = Map.lookup n xs + +insertx n x (xs,tys) + = (Map.insert n x xs, tys) + + +-- Match Exp ------------------------------------------------------------------ +-- | Create substitution to make (subst template) == target +-- Does not handle higher-order templates (ie ones with binders) +-- +-- @ match emptySubstInfo (Set.fromList [r1, r2, s]) +-- (stream [r1] (unstream [r2] s)) +-- (stream [R0#] (unstream [R1#] (someStream 23)) +-- +-- => { r1 |-> R0#, r2 |-> R1, s |-> someStream 23 } +-- @ +match :: (Show a, Show n, Ord n) + => SubstInfo a n -- ^ Current substitution + -> Set n -- ^ Variables we're interested in + -> Exp a n -- ^ Template expression. + -> Exp a n -- ^ Target expression. + -> Maybe (SubstInfo a n) + +-- Variables bound by the rule: restricted to just UName earlier. +match m bs (XVar _ (UName n)) r + | n `Set.member` bs + -- Check if it's already been matched + = case lookupx n m of + Nothing -> return $ insertx n r m + Just x + -> -- Check if they're equal. Anonymize so names don't matter. + -- Reannotate so annotations are ignored. + let x' = T.anonymizeX $ T.reannotate (const ()) x + r' = T.anonymizeX $ T.reannotate (const ()) r + in if x' == r' + then Just m + else Nothing + +match m _ (XVar _ v1) (XVar _ v2) + | v1 == v2 = Just m + +match m _ (XCon _ c1) (XCon _ c2) + | c1 == c2 = Just m + +match m bs (XApp _ x11 x12) (XApp _ x21 x22) + = do m' <- match m bs x11 x21 + match m' bs x12 x22 + +match m bs (XCast _ c1 x1) (XCast _ c2 x2) + | eqCast c1 c2 + = match m bs x1 x2 + +match (xs, tys) bs (XType _ t1) (XType _ t2) + = do tys' <- matchT t1 t2 bs tys + return (xs, tys') + +match m _ (XWitness _ w1) (XWitness _ w2) + | eqWit w1 w2 = return m + +match _ _ _ _ + = Nothing + + +eqCast :: Ord n => Cast a n -> Cast a n -> Bool +eqCast lc rc + = clean lc == clean rc + where clean c + = T.reannotate (const ()) + $ case c of + CastWeakenEffect eff -> CastWeakenEffect $ T.anonymizeT eff + CastPurify wit -> CastPurify wit + CastBox -> CastBox + CastRun -> CastRun + + +eqWit :: Ord n => Witness a n -> Witness a n -> Bool +eqWit lw rw + = T.reannotate (const ()) lw + == T.reannotate (const ()) rw + + +-- Types ---------------------------------------------------------------------- +type VarSet n = Set.Set n +type Subst n = Map.Map n (Type n) + + +-- | Try to find a simple substitution between two types. +-- Ignoring complicated effect sums. +-- Also ignoring TForall - checkRewriteRule outlaws foralls in the template, so it's safe. +-- Eg given template @a -> b@ and target @Int -> Float@, +-- returns substitution: +-- @{ a |-> Int, b |-> Float }@ +-- +matchT :: Ord n + => Type n -- ^ Template type. + -> Type n -- ^ Target type. + -> VarSet n -- ^ Only attempt to match these names. + -> Subst n -- ^ Already matched (or @Map.empty@) + -> Maybe (Subst n) + +matchT t1 t2 vs subst + = let t1' = unpackSumT $ T.crushSomeT EnvT.empty t1 + t2' = unpackSumT $ T.crushSomeT EnvT.empty t2 + in case (t1', t2') of + -- Constructor names must be equal. + -- + -- Will this still work when it's a TyConBound - basically same as TVar? + (TCon tc1, TCon tc2) + | tc1 == tc2 + -> Just subst + + -- Decend into applications. + (TApp t11 t12, TApp t21 t22) + -> matchT t11 t21 vs subst >>= matchT t12 t22 vs + + -- Sums are equivalent if all of their components are. + -- Very simple matching, only consider equivalent if both have same + -- length and in the same order. + -- + -- > (Read + Write + a) `matchT` (Read + Write + Alloc) + -- > = + -- > Just { a |-> Alloc } + -- but + -- > (Read + a + Write) `matchT` (Read + Write + Alloc) + -- > = + -- > Nothing + -- and + -- > (Read + Write + Alloc + a) `matchT` (Read + Write + Alloc) + -- > = + -- > Nothing + -- despite a valid substitution existing as + -- > { a |-> !0 } + -- + (TSum ts1, TSum ts2) + -> let ts1' = Sum.toList ts1 + ts2' = Sum.toList ts2 + + go (l:ls) (r:rs) s = matchT l r vs s >>= go ls rs + go _ _ s = Just s + in if length ts1' /= length ts2' + then Nothing + else go ts1' ts2' subst + + + -- If template is in variable set, push the target into substitution + (TVar (UName n), _) + | Set.member n vs + , Nothing <- Map.lookup n subst + -> Just $ Map.insert n t2' subst + + | Set.member n vs + , Just t1'' <- Map.lookup n subst + , T.equivT EnvT.empty t1'' t2' + -> Just subst + + -- Both are variables but it's not a template variable, + -- so it's only valid if they're equal. + (TVar (UName n), TVar v2) + | not $ Set.member n vs + , UName n == v2 + -> Just subst + + (TVar (UIx i), TVar v2) + | UIx i == v2 + -> Just subst + + (TVar (UPrim n t), TVar v2) + | UPrim n t == v2 + -> Just subst + + -- Otherwise the two are different + (_, _) -> Nothing + + +-- | Unpack single element sums into plain types. +unpackSumT :: Type n -> Type n +unpackSumT (TSum ts) + | [t] <- Sum.toList ts = t +unpackSumT tt = tt + diff --git a/DDC/Core/Transform/Rewrite/Parser.hs b/DDC/Core/Transform/Rewrite/Parser.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Rewrite/Parser.hs @@ -0,0 +1,130 @@ + +-- | Core language parser. +module DDC.Core.Transform.Rewrite.Parser + (pRule, pRuleMany) +where +import DDC.Core.Exp +import DDC.Core.Parser +import DDC.Core.Lexer.Tokens +import qualified DDC.Control.Parser as P +import qualified DDC.Type.Exp.Simple as T +import qualified DDC.Core.Transform.Rewrite.Rule as R + + +-- Rewrite Rules ---------------------------------------------------------------- +{- + [r1 r2 : %] (x : Int r1). + Const r1 => + addInt [:r1 r2 r1:] x (0 [r2] ()) = + x +-} +-- | Parse a rewrite rule. +pRule :: Ord n + => Context n -> Parser n (R.RewriteRule P.SourcePos n) +pRule c + = do bs <- pRuleBinders c + (cs,lhs) <- pRuleCsLhs c + hole <- pRuleHole c + pSym SEquals + rhs <- pExp c + + return $ R.mkRewriteRule bs cs lhs hole rhs + + +{- +add_zero_r + [r1 r2 : %] (x : Int r1). + Const r1 => + addInt [:r1 r2 r1:] x (0 [r2] ()) = + x; +add_zero_l + [r1 r2 : %] ... + ; +-} +-- | Parse many rewrite rules. +pRuleMany + :: Ord n + => Context n -> Parser n [(n,R.RewriteRule P.SourcePos n)] +pRuleMany c + = P.many (do + n <- pName + r <- pRule c + pSym SSemiColon + return (n,r)) + + +pRuleBinders + :: Ord n + => Context n -> Parser n [(R.BindMode,Bind n)] + +pRuleBinders c + = P.choice + [ do bs <- P.many1 (pBinders c) + pSym SDot + return $ concat bs + , return [] + ] + + +pRuleCsLhs + :: Ord n + => Context n -> Parser n ([Type n], Exp P.SourcePos n) +pRuleCsLhs c + = P.choice + [ do cs <- P.many1 $ P.try (do + cc <- pTypeApp c + pSym SArrowEquals + return cc) + lhs <- pExp c + return (cs,lhs) + , do lhs <- pExp c + return ([],lhs) + ] + + +pRuleHole + :: Ord n + => Context n -> Parser n (Maybe (Exp P.SourcePos n)) +pRuleHole c + = P.optionMaybe + $ do pSym SUnderscore + pSym SBraceBra + e <- pExp c + pSym SBraceKet + pSym SUnderscore + return e + + +-- | Parse rewrite binders +-- +-- Many of: +-- [BIND1 BIND2 .. BINDN : TYPE] +-- or (BIND : TYPE) +-- +pBinders + :: Ord n + => Context n -> Parser n [(R.BindMode, Bind n)] +pBinders c + = P.choice + [ pBindersBetween c R.BMSpec (pSym SSquareBra) (pSym SSquareKet) + , pBindersBetween c (R.BMValue 0) (pSym SRoundBra) (pSym SRoundKet) + ] + + +pBindersBetween + :: Ord n + => Context n + -> R.BindMode + -> Parser n a + -> Parser n a + -> Parser n [(R.BindMode,Bind n)] + +pBindersBetween c bm bra ket + = do bra + bs <- P.many1 pBinder + pTok (KOp ":") + t <- pType c + ket + return $ map (mk t) bs + where mk t b = (bm,T.makeBindFromBinder b t) + diff --git a/DDC/Core/Transform/Rewrite/Rule.hs b/DDC/Core/Transform/Rewrite/Rule.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Rewrite/Rule.hs @@ -0,0 +1,511 @@ +-- | Constructing and checking whether rewrite rules are valid +module DDC.Core.Transform.Rewrite.Rule + ( -- * Binding modes + BindMode (..) + , isBMSpec + , isBMValue + + , RewriteRule (..) + , NamedRewriteRule + + -- * Construction + , mkRewriteRule + , checkRewriteRule + , Error (..) + , Side (..)) +where +import DDC.Core.Transform.Rewrite.Error +import DDC.Core.Transform.Reannotate +import DDC.Core.Transform.TransformUpX +import DDC.Core.Exp.Annot +import DDC.Core.Pretty () +import DDC.Core.Collect +import DDC.Core.Pretty () +import DDC.Core.Env.EnvX (EnvX) +import DDC.Data.Pretty +import qualified DDC.Core.Analysis.Usage as U +import qualified DDC.Core.Check as C +import qualified DDC.Core.Collect as C +import qualified DDC.Core.Transform.SpreadX as S +import qualified DDC.Type.Env as T +import qualified DDC.Type.Exp.Simple as T +import qualified DDC.Type.Transform.SpreadT as S +import qualified Data.Map as Map +import qualified Data.Maybe as Maybe +import qualified Data.Set as Set +import qualified DDC.Type.Env as Env +import qualified DDC.Core.Env.EnvT as EnvT +import qualified DDC.Core.Env.EnvX as EnvX + +-- | A rewrite rule. For example: +-- +-- @ RULE [r1 r2 r3 : %] (x : Int r1) +-- . addInt [:r1 r2 r3:] x (0 [r2] () +-- = copyInt [:r1 r3:] x +-- @ +data RewriteRule a n + = RewriteRule + { -- | Variables bound by the rule. + ruleBinds :: [(BindMode, Bind n)] + + -- | Extra constraints on the rule. + -- These must all be satisfied for the rule to fire. + , ruleConstraints :: [Type n] + + -- | Left-hand side of the rule. + -- We match on this part. + , ruleLeft :: Exp a n + + -- | Extra part of left-hand side, + -- but allow this bit to be out-of-context. + , ruleLeftHole :: Maybe (Exp a n) + + -- | Right-hand side of the rule. + -- We replace the matched expression with this part. + , ruleRight :: Exp a n + + -- | Effects that are caused by the left but not the right. + -- When applying the rule we add an effect weakning to ensure + -- the rewritten expression has the same effects. + , ruleWeakEff :: Maybe (Effect n) + + -- | Closure that the left has that is not present in the right. + -- When applying the rule we add a closure weakening to ensure + -- the rewritten expression has the same closure. + , ruleWeakClo :: [Exp a n] + + -- | References to environment. + -- Used to check whether the rule is shadowed. + , ruleFreeVars :: [Bound n] + } deriving (Eq, Show) + + +type NamedRewriteRule a n + = (String, RewriteRule a n) + + +instance (Pretty n, Eq n) => Pretty (RewriteRule a n) where + ppr (RewriteRule bs cs lhs hole rhs _ _ _) + = pprBinders bs <> pprConstrs cs <> ppr lhs <> pprHole <> text " = " <> ppr rhs + where pprBinders [] = text "" + pprBinders bs' = foldl1 (<>) (map pprBinder bs') <> text ". " + + pprBinder (BMSpec, b) = text "[" <> ppr b <> text "] " + pprBinder (BMValue _, b) = text "(" <> ppr b <> text ") " + + pprConstrs [] = text "" + pprConstrs (c:cs') = ppr c <> text " => " <> pprConstrs cs' + + pprHole + | Just h <- hole + = text " {" <> ppr h <> text "}" + + | otherwise + = text "" + + +-- BindMode ------------------------------------------------------------------- +-- | Binding level for the binders in a rewrite rule. +data BindMode + -- | Level-1 binder (specs) + = BMSpec + + -- | Level-0 binder (data values and witnesses) + | BMValue Int -- ^ number of usages + deriving (Eq, Show) + + +-- | Check if a `BindMode` is a `BMSpec`. +isBMSpec :: BindMode -> Bool +isBMSpec BMSpec = True +isBMSpec _ = False + + +-- | Check if a `BindMode` is a `BMValue`. +isBMValue :: BindMode -> Bool +isBMValue (BMValue _) = True +isBMValue _ = False + + +-- Make ----------------------------------------------------------------------- +-- | Construct a rewrite rule, but do not check if it's valid. +-- +-- You then need to apply 'checkRewriteRule' to check it. +-- +mkRewriteRule + :: [(BindMode,Bind n)] -- ^ Variables bound by the rule. + -> [Type n] -- ^ Extra constraints on the rule. + -> Exp a n -- ^ Left-hand side of the rule. + -> Maybe (Exp a n) -- ^ Extra part of left, can be out of context. + -> Exp a n -- ^ Right-hand side (replacement) + -> RewriteRule a n + +mkRewriteRule bs cs lhs hole rhs + = RewriteRule bs cs lhs hole rhs Nothing [] [] + + +-- Check ---------------------------------------------------------------------- +-- | Take a rule, make sure it's valid and fill in type, closure and effect +-- information. +-- +-- The left-hand side of rule can't have any binders (lambdas, lets etc). +-- +-- All binders must appear in the left-hand side, otherwise they would match +-- with no value. +-- +-- Both sides must have the same types, but the right can have fewer effects +-- and smaller closure. +-- +-- We don't handle anonymous binders on either the left or right. +-- +checkRewriteRule + :: (Show a, Ord n, Show n, Pretty n) + => C.Config n -- ^ Type checker config. + -> EnvX n -- ^ Type checker environment. + -> RewriteRule a n -- ^ Rule to check + -> Either (Error a n) + (RewriteRule (C.AnTEC a n) n) + +checkRewriteRule config env + (RewriteRule bs cs lhs hole rhs _ _ _) + = do + -- Extend the environments with variables bound by the rule. + let (env', bs') = extendBinds bs env + let kenv' = EnvX.kindEnvOfEnvX env' + let csSpread = map (S.spreadT kenv') cs + + -- Check that all constraints are valid types. + mapM_ (checkConstraint config) csSpread + + -- Typecheck, spread and annotate with type information + (lhs', _, _) + <- checkExp config env' Lhs lhs + + -- If the extra left part is there, typecheck and annotate it. + hole' <- case hole of + Just h + -> do (h',_,_) <- checkExp config env' Lhs h + return $ Just h' + + Nothing -> return Nothing + + -- Build application from lhs and the hole so we can check its + -- type against rhs + let a = annotOfExp lhs + let lhs_full = maybe lhs (XApp a lhs) hole + + -- Check the full left hand side. + (lhs_full', tLeft, effLeft) + <- checkExp config env' Lhs lhs_full + + -- Check the full right hand side. + (rhs', tRight, effRight) + <- checkExp config env' Rhs rhs + + -- Check that types of both sides are equivalent. + let err = ErrorTypeConflict + (tLeft, effLeft, tBot kClosure) + (tRight, effRight, tBot kClosure) + + checkEquiv tLeft tRight err + + -- Check the effect of the right is smaller than that + -- of the left, and add a weakeff cast if nessesary + effWeak <- makeEffectWeakening T.kEffect effLeft effRight err + + -- Check that the closure of the right is smaller than that + -- of the left, and add a weakclo cast if nessesary. + cloWeak <- makeClosureWeakening config env' lhs_full' rhs' + + -- Check that all the bound variables are mentioned + -- in the left-hand side. + checkUnmentionedBinders bs' lhs_full' + + -- No BAnons allowed. + -- We don't handle deBruijn binders. + checkAnonymousBinders bs' + + -- No lets or lambdas in left-hand side. + -- We can't match against these. + checkValidPattern lhs_full + + -- Count how many times each binder is used in the right-hand side. + bs'' <- countBinderUsage bs' rhs + + -- Get the free variables of the rule. + let binds = Set.fromList + $ Maybe.catMaybes + $ map (T.takeSubstBoundOfBind . snd) bs + + let freeVars = Set.toList + $ (C.freeX T.empty lhs_full' + `Set.union` C.freeX T.empty rhs) + `Set.difference` binds + + return $ RewriteRule + bs'' csSpread + lhs' hole' rhs' + effWeak cloWeak + freeVars + + +-- | Extend kind and type environments with a rule's binders. +-- Which environment a binder goes into depends on its BindMode. +-- Also return list of binders which have been spread. +extendBinds + :: Ord n + => [(BindMode, Bind n)] + -> EnvX n + -> (EnvX n, [(BindMode, Bind n)]) + +extendBinds binds env0 + = go binds env0 [] + where + go [] env acc + = (env, acc) + + go ((bm,b):bs) env acc + = let kenv = EnvX.kindEnvOfEnvX env + tenv = EnvX.typeEnvOfEnvX env + b' = S.spreadX kenv tenv b + env' = case bm of + BMSpec -> EnvX.extendT b' env + BMValue _ -> EnvX.extendX b' env + + in go bs env' (acc ++ [(bm,b')]) + + +-- | Type check the expression on one side of the rule. +checkExp + :: (Show a, Ord n, Show n, Pretty n) + => C.Config n -- ^ Type checker config. + -> EnvX n -- ^ Type checker environment. + -> Side -- ^ Side that the expression appears on for errors. + -> Exp a n -- ^ Expression to check. + -> Either (Error a n) + (Exp (C.AnTEC a n) n, Type n, Effect n) + +checkExp defs env side xx + = let kenv = EnvX.kindEnvOfEnvX env + tenv = EnvX.typeEnvOfEnvX env + xx' = S.spreadX kenv tenv xx + + in case fst $ C.checkExp defs env C.Recon C.DemandNone xx' of + Left err -> Left $ ErrorTypeCheck side xx' err + Right rhs -> return rhs + + +-- | Type check a constraint on the rule. +checkConstraint + :: (Ord n, Show n, Pretty n) + => C.Config n + -> Type n -- ^ The constraint type to check. + -> Either (Error a n) (Kind n) + +checkConstraint config tt + = case C.checkSpec config tt of + Left _err -> Left $ ErrorBadConstraint tt + Right (_, k) + | T.isWitnessType tt -> return k + | otherwise -> Left $ ErrorBadConstraint tt + + +-- | Check equivalence of types or error +checkEquiv + :: Ord n + => Type n -- ^ Type of left of rule. + -> Type n -- ^ Type of right of rule. + -> Error a n -- ^ Error to report if the types don't match. + -> Either (Error a n) () + +checkEquiv tLeft tRight err + | T.equivT EnvT.empty tLeft tRight + = return () + | otherwise = Left err + + +-- Weaken --------------------------------------------------------------------- +-- | Make the effect weakening for a rule. +-- This contains the effects that are caused by the left of the rule +-- but not the right. +-- If the right has more effects than the left then return an error. +-- +makeEffectWeakening + :: Ord n + => Kind n -- ^ Should be the effect kind. + -> Effect n -- ^ Effect of the left of the rule. + -> Effect n -- ^ Effect of the right of the rule. + -> Error a n -- ^ Error to report if the right is bigger. + -> Either (Error a n) (Maybe (Type n)) + +makeEffectWeakening k effLeft effRight onError + -- When the effect of the left matches that of the right + -- then we don't have to do anything else. + | T.equivT EnvT.empty effLeft effRight + = return Nothing + + -- When the effect of the right is smaller than that of + -- the left then we need to wrap it in an effect weaking + -- so the rewritten expression retains its original effect. + | T.subsumesT EnvT.empty k effLeft effRight + = return $ Just effLeft + + -- When the effect of the right is more than that of the left + -- then this is an error. The rewritten expression can't have + -- can't have more effects than the source. + | otherwise + = Left onError + + +-- | Make the closure weakening for a rule. +-- This contains a closure term for all variables that are present +-- in the left of a rule but not in the right. +-- +makeClosureWeakening + :: (Ord n, Pretty n, Show n) + => C.Config n -- ^ Type-checker config + -> EnvX n -- ^ Type checker environment. + -> Exp (C.AnTEC a n) n -- ^ Expression on the left of the rule. + -> Exp (C.AnTEC a n) n -- ^ Expression on the right of the rule. + -> Either (Error a n) + [Exp (C.AnTEC a n) n] + +makeClosureWeakening config env lhs rhs + = let lhs' = removeEffects config env lhs + supportLeft = support Env.empty Env.empty lhs' + daLeft = supportDaVar supportLeft + wiLeft = supportWiVar supportLeft + spLeft = supportSpVar supportLeft + + rhs' = removeEffects config env rhs + supportRight = support Env.empty Env.empty rhs' + daRight = supportDaVar supportRight + wiRight = supportWiVar supportRight + spRight = supportSpVar supportRight + + a = annotOfExp lhs + + in Right + $ [XVar a u + | u <- Set.toList $ daLeft `Set.difference` daRight ] + + ++ [XWitness a (WVar a u) + | u <- Set.toList $ wiLeft `Set.difference` wiRight ] + + ++ [XType a (TVar u) + | u <- Set.toList $ spLeft `Set.difference` spRight ] + + +-- | Replace all effects with !0. +-- This is done so that when @makeClosureWeakening@ finds free variables, +-- it ignores those only mentioned in effects. +removeEffects + :: (Ord n, Pretty n, Show n) + => C.Config n -- ^ Type-checker config + -> EnvX n -- ^ Type checker environment. + -> Exp a n -- ^ Target expression - has all effects replaced with bottom. + -> Exp a n + +removeEffects config + = transformUpX remove + where + remove _env x + + | XType a et <- x + , Right (_, k) <- C.checkSpec config et + , T.isEffectKind k + = XType a $ T.tBot T.kEffect + + | otherwise + = x + + +-- Structural Checks ---------------------------------------------------------- +-- | Check for rule variables that have no uses. +checkUnmentionedBinders + :: Ord n + => [(BindMode, Bind n)] + -> Exp (C.AnTEC a n) n + -> Either (Error a n) () + +checkUnmentionedBinders bs expr + = let used = C.freeX T.empty expr `Set.union` C.freeT T.empty expr + + binds = Set.fromList + $ Maybe.catMaybes + $ map (T.takeSubstBoundOfBind . snd) bs + + in if binds `Set.isSubsetOf` used + then return () + else Left ErrorVarUnmentioned + + +-- | Check for anonymous binders in the rule. We don't handle these. +checkAnonymousBinders + :: [(BindMode, Bind n)] + -> Either (Error a n) () + +checkAnonymousBinders bs + | (b:_) <- filter T.isBAnon $ map snd bs + = Left $ ErrorAnonymousBinder b + + | otherwise + = return () + + +-- | Check whether the form of the left-hand side of the rule is valid +-- we can only match against nested applications, and not general +-- expressions containing let-bindings and the like. +checkValidPattern :: Exp a n -> Either (Error a n) () +checkValidPattern expr + = go expr + where go (XVar _ _) = return () + go (XCon _ _) = return () + go x@(XLAM _ _ _) = Left $ ErrorNotFirstOrder x + go x@(XLam _ _ _) = Left $ ErrorNotFirstOrder x + go (XApp _ l r) = go l >> go r + go x@(XLet _ _ _) = Left $ ErrorNotFirstOrder x + go x@(XCase _ _ _) = Left $ ErrorNotFirstOrder x + go (XCast _ _ x) = go x + go (XType a t) = go_t a t + go (XWitness _ _) = return () + + go_t _ (TVar _) = return () + go_t _ (TCon _) = return () + go_t a t@(TAbs _ _) = Left $ ErrorNotFirstOrder (XType a t) + go_t a (TApp l r) = go_t a l >> go_t a r + go_t a t@(TForall _ _) = Left $ ErrorNotFirstOrder (XType a t) + go_t _ (TSum _) = return () + + +-- | Count how many times each binder is used in right-hand side. +countBinderUsage + :: Ord n + => [(BindMode, Bind n)] + -> Exp a n + -> Either (Error a n) [(BindMode, Bind n)] + +countBinderUsage bs x + = let U.UsedMap um + = fst $ annotOfExp $ U.usageX x + + get (BMValue _, BName n t) + = (BMValue + $ length + $ Maybe.fromMaybe [] + $ Map.lookup n um + , BName n t) + + get b + = b + + in return $ map get bs + + +-- | Allow the expressions and anything else with annotations to be reannotated +instance Reannotate RewriteRule where + reannotate f (RewriteRule bs cs lhs hole rhs eff clo fv) + = RewriteRule bs cs (re lhs) (fmap re hole) (re rhs) eff (map re clo) fv + where + re = reannotate f + diff --git a/DDC/Core/Transform/Snip.hs b/DDC/Core/Transform/Snip.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Snip.hs @@ -0,0 +1,350 @@ + +-- | Snip out nested applications. +module DDC.Core.Transform.Snip + ( Snip (..) + , Config (..) + , configZero) +where +import DDC.Core.Analysis.Arity +import DDC.Core.Module +import DDC.Core.Exp.Annot +import qualified DDC.Core.Transform.BoundX as L +import qualified DDC.Type.Exp.Simple as T + + +------------------------------------------------------------------------------- +-- | Snipper configuration. +data Config + = Config + { -- | Introduce new bindings for over-applied functions. + configSnipOverApplied :: Bool + + -- | Ensure the body of a let-expression is a variable. + , configSnipLetBody :: Bool + + -- | Treat lambda abstractions as atomic, + -- and don't snip them. + , configPreserveLambdas :: Bool + } + + +-- | Snipper configuration with all flags set to False. +configZero :: Config +configZero + = Config + { configSnipOverApplied = False + , configSnipLetBody = False + , configPreserveLambdas = False } + + +------------------------------------------------------------------------------- +-- | Class of things that can have things snipped out of them. +class Snip (c :: * -> *) where + + -- | Snip out nested applications as anonymous bindings. + -- + -- @ + -- f (g x) (h y) + -- ==> let ^ = g x in ^ = h y in f ^1 ^0 + -- @ + snip :: Ord n => Config -> c n -> c n + + +instance Snip (Module a) where + snip config mm + = let arities = aritiesOfModule mm + body' = snipX config arities (moduleBody mm) [] + in mm { moduleBody = body' } + + +instance Snip (Exp a) where + snip config x + = snipX config emptyArities x [] + + +-- | Convert an expression into A-normal form. +snipX :: Ord n + => Config + -> Arities n -- ^ Arities of functions in environment. + -> Exp a n -- ^ Expression to transform. + -> [(Exp a n, a)] -- ^ Arguments being applied to current expression. + -> Exp a n + +snipX config arities x args + -- For applications, remember the argument that the function is being + -- applied to, and decend into the function part. + -- This unzips application nodes as we decend into the tree. + | XApp a fun arg <- x + = snipX config arities fun + $ (snipX config arities arg [], a) : args + + -- Some non-application node with no arguments. + | null args + = enterX config arities x + + -- Some non-application node being applied to arguments. + | otherwise + = let x' = enterX config arities x + in buildNormalisedApp config arities x' args + +-- Enter into a non-application. +enterX config arities xx + = let down ars e + = snipX config (extendsArities arities ars) e [] + + in case xx of + -- The snipX function shouldn't have called us with an XApp. + XApp{} + -> error "ddc-core-simpl.Snip: snipX shouldn't give us an XApp" + + -- leafy constructors + XVar{} -> xx + XCon{} -> xx + XType{} -> xx + XWitness{} -> xx + + -- lambdas + XLAM a b e + -> XLAM a b (down [(b,0)] e) + + XLam a b e + -> XLam a b (down [(b,0)] e) + + -- non-recursive let + XLet a (LLet b x1) x2 + -> let x1' = down [] x1 + x2' = snipLetBody config a + $ down [(b, arityOfExp' x1')] x2 + in XLet a (LLet b x1') x2' + + -- recursive let + XLet a (LRec lets) x2 + -> let bs = map fst lets + xs = map snd lets + ars = zip bs (map arityOfExp' xs) + xs' = map (down ars) xs + x2' = snipLetBody config a $ down ars x2 + in XLet a (LRec $ zip bs xs') x2' + + -- private, just make sure we record bindings with dummy val. + XLet a (LPrivate b mt bs) x2 + -> let ars = zip bs (repeat 0) + x2' = snipLetBody config a $ down ars x2 + in XLet a (LPrivate b mt bs) x2' + + -- case + -- Split out non-atomic discriminants into their own bindings. + XCase a e alts + | isAtom e + -> let e' = down [] e + alts' = map (\(AAlt pat ae) + -> AAlt pat (down (aritiesOfPat pat) ae)) alts + in XCase a e' alts' + + | otherwise + -> let e' = down [] e + alts' = [AAlt pat (down (aritiesOfPat pat) ae) + | AAlt pat ae <- alts] + xBody' = snipLetBody config a + $ XCase a (XVar a $ UIx 0) + (map (L.liftX 1) alts') + + in XLet a (LLet (BAnon (T.tBot T.kData)) e') + xBody' + + -- cast + XCast a c e + -> XCast a c (down [] e) + + +-- | Build an A-normalised application of some functional expression to +-- its arguments. Atomic arguments are applied directly, while +-- non-atomic arguments are bound via let-expressions, then the +-- associated let-bound variable is passed to the function. +buildNormalisedApp + :: Ord n + => Config -- ^ Snipper config. + -> Arities n -- ^ environment, arities of bound variables + -> Exp a n -- ^ function + -> [(Exp a n,a)] -- ^ arguments being applied to current expression + -> Exp a n + +buildNormalisedApp _ _ f0 [] = f0 +buildNormalisedApp config arities f0 args@( (_, annot) : _) + = make annot f0 args + where + tBot' = T.tBot T.kData + + -- Lookup the arity of the function. + f0Arity + = case f0 of + XVar _ b + | Just arity <- getArity arities b + -> max arity 1 + + _ -> max (arityOfExp' f0) 1 + + -- Make a normalised function application. + make a xFun xsArgs + + -- The function part is already atomic. + | isAtom xFun + = buildNormalisedFunApp config a f0Arity xFun xsArgs + + -- The function part is not atomic, + -- so we need to add an outer-most let-binding for it. + | otherwise + = XLet a (LLet (BAnon tBot') xFun) + (snipLetBody config a + $ buildNormalisedFunApp config a f0Arity + (XVar a (UIx 0)) + [ (L.liftX 1 x, a') | (x, a') <- xsArgs]) + + +-- | Build an A-normalised application of some functional expression to +-- its arguments. Atomic arguments are applied directly, while +-- on-atomic arguments are bound via let-expressions, then the +-- associated let-bound variable is passed to the function. +-- +-- Unlike the `buildNormalisedFunApp` function above, this one +-- wants the function part to be normalised as well. +buildNormalisedFunApp + :: Config -- ^ Snipper configuration. + -> a -- ^ Annotation to use. + -> Int -- ^ Arity of the function part. + -> Exp a n -- ^ Function part. + -> [(Exp a n, a)] -- ^ Arguments to apply + -> Exp a n + +buildNormalisedFunApp config an funArity xFun xsArgs + = let tBot' = T.tBot T.kData + + -- Split arguments into the already atomic ones, + -- and the ones we need to introduce let-expressions for. + argss = splitArgs config xsArgs + + -- Collect up the new let-bindings. + xsLets = [ (x, a) + | (_, a, _, Just x) <- argss] + + -- The total number of new let-bindings. + nLets = length xsLets + + -- Lift indices in each binding over the bindings before it. + xsLets' = [ (L.liftX n x, a) + | (x, a) <- xsLets + | (n :: Int) <- [0..] ] + + -- Lift indices in the function over the bindings before it. + xFun' = L.liftX nLets xFun + + -- Collect up the new function arguments. + -- If the argument was already atomic then we have to lift + -- its indices past the new let bindings we're about to add. + -- Otherwise it's a reference to one of the bindings directly. + xsArgs' = [if liftMe + then (L.liftX nLets xArg, a) + else (xArg, a) + | (xArg, a, liftMe, _) <- argss] + + -- Construct the new function application. + xFunApps + + -- If the function is over-applied then create an intermediate + -- binding that saturates it, then apply the extra arguments + -- separately. + | configSnipOverApplied config + , length xsArgs' > funArity + , (xsSat, xsOver) <- splitAt funArity xsArgs' + = XLet an (LLet (BAnon tBot') + (makeXAppsWithAnnots xFun' xsSat)) + (snipLetBody config an + $ makeXAppsWithAnnots + (XVar an (UIx 0)) + [ (L.liftX 1 x, a) | (x, a) <- xsOver ]) + + -- Function has the correct number of arguments, + -- or is partially applied. + | otherwise + = makeXAppsWithAnnots + xFun' + xsArgs' + + -- Wrap the function application in the let-bindings + -- for its arguments. + in case xsLets' of + [] -> xFunApps + _ -> foldr (\(x, a) x' -> XLet a x x') + (snipLetBody config an xFunApps) + [ (LLet (BAnon tBot') x, a) + | (x, a) <- xsLets' ] + + +-- | Sort function arguments into either the atomic ones, +-- or compound ones. +splitArgs + :: Config + -> [(Exp a n, a)] + -> [( Exp a n -- Expression to use as the new argument. + , a -- Annoation for the argument application. + , Bool -- Whether this argument was already atomic. + , Maybe (Exp a n))] -- New expression to let-bind. + +splitArgs config args + = reverse $ go 0 $ reverse args + where + go _n [] = [] + go n ((xArg, a) : xsArgs) + | isAtom xArg + = (xArg, a, True, Nothing) : go n xsArgs + + | configPreserveLambdas config + , isXLam xArg || isXLAM xArg + = (xArg, a, True, Nothing) : go n xsArgs + + | otherwise + = (XVar a (UIx n), a, False, Just xArg) : go (n + 1) xsArgs + + +-- | If `snipLetResults` is set and this is not an atomic expression then +-- introduce a new binding for it. +snipLetBody :: Config -> a -> Exp a n -> Exp a n +snipLetBody config a xx + | configSnipLetBody config + , not (isAtom xx) + , not (isXLet xx) + = let tBot' = T.tBot T.kData + in XLet a (LLet (BAnon tBot') xx) + (XVar a (UIx 0)) + + | otherwise + = xx + + +-- | Check if an expression needs a binding, or if it's simple enough to be +-- applied as-is. +isAtom :: Exp a n -> Bool +isAtom xx + = case xx of + XVar{} -> True + XCon{} -> True + XType{} -> True + XWitness{} -> True + + -- Keep applications of variables to their types together. +-- XApp _ x1 XType{} -> isAtom x1 + + -- Casts are ignored by code generator, so we can leave them in if + -- their subexpression is normal + XCast _ _ x -> isAtom x + _ -> False + + +-- | Take the arity of an expression, +-- returning 0 for XType and XWitness. +arityOfExp' :: Ord n => Exp a n -> Int +arityOfExp' xx + = case arityOfExp xx of + Nothing -> 0 + Just a -> a + diff --git a/DDC/Core/Transform/Thread.hs b/DDC/Core/Transform/Thread.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Thread.hs @@ -0,0 +1,413 @@ + +-- | Thread a state token through calls to given functions. +-- +-- ASSUMPTIONS: +-- * Program is a-normalized and fully named. +-- +module DDC.Core.Transform.Thread + ( Thread (..) + , Config (..) + , injectStateType) +where +import DDC.Core.Module +import DDC.Core.Exp.Annot +import DDC.Data.Pretty +import DDC.Core.Transform.Reannotate +import DDC.Core.Check (AnTEC (..)) +import DDC.Type.Env (KindEnv, TypeEnv) +import qualified DDC.Type.Env as Env +import qualified DDC.Core.Check as Check + + +------------------------------------------------------------------------------- +-- | Configuration for the Thread transform. +data Config a n + = Config + { -- | Config for the type checker. + -- We need to reconstruct the type of the result of stateful + -- functions when bundling them into the tuple that holds the + -- state token. + configCheckConfig :: Check.Config n + + -- | Function to decide which top-level bindings are stateful and + -- need the state token threaded through them. If the binding with + -- the given name is stateful then the function should return the + -- new type for the binding that accepts and returns the state token. + , configThreadMe :: n -> Type n -> Maybe (Type n) + + -- | Type of the state token to use. + , configTokenType :: Type n + + -- | Type that represents a missing value. + -- If a stateful function returns a void then our thread transform + -- rewrites it to return the state token, instead of a tuple + -- that contains the token as well as a void value. + , configVoidType :: Type n + + -- | Wrap a type with the world token. + -- eg change Int to (World#, Int) + , configWrapResultType :: Type n -> Type n + + -- | Wrap a result expression with the state token. + -- The function is given the types of the world token and result, + -- then the expressions for the same. + , configWrapResultExp :: Exp (AnTEC a n) n -> Exp (AnTEC a n) n + -> Exp a n + + -- | Make a pattern which binds the world argument + -- from a threaded primop. + , configThreadPat :: n -> Maybe (Bind n -> [Bind n] -> Pat n) + } + + +-- | Class of things that can have a state token threaded through them. +class Thread (c :: * -> * -> *) where + thread :: (Ord n, Show n, Pretty n) + => Config a n + -> KindEnv n -> TypeEnv n + -> c (AnTEC a n) n + -> c a n + + +instance Thread Module where + thread config kenv tenv mm + = let body' = threadModuleBody config kenv tenv (moduleBody mm) + in mm { moduleBody = body' } + + +-- | Keeps track of which recursive functions we're inside. +data Context n + -- | We're in the body of an effectful recursive function. + = ContextRec n + + -- | This effectful function in the context had a world token threaded + -- through it, but we're not in its body. + | ContextFun n + deriving Eq + + +-- Module --------------------------------------------------------------------- +-- | Thread state token though a module body. +-- We assume every top-level binding is a stateful function +-- that needs to accept and return the state token. +threadModuleBody + :: (Ord n, Show n, Pretty n) + => Config a n + -> KindEnv n -> TypeEnv n + -> Exp (AnTEC a n) n + -> Exp a n + +threadModuleBody config kenv tenv xx + = case xx of + XLet a lts x + -> let lts' = threadTopLets config kenv tenv lts + (bks, bts) = bindsOfLets lts + kenv' = Env.extends bks kenv + tenv' = Env.extends bts tenv + x' = threadModuleBody config kenv' tenv' x + in XLet (annotTail a) lts' x' + + _ -> reannotate annotTail xx + + +-- | Thread state token through some top-level bindings in a module. +threadTopLets + :: (Ord n, Show n, Pretty n) + => Config a n + -> KindEnv n -> TypeEnv n + -> Lets (AnTEC a n) n + -> Lets a n + +threadTopLets config kenv tenv lts + = case lts of + LLet b x + -> let (b', x') = threadTopBind config [] kenv tenv b x + in LLet b' x' + + LRec bxs + -> let tenv' = Env.extends (map fst bxs) tenv + bxs' = [ threadTopBind config [ContextRec n] kenv tenv' b x + | (b, x) <- bxs + , let BName n _ = b ] + in LRec bxs' + + _ -> reannotate annotTail lts + + +-- TopBind ------------------------------------------------------------------ +-- | Thread state token into a top-level binding. +-- We assume every top-level binding is stateful function that needs to +-- accept and return the state token. +-- +-- We inject the world type into the type of the function and then call +-- threadBind which will add the actual lambda for the new argument. +-- +threadTopBind + :: (Ord n, Show n, Pretty n) + => Config a n + -> [Context n] + -> KindEnv n -> TypeEnv n + -> Bind n -> Exp (AnTEC a n) n + -> (Bind n, Exp a n) + +threadTopBind config context kenv tenv b xBody + = let tBind = typeOfBind b + tBind' = injectStateType config tBind + b' = replaceTypeOfBind tBind' b + tenv' = Env.extend b' tenv + tsArgs = fst $ takeTFunAllArgResult tBind' + in ( b' + , threadProc config context kenv tenv' xBody tsArgs) + + +-- Arg ------------------------------------------------------------------------ +-- | Thread state token into an argument expression. +-- If it is a syntactic function then we assume the function is stateful +-- and needs the state token added, otherwise return it unharmed. +threadArg + :: (Ord n, Show n, Pretty n) + => Config a n + -> [Context n] + -> KindEnv n -> TypeEnv n + -> Type n -> Exp (AnTEC a n) n + -> Exp a n + +threadArg config context kenv tenv t xx + = case xx of + XLam{} -> threadProcArg config context kenv tenv t xx + XLAM{} -> threadProcArg config context kenv tenv t xx + _ -> reannotate annotTail xx + +threadProcArg config context kenv tenv t xx + = let tsArgs = fst $ takeTFunAllArgResult t + in threadProc config context kenv tenv xx tsArgs + + +-- Proc ----------------------------------------------------------------------- +-- | Thread world token into the body of a stateful function (procedure). +threadProc + :: (Ord n, Show n, Pretty n) + => Config a n + -> [Context n] + -> KindEnv n -> TypeEnv n + -> Exp (AnTEC a n) n -- Whole expression, including lambdas. + -> [Type n] -- Types of function parameters. + -> Exp a n + +-- We're out of parameters. +-- Now thread into the statements in the function body. +threadProc config context kenv tenv xx [] + = threadProcBody config context kenv tenv xx + +-- We're still decending past all the lambdas. +-- When we get to the inner-most one then add the state parameter. +threadProc config context kenv tenv xx (t : tsArgs) + = case xx of + XLAM a b x + -> let kenv' = Env.extend b kenv + x' = threadProc config context kenv' tenv x tsArgs + in XLAM (annotTail a) b x' + + XLam a b x + -> let tenv' = Env.extend b tenv + x' = threadProc config context kenv tenv' x tsArgs + in XLam (annotTail a) b x' + + -- Inject a new lambda to bind the state parameter. + _ | a <- annotOfExp xx + , t == configTokenType config + -> let b' = BAnon (configTokenType config) + tenv' = Env.extend b' tenv + x' = threadProc config context kenv tenv' xx tsArgs + in XLam (annotTail a) b' x' + + -- We've decended past all the lambdas, + -- so now thread into the procedure body. + _ -> threadProcBody config context kenv tenv xx + + +-- | Thread world token into the body of a procedure, +-- after we've decended past all the lambdas. +threadProcBody + :: (Ord n, Show n, Pretty n) + => Config a n + -> [Context n] + -> KindEnv n -> TypeEnv n + -> Exp (AnTEC a n) n + -> Exp a n + +threadProcBody config context kenv tenv xx + = case xx of + + -- Recursive let bindings in a procedure body. + -- These will be local loops. + XLet a (LRec bxs) x2 + -> let bxs' = [threadTopBind config + (context ++ [ContextRec n]) + kenv tenv b x + | (b, x) <- bxs + , let BName n _ = b ] + + tenv' = Env.extends (map fst bxs) tenv + + + x2' = threadProcBody config + (context ++ [ContextFun n + | (b, _x) <- bxs + , let BName n _ = b ]) + kenv tenv' x2 + in XLet (annotTail a) (LRec bxs') x2' + + -- A statement in the procedure body. + XLet _ (LLet b x) x2 + | Just (XVar a u, xsArgs) <- takeXApps x + , Just n <- takeNameOfBound u + , Just tOld <- Env.lookup u tenv + , Just tNew <- configThreadMe config n tOld + , Just mkPat <- configThreadPat config n + -> let + tWorld = configTokenType config + + -- Add world token as final argument + xsArgs' = xsArgs ++ [XVar a (UIx 0)] + + -- Thread into possibly higher order arguments. + tsArgs = fst $ takeTFunAllArgResult tNew + xsArgs'' = zipWith (threadArg config context kenv tenv) tsArgs xsArgs' + + -- Build the final expression. + u' = replaceTypeOfBound tNew u + x' = xApps (annotTail a) (XVar (annotTail a) u') xsArgs'' + + -- Thread into let-expression body. + tenv' = Env.extend b tenv + x2' = threadProcBody config context kenv tenv' x2 + pat' = mkPat (BAnon tWorld) [b] + in XCase (annotTail a) x' [AAlt pat' x2'] + + + -- Let bound effectful function. + -- Needs to be converted to a 'case'. + XLet a (LLet b x1) x2 + | Just (XVar _ (UName n), _xsArgs) <- takeXApps x1 + , elem (ContextFun n) context + , Just mkPat <- configThreadPat config n + -> let + tWorld = configTokenType config + a' = annotTail a + x1' = XApp a' (reannotate annotTail x1) (XVar a' (UIx 0)) + x2' = threadProcBody config context kenv tenv x2 + pat' = mkPat (BAnon tWorld) [b] + + in XCase (annotTail a) x1' [AAlt pat' x2'] + + + -- A pure binding that doesn't need the token. + XLet a lts x + -> let (bks, bts) = bindsOfLets lts + kenv' = Env.extends bks kenv + tenv' = Env.extends bts tenv + lts' = reannotate annotTail lts + x' = threadProcBody config context kenv' tenv' x + in XLet (annotTail a) lts' x' + + + -- Case of an effectful function. + XCase a xScrut [AAlt (PData _dc bs) xBody] + | Just ((XVar _ (UName n), _xsArgs)) <- takeXApps xScrut + , elem (ContextFun n) context + , Just mkPat <- configThreadPat config n + -> let + a' = annotTail a + tWorld = configTokenType config + xScrut' = XApp a' (reannotate annotTail xScrut) (XVar a' (UIx 0)) + pat' = mkPat (BAnon tWorld) bs + alt' = threadAlt config context kenv tenv + (AAlt pat' xBody) + + in XCase (annotTail a) xScrut' [alt'] + + + -- Pure case. + XCase a x alts + -> let alts' = map (threadAlt config context kenv tenv) alts + x' = reannotate annotTail x + in XCase (annotTail a) x' alts' + + -- We shouldn't see these things in a proc body. + XLAM{} -> error "ddc-core-simpl.Thread: unexpected XLAM" + XLam{} -> error "ddc-core-simpl.Thread: unexpected XLam" + XCast{} -> error "ddc-core-simpl.Thread: unexpected cast." + + XType a t + -> XType (annotTail a) t + + XWitness a w + -> XWitness (annotTail a) (reannotate annotTail w) + + -- Tailcalls + XApp a _ _ + | Just ((XVar _ (UName n), _xsArgs)) <- takeXApps xx + , elem (ContextRec n) context + -> let a' = annotTail a + in XApp a' (reannotate annotTail xx) + (XVar a' (UIx 0)) + + + -- For XVar, XCon, XApp as result value of function. + _ + -- Otherwise wrap the returned value with a tuple holding + -- the world. + | otherwise + -> let a = annotOfExp xx + a' = AnTEC (configTokenType config) + (tBot kEffect) + (tBot kClosure) + (annotTail a) + + xWorld = XVar a' (UIx 0) + wrap = configWrapResultExp config + in wrap xWorld xx + + + +-- | Thread world token into a case alternative +threadAlt + :: (Ord n, Show n, Pretty n) + => Config a n + -> [Context n] + -> KindEnv n -> TypeEnv n + -> Alt (AnTEC a n) n + -> Alt a n + +threadAlt config context kenv tenv (AAlt pat xx) + = case pat of + PDefault + -> AAlt pat (threadProcBody config context kenv tenv xx) + + PData _ bs + -> let tenv' = Env.extends bs tenv + in AAlt pat (threadProcBody config context kenv tenv' xx) + + +------------------------------------------------------------------------------- +-- | Inject the state token into the type of an effectful function. +-- Eg, change ([a b : Data]. a -> b -> Int) +-- to ([a b : Data]. a -> b -> World -> (World, Int) +injectStateType :: Eq n => Config a n -> Type n -> Type n +injectStateType config tt + = let down = injectStateType config + in case tt of + TForall b x + -> TForall b (down x) + + TApp{} + | (tsArg@(_ : _), tResult) <- takeTFunArgResult tt + -> let tsArg' = tsArg ++ [configTokenType config] + tResult' = injectStateType config tResult + in foldr tFun tResult' tsArg' + + _ | tt == configTokenType config -> tt + | tt == configVoidType config -> configTokenType config + | otherwise -> configWrapResultType config tt + diff --git a/DDC/Core/Transform/TransformDownX.hs b/DDC/Core/Transform/TransformDownX.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/TransformDownX.hs @@ -0,0 +1,139 @@ + +-- | General purpose tree walking boilerplate. +module DDC.Core.Transform.TransformDownX + ( TransformDownMX(..) + , transformDownX + , transformDownX') +where +import DDC.Core.Module +import DDC.Core.Exp.Annot +import DDC.Type.Env (KindEnv, TypeEnv) +import Data.Functor.Identity +import Control.Monad +import qualified DDC.Type.Env as Env + + +-- | Top-down rewrite of all core expressions in a thing. +transformDownX + :: forall (c :: * -> * -> *) a n + . (Ord n, TransformDownMX Identity c) + => (KindEnv n -> TypeEnv n -> Exp a n -> Exp a n) + -- ^ The worker function is given the current + -- kind and type environments. + -> KindEnv n -- ^ Initial kind environment. + -> TypeEnv n -- ^ Initial type environment. + -> c a n -- ^ Transform this thing. + -> c a n + +transformDownX f kenv tenv xx + = runIdentity + $ transformDownMX + (\kenv' tenv' x -> return (f kenv' tenv' x)) + kenv tenv xx + + +-- | Like transformDownX, but without using environments. +transformDownX' + :: forall (c :: * -> * -> *) a n + . (Ord n, TransformDownMX Identity c) + => (Exp a n -> Exp a n) + -- ^ The worker function is given the current + -- kind and type environments. + -> c a n -- ^ Transform this thing. + -> c a n + +transformDownX' f xx + = transformDownX (\_ _ -> f) Env.empty Env.empty xx + + +------------------------------------------------------------------------------- +class TransformDownMX m (c :: * -> * -> *) where + -- | Top-down monadic rewrite of all core expressions in a thing. + transformDownMX + :: Ord n + => (KindEnv n -> TypeEnv n -> Exp a n -> m (Exp a n)) + -- ^ The worker function is given the current + -- kind and type environments. + -> KindEnv n -- ^ Initial kind environment. + -> TypeEnv n -- ^ Initial type environment. + -> c a n -- ^ Transform this thing. + -> m (c a n) + + +instance Monad m => TransformDownMX m Module where + transformDownMX f kenv tenv !mm + = do x' <- transformDownMX f kenv tenv $ moduleBody mm + return $ mm { moduleBody = x' } + + +instance Monad m => TransformDownMX m Exp where + transformDownMX f kenv tenv !xx + = {-# SCC transformDownMX #-} + f kenv tenv xx >>= \xx' -> + case xx' of + XVar{} -> return xx' + XCon{} -> return xx' + + XLAM a b x1 + -> liftM3 XLAM (return a) (return b) + (transformDownMX f (Env.extend b kenv) tenv x1) + + XLam a b x1 + -> liftM3 XLam (return a) (return b) + (transformDownMX f kenv (Env.extend b tenv) x1) + + XApp a x1 x2 + -> liftM3 XApp (return a) + (transformDownMX f kenv tenv x1) + (transformDownMX f kenv tenv x2) + + XLet a lts x + -> do lts' <- transformDownMX f kenv tenv lts + let kenv' = Env.extends (specBindsOfLets lts') kenv + let tenv' = Env.extends (valwitBindsOfLets lts') tenv + x' <- transformDownMX f kenv' tenv' x + return $ XLet a lts' x' + + XCase a x alts + -> liftM3 XCase (return a) + (transformDownMX f kenv tenv x) + (mapM (transformDownMX f kenv tenv) alts) + + XCast a c x + -> liftM3 XCast + (return a) (return c) + (transformDownMX f kenv tenv x) + + XType{} -> return xx' + XWitness{} -> return xx' + + +instance Monad m => TransformDownMX m Lets where + transformDownMX f kenv tenv xx + = case xx of + LLet b x + -> liftM2 LLet (return b) + (transformDownMX f kenv tenv x) + + LRec bxs + -> do let (bs, xs) = unzip bxs + let tenv' = Env.extends bs tenv + xs' <- mapM (transformDownMX f kenv tenv') xs + return $ LRec $ zip bs xs' + + LPrivate{} + -> return xx + + +instance Monad m => TransformDownMX m Alt where + transformDownMX f kenv tenv alt + = case alt of + AAlt p@(PData _ bsArg) x + -> let tenv' = Env.extends bsArg tenv + in liftM2 AAlt (return p) + (transformDownMX f kenv tenv' x) + + AAlt PDefault x + -> liftM2 AAlt (return PDefault) + (transformDownMX f kenv tenv x) + diff --git a/DDC/Core/Transform/TransformModX.hs b/DDC/Core/Transform/TransformModX.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/TransformModX.hs @@ -0,0 +1,45 @@ + +-- | Helper for transforming the bindings in a module +module DDC.Core.Transform.TransformModX + ( transformModX + , transformModLet + ) +where +import DDC.Core.Module +import DDC.Core.Exp.Annot + +import Control.Arrow + + +-- | Apply transform to each expression let binding in module +transformModX :: (Exp a n -> Exp a n) + -> Module a n + -> Module a n +transformModX f mm + = transformModLet (const f) mm + + +-- | Apply transform to each expression let binding in module, with bind too +transformModLet :: (Bind n -> Exp a n -> Exp a n) + -> Module a n + -> Module a n +transformModLet f mm + = let body = moduleBody mm + + (lets,xx) = splitXLetsAnnot body + lets' = map (first go) lets + + body' = xLetsAnnot lets' xx + + in mm { moduleBody = body' } + where + go (LRec binds) + = LRec [ (b, f b x) + | (b, x) <- binds] + + go (LLet b x) + = LLet b (f b x) + + go l + = l + diff --git a/DDC/Core/Transform/TransformUpX.hs b/DDC/Core/Transform/TransformUpX.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/TransformUpX.hs @@ -0,0 +1,133 @@ +-- | General purpose tree walking boilerplate. +module DDC.Core.Transform.TransformUpX + ( TransformUpMX(..) + , transformUpX + , transformUpX') +where +import DDC.Core.Module +import DDC.Core.Exp.Annot +import Data.Functor.Identity +import Control.Monad +import DDC.Core.Env.EnvX (EnvX) +import qualified DDC.Core.Env.EnvX as EnvX + + +-- | Bottom up rewrite of all core expressions in a thing. +transformUpX + :: forall (c :: * -> * -> *) a n + . (Ord n, TransformUpMX Identity c) + => (EnvX n -> Exp a n -> Exp a n) + -- ^ The worker function is given the current kind and type environments. + -> EnvX n -- ^ Initial environment. + -> c a n -- ^ Transform this thing. + -> c a n + +transformUpX f env xx + = runIdentity + $ transformUpMX (\env' x -> return (f env' x)) env xx + + +-- | Like transformUpX, but without using environments. +transformUpX' + :: forall (c :: * -> * -> *) a n + . (Ord n, TransformUpMX Identity c) + => (Exp a n -> Exp a n) + -- ^ The worker function is given the current + -- kind and type environments. + -> c a n -- ^ Transform this thing. + -> c a n + +transformUpX' f xx + = transformUpX (\_ -> f) EnvX.empty xx + + +------------------------------------------------------------------------------- +class TransformUpMX m (c :: * -> * -> *) where + -- | Bottom-up monadic rewrite of all core expressions in a thing. + transformUpMX + :: Ord n + => (EnvX n -> Exp a n -> m (Exp a n)) + -- ^ The worker function is given the current + -- kind and type environments. + -> EnvX n -- ^ Initial environment. + -> c a n -- ^ Transform this thing. + -> m (c a n) + + +instance Monad m => TransformUpMX m Module where + transformUpMX f env !mm + = do x' <- transformUpMX f env $ moduleBody mm + return $ mm { moduleBody = x' } + + +instance Monad m => TransformUpMX m Exp where + transformUpMX f env !xx + = (f env =<<) + $ case xx of + XVar{} -> return xx + XCon{} -> return xx + + XLAM a b x1 + -> liftM3 XLAM (return a) (return b) + (transformUpMX f (EnvX.extendT b env) x1) + + XLam a b x1 + -> liftM3 XLam (return a) (return b) + (transformUpMX f (EnvX.extendX b env) x1) + + XApp a x1 x2 + -> liftM3 XApp (return a) + (transformUpMX f env x1) + (transformUpMX f env x2) + + XLet a lts x + -> do lts' <- transformUpMX f env lts + + let env' = EnvX.extendsX (valwitBindsOfLets lts') + $ EnvX.extendsT (specBindsOfLets lts') + $ env + + x' <- transformUpMX f env' x + return $ XLet a lts' x' + + XCase a x alts + -> liftM3 XCase (return a) + (transformUpMX f env x) + (mapM (transformUpMX f env) alts) + + XCast a c x + -> liftM3 XCast + (return a) (return c) + (transformUpMX f env x) + + XType{} -> return xx + XWitness{} -> return xx + + +instance Monad m => TransformUpMX m Lets where + transformUpMX f env xx + = case xx of + LLet b x + -> liftM2 LLet (return b) + (transformUpMX f env x) + + LRec bxs + -> do let (bs, xs) = unzip bxs + let env' = EnvX.extendsX bs env + xs' <- mapM (transformUpMX f env') xs + return $ LRec $ zip bs xs' + + LPrivate{} -> return xx + + +instance Monad m => TransformUpMX m Alt where + transformUpMX f env alt + = case alt of + AAlt p@(PData _ bsArg) x + -> let env' = EnvX.extendsX bsArg env + in liftM2 AAlt (return p) + (transformUpMX f env' x) + + AAlt PDefault x + -> liftM2 AAlt (return PDefault) + (transformUpMX f env x) diff --git a/DDC/Core/Transform/TransformX.hs b/DDC/Core/Transform/TransformX.hs deleted file mode 100644 --- a/DDC/Core/Transform/TransformX.hs +++ /dev/null @@ -1,112 +0,0 @@ - --- | General purpose tree walking boilerplate. -module DDC.Core.Transform.TransformX - ( TransformUpMX(..) - , transformUpX) -where -import DDC.Core.Exp -import DDC.Core.Compounds -import DDC.Type.Env (Env) -import Data.Functor.Identity -import Control.Monad -import qualified DDC.Type.Env as Env - - --- | Bottom up rewrite of all core expressions in a thing. -transformUpX - :: forall (c :: * -> * -> *) a n - . (Ord n, TransformUpMX Identity c) - => (Env n -> Env n -> Exp a n -> Exp a n) - -- ^ The worker function is given the current kind and type environments. - -> Env n -- ^ Initial kind environment. - -> Env n -- ^ Initial type environment. - -> c a n -- ^ Transform this thing. - -> c a n - -transformUpX f kenv tenv xx - = runIdentity - $ transformUpMX - (\kenv' tenv' x -> return (f kenv' tenv' x)) - kenv tenv xx - - -class TransformUpMX m (c :: * -> * -> *) where - -- | Bottom-up monadic rewrite of all core expressions in a thing. - transformUpMX - :: Ord n - => (Env n -> Env n -> Exp a n -> m (Exp a n)) - -- ^ The worker function is given the current kind and type environments. - -> Env n -- ^ Initial kind environment. - -> Env n -- ^ Initial type environment. - -> c a n -- ^ Transform this thing. - -> m (c a n) - -instance Monad m => TransformUpMX m Exp where - transformUpMX f kenv tenv xx - = (f kenv tenv =<<) - $ case xx of - XVar{} -> return xx - XCon{} -> return xx - - XLAM a b x1 - -> liftM3 XLAM (return a) (return b) - (transformUpMX f (Env.extend b kenv) tenv x1) - - XLam a b x1 - -> liftM3 XLam (return a) (return b) - (transformUpMX f kenv (Env.extend b tenv) x1) - - XApp a x1 x2 - -> liftM3 XApp (return a) - (transformUpMX f kenv tenv x1) - (transformUpMX f kenv tenv x2) - - XLet a lts x - -> do lts' <- transformUpMX f kenv tenv lts - let kenv' = Env.extends (specBindsOfLets lts') kenv - let tenv' = Env.extends (valwitBindsOfLets lts') tenv - x' <- transformUpMX f kenv' tenv' x - return $ XLet a lts' x' - - XCase a x alts - -> liftM3 XCase (return a) - (transformUpMX f kenv tenv x) - (mapM (transformUpMX f kenv tenv) alts) - - XCast a c x - -> liftM3 XCast - (return a) (return c) - (transformUpMX f kenv tenv x) - - XType _ -> return xx - XWitness _ -> return xx - - -instance Monad m => TransformUpMX m Lets where - transformUpMX f kenv tenv xx - = case xx of - LLet m b x - -> liftM3 LLet (return m) (return b) - (transformUpMX f kenv tenv x) - - LRec bxs - -> do let (bs, xs) = unzip bxs - let tenv' = Env.extends bs tenv - xs' <- mapM (transformUpMX f kenv tenv') xs - return $ LRec $ zip bs xs' - - LLetRegion{} -> return xx - LWithRegion{} -> return xx - - -instance Monad m => TransformUpMX m Alt where - transformUpMX f kenv tenv alt - = case alt of - AAlt p@(PData _ bsArg) x - -> let tenv' = Env.extends bsArg tenv - in liftM2 AAlt (return p) - (transformUpMX f kenv tenv' x) - - AAlt PDefault x - -> liftM2 AAlt (return PDefault) - (transformUpMX f kenv tenv x) diff --git a/DDC/Core/Transform/Unshare.hs b/DDC/Core/Transform/Unshare.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Unshare.hs @@ -0,0 +1,334 @@ + +module DDC.Core.Transform.Unshare + (unshareModule) +where +import DDC.Core.Exp.Annot.AnTEC +import DDC.Core.Exp.Annot +import DDC.Core.Module +import DDC.Type.Transform.SubstituteT +import Data.Map (Map) +import qualified Data.Map.Strict as Map + + +------------------------------------------------------------------------------- +-- | Apply the unsharing transform to a module. +unshareModule + :: (Show a, Ord n, Show n) + => Module (AnTEC a n) n -> Module (AnTEC a n) n + +unshareModule !mm + = let + -- Add extra parameters to the types of imported CAFs. + importValuesNts + = [ let (iv', m) = addParamsImportValue iv + in ((n, iv'), m) + | (n, iv) <- moduleImportValues mm] + + (importValues', ntssImport') + = unzip importValuesNts + + -- Add extra parameters to the CAFs, + -- returning the names of the ones we've transformed + -- along with the transformed module body. + (ntsBody, xx) = addParamsX $ moduleBody mm + + -- Add the corresponding arguments to each use. + nts' = Map.union (Map.unions ntssImport') ntsBody + xx' = addArgsX nts' xx + + -- Update the types of exports with the transformed ones. + exportValues' + = [ (n, updateExportSource nts' ex) + | (n, ex) <- moduleExportValues mm ] + + in mm { moduleBody = xx' + , moduleExportValues = exportValues' + , moduleImportValues = importValues' } + + +------------------------------------------------------------------------------- +-- | If this import def imports a CAF then then add an extra parameter to its +-- type, assuming that the unsharing transform has also been applied to the +-- imported module. +-- +addParamsImportValue + :: ImportValue n (Type n) + -> (ImportValue n (Type n), Map n (Type n)) + +addParamsImportValue iv + = case iv of + ImportValueModule m n t (Just (nType, nValue, nBoxes)) + -> case addParamsT t of + Just t' + -> ( ImportValueModule m n t' + (Just (nType, nValue + 1, nBoxes)) + , Map.singleton n t') + + Nothing + -> ( iv, Map.empty) + + ImportValueModule{} -> (iv, Map.empty) + ImportValueSea{} -> (iv, Map.empty) + + +-- | If this is the type of a CAF then add an extra unit parameter to it. +addParamsT :: Type n -> Maybe (Type n) +addParamsT tt + = case tt of + TVar{} -> Just $ tUnit `tFun` tt + TCon{} -> Just $ tUnit `tFun` tt + + TAbs b tBody + -> do tBody' <- addParamsT tBody + return $ TAbs b tBody' + + TApp{} + -> case takeTFun tt of + Nothing -> Just $ tUnit `tFun` tt + Just _ -> Nothing + + TForall b tBody + -> do tBody' <- addParamsT tBody + return $ TForall b tBody' + + TSum{} + -> Nothing + + +------------------------------------------------------------------------------- +-- | Add unit parameters to the top-level CAFs in the given module body, +-- returning a map of names of transformed CAFs to their transformed +-- types. +addParamsX + :: Ord n + => Exp (AnTEC a n) n -- Module body to transform. + -> ( Map n (Type n) -- Map of transformed bindings to their + -- transformed types. + , Exp (AnTEC a n) n) -- Transformed module body. + +addParamsX xx + = case xx of + -- Transform all the top-level bindings of a module body. + XLet a (LRec bxs) xBody + -> let (ns, bxs') = addParamsBXS a bxs + in ( ns + , XLet a (LRec bxs') xBody) + + _ -> ( Map.empty + , xx) + + +-- | Add unit parameters to the bound CAFs in the given list. +addParamsBXS _a [] + = (Map.empty, []) + +addParamsBXS a ((b, x) : bxs) + = let (ns1, b', x') = addParamsBX a b x + (ns2, bxs') = addParamsBXS a bxs + in ( Map.union ns1 ns2 + , (b', x') : bxs') + + +-- | Add unit parameter to a single top-level binding, if it needs one. +addParamsBX _ b@(BName n _) x + = case addParamsBodyX x of + Nothing + -> (Map.empty, b, x) + + Just (x', t') + -> ( Map.singleton n t' + , replaceTypeOfBind t' b + , x') + +addParamsBX _ b x + = (Map.empty, b, x) + + +-- | Add unit parameters to the right of a let-binding. +addParamsBodyX xx + = case xx of + -- This binding already has an outer value abstraction, + -- so we don't need to add any more. + XLam{} + -> Nothing + + -- Decend under type abstractions. To keep the supers + -- in standard form with all the type abstractions first, + -- if we need to add a value abstraction we want to add it + -- under exising type abstractions. + XLAM a bParam xBody + -> case addParamsBodyX xBody of + Nothing + -> Nothing + + Just (xBody', tBody') + -> let t' = TForall bParam tBody' + a' = a { annotType = t' } + in Just ( XLAM a' bParam xBody', t') + + -- We've hit a plain value, so need to wrap it in a + -- value abstraction. + _ + -> let a = annotOfExp xx + t' = tFun tUnit (annotType a) + a' = a { annotType = t' } + in Just (XLam a' (BNone tUnit) xx, t') + + +------------------------------------------------------------------------------- +-- | Decend into an expression looking for applications of CAFs that +-- we've already added an extra unit parameter to. When we find them, +-- add the matching unit argument. +-- +addArgsX :: (Show n, Ord n, Show a) + => Map n (Type n) -- ^ Map of names of CAFs that we've added + -- parameters to, to their transformed types. + -> Exp (AnTEC a n) n -- ^ Transform this expression. + -> Exp (AnTEC a n) n -- ^ Transformed expression. + +addArgsX nts xx + = let downX = addArgsX nts + downLts = addArgsLts nts + downA = addArgsAlt nts + + in case xx of + + -- Add an extra argument for a monomorphic CAF. + XVar a (UName n) + -> case Map.lookup n nts of + Just tF + -> let xx' = XVar (a { annotType = tF }) (UName n) + in wrapAppX a tF xx' + + Nothing -> xx + + XVar{} -> xx + XCon{} -> xx + + XApp{} -> addArgsAppX nts xx [] + + -- For the rest of the constructs their types do not + -- change during the transform so we can resuse the old ones. + XLAM a b xBody -> XLAM a b (downX xBody) + XLam a b xBody -> XLam a b (downX xBody) + XLet a lts xBody -> XLet a (downLts lts) (downX xBody) + XCase a xScrut as -> XCase a (downX xScrut) (map downA as) + XCast a c x -> XCast a c (downX x) + XType{} -> xx + XWitness{} -> xx + + +addArgsAppX !nts !xx !ats + = let downX = addArgsX nts + tA = annotType $ annotOfExp xx + in case xx of + XVar a (UName n) + -> case Map.lookup n nts of + Just tF + -> let xx' = XVar (a { annotType = tF }) (UName n) + (x1, t1) = wrapAtsX xx' tF ats + x2 = wrapAppX a t1 x1 + in x2 + + Nothing + -> fst $ wrapAtsX xx tA ats + + XVar{} + -> fst $ wrapAtsX xx tA ats + + XCon{} + -> fst $ wrapAtsX xx tA ats + + XApp _a1 x1 (XType a2 t) + -> addArgsAppX nts x1 ((a2, t) : ats) + + XApp a x1 x2 + -> XApp a (addArgsAppX nts x1 ats) (downX x2) + + _ -> fst $ wrapAtsX xx tA ats + + +addArgsLts nts lts + = let downX = addArgsX nts + in case lts of + LLet b x -> LLet b (downX x) + LRec bxs -> LRec [(b, downX x) | (b, x) <- bxs] + LPrivate{} -> lts + + +addArgsAlt nts aa + = let downX = addArgsX nts + in case aa of + AAlt p x -> AAlt p (downX x) + + +-- Wrap an expression with an application of a unit value. +wrapAppX :: (Show a, Show n) + => AnTEC a n + -> Type n + -> Exp (AnTEC a n) n + -> Exp (AnTEC a n) n + +wrapAppX a tF xF + | Just (_, tResult) <- takeTFun tF + = let a' = annotOfExp xF + aR = a' { annotType = tResult } + aV = a' { annotType = tF } + aU = a' { annotType = tUnit } + xF' = mapAnnotOfExp (const aV) xF + in XApp aR xF' (xUnit aU) + + + -- ISSUE #384: Unshare transform produces AST node with wrong type annotation. + | Just (bs, tBody) <- takeTForalls tF + = let Just us = sequence + $ map takeSubstBoundOfBind bs + + xF' = makeXLamFlags a [(True, b) | b <- bs] + $ wrapAppX a tBody + $ xApps a xF (map (XType a) $ map TVar us) + + in xF' + + + | otherwise + = xF + + +-- Apply the given type arguments to an expression. +wrapAtsX !xF !tF [] + = (xF, tF) + +wrapAtsX !xF !tF ((aArg, tArg): ats) + = case tF of + TForall bParam tBody + -> let a = annotOfExp xF + tR = substituteT bParam tArg tBody + aR = a { annotType = tR } + aV = a { annotType = tF } + xF' = mapAnnotOfExp (const aV) xF + in wrapAtsX + (XApp aR xF' (XType aArg tArg)) + tR ats + + _ -> (xF, tF) + + +------------------------------------------------------------------------------- +-- | Update the types of exported things with the ones in +-- the give map. +updateExportSource + :: Ord n + => Map n (Type n) + -> ExportSource n (Type n) -> ExportSource n (Type n) + +updateExportSource mm ex + = case ex of + ExportSourceLocal n _t + -> case Map.lookup n mm of + Nothing -> ex + Just t' -> ExportSourceLocal n t' + + ExportSourceLocalNoType _ + -> ex + diff --git a/DDC/Type/Transform/Alpha.hs b/DDC/Type/Transform/Alpha.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Transform/Alpha.hs @@ -0,0 +1,55 @@ + +module DDC.Type.Transform.Alpha + (Alpha(..)) +where +import DDC.Type.Exp +import DDC.Type.Sum + + +class Alpha (c :: * -> *) where + -- | Apply a function to all the names in a thing. + alpha :: forall n1 n2. Ord n2 => (n1 -> n2) -> c n1 -> c n2 + + +instance Alpha Type where + alpha f tt + = case tt of + TVar u -> TVar (alpha f u) + TCon c -> TCon (alpha f c) + TAbs b t -> TAbs (alpha f b) (alpha f t) + TApp t1 t2 -> TApp (alpha f t1) (alpha f t2) + TForall b t -> TForall (alpha f b) (alpha f t) + TSum ts -> TSum (alpha f ts) + + +instance Alpha TypeSum where + alpha f ts + = fromList (alpha f $ kindOfSum ts) $ map (alpha f) $ toList ts + + +instance Alpha Bind where + alpha f bb + = case bb of + BName n t -> BName (f n) (alpha f t) + BAnon t -> BAnon (alpha f t) + BNone t -> BNone (alpha f t) + + +instance Alpha Bound where + alpha f uu + = case uu of + UIx i -> UIx i + UName n -> UName (f n) + UPrim n t -> UPrim (f n) (alpha f t) + + +instance Alpha TyCon where + alpha f cc + = case cc of + TyConSort sc -> TyConSort sc + TyConKind kc -> TyConKind kc + TyConWitness tc -> TyConWitness tc + TyConSpec tc -> TyConSpec tc + TyConBound u k -> TyConBound (alpha f u) (alpha f k) + TyConExists i k -> TyConExists i (alpha f k) + diff --git a/DDC/Type/Transform/AnonymizeT.hs b/DDC/Type/Transform/AnonymizeT.hs --- a/DDC/Type/Transform/AnonymizeT.hs +++ b/DDC/Type/Transform/AnonymizeT.hs @@ -4,8 +4,7 @@ , AnonymizeT(..) , pushAnonymizeBindT) where -import DDC.Type.Exp -import DDC.Type.Compounds +import DDC.Type.Exp.Simple import Data.List import qualified DDC.Type.Sum as T @@ -36,13 +35,17 @@ TCon{} -> tt - TForall b t + TAbs b t -> let (kstack', b') = pushAnonymizeBindT kstack b - in TForall b' (anonymizeWithT kstack' t) + in TAbs b' (anonymizeWithT kstack' t) TApp t1 t2 -> TApp (anonymizeWithT kstack t1) (anonymizeWithT kstack t2) + TForall b t + -> let (kstack', b') = pushAnonymizeBindT kstack b + in TForall b' (anonymizeWithT kstack' t) + TSum ss -> TSum (anonymizeWithT kstack ss) @@ -57,17 +60,21 @@ instance AnonymizeT Bound where anonymizeWithT kstack bb = case bb of - UName _ t + UName _ | Just ix <- findIndex (boundMatchesBind bb) kstack - -> UIx ix (anonymizeWithT kstack t) + -> UIx ix _ -> bb -- Push ---------------------------------------------------------------------- --- Push a binding occurrence of a type variable on the stack, --- returning the anonyized binding occurrence and the new stack. -pushAnonymizeBindT :: Ord n => [Bind n] -> Bind n -> ([Bind n], Bind n) +-- | Push a binding occurrence of a level-1 variable on the stack, +-- returning the anonyized binding occurrence and the new stack. +pushAnonymizeBindT + :: [Bind n] -- ^ Stack for Spec binders (level-1) + -> Bind n + -> ([Bind n], Bind n) + pushAnonymizeBindT kstack b = let t' = typeOfBind b kstack' = b : kstack diff --git a/DDC/Type/Transform/Rename.hs b/DDC/Type/Transform/Rename.hs deleted file mode 100644 --- a/DDC/Type/Transform/Rename.hs +++ /dev/null @@ -1,53 +0,0 @@ - -module DDC.Type.Transform.Rename - (Rename(..)) -where -import DDC.Type.Exp -import DDC.Type.Sum - - -class Rename (c :: * -> *) where - -- | Apply a function to all the names in a thing. - rename :: forall n1 n2. Ord n2 => (n1 -> n2) -> c n1 -> c n2 - - -instance Rename Type where - rename f tt - = case tt of - TVar u -> TVar (rename f u) - TCon c -> TCon (rename f c) - TForall b t -> TForall (rename f b) (rename f t) - TApp t1 t2 -> TApp (rename f t1) (rename f t2) - TSum ts -> TSum (rename f ts) - - -instance Rename TypeSum where - rename f ts - = fromList (rename f $ kindOfSum ts) $ map (rename f) $ toList ts - - -instance Rename Bind where - rename f bb - = case bb of - BName n t -> BName (f n) (rename f t) - BAnon t -> BAnon (rename f t) - BNone t -> BNone (rename f t) - - -instance Rename Bound where - rename f uu - = case uu of - UIx i k -> UIx i (rename f k) - UName n k -> UName (f n) (rename f k) - UPrim n k -> UName (f n) (rename f k) - - -instance Rename TyCon where - rename f cc - = case cc of - TyConSort sc -> TyConSort sc - TyConKind kc -> TyConKind kc - TyConWitness tc -> TyConWitness tc - TyConSpec tc -> TyConSpec tc - TyConBound u -> TyConBound $ rename f u - diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,7 +1,7 @@ -------------------------------------------------------------------------------- The Disciplined Disciple Compiler License (MIT style) -Copyrite (K) 2007-2012 The Disciplined Disciple Compiler Strike Force +Copyrite (K) 2007-2016 The Disciplined Disciple Compiler Strike Force All rights reversed. Permission is hereby granted, free of charge, to any person obtaining a copy @@ -13,18 +13,4 @@ The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. - -------------------------------------------------------------------------------- -Under Australian law copyright is free and automatic. -By contributing to DDC authors grant all rights they have regarding their -contributions to the other members of the Disciplined Disciple Compiler Strike -Force, past, present and future, as well as placing their contributions under -the above license. - -Use "darcs show authors" to get a list of Strike Force members. - -------------------------------------------------------------------------------- -Redistributions of libraries in ./external are governed by their own licenses: - - - TinyPTC GNU Lesser General Public License - diff --git a/ddc-core-simpl.cabal b/ddc-core-simpl.cabal --- a/ddc-core-simpl.cabal +++ b/ddc-core-simpl.cabal @@ -1,5 +1,5 @@ Name: ddc-core-simpl -Version: 0.2.1.2 +Version: 0.4.3.1 License: MIT License-file: LICENSE Author: The Disciplined Disciple Compiler Strike Force @@ -9,39 +9,87 @@ Stability: experimental Category: Compilers/Interpreters Homepage: http://disciple.ouroborus.net -Bug-reports: disciple@ouroborus.net -Synopsis: Disciple Core language simplifying code transformations. -Description: Disciple Core language simplifying code transformations. +Synopsis: Disciplined Disciple Compiler code transformations. +Description: Disciplined Disciple Compiler code transformations. Library Build-Depends: - base == 4.6.*, + base >= 4.6 && < 4.10, + array >= 0.4 && < 0.6, + deepseq >= 1.3 && < 1.5, containers == 0.5.*, - array >= 0.3 && < 0.5, - transformers == 0.3.*, - mtl == 2.1.*, - ddc-base == 0.2.1.*, - ddc-core == 0.2.1.* + transformers == 0.5.*, + mtl == 2.2.1.*, + ddc-core == 0.4.3.* Exposed-modules: + DDC.Core.Analysis.Arity + DDC.Core.Analysis.Usage + + DDC.Core.Simplifier.Parser + DDC.Core.Simplifier.Recipe + DDC.Core.Simplifier.Result + + DDC.Core.Transform.Rewrite.Disjoint + DDC.Core.Transform.Rewrite.Env + DDC.Core.Transform.Rewrite.Match + DDC.Core.Transform.Rewrite.Parser + DDC.Core.Transform.Rewrite.Rule + DDC.Core.Transform.AnonymizeX - DDC.Core.Transform.ANormal DDC.Core.Transform.Beta - DDC.Core.Transform.TransformX + DDC.Core.Transform.Boxing + DDC.Core.Transform.Bubble + DDC.Core.Transform.Elaborate + DDC.Core.Transform.Eta + DDC.Core.Transform.Flatten + DDC.Core.Transform.FoldCase + DDC.Core.Transform.Forward + DDC.Core.Transform.Inline + DDC.Core.Transform.Lambdas + DDC.Core.Transform.Namify + DDC.Core.Transform.Prune + DDC.Core.Transform.Rewrite + DDC.Core.Transform.Snip + DDC.Core.Transform.Thread + DDC.Core.Transform.TransformDownX + DDC.Core.Transform.TransformModX + DDC.Core.Transform.TransformUpX + DDC.Core.Transform.Unshare + + DDC.Core.Simplifier + + DDC.Type.Transform.Alpha DDC.Type.Transform.AnonymizeT - DDC.Type.Transform.Rename - + + Other-modules: + DDC.Core.Simplifier.Apply + DDC.Core.Simplifier.Base + DDC.Core.Simplifier.Lexer + + DDC.Core.Transform.Inline.Templates + DDC.Core.Transform.Lambdas.Base + DDC.Core.Transform.Lambdas.Lift + DDC.Core.Transform.Rewrite.Error + GHC-options: -Wall -fno-warn-orphans -fno-warn-missing-signatures + -fno-warn-missing-methods -fno-warn-unused-do-bind Extensions: NoMonomorphismRestriction + ExistentialQuantification + MultiParamTypeClasses + ScopedTypeVariables + DeriveDataTypeable + FlexibleInstances + FlexibleContexts + ParallelListComp ExplicitForAll KindSignatures PatternGuards - MultiParamTypeClasses - FlexibleContexts - FlexibleInstances + BangPatterns + RankNTypes