unbound-generics 0.2 → 0.3

raw patch · 16 files changed

+202/−117 lines, 16 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Changelog.md +6/−0
• README.md +9/−2
• src/Unbound/Generics/LocallyNameless/Alpha.hs +132/−68
• src/Unbound/Generics/LocallyNameless/Bind.hs +2/−2
• src/Unbound/Generics/LocallyNameless/Embed.hs +6/−6
• src/Unbound/Generics/LocallyNameless/Operations.hs +11/−9
• src/Unbound/Generics/LocallyNameless/Rebind.hs +2/−2
• src/Unbound/Generics/LocallyNameless/Rec.hs +7/−5
• src/Unbound/Generics/LocallyNameless/Shift.hs +4/−4
• src/Unbound/Generics/LocallyNameless/TH.hs +6/−6
• src/Unbound/Generics/LocallyNameless/Unsafe.hs +1/−1
• test/Calc.hs +2/−2
• test/PropOpenClose.hs +2/−2
• test/TestTH.hs +5/−3
• test/TinyLam.hs +3/−3
• unbound-generics.cabal +4/−2

@@ -1,3 +1,9 @@+# 0.3++* Change types of `open` and `close` to take `NthPatFind` and `NamePatFind` instead of generic patterns, update call sites.+* Add newtype wrappers and Monoid instances for `NthPatFind` and `NamePatFind`+* Change `isTerm` to return `All` instead of `Bool`+ # 0.2  * Incorporating some of the extras/oversights from

@@ -1,5 +1,7 @@ # unbound-generics +[![Join the chat at https://gitter.im/lambdageek/unbound-generics](https://badges.gitter.im/Join%20Chat.svg)](https://gitter.im/lambdageek/unbound-generics?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge)+ [![Build Status](https://travis-ci.org/lambdageek/unbound-generics.svg)](https://travis-ci.org/lambdageek/unbound-generics)  Support for programming with names and binders using GHC Generics.@@ -75,10 +77,15 @@    The `fv` method returns a `Fold` (in the sense of the [lens](http://hackage.haskell.org/package/lens) library),    rather than an `Unbound.Util.Collection` instance.  That means you will generally have to write `toListOf fv t` or some    other summary operation. -2. `isPat :: Alpha t => t -> DisjointSet AnyName`+2. Utility methods in the `Alpha` class have different types.     You should only notice this if you're implementing an instance of `Alpha` by hand (rather than by using the default-   generic instance).  The original `unbound` returned a `Maybe [AnyName]` here with the same interpretation as `DisjointSet`: `Nothing` means an inconsistency was encountered, or `Just` the free variables of the pattern.+   generic instance).+   +   1. `isPat :: Alpha t => t -> DisjointSet AnyName`+     The original `unbound` returned a `Maybe [AnyName]` here with the same interpretation as `DisjointSet`: `Nothing` means an inconsistency was encountered, or `Just` the free variables of the pattern.+   2. `isTerm :: Alpha t => t -> All`+   3. `open :: Alpha t => AlphaCtx -> NthPatFind -> t -> t`, `close :: Alpha t => AlphaCtx -> NamePatFind -> t -> t` where `NthPatFind` and `NamePatFind` are newtypes  3. `embed :: IsEmbed e => Embedded e -> e` and `unembed :: IsEmbed e => e -> Embedded e` 

@@ -22,8 +22,8 @@   , isConsistentDisjointSet   , isNullDisjointSet   -- * Implementation details-  , NthPatFind-  , NamePatFind+  , NthPatFind(..)+  , NamePatFind(..)   , AlphaCtx   , initialCtx   , patternCtx@@ -58,7 +58,7 @@ import Data.Functor.Contravariant (Contravariant(..)) import Data.Foldable (Foldable(..)) import Data.List (intersect)-import Data.Monoid (Monoid(..), (<>))+import Data.Monoid (Monoid(..), (<>), All(..)) import Data.Ratio (Ratio) import Data.Typeable (Typeable, gcast, typeOf) import GHC.Generics@@ -157,6 +157,7 @@   aeq' :: AlphaCtx -> a -> a -> Bool   default aeq' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Bool   aeq' c = (gaeq c) `on` from+  {-# INLINE aeq' #-}    -- | See 'Unbound.Generics.LocallyNameless.Operations.fvAny'.   --@@ -166,26 +167,31 @@   fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a   default fvAny' :: (Generic a, GAlpha (Rep a), Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a   fvAny' c nfn = fmap to . gfvAny c nfn . from+  {-# INLINE fvAny' #-}    -- | Replace free names by bound names.-  close :: Alpha b => AlphaCtx -> b -> a -> a-  default close :: (Generic a, GAlpha (Rep a), Alpha b) => AlphaCtx -> b -> a -> a+  close :: AlphaCtx -> NamePatFind -> a -> a+  default close :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> NamePatFind -> a -> a   close c b = to . gclose c b . from+  {-# INLINE close #-}    -- | Replace bound names by free names.-  open :: Alpha b => AlphaCtx -> b -> a -> a-  default open :: (Generic a, GAlpha (Rep a), Alpha b) => AlphaCtx -> b -> a -> a+  open :: AlphaCtx -> NthPatFind -> a -> a+  default open :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> NthPatFind -> a -> a   open c b = to . gopen c b . from+  {-# INLINE open #-}    -- | @isPat x@ dynamically checks whether @x@ can be used as a valid pattern.   isPat :: a -> DisjointSet AnyName   default isPat :: (Generic a, GAlpha (Rep a)) => a -> DisjointSet AnyName   isPat = gisPat . from+  {-# INLINE isPat #-}    -- | @isPat x@ dynamically checks whether @x@ can be used as a valid term.-  isTerm :: a -> Bool-  default isTerm :: (Generic a, GAlpha (Rep a)) => a -> Bool+  isTerm :: a -> All+  default isTerm :: (Generic a, GAlpha (Rep a)) => a -> All   isTerm = gisTerm . from+  {-# INLINE isTerm #-}    -- | @isEmbed@ is needed internally for the implementation of   --   'isPat'.  @isEmbed@ is true for terms wrapped in 'Embed' and zero@@ -193,6 +199,7 @@   --   simply returns @False@.   isEmbed :: a -> Bool   isEmbed _ = False+  {-# INLINE isEmbed #-}    -- | If @a@ is a pattern, finds the @n@th name in the pattern   -- (starting from zero), returning the number of names encountered@@ -200,23 +207,27 @@   nthPatFind :: a -> NthPatFind   default nthPatFind :: (Generic a, GAlpha (Rep a)) => a -> NthPatFind   nthPatFind = gnthPatFind . from+  {-# INLINE nthPatFind #-}    -- | If @a@ is a pattern, find the index of the given name in the pattern.   namePatFind :: a -> NamePatFind   default namePatFind :: (Generic a, GAlpha (Rep a)) => a -> NamePatFind   namePatFind = gnamePatFind . from+  {-# INLINE namePatFind #-}    -- | See 'Unbound.Generics.LocallyNameless.Operations.swaps'. Apply   -- the given permutation of variable names to the given pattern.   swaps' :: AlphaCtx -> Perm AnyName -> a -> a   default swaps' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> Perm AnyName -> a -> a   swaps' ctx perm = to . gswaps ctx perm . from+  {-# INLINE swaps' #-}    -- | See 'Unbound.Generics.LocallyNameless.Operations.freshen'.   lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b   default lfreshen' :: (LFresh m, Generic a, GAlpha (Rep a))                        => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b   lfreshen' ctx m cont = glfreshen ctx (from m) (cont . to)+  {-# INLINE lfreshen' #-}    -- | See 'Unbound.Generics.LocallyNameless.Operations.freshen'.  Rename the free variables   -- in the given term to be distinct from all other names seen in the monad @m@.@@ -275,28 +286,46 @@     j mmf = mmf >>= \mf -> mf {-# INLINE retractFFM #-} --- | The result of @'nthPatFind' a i@ is @Left k@ where @k@ is the--- number of names in pattern @a@ with @k < i@ or @Right x@ where @x@+-- | The result of @'nthPatFind' a i@ is @Left k@ where @i-k@ is the+-- number of names in pattern @a@ (with @k < i@) or @Right x@ where @x@ -- is the @i@th name in @a@-type NthPatFind = Integer -> Either Integer AnyName+newtype NthPatFind = NthPatFind { runNthPatFind :: Integer -> Either Integer AnyName } +instance Monoid NthPatFind where+  mempty = NthPatFind Left+  mappend (NthPatFind f) (NthPatFind g) =+    NthPatFind $ \i -> case f i of+    Left i' -> g i'+    found@Right {} -> found+ -- | The result of @'namePatFind' a x@ is either @Left i@ if @a@ is a pattern that -- contains @i@ free names none of which are @x@, or @Right j@ if @x@ is the @j@th name -- in @a@-type NamePatFind = AnyName -> Either Integer Integer -- Left - names skipped over-                                                     -- Right - index of the name we found+newtype NamePatFind = NamePatFind { runNamePatFind :: AnyName+                                                      -- Left - names skipped over+                                                      -- Right - index of the name we found+                                                      -> Either Integer Integer } +instance Monoid NamePatFind where+  mempty = NamePatFind (\_ -> Left 0)+  mappend (NamePatFind f) (NamePatFind g) =+    NamePatFind $ \nm -> case f nm of+    ans@Right {} -> ans+    Left n -> case g nm of+      Left m -> Left $! n + m+      Right i -> Right $! n + i+ -- | The "Generic" representation version of 'Alpha' class GAlpha f where   gaeq :: AlphaCtx -> f a -> f a -> Bool    gfvAny :: (Contravariant g, Applicative g) => AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a) -  gclose :: Alpha b => AlphaCtx -> b -> f a -> f a-  gopen :: Alpha b => AlphaCtx -> b -> f a -> f a+  gclose :: AlphaCtx -> NamePatFind -> f a -> f a+  gopen :: AlphaCtx -> NthPatFind -> f a -> f a    gisPat :: f a -> DisjointSet AnyName-  gisTerm :: f a -> Bool+  gisTerm :: f a -> All    gnthPatFind :: f a -> NthPatFind   gnamePatFind :: f a -> NamePatFind@@ -310,51 +339,72 @@  instance (Alpha c) => GAlpha (K1 i c) where   gaeq ctx (K1 c1) (K1 c2) = aeq' ctx c1 c2+  {-# INLINE gaeq #-}    gfvAny ctx nfn = fmap K1 . fvAny' ctx nfn . unK1-+  {-# INLINE gfvAny #-}+     gclose ctx b = K1 . close ctx b . unK1+  {-# INLINE gclose #-}   gopen ctx b = K1 . open ctx b . unK1+  {-# INLINE gopen #-}    gisPat = isPat . unK1+  {-# INLINE gisPat #-}   gisTerm = isTerm . unK1+  {-# INLINE gisTerm #-}    gnthPatFind = nthPatFind . unK1+  {-# INLINE gnthPatFind #-}   gnamePatFind = namePatFind . unK1+  {-# INLINE gnamePatFind #-}    gswaps ctx perm = K1 . swaps' ctx perm . unK1+  {-# INLINE gswaps #-}   gfreshen ctx = liftM (first K1) . liftFFM . freshen' ctx . unK1   {-# INLINE gfreshen #-}    glfreshen ctx (K1 c) cont = lfreshen' ctx c (cont . K1)+  {-# INLINE glfreshen #-}    gacompare ctx (K1 c1) (K1 c2) = acompare' ctx c1 c2  instance GAlpha f => GAlpha (M1 i c f) where   gaeq ctx (M1 f1) (M1 f2) = gaeq ctx f1 f2+  {-# INLINE gaeq #-}    gfvAny ctx nfn = fmap M1 . gfvAny ctx nfn . unM1+  {-# INLINE gfvAny #-}    gclose ctx b = M1 . gclose ctx b . unM1+  {-# INLINE gclose #-}   gopen ctx b = M1 . gopen ctx b . unM1+  {-# INLINE gopen #-}    gisPat = gisPat . unM1+  {-# INLINE gisPat #-}   gisTerm = gisTerm . unM1+  {-# INLINE gisTerm #-}    gnthPatFind = gnthPatFind . unM1+  {-# INLINE gnthPatFind #-}   gnamePatFind = gnamePatFind . unM1+  {-# INLINE gnamePatFind #-}    gswaps ctx perm = M1 . gswaps ctx perm . unM1+  {-# INLINE gswaps #-}   gfreshen ctx = liftM (first M1) . gfreshen ctx . unM1   {-# INLINE gfreshen #-}    glfreshen ctx (M1 f) cont =     glfreshen ctx f (cont . M1)+  {-# INLINE glfreshen #-}    gacompare ctx (M1 f1) (M1 f2) = gacompare ctx f1 f2  instance GAlpha U1 where   gaeq _ctx _ _ = True+  {-# INLINE gaeq #-}    gfvAny _ctx _nfn _ = pure U1 @@ -362,10 +412,10 @@   gopen _ctx _b _ = U1    gisPat _ = mempty-  gisTerm _ = True+  gisTerm _ = mempty -  gnthPatFind _ = Left-  gnamePatFind _ _ = Left 0+  gnthPatFind _ = mempty+  gnamePatFind _ = mempty    gswaps _ctx _perm _ = U1   gfreshen _ctx _ = return (U1, mempty)@@ -377,6 +427,7 @@  instance GAlpha V1 where   gaeq _ctx _ _ = False+  {-# INLINE gaeq #-}    gfvAny _ctx _nfn = pure @@ -384,10 +435,10 @@   gopen _ctx _b _ = undefined    gisPat _ = mempty-  gisTerm _ = False+  gisTerm _ = mempty -  gnthPatFind _ = Left-  gnamePatFind _ _ = Left 0+  gnthPatFind _ = mempty+  gnamePatFind _ = mempty    gswaps _ctx _perm _ = undefined   gfreshen _ctx _ = return (undefined, mempty)@@ -400,27 +451,30 @@ instance (GAlpha f, GAlpha g) => GAlpha (f :*: g) where   gaeq ctx (f1 :*: g1) (f2 :*: g2) =     gaeq ctx f1 f2 && gaeq ctx g1 g2+  {-# INLINE gaeq #-}    gfvAny ctx nfn (f :*: g) = (:*:) <$> gfvAny ctx nfn f                                    <*> gfvAny ctx nfn g+  {-# INLINE gfvAny #-}    gclose ctx b (f :*: g) = gclose ctx b f :*: gclose ctx b g+  {-# INLINE gclose #-}   gopen ctx b (f :*: g) = gopen ctx b f :*: gopen ctx b g+  {-# INLINE gopen #-}    gisPat (f :*: g) = gisPat f <> gisPat g-  gisTerm (f :*: g) = gisTerm f && gisTerm g+  {-# INLINE gisPat #-}+  gisTerm (f :*: g) = gisTerm f <> gisTerm g+  {-# INLINE gisTerm #-} -  gnthPatFind (f :*: g) i = case gnthPatFind f i of-    Left i' -> gnthPatFind g i'-    Right ans -> Right ans-  gnamePatFind (f :*: g) n = case gnamePatFind f n of-    Left j -> case gnamePatFind g n of-      Left i -> Left $! j + i-      Right k -> Right $! j + k-    Right k -> Right k+  gnthPatFind (f :*: g) = gnthPatFind f <> gnthPatFind g+  {-# INLINE gnthPatFind #-}+  gnamePatFind (f :*: g) = gnamePatFind f <> gnamePatFind g+  {-# INLINE gnamePatFind #-}    gswaps ctx perm (f :*: g) =     gswaps ctx perm f :*: gswaps ctx perm g+  {-# INLINE gswaps #-}    gfreshen ctx (f :*: g) = do     ~(g', perm2) <- gfreshen ctx g@@ -432,6 +486,7 @@     glfreshen ctx g $ \g' perm2 ->     glfreshen ctx (gswaps ctx perm2 f) $ \f' perm1 ->     cont (f' :*: g') (perm1 <> perm2)+  {-# INLINE glfreshen #-}    gacompare ctx (f1 :*: g1) (f2 :*: g2) =     (gacompare ctx f1 f2) <> (gacompare ctx g1 g2)@@ -440,29 +495,38 @@   gaeq ctx  (L1 f1) (L1 f2) = gaeq ctx f1 f2   gaeq ctx  (R1 g1) (R1 g2) = gaeq ctx g1 g2   gaeq _ctx _       _       = False+  {-# INLINE gaeq #-}    gfvAny ctx nfn (L1 f) = fmap L1 (gfvAny ctx nfn f)   gfvAny ctx nfn (R1 g) = fmap R1 (gfvAny ctx nfn g)-+  {-# INLINE gfvAny #-}+     gclose ctx b (L1 f) = L1 (gclose ctx b f)   gclose ctx b (R1 g) = R1 (gclose ctx b g)+  {-# INLINE gclose #-}   gopen ctx b (L1 f) = L1 (gopen ctx b f)   gopen ctx b (R1 g) = R1 (gopen ctx b g)+  {-# INLINE gopen #-}    gisPat (L1 f) = gisPat f   gisPat (R1 g) = gisPat g+  {-# INLINE gisPat #-}    gisTerm (L1 f) = gisTerm f   gisTerm (R1 g) = gisTerm g+  {-# INLINE gisTerm #-} -  gnthPatFind (L1 f) i = gnthPatFind f i-  gnthPatFind (R1 g) i = gnthPatFind g i-  -  gnamePatFind (L1 f) n = gnamePatFind f n-  gnamePatFind (R1 g) n = gnamePatFind g n+  gnthPatFind (L1 f) = gnthPatFind f+  gnthPatFind (R1 g) = gnthPatFind g+  {-# INLINE gnthPatFind #-} +  gnamePatFind (L1 f) = gnamePatFind f+  gnamePatFind (R1 g) = gnamePatFind g+  {-# INLINE gnamePatFind #-}+   gswaps ctx perm (L1 f) = L1 (gswaps ctx perm f)   gswaps ctx perm (R1 f) = R1 (gswaps ctx perm f)+  {-# INLINE gswaps #-}    gfreshen ctx (L1 f) = liftM (first L1) (gfreshen ctx f)   gfreshen ctx (R1 f) = liftM (first R1) (gfreshen ctx f)@@ -472,11 +536,13 @@     glfreshen ctx f (cont . L1)   glfreshen ctx (R1 g) cont =     glfreshen ctx g (cont . R1)+  {-# INLINE glfreshen #-}    gacompare _ctx (L1 _) (R1 _)   = LT   gacompare _ctx (R1 _) (L1 _)   = GT   gacompare ctx  (L1 f1) (L1 f2) = gacompare ctx f1 f2   gacompare ctx  (R1 g1) (R1 g2) = gacompare ctx g1 g2+  {-# INLINE gacompare #-}  -- ============================================================ -- Alpha instances for the usual types@@ -490,10 +556,10 @@   open _ctx _b i = i    isPat _ = mempty-  isTerm _ = True+  isTerm _ = mempty -  nthPatFind _ = Left-  namePatFind _ _ = Left 0+  nthPatFind _ = mempty+  namePatFind _ = mempty    swaps' _ctx _p i = i   freshen' _ctx i = return (i, mempty)@@ -510,10 +576,10 @@   open _ctx _b i = i    isPat _ = mempty-  isTerm _ = True+  isTerm _ = mempty -  nthPatFind _ = Left-  namePatFind _ _ = Left 0+  nthPatFind _ = mempty+  namePatFind _ = mempty    swaps' _ctx _p i = i   freshen' _ctx i = return (i, mempty)@@ -530,10 +596,10 @@   open _ctx _b i = i    isPat _ = mempty-  isTerm _ = True+  isTerm _ = mempty -  nthPatFind _ = Left-  namePatFind _ _ = Left 0+  nthPatFind _ = mempty+  namePatFind _ = mempty    swaps' _ctx _p i = i   freshen' _ctx i = return (i, mempty)@@ -550,10 +616,10 @@   open _ctx _b i = i    isPat _ = mempty-  isTerm _ = True+  isTerm _ = mempty -  nthPatFind _ = Left-  namePatFind _ _ = Left 0+  nthPatFind _ = mempty+  namePatFind _ = mempty    swaps' _ctx _p i = i   freshen' _ctx i = return (i, mempty)@@ -570,10 +636,10 @@   open _ctx _b i = i    isPat _ = mempty-  isTerm _ = True+  isTerm _ = mempty -  nthPatFind _ = Left-  namePatFind _ _ = Left 0+  nthPatFind _ = mempty+  namePatFind _ = mempty    swaps' _ctx _p i = i   freshen' _ctx i = return (i, mempty)@@ -590,10 +656,10 @@   open _ctx _b i = i    isPat _ = mempty-  isTerm _ = True+  isTerm _ = mempty -  nthPatFind _ = Left-  namePatFind _ _ = Left 0+  nthPatFind _ = mempty+  namePatFind _ = mempty    swaps' _ctx _p i = i   freshen' _ctx i = return (i, mempty)@@ -629,7 +695,7 @@    open ctx b a@(Bn l k) =     if ctxMode ctx == Term && ctxLevel ctx == l-    then case nthPatFind b k of+    then case runNthPatFind b k of       Right (AnyName nm) -> case gcast nm of         Just nm' -> nm'         Nothing -> error "LocallyNameless.open: inconsistent sorts"@@ -640,7 +706,7 @@    close ctx b a@(Fn _ _) =     if isTermCtx ctx-    then case namePatFind b (AnyName a) of+    then case runNamePatFind b (AnyName a) of       Right k -> Bn (ctxLevel ctx) k       Left _ -> a     else a@@ -651,12 +717,12 @@             then singletonDisjointSet (AnyName n)             else inconsistentDisjointSet -  isTerm _ = True+  isTerm _ = mempty -  nthPatFind nm i =+  nthPatFind nm = NthPatFind $ \i ->     if i == 0 then Right (AnyName nm) else Left $! i-1 -  namePatFind nm1 (AnyName nm2) =+  namePatFind nm1 = NamePatFind $ \(AnyName nm2) ->     case gcast nm1 of       Just nm1' -> if nm1' == nm2 then Right 0 else Left 1       Nothing -> Left 1@@ -711,7 +777,7 @@                                   then nfn n                                   else pure n -  isTerm _ = True+  isTerm _ = mempty    isPat n@(AnyName nm) = if isFreeName nm                          then singletonDisjointSet n@@ -740,13 +806,11 @@    close ctx b (AnyName nm) = AnyName (close ctx b nm)     -  nthPatFind nm i =+  nthPatFind nm = NthPatFind $ \i ->     if i == 0 then Right nm else Left $! i - 1 -  namePatFind nmHave nmWant =-    if nmHave == nmWant-    then Right 0-    else Left 1+  namePatFind nmHave = NamePatFind $ \nmWant ->+    if nmHave == nmWant then Right 0 else Left 1    acompare' _ x y | x == y = EQ 

@@ -19,7 +19,7 @@  import Control.Applicative (Applicative(..), (<$>)) import Control.DeepSeq (NFData(..))-import Data.Monoid ((<>))+import Data.Monoid ((<>), All(..))  import GHC.Generics (Generic) @@ -55,7 +55,7 @@    isPat _ = inconsistentDisjointSet -  isTerm (B p t) = isConsistentDisjointSet (isPat p) && isTerm t+  isTerm (B p t) = (All $ isConsistentDisjointSet $ isPat p) <> isTerm t    close ctx b (B p t) =     B (close (patternCtx ctx) b p) (close (incrLevelCtx ctx) b t)

@@ -12,7 +12,7 @@  import Control.Applicative (pure, (<$>)) import Control.DeepSeq (NFData(..))-import Data.Monoid (mempty)+import Data.Monoid (mempty, All(..)) import Data.Profunctor (Profunctor(..))  import GHC.Generics (Generic)@@ -57,11 +57,11 @@   showsPrec _ (Embed a) = showString "{" . showsPrec 0 a . showString "}"  instance Alpha t => Alpha (Embed t) where-  isPat (Embed t) = if (isTerm t) then mempty else inconsistentDisjointSet+  isPat (Embed t) = if getAll (isTerm t) then mempty else inconsistentDisjointSet -  isTerm _ = False+  isTerm _ = All False -  isEmbed (Embed t) = isTerm t+  isEmbed (Embed t) = getAll (isTerm t)    swaps' ctx perm (Embed t) =     if isTermCtx ctx@@ -96,7 +96,7 @@     then error "LocallyNameless.open on Embed"     else Embed (open (termCtx ctx) b x) -  nthPatFind _ = Left-  namePatFind _ _ = Left 0+  nthPatFind _ = mempty+  namePatFind _ = mempty    acompare' ctx (Embed x) (Embed y) = acompare' (termCtx ctx) x y

@@ -109,7 +109,7 @@    -- | @'bind' p t@ closes over the variables of pattern @p@ in the term @t@ bind :: (Alpha p, Alpha t) => p -> t -> Bind p t-bind p t = B p (close initialCtx p t)+bind p t = B p (close initialCtx (namePatFind p) t)  -- | @'unbind' b@ lets you descend beneath a binder @b :: 'Bind' p t@ -- by returning the pair of the pattern @p@ and the term @t@ where the@@ -118,7 +118,7 @@ unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t) unbind (B p t) = do   (p', _) <- freshen p-  return (p', open initialCtx p' t)+  return (p', open initialCtx (nthPatFind p') t)  -- | @lunbind@ opens a binding in an 'LFresh' monad, ensuring that the --   names chosen for the binders are /locally/ fresh.  The components@@ -130,7 +130,7 @@ --   class. lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c lunbind (B p t) cont =-  lfreshen p (\x _ -> cont (x, open initialCtx x t))+  lfreshen p (\x _ -> cont (x, open initialCtx (nthPatFind x) t))   -- | Simultaneously unbind two patterns in two terms, returning 'Nothing' if@@ -143,8 +143,9 @@       case mkPerm (toListOf fvAny p2) (toListOf fvAny p1) of          Just pm -> do            (p1', pm') <- freshen p1-           return $ Just (p1', open initialCtx p1' t1,-                          swaps (pm' <> pm) p2, open initialCtx p1' t2)+           let npf = nthPatFind p1'+           return $ Just (p1', open initialCtx npf t1,+                          swaps (pm' <> pm) p2, open initialCtx npf t2)          Nothing -> return Nothing  -- | Simultaneously 'lunbind' two patterns in two terms in the 'LFresh' monad,@@ -160,8 +161,9 @@   case mkPerm (toListOf fvAny p2) (toListOf fvAny p1) of     Just pm ->       lfreshen p1 $ \p1' pm' ->-      cont $ Just (p1', open initialCtx p1' t1,-                   swaps (pm' <> pm) p2, open initialCtx p1' t2)+      cont $ let npf = nthPatFind p1'+             in Just (p1', open initialCtx npf t1,+                      swaps (pm' <> pm) p2, open initialCtx npf t2)     Nothing -> cont Nothing  -- | Simultaneously unbind two patterns in two terms, returning 'mzero' if@@ -177,7 +179,7 @@ -- captures the variables of pattern @p1@ that occur within @p2@ in -- addition to providing binding occurrences for all the variables of @p1@ and @p2@ rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2-rebind p1 p2 = Rebnd p1 (close (patternCtx initialCtx) p1 p2)+rebind p1 p2 = Rebnd p1 (close (patternCtx initialCtx) (namePatFind p1) p2)  -- | @'unrebind' p@ is the elimination form for 'Rebind'. It is not -- monadic (unlike 'unbind') because a @Rebind@ pattern can only occur@@ -185,7 +187,7 @@ -- must have already been called and all names apropriately -- 'freshen'ed. unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)-unrebind (Rebnd p1 p2) = (p1, open (patternCtx initialCtx) p1 p2)+unrebind (Rebnd p1 p2) = (p1, open (patternCtx initialCtx) (nthPatFind p1) p2)  -- | Embeds a term in an 'Embed', or an 'Embed' under some number of 'Unbound.Generics.LocallyNameless.Shift.Shift' constructors. embed :: IsEmbed e => Embedded e -> e

@@ -14,7 +14,7 @@  import Control.Applicative ((<*>), (<$>)) import Control.DeepSeq (NFData(..))-import Data.Monoid ((<>))+import Data.Monoid ((<>), All(..)) import GHC.Generics  import Unbound.Generics.LocallyNameless.Alpha@@ -52,7 +52,7 @@                            . showsPrec 0 p2)  instance (Alpha p1, Alpha p2) => Alpha (Rebind p1 p2) where-  isTerm _ = False+  isTerm _ = All False    isPat (Rebnd p1 p2) = isPat p1 <> isPat p2 

@@ -22,6 +22,8 @@ import Control.DeepSeq (NFData(..)) import GHC.Generics (Generic) +import Data.Monoid(All(..))+ import Unbound.Generics.LocallyNameless.Alpha import Unbound.Generics.LocallyNameless.Bind @@ -54,11 +56,11 @@   instance Alpha p => Alpha (Rec p) where-  isTerm _ = False+  isTerm _ = All False   isPat (Rec p) = isPat p -  nthPatFind (Rec p) i = nthPatFind p i-  namePatFind (Rec p) x = namePatFind p x+  nthPatFind (Rec p) = nthPatFind p+  namePatFind (Rec p) = namePatFind p    open ctx b (Rec p) = Rec (open (incrLevelCtx ctx) b p)   close ctx b (Rec p) = Rec (close (incrLevelCtx ctx) b p)@@ -67,8 +69,8 @@  -- | Constructor for recursive patterns. rec :: Alpha p => p -> Rec p-rec p = Rec (close (patternCtx initialCtx) p p)+rec p = Rec (close (patternCtx initialCtx) (namePatFind p) p)  -- | Destructor for recursive patterns. unrec :: Alpha p => Rec p -> p-unrec (Rec p) = open (patternCtx initialCtx) p p+unrec r@(Rec p) = open (patternCtx initialCtx) (nthPatFind r) p

@@ -13,7 +13,7 @@  import Control.Applicative import Control.DeepSeq (NFData(..))-import Data.Monoid (Monoid(..))+import Data.Monoid (Monoid(..), All(..))  import Unbound.Generics.LocallyNameless.Alpha (Alpha(..),                                                decrLevelCtx, isTermCtx,@@ -43,7 +43,7 @@ instance Alpha e => Alpha (Shift e) where   isPat (Shift e) = if (isEmbed e) then mempty else inconsistentDisjointSet -  isTerm _ = False+  isTerm _ = All False    isEmbed (Shift e) = isEmbed e @@ -88,8 +88,8 @@          then se          else Shift (open (decrLevelCtx ctx) b e) -  nthPatFind (Shift e) i = nthPatFind e i-  namePatFind (Shift e) x = namePatFind e x+  nthPatFind (Shift e) = nthPatFind e+  namePatFind (Shift e) = namePatFind e     acompare' ctx (Shift x) (Shift y) = acompare' ctx x y

@@ -36,9 +36,9 @@ -- --   close _ _ = id -- --   open _ _ = id -- --   isPat _ = mempty--- --   isTerm _ = True--- --   nthPatFind _ = Left--- --   namePatFind _ _ = Left 0+-- --   isTerm _ = mempty+-- --   nthPatFind _ = mempty+-- --   namePatFind _ _ = mempty -- --   swaps' _ _ = id -- --   freshen' _ i = return (i, mempty) -- --   lfreshen' _ i cont = cont i mempty@@ -56,9 +56,9 @@              , valueD 'close               [e| \_ctx _b     -> id                 |]              , valueD 'open                [e| \_ctx _b     -> id                 |]              , valueD 'isPat               [e| \_           -> mempty             |]-             , valueD 'isTerm              [e| \_           -> True               |]-             , valueD 'nthPatFind          [e| \_           -> Left               |]-             , valueD 'namePatFind         [e| \_ _         -> Left 0             |]+             , valueD 'isTerm              [e| \_           -> mempty             |]+             , valueD 'nthPatFind          [e| \_           -> mempty             |]+             , valueD 'namePatFind         [e| \_           -> mempty             |]              , valueD (mkName "swaps'")    [e| \_ctx _p     -> id                 |]              , valueD (mkName "freshen'")  [e| \_ctx i      -> return (i, mempty) |]              , valueD (mkName "lfreshen'") [e| \_ctx i cont -> cont i mempty      |]

@@ -20,5 +20,5 @@ -- | A destructor for binders that does /not/ guarantee fresh --   names for the binders. unsafeUnbind :: (Alpha p, Alpha t) => Bind p t -> (p, t)-unsafeUnbind (B p t) = (p, open initialCtx p t)+unsafeUnbind (B p t) = (p, open initialCtx (nthPatFind p) t)        

@@ -112,10 +112,10 @@ ex2y = V (mkVar "y")  ex2xc :: Expr-ex2xc = close initialCtx (mkVar "x") ex2x+ex2xc = close initialCtx (namePatFind (mkVar "x")) ex2x  ex2yc :: Expr-ex2yc = close initialCtx (mkVar "y") ex2y+ex2yc = close initialCtx (namePatFind (mkVar "y")) ex2y  ex3x :: Expr ex3x = let x = mkVar "x"

@@ -92,13 +92,13 @@ -- if a name is already free opening it has no effect prop_open_idempotent :: T Int -> Property prop_open_idempotent t =-  forAll (arbVarsOf t) $ \v -> open initialCtx v t =~= t+  forAll (arbVarsOf t) $ \v -> open initialCtx (nthPatFind v) t =~= t  -- if you close over a variable, then it is no longer free. prop_close_binds :: T Int -> Property prop_close_binds t =   (not $ null $ toListOf fvAny t) ==>-  forAll (arbVarsOf t) $ \v -> v /~@ close initialCtx v t+  forAll (arbVarsOf t) $ \v -> v /~@ close initialCtx (namePatFind v) t  ---------------------------------------- -- Test group

@@ -10,6 +10,8 @@ {-# LANGUAGE TemplateHaskell #-} module TestTH (test_TH) where +import Data.Monoid(Monoid(..))+ import Test.Tasty import Test.Tasty.HUnit import AlphaAssertions@@ -40,9 +42,9 @@           [ testCase "TH aeq" $ assertAeq kt kt           , testCase "TH acompare" $ assertAcompare kt kF (compare kt kF)           , testCase "TH fvAny kG" $ assertEqual "" (toListOf fvAny kG) []-          , testCase "TH close" $ assertEqual "" (close initialCtx emptyPat kt) kt-          , testCase "TH open" $ assertEqual "" (open initialCtx emptyPat kG) kG-          , testCase "TH isTerm" $ assertEqual "" (isTerm kF) True+          , testCase "TH close" $ assertEqual "" (close initialCtx (namePatFind emptyPat) kt) kt+          , testCase "TH open" $ assertEqual "" (open initialCtx (nthPatFind emptyPat) kG) kG+          , testCase "TH isTerm" $ assertEqual "" (isTerm kF) mempty           , testCase "TH isPat"             $ assertBool "isNullDisjointSEt (isPat kF)" (isNullDisjointSet $ isPat kF)           ]

@@ -48,9 +48,9 @@   close _ctx _b x = x   open _ctx _b x = x   isPat _ = mempty-  isTerm _ = True-  nthPatFind _ = Left-  namePatFind _ _ = Left 0+  isTerm _ = mempty+  nthPatFind _ = mempty+  namePatFind _ = mempty    swaps' _ctx _p x = x   freshen' _ctx x = return (x, mempty)

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                unbound-generics-version:             0.2+version:             0.3 synopsis:            Support for programming with names and binders using GHC Generics description:         Specify the binding structure of your data type with an                      expressive set of type combinators, and unbound-generics@@ -29,7 +29,8 @@                      README.md,                      Changelog.md cabal-version:       >=1.10-+tested-with: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.3+              library   exposed-modules:     Unbound.Generics.LocallyNameless                        Unbound.Generics.LocallyNameless.Name@@ -104,3 +105,4 @@ source-repository head   type:                git   location:            git://github.com/lambdageek/unbound-generics.git+