kure 0.2 → 0.2.1
raw patch · 4 files changed
+220/−6 lines, 4 filesdep −containers
Dependencies removed: containers
Files
- kure.cabal +6/−6
- test/Exp.hs +29/−0
- test/Id.hs +11/−0
- test/Test.hs +174/−0
kure.cabal view
@@ -1,5 +1,5 @@ Name: kure-Version: 0.2+Version: 0.2.1 Synopsis: Combinators for Strategic Programming Description: KURE is a DSL for building rewriting DSLs. KURE shares combinator names and concepts with Stratego, but unlike Stratego, KURE is strongly typed.@@ -14,15 +14,16 @@ Maintainer: Andy Gill <andygill@ku.edu> Copyright: (c) 2006-2008 Andy Gill Homepage: http://ittc.ku.edu/~andygill/kure.php-Build-Depends: base Stability: alpha- build-type: Simple Cabal-Version: >= 1.6-+Extra-Source-Files:+ test/Test.hs+ test/Exp.hs+ test/Id.hs Library- Build-Depends: base, containers + Build-Depends: base Exposed-modules: Language.KURE, Language.KURE.RewriteMonad, @@ -39,6 +40,5 @@ -- Main-Is: Test.hs -- Hs-Source-Dirs: ., test -- buildable: True-
+ test/Exp.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE TypeFamilies #-}++module Exp where++import Language.KURE+ +type Name = String+data Exp = Lam Name Exp+ | App Exp Exp+ | Var Name+ deriving Show++instance Term Exp where+ type Generic Exp = Exp -- Exp is its own Generic root.+ inject = id+ select e = return e++-- examples+e1 = Var "x"+e2 = Var "y"+e3 = Lam "x" e1+e4 = Lam "x" e2+e5 = App e1 e2+e6 = App e3 e4+e7 = App e4 e6+e8 = Lam "z" (Var "z")+e9 = Lam "x" e3+e10 = Lam "x" e4+e11 = Lam "x" e5
+ test/Id.hs view
@@ -0,0 +1,11 @@+module Id where+ +newtype Id a = Id a++instance Monad Id where+ return = Id+ (Id a) >>= k = Id $ runId (k a)+ fail = error "Id: failure"++runId :: Id a -> a+runId (Id a) = a
+ test/Test.hs view
@@ -0,0 +1,174 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}++module Main where++import Language.KURE+import Language.KURE.Term as T++import Data.Monoid+import Control.Monad+import Data.List+import Debug.Trace+++import Exp+import Id++type R e = Rewrite Id () e+type T e1 e2 = Translate Id () e1 e2++main = do+ let es1 = [e1,e2,e3,e4,e5,e6,e7,e8,e9,e10,e11]+ sequence_ [ print e | e <- es1]++ let frees :: Exp -> Id [Name]+ frees exp = do Right (fs,b) <- runTranslate freeExpT () exp+ return $ nub fs+ let e_frees = map (runId . frees) es1+ sequence_ [ print e | e <- e_frees]+ + sequence [ print (e,function (substExp v ed) e) | v <- ["x","y","z"], ed <- es1, e <- es1 ]++ sequence [ print (runId $ runTranslate betaRedR () e) | e <- es1 ]+ let fn = extractR (topdownR (repeatR betaRedR))+ sequence [ print (runId $ runTranslate fn () e) | e <- es1 ]+ + +------------------------------------------------------------------------+--+-- First the guards+--++appG :: R Exp+appG = acceptR $ \ e -> case e of { App {} -> True ; _ -> False }++lamG :: R Exp+lamG = acceptR $ \ e -> case e of { Lam {} -> True ; _ -> False }++varG :: R Exp+varG = acceptR $ \ e -> case e of { Var {} -> True; _ -> False }++------------------------------------------------------------------------+--+-- Then the rewrites and Universals+--+++appR :: R Exp + -> R Exp+ -> R Exp+appR rr1 rr2 = appG >-> rewrite (\ (App e1 e2) -> + transparently $ + liftM2 App (apply rr1 e1) + (apply rr2 e2)) ++lamR :: R Exp + -> R Exp+lamR rr = lamG >-> rewrite (\ (Lam n e) -> + transparently $ do+ e' <- apply rr e+ return $ Lam n e')+ +varR :: R Exp+varR = varG++appU :: (Monoid r) => + T Exp r+ -> T Exp r+ -> T Exp r+appU rr1 rr2 = appG >-> translate (\ (App e1 e2) -> + liftM2 mappend (apply rr1 e1) + (apply rr2 e2)) ++lamU :: (Monoid r) => T Exp r+ -> T Exp r+lamU rr = lamG >-> translate (\ (Lam n e) -> do+ e' <- apply rr e+ return $ e')+ +varU :: (Monoid r) => T Exp r+varU = varG >-> translate (\ _ -> return $ mempty)+++------------------------------------------------------------------------+--+-- Finally, the pattern matches+--++appP ::(Exp -> Exp -> T Exp r)+ -> T Exp r+appP f = appG >-> readerT (\ (App e1 e2) -> f e1 e2) ++lamP :: (Name -> Exp -> T Exp r)+ -> T Exp r+lamP f = lamG >-> readerT (\ (Lam n e) -> f n e)++varP :: (Name -> T Exp r)+ -> T Exp r+varP f = varG >-> readerT (\ (Var n) -> f n)++------------------------------------------------------------------------++instance Walker Id () Exp where+ allR rr = appR rr rr <+ lamR rr <+ varR+ crushU rr = appU rr rr <+ lamU rr <+ varU++function :: Translate Id () a b -> a -> b+function f a = runId $ do + Right (b,_) <- runTranslate f () a+ return $ b++------------------------------------------------------------------------++freeExpT :: T Exp [Name]+freeExpT = lambda <+ var <+ crushU freeExpT+ where+ var = varG >-> translate (\ (Var v) -> return [v])+ lambda = lamG >-> translate (\ (Lam n e) -> do+ frees <- apply freeExpT e+ return (nub frees \\ [n]))+ +freeExp :: Exp -> [Name]+freeExp = function freeExpT++newName :: Name -> [Name] -> Name+newName suggest frees = + head [ nm | nm <- suggest : suggests+ , nm `notElem` frees+ ]+ where suggests = [ suggest ++ "_" ++ show n | n <- [1..]]++-- Only works for lambdas, fails for all others+shallowAlpha :: [Name] -> R Exp+shallowAlpha frees' = lamG >-> + rewrite (\ (Lam n e) -> do+ frees <- apply freeExpT e+ let n' = newName n (frees ++ frees')+ e' <- apply (substExp n (Var n')) e+ return $ Lam n' e') ++substExp :: Name -> Exp -> R Exp+substExp v s = rule1 <+ rule2 <+ rule3 <+ rule4 <+ rule5 <+ rule6+ where+ -- From Lambda Calc Textbook, the 6 rules.+ rule1 = varP $ \ n -> n == v ? constT s+ rule2 = varP $ \ n -> n /= v ? idR+ rule3 = lamP $ \ n e -> n == v ? idR+ rule4 = lamP $ \ n e -> (n `notElem` freeExp s || v `notElem` freeExp e) + ? allR (substExp v s)+ rule5 = lamP $ \ n e -> (n `elem` freeExp s && v `elem` freeExp e)+ ? (shallowAlpha (freeExp s) >-> substExp v s)+ rule6 = appG >-> allR (substExp v s)++ +-------------++betaRedR :: R Exp+betaRedR = rewrite $ \ e ->+ case e of+ (App (Lam v e1) e2) -> apply (substExp v e2) e1+ _ -> fail "betaRed"++debugR :: (Show e) => String -> R e +debugR msg = translate $ \ e -> transparently $ trace (msg ++ " : " ++ show e) (return e)+