diff --git a/hermit.cabal b/hermit.cabal --- a/hermit.cabal +++ b/hermit.cabal @@ -1,5 +1,5 @@ Name: hermit -Version: 0.1.4.0 +Version: 0.1.6.0 Synopsis: Haskell Equational Reasoning Model-to-Implementation Tunnel Description: HERMIT uses Haskell to express semi-formal models, @@ -38,12 +38,12 @@ . @ $ hermit Reverse.hs Reverse.hss resume - [starting HERMIT v0.1.4.0 on Reverse.hs] + [starting HERMIT v0.1.6.0 on Reverse.hs] % ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:main:Main: -fplugin-opt=HERMIT:main:Main:resume [1 of 2] Compiling HList ( HList.hs, HList.o ) Loading package ghc-prim ... linking ... done. ... - Loading package hermit-0.1.4.0 ... linking ... done. + Loading package hermit-0.1.6.0 ... linking ... done. [2 of 2] Compiling Main ( Reverse.hs, Reverse.o ) Linking Reverse ... $ ./Reverse @@ -54,12 +54,12 @@ . @ $ hermit Reverse.hs - [starting HERMIT v0.1.4.0 on Reverse.hs] + [starting HERMIT v0.1.6.0 on Reverse.hs] % ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:main:Main: [1 of 2] Compiling HList ( HList.hs, HList.o ) Loading package ghc-prim ... linking ... done. ... - Loading package hermit-0.1.4.0 ... linking ... done. + Loading package hermit-0.1.6.0 ... linking ... done. [2 of 2] Compiling Main ( Reverse.hs, Reverse.o ) module main:Main where \ \ rev ∷ ∀ a . [] a -> [] a @@ -135,7 +135,7 @@ data-default >= 0.5.0, ghc == 7.6.*, haskeline >= 0.7.0.3, - kure >= 2.4.10, + kure >= 2.6.14, marked-pretty >= 0.1, mtl >= 2.1.2, stm >= 2.4, diff --git a/src/Language/HERMIT/Context.hs b/src/Language/HERMIT/Context.hs --- a/src/Language/HERMIT/Context.hs +++ b/src/Language/HERMIT/Context.hs @@ -5,7 +5,6 @@ HermitC , initHermitC -- ** Adding to the Context - , (@@) , addAltBindings , addBinding , addCaseBinding @@ -65,16 +64,16 @@ -- | The HERMIT context stores an 'AbsolutePath' to the current node in the tree. instance PathContext HermitC where - contextPath :: HermitC -> AbsolutePath - contextPath = hermitPath + absPath :: HermitC -> AbsolutePath + absPath = hermitPath + (@@) :: HermitC -> Int -> HermitC + c @@ n = c { hermitPath = hermitPath c @@ n } + + -- | Create the initial HERMIT 'HermitC' by providing a 'ModGuts'. initHermitC :: ModGuts -> HermitC initHermitC modGuts = HermitC empty 0 rootAbsPath modGuts - --- | Update the context by extending the stored 'AbsolutePath' to a child. -(@@) :: HermitC -> Int -> HermitC -(@@) c v = c { hermitPath = extendAbsPath v (hermitPath c) } ------------------------------------------------------------------------ diff --git a/src/Language/HERMIT/Core.hs b/src/Language/HERMIT/Core.hs --- a/src/Language/HERMIT/Core.hs +++ b/src/Language/HERMIT/Core.hs @@ -26,20 +26,19 @@ --------------------------------------------------------------------- -- $typenote --- NOTE: 'Type' is not included in the generic datatype. +-- NOTE: 'Type' is not included in the sum type. -- However, we could have included it and provided the facility for descending into types. -- We have not done so because -- (a) we do not need that functionality, and -- (b) the types are complicated and we're not sure that we understand them. -- | Core is the sum type of all nodes in the AST that we wish to be able to traverse. --- All 'Node' instances in HERMIT define their 'Generic' type to be 'Core'. -data Core = ModGutsCore ModGuts -- ^ The module. - | ProgCore CoreProg -- ^ A program (a telescope of top-level binding groups). - | BindCore CoreBind -- ^ A binding group. - | DefCore CoreDef -- ^ A recursive definition. - | ExprCore CoreExpr -- ^ An expression. - | AltCore CoreAlt -- ^ A case alternative. +data Core = GutsCore ModGuts -- ^ The module. + | ProgCore CoreProg -- ^ A program (a telescope of top-level binding groups). + | BindCore CoreBind -- ^ A binding group. + | DefCore CoreDef -- ^ A recursive definition. + | ExprCore CoreExpr -- ^ An expression. + | AltCore CoreAlt -- ^ A case alternative. --------------------------------------------------------------------- diff --git a/src/Language/HERMIT/External.hs b/src/Language/HERMIT/External.hs --- a/src/Language/HERMIT/External.hs +++ b/src/Language/HERMIT/External.hs @@ -1,5 +1,4 @@ -{-# LANGUAGE TypeFamilies, DeriveDataTypeable, FlexibleContexts, - GADTs, TypeSynonymInstances, FlexibleInstances #-} +{-# LANGUAGE TypeFamilies, DeriveDataTypeable, FlexibleContexts, GADTs, TypeSynonymInstances, FlexibleInstances #-} module Language.HERMIT.External ( @@ -73,8 +72,8 @@ | PreCondition -- ^ Operation has a precondition. | Debug -- ^ Commands to help debugging. | VersionControl -- ^ Version control. - | Bash -- ^ Commands that are run by 'Language.HERMIT.Dicitonary.bash'. - | Context -- ^ a command that uses its context, like inline + | Bash -- ^ Commands that are run by 'Language.HERMIT.Dictionary.bash'. + | Context -- ^ A command that uses its context, such as inline | TODO -- ^ TODO: check before the release. diff --git a/src/Language/HERMIT/Kernel.hs b/src/Language/HERMIT/Kernel.hs --- a/src/Language/HERMIT/Kernel.hs +++ b/src/Language/HERMIT/Kernel.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, TypeFamilies, DeriveDataTypeable, TupleSections #-} +{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, DeriveDataTypeable, TupleSections #-} module Language.HERMIT.Kernel ( -- * The HERMIT Kernel diff --git a/src/Language/HERMIT/Kernel/Scoped.hs b/src/Language/HERMIT/Kernel/Scoped.hs --- a/src/Language/HERMIT/Kernel/Scoped.hs +++ b/src/Language/HERMIT/Kernel/Scoped.hs @@ -47,10 +47,6 @@ localPath2Path :: LocalPath -> Path localPath2Path (LocalPath p) = reverse p --- Convert between path representations. --- path2LocalPath :: Path -> LocalPath --- path2LocalPath p = LocalPath (reverse p) - localPaths2Paths :: [LocalPath] -> [Path] localPaths2Paths = reverse . map localPath2Path diff --git a/src/Language/HERMIT/Kure.hs b/src/Language/HERMIT/Kure.hs --- a/src/Language/HERMIT/Kure.hs +++ b/src/Language/HERMIT/Kure.hs @@ -1,21 +1,17 @@ -{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, FlexibleInstances, FlexibleContexts, TupleSections, LambdaCase, InstanceSigs #-} - --- Note: InstanceSigs don't expand type families (annoyingly), as of GHC 7.6.1. Check if this has been fixed in the next version. +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TupleSections, LambdaCase, InstanceSigs, ScopedTypeVariables #-} module Language.HERMIT.Kure ( - -- * KURE Modules + -- * KURE -- | All the required functionality of KURE is exported here, so other modules do not need to import KURE directly. module Language.KURE - , module Language.KURE.Injection - , KureM, runKureM, fromKureM + , module Language.KURE.Lens -- * Synonyms -- | In HERMIT, 'Translate', 'Rewrite' and 'Lens' always operate on the same context and monad. , TranslateH , RewriteH , LensH - , idR -- * Congruence combinators -- ** Modguts , modGutsT, modGutsR @@ -70,555 +66,350 @@ import GhcPlugins hiding (empty) import Language.KURE -import Language.KURE.Injection -import Language.KURE.Utilities +import Language.KURE.Lens import Language.HERMIT.Core import Language.HERMIT.Context import Language.HERMIT.Monad -import Control.Applicative -import qualified Control.Category - -import Data.Monoid +import Control.Monad --------------------------------------------------------------------- type TranslateH a b = Translate HermitC HermitM a b -type RewriteH a = Rewrite HermitC HermitM a -type LensH a b = Lens HermitC HermitM a b +type RewriteH a = Rewrite HermitC HermitM a +type LensH a b = Lens HermitC HermitM a b --- | A synonym for the identity rewrite. Convienient to avoid importing Control.Category. -idR :: RewriteH a -idR = Control.Category.id +-- I find it annoying that Applicative is not a superclass of Monad. +(<$>) :: Monad m => (a -> b) -> m a -> m b +(<$>) = liftM +{-# INLINE (<$>) #-} +(<*>) :: Monad m => m (a -> b) -> m a -> m b +(<*>) = ap +{-# INLINE (<*>) #-} + --------------------------------------------------------------------- -instance Node Core where - type Generic Core = Core +instance Injection ModGuts Core where - numChildren :: Core -> Int - numChildren (ModGutsCore x) = numChildren x - numChildren (ProgCore x) = numChildren x - numChildren (BindCore x) = numChildren x - numChildren (DefCore x) = numChildren x - numChildren (ExprCore x) = numChildren x - numChildren (AltCore x) = numChildren x + inject :: ModGuts -> Core + inject = GutsCore --- Defining Walker instances for the Generic type 'Core' is almost entirely automated by KURE. --- Unfortunately, you still need to pattern match on the 'Core' data type. + project :: Core -> Maybe ModGuts + project (GutsCore guts) = Just guts + project _ = Nothing -instance Walker HermitC HermitM Core where - childL :: Int -> LensH Core (Generic Core) - childL n = lens $ translate $ \ c -> \case - ModGutsCore x -> childLgeneric n c x - ProgCore x -> childLgeneric n c x - BindCore x -> childLgeneric n c x - DefCore x -> childLgeneric n c x - ExprCore x -> childLgeneric n c x - AltCore x -> childLgeneric n c x +instance Injection CoreProg Core where - allT :: Monoid b => TranslateH (Generic Core) b -> TranslateH Core b - allT t = translate $ \ c -> \case - ModGutsCore x -> allTgeneric t c x - ProgCore x -> allTgeneric t c x - BindCore x -> allTgeneric t c x - DefCore x -> allTgeneric t c x - ExprCore x -> allTgeneric t c x - AltCore x -> allTgeneric t c x + inject :: CoreProg -> Core + inject = ProgCore - oneT :: TranslateH (Generic Core) b -> TranslateH Core b - oneT t = translate $ \ c -> \case - ModGutsCore x -> oneTgeneric t c x - ProgCore x -> oneTgeneric t c x - BindCore x -> oneTgeneric t c x - DefCore x -> oneTgeneric t c x - ExprCore x -> oneTgeneric t c x - AltCore x -> oneTgeneric t c x + project :: Core -> Maybe CoreProg + project (ProgCore bds) = Just bds + project _ = Nothing - allR :: RewriteH (Generic Core) -> RewriteH Core - allR r = rewrite $ \ c -> \case - ModGutsCore x -> allRgeneric r c x - ProgCore x -> allRgeneric r c x - BindCore x -> allRgeneric r c x - DefCore x -> allRgeneric r c x - ExprCore x -> allRgeneric r c x - AltCore x -> allRgeneric r c x - anyR :: RewriteH (Generic Core) -> RewriteH Core - anyR r = rewrite $ \ c -> \case - ModGutsCore x -> anyRgeneric r c x - ProgCore x -> anyRgeneric r c x - BindCore x -> anyRgeneric r c x - DefCore x -> anyRgeneric r c x - ExprCore x -> anyRgeneric r c x - AltCore x -> anyRgeneric r c x +instance Injection CoreBind Core where - oneR :: RewriteH (Generic Core) -> RewriteH Core - oneR r = rewrite $ \ c -> \case - ModGutsCore x -> oneRgeneric r c x - ProgCore x -> oneRgeneric r c x - BindCore x -> oneRgeneric r c x - DefCore x -> oneRgeneric r c x - ExprCore x -> oneRgeneric r c x - AltCore x -> oneRgeneric r c x + inject :: CoreBind -> Core + inject = BindCore ---------------------------------------------------------------------- + project :: Core -> Maybe CoreBind + project (BindCore bnd) = Just bnd + project _ = Nothing -instance Injection ModGuts Core where - inject :: ModGuts -> Core - inject = ModGutsCore +instance Injection CoreDef Core where - retract :: Core -> Maybe ModGuts - retract (ModGutsCore guts) = Just guts - retract _ = Nothing + inject :: CoreDef -> Core + inject = DefCore -instance Node ModGuts where - type Generic ModGuts = Core + project :: Core -> Maybe CoreDef + project (DefCore def) = Just def + project _ = Nothing - numChildren :: ModGuts -> Int - numChildren _ = 1 -instance Walker HermitC HermitM ModGuts where +instance Injection CoreAlt Core where - childL :: Int -> LensH ModGuts (Generic ModGuts) - childL 0 = lens $ modGutsT exposeT (childL1of2 $ \ modguts p -> modguts {mg_binds = progToBinds p}) - childL n = failT (missingChild n) + inject :: CoreAlt -> Core + inject = AltCore --- | Translate a module. --- Slightly different to the other congruence combinators: it passes in *all* of the original to the reconstruction function. -modGutsT :: TranslateH CoreProg a -> (ModGuts -> a -> b) -> TranslateH ModGuts b -modGutsT t f = translate $ \ c modGuts -> f modGuts <$> apply t (c @@ 0) (bindsToProg (mg_binds modGuts)) + project :: Core -> Maybe CoreAlt + project (AltCore expr) = Just expr + project _ = Nothing --- | Rewrite the 'CoreProg' child of a module. -modGutsR :: RewriteH CoreProg -> RewriteH ModGuts -modGutsR r = modGutsT r (\ modguts p -> modguts {mg_binds = progToBinds p}) +instance Injection CoreExpr Core where + + inject :: CoreExpr -> Core + inject = ExprCore + + project :: Core -> Maybe CoreExpr + project (ExprCore expr) = Just expr + project _ = Nothing + --------------------------------------------------------------------- -instance Injection CoreProg Core where +instance Walker HermitC Core where - inject :: CoreProg -> Core - inject = ProgCore + allR :: forall m. MonadCatch m => Rewrite HermitC m Core -> Rewrite HermitC m Core + allR r = prefixFailMsg "allR failed: " $ + rewrite $ \ c -> \case + GutsCore guts -> inject <$> apply allRmodguts c guts + ProgCore p -> inject <$> apply allRprog c p + BindCore bn -> inject <$> apply allRbind c bn + DefCore def -> inject <$> apply allRdef c def + AltCore alt -> inject <$> apply allRalt c alt + ExprCore e -> inject <$> apply allRexpr c e + where + allRmodguts :: MonadCatch m => Rewrite HermitC m ModGuts + allRmodguts = modGutsR (extractR r) + {-# INLINE allRmodguts #-} - retract :: Core -> Maybe CoreProg - retract (ProgCore bds) = Just bds - retract _ = Nothing + allRprog :: MonadCatch m => Rewrite HermitC m CoreProg + allRprog = readerT $ \case + ProgCons _ _ -> progConsAllR (extractR r) (extractR r) + _ -> idR + {-# INLINE allRprog #-} -instance Node CoreProg where - type Generic CoreProg = Core + allRbind :: MonadCatch m => Rewrite HermitC m CoreBind + allRbind = readerT $ \case + NonRec _ _ -> nonRecR (extractR r) + Rec _ -> recAllR (const $ extractR r) + {-# INLINE allRbind #-} - -- A program is either empty (zero children) or a binding group and the remaining program it scopes over (two children). - numChildren :: CoreProg -> Int - numChildren ProgNil = 0 - numChildren (ProgCons _ _) = 2 + allRdef :: MonadCatch m => Rewrite HermitC m CoreDef + allRdef = defR (extractR r) + {-# INLINE allRdef #-} -instance Walker HermitC HermitM CoreProg where + allRalt :: MonadCatch m => Rewrite HermitC m CoreAlt + allRalt = altR (extractR r) + {-# INLINE allRalt #-} - childL :: Int -> LensH CoreProg (Generic CoreProg) - childL 0 = lens $ progConsT exposeT idR (childL0of2 ProgCons) - childL 1 = lens $ progConsT idR exposeT (childL1of2 ProgCons) - childL n = failT (missingChild n) + allRexpr :: MonadCatch m => Rewrite HermitC m CoreExpr + allRexpr = readerT $ \case + App _ _ -> appAllR (extractR r) (extractR r) + Lam _ _ -> lamR (extractR r) + Let _ _ -> letAllR (extractR r) (extractR r) + Case _ _ _ _ -> caseAllR (extractR r) (const $ extractR r) + Cast _ _ -> castR (extractR r) + Tick _ _ -> tickR (extractR r) + _ -> idR + {-# INLINE allRexpr #-} +--------------------------------------------------------------------- + +-- | Translate a module. +-- Slightly different to the other congruence combinators: it passes in /all/ of the original to the reconstruction function. +modGutsT :: Monad m => Translate HermitC m CoreProg a -> (ModGuts -> a -> b) -> Translate HermitC m ModGuts b +modGutsT t f = translate $ \ c guts -> f guts <$> apply t (c @@ 0) (bindsToProg $ mg_binds guts) + +-- | Rewrite the 'CoreProg' child of a module. +modGutsR :: Monad m => Rewrite HermitC m CoreProg -> Rewrite HermitC m ModGuts +modGutsR r = modGutsT r (\ guts p -> guts {mg_binds = progToBinds p}) + +--------------------------------------------------------------------- + -- | Translate an empty list. -progNilT :: b -> TranslateH CoreProg b +progNilT :: Monad m => b -> Translate HermitC m CoreProg b progNilT b = contextfreeT $ \case - ProgNil -> pure b + ProgNil -> return b ProgCons _ _ -> fail "not an empty program node." -progConsT' :: TranslateH CoreBind a1 -> TranslateH CoreProg a2 -> (HermitM a1 -> HermitM a2 -> HermitM b) -> TranslateH CoreProg b -progConsT' t1 t2 f = translate $ \ c -> \case - ProgCons bd p -> f (apply t1 (c @@ 0) bd) (apply t2 (addBinding bd c @@ 1) p) - _ -> fail "not a non-empty program node." - -- | Translate a program of the form: ('CoreBind' @:@ 'CoreProg') -progConsT :: TranslateH CoreBind a1 -> TranslateH CoreProg a2 -> (a1 -> a2 -> b) -> TranslateH CoreProg b -progConsT t1 t2 f = progConsT' t1 t2 (liftA2 f) +progConsT :: Monad m => Translate HermitC m CoreBind a1 -> Translate HermitC m CoreProg a2 -> (a1 -> a2 -> b) -> Translate HermitC m CoreProg b +progConsT t1 t2 f = translate $ \ c -> \case + ProgCons bd p -> f <$> apply t1 (c @@ 0) bd <*> apply t2 (addBinding bd c @@ 1) p + _ -> fail "not a non-empty program node." -- | Rewrite all children of a program of the form: ('CoreBind' @:@ 'CoreProg') -progConsAllR :: RewriteH CoreBind -> RewriteH CoreProg -> RewriteH CoreProg +progConsAllR :: Monad m => Rewrite HermitC m CoreBind -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg progConsAllR r1 r2 = progConsT r1 r2 ProgCons -- | Rewrite any children of a program of the form: ('CoreBind' @:@ 'CoreProg') -progConsAnyR :: RewriteH CoreBind -> RewriteH CoreProg -> RewriteH CoreProg -progConsAnyR r1 r2 = progConsT' (attemptR r1) (attemptR r2) (attemptAny2 ProgCons) +progConsAnyR :: MonadCatch m => Rewrite HermitC m CoreBind -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg +progConsAnyR r1 r2 = unwrapAnyR $ progConsAllR (wrapAnyR r1) (wrapAnyR r2) -- | Rewrite one child of a program of the form: ('CoreBind' @:@ 'CoreProg') -progConsOneR :: RewriteH CoreBind -> RewriteH CoreProg -> RewriteH CoreProg -progConsOneR r1 r2 = progConsT' (withArgumentT r1) (withArgumentT r2) (attemptOne2 ProgCons) +progConsOneR :: MonadCatch m => Rewrite HermitC m CoreBind -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg +progConsOneR r1 r2 = unwrapOneR $ progConsAllR (wrapOneR r1) (wrapOneR r2) --------------------------------------------------------------------- -instance Injection CoreBind Core where - - inject :: CoreBind -> Core - inject = BindCore - - retract :: Core -> Maybe CoreBind - retract (BindCore bnd) = Just bnd - retract _ = Nothing - -instance Node CoreBind where - type Generic CoreBind = Core - - numChildren :: CoreBind -> Int - numChildren (NonRec _ _) = 1 - numChildren (Rec defs) = length defs - -instance Walker HermitC HermitM CoreBind where - - childL :: Int -> LensH CoreBind (Generic CoreBind) - childL n = lens $ setFailMsg (missingChild n) $ - case n of - 0 -> nonrec <+ rec - _ -> rec - - where - nonrec = nonRecT exposeT (childL1of2 NonRec) - rec = whenM (hasChildT n) $ - recT (const exposeT) (childLMofN n defsToRecBind) - - allT :: Monoid b => TranslateH (Generic CoreBind) b -> TranslateH CoreBind b - allT t = nonRecT (extractT t) (\ _ -> id) - <+ recT (\ _ -> extractT t) mconcat - - oneT :: TranslateH (Generic CoreBind) b -> TranslateH CoreBind b - oneT t = nonRecT (extractT t) (\ _ -> id) - <+ recT' (\ _ -> extractT t) catchesM - - allR :: RewriteH (Generic CoreBind) -> RewriteH CoreBind - allR r = nonRecR (extractR r) - <+ recAllR (\ _ -> extractR r) - - anyR :: RewriteH (Generic CoreBind) -> RewriteH CoreBind - anyR r = nonRecR (extractR r) - <+ recAnyR (\ _ -> extractR r) - - oneR :: RewriteH (Generic CoreBind) -> RewriteH CoreBind - oneR r = nonRecR (extractR r) - <+ recOneR (\ _ -> extractR r) - -- | Translate a binding group of the form: @NonRec@ 'Var' 'CoreExpr' -nonRecT :: TranslateH CoreExpr a -> (Var -> a -> b) -> TranslateH CoreBind b +nonRecT :: Monad m => Translate HermitC m CoreExpr a -> (Var -> a -> b) -> Translate HermitC m CoreBind b nonRecT t f = translate $ \ c -> \case NonRec v e -> f v <$> apply t (c @@ 0) e _ -> fail "not a non-recursive binding-group node." -- | Rewrite the 'CoreExpr' child of a binding group of the form: @NonRec@ 'Var' 'CoreExpr' -nonRecR :: RewriteH CoreExpr -> RewriteH CoreBind +nonRecR :: Monad m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreBind nonRecR r = nonRecT r NonRec -recT' :: (Int -> TranslateH CoreDef a) -> ([HermitM a] -> HermitM b) -> TranslateH CoreBind b -recT' t f = translate $ \ c -> \case +-- | Translate a binding group of the form: @Rec@ ['CoreDef'] +recT :: Monad m => (Int -> Translate HermitC m CoreDef a) -> ([a] -> b) -> Translate HermitC m CoreBind b +recT t f = translate $ \ c -> \case Rec bds -> -- Notice how we add the scoping bindings here *before* descending into each individual definition. let c' = addBinding (Rec bds) c - in f [ apply (t n) (c' @@ n) (Def v e) -- here we convert from (Id,CoreExpr) to CoreDef - | ((v,e),n) <- zip bds [0..] - ] + in f <$> sequence [ apply (t n) (c' @@ n) (Def v e) -- here we convert from (Id,CoreExpr) to CoreDef + | ((v,e),n) <- zip bds [0..] + ] _ -> fail "not a recursive binding-group node." --- | Translate a binding group of the form: @Rec@ ['CoreDef'] -recT :: (Int -> TranslateH CoreDef a) -> ([a] -> b) -> TranslateH CoreBind b -recT ts f = recT' ts (fmap f . sequence) - -- | Rewrite all children of a binding group of the form: @Rec@ ['CoreDef'] -recAllR :: (Int -> RewriteH CoreDef) -> RewriteH CoreBind +recAllR :: Monad m => (Int -> Rewrite HermitC m CoreDef) -> Rewrite HermitC m CoreBind recAllR rs = recT rs defsToRecBind -- | Rewrite any children of a binding group of the form: @Rec@ ['CoreDef'] -recAnyR :: (Int -> RewriteH CoreDef) -> RewriteH CoreBind -recAnyR rs = recT' (attemptR . rs) (attemptAnyN defsToRecBind) +recAnyR :: MonadCatch m => (Int -> Rewrite HermitC m CoreDef) -> Rewrite HermitC m CoreBind +recAnyR rs = unwrapAnyR $ recAllR (wrapAnyR . rs) -- | Rewrite one child of a binding group of the form: @Rec@ ['CoreDef'] -recOneR :: (Int -> RewriteH CoreDef) -> RewriteH CoreBind -recOneR rs = recT' (withArgumentT . rs) (attemptOneN defsToRecBind) +recOneR :: MonadCatch m => (Int -> Rewrite HermitC m CoreDef) -> Rewrite HermitC m CoreBind +recOneR rs = unwrapOneR $ recAllR (wrapOneR . rs) --------------------------------------------------------------------- -instance Injection CoreDef Core where - - inject :: CoreDef -> Core - inject = DefCore - - retract :: Core -> Maybe CoreDef - retract (DefCore def) = Just def - retract _ = Nothing - -instance Node CoreDef where - type Generic CoreDef = Core - - numChildren :: CoreDef -> Int - numChildren _ = 1 - -instance Walker HermitC HermitM CoreDef where - - childL :: Int -> LensH CoreDef (Generic CoreDef) - childL 0 = lens $ defT exposeT (childL1of2 Def) - childL n = failT (missingChild n) - -- | Translate a recursive definition of the form: @Def@ 'Id' 'CoreExpr' -defT :: TranslateH CoreExpr a -> (Id -> a -> b) -> TranslateH CoreDef b +defT :: Monad m => Translate HermitC m CoreExpr a -> (Id -> a -> b) -> Translate HermitC m CoreDef b defT t f = translate $ \ c (Def v e) -> f v <$> apply t (c @@ 0) e -- | Rewrite the 'CoreExpr' child of a recursive definition of the form: @Def@ 'Id' 'CoreExpr' -defR :: RewriteH CoreExpr -> RewriteH CoreDef +defR :: Monad m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreDef defR r = defT r Def --------------------------------------------------------------------- -instance Injection CoreAlt Core where - - inject :: CoreAlt -> Core - inject = AltCore - - retract :: Core -> Maybe CoreAlt - retract (AltCore expr) = Just expr - retract _ = Nothing - -instance Node CoreAlt where - type Generic CoreAlt = Core - - numChildren :: CoreAlt -> Int - numChildren _ = 1 - -instance Walker HermitC HermitM CoreAlt where - - childL :: Int -> LensH CoreAlt (Generic CoreAlt) - childL 0 = lens $ altT exposeT (childL2of3 (,,)) - childL n = failT (missingChild n) - -- | Translate a case alternative of the form: ('AltCon', ['Id'], 'CoreExpr') -altT :: TranslateH CoreExpr a -> (AltCon -> [Id] -> a -> b) -> TranslateH CoreAlt b +altT :: Monad m => Translate HermitC m CoreExpr a -> (AltCon -> [Id] -> a -> b) -> Translate HermitC m CoreAlt b altT t f = translate $ \ c (con,bs,e) -> f con bs <$> apply t (addAltBindings bs c @@ 0) e -- | Rewrite the 'CoreExpr' child of a case alternative of the form: ('AltCon', 'Id', 'CoreExpr') -altR :: RewriteH CoreExpr -> RewriteH CoreAlt +altR :: Monad m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreAlt altR r = altT r (,,) --------------------------------------------------------------------- -instance Injection CoreExpr Core where - - inject :: CoreExpr -> Core - inject = ExprCore - - retract :: Core -> Maybe CoreExpr - retract (ExprCore expr) = Just expr - retract _ = Nothing - -instance Node CoreExpr where - type Generic CoreExpr = Core - - numChildren :: CoreExpr -> Int - numChildren (Var _) = 0 - numChildren (Lit _) = 0 - numChildren (App _ _) = 2 - numChildren (Lam _ _) = 1 - numChildren (Let _ _) = 2 - numChildren (Case _ _ _ es) = 1 + length es - numChildren (Cast _ _) = 1 - numChildren (Tick _ _) = 1 - numChildren (Type _) = 0 - numChildren (Coercion _) = 0 - -instance Walker HermitC HermitM CoreExpr where - - childL :: Int -> LensH CoreExpr (Generic CoreExpr) - childL n = lens $ setFailMsg (missingChild n) $ - case n of - 0 -> appT exposeT idR (childL0of2 App) - <+ lamT exposeT (childL1of2 Lam) - <+ letT exposeT idR (childL0of2 Let) - <+ caseT exposeT (const idR) (childL0of4 Case) - <+ castT exposeT (childL0of2 Cast) - <+ tickT exposeT (childL1of2 Tick) - - 1 -> appT idR exposeT (childL1of2 App) - <+ letT idR exposeT (childL1of2 Let) - <+ caseChooseL - - _ -> caseChooseL - where - -- Note we use index (n-1) because 0 refers to the expression being scrutinised. - caseChooseL = whenM (hasChildT n) $ - caseT idR (const exposeT) (\ e v t -> childLMofN (n-1) (Case e v t)) - - allT :: Monoid b => TranslateH (Generic CoreExpr) b -> TranslateH CoreExpr b - allT t = varT (\ _ -> mempty) - <+ litT (\ _ -> mempty) - <+ appT (extractT t) (extractT t) mappend - <+ lamT (extractT t) (\ _ -> id) - <+ letT (extractT t) (extractT t) mappend - <+ caseT (extractT t) (\ _ -> extractT t) (\ r _ _ rs -> mconcat (r:rs)) - <+ castT (extractT t) const - <+ tickT (extractT t) (\ _ -> id) - <+ typeT (\ _ -> mempty) - <+ coercionT (\ _ -> mempty) - - oneT :: TranslateH (Generic CoreExpr) b -> TranslateH CoreExpr b - oneT t = appT' (extractT t) (extractT t) (<<+) - <+ lamT (extractT t) (\ _ -> id) - <+ letT' (extractT t) (extractT t) (<<+) - <+ caseT' (extractT t) (\ _ -> extractT t) (\ _ _ r rs -> catchesM (r:rs)) - <+ castT (extractT t) const - <+ tickT (extractT t) (\ _ -> id) - - allR :: RewriteH (Generic CoreExpr) -> RewriteH CoreExpr - allR r = varT Var - <+ litT Lit - <+ appAllR (extractR r) (extractR r) - <+ lamR (extractR r) - <+ letAllR (extractR r) (extractR r) - <+ caseAllR (extractR r) (\ _ -> extractR r) - <+ castR (extractR r) - <+ tickR (extractR r) - <+ typeT Type - <+ coercionT Coercion - - anyR :: RewriteH (Generic CoreExpr) -> RewriteH CoreExpr - anyR r = appAnyR (extractR r) (extractR r) - <+ lamR (extractR r) - <+ letAnyR (extractR r) (extractR r) - <+ caseAnyR (extractR r) (\ _ -> extractR r) - <+ castR (extractR r) - <+ tickR (extractR r) - <+ fail "anyR failed" - - oneR :: RewriteH (Generic CoreExpr) -> RewriteH CoreExpr - oneR r = appOneR (extractR r) (extractR r) - <+ lamR (extractR r) - <+ letOneR (extractR r) (extractR r) - <+ caseOneR (extractR r) (\ _ -> extractR r) - <+ castR (extractR r) - <+ tickR (extractR r) - <+ fail "oneR failed" - ---------------------------------------------------------------------- - -- | Translate an expression of the form: @Var@ 'Var' -varT :: (Var -> b) -> TranslateH CoreExpr b +varT :: Monad m => (Var -> b) -> Translate HermitC m CoreExpr b varT f = contextfreeT $ \case - Var v -> pure (f v) + Var v -> return (f v) _ -> fail "not a variable node." -- | Translate an expression of the form: @Lit@ 'Literal' -litT :: (Literal -> b) -> TranslateH CoreExpr b +litT :: Monad m => (Literal -> b) -> Translate HermitC m CoreExpr b litT f = contextfreeT $ \case - Lit x -> pure (f x) + Lit x -> return (f x) _ -> fail "not a literal node." -appT' :: TranslateH CoreExpr a1 -> TranslateH CoreExpr a2 -> (HermitM a1 -> HermitM a2 -> HermitM b) -> TranslateH CoreExpr b -appT' t1 t2 f = translate $ \ c -> \case - App e1 e2 -> f (apply t1 (c @@ 0) e1) (apply t2 (c @@ 1) e2) - _ -> fail "not an application node." - -- | Translate an expression of the form: @App@ 'CoreExpr' 'CoreExpr' -appT :: TranslateH CoreExpr a1 -> TranslateH CoreExpr a2 -> (a1 -> a2 -> b) -> TranslateH CoreExpr b -appT t1 t2 = appT' t1 t2 . liftA2 +appT :: Monad m => Translate HermitC m CoreExpr a1 -> Translate HermitC m CoreExpr a2 -> (a1 -> a2 -> b) -> Translate HermitC m CoreExpr b +appT t1 t2 f = translate $ \ c -> \case + App e1 e2 -> f <$> apply t1 (c @@ 0) e1 <*> apply t2 (c @@ 1) e2 + _ -> fail "not an application node." -- | Rewrite all children of an expression of the form: @App@ 'CoreExpr' 'CoreExpr' -appAllR :: RewriteH CoreExpr -> RewriteH CoreExpr -> RewriteH CoreExpr +appAllR :: Monad m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr appAllR r1 r2 = appT r1 r2 App -- | Rewrite any children of an expression of the form: @App@ 'CoreExpr' 'CoreExpr' -appAnyR :: RewriteH CoreExpr -> RewriteH CoreExpr -> RewriteH CoreExpr -appAnyR r1 r2 = appT' (attemptR r1) (attemptR r2) (attemptAny2 App) +appAnyR :: MonadCatch m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr +appAnyR r1 r2 = unwrapAnyR $ appAllR (wrapAnyR r1) (wrapAnyR r2) -- | Rewrite one child of an expression of the form: @App@ 'CoreExpr' 'CoreExpr' -appOneR :: RewriteH CoreExpr -> RewriteH CoreExpr -> RewriteH CoreExpr -appOneR r1 r2 = appT' (withArgumentT r1) (withArgumentT r2) (attemptOne2 App) +appOneR :: MonadCatch m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr +appOneR r1 r2 = unwrapOneR $ appAllR (wrapOneR r1) (wrapOneR r2) + -- | Translate an expression of the form: @Lam@ 'Var' 'CoreExpr' -lamT :: TranslateH CoreExpr a -> (Var -> a -> b) -> TranslateH CoreExpr b +lamT :: Monad m => Translate HermitC m CoreExpr a -> (Var -> a -> b) -> Translate HermitC m CoreExpr b lamT t f = translate $ \ c -> \case - Lam b e -> f b <$> apply t (addLambdaBinding b c @@ 0) e + Lam v e -> f v <$> apply t (addLambdaBinding v c @@ 0) e _ -> fail "not a lambda node." -- | Rewrite the 'CoreExpr' child of an expression of the form: @Lam@ 'Var' 'CoreExpr' -lamR :: RewriteH CoreExpr -> RewriteH CoreExpr +lamR :: Monad m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr lamR r = lamT r Lam -letT' :: TranslateH CoreBind a1 -> TranslateH CoreExpr a2 -> (HermitM a1 -> HermitM a2 -> HermitM b) -> TranslateH CoreExpr b -letT' t1 t2 f = translate $ \ c -> \case - Let bds e -> f (apply t1 (c @@ 0) bds) (apply t2 (addBinding bds c @@ 1) e) - -- use *original* env, because the bindings are self-binding, - -- if they are recursive. See recT'. - _ -> fail "not a let node." - -- | Translate an expression of the form: @Let@ 'CoreBind' 'CoreExpr' -letT :: TranslateH CoreBind a1 -> TranslateH CoreExpr a2 -> (a1 -> a2 -> b) -> TranslateH CoreExpr b -letT t1 t2 = letT' t1 t2 . liftA2 +letT :: Monad m => Translate HermitC m CoreBind a1 -> Translate HermitC m CoreExpr a2 -> (a1 -> a2 -> b) -> Translate HermitC m CoreExpr b +letT t1 t2 f = translate $ \ c -> \case + Let bds e -> -- Note we use the *original* context for the binding group. + -- If the bindings are recursive, they will be added to the context by recT. + f <$> apply t1 (c @@ 0) bds <*> apply t2 (addBinding bds c @@ 1) e + _ -> fail "not a let node." -- | Rewrite all children of an expression of the form: @Let@ 'CoreBind' 'CoreExpr' -letAllR :: RewriteH CoreBind -> RewriteH CoreExpr -> RewriteH CoreExpr +letAllR :: Monad m => Rewrite HermitC m CoreBind -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr letAllR r1 r2 = letT r1 r2 Let -- | Rewrite any children of an expression of the form: @Let@ 'CoreBind' 'CoreExpr' -letAnyR :: RewriteH CoreBind -> RewriteH CoreExpr -> RewriteH CoreExpr -letAnyR r1 r2 = letT' (attemptR r1) (attemptR r2) (attemptAny2 Let) +letAnyR :: MonadCatch m => Rewrite HermitC m CoreBind -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr +letAnyR r1 r2 = unwrapAnyR $ letAnyR (wrapAnyR r1) (wrapAnyR r2) -- | Rewrite one child of an expression of the form: @Let@ 'CoreBind' 'CoreExpr' -letOneR :: RewriteH CoreBind -> RewriteH CoreExpr -> RewriteH CoreExpr -letOneR r1 r2 = letT' (withArgumentT r1) (withArgumentT r2) (attemptOne2 Let) +letOneR :: MonadCatch m => Rewrite HermitC m CoreBind -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr +letOneR r1 r2 = unwrapOneR $ letOneR (wrapOneR r1) (wrapOneR r2) -caseT' :: TranslateH CoreExpr a1 -> (Int -> TranslateH CoreAlt a2) -> (Id -> Type -> HermitM a1 -> [HermitM a2] -> HermitM b) -> TranslateH CoreExpr b -caseT' t ts f = translate $ \ c -> \case - Case e b ty alts -> f b ty (apply t (c @@ 0) e) $ [ apply (ts n) (addCaseBinding (b,e,alt) c @@ (n+1)) alt - | (alt,n) <- zip alts [0..] - ] - _ -> fail "not a case node." - -- | Translate an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' ['CoreAlt'] -caseT :: TranslateH CoreExpr a1 -> (Int -> TranslateH CoreAlt a2) -> (a1 -> Id -> Type -> [a2] -> b) -> TranslateH CoreExpr b -caseT t ts f = caseT' t ts (\ b ty me malts -> f <$> me <*> pure b <*> pure ty <*> sequence malts) +caseT :: Monad m => Translate HermitC m CoreExpr a1 -> (Int -> Translate HermitC m CoreAlt a2) -> (a1 -> Id -> Type -> [a2] -> b) -> Translate HermitC m CoreExpr b +caseT t ts f = translate $ \ c -> \case + Case e x ty alts -> f <$> apply t (c @@ 0) e + <*> return x + <*> return ty + <*> sequence [ apply (ts n) (addCaseBinding (x,e,alt) c @@ (n+1)) alt + | (alt,n) <- zip alts [0..] + ] + _ -> fail "not a case node." -- | Rewrite all children of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' ['CoreAlt'] -caseAllR :: RewriteH CoreExpr -> (Int -> RewriteH CoreAlt) -> RewriteH CoreExpr +caseAllR :: Monad m => Rewrite HermitC m CoreExpr -> (Int -> Rewrite HermitC m CoreAlt) -> Rewrite HermitC m CoreExpr caseAllR r rs = caseT r rs Case -- | Rewrite any children of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' ['CoreAlt'] -caseAnyR :: RewriteH CoreExpr -> (Int -> RewriteH CoreAlt) -> RewriteH CoreExpr -caseAnyR r rs = caseT' (attemptR r) (attemptR . rs) (\ b ty -> attemptAny1N (\ e -> Case e b ty)) +caseAnyR :: MonadCatch m => Rewrite HermitC m CoreExpr -> (Int -> Rewrite HermitC m CoreAlt) -> Rewrite HermitC m CoreExpr +caseAnyR r rs = unwrapAnyR $ caseAllR (wrapAnyR r) (wrapAnyR . rs) -- | Rewrite one child of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' ['CoreAlt'] -caseOneR :: RewriteH CoreExpr -> (Int -> RewriteH CoreAlt) -> RewriteH CoreExpr -caseOneR r rs = caseT' (withArgumentT r) (withArgumentT . rs) (\ b ty -> attemptOne1N (\ e -> Case e b ty)) +caseOneR :: MonadCatch m => Rewrite HermitC m CoreExpr -> (Int -> Rewrite HermitC m CoreAlt) -> Rewrite HermitC m CoreExpr +caseOneR r rs = unwrapOneR $ caseAllR (wrapOneR r) (wrapOneR . rs) + -- | Translate an expression of the form: @Cast@ 'CoreExpr' 'Coercion' -castT :: TranslateH CoreExpr a -> (a -> Coercion -> b) -> TranslateH CoreExpr b +castT :: Monad m => Translate HermitC m CoreExpr a -> (a -> Coercion -> b) -> Translate HermitC m CoreExpr b castT t f = translate $ \ c -> \case - Cast e cast -> f <$> apply t (c @@ 0) e <*> pure cast + Cast e cast -> f <$> apply t (c @@ 0) e <*> return cast _ -> fail "not a cast node." -- | Rewrite the 'CoreExpr' child of an expression of the form: @Cast@ 'CoreExpr' 'Coercion' -castR :: RewriteH CoreExpr -> RewriteH CoreExpr +castR :: Monad m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr castR r = castT r Cast -- | Translate an expression of the form: @Tick@ 'CoreTickish' 'CoreExpr' -tickT :: TranslateH CoreExpr a -> (CoreTickish -> a -> b) -> TranslateH CoreExpr b +tickT :: Monad m => Translate HermitC m CoreExpr a -> (CoreTickish -> a -> b) -> Translate HermitC m CoreExpr b tickT t f = translate $ \ c -> \case Tick tk e -> f tk <$> apply t (c @@ 0) e _ -> fail "not a tick node." -- | Rewrite the 'CoreExpr' child of an expression of the form: @Tick@ 'CoreTickish' 'CoreExpr' -tickR :: RewriteH CoreExpr -> RewriteH CoreExpr +tickR :: Monad m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr tickR r = tickT r Tick -- | Translate an expression of the form: @Type@ 'Type' -typeT :: (Type -> b) -> TranslateH CoreExpr b +typeT :: Monad m => (Type -> b) -> Translate HermitC m CoreExpr b typeT f = contextfreeT $ \case - Type t -> pure (f t) + Type t -> return (f t) _ -> fail "not a type node." -- | Translate an expression of the form: @Coercion@ 'Coercion' -coercionT :: (Coercion -> b) -> TranslateH CoreExpr b +coercionT :: Monad m => (Coercion -> b) -> Translate HermitC m CoreExpr b coercionT f = contextfreeT $ \case - Coercion co -> pure (f co) + Coercion co -> return (f co) _ -> fail "not a coercion node." --------------------------------------------------------------------- @@ -626,190 +417,190 @@ -- Some composite congruence combinators to export. -- | Translate a binding group of the form: @Rec@ [('Id', 'CoreExpr')] -recDefT :: (Int -> TranslateH CoreExpr a1) -> ([(Id,a1)] -> b) -> TranslateH CoreBind b +recDefT :: Monad m => (Int -> Translate HermitC m CoreExpr a1) -> ([(Id,a1)] -> b) -> Translate HermitC m CoreBind b recDefT ts = recT (\ n -> defT (ts n) (,)) -- | Rewrite all children of a binding group of the form: @Rec@ [('Id', 'CoreExpr')] -recDefAllR :: (Int -> RewriteH CoreExpr) -> RewriteH CoreBind +recDefAllR :: Monad m => (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreBind recDefAllR rs = recAllR (\ n -> defR (rs n)) -- | Rewrite any children of a binding group of the form: @Rec@ [('Id', 'CoreExpr')] -recDefAnyR :: (Int -> RewriteH CoreExpr) -> RewriteH CoreBind +recDefAnyR :: MonadCatch m => (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreBind recDefAnyR rs = recAnyR (\ n -> defR (rs n)) -- | Rewrite one child of a binding group of the form: @Rec@ [('Id', 'CoreExpr')] -recDefOneR :: (Int -> RewriteH CoreExpr) -> RewriteH CoreBind +recDefOneR :: MonadCatch m => (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreBind recDefOneR rs = recOneR (\ n -> defR (rs n)) -- | Translate a program of the form: (@NonRec@ 'Var' 'CoreExpr') @:@ 'CoreProg' -consNonRecT :: TranslateH CoreExpr a1 -> TranslateH CoreProg a2 -> (Var -> a1 -> a2 -> b) -> TranslateH CoreProg b +consNonRecT :: Monad m => Translate HermitC m CoreExpr a1 -> Translate HermitC m CoreProg a2 -> (Var -> a1 -> a2 -> b) -> Translate HermitC m CoreProg b consNonRecT t1 t2 f = progConsT (nonRecT t1 (,)) t2 (uncurry f) -- | Rewrite all children of an expression of the form: (@NonRec@ 'Var' 'CoreExpr') @:@ 'CoreProg' -consNonRecAllR :: RewriteH CoreExpr -> RewriteH CoreProg -> RewriteH CoreProg +consNonRecAllR :: Monad m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg consNonRecAllR r1 r2 = progConsAllR (nonRecR r1) r2 -- | Rewrite any children of an expression of the form: (@NonRec@ 'Var' 'CoreExpr') @:@ 'CoreProg' -consNonRecAnyR :: RewriteH CoreExpr -> RewriteH CoreProg -> RewriteH CoreProg +consNonRecAnyR :: MonadCatch m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg consNonRecAnyR r1 r2 = progConsAnyR (nonRecR r1) r2 -- | Rewrite one child of an expression of the form: (@NonRec@ 'Var' 'CoreExpr') @:@ 'CoreProg' -consNonRecOneR :: RewriteH CoreExpr -> RewriteH CoreProg -> RewriteH CoreProg +consNonRecOneR :: MonadCatch m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg consNonRecOneR r1 r2 = progConsOneR (nonRecR r1) r2 -- | Translate an expression of the form: (@Rec@ ['CoreDef']) @:@ 'CoreProg' -consRecT :: (Int -> TranslateH CoreDef a1) -> TranslateH CoreProg a2 -> ([a1] -> a2 -> b) -> TranslateH CoreProg b +consRecT :: Monad m => (Int -> Translate HermitC m CoreDef a1) -> Translate HermitC m CoreProg a2 -> ([a1] -> a2 -> b) -> Translate HermitC m CoreProg b consRecT ts t = progConsT (recT ts id) t -- | Rewrite all children of an expression of the form: (@Rec@ ['CoreDef']) @:@ 'CoreProg' -consRecAllR :: (Int -> RewriteH CoreDef) -> RewriteH CoreProg -> RewriteH CoreProg +consRecAllR :: Monad m => (Int -> Rewrite HermitC m CoreDef) -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg consRecAllR rs r = progConsAllR (recAllR rs) r -- | Rewrite any children of an expression of the form: (@Rec@ ['CoreDef']) @:@ 'CoreProg' -consRecAnyR :: (Int -> RewriteH CoreDef) -> RewriteH CoreProg -> RewriteH CoreProg +consRecAnyR :: MonadCatch m => (Int -> Rewrite HermitC m CoreDef) -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg consRecAnyR rs r = progConsAnyR (recAnyR rs) r -- | Rewrite one child of an expression of the form: (@Rec@ ['CoreDef']) @:@ 'CoreProg' -consRecOneR :: (Int -> RewriteH CoreDef) -> RewriteH CoreProg -> RewriteH CoreProg +consRecOneR :: MonadCatch m => (Int -> Rewrite HermitC m CoreDef) -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg consRecOneR rs r = progConsOneR (recOneR rs) r -- | Translate an expression of the form: (@Rec@ [('Id', 'CoreExpr')]) @:@ 'CoreProg' -consRecDefT :: (Int -> TranslateH CoreExpr a1) -> TranslateH CoreProg a2 -> ([(Id,a1)] -> a2 -> b) -> TranslateH CoreProg b +consRecDefT :: Monad m => (Int -> Translate HermitC m CoreExpr a1) -> Translate HermitC m CoreProg a2 -> ([(Id,a1)] -> a2 -> b) -> Translate HermitC m CoreProg b consRecDefT ts t = consRecT (\ n -> defT (ts n) (,)) t -- | Rewrite all children of an expression of the form: (@Rec@ [('Id', 'CoreExpr')]) @:@ 'CoreProg' -consRecDefAllR :: (Int -> RewriteH CoreExpr) -> RewriteH CoreProg -> RewriteH CoreProg +consRecDefAllR :: Monad m => (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg consRecDefAllR rs r = consRecAllR (\ n -> defR (rs n)) r -- | Rewrite any children of an expression of the form: (@Rec@ [('Id', 'CoreExpr')]) @:@ 'CoreProg' -consRecDefAnyR :: (Int -> RewriteH CoreExpr) -> RewriteH CoreProg -> RewriteH CoreProg +consRecDefAnyR :: MonadCatch m => (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg consRecDefAnyR rs r = consRecAnyR (\ n -> defR (rs n)) r -- | Rewrite one child of an expression of the form: (@Rec@ [('Id', 'CoreExpr')]) @:@ 'CoreProg' -consRecDefOneR :: (Int -> RewriteH CoreExpr) -> RewriteH CoreProg -> RewriteH CoreProg +consRecDefOneR :: MonadCatch m => (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreProg -> Rewrite HermitC m CoreProg consRecDefOneR rs r = consRecOneR (\ n -> defR (rs n)) r -- | Translate an expression of the form: @Let@ (@NonRec@ 'Var' 'CoreExpr') 'CoreExpr' -letNonRecT :: TranslateH CoreExpr a1 -> TranslateH CoreExpr a2 -> (Var -> a1 -> a2 -> b) -> TranslateH CoreExpr b +letNonRecT :: Monad m => Translate HermitC m CoreExpr a1 -> Translate HermitC m CoreExpr a2 -> (Var -> a1 -> a2 -> b) -> Translate HermitC m CoreExpr b letNonRecT t1 t2 f = letT (nonRecT t1 (,)) t2 (uncurry f) -- | Rewrite all children of an expression of the form: @Let@ (@NonRec@ 'Var' 'CoreExpr') 'CoreExpr' -letNonRecAllR :: RewriteH CoreExpr -> RewriteH CoreExpr -> RewriteH CoreExpr +letNonRecAllR :: Monad m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr letNonRecAllR r1 r2 = letAllR (nonRecR r1) r2 -- | Rewrite any children of an expression of the form: @Let@ (@NonRec@ 'Var' 'CoreExpr') 'CoreExpr' -letNonRecAnyR :: RewriteH CoreExpr -> RewriteH CoreExpr -> RewriteH CoreExpr +letNonRecAnyR :: MonadCatch m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr letNonRecAnyR r1 r2 = letAnyR (nonRecR r1) r2 -- | Rewrite one child of an expression of the form: @Let@ (@NonRec@ 'Var' 'CoreExpr') 'CoreExpr' -letNonRecOneR :: RewriteH CoreExpr -> RewriteH CoreExpr -> RewriteH CoreExpr +letNonRecOneR :: MonadCatch m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr letNonRecOneR r1 r2 = letOneR (nonRecR r1) r2 -- | Translate an expression of the form: @Let@ (@Rec@ ['CoreDef']) 'CoreExpr' -letRecT :: (Int -> TranslateH CoreDef a1) -> TranslateH CoreExpr a2 -> ([a1] -> a2 -> b) -> TranslateH CoreExpr b +letRecT :: Monad m => (Int -> Translate HermitC m CoreDef a1) -> Translate HermitC m CoreExpr a2 -> ([a1] -> a2 -> b) -> Translate HermitC m CoreExpr b letRecT ts t = letT (recT ts id) t -- | Rewrite all children of an expression of the form: @Let@ (@Rec@ ['CoreDef']) 'CoreExpr' -letRecAllR :: (Int -> RewriteH CoreDef) -> RewriteH CoreExpr -> RewriteH CoreExpr +letRecAllR :: Monad m => (Int -> Rewrite HermitC m CoreDef) -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr letRecAllR rs r = letAllR (recAllR rs) r -- | Rewrite any children of an expression of the form: @Let@ (@Rec@ ['CoreDef']) 'CoreExpr' -letRecAnyR :: (Int -> RewriteH CoreDef) -> RewriteH CoreExpr -> RewriteH CoreExpr +letRecAnyR :: MonadCatch m => (Int -> Rewrite HermitC m CoreDef) -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr letRecAnyR rs r = letAnyR (recAnyR rs) r -- | Rewrite one child of an expression of the form: @Let@ (@Rec@ ['CoreDef']) 'CoreExpr' -letRecOneR :: (Int -> RewriteH CoreDef) -> RewriteH CoreExpr -> RewriteH CoreExpr +letRecOneR :: MonadCatch m => (Int -> Rewrite HermitC m CoreDef) -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr letRecOneR rs r = letOneR (recOneR rs) r -- | Translate an expression of the form: @Let@ (@Rec@ [('Id', 'CoreExpr')]) 'CoreExpr' -letRecDefT :: (Int -> TranslateH CoreExpr a1) -> TranslateH CoreExpr a2 -> ([(Id,a1)] -> a2 -> b) -> TranslateH CoreExpr b +letRecDefT :: Monad m => (Int -> Translate HermitC m CoreExpr a1) -> Translate HermitC m CoreExpr a2 -> ([(Id,a1)] -> a2 -> b) -> Translate HermitC m CoreExpr b letRecDefT ts t = letRecT (\ n -> defT (ts n) (,)) t -- | Rewrite all children of an expression of the form: @Let@ (@Rec@ [('Id', 'CoreExpr')]) 'CoreExpr' -letRecDefAllR :: (Int -> RewriteH CoreExpr) -> RewriteH CoreExpr -> RewriteH CoreExpr +letRecDefAllR :: Monad m => (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr letRecDefAllR rs r = letRecAllR (\ n -> defR (rs n)) r -- | Rewrite any children of an expression of the form: @Let@ (@Rec@ [('Id', 'CoreExpr')]) 'CoreExpr' -letRecDefAnyR :: (Int -> RewriteH CoreExpr) -> RewriteH CoreExpr -> RewriteH CoreExpr +letRecDefAnyR :: MonadCatch m => (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr letRecDefAnyR rs r = letRecAnyR (\ n -> defR (rs n)) r -- | Rewrite one child of an expression of the form: @Let@ (@Rec@ [('Id', 'CoreExpr')]) 'CoreExpr' -letRecDefOneR :: (Int -> RewriteH CoreExpr) -> RewriteH CoreExpr -> RewriteH CoreExpr +letRecDefOneR :: MonadCatch m => (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreExpr -> Rewrite HermitC m CoreExpr letRecDefOneR rs r = letRecOneR (\ n -> defR (rs n)) r -- | Translate an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' [('AltCon', ['Id'], 'CoreExpr')] -caseAltT :: TranslateH CoreExpr a1 -> (Int -> TranslateH CoreExpr a2) -> (a1 -> Id -> Type -> [(AltCon,[Id],a2)] -> b) -> TranslateH CoreExpr b +caseAltT :: Monad m => Translate HermitC m CoreExpr a1 -> (Int -> Translate HermitC m CoreExpr a2) -> (a1 -> Id -> Type -> [(AltCon,[Id],a2)] -> b) -> Translate HermitC m CoreExpr b caseAltT t ts = caseT t (\ n -> altT (ts n) (,,)) -- | Rewrite all children of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' [('AltCon', ['Id'], 'CoreExpr')] -caseAltAllR :: RewriteH CoreExpr -> (Int -> RewriteH CoreExpr) -> RewriteH CoreExpr +caseAltAllR :: Monad m => Rewrite HermitC m CoreExpr -> (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreExpr caseAltAllR t ts = caseAllR t (\ n -> altR (ts n)) -- | Rewrite any children of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' [('AltCon', ['Id'], 'CoreExpr')] -caseAltAnyR :: RewriteH CoreExpr -> (Int -> RewriteH CoreExpr) -> RewriteH CoreExpr +caseAltAnyR :: MonadCatch m => Rewrite HermitC m CoreExpr -> (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreExpr caseAltAnyR t ts = caseAnyR t (\ n -> altR (ts n)) -- | Rewrite one child of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' [('AltCon', ['Id'], 'CoreExpr')] -caseAltOneR :: RewriteH CoreExpr -> (Int -> RewriteH CoreExpr) -> RewriteH CoreExpr +caseAltOneR :: MonadCatch m => Rewrite HermitC m CoreExpr -> (Int -> Rewrite HermitC m CoreExpr) -> Rewrite HermitC m CoreExpr caseAltOneR t ts = caseOneR t (\ n -> altR (ts n)) --------------------------------------------------------------------- -- | Promote a rewrite on 'ModGuts' to a rewrite on 'Core'. -promoteModGutsR :: RewriteH ModGuts -> RewriteH Core +promoteModGutsR :: Monad m => Rewrite HermitC m ModGuts -> Rewrite HermitC m Core promoteModGutsR = promoteWithFailMsgR "This rewrite can only succeed at the module level." -- | Promote a rewrite on 'CoreProg' to a rewrite on 'Core'. -promoteProgR :: RewriteH CoreProg -> RewriteH Core +promoteProgR :: Monad m => Rewrite HermitC m CoreProg -> Rewrite HermitC m Core promoteProgR = promoteWithFailMsgR "This rewrite can only succeed at program nodes (the top-level)." -- | Promote a rewrite on 'CoreBind' to a rewrite on 'Core'. -promoteBindR :: RewriteH CoreBind -> RewriteH Core +promoteBindR :: Monad m => Rewrite HermitC m CoreBind -> Rewrite HermitC m Core promoteBindR = promoteWithFailMsgR "This rewrite can only succeed at binding group nodes." -- | Promote a rewrite on 'CoreDef' to a rewrite on 'Core'. -promoteDefR :: RewriteH CoreDef -> RewriteH Core +promoteDefR :: Monad m => Rewrite HermitC m CoreDef -> Rewrite HermitC m Core promoteDefR = promoteWithFailMsgR "This rewrite can only succeed at recursive definition nodes." -- | Promote a rewrite on 'CoreAlt' to a rewrite on 'Core'. -promoteAltR :: RewriteH CoreAlt -> RewriteH Core +promoteAltR :: Monad m => Rewrite HermitC m CoreAlt -> Rewrite HermitC m Core promoteAltR = promoteWithFailMsgR "This rewrite can only succeed at case alternative nodes." -- | Promote a rewrite on 'CoreExpr' to a rewrite on 'Core'. -promoteExprR :: RewriteH CoreExpr -> RewriteH Core +promoteExprR :: Monad m => Rewrite HermitC m CoreExpr -> Rewrite HermitC m Core promoteExprR = promoteWithFailMsgR "This rewrite can only succeed at expression nodes." --------------------------------------------------------------------- -- | Promote a translate on 'ModGuts' to a translate on 'Core'. -promoteModGutsT :: TranslateH ModGuts b -> TranslateH Core b +promoteModGutsT :: Monad m => Translate HermitC m ModGuts b -> Translate HermitC m Core b promoteModGutsT = promoteWithFailMsgT "This translate can only succeed at the module level." -- | Promote a translate on 'CoreProg' to a translate on 'Core'. -promoteProgT :: TranslateH CoreProg b -> TranslateH Core b +promoteProgT :: Monad m => Translate HermitC m CoreProg b -> Translate HermitC m Core b promoteProgT = promoteWithFailMsgT "This translate can only succeed at program nodes (the top-level)." -- | Promote a translate on 'CoreBind' to a translate on 'Core'. -promoteBindT :: TranslateH CoreBind b -> TranslateH Core b +promoteBindT :: Monad m => Translate HermitC m CoreBind b -> Translate HermitC m Core b promoteBindT = promoteWithFailMsgT "This translate can only succeed at binding group nodes." -- | Promote a translate on 'CoreDef' to a translate on 'Core'. -promoteDefT :: TranslateH CoreDef b -> TranslateH Core b +promoteDefT :: Monad m => Translate HermitC m CoreDef b -> Translate HermitC m Core b promoteDefT = promoteWithFailMsgT "This translate can only succeed at recursive definition nodes." -- | Promote a translate on 'CoreAlt' to a translate on 'Core'. -promoteAltT :: TranslateH CoreAlt b -> TranslateH Core b +promoteAltT :: Monad m => Translate HermitC m CoreAlt b -> Translate HermitC m Core b promoteAltT = promoteWithFailMsgT "This translate can only succeed at case alternative nodes." -- | Promote a translate on 'CoreExpr' to a translate on 'Core'. -promoteExprT :: TranslateH CoreExpr b -> TranslateH Core b +promoteExprT :: Monad m => Translate HermitC m CoreExpr b -> Translate HermitC m Core b promoteExprT = promoteWithFailMsgT "This translate can only succeed at expression nodes." --------------------------------------------------------------------- diff --git a/src/Language/HERMIT/Monad.hs b/src/Language/HERMIT/Monad.hs --- a/src/Language/HERMIT/Monad.hs +++ b/src/Language/HERMIT/Monad.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TupleSections, GADTs, KindSignatures, InstanceSigs #-} +{-# LANGUAGE InstanceSigs #-} module Language.HERMIT.Monad ( @@ -34,8 +34,7 @@ import Control.Monad import Control.Arrow -import Language.KURE.Combinators -import Language.KURE.Utilities +import Language.KURE import Language.HERMIT.Core import Language.HERMIT.Context @@ -66,9 +65,8 @@ putStash s = HermitM (\ _ _ -> return $ return (s, ())) sendDebugMessage :: DebugMessage -> HermitM () -sendDebugMessage msg = - do env <- HermitM $ \ ch s -> return $ return (s, ch) - hs_debugChan env msg +sendDebugMessage msg = do env <- HermitM $ \ ch s -> return $ return (s, ch) + hs_debugChan env msg -- | Save a definition for future use. saveDef :: Label -> CoreDef -> HermitM () @@ -174,9 +172,8 @@ ---------------------------------------------------------------------------- -- | A message packet. -data DebugMessage :: * where - DebugTick :: String -> DebugMessage - DebugCore :: String -> HermitC -> Core -> DebugMessage -- A postcard +data DebugMessage = DebugTick String + | DebugCore String HermitC Core -- ^ A postcard. mkHermitMEnv :: (DebugMessage -> HermitM ()) -> HermitMEnv mkHermitMEnv debugger = HermitMEnv diff --git a/src/Language/HERMIT/PrettyPrinter/Clean.hs b/src/Language/HERMIT/PrettyPrinter/Clean.hs --- a/src/Language/HERMIT/PrettyPrinter/Clean.hs +++ b/src/Language/HERMIT/PrettyPrinter/Clean.hs @@ -1,6 +1,7 @@ -- | Output the raw Expr constructors. Helpful for writing pattern matching rewrites. module Language.HERMIT.PrettyPrinter.Clean where +import Control.Monad (ap) import Control.Arrow hiding ((<+>)) import Data.Char (isSpace) @@ -119,7 +120,7 @@ ppModGuts :: PrettyH GHC.ModGuts ppModGuts = arr $ \ m -> hang (keyword "module" <+> ppSDoc (GHC.mg_module m) <+> keyword "where") 2 - (vcat [ (optional (ppBinder v) (\b -> b <+> specialSymbol TypeOfSymbol <+> ppCoreType True (GHC.idType v))) + (vcat [ (optional (ppBinder v) (\b -> b <+> specialSymbol TypeOfSymbol <+> normalExpr (ppCoreType True (GHC.idType v)))) | bnd <- GHC.mg_binds m , v <- case bnd of GHC.NonRec f _ -> [f] @@ -141,10 +142,7 @@ appendBind (Just v) xs = v : xs ppCoreExprR :: TranslateH GHC.CoreExpr RetExpr - ppCoreExprR = do - ret <- ppCoreExprPR - absPath <- absPathT - return $ ret (rootPath absPath) + ppCoreExprR = ppCoreExprPR `ap` rootPathT ppCoreExprPR :: TranslateH GHC.CoreExpr (Path -> RetExpr) ppCoreExprPR = lamT ppCoreExprR (\ v e _ -> case e of @@ -166,7 +164,7 @@ <+ (acceptR (\ e -> case e of GHC.App (GHC.Type _) (GHC.Lam {}) | po_exprTypes opts == Omit -> True GHC.App (GHC.App (GHC.Var _) (GHC.Type _)) (GHC.Lam {}) | po_exprTypes opts == Omit -> True - _ -> False) "TODO: add decent error message here" >>> + _ -> False) >>> (appT ppCoreExprR ppCoreExprR (\ (RetAtom e1) (RetLam vs e0) _ -> RetExpr $ hang (e1 <+> symbol '(' <> @@ -186,24 +184,27 @@ <+ varT (\ i p -> RetAtom (attrP p $ ppVar i)) <+ litT (\ i p -> RetAtom (attrP p $ ppSDoc i)) <+ typeT (\ t p -> case po_exprTypes opts of - Show -> RetAtom (attrP p $ ppCoreType False t) + Show -> case ppCoreType False t of + RetAtom d -> RetAtom $ attrP p d + RetExpr d -> RetExpr $ attrP p d + _ -> error "not possible!" Abstract -> RetAtom (attrP p $ typeSymbol) Omit -> RetEmpty) <+ (ppCoreExpr0 >>^ \ e p -> RetExpr (attrP p e)) - ppCoreType :: Bool -> GHC.Type -> DocH - ppCoreType isTySig = normalExpr . go + ppCoreType :: Bool -> GHC.Type -> RetExpr + ppCoreType isTySig = go where go (TyVarTy v) = RetAtom $ ppVar' isTySig v go (LitTy tylit) = RetAtom $ ppLitTy isTySig tylit - go (AppTy t1 t2) = RetExpr $ ppCoreType isTySig t1 <+> ppCoreType isTySig t2 + go (AppTy t1 t2) = RetExpr $ normalExpr (go t1) <+> normalExpr (go t2) go (TyConApp tyCon tys) | GHC.isFunTyCon tyCon, [ty1,ty2] <- tys = go (FunTy ty1 ty2) - | GHC.isTupleTyCon tyCon = case map (ppCoreType isTySig) tys of + | GHC.isTupleTyCon tyCon = case map (normalExpr . go) tys of [] -> RetAtom $ tyText "()" - ds -> RetExpr $ tyText "(" <> (foldr1 (\d r -> d <> tyText "," <+> r) ds) <> tyText ")" - | otherwise = RetAtom $ ppName' isTySig (GHC.getName tyCon) <+> sep (map (ppCoreType isTySig) tys) -- has spaces, but we never want parens - go (FunTy ty1 ty2) = RetExpr $ atomExpr (go ty1) <+> text "->" <+> ppCoreType isTySig ty2 - go (ForAllTy v ty) = RetExpr $ specialSymbol ForallSymbol <+> ppVar' isTySig v <+> symbol '.' <+> ppCoreType isTySig ty + ds -> RetAtom $ tyText "(" <> (foldr1 (\d r -> d <> tyText "," <+> r) ds) <> tyText ")" + | otherwise = RetAtom $ ppName' isTySig (GHC.getName tyCon) <+> sep (map (normalExpr . go) tys) -- has spaces, but we never want parens + go (FunTy ty1 ty2) = RetExpr $ atomExpr (go ty1) <+> tyText "->" <+> normalExpr (go ty2) + go (ForAllTy v ty) = RetExpr $ specialSymbol ForallSymbol <+> ppVar' isTySig v <+> symbol '.' <+> normalExpr (go ty) tyText = if isTySig then text else markColor TypeColor . text diff --git a/src/Language/HERMIT/Primitive/AlphaConversion.hs b/src/Language/HERMIT/Primitive/AlphaConversion.hs --- a/src/Language/HERMIT/Primitive/AlphaConversion.hs +++ b/src/Language/HERMIT/Primitive/AlphaConversion.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeFamilies, FlexibleContexts #-} +{-# LANGUAGE FlexibleContexts #-} module Language.HERMIT.Primitive.AlphaConversion ( -- * Alpha-Renaming and Shadowing externals @@ -125,7 +125,7 @@ -- | Lifted version of 'shadowedBy'. -- Additionally, it fails if no shadows are found. shadowedByT :: TranslateH a [Var] -> TranslateH a [Var] -> TranslateH a [Var] -shadowedByT t1 t2 = (shadowedBy <$> t1 <*> t2) >>> acceptR (not . null) "No shadowing detected." +shadowedByT t1 t2 = setFailMsg "No shadows detected." $ (shadowedBy <$> t1 <*> t2) >>> acceptR (not . null) -- | Rename local variables with manifestly unique names (x, x0, x1, ...). -- Does not rename top-level definitions (though this may change in the future). @@ -145,7 +145,7 @@ -- | Replace all occurrences of a specified variable. -- Arguments are the variable to replace and the replacement variable, respectively. -replaceVarR :: (Injection a Core, Generic a ~ Core) => Var -> Var -> RewriteH a +replaceVarR :: (Injection a Core) => Var -> Var -> RewriteH a replaceVarR v v' = extractR $ tryR $ substR v (Var v') -- | Given a variable to replace, and a replacement, produce a 'Var' @->@ 'Var' function that diff --git a/src/Language/HERMIT/Primitive/Debug.hs b/src/Language/HERMIT/Primitive/Debug.hs --- a/src/Language/HERMIT/Primitive/Debug.hs +++ b/src/Language/HERMIT/Primitive/Debug.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE FlexibleContexts, TypeFamilies #-} +{-# LANGUAGE FlexibleContexts #-} module Language.HERMIT.Primitive.Debug ( -- * Debugging Primitives externals @@ -25,11 +25,11 @@ ] -- | If the 'Rewrite' fails, print out the 'Core', with a message. -observeFailureR :: (Injection a Core, Generic a ~ Core) => String -> RewriteH a -> RewriteH a +observeFailureR :: Injection a Core => String -> RewriteH a -> RewriteH a observeFailureR str m = m <+ observeR str -- | Print out the 'Core', with a message. -observeR :: (Injection a Core, Generic a ~ Core) => String -> RewriteH a +observeR :: Injection a Core => String -> RewriteH a observeR msg = extractR $ sideEffectR $ \ cxt core -> sendDebugMessage $ DebugCore msg cxt core diff --git a/src/Language/HERMIT/Primitive/Fold.hs b/src/Language/HERMIT/Primitive/Fold.hs --- a/src/Language/HERMIT/Primitive/Fold.hs +++ b/src/Language/HERMIT/Primitive/Fold.hs @@ -76,7 +76,7 @@ fold :: Id -> CoreExpr -> CoreExpr -> Maybe CoreExpr fold i lam exp = do - let (vs,body) = foldArgs lam + let (vs,body) = collectBinders lam -- return Nothing if not equal, so sequence will fail below checkEqual :: Maybe CoreExpr -> Maybe CoreExpr -> Maybe CoreExpr checkEqual m1 m2 = ifM (exprEqual <$> m1 <*> m2) m1 Nothing @@ -88,12 +88,6 @@ es <- sequence [ join (Map.lookup v m) | v <- vs ] return $ mkCoreApps (Var i) es --- | Collect arguments to function we are folding, so we can unify with them. -foldArgs :: CoreExpr -> ([Var], CoreExpr) -foldArgs = go [] - where go vs (Lam v e) = go (v:vs) e - go vs e = (reverse vs, e) - -- Note: Id in the concrete instance is first -- (not the Id found in the definition we are trying to fold). addAlpha :: Id -> Id -> [(Id,Id)] -> [(Id,Id)] @@ -145,6 +139,10 @@ y <- zipWithM altMatch alts alts' return (x ++ concat y) foldMatch vs as (Cast e c) (Cast e' c') | coreEqCoercion c c' = foldMatch vs as e e' +-- don't try to alpha type variables for now +foldMatch vs _ (Type t@(TyVarTy v)) e@(Type t') | v `elem` vs = return [(v,e)] + | eqType t t' = return [] + | otherwise = Nothing foldMatch _ _ (Type t) (Type t') | eqType t t' = return [] foldMatch _ _ (Coercion c) (Coercion c') | coreEqCoercion c c' = return [] foldMatch _ _ _ _ = Nothing diff --git a/src/Language/HERMIT/Primitive/GHC.hs b/src/Language/HERMIT/Primitive/GHC.hs --- a/src/Language/HERMIT/Primitive/GHC.hs +++ b/src/Language/HERMIT/Primitive/GHC.hs @@ -175,7 +175,7 @@ info :: TranslateH Core String info = translate $ \ c core -> do dynFlags <- getDynFlags - let pa = "Path: " ++ show (contextPath c) + let pa = "Path: " ++ show (absPath c) node = "Node: " ++ coreNode core con = "Constructor: " ++ coreConstructor core bds = "Bindings in Scope: " ++ show (map unqualifiedVarName $ boundVars c) @@ -197,34 +197,34 @@ -- showIdInfo dynFlags v = showSDoc dynFlags $ ppIdInfo v $ idInfo v coreNode :: Core -> String -coreNode (ModGutsCore _) = "Module" -coreNode (ProgCore _) = "Program" -coreNode (BindCore _) = "Binding Group" -coreNode (DefCore _) = "Recursive Definition" -coreNode (ExprCore _) = "Expression" -coreNode (AltCore _) = "Case Alternative" +coreNode (GutsCore _) = "Module" +coreNode (ProgCore _) = "Program" +coreNode (BindCore _) = "Binding Group" +coreNode (DefCore _) = "Recursive Definition" +coreNode (ExprCore _) = "Expression" +coreNode (AltCore _) = "Case Alternative" coreConstructor :: Core -> String -coreConstructor (ModGutsCore _) = "ModGuts" -coreConstructor (ProgCore prog) = case prog of - ProgNil -> "ProgNil" - ProgCons _ _ -> "ProgCons" -coreConstructor (BindCore bnd) = case bnd of - Rec _ -> "Rec" - NonRec _ _ -> "NonRec" -coreConstructor (DefCore _) = "Def" -coreConstructor (AltCore _) = "(,,)" -coreConstructor (ExprCore expr) = case expr of - Var _ -> "Var" - Type _ -> "Type" - Lit _ -> "Lit" - App _ _ -> "App" - Lam _ _ -> "Lam" - Let _ _ -> "Let" - Case _ _ _ _ -> "Case" - Cast _ _ -> "Cast" - Tick _ _ -> "Tick" - Coercion _ -> "Coercion" +coreConstructor (GutsCore _) = "ModGuts" +coreConstructor (ProgCore prog) = case prog of + ProgNil -> "ProgNil" + ProgCons _ _ -> "ProgCons" +coreConstructor (BindCore bnd) = case bnd of + Rec _ -> "Rec" + NonRec _ _ -> "NonRec" +coreConstructor (DefCore _) = "Def" +coreConstructor (AltCore _) = "(,,)" +coreConstructor (ExprCore expr) = case expr of + Var _ -> "Var" + Type _ -> "Type" + Lit _ -> "Lit" + App _ _ -> "App" + Lam _ _ -> "Lam" + Let _ _ -> "Let" + Case _ _ _ _ -> "Case" + Cast _ _ -> "Cast" + Tick _ _ -> "Tick" + Coercion _ -> "Coercion" ------------------------------------------------------------------------ diff --git a/src/Language/HERMIT/Primitive/Inline.hs b/src/Language/HERMIT/Primitive/Inline.hs --- a/src/Language/HERMIT/Primitive/Inline.hs +++ b/src/Language/HERMIT/Primitive/Inline.hs @@ -77,7 +77,8 @@ withPatFailMsg (wrongExprForm "Var v") $ do (c, Var v) <- exposeT (e,d) <- getUnfolding scrutinee caseBinderOnly v c - return e >>> accepterR (extractT $ ensureDepth d) "values in inlined expression have been rebound." + return e >>> (setFailMsg "values in inlined expression have been rebound." $ + accepterR (extractT $ ensureDepth d)) -- | Ensure all the free variables in an expression were bound above a given depth. diff --git a/src/Language/HERMIT/Primitive/Local/Let.hs b/src/Language/HERMIT/Primitive/Local/Let.hs --- a/src/Language/HERMIT/Primitive/Local/Let.hs +++ b/src/Language/HERMIT/Primitive/Local/Let.hs @@ -1,8 +1,8 @@ module Language.HERMIT.Primitive.Local.Let ( -- * Rewrites on Let Expressions - letExternals + letElim + , letExternals , letIntro - , letElim , letFloatApp , letFloatArg , letFloatLet @@ -10,7 +10,11 @@ , letFloatCase , letFloatExpr , letFloatLetTop + , letNonRecElim + , letRecElim , letToCase + , letUnfloatApp + , letUnfloatCase ) where @@ -68,6 +72,13 @@ [ "let v = ev in e ==> case ev of v -> e" ] .+ Commute .+ Shallow .+ PreCondition -- , external "let-to-case-unbox" (promoteR $ not_defined "let-to-case-unbox" :: RewriteH Core) -- [ "let v = ev in e ==> case ev of C v1..vn -> let v = C v1..vn in e" ] .+ Unimplemented + , external "let-unfloat" (promoteExprR (letUnfloatApp <+ letUnfloatCase) >+> anybuR (promoteExprR letElim) :: RewriteH Core) + [ "Unfloat a let if possible." ] .+ Commute .+ Shallow + , external "let-unfloat-app" ((promoteExprR letUnfloatApp >+> anybuR (promoteExprR letElim)) :: RewriteH Core) + [ "let v = ev in f a ==> (let v = ev in f) (let v = ev in a)" ] .+ Commute .+ Shallow + , external "let-unfloat-case" ((promoteExprR letUnfloatCase >+> anybuR (promoteExprR letElim)) :: RewriteH Core) + [ "let v = ev in case s of p -> e ==> case (let v = ev in s) of p -> let v = ev in e" + , "if v does not shadow a pattern binder in p" ] .+ Commute .+ Shallow ] ------------------------------------------------------------------------------------------- @@ -79,15 +90,35 @@ v <- newIdH (show nm) (exprTypeOrKind e) return $ Let (NonRec v e) (Var v) --- | Remove an unused let binding. --- (let v = E1 in E2) => E2, if v is not free in E2 letElim :: RewriteH CoreExpr -letElim = prefixFailMsg "Dead-let-elimination failed: " $ +letElim = letNonRecElim <+ letRecElim + +-- | Remove an unused non-recursive let binding. +-- (let v = E1 in E2) => E2, if v is not free in E2 +letNonRecElim :: RewriteH CoreExpr +letNonRecElim = prefixFailMsg "Dead-let-elimination failed: " $ withPatFailMsg (wrongExprForm "Let (NonRec v e1) e2") $ do Let (NonRec v _) e <- idR guardMsg (v `notElem` coreExprFreeVars e) "let-bound variable appears in the expression." return e +-- TODO: find the GHC way to do this, as this implementation will be defeated by mutual recursion +-- | Remove all unused recursive let bindings in the current group. +letRecElim :: RewriteH CoreExpr +letRecElim = prefixFailMsg "Dead-let-elimination failed: " $ do + Let (Rec bnds) body <- idR + (vsAndFrees, bodyFrees) <- letT (recT (\_ -> defT freeVarsT (,)) id) freeVarsT (,) + -- binder is alive if it is found free anywhere but its own rhs + let living = [ v + | (v,_) <- vsAndFrees + , v `elem` bodyFrees || v `elem` (concat [ fs | (v',fs) <- vsAndFrees, v' /= v ]) + ] + if null living + then return body + else if length living == length bnds + then fail "no dead code." + else return $ Let (Rec [ (v,rhs) | (v,rhs) <- bnds, v `elem` living ]) body + -- | let v = ev in e ==> case ev of v -> e letToCase :: RewriteH CoreExpr letToCase = prefixFailMsg "Converting Let to Case failed: " $ @@ -158,3 +189,15 @@ return (NonRec w ew `ProgCons` NonRec v ev `ProgCons` p) ------------------------------------------------------------------------------------------- + +letUnfloatCase :: RewriteH CoreExpr +letUnfloatCase = prefixFailMsg "Let unfloating from case failed: " $ do + Let bnds (Case s w ty alts) <- idR + captured <- letT bindVarsT caseVarsT intersect + guardMsg (null captured) "let bindings would capture case pattern bindings." + return $ Case (Let bnds s) w ty [ (ac, vs, Let bnds e) | (ac, vs, e) <- alts ] + +letUnfloatApp :: RewriteH CoreExpr +letUnfloatApp = prefixFailMsg "Let unfloating from app failed: " $ do + Let bnds (App e1 e2) <- idR + return $ App (Let bnds e1) (Let bnds e2) diff --git a/src/Language/HERMIT/Primitive/New.hs b/src/Language/HERMIT/Primitive/New.hs --- a/src/Language/HERMIT/Primitive/New.hs +++ b/src/Language/HERMIT/Primitive/New.hs @@ -6,8 +6,9 @@ import Control.Applicative import Control.Arrow -import Data.List(intersect) +import Data.List(intersect,transpose) +import Language.HERMIT.Context import Language.HERMIT.Core import Language.HERMIT.Monad import Language.HERMIT.Kure @@ -48,6 +49,8 @@ [ "any-call (.. unfold command ..) applies an unfold commands to all applications" , "preference is given to applications with more arguments" ] .+ Deep + , external "static-arg" (promoteDefR staticArg :: RewriteH Core) + [ "perform the static argument transformation on a recursive function" ] ] ------------------------------------------------------------------------------------------------------ @@ -95,6 +98,62 @@ -- Others -- let v = E1 in E2 E3 <=> (let v = E1 in E2) E3 -- let v = E1 in E2 E3 <=> E2 (let v = E1 in E3) + +staticArg :: RewriteH CoreDef +staticArg = prefixFailMsg "static-arg failed: " $ do + Def f rhs <- idR + let (bnds, body) = collectBinders rhs + guardMsg (notNull bnds) "rhs is not a function" + c <- contextT + constT $ do + let bodyContext = foldl (flip addLambdaBinding) c bnds + + callPats <- apply (callsT (var2THName f) (collectArgsT >>> arr snd)) bodyContext (ExprCore body) + let argExprs = transpose callPats + numCalls = length callPats + -- ensure argument is present in every call (partial applications boo) + (ps,dbnds) = unzip [ (i,b) | (i,b,exprs) <- zip3 [0..] bnds $ argExprs ++ repeat [] + , length exprs /= numCalls || isDynamic b exprs + ] + + isDynamic _ [] = False -- all were static, so static + isDynamic b ((Var b'):es) | b == b' = isDynamic b es + isDynamic b ((Type (TyVarTy v)):es) | b == v = isDynamic b es + isDynamic _ _ = True -- not a simple repass, so dynamic + + wkr <- newIdH (var2String f ++ "'") (exprType (mkCoreLams dbnds body)) + + let replaceCall :: RewriteH CoreExpr + replaceCall = do + (_,exprs) <- collectArgsT + return $ mkApps (Var wkr) [ e | (p,e) <- zip [0..] exprs, (p::Int) `elem` ps ] + + ExprCore body' <- apply (callsR (var2THName f) replaceCall) bodyContext (ExprCore body) + + return $ Def f $ mkCoreLams bnds $ Let (Rec [(wkr, mkCoreLams dbnds body')]) + $ mkApps (Var wkr) (varsToCoreExprs dbnds) + +-- | Like GHC's collectArgs, but fails if not an application +collectArgsT :: TranslateH CoreExpr (CoreExpr, [CoreExpr]) +collectArgsT = do + App {} <- idR + arr collectArgs + +-- | Succeeds if we are looking at an application of given function +callG :: TH.Name -> TranslateH CoreExpr () +callG nm = prefixFailMsg "callG failed: " $ do + (Var i,_) <- collectArgsT + guardMsg (cmpTHName2Var nm i) $ "not a call to " ++ show nm + return () + +-- | Apply a rewrite to all applications of a given function in a top-down manner, pruning on success. +callsR :: TH.Name -> RewriteH CoreExpr -> RewriteH Core +callsR nm rr = prunetdR (promoteExprR $ callG nm >> rr) + +-- | Apply a translate to all applications of a given function in a top-down manner, +-- pruning on success, collecting the results. +callsT :: TH.Name -> TranslateH CoreExpr b -> TranslateH Core [b] +callsT nm t = collectPruneT (promoteExprT $ callG nm >> t) ------------------------------------------------------------------------------------------------------ diff --git a/src/Language/HERMIT/Primitive/Unfold.hs b/src/Language/HERMIT/Primitive/Unfold.hs --- a/src/Language/HERMIT/Primitive/Unfold.hs +++ b/src/Language/HERMIT/Primitive/Unfold.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE ScopedTypeVariables, TypeFamilies, FlexibleContexts, TupleSections #-} +{-# LANGUAGE TupleSections #-} module Language.HERMIT.Primitive.Unfold ( externals , stashDef diff --git a/src/Language/HERMIT/Shell/Command.hs b/src/Language/HERMIT/Shell/Command.hs --- a/src/Language/HERMIT/Shell/Command.hs +++ b/src/Language/HERMIT/Shell/Command.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE FlexibleInstances, ScopedTypeVariables, GADTs, KindSignatures, TypeFamilies, DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances, ScopedTypeVariables, GADTs, TypeFamilies, DeriveDataTypeable #-} module Language.HERMIT.Shell.Command ( -- * The HERMIT Command-line Shell @@ -35,8 +35,6 @@ import Language.HERMIT.Primitive.Navigation import Language.HERMIT.Primitive.Inline - --- import Language.HERMIT.Primitive.GHC import System.Console.ANSI import System.IO