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,142 @@ + +-- | 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.Predicates +import DDC.Core.Compounds +import DDC.Core.Module +import DDC.Core.Exp +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 :: Ord n => 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 t of + Just a -> Just (BName n t, a) + Nothing -> Nothing + | (n, (_, t)) <- Map.toList $ moduleImportTypes 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 :: Ord n => 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 _ dc -> arityFromType (typeOfDaCon dc) + + -- 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,248 @@ + +-- | 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 +import Data.List +import Data.Map (Map) +import qualified Data.Map as Map + + +-- Used ----------------------------------------------------------------------- +-- | Tracks how a bound variable is used. +data Used + -- | Bound variable is used as the function of 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 + + +-- Usage ---------------------------------------------------------------------- +-- | 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 + , moduleExportKinds = exportKinds + , moduleExportTypes = exportTypes + , moduleImportKinds = importKinds + , moduleImportTypes = importTypes + , moduleBody = body }) + + = ModuleCore + { moduleName = name + , moduleExportKinds = exportKinds + , moduleExportTypes = exportTypes + , moduleImportKinds = importKinds + , moduleImportTypes = importTypes + , moduleBody = usageX body } + + +-- | 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) + -> ( used2' + , 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) + -> ( used2' + , 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 + -> ( used' + , 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 t + -> (empty, XType t) + + XWitness w + -> (empty, XWitness 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 mode b x + | (used, x') <- usageX' x + -> (used, LLet mode b x') + + LRec bxs + | (bs, xs) <- unzip bxs + , (useds', xs') <- unzip $ map usageX' xs + , used' <- sumUsedMap useds' + -> (used', LRec $ zip bs xs') + + LLetRegions b bs + -> (empty, LLetRegions b bs) + + LWithRegion b + -> (empty, LWithRegion b) + + +-- | 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) + + CastWeakenClosure xs + | (useds, xs') <- unzip $ map usageX' xs + , UsedMap used' <- sumUsedMap useds + , usedCasts <- Map.map (map $ const UsedInCast) used' + -> (UsedMap usedCasts, CastWeakenClosure xs') + + CastPurify w + -> (empty, CastPurify w) + + CastForget w + -> (empty, CastForget w) + + +-- | 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') + + 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,240 @@ + +-- | Application of simplifiers to modules and expressions. +module DDC.Core.Simplifier.Apply + ( applySimplifier + , applyTransform + , applySimplifierX + , applyTransformX) +where +import DDC.Base.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.Snip +import DDC.Core.Transform.Flatten +import DDC.Core.Transform.Beta +import DDC.Core.Transform.Prune +import DDC.Core.Transform.Forward +import DDC.Core.Transform.Bubble +import DDC.Core.Transform.Inline +import DDC.Core.Transform.Namify +import DDC.Core.Transform.Rewrite +import DDC.Core.Transform.Elaborate +import DDC.Type.Env (KindEnv, TypeEnv) +import Data.Typeable (Typeable) +import Control.Monad.State.Strict +import Control.DeepSeq +import qualified DDC.Base.Pretty as P +import qualified Data.Set as Set + + +-- Modules -------------------------------------------------------------------- +-- | Apply a simplifier to a module. +-- +-- The state monad can be used by `Namifier` functions to generate fresh names. +--- +-- ISSUE #277: Make 'applySimplifier' return a TransformResult +-- Applying a simplifier to an expression yields a TransformResult +-- with the transform log, and we should get one for a module as well. +-- +applySimplifier + :: (Show a, Ord n, Show n, Pretty n, NFData a, NFData 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 (Module a n) + +applySimplifier !profile !kenv !tenv !spec !mm + = case spec of + Seq t1 t2 + -> do !mm' <- applySimplifier profile kenv tenv t1 mm + applySimplifier profile kenv tenv t2 mm' + + Trans t1 + -> applyTransform profile kenv tenv t1 mm + + Fix 0 _ + -> return mm + + Fix !n !s + -> do !mm' <- applySimplifier profile kenv tenv s mm + applySimplifier profile kenv tenv (Fix (n - 1) s) mm' + + +-- | Apply a transform to a module. +applyTransform + :: (Show a, Ord n, Show 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. + -> Module a n -- ^ Module to simplify. + -> State s (Module a n) + +applyTransform !profile !_kenv !_tenv !spec !mm + = case spec of + Id -> return mm + Anonymize -> return $ anonymizeX mm + Snip -> return $ snip False mm + SnipOver -> return $ snip True mm + Flatten -> return $ flatten mm + Beta -> return $ result $ betaReduce False mm + BetaLets -> return $ result $ betaReduce True mm + Forward -> return $ forwardModule profile mm + Bubble -> return $ bubbleModule mm + Namify namK namT -> namifyUnique namK namT mm + Inline getDef -> return $ inline getDef Set.empty mm + Rewrite rules -> return $ rewriteModule rules mm + Prune -> return $ pruneModule profile mm + Elaborate -> return $ elaborateModule mm + + +-- Expressions ---------------------------------------------------------------- +-- | Apply a simplifier to an expression. +-- +-- The state monad can be used by `Namifier` functions to generate fresh names. +-- +applySimplifierX + :: (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 + -> 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, Show n, Ord n, Pretty 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 + in case spec of + Id -> res xx + Anonymize -> res $ anonymizeX xx + Snip -> res $ snip False xx + SnipOver -> res $ snip True xx + Flatten -> res $ flatten xx + Inline getDef -> res $ inline getDef Set.empty xx + Beta -> return $ betaReduce False xx + BetaLets -> return $ betaReduce True xx + Prune -> return $ pruneX profile kenv tenv xx + Forward -> return $ forwardX profile xx + Bubble -> res $ bubbleX kenv tenv xx + Namify namK namT -> namifyUnique namK namT xx >>= res + Rewrite rules -> return $ rewriteX rules xx + Elaborate{} -> res $ elaborateX 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,207 @@ + +module DDC.Core.Simplifier.Base + ( -- * Simplifier Specifications + Simplifier(..) + + -- * Transform Specifications + , Transform(..) + , InlinerTemplates + , NamedRewriteRules + + -- * Transform Results + , TransformResult(..) + , TransformInfo(..) + , NoInformation(..) + , resultDone) +where +import DDC.Core.Transform.Rewrite.Rule +import DDC.Core.Transform.Namify +import DDC.Core.Exp +import DDC.Type.Env +import DDC.Base.Pretty +import qualified DDC.Base.Pretty as P +import Data.Monoid +import Data.Typeable (Typeable) + + +-- 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 + + -- | Introduce let-bindings for nested applications. + | Snip + + -- | Introduce let-bindings for nested applications and over-applied + -- functions + | SnipOver + + -- | Flatten nested let and case expressions. + | Flatten + + -- | Perform beta reduction when the argument is not a redex. + | Beta + + -- | Perform beta reduction, introducing new let-bindings for + -- arguments that are redexes. + | BetaLets + + -- | Remove unused, pure let bindings. + | Prune + + -- | Float single-use bindings forward into their use sites. + | Forward + + -- | Float casts outwards. + | Bubble + + -- | Elaborate possible Const and Distinct witnesses that aren't + -- otherwise in the program. + | Elaborate + + -- | Inline definitions into their use sites. + | Inline + { -- | Get the unfolding for a named variable. + transInlineDef :: InlinerTemplates a n } + + -- | Apply general rule-based rewrites. + | Rewrite + { -- | List of rewrite rules along with their names. + transRules :: NamedRewriteRules a n } + + -- | 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 } + + +-- | 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" + Snip -> text "Snip" + SnipOver -> text "Snip" + Flatten -> text "Flatten" + Beta -> text "Beta" + BetaLets -> text "BetaLets" + Prune -> text "Prune" + Forward -> text "Forward" + Bubble -> text "Bubble" + Inline{} -> text "Inline" + Namify{} -> text "Namify" + Rewrite{} -> text "Rewrite" + Elaborate -> text "Elaborate" + + +-- 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/Simplifier/Lexer.hs b/DDC/Core/Simplifier/Lexer.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Simplifier/Lexer.hs @@ -0,0 +1,85 @@ + +module DDC.Core.Simplifier.Lexer + ( Tok(..) + , lexSimplifier) +where +import DDC.Data.Token +import DDC.Data.SourcePos +import Data.Char + + +lexSimplifier + :: (String -> Maybe n) -- ^ Function to read a name. + -> String -- ^ String to parse. + -> [Token (Tok n)] + +lexSimplifier readName str + = map (\t -> Token t (SourcePos "" 0 0)) + $ 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,227 @@ + +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.Token +import DDC.Data.SourcePos +import DDC.Base.Parser (pTok) +import Data.Set (Set) +import qualified DDC.Base.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 = Token KEnd (SourcePos "" 0 0) + 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, Show 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 + "Snip" -> Just Snip + "SnipOver" -> Just SnipOver + "Flatten" -> Just Flatten + "Beta" -> Just Beta + "BetaLets" -> Just BetaLets + "Prune" -> Just Prune + "Forward" -> Just Forward + "Bubble" -> Just Bubble + "Elaborate" -> Just Elaborate + _ -> 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,110 @@ + +-- | Common simplifier recipes that combine multiple transforms. +module DDC.Core.Simplifier.Recipe + ( -- * Atomic recipies + idsimp + , anonymize + , snip + , snipOver + , flatten + , beta + , betaLets + , prune + , forward + , bubble + , elaborate + + -- * Compound recipies + , anormalize + , rewriteSimp) +where +import DDC.Core.Simplifier.Base +import DDC.Core.Transform.Namify +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 + + +-- | Introduce let-bindings for nested applications. +snip :: Simplifier s a n +snip = Trans Snip + + +-- | Introduce let-bindings for nested applications. +snipOver :: Simplifier s a n +snipOver = Trans SnipOver + + +-- | Flatten nested let and case expressions. +flatten :: Simplifier s a n +flatten = Trans Flatten + + +-- | Perform beta reduction +beta :: Simplifier s a n +beta = Trans Beta + + +-- | Perform beta reduction, introducing let-expressions for compound arguments. +betaLets :: Simplifier s a n +betaLets = Trans BetaLets + + +-- | Remove unused, pure let bindings. +prune :: Simplifier s a n +prune = Trans Prune + + +-- | Float single-use bindings forward into their use sites. +forward :: Simplifier s a n +forward = Trans Forward + + +-- | 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 + + +-- 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 + = Trans 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/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,24 @@ +-- | 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 Data.List - +import Data.Set (Set) +import qualified Data.Set as Set +import qualified Data.Map as Map --- | 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 ------------------------------------------------------------------------------- @@ -25,31 +30,54 @@ -- will be replaced by references into these stacks. anonymizeWithX :: forall n. Ord n - => [Bind n] -- ^ Stack for Spec binders (level-1). + => 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.keys $ 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) + = 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) @@ -57,39 +85,53 @@ XWitness w -> XWitness (down w) -instance AnonymizeX Cast where - anonymizeWithX kstack tstack cc - = 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 (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 xs + -> CastWeakenClosure (map down xs) + CastPurify w + -> CastPurify (down w) + + CastForget w + -> CastForget (down w) + + instance AnonymizeX LetMode where - anonymizeWithX kstack tstack lm - = case lm of + anonymizeWithX keep kstack tstack lm + = let down = anonymizeWithX keep kstack tstack + in case lm of LetStrict -> lm - LetLazy mw -> LetLazy $ liftM (anonymizeWithX kstack tstack) mw + LetLazy mw -> LetLazy $ liftM down mw 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 + anonymizeWithX keep kstack tstack ww + = let down = anonymizeWithX keep kstack tstack in case ww of - WVar u -> WVar (down u) + WVar u@(UName _) + | Just ix <- findIndex (boundMatchesBind u) tstack + -> WVar (UIx ix) + + WVar u -> WVar u WCon c -> WCon c WApp w1 w2 -> WApp (down w1) (down w2) WJoin w1 w2 -> WJoin (down w1) (down w2) @@ -97,78 +139,83 @@ 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 - - -- Push ---------------------------------------------------------------------- --- Push a binding occurrence of a type variable on the stack, --- returning the anonyized binding occurrence and the new stack. +-- | Push a binding occurrence of a level-0 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) + => 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`. +-- | 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) + => 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] + => 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 + -> let mode' = anonymizeWithX keep kstack tstack mode + x' = anonymizeWithX keep kstack tstack x + (tstack', b') = pushAnonymizeBindX keep kstack tstack b in (kstack, tstack', LLet mode' b' x') 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') + LLetRegions b bs + -> let (kstack', b') = mapAccumL pushAnonymizeBindT kstack b + (tstack', bs') = pushAnonymizeBindXs keep kstack' tstack bs + in (kstack', tstack', LLetRegions b' bs') LWithRegion{} -> (kstack, tstack, lts) 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,182 @@ +-- | Beta-reduce applications of a explicit lambda abstractions +-- to variables and values. module DDC.Core.Transform.Beta - (betaReduce) + ( BetaReduceInfo(..) + , betaReduce) where +import DDC.Base.Pretty +import DDC.Core.Collect import DDC.Core.Exp +import DDC.Core.Predicates +import DDC.Core.Simplifier.Base import DDC.Core.Transform.TransformX 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 Control.Monad.Writer (Writer, runWriter, tell) +import Data.Monoid (Monoid, mempty, mappend) +import Data.Typeable (Typeable) +import DDC.Type.Env (Env) +import DDC.Type.Compounds +import qualified DDC.Type.Env as Env +import qualified Data.Set as Set +------------------------------------------------------------------------------- +-- | A summary of what the beta reduction transform did. +data BetaReduceInfo + = BetaReduceInfo + { -- | 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 BetaReduceInfo where + ppr (BetaReduceInfo 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 BetaReduceInfo where + mempty = BetaReduceInfo 0 0 0 0 0 + mappend (BetaReduceInfo ty1 wit1 val1 lets1 skip1) + (BetaReduceInfo ty2 wit2 val2 lets2 skip2) + = (BetaReduceInfo + (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 BetaReduceInfo) c) + => Bool -- ^ Let-bind redexes. + -> c a n + -> TransformResult (c a n) +betaReduce lets x + = {-# SCC betaReduce #-} + let (x', info) = runWriter + $ transformUpMX (betaReduce1 lets) Env.empty Env.empty x + -- Check if any actual work was performed + progress + = case info of + BetaReduceInfo ty wit val lets' _ + -> (ty + wit + val + lets') > 0 -betaReduce1 :: Ord n => Env n -> Env n -> Exp a n -> Exp a n -betaReduce1 _ _ xx - = case xx of + in TransformResult + { result = x' + , resultAgain = progress + , resultProgress = progress + , resultInfo = TransformInfo info } + + +-- | 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 + => Bool -- ^ Let-bind redexes. + -> Env n + -> Env n + -> Exp a n + -> Writer BetaReduceInfo (Exp a n) + +betaReduce1 lets _kenv tenv 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 t2) + | isRegionKind $ typeOfBind b11 + -> let sup = support Env.empty Env.empty x12 + + usUsed = Set.unions + [ supportTyConXArg sup + , supportSpVarXArg sup ] + + usesBind = any (flip boundMatchesBind b11) + $ Set.toList usUsed + + fvs2 = freeT Env.empty t2 + + in ret mempty { infoTypes = 1} + $ if usesBind || Set.null fvs2 + then substituteTX b11 t2 x12 + else XCast a (CastWeakenClosure [XType t2]) + $ substituteTX b11 t2 x12 + + -- Substitute type arguments into type abstractions, + -- Where the argument is not a region type. XApp _ (XLAM _ b11 x12) (XType t2) - -> substituteTX b11 t2 x12 + -> ret mempty { infoTypes = 1 } + $ substituteTX b11 t2 x12 - XApp _ (XLam _ b11 x12) (XWitness w2) - -> substituteWX b11 w2 x12 + -- Substitute witness arguments into witness abstractions. + XApp a (XLam _ b11 x12) (XWitness w2) + -> let usesBind = any (flip boundMatchesBind b11) + $ Set.toList $ freeX tenv x12 + fvs2 = freeX Env.empty w2 + in ret mempty { infoWits = 1 } + $ if usesBind || Set.null fvs2 + then substituteWX b11 w2 x12 + else XCast a (CastWeakenClosure [XWitness w2]) + $ substituteWX b11 w2 x12 - XApp _ (XLam _ b11 x12) x2 - | canBetaSubstX x2 - -> substituteXX b11 x2 x12 + -- Substitute value arguments into value abstractions. + XApp a (XLam _ b11 x12) x2 + | canBetaSubstX x2 + -> let usesBind = any (flip boundMatchesBind b11) + $ Set.toList $ freeX tenv x12 + fvs2 = freeX Env.empty x2 + in ret mempty { infoValues = 1 } + $ if usesBind || Set.null fvs2 + then substituteXX b11 x2 x12 + else XCast a (CastWeakenClosure [x2]) + $ substituteXX b11 x2 x12 + + | lets + -> ret mempty { infoValuesLetted = 1 } + $ XLet a (LLet LetStrict 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 +185,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 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,346 @@ + +-- | 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.LiftX +import DDC.Core.Predicates +import DDC.Core.Compounds +import DDC.Core.Module +import DDC.Core.Exp +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 + Just a = takeAnnotOfExp 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 m b x + -> let (cs, x') = bubble kenv tenv x + Just a = takeAnnotOfExp x' + (cs', xc') = dropCasts kenv tenv a [] [b] cs x' + in (cs', LLet m 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 + Just a = takeAnnotOfExp x' + in (b, dropAllCasts kenv tenv' a cs x') + + bxs' = map bubbleRec bxs + + in ([], LRec bxs') + + LLetRegions{} -> ([], lts) + LWithRegion{} -> ([], 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 + Just a = takeAnnotOfExp 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 + + CastWeakenClosure xs : cs + -> collect weakEffs (xs ++ weakClos) others cs + + c : cs + -> collect weakEffs weakClos (c : others) cs + + + (effs, xsClos, csOthers) + = collect [] [] [] vs + + xsClos_packed + = packWeakenClosureXs kenv tenv a xsClos + + in (if null effs + then [] + else [CastWeakenEffect (TSum $ Sum.fromList kEffect effs)]) + ++ (if null xsClos_packed + then [] + else [CastWeakenClosure xsClos_packed]) + ++ csOthers + + +-- | Pack the expressions given to a `WeakenClosure` to just the ones that we +-- care about. We only need region variables, and value variables with +-- open types. +packWeakenClosureXs + :: Ord n + => KindEnv n -> TypeEnv n + -> a -> [Exp a n] -> [Exp a n] + +packWeakenClosureXs kenv tenv a xx + = let + eat fvsSp fvsDa [] + = (fvsSp, fvsDa) + + eat fvsSp fvsDa (x : xs) + = let sup = support Env.empty Env.empty x + fvsSp' = supportSpVar sup + fvsDa' = supportDaVar sup + in eat (Set.union fvsSp fvsSp') (Set.union fvsDa fvsDa') xs + + (vsSp, vsDa) = eat Set.empty Set.empty xx + + in [XType (TVar u) | u <- Set.toList vsSp] + ++ [XVar a u | u <- Set.toList vsDa, keepBound kenv tenv u] + + +-- | When packing vars given to a closure weakening, we only need to keep +-- vars that have open types or contain region handles. +keepBound :: Ord n => KindEnv n -> TypeEnv n -> Bound n -> Bool +keepBound _kenv tenv u + | Just t <- Env.lookup u tenv + , sup <- support Env.empty Env.empty t + , Set.null (supportSpVar sup) + , all (not . isRegionHandle) $ Set.toList $ supportTyCon sup + = False + + | otherwise + = True + + +-- | Treat primitive constructors with region kind as region handles. +-- Region handles are only really a part of the 'Disciple Core Eval' +-- language, but they're easy to check for even if the name type 'n' +-- hasn't been revealed. +isRegionHandle :: Bound n -> Bool +isRegionHandle u + = case u of + UPrim _ k -> isRegionKind k + _ -> False + + +-- 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,114 @@ + +-- | 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.Compounds +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 + = case cst of + CastWeakenClosure es + -> CastWeakenClosure $ map (elaborate us) es + _ -> 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 m b x -> (us, LLet m b (down x)) + LRec bs -> (us, LRec $ map (second down) bs) + + LLetRegions brs 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 + , LLetRegions brs $ 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/Flatten.hs b/DDC/Core/Transform/Flatten.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Flatten.hs @@ -0,0 +1,156 @@ + +-- | Flattening nested let and case expressions. +module DDC.Core.Transform.Flatten + (flatten) +where +import DDC.Core.Transform.LiftT +import DDC.Core.Transform.TransformX +import DDC.Core.Transform.AnonymizeX +import DDC.Core.Transform.LiftX +import DDC.Core.Exp +import DDC.Core.Compounds +import DDC.Type.Predicates +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 + +-- 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 LetStrict b1 + inner@(XLet a2 (LLet LetStrict b2 def2) x2)) + x1) + + | isBName b2 + = flatten1 + $ XLet a1 (LLet LetStrict b1 + (anonymizeX inner)) + x1 + + | otherwise + = let x1' = liftAcrossX [b1] [b2] x1 + in XLet a2 (LLet LetStrict b2 def2) + $ flatten1 + $ XLet a1 (LLet LetStrict b1 x2) + x1' + + +-- Drag 'letregion' out of the top-level of a binding. +-- @ +-- let b1 = letregion b2 in x2 in +-- x1 +-- +-- => letregion b2 in +-- let b1 = x2 in +-- x1 +-- @ +-- +-- NOTE: For region allocation this increases the lifetime of the region. +-- Maybe use a follow on transform to reduce the lifetime again. +-- +flatten1 (XLet a1 (LLet LetStrict b1 + inner@(XLet a2 (LLetRegions b2 bs2) x2)) + x1) + | all isBName b2 + = flatten1 + $ XLet a1 (LLet LetStrict b1 + (anonymizeX inner)) + x1 + + | otherwise + = let x1' = liftAcrossT [] b2 + $ liftAcrossX [b1] bs2 x1 + in XLet a2 (LLetRegions b2 bs2) + $ flatten1 + $ XLet a1 (LLet LetStrict (zapX 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 LetStrict b1 + inner@(XCase a2 x1 [AAlt p x2])) + x3) + | any isBName $ bindsOfPat p + = flatten1 + $ XLet a1 (LLet LetStrict b1 + (anonymizeX inner)) + x3 + + | otherwise + = let x3' = liftAcrossX [b1] (bindsOfPat p) x3 + in XCase a2 x1 + [AAlt p ( flatten1 + $ XLet a1 (LLet LetStrict 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 :: Ord n => [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 + + +liftAcrossT :: Ord n => [Bind n] -> [Bind n] -> Exp a n -> Exp a n +liftAcrossT bsDepth bsLevels x + = let depth = length [b | b@(BAnon _) <- bsDepth] + levels = length [b | b@(BAnon _) <- bsLevels] + in liftAtDepthT levels depth x + + +-- | Erase the type of a data binder. +zapX :: Bind n -> Bind n +zapX b = replaceTypeOfBind (tBot kData) b 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,195 @@ + +-- | Float let-bindings with a single use forward into their use-sites. +module DDC.Core.Transform.Forward + ( ForwardInfo (..) + , forwardModule + , forwardX) +where +import DDC.Base.Pretty +import DDC.Core.Analysis.Usage +import DDC.Core.Exp +import DDC.Core.Module +import DDC.Core.Simplifier.Base +import DDC.Core.Fragment +import DDC.Core.Predicates +import Data.Map (Map) +import Control.Monad +import Control.Monad.Writer (Writer, runWriter, tell) +import Data.Monoid (Monoid, mempty, mappend) +import Data.Typeable +import qualified Data.Map as Map +import qualified DDC.Core.Transform.SubstituteXX as S + +------------------------------------------------------------------------------- +-- | Summary of number of bindings floated. +data ForwardInfo + = ForwardInfo + { -- | Number of trivial @v1 = v2@ bindings inlined. + infoSubsts :: Int + + -- | Number of bindings floated forwards. + , infoBindings :: Int } + deriving Typeable + + +instance Pretty ForwardInfo where + ppr (ForwardInfo substs bindings) + = text "Forward:" + <$> indent 4 (vcat + [ text "Substitutions: " <> int substs + , text "Bindings: " <> int bindings ]) + + +instance Monoid ForwardInfo where + mempty = ForwardInfo 0 0 + mappend (ForwardInfo s1 b1)(ForwardInfo s2 b2) + = ForwardInfo (s1 + s2) (b1 + b2) + + +------------------------------------------------------------------------------- +-- | Float let-bindings in a module with a single use forward into +-- their use sites. +forwardModule + :: Ord n + => Profile n -> Module a n -> Module a n + +forwardModule profile mm + = fst $ runWriter + $ forwardWith profile Map.empty + $ usageModule mm + + +-- | Float let-bindings in an expression with a single use forward into +-- their use-sites. +forwardX :: Ord n + => Profile n -> Exp a n -> TransformResult (Exp a n) +forwardX profile xx + = let (x',info) = runWriter + $ forwardWith profile Map.empty + $ usageX xx + + progress (ForwardInfo s _) + = s > 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 + -> Map n (Exp a n) + -> c (UsedMap n, a) n + -> Writer ForwardInfo (c a n) + +instance Forward Module where + forwardWith profile bindings + (ModuleCore + { moduleName = name + , moduleExportKinds = exportKinds + , moduleExportTypes = exportTypes + , moduleImportKinds = importKinds + , moduleImportTypes = importTypes + , moduleBody = body }) + + = do body' <- forwardWith profile bindings body + return ModuleCore + { moduleName = name + , moduleExportKinds = exportKinds + , moduleExportTypes = exportTypes + , moduleImportKinds = importKinds + , moduleImportTypes = importTypes + , moduleBody = body' } + + +instance Forward Exp where + forwardWith profile bindings xx + = {-# SCC forwardWith #-} + let down = forwardWith profile 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) + + XLet (UsedMap um, _) (LLet _mode (BName n _) x1) x2 + | isXLam x1 || isXLAM x1 + , Just usage <- Map.lookup n um + , [UsedFunction] <- filterUsedInCasts usage + -> do + -- Record that we've moved this binding. + tell mempty { infoBindings = 1 } + x1' <- down x1 + forwardWith profile (Map.insert n x1' bindings) x2 + + -- Always float atomic bindings (variables, constructors) + XLet _ (LLet _mode b x1) x2 + | isAtomX x1 + -> do + -- Record that we've moved this binding. + tell mempty { infoBindings = 1 } + + -- Slow, but handles anonymous binders and shadowing + down $ S.substituteXX b 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 t -> return $ XType t + XWitness w -> return $ XWitness w + + +filterUsedInCasts :: [Used] -> [Used] +filterUsedInCasts = filter notCast + where notCast UsedInCast = False + notCast _ = True + + +instance Forward Cast where + forwardWith profile bindings xx + = let down = forwardWith profile bindings + in case xx of + CastWeakenEffect eff -> return $ CastWeakenEffect eff + CastWeakenClosure xs -> liftM CastWeakenClosure (mapM down xs) + CastPurify w -> return $ CastPurify w + CastForget w -> return $ CastForget w + + +instance Forward Lets where + forwardWith profile bindings lts + = let down = forwardWith profile bindings + in case lts of + LLet mode b x -> liftM (LLet mode b) (down x) + + LRec bxs + -> liftM LRec + $ mapM (\(b,x) + -> do x' <- down x + return (b, x')) + bxs + + LLetRegions b bs -> return $ LLetRegions b bs + LWithRegion b -> return $ LWithRegion b + + +instance Forward Alt where + forwardWith profile bindings (AAlt p x) + = liftM (AAlt p) (forwardWith profile 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,76 @@ + +-- | 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 mode b x -> LLet mode b (enter b x) + LRec bxs -> LRec [(b, enter b x) | (b, x) <- bxs] + LLetRegions{} -> lts + LWithRegion{} -> 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 + :: (Eq n, 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 + :: (Eq n, Ord n, Show 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, Show 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/Namify.hs b/DDC/Core/Transform/Namify.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Namify.hs @@ -0,0 +1,301 @@ + +-- | 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.Type.Collect +import DDC.Type.Compounds +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) + => (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 + + TForall b t + -> do (tnam', b') <- pushT tnam b + t' <- namify tnam' xnam t + return $ TForall b' t' + + TApp t1 t2 -> liftM2 TApp (down t1) (down t2) + 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 LetMode where + namify tnam xnam mm + = case mm of + LetStrict -> return mm + LetLazy Nothing -> return mm + LetLazy (Just w) -> liftM (LetLazy . Just) $ namify tnam xnam w + + +instance Namify Witness where + namify tnam xnam ww + = let down = namify tnam xnam + in case ww of + WVar u -> liftM WVar (rewriteX tnam xnam u) + WCon{} -> return ww + WApp w1 w2 -> liftM2 WApp (down w1) (down w2) + WJoin w1 w2 -> liftM2 WJoin (down w1) (down w2) + WType t -> liftM WType (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 mode b x1) x2 + -> do mode' <- down mode + x1' <- namify tnam xnam x1 + (xnam', b') <- pushX tnam xnam b + x2' <- namify tnam xnam' x2 + return $ XLet a (LLet mode' 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 (LLetRegions b bs) x2 + -> do (tnam', b') <- pushTs tnam b + (xnam', bs') <- pushXs tnam' xnam bs + x2' <- namify tnam' xnam' x2 + return $ XLet a (LLetRegions b' bs') x2' + + XLet a (LWithRegion u) x2 + -> do u' <- rewriteX tnam xnam u + x2' <- down x2 + return $ XLet a (LWithRegion u') x2' + + XCase a x1 alts -> liftM3 XCase (return a) (down x1) (mapM down alts) + XCast a c x -> liftM3 XCast (return a) (down c) (down x) + XType t -> liftM XType (down t) + XWitness w -> liftM XWitness (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) + + CastWeakenClosure xs + -> do xs' <- mapM down xs + return $ CastWeakenClosure xs' + + CastPurify w + -> liftM CastPurify (down w) + + CastForget w + -> liftM CastForget (down w) + + +-- | 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 :: Ord n + => 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,225 @@ + +-- | 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.TransformX +import DDC.Core.Fragment +import DDC.Core.Check +import DDC.Core.Module +import DDC.Core.Exp +import DDC.Type.Env +import DDC.Base.Pretty +import Data.Typeable +import Control.Monad.Writer (Writer, runWriter, tell) +import Data.Monoid (Monoid, mempty, mappend) +import qualified Data.Map as Map +import qualified Data.Set as Set +import qualified DDC.Type.Env as Env +import qualified DDC.Core.Collect as C +import qualified DDC.Core.Transform.SubstituteXX as S +import qualified DDC.Core.Transform.Trim as Trim +import qualified DDC.Type.Compounds as T +import qualified DDC.Type.Sum as TS +import qualified DDC.Type.Transform.Crush as T + + +------------------------------------------------------------------------------- +-- | 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. + | featuresUntrackedEffects + $ profileFeatures profile + = mm + + | otherwise + = mm { moduleBody + = result + $ pruneX profile (moduleKindEnv mm) (moduleTypeEnv mm) + $ 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 + -> KindEnv n -- ^ Kind environment + -> TypeEnv n -- ^ Type environment + -> Exp a n + -> TransformResult (Exp a n) + +pruneX profile kenv tenv xx + = {-# SCC pruneX #-} + let + (xx', info) + = transformTypeUsage profile kenv tenv + (transformUpMX pruneTrans kenv tenv) + 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 kenv tenv trans xx + = case checkExp (configOfProfile profile) kenv tenv xx of + Right (xx1, _, _,_) + -> let xx2 = usageX xx1 + (x', info) = runWriter (trans xx2) + x'' = reannotate (\(_, AnTEC { annotTail = a }) -> a) x' + in (x'', info) + + Left err + -> error $ renderIndent + $ vcat [ text "DDC.Core.Transform.Prune: core type error" + , ppr err ] + + +------------------------------------------------------------------------------- +-- | 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 + :: (Show a, Show n, Ord n, Pretty n) + => KindEnv n + -> TypeEnv n + -> Exp (Annot a n) n + -> Writer PruneInfo + (Exp (Annot a n) n) + +pruneTrans _ _ xx + = case xx of + XLet a@(usedMap, antec) (LLet _mode b x1) x2 + | isUnusedBind b usedMap + , isContainedEffect $ annotEffect antec + -> do + -- We still need to substitute value into casts + let x2' = transformUpX' Trim.trimX $ S.substituteXX b x1 x2 + + -- Record that we've erased a binding. + tell mempty {infoBindingsErased = 1} + + -- + return $ XCast a (weakEff antec) + $ XCast a (weakClo a x1) + $ x2' + + _ -> return xx + + where + weakEff antec + = CastWeakenEffect + $ T.crushEffect + $ annotEffect antec + + weakClo a x1 + = CastWeakenClosure + $ Trim.trimClosures a + ( (map (XType . TVar) + $ Set.toList + $ C.freeT Env.empty x1) + ++ (map (XVar a) + $ Set.toList + $ C.freeX Env.empty x1)) + + +-- | 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 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,562 @@ + +-- | Apply rewrite rules. +module DDC.Core.Transform.Rewrite + ( RewriteRule(..) + , rewriteModule + , rewriteX) +where +import DDC.Base.Pretty +import DDC.Core.Exp +import DDC.Core.Module +import Data.Map (Map) +import DDC.Core.Simplifier.Base (TransformResult(..), TransformInfo(..)) +import qualified DDC.Core.Compounds as X +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.Trim as Trim +import qualified DDC.Core.Transform.LiftX as L +import qualified DDC.Type.Compounds 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 + + +-- 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 lm b e) ws + = do e' <- down ws e + return $ LLet lm 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 LetStrict 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 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 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 LetStrict b v) values + + def' = S.substituteXArgs basK + $ S.substituteXArgs anons hole + + let_bind' = S.substituteTs basK' let_bind + lets' = lets ++ [LLet LetStrict 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 Just a = X.takeAnnotOfExp f + + let bas2 = lookupFromSubst 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 the closure of the right of the rule. + let clo' = Trim.trimClosures a + $ map (S.substituteXArgs bas3) clo + + -- 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' + $ weakclo a clo' + $ 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, Show 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 :: Ord n + => a -> Maybe (Effect n) + -> Exp a n -> Exp a n + +weakeff a meff x + = maybe x (\e -> XCast a (CastWeakenEffect e) x) meff + + +-- | Wrap an expression in a closure weakening. +weakclo :: Ord n + => a -> [Exp a n] + -> Exp a n -> Exp a n + +weakclo a clos x + = case clos of + [] -> x + _ -> XCast a (CastWeakenClosure clos) x + + +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 LetStrict 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)) + | Just a <- X.takeAnnotOfExp 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 + => [(BindMode,Bind n)] + -> (Map n (Exp a n), Map n (Type n)) + -> [(Bind n, Exp a n)] + +lookupFromSubst 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 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,203 @@ +-- | Check whether two effects are non-interfering +module DDC.Core.Transform.Rewrite.Disjoint + ( checkDisjoint + , checkDistinct ) +where +import DDC.Core.Exp +import DDC.Type.Predicates +import DDC.Type.Compounds +import qualified DDC.Core.Transform.Rewrite.Env as RE +import qualified DDC.Type.Sum as Sum +import qualified DDC.Type.Transform.Crush as TC + + +-- | 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, Show 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 $ TC.crushEffect fs + , g <- sumList $ TC.crushEffect gs ] + + | otherwise + = False + where sumList (TSum ts) = Sum.toList ts + sumList tt = [tt] + + +-- | Check whether two atomic effects are disjoint. +areDisjoint + :: (Ord n, Show 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,219 @@ +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 as T +import qualified DDC.Type.Compounds as T +import qualified DDC.Type.Predicates as T +import qualified DDC.Type.Transform.LiftT as L +import qualified DDC.Core.Transform.LiftX 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 :: Ord n => 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 (LLetRegions bs 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) + + +extendLets _ env = env + + +-- 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,80 @@ +module DDC.Core.Transform.Rewrite.Error + ( Error (..) + , Side (..)) +where +import DDC.Core.Exp +import DDC.Core.Check () +import DDC.Type.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 (Show 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,209 @@ +-- | Create substitution to make (subst template) == target +module DDC.Core.Transform.Rewrite.Match + ( -- * Substitutions + SubstInfo + , emptySubstInfo + + -- * Matching + , match) +where +import DDC.Core.Exp +import DDC.Type.Transform.Crush +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.Equiv as TE +import qualified Data.Map as Map +import qualified Data.Set as Set + + +------------------------------------------------------------------------------- +-- | 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 lc rc + = clean lc == clean rc + where clean c + = case c of + CastWeakenEffect eff -> CastWeakenEffect $ T.anonymizeT eff + CastWeakenClosure clo -> CastWeakenClosure $ map cleanX clo + CastPurify wit -> CastPurify wit + CastForget wit -> CastForget wit + + cleanX + = T.anonymizeX . T.reannotate (const ()) + +eqWit lw rw + = lw == 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 $ crushSomeT t1 + t2' = unpackSumT $ crushSomeT 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 + , TE.equivT 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,115 @@ + +-- | 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.Base.Parser as P +import qualified DDC.Type.Compounds 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 => Parser n (R.RewriteRule () n) +pRule + = do bs <- pRuleBinders + (cs,lhs) <- pRuleCsLhs + hole <- pRuleHole + pTok KEquals + rhs <- pExp + + 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 => Parser n [(n,R.RewriteRule () n)] +pRuleMany + = P.many (do + n <- pName + r <- pRule + pTok KSemiColon + return (n,r)) + + +pRuleBinders :: Ord n => Parser n [(R.BindMode,Bind n)] +pRuleBinders + = P.choice + [ do bs <- P.many1 pBinders + pTok KDot + return $ concat bs + , return [] + ] + + +pRuleCsLhs :: Ord n => Parser n ([Type n], Exp () n) +pRuleCsLhs + = P.choice + [ do cs <- P.many1 $ P.try (do + c <- pTypeApp + pTok KArrowEquals + return c) + lhs <- pExp + return (cs,lhs) + , do lhs <- pExp + return ([],lhs) + ] + + +pRuleHole :: Ord n => Parser n (Maybe (Exp () n)) +pRuleHole + = P.optionMaybe + $ do pTok KBraceBra + e <- pExp + pTok KBraceKet + return e + + +-- | Parse rewrite binders +-- +-- Many of: +-- [BIND1 BIND2 .. BINDN : TYPE] +-- or (BIND : TYPE) +-- +pBinders :: Ord n => Parser n [(R.BindMode, Bind n)] +pBinders + = P.choice + [ pBindersBetween R.BMSpec (pTok KSquareBra) (pTok KSquareKet) + , pBindersBetween (R.BMValue 0) (pTok KRoundBra) (pTok KRoundKet) + ] + + +pBindersBetween + :: Ord n + => R.BindMode + -> Parser n () + -> Parser n () + -> Parser n [(R.BindMode,Bind n)] + +pBindersBetween bm bra ket + = do bra + bs <- P.many1 pBinder + pTok KColon + t <- pType + 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,513 @@ +-- | 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.TransformX +import DDC.Core.Exp +import DDC.Core.Pretty () +import DDC.Core.Collect +import DDC.Core.Compounds +import DDC.Type.Pretty () +import DDC.Type.Env (KindEnv, TypeEnv) +import DDC.Base.Pretty +import Control.Monad +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.Check as T +import qualified DDC.Type.Compounds as T +import qualified DDC.Type.Env as T +import qualified DDC.Type.Equiv as T +import qualified DDC.Type.Predicates as T +import qualified DDC.Type.Subsumes 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 + + +-- | 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 + :: Ord n + => [(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 + :: (Ord n, Show n, Pretty n) + => C.Config n -- ^ Type checker config. + -> T.Env n -- ^ Kind environment. + -> T.Env n -- ^ Type environment. + -> RewriteRule a n -- ^ Rule to check + -> Either (Error a n) + (RewriteRule (C.AnTEC a n) n) + +checkRewriteRule config kenv tenv + (RewriteRule bs cs lhs hole rhs _ _ _) + = do + -- Extend the environments with variables bound by the rule. + let (kenv', tenv', bs') = extendBinds bs kenv tenv + let csSpread = map (S.spreadT kenv') cs + + -- Check that all constraints are valid types. + mapM_ (checkConstraint config kenv') csSpread + + -- Typecheck, spread and annotate with type information + (lhs', _, _, _) + <- checkExp config kenv' tenv' Lhs lhs + + -- If the extra left part is there, typecheck and annotate it. + hole' <- case hole of + Just h + -> do (h',_,_,_) <- checkExp config kenv' tenv' Lhs h + return $ Just h' + + Nothing -> return Nothing + + -- Build application from lhs and the hole so we can check its + -- type against rhs + let Just a = takeAnnotOfExp lhs + let lhs_full = maybe lhs (XApp a lhs) hole + + -- Check the full left hand side. + (lhs_full', tLeft, effLeft, cloLeft) + <- checkExp config kenv' tenv' Lhs lhs_full + + -- Check the full right hand side. + (rhs', tRight, effRight, cloRight) + <- checkExp config kenv' tenv' Rhs rhs + + -- Check that types of both sides are equivalent. + let err = ErrorTypeConflict + (tLeft, effLeft, cloLeft) + (tRight, effRight, cloRight) + + 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 kenv' tenv' 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)] + -> KindEnv n -> TypeEnv n + -> (T.KindEnv n, T.TypeEnv n, [(BindMode, Bind n)]) + +extendBinds binds kenv tenv + = go binds kenv tenv [] + where + go [] k t acc + = (k,t,acc) + + go ((bm,b):bs) k t acc + = let b' = S.spreadX k t b + (k',t') = case bm of + BMSpec -> (T.extend b' k, t) + BMValue _ -> (k, T.extend b' t) + + in go bs k' t' (acc ++ [(bm,b')]) + + +-- | Type check the expression on one side of the rule. +checkExp + :: (Ord n, Show n, Pretty n) + => C.Config n + -> KindEnv n -- ^ Kind environment of expression. + -> TypeEnv n -- ^ Type environment of expression. + -> 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, Closure n) + +checkExp defs kenv tenv side xx + = let xx' = S.spreadX kenv tenv xx + in case C.checkExp defs kenv tenv 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 + -> KindEnv n -- ^ Kind environment of the constraint. + -> Type n -- ^ The constraint type to check. + -> Either (Error a n) (Kind n) + +checkConstraint defs kenv tt + = case T.checkType (C.configPrimDataDefs defs) kenv 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 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, Show 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 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 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 + -> T.Env n -- ^ Kind environment. + -> T.Env n -- ^ Type 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 kenv tenv lhs rhs + = let lhs' = removeEffects config kenv tenv lhs + supportLeft = support Env.empty Env.empty lhs' + daLeft = supportDaVar supportLeft + wiLeft = supportWiVar supportLeft + spLeft = supportSpVar supportLeft + + rhs' = removeEffects config kenv tenv rhs + supportRight = support Env.empty Env.empty rhs' + daRight = supportDaVar supportRight + wiRight = supportWiVar supportRight + spRight = supportSpVar supportRight + + Just a = takeAnnotOfExp lhs + + in Right + $ [XVar a u + | u <- Set.toList $ daLeft `Set.difference` daRight ] + + ++ [XWitness (WVar u) + | u <- Set.toList $ wiLeft `Set.difference` wiRight ] + + ++ [XType (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 + -> T.Env n -- ^ Kind environment + -> T.Env n -- ^ Type environment + -> Exp a n -- ^ Target expression - has all effects replaced with bottom. + -> Exp a n +removeEffects config = transformUpX remove + where + remove kenv _tenv x + + | XType et <- x + , Right k <- T.checkType (C.configPrimDataDefs config) + kenv et + , T.isEffectKind k + = XType $ T.tBot T.kEffect + + | otherwise + = x + + +-- Structural Checks ---------------------------------------------------------- +-- | Check for rule variables that have no uses. +checkUnmentionedBinders + :: (Ord n, Show 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 t) = go_t t + go (XWitness _) = return () + + go_t (TVar _) = return () + go_t (TCon _) = return () + go_t t@(TForall _ _) = Left $ ErrorNotFirstOrder (XType t) + go_t (TApp l r) = go_t l >> go_t r + 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 Just (U.UsedMap um) + = liftM fst $ takeAnnotOfExp $ 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,300 @@ + +-- | Snip out nested applications. +module DDC.Core.Transform.Snip + (Snip(..)) +where +import DDC.Core.Analysis.Arity +import DDC.Core.Module +import DDC.Core.Exp +import DDC.Core.Compounds +import qualified DDC.Core.Transform.LiftX as L +import qualified DDC.Type.Compounds as T + + +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 + => Bool -- ^ Introduce extra bindings for over-applied functions. + -> c n + -> c n + + +instance Snip (Module a) where + snip bOver mm + = {-# SCC "snip[Module]" #-} + let arities = aritiesOfModule mm + body' = snipX bOver arities (moduleBody mm) [] + in mm { moduleBody = body' } + + +instance Snip (Exp a) where + snip bOver x + = {-# SCC "snip[Exp]" #-} + snipX bOver emptyArities x [] + + +-- | Convert an expression into A-normal form. +snipX + :: Ord n + => Bool -- ^ Introduce extra bindings for over-applied functions. + -> 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 bOver 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 bOver arities fun $ (snipX bOver arities arg [], a) : args + + -- Some non-application node with no arguments. + | null args + = enterX bOver arities x + + -- Some non-application node being applied to arguments. + | otherwise + = buildNormalisedApp bOver arities (enterX bOver arities x) args + +-- Enter into a non-application. +enterX bOver arities xx + = let down ars e + = snipX bOver (extendsArities arities ars) e [] + + in case xx of + -- The snipX function shouldn't have called us with an XApp. + XApp{} + -> error "DDC.Core.Transform.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 m b x1) x2 + -> let x1' = down [] x1 + x2' = down [(b, arityOfExp' x1')] x2 + in XLet a (LLet m 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' = down ars x2 + in XLet a (LRec $ zip bs xs') x2' + + -- letregion, just make sure we record bindings with dummy val. + XLet a (LLetRegions b bs) x2 + -> let ars = zip bs (repeat 0) + in XLet a (LLetRegions b bs) (down ars x2) + + -- withregion + XLet a (LWithRegion b) z2 + -> XLet a (LWithRegion b) (down [] z2) + + -- 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] + + in XLet a (LLet LetStrict (BAnon (T.tBot T.kData)) e') + (XCase a (XVar a $ UIx 0) + (map (L.liftX 1) alts')) + + -- 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 +-- on-atomic arguments are bound via let-expressions, then the +-- associated let-bound variable is passed to the function. +buildNormalisedApp + :: Ord n + => Bool -- ^ Introduce extra bindings for over-applied functions. + -> 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 _bOver _ f0 [] = f0 +buildNormalisedApp bOver 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 bOver 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 LetStrict (BAnon tBot') xFun) + (buildNormalisedFunApp bOver 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 + :: Ord n + => Bool -- ^ Introduce extra bindings for over-applied functions. + -> 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 bOver 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 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. + | bOver + , length xsArgs' > funArity + , (xsSat, xsOver) <- splitAt funArity xsArgs' + = XLet an (LLet LetStrict (BAnon tBot') + (makeXAppsWithAnnots xFun' xsSat)) + (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 foldr (\(x, a) x' -> XLet a x x') + xFunApps + [ (LLet LetStrict (BAnon tBot') x, a) + | (x, a) <- xsLets' ] + + +-- | Sort function arguments into either the atomic ones, +-- or compound ones. +splitArgs + :: Ord n + => [(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 args + = reverse $ go 0 $ reverse args + where + go _n [] = [] + go n ((xArg, a) : xsArgs) + | isAtom xArg + = (xArg, a, True, Nothing) : go n xsArgs + + | otherwise + = (XVar a (UIx n), a, False, Just xArg) : go (n + 1) xsArgs + + +-- | Check if an expression needs a binding, or if it's simple enough to be +-- applied as-is. +isAtom :: Ord n => Exp a n -> Bool +isAtom xx + = case xx of + XVar{} -> True + XCon{} -> True + XType{} -> True + XWitness{} -> True + + -- 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/TransformX.hs b/DDC/Core/Transform/TransformX.hs --- a/DDC/Core/Transform/TransformX.hs +++ b/DDC/Core/Transform/TransformX.hs @@ -2,11 +2,13 @@ -- | General purpose tree walking boilerplate. module DDC.Core.Transform.TransformX ( TransformUpMX(..) - , transformUpX) + , transformUpX + , transformUpX') where +import DDC.Core.Module import DDC.Core.Exp import DDC.Core.Compounds -import DDC.Type.Env (Env) +import DDC.Type.Env (KindEnv, TypeEnv) import Data.Functor.Identity import Control.Monad import qualified DDC.Type.Env as Env @@ -16,10 +18,10 @@ transformUpX :: forall (c :: * -> * -> *) a n . (Ord n, TransformUpMX Identity c) - => (Env n -> Env n -> Exp a n -> Exp a n) + => (KindEnv n -> TypeEnv 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. + -> KindEnv n -- ^ Initial kind environment. + -> TypeEnv n -- ^ Initial type environment. -> c a n -- ^ Transform this thing. -> c a n @@ -30,20 +32,44 @@ kenv tenv 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) Env.empty Env.empty 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. + => (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 => TransformUpMX m Module where + transformUpMX f kenv tenv !mm + = do x' <- transformUpMX f kenv tenv $ moduleBody mm + return $ mm { moduleBody = x' } + + instance Monad m => TransformUpMX m Exp where - transformUpMX f kenv tenv xx - = (f kenv tenv =<<) + transformUpMX f kenv tenv !xx + = {-# SCC transformUpMX #-} + (f kenv tenv =<<) $ case xx of XVar{} -> return xx XCon{} -> return xx @@ -95,7 +121,7 @@ xs' <- mapM (transformUpMX f kenv tenv') xs return $ LRec $ zip bs xs' - LLetRegion{} -> return xx + LLetRegions{} -> return xx LWithRegion{} -> return xx @@ -110,3 +136,4 @@ AAlt PDefault x -> liftM2 AAlt (return PDefault) (transformUpMX f kenv tenv x) + 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,53 @@ + +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) + TForall b t -> TForall (alpha f b) (alpha f t) + TApp t1 t2 -> TApp (alpha f t1) (alpha f t2) + 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 t -> TyConBound (alpha f u) (alpha f t) + 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 @@ -57,17 +57,22 @@ 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 + :: Ord n + => [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/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.3.1.1 License: MIT License-file: LICENSE Author: The Disciplined Disciple Compiler Strike Force @@ -10,27 +10,56 @@ 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.*, + deepseq == 1.3.*, containers == 0.5.*, - array >= 0.3 && < 0.5, + array == 0.4.*, transformers == 0.3.*, mtl == 2.1.*, - ddc-base == 0.2.1.*, - ddc-core == 0.2.1.* + ddc-base == 0.3.1.*, + ddc-core == 0.3.1.* Exposed-modules: + DDC.Core.Analysis.Arity + DDC.Core.Analysis.Usage + DDC.Core.Simplifier.Recipe + DDC.Core.Simplifier.Parser + 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.Bubble + DDC.Core.Transform.Prune + DDC.Core.Transform.Elaborate + DDC.Core.Transform.Flatten + DDC.Core.Transform.Forward + DDC.Core.Transform.Inline + DDC.Core.Transform.Namify + DDC.Core.Transform.Rewrite + DDC.Core.Transform.Snip DDC.Core.Transform.TransformX + DDC.Core.Simplifier + + DDC.Type.Transform.Alpha DDC.Type.Transform.AnonymizeT - DDC.Type.Transform.Rename - + + Other-modules: + DDC.Core.Simplifier.Apply + DDC.Core.Simplifier.Lexer + DDC.Core.Simplifier.Base + + DDC.Core.Transform.Inline.Templates + DDC.Core.Transform.Rewrite.Error + + GHC-options: -Wall -fno-warn-orphans @@ -38,10 +67,18 @@ -fno-warn-unused-do-bind Extensions: + BangPatterns NoMonomorphismRestriction + ParallelListComp ExplicitForAll KindSignatures PatternGuards MultiParamTypeClasses FlexibleContexts FlexibleInstances + RankNTypes + ExistentialQuantification + DeriveDataTypeable + ScopedTypeVariables + +