diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -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
diff --git a/Language/KURE/Combinators.hs b/Language/KURE/Combinators.hs
--- a/Language/KURE/Combinators.hs
+++ b/Language/KURE/Combinators.hs
@@ -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')
 
diff --git a/Language/KURE/Rewrite.hs b/Language/KURE/Rewrite.hs
--- a/Language/KURE/Rewrite.hs
+++ b/Language/KURE/Rewrite.hs
@@ -42,5 +42,5 @@
 	   => Rewrite m dec exp
 	   -> dec 
 	   -> exp 
-	   -> m (Either String (exp,dec))
+	   -> m (Either String (exp,dec,Int))
 runRewrite = runTranslate
diff --git a/Language/KURE/RewriteMonad.hs b/Language/KURE/RewriteMonad.hs
--- a/Language/KURE/RewriteMonad.hs
+++ b/Language/KURE/RewriteMonad.hs
@@ -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)
+
diff --git a/Language/KURE/Term.hs b/Language/KURE/Term.hs
--- a/Language/KURE/Term.hs
+++ b/Language/KURE/Term.hs
@@ -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))  
 
diff --git a/Language/KURE/Translate.hs b/Language/KURE/Translate.hs
--- a/Language/KURE/Translate.hs
+++ b/Language/KURE/Translate.hs
@@ -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)
-
 
diff --git a/kure.cabal b/kure.cabal
--- a/kure.cabal
+++ b/kure.cabal
@@ -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
-
 
diff --git a/test/Exp.hs b/test/Exp.hs
deleted file mode 100644
--- a/test/Exp.hs
+++ /dev/null
@@ -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
diff --git a/test/Id.hs b/test/Id.hs
deleted file mode 100644
--- a/test/Id.hs
+++ /dev/null
@@ -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
diff --git a/test/Test.hs b/test/Test.hs
deleted file mode 100644
--- a/test/Test.hs
+++ /dev/null
@@ -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)
-