kure 0.2.3 → 0.3.1
raw patch · 10 files changed
+130/−296 lines, 10 files
Files
- LICENSE +1/−1
- Language/KURE/Combinators.hs +54/−16
- Language/KURE/Rewrite.hs +1/−1
- Language/KURE/RewriteMonad.hs +50/−32
- Language/KURE/Term.hs +9/−10
- Language/KURE/Translate.hs +13/−6
- kure.cabal +2/−16
- test/Exp.hs +0/−29
- test/Id.hs +0/−11
- test/Test.hs +0/−174
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2006-2008 Andy Gill+Copyright (c) 2006-2009 Andy Gill All rights reserved. Redistribution and use in source and binary forms, with or without
Language/KURE/Combinators.hs view
@@ -18,8 +18,9 @@ , (>->) , failT , readerT- , getDecsT- , mapDecsT+ , readEnvT+ , mapEnvT+ , writeEnvT , pureT , constT , concatT@@ -32,6 +33,13 @@ , acceptR , idR , failR+ , -- * The Prelude combinators+ tuple2R+ , listR+ , maybeR+ , tuple2U+ , listU+ , maybeU , -- * Generic failure, over both 'Monad's and 'Translate's. (?) , Failable(..)@@ -41,6 +49,7 @@ import Language.KURE.Translate import Language.KURE.Rewrite import Data.Monoid+import Control.Monad infixl 3 <+, >->, .+, !-> infixr 3 ?@@ -52,11 +61,11 @@ -- | like a catch, '<+' does the first translate , and if it fails, then does the second translate. (<+) :: (Monoid dec, Monad m) => Translate m dec a b -> Translate m dec a b -> Translate m dec a b-(<+) rr1 rr2 = translate $ \ e -> transparently $ apply rr1 e `catchM` (\ _ -> apply rr2 e)+(<+) rr1 rr2 = transparently $ translate $ \ e -> apply rr1 e `catchM` (\ _ -> apply rr2 e) -- | like a @;@ If the first translate succeeds, then do to the second translate after the first translate. (>->) :: (Monoid dec, Monad m) => Translate m dec a b -> Translate m dec b c -> Translate m dec a c-(>->) rr1 rr2 = translate $ \ e -> transparently $ chainM (apply rr1 e) ( \ _i e2 -> apply rr2 e2)+(>->) rr1 rr2 = transparently $ translate $ \ e -> chainM (apply rr1 e) ( \ _i e2 -> apply rr2 e2) -- | failing translation. failT :: (Monad m, Monoid dec) => String -> Translate m dec a b@@ -65,17 +74,21 @@ -- | look at the argument for the translation before choosing which translation to perform. readerT :: (Monoid dec, Monad m) => (a -> Translate m dec a b) -> Translate m dec a b-readerT fn = translate $ \ expA -> transparently $ apply (fn expA) expA+readerT fn = transparently $ translate $ \ expA -> apply (fn expA) expA -- | look at the @dec@ before choosing which translation to do.-getDecsT :: (Monad m, Monoid dec) => (dec -> Translate m dec a b) -> Translate m dec a b-getDecsT f = translate $ \ e -> transparently $- do dec <- getDecsM +readEnvT :: (Monad m, Monoid dec) => (dec -> Translate m dec a b) -> Translate m dec a b+readEnvT f = transparently $ translate $ \ e -> + do dec <- readEnvM apply (f dec) e +-- | add to the context 'dec', which is propogated using a writer monad.+writeEnvT :: (Monad m, Monoid dec) => dec -> Rewrite m dec a+writeEnvT dec = translate $ \ e -> do writeEnvM dec ; return e+ -- | change the @dec@'s for a scoped translation.-mapDecsT :: (Monoid dec,Monad m) => (dec -> dec) -> Translate m dec a r -> Translate m dec a r-mapDecsT f_env rr = translate $ \ e -> mapDecsM f_env (apply rr e)+mapEnvT :: (Monoid dec,Monad m) => (dec -> dec) -> Translate m dec a r -> Translate m dec a r+mapEnvT f_env rr = transparently $ translate $ \ e -> mapEnvM f_env (apply rr e) -- | 'pureT' promotes a function into an unfailable, non-identity 'Translate'. pureT :: (Monad m,Monoid dec) => (a -> b) -> Translate m dec a b@@ -95,11 +108,11 @@ -- | if the first rewrite is an identity, then do the second rewrite. (.+) :: (Monoid dec, Monad m) => Rewrite m dec a -> Rewrite m dec a -> Rewrite m dec a-(.+) a b = a `wasId` (\ i -> if i then b else idR)+(.+) a b = a `countTrans` (\ i -> if i == 0 then b else idR) -- | if the first rewrite was /not/ an identity, then also do the second rewrite. (!->) :: (Monoid dec, Monad m) => Rewrite m dec a -> Rewrite m dec a -> Rewrite m dec a -(!->) a b = a `wasId` (\ i -> if i then idR else b)+(!->) a b = a `countTrans` (\ i -> if i == 0 then idR else b) -- | catch a failing 'Rewrite', making it into an identity. tryR :: (Monoid dec, Monad m) => Rewrite m dec a -> Rewrite m dec a@@ -115,7 +128,7 @@ -- | look at the argument to a rewrite, and choose to be either a failure of trivial success. acceptR :: (Monoid dec, Monad m) => (a -> Bool) -> Rewrite m dec a-acceptR fn = translate $ \ expA -> transparently $+acceptR fn = transparently $ translate $ \ expA -> if fn expA then return expA else fail "accept failed"@@ -123,13 +136,38 @@ -- | identity rewrite. idR :: (Monad m, Monoid dec) => Rewrite m dec exp-idR = rewrite $ \ e -> transparently $ return e+idR = transparently $ rewrite $ \ e -> return e -- | failing rewrite. failR :: (Monad m, Monoid dec) => String -> Rewrite m dec a failR = failT --------------------------------------------------------------------------------+-- Prelude structures++tuple2R :: (Monoid dec, Monad m) => Rewrite m dec a -> Rewrite m dec b -> Rewrite m dec (a,b)+tuple2R rra rrb = transparently $ rewrite $ \ (a,b) -> liftM2 (,) (apply rra a) (apply rrb b)++listR :: (Monoid dec, Monad m) => Rewrite m dec a -> Rewrite m dec [a]+listR rr = transparently $ rewrite $ mapM (apply rr)++maybeR :: (Monoid dec, Monad m) => Rewrite m dec a -> Rewrite m dec (Maybe a)+maybeR rr = transparently $ rewrite $ \ e -> case e of+ Just e' -> liftM Just (apply rr e')+ Nothing -> return $ Nothing++tuple2U :: (Monoid dec, Monad m, Monoid r) => Translate m dec a r -> Translate m dec b r -> Translate m dec (a,b) r+tuple2U rra rrb = translate $ \ (a,b) -> liftM2 mappend (apply rra a) (apply rrb b)++listU :: (Monoid dec, Monad m, Monoid r) => Translate m dec a r -> Translate m dec [a] r+listU rr = translate $ liftM mconcat . mapM (apply rr)++maybeU :: (Monoid dec, Monad m, Monoid r) => Translate m dec a r -> Translate m dec (Maybe a) r+maybeU rr = translate $ \ e -> case e of+ Just e' -> apply rr e'+ Nothing -> return $ mempty++-------------------------------------------------------------------------------- -- | Failable structure. class Failable f where failure :: String -> f a@@ -148,8 +186,8 @@ -------------------------------------------------------------------------------- -- internal to this module.-wasId :: (Monoid dec, Monad m) => Rewrite m dec a -> (Bool -> Rewrite m dec a) -> Rewrite m dec a-wasId rr fn = translate $ \ e -> transparently $+countTrans :: (Monoid dec, Monad m) => Rewrite m dec a -> (Int -> Rewrite m dec a) -> Rewrite m dec a+countTrans rr fn = transparently $ translate $ \ e -> chainM (apply rr e) (\ i e' -> apply (fn i) e')
Language/KURE/Rewrite.hs view
@@ -42,5 +42,5 @@ => Rewrite m dec exp -> dec -> exp - -> m (Either String (exp,dec))+ -> m (Either String (exp,dec,Int)) runRewrite = runTranslate
Language/KURE/RewriteMonad.hs view
@@ -12,15 +12,18 @@ module Language.KURE.RewriteMonad ( RewriteM -- abstract , RewriteStatusM(..)+ , Count(..)+ , theCount , runRewriteM , failM , catchM , chainM , liftQ , markM- , transparently- , getDecsM- , mapDecsM+ , transparentlyM+ , readEnvM+ , mapEnvM+ , writeEnvM ) where @@ -34,18 +37,28 @@ runRewriteM :: dec -> m (RewriteStatusM dec exp) } -data IdStatus = EmptyId | IsId | NotId -instance Monoid IdStatus where- mempty = EmptyId- - mappend EmptyId y = y- mappend x EmptyId = x- mappend IsId IsId = IsId- mappend _ _ = NotId+data Count = LoneTransform+ | Count !Int +-- | How many transformations have been performed?++theCount :: Count -> Int +theCount (LoneTransform) = 1+theCount (Count n) = n++instance Monoid Count where+ mempty = Count 0++ mappend (Count 0) other = other+ mappend other (Count 0) = other+ mappend (Count i1) (Count i2) = Count (i1 + i2)+ mappend (LoneTransform) (Count i2) = Count $ succ i2+ mappend (Count i1) (LoneTransform) = Count $ succ i1+ mappend (LoneTransform) (LoneTransform) = Count $ 2+ data RewriteStatusM dec exp- = RewriteReturnM exp !(Maybe dec) !IdStatus -- ^ a regular success+ = RewriteReturnM exp !(Maybe dec) !Count -- ^ a regular success | RewriteFailureM String -- ^ a real failure -- | RewriteIdM exp -- ^ identity marker on a value @@ -56,7 +69,7 @@ -- C1 (e1) => C1 (C2 (e2)) => C1 (C2 (C3 (e3))) -- will require mergeing?? instance (Monoid dec,Monad m) => Monad (RewriteM m dec) where- return e = RewriteM $ \ _ -> return $ RewriteReturnM e Nothing EmptyId+ return e = RewriteM $ \ _ -> return $ RewriteReturnM e Nothing mempty (RewriteM m) >>= k = RewriteM $ \ dec -> do r <- m dec case r of@@ -96,13 +109,14 @@ chainM :: (Monoid dec,Monad m) => (RewriteM m dec b) - -> (Bool -> b -> RewriteM m dec c)+ -> (Int -> b -> RewriteM m dec c) -> RewriteM m dec c chainM m k = RewriteM $ \ dec -> do r <- runRewriteM m dec case r of RewriteReturnM a ds ids -> - do r2 <- runRewriteM (k (isId ids) a) (case ds of+ do r2 <- runRewriteM (k (theCount ids) a) + (case ds of Nothing -> dec Just ds2 -> ds2 `mappend` dec) case r2 of@@ -110,9 +124,8 @@ return $ RewriteReturnM a' (ds' `mappend` ds) (ids' `mappend` ids) RewriteFailureM msg -> return $ RewriteFailureM msg RewriteFailureM msg -> return $ RewriteFailureM msg -- and still fail - where- isId NotId = False- isId _ = True++ -- | 'markM' is used to mark a monadic rewrite as a non-identity, -- unless the congruence flag is set.@@ -120,28 +133,33 @@ markM (RewriteM m) = RewriteM $ \ dec -> do r <- m dec case r of- RewriteReturnM a ds EmptyId -> return $ RewriteReturnM a ds NotId- RewriteReturnM a ds IsId -> return $ RewriteReturnM a ds EmptyId- RewriteReturnM a ds ids -> return $ RewriteReturnM a ds ids- RewriteFailureM msg -> return $ RewriteFailureM msg+ RewriteReturnM a ds (Count 0) -> return $ RewriteReturnM a ds LoneTransform+ RewriteReturnM a ds (Count n) -> return $ RewriteReturnM a ds (Count $ succ n)+ RewriteReturnM a ds (LoneTransform) -> return $ RewriteReturnM a ds (Count 2)+ RewriteFailureM msg -> return $ RewriteFailureM msg -- | 'transparently' sets the congruence flag, such that if the -- monadic action was identity preserving, then a 'markM' does -- not set the non-indentity flag. -transparently :: (Monad m) => RewriteM m dec a -> RewriteM m dec a-transparently (RewriteM m) = RewriteM $ \ dec -> do+transparentlyM :: (Monad m) => RewriteM m dec a -> RewriteM m dec a+transparentlyM (RewriteM m) = RewriteM $ \ dec -> do r <- m dec case r of- RewriteReturnM a ds EmptyId -> return $ RewriteReturnM a ds IsId- RewriteReturnM a ds ids -> return $ RewriteReturnM a ds ids- RewriteFailureM msg -> return $ RewriteFailureM msg-+ RewriteReturnM a ds LoneTransform -> return $ RewriteReturnM a ds (Count 0)+ RewriteReturnM a ds other -> return $ RewriteReturnM a ds other+ RewriteFailureM msg -> return $ RewriteFailureM msg -- | 'getDecsM' reads the local environment-getDecsM :: (Monad m, Monoid dec) => RewriteM m dec dec-getDecsM = RewriteM $ \ dec -> return $ RewriteReturnM dec mempty mempty+readEnvM :: (Monad m, Monoid dec) => RewriteM m dec dec+readEnvM = RewriteM $ \ dec -> return $ RewriteReturnM dec mempty mempty -- | 'mapDecs' changes the local environment, inside a local monadic invocation.-mapDecsM :: (Monad m, Monoid dec) => (dec -> dec) -> RewriteM m dec a -> RewriteM m dec a-mapDecsM fn (RewriteM m) = RewriteM $ \ dec -> m (fn dec)+mapEnvM :: (Monad m, Monoid dec) => (dec -> dec) -> RewriteM m dec a -> RewriteM m dec a+mapEnvM fn (RewriteM m) = RewriteM $ \ dec -> m (fn dec)+++-- | 'writeDecM' writes a value to the writer monad inside the 'RewriteM'.+writeEnvM :: (Monad m,Monoid dec) => dec -> RewriteM m dec ()+writeEnvM dec = RewriteM $ \ _dec -> return $ RewriteReturnM () (Just dec) (Count 0)+
Language/KURE/Term.hs view
@@ -22,7 +22,6 @@ , foldU ) where -import Language.KURE.RewriteMonad import Language.KURE.Translate import Language.KURE.Rewrite import Language.KURE.Combinators@@ -57,7 +56,7 @@ -- | 'extractR' converts a 'Rewrite' over a 'Generic' into a rewrite over a specific expression type. extractR :: (Monad m, Term exp, Monoid dec) => Rewrite m dec (Generic exp) -> Rewrite m dec exp -- at *this* type-extractR rr = rewrite $ \ e -> transparently $ do+extractR rr = transparently $ rewrite $ \ e -> do e' <- apply rr (inject e) case select e' of Nothing -> fail "extractR"@@ -66,13 +65,13 @@ -- | 'extractU' converts a 'Translate' taking a 'Generic' into a translate over a specific expression type. extractU :: (Monad m, Term exp, Monoid dec) => Translate m dec (Generic exp) r -> Translate m dec exp r-extractU rr = translate $ \ e -> transparently $ apply rr (inject e)+extractU rr = transparently $ translate $ \ e -> apply rr (inject e) -- | 'promoteR' promotes a 'Rewrite' into a 'Generic' 'Rewrite'; other types inside Generic cause failure. -- 'try' can be used to convert a failure-by-default promotion into a 'id-by-default' promotion. promoteR :: (Monad m, Term exp, Monoid dec) => Rewrite m dec exp -> Rewrite m dec (Generic exp)-promoteR rr = rewrite $ \ e -> transparently $ do+promoteR rr = transparently $ rewrite $ \ e -> do case select e of Nothing -> fail "promoteR" Just e' -> do@@ -82,30 +81,30 @@ -- | 'promoteU' promotes a 'Translate' into a 'Generic' 'Translate'; other types inside Generic cause failure. promoteU :: (Monad m, Term exp, Monoid dec) => Translate m dec exp r -> Translate m dec (Generic exp) r-promoteU rr = translate $ \ e -> transparently $ do+promoteU rr = transparently $ translate $ \ e -> do case select e of Nothing -> fail "promoteI" Just e' -> apply rr e' ------------------------------------------------------------------------------- --- apply a rewrite in a top down manner.+-- | apply a rewrite in a top down manner. topdownR :: (e ~ Generic e, Walker m dec e) => Rewrite m dec (Generic e) -> Rewrite m dec (Generic e) topdownR s = s >-> allR (topdownR s) --- apply a rewrite in a bottom up manner.+-- | apply a rewrite in a bottom up manner. bottomupR :: (e ~ Generic e, Walker m dec e) => Rewrite m dec (Generic e) -> Rewrite m dec (Generic e) bottomupR s = allR (bottomupR s) >-> s --- apply a rewrite in a top down manner, prunning at successful rewrites.+-- | apply a rewrite in a top down manner, prunning at successful rewrites. alltdR :: (e ~ Generic e, Walker m dec e) => Rewrite m dec (Generic e) -> Rewrite m dec (Generic e) alltdR s = s <+ allR (alltdR s) --- apply a rewrite twice, in a topdown and bottom up way, using one single tree traversal.+-- | apply a rewrite twice, in a topdown and bottom up way, using one single tree traversal. downupR :: (e ~ Generic e, Walker m dec e) => Rewrite m dec (Generic e) -> Rewrite m dec (Generic e) downupR s = s >-> allR (downupR s) >-> s --- a fixed point traveral, starting with the innermost term.+-- | a fixed point traveral, starting with the innermost term. innermostR :: (e ~ Generic e, Walker m dec e) => Rewrite m dec (Generic e) -> Rewrite m dec (Generic e) innermostR s = bottomupR (tryR (s >-> innermostR s))
Language/KURE/Translate.hs view
@@ -16,6 +16,7 @@ ( Translate , apply , runTranslate+ , transparently , translate ) where @@ -34,17 +35,24 @@ apply :: (Monoid dec, Monad m) => Translate m dec exp1 exp2 -> exp1 -> RewriteM m dec exp2 apply (Translate t) exp1 = t exp1 - -- | 'translate' is the standard way of building a 'Translate', where if the translation is successful it -- is automatically marked as a non-identity translation. ----- Note: @translate $ \ _ e -> return e@ /is not/ an identity rewrite, but a succesful rewrite that+-- Note: @translate $ \\ e -> return e@ /is not/ an identity rewrite, but a succesful rewrite that -- returns its provided argument. translate :: (Monoid dec, Monad m) => (exp1 -> RewriteM m dec exp2) -> Translate m dec exp1 exp2 translate f = Translate $ \ e -> markM $ f e +-- | 'transparently' marks a 'translate' (or 'rewrite') as transparent, that is the identity status+-- of any internal applications of 'apply' is preserved across the translate.+--+-- Note: @transparently $ translate $ \\ e -> return e@ /is/ an identity rewrite.++transparently :: (Monoid dec, Monad m) => Translate m dec exp1 exp2 -> Translate m dec exp1 exp2+transparently (Translate m) = Translate $ \ e -> transparentlyM (m e)+ -- | 'runTranslate' executes the translation, returning either a failure message, -- or a success and the new parts of the environment. @@ -52,12 +60,11 @@ => Translate m dec exp res -> dec -> exp - -> m (Either String (res,dec))+ -> m (Either String (res,dec,Int)) runTranslate rr dec e = do res <- runRewriteM (apply rr e) dec case res of- RewriteReturnM exp' Nothing _ -> return (Right (exp',mempty))- RewriteReturnM exp' (Just ds) _ -> return (Right (exp',ds))+ RewriteReturnM exp' Nothing c -> return (Right (exp',mempty,theCount c))+ RewriteReturnM exp' (Just ds) c -> return (Right (exp',ds,theCount c)) RewriteFailureM msg -> return (Left msg)-
kure.cabal view
@@ -1,5 +1,5 @@ Name: kure-Version: 0.2.3+Version: 0.3.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.@@ -12,15 +12,11 @@ License-file: LICENSE Author: Andy Gill Maintainer: Andy Gill <andygill@ku.edu>-Copyright: (c) 2006-2008 Andy Gill+Copyright: (c) 2006-2009 Andy Gill Homepage: http://ittc.ku.edu/~andygill/kure.php 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@@ -31,15 +27,5 @@ Language.KURE.Rewrite, Language.KURE.Combinators, Language.KURE.Term- Ghc-Options: -Wall------Executable test1--- Ghc-Options: --- Main-Is: Test.hs--- Hs-Source-Dirs: ., test--- buildable: True-
− test/Exp.hs
@@ -1,29 +0,0 @@-{-# 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
@@ -1,11 +0,0 @@-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
@@ -1,174 +0,0 @@-{-# 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)-