ho-rewriting 0.1 → 0.2

raw patch · 8 files changed

+199/−77 lines, 8 filesdep ~basedep ~compdataPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, compdata

API changes (from Hackage documentation)

Files

• README.md +1/−1
• examples/Feldspar.hs +17/−14
• examples/Simple.hs +12/−15
• ho-rewriting.cabal +8/−7
• src/Data/Rewriting/FirstOrder.hs +5/−7
• src/Data/Rewriting/HigherOrder.hs +84/−24
• src/Data/Rewriting/Rules.hs +2/−9
• tests/Capture.hs +70/−0

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

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

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

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

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

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

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

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