ho-rewriting (empty) → 0.1

raw patch · 9 files changed

+1002/−0 lines, 9 filesdep +basedep +compdatadep +containerssetup-changed

Dependencies added: base, compdata, containers, ho-rewriting, mtl, patch-combinators

Files

LICENSE +30/−0
README.md +6/−0
Setup.hs +2/−0
examples/Feldspar.hs +117/−0
examples/Simple.hs +158/−0
ho-rewriting.cabal +85/−0
src/Data/Rewriting/FirstOrder.hs +92/−0
src/Data/Rewriting/HigherOrder.hs +304/−0
src/Data/Rewriting/Rules.hs +208/−0

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2015, Emil Axelsson++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Emil Axelsson nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ README.md view

@@ -0,0 +1,6 @@+This package gives a generic implementation of higher-order rewriting. The main idea is to use techniques from embedded domain-specific languages to offer an interface which is both safe and syntactically appealing.++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)+  * [Slides](http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_slides.pdf)

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ examples/Feldspar.hs view

@@ -0,0 +1,117 @@+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-missing-methods #-}++import Data.Comp+import Data.Comp.Derive+import Data.Comp.Render++import Data.Rewriting.Rules+import Data.Rewriting.HigherOrder++import Simple++++main = return () -- For `cabal test`++data FORLOOP a = ForLoop a a a+  deriving (Eq, Show, Functor, Foldable, Traversable)++derive [makeEqF, makeShowF, makeShowConstr] [''FORLOOP]++instance Render FORLOOP++type Feld = VAR :+: LAM :+: APP :+: NUM :+: LOGIC :+: FORLOOP++newtype Data a = Data { unData :: Term Feld }+  deriving (Eq, Show)++instance Rep Data+  where+    type PF Data = Feld+    toRep   = Data+    fromRep = unData++type instance Var Data = Data++instance Bind Data+  where+    var = id+    lam = mkLam (Data . inject . Var . toInteger)++deriving instance Num a => Num (Data a)++class ForLoop r+  where+    forLoop_ :: r Int -> r s -> r (Int -> s -> s) -> r s++instance (Rep r, FORLOOP :<: PF r) => ForLoop r+  where+    forLoop_ len init step = toRep $ inject $ ForLoop (fromRep len) (fromRep init) (fromRep step)++forLoop :: (ForLoop r, Bind r) => r Int -> r s -> (Var r Int -> Var r s -> r s) -> r s+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++-- forLoop 0 init (\i s -> s)  ===>  init+rule_for2 init = forLoop __ (mvar init) (\i s -> var s)  ===>  mvar init++rule_for3 len init body =+    forLoop (mvar len) (mvar init) (\i s -> body -$- i)+      ===>+    cond (mvar len === 0) (mvar init) (body -$- (mvar len - 1))++rulesFeld = rules +++    [ quantify rule_for1+    , quantify rule_for2+    , quantify rule_for3+    ]++stripAnn :: Functor f => Term (f :&: a) -> Term f+stripAnn = cata (\(f :&: _) -> Term f)++forExample :: Data Int -> Data Int+forExample a+    = forLoop (a-a) a (\i s -> i*s+70)+    + forLoop a a (\i s -> i*i+100)++drawForExample  = drawTerm $ unData $ lam forExample+drawForExampleR = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData $ 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++feld2 :: Data Int+feld2 = forLoop 0 0 (+)++drawFeld2  = drawTerm $ unData feld2+drawFeld2R = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData 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++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+

+ examples/Simple.hs view

@@ -0,0 +1,158 @@+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-missing-methods #-}++module Simple where++++import Data.Comp+import Data.Comp.Derive+import Data.Comp.Render+import Data.Patch++import Data.Rewriting.Rules+import Data.Rewriting.FirstOrder++++-- 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++-- x + x  ===>  x*2+rule_add2 x = mvar x + mvar x  ===>  mvar x * 2++-- x - x  ===>  0+rule_sub x = mvar x - mvar x  ===>  0++-- 0 * x  ===>  0+rule_mul = 0 * __  ===>  (0 -:: tCon tInteger)+  -- Rules cannot be polymorphic++-- Adding language constructs for "logic" expressions:++class Logic r+  where+    false :: r Bool+    true  :: r Bool+    noT   :: r Bool -> r Bool+    (<&>) :: r Bool -> r Bool -> r Bool+    (===) :: Eq a => r a -> r a -> r Bool+    cond  :: r Bool -> r a -> r a -> r a++-- not (not x)  ===>  x+rule_not x = noT (noT (mvar x))  ===>  mvar x++-- false <&> x  ===>  false+rule_and x = false <&> mvar x  ===>  false++-- x === x  ===>  true+rule_eq x = mvar x === mvar x  ===>  true++-- cond _ tf tf  ===>  tf+rule_cond1 tf = cond __ (mvar tf) (mvar tf)  ===>  mvar 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)++data NUM a+    = Num Integer+    | Add a a+    | Sub a a+    | Mul a a+  deriving (Eq, Show, Functor, Foldable, Traversable)++derive [makeEqF, makeShowF, makeShowConstr] [''NUM]++instance Render NUM++data LOGIC a+    = Bool Bool+    | Not a+    | And a a+    | Equal a a+    | Cond a a a+  deriving (Eq, Show, Functor, Foldable, Traversable)++derive [makeEqF, makeShowF, makeShowConstr] [''LOGIC]++instance Render LOGIC++type Lang = NUM :+: LOGIC++newtype Expr a = Expr { unExpr :: Term Lang }+  deriving (Eq, Show)++instance Rep Expr+  where+    type PF Expr = Lang+    toRep   = Expr+    fromRep = unExpr++instance (NUM :<: f) => Num (Term f)+  where+    fromInteger = inject . Num+    a + b       = inject $ Add a b+    a - b       = inject $ Sub a b+    a * b       = inject $ Mul a b++deriving instance Num a => Num (Expr a)++deriving instance (NUM :<: PF (LHS f), Num a) => Num (LHS f a)+deriving instance (NUM :<: PF (RHS f), Num a) => Num (RHS f a)++instance (Rep r, LOGIC :<: PF r) => Logic r+  where+    false      = toRep $ inject (Bool False)+    true       = toRep $ inject (Bool True)+    noT        = toRep . inject . Not . fromRep+    a <&> b    = toRep $ inject $ And (fromRep a) (fromRep b)+    a === b    = toRep $ inject $ Equal (fromRep a) (fromRep b)+    cond c t f = toRep $ inject $ Cond (fromRep c) (fromRep t) (fromRep f)++rules =+    [ quantify rule_add1+    , quantify rule_add2+    , quantify rule_sub+    , quantify rule_mul+    , quantify rule_and+    , quantify (rule_eq -:: tCon tA >-> tRule)+    , quantify rule_cond1+    , quantify rule_cond2+    ]++expr1 :: Expr Integer+expr1 = 0 + 4++draw1  = drawTerm $ unExpr expr1+draw1R = drawTerm $ bottomUp rules (unExpr expr1)++expr2 :: Expr Integer+expr2 = (5 + 5 + 3) + (0 + 4)++draw2  = drawTerm $ unExpr expr2+draw2R = drawTerm $ bottomUp rules (unExpr expr2)++expr3 :: Expr Integer+expr3 = cond (0 === 1) (5+5) (5*2)++draw3  = drawTerm $ unExpr expr3+draw3R = drawTerm $ bottomUp rules (unExpr expr3)+

+ ho-rewriting.cabal view

@@ -0,0 +1,85 @@+name:                ho-rewriting+version:             0.1+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+                     domain-specific languages to offer an interface which is+                     both safe and syntactically appealing.+                     .+                     Some examples are found in the @examples@ directory. For+                     more information, see+                     "Lightweight Higher-Order Rewriting in Haskell" (presented at TFP 2015):+                     .+                       * Paper: <http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_DRAFT.pdf>+                     .+                       * Slides: <http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_slides.pdf>+homepage:            https://github.com/emilaxelsson/ho-rewriting+bug-reports:         https://github.com/emilaxelsson/ho-rewriting/issues+license:             BSD3+license-file:        LICENSE+author:              Emil Axelsson+maintainer:          emax@chalmers.se+copyright:           Copyright (c) 2015, Emil Axelsson+category:            Language+build-type:          Simple+extra-source-files:  README.md+cabal-version:       >=1.10++extra-source-files:+  examples/*.hs++source-repository head+  type:     git+  location: https://github.com/emilaxelsson/ho-rewriting++library+  exposed-modules:+    Data.Rewriting.Rules+    Data.Rewriting.FirstOrder+    Data.Rewriting.HigherOrder++  hs-source-dirs:+    src++  build-depends:+    base >=4.7 && <5,+    containers,+    compdata >=0.9,+    mtl,+    patch-combinators++  default-language: Haskell2010++  default-extensions:+    DeriveFoldable+    DeriveFunctor+    DeriveTraversable+    FlexibleContexts+    GeneralizedNewtypeDeriving+    ScopedTypeVariables+    TypeFamilies+    TypeOperators++  other-extensions:+    NoMonomorphismRestriction+    TemplateHaskell+    TupleSections+    UndecidableInstances++  default-language:+    Haskell2010++test-suite examples+  type: exitcode-stdio-1.0++  hs-source-dirs: examples++  main-is: Feldspar.hs++  build-depends:+    base,+    compdata,+    ho-rewriting,+    patch-combinators++  default-language: Haskell2010

+ src/Data/Rewriting/FirstOrder.hs view

@@ -0,0 +1,92 @@+{-# LANGUAGE TupleSections #-}++-- | First-order rewriting+module Data.Rewriting.FirstOrder where++++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++import Data.Rewriting.Rules++++-- | First-order matching. Results in a list of candidate mappings.+--+-- This function assumes that there are no applications of meta-variables in `LHS`.+matchM :: (Functor f, Foldable f, EqF f) => LHS f a -> Term f -> WriterT (Subst f) Maybe ()+matchM (LHS lhs) t = go lhs t+  where+    go (Term (Inl WildCard)) _                       = return ()+    go (Term (Inr (Inl (Meta (MVar (MetaId v)))))) t = tell [(v,t)]+    go (Term (Inr (Inr f))) (Term g)+      | Just subs <- eqMod f g                       = mapM_ (uncurry go) subs+    go _ _                                           = fail "No match"++-- | Check if all terms are equal, and if so, return one of them+solveTerm :: EqF f => [Term f] -> Maybe (Term f)+solveTerm (t:ts) = guard (all (==t) ts) >> return t+solveTerm _      = Nothing++-- | Turn a list of candidate mappings into a substitution. Succeeds iff. all mappings for the same+-- variable are equal.+solveSubst :: EqF f => [(Name, Term f)] -> Maybe (Subst f)+solveSubst s = sequence [fmap (v,) $ solveTerm ts | g <- gs, let (v:_,ts) = unzip g]+  where+    gs = groupBy ((==) `on` fst) s+      -- TODO Make O(n * log n)++-- | First-order matching. Succeeds if the pattern matches and all occurrences of a given+-- meta-variable are matched against equal terms.+--+-- This function assumes that there are no applications of meta-variables in `LHS`.+match :: (Functor f, Foldable f, EqF f) => LHS f a -> Term f -> Maybe (Subst f)+match lhs = solveSubst <=< execWriterT . matchM lhs++-- | Naive substitution. Succeeds iff. each meta-variable in 'RHS' has a mapping in the+-- substitution.+--+-- This function assumes that there are no applications of meta-variables in `RHS`.+substitute :: Traversable f => Subst f -> RHS f a -> Maybe (Term f)+substitute subst = cataM go . unRHS+  where+    go (Inl (Meta (MVar (MetaId v)))) = lookup v subst+    go (Inr f)                        = return (Term f)++-- | Apply a rule. Succeeds iff. both matching and substitution succeeds.+--+-- This function assumes that there are no applications of meta-variables in `LHS` or `RHS`.+rewrite :: (Traversable f, EqF f) => Rule (LHS f) (RHS f) -> Term f -> Maybe (Term f)+rewrite (Rule lhs rhs) t = do+    subst <- match lhs t+    substitute subst rhs++-- | Apply the first succeeding rule from a list of rules. If no rule succeeds the term is returned+-- unchanged.+--+-- 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+    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++-- | 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+

+ src/Data/Rewriting/HigherOrder.hs view

@@ -0,0 +1,304 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Higher-order rewriting+module Data.Rewriting.HigherOrder where++++import Control.Monad.Reader+import Control.Monad.Writer+import qualified Data.Foldable as Foldable+import Data.Function (on)+import Data.List (groupBy)+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Set (Set)+import qualified Data.Set as Set++import Data.Comp+import Data.Comp.Derive+import Data.Comp.Ops+import Data.Comp.Render++import Data.Rewriting.Rules++++-- | Representations supporting variable binding+class Bind r+  where+    var :: Var r a -> r a+    lam :: (Var r a -> r b) -> r (a -> b)++-- | Functor representing object variables+newtype VAR a = Var Name+  deriving (Eq, Show, Ord, Num, Enum, Real, Integral, Functor, Foldable, Traversable)++-- | Functor representing lambda abstraction+data LAM a = Lam Name a+  deriving (Eq, Show, Functor, Foldable, Traversable)++-- | Functor representing application+data APP a = App a a+  deriving (Eq, Show, Functor, Foldable, Traversable)++derive [makeEqF, makeShowF, makeShowConstr] [''VAR]+derive [makeEqF, makeShowF, makeShowConstr] [''LAM]+derive [makeEqF, makeShowF, makeShowConstr] [''APP]++instance Render VAR+instance Render LAM+instance Render APP++fresh :: (LAM :<: f, Functor f, Foldable f) => Term f -> Name+fresh f+    | Just (Lam v _) <- project f = v+1+    | otherwise = maximum $ (0:) $ Foldable.toList $ fmap fresh $ unTerm f++-- | Generic lambda abstraction+mkLam+    :: (Rep r, VAR :<: PF r, LAM :<: PF r, Functor (PF r), Foldable (PF r))+    => (VAR a -> Var r a) -> (Var r a -> r b) -> r (a -> b)+mkLam mkVar f = toRep $ inject $ Lam v $ fromRep body+  where+    body = f (mkVar $ Var v)+    v    = fresh (fromRep body)++-- | Application operator, to use as argument to functions like 'applyFirst', 'bottomUp', etc.+app :: (APP :<: f) => Term (f :&: Set Name) -> Term (f :&: Set Name) -> Term (f :&: Set Name)+app f@(Term (_ :&: fv)) a@(Term (_ :&: av)) = Term (inj (App f a) :&: Set.union fv av)++type instance Var (LHS f) = VAR+type instance Var (RHS f) = VAR++instance (VAR :<: PF (LHS f), LAM :<: PF (LHS f), Functor f, Foldable f) =>+    Bind (LHS f)+  where+    var = LHS . inject . Var . toInteger+    lam = mkLam id++instance (VAR :<: PF (RHS f), LAM :<: PF (RHS f), Functor f, Foldable f) =>+    Bind (RHS f)+  where+    var = RHS . inject . Var . toInteger+    lam = mkLam id++-- | One-to-one map+type OneToOne a b = (Map a b, Map b a)++-- | Empty one-to-one map+oEmpty :: OneToOne a b+oEmpty = (Map.empty, Map.empty)++-- | Test if a mapping is in a one-to-one map+oMember :: (Ord a, Ord b) => (a,b) -> OneToOne a b -> Bool+oMember (a,b) (ab,_) = case Map.lookup a ab of+    Just b' -> b == b'+    Nothing -> False++-- | Test if either side of a mapping is in a one-to-one map+oMemberEither :: (Ord a, Ord b) => (a,b) -> OneToOne a b -> Bool+oMemberEither (a,b) (ab,ba) = Map.member a ab || Map.member b ba++-- | Left lookup in a one-to-one map+oLookupL :: Ord a => a -> OneToOne a b -> Maybe b+oLookupL a (ab,_) = Map.lookup a ab++-- | Insert a one-to-one mapping+oInsert :: (Ord a, Ord b) => (a,b) -> OneToOne a b -> OneToOne a b+oInsert (a,b) (ab,ba) = (Map.insert a b ab', Map.insert b a ba')+  where+    ab' = case Map.lookup b ba of+      Just a' -> Map.delete a' ab+      Nothing -> ab+    ba' = case Map.lookup a ab of+      Just b' -> Map.delete b' ba+      Nothing -> ba++getAnn :: Term (f :&: a) -> a+getAnn (Term (_ :&: a)) = a++-- | Environment keeping track of alpha-renaming+type AlphaEnv = OneToOne Name {-pattern-} Name {-term-}++-- | Higher-order matching. Results in a list of candidate mappings.+matchM :: forall f a+    .  ( VAR :<: f+       , LAM :<: f+       , VAR :<: PF (LHS f)+       , LAM :<: PF (LHS f)+       , Functor f, Foldable f, EqF f+       )+    => LHS f a+    -> Term (f :&: Set Name)+    -> ReaderT AlphaEnv (WriterT (Subst (f :&: Set Name)) Maybe) ()+matchM (LHS lhs) t = go lhs t+  where+    go (Term (Inl WildCard)) _ = return ()++    go (Term (Inr (Inl (Meta mv)))) t = ReaderT $ \env -> goo env mv t+      where+        goo :: AlphaEnv+            -> MetaExp (LHS f) b+            -> Term (f :&: Set Name)+            -> WriterT (Subst (f :&: Set Name)) Maybe ()+        goo env (MVar (MetaId m)) t+            | Set.null (Set.intersection boundInPatt freeIn_t) = tell [(m,t)]+            | otherwise = fail "Variables would escape"+          where+            boundInPatt = Map.keysSet $ snd env+            freeIn_t    = getAnn t+        goo env (MApp mv (Var v)) t = do+          let Just w = oLookupL v env+                -- Lookup failure is a bug rather than a matching failure+          goo env mv (Term (inj (Lam w t) :&: Set.delete w (getAnn t)))++    go p (Term (g :&: _))+      | Just (Var v) <- project p+      , Just (Var w) <- proj g+      = do+          env <- ask+          guard ((v,w) `oMember` env)+            -- Rules should be closed, so `w` can't be free++    go p (Term (g :&: _))+      | Just (Lam v a) <- project p+      , Just (Lam w b) <- proj g+      = local (oInsert (v,w)) $ go a b++    go (Term (Inr (Inr f))) (Term (g :&: _))+      | Just subs <- eqMod f g+      = mapM_ (uncurry go) subs++    go _ _ = fail "No match"++-- | Alpha-equivalence+alphaEq :: (VAR :<: f, LAM :<: f, Functor f, Foldable f, EqF f) => Term f -> Term f -> Bool+alphaEq a b = runReader (go a b) oEmpty+  where+    go t u+      | Just (Var v) <- project t+      , Just (Var w) <- project u+      = reader $ \env -> oMember (v,w) env || (not (oMemberEither (v,w) env) && v==w)+    go t u+      | Just (Lam v a) <- project t+      , Just (Lam w b) <- project u+      = local (oInsert (v,w)) $ go a b+    go (Term f) (Term g)+      | Just subs <- eqMod f g+      = fmap and $ mapM (uncurry go) subs+    go _ _ = return False++-- | Check if all terms are alpha-equivalent, and if so, return one of them+solveTermAlpha :: (VAR :<: f, LAM :<: f, Functor f, Foldable f, EqF f) =>+    [Term (f :&: a)] -> Maybe (Term (f :&: a))+solveTermAlpha (t:ts) = guard (all (alphaEq (stripA t)) (map stripA ts)) >> return t+solveTermAlpha _      = Nothing++-- | Turn a list of candidate mappings into a substitution. Succeeds iff. all mappings for the same+-- variable are alpha-equivalent.+solveSubstAlpha :: (VAR :<: f, LAM :<: f, Functor f, Foldable f, EqF f) =>+    Subst (f :&: a) -> Maybe (Subst (f :&: a))+solveSubstAlpha s = sequence [fmap (v,) $ solveTermAlpha ts | g <- gs, let (v:_,ts) = unzip g]+  where+    gs = groupBy ((==) `on` fst) s+      -- TODO Make O(n * log n)++-- | Higher-order matching. Succeeds if the pattern matches and all occurrences of a given+-- meta-variable are matched against equal terms.+match+    :: ( VAR :<: f+       , LAM :<: f+       , VAR :<: PF (LHS f)+       , LAM :<: PF (LHS f)+       , Functor f, Foldable f, EqF f+       )+    => LHS f a -> Term (f :&: Set Name) -> Maybe (Subst (f :&: Set Name))+match lhs = solveSubstAlpha <=< execWriterT . flip runReaderT oEmpty . matchM lhs++-- | Annotate a node with its set of free variables+annFreeVars :: (VAR :<: f, LAM :<: f, Functor f, Foldable f) =>+    f (Term (f :&: Set Name)) -> Term (f :&: Set Name)+annFreeVars f+    | 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)+annFreeVars f = Term (f :&: Foldable.foldMap getAnn f)++-- | Capture-avoiding substitution. Succeeds iff. each meta-variable in 'RHS' has a mapping in the+-- substitution.+substitute :: forall f g a+    .  ( VAR :<: f+       , LAM :<: f+       , Traversable f+       , g ~ (f :&: Set Name)+       )+    => (Term g -> Term g -> Term g)  -- ^ Application operator+    -> Subst g+    -> RHS f a+    -> Maybe (Term g)+substitute app subst = cataM go . unRHS+  where+    go :: PF (RHS f) (Term g) -> Maybe (Term g)+    go (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++-- | Apply a rule. Succeeds iff. both matching and substitution succeeds.+rewrite+    :: ( VAR :<: f+       , LAM :<: f+       , VAR :<: PF (LHS f)+       , LAM :<: PF (LHS 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))+rewrite app (Rule lhs rhs) t = do+    subst <- match lhs t+    substitute app subst rhs++-- | Apply the first succeeding rule from a list of rules. If no rule succeeds the term is returned+-- unchanged.+applyFirst+    :: ( VAR :<: f+       , LAM :<: f+       , VAR :<: PF (LHS f)+       , LAM :<: PF (LHS 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)+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+    :: ( VAR :<: f+       , LAM :<: f+       , VAR :<: PF (LHS f)+       , LAM :<: PF (LHS f)+       , Traversable f, EqF 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+

+ src/Data/Rewriting/Rules.hs view

@@ -0,0 +1,208 @@+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Rewrite rules+module Data.Rewriting.Rules where++++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++++----------------------------------------------------------------------------------------------------+-- * Tagless rewrite rules+----------------------------------------------------------------------------------------------------++-- | Rewrite rules+data Rule lhs rhs+  where+    Rule :: lhs a -> rhs a -> Rule lhs rhs++-- | Construct a rule from an LHS and an RHS+(===>) :: lhs a -> rhs a -> Rule lhs rhs+(===>) = Rule++infix 1 ===>++-- | Representations supporting wildcards+class WildCard r+  where+    __ :: r a++-- | Meta-variable applied to a number of 'Var' expressions+data MetaExp r a+  where+    MVar :: MetaRep r a -> MetaExp r a+    MApp :: MetaExp r (a -> b) -> MetaArg r a -> MetaExp r b++-- | Representations supporting meta-variables+class MetaVar r+  where+    -- Representation of meta-variable identifiers+    type MetaRep r :: * -> *+    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-variable application (used for all but the first and last variable)+($$) :: MetaExp r (a -> b) -> MetaArg r a -> MetaExp r b+($$) = MApp++-- | Meta-variable application (used for the last variable)+($-) :: MetaVar r => MetaExp r (a -> b) -> MetaArg r a -> r b+f $- a = metaExp (MApp f a)++-- | Meta-variable application (used for the first variable)+(-$) :: MetaRep r (a -> b) -> MetaArg r a -> MetaExp r b+f -$ a = MApp (MVar f) a++-- | Meta-variable application (used when there is only variable)+(-$-) :: MetaVar r => MetaRep r (a -> b) -> MetaArg r a -> r b+f -$- a = metaExp (MApp (MVar f) a)++infixl 2 $$, $-, -$, -$-++-- | Variable identifier+type Name = Integer++-- | Typed meta-variable identifiers+newtype MetaId a = MetaId Name+  deriving (Eq, Show, Ord, Num, Enum, Real, Integral)++-- | Rules that may take a number of meta-variables as arguments. Those meta-variables are+-- implicitly forall-quantified.+class Quantifiable rule+  where+    -- | Rule type after quantification+    type RuleType rule++    -- | Quantify a rule starting from the provided variable identifier+    quantify' :: Name -> rule -> RuleType rule++-- | Base case: no meta-variables+instance Quantifiable (Rule lhs rhs)+  where+    type RuleType (Rule lhs rhs) = Rule lhs rhs+    quantify' _ = id++-- | Recursive case: one more meta-variable+instance (Quantifiable rule, m ~ MetaId a) => Quantifiable (m -> rule)+  where+    type RuleType (m -> rule) = RuleType rule+    quantify' i rule = quantify' (i+1) (rule (MetaId i))++-- | Forall-quantify the meta-variable arguments of a rule+quantify :: (Quantifiable rule, RuleType rule ~ Rule lhs rhs) => rule -> Rule lhs rhs+quantify = quantify' 0++++----------------------------------------------------------------------------------------------------+-- * Representation of rules+----------------------------------------------------------------------------------------------------++-- | Functor representing wildcards+data WILD a = WildCard+  deriving (Eq, Show, Functor, Foldable, Traversable)++-- | Functor representing meta variables applied to a number of 'Var' expressions+data META r a = forall b . Meta (MetaExp r b)++instance Functor     (META r) where fmap f (Meta m) = Meta m+instance Foldable    (META r) where foldr _ a _ = a+instance Traversable (META r) where traverse _ (Meta m) = pure (Meta m)++-- | Left hand side of a rule+newtype LHS f a = LHS { unLHS :: Term (WILD :+: META (LHS f) :+: f) }++-- | Right hand side of a rule+newtype RHS f a = RHS { unRHS :: Term (META (RHS f) :+: f) }++instance WildCard (LHS f)+  where+    __ = LHS $ Term $ Inl WildCard++-- | Representation of object variables+type family Var (r :: * -> *) :: * -> *++instance MetaVar (LHS f)+  where+    type MetaRep (LHS f) = MetaId+    type MetaArg (LHS f) = Var (LHS f)+    metaExp = LHS . Term . Inr . Inl . Meta++instance MetaVar (RHS f)+  where+    type MetaRep (RHS f) = MetaId+    type MetaArg (RHS f) = RHS f+    metaExp = RHS . Term . Inl . Meta++++----------------------------------------------------------------------------------------------------+-- * Generalize over representations+----------------------------------------------------------------------------------------------------++class Rep r+  where+    type PF r :: * -> *+    toRep   :: Term (PF r) -> r a+    fromRep :: r a -> Term (PF r)++instance Rep (LHS f)+  where+    type PF (LHS f) = WILD :+: META (LHS f) :+: f+    toRep   = LHS+    fromRep = unLHS++instance Rep (RHS f)+  where+    type PF (RHS f) = META (RHS f) :+: f+    toRep   = RHS+    fromRep = unRHS++++----------------------------------------------------------------------------------------------------+-- * Misc.+----------------------------------------------------------------------------------------------------++tRule :: Patch (Rule (LHS f) (RHS f)) (Rule (LHS f) (RHS f))+tRule = id++data A = A deriving (Eq)  -- Denoting a polymorphic type+data B = B deriving (Eq)  -- Denoting a polymorphic type+data C = C deriving (Eq)  -- Denoting a polymorphic type++tA :: Patch A A+tA = id++tB :: Patch B B+tB = id++tC :: Patch C C+tC = id++-- | Substitution+type Subst f = [(Name, Term f)]+