RepLib 0.3 → 0.4.0

raw patch · 14 files changed

+9/−3621 lines, 14 filesdep −containersdep ~mtlPVP ok

version bump matches the API change (PVP)

Dependencies removed: containers

Dependency ranges changed: mtl

API changes (from Hackage documentation)

Files

• Generics/RepLib/Bind/LocallyNameless.hs +0/−1298
• Generics/RepLib/Bind/Nominal.hs +0/−1108
• Generics/RepLib/Bind/PermM.hs +0/−115
• README +1/−9
• RepLib.cabal +8/−12
• examples/Basic.hs +0/−185
• examples/LC-smallstep.hs +0/−102
• examples/LC.hs +0/−145
• examples/LF.hs +0/−71
• examples/Main.hs +0/−31
• examples/STLC.hs +0/−193
• examples/UnifyExp.hs +0/−161
• examples/abstract.hs +0/−178
• examples/issue15.hs +0/−13

@@ -1,1298 +0,0 @@-{-# LANGUAGE FlexibleInstances,
-             UndecidableInstances,
-             FlexibleContexts,
-             MultiParamTypeClasses,
-             TemplateHaskell,
-             TypeOperators,
-             ScopedTypeVariables,
-             TypeSynonymInstances,
-             RankNTypes,
-             GADTs,
-             EmptyDataDecls,
-             StandaloneDeriving
-  #-}
-{- LANGUAGE  KitchenSink -}
-
-{- Tricky things about the design.
-
-Equality for binders is defined in terms of aeq, *not* equality for
-the subcomponents. If you want to use a specialized form of equality
-for a particular type, (to ignore source locations for example) you
-need to edit match to take that into accont. Merely creating a special
-instance of Eq won't work!
-
-Single/multiple substitutions are *not* defined in terms of
-each other.
-
- -}
-
-----------------------------------------------------------------------
--- |
--- Module      :  Generics.RepLib.Bind.LocallyNameless
--- License     :  BSD-like (see LICENSE)
---
--- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>
--- Stability   :  experimental
--- Portability :  non-portable (-XKitchenSink)
---
--- A generic implementation of name binding functions using a locally
--- nameless representation.  Datatypes with binding can be defined
--- using the 'Name' and 'Bind' types.  Expressive patterns for binding
--- come from the 'Annot' and 'Rebind' types.
---
--- Important classes are:
---
---   * 'Alpha' -- the class of types and patterns that include binders,
---
---   * 'Subst' -- for subtitution functions.
---
--- Name generation is controlled via monads which implement the
--- 'Fresh' and 'LFresh' classes.
-----------------------------------------------------------------------
-
-module Generics.RepLib.Bind.LocallyNameless
-  ( -- * Basic types
-    Name, AnyName(..), Bind, Annot(..), Rebind,
-
-    -- ** Utilities
-    integer2Name, string2Name, makeName,
-    name2Integer, name2String, anyName2Integer, anyName2String,
-    name1,name2,name3,name4,name5,name6,name7,name8,name9,name10,
-
-    -- * The 'Alpha' class
-    Alpha(..),
-    swaps, swapsAnnots, swapsBinders,
-    match, matchAnnots, matchBinders,
-    fv, patfv, binders,
-    aeq, aeqBinders,
-
-    -- * Binding operations
-    bind, unsafeUnBind,
-
-    -- * The 'Fresh' class
-    Fresh(..), freshen,
-    unbind, unbind2, unbind3,
-
-    -- * The 'LFresh' class
-    HasNext(..), LFresh(..),
-    lfreshen,
-    lunbind, lunbind2, lunbind3,
-
-    -- * Rebinding operations
-    rebind, reopen,
-
-    -- * Substitution
-    Subst(..),
-
-    -- * For abstract types
-    abs_swaps,abs_fv,abs_freshen,abs_match,
-    abs_nthpatrec,abs_findpatrec,abs_close,abs_open,
-
-   -- * Advanced
-   AlphaCtx, matchR1,
-
-   -- * Pay no attention to the man behind the curtain
-   -- $paynoattention
-   rName, rBind, rRebind, rAnnot
-) where
-
-import Generics.RepLib
-import Generics.RepLib.Bind.PermM
-
-import qualified Data.List as List
-import qualified Data.Char as Char
-import Data.Maybe
-import Data.Set (Set)
-import qualified Data.Set as S
-import qualified Text.Read as R
-import Prelude hiding (or)
-import Data.Monoid
-import Control.Monad.Reader (Reader,ask,local,runReader)
-import System.IO.Unsafe (unsafePerformIO)
-
-
-------------------------------------------------------------
--- Basic types
-------------------------------------------------------------
-
-$(derive_abstract [''R])
--- The above only works with GHC 7.
-
-
--- | 'Name's are things that get bound.  This type is intentionally
---   abstract; to create a 'Name' you can use 'string2Name' or
---   'integer2Name'. The type parameter is a tag, or /sort/, which tells
---   us what sorts of things this name may stand for. The sort must
---   be an instance of the 'Rep' type class.
-data Name a
-  = Nm (R a) (String, Integer)   -- free names
-  | Bn (R a) Integer Integer     -- bound names / binding level + pattern index
-   deriving (Eq, Ord)
-
--- | A name with a hidden (existentially quantified) sort.
-data AnyName = forall a. Rep a => AnyName (Name a)
-
-
-
--- | The type of a binding.  We can 'Bind' an @a@ object in a @b@
---   object if we can create \"fresh\" @a@ objects, and @a@ objects
---   can occur unbound in @b@ objects. Often @a@ is 'Name' but that
---   need not be the case.
---
---   Like 'Name', 'Bind' is also abstract. You can create bindings
---   using 'bind' and take them apart with 'unbind' and friends.
-data Bind a b = B a b
-
--- Set bindings.  TODO: implement.
-data SBind a b = SB a b
-
--- | An annotation is a \"hole\" in a pattern where variables can be
---   used, but not bound. For example, patterns may include type
---   annotations, and those annotations can reference variables
---   without binding them.  Annotations do nothing special when they
---   appear elsewhere in terms.
-newtype Annot a = Annot a deriving (Show, Read, Eq)
-
--- | 'Rebind' supports \"telescopes\" --- that is, patterns where
---   bound variables appear in multiple subterms.
-data Rebind a b = R a b
-
-$(derive [''Bind, ''Name, ''Annot, ''Rebind])
-
--- AnyName has an existential in it, so we cannot create a complete
--- representation for it, unfortunately.
-
-$(derive_abstract [''AnyName])
-
-instance Show AnyName where
-  show (AnyName n1) = show n1
-
-instance Eq AnyName where
-   (AnyName n1) == (AnyName n2) =
-      case gcastR (getR n1) (getR n2) n1 of
-           Just n1' -> n1' == n2
-           Nothing  -> False
-
-instance Ord AnyName where
-   compare (AnyName n1) (AnyName n2) =
-       case compareR (getR n1) (getR n2) of
-         EQ  -> case gcastR (getR n1) (getR n2) n1 of
-           Just n1' -> compare n1' n2
-           Nothing  -> error "Panic: equal types are not equal in Ord AnyName instance!"
-         ord -> ord
-
-------------------------------------------------------------
--- Utilities
-------------------------------------------------------------
-
--- some convenient names for testing
-name1, name2, name3, name4, name5, name6, name7, name8, name9, name10, name11
-  :: Rep a => Name a
-name1 = integer2Name 1
-name2 = integer2Name 2
-name3 = integer2Name 3
-name4 = integer2Name 4
-name5 = integer2Name 5
-name6 = integer2Name 6
-name7 = integer2Name 7
-name8 = integer2Name 8
-name9 = integer2Name 9
-name10 = integer2Name 10
-name11 = integer2Name 11
-
---instance Read Name where
---  read s = error "FIXME"
-
-instance Show (Name a) where
-  show (Nm _ ("",n)) = "_" ++ (show n)
-  show (Nm _ (x,0))  = x
-  show (Nm _ (x,n))  = x ++ (show n)
-  show (Bn _ x y)    =  show x ++ "@" ++ show y
-
--- | Get the integer index of a 'Name'.
-name2Integer :: Name a -> Integer
-name2Integer (Nm _ (_,x)) = x
-name2Integer (Bn _ _ _)   = error "Internal Error: cannot call name2Integer for bound names"
-
--- | Get the string part of a 'Name'.
-name2String :: Name a -> String
-name2String (Nm _ (s,_)) = s
-name2String (Bn _ _ _)   = error "Internal Error: cannot call name2Integer for bound names"
-
--- | Get the integer index of an 'AnyName'.
-anyName2Integer :: AnyName -> Integer
-anyName2Integer (AnyName nm) = name2Integer nm
-
--- | Get the string part of an 'AnyName'.
-anyName2String :: AnyName -> String
-anyName2String (AnyName nm) = name2String nm
-
-toSortedName :: Rep a => AnyName -> Maybe (Name a)
-toSortedName (AnyName n) = gcastR (getR n) rep n
-
--- | Create a 'Name' from an 'Integer'.
-integer2Name :: Rep a => Integer -> Name a
-integer2Name n = makeName "" n
-
--- | Create a 'Name' from a 'String'.
-string2Name :: Rep a => String -> Name a
-string2Name s = makeName s 0
-
--- | Create a 'Name' from a @String@ and an @Integer@ index.
-makeName :: Rep a => String -> Integer -> Name a
-makeName s i = Nm rep (s,i)
-
--- | Determine the sort of a 'Name'.
-getR :: Name a -> R a
-getR (Nm r _)   = r
-getR (Bn r _ _) = r
-
-------------------------------------------------------------
--- The Alpha class
-------------------------------------------------------------
-
--- | The 'Alpha' type class is for types which may contain names.  The
---   'Rep1' constraint means that we can only make instances of this
---   class for types that have generic representations (which can be
---   automatically derived by RepLib.)
---
---   Note that the methods of 'Alpha' should never be called directly!
---   Instead, use other methods provided by this module which are
---   defined in terms of 'Alpha' methods. (The only reason they are
---   exported is to make them available to automatically-generated
---   code.)
---
---   Most of the time, the default definitions of these methods will
---   suffice, so you can make an instance for your data type by simply
---   declaring
---
---   > instance Alpha MyType
---
-class (Show a, Rep1 AlphaD a) => Alpha a where
-
-  -- | See 'swaps'.
-  swaps' :: AlphaCtx -> Perm AnyName -> a -> a
-  swaps' = swapsR1 rep1
-
-  -- | See 'fv'.
-  fv' :: AlphaCtx -> a -> Set AnyName
-  fv' = fvR1 rep1
-
-  -- | See 'lfreshen'.
-  lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
-  lfreshen' = lfreshenR1 rep1
-
-  -- | See 'freshen'.
-  freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
-  freshen' = freshenR1 rep1
-
-{-
-  -- | See 'match'.
-   compare'   :: Ord a => AlphaCtx -> a -> a -> POrdering
-   compare'   = compareR1 rep1
--}
-
-  match'   :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)
-  match'   = matchR1 rep1
-
-  -- | Replace free names by bound names.
-  close :: Alpha b => AlphaCtx -> b -> a -> a
-  close = closeR1 rep1
-
-  -- | Replace bound names by free names.
-  open :: Alpha b => AlphaCtx -> b -> a -> a
-  open = openR1 rep1
-
-  ---------------- PATTERN OPERATIONS ----------------------------
-
-  -- | @'nthpatrec' b n@ looks up the @n@th name in the pattern @b@
-  -- (zero-indexed), returning the number of names encountered if not
-  -- found.
-  nthpatrec :: a -> Integer -> (Integer, Maybe AnyName)
-  nthpatrec = nthpatR1 rep1
-
-  -- | Find the (first) index of the name in the pattern if it exists;
-  --   if not found ('Bool' = 'False'), return the number of names
-  --   encountered instead.
-  findpatrec :: a -> AnyName -> (Integer, Bool)
-  findpatrec = findpatR1 rep1
-
--- | Match returns a "permutation ordering". Either the terms are known 
--- to be LT or GT, or there is some permutation that can make them equal
--- to eachother
--- data POrdering = PLT | PEq (Perm AnyName) | PGT
-
-
--- | Many of the operations in the 'Alpha' class take an 'AlphaCtx':
--- stored information about the iteration as it progresses. This type
--- is abstract, as classes that override these operations should just pass
--- the context on.
-data AlphaCtx = AC { mode :: Mode , level :: Integer }
-
-initial :: AlphaCtx
-initial = AC Term 0
-
-incr :: AlphaCtx -> AlphaCtx
-incr c = c { level = level c + 1 }
-
-pat  :: AlphaCtx -> AlphaCtx
-pat c  = c { mode = Pat }
-
-term  :: AlphaCtx -> AlphaCtx
-term c  = c { mode = Term }
-
--- | A mode is basically a flag that tells us whether we should be
---   looking at the names in the term, or if we are in a pattern and
---   should /only/ be looking at the names in the annotations. The
---   standard mode is to use 'Term'; the function 'fv', 'swaps',
---   'lfreshen', 'freshen' and 'match' do this by default.
-data Mode = Term | Pat deriving (Show, Eq, Read)
-
--- | Class constraint hackery to allow us to override the default
---   definitions for certain classes.  'AlphaD' is essentially a
---   reified dictionary for the 'Alpha' class.
-data AlphaD a = AlphaD {
-  swapsD    :: AlphaCtx -> Perm AnyName -> a -> a,
-  fvD       :: AlphaCtx -> a -> Set AnyName,
-  freshenD  :: forall m. Fresh m => AlphaCtx -> a -> m (a, Perm AnyName),
-  lfreshenD :: forall b m. LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b,
-  matchD    :: AlphaCtx -> a -> a -> Maybe (Perm AnyName),
---  compareD  :: Ord a => AlphaCtx -> a -> a -> POrdering,
-  closeD    :: Alpha b => AlphaCtx -> b -> a -> a,
-  openD     :: Alpha b => AlphaCtx -> b -> a -> a,
-  findpatD  :: a -> AnyName -> (Integer, Bool),
-  nthpatD   :: a -> Integer -> (Integer, Maybe AnyName)
-  }
-
-instance Alpha a => Sat (AlphaD a) where
-  dict = AlphaD swaps' fv' freshen' lfreshen' match'
-           close open findpatrec nthpatrec
-
-----------------------------------------------------------------------
--- Generic definitions for 'Alpha' methods.  (Note that all functions
--- that take representations end in 'R1'.)
-----------------------------------------------------------------------
-
-closeR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a
-closeR1 (Data1 _ cons) = \i a d ->
-   case (findCon cons d) of
-      Val c rec kids ->
-        to c (map_l (\z -> closeD z i a) rec kids)
-closeR1 _               = \_ _ d -> d
-
-
-openR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a
-openR1 (Data1 _ cons) = \i a d ->
-   case (findCon cons d) of
-      Val c rec kids ->
-        to c (map_l (\z -> openD z i a) rec kids)
-openR1 _               = \_ _ d -> d
-
-
-
-swapsR1 :: R1 AlphaD a -> AlphaCtx -> Perm AnyName -> a -> a
-swapsR1 (Data1 _ cons)  = \ p x d ->
-  case (findCon cons d) of
-    Val c rec kids -> to c (map_l (\z -> swapsD z p x) rec kids)
-swapsR1 _               = \ _ _ d -> d
-
-
-fvR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> Set AnyName
-fvR1 (Data1 _ cons) = \ p  d ->
-  case (findCon cons d) of
-    Val _ rec kids -> fv1 rec p kids
-fvR1 _ = \ _ _ -> S.empty
-
-fv1 :: MTup (AlphaD) l -> AlphaCtx -> l -> Set AnyName
-fv1 MNil _ Nil = S.empty
-fv1 (r :+: rs) p (p1 :*: t1) =
-   fvD r p p1 `S.union` fv1 rs p t1
-
--- Generic definition of freshen and match
-{-
-toPOrdering :: Ordering -> POrdering 
-toPOrdering LT = PLT
-toPOrdering GT = PGT
-toPOrdering EQ = PEQ empty
-
-compareR1 :: Ord a => R1 (AlphaD) a -> AlphaCtx -> a -> a -> POrdering 
-compareR1 (Data1 _ cons) = loop cons where
-  loop (Con emb reps : rest) p x y =
-    case (from emb x, from emb y) of
-      (Just p1, Just p2) -> compare1 reps p p1 p2
-      (Nothing, Nothing) -> loop rest p x y
-      (Just p1, Nothing) -> PLT
-      (Nothing, Just p1) -> PGT
-  loop [] _ _ _ = error "Impossible"
-compareR1 _ = \ _ x y     -> toPOrdering (compare x y)
-
-compare1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> POrdering (Perm AnyName)
-compare1 MNil _ Nil Nil = PEQ empty
-compare1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) = 
-  case compareD r c p1 p2 of 
-    PEQ l1 -> case compare1 rs c t1 t2 of 
-                  PEQ l2 -> (l1 `join` l2)
-                  otherwise -> otherwise
-    otherwise -> otherwise
--}
-
-
-matchR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)
-matchR1 (Data1 _ cons) = loop cons where
-   loop (Con emb reps : rest) p x y =
-     case (from emb x, from emb y) of
-      (Just p1, Just p2) -> match1 reps p p1 p2
-      (Nothing, Nothing) -> loop rest p x y
-      (_,_)              -> Nothing
-   loop [] _ _ _ = error "Impossible"
-matchR1 Int1 = \ _ x y -> if x == y then Just empty else Nothing
-matchR1 Integer1 = \ _ x y -> if x == y then Just empty else Nothing
-matchR1 Char1 = \ _ x y -> if x == y then Just empty else Nothing
-matchR1 _ = \ _ _ _ -> Nothing
- 
-match1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Maybe (Perm AnyName)
-match1 MNil _ Nil Nil = Just empty
-match1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) = do
-  l1 <- matchD r c p1 p2
-  l2 <- match1 rs c t1 t2
-  (l1 `join` l2)
-
-
-
-
-freshenR1 :: Fresh m => R1 (AlphaD) a -> AlphaCtx -> a -> m (a,Perm AnyName)
-freshenR1 (Data1 _ cons) = \ p d ->
-   case findCon cons d of
-     Val c rec kids -> do
-       (l, p') <- freshenL rec p kids
-       return (to c l, p')
-freshenR1 _ = \ _ n -> return (n, empty)
-
-freshenL :: Fresh m => MTup (AlphaD) l -> AlphaCtx -> l -> m (l, Perm AnyName)
-freshenL MNil _ Nil = return (Nil, empty)
-freshenL (r :+: rs) p (t :*: ts) = do
-  (xs, p2) <- freshenL rs p ts
-  (x, p1) <- freshenD r p (swapsD r p p2 t)
-  return ( x :*: xs, p1 <> p2)
-
-lfreshenR1 :: LFresh m => R1 AlphaD a -> AlphaCtx -> a ->
-              (a -> Perm AnyName -> m b) -> m b
-lfreshenR1 (Data1 _ cons) = \p d f ->
-   case findCon cons d of
-     Val c rec kids -> lfreshenL rec p kids (\ l p' -> f (to c l) p')
-lfreshenR1 _ = \ _ n f -> f n empty
-
-lfreshenL :: LFresh m => MTup (AlphaD) l -> AlphaCtx -> l ->
-              (l -> Perm AnyName -> m b) -> m b
-lfreshenL MNil _ Nil f = f Nil empty
-lfreshenL (r :+: rs) p (t :*: ts) f =
-  lfreshenL rs p ts ( \ y p2 ->
-  lfreshenD r p (swapsD r p p2 t) ( \ x p1 ->
-     f (x :*: y) (p1 <> p2)))
-
-
--- returns either (# of names in b, false) or (index, true)
-findpatR1 :: R1 AlphaD b -> b -> AnyName -> (Integer, Bool)
-findpatR1 (Data1 dt cons) = \ d n ->
-   case findCon cons d of
-     Val c rec kids -> findpatL rec kids n
-findpatR1 _ = \ x n -> (0, False)
-
-findpatL :: MTup AlphaD l -> l -> AnyName -> (Integer, Bool)
-findpatL MNil Nil n = (0, False)
-findpatL (r :+: rs) (t :*: ts) n =
-  case findpatD r t n of
-    s@(i, True) -> s
-    (i, False) -> case findpatL rs ts n of
-                    (j, b) -> (i+j, b)
-
-nthpatR1 :: R1 AlphaD b -> b -> Integer -> (Integer, Maybe AnyName)
-nthpatR1 (Data1 dt cons) = \ d n ->
-   case findCon cons d of
-     Val c rec kids -> nthpatL rec kids n
-nthpatR1 _ = \ x n -> (n, Nothing)
-
-nthpatL :: MTup AlphaD l -> l -> Integer -> (Integer, Maybe AnyName)
-nthpatL MNil Nil i = (i, Nothing)
-nthpatL (r :+: rs) (t :*: ts) i =
-  case nthpatD r t i of
-    s@(_, Just n) -> s
-    (j, Nothing) -> nthpatL rs ts j
-
-------------------------------------------------------------
--- Specific Alpha instances
------------------------------------------------------------
-
-instance Rep a => Alpha (Name a) where
-  fv' c n@(Nm _ _)  | mode c == Term = S.singleton (AnyName n)
-  fv' c (Bn _ _ _)  | mode c == Term = S.empty
-  fv' c n           | mode c == Pat  = S.empty
-
-  swaps' c p x = case mode c of
-                   Term ->
-                     case apply p (AnyName x) of
-                       AnyName y ->
-                         case gcastR (getR y) (getR x) y of
-                           Just y' -> y'
-                           Nothing -> error "Internal error in swaps': sort mismatch"
-                   Pat  -> x
-
-  match' _ x  y   | x == y         = Just empty
-  match' c n1 n2  | mode c == Term = Just $ single (AnyName n1) (AnyName n2)
-  match' c _ _    | mode c == Pat  = Just empty
-
-{-
-  compare' _ x  y   | x == y         = PEQ empty
-  compare' c n1 n2  | mode c == Term = PEQ $ single (AnyName n1) (AnyName n2)
-  compare' c _ _    | mode c == Pat  = PEQ empty
--}
-
-  freshen' c nm = case mode c of
-     Term -> do x <- fresh nm
-                return (x, single (AnyName nm) (AnyName x))
-     Pat  -> return (nm, empty)
-
-  --lfreshen' :: LFresh m => Pat a -> (a -> Perm Name -> m b) -> m b
-  lfreshen' c nm f = case mode c of
-     Term -> do x <- lfresh nm
-                avoid [AnyName x] $ f x (single (AnyName nm) (AnyName x))
-     Pat  -> f nm empty
-
-  open c a (Bn r j x) | level c == j =
-    case nthpat a x of
-      AnyName nm -> case gcastR (getR nm) r nm of
-        Just nm' -> nm'
-        Nothing  -> error "Internal error in open: sort mismatch"
-  open _ _ n = n
-
-  close c a nm@(Nm r n)
-    | mode c == Term =
-      case findpat a (AnyName nm) of
-        Just x  -> Bn r (level c) x
-        Nothing -> nm
-
-  close _ _ n = n
-
-  findpatrec nm1 (AnyName nm2) =
-    case gcastR (getR nm1) (getR nm2) nm1 of
-      Just nm1' -> if nm1' == nm2 then (0, True) else (1, False)
-      Nothing -> (1, False)
-
-  nthpatrec nm 0 = (0, Just (AnyName nm))
-  nthpatrec nm i = (i - 1, Nothing)
-
-instance Alpha AnyName  where
-  fv' c n@(AnyName (Nm _ _))  | mode c == Term = S.singleton n
-  fv' c (AnyName (Bn _ _ _))  | mode c == Term = S.empty
-  fv' c n                     | mode c == Pat  = S.empty
-
-  swaps' c p x = case mode c of
-                   Term -> apply p x
-                   Pat  -> x
-
-  match' _ x y | x == y          = Just empty
-  match' c (AnyName n1) (AnyName n2)
-    | mode c == Term =
-      case gcastR (getR n1) (getR n2) n1 of
-        Just n1' -> Just $ single (AnyName n1) (AnyName n2)
-        Nothing  -> Nothing
-  match' c _ _           | mode c == Pat   = Just empty
-
-{-
-  compare' _ x y | x == y          = PEQ empty
-  compare' c (AnyName n1) (AnyName n2)
-    | mode c == Term =
-      case compareR (getR n1) (getR n2) of 
-       EQ ->  case gcastR (getR n1) (getR n2) n1 of
-          Just n1' -> PEQ $ single (AnyName n1) (AnyName n2)
-          Nothing  -> error "impossible"
-       otherwise -> otherwise
-  compare' c _ _           | mode c == Pat   = PEQ empty
--}
-
-
-  freshen' c (AnyName nm) = case mode c of
-     Term -> do x <- fresh nm
-                return (AnyName x, single (AnyName nm) (AnyName x))
-     Pat  -> return (AnyName nm, empty)
-
-  --lfreshen' :: LFresh m => Pat a -> (a -> Perm Name -> m b) -> m b
-  lfreshen' c (AnyName nm) f = case mode c of
-     Term -> do x <- lfresh nm
-                avoid [AnyName x] $ f (AnyName x) (single (AnyName nm) (AnyName x))
-     Pat  -> f (AnyName nm) empty
-
-  open c a (AnyName (Bn _ j x)) | level c == j = nthpat a x
-  open _ _ n = n
-
-  close c a nm@(AnyName (Nm r n)) =
-    case findpat a nm of
-      Just x  -> AnyName (Bn r (level c) x)
-      Nothing -> nm
-
-  close _ _ n = n
-
-  findpatrec nm1 nm2 | nm1 == nm2 = ( 0 , True )
-  findpatrec _ _ = (1, False)
-
-  nthpatrec nm 0 = (0, Just nm)
-  nthpatrec nm i = (i - 1, Nothing)
-
-{-
-instance (Alpha a, Alpha b) => Alpha (SBind a b) where
-    open i a (SB x y)    = SB (open i a x)  (open (incr i) a y)
-    close i a (SB x y)   = SB (close i a x) (close (incr i) a y)
-
-    swaps' p pm (SB x y) =
-        (SB (swaps' (pat p) pm x) (swaps' (incr p) pm y))
-
-    fv' p (SB x y) = fv' (pat p) x ++ fv' p y
-
-    freshen' p (SB x y) = do
-      (x', pm1) <- freshen' (pat p) x
-      (y', pm2) <- freshen' (incr p) (swaps' (incr p) pm1 y)
-      return (SB x' y', pm1 <> pm2)
-
-    lfreshen' p (SB x y) f =
-      avoid (fv' p x) $
-        lfreshen' (pat p) x (\ x' pm1 ->
-        lfreshen' (incr p)   (swaps' (incr p) pm1 y) (\ y' pm2 ->
-        f (SB x' y') (pm1 <> pm2)))
-
-    -- determine a permutation of free variables
-    -- such that p (SB x1 y1) `aeq` SB x2 y2
-    -- this is fairly inefficient with the locally
-    -- nameless representation (unless we can match bound names too)
-    -- but to do that, we need to pass the binding level as
-    -- an argument to match'
-    match' p (SB x1 y1) (SB x2 y2) = do
-      px <- match' (pat p) x1 x2
-      py <- match' (incr p) (swaps' (incr p) px y1) (swaps' (incr p) px y2)
-      return (px <> py)
--}
-
-instance (Alpha a, Alpha b) => Alpha (Bind a b) where
-    swaps' c pm (B x y) =
-        (B (swaps' (pat c) pm x)
-           (swaps' (incr c) pm y))
-
-    fv' c (B x y) = fv' (pat c) x `S.union` fv' (incr c) y
-
-    freshen' c (B x y) = do
-      (x', pm1) <- freshen' (pat c) x
-      (y', pm2) <- freshen' (incr c) (swaps' (incr c) pm1 y)
-      return (B x' y', pm1 <> pm2)
-
-    lfreshen' c (B x y) f =
---      avoid (S.elems $ fv' c x) $ -- I don't think we need this
-        lfreshen' (pat c) x (\ x' pm1 ->
-        lfreshen' (incr c) (swaps' (incr c) pm1 y) (\ y' pm2 ->
-        f (B x' y') (pm1 <> pm2)))
-
-    match' c (B x1 y1) (B x2 y2) = do
-      px <- match' (pat c) x1 x2
-      --- check this!
-      py <- match' (incr c) y1 y2
-      -- need to make sure that all permutations of
-      -- bound variables at this
-      -- level are the identity
-      (px `join` py)
-{-
-    compare' c (B x1 y1) (B x2 y2) = 
-      case compare' (pat c) x1 x2 of 
-        PEQ px -> case compare' (incr c) y1 y2 of
-           PEQ py -> PEQ (px `join` py)
-           otherwise -> otherwise
-        otherwise -> otherwise
--}
-
-    open  c a (B x y)    = B (open (pat c) a x)  (open  (incr c) a y)
-    close c a (B x y)    = B (close (pat c) a x) (close (incr c) a y)
-
-instance (Alpha a, Alpha b) => Alpha (Rebind a b) where
-
-  swaps' p pm (R x y) = R (swaps' p pm x) (swaps' (incr p) pm y)
-
-  fv' p (R x y) =  fv' p x `S.union` fv' (incr p) y
-
-  lfreshen' p (R x y) g =
-    lfreshen' p x $ \ x' pm1 ->
-      lfreshen' (incr p) (swaps' (incr p) pm1 y) $ \ y' pm2 ->
-        g (R x' y') (pm1 <> pm2)
-
-  freshen' p (R x y) = do
-      (x', pm1) <- freshen' p x
-      (y', pm2) <- freshen' (incr p) (swaps' (incr p) pm1 y)
-      return (R x' y', pm1 <> pm2)
-
-  match' p (R x1 y1) (R x2 y2) = do
-     px <- match' p x1 x2
-     py <- match' (incr p)  y1 y2
-     (px `join` py)
-
-  open c a (R x y)  = R (open c a x) (open (incr c) a y)
-  close c a (R x y) = R (close c a x) (close (incr c) a y)
-
-  findpatrec (R x y) nm =
-     case findpatrec x nm of
-         (i, True) -> (i, True)
-         (i, False) -> case findpatrec y nm of
-                         (j, True) -> (i + j, True)
-                         (j, False) -> (i+j, False)
-
-  nthpatrec (R x y) i =
-      case nthpatrec x i of
-        (j , Just n) -> (j, Just n)
-        (j , Nothing) -> nthpatrec y j
-
-
-instance Alpha a => Alpha (Annot a) where
-   swaps' c pm (Annot t) | mode c == Pat  = Annot (swaps' (term c) pm t)
-   swaps' c pm (Annot t) | mode c == Term = Annot t
-
-   fv' c (Annot t) | mode c == Pat  = fv' (term c) t
-   fv' c _         | mode c == Term = S.empty
-
-   freshen' c (Annot t) | mode c == Pat = do
-       (t', p) <- freshen' (term c) t
-       return (Annot t', p)
-   freshen' c a | mode c == Term = return (a, empty)
-
----   lfreshen' c (Annot t) | mode c == Pat
-
-
-   match' c (Annot x) (Annot y) | mode c == Pat  = match' (term c) x y
-   match' c (Annot x) (Annot y) | mode c == Term = if x `aeq` y
-                                    then Just empty
-                                    else Nothing
-   findpatrec _ _ = (0, False)
-   nthpatrec nm i = (i, Nothing)
-
--- Instances for other types use the default definitions.
-instance Alpha Bool where
-instance Alpha Float where
-instance Alpha () where
-instance Alpha a => Alpha [a] where
-instance Alpha Int where
-instance Alpha Integer where
-instance Alpha Double where
-instance Alpha Char where
-instance Alpha a => Alpha (Maybe a) where
-instance (Alpha a,Alpha b) => Alpha (Either a b) where
-instance (Alpha a,Alpha b) => Alpha (a,b) where
-instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c) where
-instance (Alpha a, Alpha b,Alpha c, Alpha d) => Alpha (a,b,c,d)
-instance (Alpha a, Alpha b,Alpha c, Alpha d, Alpha e) =>
-   Alpha (a,b,c,d,e)
-
-
-instance (Rep a) => Alpha (R a) where
-{- we don't need these any more because of derive_abstract. The default definitions
-   work just fine now. -}
-{-
-  swaps'      = abs_swaps
-  fv'         = abs_fv
-  freshen'    = abs_freshen
-  match'      = abs_match
-  nthpatrec  = abs_nthpatrec
-  findpatrec = abs_findpatrec
-  close      = abs_close
-  open       = abs_open
--}
-
--- Definitions of the class members for abstract types.
--- These will go away soon.
-abs_swaps _ p s = s
-abs_fv _ s = S.empty
-abs_freshen _ b = return (b, empty)
-abs_match _ x1 x2 = if x1 == x2 then Just empty else Nothing
-abs_nthpatrec b i = (i, Nothing)
-abs_findpatrec b n = (0, False)
-abs_close i b x = x
-abs_open i b x = x
-
-
-----------------------------------------------------------
--- Binding operations & instances
-----------------------------------------------------------
--- | A smart constructor for binders, also sometimes known as
--- \"close\".
-bind ::(Alpha b, Alpha c) => b -> c -> Bind b c
-bind b c = B b (close initial b c)
-
--- | A destructor for binders that does /not/ guarantee fresh
---   names for the binders.
-unsafeUnBind :: (Alpha a, Alpha b) => Bind a b -> (a,b)
-unsafeUnBind (B a b) = (a, open initial a b)
-
--- | The 'Eq' instance for 'Bind' compares bindings for
--- alpha-equality.
-
---- SCW: REMOVE THIS INSTANCE
-{-
-instance (Alpha a, Alpha b, Eq b) => Eq (Bind a b) where
-   b1 == b2 = b1 `aeq` b2
--}
--- fixme: in the 'otherwise' case the comparison is not alpha-respecting,
--- e.g.
---   compare (bind [name1] name1) (bind [name1,name1] name1) == LT
---   compare (bind [name3] name3) (bind [name1,name1] name1) == GT
-
---- SCW: REMOVE THIS INSTANCE
-{-
-instance (Alpha a, Alpha b, Ord a, Ord b) => Ord (Bind a b) where
-   compare (B a1 b1) (B a2 b2) =
-       case (match a1 a2) of
-         Just p  -> case compare a1 (swaps p a2) of
-                      EQ -> compare b1 b2
-                      otherwise -> otherwise
-         Nothing -> compare a1 a2
--}
-
-instance (Alpha a, Alpha b, Read a, Read b) => Read (Bind a b) where
-         readPrec = R.parens $ (R.prec app_prec $ do
-                                  R.Ident "<" <- R.lexP
-                                  m1 <- R.step R.readPrec
-                                  R.Ident ">" <- R.lexP
-                                  m2 <- R.step R.readPrec
-                                  return (bind m1 m2))
-           where app_prec = 10
-
-         readListPrec = R.readListPrecDefault
-
-instance (Show a, Show b) => Show (Bind a b) where
-  showsPrec p (B a b) = showParen (p>0)
-      (showString "<" . showsPrec p a . showString "> " . showsPrec 0 b)
-
-----------------------------------------------------------
--- Rebinding operations 
-----------------------------------------------------------
-
--- | Constructor for binding in patterns.
-rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b
-rebind a b = R a (close initial a b)
-
--- | Compare for alpha-equality.
-instance (Alpha a, Alpha b, Eq b) => Eq (Rebind a b) where
-   b1 == b2 = b1 `aeqBinders` b2
-
-instance (Show a, Show b) => Show (Rebind a b) where
-  showsPrec p (R a b) = showParen (p>0)
-      (showString "<<" . showsPrec p a . showString ">> " . showsPrec 0 b)
-
--- | destructor for binding patterns, the names should have already
--- been freshened.
-reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b)
-reopen (R a b) = (a, open initial a b)
-
-----------------------------------------------------------
--- Wrappers for operations in the Alpha class
-----------------------------------------------------------
--- | Determine alpha-equivalence.
-aeq :: Alpha a => a -> a -> Bool
-aeq t1 t2 = case match t1 t2 of
-              Just p -> isid p
-              _      -> False
-
--- | Determine (alpha-)equivalence of patterns
-aeqBinders :: Alpha a => a -> a -> Bool
-aeqBinders t1 t2 = case matchBinders t1 t2 of
-              Just p -> isid p
-              _      -> False
-
--- | Calculate the free variables of a particular sort contained in a term.
-fv :: (Rep b, Alpha a) => a -> Set (Name b)
-fv = S.map fromJust . S.filter isJust . S.map toSortedName . fv' initial
-
--- | List all the binding variables (of a particular sort) in a pattern.
-binders :: (Rep a, Alpha b) => b -> Set (Name a)
-binders = fv
-
--- | List variables of a particular sort that occur freely in
---   annotations (not bindings).
-patfv :: (Rep a, Alpha b) => b -> Set (Name a)
-patfv = S.map fromJust . S.filter isJust . S.map toSortedName . fv' (pat initial)
-
-
--- | Apply a permutation to a term.
-swaps :: Alpha a => Perm AnyName -> a -> a
-swaps = swaps' initial
-
--- | Apply a permutation to the binding variables in a pattern. 
--- Annotations are left alone by the permutation.
-swapsBinders :: Alpha a => Perm AnyName -> a -> a
-swapsBinders = swaps' initial
-
--- | Apply a permutation to the annotations in a pattern. Binding
--- names are left alone by the permutation.
-swapsAnnots :: Alpha a => Perm AnyName -> a -> a
-swapsAnnots = swaps' (pat initial)
-
-
--- | \"Locally\" freshen a term.  TODO: explain this type signature a bit better.
-lfreshen :: (Alpha a, LFresh m) => a -> (a -> Perm AnyName -> m b) -> m b
-lfreshen = lfreshen' initial
-
--- | Freshen a term by replacing all old /binding/ 'Name's with new
--- fresh 'Name's, returning a new term and a @'Perm' 'Name'@
--- specifying how 'Name's were replaced.
-freshen :: (Fresh m, Alpha a) => a -> m (a, Perm AnyName)
-freshen = freshen' initial
-
--- | Compare two data structures and produce a permutation of their
--- 'Name's that will make them alpha-equivalent to each other ('Name's
--- that appear in annotations must match exactly).  Return 'Nothing'
--- if no such renaming is possible.  Note that two terms are
--- alpha-equivalent if the empty permutation is returned.
-match   :: Alpha a => a -> a -> Maybe (Perm AnyName)
-match   = match' initial
-
--- | Compare two patterns, ignoring the names of binders, and produce
--- a permutation of their annotations to make them alpha-equivalent 
--- to eachother. Return 'Nothing' if no such renaming is possible.
-matchAnnots :: Alpha a => a -> a -> Maybe (Perm AnyName)
-matchAnnots = match' (pat initial)
-
--- | Compare two patterns for equality and produce a permutation of
--- their binding 'Names' to make them alpha-equivalent to each other
--- ('Name's that appear in annotations must match exactly). Return
--- 'Nothing' if no such renaming is possible.  
-matchBinders ::  Alpha a => a -> a -> Maybe (Perm AnyName)
-matchBinders = match' initial
-
-
--- | @'nthpat' b n@ looks up up the @n@th name in the pattern @b@
--- (zero-indexed).  PRECONDITION: the number of names in the pattern
--- must be at least @n@.
-nthpat :: Alpha a => a -> Integer -> AnyName
-nthpat x i = case nthpatrec x i of
-                 (j, Nothing) -> error
-                   ("BUG: pattern index " ++ show i ++ " out of bounds by " ++ show j ++ "in" ++ show x)
-                 (_, Just n)  -> n
-
--- | Find the (first) index of the name in the pattern, if it exists.
-findpat :: Alpha a => a -> AnyName -> Maybe Integer
-findpat x n = case findpatrec x n of
-                   (i, True) -> Just i
-                   (_, False) -> Nothing
-
-------------------------------------------------------------
--- Freshening
-------------------------------------------------------------
-
--- | Type class for contexts which can generate new globally fresh
--- integers.
-class HasNext m where
-  -- | Get a new, globally fresh 'Integer'.
-  nextInteger :: m Integer
-
-  -- | Reset the internal state, i.e. forget about 'Integers' that
-  -- have already been generated.
-  resetNext   :: Integer -> m ()
-
--- | Type class for monads which can generate new globally unique
--- 'Name's based on a given 'Name'.
-class Monad m => Fresh m where
-  fresh :: Name a -> m (Name a)
-
--- | A monad @m@ supports the 'fresh' operation if it
--- can generate a new unique names.
-instance (Monad m, HasNext m) => Fresh m where
-  fresh (Nm r (s,j)) = do { n <- nextInteger; return (Nm r (s,n)) }
-  fresh (Bn _ _ _)   = error "BUG: cannot freshen bound vars"
-
-
--- | Unbind (also known as \"open\") is the destructor for
--- bindings. It ensures that the names in the binding are fresh.
-unbind  :: (Fresh m, Alpha b, Alpha c) => Bind b c -> m (b,c)
-unbind (B b c) = do
-      (b', _) <- freshen b
-      return (b', open initial b' c)
-
--- | Unbind two terms with the same fresh names, provided the
--- binders match.
-unbind2  :: (Fresh m, Alpha b, Alpha c, Alpha d) =>
-            Bind b c -> Bind b d -> m (Maybe (b,c,d))
-unbind2 (B b1 c) (B b2 d) = do
-      case match b1 b2 of
-         Just _ -> do
-           (b', _) <- freshen b1
-           return $ Just (b', open initial b' c, open initial b' d)
-         Nothing -> return Nothing
-
-unbind3  :: (Fresh m, Alpha b, Alpha c, Alpha d, Alpha e) =>
-            Bind b c -> Bind b d -> Bind b e ->  m (Maybe (b,c,d,e))
-unbind3 (B b1 c) (B b2 d) (B b3 e) = do
-      case (match b1 b2, match b1 b3) of
-         (Just _, Just _) -> do
-           (b', _) <- freshen b1
-           return $ Just (b', open initial b' c, open initial b' d, open initial b' e)
-         _ -> return Nothing
-
----------------------------------------------------
--- LFresh
-
--- | This is the class of monads that support freshness in an
--- (implicit) local scope.  Generated names are fresh for the current
--- local scope, but not globally fresh.  This class has a basic
--- instance based on the reader monad.
-class Monad m => LFresh m where
-  -- | Pick a new name that is fresh for the current (implicit) scope.
-  lfresh  :: Rep a => Name a -> m (Name a)
-  -- | Avoid the given names when freshening in the subcomputation.
-  avoid   :: [AnyName] -> m a -> m a
-
--- XXX TODO: move these instances somewhere else
--- | Simple reader monad instance for 'LFresh'.
-instance LFresh (Reader Integer) where
-  lfresh (Nm r (s,j)) = do { n <- ask; return (Nm r (s, max j (n+1))) }
-  avoid []          = id
-  avoid names       = local (max k)
-    where k = maximum (map anyName2Integer names)
-
--- | A monad instance for 'LFresh' which renames to the lowest
---  number not currently being used
-instance LFresh (Reader (Set AnyName)) where
-  lfresh nm = do
-    let s = name2String nm
-    used <- ask
-    return $ head (filter (\x -> not (S.member (AnyName x) used))
-                          (map (makeName s) [0..]))
-  avoid names = local (S.union (S.fromList names))
-
-
--- | Destruct a binding in an 'LFresh' monad.
-lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> ((a, b) -> m c) -> m c
-lunbind (B a b) g =
-  -- avoid (S.elems $ fv b) $ -- don't think we need this
-  lfreshen a (\x _ -> g (x, open initial x b))
-
-
--- | Unbind two terms with the same fresh names, provided the
---   binders match.
-lunbind2  :: (LFresh m, Alpha b, Alpha c, Alpha d) =>
-            Bind b c -> Bind b d -> (Maybe (b,c,d) -> m e) -> m e
-lunbind2 (B b1 c) (B b2 d) g =
-      case match b1 b2 of
-         Just _ ->
-           lunbind (B b1 c) $ \ (b', c') ->
-             g $ Just (b', c', open initial b' d)  -- BAY: the c' used to be c,
-         Nothing -> g Nothing                      -- am I correct in assuming
-                                                   -- that was a bug?
-
--- | Unbind three terms with the same fresh names, provided the
---   binders match.
-lunbind3  :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) =>
-            Bind b c -> Bind b d -> Bind b e ->  (Maybe (b,c,d,e) -> m f) -> m f
-lunbind3 (B b1 c) (B b2 d) (B b3 e) g = do
-      case (match b1 b2, match b1 b3) of
-         (Just _, Just _) ->
-           lunbind (B b1 c) $ \ (b', c') ->
-              g $ Just (b', c', open initial b' d, open initial b' e)
-         _ -> g Nothing
-
-------------------------------------------------------------
--- Substitution
-------------------------------------------------------------
-
--- | The 'Subst' class governs capture-avoiding substitution.  To
---   derive this class, you only need to indicate where the variables
---   are in the data type, by overriding the method 'isvar'.
-class (Rep1 (SubstD b) a) => Subst b a where
-
-  -- | If the argument is a variable, return its name and a function
-  --   to generate a substituted term.  Return 'Nothing' for
-  --   non-variable arguments.
-  isvar :: a -> Maybe (Name b, b -> a)
-  isvar x = Nothing
-
-  -- | @'subst' nm sub tm@ substitutes @sub@ for @nm@ in @tm@.
-  subst :: Name b -> b -> a -> a
-  subst n u x =
-      case isvar x of
-        Just (m, f) | m == n -> f u
-        Just (_, _) -> x
-        Nothing -> substR1 rep1 n u x
-
-  -- | Perform several simultaneous substitutions.
-  substs :: [Name b] -> [b] -> a -> a
-  substs ns us x =
-      case isvar x of
-        Just (m, f) ->
-          if length ns /= length us
-            then error "BUG: Number of vars and terms must match in multisubstitution"
-            else case m `List.elemIndex` ns of
-               Just i  -> f (us !! i)
-               Nothing -> x
-        Nothing -> substsR1 rep1 ns us x
-
--- | Reified class dictionary for 'Subst'.
-data SubstD b a = SubstD {
-  isvarD  :: a -> Maybe (Name b, b -> a),
-  substD  ::  Name b -> b -> a -> a ,
-  substsD :: [Name b] -> [b] -> a -> a
-}
-
-instance Subst b a => Sat (SubstD b a) where
-  dict = SubstD isvar subst substs
-
-substDefault :: Rep1 (SubstD b) a => Name b -> b -> a -> a
-substDefault = substR1 rep1
-
-substR1 :: R1 (SubstD b) a -> Name b -> b -> a -> a
-substR1 (Data1 dt cons) = \ x y d ->
-  case (findCon cons d) of
-  Val c rec kids ->
-      let z = map_l (\ w -> substD w x y) rec kids
-      in (to c z)
-substR1 r               = \ x y c -> c
-
-substsR1 :: R1 (SubstD b) a -> [Name b] -> [b] -> a -> a
-substsR1 (Data1 dt cons) = \ x y d ->
-  case (findCon cons d) of
-  Val c rec kids ->
-      let z = map_l (\ w -> substsD w x y) rec kids
-      in (to c z)
-substsR1 r               = \ x y c -> c
-
-instance Subst b Int
-instance Subst b Bool
-instance Subst b ()
-instance Subst b Char
-instance Subst b Integer
-instance Subst b Float
-instance Subst b Double
-
-instance Subst b AnyName
-instance Rep a => Subst b (R a)
-instance Rep a => Subst b (Name a)
-
-instance (Subst c a, Subst c b) => Subst c (a,b)
-instance (Subst c a, Subst c b, Subst c d) => Subst c (a,b,d)
-instance (Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a,b,d,e)
-instance (Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) =>
-   Subst c (a,b,d,e,f)
-instance (Subst c a) => Subst c [a]
-instance (Subst c a) => Subst c (Maybe a)
-instance (Subst c a, Subst c b) => Subst c (Either a b)
-
-instance (Subst c b, Subst c a, Alpha a,Alpha b) =>
-    Subst c (Bind a b)
-instance (Subst c b, Subst c a, Alpha a, Alpha b) =>
-    Subst c (Rebind a b)
-
-instance (Subst c a) => Subst c (Annot a)
-
-
--------------------- TESTING CODE --------------------------------
-data Exp = V (Name Exp)
-         | A Exp Exp
-         | L (Bind (Name Exp) Exp) deriving (Show)
-
-$(derive [''Exp])
-
-instance Alpha Exp
-instance Subst Exp Exp where
-   isvar (V n) = Just (n, id)
-   isvar _     = Nothing
-
--- deriving instance Eq Exp
--- deriving instance Ord Exp
-
-nameA, nameB, nameC :: Name Exp
-nameA = integer2Name 1
-nameB = integer2Name 2
-nameC = integer2Name 3
-
-assert :: String -> Bool -> IO ()
-assert s True = return ()
-assert s False = print ("Assertion " ++ s ++ " failed")
-
-do_tests :: ()
-do_tests =
-   unsafePerformIO $ do
-   tests_aeq
-   tests_fv
-   tests_big
-   tests_nth
-
-perm = single nameA nameB
-
-naeq x y = not (aeq x y)
-
-tests_aeq = do
-   assert "a1" $ (bind nameA nameA) `naeq` (bind nameA nameB)
-   assert "a2" $ (bind nameA nameA) `aeq` (bind nameA nameA)
-   assert "a3" $ (bind nameA nameA) `aeq` (bind nameB nameB)
-   assert "a4" $ (bind nameA nameB) `naeq` (bind nameB nameA)
-   assert "a5" $ (bind (nameA, Annot nameB) nameA) `naeq`
-                 (bind (nameA, Annot nameC) nameA)
-   assert "a6" $ (bind (nameA, Annot nameB) nameA) `aeq`
-                 (bind (nameA, Annot nameB) nameA)
-   assert "a7" $ (bind (nameA, Annot nameB) nameA) `aeq`
-                 (bind (nameB, Annot nameB) nameB)
-   assert "a8" $ rebind nameA nameB `naeq` rebind nameB nameB
-   assert "a9" $ rebind nameA nameA `naeq` rebind nameB nameB
-   assert "a9" $ (bind (rebind nameA (Annot nameA)) nameA) `aeq`
-                 (bind (rebind nameB (Annot nameB)) nameB)
-   assert "a10" $ bind (rebind (nameA, Annot nameA) ()) nameA `aeq`
-                  bind (rebind (nameB, Annot nameA) ()) nameB
-   assert "a11" $ bind (rebind (nameA, Annot nameA) ()) nameA `naeq`
-                  bind (rebind (nameB, Annot nameB) ()) nameB
-   assert "a12" $ bind (Annot nameA) () `naeq` bind (Annot nameB) ()
-   assert "a13" $ bind (Annot nameA) () `aeq` bind (Annot nameA) ()
-   assert "a14" $ bind (rebind (Annot nameA) ()) () `naeq`
-                  bind (rebind (Annot nameB) ()) ()
-   assert "a15" $ (rebind (nameA, Annot nameA) ()) `naeq`
-                  (rebind (name4, Annot nameC) ())
-   assert "a16" $ bind (nameA, nameB) nameA `naeq` bind (nameB, nameA) nameA
-   assert "a17" $ bind (nameA, nameB) nameA `naeq` bind (nameA, nameB) nameB
-   assert "a18" $ (nameA, nameA) `naeq` (nameA, nameB)
-   assert "a19" $ match (nameA, nameA) (nameB, nameC) == Nothing
-
-emptyNE :: Set (Name Exp)
-emptyNE = S.empty
-
-tests_fv = do
-   assert "f1" $ fv (bind nameA nameA) == emptyNE
-   assert "f2" $ fv' (pat initial) (bind nameA nameA) == S.empty
-   assert "f4" $ fv (bind nameA nameB) == S.singleton nameB
-   assert "f5" $ fv (bind (nameA, Annot nameB) nameA) == S.singleton nameB
-   assert "f7" $ fv (bind (nameB, Annot nameB) nameB) == S.singleton nameB
-   assert "f8" $ fv (rebind nameA nameB) == S.fromList [nameA, nameB]
-   assert "f9" $ fv' (pat initial) (rebind nameA nameA) == S.empty
-   assert "f3" $ fv (bind (rebind nameA (Annot nameA)) nameA) == emptyNE
-   assert "f10" $ fv (rebind (nameA, Annot nameA) ()) == S.singleton nameA
-   assert "f11" $ fv' (pat initial) (rebind (nameA, Annot nameA) ()) == S.singleton (AnyName nameA)
-   assert "f12" $ fv (bind (Annot nameA) ()) == S.singleton nameA
-   assert "f14" $ fv (rebind (Annot nameA) ()) == emptyNE
-
-mkbig :: [Name Exp] -> Exp -> Exp
-mkbig (n : names) body =
-    L (bind n (mkbig names (A (V n) body)))
-mkbig [] body = body
-
-big1 = mkbig (map integer2Name (take 100 [1 ..])) (V name11)
-big2 = mkbig (map integer2Name (take 101 [1 ..])) (V name11)
-
-
-tests_nth = do
-  assert "n1" $ nthpat ([nameA],nameB) 0 == AnyName nameA
-  assert "n2" $ nthpat ([nameA],nameB) 1 == AnyName nameB
-  assert "n3" $ nthpat (nameA, nameB) 0 == AnyName nameA
-  assert "p1" $ findpat ([nameA],nameB) (AnyName nameA) == Just 0
-  assert "p2" $ findpat ([nameA],nameB) (AnyName nameB) == Just 1
-  assert "p3" $ findpat ([nameA],nameB) (AnyName nameC) == Nothing
-
-tests_big = do
-   assert "b1" $ big1 `naeq` big2
-   assert "b2" $ fv big1 == emptyNE
-   assert "b3" $ big1 `aeq` subst name11 (V name11) big1
-
--- properties
--- if match t1 t2 = Some p then swaps p t1 = t2
-
--- $paynoattention
--- These type representation objects are exported so they can be
--- referenced by auto-generated code.  Please pretend they do not
--- exist.

@@ -1,1108 +0,0 @@-{-# LANGUAGE FlexibleInstances, UndecidableInstances, FlexibleContexts, MultiParamTypeClasses, TemplateHaskell, TypeOperators, ScopedTypeVariables, TypeSynonymInstances, RankNTypes, GADTs, EmptyDataDecls, StandaloneDeriving #-}
-
-----------------------------------------------------------------------
--- |
--- Module      :  Generics.RepLib.Bind.Nominal
--- License     :  BSD-like (see LICENSE)
---
--- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>
--- Stability   :  experimental
--- Portability :  non-portable (-XKitchenSink)
---
--- Generic implementation of name binding functions, based on the library
--- RepLib. This version uses a nominal representation of binding structure.
---
--- DISCLAIMER: this module probably contains bugs and is noticeably
--- slower than "Generics.RepLib.Bind.LocallyNameless".  At this point
--- we recommend it only for the curious or intrepid.
---
--- Datatypes with binding defined using the 'Name' and 'Bind' types.
--- Important classes are
---     'Alpha' -- the class of types that include binders.
--- These classes are generic, and default implementations exist for all
--- representable types. This file also defines a third generic class,
---     'Subst' -- for subtitution functions.
---
---------------------------------------------------------------------------
-module Generics.RepLib.Bind.Nominal
-  (-- * Basic types
-    Name, Bind, Annot(..), Rebind,
-
-    -- ** Utilities
-    integer2Name, string2Name, name2Integer, name2String, makeName,
-    name1,name2,name3,name4,name5,name6,name7,name8,name9,name10,
-
-    -- * The 'Alpha' class
-    Alpha(..),
-    swaps, -- is a bit wonky
-    -- match is not working yet
-    binders, patfv, fv,
-    aeq,
-
-    -- * Binding operations
-    bind, unsafeUnBind,
-
-    -- * The 'Fresh' class
-    Fresh(..), freshen,
-    unbind, unbind2, unbind3,
-
-    -- * The 'LFresh' class
-    HasNext(..), LFresh(..),
-    lfreshen,
-    lunbind, lunbind2, lunbind3,
-
-    -- * Rebinding operations
-    rebind, reopen,
-
-    -- * Substitution
-    Subst(..),
-
-   -- * Advanced
-   AlphaCtx, matchR1,
-
-   -- * Pay no attention to the man behind the curtain
-   -- $paynoattention
-   rName, rBind, rRebind, rAnnot) where
-
-import Generics.RepLib
-import Generics.RepLib.Bind.PermM
-
-import qualified Data.List as List
-import qualified Text.Read as R
-import Data.Set (Set)
-import Data.Maybe
-import qualified Data.Set as S
-import Prelude hiding (or)
-import Data.Monoid
-import Control.Monad.Reader (Reader,ask,local,runReader)
-import System.IO.Unsafe (unsafePerformIO)
-
----------------------------------------------------
-
-$(derive_abstract [''R])
--- The above only works with GHC 7.
-
--- | Names are things that get bound. The usual protocol
--- is for names to get created by some automatic process,
--- that preserves alpha renaming under operations over
--- Binding instances.
-data Name a = Nm (R a) (String,Integer) deriving (Eq, Ord)
-
--- | Type of a binding.  Morally, the type a should be in the
--- class 'Pattern' and the type b should be in the class 'Alpha'.
--- The Pattern class contains the constructor and a safe
--- destructor for these types.
--- We can Bind an "a" object in a "b" object if we
--- can create "fresh" a objects, and Names can be
--- swapped in "b" objects. Often "a" is Name
--- but that need not be the case.
-data Bind a b = B a b
-
-
--- | A name with a hidden (existentially quantified) sort.
-data AnyName = forall a. Rep a => AnyName (Name a)
-
--- | An annotation is a 'hole' in a pattern where variables
--- can be used, but not bound. For example patterns may include
--- type annotations, and those annotations can reference variables
--- without binding them.
--- Annotations do nothing special when they appear elsewhere in terms
-newtype Annot a = Annot a deriving (Read, Eq)
-
--- | Rebinding is for telescopes --- i.e. to support patterns that
--- also bind variables that appear later
-data Rebind a b = R a (Bind [AnyName] b)
-
--- Fragily deriving the replib instances for Bind and Name
--- in the same file that they are defined in. This shouldn't
--- work but it does.
-$(derive [''Bind, ''Name, ''Annot, ''Rebind])
-
-
--- AnyName has an existential in it, so we cannot create a complete
--- representation for it, unfortunately.
-
-$(derive_abstract [''AnyName])
-
-instance Show AnyName where
-  show (AnyName n1) = show n1
-
-instance Eq AnyName where
-   (AnyName n1) == (AnyName n2) =
-      case gcastR (getR n1) (getR n2) n1 of
-           Just n1' -> n1' == n2
-           Nothing  -> False
-
-instance Ord AnyName where
-   compare (AnyName n1) (AnyName n2) =
-       case compareR (getR n1) (getR n2) of
-         EQ  -> case gcastR (getR n1) (getR n2) n1 of
-           Just n1' -> compare n1' n2
-           Nothing  -> error "Panic: equal types are not equal in Ord AnyName instance!"
-         ord -> ord
-
--- | Get the integer index of an 'AnyName'.
-anyName2Integer :: AnyName -> Integer
-anyName2Integer (AnyName nm) = name2Integer nm
-
--- | Get the string part of an 'AnyName'.
-anyName2String :: AnyName -> String
-anyName2String (AnyName nm) = name2String nm
-
-toSortedName :: Rep a => AnyName -> Maybe (Name a)
-toSortedName (AnyName n) = gcastR (getR n) rep n
-
----------------------------------------------------------------
--- Constructors and destructors for builtin types
----------------------------------------------------------------
-name1, name2, name3, name4, name5, name6, name7, name8, name9, name10, name11
-  :: Rep a => Name a
-name1 = integer2Name 1
-name2 = integer2Name 2
-name3 = integer2Name 3
-name4 = integer2Name 4
-name5 = integer2Name 5
-name6 = integer2Name 6
-name7 = integer2Name 7
-name8 = integer2Name 8
-name9 = integer2Name 9
-name10 = integer2Name 10
-name11 = integer2Name 11
-
-instance Show (Name a)  where
-  show (Nm _ ("",n)) = "_" ++ (show n)
-  show (Nm _ (x,0)) = x
-  show (Nm _ (x,n)) = x ++ (show n)
-
-name2Integer :: Name a -> Integer
-name2Integer (Nm _ (_,x)) = x
-
-integer2Name :: Rep a => Integer -> Name a
-integer2Name n = Nm rep ("",n)
-
--- | Get the string part of a 'Name'.
-name2String :: Name a -> String
-name2String (Nm _ (s,_)) = s
-
-string2Name :: Rep a => String -> Name a
-string2Name s = Nm rep (s,0)
-
-makeName :: Rep a => String -> Integer -> Name a
-makeName s i = Nm rep (s,i)
-
--- | Determine the sort of a 'Name'.
-getR :: Name a -> R a
-getR (Nm r _)   = r
-
-
-----------------------------------------------------------
--- Binding operations & instances
-----------------------------------------------------------
--- | Smart constructor for binders
-bind :: (Alpha b,Alpha c) => b -> c -> Bind b c
-bind a b = B a b
-
--- | A destructor for binders that does not guarantee fresh
--- names for the binders.
-unsafeUnBind :: Bind a b -> (a,b)
-unsafeUnBind (B a b) = (a,b)
-
-{-
-instance (Alpha a, Alpha b, Eq b) => Eq (Bind a b) where
-   (B x y) == (B m n) =
-      case match x m of
-         Just p | isid p -> y == n
-         Just p -> y == swaps p n &&
-                   S.null (fv x `S.intersection` fv n)
-         Nothing -> False
-
-instance (Alpha a, Alpha b, Ord a, Ord b) => Ord (Bind a b) where
-   compare (B a1 b1) (B a2 b2) =
-       case (match a1 a2) of
-         Just p  -> case compare a1 (swaps p a2) of
-                      EQ -> compare b1 b2
-                      otherwise -> otherwise
-         Nothing -> compare a1 a2
--}
-
-instance (Show a, Show b) => Show (Bind a b) where
-  showsPrec p (B a b) = showParen (p>0)
-      (showString "<" . showsPrec p a . showString "> " . showsPrec 0 b)
-
-instance (Show a) => Show (Annot a) where
-  showsPrec p (Annot a) = (showString "[:" . showsPrec 0 a . showString "]")
-
-instance (Alpha a, Alpha b, Read a, Read b) => Read (Bind a b) where
-         readPrec = R.parens $ (R.prec app_prec $ do
-                                  R.Ident "B" <- R.lexP
-                                  m1 <- R.step R.readPrec
-                                  m2 <- R.step R.readPrec
-                                  return (bind m1 m2))
-           where app_prec = 10
-
-         readListPrec = R.readListPrecDefault
-
-----------------------------------------------------------
--- Rebinding operations
-----------------------------------------------------------
-
--- | Constructor for binding in patterns
-rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b
-rebind a b = R a (bind (binders' initial a) b)
-
-{-
-instance (Eq a, Alpha a, Alpha b, Eq b) => Eq (Rebind a b) where
-   (R a1 b1) == (R a2 b2) = a1 == a2 && b1 == b2
--}
-
-instance (Alpha a, Show a, Show b) => Show (Rebind a b) where
-  showsPrec p (R a (B a' b)) =  showParen (p>0)
-      (showString "<<" . showsPrec p a . sa' . showString ">> " . showsPrec 0 b)
-   where sa' =  if binders' initial a == a' then showString ""
-                  else showString "/" . showsPrec p a'
-
--- | destructor for binding patterns, the external names should have already
--- been freshen'ed. We swap the internal names so that they use the
--- external names
-reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b)
-reopen (R a1 (B names b)) = (a1, swaps p b) where
-   p = foldl (<>) empty (zipWith single (S.elems $ fv' initial a1)
-                                        names)
-
-----------------------------------------------------------
--- Wrappers for operations in the Alpha class
-----------------------------------------------------------
-
-aeq :: Alpha a => a -> a -> Bool
-aeq t1 t2 = aeq' initial t1 t2
-{-
-  case match t1 t2 of
-              Just p -> isid p
-              _       -> False
--}
-
--- | calculate the free variables of the term
-fv :: (Rep b, Alpha a) => a -> Set (Name b)
-fv = S.map fromJust . S.filter isJust . S.map toSortedName . fv' initial
-
--- | List the binding variables in a pattern
-binders :: (Rep b, Alpha b) => b -> [AnyName]
-binders = binders' initial
-
--- | Set of variables that occur freely in annotations (not binding)
-patfv :: (Rep a, Alpha b) => b -> Set (Name a)
-patfv = S.map fromJust . S.filter isJust . S.map toSortedName . fv' (pat initial)
-
--- | The method "swaps" applys a permutation to all free variables
--- in the term.
-swaps :: Alpha a => Perm AnyName -> a -> a
-swaps = swaps' initial
-
--- | Apply a permutation to the binding variables in a pattern.
--- Annotations are left alone by the permutation.
-swapsBinders :: Alpha a => Perm AnyName -> a -> a
-swapsBinders = swaps' initial
-
--- | Apply a permutation to the annotations in a pattern. Binding
--- names are left alone by the permutation.
-swapsAnnots :: Alpha a => Perm AnyName -> a -> a
-swapsAnnots = swaps' (pat initial)
-
-
--- | "Locally" freshen an object
-lfreshen :: Alpha a => LFresh m => a -> (a -> Perm AnyName -> m b) -> m b
-lfreshen = lfreshen' initial
-
--- | An object of type "b" can be freshened if a new
--- copy of "b" can be produced where all old *binding* Names
--- in "b" are replaced with new fresh Names, and the
--- permutation reports which Names were swapped by others.
-freshen :: (Fresh m, Alpha a) => a -> m (a, Perm AnyName)
-freshen = freshen' initial
-
--- | Match compares two data structures and produces a permutation
--- of their Names that will make them alpha-equivalent to
--- eachother. (Names that appear in annotations must match exactly.)
--- Also note that two terms are alpha-equivalent when the empty
--- permutation is returned.
-match   :: Alpha a => a -> a -> Maybe (Perm AnyName)
-match   = match' initial
-
-
--- | Compare two patterns, ignoring the names of binders, and produce
--- a permutation of their annotations to make them alpha-equivalent
--- to eachother. Return 'Nothing' if no such renaming is possible.
-matchAnnots :: Alpha a => a -> a -> Maybe (Perm AnyName)
-matchAnnots = match' (pat initial)
-
--- | Compare two patterns for equality and produce a permutation of
--- their binding 'Names' to make them alpha-equivalent to each other
--- ('Name's that appear in annotations must match exactly). Return
--- 'Nothing' if no such renaming is possible.
-matchBinders ::  Alpha a => a -> a -> Maybe (Perm AnyName)
-matchBinders = match' initial
-
----------------------------------------------------------------
--- | Many of the operations in the 'Alpha' class take an 'AlphaCtx':
--- stored information about the iteration as it progresses. This type
--- is abstract, as classes that override these operations should just pass
--- the context on.
-data AlphaCtx = Term | Pat deriving (Show, Eq, Read)
-
-initial :: AlphaCtx
-initial = Term
-
-pat  :: AlphaCtx -> AlphaCtx
-pat c  = Pat
-
-term  :: AlphaCtx -> AlphaCtx
-term c  = Term
-
-mode :: AlphaCtx -> AlphaCtx
-mode = id
-
--- | The Alpha class is for all terms that may contain binders
--- The 'Rep1' class constraint means that we can only
--- make instances of this class for types that have
--- generic representations. (Derive these using TH and
--- RepLib.)
-
-class (Rep1 (AlphaD) a) => Alpha a where
-
-  aeq' :: AlphaCtx -> a -> a -> Bool
-  aeq' = aeqR1 rep1
-
-  swapall' :: AlphaCtx -> Perm AnyName -> a -> a
-  swapall' = swapallR1 rep1
-
-  -- | The method "swaps'" applys a compound permutation.
-  swaps' :: AlphaCtx -> Perm AnyName -> a -> a
-  swaps' = swapsR1 rep1
-
-  -- | calculate the free variables (aka support)
-  fv' :: AlphaCtx -> a -> Set AnyName
-  fv' = fvR1 rep1
-
-  binders' :: AlphaCtx -> a -> [AnyName]
-  binders' = bindersR1 rep1
-
-  -- | Match' compares two data structures and produces a
-  -- permutation of their free variables that will make them
-  -- alpha-equivalent to eachother.
-  match' :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)
-  match' = matchR1 rep1
-
-  -- | An object of type "a" can be freshened if a new
-  -- copy of "a" can be produced where all old Names
-  -- in "a" are replaced with new fresh Names, and the
-  -- permutation reports which names were swapped by others.
-  freshen' :: Fresh m => AlphaCtx -> a -> m (a,Perm AnyName)
-  freshen' = freshenR1 rep1
-
-  -- | See 'lfreshen'
-  lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
-  lfreshen' = lfreshenR1 rep1
-
-
--- class constraint hackery to allow us to override the
--- default definitions for certain classes
-data AlphaD a = AlphaD {
-  aeqD     :: AlphaCtx -> a -> a -> Bool,
-  swapallD   :: AlphaCtx -> (Perm AnyName) -> a -> a,
-  swapsD   :: AlphaCtx -> (Perm AnyName) -> a -> a,
-  fvD      :: AlphaCtx -> a -> Set AnyName,
-  bindersD :: AlphaCtx -> a -> [AnyName],
-
-  matchD   :: AlphaCtx -> a -> a -> Maybe (Perm AnyName),
-  freshenD :: forall m. Fresh m => AlphaCtx -> a -> m (a,Perm AnyName),
-  lfreshenD :: forall b m. LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
- }
-
-instance Alpha a => Sat (AlphaD a) where
-  dict = AlphaD aeq' swapall' swaps' fv' binders' match' freshen' lfreshen'
-
--- Generic definitions of the class functions.
--- (All functions that take representations end
--- in 'R1')
-aeqR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Bool
-aeqR1 (Data1 _ cons) = loop cons where
-  loop (Con emb reps : rest) p x y =
-    case (from emb x, from emb y) of
-      (Just p1, Just p2) -> aeq1 reps p p1 p2
-      (Nothing, Nothing) -> loop rest p x y
-      (_,_)              -> False
-  loop [] _ _ _ = error "Impossible"
-aeqR1 Int1 = \ _ x y -> x == y
-aeqR1 Integer1 = \ _ x y -> x == y
-aeqR1 Char1 = \ _ x y -> x == y
-aeqR1 _ = \ _ _ _ -> error "Cannot aeq this type"
-
-aeq1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Bool
-aeq1 MNil _ Nil Nil = True
-aeq1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) =
-  aeqD r c p1 p2 && aeq1 rs c t1 t2
-
-swapsR1 :: R1 (AlphaD) a -> AlphaCtx -> (Perm AnyName) -> a -> a
-swapsR1 Char1           = \ _ _ c -> c
-swapsR1 Int1            = \ _ _ c -> c
-swapsR1 Float1          = \ _ _ c -> c
-swapsR1 Integer1        = \ _ _ c -> c
-swapsR1 (Data1 _ cons)  = \ p x d ->
-  case (findCon cons d) of
-  Val c rec kids -> to c (map_l (\z -> swapsD z p x) rec kids)
-swapsR1 r               = error ("Cannot swap type " ++ (show r))
-
-
-swapallR1 :: R1 (AlphaD) a -> AlphaCtx -> (Perm AnyName) -> a -> a
-swapallR1 Char1           = \ _ _ c -> c
-swapallR1 Int1            = \ _ _ c -> c
-swapallR1 Float1          = \ _ _ c -> c
-swapallR1 Integer1        = \ _ _ c -> c
-swapallR1 (Data1 _ cons)  = \ p x d ->
-  case (findCon cons d) of
-  Val c rec kids -> to c (map_l (\z -> swapallD z p x) rec kids)
-swapallR1 r               = error ("Cannot swap type " ++ (show r))
-
-fvR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> Set AnyName
-fvR1 (Data1 _ cons) = \ p  d ->
-  case (findCon cons d) of
-    Val _ rec kids -> fv1 rec p kids
-fvR1 _ = \ _ _ -> S.empty
-
-fv1 :: MTup (AlphaD) l -> AlphaCtx -> l -> Set AnyName
-fv1 MNil _ Nil = S.empty
-fv1 (r :+: rs) p (p1 :*: t1) =
-   fvD r p p1 `S.union` fv1 rs p t1
-
-bindersR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> [AnyName]
-bindersR1 (Data1 _ cons) = \ p  d ->
-  case (findCon cons d) of
-    Val _ rec kids -> binders1 rec p kids
-bindersR1 _ = \ _ _ -> []
-
-binders1 :: MTup (AlphaD) l -> AlphaCtx -> l -> [AnyName]
-binders1 MNil _ Nil = []
-binders1 (r :+: rs) p (p1 :*: t1) =
-   bindersD r p p1 ++ binders1 rs p t1
-
-
-matchR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)
-matchR1 (Data1 _ cons) = loop cons where
-  loop (Con emb reps : rest) p x y =
-    case (from emb x, from emb y) of
-      (Just p1, Just p2) -> match1 reps p p1 p2
-      (Nothing, Nothing) -> loop rest p x y
-      (_,_)              -> Nothing
-  loop [] _ _ _ = error "Impossible"
-matchR1 Int1 = \ _ x y -> if x == y then Just empty else Nothing
-matchR1 Integer1 = \ _ x y -> if x == y then Just empty else Nothing
-matchR1 Char1 = \ _ x y -> if x == y then Just empty else Nothing
-matchR1 _ = \ _ _ _ -> Nothing
-
-match1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Maybe (Perm AnyName)
-match1 MNil _ Nil Nil = Just empty
-match1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) = do
-  l1 <- matchD r c p1 p2
-  l2 <- match1 rs c t1 t2
-  (l1 `join` l2)
-
-
-freshenR1 :: R1 (AlphaD) a -> Fresh m => AlphaCtx -> a -> m (a,Perm AnyName)
-freshenR1 (Data1 _ cons) = \ p d ->
-   case findCon cons d of
-     Val c rec kids -> do
-       (l, p') <- freshenL rec p kids
-       return (to c l, p')
-freshenR1 _ = \ _ n -> return (n, empty)
-
-freshenL :: Fresh m => MTup (AlphaD) l -> AlphaCtx -> l -> m (l, Perm AnyName)
-freshenL MNil _ Nil = return (Nil, empty)
-freshenL (r :+: rs) p (t :*: ts) = do
-  (xs, p2) <- freshenL rs p ts
-  (x, p1) <- freshenD r p (swapsD r p p2 t)
-  return ( x :*: xs, p1 <> p2)
-
-lfreshenR1 :: LFresh m => R1 AlphaD a -> AlphaCtx -> a ->
-              (a -> Perm AnyName -> m b) -> m b
-lfreshenR1 (Data1 _ cons) = \p d f ->
-   case findCon cons d of
-     Val c rec kids -> lfreshenL rec p kids (\ l p' -> f (to c l) p')
-lfreshenR1 _ = \ _ n f -> f n empty
-
-lfreshenL :: LFresh m => MTup (AlphaD) l -> AlphaCtx -> l ->
-              (l -> Perm AnyName -> m b) -> m b
-lfreshenL MNil _ Nil f = f Nil empty
-lfreshenL (r :+: rs) p (t :*: ts) f =
-  lfreshenL rs p ts ( \ y p2 ->
-  lfreshenD r p (swapsD r p p2 t) ( \ x p1 ->
-     f (x :*: y) (p1 <> p2)))
-
-
-instance (Rep a) => Alpha (Name a) where
-  fv' c n@(Nm _ _)  | mode c == Term = S.singleton (AnyName n)
-  fv' c n           | mode c == Pat  = S.empty
-
-  binders' c n@(Nm _ _)  | mode c == Term = [AnyName n]
-  binders' c n           | mode c == Pat  = []
-
-  swapall' c p x =
-      case apply p (AnyName x) of
-       AnyName y ->
-        case cast y of
-          Just y' -> y'
-          Nothing -> error "Internal error in swaps': sort mismatch"
-
-  swaps' c p x | mode c == Term =
-      case apply p (AnyName x) of
-       AnyName y ->
-        case cast y of
-          Just y' -> y'
-          Nothing -> error "Internal error in swaps': sort mismatch"
-  swaps' c p x | mode c == Pat = x
-
-  aeq' c x y = x == y
-
-  match' c x y  | x == y         = Just empty
-  match' c x y  | mode c == Term =
-    Just $ single (AnyName x) (AnyName y)
-  match' c _ _  | mode c == Pat  = Just empty
-
-  freshen' c nm = case mode c of
-     Term -> do x <- fresh nm
-                return (x, single (AnyName nm) (AnyName x))
-     Pat  -> return (nm, empty)
-
-  lfreshen' c nm f = case mode c of
-     Term -> do x <- lfresh nm
-                avoid [AnyName x] $ f x (single (AnyName nm) (AnyName x))
-     Pat  -> f nm empty
-
-
-instance Alpha AnyName  where
-
-  fv' Term n = S.singleton n
-  fv' Pat n  = S.empty
-
-  binders' Term n = [n]
-  binders' Pat n  = []
-
-  swapall' c p x = apply p x
-
-  swaps' Term p x = apply p x
-  swaps' Pat perm x = x
-
-  aeq' c x y = x == y
-
-  match' Term x y = if x == y then Just empty else Just (single x y)
-  match' Pat x y = Just empty
-
-  freshen' Term (AnyName nm) = do { x <- fresh nm; return(AnyName x,
-                                  (single (AnyName nm) (AnyName x))) }
-  freshen' Pat nm = return (nm, empty)
-
-  lfreshen' c (AnyName nm) f = case mode c of
-     Term -> do { x <- lfresh nm; avoid [AnyName x] $ f (AnyName x)
-                     (single (AnyName nm) (AnyName x)) }
-     Pat  -> f (AnyName nm) empty
-
-instance (Alpha a, Alpha b) => Alpha (Bind a b) where
-
-    -- to swap in a binder, swap the free variables in the
-    -- pattern, then remove the binders from the permutation
-    -- and swap in the body
-    -- ? why don't we just swap everywhere?
-    swaps' p pm (B x y) =
-        B (swaps' (pat p) pm x) (swaps' p pm' y) where
-            pm' = restrict pm (binders x)
-
-    -- free variables of a binder are the free variables in
-    -- the annotations in the pattern plus the free variables
-    -- of the body, minus the binders.
-    fv' p (B x y) = fv' Pat x `S.union` (fv' p y S.\\ fv' Term x)
-
-    binders' p (B x y) = binders' Pat x ++
-                         (binders' p y List.\\ binders' Term x)
-
-{-
-    freshen' p (B x y) = do
---       (x', p1)  <- freshen' (all p) x -- freshen the binders & annots
-       (y', p3) <- freshen' p (swaps' p p1 y) -- freshen body
-       return (B x' y', p1 <> p3)
--}
-
-    lfreshen' c (B x y) f =
-      avoid (S.elems $ fv' c x) $
-        lfreshen' (pat c) x (\ x' pm1 ->
-        lfreshen' c (swaps' c pm1 y) (\ y' pm2 ->
-        f (B x' y') (pm1 <> pm2)))
-
-    -- this version of aeq seems to work
-    aeq' p (B x1 y1) (B x2 y2) =
-       case () of
-         () | bx1 == bx2 -> aeq' p x1 x2 && aeq' p y1 y2
-         () | (S.fromList bx1) `S.intersection` (fv' Term y2 S.\\ fv' Term y1)
-            /= S.empty -> False
-         _ -> aeq' p x1 (swaps' Term pm x2) && aeq' p y1 (swapall' Term pm y2)
-       where bx1 = binders' Term x1
-             bx2 = binders' Term x2
-             pm  = foldl (<>) empty (zipWith single bx1 bx2)
-    -- basic idea of match
-    -- if binders x1 == binders x2 then
-        --- match the annots in x1 and x2 and match the bodies y1 y2
-    -- if binders x1 /= binders x2 then
-        -- make sure binders of x1 are not free in the body of y2
-        -- swap (x1,x2) in y2
-        -- match the annots & match the bodies
-        -- make sure none of the binders escapes in the resulting match
-    -- ingredients:
-        -- match the binders, ignoring the annots
-        -- match the annots, ignoring the binders
-        -- list the binding variables
-    match' p (B x1 y1) (B x2 y2)  =
-      case () of
-        () | bx1 == bx2 -> do
-            pm1 <- match' Pat x1 x2
-            pm2 <- match' p y1 y2
-            pm1 `join` pm2
-        () | (S.fromList bx1) `S.intersection` (fv' Term y2 S.\\ fv' Term y1)
-            /= S.empty -> Nothing
-        _ -> do
-            pm1 <- match' Pat x1 x2'
-            pm2 <- match' p y1 y2'
-            if S.fromList bx1 `S.intersection` S.fromList (support pm2) /= S.empty
-              then Nothing
-              else pm1 `join` pm2
-            -- note pm2 should not have any of the binders in the support
-       where bx1 = binders' Term x1
-             bx2 = binders' Term x2
-             pm  = foldl (<>) empty (zipWith single bx1 bx2)
-             x2' = swaps' Term pm x2
-             y2' = swaps' Term pm (swaps' Pat pm y2)
-{-
-        case (match' Term x1 x2) of
-          Just pmt | isid pmt -> do
-            pm1 <- match' Pat x1 x2
-            pm2 <- match' p y1 y2
-            pm1 `join` pm2
-          Just pmt ->
-            let xs = fv' Term x1 in
-            if xs `S.intersection` fv' Term (B x2 y2) == S.empty then do
-               pm1 <- match' Pat x1 (swaps' p pmt x2)
-               pm2 <- match' p y1 (swaps' p pmt y2)
-               pm1 `join` pm2
-             else Nothing
-          _ -> Nothing
-   -- match' Pat _ _ = error "cannot match binders here."
--}
-
-instance (Alpha a, Alpha b) => Alpha (Rebind a b) where
-
-   -- free variables of the external binder
-   -- plus free vars of the annots in the binder
-   -- plus free vars of the body minus any
-   --     binding vars of internal binder
-   fv' p (R x (B ns y)) = fv' p x `S.union`
-      (fv' p y S.\\ S.fromList ns)
-
-   binders' p (R x (B ns y)) = binders' p x ++
-      (binders' p y List.\\ ns)
-
-
-   swaps' Term pm (R x (B ns y)) =
-      R (swaps' Term pm x) (B ns (swaps' Term pm' y)) where
-            pm' = restrict pm ns
-
-   match' p (R x1 (B n1 y1)) (R x2 (B n2 y2)) = do
-      px  <- match' p x1 x2   -- external names
-      pb  <- match' p (B n1 y1) (B n2 y2)
-      px `join` pb
-
-   freshen' p (R x (B x1 y)) = do
-      (x', pm1) <- freshen' p x
-      (y', pm2) <- freshen' p (swaps' p pm1 y)
-      return (R x (B x1 y'), pm1 <> pm2)
-
-
-instance (Eq a, Alpha a) => Alpha (Annot a) where
-
-   swaps' Pat  pm (Annot t) = Annot (swaps' Term pm t)
-   swaps' Term pm (Annot t) = Annot t
-
-   fv' Pat (Annot t)        = fv' Term t
-   fv' Term _               = S.empty
-
-   binders' Pat (Annot t)   = binders' Term t
-   binders' Term _          = []
-
-
-   freshen' Pat (Annot t)  = do
-     (t', p) <- freshen' Term t
-     return (Annot t', p)
-   freshen' Term a       = return (a, empty)
-
-   match' Pat (Annot x) (Annot y)  = match' Term x y
-   match' Term (Annot x) (Annot y) = if x `aeq` y
-                                    then Just empty
-                                    else Nothing
-
--- Instances for other types (mostly) use the default definitions.
-instance Alpha Bool where
-instance Alpha Float where
-instance Alpha () where
-instance Alpha a => Alpha [a] where
-instance Alpha Int where
-instance Alpha Integer where
-instance Alpha Double where
-instance Alpha Char where
-instance Alpha a => Alpha (Maybe a) where
-instance (Alpha a,Alpha b) => Alpha (Either a b) where
-instance (Alpha a,Alpha b) => Alpha (a,b) where
-instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c) where
-instance (Alpha a, Alpha b,Alpha c, Alpha d) => Alpha (a,b,c,d)
-instance (Alpha a, Alpha b,Alpha c, Alpha d, Alpha e) =>
-   Alpha (a,b,c,d,e)
-instance (Rep a) => Alpha (R a) where
-
-
--- Definitions of the class members for abstract types.
-{-
-abs_swaps' :: Alpha a => AlphaCtx -> Perm Name -> a -> a
-abs_swaps' _ p s = s
-abs_fv' :: Alpha a => AlphaCtx -> a -> [Name]
-abs_fv' _ s = []
-abs_freshen' :: (Fresh m, Alpha a) => AlphaCtx -> a -> m (a, Perm Name)
-abs_freshen' _ b = return (b, empty)
-abs_match' :: (Eq a, Alpha a) => AlphaCtx -> a -> a -> Maybe (Perm Name)
-abs_match' _ x1 x2 = if x1 == x2 then Just empty else Nothing
--}
-
--------------------------------------------------------
--- | A monad "m" supports the nextInteger operation if it
--- can generate new fresh integers
-
-class Monad m => HasNext m where
-  nextInteger :: m Integer
-  resetNext   :: Integer -> m ()
-
--- | A monad "m" supports the "fresh" operation if it
--- can generate a new unique names.
-
-class (Monad m, HasNext m) => Fresh m where
-  fresh :: Name a -> m (Name a)
-  fresh (Nm r (s,j)) = do { i <- nextInteger; return (Nm r (s,i)) }
-
-instance HasNext m => Fresh m where
-  fresh (Nm r (s,j)) = do { n <- nextInteger; return (Nm r (s,n)) }
-
--- | Unbind is the destructor of a binding. It ensures that
--- the names in the binding b are fresh.
-unbind  :: (Alpha b,Fresh m,Alpha c) => Bind b c -> m (b,c)
-unbind (B x y) = do
-    (x',perm) <- freshen x
-    return(x', swaps perm y)
-
--- | Destruct two bindings simultanously, if they match, using the
--- same list of fresh names
-unbind2  :: (Fresh m,Alpha b,Alpha c, Alpha d) =>
-   Bind b c -> Bind b d -> m (Maybe (b,c,d))
-unbind2 (B x1 y1) (B x2 y2) = do
-   (x1', perm1) <- freshen x1
-   case match x1' x2 of
-      (Just perm2) ->
-         return $ Just (x1', swaps perm1 y1, swaps perm2 y2)
-      Nothing -> return Nothing
-
-unbind3  :: (Fresh m,Alpha b,Alpha c, Alpha d, Alpha e) =>
-   Bind b c -> Bind b d -> Bind b e -> m (Maybe (b,c,d,e))
-unbind3 (B x1 y1) (B x2 y2) (B x3 y3) = do
-   (x1', perm1) <- freshen x1
-   case (match x1' x2, match x1' x3) of
-      (Just perm2, Just perm3) ->
-         return $ Just (x1', swaps perm1 y1, swaps perm2 y2, swaps perm3 y3)
-      _ -> return Nothing
-
------------------------------------------------------------------
--- | Locally fresh monad
--- This is the class of
--- monads that support freshness in an (implicit) local scope.  Names
--- drawn are fresh for this particular scope, but not globally fresh.
--- This class has a basic instance based on the reader monad.
-class Monad m => LFresh m where
-  -- | pick a new name that is fresh for the current (implicit) scope.
-  lfresh  :: Rep a => Name a -> m (Name a)
-  -- | avoid these names when freshening in the subcomputation.
-  avoid   :: [AnyName] -> m a -> m a
-
--- | Reader monad instance for local freshness class.
-instance LFresh (Reader Integer) where
-  lfresh (Nm r (s,j)) = do { n <- ask; return (Nm r (s, max j (n+1))) }
-  avoid []          = id
-  avoid names       = local (max k) where
-        k = maximum (map anyName2Integer names)
-
--- | Destruct a binding in the LFresh monad.
-lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> m (a, b)
-lunbind (B a b) =
-  avoid (S.elems $ fv' initial b) $ error "UNIMP"
-
-
-lunbind2  :: (LFresh m, Alpha b, Alpha c, Alpha d) =>
-            Bind b c -> Bind b d -> m (Maybe (b,c,d))
-lunbind2 (B b1 c) (B b2 d) = do
-      case match b1 b2 of
-         Just _ -> do
-           (b', c') <- lunbind (B b1 c)
-           return $ error "UNIMP"
-         Nothing -> return Nothing
-
-lunbind3  :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) =>
-            Bind b c -> Bind b d -> Bind b e ->  m (Maybe (b,c,d,e))
-lunbind3 (B b1 c) (B b2 d) (B b3 e) = do
-      case (match b1 b2, match b1 b3) of
-         (Just _, Just _) -> do
-           (b', c') <- lunbind (B b1 c)
-           return $ error "UNIMP"
-         _ -> return Nothing
-
-
----------------------------------------------------------------
-
--- | Capture-avoiding substitution, in a monad so that we can rename
--- variables at binding locations and avoid capture
-
-subst :: (Alpha a, Alpha b, Subst b a) => Name b -> b -> a -> a
-subst n u x =
- runReader (avoid ([AnyName n] ++ (S.elems $ fv' initial u)++(S.elems $ fv' initial x)) $ lsubst n u x) (0 :: Integer)
-
-substs :: (Alpha a, Alpha b, Subst b a) => [Name b] -> [b] -> a -> a
-substs ns us x =
- runReader (avoid ((map AnyName ns) ++ (concatMap (S.elems . (fv' initial)) us)++(S.elems $ fv' initial x)) $ lsubsts ns us x)
-     (0 :: Integer)
-
-
-class (Rep1 (SubstD b) a) => Subst b a where
-  isvar :: a -> Maybe (Name b, b -> a)
-  isvar x = Nothing
-
-  lsubst :: LFresh m => Name b -> b -> a -> m a
-  lsubst n u x =
-      case isvar x of
-        Just (m, f) | m == n -> return (f u)
-        Just (_, _) -> return x
-        Nothing -> substR1 rep1 n u x
-
-
-  lsubsts :: LFresh m => [Name b] -> [b] -> a -> m a
-  lsubsts ns us x =
-      case isvar x of
-        Just (m, f) -> case m `List.elemIndex` ns of
-                    Just i  -> return (f (us !! i))
-                    Nothing -> return x
-        Nothing -> substsR1 rep1 ns us x
-
-
-data SubstD b a = SubstD {
-   substD  :: LFresh m => Name b -> b -> a -> m a
-  ,substsD :: LFresh m => [Name b] -> [b] -> a -> m a
-}
-
-instance Subst b a => Sat (SubstD b a) where
-  dict = SubstD lsubst lsubsts
-
-substR1 :: LFresh m => R1 (SubstD b) a -> Name b -> b -> a -> m a
-substR1 (Data1 _ cons) = \ x y d ->
-  case (findCon cons d) of
-  Val c rec kids -> do
-      w <- mapM_l (\z -> substD z x y) rec kids
-      return (to c w)
-substR1 _               = \ _ _ c -> return c
-
-substsR1 :: LFresh m => R1 (SubstD b) a -> [Name b] -> [b] -> a -> m a
-substsR1 (Data1 _ cons) = \ x y d ->
-  case (findCon cons d) of
-  Val c rec kids -> do
-      z <- mapM_l (\ w -> substsD w x y) rec kids
-      return (to c z)
-substsR1 _               = \ _ _ c -> return c
-
-instance Subst c AnyName where
-
-instance Subst b Int where
-instance Subst b Bool where
-instance Subst b () where
-instance Subst b Char where
-instance Subst b Integer where
-instance Subst b Float where
-instance Subst b Double where
-instance (Subst c a, Subst c b) => Subst c (a,b) where
-instance (Subst c a, Subst c b, Subst c d) => Subst c (a,b,d) where
-instance (Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a,b,d,e) where
-instance (Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a,b,d,e,f) where
-
-instance (Subst c a) => Subst c [a] where
-instance (Subst c a) => Subst c (Maybe a) where
-instance (Subst c a, Subst c b) => Subst c (Either a b) where
-
-instance Rep a => Subst b (R a) where
-instance Rep a => Subst b (Name a) where
-
-
-instance (Subst c a, Alpha a, Subst c b, Alpha b) =>
-    Subst c (Bind a b) where
-  lsubst n u (B a b) =
-      lfreshen' Term a ( \ a' p -> do
-         let b' = swapall' Term p b
-         a'' <- lsubst n u a'
-         b'' <- lsubst n u b'
-         return (B a'' b''))
-
-  lsubsts n u (B a b) =
-      lfreshen' Term a ( \ a' p -> do
-         a'' <- lsubsts n u a'
-         let b' = swaps' Pat p (swaps' Term p b)
-         b'' <- lsubsts n u b'
-         return (B a'' b''))
-
-instance (Subst c b, Subst c a, Alpha a, Alpha b) =>
-    Subst c (Rebind a b) where
-instance (Subst c a) => Subst c (Annot a) where
-
-
--------------------- TESTING CODE --------------------------------
-data Exp = V (Name Exp)
-         | A Exp Exp
-         | L (Bind (Name Exp) Exp) deriving (Show)
-
-$(derive [''Exp])
-
-instance Alpha Exp
-instance Subst Exp Exp where
-   isvar (V n) = Just (n, id)
-   isvar _     = Nothing
-
--- deriving instance Eq Exp
--- deriving instance Ord Exp
-
-nameA, nameB, nameC :: Name Exp
-nameA = string2Name "A"
-nameB = string2Name "B"
-nameC = string2Name "C"
-
-assert :: String -> Bool -> IO ()
-assert s True = return ()
-assert s False = print ("Assertion " ++ s ++ " failed")
-
-do_tests :: ()
-do_tests =
-   unsafePerformIO $ do
-   tests_aeq
-   tests_fv
-   tests_big
-   tests_subst
-
-perm = single (AnyName nameA)(AnyName nameB)
-
-naeq x y = not (aeq x y)
-
-a10a = bind (rebind (nameA, Annot nameC) ()) nameA
-a10b = bind (rebind (nameB, Annot nameC) ()) nameB
-
-a10c = bind (rebind (nameA, Annot nameA) ()) nameA
-a10d = bind (rebind (nameB, Annot nameA) ()) nameB
-
-tests_aeq = do
-   assert "a1" $ (bind nameA nameA) `naeq` (bind nameA nameB)
-   assert "a2" $ (bind nameA nameA) `aeq` (bind nameA nameA)
-   assert "a3" $ (bind nameA nameA) `aeq` (bind nameB nameB)
-   assert "a4" $ (bind nameA nameB) `naeq` (bind nameB nameA)
-   assert "a5" $ (bind (nameA, Annot nameB) nameA) `naeq`
-                 (bind (nameA, Annot nameC) nameA)
-   assert "a6" $ (bind (nameA, Annot nameB) nameA) `aeq`
-                 (bind (nameA, Annot nameB) nameA)
-   assert "a7" $ (bind (nameA, Annot nameB) nameA) `aeq`
-                 (bind (nameB, Annot nameB) nameB)
-   assert "a8" $ rebind nameA nameB `naeq` rebind nameB nameB
-   assert "a9" $ rebind nameA nameA `naeq` rebind nameB nameB
-   assert "a9a" $ (bind (rebind nameA (Annot nameA)) nameA) `aeq`
-                  (bind (rebind nameB (Annot nameB)) nameB)
-   assert "a10" $ bind (rebind (nameA, Annot nameA) ()) nameA `aeq`
-                  bind (rebind (nameB, Annot nameA) ()) nameB
-   assert "a10a" $ a10a `aeq` a10b
-   assert "a11" $ bind (rebind (nameA, Annot nameA) ()) nameA `naeq`
-                  bind (rebind (nameB, Annot nameB) ()) nameB
-   assert "a12" $ bind (Annot nameA) () `naeq` bind (Annot nameB) ()
-   assert "a13" $ bind (Annot nameA) () `aeq` bind (Annot nameA) ()
-   assert "a14" $ bind (rebind (Annot nameA) ()) () `naeq`
-                  bind (rebind (Annot nameB) ()) ()
-   assert "a15" $ (rebind (nameA, Annot nameA) ()) `naeq`
-                  (rebind (name4, Annot nameC) ())
-   assert "a16" $ bind (nameA, nameB) nameA `naeq` bind (nameB, nameA) nameA
-   assert "a17" $ bind (nameA, nameB) nameA `naeq` bind (nameA, nameB) nameB
-   assert "a18" $ (nameA, nameA) `naeq` (nameA, nameB)
-   assert "a19" $ match (nameA, nameA) (nameB, nameC) == Nothing
-   assert "a20" $ (L (bind name2 (L (bind name3 (L (bind name4  (A (V name2) (A (V name3) (V name4))))))))) `aeq`  (L (bind name1 (L (bind name2 (L (bind name3  (A (V name1) (A (V name2) (V name3)))))))))
-
-emptyNE :: Set (Name Exp)
-emptyNE = S.empty
-
-tests_fv = do
-   assert "f1" $ fv (bind nameA nameA) == emptyNE
-   assert "f2" $ fv' Pat (bind nameA nameA) == S.empty
-   assert "f3" $ fv (bind (rebind nameA (Annot nameA)) nameA) == emptyNE
-   assert "f4" $ fv (bind nameA nameB) == S.singleton nameB
-   assert "f5" $ fv (bind (nameA, Annot nameB) nameA) == S.singleton nameB
-   assert "f7" $ fv (bind (nameB, Annot nameB) nameB) == S.singleton nameB
-   assert "f8" $ fv (rebind nameA nameB) == S.fromList [nameA, nameB]
-   assert "f9" $ fv' Pat (rebind nameA nameA) == S.empty
-   assert "f9a" $ fv (rebind nameA (Annot nameA)) == S.singleton nameA
-   assert "f9b" $ fv' Pat (rebind nameA (Annot nameA)) == S.empty
-   assert "f10" $ fv (rebind (nameA, Annot nameA) ()) == S.singleton nameA
-   assert "f11" $ fv' Pat (rebind (nameA, Annot nameA) ()) == S.singleton (AnyName nameA)
-   assert "f10a" $ fv (rebind (nameA, Annot nameB) ()) == S.singleton nameA
-   assert "f11a" $ fv' Pat (rebind (nameA, Annot nameB) ()) == S.singleton (AnyName nameB)
-
-
-   assert "f12" $ fv (bind (Annot nameA) ()) == S.singleton nameA
-   assert "f12a" $ fv' Pat (bind (Annot nameA) ()) == S.singleton (AnyName nameA)
-
-   assert "f14" $ fv (rebind (Annot nameA) ()) == emptyNE
-   assert "f14a" $ fv' Pat (rebind (Annot nameA) ()) == S.singleton (AnyName nameA)
-
-tests_subst = do
-   assert "s1" $ subst nameA (V nameB) (V nameA) `aeq` (V nameB)
-   assert "s2" $ subst nameA (V nameB) (V nameC) `aeq` (V nameC)
-   assert "s3" $ subst nameA (V nameB) (L (bind nameA (V nameA))) `aeq`
-                                       (L (bind nameA (V nameA)))
-
-   assert "s4" $ subst nameA (V nameB) (L (bind nameB (V nameB))) `aeq`
-                                       (L (bind nameA (V nameA)))
-
-   assert "s5" $ subst nameA (V nameB) (L (bind nameC (V nameA))) `aeq`
-                                       (L (bind nameC (V nameB)))
-
-   assert "s6" $ subst nameA (V nameA) (L (bind nameC (V nameA))) `aeq`
-                                       (L (bind nameC (V nameA)))
-
-   assert "s7" $ subst nameA (V nameA) (L (bind nameA (V nameB))) `aeq`
-                                       (L (bind nameA (V nameB)))
-   assert "s9" $ subst name1 (V name1)
-                  (L (bind name1 (L (bind name2 (L (bind name3
-                           (A (V name1) (A (V name2) (V name3))))))))) `aeq`
-                  (L (bind name1 (L (bind name2 (L (bind name3
-                           (A (V name1) (A (V name2) (V name3)))))))))
-
-
-mkbig :: [Name Exp] -> Exp -> Exp
-mkbig (n : names) body =
-    L (bind n (mkbig names (A (V n) body)))
-mkbig [] body = body
-
-big1 = mkbig (map integer2Name (take 100 [1 ..])) (V name11)
-big2 = mkbig (map integer2Name (take 101 [1 ..])) (V name11)
-
-tests_big = do
-   assert "b1" $ big1 `naeq` big2
-   assert "b2" $ fv big1 == emptyNE
-   assert "b3" $ big1 `aeq` subst name11 (V name11) big1
-
-

@@ -1,115 +0,0 @@-------------------------------------------------------------------------- |--- Module      :  Generics.RepLib.Bind.Perm--- Copyright   :  ???--- License     :  BSD------ Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>--- Stability   :  experimental--- Portability :  portable------ A slow, but hopefully correct implementation of permutations.----------------------------------------------------------------------------module Generics.RepLib.Bind.PermM (-    Perm, single, (<>), apply, support, isid, join, empty, restrict-  ) where--import Data.List-import Data.Map (Map)-import qualified Data.Map as Map-import System.IO.Unsafe--newtype Perm a = Perm (Map a a)--instance Ord a => Eq (Perm a) where-  (Perm p1) == (Perm p2) =-    all (\x -> Map.findWithDefault x x p1 == Map.findWithDefault x x p2) (Map.keys p1) &&-    all (\x -> Map.findWithDefault x x p1 == Map.findWithDefault x x p2) (Map.keys p2)--instance Show a => Show (Perm a) where-  show (Perm p) = show p---apply :: Ord a => Perm a -> a -> a-apply (Perm p) x = Map.findWithDefault x x p--single :: Ord a => a -> a -> Perm a-single x y = if x == y then Perm Map.empty else-    Perm (Map.insert x y (Map.insert y x Map.empty))--empty :: Perm a-empty = Perm Map.empty---- | Compose two permutations.  The right-hand permutation will be---   applied first.-(<>) :: Ord a => Perm a -> Perm a -> Perm a-(Perm b) <> (Perm a) =-  Perm (Map.fromList ([ (x,Map.findWithDefault y y b) | (x,y) <- Map.toList a]-         ++ [ (x, Map.findWithDefault x x b) | x <- Map.keys b, Map.notMember x a]))---- | isid -- do all keys map to themselves?-isid :: Ord a => Perm a -> Bool-isid (Perm p) =-     Map.foldrWithKey (\ a b r -> r && a == b) True p---- | Join two permutation. Fail if the two permutations map the same--- name to two different variables.-join :: Ord a => Perm a -> Perm a -> Maybe (Perm a)-join (Perm p1) (Perm p2) =-     let overlap = Map.intersectionWith (\x y -> (x,y)) p1 p2 in-     if Map.fold (\ (n1, n2) b -> b && n1 == n2) True overlap then-       Just (Perm (Map.union p1 p2))-       else Nothing--support :: Ord a => Perm a -> [a]-support (Perm p) = [ x | x <- Map.keys p, Map.findWithDefault x x p /= x]--restrict :: Ord a => Perm a -> [a] -> Perm a-restrict (Perm p) l = Perm (foldl' (\p' k -> Map.delete k p') p l)------------------------------------------------------------------------seteq :: Ord a => [a] -> [a] -> Bool-seteq x y = nub (sort x) == nub (sort y)---assert :: String -> Bool -> IO ()-assert s True = return ()-assert s False = print ("Assertion " ++ s ++ " failed")--do_tests :: ()-do_tests =-   unsafePerformIO $ do-     tests_apply-     tests_isid-     tests_support-     tests_join--tests_join = do-  assert "j1" $ join empty (empty :: Perm Int) == Just empty-  assert "j2" $ join (single 1 2) empty == Just (single 1 2)-  assert "j3" $ join (single 1 2) (single 2 1) == Just (single 1 2)-  assert "j4" $ join (single 1 2) (single 1 3) == Nothing--tests_apply = do-  assert "a1" $ apply empty 1 == 1-  assert "a2" $ apply (single 1 2) 1 == 2-  assert "a3" $ apply (single 2 1) 1 == 2-  assert "a4" $ apply ((single 1 2) <> (single 2 1)) 1 == 1--tests_isid = do-  assert "i1" $ isid (empty :: Perm Int) == True-  assert "i2" $ isid (single 1 2) == False-  assert "i3" $ isid (single 1 1) == True-  assert "i4" $ isid ((single 1 2) <> (single 1 2)) == True-  assert "i5" $ isid ((single 1 2) <> (single 2 1)) == True-  assert "i6" $ isid ((single 1 2) <> (single 3 2)) == False--tests_support = do-  assert "s1" $ support (empty :: Perm Int) `seteq` []-  assert "s2" $ support (single 1 2) `seteq` [1,2]-  assert "s3" $ support (single 1 1) `seteq` []-  assert "s4" $ support ((single 1 2) <> (single 1 2)) `seteq` []-  assert "s5" $ support ((single 1 2) <> (single 2 1)) `seteq` []-  assert "s6" $ support ((single 1 2) <> (single 3 2)) `seteq` [1,2,3]

@@ -1,6 +1,6 @@ ----------------------------------------------------------------------------- -- --- Copyright   :  (c) 2006-2010, RepLib team (see LICENSE)+-- Copyright   :  (c) 2006-2011, RepLib team (see LICENSE) -- License     :  BSD --  -- Maintainer  :  sweirich@cis.upenn.edu, byorgey@cis.upenn.edu@@ -32,14 +32,6 @@ Generics.RepLib.SYB.Schemes - SYB: Port of Data.Generics.Schemes  RepLib                      - Top-level module that re-exports all of the above--Generics.RepLib.Bind.LocallyNameless-                             - Tools for generic programming with-                               binders (alpha renaming, substitution,-                               unification, etc.)--Generics.RepLib.Bind.Nominal - Tools for generic programming with-                               binders (alternate implementation)  To use this library, import RepLib and derive representations of your datatypes. The "Lib" module contains a number of type-indexed

@@ -1,26 +1,25 @@ name:           RepLib-version:        0.3+version:        0.4.0 license:        BSD3 license-file:   LICENSE build-type:     Simple cabal-version:  >= 1.6 tested-with:    GHC == 7.0.1 author:         Stephanie Weirich-maintainer:     Chris Casinghino <ccasin@cis.upenn.edu>-                Brent Yorgey <byorgey@cis.upenn.edu>+maintainer:     Brent Yorgey <byorgey@cis.upenn.edu>+		Chris Casinghino <ccasin@cis.upenn.edu>                 Stephanie Weirich <sweirich@cis.upenn.edu> homepage:       http://code.google.com/p/replib/ category:       Generics-extra-source-files: README, -                    examples/*.hs+extra-source-files: README synopsis:       Generic programming library with representation types description:    Generic programming library providing structural-                polymorphism, simple programming with binders, and other features.+                polymorphism and other features.  Library   build-depends: base >= 4.3 && < 5, -                 template-haskell >= 2.4 && < 2.6, mtl >= 1.1 && < 2.1,-                 containers >= 0.3 && < 0.5+                 template-haskell >= 2.4 && < 2.6, +                 mtl >= 2.0 && < 2.1    exposed-modules:     Generics.RepLib,     Generics.RepLib.R,@@ -32,8 +31,5 @@     Generics.RepLib.Derive,     Generics.RepLib.SYB.Aliases,     Generics.RepLib.SYB.Schemes,-    Generics.RepLib.Unify,-    Generics.RepLib.Bind.Nominal,-    Generics.RepLib.Bind.LocallyNameless,-    Generics.RepLib.Bind.PermM+    Generics.RepLib.Unify   extensions: GADTs

@@ -1,185 +0,0 @@--- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses  #-}--------------------------------------------------------------------------------- |--- Module      :  Main--- Copyright   :  (c) The University of Pennsylvania, 2006--- License     :  BSD------ Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------ A file demonstrating the use of RepLib-----------------------------------------------------------------------------------module Basic where--import Generics.RepLib-import Language.Haskell.TH----- For each datatype that we define, we need to also create its representation.--- The template Haskell function derive does this automatically for--- each type.--data Tree a = Leaf a | Node (Tree a) (Tree a)-$(derive [''Tree])--data Day = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday--$(derive [''Day])---- Note, for mutually recursive datatypes, use "derive" and give list--- of type names.---- Note also that the functions of RepLib can cooperate with the--- traditional 'deriving' mechanism-data Company   = C [Dept]                 deriving (Eq, Ord, Show)-data Dept      = D String Manager [CUnit] deriving (Eq, Ord, Show)-data Manager   = M Employee               deriving (Eq, Ord, Show)-data CUnit     = PU Employee | DU Dept    deriving (Eq, Ord, Show)-data Employee  = E Person Salary          deriving (Eq, Ord, Show)-data Person    = P String                 deriving (Eq, Ord, Show)-data Salary    = S Float                  deriving (Eq, Ord, Show)--$(derive-    [''Company,-     ''Dept,-     ''CUnit,-     ''Employee,- 	  ''Manager,- 	  ''Person,- 	  ''Salary])-------- Some sample data for these types----t1 :: Tree Int-t1 = Node (Node (Leaf 3) (Leaf 4)) (Node (Leaf 5) (Leaf 6))--t2 :: Tree Int-t2 = Node (Node (Leaf 0) (Leaf 7)) (Leaf 20)--s1 :: Company-s1 = C [D "Types" (M (E (P "Stephanie") (S 1000.0)))-            [PU (E (P "Michael") (S 50)),-             PU (E (P "Samuel") (S 50)),-             PU (E (P "Theodore") (S 50))],-        D "Terms" (M (E (P "Stephanie") (S 200)))-            [DU (D "Shipping" (M (E (P "Alice") (S 3000)))-                [])]]-------- Prelude operations.------ Note that we didn't derive Eq, Ord, Bounded or Show for "Day" and "Tree". We can--- do that now with operations from RepLib.PreludeLib.---- for Day-instance Eq Day      where-  (==) = eqR1 rep1-instance Ord Day     where-  compare = compareR1 rep1-instance Bounded Day where-  minBound = minBoundR1 rep1-  maxBound = maxBoundR1 rep1-instance Show Day    where-  showsPrec = showsPrecR1 rep1---- for Tree-instance (Rep a, Eq a) => Eq (Tree a)     where (==) = eqR1 rep1-instance (Rep a, Show a) => Show (Tree a) where showsPrec = showsPrecR1 rep1-instance (Rep a, Ord a) => Ord (Tree a)   where compare = compareR1 rep1---- Besides the prelude operations, RepLib provides a number of other--- type-indexed operations.------- Instances for RepLib.Lib operations------- Generate creates arbitrary elements of a type, up to a certain depth.-instance Generate Day-instance Generate a => Generate (Tree a)-instance Generate Company-instance Generate Dept-instance Generate Manager-instance Generate CUnit-instance Generate Employee-instance Generate Person-instance Generate Salary----- Sum adds together all of the Ints in a datastructure-instance GSum a => GSum (Tree a)-instance GSum Company-instance GSum Dept-instance GSum Manager-instance GSum CUnit-instance GSum Employee-instance GSum Person-instance GSum Salary---- Shrink creates smaller versions of a data structure.-instance Shrink a => Shrink (Tree a)------- SYB Style operations------ RepLib also supports many of the combinators from the SYB library. For example,--- we can include the following code from the "Paradise" benchmark that gives everyone--- in the company a raise.---- Increase salary by percentage-increase :: Float -> Company -> Company-increase k = everywhere (mkT (incS k))---- "interesting" code for increase-incS :: Float -> Salary -> Salary-incS k (S s) = S (s * (1+k))-------- Generalized folds------ finally, we define generalized versions of fold left and--- fold right for the Tree type constructor.-instance Fold Tree where-  foldRight op = rreduceR1 (rTree1 (RreduceD { rreduceD = op })-                                   (RreduceD { rreduceD = foldRight op}))-  foldLeft  op = lreduceR1 (rTree1 (LreduceD { lreduceD = op })-                                   (LreduceD { lreduceD = foldLeft op }))--assert :: String -> Bool -> IO ()-assert s True  = return ()-assert s False = print ("Assertion " ++ s ++ " failed")---main = do-   assert "m1" (minBound == Monday)-   assert "m2" (maxBound == Sunday)--   assert "e1" (t1 == Node (Node (Leaf 3) (Leaf 4)) (Node (Leaf 5) (Leaf 6)))--   assert "o3" (Monday < Tuesday)-   assert "o4" (not (t1 < t2))----   assert "g1" (generate 7 == [Monday,Tuesday,Wednesday,Thursday,Friday,Saturday,Sunday])-   assert "g2" ((generate 3 :: [Tree Int]) == [Leaf 0,Leaf 1,Leaf 2,Node (Leaf 0) (Leaf 0),Node (Leaf 0) (Leaf 1),Node (Leaf 0) (Node (Leaf 0) (Leaf 0)),Node (Leaf 1) (Leaf 0),Node (Leaf 1) (Leaf 1),Node (Leaf 1) (Node (Leaf 0) (Leaf 0)),Node (Node (Leaf 0) (Leaf 0)) (Leaf 0),Node (Node (Leaf 0) (Leaf 0)) (Leaf 1),Node (Node (Leaf 0) (Leaf 0)) (Node (Leaf 0) (Leaf 0))])-----   assert "s1" (subtrees t1 == [Node (Leaf 3) (Leaf 4),Node (Leaf 5) (Leaf 6)])-   assert "s2" (gsum t1 == 18)-   assert "s3" (gsum t2 == 27)----   assert "i1" (increase 0.1 s1 == C [D "Types" (M (E (P "Stephanie") (S 1100.0))) [PU (E (P "Michael") (S 55.0)),PU (E (P "Samuel") (S 55.0)),PU (E (P "Theodore") (S 55.0))],D "Terms" (M (E (P "Stephanie") (S 220.0))) [DU (D "Shipping" (M (E (P "Alice") (S 3300.0))) [])]])--   assert "i2" (s1 < (increase 0.2 s1))----   assert "f1" (gproduct t1 == 360)-   assert "f2" (count t1 == 4)-

@@ -1,102 +0,0 @@--- Untyped lambda calculus, with small-step evaluation and an example parser--{-# LANGUAGE PatternGuards-           , MultiParamTypeClasses-           , TemplateHaskell-           , ScopedTypeVariables-           , FlexibleInstances-           , FlexibleContexts-           , UndecidableInstances-  #-}-import Control.Applicative-import Control.Arrow-import Control.Monad.Reader--import Control.Monad.Trans.Maybe--import Text.Parsec hiding ((<|>))-import qualified Text.Parsec.Token as P-import Text.Parsec.Language (haskellDef)--import Generics.RepLib.Bind.LocallyNameless-import Generics.RepLib--data Term = Var (Name Term)-          | App Term Term-          | Lam (Bind (Name Term) Term)-  deriving Show--$(derive [''Term])--instance Alpha Term-instance Subst Term Term where-  isvar (Var v) = Just (v, id)-  isvar _       = Nothing--isValue (App _ _) = False-isValue _         = True--done :: Monad m => MaybeT m a-done = MaybeT $ return Nothing--instance (Functor m, LFresh m) => LFresh (MaybeT m) where-  lfresh    = MaybeT . fmap Just . lfresh-  avoid nms = MaybeT . avoid nms . runMaybeT--step :: (Functor m, LFresh m) => Term -> MaybeT m Term-step (Var _) = done-step (Lam _) = done-step (App (Lam b) t2) =-  lunbind b $ \(x,t1) ->-    return (subst x t2 t1)-step (App t1 t2) =-      App <$> step t1 <*> pure t2-  <|> App <$> pure t1 <*> step t2--tc :: Monad m => (a -> MaybeT m a) -> (a -> m a)-tc f a = do-  ma' <- runMaybeT (f a)-  case ma' of-    Just a' -> tc f a'-    Nothing -> return a--eval :: Term -> Term-eval x = runReader (tc step x) (0::Integer)---- Some example terms--nm = string2Name--idT = Lam (bind (nm "y") (Var (nm "y")))--foo = Lam (bind (nm "z") (Var (nm "y")))--trueT  = Lam (bind (nm "x") (Lam (bind (nm "y") (Var (nm "x")))))--- falseT = Lam (bind (nm "x") (Lam (bind (nm "x") (Var (nm "x")))))--- above doesn't work like I would expect!--falseT = Lam (bind (nm "x") (Lam (bind (nm "y") (Var (nm "y")))))---- A small parser for Terms-lexer = P.makeTokenParser haskellDef--parens = P.parens lexer-var    = P.identifier lexer-op     = P.symbol lexer--parseTerm = parseAtom `chainl1` (pure App)--parseAtom = parens parseTerm-         <|> (Var . string2Name <$> var)-         <|> Lam <$> (bind <$> (op "\\" *> (string2Name <$> var))-                           <*> (op "." *> parseTerm))--runTerm :: String -> Either ParseError Term-runTerm = (id +++ eval) . parse parseTerm ""--{- example, 2 + 3 = 5:--  *Main> runTerm "(\\m. \\n. \\s. \\z. m s (n s z)) (\\s. \\z. s (s z)) (\\s. \\z. s (s (s z))) s z"-  Right (App (Var s) (App (Var s) (App (Var s) (App (Var s) (App (Var s) (Var z))))))---}

@@ -1,145 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,-    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,-    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving- #-}--------------------------------------------------------------------------------- |--- Module      :  LC--- Copyright   :  (c) The University of Pennsylvania, 2010--- License     :  BSD------ Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------------------------------------------------------------------------------------------- | A very simple example demonstration of the binding library--- based on the untyped lambda calculus.-module LC where--import Generics.RepLib-import Generics.RepLib.Bind.LocallyNameless-import Control.Monad.Reader (Reader, runReader)-import Data.Set as S---- | A Simple datatype for the Lambda Calculus-data Exp = Var Name-         | Lam (Bind Name Exp)-         | App Exp Exp-  deriving Show---- Use RepLib to derive representation types-$(derive [''Exp])---- | With representation types, tbe default implementation of Alpha--- provides alpha-equivalence and free variable calculation.-instance Alpha Exp---- | Equivalence for bind expressions is alpha equivalence. So we can't derive Eq--- for Exp until we've first made it a member of the Alpha class-deriving instance Eq Exp---- | The subst class uses generic programming to implement capture--- avoiding substitution. It just needs to know where the variables--- are.-instance Subst Exp Exp where-   isvar (Var x) = Just (x,id)-   isvar _       = Nothing----- | All new functions should be defined in a monad that can generate--- locally fresh names. One such monad is the Reader Monad. (Automatically--- a member of the class LFresh.)-type M a = Reader Integer a---- | Beta-Eta equivalence for lambda calculus terms.--- If the terms have a normal form--- then the algorithm will terminate. Otherwise, the algorithm may--- loop for certain inputs.-(=~) :: Exp -> Exp -> M Bool-e1 =~ e2 | e1 == e2 = return True-e1 =~ e2 = do-    e1' <- red e1-    e2' <- red e2-    if e1' == e1 && e2' == e2-      then return False-      else e1' =~ e2'----- | Parallel beta-eta reduction for lambda calculus terms.--- Do as many reductions as possible in one step, while still ensuring--- termination.-red :: Exp -> M Exp-red (App e1 e2) = do-  e1' <- red e1-  e2' <- red e2-  case e1' of-    -- look for a beta-reduction-    Lam bnd ->-      lunbind bnd $ \ (x, e1'') ->-        return $ subst x e2' e1''-    otherwise -> return $ App e1' e2'-red (Lam bnd) = lunbind bnd $ \ (x, e) -> do-   e' <- red e-   case e of-     -- look for an eta-reduction-     App e1 (Var y) | y == x && x `S.notMember` fv e1 -> return e1-     otherwise -> return (Lam (bind x e'))-red (Var x) = return $ (Var x)--------------------------------------------------------------------------- Some testing code to demonstrate this library in action.--assert :: String -> Bool -> IO ()-assert s True  = return ()-assert s False = print ("Assertion " ++ s ++ " failed")--assertM :: String -> M Bool -> IO ()-assertM s c =-  if (runReader c (0 :: Integer)) then return ()-  else print ("Assertion " ++ s ++ " failed")--x :: Name-x = string2Name "x"--y :: Name-y = string2Name "y"--z :: Name-z = string2Name "z"--s :: Name-s = string2Name "s"--lam :: Name -> Exp -> Exp-lam x y = Lam (bind x y)--zero  = lam s (lam z (Var z))-one   = lam s (lam z (App (Var s) (Var z)))-two   = lam s (lam z (App (Var s) (App (Var s) (Var z))))-three = lam s (lam z (App (Var s) (App (Var s) (App (Var s) (Var z)))))--plus = lam x (lam y (lam s (lam z (App (App (Var x) (Var s)) (App (App (Var y) (Var s)) (Var z))))))--true = lam x (lam y (Var x))-false = lam x (lam y (Var y))-if_ x y z = (App (App x y) z)--main :: IO ()-main = do-  -- \x.x == \x.y-  assert "a1" $ lam x (Var x) == lam y (Var y)-  -- \x.x /= \x.y-  assert "a2" $ lam x (Var y) /= lam x (Var x)-  -- \x.(\y.x) (\y.y) == \y.y-  assertM "be1" $ lam x (App (lam y (Var x)) (lam y (Var y))) =~ (lam y (Var y))-  -- \x. f x === f-  assertM "be2" $ lam x (App (Var y) (Var x)) =~ Var y-  assertM "be3" $ if_ true (Var x) (Var y) =~ Var x-  assertM "be4" $ if_ false (Var x) (Var y) =~ Var y-  assertM "be5" $ App (App plus one) two =~ three-

@@ -1,71 +0,0 @@-{- Type checker for LF, based on algorithm in Harper and Pfennig, "On-   Equivalence and Canonical Forms in the LF Type Theory", ACM-   Transactions on Computational Logic, 2000.--}--{-# LANGUAGE TemplateHaskell-           , ScopedTypeVariables-           , FlexibleInstances-           , MultiParamTypeClasses-           , FlexibleContexts-           , UndecidableInstances-  #-}--module LF where--import Generics.RepLib.Bind.LocallyNameless-import Generics.RepLib--import qualified Data.Set as S---- Kinds-data Kind = KPi (Bind (Name Tm, Annot Ty) Kind) -- {x:ty} k-          | Type                                -- type-  deriving Show---- Types, also called "Families"-data Ty   = TyPi (Bind (Name Tm, Annot Ty) Ty)  -- {x:ty} ty-          | TyApp Ty Tm                         -- ty tm-          | TyConst (Name Ty)                   -- a-  deriving Show---- Terms, also called "Objects"-data Tm   = Lam (Bind (Name Tm, Annot Ty) Tm)   -- [x:ty] tm-          | TmApp Tm Tm                         -- tm tm-          | TmVar (Name Tm)                     -- x-  deriving Show-  -- Note, Harper and Pfennig distinguish between term variables and-  -- constants.  Variables are things which can be bound by a lambda-  -- or pi; constants are things which are bound in a signature.  For-  -- our purposes there is little value in distinguishing between-  -- them.--$(derive [''Kind, ''Ty, ''Tm])--instance Alpha Kind-instance Alpha Ty-instance Alpha Tm---- There are no term variables in types or kinds, so we can just--- use the default structural Subst instances.-instance Subst Tm Kind-instance Subst Tm Ty---- For Tm we must implement isvar so the Subst instance knows about--- term variables.-instance Subst Tm Tm where-  isvar (TmVar v) = Just (v, id)-  isvar _         = Nothing---- A declaration is either a type constant declaration (a name and a kind)--- or a term constant declaration (a name, type, and optional definition).-data Decl = DeclTy (Name Ty) (Annot Kind)-          | DeclTm (Name Tm) (Annot Ty) (Maybe (Annot Tm))  -- is this right?---- A program is a sequence of declarations, where each name is bound--- in the remainder of the program.-data Prog = Nil-          | Cons (Bind Decl Prog)---- A signature is a set of declarations.-type Sig = S.Set Decl

@@ -1,31 +0,0 @@--- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances -{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses  #-}--------------------------------------------------------------------------------- |--- Module      :  Main--- Copyright   :  (c) The University of Pennsylvania, 2006--- License     :  BSD--- --- Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------ Testsuite-----------------------------------------------------------------------------------module Main where--import qualified Basic-import qualified LC-import qualified STLC-import qualified Abstract---main = do-     Basic.main-     LC.main-     STLC.main-     Abstract.main-     print "Tests completed"-     

@@ -1,193 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,-    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,-    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving- #-}--------------------------------------------------------------------------------- |--- Module      :  STLC--- Copyright   :  (c) The University of Pennsylvania, 2010--- License     :  BSD------ Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable-----------------------------------------------------------------------------------------module STLC where--import Generics.RepLib-import Generics.RepLib.Bind.LocallyNameless-import Control.Monad.Reader-import Data.Set as S--data Ty = TInt | TUnit | Arr Ty Ty-  deriving (Show, Eq)-data Exp = Lit Int | Var Name | Lam (Bind Name Exp) | App Exp Ty Exp | EUnit-  deriving Show---- Use RepLib to derive representation types-$(derive [''Ty,''Exp])---- With representation types, default implementations of these--- classes are available.-instance Alpha Ty where-instance Alpha Exp where--instance Subst Exp Ty where-instance Subst Exp Exp where-   isvar (Var x) = Just (x,id)-   isvar _       = Nothing---- Equivalence for expressions is alpha equivalence. So we can't derive Eq--- until we've made it a member of the Alpha class-deriving instance Eq Exp--type Ctx = [(Name, Ty)]---- A monad that can generate locally fresh names-type M a = Reader Integer a---- A type checker for STLC terms-tc :: Ctx -> Exp -> Ty -> M Bool-tc g (Var n) ty =-  case lookup n g of-    Just ty' -> return (ty == ty')-    Nothing  -> return False-tc g (Lam bnd) (Arr t1 t2) = do-  lunbind bnd $ \ (x , e) ->-    tc ((x,t1) : g) e t2-tc g (App e1 t1 e2) t2= do-  b1 <- tc g e1 (Arr t1 t2)-  b2 <- tc g e2 t1-  return $ b1 && b2-tc g EUnit TUnit = return True-tc g (Lit i) TInt = return True-tc g e t = return False----- beta-eta equivalence, from Karl Crary's ATTAPL chapter--- assumes both terms type check-algeq :: Exp -> Exp -> Ty -> M Bool-algeq e1 e2 TInt  = do-  e1' <- wh e1-  e2' <- wh e2-  patheq e1' e2'-algeq e1 e2 TUnit = return True-algeq e1 e2 (Arr t1 t2) = do-  x <- lfresh name1-  algeq (App e1 t1 (Var x)) (App e2 t1 (Var x)) t2---- path equivalence (for terms in weak-head normal form)-patheq :: Exp -> Exp -> M Bool-patheq (Var x) (Var y) | x == y = return True-patheq (Lit x) (Lit y) | x == y = return True-patheq (App e1 ty e2) (App e1' ty' e2') | ty == ty' = do- b1 <- patheq e1 e1'- b2 <- algeq e2 e2' ty- return $ b1 && b2-patheq _ _ = return False---- weak-head reduction-wh :: Exp -> M Exp-wh (App e1 ty e2) = do-   e1' <- wh e1-   case e1' of-     Lam bnd ->-       lunbind bnd $ \ (x, e1') ->-       wh (subst x e2 e1')-     _ -> return $ App e1' ty e2-wh e = return e----- A different equivalence algorithm, based on reduce and compare.---- (Doesn't support eta equivalences for the unit type.)---- Parallel beta-eta reduction, prefers beta reductions to--- eta reductions-red :: Exp -> M Exp-red (App e1 t e2) = do-  e1' <- red e1-  e2' <- red e2-  case e1' of-    Lam bnd ->-      lunbind bnd $ \ (x, e1'') ->-        return $ subst x e2' e1''-    _ -> return $ App e1' t e2'-red (Lam bnd) =-   lunbind bnd $ \ (x, e) -> do-    e' <- red e-    case e of-     -- look for an eta-reduction-     App e1 t (Var y) | y == x && x `S.notMember` fv e1 -> return e1-     otherwise -> return e-red e = return $ e---- Reduce both sides until you find a match.-redcomp :: Exp -> Exp -> M Bool-redcomp e1 e2 = if e1 == e2 then return True                                         else do-    e1' <- red e1-    e2' <- red e2-    if e1' == e1 && e2' == e2-      then return False-      else redcomp e1' e2'-------------------------------------------------------------------------- TDPE ???-{--data RExp a where-   RVar  :: Name a -> RExp a-   RLam  :: (Bind (Name b) (Exp b)) -> Exp (a -> b)-   RApp  :: RExp (a -> b) -> (RExp a) -> RExp b-   RUnit :: RExp ()--reify   :: (Fresh m, Rep a) => Exp a -> m a-reify e = case rep of-           Unit -> return ()-           (Arr a b) -> do-              e' <- reflect x --here's the rub!-              return $ \ x -> reify (RApp e e')--reflect :: (Fresh m, Rep a) => a -> m (RExp a)-reflect m = case rep of-   Unit -> return RUnit-   (Arr a b) -> do-      x <- fresh "x"-      e' <- reflect (m (reify (RVar x)))-      return $ RLam (bind x e')--}------------------------------------------------------------------------assert :: String -> Bool -> IO ()-assert s True  = return ()-assert s False = print ("Assertion " ++ s ++ " failed")--assertM :: (a -> Bool) -> String -> M a -> IO ()-assertM f s c =-  if f (runReader c (0 :: Integer)) then return ()-  else print ("Assertion " ++ s ++ " failed")---main :: IO ()-main = do-  -- \x.x == \x.y-  assert "a1" $ Lam (bind name1 (Var name1)) == Lam (bind name2 (Var name2))-  -- \x.x /= \x.y-  assert "a2" $ Lam (bind name1 (Var name2)) /= Lam (bind name1 (Var name1))-  -- [] |- \x. x : () -> ()-  assertM id "tc1" $ tc [] (Lam (bind name1 (Var name1))) (Arr TUnit TUnit)-  -- [] |- \x. x ()  : (Unit -> Int) -> Int-  assertM id "tc2" $ tc []-     (Lam (bind name1-        (App (Var name1) TUnit EUnit))) (Arr (Arr TUnit TInt) TInt)-  -- \x. x  === \x. () :: Unit -> Unit-  assertM id "be1" $-     algeq (Lam (bind name1 (Var name1)))-           (Lam (bind name2 EUnit))-           (Arr TUnit TUnit)-  -- \x. f x === f  :: Int -> Int-  assertM id "be2" $-     algeq (Lam (bind name1 (App (Var name2) TInt (Var name1))))-           (Var name2)-           (Arr TInt TInt)

@@ -1,161 +0,0 @@-{-# OPTIONS -fglasgow-exts #-}-{-# OPTIONS -fallow-undecidable-instances #-}-{-# OPTIONS -fallow-overlapping-instances #-}-{-# OPTIONS -fth #-}---------------------------------------------------------------------------------- |--- Module      :  UnifyExp--- Copyright   :  (c) Ben Kavanagh 2008--- License     :  BSD------ Maintainer  :  ben.kavanagh@gmail.com--- Stability   :  experimental--- Portability :  non-portable------ A file demonstrating the use of Generics.Replib.Unify-----------------------------------------------------------------------------------module UnifyExp-where--import Generics.RepLib-import Generics.RepLib.Unify-import Test.HUnit-import Control.Monad.Error----data Exp = Var Int-	 | Plus Exp Exp-	 | K String-	 deriving (Show, Eq)-$(derive [''Exp])--instance HasVar Int Exp where-    is_var (Var i) = Just i-    is_var _ = Nothing-    var = Var---- A = "f" ==> [(A, "f")]-test1 :: Maybe [(Int, Exp)]-test1 = solveUnification [(Var 1, K "f")]----- A = "f" + A  ==>   fails occurs check-test2 :: Maybe [(Int, Exp)]-test2 = solveUnification [(Var 1, Plus (K "f") (Var 1))]----- A + B = B + B ==> A = B-test3 :: Maybe [(Int, Exp)]-test3 = solveUnification [(Plus (Var 1) (Var 2), Plus (Var 2) (Var 2))]---- A + B = B + C ==> [(A, C), (B, C)]-test4 :: Maybe [(Int, Exp)]-test4 = solveUnification [(Plus (Var 1) (Var 2), Plus (Var 2) (Var 3))]-----data Term = TVar Int-	  | K2 String-	  | App Term Term-	 deriving (Show, Eq)-$(derive [''Term])--instance HasVar Int Term where-    is_var (TVar i) = Just i-    is_var _ = Nothing-    var = TVar---- There are two ways to override the unify [Char] [Char] problem. the first is to implement--- unify and only offer the case for K2, defaulting to generic unify in other cases. The other--- is to implement unify for String using equality, overriding the default Cons/Nil case handling----- special instance of unify for String--- Writing an instance for String which leaves 'special' term 'a' abstract has a problem with case a = String,--- which leads to overlap with a a case.. So we can only specialise String for a known 'special' term (here Term)-instance (Eq n, Show n, HasVar n Term) => Unify n Term String where-    unifyStep _ x y = if x == y-		      then return ()-		      else throwError $ strMsg ("unify failed when testing equality for " ++ show x ++ " = " ++ show y)------- f(g(A)) = f(B)  ==>   [(B, g(A))]-test5 :: Maybe [(Int, Term)]-test5 = solveUnification [(App (K2 "f") (App (K2 "g") (TVar 1)), App (K2 "f") (TVar 2))]----- f(g(A), A) = f(B, xyz) ==> [(A, xyz), (B, g(xyz))]-test6 :: Maybe [(Int, Term)]-test6 = solveUnification [(App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1), App (App (K2 "f") (TVar 2)) (K2 "xyz"))]---- f(A) = f(B, C) ==> fail. constructor mismatch. App vs K2. This is in essence an 'arity' failure.--- in a term datatype that had Application as an arity plus list, the arity would not be equal and would call failure.--- I'm not sure the error message would be adequate. Perhaps I could use a typeclass/newtype to get better error messages--- on equality failures.-test7 :: Maybe [(Int, Term)]-test7 = solveUnification [(App (K2 "f") (TVar 1),  App (App (K2 "f") (TVar 2)) (TVar 3))]---- f(A) = f(B) ==> [(A, B)]-test8 :: Maybe [(Int, Term)]-test8 = solveUnification [(App (K2 "f") (TVar 1), App (K2 "f") (TVar 2))]---- A = B, B = abc  ==>  [(B, abc), (A, abc)]-test9 :: Maybe [(Int, Term)]-test9 = solveUnification [(TVar 1, TVar 2), (TVar 2, K2 "abc")]---- A = abc, xyz = X, A = X  ==>  fails with built in equality since we effectively ask abc = xyz-test10 :: Maybe [(Int, Term)]-test10 = solveUnification [(TVar 1, K2 "abc"), (K2 "xyz", TVar 2), (TVar 1, TVar 2)]------ Test that unification works with surrounding term structure (other datatypes) which are closed, i.e. they have no free variables.-data OuterTerm =  K3 String-	       | Inner Term-	       | App3 OuterTerm OuterTerm-	 deriving (Show, Eq)-$(derive [''OuterTerm])----- H(f(g(A), A)) = H(f(B, xyz)) ==> [(A, xyz), (B, g(xyz))]  where H is outer-test11 :: Maybe [(Int, Term)]-test11 = solveUnification'-	   (undefined :: Proxy (Int, Term))-	   [(App3 (K3 "H") (Inner $ App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1)),-	     App3 (K3 "H") (Inner $ App (App (K2 "f") (TVar 2)) (K2 "xyz")))]----- H(f(g(A), A)) = H(f(B, xyz)) ==> [(A, xyz), (B, g(xyz))]  where H is outer-test12 :: Maybe [(Int, Term)]-test12 = solveUnification'-	   (undefined :: Proxy (Int, Term))-	   [(App3 (K3 "H") (Inner $ App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1)),-	     App3 (K3 "I") (Inner $ App (App (K2 "f") (TVar 2)) (K2 "xyz")))]------- todo. fix tests so that errors are tested properly.-tests = test [ test1 ~?= Just [(1,K "f")],-	       test2 ~?= error "***Exception: occurs check failed",-	       test3 ~?= Just [(1,Var 2)],-	       test4 ~?= Just [(1,Var 3),(2,Var 3)],-	       test5 ~?= Just [(2,App (K2 "g") (TVar 1))],-	       test6 ~?= Just [(2,App (K2 "g") (K2 "xyz")),(1,K2 "xyz")],-	       test7 ~?= error "*** Exception: constructor mismatch",-	       test8 ~?= Just [(1,TVar 2)],-	       test9 ~?= Just [(2,K2 "abc"),(1,K2 "abc")],-	       test10 ~?= error "*** Exception: unify failed in built in equality",-	       test11 ~?= Just [(2,App (K2 "g") (K2 "xyz")),(1,K2 "xyz")],-	       test12 ~?= error "*** Exception: unify failed when testing equality for \"H\" = \"I\""]---main = runTestTT tests-

@@ -1,178 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,-    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,-    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving- #-}--------------------------------------------------------------------------------- |--- Module      :  LC--- Copyright   :  (c) The University of Pennsylvania, 2010--- License     :  BSD------ Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------------------------------------------------------------------------------------------- | This example demonstrates how to use abstract types as part of--- the syntax of the untyped lambda calculus------ Suppose we wish to include Source positions in our Abstract Syntax----module Abstract where--import Generics.RepLib-import Generics.RepLib.Bind.LocallyNameless-import Generics.RepLib.Bind.PermM-import qualified Data.Set as S--import Control.Monad.Reader (Reader, runReader)----- We import the type SourcePos, but it is an abstract data type--- all we know about it is that it is an instance of the Eq, Show and Ord classes.-import Text.ParserCombinators.Parsec.Pos (SourcePos, newPos)---- Since we don't know the structure of the type, we create an "abstract"--- representation for it. This defines rSourcePos :: R SourcePos and makes--- SourcePos an instance of the Rep and Rep1 type classes.------ Right now, this line triggers a warning because the TemplateHaskell code--- does not work well with type abbreviations. The warning is safe to ignore.-$(derive_abstract [''SourcePos])---- | A Simple datatype for the Lambda Calculus that includes source position--- information-data Exp = Var SourcePos Name-         | Lam (Bind Name Exp)-         | App Exp Exp-  deriving Show--$(derive [''Exp])---- To make Exp an instance of Alpha, we also need SourcePos to be an--- instance of Alpha, because it appears inside the Exp type.  When we--- do so, we override the default definition of match'.  There are a--- few reasonable choices for this:------ (1) match no source positions together  --- default definition---      match' c s1 s2 = Nothing--- (2) match all source positions together---      match' c s1 s2 = Just empty--- (3) only match equal source positions together---      match' c s1 s2 | s1 == s2 = Just empty---      match' c s1 s2 = Nothing------ Below, we choose option (2) because we would like--- (alpha-)equivalence for Exp to ignore the source position--- information. Two free variables with the same name but with--- different source positions should be equal.------ The other defaults for Alpha are fine.-instance Alpha SourcePos where-   match' c s1 s2 = Just empty--instance Alpha Exp where-deriving instance Eq Exp--instance Subst Exp SourcePos where-instance Subst Exp Exp where-   isvar (Var _ x) = Just (x,id)-   isvar _       = Nothing--type M a = Reader Integer a---- | Beta-Eta equivalence for lambda calculus terms.-(=~) :: Exp -> Exp -> M Bool-e1 =~ e2 | e1 == e2 = return True-e1 =~ e2 = do-    e1' <- red e1-    e2' <- red e2-    if e1' == e1 && e2' == e2-      then return False-      else e1' =~ e2'----- | Parallel beta-eta reduction for lambda calculus terms.--- Do as many reductions as possible in one step, while still ensuring--- termination.-red :: Exp -> M Exp-red (App e1 e2) = do-  e1' <- red e1-  e2' <- red e2-  case e1' of-    -- look for a beta-reduction-    Lam bnd ->-      lunbind bnd $ \ (x, e1'') ->-        return $ subst x e2' e1''-    otherwise -> return $ App e1' e2'-red (Lam bnd) = lunbind bnd $ \ (x, e) -> do-   e' <- red e-   case e of-     -- look for an eta-reduction-     App e1 (Var _ y) | y == x && x `S.notMember` fv e1 -> return e1-     otherwise -> return (Lam (bind x e'))-red v = return $ v---------------------------------------------------------------------------- Some testing code to demonstrate this library in action.--assert :: String -> Bool -> IO ()-assert s True  = return ()-assert s False = print ("Assertion " ++ s ++ " failed")--assertM :: String -> M Bool -> IO ()-assertM s c =-  if (runReader c (0 :: Integer)) then return ()-  else print ("Assertion " ++ s ++ " failed")--x :: Name-x = string2Name "x"--y :: Name-y = string2Name "y"--z :: Name-z = string2Name "z"--s :: Name-s = string2Name "s"--sp = newPos "Foo" 1 2-sp2 = newPos "Bar" 3 4--lam :: Name -> Exp -> Exp-lam x y = Lam (bind x y)--var :: Name -> Exp-var n = Var sp n--zero  = lam s (lam z (var z))-one   = lam s (lam z (App (var s) (var z)))-two   = lam s (lam z (App (var s) (App (var s) (var z))))-three = lam s (lam z (App (var s) (App (var s) (App (var s) (var z)))))--plus = lam x (lam y (lam s (lam z (App (App (var x) (var s)) (App (App (var y) (var s)) (var z))))))--true = lam x (lam y (var x))-false = lam x (lam y (var y))-if_ x y z = (App (App x y) z)--main :: IO ()-main = do-  -- \x.x == \x.y, no matter what the source positions are-  assert "a1" $ lam x (var x) == lam y (Var sp2 y)-  -- \x.x /= \x.y-  assert "a2" $ lam x (var y) /= lam x (var x)-  -- \x.(\y.x) (\y.y) == \y.y-  assertM "be1" $ lam x (App (lam y (var x)) (lam y (var y))) =~ (lam y (var y))-  -- \x. f x === f-  assertM "be2" $ lam x (App (var y) (var x)) =~ var y-  assertM "be3" $ if_ true (var x) (var y) =~ var x-  assertM "be4" $ if_ false (var x) (var y) =~ var y-  assertM "be5" $ App (App plus one) two =~ three-

@@ -1,13 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,-    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,-    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving- #-}--module Issue15 where--import Generics.RepLib-import qualified Generics.RepLib.Bind.LocallyNameless as LN--data Foo = Foo (LN.Name Foo)--$(derive [''Foo])