packages feed

unbound-generics (empty) → 0.0.0.90

raw patch · 23 files changed

+2551/−0 lines, 23 filesdep +HUnitdep +basedep +containerssetup-changed

Dependencies added: HUnit, base, containers, contravariant, mtl, transformers, unbound-generics

Files

+ Changelog.md view
@@ -0,0 +1,2 @@+* 0.0.0.90+  Initial (re-)implementation effort.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2014, Aleksey Kliger++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Aleksey Kliger nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,20 @@+# unbound-generics++[![Build Status](https://travis-ci.org/lambdageek/unbound-generics.svg)](https://travis-ci.org/lambdageek/unbound-generics)+++This is a reimplementation of (parts of) [unbound](http://hackage.haskell.org/package/unbound) but using [GHC generics](http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.7.0.1/GHC-Generics.html) instead of [RepLib](https://hackage.haskell.org/package/RepLib).++## Differences from `unbound`++For the most part, I tried to keep the same methods with the same signatures.  However there are a few differences.++1. `fv :: Alpha t => t -> Fold t (Name n)`++   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`++   You should olnly 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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ examples/F.hs view
@@ -0,0 +1,170 @@+{-# LANGUAGE DeriveGeneric,+             DeriveDataTypeable,+             FlexibleInstances,+             FlexibleContexts,+             MultiParamTypeClasses,+             ScopedTypeVariables+  #-}++module F where++import Unbound.Generics.LocallyNameless++import GHC.Generics+import Data.Typeable (Typeable)++import Control.Monad.Identity+import Control.Monad.Writer hiding (All)+import Control.Monad.Trans.Error+import Data.List as List+++-- System F with type and term variables++type TyName = Name Ty+type TmName = Name Tm++data Ty = TyVar TyName+        | Arr Ty Ty+        | All (Bind TyName Ty)+   deriving (Show, Generic, Typeable)++data Tm = TmVar TmName+        | Lam (Bind (TmName, Embed Ty) Tm)+        | TLam (Bind TyName Tm)+        | App Tm Tm+        | TApp Tm Ty+   deriving (Show, Generic, Typeable)++------------------------------------------------------+instance Alpha Ty+instance Alpha Tm++instance Subst Tm Ty+instance Subst Tm Tm where+  isvar (TmVar v) = Just (SubstName v)+  isvar _  = Nothing++instance Subst Ty Ty where+  isvar (TyVar v) = Just (SubstName v)+  isvar _ = Nothing++------------------------------------------------------+-- Example terms+------------------------------------------------------++x :: Name Tm+y :: Name Tm+z :: Name Tm+(x,y,z) = (string2Name "x", string2Name "y", string2Name "z")++a :: Name Ty+b :: Name Ty+c :: Name Ty+(a,b,c) = (string2Name "a", string2Name "b", string2Name "c")++-- /\a. \x:a. x+polyid :: Tm+polyid = TLam (bind a (Lam (bind (x, Embed (TyVar a)) (TmVar x))))++-- All a. a -> a+polyidty :: Ty+polyidty = All (bind a (Arr (TyVar a) (TyVar a)))++-- /\b. \y:b. y+polyid2 :: Tm+polyid2 = TLam (bind b (Lam (bind (y, Embed (TyVar b)) (TmVar y))))++-- /\c. \y:b. y+bad_polyid2 :: Tm+bad_polyid2 = TLam (bind c (Lam (bind (y, Embed (TyVar b)) (TmVar y))))+++-----------------------------------------------------------------+-- Typechecker+-----------------------------------------------------------------+type Delta = [ TyName ]+type Gamma = [ (TmName, Ty) ]++data Ctx = Ctx { getDelta :: Delta , getGamma :: Gamma }+           deriving (Show)+                    +emptyCtx :: Ctx+emptyCtx = Ctx { getDelta = [], getGamma = [] }++type M = ErrorT String (WriterT [String] (FreshMT Identity))++runM :: M a -> (a, [String])+runM m = case (runIdentity $ runFreshMT $ runWriterT (runErrorT m)) of+   (Left s, msgs)  -> error $ s ++ "\nLog: " ++ show msgs+   (Right ans, msgs) -> (ans, msgs)++checkTyVar :: Ctx -> TyName -> M ()+checkTyVar g v = do+    if List.elem v (getDelta g) then+      return ()+    else+      throwError $ "NotFound: " ++ show v ++ " in " ++ show g++lookupTmVar :: Ctx -> TmName -> M Ty+lookupTmVar g v = do+    case lookup v (getGamma g) of+      Just s -> return s+      Nothing -> throwError "NotFound"++extendTy :: TyName -> Ctx -> Ctx+extendTy n ctx = ctx { getDelta =  n : (getDelta ctx) }++extendTm :: TmName -> Ty -> Ctx -> Ctx+extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) }++tcty :: Ctx -> Ty -> M ()+tcty g  (TyVar alpha) = do+   trace $ "looking up tyvar " ++ show alpha+   checkTyVar g alpha+tcty g  (All bnder) = do+   trace $ "checking " ++ show (All bnder)+   (alpha, ty') <- unbind bnder+   trace $ "unbinding All gave " ++ show alpha ++ " in " ++ show ty'+   tcty (extendTy alpha g) ty'+tcty g  (Arr t1 t2) = do+   trace $ "checking " ++ show (Arr t1 t2)+   tcty g  t1+   tcty g  t2++trace :: String -> M ()+trace s = lift (tell [s])++ti :: Ctx -> Tm -> M Ty+ti g (TmVar v) = trace ("looking up " ++ show v) >> lookupTmVar g v+ti g (Lam bnd) = do+  trace $ "checking " ++ show (Lam bnd)+  ((v, Embed ty1), t) <- unbind bnd+  tcty g ty1+  ty2 <- ti (extendTm v ty1 g) t+  return (Arr ty1 ty2)+ti g (App t1 t2) = do+  trace $ "checking " ++ show (App t1 t2)+  ty1 <- ti g t1+  ty2 <- ti g t2+  case ty1 of+    Arr ty11 ty21 | ty2 `aeq` ty11 ->+      return ty21+    _ -> throwError "TypeError"+ti g (TLam bnd) = do+  trace $ "checking " ++ show (TLam bnd)+  (v, t) <- unbind bnd+  trace $ "unbinding TLam gave " ++ show v ++ " in " ++ show t+  ty <- ti (extendTy v g) t+  return (All (bind v ty))+ti g (TApp t ty) = do+  trace $ "checking " ++ show (TApp t ty)+  tyt <- ti g t+  case tyt of+   (All bnder) -> do+      tcty g  ty+      (n1, ty1) <- unbind bnder+      return $ subst n1 ty ty1+   _ -> throwError $ "Expected a ForAll in a type application, got " ++ show tyt++
+ src/Unbound/Generics/LocallyNameless.hs view
@@ -0,0 +1,30 @@+-- |+-- Module     : Unbound.Generics.LocallyNameless+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+--+-- See 'Alpha', 'Bind', "Unbound.Generics.LocallyNameless.Operations" to get started. +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.Rebind,+  module Unbound.Generics.LocallyNameless.Fresh,+  module Unbound.Generics.LocallyNameless.LFresh,+  module Unbound.Generics.LocallyNameless.Subst+  ) where++import Unbound.Generics.LocallyNameless.Alpha+import Unbound.Generics.LocallyNameless.Name hiding (Bn, Fn)+import Unbound.Generics.LocallyNameless.Bind hiding (B)+import Unbound.Generics.LocallyNameless.Embed+import Unbound.Generics.LocallyNameless.Rebind hiding (Rebnd)+import Unbound.Generics.LocallyNameless.Fresh+import Unbound.Generics.LocallyNameless.LFresh+import Unbound.Generics.LocallyNameless.Operations+import Unbound.Generics.LocallyNameless.Subst
+ src/Unbound/Generics/LocallyNameless/Alpha.hs view
@@ -0,0 +1,610 @@+{-# OPTIONS_HADDOCK show-extensions #-}+-- |+-- Module     : Unbound.Generics.LocallyNameless.Alpha+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- Use the 'Alpha' typeclass to mark types that may contain 'Name's.+{-# LANGUAGE DefaultSignatures+             , FlexibleContexts+             , TypeOperators #-}+module Unbound.Generics.LocallyNameless.Alpha (+  -- * Name-aware opertions+  Alpha(..)+  -- * Binder variables+  , DisjointSet(..)+  , inconsistentDisjointSet+  , singletonDisjointSet+  , isConsistentDisjointSet+  -- * Implementation details+  , NthPatFind+  , NamePatFind+  , AlphaCtx+  , initialCtx+  , patternCtx+  , termCtx+  , isTermCtx+  , incrLevelCtx+  ) where++import Control.Applicative (Applicative(..), (<$>))+import Control.Arrow (first)+import Control.Monad (liftM)+import Data.Function (on)+import Data.Functor.Contravariant (Contravariant(..))+import Data.Foldable (Foldable(..))+import Data.List (intersect)+import Data.Monoid (Monoid(..), (<>))+import Data.Ratio (Ratio)+import Data.Typeable (Typeable, gcast)+import GHC.Generics++import Unbound.Generics.LocallyNameless.Name+import Unbound.Generics.LocallyNameless.Fresh+import Unbound.Generics.LocallyNameless.LFresh+import Unbound.Generics.PermM++-- | Some 'Alpha' operations need to record information about their+-- progress.  Instances should just pass it through unchanged.+--+-- The context records whether we are currently operating on terms or patterns,+-- and how many binding levels we've descended.+data AlphaCtx = AlphaCtx { ctxMode :: !Mode, ctxLevel :: !Integer }++data Mode = Term | Pat+          deriving Eq++-- | The starting context for alpha operations: we are expecting to+-- work on terms and we are under no binders.+initialCtx :: AlphaCtx+initialCtx = AlphaCtx { ctxMode = Term, ctxLevel = 0 }++-- | Switches to a context where we expect to operate on patterns.+patternCtx :: AlphaCtx -> AlphaCtx+patternCtx ctx = ctx { ctxMode = Pat }++-- | Switches to a context where we expect to operate on terms.+termCtx :: AlphaCtx -> AlphaCtx+termCtx ctx = ctx { ctxMode = Term }++-- | Returns 'True' iff we are in a context where we expect to see terms.+isTermCtx :: AlphaCtx -> Bool+isTermCtx (AlphaCtx {ctxMode = Term}) = True+isTermCtx _                           = False++-- | Increment the number of binders that we are operating under.+incrLevelCtx :: AlphaCtx -> AlphaCtx+incrLevelCtx ctx = ctx { ctxLevel = 1 + ctxLevel ctx }++-- | 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'.+--+-- @+--   inconsistentDisjointSet \<> s == inconsistentDisjointSet+--   s \<> inconsistentDisjoinSet == inconsistentDisjointSet+-- @+newtype DisjointSet a = DisjointSet (Maybe [a])++instance Eq a => Monoid (DisjointSet a) where+  mempty = DisjointSet (Just [])+  mappend s1 s2 =+    case (s1, s2) of+      (DisjointSet (Just xs), DisjointSet (Just ys)) | disjointLists xs ys -> DisjointSet (Just (xs <> ys))+      _ -> inconsistentDisjointSet++instance Foldable DisjointSet where+  foldMap summarize (DisjointSet ms) = foldMap (foldMap summarize) ms++-- | Returns a @DisjointSet a@ that is the annihilator element for the 'Monoid' instance of 'DisjointSet'.+inconsistentDisjointSet :: DisjointSet a+inconsistentDisjointSet = DisjointSet Nothing++-- | @singletonDisjointSet x@ a @DisjointSet a@ that contains the single element @x@+singletonDisjointSet :: a -> DisjointSet a+singletonDisjointSet x = DisjointSet (Just [x])++disjointLists :: Eq a => [a] -> [a] -> Bool+disjointLists xs ys = null (intersect xs ys)++-- | @isConsistentDisjointSet@ returns @True@ iff the given disjoint set is not inconsistent.+isConsistentDisjointSet :: DisjointSet a -> Bool+isConsistentDisjointSet (DisjointSet Nothing) = False+isConsistentDisjointSet _ = True++-- | Types that are instances of @Alpha@ may participate in name representation.+--+-- Minimal instance is entirely empty, provided that your type is an instance of+-- 'Generic'.+class (Show a) => Alpha a where+  -- | See 'Unbound.Generics.LocallyNameless.Operations.aeq'.+  aeq' :: AlphaCtx -> a -> a -> Bool+  default aeq' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Bool+  aeq' c = (gaeq c) `on` from++  -- | See 'Unbound.Generics.LocallyNameless.Operations.fvAny'.+  -- @@@ fvAny' :: AlphaCtx -> Fold a AnyName @@@+  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++  -- | 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 c b = to . gclose c b . from++  -- | 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 c b = to . gopen c b . from++  -- | @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++  -- | @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 = gisTerm . from++  -- | @isEmbed@ is needed internally for the implementation of+  --   'isPat'.  @isEmbed@ is true for terms wrapped in 'Embed' and zero+  --   or more occurrences of 'Shift'.  The default implementation+  --   simply returns @False@.+  isEmbed :: a -> Bool+  isEmbed _ = False++  -- | If @a@ is a pattern, finds the @n@th name in the pattern+  -- (starting from zero), returning the number of names encountered+  -- if not found.+  nthPatFind :: a -> NthPatFind+  default nthPatFind :: (Generic a, GAlpha (Rep a)) => a -> NthPatFind+  nthPatFind = gnthPatFind . from++  -- | 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++  -- | 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++  -- | 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)++  -- | 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@.+  freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)+  default freshen'  :: (Generic a, GAlpha (Rep a), Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName)+  freshen' ctx = liftM (first to) . gfreshen ctx . from++-- | 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@+-- is the @i@th name in @a@+type NthPatFind = Integer -> Either Integer AnyName++-- | 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++-- | 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++  gisPat :: f a -> DisjointSet AnyName+  gisTerm :: f a -> Bool++  gnthPatFind :: f a -> NthPatFind+  gnamePatFind :: f a -> NamePatFind++  gswaps :: AlphaCtx -> Perm AnyName -> f a -> f a+  gfreshen :: Fresh m => AlphaCtx -> f a -> m (f a, Perm AnyName)++  glfreshen :: LFresh m => AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b+  +instance (Alpha c) => GAlpha (K1 i c) where+  gaeq ctx (K1 c1) (K1 c2) = aeq' ctx c1 c2++  gfvAny ctx nfn = fmap K1 . fvAny' ctx nfn . unK1++  gclose ctx b = K1 . close ctx b . unK1+  gopen ctx b = K1 . open ctx b . unK1++  gisPat = isPat . unK1+  gisTerm = isTerm . unK1++  gnthPatFind = nthPatFind . unK1+  gnamePatFind = namePatFind . unK1++  gswaps ctx perm = K1 . swaps' ctx perm . unK1+  gfreshen ctx = liftM (first K1) . freshen' ctx . unK1++  glfreshen ctx (K1 c) cont = lfreshen' ctx c (cont . K1)++instance GAlpha f => GAlpha (M1 i c f) where+  gaeq ctx (M1 f1) (M1 f2) = gaeq ctx f1 f2++  gfvAny ctx nfn = fmap M1 . gfvAny ctx nfn . unM1++  gclose ctx b = M1 . gclose ctx b . unM1+  gopen ctx b = M1 . gopen ctx b . unM1++  gisPat = gisPat . unM1+  gisTerm = gisTerm . unM1++  gnthPatFind = gnthPatFind . unM1+  gnamePatFind = gnamePatFind . unM1+  +  gswaps ctx perm = M1 . gswaps ctx perm . unM1+  gfreshen ctx = liftM (first M1) . gfreshen ctx . unM1++  glfreshen ctx (M1 f) cont =+    glfreshen ctx f (cont . M1)++instance GAlpha U1 where+  gaeq _ctx _ _ = True++  gfvAny _ctx _nfn _ = pure U1++  gclose _ctx _b _ = U1+  gopen _ctx _b _ = U1++  gisPat _ = mempty+  gisTerm _ = True++  gnthPatFind _ = Left+  gnamePatFind _ _ = Left 0++  gswaps _ctx _perm _ = U1+  gfreshen _ctx _ = return (U1, mempty)++  glfreshen _ctx _ cont = cont U1 mempty++instance GAlpha V1 where+  gaeq _ctx _ _ = False++  gfvAny _ctx _nfn = pure++  gclose _ctx _b _ = undefined+  gopen _ctx _b _ = undefined++  gisPat _ = mempty+  gisTerm _ = False++  gnthPatFind _ = Left+  gnamePatFind _ _ = Left 0++  gswaps _ctx _perm _ = undefined+  gfreshen _ctx _ = return (undefined, mempty)++  glfreshen _ctx _ cont = cont undefined mempty++instance (GAlpha f, GAlpha g) => GAlpha (f :*: g) where+  gaeq ctx (f1 :*: g1) (f2 :*: g2) =+    gaeq ctx f1 f2 && gaeq ctx g1 g2++  gfvAny ctx nfn (f :*: g) = (:*:) <$> gfvAny ctx nfn f+                                   <*> gfvAny ctx nfn g++  gclose ctx b (f :*: g) = gclose ctx b f :*: gclose ctx b g+  gopen ctx b (f :*: g) = gopen ctx b f :*: gopen ctx b g++  gisPat (f :*: g) = gisPat f <> gisPat g+  gisTerm (f :*: g) = gisTerm f && gisTerm g++  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++  gswaps ctx perm (f :*: g) =+    gswaps ctx perm f :*: gswaps ctx perm g++  gfreshen ctx (f :*: g) = do+    (g', perm2) <- gfreshen ctx g+    (f', perm1) <- gfreshen ctx (gswaps ctx perm2 f)+    return (f' :*: g', perm1 <> perm2)++  glfreshen ctx (f :*: g) cont =+    glfreshen ctx g $ \g' perm2 ->+    glfreshen ctx (gswaps ctx perm2 f) $ \f' perm1 ->+    cont (f' :*: g') (perm1 <> perm2)++instance (GAlpha f, GAlpha g) => GAlpha (f :+: g) where+  gaeq ctx  (L1 f1) (L1 f2) = gaeq ctx f1 f2+  gaeq ctx  (R1 g1) (R1 g2) = gaeq ctx g1 g2+  gaeq _ctx _       _       = False++  gfvAny ctx nfn (L1 f) = fmap L1 (gfvAny ctx nfn f)+  gfvAny ctx nfn (R1 g) = fmap R1 (gfvAny ctx nfn g)++  gclose ctx b (L1 f) = L1 (gclose ctx b f)+  gclose ctx b (R1 g) = R1 (gclose ctx b g)+  gopen ctx b (L1 f) = L1 (gopen ctx b f)+  gopen ctx b (R1 g) = R1 (gopen ctx b g)++  gisPat (L1 f) = gisPat f+  gisPat (R1 g) = gisPat g++  gisTerm (L1 f) = gisTerm f+  gisTerm (R1 g) = gisTerm g++  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++  gswaps ctx perm (L1 f) = L1 (gswaps ctx perm f)+  gswaps ctx perm (R1 f) = R1 (gswaps ctx perm f)++  gfreshen ctx (L1 f) = liftM (first L1) (gfreshen ctx f)+  gfreshen ctx (R1 f) = liftM (first R1) (gfreshen ctx f)+  +  glfreshen ctx (L1 f) cont =+    glfreshen ctx f (cont . L1)+  glfreshen ctx (R1 g) cont =+    glfreshen ctx g (cont . R1)+  ++-- ============================================================+-- Alpha instances for the usual types++instance Alpha Int where+  aeq' _ctx i j = i == j++  fvAny' _ctx _nfn i = pure i++  close _ctx _b i = i+  open _ctx _b i = i++  isPat _ = mempty+  isTerm _ = True++  nthPatFind _ = Left+  namePatFind _ _ = Left 0++  swaps' _ctx _p i = i+  freshen' _ctx i = return (i, mempty)+  lfreshen' _ctx i cont = cont i mempty++instance Alpha Char where+  aeq' _ctx i j = i == j++  fvAny' _ctx _nfn i = pure i++  close _ctx _b i = i+  open _ctx _b i = i++  isPat _ = mempty+  isTerm _ = True++  nthPatFind _ = Left+  namePatFind _ _ = Left 0++  swaps' _ctx _p i = i+  freshen' _ctx i = return (i, mempty)+  lfreshen' _ctx i cont = cont i mempty++instance Alpha Integer where+  aeq' _ctx i j = i == j++  fvAny' _ctx _nfn i = pure i++  close _ctx _b i = i+  open _ctx _b i = i++  isPat _ = mempty+  isTerm _ = True++  nthPatFind _ = Left+  namePatFind _ _ = Left 0++  swaps' _ctx _p i = i+  freshen' _ctx i = return (i, mempty)+  lfreshen' _ctx i cont = cont i mempty++instance Alpha Float where+  aeq' _ctx i j = i == j++  fvAny' _ctx _nfn i = pure i++  close _ctx _b i = i+  open _ctx _b i = i++  isPat _ = mempty+  isTerm _ = True++  nthPatFind _ = Left+  namePatFind _ _ = Left 0++  swaps' _ctx _p i = i+  freshen' _ctx i = return (i, mempty)+  lfreshen' _ctx i cont = cont i mempty++instance Alpha Double where+  aeq' _ctx i j = i == j++  fvAny' _ctx _nfn i = pure i++  close _ctx _b i = i+  open _ctx _b i = i++  isPat _ = mempty+  isTerm _ = True++  nthPatFind _ = Left+  namePatFind _ _ = Left 0++  swaps' _ctx _p i = i+  freshen' _ctx i = return (i, mempty)+  lfreshen' _ctx i cont = cont i mempty++instance (Integral n, Alpha n) => Alpha (Ratio n) where+  aeq' _ctx i j = i == j++  fvAny' _ctx _nfn i = pure i++  close _ctx _b i = i+  open _ctx _b i = i++  isPat _ = mempty+  isTerm _ = True++  nthPatFind _ = Left+  namePatFind _ _ = Left 0++  swaps' _ctx _p i = i+  freshen' _ctx i = return (i, mempty)+  lfreshen' _ctx i cont = cont i mempty++instance Alpha Bool++instance Alpha a => Alpha (Maybe a)+instance Alpha a => Alpha [a]+instance (Alpha a,Alpha b) => Alpha (Either a b)+instance (Alpha a,Alpha b) => Alpha (a,b)+instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c)+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)++-- ============================================================+-- Alpha instances for interesting types++instance Typeable a => Alpha (Name a) where+  aeq' ctx n1 n2 =+    if isTermCtx ctx+    then n1 == n2 -- in terms, better be the same name+    else True     -- in a pattern, names are always equivlent (since+                  -- they're both bound, so they can vary).++  fvAny' ctx nfn nm = if isTermCtx ctx && isFreeName nm+                      then contramap AnyName  (nfn (AnyName nm))+                      else pure nm++  open ctx b a@(Bn l k) =+    if ctxMode ctx == Term && ctxLevel ctx == l+    then case nthPatFind b k of+      Right (AnyName nm) -> case gcast nm of+        Just nm' -> nm'+        Nothing -> error "LocallyNameless.open: inconsistent sorts"+      Left _ -> error "LocallyNameless.open : inconsistency - pattern had too few variables"+    else+      a+  open _ctx _ a = a++  close ctx b a@(Fn _ _) =+    if isTermCtx ctx+    then case namePatFind b (AnyName a) of+      Right k -> Bn (ctxLevel ctx) k+      Left _ -> a+    else a+  close _ctx _ a = a+  ++  isPat n = if isFreeName n+            then singletonDisjointSet (AnyName n)+            else inconsistentDisjointSet++  isTerm _ = True++  nthPatFind nm i =+    if i == 0 then Right (AnyName nm) else Left $! i-1++  namePatFind nm1 (AnyName nm2) =+    case gcast nm1 of+      Just nm1' -> if nm1' == nm2 then Right 0 else Left 1+      Nothing -> Left 1++  swaps' ctx perm nm =+    if isTermCtx ctx+    then case apply perm (AnyName nm) of+      AnyName nm' ->+        case gcast nm' of+          Just nm'' -> nm''+          Nothing -> error "Internal error swaps' on a Name returned permuted name of wrong sort"+    else nm+      +  freshen' ctx nm =+    if not (isTermCtx ctx)+    then do+      nm' <- fresh nm+      return (nm', single (AnyName nm) (AnyName nm'))+    else error "freshen' on a Name in term position"++  lfreshen' ctx nm cont =+    if not (isTermCtx ctx)+    then do+      nm' <- lfresh nm+      avoid [AnyName nm'] $ cont nm' $ single (AnyName nm) (AnyName nm')+    else error "lfreshen' on a Name in term position"++instance Alpha AnyName where+  aeq' ctx x y =+    if x == y+    then True+    else+      -- in a term unequal variables are unequal, in a pattern it's+      -- ok.+      not (isTermCtx ctx)++  fvAny' ctx nfn n@(AnyName nm) = if isTermCtx ctx && isFreeName nm+                                  then nfn n+                                  else pure n++  isTerm _ = True++  isPat n@(AnyName nm) = if isFreeName nm+                         then singletonDisjointSet n+                         else inconsistentDisjointSet++  swaps' ctx perm n =+    if isTermCtx ctx+    then apply perm n+    else n++  freshen' ctx (AnyName nm) =+    if isTermCtx ctx+    then error "LocallyNameless.freshen' on AnyName in Term mode"+    else do+      nm' <- fresh nm+      return (AnyName nm', single (AnyName nm) (AnyName nm'))++  lfreshen' ctx (AnyName nm) cont =+    if isTermCtx ctx+    then error "LocallyNameless.lfreshen' on AnyName in Term mode"+    else do+      nm' <- lfresh nm+      avoid [AnyName nm'] $ cont (AnyName nm') $ single (AnyName nm) (AnyName nm')++  open ctx b (AnyName nm) = AnyName (open ctx b nm)++  close ctx b (AnyName nm) = AnyName (close ctx b nm)+    +  nthPatFind nm i =+    if i == 0 then Right nm else Left $! i - 1++  namePatFind nmHave nmWant =+    if nmHave == nmWant+    then Right 0+    else Left 1
+ src/Unbound/Generics/LocallyNameless/Bind.hs view
@@ -0,0 +1,77 @@+{-# OPTIONS_HADDOCK show-extensions #-}+-- |+-- Module     : Unbound.Generics.LocallyNameless.Bind+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- The fundamental binding form.  The type @'Bind' p t@ allows you to+-- place a pattern @p@ in a term @t@ such that the names in the+-- pattern scope over the term.  Use 'Unbound.Generics.LocallyNameless.Operations.bind'+-- and 'Unbound.Generics.LocallyNameless.Operations.unbind' and 'Unbound.Generics.LocallyNameless.Operations.lunbind'+-- to work with @'Bind' p t@+{-# LANGUAGE DeriveGeneric #-}+module Unbound.Generics.LocallyNameless.Bind (+  -- * Name binding+  Bind(..)+  ) where++import Control.Applicative (Applicative(..), (<$>))+import Data.Monoid ((<>))++import GHC.Generics (Generic)++import Unbound.Generics.LocallyNameless.Alpha++-- | A term of type @'Bind' p t@ is a term that binds the free+-- variable occurrences of the variables in pattern @p@ in the term+-- @t@.  In the overall term, those variables are now bound. See also+-- 'Unbound.Generics.LocallyNameless.Operations.bind' and+-- 'Unbound.Generics.LocallyNameless.Operations.unbind' and+-- 'Unbound.Generics.LocallyNameless.Operations.lunbind'+data Bind p t = B p t+              deriving (Generic)++instance (Show p, Show t) => Show (Bind p t) where+  showsPrec prec (B p t) =+    showParen (prec > 0) (showString "<"+                          . showsPrec prec p+                          . showString "> "+                          . showsPrec 0 t)++instance (Alpha p, Alpha t) => Alpha (Bind p t) where++  aeq' ctx (B p1 t1) (B p2 t2) =+    aeq' (patternCtx ctx) p1 p2+    && aeq' (incrLevelCtx ctx) t1 t2++  fvAny' ctx nfn (B p t) = B <$> fvAny' (patternCtx ctx) nfn p+                             <*> fvAny' (incrLevelCtx ctx) nfn t++  isPat _ = inconsistentDisjointSet++  isTerm (B p t) = isConsistentDisjointSet (isPat p) && isTerm t++  close ctx b (B p t) =+    B (close (patternCtx ctx) b p) (close (incrLevelCtx ctx) b t)++  open ctx b (B p t) =+    B (open (patternCtx ctx) b p) (open (incrLevelCtx ctx) b t)++  nthPatFind b = error $ "Binding " ++ show b ++ " used as a pattern"+  namePatFind b = error $ "Binding " ++ show b ++ " used as a pattern"++  swaps' ctx perm (B p t) =+    B (swaps' (patternCtx ctx) perm p)+      (swaps' (incrLevelCtx ctx) perm t)++  freshen' ctx (B p t) = do+    (p', perm1) <- freshen' (patternCtx ctx) p+    (t', perm2) <- freshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) perm1 t)+    return (B p' t', perm1 <> perm2)++  lfreshen' ctx (B p t) cont =+    lfreshen' (patternCtx ctx) p $ \p' pm1 ->+    lfreshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) pm1 t) $ \t' pm2 ->+    cont (B p' t') (pm1 <> pm2)
+ src/Unbound/Generics/LocallyNameless/Embed.hs view
@@ -0,0 +1,77 @@+{-# OPTIONS_HADDOCK show-extensions #-}+-- |+-- Module     : Unbound.Generics.LocallyNameless.Embed+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- The pattern @'Embed' t@ contains a term @t@.+{-# LANGUAGE DeriveGeneric #-}+module Unbound.Generics.LocallyNameless.Embed where++import Control.Applicative (pure, (<$>))+import Data.Monoid (mempty)+import GHC.Generics (Generic)++import Unbound.Generics.LocallyNameless.Alpha++-- | @Embed@ allows for terms to be /embedded/ within patterns.  Such+--   embedded terms do not bind names along with the rest of the+--   pattern.  For examples, see the tutorial or examples directories.+--+--   If @t@ is a /term type/, then @Embed t@ is a /pattern type/.+--+--   @Embed@ is not abstract since it involves no binding, and hence+--   it is safe to manipulate directly.  To create and destruct+--   @Embed@ terms, you may use the @Embed@ constructor directly.+--   (You may also use the functions 'embed' and 'unembed', which+--   additionally can construct or destruct any number of enclosing+--   'Shift's at the same time.)+newtype Embed t = Embed t deriving (Eq, Generic)++instance Show a => Show (Embed a) where+  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++  isTerm _ = False++  isEmbed (Embed t) = isTerm t++  swaps' ctx perm (Embed t) =+    if isTermCtx ctx+    then Embed t+    else Embed (swaps' (termCtx ctx) perm t)++  freshen' ctx p =+    if isTermCtx ctx+    then error "LocallyNameless.freshen' called on a term"+    else return (p, mempty)++  lfreshen' ctx p cont =+    if isTermCtx ctx+    then error "LocallyNameless.lfreshen' called on a term"+    else cont p mempty+++  aeq' ctx (Embed x) (Embed y) = aeq' (termCtx ctx) x y++  fvAny' ctx afa ex@(Embed x) =+    if isTermCtx ctx+    then pure ex+    else Embed <$> fvAny' (termCtx ctx) afa x++  close ctx b (Embed x) =+    if isTermCtx ctx+    then error "LocallyNameless.close on Embed"+    else Embed (close (termCtx ctx) b x)++  open ctx b (Embed x) =+    if isTermCtx ctx+    then error "LocallyNameless.open on Embed"+    else Embed (open (termCtx ctx) b x)++  nthPatFind _ = Left+  namePatFind _ _ = Left 0
+ src/Unbound/Generics/LocallyNameless/Fresh.hs view
@@ -0,0 +1,140 @@+-- |+-- Module     : Unbound.Generics.LocallyNameless.Fresh+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- Global freshness monad.+{-# LANGUAGE CPP, GeneralizedNewtypeDeriving,+             FlexibleInstances, MultiParamTypeClasses,+             UndecidableInstances+  #-}+-- (we expect deprecation warnings about Control.Monad.Trans.Error)+{-# OPTIONS_GHC -Wwarn #-}+module Unbound.Generics.LocallyNameless.Fresh where++import Control.Applicative (Applicative, Alternative)+import Control.Monad ()++import Control.Monad.Identity++import Control.Monad.Trans+#if MIN_VERSION_transformers(0,4,0)+import Control.Monad.Trans.Except+#endif+import Control.Monad.Trans.Error+import Control.Monad.Trans.Maybe+import Control.Monad.Trans.Reader+import Control.Monad.Trans.State.Lazy as Lazy+import Control.Monad.Trans.State.Strict as Strict+import Control.Monad.Trans.Writer.Lazy as Lazy+import Control.Monad.Trans.Writer.Strict as Strict++import qualified Control.Monad.Cont.Class as CC+import qualified Control.Monad.Error.Class as EC+import qualified Control.Monad.State.Class as StC+import qualified Control.Monad.Reader.Class as RC+import qualified Control.Monad.Writer.Class as WC++import Data.Monoid (Monoid)++import qualified Control.Monad.State as St++import Unbound.Generics.LocallyNameless.Name++-- | The @Fresh@ type class governs monads which can generate new+--   globally unique 'Name's based on a given 'Name'.+class Monad m => Fresh m where++  -- | Generate a new globally unique name based on the given one.+  fresh :: Name a -> m (Name a)+++-- | The @FreshM@ monad transformer.  Keeps track of the lowest index+--   still globally unused, and increments the index every time it is+--   asked for a fresh name.+newtype FreshMT m a = FreshMT { unFreshMT :: St.StateT Integer m a }+  deriving (Functor, Applicative, Alternative, Monad, MonadPlus, MonadIO, MonadFix)++-- | Run a 'FreshMT' computation (with the global index starting at zero).+runFreshMT :: Monad m => FreshMT m a -> m a+runFreshMT m = contFreshMT m 0++-- | Run a 'FreshMT' computation given a starting index for fresh name+--   generation.+contFreshMT :: Monad m => FreshMT m a -> Integer -> m a+contFreshMT (FreshMT m) = St.evalStateT m++instance MonadTrans FreshMT where+  lift = FreshMT . lift++instance CC.MonadCont m => CC.MonadCont (FreshMT m) where+  callCC c = FreshMT $ CC.callCC (unFreshMT . (\k -> c (FreshMT . k)))++instance EC.MonadError e m => EC.MonadError e (FreshMT m) where+  throwError = lift . EC.throwError+  catchError m h = FreshMT $ EC.catchError (unFreshMT m) (unFreshMT . h)++instance StC.MonadState s m => StC.MonadState s (FreshMT m) where+  get = lift StC.get+  put = lift . StC.put++instance RC.MonadReader r m => RC.MonadReader r (FreshMT m) where+  ask   = lift RC.ask+  local f = FreshMT . RC.local f . unFreshMT++instance WC.MonadWriter w m => WC.MonadWriter w (FreshMT m) where+  tell   = lift . WC.tell+  listen = FreshMT . WC.listen . unFreshMT+  pass   = FreshMT . WC.pass . unFreshMT+++instance Monad m => Fresh (FreshMT m) where+  fresh (Fn s _) = FreshMT $ do+    n <- St.get+    St.put $! n + 1+    return $ (Fn s n)+  fresh nm@(Bn {}) = return nm++instance (Error e, Fresh m) => Fresh (ErrorT e m) where+  fresh = lift . fresh++#if MIN_VERSION_transformers(0,4,0)+instance Fresh m => Fresh (ExceptT e m) where+  fresh = lift . fresh+#endif++instance Fresh m => Fresh (MaybeT m) where+  fresh = lift . fresh++instance Fresh m => Fresh (ReaderT r m) where+  fresh = lift . fresh++instance Fresh m => Fresh (Lazy.StateT s m) where+  fresh = lift . fresh++instance Fresh m => Fresh (Strict.StateT s m) where+  fresh = lift . fresh++instance (Monoid w, Fresh m) => Fresh (Lazy.WriterT w m) where+  fresh = lift . fresh++instance (Monoid w, Fresh m) => Fresh (Strict.WriterT w m) where+  fresh = lift . fresh++------------------------------------------------------------+-- FreshM monad++-- | A convenient monad which is an instance of 'Fresh'.  It keeps+--   track of a global index used for generating fresh names, which is+--   incremented every time 'fresh' is called.+type FreshM = FreshMT Identity++-- | Run a FreshM computation (with the global index starting at zero).+runFreshM :: FreshM a -> a+runFreshM = runIdentity . runFreshMT++-- | Run a FreshM computation given a starting index.+contFreshM :: FreshM a -> Integer -> a+contFreshM m = runIdentity . contFreshMT m
+ src/Unbound/Generics/LocallyNameless/Internal/Fold.hs view
@@ -0,0 +1,44 @@+-- |+-- Module     : Unbound.Generics.LocallyNameless.Internal.Fold+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- | Some utilities for working with Folds.+{-# LANGUAGE RankNTypes #-}+module Unbound.Generics.LocallyNameless.Internal.Fold (Fold, Traversal', toListOf, filtered, justFiltered) where++import Control.Applicative+import Data.Maybe (fromJust)+import Data.Functor.Contravariant+import Data.Monoid++type Getting r s a = (a -> Const r a) -> s -> Const r s++type Fold s a = forall f . (Contravariant f, Applicative f) => (a -> f a) -> s -> f s++type Traversal' s a = forall f . Applicative f => (a -> f a) -> s -> f s++toListOf :: Fold s a -> s -> [a]+-- toListOf :: Getting (Endo [a]) s a -> s -> [a]+toListOf l = foldrOf l (:) []+{-# INLINE toListOf #-}++foldMapOf :: Getting r s a -> (a -> r) -> s -> r+foldMapOf l f = getConst . l (Const . f)+{-# INLINE foldMapOf #-}++foldrOf :: Getting (Endo r) s a -> (a -> r -> r) -> r -> s -> r+foldrOf l f z = fmap (flip appEndo z) (foldMapOf l (Endo .f))+{-# INLINE foldrOf #-}++filtered :: (a -> Bool) -> Traversal' a a+filtered p afa x = if p x then afa x else pure x+{-# INLINE filtered #-}++justFiltered :: (a -> Maybe b) -> Fold a b+justFiltered p bfb x = case p x of+                        Just b -> contramap (fromJust . p) (bfb b)+                        Nothing -> pure x+{-# INLINE justFiltered #-}
+ src/Unbound/Generics/LocallyNameless/LFresh.hs view
@@ -0,0 +1,220 @@+{-# OPTIONS_HADDOCK show-extensions #-}+-- |+-- Module     : Unbound.Generics.LocallyNameless.LFresh+-- Copyright  : (c) 2011, Stephanie Weirich+-- License    : BSD3 (See LFresh.hs)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- Local freshness monad.+{-+Copyright (c)2011, Stephanie Weirich++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Stephanie Weirich nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+-}+-- we expect deprecation warnings about Control.Monad.Trans.Error+{-# OPTIONS_GHC -Wwarn #-}+{-# LANGUAGE CPP+             , GeneralizedNewtypeDeriving+             , FlexibleInstances+             , MultiParamTypeClasses+             , UndecidableInstances #-}+module Unbound.Generics.LocallyNameless.LFresh+       (+         -- * The 'LFresh' class++         LFresh(..),++         LFreshM, runLFreshM, contLFreshM,+         LFreshMT(..), runLFreshMT, contLFreshMT++       ) where++import Data.Set (Set)+import qualified Data.Set as S++import Data.Monoid+import Data.Typeable (Typeable)++import Control.Monad.Reader+import Control.Monad.Identity+import Control.Applicative (Applicative, Alternative)++import Control.Monad.Trans.Cont+import Control.Monad.Trans.Error+#if MIN_VERSION_transformers(0,4,0)+import Control.Monad.Trans.Except+#endif+import Control.Monad.Trans.Identity+import Control.Monad.Trans.List+import Control.Monad.Trans.Maybe+import Control.Monad.Trans.State.Lazy as Lazy+import Control.Monad.Trans.State.Strict as Strict+import Control.Monad.Trans.Writer.Lazy as Lazy+import Control.Monad.Trans.Writer.Strict as Strict++import qualified Control.Monad.Cont.Class as CC+import qualified Control.Monad.Error.Class as EC+import qualified Control.Monad.State.Class as StC+import qualified Control.Monad.Reader.Class as RC+import qualified Control.Monad.Writer.Class as WC++import Unbound.Generics.LocallyNameless.Name++-- | This is the class of monads that support freshness in an+--   (implicit) local scope.  Generated names are fresh for the current+--   local scope, not necessarily globally fresh.+class Monad m => LFresh m where+  -- | Pick a new name that is fresh for the current (implicit) scope.+  lfresh  :: Typeable a => Name a -> m (Name a)+  -- | Avoid the given names when freshening in the subcomputation,+  --   that is, add the given names to the in-scope set.+  avoid   :: [AnyName] -> m a -> m a+  -- | Get the set of names currently being avoided.+  getAvoids :: m (Set AnyName)++-- | The LFresh monad transformer.  Keeps track of a set of names to+-- avoid, and when asked for a fresh one will choose the first numeric+-- prefix of the given name which is currently unused.+newtype LFreshMT m a = LFreshMT { unLFreshMT :: ReaderT (Set AnyName) m a }+  deriving (Functor, Applicative, Alternative, Monad, MonadIO, MonadPlus, MonadFix)++-- | Run an 'LFreshMT' computation in an empty context.+runLFreshMT :: LFreshMT m a -> m a+runLFreshMT m = contLFreshMT m S.empty++-- | Run an 'LFreshMT' computation given a set of names to avoid.+contLFreshMT :: LFreshMT m a -> Set AnyName -> m a+contLFreshMT (LFreshMT m) = runReaderT m++instance Monad m => LFresh (LFreshMT m) where+  lfresh nm = LFreshMT $ do+    let s = name2String nm+    used <- ask+    return $ head (filter (\x -> not (S.member (AnyName x) used))+                          (map (makeName s) [0..]))+  avoid names = LFreshMT . local (S.union (S.fromList names)) . unLFreshMT++  getAvoids = LFreshMT ask++-- | A convenient monad which is an instance of 'LFresh'.  It keeps+--   track of a set of names to avoid, and when asked for a fresh one+--   will choose the first unused numerical name.+type LFreshM = LFreshMT Identity++-- | Run a LFreshM computation in an empty context.+runLFreshM :: LFreshM a -> a+runLFreshM = runIdentity . runLFreshMT++-- | Run a LFreshM computation given a set of names to avoid.+contLFreshM :: LFreshM a -> Set AnyName -> a+contLFreshM m = runIdentity . contLFreshMT m++instance LFresh m => LFresh (ContT r m) where+  lfresh = lift . lfresh+  avoid  = mapContT . avoid+  getAvoids = lift getAvoids++instance (Error e, LFresh m) => LFresh (ErrorT e m) where+  lfresh = lift . lfresh+  avoid  = mapErrorT . avoid+  getAvoids = lift getAvoids++#if MIN_VERSION_transformers(0,4,0)+instance LFresh m => LFresh (ExceptT e m) where+  lfresh = lift . lfresh+  avoid = mapExceptT . avoid+  getAvoids = lift getAvoids+#endif++instance LFresh m => LFresh (IdentityT m) where+  lfresh = lift . lfresh+  avoid  = mapIdentityT . avoid+  getAvoids = lift getAvoids++instance LFresh m => LFresh (ListT m) where+  lfresh = lift . lfresh+  avoid  = mapListT . avoid+  getAvoids = lift getAvoids++instance LFresh m => LFresh (MaybeT m) where+  lfresh = lift . lfresh+  avoid  = mapMaybeT . avoid+  getAvoids = lift getAvoids++instance LFresh m => LFresh (ReaderT r m) where+  lfresh = lift . lfresh+  avoid  = mapReaderT . avoid+  getAvoids = lift getAvoids++instance LFresh m => LFresh (Lazy.StateT s m) where+  lfresh = lift . lfresh+  avoid  = Lazy.mapStateT . avoid+  getAvoids = lift getAvoids++instance LFresh m => LFresh (Strict.StateT s m) where+  lfresh = lift . lfresh+  avoid  = Strict.mapStateT . avoid+  getAvoids = lift getAvoids++instance (Monoid w, LFresh m) => LFresh (Lazy.WriterT w m) where+  lfresh = lift . lfresh+  avoid  = Lazy.mapWriterT . avoid+  getAvoids = lift getAvoids++instance (Monoid w, LFresh m) => LFresh (Strict.WriterT w m) where+  lfresh = lift . lfresh+  avoid  = Strict.mapWriterT . avoid+  getAvoids = lift getAvoids++-- Instances for applying LFreshMT to other monads++instance MonadTrans LFreshMT where+  lift = LFreshMT . lift++instance CC.MonadCont m => CC.MonadCont (LFreshMT m) where+  callCC c = LFreshMT $ CC.callCC (unLFreshMT . (\k -> c (LFreshMT . k)))++instance EC.MonadError e m => EC.MonadError e (LFreshMT m) where+  throwError = lift . EC.throwError+  catchError m h = LFreshMT $ EC.catchError (unLFreshMT m) (unLFreshMT . h)++instance StC.MonadState s m => StC.MonadState s (LFreshMT m) where+  get = lift StC.get+  put = lift . StC.put++instance RC.MonadReader r m => RC.MonadReader r (LFreshMT m) where+  ask   = lift RC.ask+  local f = LFreshMT . mapReaderT (RC.local f) . unLFreshMT++instance WC.MonadWriter w m => WC.MonadWriter w (LFreshMT m) where+  tell   = lift . WC.tell+  listen = LFreshMT . WC.listen . unLFreshMT+  pass   = LFreshMT . WC.pass . unLFreshMT
+ src/Unbound/Generics/LocallyNameless/Name.hs view
@@ -0,0 +1,96 @@+-- |+-- Module     : Unbound.Generics.LocallyNameless.Name+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- Names stand for values.  They may be bound or free.+{-# LANGUAGE DeriveDataTypeable+             , DeriveGeneric+             , ExistentialQuantification+             , FlexibleContexts+             , GADTs #-}+module Unbound.Generics.LocallyNameless.Name+       (+         -- * Names over terms+         Name(..)+       , isFreeName+         -- * Name construction+       , string2Name+       , s2n+       , makeName+         -- * Name inspection+       , name2String+         -- * Heterogeneous names+       , AnyName(..)+       ) where++import Data.Typeable (Typeable, gcast, typeOf)+import GHC.Generics (Generic)++-- | An abstract datatype of names @Name a@ that stand for terms of+-- type @a@.  The type @a@ is used as a tag to distinguish these names+-- from names that may stand for other sorts of terms.+--+-- Two names in a term are consider+-- 'Unbound.Generics.LocallyNameless.Operations.aeq' equal when they+-- are the same name (in the sense of '(==)').  In patterns, however,+-- any two names are equal if they occur in the same place within the+-- pattern.  This induces alpha equivalence on terms in general.+--+-- Names may either be free or bound (see 'isFreeName').  Free names+-- may be extracted from patterns using+-- 'Unbound.Generics.LocallyNameless.Alpha.isPat'.  Bound names+-- cannot be.+-- +data Name a = Fn String !Integer    -- free names+            | Bn !Integer !Integer  -- bound names / binding level + pattern index+            deriving (Eq, Ord, Typeable, Generic)++-- | Returns 'True' iff the given @Name a@ is free.+isFreeName :: Name a -> Bool+isFreeName (Fn _ _) = True+isFreeName _ = False++-- | Make a free 'Name a' from a 'String'+string2Name :: String -> Name a+string2Name s = makeName s 0++-- | Synonym for 'string2Name'.+s2n :: String -> Name a+s2n = string2Name++-- | Make a name from a 'String' and an 'Integer' index+makeName :: String -> Integer -> Name a+makeName = Fn++-- | Get the string part of a 'Name'.+name2String :: Name a -> String+name2String (Fn s _) = s+name2String (Bn _ _)   = error "Internal Error: cannot call name2Integer for bound names"++instance Show (Name a) where+  show (Fn "" n) = "_" ++ (show n)+  show (Fn x 0) = x+  show (Fn x n) = x ++ (show n)+  show (Bn x y) = show x ++ "@" ++ show y++-- | An @AnyName@ is a name that stands for a term of some (existentially hidden) type.+data AnyName where+  AnyName :: Typeable a => Name a -> AnyName++instance Show AnyName where+  show (AnyName nm) = show nm++instance Eq AnyName where+  (AnyName n1) == (AnyName n2) = case gcast n2 of+    Just n2' -> n1 == n2'+    Nothing -> False++instance Ord AnyName where+  compare (AnyName n1) (AnyName n2) = case compare (typeOf n1) (typeOf n2) of+    EQ -> case gcast n2 of+      Just n2' -> compare n1 n2'+      Nothing -> error "Equal type representations, but gcast failed in comparing two AnyName values"+    ord -> ord
+ src/Unbound/Generics/LocallyNameless/Operations.hs view
@@ -0,0 +1,162 @@+-- |+-- Module     : Unbound.Generics.LocallyNameless.Operations+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- Operations on terms and patterns that contain names.+{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}+module Unbound.Generics.LocallyNameless.Operations+       (-- * Equivalence, free variables, freshness+         aeq+       , fvAny+       , fv+       , freshen+       , lfreshen+       , swaps+         -- * Binding, unbinding+       , Bind+       , bind+       , unbind+       , lunbind+       , unbind2+       , unbind2Plus+         -- * Rebinding, embedding+       , Rebind+       , rebind+       , unrebind+       , Embed(..)+       , embed+       , unembed+       ) where++import Control.Applicative (Applicative)+import Control.Monad (MonadPlus(mzero))+import Data.Functor.Contravariant (Contravariant)+import Data.Monoid ((<>))+import Data.Typeable (Typeable, cast)+import Unbound.Generics.LocallyNameless.Alpha+import Unbound.Generics.LocallyNameless.Fresh+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.Rebind+import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf, justFiltered)+import Unbound.Generics.PermM++-- | @'aeq' t1 t2@ returns @True@ iff @t1@ and @t2@ are alpha-equivalent terms.+aeq :: Alpha a => a -> a -> Bool+aeq = aeq' initialCtx++-- | @'fvAny' t@ returns the free variables of the term @t@.+--+-- @+--   fvAny :: Alpha a => a -> Fold a AnyName+-- @+fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a+fvAny = fvAny' initialCtx++-- | @'fv' t@ returns the free @b@ variables of term @t@.+--+-- @+--  fv :: (Alpha a, Typeable b) => a -> Fold a (Name b)+-- @+fv :: forall a f b . (Alpha a, Typeable b, Contravariant f, Applicative f)+      => (Name b -> f (Name b)) -> a -> f a+fv = fvAny . justFiltered f+  where f :: AnyName -> Maybe (Name b)+        f (AnyName n) = cast n++-- | Freshen a pattern by replacing all old binding 'Name's with new+--   fresh 'Name's, returning a new pattern and a @'Perm' 'Name'@+--   specifying how 'Name's were replaced.+freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)+freshen = freshen' (patternCtx initialCtx)++-- | \"Locally\" freshen a pattern, replacing all binding names with+--   new names that are not already \"in scope\". The second argument+--   is a continuation, which takes the renamed term and a permutation+--   that specifies how the pattern has been renamed.  The resulting+--   computation will be run with the in-scope set extended by the+--   names just generated.+lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b+lfreshen = lfreshen' (patternCtx initialCtx)++-- | Apply the given permutation of variable names to the given term.+swaps :: Alpha t => Perm AnyName -> t -> t+swaps = swaps' initialCtx++  +-- | @'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)++-- | @'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+-- variables in the pattern have been made globally fresh with respect+-- to the freshness monad @m@.+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)++-- | @lunbind@ opens a binding in an 'LFresh' monad, ensuring that the+--   names chosen for the binders are /locally/ fresh.  The components+--   of the binding are passed to a /continuation/, and the resulting+--   monadic action is run in a context extended to avoid choosing new+--   names which are the same as the ones chosen for this binding.+--+--   For more information, see the documentation for the 'LFresh' type+--   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))+++-- | Simultaneously unbind two patterns in two terms, returning 'Nothing' if+-- the two patterns don't bind the same number of variables.+unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2)+           => Bind p1 t1+           -> Bind p2 t2+           -> m (Maybe (p1, t1, p2, t2))+unbind2 (B p1 t1) (B p2 t2) = do+      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)+         Nothing -> return Nothing+++-- | Simultaneously unbind two patterns in two terms, returning 'mzero' if+-- the patterns don't bind the same number of variables.+unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2)+         => Bind p1 t1+         -> Bind p2 t2+         -> m (p1, t1, p2, t2)+unbind2Plus bnd bnd' = maybe mzero return =<< unbind2 bnd bnd'+++-- | @'rebind' p1 p2@ is a smart constructor for 'Rebind'.  It+-- 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)++-- | @'unrebind' p@ is the elimination form for 'Rebind'. It is not+-- monadic (unlike 'unbind') because a @Rebind@ pattern can only occur+-- somewhere in a pattern position of a 'Bind', and therefore 'unbind'+-- 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)++-- | An alias for 'Embed'+embed :: t -> Embed t+embed = Embed++-- | @'unembed' p@ extracts the term embedded in the pattern @p@.+unembed :: Embed t -> t+unembed (Embed t) = t
+ src/Unbound/Generics/LocallyNameless/Rebind.hs view
@@ -0,0 +1,85 @@+{-# OPTIONS_HADDOCK show-extensions #-}+-- |+-- Module     : Unbound.Generics.LocallyNameless.Rebind+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- The pattern @'Rebind' p1 p2@ binds the names in @p1@ and @p2@ just as @(p1, p2)@ would,+-- however it additionally also brings the names of @p1@ into scope in @p2@.+--+{-# LANGUAGE DeriveGeneric #-}+module Unbound.Generics.LocallyNameless.Rebind where++import Control.Applicative ((<*>), (<$>))+import Data.Monoid ((<>))+import GHC.Generics++import Unbound.Generics.LocallyNameless.Alpha+++-- | @'Rebind' p1 p2@ is a pattern that binds the names of @p1@ and @p2@, and additionally+-- brings the names of @p1@ into scope over @p2@.+--+-- This may be used, for example, to faithfully represent Scheme's @let*@ binding form, defined by:+-- +-- >  (let* () body) ≙ body+-- >  (let* ([v1, e1] binds ...) body) ≙ (let ([v1, e1]) (let* (binds ...) body))+-- +-- using the following AST:+--+-- @+-- type Var = Name Expr+-- data Lets = EmptyLets+--           | Bind (Rebind (Var, Embed Expr) Lets)+-- data Expr = ...+--           | LetStar { letStarBindings :: Lets+--                     , letStarBody :: Expr+--                     }+--           | ...+-- @+data Rebind p1 p2 = Rebnd p1 p2+                  deriving (Generic, Eq)++instance (Show p1, Show p2) => Show (Rebind p1 p2) where+  showsPrec paren (Rebnd p1 p2) =+    showParen (paren > 0) (showString "<<"+                           . showsPrec paren p1+                           . showString ">> "+                           . showsPrec 0 p2)++instance (Alpha p1, Alpha p2) => Alpha (Rebind p1 p2) where+  isTerm _ = False++  isPat (Rebnd p1 p2) = isPat p1 <> isPat p2++  swaps' ctx perm (Rebnd p1 p2) =+    Rebnd (swaps' ctx perm p1) (swaps' (incrLevelCtx ctx) perm p2)++  freshen' ctx (Rebnd p1 p2) =+    if isTermCtx ctx+    then error "freshen' on Rebind in Term mode"+    else do+      (p1', perm1) <- freshen' ctx p1+      (p2', perm2) <- freshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) perm1 p2)+      return (Rebnd p1' p2', perm1 <> perm2)++  lfreshen' ctx (Rebnd p q) cont =+    if isTermCtx ctx+    then error "lfreshen' on Rebind in Term mode"+    else+      lfreshen' ctx p $ \ p' pm1 ->+      lfreshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) pm1 q) $ \ q' pm2 ->+      cont (Rebnd p' q') (pm1 <> pm2)+++  aeq' ctx (Rebnd p1 p2) (Rebnd q1 q2) =+    -- XXX TODO: Unbound had (aeq' ctx p2 q2) here.  But that doesn't seem right.+    aeq' ctx p1 q1 && aeq' (incrLevelCtx ctx) p2 q2++  fvAny' ctx afa (Rebnd p1 p2) = Rebnd <$> fvAny' ctx afa p1+                                       <*> fvAny' (incrLevelCtx ctx) afa p2++  open ctx b (Rebnd p1 p2) = Rebnd (open ctx b p1) (open (incrLevelCtx ctx) b p2)+  close ctx b (Rebnd p1 p2) = Rebnd (close ctx b p1) (close (incrLevelCtx ctx) b p2)
+ src/Unbound/Generics/LocallyNameless/Subst.hs view
@@ -0,0 +1,177 @@+-- |+-- Module     : Unbound.Generics.LocallyNameless.Subst+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- A typeclass for types that may participate in capture-avoiding substitution+--+-- The minimal definition is empty, provided your type is an instance of 'GHC.Generics.Generic'+-- +-- @+-- type Var = Name Factor+-- data Expr = SumOf [Summand]+--           deriving (Show, Generic)+-- data Summand = ProductOf [Factor]+--           deriving (Show, Generic)+-- instance Subst Var Expr+-- instance Subst Var Summand+-- @+-- +-- The default instance just propagates the substitution into the constituent factors.+-- +-- If you identify the variable occurrences by implementing the 'isvar' function, the derived 'subst' function+-- will be able to substitute a factor for a variable.+-- +-- @+-- data Factor = V Var+--             | C Int+--             | Subexpr Expr+--           deriving (Show, Generic)+-- instance Subst Var Factor where+--   isvar (V v) = Just (SubstName v)+--   isvar _     = Nothing+-- @+--+{-# LANGUAGE DefaultSignatures+             , FlexibleContexts+             , FlexibleInstances+             , GADTs+             , MultiParamTypeClasses+             , ScopedTypeVariables+             , TypeOperators+ #-}+module Unbound.Generics.LocallyNameless.Subst (+  SubstName(..)+  , SubstCoerce(..)+  , Subst(..)+  ) where++import GHC.Generics++import Data.List (find)++import Unbound.Generics.LocallyNameless.Name+import Unbound.Generics.LocallyNameless.Alpha+import Unbound.Generics.LocallyNameless.Embed+import Unbound.Generics.LocallyNameless.Bind+import Unbound.Generics.LocallyNameless.Rebind++-- | See 'isVar'+data SubstName a b where+  SubstName :: (a ~ b) => Name a -> SubstName a b++-- | See 'isCoerceVar'  +data SubstCoerce a b where  +  SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b++-- | Instances of @'Subst' b a@ are terms of type @a@ that may contain+-- variables of type @b@ that may participate in capture-avoiding+-- substitution.+class Subst b a where+  -- | This is the only method that must be implemented+  isvar :: a -> Maybe (SubstName a b)+  isvar _ = Nothing++  -- | This is an alternative version to 'isvar', useable in the case +  --   that the substituted argument doesn't have *exactly* the same type+  --   as the term it should be substituted into.+  --   The default implementation always returns 'Nothing'.+  isCoerceVar :: a -> Maybe (SubstCoerce a b)+  isCoerceVar _ = Nothing++  -- | @'subst' nm e tm@ substitutes @e@ for @nm@ in @tm@.  It has+  -- a default generic implementation in terms of @isvar@+  subst :: Name b -> b -> a -> a+  default subst :: (Generic a, GSubst b (Rep a)) => Name b -> b -> a -> a+  subst n u x =+    if (isFreeName n)+    then case (isvar x :: Maybe (SubstName a b)) of+      Just (SubstName m) -> if m == n then u else x+      Nothing -> case (isCoerceVar x :: Maybe (SubstCoerce a b)) of+        Just (SubstCoerce m f) -> if m == n then maybe x id (f u) else x+        Nothing -> to $ gsubst n u (from x)+    else error $ "Cannot substitute for bound variable " ++ show n++  substs :: [(Name b, b)] -> a -> a+  default substs :: (Generic a, GSubst b (Rep a)) => [(Name b, b)] -> a -> a+  substs ss x+    | all (isFreeName . fst) ss =+      case (isvar x :: Maybe (SubstName a b)) of+        Just (SubstName m) ->+          case find ((==m) . fst) ss of+            Just (_, u) -> u+            Nothing     -> x+        Nothing -> case isCoerceVar x :: Maybe (SubstCoerce a b) of +            Just (SubstCoerce m f) ->+              case find ((==m) . fst) ss of +                  Just (_, u) -> maybe x id (f u)+                  Nothing -> x+            Nothing -> to $ gsubsts ss (from x)+    | otherwise =+      error $ "Cannot substitute for bound variable in: " ++ show (map fst ss)++---- generic structural substitution.++class GSubst b f where+  gsubst :: Name b -> b -> f c -> f c+  gsubsts :: [(Name b, b)] -> f c -> f c++instance Subst b c => GSubst b (K1 i c) where+  gsubst nm val = K1 . subst nm val . unK1+  gsubsts ss = K1 . substs ss . unK1++instance GSubst b f => GSubst b (M1 i c f) where+  gsubst nm val = M1 . gsubst nm val . unM1+  gsubsts ss = M1 . gsubsts ss . unM1++instance GSubst b U1 where+  gsubst _nm _val _ = U1+  gsubsts _ss _ = U1++instance GSubst b V1 where+  gsubst _nm _val = id+  gsubsts _ss = id++instance (GSubst b f, GSubst b g) => GSubst b (f :*: g) where+  gsubst nm val (f :*: g) = gsubst nm val f :*: gsubst nm val g+  gsubsts ss (f :*: g) = gsubsts ss f :*: gsubsts ss g++instance (GSubst b f, GSubst b g) => GSubst b (f :+: g) where+  gsubst nm val (L1 f) = L1 $ gsubst nm val f+  gsubst nm val (R1 g) = R1 $ gsubst nm val g++  gsubsts ss (L1 f) = L1 $ gsubsts ss f+  gsubsts ss (R1 g) = R1 $ gsubsts ss g++-- these have a Generic instance, but+-- it's self-refential (ie: Rep Int = D1 (C1 (S1 (Rec0 Int))))+-- so our structural GSubst instances get stuck in an infinite loop.+instance Subst b Int where subst _ _ = id ; substs _ = id+instance Subst b Bool where subst _ _ = id ; substs _ = id+instance Subst b () where subst _ _ = id ; substs _ = id+instance Subst b Char where subst _ _ = id ; substs _ = id+instance Subst b Float where subst _ _ = id ; substs _ = id+instance Subst b Double where subst _ _ = id ; substs _ = id++-- huh, apparently there's no instance Generic Integer. +instance Subst b Integer where subst _ _ = id ; substs _ = id++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 Generic a => Subst b (Name a) where subst _ _ = id ; substs _ = id+instance Subst b AnyName where subst _ _ = id ; substs _ = id++instance (Subst c a) => Subst c (Embed a)++instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)++instance (Subst c p1, Subst c p2) => Subst c (Rebind p1 p2)
+ src/Unbound/Generics/LocallyNameless/Unsafe.hs view
@@ -0,0 +1,24 @@+{-# OPTIONS_HADDOCK show-extensions #-}+-- |+-- Module     : Unbound.Generics.LocallyNameless.Unsafe+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- Dangerous operations that may disturb the invariants of+-- "Unbind.Generics.LocallyNameless" or of your AST.+{-# LANGUAGE DeriveGeneric #-}+module Unbound.Generics.LocallyNameless.Unsafe+       (+         unsafeUnbind+       ) where++import Unbound.Generics.LocallyNameless.Alpha+import Unbound.Generics.LocallyNameless.Bind++-- | 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)+
+ src/Unbound/Generics/PermM.hs view
@@ -0,0 +1,165 @@+----------------------------------------------------------------------+-- |+-- Module      :  Unbound.Generics.PermM+-- Copyright   :  (c) 2011, Stephanie Weirich <sweirich@cis.upenn.edu>+-- License     :  BSD-like (see PermM.hs)+-- Maintainer  :  Aleksey Kliger+-- Portability :  portable+--+-- A slow, but hopefully correct implementation of permutations.+--+----------------------------------------------------------------------+{-+Copyright (c)2011, Stephanie Weirich++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Stephanie Weirich nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+-}+{-# LANGUAGE PatternGuards #-}+module Unbound.Generics.PermM (+    Perm(..), permValid, single, compose, apply, support, isid, join, empty, restrict, mkPerm+  ) where++import Prelude (Eq(..), Show(..), (.), ($), Monad(return), Ord(..), Maybe(..), otherwise, (&&), Bool(..), id, uncurry, Functor(..))+import Data.Monoid+import Data.List+import Data.Map (Map)+import qualified Data.Map as M+import qualified Data.Set as S+import Control.Arrow ((&&&))+import Control.Monad ((>=>))++-- | A /permutation/ is a bijective function from names to names+--   which is the identity on all but a finite set of names.  They+--   form the basis for nominal approaches to binding, but can+--   also be useful in general.+newtype Perm a = Perm (Map a a)++-- | @'permValid' p@ returns @True@ iff the perumation is /valid/: if+-- each value in the range of the permutation is also a key.+permValid :: Ord a => Perm a -> Bool+permValid (Perm p) = all (\(_,v) -> M.member v p) (M.assocs p)+  -- a Map sends every key uniquely to a value by construction.  So if+  -- every value is also a key, the sizes of the domain and range must+  -- be equal and hence the mapping is a bijection.++instance Ord a => Eq (Perm a) where+  (Perm p1) == (Perm p2) =+    all (\x -> M.findWithDefault x x p1 == M.findWithDefault x x p2) (M.keys p1) &&+    all (\x -> M.findWithDefault x x p1 == M.findWithDefault x x p2) (M.keys p2)++instance Show a => Show (Perm a) where+  show (Perm p) = show p++-- | Apply a permutation to an element of the domain.+apply :: Ord a => Perm a -> a -> a+apply (Perm p) x = M.findWithDefault x x p++-- | Create a permutation which swaps two elements.+single :: Ord a => a -> a -> Perm a+single x y = if x == y then Perm M.empty else+    Perm (M.insert x y (M.insert y x M.empty))++-- | The empty (identity) permutation.+empty :: Perm a+empty = Perm M.empty++-- | Compose two permutations.  The right-hand permutation will be+--   applied first.+compose :: Ord a => Perm a -> Perm a -> Perm a+compose (Perm b) (Perm a) =+  Perm (M.fromList ([ (x,M.findWithDefault y y b) | (x,y) <- M.toList a]+         ++ [ (x, M.findWithDefault x x b) | x <- M.keys b, M.notMember x a]))++-- | Permutations form a monoid under composition.+instance Ord a => Monoid (Perm a) where+  mempty  = empty+  mappend = compose++-- | Is this the identity permutation?+isid :: Ord a => Perm a -> Bool+isid (Perm p) =+     M.foldrWithKey (\ a b r -> r && a == b) True p++-- | /Join/ two permutations by taking the union of their relation+--   graphs. Fail if they are inconsistent, i.e. map the same element+--   to two different elements.+join :: Ord a => Perm a -> Perm a -> Maybe (Perm a)+join (Perm p1) (Perm p2) =+     let overlap = M.intersectionWith (==) p1 p2 in+     if M.fold (&&) True overlap then+       Just (Perm (M.union p1 p2))+       else Nothing++-- | The /support/ of a permutation is the set of elements which are+--   not fixed.+support :: Ord a => Perm a -> [a]+support (Perm p) = [ x | x <- M.keys p, M.findWithDefault x x p /= x]++-- | Restrict a permutation to a certain domain.+restrict :: Ord a => Perm a -> [a] -> Perm a+restrict (Perm p) l = Perm (foldl' (\p' k -> M.delete k p') p l)++-- | A partial permutation consists of two maps, one in each direction+--   (inputs -> outputs and outputs -> inputs).+data PartialPerm a = PP (M.Map a a) (M.Map a a)+  deriving Show++emptyPP :: PartialPerm a+emptyPP = PP M.empty M.empty++extendPP :: Ord a => a -> a -> PartialPerm a -> Maybe (PartialPerm a)+extendPP x y pp@(PP mfwd mrev)+  | Just y' <- M.lookup x mfwd = if y == y' then Just pp+                                            else Nothing+  | Just x' <- M.lookup y mrev = if x == x' then Just pp+                                            else Nothing+  | otherwise = Just $ PP (M.insert x y mfwd) (M.insert y x mrev)++-- | Convert a partial permutation into a full permutation by closing+--   off any remaining open chains into a cycles.+ppToPerm :: Ord a => PartialPerm a -> Perm a+ppToPerm (PP mfwd mrev) = Perm $ foldr (uncurry M.insert) mfwd+                                       (map (findEnd &&& id) chainStarts)+        -- beginnings of open chains are elements which map to+        -- something in the forward direction but have no ancestor.+  where chainStarts = S.toList (M.keysSet mfwd `S.difference` M.keysSet mrev)+        findEnd x = case M.lookup x mfwd of+                      Nothing -> x+                      Just x' -> findEnd x'++-- | @mkPerm l1 l2@ creates a permutation that sends @l1@ to @l2@.+--   Fail if there is no such permutation, either because the lists+--   have different lengths or because they are inconsistent (which+--   can only happen if @l1@ or @l2@ have repeated elements).+mkPerm :: Ord a => [a] -> [a] -> Maybe (Perm a)+mkPerm xs ys+  | length xs /= length ys = Nothing+  | otherwise =+    fmap ppToPerm . ($emptyPP) . foldr (>=>) return $ zipWith extendPP xs ys
+ test/Calc.hs view
@@ -0,0 +1,165 @@+-- |+-- Module     : Calc+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}+module Calc where++import Control.Arrow (second)+import Data.Typeable (Typeable)+import GHC.Generics (Generic)++import Unbound.Generics.LocallyNameless+import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf)++-- variables will range over expressions+type Var = Name Expr++-- expression is either a variable, a constant int, a summation of two+-- expressions, a list of variables bound to expressions that may+-- occur in the body of an expression (where the expressions in the+-- list of bindings refer to an outer scope), or a sequence of nested bindings+-- where each binding expression can refer to previously bound variables.+data Expr = V Var+          | C Int+          | Add Expr Expr+          | Let (Bind [(Var, Embed Expr)] Expr)+          | LetStar (Bind LetStarBinds Expr)+          deriving (Generic, Typeable, Show)++data LetStarBinds = EmptyLSB+                  | ConsLSB (Rebind (Var, Embed Expr) LetStarBinds)+                  deriving (Generic, Typeable, Show)++instance Alpha Expr+instance Alpha LetStarBinds++mkVar :: String -> Var+mkVar = s2n++anyFreeVarList :: Alpha a => a -> [AnyName]+anyFreeVarList = toListOf fvAny++freeVarList :: (Alpha a, Typeable b) => a -> [Name b]+freeVarList = toListOf fv++-- smart constructor for Let+mkLet :: [(Var, Expr)] -> Expr -> Expr+mkLet binds body = Let (bind (map (second Embed) binds) body)++-- smart constructor for Let*+mkLetStar :: [(Var, Expr)] -> Expr -> Expr+mkLetStar binds body = LetStar (bind (mkLsb binds) body)+  where+    mkLsb [] = EmptyLSB+    mkLsb ((v,e):rest) = ConsLSB (rebind (v, Embed e) (mkLsb rest))++-- environments are partial maps from (free) variables to expressions.+type Env = Var -> Maybe Expr++emptyEnv :: Env+emptyEnv = const Nothing++extendEnv :: Var -> Expr -> Env -> Env+extendEnv v e rho w =+  if v == w then Just e else rho w++whnf :: (Fresh m) => Env -> Expr -> m Expr+whnf rho (V v) = case rho v of+  Just e -> return e+  Nothing -> fail $ "unbound variable " ++ show v+whnf _rho (C i) = return (C i)+whnf rho (Add e1 e2) = do+  v1 <- whnf rho e1+  v2 <- whnf rho e2+  add v1 v2+  where add :: Monad m => Expr -> Expr -> m Expr+        add (C i1) (C i2) = return (C $ i1 + i2)+        add _ _ = fail "add of two non-integers"+whnf rho0 (Let b) = do+  (binds, body) <- unbind b+  binds' <- mapM (\(v, Embed e) -> do+                     e' <- whnf rho0 e+                     return (v, e')) binds+  let rho' = foldl (\rho (v,e) -> extendEnv v e rho) rho0 binds'+  whnf rho' body+whnf rho0 (LetStar b) = do+  (lsb, body) <- unbind b+  rho' <- whnfLsb lsb rho0+  whnf rho' body++whnfLsb :: Fresh m => LetStarBinds -> Env -> m Env+whnfLsb EmptyLSB = return+whnfLsb (ConsLSB rbnd) = \rho -> do+  let ((v, Embed e), lsb) = unrebind rbnd+  e' <- whnf rho e+  whnfLsb lsb (extendEnv v e' rho)++runWhnf :: Env -> Expr -> Maybe Expr+runWhnf rho e = runFreshMT (whnf rho e)++ex1 :: Expr+ex1 = Add (C 1) (C 2)++ex2x :: Expr+ex2x = V (mkVar "x")++ex2y :: Expr+ex2y = V (mkVar "y")++ex2xc :: Expr+ex2xc = close initialCtx (mkVar "x") ex2x++ex2yc :: Expr+ex2yc = close initialCtx (mkVar "y") ex2y++ex3x :: Expr+ex3x = let x = mkVar "x"+       in mkLet [(x, (C 1))] $ Add (V x) (C 2)++ex3y :: Expr+ex3y = let y = mkVar "y"+       in mkLet [(y, (C 1))] $ Add (V y) (C 2)++ex4 :: Expr+ex4 = let+  x = mkVar "x"+  y = mkVar "y"+  in+   mkLet [(y, (C 5))]+   $ mkLet [(y, (C 200))+           , (x, (Add (V y) -- refers to the outer y+                  (C 6)))]+   $ Add (V x) (V x) -- expect (C 22), not (C 412)++ex4_ans :: Expr+ex4_ans = C 22+   +ex5 :: Expr+ex5 = let+  x = mkVar "x"+  y = mkVar "y"+  in+   mkLet [(y, (C 5))]+   $ mkLetStar [(y, (C 200))+               , (x, (Add (V y) -- refers to the inner y+                      (C 6)))]+   $ Add (V x) (V x) -- expect (C 412), not (C 22)++ex5_ans :: Expr+ex5_ans = C 412++ex6 :: [Expr]+ex6 = [V (mkVar "x"), V (mkVar "z"), mkLet [(mkVar "y", C 1)] (V (mkVar "y"))]++ex6_ans :: [AnyName]+ex6_ans = [AnyName (mkVar "x"), AnyName (mkVar "z")]++ex7 :: [Expr]+ex7 = [V (mkVar "x"), V (mkVar "z"), mkLet [(mkVar "y", C 1)] (V (mkVar "y"))]++ex7_ans :: [Var]+ex7_ans = [mkVar "x", mkVar "z"]
+ test/ParallelReduction.hs view
@@ -0,0 +1,92 @@+--+-- We implement the parallel reduction relation e ⇛ e'+-- that is a key to some kinds of confluence proofs for lambda calculi.+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable, MultiParamTypeClasses #-}+module ParallelReduction where++import Control.Applicative +import Control.Monad.Identity+import GHC.Generics (Generic)+import Data.Typeable (Typeable)++import Unbound.Generics.LocallyNameless++type Var = Name Expr++-- in this case we just have an untyped lambda calculus+data Expr = V Var+          | Lam (Bind Var Expr)+          | App Expr Expr+          deriving (Show, Generic, Typeable)++instance Alpha Expr++instance Subst Expr Expr where+  isvar (V n) = Just (SubstName n)+  isvar _     = Nothing++run :: FreshMT Identity Expr -> Expr+run = runIdentity . runFreshMT++-- parallel reduction is the compatible closure of cbn beta : (λx.e)f ⇛ {f'/x}e' where e⇛e' and f⇛f'+-- we choose to allow reduction under a lambda.+parStep :: (Applicative m, Fresh m) => Expr -> m Expr+parStep v@(V _) = return v+parStep (App e1 e2) =+  case e1 of+    Lam b -> betaStep e2 b+    _ -> App <$> parStep e1 <*> parStep e2+parStep (Lam b) = do+  (v, e) <- unbind b+  (Lam . (bind v)) <$> parStep e++betaStep :: (Applicative m, Fresh m) => Expr -> Bind Var Expr -> m Expr+betaStep f b = do+  f' <- parStep f+  (v, e) <- unbind b+  e' <- parStep e+  return (subst v f' e')++-- repeatedly take parStep steps until the term doesn't change anymore.+parSteps :: (Applicative m, Fresh m) => Expr -> m Expr+parSteps e = do+  e' <- parStep e+  if (e `aeq` e')+    then return e+    else parSteps e'++ex1 :: Bind Var Expr+ex1 = let+  x = s2n "x"+  in bind x (V x)+ex1' :: (Var, Expr)+ex1' = let+  y = s2n "y"+  in+   (y, V y)++ex2 :: Expr+ex2 = App (Lam ex2_1) ex2_2++ex2_1 :: Bind Var Expr+ex2_1 = let+  x = s2n "x"+  y = s2n "y"+  in+   bind x $ Lam $ bind y $ App (V x) (V y)++ex2_2 :: Expr+ex2_2 = let+  z = s2n "z"+  in+   (Lam $ bind z $ V z)++ident :: Expr+ident = let+  u = s2n "u"+  in Lam $ bind u $ V u++-- same as ex2 but with some extra beta redices in both halves of the application+ex2_alt :: Expr+ex2_alt = App (App ident (Lam ex2_1)) (App (App ident ident) ex2_2)+
+ test/test-calc.hs view
@@ -0,0 +1,55 @@+-- |+-- Module     : test-stlc+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}+module Main where++import Unbound.Generics.LocallyNameless++import Calc++import Test.HUnit++test_ex1 :: Test+test_ex1 = TestCase $ assertBool "example 1" (runWhnf emptyEnv ex1 `aeq` (Just $ C 3))++test_ex2_open :: Test+test_ex2_open = TestCase $ assertBool "example 2 (open)" (not $ aeq ex2x ex2y)++test_ex2_closed :: Test+test_ex2_closed = TestCase $ assertBool "example 2 (closed)" (aeq ex2xc ex2yc)++test_ex3 :: Test+test_ex3 = TestCase $ assertBool "example 3" (aeq ex3x ex3y)++test_ex4 :: Test+test_ex4 = TestCase $ assertBool "example 4 (let scoping)" (runWhnf emptyEnv ex4 `aeq` Just ex4_ans)++test_ex5 :: Test+test_ex5 = TestCase $ assertBool "example 5 (let* scoping)" (runWhnf emptyEnv ex5 `aeq` Just ex5_ans)++test_ex6 :: Test+test_ex6 = TestCase $ assertBool "example 6 (free variables)" (anyFreeVarList ex6 `aeq` ex6_ans)++test_ex7 :: Test+test_ex7 = TestCase $ assertBool "example 7 (sorted free variables)" (freeVarList ex7 `aeq` ex7_ans)+++main :: IO ()+main = do+  result <- runTestTT $ TestList [test_ex1+                                 , test_ex2_open+                                 , test_ex2_closed+                                 , test_ex3+                                 , test_ex4+                                 , test_ex5+                                 , test_ex6+                                 , test_ex7+                            ]+  if failures result > 0+    then fail "Some tests failed!"+    else return ()
+ test/test-parallelreduction.hs view
@@ -0,0 +1,25 @@+module Main where++import Test.HUnit++import Unbound.Generics.LocallyNameless (subst, aeq)++import ParallelReduction+++++test_ex1 :: Test+test_ex1 = TestCase $ assertBool "simple substitution" (subst (fst ex1') (Lam ex1) (snd ex1') `aeq` (Lam ex1))++test_ex2 :: Test+test_ex2 = TestCase $ assertBool "parallel reduction" (run (parSteps ex2) `aeq` run (parSteps ex2_alt))++main :: IO ()+main = do+  result <- runTestTT $ TestList [test_ex1+                                 , test_ex2+                                 ]+  if failures result > 0+    then fail "Some tests failed!"+    else return ()
+ unbound-generics.cabal view
@@ -0,0 +1,83 @@+-- Initial unbound-generics.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++name:                unbound-generics+version:             0.0.0.90+synopsis:            Reimplementation of Unbound 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+                     alpha-equivalence, free variable calculation,+                     capture-avoiding substitution, and more. See+                     @Unbound.Generics.LocallyNameless@ to get started.+                     .+                     This is an independent re-implementation of <http://hackage.haskell.org/package/unbound Unbound>+                     but using <http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.7.0.1/GHC-Generics.html GHC.Generics>+                     instead of <http://http://hackage.haskell.org/package/RepLib RepLib>.+                     See the accompanying README for some porting notes.+                     +homepage:            http://github.com/lambdageek/unbound-generics+bug-reports:         http://github.com/lambdageek/unbound-generics/issues+license:             BSD3+license-file:        LICENSE+author:              Aleksey Kliger+maintainer:          aleksey@lambdageek.org+copyright:           (c) 2014, Aleksey Kliger+category:            Language+build-type:          Simple+extra-source-files:  examples/*.hs,+                     README.md,+                     Changelog.md+cabal-version:       >=1.10++library+  exposed-modules:     Unbound.Generics.LocallyNameless+                       Unbound.Generics.LocallyNameless.Name+                       Unbound.Generics.LocallyNameless.Fresh+                       Unbound.Generics.LocallyNameless.LFresh+                       Unbound.Generics.LocallyNameless.Alpha+                       Unbound.Generics.LocallyNameless.Bind+                       Unbound.Generics.LocallyNameless.Rebind+                       Unbound.Generics.LocallyNameless.Embed+                       Unbound.Generics.LocallyNameless.Operations+                       Unbound.Generics.LocallyNameless.Unsafe+                       Unbound.Generics.LocallyNameless.Internal.Fold+                       Unbound.Generics.PermM+                       Unbound.Generics.LocallyNameless.Subst+  -- other-modules:       +  -- other-extensions:    +  build-depends:       base >=4.6 && <5,+                       mtl >= 2.1,+                       transformers >= 0.3,+                       containers == 0.5.*,+                       contravariant >= 0.5+  hs-source-dirs:      src+  default-language:    Haskell2010+  ghc-options:         -Wall++Test-Suite test-calc+  type:                exitcode-stdio-1.0+  main-is:             test-calc.hs+  other-modules:       Calc+  build-depends:       base,+                       HUnit == 1.2.*,+                       unbound-generics+  hs-source-dirs:      test+  default-language:    Haskell2010+  ghc-options:         -Wall++Test-Suite test-parallelreduction+  type:                exitcode-stdio-1.0+  main-is:             test-parallelreduction.hs+  other-modules:       ParallelReduction+  build-depends:       base,+                       HUnit == 1.2.*,+                       mtl >= 2.1,+                       unbound-generics+  hs-source-dirs:      test+  default-language:    Haskell2010+  ghc-options:         -Wall++source-repository head+  type:                git+  location:            git://github.com/lambdageek/unbound-generics.git