diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -2,5 +2,5 @@ Some examples are found in the [examples directory](examples). For more information, see "Lightweight Higher-Order Rewriting in Haskell": - * [Paper](http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_DRAFT.pdf) + * [Paper](http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight.pdf) * [Slides](http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_slides.pdf) diff --git a/examples/Feldspar.hs b/examples/Feldspar.hs --- a/examples/Feldspar.hs +++ b/examples/Feldspar.hs @@ -12,19 +12,22 @@ {-# OPTIONS_GHC -fno-warn-missing-methods #-} +module Feldspar where + + + import Data.Comp import Data.Comp.Derive import Data.Comp.Render import Data.Rewriting.Rules +import Data.Rewriting.FirstOrder hiding (applyFirst) import Data.Rewriting.HigherOrder import Simple -main = return () -- For `cabal test` - data FORLOOP a = ForLoop a a a deriving (Eq, Show, Functor, Foldable, Traversable) @@ -64,15 +67,15 @@ forLoop len init body = forLoop_ len init (lam $ \i -> lam $ \s -> body i s) -- forLoop 0 init _ ===> init -rule_for1 init = forLoop 0 (mvar init) (\i s -> __) ===> mvar init +rule_for1 init = forLoop 0 (meta init) (\i s -> __) ===> meta init -- forLoop 0 init (\i s -> s) ===> init -rule_for2 init = forLoop __ (mvar init) (\i s -> var s) ===> mvar init +rule_for2 init = forLoop __ (meta init) (\i s -> var s) ===> meta init rule_for3 len init body = - forLoop (mvar len) (mvar init) (\i s -> body -$- i) + forLoop (meta len) (meta init) (\i s -> body -$- i) ===> - cond (mvar len === 0) (mvar init) (body -$- (mvar len - 1)) + cond (meta len === 0) (meta init) (body -$- (meta len - 1)) rulesFeld = rules ++ [ quantify rule_for1 @@ -80,38 +83,38 @@ , quantify rule_for3 ] -stripAnn :: Functor f => Term (f :&: a) -> Term f -stripAnn = cata (\(f :&: _) -> Term f) +simplify :: Data a -> Data a +simplify = Data . rewriteWith (bottomUp (applyFirst app rulesFeld)) . unData forExample :: Data Int -> Data Int forExample a - = forLoop (a-a) a (\i s -> i*s+70) + = forLoop a a (\i s -> (i-i)+s) + forLoop a a (\i s -> i*i+100) drawForExample = drawTerm $ unData $ lam forExample -drawForExampleR = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData $ lam forExample +drawForExampleR = drawTerm $ unData $ simplify $ lam forExample feld1 :: Data Int -> Data Int feld1 a = a + a + 3 drawFeld1 = drawTerm $ unData $ lam feld1 -drawFeld1R = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData $ lam feld1 +drawFeld1R = drawTerm $ unData $ simplify $ lam feld1 feld2 :: Data Int feld2 = forLoop 0 0 (+) drawFeld2 = drawTerm $ unData feld2 -drawFeld2R = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData feld2 +drawFeld2R = drawTerm $ unData $ simplify feld2 feld3 :: Data Int -> Data Int feld3 a = forLoop a 0 (\i s -> a+i) drawFeld3 = drawTerm $ unData $ lam feld3 -drawFeld3R = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData $ lam feld3 +drawFeld3R = drawTerm $ unData $ simplify $ lam feld3 feld4 :: Data Int -> Data Int feld4 a = forLoop a 0 (\i s -> a + i + s) + forLoop a 0 (\i s -> a + i + s) drawFeld4 = drawTerm $ unData $ lam feld4 -drawFeld4R = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData $ lam feld4 +drawFeld4R = drawTerm $ unData $ simplify $ lam feld4 diff --git a/examples/Simple.hs b/examples/Simple.hs --- a/examples/Simple.hs +++ b/examples/Simple.hs @@ -21,6 +21,7 @@ import Data.Comp.Derive import Data.Comp.Render import Data.Patch + -- Could use partial type signatures instead (on GHC >= 7.10) import Data.Rewriting.Rules import Data.Rewriting.FirstOrder @@ -30,17 +31,13 @@ -- Using the `Num` class as a tagless DSL: -- 0 + x ===> x -rule_add1 x = 0 + mvar x ===> mvar x - -rule_add1 - :: (Num (lhs a), MetaVar lhs, MetaVar rhs, MetaRep lhs ~ MetaRep rhs) - => MetaRep rhs a -> Rule lhs rhs +rule_add1 x = 0 + meta x ===> meta x -- x + x ===> x*2 -rule_add2 x = mvar x + mvar x ===> mvar x * 2 +rule_add2 x = meta x + meta x ===> meta x * 2 -- x - x ===> 0 -rule_sub x = mvar x - mvar x ===> 0 +rule_sub x = meta x - meta x ===> 0 -- 0 * x ===> 0 rule_mul = 0 * __ ===> (0 -:: tCon tInteger) @@ -58,19 +55,19 @@ cond :: r Bool -> r a -> r a -> r a -- not (not x) ===> x -rule_not x = noT (noT (mvar x)) ===> mvar x +rule_not x = noT (noT (meta x)) ===> meta x -- false <&> x ===> false -rule_and x = false <&> mvar x ===> false +rule_and x = false <&> meta x ===> false -- x === x ===> true -rule_eq x = mvar x === mvar x ===> true +rule_eq x = meta x === meta x ===> true -- cond _ tf tf ===> tf -rule_cond1 tf = cond __ (mvar tf) (mvar tf) ===> mvar tf +rule_cond1 tf = cond __ (meta tf) (meta tf) ===> meta tf -- cond (not c) t f ===> cond c f t -rule_cond2 c t f = cond (noT (mvar c)) (mvar t) (mvar f) ===> cond (mvar c) (mvar f) (mvar t) +rule_cond2 c t f = cond (noT (meta c)) (meta t) (meta f) ===> cond (meta c) (meta f) (meta t) data NUM a = Num Integer @@ -142,17 +139,17 @@ expr1 = 0 + 4 draw1 = drawTerm $ unExpr expr1 -draw1R = drawTerm $ bottomUp rules (unExpr expr1) +draw1R = drawTerm $ bottomUp (applyFirst rules) (unExpr expr1) expr2 :: Expr Integer expr2 = (5 + 5 + 3) + (0 + 4) draw2 = drawTerm $ unExpr expr2 -draw2R = drawTerm $ bottomUp rules (unExpr expr2) +draw2R = drawTerm $ bottomUp (applyFirst rules) (unExpr expr2) expr3 :: Expr Integer expr3 = cond (0 === 1) (5+5) (5*2) draw3 = drawTerm $ unExpr expr3 -draw3R = drawTerm $ bottomUp rules (unExpr expr3) +draw3R = drawTerm $ bottomUp (applyFirst rules) (unExpr expr3) diff --git a/ho-rewriting.cabal b/ho-rewriting.cabal --- a/ho-rewriting.cabal +++ b/ho-rewriting.cabal @@ -1,5 +1,5 @@ name: ho-rewriting -version: 0.1 +version: 0.2 synopsis: Generic rewrite rules with safe treatment of variables and binders description: This package gives a generic implementation of higher-order rewriting. The main idea is to use techniques from embedded @@ -8,9 +8,9 @@ . Some examples are found in the @examples@ directory. For more information, see - "Lightweight Higher-Order Rewriting in Haskell" (presented at TFP 2015): + \"Lightweight Higher-Order Rewriting in Haskell\" (presented at TFP 2015): . - * Paper: + * Paper: . * Slides: homepage: https://github.com/emilaxelsson/ho-rewriting @@ -44,7 +44,7 @@ build-depends: base >=4.7 && <5, containers, - compdata >=0.9, + compdata ==0.10.*, mtl, patch-combinators @@ -69,12 +69,12 @@ default-language: Haskell2010 -test-suite examples +test-suite capture type: exitcode-stdio-1.0 - hs-source-dirs: examples + hs-source-dirs: examples, tests - main-is: Feldspar.hs + main-is: Capture.hs build-depends: base, @@ -83,3 +83,4 @@ patch-combinators default-language: Haskell2010 + diff --git a/src/Data/Rewriting/FirstOrder.hs b/src/Data/Rewriting/FirstOrder.hs --- a/src/Data/Rewriting/FirstOrder.hs +++ b/src/Data/Rewriting/FirstOrder.hs @@ -7,10 +7,8 @@ import Control.Monad.Reader import Control.Monad.Writer -import Data.Foldable (Foldable) import Data.Function (on) import Data.List (groupBy) -import Data.Traversable (Traversable) import Data.Comp import Data.Comp.Ops @@ -74,19 +72,19 @@ -- -- This function assumes that there are no applications of meta-variables in `LHS` or `RHS`. applyFirst :: (Traversable f, EqF f) => [Rule (LHS f) (RHS f)] -> Term f -> Term f -applyFirst rs t = case [t' | r <- rs, Just t' <- [rewrite r t]] of +applyFirst rs t = case [t' | rule <- rs, Just t' <- [rewrite rule t]] of t':_ -> t' _ -> t -- | Apply a list of rules bottom-up across a term -- -- This function assumes that there are no applications of meta-variables in `LHS` or `RHS`. -bottomUp :: (Traversable f, EqF f) => [Rule (LHS f) (RHS f)] -> Term f -> Term f -bottomUp rs = applyFirst rs . Term . fmap (bottomUp rs) . unTerm +bottomUp :: Functor f => (Term f -> Term f) -> Term f -> Term f +bottomUp rew = rew . Term . fmap (bottomUp rew) . unTerm -- | Apply a list of rules top-down across a term -- -- This function assumes that there are no applications of meta-variables in `LHS` or `RHS`. -topDown :: (Traversable f, EqF f) => [Rule (LHS f) (RHS f)] -> Term f -> Term f -topDown rs = Term . fmap (topDown rs) . unTerm . applyFirst rs +topDown :: Functor f => (Term f -> Term f) -> Term f -> Term f +topDown rew = Term . fmap (topDown rew) . unTerm . rew diff --git a/src/Data/Rewriting/HigherOrder.hs b/src/Data/Rewriting/HigherOrder.hs --- a/src/Data/Rewriting/HigherOrder.hs +++ b/src/Data/Rewriting/HigherOrder.hs @@ -225,15 +225,46 @@ | Just (Var v) <- proj f = Term (inj (Var v) :&: Set.singleton v) annFreeVars f | Just (Lam v a) <- proj f - , vars <- getAnn a - = Term (inj (Lam v a) :&: Set.delete v vars) + = Term (inj (Lam v a) :&: Set.delete v (getAnn a)) annFreeVars f = Term (f :&: Foldable.foldMap getAnn f) --- | Capture-avoiding substitution. Succeeds iff. each meta-variable in 'RHS' has a mapping in the --- substitution. +-- | Environment for aliases +type Aliases = (Map Name Name, Name) + -- Invariant: The second component of the pair is a name that is greater than + -- all names in the co-domain of the map. + +-- | Set up an initial alias environment from a set of reserved names +initAliases :: Set Name -> Aliases +initAliases ns = (mp,next) + where + mp = Map.fromList [(n,n) | n <- Set.toList ns] + next = Set.findMax (Set.insert (-1) ns) + 1 + +-- | Rename to a fresh name +rename :: Name -> Aliases -> (Name,Aliases) +rename n (mp,next) = case Map.lookup n mp of + Nothing -> (n, (Map.insert n n mp, max next (n+1))) + Just _ -> (next, (Map.insert n next mp, next + 1)) + +-- | Naive renaming. Use instead of 'rename' to get naive substitution. +renameNaive :: Name -> Aliases -> (Name,Aliases) +renameNaive n (mp,next) = (n, (Map.insert n n mp, max next (n+1))) + +-- | Lookup a name in an alias environment +lookAlias :: Name -> Aliases -> Maybe Name +lookAlias n (mp,_) = Map.lookup n mp + +-- | Capture-avoiding substitution. Succeeds iff. each meta-variable in 'RHS' +-- has a mapping in the substitution. +-- +-- Uses the "rapier" method described in "Secrets of the Glasgow Haskell +-- Compiler inliner" (Peyton Jones and Marlow, JFP 2006) to rename variables +-- where there's risk for capturing. substitute :: forall f g a . ( VAR :<: f , LAM :<: f + , VAR :<: PF (RHS f) + , LAM :<: PF (RHS f) , Traversable f , g ~ (f :&: Set Name) ) @@ -241,16 +272,33 @@ -> Subst g -> RHS f a -> Maybe (Term g) -substitute app subst = cataM go . unRHS +substitute app subst rhs = go (initAliases (Set.union fvS fvR)) (unRHS rhs) where - go :: PF (RHS f) (Term g) -> Maybe (Term g) - go (Inl (Meta mv)) = goo mv + -- Free variables in the co-domain of the substitution + fvS = Foldable.fold [fv | (_, Term (_ :&: fv)) <- subst] + + -- Free variables in the RHS + Term (_ :&: fvR) = cata annFreeVars $ unRHS rhs + -- It's usually strange to have free variables in the RHS since then the + -- meaning of the rule depends on the context. But we take care of that + -- situation here anyway. + + go :: Aliases -> Term (PF (RHS f)) -> Maybe (Term g) + go aliases (Term (Inl (Meta mv))) = goo mv where goo :: MetaExp (RHS f) b -> Maybe (Term g) goo (MVar (MetaId v)) = lookup v subst - goo (MApp mv t) = liftM2 app (goo mv) $ cataM go (unRHS t) - go (Inr f) = return $ annFreeVars f - -- TODO Should avoid capturing + goo (MApp mv t) = liftM2 app (goo mv) $ go aliases (unRHS t) + go aliases t + | Just (Var v) <- project t + , Just v' <- lookAlias v aliases + = Just $ Term (inj (Var v') :&: Set.singleton v') + go aliases t + | Just (Lam v body) <- project t = do + let (v',aliases') = rename v aliases + body'@(Term (_ :&: fv)) <- go aliases' body + return $ Term (inj (Lam v' body') :&: Set.delete v' fv) + go aliases (Term (Inr f)) = fmap annFreeVars $ traverse (go aliases) f -- | Apply a rule. Succeeds iff. both matching and substitution succeeds. rewrite @@ -258,13 +306,15 @@ , LAM :<: f , VAR :<: PF (LHS f) , LAM :<: PF (LHS f) + , VAR :<: PF (RHS f) + , LAM :<: PF (RHS f) , Traversable f, EqF f , g ~ (f :&: Set Name) ) => (Term g -> Term g -> Term g) -- ^ Application operator -> Rule (LHS f) (RHS f) - -> Term (f :&: Set Name) - -> Maybe (Term (f :&: Set Name)) + -> Term g + -> Maybe (Term g) rewrite app (Rule lhs rhs) t = do subst <- match lhs t substitute app subst rhs @@ -276,29 +326,39 @@ , LAM :<: f , VAR :<: PF (LHS f) , LAM :<: PF (LHS f) + , VAR :<: PF (RHS f) + , LAM :<: PF (RHS f) , Traversable f, EqF f , g ~ (f :&: Set Name) ) => (Term g -> Term g -> Term g) -- ^ Application operator -> [Rule (LHS f) (RHS f)] - -> Term (f :&: Set Name) - -> Term (f :&: Set Name) + -> Term g + -> Term g applyFirst app rs t = case [t' | r <- rs, Just t' <- [rewrite app r t]] of t':_ -> t' _ -> t --- | Apply a list of rules bottom-up across a term -bottomUp +-- | Prepare a term for rewriting by annotating each node with its set of free +-- variables +prepare :: (VAR :<: f, LAM :<: f, Functor f, Foldable f) => Term f -> Term (f :&: Set Name) +prepare = cata annFreeVars + +-- | Strip out the annotations from a term +stripAnn :: Functor f => Term (f :&: a) -> Term f +stripAnn = cata (\(f :&: _) -> Term f) + +-- | Apply a higher-order rewriter to a term +-- +-- Typically used as @`rewriteWith` (`bottomUp` (`applyFirst` ...)) :: (...) => Term f -> Term f@, +-- where @f@ is not annotated +rewriteWith :: ( VAR :<: f , LAM :<: f - , VAR :<: PF (LHS f) - , LAM :<: PF (LHS f) - , Traversable f, EqF f + , Functor f + , Foldable f , g ~ (f :&: Set Name) ) - => (Term g -> Term g -> Term g) -- ^ Application operator - -> [Rule (LHS f) (RHS f)] - -> Term f - -> Term (f :&: Set Name) -bottomUp app rs = applyFirst app rs . annFreeVars . fmap (bottomUp app rs) . unTerm + => (Term g -> Term g) -> Term f -> Term f +rewriteWith rew = stripAnn . rew . prepare diff --git a/src/Data/Rewriting/Rules.hs b/src/Data/Rewriting/Rules.hs --- a/src/Data/Rewriting/Rules.hs +++ b/src/Data/Rewriting/Rules.hs @@ -13,12 +13,7 @@ -import Control.Applicative (pure) -import qualified Data.Foldable as Fold -import Data.Traversable (Traversable (traverse)) - import Data.Comp -import Data.Comp.Derive import Data.Comp.Ops import Data.Patch @@ -58,11 +53,9 @@ type MetaArg r :: * -> * metaExp :: MetaExp r a -> r a --- TODO Move `MetaRep` and `MetaArg` out of the class as in the paper? - -- | Construct a meta-variable -mvar :: MetaVar r => MetaRep r a -> r a -mvar = metaExp . MVar +meta :: MetaVar r => MetaRep r a -> r a +meta = metaExp . MVar -- | Meta-variable application (used for all but the first and last variable) ($$) :: MetaExp r (a -> b) -> MetaArg r a -> MetaExp r b diff --git a/tests/Capture.hs b/tests/Capture.hs new file mode 100644 --- /dev/null +++ b/tests/Capture.hs @@ -0,0 +1,70 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +-- Test that rule application does not lead to capturing + +import System.Exit + +import Data.Comp +-- import Data.Comp.Render +import Data.Patch + -- Could use partial type signatures instead (on GHC >= 7.10) + +import Data.Rewriting.Rules +import Data.Rewriting.FirstOrder hiding (applyFirst) +import Data.Rewriting.HigherOrder + +import Feldspar + +lamm :: (LAM :<: PF rep, Rep rep) => Name -> rep b -> rep (a -> b) +lamm v body = toRep $ inject $ Lam v $ fromRep body + +dvar :: Name -> Data a +dvar = Data . inject . Var + +rule_strange1 aa bb = + meta aa + meta bb + ===> + forLoop 1 0 (\x y -> meta bb + var x + meta aa + var y) + +-- Strange rule with a free variable on the RHS +rule_strange2 = + __ - __ + ===> + forLoop_ 1 0 (lamm 0 $ lamm 0 $ (var 0 + (var 1 -:: tCon tInt))) + +simplify' :: Data a -> Data a +simplify' = Data . rewriteWith (bottomUp (applyFirst app rulesStrange)) . unData + where + rulesStrange = + [ quantify (rule_strange1 -:: tCon tInt >-> id) + , quantify (rule_strange2) + ] + +testFun1 :: Data (Int -> Int -> Int) +testFun1 = lam $ \v1 -> lam $ \v0 -> v1 + v0 + +testFun2 :: Data (Int -> Int -> Int) +testFun2 = lam $ \v1 -> lam $ \v0 -> v1 - v0 + +testFun1_simp_golden :: Data (Int -> Int -> Int) +testFun1_simp_golden = + lamm 1 $ lamm 0 $ forLoop_ 1 0 $ lamm 2 $ lamm 3 $ dvar 0 + dvar 2 + dvar 1 + dvar 3 + +testFun2_simp_golden :: Data (Int -> Int -> Int) +testFun2_simp_golden = + lamm 1 $ lamm 0 $ forLoop_ 1 0 $ lamm 0 $ lamm 2 $ dvar 2 + dvar 1 + +tests = + [ unData (simplify' testFun1) == unData testFun1_simp_golden + , unData (simplify' testFun2) == unData testFun2_simp_golden + ] + +main = if and tests + then putStrLn "All tests passed" + else do + putStrLn $ "Tests " ++ show [i | (i,False) <- zip [0..] tests] ++ " failed" + exitFailure + +