ddc-core-simpl 0.2.1.2 → 0.3.1.1

raw patch · 32 files changed

+5413/−417 lines, 32 filesdep +deepseqdep ~arraydep ~ddc-basedep ~ddc-corePVP ok

version bump matches the API change (PVP)

Dependencies added: deepseq

Dependency ranges changed: array, ddc-base, ddc-core

API changes (from Hackage documentation)

Files

• DDC/Core/Analysis/Arity.hs +142/−0
• DDC/Core/Analysis/Usage.hs +248/−0
• DDC/Core/Simplifier.hs +21/−0
• DDC/Core/Simplifier/Apply.hs +240/−0
• DDC/Core/Simplifier/Base.hs +207/−0
• DDC/Core/Simplifier/Lexer.hs +85/−0
• DDC/Core/Simplifier/Parser.hs +227/−0
• DDC/Core/Simplifier/Recipe.hs +110/−0
• DDC/Core/Transform/ANormal.hs +0/−253
• DDC/Core/Transform/AnonymizeX.hs +115/−68
• DDC/Core/Transform/Beta.hs +160/−17
• DDC/Core/Transform/Bubble.hs +346/−0
• DDC/Core/Transform/Elaborate.hs +114/−0
• DDC/Core/Transform/Flatten.hs +156/−0
• DDC/Core/Transform/Forward.hs +195/−0
• DDC/Core/Transform/Inline.hs +76/−0
• DDC/Core/Transform/Inline/Templates.hs +96/−0
• DDC/Core/Transform/Namify.hs +301/−0
• DDC/Core/Transform/Prune.hs +225/−0
• DDC/Core/Transform/Rewrite.hs +562/−0
• DDC/Core/Transform/Rewrite/Disjoint.hs +203/−0
• DDC/Core/Transform/Rewrite/Env.hs +219/−0
• DDC/Core/Transform/Rewrite/Error.hs +80/−0
• DDC/Core/Transform/Rewrite/Match.hs +209/−0
• DDC/Core/Transform/Rewrite/Parser.hs +115/−0
• DDC/Core/Transform/Rewrite/Rule.hs +513/−0
• DDC/Core/Transform/Snip.hs +300/−0
• DDC/Core/Transform/TransformX.hs +39/−12
• DDC/Type/Transform/Alpha.hs +53/−0
• DDC/Type/Transform/AnonymizeT.hs +10/−5
• DDC/Type/Transform/Rename.hs +0/−53
• ddc-core-simpl.cabal +46/−9

@@ -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)+

@@ -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')++

@@ -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

@@ -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+    

@@ -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

@@ -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 "<simplifier spec>" 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)

@@ -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 "<simplifier spec>" 0 0)+        toks    = lexSimplifier readName str ++ [kend]+   in   P.runTokenParser show "<simplifier spec>" +                (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++

@@ -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)+

@@ -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

@@ -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)

@@ -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

@@ -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+

@@ -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+

@@ -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

@@ -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)+

@@ -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)++

@@ -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+

@@ -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)

@@ -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]+

@@ -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+

@@ -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+

@@ -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+

@@ -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+

@@ -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+

@@ -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)+

@@ -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+

@@ -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+

@@ -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) +

@@ -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)+

@@ -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

@@ -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-

@@ -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++