unbound-generics 0.1 → 0.1.2

raw patch · 20 files changed

+437/−22 lines, 20 filesdep +profunctorsdep +template-haskell

Dependencies added: profunctors, template-haskell

Files

• Changelog.md +15/−0
• README.md +6/−0
• src/Unbound/Generics/LocallyNameless.hs +11/−1
• src/Unbound/Generics/LocallyNameless/Alpha.hs +16/−0
• src/Unbound/Generics/LocallyNameless/Embed.hs +17/−1
• src/Unbound/Generics/LocallyNameless/Internal/Iso.hs +28/−0
• src/Unbound/Generics/LocallyNameless/Internal/Lens.hs +11/−0
• src/Unbound/Generics/LocallyNameless/Operations.hs +10/−6
• src/Unbound/Generics/LocallyNameless/Rec.hs +4/−1
• src/Unbound/Generics/LocallyNameless/Shift.hs +93/−0
• src/Unbound/Generics/LocallyNameless/Subst.hs +5/−0
• src/Unbound/Generics/LocallyNameless/TH.hs +68/−0
• test/AlphaAssertions.hs +13/−0
• test/Calc.hs +1/−0
• test/TestACompare.hs +2/−5
• test/TestCalc.hs +2/−3
• test/TestShiftEmbed.hs +69/−0
• test/TestTH.hs +48/−0
• test/test-main.hs +4/−0
• unbound-generics.cabal +14/−5

@@ -1,3 +1,18 @@+# 0.1.2++* Added `IsEmbed` typeclass++    * Depend on 'profunctors'++* Changed `embed` and `unembed` to work over any `IsEmbed` type.++* Added `Shift` type for shifting the scope of embedded terms out one level.++# 0.1.1++* Added `isNullDisjointSet` function.+* Implement a TH `makeClosedAlpha` splice for constructing trivial leaf instances.+ # 0.1  * Add `acompare` functiona and `acompare'` method to `Alpha` typeclass.  (christiaanb)

@@ -18,3 +18,9 @@     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.++3. `embed :: IsEmbed e => Embedded e -> e` and `unembed :: IsEmbed e => e -> Embedded e`++    The typeclass `IsEmbed` has an `Iso` (again in the sense of the `lens` library) as a method instead of the above pair of methods.++    Again, you should only notice this if you're implementing your own types that are instances of `IsEmbed`.  The easiest thing to do is to use implement `embedded = iso yourEmbed yourUnembed` where `iso` comes from `lens`.  (Although you can also implement it in terms of `dimap` if you don't want to depend on lens)

@@ -6,13 +6,22 @@ -- Stability  : experimental -- ----- See 'Alpha', 'Bind', "Unbound.Generics.LocallyNameless.Operations" to get started. +-- The purpose of @unbound-genrics@ is to simplify the construction of+-- data structures with rich variable binding structure by providing+-- generic implementations of alpha-equivalence ('aeq'), free variable+-- permutation ('swaps'), local and glocal variable freshness+-- ('lfresh', 'fresh'), +--+--+-- +-- See 'Alpha', 'Bind', "Unbound.Generics.LocallyNameless.Operations" for more information. module Unbound.Generics.LocallyNameless (   module Unbound.Generics.LocallyNameless.Alpha,   module Unbound.Generics.LocallyNameless.Name,   module Unbound.Generics.LocallyNameless.Operations,   module Unbound.Generics.LocallyNameless.Bind,   module Unbound.Generics.LocallyNameless.Embed,+  module Unbound.Generics.LocallyNameless.Shift,   module Unbound.Generics.LocallyNameless.Rebind,   module Unbound.Generics.LocallyNameless.Rec,   module Unbound.Generics.LocallyNameless.Fresh,@@ -24,6 +33,7 @@ import Unbound.Generics.LocallyNameless.Name hiding (Bn, Fn) import Unbound.Generics.LocallyNameless.Bind hiding (B) import Unbound.Generics.LocallyNameless.Embed+import Unbound.Generics.LocallyNameless.Shift import Unbound.Generics.LocallyNameless.Rebind hiding (Rebnd) import Unbound.Generics.LocallyNameless.Rec import Unbound.Generics.LocallyNameless.Fresh

@@ -18,6 +18,7 @@   , inconsistentDisjointSet   , singletonDisjointSet   , isConsistentDisjointSet+  , isNullDisjointSet   -- * Implementation details   , NthPatFind   , NamePatFind@@ -27,6 +28,8 @@   , termCtx   , isTermCtx   , incrLevelCtx+  , decrLevelCtx+  , isZeroLevelCtx   -- * Internal   , gaeq   , gfvAny@@ -91,6 +94,14 @@ incrLevelCtx :: AlphaCtx -> AlphaCtx incrLevelCtx ctx = ctx { ctxLevel = 1 + ctxLevel ctx } +-- | Decrement the number of binders that we are operating under.+decrLevelCtx :: AlphaCtx -> AlphaCtx+decrLevelCtx ctx = ctx { ctxLevel = ctxLevel ctx - 1 }++-- | Are we operating under no binders?+isZeroLevelCtx :: AlphaCtx -> Bool+isZeroLevelCtx ctx = ctxLevel ctx == 0+ -- | A @DisjointSet a@ is a 'Just' a list of distinct @a@s.  In addition to a monoidal -- structure, a disjoint set also has an annihilator 'inconsistentDisjointSet'. --@@ -125,6 +136,11 @@ isConsistentDisjointSet :: DisjointSet a -> Bool isConsistentDisjointSet (DisjointSet Nothing) = False isConsistentDisjointSet _ = True++-- | @isNullDisjointSet@ return @True@ iff the given disjoint set is 'mempty'.+isNullDisjointSet :: DisjointSet a -> Bool+isNullDisjointSet (DisjointSet (Just [])) = True+isNullDisjointSet _ = False  -- | Types that are instances of @Alpha@ may participate in name representation. --

@@ -7,14 +7,17 @@ -- Stability  : experimental -- -- The pattern @'Embed' t@ contains a term @t@.-{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveGeneric, TypeFamilies #-} module Unbound.Generics.LocallyNameless.Embed where  import Control.Applicative (pure, (<$>)) import Data.Monoid (mempty)+import Data.Profunctor (Profunctor(..))+ import GHC.Generics (Generic)  import Unbound.Generics.LocallyNameless.Alpha+import Unbound.Generics.LocallyNameless.Internal.Iso (iso)  -- | @Embed@ allows for terms to be /embedded/ within patterns.  Such --   embedded terms do not bind names along with the rest of the@@ -30,6 +33,19 @@ --   'Shift's at the same time.) newtype Embed t = Embed t deriving (Eq, Generic) +class IsEmbed e where+  type Embedded e :: *+  -- | Insert or extract the embedded term.+  -- If you're not using the lens library, see 'Unbound.Generics.LocallyNameless.Operations.embed'+  -- and 'Unbound.Generics.LocallyNameless.Operations.unembed'+  -- otherwise 'embedded' is an isomorphism that you can use with lens.+  -- @embedded :: Iso' (Embedded e) e@+  embedded :: (Profunctor p, Functor f) => p (Embedded e) (f (Embedded e)) -> p e (f e)++instance IsEmbed (Embed t) where+  type Embedded (Embed t) = t+  embedded = iso (\(Embed t) -> t) Embed+   instance Show a => Show (Embed a) where   showsPrec _ (Embed a) = showString "{" . showsPrec 0 a . showString "}" 

@@ -0,0 +1,28 @@+{-# LANGUAGE RankNTypes #-}+module Unbound.Generics.LocallyNameless.Internal.Iso where++import Data.Profunctor (Profunctor(..))+import Data.Functor.Identity (Identity(..))++data Exchange a b s t = Exchange (s -> a) (b -> t)++instance Profunctor (Exchange a b) where+  dimap f g (Exchange h k) = Exchange (h . f ) (g . k)++type Iso s t a b = forall p f . (Profunctor p, Functor f) => p a (f b) -> p s (f t)++type AnIso s t a b = Exchange a b a (Identity b) -> Exchange a b s (Identity t)++iso :: (s -> a) -> (b -> t) -> Iso s t a b+iso sa bt = dimap sa (fmap bt)+{-# INLINE iso #-}++from :: AnIso s t a b -> Iso b a t s+from l = withIso l $  \ sa bt -> iso bt sa+{-# INLINE from #-}++withIso :: AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r+withIso ai k =+  case ai (Exchange id Identity) of+   Exchange sa bt -> k sa (runIdentity . bt)+{-# INLINE withIso #-}

@@ -0,0 +1,11 @@+module Unbound.Generics.LocallyNameless.Internal.Lens where++import Control.Monad.Reader (MonadReader(..))+import qualified Control.Monad.Reader as Reader+import Control.Applicative (Const(..))++type Getting r s a = (a -> Const r a) -> s -> Const r s++view :: MonadReader s m => Getting a s a -> m a+view l = Reader.asks (getConst . l Const)+{-# INLINE view #-}

@@ -29,6 +29,7 @@        , rebind        , unrebind        , Embed(..)+       , IsEmbed(..)        , embed        , unembed          -- * Recursive bindings@@ -51,10 +52,12 @@ import Unbound.Generics.LocallyNameless.LFresh import Unbound.Generics.LocallyNameless.Name import Unbound.Generics.LocallyNameless.Bind-import Unbound.Generics.LocallyNameless.Embed (Embed(..))+import Unbound.Generics.LocallyNameless.Embed (Embed(..), IsEmbed(..)) import Unbound.Generics.LocallyNameless.Rebind import Unbound.Generics.LocallyNameless.Rec import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf, justFiltered)+import Unbound.Generics.LocallyNameless.Internal.Lens (view)+import Unbound.Generics.LocallyNameless.Internal.Iso (from) import Unbound.Generics.PermM  -- | @'aeq' t1 t2@ returns @True@ iff @t1@ and @t2@ are alpha-equivalent terms.@@ -184,13 +187,14 @@ unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2) unrebind (Rebnd p1 p2) = (p1, open (patternCtx initialCtx) p1 p2) --- | An alias for 'Embed'-embed :: t -> Embed t-embed = Embed+-- | Embeds a term in an 'Embed', or an 'Embed' under some number of 'Shift's+embed :: IsEmbed e => Embedded e -> e+embed = view (from embedded)  -- | @'unembed' p@ extracts the term embedded in the pattern @p@.-unembed :: Embed t -> t-unembed (Embed t) = t+-- unembed :: Embed t -> t+unembed :: IsEmbed e => e -> Embedded e+unembed = view embedded  -- | Constructor for recursive abstractions. trec :: Alpha p => p -> TRec p

@@ -7,7 +7,7 @@ -- Stability  : experimental -- -- The pattern @'Rec' p@ binds the names in @p@ like @p@ itself would,--- but additinoally, the names in @p@ are scope over @p@.+-- but additionally, the names in @p@ are scope over @p@. -- -- The term @'TRec' p@ is shorthand for @'Bind' (Rec p) ()@ {-# LANGUAGE DeriveGeneric #-}@@ -52,6 +52,9 @@ instance Alpha p => Alpha (Rec p) where   isTerm _ = False   isPat (Rec p) = isPat p++  nthPatFind (Rec p) i = nthPatFind p i+  namePatFind (Rec p) x = namePatFind p x    open ctx b (Rec p) = Rec (open (incrLevelCtx ctx) b p)   close ctx b (Rec p) = Rec (close (incrLevelCtx ctx) b p)

@@ -0,0 +1,93 @@+{-# OPTIONS_HADDOCK show-extensions #-}+-- |+-- Module     : Unbound.Generics.LocallyNameless.Shift+-- Copyright  : (c) 2015, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- The pattern @'Shift' e@ shifts the scope of the embedded term in @e@ one level outwards.+--+{-# LANGUAGE TypeFamilies #-}+module Unbound.Generics.LocallyNameless.Shift where++import Control.Applicative+import Data.Monoid (Monoid(..))++import Unbound.Generics.LocallyNameless.Alpha (Alpha(..),+                                               decrLevelCtx, isTermCtx,+                                               isZeroLevelCtx,+                                               inconsistentDisjointSet)+import Unbound.Generics.LocallyNameless.Embed (IsEmbed(..))++import Unbound.Generics.LocallyNameless.Internal.Iso (iso)++-- | The type @Shift e@ is an embedding pattern that shifts the scope of the+-- free variables of the embedded term @'Embedded' e@ up by one level.+newtype Shift e = Shift e++instance Functor Shift where+  fmap f (Shift e) = Shift (f e)++instance IsEmbed e => IsEmbed (Shift e) where+  type Embedded (Shift e) = Embedded e+  embedded = iso (\(Shift e) -> e) Shift . embedded+  +instance Show e => Show (Shift e) where+  showsPrec _ (Shift e) = showString "{" . showsPrec 0 e . showString "}"++instance Alpha e => Alpha (Shift e) where+  isPat (Shift e) = if (isEmbed e) then mempty else inconsistentDisjointSet++  isTerm _ = False++  isEmbed (Shift e) = isEmbed e++  swaps' ctx perm (Shift e) = Shift (swaps' (decrLevelCtx ctx) perm e)++  freshen' ctx p =+    if isTermCtx ctx+    then error "LocallyNameless.freshen' called on a term"+    else return (p, mempty)++  lfreshen' ctx p kont =+    if isTermCtx ctx+    then error "LocallyNameless.lfreshen' called on a term"+    else kont p mempty++  aeq' ctx (Shift e1) (Shift e2) = aeq' ctx e1 e2++  fvAny' ctx afa (Shift e) = Shift <$> fvAny' ctx afa e++  close ctx b se@(Shift e) =+    if isTermCtx ctx+    then error "LocallyNameless.close on Shift"+    else if isZeroLevelCtx ctx+         then+           -- consider type A = Rec (Name t, Shift (Embed e), (Embed e))+           --  (ie the 2nd element of the tuple is not allowed to refer to itself,+           --   but the third is)+           -- if we have (x, e1, e2) and we apply 'rec' to it,+           -- we must close the tuple with respect to itself.+           -- in that case, the ctxLevel is 0 and so none of the names in+           -- e1 need be bound.+           -- on the other hand once we go to+           --   Bind P (Bind A B) for some P and B,+           -- the free vars of e1 in A are bound by P.+           se+         else Shift (close (decrLevelCtx ctx) b e)++  open ctx b se@(Shift e) =+    if isTermCtx ctx+    then error "LocallyNameless.open on Shift"+    else if isZeroLevelCtx ctx+         then se+         else Shift (open (decrLevelCtx ctx) b e)++  nthPatFind (Shift e) i = nthPatFind e i+  namePatFind (Shift e) x = namePatFind e x+++  acompare' ctx (Shift x) (Shift y) = acompare' ctx x y++  

@@ -55,6 +55,7 @@ import Unbound.Generics.LocallyNameless.Name import Unbound.Generics.LocallyNameless.Alpha import Unbound.Generics.LocallyNameless.Embed+import Unbound.Generics.LocallyNameless.Shift import Unbound.Generics.LocallyNameless.Bind import Unbound.Generics.LocallyNameless.Rebind import Unbound.Generics.LocallyNameless.Rec@@ -172,6 +173,10 @@ instance Subst b AnyName where subst _ _ = id ; substs _ = id  instance (Subst c a) => Subst c (Embed a)++instance (Subst c e) => Subst c (Shift e) where+  subst x b (Shift e) = Shift (subst x b e)+  substs ss (Shift e) = Shift (substs ss e)  instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) 

@@ -0,0 +1,68 @@+{-# OPTIONS_HADDOCK show-extensions #-}+-- |+-- Module     : Unbound.Generics.LocallyNameless.TH+-- Copyright  : (c) 2015, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- Template Haskell methods to construct instances of 'Alpha' for+-- datatypes that don't contain any names and don't participate in+-- 'Alpha' operations in any non-trivial way.+{-# LANGUAGE TemplateHaskell #-}+module Unbound.Generics.LocallyNameless.TH (makeClosedAlpha) where+import Language.Haskell.TH++import Control.Applicative (Applicative(..))+import Data.Monoid (Monoid(..))+import Unbound.Generics.LocallyNameless.Alpha (Alpha(..))++-- | Make a trivial @instance 'Alpha' T@ for a type @T@ that does not+-- contains no bound nor free values of type @'Name' a@ or @'AnyName'@+-- (or any in general any values that are themselves non-trivial+-- instances of 'Alpha').  Use this to write 'Alpha' instances for+-- types that you don't want to traverse via their @GHC.Generics.Rep@+-- representation just to find out that there aren't any names.+--+-- @@@+-- data T = T Int deriving (Eq, Ord, Show)+-- $(makeClosedAlpha T)+-- -- constructs+-- -- instance Alpha T where+-- --   aeq' _ = (==)+-- --   acompare' _ = compare+-- --   fvAny' _ _ = pure+-- --   close _ _ = id+-- --   open _ _ = id+-- --   isPat _ = mempty+-- --   isTerm _ = True+-- --   nthPatFind _ = Left+-- --   namePatFind _ _ = Left 0+-- --   swaps' _ _ = id+-- --   freshen' _ i = return (i, mempty)+-- --   lfreshen' _ i cont = cont i mempty+-- @@@+--+makeClosedAlpha :: Name -> DecsQ+makeClosedAlpha tyName = do+  +  let valueD vName e = valD (varP vName) (normalB e) []+      -- methods :: [Q Dec]+      methods =+             [+               valueD (mkName "aeq'")      [e| \_ctx        -> (==)               |]+             , valueD (mkName "fvAny'")    [e| \_ctx _nfn   -> pure               |]+             , 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 (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      |]+             , valueD (mkName "acompare'") [e| \_ctx        -> compare            |]+             ]+  d <- instanceD (cxt []) (appT [t|Alpha|] (conT tyName)) methods+  return [d]+

@@ -0,0 +1,13 @@+module AlphaAssertions where++import Test.Tasty.HUnit++import Unbound.Generics.LocallyNameless++assertAeq :: (Alpha t, Show t) => t -> t -> Assertion+assertAeq x y = assertBool (show x ++ " not alpha equivalent to " ++ show y) (x `aeq` y)++assertAcompare :: (Alpha t, Show t) => t -> t -> Ordering -> Assertion+assertAcompare x y o =+  let o' = acompare x y+  in  assertBool (show x ++ " not alpha-" ++ show o' ++ " to " ++ show y ++ ", but alpha-" ++ show o) (o' == o)

@@ -14,6 +14,7 @@  import Unbound.Generics.LocallyNameless import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf)+import Unbound.Generics.LocallyNameless.TH  -- variables will range over expressions type Var = Name Expr

@@ -8,6 +8,8 @@ import Test.Tasty import Test.Tasty.HUnit +import AlphaAssertions+ data Expr   = V (Name Expr)   | Add Expr Expr@@ -15,11 +17,6 @@   deriving (Show,Generic,Typeable)  instance Alpha Expr--assertAcompare :: (Alpha t, Show t) => t -> t -> Ordering -> Assertion-assertAcompare x y o =-  let o' = acompare x y-  in  assertBool (show x ++ " not alpha-" ++ show o' ++ " to " ++ show y ++ ", but alpha-" ++ show o) (o' == o)  nameA, nameB, nameC :: Name Expr nameA = s2n "a"

@@ -14,9 +14,8 @@  import Test.Tasty import Test.Tasty.HUnit--assertAeq :: (Alpha t, Show t) => t -> t -> Assertion-assertAeq x y = assertBool (show x ++ " not alpha equivalent to " ++ show y) (x `aeq` y)+  +import AlphaAssertions  test_ex1 :: TestTree test_ex1 = testCase "example 1" $ assertAeq (runWhnf emptyEnv ex1) (Just $ C 3)

@@ -0,0 +1,69 @@+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}+module TestShiftEmbed (test_shiftEmbed) where++import Prelude hiding (pi)++import Data.Typeable (Typeable)+import GHC.Generics (Generic)+import Unbound.Generics.LocallyNameless+import qualified Unbound.Generics.PermM as PermM++import AlphaAssertions++import Test.Tasty+import Test.Tasty.HUnit++type Var = Name Term++data Term+  = V Var+  | Pi (Bind (Var, Embed Term) Term)+  | LetRec (Bind (Rec Decl) Term)+    deriving (Show, Generic, Typeable)++data Decl =+  -- a recursive declaration  x : A = m+  -- where x may occur in m but not in A+  Decl {+    declVar :: Var+    , declClass :: Shift (Embed Term)+    , declVal :: Embed Term+    }+  deriving (Show, Generic, Typeable)++instance Alpha Term+instance Alpha Decl++x, y, z :: Var+x = s2n "x"+y = s2n "y"+z = s2n "z"++pi :: Var -> Term -> Term -> Term+pi v a b = Pi $ bind (v, embed a) b++letrec :: Decl -> Term -> Term+letrec d e = LetRec $ bind (rec d) e++decl :: Var -> Term -> Term -> Decl+decl v klass e = Decl v (embed klass) (embed e)+++test_shiftEmbed =+  testGroup "Embedded and Shifted terms"+  [+    testGroup "Embed"+    [+      testCase "(pi x:x . x) = (pi y:x . y)" $ let m1 = pi x (V x) (V x)+                                                   m2 = pi y (V x) (V y)+                                               in assertAeq m1 m2+    , testCase "(letrec x : x = x in x) = (letrec y : x = y in y)"+      $ let m1 = letrec (decl x (V x) (V x)) (V x)+            m2 = letrec (decl y (V x) (V y)) (V y)+        in assertAeq m1 m2+    , testCase "pi x : z . (letrec x : x = x in x) = pi y : z . (letrec x : y = x in x)"+      $ let m1 = pi x (V z) $ letrec (decl x (V x) (V x)) (V x)+            m2 = pi y (V z) $ letrec (decl x (V y) (V x)) (V x)+        in assertAeq m1 m2+    ]+  ]

@@ -0,0 +1,48 @@+{-# OPTIONS_HADDOCK show-extensions #-}+-- |+-- Module     : TestTH+-- Copyright  : (c) 2015, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- Test of 'makeClosedAlpha' splice.+{-# LANGUAGE TemplateHaskell #-}+module TestTH (test_TH) where++import Test.Tasty+import Test.Tasty.HUnit+import AlphaAssertions++import Unbound.Generics.LocallyNameless+import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf)+import Unbound.Generics.LocallyNameless.TH++++data K =+  KT+  | KArr K K+    deriving (Eq, Ord, Show)++$(makeClosedAlpha ''K)++kt, kF, kG :: K+kt = KT+kF = KT `KArr` KT+kG = kF `KArr` KT++emptyPat :: [Name ()]+emptyPat = []++test_TH :: TestTree+test_TH = testGroup "TH makeClosedAlpha splice"+          [ 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 isPat"+            $ assertBool "isNullDisjointSEt (isPat kF)" (isNullDisjointSet $ isPat kF)+          ]

@@ -7,6 +7,8 @@ import PropOpenClose import TinyLam import TestACompare+import TestShiftEmbed+import TestTH  main :: IO () main = defaultMain $ testGroup "unboundGenerics"@@ -16,4 +18,6 @@        , test_openClose        , test_tinyLam        , test_acompare+       , test_shiftEmbed+       , test_TH        ]

@@ -2,8 +2,8 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                unbound-generics-version:             0.1-synopsis:            Reimplementation of Unbound using GHC Generics+version:             0.1.2+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                      handles the rest!  Automatically derives@@ -22,7 +22,7 @@ license-file:        LICENSE author:              Aleksey Kliger maintainer:          aleksey@lambdageek.org-copyright:           (c) 2014, Aleksey Kliger+copyright:           (c) 2014-2015, Aleksey Kliger category:            Language build-type:          Simple extra-source-files:  examples/*.hs,@@ -39,20 +39,26 @@                        Unbound.Generics.LocallyNameless.Bind                        Unbound.Generics.LocallyNameless.Rebind                        Unbound.Generics.LocallyNameless.Embed+                       Unbound.Generics.LocallyNameless.Shift                        Unbound.Generics.LocallyNameless.Operations                        Unbound.Generics.LocallyNameless.Unsafe                        Unbound.Generics.LocallyNameless.Internal.Fold+                       Unbound.Generics.LocallyNameless.Internal.Iso+                       Unbound.Generics.LocallyNameless.Internal.Lens                        Unbound.Generics.LocallyNameless.Rec+                       Unbound.Generics.LocallyNameless.TH                        Unbound.Generics.PermM                        Unbound.Generics.LocallyNameless.Subst   -- other-modules:          -- other-extensions:       build-depends:       base >=4.6 && <5,+                       template-haskell >= 2.8.0.0,                        mtl >= 2.1,                        transformers >= 0.3,                        transformers-compat >= 0.3,                        containers == 0.5.*,-                       contravariant >= 0.5+                       contravariant >= 0.5,+                       profunctors >= 4.0   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall@@ -60,13 +66,16 @@ Test-Suite test-unbound-generics   type:                exitcode-stdio-1.0   main-is:             test-main.hs-  other-modules:       Calc+  other-modules:       AlphaAssertions+                       Calc                        TestCalc                        ParallelReduction                        TestParallelReduction                        PropOpenClose                        TinyLam                        TestACompare+                       TestShiftEmbed+                       TestTH   build-depends:       base,                        mtl,                        tasty,