RepLib 0.2.2 → 0.3

raw patch · 37 files changed

+5908/−2527 lines, 37 filesdep +containersdep −haskell98dep ~basedep ~mtldep ~template-haskellPVP ok

version bump matches the API change (PVP)

Dependencies added: containers

Dependencies removed: haskell98

Dependency ranges changed: base, mtl, template-haskell

API changes (from Hackage documentation)

Files

• Data/RepLib.hs +0/−45
• Data/RepLib/Derive.hs +0/−326
• Data/RepLib/Lib.hs +0/−331
• Data/RepLib/PreludeLib.hs +0/−205
• Data/RepLib/PreludeReps.hs +0/−35
• Data/RepLib/R.hs +0/−231
• Data/RepLib/R1.hs +0/−122
• Data/RepLib/RepAux.hs +0/−234
• Data/RepLib/SYB/Aliases.hs +0/−374
• Data/RepLib/SYB/Schemes.hs +0/−169
• Data/RepLib/Unify.hs +0/−243
• Generics/RepLib.hs +52/−0
• Generics/RepLib/Bind/LocallyNameless.hs +1298/−0
• Generics/RepLib/Bind/Nominal.hs +1108/−0
• Generics/RepLib/Bind/PermM.hs +115/−0
• Generics/RepLib/Derive.hs +355/−0
• Generics/RepLib/Lib.hs +375/−0
• Generics/RepLib/PreludeLib.hs +206/−0
• Generics/RepLib/PreludeReps.hs +34/−0
• Generics/RepLib/R.hs +189/−0
• Generics/RepLib/R1.hs +122/−0
• Generics/RepLib/RepAux.hs +297/−0
• Generics/RepLib/SYB/Aliases.hs +373/−0
• Generics/RepLib/SYB/Schemes.hs +171/−0
• Generics/RepLib/Unify.hs +243/−0
• LICENSE +4/−1
• README +23/−16
• RepLib.cabal +26/−21
• examples/Basic.hs +185/−0
• examples/LC-smallstep.hs +102/−0
• examples/LC.hs +145/−0
• examples/LF.hs +71/−0
• examples/Main.hs +12/−156
• examples/STLC.hs +193/−0
• examples/UnifyExp.hs +18/−18
• examples/abstract.hs +178/−0
• examples/issue15.hs +13/−0

@@ -1,45 +0,0 @@--- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances -{-# LANGUAGE TemplateHaskell, UndecidableInstances #-} ---------------------------------------------------------------------------------- |--- Module      :  Data.RepLib--- Copyright   :  (c) The University of Pennsylvania, 2006--- License     :  BSD--- --- Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------------------------------------------------------------------------------------------- Toplevel module to import all others.--module Data.RepLib (-- module Data.RepLib.R,   - module Data.RepLib.R1,	- module Data.RepLib.Lib,- module Data.RepLib.PreludeReps,- module Data.RepLib.PreludeLib,- module Data.RepLib.RepAux,- module Data.RepLib.Derive,- module Data.RepLib.SYB.Aliases, - module Data.RepLib.SYB.Schemes--) where--import Data.RepLib.R-import Data.RepLib.R1-import Data.RepLib.PreludeReps-import Data.RepLib.Lib-import Data.RepLib.PreludeLib-import Data.RepLib.RepAux-import Data.RepLib.Derive-import Data.RepLib.SYB.Aliases-import Data.RepLib.SYB.Schemes--------------------------------------------------------------------------------

@@ -1,326 +0,0 @@--- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances -ddump-splices ----{-# LANGUAGE TemplateHaskell, UndecidableInstances #-} ---------------------------------------------------------------------------------- |--- Module      :  Derive--- Copyright   :  (c) The University of Pennsylvania, 2006--- License     :  TBD--- --- Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------ code to automatically derive representations and instance declarations --- for user defined datatypes. ---------------------------------------------------------------------------------------module Data.RepLib.Derive (-	repr, reprs, repr1, repr1s, derive-) where--import Data.RepLib.R -import Data.RepLib.R1 -import Language.Haskell.TH-import Data.List (nub)-import Data.Tuple----- Given a type, produce its representation. --- Note, that the representation of a type variable "a" is (rep :: R a) so Rep a must be --- in the context-repty :: Type -> Exp-repty (ForallT _ _ _) = error "cannot rep"-repty (VarT n) = (SigE (VarE (mkName "rep")) ((ConT ''R) `AppT` (VarT n)))-repty (AppT t1 t2) = (repty t1) -- `AppE` (repty t2)-repty (ConT n) = -    case nameBase n of -      "Int"     -> (ConE 'Int)-      "Char"    -> (ConE 'Char)-      "Float"   -> (ConE 'Float)-      "Double"  -> (ConE 'Double)-      "Rational"-> (ConE 'Rational)-      "Integer" -> (ConE 'Integer)-      "IOError" -> (ConE 'IOError)-      "IO"      -> (ConE 'IO)-      "[]"      -> (VarE 'rList)  --- don't know why this isn't ListT -      "String"  -> (VarE 'rList)-      c         -> (VarE (rName n))--- repty (TupleT 2) = (VarE (mkName "rTup2"))-repty (TupleT i) = error "urk"-repty (ArrowT)   = (ConE 'Arrow)-repty (ListT)    = (VarE 'rList)- --rName :: Name -> Name-rName n = - case nameBase n of -    "(,,,,,,)" -> mkName ("rTup7")-    "(,,,,,)" -> mkName ("rTup6")-    "(,,,,)" -> mkName ("rTup5")-    "(,,,)" -> mkName ("rTup4")-    "(,,)" -> mkName ("rTup3")-    "(,)" -> mkName ("rTup2")-    c      -> mkName ("r" ++ c)--rName1 :: Name -> Name-rName1 n = - case nameBase n of -    "(,,,,,,)" -> mkName ("rTup7_1")-    "(,,,,,)" -> mkName ("rTup6_1")-    "(,,,,)" -> mkName ("rTup5_1")-    "(,,,)" -> mkName ("rTup4_1")-    "(,,)" -> mkName ("rTup3_1")-    "(,)" -> mkName ("rTup2_1")-    c      -> mkName ("r" ++ c ++ "1")------------------------------------------------------------------------------------------------------------ represent a data constructor. --- As our representation of data constructors evolves, so must this definition.---    Currently, we don't handle data constructors with record components --repcon :: Bool ->  -- Is this the ONLY constructor for the datatype-          Type ->  -- The type that this is a constructor for (applied to all of its parameters)-          (Name, [(Maybe Name, Type)]) ->  -- data constructor name * list of [record name * type]-	  Q Exp-repcon single d (name, sttys) = -	 let rargs = foldr (\ (_,t) tl -> -		 [| $(return (repty t)) :+: $(tl) |]) [| MNil |] sttys in-		 [| Con $(remb single d (name,sttys)) $(rargs) |]---- the "from" function that coerces from an "a" to the arguments-rfrom :: Bool ->  -- does this datatype have only a single constructor-          Type ->  -- the datatype itself-          (Name, [(Maybe Name, Type)]) ->  -- data constructor name, list of parameters with record names-          Q Exp-rfrom single d (name, sttys) = do-       vars <- mapM (\_ -> newName "x") sttys-       outvar <- newName "y"-       let outpat :: Pat-           outpat = ConP name (map VarP vars)-           outbod :: Exp-           outbod = foldr (\v tl -> (ConE (mkName (":*:"))) `AppE` (VarE v) `AppE` tl)-                    (ConE 'Nil) vars-           success = Match outpat (NormalB ((ConE 'Just) `AppE` outbod)) []-           outcase x = if single then -							  CaseE x [success]-							  else-							  CaseE x -                       [success, Match WildP  (NormalB (ConE 'Nothing)) [] ]-       return (LamE [VarP outvar] (outcase (VarE outvar)))---- to component of th embedding-rto :: Type -> (Name, [(Maybe Name, Type)]) -> Q Exp-rto d (name,sttys) =  -  do vars <- mapM (\_ -> newName "x") sttys-     let topat = foldr (\v tl -> InfixP  (VarP v) (mkName ":*:") tl)-                         (ConP 'Nil []) vars-         tobod = foldl (\tl v -> tl `AppE` (VarE v)) (ConE name) vars           -     return (LamE [topat] tobod) ---- the embedding record-remb :: Bool -> Type -> (Name, [(Maybe Name, Type)]) -> Q Exp-remb single d (name, sttys) = -    [| Emb  { name   = $(stringName name), -              to     = $(rto d (name,sttys)), -              from   = $(rfrom single d (name,sttys)),-              labels = Nothing,-              fixity = Nonfix } |]--repDT :: Name -> [Name] -> Q Exp-repDT name param = -      do str <- stringName name-         let reps = foldr (\p f -> -									  (ConE (mkName ":+:")) `AppE`-									     (SigE (VarE (mkName "rep")) -											((ConT ''R) `AppT` (VarT p)))  `AppE` f)-						  (ConE 'MNil) param-         [| DT $(return str) $(return reps) |]---- Create an "R" representation for a given type constructor-repr :: Name -> Q [Dec]-repr n = do info' <- reify n-            case info' of -               TyConI d -> do-                  (name, param, ca, terms) <- typeInfo ((return d) :: Q Dec) -                  let paramNames = map tyVarBndrName param-                  baseT <- conT name                      -                  -- the type that we are defining, applied to its parameters.-                  let ty = foldl (\x p -> x `AppT` (VarT p)) baseT paramNames-                  -- the representations of the paramters, as a list-                  -- representations of the data constructors-                  rcons <- mapM (repcon (length terms == 1) ty) terms-                  body  <- [| Data $(repDT name paramNames) $(return (ListE rcons)) |]-                  let ctx = map (\p -> ClassP (mkName "Rep") [VarT p]) paramNames-                  let rTypeName :: Name -                      rTypeName = rName n-                      rSig :: Dec-                      rSig = SigD rTypeName (ForallT (map PlainTV paramNames) -                                                     ctx ((ConT (mkName "R"))-         	                                          `AppT` ty))-                      rType :: Dec -                      rType = ValD (VarP rTypeName) (NormalB body) [] -                  let inst  = InstanceD ctx ((ConT (mkName "Rep")) `AppT` ty)-                                 [ValD (VarP (mkName "rep")) (NormalB (VarE rTypeName)) []]-                  return [rSig, rType, inst]--reprs :: [Name] -> Q [Dec]-reprs ns = foldl (\qd n -> do decs1 <- repr n -                              decs2 <- qd-                              return (decs1 ++ decs2)) (return []) ns-------------------------------------------------------------------------------------------------- Generating the R1 representation---- The difficult part of repr1 is that we need to paramerize over recs for types that --- appear in the constructors, as well as the reps of parameters.--ctx_params :: Type ->    -- type we are defining-              Name ->    -- name of the type variable "ctx"-				  [(Name, [(Maybe Name, Type)])] -> -- list of constructor names-				                                    -- and the types of their arguments (plus record labels)-            Q [(Name, Type, Type)] -				-- name of termvariable "pt"-            -- (ctx t)-            -- t -ctx_params ty ctxName l = do -   let tys = nub (map snd (foldr (++) [] (map snd l))) -   mapM (\t -> do n <- newName "p"-                  let ctx_t = (VarT ctxName) `AppT` t-                  return (n, ctx_t, t)) tys    --lookupName :: Type -> [(Name, Type, Type)] -> [(Name, Type, Type)] ->  Name-lookupName t l ((n, t1, t2):rest) = if t == t2 then n else lookupName t l rest-lookupName t l [] = error ("lookupName: Cannot find type " ++ show t ++ " in " ++ show l)--repcon1 :: Type                               -- result type of the constructor       -   		  -> Bool-          -> Exp                              -- recursive call (rList1 ra pa)-          -> [(Name,Type,Type)]               -- ctxParams -          -> (Name, [(Maybe Name, Type)])     -- name of data constructor + args-          -> Q Exp-repcon1 d single rd1 ctxParams (name, sttys) = -       let rec = foldr (\ (_,t) tl -> -                    let expQ = (VarE (lookupName t ctxParams ctxParams))-                    in [| $(return expQ) :+: $(tl) |]) [| MNil |] sttys in-       [| Con $(remb single d (name,sttys)) $(rec) |]--repr1 :: Name -> Q [Dec]-repr1 n = do info' <- reify n-             case info' of-               TyConI d -> do-                  (name, param, ca, terms) <- typeInfo ((return d) :: Q Dec) -                  let paramNames = map tyVarBndrName param-                  -- the type that we are defining, applied to its parameters.                      -                  let ty = foldl (\x p -> x `AppT` (VarT p)) (ConT name) paramNames-                  let rTypeName = rName1 n--                  ctx <- newName "ctx"-                  ctxParams <- ctx_params ty ctx terms-                               -                  -- parameters to the rep function-                  -- let rparams = map (\p -> SigP (VarP p) ((ConT ''R) `AppT` (VarT p))) param-                  let cparams = map (\(n,t,_) -> SigP (VarP n) t) ctxParams              --                  -- the recursive call of the rep function-                  let e1 = foldl (\a r -> a `AppE` (VarE r)) (VarE rTypeName) paramNames-                  let e2 = foldl (\a (n,_,_) -> a `AppE` (VarE n)) e1 ctxParams--                  -- the representations of the parameters, as a list-                  -- representations of the data constructors-                  rcons <- mapM (repcon1 ty (length terms == 1) e2 ctxParams) terms-                  body  <- [| Data1 $(repDT name paramNames) -                                    $(return (ListE rcons)) |]-                           -                  let rhs = LamE (cparams) body-{-                    rhs_type = ForallT (ctx:param) rparams -                                  (foldr (\ (p,t) ret -> `ArrowT` `AppT` t `AppT` ret) ty params) -}-                      rTypeDecl = ValD (VarP rTypeName) (NormalB rhs) [] ---                  let ctxRep = map (\p -> ClassP (mkName "Rep") [VarT p]) paramNames-                      ctxRec = map (\(_,t,_) -> ClassP ''Sat [t]) ctxParams--                      -- appRep t = foldl (\a p -> a `AppE` (VarE 'rep)) t param-                      appRec t = foldl (\a p -> a `AppE` (VarE 'dict)) t ctxParams--                  let inst  = InstanceD (ctxRep ++ ctxRec)-                                ((ConT ''Rep1) `AppT` (VarT ctx) `AppT` ty)-                                [ValD (VarP (mkName "rep1"))-                                  (NormalB (appRec (VarE rTypeName))) []]--                  let rSig = SigD rTypeName (ForallT (map PlainTV (ctx : paramNames)) ctxRep-                              (foldr (\(_,p,_) f -> (ArrowT `AppT` p `AppT` f))-                                     ((ConT (mkName "R1")) `AppT` (VarT ctx) `AppT` ty)-                                     ctxParams))-                  decs <- repr n-                  return (decs ++ [rSig, rTypeDecl, inst])---repr1s :: [Name] -> Q [Dec]---repr1s ns = foldl (\qd n -> do decs1 <- repr1 n -                               decs2 <- qd-                               return (decs1 ++ decs2)) (return []) ns-derive = repr1s----------------------------------------------------------------------------------------------- Helper functions--stringName :: Name -> Q Exp-stringName n = return (LitE (StringL (nameBase n)))-----  from SYB III code....--typeInfo :: DecQ -> Q (Name, [TyVarBndr], [(Name, Int)], [(Name, [(Maybe Name, Type)])])-typeInfo m =-     do d <- m-        case d of-           d@(DataD _ _ _ _ _) ->-            return $ (name d, paramsA d, consA d, termsA d)-           d@(NewtypeD _ _ _ _ _) ->-            return $ (name d, paramsA d, consA d, termsA d)-           _ -> error ("derive: not a data type declaration: " ++ show d)--     where-        consA (DataD _ _ _ cs _)    = map conA cs-        consA (NewtypeD _ _ _ c _)  = [ conA c ]--        paramsA (DataD _ _ ps _ _) = ps-        paramsA (NewtypeD _ _ ps _ _) = ps--        termsA (DataD _ _ _ cs _) = map termA cs-        termsA (NewtypeD _ _ _ c _) = [ termA c ]--        termA (NormalC c xs)        = (c, map (\x -> (Nothing, snd x)) xs)-        termA (RecC c xs)           = (c, map (\(n, _, t) -> (Just $ simpleName n, t)) xs)-        termA (InfixC t1 c t2)      = (c, [(Nothing, snd t1), (Nothing, snd t2)])--        conA (NormalC c xs)         = (simpleName c, length xs)-        conA (RecC c xs)            = (simpleName c, length xs)-        conA (InfixC _ c _)         = (simpleName c, 2)--        name (DataD _ n _ _ _)      = n-        name (NewtypeD _ n _ _ _)   = n-        name d                      = error $ show d--simpleName :: Name -> Name-simpleName nm =-   let s = nameBase nm-   in case dropWhile (/=':') s of-        []          -> mkName s-        _:[]        -> mkName s-        _:t         -> mkName t---tyVarBndrName :: TyVarBndr -> Name-tyVarBndrName (PlainTV n) = n-tyVarBndrName (KindedTV n _) = n

@@ -1,331 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables,-    MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,-    TypeSynonymInstances-  #-} ----------------------------------------------------------------------------------- |--- Module      :  RepLib.Lib--- Copyright   :  (c) The University of Pennsylvania, 2006--- License     :  BSD--- --- Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------ A library of specializable, type-indexed functions ----------------------------------------------------------------------------------module Data.RepLib.Lib (-  -- * Available for all representable types-  subtrees, deepSeq, rnf,-  -- * Derivable classes-  GSum(..),-  Zero(..),-  Generate(..),-  Enumerate(..), -  Shrink(..), -  Lreduce(..),-  Rreduce(..),--  -- * Generic operations based on Fold-  Fold(..),-  crush, gproduct, gand, gor, flatten, count, comp, gconcat, gall, gany, gelem,--  -- * Types and generators for derivable classes-  GSumD(..), ZeroD(..), GenerateD(..), EnumerateD(..), ShrinkD(..), LreduceD(..), RreduceD(..),-  rnfR, deepSeqR, gsumR1, zeroR1, generateR1, enumerateR1, lreduceR1, rreduceR1-  -) where--import Data.RepLib.R -import Data.RepLib.R1-import Data.RepLib.RepAux-import Data.RepLib.PreludeReps()--------------------- Subtrees ----------------------------- there is no point in using R1 for subtrees--- From Mark P. Jones, Functional programming with --- overloading and higher-order polymorphism--- Also the same function as "children" from SYB III---- | Produce all children of a datastructure with the same type--- Note that subtrees is available for all representable types. For those that --- are not recursive datatypes, subtrees will always return the--- empty list. But, these trivial instances are convenient to have --- for the Shrink operation below.--subtrees :: forall a. Rep a => a -> [a]-subtrees x = [y | Just y <- gmapQ (cast :: Query (Maybe a)) x]---------------------- DeepSeq ---------------------------- | deepSeq recursively forces the evaluation of its entire--- argument.-deepSeq :: Rep a => a -> b -> b-deepSeq = deepSeqR rep---- | rnf forces the evaluation of *datatypes* to their normal --- forms.  However, other types are left alone and not forced.-rnf :: Rep a => a -> a -rnf = rnfR rep---rnfR :: R a -> a -> a-rnfR (Data dt cons) x = -    case (findCon cons x) of -      Val emb reps args -> to emb (map_l rnfR reps args)       -rnfR _ x = x--deepSeqR :: R a -> a -> b -> b-deepSeqR (Data dt cons) = \x ->-    case (findCon cons x) of -      Val _ reps args -> foldl_l (\ra bb a -> (deepSeqR ra a) . bb) id reps args-deepSeqR _ = seq --deepSeq_l :: MTup R l -> l -> b -> b-deepSeq_l MNil Nil = id-deepSeq_l (rb :+: rs) (b :*: bs) = deepSeqR rb b . deepSeq_l rs bs --------------------- Generic Sum ------------------------- | Add together all of the @Int@s in a datastructure-class Rep1 GSumD a => GSum a where-   gsum :: a -> Int -   gsum = gsumR1 rep1--data GSumD a = GSumD { gsumD :: a -> Int }--gsumR1 :: R1 GSumD a -> a -> Int-gsumR1 Int1              x  = x-gsumR1 (Arrow1 r1 r2)    f  = error "urk"-gsumR1 (Data1 dt cons)   x  =  -  case (findCon cons x) of -      Val emb rec kids -> -        foldl_l (\ca a b -> (gsumD ca b) + a) 0 rec kids-gsumR1 _                 x  = 0--instance GSum a => Sat (GSumD a) where-   dict = GSumD gsum--instance GSum Float-instance GSum Int-instance GSum Bool-instance GSum ()-instance GSum Integer-instance GSum Char-instance GSum Double-instance (GSum a, GSum b) => GSum (a,b)-instance (GSum a) => GSum [a]---------------------- Zero --------------------------------- | Create a zero element of a type-class (Rep1 ZeroD a) => Zero a where-    zero :: a-    zero = zeroR1 rep1--data ZeroD a = ZD { zeroD :: a }--instance Zero a => Sat (ZeroD a) where-    dict = ZD zero--zeroR1 :: R1 ZeroD a -> a -zeroR1 Int1 = minBound-zeroR1 Char1 = minBound-zeroR1 (Arrow1 z1 z2) = \x -> zeroD z2-zeroR1 Integer1 = 0-zeroR1 Float1 = 0.0-zeroR1 Double1 = 0.0-zeroR1 (Data1 dt (Con emb rec : rest)) = to emb (fromTup zeroD rec)-zeroR1 IOError1 = userError "Default Error"-zeroR1 r1 = error ("No zero element of type: " ++ show r1)--instance Zero Int-instance Zero Char-instance (Zero a, Zero b) => Zero (a -> b)-instance Zero Integer-instance Zero Float-instance Zero Double-instance Zero IOError--instance Zero ()-instance Zero Bool-instance (Zero a, Zero b) => Zero (a,b)-instance Zero a => Zero [a]------------ Generate --------------------------------data GenerateD a = GenerateD { generateD :: Int -> [a] }---- | Generate elements of a type up to a certain depth-class Rep1 GenerateD a => Generate a where-  generate :: Int -> [a]-  generate = generateR1 rep1--instance Generate a => Sat (GenerateD a) where-  dict = GenerateD generate--genEnum :: (Enum a) => Int -> [a]-genEnum d = enumFromTo (toEnum 0) (toEnum d)--generateR1 :: R1 GenerateD a -> Int -> [a]-generateR1 Int1  d = genEnum d-generateR1 Char1 d = genEnum d-generateR1 Integer1 d = genEnum d-generateR1 Float1 d = genEnum d-generateR1 Double1 d = genEnum d-generateR1 (Data1 dt cons) 0 = []-generateR1 (Data1 dt cons) d = -  [ to emb l | (Con emb rec) <- cons, -               l <- fromTupM (\x -> generateD x (d-1)) rec]--instance Generate Int-instance Generate Char-instance Generate Integer-instance Generate Float-instance Generate Double--instance Generate ()-instance (Generate a, Generate b) => Generate (a,b)-instance Generate a => Generate [a]-------------- Enumerate ---------------------------------- note that this is not the same as the Enum class in the standard prelude--data EnumerateD a = EnumerateD { enumerateD :: [a] }--instance Enumerate a => Sat (EnumerateD a) where-    dict = EnumerateD { enumerateD = enumerate }---- | enumerate the elements of a type, in DFS order.-class Rep1 EnumerateD a => Enumerate a where -    enumerate :: [a]-    enumerate = enumerateR1 rep1--enumerateR1 :: R1 EnumerateD a -> [a] -enumerateR1 Int1 =  [minBound .. (maxBound::Int)]-enumerateR1 Char1 = [minBound .. (maxBound::Char)]-enumerateR1 (Data1 dt cons) = enumerateCons cons--enumerateCons :: [Con EnumerateD a] -> [a] -enumerateCons (Con emb rec:rest) = (map (to emb) (fromTupM enumerateD rec)) ++ (enumerateCons rest)-enumerateCons [] = []------------------- Shrink (from SYB III) ---------------------------------data ShrinkD a = ShrinkD { shrinkD :: a -> [a] }--instance Shrink a => Sat (ShrinkD a) where-    dict = ShrinkD { shrinkD    = shrink }--class (Rep1 ShrinkD a) => Shrink a where-    shrink :: a -> [a]-    shrink a = subtrees a ++ shrinkStep a -               where shrinkStep t = let M _ ts = gmapM1 m a-                                    in ts-                     m dict x = M x ((shrinkD dict) x)--data M a = M a [a]--instance Monad M where- return x = M x []- (M x xs) >>= k = M r (rs1 ++ rs2)-   where-     M r rs1 = k x-     rs2 = [r | x <- xs, let M r _ = k x]--instance Shrink Int-instance Shrink a => Shrink [a]-instance Shrink Char-instance Shrink ()-instance (Shrink a, Shrink b) => Shrink (a,b)-------------- Reduce ---------------------------------data RreduceD b a = RreduceD { rreduceD :: a -> b -> b }-data LreduceD b a = LreduceD { lreduceD :: b -> a -> b }--class Rep1 (RreduceD b) a => Rreduce b a where-    rreduce :: a -> b -> b-    rreduce = rreduceR1 rep1 --class Rep1 (LreduceD b) a => Lreduce b a where-    lreduce :: b -> a -> b -    lreduce = lreduceR1 rep1--instance Rreduce b a => Sat (RreduceD b a) where-    dict = RreduceD { rreduceD = rreduce }-instance Lreduce b a => Sat (LreduceD b a) where-    dict = LreduceD { lreduceD = lreduce }--lreduceR1 :: R1 (LreduceD b) a -> b -> a -> b-lreduceR1 (Data1 dt cons) b a = case (findCon cons a) of -  Val emb rec args -> foldl_l lreduceD b rec args-lreduceR1 _               b a = b--rreduceR1 :: R1 (RreduceD b) a -> a -> b -> b-rreduceR1 (Data1 dt cons) a b = case (findCon cons a) of -  Val emb rec args -> foldr_l rreduceD b rec args-rreduceR1 _               a b = b---- Instances for standard types-instance Lreduce b Int -instance Lreduce b ()-instance Lreduce b Char-instance Lreduce b Bool-instance (Lreduce c a, Lreduce c b) => Lreduce c (a,b)-instance Lreduce c a => Lreduce c[a] --instance Rreduce b Int -instance Rreduce b ()-instance Rreduce b Char-instance Rreduce b Bool-instance (Rreduce c a, Rreduce c b) => Rreduce c (a,b)-instance Rreduce c a => Rreduce c[a] ---------------------- Fold --------------------------------class Fold f where-	 foldRight :: Rep a => (a -> b -> b) -> f a -> b -> b-	 foldLeft  :: Rep a => (b -> a -> b) -> b -> f a -> b--crush      :: (Rep a, Fold t) => (a -> a -> a) -> a -> t a -> a -crush op   = foldLeft op--gproduct   :: (Rep a, Num a, Fold t) => t a -> a-gproduct t = foldLeft (*) 1 t --gand       :: (Fold t) => t Bool -> Bool-gand t     = foldLeft (&&) True t--gor        :: (Fold t) => t Bool -> Bool-gor  t     = foldLeft (||) False t--flatten    :: (Rep a, Fold t) => t a -> [a]-flatten t  = foldRight (:) t [] --count      :: (Rep a, Fold t) => t a -> Int-count t    = foldRight (const (+1)) t 0 --comp       :: (Rep a, Fold t) => t (a -> a) -> a -> a-comp t     = foldLeft (.) id t--gconcat    :: (Rep a, Fold t) => t [a] -> [a]-gconcat t  = foldLeft (++) []  t--gall       :: (Rep a, Fold t) => (a -> Bool) -> t a -> Bool-gall p t   = foldLeft (\a b -> a && p b) True t-			  -gany       :: (Rep a, Fold t) => (a -> Bool) -> t a -> Bool-gany p t   = foldLeft (\a b -> a || p b) False t--gelem      :: (Rep a, Eq a, Fold t) => a -> t a -> Bool-gelem x t  = foldRight (\a b -> a == x || b) t False ---instance Fold [] where-	 foldRight op = rreduceR1 (rList1 (RreduceD { rreduceD = op })-					  (RreduceD { rreduceD = foldRight op }))-	 foldLeft op = lreduceR1 (rList1 (LreduceD  { lreduceD = op })-					 (LreduceD { lreduceD = foldLeft op }))-

@@ -1,205 +0,0 @@--- OPTIONS -fglasgow-exts -fallow-undecidable-instances -{-# LANGUAGE TemplateHaskell, UndecidableInstances #-} ---------------------------------------------------------------------------------- --- Module      :  RepLib.PreludeLib--- Copyright   :  (c) The University of Pennsylvania, 2006--- License     :  BSD--- --- Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------ ----------------------------------------------------------------------------------- | The module PreludeLib contains generic operations to derive members of the standard --- prelude classess: Eq, Bounded, Compare, Show  (TODO: add Enum and Read)------ Although these classes may already be automatically derived via the--- "deriving" mechanism, this module is included for two reasons:------  * Deriving only works when datatypes are defined. This library--- allows instances of these classes to be generated anywhere. For--- example, suppose some other module contains the definition of the--- datatype T and exposes all of its constructors, but, frustratingly,--- does not derive an instance of the Show class.------   You could define a Show instance of 'T' in your own module with the---   following code:------   > import RepLib  ---   >---   > (repr1 ''T)  -- make the Rep1 instance of T available---   >---   > instance Show T where---   >   showsPrec = showsPrecR1 rep1   -- showsPrecR1 is defined in this module-													 -- ---  * This library also serves as a model for generic functions that are--- slight modifications to these prelude operations. For example, if you--- wanted to define reverse lexicographic ordering or an XML pretty--- printer for datatypes, you might start here. This library is also a--- good place to start learning how to define your own generic--- operations, because the behavior of these operations should match the--- deriving mechanism specified by Haskell 98.--- -module Data.RepLib.PreludeLib (-  EqD,-  eqR1,-  OrdD,-  compareR1,-  BoundedD,-  minBoundR1, -  maxBoundR1, -  ShowD,-  showsPrecR1-)where--import Data.RepLib.R-import Data.RepLib.R1-import Data.RepLib.RepAux----- Polymorphic equality ---------------------------data EqD a = EqD { eqD :: a -> a -> Bool }-instance Eq a => Sat (EqD a) where-    dict = EqD (==)---- | Polymorphic equality, given an R1 representation-eqR1 :: R1 EqD a -> a -> a -> Bool-eqR1 Int1           = (==)-eqR1 Char1          = (==)-eqR1 Integer1       = (==)-eqR1 Float1         = (==)-eqR1 Double1        = (==)-eqR1 (Data1 _ cons) = \x y -> -   let loop (Con rcd rec : rest) = -         case (from rcd x, from rcd y) of -          (Just p1, Just p2) -> eqRL1 rec p1 p2-          (Nothing, Nothing) -> loop rest-          (_,_) -> False-   in loop cons-eqR1 r1  = error ("eqR1 undefined for " ++ show r1)--eqRL1 :: MTup EqD l -> l -> l -> Bool-eqRL1 MNil Nil Nil = True-eqRL1 (r :+: rl) (p1 :*: t1) (p2 :*: t2) =-  eqD r p1 p2 && eqRL1 rl t1 t2-------------- Ord ----------------------------------- compare :: a -> a -> Ordering is a minimal instance --- of the Ord class--data OrdD a = OrdD { compareD :: a -> a -> Ordering }--instance Ord a => Sat (OrdD a) where-    dict = OrdD { compareD = compare }-           -lexord         :: Ordering -> Ordering -> Ordering-lexord LT ord  =  LT-lexord EQ ord  =  ord-lexord GT ord  =  GT---- | Minimal completion of the Ord class-compareR1 :: R1 OrdD a -> a -> a -> Ordering-compareR1 Int1  = compare-compareR1 Char1 = compare-compareR1 (Data1 str cons) = \ x y -> -             let loop (Con emb rec : rest) = -                     case (from emb x, from emb y) of-                        (Just t1, Just t2) -> compareTup rec t1 t2-                        (Just t1, Nothing) -> LT-                        (Nothing, Just t2) -> GT-                        (Nothing, Nothing) -> loop rest-             in loop cons-compareR1 r1 = error ("compareR1 not supported for " ++ show r1)--compareTup :: MTup OrdD l -> l -> l -> Ordering-compareTup MNil Nil Nil = EQ-compareTup (x :+: xs) (y :*: ys) (z :*: zs) = -    lexord (compareD x y z) (compareTup xs ys zs)-------------- Bounded --------------------------------data BoundedD a = BoundedD { minBoundD :: a, maxBoundD :: a } -    -instance Bounded a => Sat (BoundedD a) where-    dict = BoundedD { minBoundD = minBound, maxBoundD = maxBound }---- | To generate the Bounded class-minBoundR1 :: R1 BoundedD a -> a -minBoundR1 Int1  = minBound-minBoundR1 Char1 = minBound-minBoundR1 (Data1 dt (Con emb rec:rest)) = to emb (fromTup minBoundD rec)-minBoundR1 r1     = error ("minBoundR1 not supported for " ++ show r1)---- | To generate the Bounded class-maxBoundR1 :: R1 BoundedD a -> a -maxBoundR1 Int1  = maxBound-maxBoundR1 Char1 = maxBound-maxBoundR1 (Data1 dt cons) = -   case last cons of (Con emb rec) -> to emb (fromTup maxBoundD rec)-maxBoundR1 r1     = error ("maxBoundR1 not supported for " ++ show r1)---------------------- Show ---------------------------------------- Inspired by the Generic Haskell implementation--- Current version doesn't correctly handle fixity--data ShowD a = ShowD { showsPrecD :: Int -> a -> ShowS }-	 -instance Show a => Sat (ShowD a) where-	 dict = ShowD { showsPrecD = showsPrec }--getFixity :: Emb a b -> Int-getFixity c = case fixity c of -				    Nonfix   -> 0-				    Infix  i -> i-				    Infixl i -> i-				    Infixr i -> i---- | Minimal completion of the show class-showsPrecR1 :: R1 ShowD a -> -               Int  -> -- precendence level-               a    -> -- value to be shown-               ShowS-showsPrecR1 (Data1 (DT str _) cons) = \p a -> -	case (findCon cons a) of -      Val c rec kids -> -          case (labels c) of -            Just labs -> par $ showString (name c) . -                               showString "{" .-	 		       showRecord rec kids labs . -			       showString "}" -            Nothing   -> par $ showString (name c) . -                               maybespace .-                               showKids rec kids-          where par        = showParen (p > p' && conArity > 0)-                p'         = getFixity c-                maybespace = if conArity == 0 then id else (' ':)       -                conArity   = foldr_l (\_ _ i -> 1 + i) 0 rec kids--                showKid r x = showsPrecD r (p'+1) x--                showRecord ::  MTup ShowD l -> l -> [String] -> ShowS-                showRecord (r :+: MNil) (a :*: Nil) (l : ls) = showString l . ('=':) . showKid r a-                showRecord (r :+: rs) (a :*: aa) (l : ls) = -                    showString l . ('=':) . showKid r a . showString (", ") . showRecord rs aa ls-                showRecord _ _ _ = error ("Incorrect representation: " ++-				          "wrong number of labels in record type")--                showKids :: MTup ShowD l -> l -> ShowS-                showKids MNil Nil = id-                showKids (r :+: MNil) (x :*: Nil) = showsPrecD r (p'+1) x -                showKids (r :+: cl)   (x :*: l)   = showsPrecD r (p'+1) x . (' ':) . (showKids cl l)-					 -showsPrecR1 Int1      = showsPrec 	 -showsPrecR1 Char1     = showsPrec-showsPrecR1 Integer1  = showsPrec-showsPrecR1 Float1    = showsPrec-showsPrecR1 Double1   = showsPrec-showsPrecR1 r1        = error ("showsPrecR1 not supported for " ++ show r1)-	             -

@@ -1,35 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables,-    FlexibleInstances, MultiParamTypeClasses-  #-} --------------------------------------------------------------------------------- |--- Module      :  RepLib.PreludeReps--- Copyright   :  (c) The University of Pennsylvania, 2006--- License     :  BSD--- --- Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------ --- Automatically derive representations for prelude types----------------------------------------------------------------------------------module Data.RepLib.PreludeReps where--import Data.RepLib.R-import Data.RepLib.R1-import Data.RepLib.Derive-import Language.Haskell.TH--$(derive [''Bool,-	       ''Maybe,-  	       ''Either, - 	       ''Ordering, -          tupleTypeName 3,-			 tupleTypeName 4,-			 tupleTypeName 5,-			 tupleTypeName 6,-			 tupleTypeName 7]) --

@@ -1,231 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,-    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,-    ScopedTypeVariables- #-} --------------------------------------------------------------------------------- |--- Module      :  Data.RepLib.R--- Copyright   :  (c) The University of Pennsylvania, 2006--- License     :  BSD--- --- Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable-----------------------------------------------------------------------------------------module Data.RepLib.R where--import Data.List---data R a where-   Int     :: R Int-   Char    :: R Char -   Integer :: R Integer-   Float   :: R Float-   Double  :: R Double-   Rational:: R Rational-   IOError :: R IOError-   IO      :: (Rep a) => R a -> R (IO a)-   Arrow   :: (Rep a, Rep b) => R a -> R b -> R (a -> b)-   Data    :: DT -> [Con R a] -> R a --data Emb l a  = Emb { to     :: l -> a, -                      from   :: a -> Maybe l, -                      labels :: Maybe [String],  -                      name   :: String,-							 fixity :: Fixity-                     }--data Fixity =  Nonfix-                | Infix      { prec      :: Int }-                | Infixl     { prec      :: Int }-                | Infixr     { prec      :: Int }---data DT       = forall l. DT String (MTup R l)-data Con r a  = forall l. Con (Emb l a) (MTup r l)---data Nil = Nil -data a :*: l = a :*: l-infixr 7 :*:--data MTup r l where-    MNil   :: MTup ctx Nil-    (:+:)  :: (Rep a) => r a -> MTup r l -> MTup r (a :*: l)--infixr 7 :+:--class Rep a where rep :: R a-------- Showing representations  (rewrite this with showsPrec?)--instance Show (R a) where-  show Int     = "Int"-  show Char    = "Char"-  show Integer = "Integer"-  show Float   = "Float"-  show Double  = "Double"-  show Rational= "Rational"-  show (IO t)  = "(IO " ++ show t ++ ")"-  show IOError = "IOError"-  show (Arrow r1 r2) = -     "(" ++ (show r1) ++ " -> " ++ (show r2) ++ ")"-  show (Data dt _) = -     "(Data" ++ show dt ++ ")"--instance Show DT where-  show (DT str reps) = str ++ show reps -  -instance Show (MTup R l) where-  show MNil         = ""-  show (r :+: MNil) = show r -  show (r :+: rs)   = " " ++ show r ++ show rs--instance Eq (R a) where-	 r1 == r2 = True------ Representations for Haskell Prelude types--instance Rep Int where rep = Int-instance Rep Char where rep = Char-instance Rep Double where rep = Double-instance Rep Rational where rep = Rational-instance Rep Float where rep = Float-instance Rep Integer where rep = Integer-instance Rep a => Rep (IO a) where rep = IO rep-instance Rep IOError where rep = IOError-instance (Rep a, Rep b) => Rep (a -> b) where rep = Arrow rep rep---- Booleans-{--rTrueEmb :: Emb Nil Bool-rTrueEmb =  Emb { to = \Nil -> True,-                  from = \x -> if x then Just Nil else Nothing,-                  labels = Nothing,-                  name = "True",-						fixity = Nonfix-                 }--rFalseEmb :: Emb Nil Bool-rFalseEmb =  Emb { to = \Nil -> False,-                   from = \x -> if x then Nothing else Just Nil,-                   labels = Nothing,-                   name = "False",-						 fixity = Nonfix-                  }--rBool :: R Bool-rBool = Data (DT "Bool" MNil) [Con rTrueEmb, Con rFalseEmb]--instance Rep Bool where rep = rBool- -}-      --- Unit--rUnitEmb :: Emb Nil ()-rUnitEmb = Emb { to = \Nil -> (), -                 from = \() -> Just Nil, -			        labels = Nothing, -                 name = "()", -                 fixity = Nonfix }--rUnit :: R ()-rUnit = Data (DT "()" MNil) -        [Con rUnitEmb MNil]- -instance Rep () where rep = rUnit---- Tuples --instance (Rep a, Rep b) => Rep (a,b) where-   rep = rTup2--rTup2 :: forall a b. (Rep a, Rep b) => R (a,b)-rTup2 = let args =  ((rep :: R a) :+: (rep :: R b) :+: MNil) in-			Data (DT "," args) [ Con rPairEmb args ]--rPairEmb :: Emb (a :*: b :*: Nil) (a,b)-rPairEmb = -  Emb { to = \( t1 :*: t2 :*: Nil) -> (t1,t2),-        from = \(a,b) -> Just (a :*: b :*: Nil),-        labels = Nothing, -        name = "(,)",-		  fixity = Nonfix -- ???-      }---- Lists-rList :: forall a. Rep a => R [a]-rList = Data (DT "[]" ((rep :: R a) :+: MNil))-             [ Con rNilEmb MNil, Con rConsEmb ((rep :: R a) :+: rList :+: MNil) ]--rNilEmb :: Emb Nil [a]-rNilEmb = Emb {   to   = \Nil -> [],-                  from  = \x -> case x of -                           (x:xs) -> Nothing-                           []     ->  Just Nil,-                  labels = Nothing, -                  name = "[]",-						fixity = Nonfix-					-                 }--rConsEmb :: Emb (a :*: [a] :*: Nil) [a]-rConsEmb = -   Emb { -            to   = (\ (hd :*: tl :*: Nil) -> (hd : tl)),-            from  = \x -> case x of -                    (hd : tl) -> Just (hd :*: tl :*: Nil)-                    []        -> Nothing,-            labels = Nothing, -            name = ":",-				fixity = Nonfix -- ???-          }--instance Rep a => Rep [a] where-   rep = rList --{---- Maybe representation--rJust :: Rep a => Con (Maybe a)-rJust = Con (rJustEmb)--rJustEmb :: Emb (a :*: Nil) (Maybe a)-rJustEmb = Emb -  { to   = (\(x :*: Nil) -> Just x),-    from  = \x -> case x of -            (Just y) -> Just (y :*: Nil)-            Nothing  -> Nothing,-    labels = Nothing, -    name = "Just"-   }--rNothing :: Con (Maybe a)-rNothing = Con rNothingEmb--rNothingEmb :: Emb Nil (Maybe a)-rNothingEmb = Emb -  { to   = \Nil -> Nothing,-    from  = \x -> case x of -             Nothing -> Just Nil-             _       -> Nothing,-    labels = Nothing,-    name = "Nothing"-  }--rMaybe :: forall a. Rep a => R (Maybe a)-rMaybe = Data (DT "Maybe" ((rep :: R a) :+: MNil))-              [rJust, rNothing]--instance Rep a => Rep (Maybe a) where-   rep = rMaybe--}--- Ordering--- Either-

@@ -1,122 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, GADTs, ScopedTypeVariables,-    MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances- #-} ---------------------------------------------------------------------------------- |--- Module      :  RepLib.R1--- Copyright   :  (c) The University of Pennsylvania, 2006--- License     :  BSD--- --- Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable-----------------------------------------------------------------------------------------module Data.RepLib.R1 where--import Data.RepLib.R-import Data.List------------ Basic infrastructure--data R1 ctx a where-    Int1      :: R1 ctx Int-    Char1     :: R1 ctx Char-    Integer1  :: R1 ctx Integer-    Float1    :: R1 ctx Float-    Double1   :: R1 ctx Double-    Rational1 :: R1 ctx Rational-    IOError1  :: R1 ctx IOError-    IO1       :: (Rep a) => ctx a -> R1 ctx (IO a)-    Arrow1    :: (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a -> b)-    Data1     :: DT -> [Con ctx a] -> R1 ctx a--class Sat a where dict :: a --class Rep a => Rep1 ctx a where rep1 :: R1 ctx a--instance Show (R1 c a) where-    show Int1           = "Int1"-    show Char1          = "Char1"-    show Integer1       = "Integer1"-    show Float1         = "Float1"-    show Double1        = "Double1"-    show Rational1      = "Rational1"-    show IOError1       = "IOError1"-    show (IO1 cb)       = "(IO1 " ++ show (getRep cb) ++ ")"-    show (Arrow1 cb cc) = "(Arrow1 " ++ show (getRep cb) ++ " " ++ show (getRep cc) ++ ")" -    show (Data1 dt _)   = "(Data1 " ++ show dt ++ ")"---- | Access a representation, given a proxy-getRep :: Rep b => c b -> R b-getRep cb = rep ---- | Transform a parameterized rep to a vanilla rep-toR :: R1 c a -> R a-toR Int1            = Int-toR Char1           = Char-toR Integer1        = Integer-toR Float1          = Float-toR Double1         = Double-toR Rational1       = Rational-toR IOError1        = IOError-toR (Arrow1 t1 t2)  = Arrow (getRep t1) (getRep t2)-toR (IO1 t1)        = IO (getRep t1)-toR (Data1 dt cons) = (Data dt (map toCon cons))-  where toCon (Con emb rec) = Con emb (toRs rec)-        toRs           :: MTup c a -> MTup R a -        toRs MNil      = MNil-        toRs (c :+: l) = (getRep c :+: toRs l)-----------------  Representations of Prelude types--instance Rep1 ctx Int      where rep1 = Int1-instance Rep1 ctx Char     where rep1 = Char1-instance Rep1 ctx Integer  where rep1 = Integer1-instance Rep1 ctx Float    where rep1 = Float1-instance Rep1 ctx Double   where rep1 = Double1-instance Rep1 ctx IOError  where rep1 = IOError1-instance Rep1 ctx Rational where rep1 = Rational1-instance (Rep a, Sat (ctx a)) => -         Rep1 ctx (IO a)   where rep1 = IO1 dict-instance (Rep a, Rep b, Sat (ctx a), Sat (ctx b)) => -         Rep1 ctx (a -> b) where rep1 = Arrow1 dict dict----- Data structures---- unit-instance Rep1 ctx ()   where - rep1 = Data1 (DT "()" MNil)-        [Con rUnitEmb MNil]---- pairs-rTup2_1 :: forall a b ctx. (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a,b)-rTup2_1 ca cb = -  case (rep :: R (a,b)) of -     Data rdt _ -> Data1 rdt -       [Con rPairEmb (ca :+: cb :+: MNil)]-     -instance (Rep a, Sat (ctx a), Rep b, Sat (ctx b)) => Rep1 ctx (a,b) where-  rep1 = rTup2_1 dict dict----- Lists-rList1 :: forall a ctx. -  Rep a => ctx a -> ctx [a] -> R1 ctx [a]-rList1 ca cl = Data1 (DT "[]" ((rep :: R a) :+: MNil))-                  [ rCons1 ca cl, rNil1 ]--rNil1  :: Con ctx [a]-rNil1  = Con rNilEmb MNil--rCons1 :: Rep a => ctx a -> ctx [a] -> Con ctx [a]-rCons1 ca cl = Con rConsEmb (ca :+: cl :+: MNil)--instance (Rep a, Sat (ctx a), Sat (ctx [a])) => Rep1 ctx [a] where-  rep1 = rList1 dict dict-

@@ -1,234 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, MagicHash,-    ScopedTypeVariables, GADTs, Rank2Types-  #-} --------------------------------------------------------------------------------- |--- Module      :  RepAux--- Copyright   :  (c) The University of Pennsylvania, 2006--- License     :  BSD--- --- Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------ Auxiliary operations to aid in the definition of type-indexed functions----------------------------------------------------------------------------------module Data.RepLib.RepAux (-  -- ** Casting operations -  compR, cast, castR, gcast, gcastR,--  -- ** Operations for heterogeneous lists -  findCon, Val(..), foldl_l, foldr_l, map_l, mapQ_l, mapM_l, fromTup, fromTupM, toList,--  -- ** SYB style operations (Rep)-  Traversal, Query, MapM, -  gmapT, gmapQ, gmapM,--  -- ** SYB style operations (Rep1)-  Traversal1, Query1, MapM1,-  gmapT1, gmapQ1, gmapM1,--  -- ** SYB Reloaded-  Typed(..),Spine(..), toSpine, fromSpine-) where--import Data.RepLib.R-import Data.RepLib.R1-import GHC.Base (unsafeCoerce#)--------- Casting---- | Determine if two reps are for the same type-compR :: R a -> R b -> Bool-compR Int Int = True-compR Char Char = True-compR Float Float = True-compR Integer Integer = True-compR Double Double = True-compR (IO t1) (IO t2) = compR t1 t2-compR IOError IOError = True-compR (Arrow t1 t2) (Arrow s1 s2) = compR t1 s1 && compR t2 s2-compR (Data rc1 _) (Data rc2 _) = compDT rc1 rc2-compR _ _ = False--compDT :: DT -> DT -> Bool-compDT (DT str1 rt1) (DT str2 rt2) = str1 == str2 && compRTup rt1 rt2--compRTup :: MTup R t1 -> MTup R t2 -> Bool-compRTup MNil MNil = True-compRTup (r1 :+: rt1) (r2 :+: rt2) = compR r1 r2 && compRTup rt1 rt2---- | The type-safe cast operation, explicit arguments-castR :: R a -> R b -> a -> Maybe b-castR (ra::R a) (rb::R b) = -    if compR ra rb then \(x::a) -> Just (unsafeCoerce# x::b) else \x -> Nothing---- | The type-safe cast operation, implicit arguments-cast :: forall a b. (Rep a, Rep b) => a -> Maybe b-cast x = castR (rep :: R a) (rep :: R b) x---- | Leibniz equality between types, explicit representations-gcastR :: forall a b c. R a -> R b -> c a -> Maybe (c b)-gcastR ra rb = if compR ra rb-        then \(x :: c a) -> Just (unsafeCoerce# x :: c b)-        else \x -> Nothing---- | Leibniz equality between types, implicity representations-gcast :: forall a b c. (Rep a, Rep b) => c a -> Maybe (c b)-gcast = gcastR (rep :: R a) (rep :: R b)      ----------- Basic instances and library operations for heterogeneous lists ------------------- | A datastructure to store the results of findCon-data Val ctx a = forall l.  Val (Emb l a) (MTup ctx l) l---- | Given a list of constructor representations for a datatype, --- determine which constructor formed the datatype.-findCon :: [Con ctx a] -> a -> Val ctx a-findCon (Con rcd rec : rest) x = case (from rcd x) of -       Just ys -> Val rcd rec ys-       Nothing -> findCon rest x---- | A fold right operation for heterogeneous lists, that folds a function --- expecting a type type representation across each element of the list.-foldr_l :: (forall a. Rep a => ctx a -> a -> b -> b) -> b -            -> (MTup ctx l) -> l -> b-foldr_l f b MNil Nil = b-foldr_l f b (ca :+: cl) (a :*: l) = f ca a (foldr_l f b cl l ) ---- | A fold left for heterogeneous lists-foldl_l :: (forall a. Rep a => ctx a -> b -> a -> b) -> b -            -> (MTup ctx l) ->  l -> b-foldl_l f b MNil Nil = b-foldl_l f b (ca :+: cl) (a :*: l) = foldl_l f (f ca b a) cl l ---- | A map for heterogeneous lists-map_l :: (forall a. Rep a => ctx a -> a -> a) -           -> (MTup ctx l) ->  l ->  l-map_l f MNil Nil = Nil-map_l f (ca :+: cl) (a :*: l) = (f ca a) :*: (map_l f cl l)---- | Transform a heterogeneous list in to a standard list-mapQ_l :: (forall a. Rep a => ctx a -> a -> r) -> MTup ctx l -> l -> [r]-mapQ_l q MNil Nil = []-mapQ_l q (r :+: rs) (a :*: l) = q r a : mapQ_l q rs l---- | mapM for heterogeneous lists-mapM_l :: (Monad m) => (forall a. Rep a => ctx a -> a -> m a) -> MTup ctx l -> l -> m l-mapM_l f MNil Nil = return Nil-mapM_l f (ca :+: cl) (a :*: l) = do -  x1 <- f ca a-  x2 <- mapM_l f cl l-  return (x1 :*: x2)---- | Generate a heterogeneous list from metadata-fromTup :: (forall a. Rep a => ctx a -> a) -> MTup ctx l -> l-fromTup f MNil = Nil-fromTup f (b :+: l) = (f b) :*: (fromTup f l)---- | Generate a heterogeneous list from metadata, in a monad-fromTupM :: (Monad m) => (forall a. Rep a => ctx a -> m a) -> MTup ctx l -> m l-fromTupM f MNil = return Nil-fromTupM f (b :+: l) = do hd <- f b-                          tl <- fromTupM f l-                          return (hd :*: tl)---- | Generate a normal lists from metadata-toList :: (forall a. Rep a => ctx a -> b) -> MTup ctx l -> [b]-toList f MNil = []-toList f (b :+: l) = f b : toList f l-----------------------  SYB style operations ------------------------------ | A SYB style traversal-type Traversal = forall a. Rep a => a -> a---- | Map a traversal across the kids of a data structure -gmapT :: forall a. Rep a => Traversal -> a -> a-gmapT t = -  case (rep :: R a) of -   (Data dt cons) -> \x -> -     case (findCon cons x) of -      Val emb reps ys -> to emb (map_l (const t) reps ys)-   _ -> id----- | SYB style query type-type Query r = forall a. Rep a => a -> r --gmapQ :: forall a r. Rep a => Query r -> a -> [r]-gmapQ q =-  case (rep :: R a) of -    (Data dt cons) -> \x -> case (findCon cons x) of -		Val emb reps ys -> mapQ_l (const q) reps ys-    _ -> const []----- | SYB style monadic map type-type MapM m = forall a. Rep a => a -> m a--gmapM   :: forall a m. (Rep a, Monad m) => MapM m -> a -> m a-gmapM m = case (rep :: R a) of-   (Data dt cons) -> \x -> case (findCon cons x) of -     Val emb reps ys -> do l <- mapM_l (const m) reps ys-                           return (to emb l)-   _ -> return ----------------- Generalized  SYB ops -----------------------------type Traversal1 ctx = forall a. Rep a => ctx a -> a -> a-gmapT1 :: forall a ctx. (Rep1 ctx a) => Traversal1 ctx -> a -> a -gmapT1 t = -  case (rep1 :: R1 ctx a) of -   (Data1 dt cons) -> \x -> -     case (findCon cons x) of -      Val emb recs kids -> to emb (map_l t recs kids)-   _ -> id--type Query1 ctx r = forall a. Rep a => ctx a -> a -> r-gmapQ1 :: forall a ctx r. (Rep1 ctx a) => Query1 ctx r -> a -> [r]-gmapQ1 q  =-  case (rep1 :: R1 ctx a) of -    (Data1 dt cons) -> \x -> case (findCon cons x) of -		Val emb recs kids -> mapQ_l q recs kids-    _ -> const []--type MapM1 ctx m = forall a. Rep a => ctx a -> a -> m a-gmapM1  :: forall a ctx m. (Rep1 ctx a, Monad m) => MapM1 ctx m -> a -> m a-gmapM1 m = case (rep1 :: R1 ctx a) of-   (Data1 dt cons) -> \x -> case (findCon cons x) of -     Val emb rec ys -> do l <- mapM_l m rec ys-                          return (to emb l)-   _ -> return ---------------- Spine from SYB Reloaded -----------------------------data Typed a = a ::: R a -infixr 7 :::--data Spine a where-	 Constr :: a -> Spine a-	 (:<>)  :: Spine (a -> b) -> Typed a -> Spine b--toSpineR :: R a -> a -> Spine a-toSpineR (Data _ cons) a = -	 case (findCon cons a) of -	    Val emb reps kids -> toSpineRl reps kids (to emb)-toSpineR _ a = Constr a--toSpineRl :: MTup R l -> l -> (l -> a) -> Spine a -toSpineRl MNil Nil into = Constr (into Nil)-toSpineRl (ra :+: rs) (a :*: l) into = -	 (toSpineRl rs l into') :<> (a ::: ra)-		  where into' tl1 x1 = into (x1 :*: tl1)--toSpine :: Rep a => a -> Spine a -toSpine = toSpineR rep--fromSpine :: Spine a -> a-fromSpine (Constr x) = x-fromSpine (x :<> (y:::_)) = fromSpine x y-

@@ -1,374 +0,0 @@-{-# OPTIONS -fglasgow-exts #-}---------------------------------------------------------------------------------- |--- Module      :  RAliases--- Copyright   :  (c) The University of Pennsylvania, 2006--- License     :  BSD--- --- Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------- This module is derived from Data.Generics.Aliases------ The present module provides a number of declarations for typical--- generic function types, corresponding type case, and others.  ------ -------------------------------------------------------------------------------module Data.RepLib.SYB.Aliases ( --	-- * Combinators to \"make\" generic functions via cast-	mkT, mkQ, mkM, mkMp, mkR,-	ext0, extT, extQ, extM, extMp, extB, extR,--	-- * Type synonyms for generic function types-	GenericT, -	GenericQ,-	GenericM,-	GenericB,-	GenericR,-   Generic,-   Generic'(..),-   GenericT'(..),-   GenericQ'(..),-   GenericM'(..),--	-- * Inredients of generic functions-	orElse,--	-- * Function combinators on generic functions-	recoverMp,-	recoverQ,-	choiceMp,-	choiceQ--	-- * Type extension for unary type constructors---	ext1T, ---	ext1M,---	ext1Q,---	ext1R--  ) where--import Control.Monad-import Data.RepLib.R-import Data.RepLib.RepAux---- Derived from Data.Generics.Aliases--- Only modification: "Data" and "Typeable" classes become "Rep" class---   otherwise import our version of the libraries--------------------------------------------------------------------------------------	Combinators to "make" generic functions---	We use type-safe cast in a number of ways to make generic functions.-------------------------------------------------------------------------------------- | Make a generic transformation;---   start from a type-specific case;---   preserve the term otherwise----mkT :: ( Rep a-       , Rep b-       )-    => (b -> b)-    -> a -    -> a-mkT = extT id----- | Make a generic query;---   start from a type-specific case;---   return a constant otherwise----mkQ :: ( Rep a-       , Rep b-       )-    => r-    -> (b -> r)-    -> a -    -> r-(r `mkQ` br) a = case cast a of-                        Just b  -> br b-                        Nothing -> r----- | Make a generic monadic transformation;---   start from a type-specific case;---   resort to return otherwise----mkM :: ( Monad m-       , Rep a-       , Rep b-       )-    => (b -> m b)-    -> a -    -> m a-mkM = extM return---{---For the remaining definitions, we stick to a more concise style, i.e.,-we fold maybies with "maybe" instead of case ... of ..., and we also-use a point-free style whenever possible.---}----- | Make a generic monadic transformation for MonadPlus;---   use \"const mzero\" (i.e., failure) instead of return as default.----mkMp :: ( MonadPlus m-        , Rep a-        , Rep b-        )-     => (b -> m b)-     -> a-     -> m a-mkMp = extM (const mzero)----- | Make a generic builder;---   start from a type-specific ase;---   resort to no build (i.e., mzero) otherwise----mkR :: ( MonadPlus m-       , Rep a-       , Rep b-       )-    => m b -> m a-mkR f = mzero `extR` f----- | Flexible type extension-ext0 :: (Rep a, Rep b) => c a -> c b -> c a-ext0 def ext = maybe def id (gcast ext)----- | Extend a generic transformation by a type-specific case-extT :: ( Rep a-        , Rep b-        )-     => (a -> a)-     -> (b -> b)-     -> a-     -> a-extT def ext = unT ((T def) `ext0` (T ext))----- | Extend a generic query by a type-specific case-extQ :: ( Rep a-        , Rep b-        )-     => (a -> q)-     -> (b -> q)-     -> a-     -> q-extQ f g a = maybe (f a) g (cast a)----- | Extend a generic monadic transformation by a type-specific case-extM :: ( Monad m-        , Rep a-        , Rep b-        )-     => (a -> m a) -> (b -> m b) -> a -> m a-extM def ext = unM ((M def) `ext0` (M ext))----- | Extend a generic MonadPlus transformation by a type-specific case-extMp :: ( MonadPlus m-         , Rep a-         , Rep b-         )-      => (a -> m a) -> (b -> m b) -> a -> m a-extMp = extM----- | Extend a generic builder-extB :: ( Rep a-        , Rep b-        )-     => a -> b -> a-extB a = maybe a id . cast----- | Extend a generic reader-extR :: ( Monad m-        , Rep a-        , Rep b-        )-     => m a -> m b -> m a-extR def ext = unR ((R def) `ext0` (R ext))----------------------------------------------------------------------------------------	Type synonyms for generic function types--------------------------------------------------------------------------------------- | Generic transformations,---   i.e., take an \"a\" and return an \"a\"----type GenericT = forall a. Rep a => a -> a----- | Generic queries of type \"r\",---   i.e., take any \"a\" and return an \"r\"----type GenericQ r = forall a. Rep a => a -> r----- | Generic monadic transformations,---   i.e., take an \"a\" and compute an \"a\"----type GenericM m = forall a. Rep a => a -> m a----- | Generic builders---   i.e., produce an \"a\".----type GenericB = forall a. Rep a => a----- | Generic readers, say monadic builders,---   i.e., produce an \"a\" with the help of a monad \"m\".----type GenericR m = forall a. Rep a => m a----- | The general scheme underlying generic functions---   assumed by gfoldl; there are isomorphisms such as---   GenericT = Generic T.----type Generic c = forall a. Rep a => a -> c a----- | Wrapped generic functions;---   recall: [Generic c] would be legal but [Generic' c] not.----data Generic' c = Generic' { unGeneric' :: Generic c }----- | Other first-class polymorphic wrappers-newtype GenericT'   = GT { unGT :: Rep a => a -> a }-newtype GenericQ' r = GQ { unGQ :: GenericQ r }-newtype GenericM' m = GM { unGM :: Rep a => a -> m a }----- | Left-biased choice on maybies-orElse :: Maybe a -> Maybe a -> Maybe a-x `orElse` y = case x of-                 Just _  -> x-                 Nothing -> y---{---The following variations take "orElse" to the function-level. Furthermore, we generalise from "Maybe" to any-"MonadPlus". This makes sense for monadic transformations and-queries. We say that the resulting combinators modell choice. We also-provide a prime example of choice, that is, recovery from failure. In-the case of transformations, we recover via return whereas for-queries a given constant is returned.---}---- | Choice for monadic transformations-choiceMp :: MonadPlus m => GenericM m -> GenericM m -> GenericM m-choiceMp f g x = f x `mplus` g x----- | Choice for monadic queries-choiceQ :: MonadPlus m => GenericQ (m r) -> GenericQ (m r) -> GenericQ (m r)-choiceQ f g x = f x `mplus` g x----- | Recover from the failure of monadic transformation by identity-recoverMp :: MonadPlus m => GenericM m -> GenericM m-recoverMp f = f `choiceMp` return----- | Recover from the failure of monadic query by a constant-recoverQ :: MonadPlus m => r -> GenericQ (m r) -> GenericQ (m r)-recoverQ r f = f `choiceQ` const (return r)----------------------------------------------------------------------------------------	Type extension for unary type constructors------------------------------------------------------------------------------------{------ | Flexible type extension-ext1 :: (Rep a, Typeable1 t)-     => c a-     -> (forall a. Rep a => c (t a))-     -> c a-ext1 def ext = maybe def id (dataCast1 ext)----- | Type extension of transformations for unary type constructors-ext1T :: (Rep d, Typeable1 t)-      => (forall d. Rep d => d -> d)-      -> (forall d. Rep d => t d -> t d)-      -> d -> d-ext1T def ext = unT ((T def) `ext1` (T ext))----- | Type extension of monadic transformations for type constructors-ext1M :: (Monad m, Rep d, Typeable1 t)-      => (forall d. Rep d => d -> m d)-      -> (forall d. Rep d => t d -> m (t d))-      -> d -> m d-ext1M def ext = unM ((M def) `ext1` (M ext))----- | Type extension of queries for type constructors-ext1Q :: (Rep d, Typeable1 t)-      => (d -> q)-      -> (forall d. Rep d => t d -> q)-      -> d -> q-ext1Q def ext = unQ ((Q def) `ext1` (Q ext))----- | Type extension of readers for type constructors-ext1R :: (Monad m, Rep d, Typeable1 t)-      => m d-      -> (forall d. Rep d => m (t d))-      -> m d-ext1R def ext = unR ((R def) `ext1` (R ext))---}--------------------------------------------------------------------------------------	Type constructors for type-level lambdas--------------------------------------------------------------------------------------- | The type constructor for transformations-newtype T x = T { unT :: x -> x }---- | The type constructor for transformations-newtype M m x = M { unM :: x -> m x }---- | The type constructor for queries-newtype Q q x = Q { unQ :: x -> q }---- | The type constructor for readers-newtype R m x = R { unR :: m x }

@@ -1,169 +0,0 @@-{-# OPTIONS -fglasgow-exts #-}---------------------------------------------------------------------------------- |--- Module      :  RSchemes--- Copyright   :  (c) The University of Pennsylvania 2006--- License     :  BSD--- --- Maintainer  :  sweirich@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable------ Derived from Data.Generics.Schemes--- Only modification: "Data" class becomes "Rep" class---   otherwise import our version of the libraries--- For now,  missing "somewhere" (lacking mapMp)-----------------------------------------------------------------------------------module Data.RepLib.SYB.Schemes ( --   everywhere,-   everywhere',-   everywhereBut,-   everywhereM,---   somewhere,-	everything,-	listify,-   something,-	synthesize,-	gsize,-	glength,-	gdepth,-	gcount,-	gnodecount,-	gtypecount,-	gfindtype-- ) where-----------------------------------------------------------------------------------import Data.RepLib.R-import Data.RepLib.RepAux-import Data.RepLib.SYB.Aliases----- | Apply a transformation everywhere in bottom-up manner-everywhere :: (forall a. Rep a => a -> a)-           -> (forall a. Rep a => a -> a)---- Use gmapT to recurse into immediate subterms;--- recall: gmapT preserves the outermost constructor;--- post-process recursively transformed result via f--- -everywhere f = f . gmapT (everywhere f)----- | Apply a transformation everywhere in top-down manner-everywhere' :: (forall a. Rep a => a -> a)-            -> (forall a. Rep a => a -> a)---- Arguments of (.) are flipped compared to everywhere-everywhere' f = gmapT (everywhere' f) . f----- | Variation on everywhere with an extra stop condition-everywhereBut :: GenericQ Bool -> GenericT -> GenericT---- Guarded to let traversal cease if predicate q holds for x-everywhereBut q f x-    | q x       = x-    | otherwise = f (gmapT (everywhereBut q f) x)----- | Monadic variation on everywhere-everywhereM :: Monad m => GenericM m -> GenericM m---- Bottom-up order is also reflected in order of do-actions-everywhereM f x = do x' <- gmapM (everywhereM f) x-                     f x'----- | Apply a monadic transformation at least somewhere--- somewhere :: MonadPlus m => GenericM m -> GenericM m---- We try "f" in top-down manner, but descent into "x" when we fail--- at the root of the term. The transformation fails if "f" fails--- everywhere, say succeeds nowhere.--- --- somewhere f x = f x `mplus` gmapMp (somewhere f) x----- | Summarise all nodes in top-down, left-to-right order-everything :: (r -> r -> r) -> GenericQ r -> GenericQ r---- Apply f to x to summarise top-level node;--- use gmapQ to recurse into immediate subterms;--- use ordinary foldl to reduce list of intermediate results--- -everything k f x -  = foldl k (f x) (gmapQ (everything k f) x)----- | Get a list of all entities that meet a predicate-listify :: Rep r => (r -> Bool) -> GenericQ [r]-listify p-  = everything (++) ([] `mkQ` (\x -> if p x then [x] else []))----- | Look up a subterm by means of a maybe-typed filter-something :: GenericQ (Maybe u) -> GenericQ (Maybe u)---- "something" can be defined in terms of "everything"--- when a suitable "choice" operator is used for reduction--- -something = everything orElse----- | Bottom-up synthesis of a data structure;---   1st argument z is the initial element for the synthesis;---   2nd argument o is for reduction of results from subterms;---   3rd argument f updates the synthesised data according to the given term----synthesize :: s  -> (s -> s -> s) -> GenericQ (s -> s) -> GenericQ s-synthesize z o f x = f x (foldr o z (gmapQ (synthesize z o f) x))----- | Compute size of an arbitrary data structure-gsize :: Rep a => a -> Int-gsize t = 1 + sum (gmapQ gsize t)----- | Count the number of immediate subterms of the given term-glength :: GenericQ Int-glength = length . gmapQ (const ())----- | Determine depth of the given term-gdepth :: GenericQ Int-gdepth = (+) 1 . foldr max 0 . gmapQ gdepth----- | Determine the number of all suitable nodes in a given term-gcount :: GenericQ Bool -> GenericQ Int-gcount p =  everything (+) (\x -> if p x then 1 else 0)----- | Determine the number of all nodes in a given term-gnodecount :: GenericQ Int-gnodecount = gcount (const True)----- | Determine the number of nodes of a given type in a given term-gtypecount :: Rep a => a -> GenericQ Int-gtypecount (_::a) = gcount (False `mkQ` (\(_::a) -> True))----- | Find (unambiguously) an immediate subterm of a given type-gfindtype :: (Rep x, Rep y) => x -> Maybe y-gfindtype = singleton-          . foldl unJust []-          . gmapQ (Nothing `mkQ` Just)- where-  unJust l (Just x) = x:l-  unJust l Nothing  = l-  singleton [s] = Just s-  singleton _   = Nothing

@@ -1,243 +0,0 @@-{-# LANGUAGE UndecidableInstances, OverlappingInstances, IncoherentInstances,-    ExistentialQuantification, ScopedTypeVariables, EmptyDataDecls,-    MultiParamTypeClasses, FlexibleInstances, FlexibleContexts-  #-}---------------------------------------------------------------------------------- --- Module      :  Data.RepLib.Unify--- Copyright   :  (c) Ben Kavanagh 2008--- License     :  BSD--- --- Maintainer  :  Ben Kavanagh (ben.kavanagh@gmail.com)--- Stability   :  experimental--- Portability :  non-portable------ Generic unification with Replib------------------------------------------------------------------------------------module Data.RepLib.Unify-where--import Data.RepLib.R -import Data.RepLib.R1-import Data.RepLib.RepAux-import Data.RepLib.PreludeReps()-import Control.Monad.State-import Control.Monad.Error--data Proxy a -------------------- Unification ----------------------------- unify takes an equality constraint (from a pool of constraints) and processes it. --- if there is a variable we do an occurs check and if passes add the assignment and apply--- to the current substitution/constraints. otherwise it either matches leafs w/equality or decomposes--- function terms (constructors) to produce additional constraints. So it takes a substitution--- and a set of constraints and returns a new substitution, and a new set of constraints, --- with the possibility of failure. ----- just use string errors for now.-type UnifyError = String----- Error/State monad for unification. This version does not abstract the monad. -type UM n a b = ErrorT UnifyError (State (UnificationState n a)) b---data UnifySubD n a b = UnifySubD { unifyStepD :: Proxy (n, a) -> b -> b -> UM n a (),-				   substD:: n -> a -> b -> b,-				   occursCheckD :: n -> Proxy a -> b -> Bool}--instance (Unify n a b, Subst n a b, Occurs n a b) => Sat (UnifySubD n a b) where-    dict = UnifySubD {unifyStepD = unifyStep, substD = subst, occursCheckD = occursCheck}---data UConstraint n a = forall b. UC (UnifySubD n a b) b b-data UnificationState n a = UState {uConstraints :: [UConstraint n a],-				    uSubst :: [(n, a)]}------ Unification Step--class (Eq n, Show n, Show a, Show b, HasVar n a) => Unify n a b where-    unifyStep :: Proxy (n, a) -> b -> b -> UM n a ()---- Generic unify instance-instance (Eq n, Show n, Show a, Show b, HasVar n a, Rep1 (UnifySubD n a) b) => Unify n a b where-    unifyStep = unifyStepR1 rep1--				 --- | Generic unifyStep. almost identical to polymorphic equality-unifyStepR1 :: (Eq n, Show n, Show a, Show b, HasVar n a) => R1 (UnifySubD n a) b -> Proxy (n, a) -> b -> b -> UM n a ()-unifyStepR1 Int1 _       =  unifyStepEq-unifyStepR1 Char1 _      =  unifyStepEq-unifyStepR1 Integer1 _   =  unifyStepEq-unifyStepR1 Float1 _     =  unifyStepEq-unifyStepR1 Double1 _    =  unifyStepEq-unifyStepR1 (Data1 _ cons) dum = -    \ x y ->                          -       let loop (Con rcd rec : rest) = -              case (from rcd x, from rcd y) of -	         (Just p1, Just p2) -> addConstraintsRL1 rec dum p1 p2 -		 (Nothing, Nothing) -> loop rest-		 (_,_) -> throwError (strMsg $ "constructor mismatch when trying to match " ++ show x ++ " = " ++ show y)   -	   in loop cons-unifyStepR1 r1 _ = \_ _ -> throwError (strMsg ("unifyStepR1 unhandled generic type constructor"))----addConstraintsRL1 ::  MTup (UnifySubD n a) l -> Proxy (n, a) -> l -> l -> UM n a ()-addConstraintsRL1 MNil _ Nil Nil = return ()-addConstraintsRL1 (r :+: rl) (dum :: Proxy (n, a)) (p1 :*: t1) (p2 :*: t2) =-  do queueConstraint $ UC r p1 p2-     addConstraintsRL1 rl dum t1 t2---unifyStepEq x y = if x == y -		    then return ()-		    else throwError $ strMsg ("unify failed when testing equality for " ++ show x ++ " = " ++ show y)    -- " show x ++ " /= " ++ show y)----- a a instance-instance (Eq n, Show n, Show a, HasVar n a, Rep1 (UnifySubD n a) a) => Unify n a a where-    unifyStep (dum :: Proxy (n, a)) (a1::a) a2 =-	case ((is_var a1) :: Maybe n, (is_var a2) :: Maybe n) of-	    (Just n1, Just n2) ->  if n1 == n2-				     then return ()-				     else addSub n1 ((var n2) :: a); -	    (Just n1, _) -> addSub n1 a2-	    (_, Just n2) ->  addSub n2 a1-	    (_, _) -> unifyStepR1 rep1 dum a1 a2-	where -        addSub n t = extendSubstitution (n, t) ---dequeueConstraint :: UM n a (Maybe (UConstraint n a))-dequeueConstraint = do s <- get -		       case s of (UState [] _) -> return Nothing-				 (UState (x : xs) sub) -> do put $ UState xs sub -							     return $ Just x-   -queueConstraint ::  UConstraint n a -> UM n a ()-queueConstraint eq = modify (\ (UState xs sub) -> (UState (eq : xs) sub))----- --- I know of three ways to extend subst. --- 1. Just extend the list. ---    this does not remove instances of the variable assigned from the remaining ---    substitution. This means that when doing occurs checks will ---    need to unfold the substitution as you step down the tree. This is done lazily---    but repeat unfoldings will very often be necessary. --- 2. Apply the sub everywhere in the current sub/constraints and then extend the list. This---    Does unnecessary work by unfolding nodes that may never be examined but does not repeat---    work. --- 3. Just extend the list but construct the terms from references (graph datatype) so---    that when unfolding substitution lazily during occurs check, no further unfolding will---    be necessary once completed. This is more efficient but not as straightforward to ---    analyse.--- --- I use (2) --extendSubstitution ::  (HasVar n a, Eq n, Show n, Show a, Rep1 (UnifySubD n a) a) => (n, a) -> UM n a ()        -- (could fail with occurs check)-extendSubstitution asgn@((n :: n), (a :: a)) =-    if (occursCheck n (undefined :: Proxy a) a)-       then throwError $ "occurs check failed when extending sub with " ++ (show n) ++ " = " ++ (show a)-       else do (UState xs sub) <- get- 	       let sub' = [(n', subst n a a') | (n', a') <- sub]                            -- these might have side effects if we want to handle binding via freshmonad.-               let xs' = [UC d (substD d n a b1) (substD d n a b2) | (UC d b1 b2) <- xs]-               put (UState xs' (asgn : sub'))--------- Solving unification = 1) initialise problem, 2) run rewrites until no constraints or error.-solveUnification :: (HasVar n a, Eq n, Show n, Show a, Rep1 (UnifySubD n a) a) => [(a, a)] -> Maybe [(n, a)]-solveUnification (eqs :: [(a, a)]) = -    case r of Left e -> error e-	      Right _ -> Just $ uSubst final-    where-    (r, final) = runState (runErrorT rwConstraints) (UState cs [])-    cs = [(UC dict a1 a2) | (a1, a2) <- eqs]-    rwConstraints :: UM n a ()-    rwConstraints = do c <- dequeueConstraint-		       case c of Just (UC d a1 a2) -> do result <- unifyStepD d (undefined :: Proxy (n, a)) a1 a2-							 rwConstraints-				 Nothing -> return ()------ To offer this I have to turn on -fallow-overlapping-instances. This rejects the a a instance of the dictionary, --- choosing the more general a b instance instead. Thus this can only be used when a /= b, for example Term, OuterTerm--- in the example testcase. because the instances chosen for dict here are different than above I cannot reduce--- solveUnification to a call to solveUnification'. Please forgive the code duplication. ugh.--solveUnification' :: (HasVar n a, Eq n, Show n, Show a, Show b, Rep1 (UnifySubD n a) b) => Proxy (n, a) -> [(b, b)] -> Maybe [(n, a)]-solveUnification' (dum :: Proxy (n, a)) (eqs :: [(b, b)]) = -    case r of Left e -> error e-	      Right _ -> Just $ uSubst final-    where-    (r, final) = runState (runErrorT rwConstraints) (UState cs [])-    cs = [(UC dict a1 a2) | (a1, a2) <- eqs]-    rwConstraints :: UM n a ()-    rwConstraints = do c <- dequeueConstraint-		       case c of Just (UC d a1 a2) -> do result <- unifyStepD d dum a1 a2-							 rwConstraints-				 Nothing -> return ()-----class HasVar a b where-    is_var :: b -> Maybe a     -- retrieve the name of a variable-    var :: a -> b              -- inject name as a variable------ Generic substitution without binding. (No freshness monad required)--- substitute [a -> t] t'. -class Subst a t t' where-    subst ::  a -> t -> t' -> t'---- generic instance-instance Rep1 (UnifySubD a t) t' => Subst a t t' where-    subst = substR1 rep1---- generic subst.-substR1 :: Rep1 (UnifySubD a t) t' => R1 (UnifySubD a t) t' -> a -> t -> t' -> t'-substR1 r (a::a) (t::t) t' = gmapT1 (\cb b -> substD cb a t b) t'---- a a instance-instance (Eq a, HasVar a t, Rep1 (UnifySubD a t) t) => Subst a t t where-    subst a t t' = if is_var t' == Just a -		  then t -		  else gmapT1 (\cb b -> substD cb a t b) t'----- Generic Occurs checking-class Occurs n a b where-    occursCheck :: n -> Proxy a -> b -> Bool-		   --- generic instance-instance Rep1 (UnifySubD n a) b => Occurs n a b where-    occursCheck = occursCheckR1 rep1---- generic subst.-occursCheckR1 :: Rep1 (UnifySubD n a) b => R1 (UnifySubD n a) b -> n -> Proxy a -> b -> Bool-occursCheckR1 r (n::n) pa b = or $ gmapQ1 (\cb b -> occursCheckD cb n pa b) b---- a a instance.-instance (Eq n, HasVar n a, Rep1 (UnifySubD n a) a) => Occurs n a a where-    occursCheck n pa a = if is_var a == Just n -		  then True -		  else or $ gmapQ1 (\cb b -> occursCheckD cb n pa b) a--

@@ -0,0 +1,52 @@+-- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances+{-# LANGUAGE TemplateHaskell, UndecidableInstances #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Generics.RepLib+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+--+--+-----------------------------------------------------------------------------++--  Toplevel module to import all others+module Generics.RepLib (+ -- * Basic infrastructure+ -- ** Basic Representations of types+ module Generics.RepLib.R,+ -- ** Parameterized Representations of types+ module Generics.RepLib.R1,+ -- ** Representations of Prelude Types+ module Generics.RepLib.PreludeReps,+ -- ** Template Haskell for deriving representations+ module Generics.RepLib.Derive,+ -- * Libraries for defining Generic Operations+ -- ** Library code for defining generic operations+ module Generics.RepLib.RepAux,+ -- ** Scrap your boilerplate operations+ module Generics.RepLib.SYB.Aliases,+ module Generics.RepLib.SYB.Schemes,+ -- * Generic Utilities and Applications+ -- ** Library of generic operations+ module Generics.RepLib.Lib,+ -- ** Derivable type classes written as generic operations+ module Generics.RepLib.PreludeLib+) where+++import Generics.RepLib.R+import Generics.RepLib.R1+import Generics.RepLib.PreludeReps+import Generics.RepLib.Derive+import Generics.RepLib.RepAux+import Generics.RepLib.SYB.Aliases+import Generics.RepLib.SYB.Schemes+import Generics.RepLib.Lib+import Generics.RepLib.PreludeLib+-----------------------------------------------------------------------------+

@@ -0,0 +1,1298 @@+{-# 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.

@@ -0,0 +1,1108 @@+{-# 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
+
+

@@ -0,0 +1,115 @@+----------------------------------------------------------------------+-- |+-- 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]

@@ -0,0 +1,355 @@+-- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances -ddump-splices --++{-# LANGUAGE TemplateHaskell, UndecidableInstances #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Derive+-- License     :  TBD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Automatically derive representations and instance declarations+-- for user defined datatypes.+-- The typical use is+-- @+--     $(derive [''MyType1, ''MyType2])+-- @+--+-----------------------------------------------------------------------------+++module Generics.RepLib.Derive (+	derive, derive_abstract+) where++import Generics.RepLib.R+import Generics.RepLib.R1+import Language.Haskell.TH+import Data.List (nub)+import Data.Tuple+++-- | Given a type, produce its representation.++-- Note, that the representation of a type variable "a" is (rep :: R a) so Rep a must be+-- in the context+repty :: Type -> Q Exp+repty (ForallT _ _ _) = error "cannot rep"+repty (VarT n) = return (SigE (VarE (mkName "rep")) ((ConT ''R) `AppT` (VarT n)))+repty (AppT t1 t2) = (repty t1) -- `AppE` (repty t2)+repty (ConT n) = do+  info <- reify n+  case info of+    TyConI (TySynD n' vars t) -> repty t+    _ ->+     return $+      case nameBase n of+       "Int"     -> (ConE 'Int)+       "Char"    -> (ConE 'Char)+       "Float"   -> (ConE 'Float)+       "Double"  -> (ConE 'Double)+       "Rational"-> (ConE 'Rational)+       "Integer" -> (ConE 'Integer)+       "IOError" -> (ConE 'IOError)+       "IO"      -> (ConE 'IO)+       "[]"      -> (VarE 'rList)  --- don't know why this isn't ListT+       "String"  -> (VarE 'rList)+       c         -> (VarE (rName n))+repty (TupleT i)+  | i <= 7    = return $ VarE (mkName $ "rTup" ++ show i)+  | otherwise = error $ "Why on earth are you using " ++ (show i) ++ "-tuples??"++repty (ArrowT)   = return (ConE 'Arrow)+repty (ListT)    = return (VarE 'rList)+++rName :: Name -> Name+rName n =+ case nameBase n of+    "(,,,,,,)" -> mkName ("rTup7")+    "(,,,,,)" -> mkName ("rTup6")+    "(,,,,)" -> mkName ("rTup5")+    "(,,,)" -> mkName ("rTup4")+    "(,,)" -> mkName ("rTup3")+    "(,)" -> mkName ("rTup2")+    c      -> mkName ("r" ++ c)++rName1 :: Name -> Name+rName1 n =+ case nameBase n of+    "(,,,,,,)" -> mkName ("rTup7_1")+    "(,,,,,)" -> mkName ("rTup6_1")+    "(,,,,)" -> mkName ("rTup5_1")+    "(,,,)" -> mkName ("rTup4_1")+    "(,,)" -> mkName ("rTup3_1")+    "(,)" -> mkName ("rTup2_1")+    c      -> mkName ("r" ++ c ++ "1")++-------------------------------------------------------------------------------------------------------+-- represent a data constructor.+-- As our representation of data constructors evolves, so must this definition.+--    Currently, we don't handle data constructors with record components++repcon :: Bool ->  -- Is this the ONLY constructor for the datatype+          Type ->  -- The type that this is a constructor for (applied to all of its parameters)+          (Name, [(Maybe Name, Type)]) ->  -- data constructor name * list of [record name * type]+	  Q Exp+repcon single d (name, sttys) =+	 let rargs = foldr (\ (_,t) tl ->+		 [| $(repty t) :+: $(tl) |]) [| MNil |] sttys in+		 [| Con $(remb single d (name,sttys)) $(rargs) |]++-- the "from" function that coerces from an "a" to the arguments+rfrom :: Bool ->  -- does this datatype have only a single constructor+          Type ->  -- the datatype itself+          (Name, [(Maybe Name, Type)]) ->  -- data constructor name, list of parameters with record names+          Q Exp+rfrom single d (name, sttys) = do+       vars <- mapM (\_ -> newName "x") sttys+       outvar <- newName "y"+       let outpat :: Pat+           outpat = ConP name (map VarP vars)+           outbod :: Exp+           outbod = foldr (\v tl -> (ConE (mkName (":*:"))) `AppE` (VarE v) `AppE` tl)+                    (ConE 'Nil) vars+           success = Match outpat (NormalB ((ConE 'Just) `AppE` outbod)) []+           outcase x = if single then+							  CaseE x [success]+							  else+							  CaseE x+                       [success, Match WildP  (NormalB (ConE 'Nothing)) [] ]+       return (LamE [VarP outvar] (outcase (VarE outvar)))++-- to component of th embedding+rto :: Type -> (Name, [(Maybe Name, Type)]) -> Q Exp+rto d (name,sttys) =+  do vars <- mapM (\_ -> newName "x") sttys+     let topat = foldr (\v tl -> InfixP  (VarP v) (mkName ":*:") tl)+                         (ConP 'Nil []) vars+         tobod = foldl (\tl v -> tl `AppE` (VarE v)) (ConE name) vars+     return (LamE [topat] tobod)++-- the embedding record+remb :: Bool -> Type -> (Name, [(Maybe Name, Type)]) -> Q Exp+remb single d (name, sttys) =+    [| Emb  { name   = $(stringName name),+              to     = $(rto d (name,sttys)),+              from   = $(rfrom single d (name,sttys)),+              labels = Nothing,+              fixity = Nonfix } |]++repDT :: Name -> [Name] -> Q Exp+repDT name param =+      do str <- stringName name+         let reps = foldr (\p f ->+									  (ConE (mkName ":+:")) `AppE`+									     (SigE (VarE (mkName "rep"))+											((ConT ''R) `AppT` (VarT p)))  `AppE` f)+						  (ConE 'MNil) param+         [| DT $(return str) $(return reps) |]++data Flag = Abs | Conc++-- Create an "R" representation for a given type constructor++repr :: Flag -> Name -> Q [Dec]+repr f n = do info' <- reify n+              case info' of+               TyConI d -> do+                  (name, param, ca, terms) <- typeInfo ((return d) :: Q Dec)+                  let paramNames = map tyVarBndrName param+                  baseT <- conT name+                  -- the type that we are defining, applied to its parameters.+                  let ty = foldl (\x p -> x `AppT` (VarT p)) baseT paramNames+                  -- the representations of the paramters, as a list+                  -- representations of the data constructors+                  rcons <- mapM (repcon (length terms == 1) ty) terms+                  body  <- case f of+                     Conc -> [| Data $(repDT name paramNames) $(return (ListE rcons)) |]+                     Abs  -> [| Abstract $(repDT name paramNames) |]+                  let ctx = map (\p -> ClassP (mkName "Rep") [VarT p]) paramNames+                  let rTypeName :: Name+                      rTypeName = rName n+                      rSig :: Dec+                      rSig = SigD rTypeName (ForallT (map PlainTV paramNames)+                                                     ctx ((ConT (mkName "R"))+         	                                          `AppT` ty))+                      rType :: Dec+                      rType = ValD (VarP rTypeName) (NormalB body) []+                  let inst  = InstanceD ctx ((ConT (mkName "Rep")) `AppT` ty)+                                 [ValD (VarP (mkName "rep")) (NormalB (VarE rTypeName)) []]+                  return [rSig, rType, inst]++reprs :: Flag -> [Name] -> Q [Dec]+reprs f ns = foldl (\qd n -> do decs1 <- repr f n+                                decs2 <- qd+                                return (decs1 ++ decs2)) (return []) ns++--------------------------------------------------------------------------------------------+--- Generating the R1 representation++-- The difficult part of repr1 is that we need to paramerize over recs for types that+-- appear in the constructors, as well as the reps of parameters.++ctx_params :: Type ->    -- type we are defining+              Name ->    -- name of the type variable "ctx"+				  [(Name, [(Maybe Name, Type)])] -> -- list of constructor names+				                                    -- and the types of their arguments (plus record labels)+            Q [(Name, Type, Type)]+				-- name of termvariable "pt"+            -- (ctx t)+            -- t+ctx_params ty ctxName l = do+   let tys = nub (map snd (foldr (++) [] (map snd l)))+   mapM (\t -> do n <- newName "p"+                  let ctx_t = (VarT ctxName) `AppT` t+                  return (n, ctx_t, t)) tys++lookupName :: Type -> [(Name, Type, Type)] -> [(Name, Type, Type)] ->  Name+lookupName t l ((n, t1, t2):rest) = if t == t2 then n else lookupName t l rest+lookupName t l [] = error ("lookupName: Cannot find type " ++ show t ++ " in " ++ show l)++repcon1 :: Type                               -- result type of the constructor+          -> Bool+          -> Exp                              -- recursive call (rList1 ra pa)+          -> [(Name,Type,Type)]               -- ctxParams+          -> (Name, [(Maybe Name, Type)])     -- name of data constructor + args+          -> Q Exp+repcon1 d single rd1 ctxParams (name, sttys) =+       let rec = foldr (\ (_,t) tl ->+                    let expQ = (VarE (lookupName t ctxParams ctxParams))+                    in [| $(return expQ) :+: $(tl) |]) [| MNil |] sttys in+       [| Con $(remb single d (name,sttys)) $(rec) |]++-- Generate a parameterized representation of a type+repr1 :: Flag -> Name -> Q [Dec]+repr1 f n = do info' <- reify n+               case info' of+                TyConI d -> do+                  (name, param, ca, terms) <- typeInfo ((return d) :: Q Dec)+                  let paramNames = map tyVarBndrName param+                  -- the type that we are defining, applied to its parameters.+                  let ty = foldl (\x p -> x `AppT` (VarT p)) (ConT name) paramNames+                  let rTypeName = rName1 n++                  ctx <- newName "ctx"+                  ctxParams <- case f of+                                    Conc -> ctx_params ty ctx terms+                                    Abs  -> return []++                  -- parameters to the rep function+                  -- let rparams = map (\p -> SigP (VarP p) ((ConT ''R) `AppT` (VarT p))) param+                  let cparams = map (\(n,t,_) -> SigP (VarP n) t) ctxParams++                  -- the recursive call of the rep function+                  let e1 = foldl (\a r -> a `AppE` (VarE r)) (VarE rTypeName) paramNames+                  let e2 = foldl (\a (n,_,_) -> a `AppE` (VarE n)) e1 ctxParams++                  -- the representations of the parameters, as a list+                  -- representations of the data constructors+                  rcons <- mapM (repcon1 ty (length terms == 1) e2 ctxParams) terms+                  body  <- case f of+                            Conc -> [| Data1 $(repDT name paramNames)+                                           $(return (ListE rcons)) |]+                            Abs  -> [| Abstract1 $(repDT name paramNames) |]++                  let rhs = LamE (cparams) body+{-                    rhs_type = ForallT (ctx:param) rparams+                                  (foldr (\ (p,t) ret -> `ArrowT` `AppT` t `AppT` ret) ty params) -}+                      rTypeDecl = ValD (VarP rTypeName) (NormalB rhs) []+++                  let ctxRep = map (\p -> ClassP (mkName "Rep") [VarT p]) paramNames+                      ctxRec = map (\(_,t,_) -> ClassP ''Sat [t]) ctxParams++                      -- appRep t = foldl (\a p -> a `AppE` (VarE 'rep)) t param+                      appRec t = foldl (\a p -> a `AppE` (VarE 'dict)) t ctxParams++                  let inst  = InstanceD (ctxRep ++ ctxRec)+                                ((ConT ''Rep1) `AppT` (VarT ctx) `AppT` ty)+                                [ValD (VarP (mkName "rep1"))+                                  (NormalB (appRec (VarE rTypeName))) []]++                  let rSig = SigD rTypeName (ForallT (map PlainTV (ctx : paramNames)) ctxRep+                              (foldr (\(_,p,_) f -> (ArrowT `AppT` p `AppT` f))+                                     ((ConT (mkName "R1")) `AppT` (VarT ctx) `AppT` ty)+                                     ctxParams))+                  decs <- repr f n+                  return (decs ++ [rSig, rTypeDecl, inst])+++repr1s :: Flag -> [Name] -> Q [Dec]+++repr1s f ns = foldl (\qd n -> do decs1 <- repr1 f n+                                 decs2 <- qd+                                 return (decs1 ++ decs2)) (return []) ns++-- | Generate representations (both basic and parameterized) for a list of+-- types.+derive :: [Name] -> Q [Dec]+derive = repr1s Conc++-- | Generate abstract representations for a list of types.+derive_abstract :: [Name] -> Q [Dec]+derive_abstract = repr1s Abs++--------------------------------------------------------------------------------------++++--- Helper functions++stringName :: Name -> Q Exp+stringName n = return (LitE (StringL (nameBase n)))++---  from SYB III code....++typeInfo :: DecQ -> Q (Name, [TyVarBndr], [(Name, Int)], [(Name, [(Maybe Name, Type)])])+typeInfo m =+     do d <- m+        case d of+           d@(DataD _ _ _ _ _) ->+            return $ (name d, paramsA d, consA d, termsA d)+           d@(NewtypeD _ _ _ _ _) ->+            return $ (name d, paramsA d, consA d, termsA d)+           _ -> error ("derive: not a data type declaration: " ++ show d)++     where+        consA (DataD _ _ _ cs _)    = map conA cs+        consA (NewtypeD _ _ _ c _)  = [ conA c ]++        paramsA (DataD _ _ ps _ _) = ps+        paramsA (NewtypeD _ _ ps _ _) = ps++        termsA (DataD _ _ _ cs _) = map termA cs+        termsA (NewtypeD _ _ _ c _) = [ termA c ]++        termA (NormalC c xs)        = (c, map (\x -> (Nothing, snd x)) xs)+        termA (RecC c xs)           = (c, map (\(n, _, t) -> (Just $ simpleName n, t)) xs)+        termA (InfixC t1 c t2)      = (c, [(Nothing, snd t1), (Nothing, snd t2)])+        termA (ForallC _ _ n)       = termA n++        conA (NormalC c xs)         = (simpleName c, length xs)+        conA (RecC c xs)            = (simpleName c, length xs)+        conA (InfixC _ c _)         = (simpleName c, 2)++        name (DataD _ n _ _ _)      = n+        name (NewtypeD _ n _ _ _)   = n+        name d                      = error $ show d++simpleName :: Name -> Name+simpleName nm =+   let s = nameBase nm+   in case dropWhile (/=':') s of+        []          -> mkName s+        _:[]        -> mkName s+        _:t         -> mkName t+++tyVarBndrName :: TyVarBndr -> Name+tyVarBndrName (PlainTV n) = n+tyVarBndrName (KindedTV n _) = n

@@ -0,0 +1,375 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables,+    MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,+    TypeSynonymInstances, GADTs+  #-}+++-----------------------------------------------------------------------------+-- |+-- Module      :  RepLib.Lib+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+-- A library of type-indexed functions+--+-----------------------------------------------------------------------------+module Generics.RepLib.Lib (+  -- * Available for all representable types+  subtrees, deepSeq, rnf,++  -- * Specializable type-indexed functions+  GSum(..),+  Zero(..),+  Generate(..),+  Enumerate(..),+  Shrink(..),+  Lreduce(..),+  Rreduce(..),++  -- * Generic operations based on Fold+  Fold(..),+  crush, gproduct, gand, gor, flatten, count, comp, gconcat, gall, gany, gelem,++  -- * Auxiliary types and generators for derivable classes+  GSumD(..), ZeroD(..), GenerateD(..), EnumerateD(..), ShrinkD(..), LreduceD(..), RreduceD(..),+  rnfR, deepSeqR, gsumR1, zeroR1, generateR1, enumerateR1, lreduceR1, rreduceR1++) where++import Generics.RepLib.R+import Generics.RepLib.R1+import Generics.RepLib.RepAux+import Generics.RepLib.PreludeReps()++------------------- Subtrees --------------------------+-- there is no point in using R1 for subtrees+-- From Mark P. Jones, Functional programming with+-- overloading and higher-order polymorphism+-- Also the same function as "children" from SYB III++-- | Produce all children of a datastructure with the same type.+-- Note that subtrees is available for all representable types. For those that+-- are not recursive datatypes, subtrees will always return the+-- empty list. But, these trivial instances are convenient to have+-- for the Shrink operation below.++subtrees :: forall a. Rep a => a -> [a]+subtrees x = [y | Just y <- gmapQ (cast :: Query (Maybe a)) x]++-------------------- DeepSeq -----------------------+++-- | Recursively force the evaluation of the first+-- argument. For example,+-- @+--  deepSeq ( x , y ) z where+--    x = ...+--    y = ...+-- @+-- will evaluate both @x@ and @y@ then return @z@+deepSeq :: Rep a => a -> b -> b+deepSeq = deepSeqR rep++-- | Force the evaluation of *datatypes* to their normal+-- forms. Other types are left alone and not forced.+rnf :: Rep a => a -> a+rnf = rnfR rep+++rnfR :: R a -> a -> a+rnfR (Data dt cons) x =+    case (findCon cons x) of+      Val emb reps args -> to emb (map_l rnfR reps args)+rnfR _ x = x++deepSeqR :: R a -> a -> b -> b+deepSeqR (Data dt cons) = \x ->+    case (findCon cons x) of+      Val _ reps args -> foldl_l (\ra bb a -> (deepSeqR ra a) . bb) id reps args+deepSeqR _ = seq++deepSeq_l :: MTup R l -> l -> b -> b+deepSeq_l MNil Nil = id+deepSeq_l (rb :+: rs) (b :*: bs) = deepSeqR rb b . deepSeq_l rs bs++------------------- Generic Sum ----------------------+-- | Add together all of the @Int@s in a datastructure+-- For example:+-- gsum ( 1 , True, ("a", Maybe 3, []) , Nothing)+-- 4+--+class Rep1 GSumD a => GSum a where+   gsum :: a -> Int+   gsum = gsumR1 rep1++data GSumD a = GSumD { gsumD :: a -> Int }++gsumR1 :: R1 GSumD a -> a -> Int+gsumR1 Int1              x  = x+gsumR1 (Arrow1 r1 r2)    f  = error "urk"+gsumR1 (Data1 dt cons)   x  =+  case (findCon cons x) of+      Val emb rec kids ->+        foldl_l (\ca a b -> (gsumD ca b) + a) 0 rec kids+gsumR1 _                 x  = 0++instance GSum a => Sat (GSumD a) where+   dict = GSumD gsum++instance GSum Float+instance GSum Int+instance GSum Bool+instance GSum ()+instance GSum Integer+instance GSum Char+instance GSum Double+instance (GSum a, GSum b) => GSum (a,b)+instance (GSum a) => GSum [a]++-------------------- Zero ------------------------------+-- | Create a zero element of a type+-- @+-- ( zero  :: ((Int, Maybe Int), Float))+-- ((0, Nothing), 0.0)+-- @+class (Rep1 ZeroD a) => Zero a where+    zero :: a+    zero = zeroR1 rep1++data ZeroD a = ZD { zeroD :: a }++instance Zero a => Sat (ZeroD a) where+    dict = ZD zero++zeroR1 :: R1 ZeroD a -> a+zeroR1 Int1 = 0+zeroR1 Char1 = minBound+zeroR1 (Arrow1 z1 z2) = \x -> zeroD z2+zeroR1 Integer1 = 0+zeroR1 Float1 = 0.0+zeroR1 Double1 = 0.0+zeroR1 (Data1 dt (Con emb rec : rest)) = to emb (fromTup zeroD rec)+zeroR1 IOError1 = userError "Default Error"+zeroR1 r1 = error ("No zero element of type: " ++ show r1)++instance Zero Int+instance Zero Char+instance (Zero a, Zero b) => Zero (a -> b)+instance Zero Integer+instance Zero Float+instance Zero Double+instance Zero IOError++instance Zero ()+instance Zero Bool+instance (Zero a, Zero b) => Zero (a,b)+instance Zero a => Zero [a]++---------- Generate ------------------------------++data GenerateD a = GenerateD { generateD :: Int -> [a] }++-- | Generate elements of a type up to a certain depth+--+class Rep1 GenerateD a => Generate a where+  generate :: Int -> [a]+  generate = generateR1 rep1++instance Generate a => Sat (GenerateD a) where+  dict = GenerateD generate++genEnum :: (Enum a) => Int -> [a]+genEnum d = enumFromTo (toEnum 0) (toEnum d)++generateR1 :: R1 GenerateD a -> Int -> [a]+generateR1 Int1  d = genEnum d+generateR1 Char1 d = genEnum d+generateR1 Integer1 d = genEnum d+generateR1 Float1 d = genEnum d+generateR1 Double1 d = genEnum d+generateR1 (Data1 dt cons) 0 = []+generateR1 (Data1 dt cons) d =+  [ to emb l | (Con emb rec) <- cons,+               l <- fromTupM (\x -> generateD x (d-1)) rec]+generateR1 r1 x = error ("No way to generate type: " ++ show r1)++instance Generate Int+instance Generate Char+instance Generate Integer+instance Generate Float+instance Generate Double++instance Generate ()+instance (Generate a, Generate b) => Generate (a,b)+instance Generate a => Generate [a]++------------ Enumerate -------------------------------+-- note that this is not the same as the Enum class in the standard prelude++data EnumerateD a = EnumerateD { enumerateD :: [a] }++instance Enumerate a => Sat (EnumerateD a) where+    dict = EnumerateD { enumerateD = enumerate }++-- | enumerate the elements of a type, in DFS order.+class Rep1 EnumerateD a => Enumerate a where+    enumerate :: [a]+    enumerate = enumerateR1 rep1++enumerateR1 :: R1 EnumerateD a -> [a]+enumerateR1 Int1 =  [minBound .. (maxBound::Int)]+enumerateR1 Char1 = [minBound .. (maxBound::Char)]+enumerateR1 (Data1 dt cons) = enumerateCons cons+enumerateR1 r1 = error ("No way to enumerate type: " ++ show r1)++enumerateCons :: [Con EnumerateD a] -> [a]+enumerateCons (Con emb rec:rest) = (map (to emb) (fromTupM enumerateD rec)) ++ (enumerateCons rest)+enumerateCons [] = []++----------------- Shrink (from SYB III) -------------------------------++data ShrinkD a = ShrinkD { shrinkD :: a -> [a] }++instance Shrink a => Sat (ShrinkD a) where+    dict = ShrinkD { shrinkD    = shrink }++-- | Given an element, return smaller elements of the same type+-- for example, to automatically find small counterexamples when testing+class (Rep1 ShrinkD a) => Shrink a where+    shrink :: a -> [a]+    shrink a = subtrees a ++ shrinkStep a+               where shrinkStep t = let M _ ts = gmapM1 m a+                                    in ts+                     m :: forall a. ShrinkD a -> a -> M a+                     m dict x = M x ((shrinkD dict) x)++data M a = M a [a]++instance Monad M where+ return x = M x []+ (M x xs) >>= k = M r (rs1 ++ rs2)+   where+     M r rs1 = k x+     rs2 = [r | x <- xs, let M r _ = k x]++instance Shrink Int+instance Shrink a => Shrink [a]+instance Shrink Char+instance Shrink ()+instance (Shrink a, Shrink b) => Shrink (a,b)++------------ Reduce -------------------------------++data RreduceD b a = RreduceD { rreduceD :: a -> b -> b }+data LreduceD b a = LreduceD { lreduceD :: b -> a -> b }++-- | A general version of fold right, use for Fold class below+class Rep1 (RreduceD b) a => Rreduce b a where+    rreduce :: a -> b -> b+    rreduce = rreduceR1 rep1++-- | A general version of fold left, use for Fold class below+class Rep1 (LreduceD b) a => Lreduce b a where+    lreduce :: b -> a -> b+    lreduce = lreduceR1 rep1++-- For example+-- @ instance Fold [] where+--	 foldRight op = rreduceR1 (rList1 (RreduceD { rreduceD = op })+--					  (RreduceD { rreduceD = foldRight op }))+--	 foldLeft op = lreduceR1 (rList1 (LreduceD  { lreduceD = op })+--					 (LreduceD { lreduceD = foldLeft op }))+-- @++instance Rreduce b a => Sat (RreduceD b a) where+    dict = RreduceD { rreduceD = rreduce }+instance Lreduce b a => Sat (LreduceD b a) where+    dict = LreduceD { lreduceD = lreduce }++lreduceR1 :: R1 (LreduceD b) a -> b -> a -> b+lreduceR1 (Data1 dt cons) b a = case (findCon cons a) of+  Val emb rec args -> foldl_l lreduceD b rec args+lreduceR1 _               b a = b++rreduceR1 :: R1 (RreduceD b) a -> a -> b -> b+rreduceR1 (Data1 dt cons) a b = case (findCon cons a) of+  Val emb rec args -> foldr_l rreduceD b rec args+rreduceR1 _               a b = b++-- Instances for standard types+instance Lreduce b Int+instance Lreduce b ()+instance Lreduce b Char+instance Lreduce b Bool+instance (Lreduce c a, Lreduce c b) => Lreduce c (a,b)+instance Lreduce c a => Lreduce c[a]++instance Rreduce b Int+instance Rreduce b ()+instance Rreduce b Char+instance Rreduce b Bool+instance (Rreduce c a, Rreduce c b) => Rreduce c (a,b)+instance Rreduce c a => Rreduce c[a]++-------------------- Fold -------------------------------+-- | All of the functions below are defined using instances+-- of the following class+class Fold f where+	 foldRight :: Rep a => (a -> b -> b) -> f a -> b -> b+	 foldLeft  :: Rep a => (b -> a -> b) -> b -> f a -> b++-- | Fold a bindary operation left over a datastructure+crush      :: (Rep a, Fold t) => (a -> a -> a) -> a -> t a -> a+crush op   = foldLeft op++-- | Multiply all elements together+gproduct   :: (Rep a, Num a, Fold t) => t a -> a+gproduct t = foldLeft (*) 1 t++-- | Ensure all booleans are true+gand       :: (Fold t) => t Bool -> Bool+gand t     = foldLeft (&&) True t++-- | Ensure at least one boolean is true+gor        :: (Fold t) => t Bool -> Bool+gor  t     = foldLeft (||) False t++-- | Convert to list+flatten    :: (Rep a, Fold t) => t a -> [a]+flatten t  = foldRight (:) t []++-- | Count number of @a@s that appear in the argument+count      :: (Rep a, Fold t) => t a -> Int+count t    = foldRight (const (+1)) t 0++-- | Compose all functions in the datastructure together+comp       :: (Rep a, Fold t) => t (a -> a) -> a -> a+comp t     = foldLeft (.) id t++-- | Concatenate all lists in the datastructure together+gconcat    :: (Rep a, Fold t) => t [a] -> [a]+gconcat t  = foldLeft (++) []  t++-- | Ensure property holds of all data+gall       :: (Rep a, Fold t) => (a -> Bool) -> t a -> Bool+gall p t   = foldLeft (\a b -> a && p b) True t+++-- | Ensure property holds of some element+gany       :: (Rep a, Fold t) => (a -> Bool) -> t a -> Bool+gany p t   = foldLeft (\a b -> a || p b) False t++-- | Is an element stored in a datastructure+gelem      :: (Rep a, Eq a, Fold t) => a -> t a -> Bool+gelem x t  = foldRight (\a b -> a == x || b) t False+++instance Fold [] where+	 foldRight op = rreduceR1 (rList1 (RreduceD { rreduceD = op })+					  (RreduceD { rreduceD = foldRight op }))+	 foldLeft op = lreduceR1 (rList1 (LreduceD  { lreduceD = op })+					 (LreduceD { lreduceD = foldLeft op }))+

@@ -0,0 +1,206 @@+-- OPTIONS -fglasgow-exts -fallow-undecidable-instances+{-# LANGUAGE TemplateHaskell, UndecidableInstances, GADTs #-}++-----------------------------------------------------------------------------+--+-- Module      :  RepLib.PreludeLib+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+--+-----------------------------------------------------------------------------+++-- | The module PreludeLib contains generic operations to derive members of the standard+-- prelude classess: Eq, Bounded, Compare, Show  (TODO: add Enum and Read)+--+-- Although these classes may already be automatically derived via the+-- "deriving" mechanism, this module is included for two reasons:+--+--  * Deriving only works when datatypes are defined. This library+-- allows instances of these classes to be generated anywhere. For+-- example, suppose some other module contains the definition of the+-- datatype T and exposes all of its constructors, but, frustratingly,+-- does not derive an instance of the Show class.+--+--   You could define a Show instance of 'T' in your own module with the+--   following code:+--+--   > import RepLib+--   >+--   > (repr1 ''T)  -- make the Rep1 instance of T available+--   >+--   > instance Show T where+--   >   showsPrec = showsPrecR1 rep1   -- showsPrecR1 is defined in this module+													 --+--  * This library also serves as a model for generic functions that are+-- slight modifications to these prelude operations. For example, if you+-- wanted to define reverse lexicographic ordering or an XML pretty+-- printer for datatypes, you might start here. This library is also a+-- good place to start learning how to define your own generic+-- operations, because the behavior of these operations should match the+-- deriving mechanism specified by Haskell 98.+--+module Generics.RepLib.PreludeLib (+  EqD,+  eqR1,+  OrdD,+  compareR1,+  BoundedD,+  minBoundR1,+  maxBoundR1,+  ShowD,+  showsPrecR1+)where++import Generics.RepLib.R+import Generics.RepLib.R1+import Generics.RepLib.RepAux++--- Polymorphic equality -------------------------++data EqD a = EqD { eqD :: a -> a -> Bool }+instance Eq a => Sat (EqD a) where+    dict = EqD (==)++-- | Polymorphic equality, given an R1 representation+eqR1 :: R1 EqD a -> a -> a -> Bool+eqR1 Int1           = (==)+eqR1 Char1          = (==)+eqR1 Integer1       = (==)+eqR1 Float1         = (==)+eqR1 Double1        = (==)+eqR1 (Data1 _ cons) = \x y ->+   let loop (Con rcd rec : rest) =+         case (from rcd x, from rcd y) of+          (Just p1, Just p2) -> eqRL1 rec p1 p2+          (Nothing, Nothing) -> loop rest+          (_,_) -> False+   in loop cons+eqR1 r1  = error ("eqR1 undefined for " ++ show r1)++eqRL1 :: MTup EqD l -> l -> l -> Bool+eqRL1 MNil Nil Nil = True+eqRL1 (r :+: rl) (p1 :*: t1) (p2 :*: t2) =+  eqD r p1 p2 && eqRL1 rl t1 t2+++------------ Ord -------------------------------++-- compare :: a -> a -> Ordering is a minimal instance+-- of the Ord class++data OrdD a = OrdD { compareD :: a -> a -> Ordering }++instance Ord a => Sat (OrdD a) where+    dict = OrdD { compareD = compare }++lexord         :: Ordering -> Ordering -> Ordering+lexord LT ord  =  LT+lexord EQ ord  =  ord+lexord GT ord  =  GT++-- | Minimal completion of the Ord class+compareR1 :: R1 OrdD a -> a -> a -> Ordering+compareR1 Int1  = compare+compareR1 Char1 = compare+compareR1 (Data1 str cons) = \ x y ->+             let loop (Con emb rec : rest) =+                     case (from emb x, from emb y) of+                        (Just t1, Just t2) -> compareTup rec t1 t2+                        (Just t1, Nothing) -> LT+                        (Nothing, Just t2) -> GT+                        (Nothing, Nothing) -> loop rest+             in loop cons+compareR1 r1 = error ("compareR1 not supported for " ++ show r1)++compareTup :: MTup OrdD l -> l -> l -> Ordering+compareTup MNil Nil Nil = EQ+compareTup (x :+: xs) (y :*: ys) (z :*: zs) =+    lexord (compareD x y z) (compareTup xs ys zs)++------------ Bounded ------------------------------++data BoundedD a = BoundedD { minBoundD :: a, maxBoundD :: a }++instance Bounded a => Sat (BoundedD a) where+    dict = BoundedD { minBoundD = minBound, maxBoundD = maxBound }++-- | To generate the Bounded class+minBoundR1 :: R1 BoundedD a -> a+minBoundR1 Int1  = minBound+minBoundR1 Char1 = minBound+minBoundR1 (Data1 dt (Con emb rec:rest)) = to emb (fromTup minBoundD rec)+minBoundR1 r1     = error ("minBoundR1 not supported for " ++ show r1)++-- | To generate the Bounded class+maxBoundR1 :: R1 BoundedD a -> a+maxBoundR1 Int1  = maxBound+maxBoundR1 Char1 = maxBound+maxBoundR1 (Data1 dt cons) =+   case last cons of (Con emb rec) -> to emb (fromTup maxBoundD rec)+maxBoundR1 r1     = error ("maxBoundR1 not supported for " ++ show r1)++-------------------- Show -------------------------------------+-- Inspired by the Generic Haskell implementation+-- Current version doesn't correctly handle fixity++data ShowD a = ShowD { showsPrecD :: Int -> a -> ShowS }++instance Show a => Sat (ShowD a) where+	 dict = ShowD { showsPrecD = showsPrec }++getFixity :: Emb a b -> Int+getFixity c = case fixity c of+				    Nonfix   -> 0+				    Infix  i -> i+				    Infixl i -> i+				    Infixr i -> i++-- | Minimal completion of the show class+showsPrecR1 :: R1 ShowD a ->+               Int  -> -- precendence level+               a    -> -- value to be shown+               ShowS+showsPrecR1 (Data1 (DT str _) cons) = \p a ->+	case (findCon cons a) of+      Val c rec kids ->+          case (labels c) of+            Just labs -> par $ showString (name c) .+                               showString "{" .+	 		       showRecord rec kids labs .+			       showString "}"+            Nothing   -> par $ showString (name c) .+                               maybespace .+                               showKids rec kids+          where par        = showParen (p > p' && conArity > 0)+                p'         = getFixity c+                maybespace = if conArity == 0 then id else (' ':)+                conArity   = foldr_l (\_ _ i -> 1 + i) 0 rec kids++                showKid :: ShowD a -> a -> ShowS+                showKid r x = showsPrecD r (p'+1) x++                showRecord ::  MTup ShowD l -> l -> [String] -> ShowS+                showRecord (r :+: MNil) (a :*: Nil) (l : ls) = showString l . ('=':) . showKid r a+                showRecord (r :+: rs) (a :*: aa) (l : ls) =+                    showString l . ('=':) . showKid r a . showString (", ") . showRecord rs aa ls+                showRecord _ _ _ = error ("Incorrect representation: " +++				          "wrong number of labels in record type")++                showKids :: MTup ShowD l -> l -> ShowS+                showKids MNil Nil = id+                showKids (r :+: MNil) (x :*: Nil) = showsPrecD r (p'+1) x+                showKids (r :+: cl)   (x :*: l)   = showsPrecD r (p'+1) x . (' ':) . (showKids cl l)++showsPrecR1 Int1      = showsPrec+showsPrecR1 Char1     = showsPrec+showsPrecR1 Integer1  = showsPrec+showsPrecR1 Float1    = showsPrec+showsPrecR1 Double1   = showsPrec+showsPrecR1 r1        = error ("showsPrecR1 not supported for " ++ show r1)++

@@ -0,0 +1,34 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables,+    FlexibleInstances, MultiParamTypeClasses+  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  RepLib.PreludeReps+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+--+-- Representations for Prelude types, necessary to (automatically) derive+-- representations of user defined types.+-----------------------------------------------------------------------------+module Generics.RepLib.PreludeReps where++import Generics.RepLib.R+import Generics.RepLib.R1+import Generics.RepLib.Derive+import Language.Haskell.TH++$(derive [''Bool,+          ''Maybe,+          ''Either,+          ''Ordering,+          tupleTypeName 3,+          tupleTypeName 4,+          tupleTypeName 5,+          tupleTypeName 6,+          tupleTypeName 7])++

@@ -0,0 +1,189 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,+    ScopedTypeVariables+ #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Generics.RepLib.R+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Basic data structure and class for representation types+--+-----------------------------------------------------------------------------++module Generics.RepLib.R where++import Data.List++-- | A value of type @R a@ is a representation of a type @a@.+data R a where+   Int      :: R Int+   Char     :: R Char+   Integer  :: R Integer+   Float    :: R Float+   Double   :: R Double+   Rational :: R Rational+   IOError  :: R IOError+   IO       :: (Rep a) => R a -> R (IO a)+   Arrow    :: (Rep a, Rep b) => R a -> R b -> R (a -> b)+   Data     :: DT -> [Con R a] -> R a+   Abstract :: DT -> R a++-- | Representation of a data constructor includes an+-- embedding between the datatype and a list of other types+-- as well as the representation of that list of other types.+data Con r a  = forall l. Con (Emb l a) (MTup r l)++-- | An embedding between a list of types @l@ and+-- a datatype @a@, based on a particular data constructor.+-- The to function is a wrapper for the constructor, the+-- from function pattern matches on the constructor.+data Emb l a  = Emb { to     :: l -> a,+                      from   :: a -> Maybe l,+                      labels :: Maybe [String],+                      name   :: String,+                      fixity :: Fixity+                     }++data Fixity =  Nonfix+                | Infix      { prec      :: Int }+                | Infixl     { prec      :: Int }+                | Infixr     { prec      :: Int }++-- | Information about a datatype, including its+-- fully qualified name and representation of+-- its type arguments.+data DT       = forall l. DT String (MTup R l)+++-- | An empty list of types+data Nil = Nil+-- | Cons for a list of types+data a :*: l = a :*: l++data Ex f = forall a. Rep a => Ex (f a)++infixr 7 :*:++-- | A heterogeneous list+data MTup r l where+    MNil   :: MTup r Nil+    (:+:)  :: (Rep a) => r a -> MTup r l -> MTup r (a :*: l)+    MEx    :: (Rep a) => MTup r (f a) -> MTup r (Ex f)++infixr 7 :+:++-- | A Class of representatble types+class Rep a where rep :: R a++------ Showing representations  (rewrite this with showsPrec?)++instance Show (R a) where+  show Int     = "Int"+  show Char    = "Char"+  show Integer = "Integer"+  show Float   = "Float"+  show Double  = "Double"+  show Rational= "Rational"+  show (IO t)  = "(IO " ++ show t ++ ")"+  show IOError = "IOError"+  show (Arrow r1 r2) =+     "(" ++ (show r1) ++ " -> " ++ (show r2) ++ ")"+  show (Data dt _) =+     "(Data" ++ show dt ++ ")"+  show (Abstract dt) =+     "(Abstract" ++ show dt ++ ")"++instance Show DT where+  show (DT str reps) = str ++ show reps++instance Show (MTup R l) where+  show MNil         = ""+  show (r :+: MNil) = show r+  show (r :+: rs)   = " " ++ show r ++ show rs++instance Eq (R a) where+	 r1 == r2 = True++instance Ord (R a) where+  compare r1 r2 = EQ  -- R a is a singleton++--- Representations for (some) Haskell Prelude types++instance Rep Int where rep = Int+instance Rep Char where rep = Char+instance Rep Double where rep = Double+instance Rep Rational where rep = Rational+instance Rep Float where rep = Float+instance Rep Integer where rep = Integer+instance Rep a => Rep (IO a) where rep = IO rep+instance Rep IOError where rep = IOError+instance (Rep a, Rep b) => Rep (a -> b) where rep = Arrow rep rep++-- Unit++rUnitEmb :: Emb Nil ()+rUnitEmb = Emb { to = \Nil -> (),+                 from = \() -> Just Nil,+			        labels = Nothing,+                 name = "()",+                 fixity = Nonfix }++rUnit :: R ()+rUnit = Data (DT "()" MNil)+        [Con rUnitEmb MNil]++instance Rep () where rep = rUnit++-- Tuples++instance (Rep a, Rep b) => Rep (a,b) where+   rep = rTup2++rTup2 :: forall a b. (Rep a, Rep b) => R (a,b)+rTup2 = let args =  ((rep :: R a) :+: (rep :: R b) :+: MNil) in+			Data (DT "," args) [ Con rPairEmb args ]++rPairEmb :: Emb (a :*: b :*: Nil) (a,b)+rPairEmb =+  Emb { to = \( t1 :*: t2 :*: Nil) -> (t1,t2),+        from = \(a,b) -> Just (a :*: b :*: Nil),+        labels = Nothing,+        name = "(,)",+        fixity = Nonfix -- ???+      }++-- Lists+rList :: forall a. Rep a => R [a]+rList = Data (DT "[]" ((rep :: R a) :+: MNil))+             [ Con rNilEmb MNil, Con rConsEmb ((rep :: R a) :+: rList :+: MNil) ]++rNilEmb :: Emb Nil [a]+rNilEmb = Emb {   to   = \Nil -> [],+                  from  = \x -> case x of+                           (x:xs) -> Nothing+                           []     ->  Just Nil,+                  labels = Nothing,+                  name = "[]",+		  fixity = Nonfix+                 }++rConsEmb :: Emb (a :*: [a] :*: Nil) [a]+rConsEmb =+   Emb {+            to   = (\ (hd :*: tl :*: Nil) -> (hd : tl)),+            from  = \x -> case x of+                    (hd : tl) -> Just (hd :*: tl :*: Nil)+                    []        -> Nothing,+            labels = Nothing,+            name = ":",+	    fixity = Nonfix -- ???+          }++instance Rep a => Rep [a] where+   rep = rList+

@@ -0,0 +1,122 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, GADTs, ScopedTypeVariables,+    MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances+ #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  RepLib.R1+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+--+--+-----------------------------------------------------------------------------++module Generics.RepLib.R1 where++import Generics.RepLib.R+import Data.List++---------- Basic infrastructure++data R1 ctx a where+    Int1      :: R1 ctx Int+    Char1     :: R1 ctx Char+    Integer1  :: R1 ctx Integer+    Float1    :: R1 ctx Float+    Double1   :: R1 ctx Double+    Rational1 :: R1 ctx Rational+    IOError1  :: R1 ctx IOError+    IO1       :: (Rep a) => ctx a -> R1 ctx (IO a)+    Arrow1    :: (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a -> b)+    Data1     :: DT -> [Con ctx a] -> R1 ctx a+    Abstract1 :: DT -> R1 ctx a+class Sat a where dict :: a++class Rep a => Rep1 ctx a where rep1 :: R1 ctx a++instance Show (R1 c a) where+    show Int1           = "Int1"+    show Char1          = "Char1"+    show Integer1       = "Integer1"+    show Float1         = "Float1"+    show Double1        = "Double1"+    show Rational1      = "Rational1"+    show IOError1       = "IOError1"+    show (IO1 cb)       = "(IO1 " ++ show (getRepC cb) ++ ")"+    show (Arrow1 cb cc) = "(Arrow1 " ++ show (getRepC cb) ++ " " ++ show (getRepC cc) ++ ")"+    show (Data1 dt _)   = "(Data1 " ++ show dt ++ ")"+    show (Abstract1 dt) = "(Abstract1 " ++ show dt ++ ")"++-- | Access a representation, given a proxy+getRepC :: Rep b => c b -> R b+getRepC cb = rep++-- | Transform a parameterized rep to a vanilla rep+toR :: R1 c a -> R a+toR Int1            = Int+toR Char1           = Char+toR Integer1        = Integer+toR Float1          = Float+toR Double1         = Double+toR Rational1       = Rational+toR IOError1        = IOError+toR (Arrow1 t1 t2)  = Arrow (getRepC t1) (getRepC t2)+toR (IO1 t1)        = IO (getRepC t1)+toR (Data1 dt cons) = (Data dt (map toCon cons))+  where toCon (Con emb rec) = Con emb (toRs rec)+        toRs           :: MTup c a -> MTup R a+        toRs MNil      = MNil+        toRs (c :+: l) = (getRepC c :+: toRs l)+toR (Abstract1 dt) = Abstract dt++---------------  Representations of Prelude types++instance Rep1 ctx Int      where rep1 = Int1+instance Rep1 ctx Char     where rep1 = Char1+instance Rep1 ctx Integer  where rep1 = Integer1+instance Rep1 ctx Float    where rep1 = Float1+instance Rep1 ctx Double   where rep1 = Double1+instance Rep1 ctx IOError  where rep1 = IOError1+instance Rep1 ctx Rational where rep1 = Rational1+instance (Rep a, Sat (ctx a)) =>+         Rep1 ctx (IO a)   where rep1 = IO1 dict+instance (Rep a, Rep b, Sat (ctx a), Sat (ctx b)) =>+         Rep1 ctx (a -> b) where rep1 = Arrow1 dict dict+++-- Data structures++-- unit+instance Rep1 ctx ()   where+ rep1 = Data1 (DT "()" MNil)+        [Con rUnitEmb MNil]++-- pairs+rTup2_1 :: forall a b ctx. (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a,b)+rTup2_1 ca cb =+  case (rep :: R (a,b)) of+     Data rdt _ -> Data1 rdt+       [Con rPairEmb (ca :+: cb :+: MNil)]++instance (Rep a, Sat (ctx a), Rep b, Sat (ctx b)) => Rep1 ctx (a,b) where+  rep1 = rTup2_1 dict dict+++-- Lists+rList1 :: forall a ctx.+  Rep a => ctx a -> ctx [a] -> R1 ctx [a]+rList1 ca cl = Data1 (DT "[]" ((rep :: R a) :+: MNil))+                  [ rCons1 ca cl, rNil1 ] where+   rNil1  :: Con ctx [a]+   rNil1  = Con rNilEmb MNil++   rCons1 :: ctx a -> ctx [a] -> Con ctx [a]+   rCons1 ca cl = Con rConsEmb (ca :+: cl :+: MNil)++instance (Rep a, Sat (ctx a), Sat (ctx [a])) => Rep1 ctx [a] where+  rep1 = rList1 dict dict+

@@ -0,0 +1,297 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, MagicHash,+    ScopedTypeVariables, GADTs, Rank2Types+  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  RepAux+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Auxiliary operations to aid in the definition of type-indexed functions+--+-----------------------------------------------------------------------------+module Generics.RepLib.RepAux (+  -- ** Casting operations+  eqR, cast, castR, gcast, gcastR,++  -- ** Comparison+  compareR,++  -- ** Operations for heterogeneous lists+  findCon, Val(..), foldl_l, foldr_l, map_l, mapQ_l, mapM_l, fromTup, fromTupM, toList,++  -- ** SYB style operations (Rep)+  Traversal, Query, MapM,+  gmapT, gmapQ, gmapM,++  -- ** SYB style operations (Rep1)+  Traversal1, Query1, MapM1,+  gmapT1, gmapQ1, gmapM1,++  -- ** SYB Reloaded+  Typed(..),Spine(..), toSpine, fromSpine+) where++import Generics.RepLib.R+import Generics.RepLib.R1+import GHC.Base (unsafeCoerce#)+++------ Casting++-- | Determine if two reps are for the same type+eqR :: R a -> R b -> Bool+eqR Int Int = True+eqR Char Char = True+eqR Float Float = True+eqR Integer Integer = True+eqR Double Double = True+eqR (IO t1) (IO t2) = eqR t1 t2+eqR IOError IOError = True+eqR (Arrow t1 t2) (Arrow s1 s2) = eqR t1 s1 && eqR t2 s2+eqR (Data rc1 _) (Data rc2 _) = eqDT rc1 rc2+eqR (Abstract rc1) (Abstract rc2) = eqDT rc1 rc2+eqR _ _ = False++eqDT :: DT -> DT -> Bool+eqDT (DT str1 rt1) (DT str2 rt2) = str1 == str2 && eqRTup rt1 rt2++instance Eq DT where+   (==) = eqDT++eqRTup :: MTup R t1 -> MTup R t2 -> Bool+eqRTup MNil MNil = True+eqRTup (r1 :+: rt1) (r2 :+: rt2) = eqR r1 r2 && eqRTup rt1 rt2++-- | The type-safe cast operation, explicit arguments+castR :: R a -> R b -> a -> Maybe b+castR (ra::R a) (rb::R b) =+    if eqR ra rb then \(x::a) -> Just (unsafeCoerce# x::b) else \x -> Nothing++-- | The type-safe cast operation, implicit arguments+cast :: forall a b. (Rep a, Rep b) => a -> Maybe b+cast x = castR (rep :: R a) (rep :: R b) x++-- | Leibniz equality between types, explicit representations+gcastR :: forall a b c. R a -> R b -> c a -> Maybe (c b)+gcastR ra rb = if eqR ra rb+        then \(x :: c a) -> Just (unsafeCoerce# x :: c b)+        else \x -> Nothing++-- | Leibniz equality between types, implicit representations+gcast :: forall a b c. (Rep a, Rep b) => c a -> Maybe (c b)+gcast = gcastR (rep :: R a) (rep :: R b)++---------- (Heterogeneous) Ordering -------------------------++-- | Heterogeneous Ordering+compareR :: R a -> R b -> Ordering+compareR Int Int = EQ+compareR Int _   = LT+compareR _   Int = GT+compareR Char Char = EQ+compareR Char _  = LT+compareR _ Char  = GT+compareR Integer Integer = EQ+compareR Integer _  = LT+compareR _ Integer  = GT+compareR Float Float = EQ+compareR Float _  = LT+compareR _ Float  = GT+compareR Rational Rational = EQ+compareR Rational _  = LT+compareR _ Rational  = GT+compareR IOError IOError = EQ+compareR IOError _  = LT+compareR _ IOError  = GT+compareR (IO r1) (IO r2) = compareR r1 r2+compareR (IO _) _  = LT+compareR _ (IO _)  = GT+compareR (Arrow r1 r2) (Arrow r3 r4) =+   case compareR r1 r3 of+      EQ -> compareR r2 r4+      ord -> ord+compareR (Arrow _ _) _  = LT+compareR _ (Arrow _ _)  = GT+compareR (Data dt1 _) (Data dt2 _) =+   compare dt1 dt2+compareR (Data _ _) _ = LT+compareR _ (Data _ _) = GT+compareR (Abstract dt1) (Abstract dt2) =+   compare dt1 dt2+compareR (Abstract _) _ = LT+compareR _ (Abstract _) = GT++instance Ord DT where+  compare (DT str1 reps1) (DT str2 reps2) =+    case compare str1 str2 of+       EQ -> compareMTup reps1 reps2+       other -> other++compareMTup :: MTup R l -> MTup R l' -> Ordering+compareMTup MNil MNil = EQ+compareMTup MNil _    = LT+compareMTup _    MNil = GT+compareMTup (a :+: as) (b :+: bs) =+  case compareR a b of+     EQ -> compareMTup as bs+     other -> other++++--------- Basic instances and library operations for heterogeneous lists ---------------++-- | A datastructure to store the results of findCon+data Val ctx a = forall l.  Val (Emb l a) (MTup ctx l) l++-- | Given a list of constructor representations for a datatype,+-- determine which constructor formed the datatype.+findCon :: [Con ctx a] -> a -> Val ctx a+findCon (Con rcd rec : rest) x = case (from rcd x) of+       Just ys -> Val rcd rec ys+       Nothing -> findCon rest x++-- | A fold right operation for heterogeneous lists, that folds a function+-- expecting a type type representation across each element of the list.+foldr_l :: (forall a. Rep a => ctx a -> a -> b -> b) -> b+            -> (MTup ctx l) -> l -> b+foldr_l f b MNil Nil = b+foldr_l f b (ca :+: cl) (a :*: l) = f ca a (foldr_l f b cl l )++-- | A fold left for heterogeneous lists+foldl_l :: (forall a. Rep a => ctx a -> b -> a -> b) -> b+            -> (MTup ctx l) ->  l -> b+foldl_l f b MNil Nil = b+foldl_l f b (ca :+: cl) (a :*: l) = foldl_l f (f ca b a) cl l++-- | A map for heterogeneous lists+map_l :: (forall a. Rep a => ctx a -> a -> a)+           -> (MTup ctx l) ->  l ->  l+map_l f MNil Nil = Nil+map_l f (ca :+: cl) (a :*: l) = (f ca a) :*: (map_l f cl l)++-- | Transform a heterogeneous list in to a standard list+mapQ_l :: (forall a. Rep a => ctx a -> a -> r) -> MTup ctx l -> l -> [r]+mapQ_l q MNil Nil = []+mapQ_l q (r :+: rs) (a :*: l) = q r a : mapQ_l q rs l++-- | mapM for heterogeneous lists+mapM_l :: (Monad m) => (forall a. Rep a => ctx a -> a -> m a) -> MTup ctx l -> l -> m l+mapM_l f MNil Nil = return Nil+mapM_l f (ca :+: cl) (a :*: l) = do+  x1 <- f ca a+  x2 <- mapM_l f cl l+  return (x1 :*: x2)++-- | Generate a heterogeneous list from metadata+fromTup :: (forall a. Rep a => ctx a -> a) -> MTup ctx l -> l+fromTup f MNil = Nil+fromTup f (b :+: l) = (f b) :*: (fromTup f l)++-- | Generate a heterogeneous list from metadata, in a monad+fromTupM :: (Monad m) => (forall a. Rep a => ctx a -> m a) -> MTup ctx l -> m l+fromTupM f MNil = return Nil+fromTupM f (b :+: l) = do hd <- f b+                          tl <- fromTupM f l+                          return (hd :*: tl)++-- | Generate a normal lists from metadata+toList :: (forall a. Rep a => ctx a -> b) -> MTup ctx l -> [b]+toList f MNil = []+toList f (b :+: l) = f b : toList f l++---------------------  SYB style operations --------------------------++-- | A SYB style traversal+type Traversal = forall a. Rep a => a -> a++-- | Map a traversal across the kids of a data structure+gmapT :: forall a. Rep a => Traversal -> a -> a+gmapT t =+  case (rep :: R a) of+   (Data dt cons) -> \x ->+     case (findCon cons x) of+      Val emb reps ys -> to emb (map_l (const t) reps ys)+   _ -> id+++-- | SYB style query type+type Query r = forall a. Rep a => a -> r++gmapQ :: forall a r. Rep a => Query r -> a -> [r]+gmapQ q =+  case (rep :: R a) of+    (Data dt cons) -> \x -> case (findCon cons x) of+		Val emb reps ys -> mapQ_l (const q) reps ys+    _ -> const []+++-- | SYB style monadic map type+type MapM m = forall a. Rep a => a -> m a++gmapM   :: forall a m. (Rep a, Monad m) => MapM m -> a -> m a+gmapM m = case (rep :: R a) of+   (Data dt cons) -> \x -> case (findCon cons x) of+     Val emb reps ys -> do l <- mapM_l (const m) reps ys+                           return (to emb l)+   _ -> return+++-------------- Generalized  SYB ops ---------------------------++type Traversal1 ctx = forall a. Rep a => ctx a -> a -> a+gmapT1 :: forall a ctx. (Rep1 ctx a) => Traversal1 ctx -> a -> a+gmapT1 t =+  case (rep1 :: R1 ctx a) of+   (Data1 dt cons) -> \x ->+     case (findCon cons x) of+      Val emb recs kids -> to emb (map_l t recs kids)+   _ -> id++type Query1 ctx r = forall a. Rep a => ctx a -> a -> r+gmapQ1 :: forall a ctx r. (Rep1 ctx a) => Query1 ctx r -> a -> [r]+gmapQ1 q  =+  case (rep1 :: R1 ctx a) of+    (Data1 dt cons) -> \x -> case (findCon cons x) of+		Val emb recs kids -> mapQ_l q recs kids+    _ -> const []++type MapM1 ctx m = forall a. Rep a => ctx a -> a -> m a+gmapM1  :: forall a ctx m. (Rep1 ctx a, Monad m) => MapM1 ctx m -> a -> m a+gmapM1 m = case (rep1 :: R1 ctx a) of+   (Data1 dt cons) -> \x -> case (findCon cons x) of+     Val emb rec ys -> do l <- mapM_l m rec ys+                          return (to emb l)+   _ -> return++-------------- Spine from SYB Reloaded ---------------------------++data Typed a = a ::: R a+infixr 7 :::++data Spine a where+	 Constr :: a -> Spine a+	 (:<>)  :: Spine (a -> b) -> Typed a -> Spine b++toSpineR :: R a -> a -> Spine a+toSpineR (Data _ cons) a =+	 case (findCon cons a) of+	    Val emb reps kids -> toSpineRl reps kids (to emb)+toSpineR _ a = Constr a++toSpineRl :: MTup R l -> l -> (l -> a) -> Spine a+toSpineRl MNil Nil into = Constr (into Nil)+toSpineRl (ra :+: rs) (a :*: l) into =+	 (toSpineRl rs l into') :<> (a ::: ra)+		  where into' tl1 x1 = into (x1 :*: tl1)++toSpine :: Rep a => a -> Spine a+toSpine = toSpineR rep++fromSpine :: Spine a -> a+fromSpine (Constr x) = x+fromSpine (x :<> (y:::_)) = fromSpine x y+

@@ -0,0 +1,373 @@+{-# LANGUAGE RankNTypes #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Generics.RepLib.SYB.Aliases+-- Copyright   :  (c) The University of Pennsylvania, 2006+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--++-- This module is derived from Data.Generics.Aliases+--+-- The present module provides a number of declarations for typical+-- generic function types, corresponding type case, and others.+--+--+-----------------------------------------------------------------------------+module Generics.RepLib.SYB.Aliases (++	-- * Combinators to \"make\" generic functions via cast+	mkT, mkQ, mkM, mkMp, mkR,+	ext0, extT, extQ, extM, extMp, extB, extR,++	-- * Type synonyms for generic function types+	GenericT,+	GenericQ,+	GenericM,+	GenericB,+	GenericR,+   Generic,+   Generic'(..),+   GenericT'(..),+   GenericQ'(..),+   GenericM'(..),++	-- * Inredients of generic functions+	orElse,++	-- * Function combinators on generic functions+	recoverMp,+	recoverQ,+	choiceMp,+	choiceQ++	-- * Type extension for unary type constructors+--	ext1T,+--	ext1M,+--	ext1Q,+--	ext1R++  ) where++import Control.Monad+import Generics.RepLib.R+import Generics.RepLib.RepAux++-- Derived from Data.Generics.Aliases+-- Only modification: "Data" and "Typeable" classes become "Rep" class+--   otherwise import our version of the libraries++------------------------------------------------------------------------------+--+--	Combinators to "make" generic functions+--	We use type-safe cast in a number of ways to make generic functions.+--+------------------------------------------------------------------------------++-- | Make a generic transformation;+--   start from a type-specific case;+--   preserve the term otherwise+--+mkT :: ( Rep a+       , Rep b+       )+    => (b -> b)+    -> a+    -> a+mkT = extT id+++-- | Make a generic query;+--   start from a type-specific case;+--   return a constant otherwise+--+mkQ :: ( Rep a+       , Rep b+       )+    => r+    -> (b -> r)+    -> a+    -> r+(r `mkQ` br) a = case cast a of+                        Just b  -> br b+                        Nothing -> r+++-- | Make a generic monadic transformation;+--   start from a type-specific case;+--   resort to return otherwise+--+mkM :: ( Monad m+       , Rep a+       , Rep b+       )+    => (b -> m b)+    -> a+    -> m a+mkM = extM return+++{-++For the remaining definitions, we stick to a more concise style, i.e.,+we fold maybies with "maybe" instead of case ... of ..., and we also+use a point-free style whenever possible.++-}+++-- | Make a generic monadic transformation for MonadPlus;+--   use \"const mzero\" (i.e., failure) instead of return as default.+--+mkMp :: ( MonadPlus m+        , Rep a+        , Rep b+        )+     => (b -> m b)+     -> a+     -> m a+mkMp = extM (const mzero)+++-- | Make a generic builder;+--   start from a type-specific ase;+--   resort to no build (i.e., mzero) otherwise+--+mkR :: ( MonadPlus m+       , Rep a+       , Rep b+       )+    => m b -> m a+mkR f = mzero `extR` f+++-- | Flexible type extension+ext0 :: (Rep a, Rep b) => c a -> c b -> c a+ext0 def ext = maybe def id (gcast ext)+++-- | Extend a generic transformation by a type-specific case+extT :: ( Rep a+        , Rep b+        )+     => (a -> a)+     -> (b -> b)+     -> a+     -> a+extT def ext = unT ((T def) `ext0` (T ext))+++-- | Extend a generic query by a type-specific case+extQ :: ( Rep a+        , Rep b+        )+     => (a -> q)+     -> (b -> q)+     -> a+     -> q+extQ f g a = maybe (f a) g (cast a)+++-- | Extend a generic monadic transformation by a type-specific case+extM :: ( Monad m+        , Rep a+        , Rep b+        )+     => (a -> m a) -> (b -> m b) -> a -> m a+extM def ext = unM ((M def) `ext0` (M ext))+++-- | Extend a generic MonadPlus transformation by a type-specific case+extMp :: ( MonadPlus m+         , Rep a+         , Rep b+         )+      => (a -> m a) -> (b -> m b) -> a -> m a+extMp = extM+++-- | Extend a generic builder+extB :: ( Rep a+        , Rep b+        )+     => a -> b -> a+extB a = maybe a id . cast+++-- | Extend a generic reader+extR :: ( Monad m+        , Rep a+        , Rep b+        )+     => m a -> m b -> m a+extR def ext = unR ((R def) `ext0` (R ext))++++------------------------------------------------------------------------------+--+--	Type synonyms for generic function types+--+------------------------------------------------------------------------------+++-- | Generic transformations,+--   i.e., take an \"a\" and return an \"a\"+--+type GenericT = forall a. Rep a => a -> a+++-- | Generic queries of type \"r\",+--   i.e., take any \"a\" and return an \"r\"+--+type GenericQ r = forall a. Rep a => a -> r+++-- | Generic monadic transformations,+--   i.e., take an \"a\" and compute an \"a\"+--+type GenericM m = forall a. Rep a => a -> m a+++-- | Generic builders+--   i.e., produce an \"a\".+--+type GenericB = forall a. Rep a => a+++-- | Generic readers, say monadic builders,+--   i.e., produce an \"a\" with the help of a monad \"m\".+--+type GenericR m = forall a. Rep a => m a+++-- | The general scheme underlying generic functions+--   assumed by gfoldl; there are isomorphisms such as+--   GenericT = Generic T.+--+type Generic c = forall a. Rep a => a -> c a+++-- | Wrapped generic functions;+--   recall: [Generic c] would be legal but [Generic' c] not.+--+data Generic' c = Generic' { unGeneric' :: Generic c }+++-- | Other first-class polymorphic wrappers+newtype GenericT'   = GT { unGT :: Rep a => a -> a }+newtype GenericQ' r = GQ { unGQ :: GenericQ r }+newtype GenericM' m = GM { unGM :: Rep a => a -> m a }+++-- | Left-biased choice on maybies+orElse :: Maybe a -> Maybe a -> Maybe a+x `orElse` y = case x of+                 Just _  -> x+                 Nothing -> y+++{-++The following variations take "orElse" to the function+level. Furthermore, we generalise from "Maybe" to any+"MonadPlus". This makes sense for monadic transformations and+queries. We say that the resulting combinators modell choice. We also+provide a prime example of choice, that is, recovery from failure. In+the case of transformations, we recover via return whereas for+queries a given constant is returned.++-}++-- | Choice for monadic transformations+choiceMp :: MonadPlus m => GenericM m -> GenericM m -> GenericM m+choiceMp f g x = f x `mplus` g x+++-- | Choice for monadic queries+choiceQ :: MonadPlus m => GenericQ (m r) -> GenericQ (m r) -> GenericQ (m r)+choiceQ f g x = f x `mplus` g x+++-- | Recover from the failure of monadic transformation by identity+recoverMp :: MonadPlus m => GenericM m -> GenericM m+recoverMp f = f `choiceMp` return+++-- | Recover from the failure of monadic query by a constant+recoverQ :: MonadPlus m => r -> GenericQ (m r) -> GenericQ (m r)+recoverQ r f = f `choiceQ` const (return r)++++------------------------------------------------------------------------------+--+--	Type extension for unary type constructors+--+------------------------------------------------------------------------------++{-+++-- | Flexible type extension+ext1 :: (Rep a, Typeable1 t)+     => c a+     -> (forall a. Rep a => c (t a))+     -> c a+ext1 def ext = maybe def id (dataCast1 ext)+++-- | Type extension of transformations for unary type constructors+ext1T :: (Rep d, Typeable1 t)+      => (forall d. Rep d => d -> d)+      -> (forall d. Rep d => t d -> t d)+      -> d -> d+ext1T def ext = unT ((T def) `ext1` (T ext))+++-- | Type extension of monadic transformations for type constructors+ext1M :: (Monad m, Rep d, Typeable1 t)+      => (forall d. Rep d => d -> m d)+      -> (forall d. Rep d => t d -> m (t d))+      -> d -> m d+ext1M def ext = unM ((M def) `ext1` (M ext))+++-- | Type extension of queries for type constructors+ext1Q :: (Rep d, Typeable1 t)+      => (d -> q)+      -> (forall d. Rep d => t d -> q)+      -> d -> q+ext1Q def ext = unQ ((Q def) `ext1` (Q ext))+++-- | Type extension of readers for type constructors+ext1R :: (Monad m, Rep d, Typeable1 t)+      => m d+      -> (forall d. Rep d => m (t d))+      -> m d+ext1R def ext = unR ((R def) `ext1` (R ext))++-}++------------------------------------------------------------------------------+--+--	Type constructors for type-level lambdas+--+------------------------------------------------------------------------------+++-- | The type constructor for transformations+newtype T x = T { unT :: x -> x }++-- | The type constructor for transformations+newtype M m x = M { unM :: x -> m x }++-- | The type constructor for queries+newtype Q q x = Q { unQ :: x -> q }++-- | The type constructor for readers+newtype R m x = R { unR :: m x }