bound 0.4 → 0.5

raw patch · 12 files changed

+481/−99 lines, 12 filesdep +comonaddep +directorydep +doctestdep ~basedep ~bifunctorsdep ~prelude-extrasPVP ok

version bump matches the API change (PVP)

Dependencies added: comonad, directory, doctest, filepath, ghc-prim, vector

Dependency ranges changed: base, bifunctors, prelude-extras, transformers

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +7/−0
• bound.cabal +51/−13
• examples/Deriving.hs +21/−21
• examples/Overkill.hs +12/−10
• examples/Simple.hs +2/−2
• src/Bound.hs +44/−24
• src/Bound/Class.hs +16/−4
• src/Bound/Name.hs +162/−0
• src/Bound/Scope.hs +65/−19
• src/Bound/Term.hs +28/−1
• src/Bound/Var.hs +41/−5
• tests/doctests.hs +32/−0

@@ -0,0 +1,7 @@+0.5+-----+* Created a `doctest`-based test suite+* Added many examples+* 100% haddock coverage+* Added the `Name` `Comonad`, to help retain names for bound variables.+* Bumped dependencies

@@ -1,6 +1,6 @@ name:          bound category:      Language, Compilers/Interpreters-version:       0.4+version:       0.5 license:       BSD3 cabal-version: >= 1.9.2 license-file:  LICENSE@@ -21,6 +21,10 @@    An untyped lambda calculus:    .    > import Bound+   > import Control.Applicative+   > import Control.Monad (ap)+   > import Data.Foldable+   > import Data.Traversable    > import Prelude.Extras    .    > infixl 9 :@@@ -98,7 +102,9 @@   examples/Simple.hs   examples/Deriving.hs   examples/Overkill.hs+  tests/doctests.hs   README.markdown+  CHANGELOG.markdown  source-repository head   type: git@@ -106,27 +112,59 @@  library   hs-source-dirs: src-  build-depends:-    base           >= 4     && < 5,-    bifunctors     >= 0.1.3 && < 0.2,-    prelude-extras >= 0.2   && < 0.3,-    transformers   >= 0.2   && < 0.4    exposed-modules:     Bound     Bound.Class+    Bound.Name     Bound.Scope     Bound.Term     Bound.Var -  ghc-options: -Wall -O2 -fspec-constr -fdicts-cheap+  build-depends:+    base           >= 4   && < 5,+    bifunctors     == 3.0.*,+    comonad        == 3.0.*,+    prelude-extras >= 0.2 && < 0.3,+    transformers   >= 0.2 && < 0.4 +  ghc-options: -Wall -O2 -fspec-constr -fdicts-cheap -funbox-strict-fields+  if impl(ghc>=7.4)+    build-depends: ghc-prim++-- Stating these, despite being more correct, causes spurious warnings to+-- end-users of older Cabal versions, so we don't.++--  other-extensions: CPP+--  if impl(ghc)+--    other-extensions: DeriveDataTypeable+--  if impl(ghc>=7.4)+--    other-extensions: DeriveGeneric DefaultSignatures+ test-suite Simple-  build-depends:-    base           >= 4     && < 5,-    prelude-extras >= 0.2   && < 0.3,-    transformers   >= 0.2   && < 0.4,-    bound   type: exitcode-stdio-1.0-  hs-source-dirs: examples   main-is: Simple.hs+  hs-source-dirs: examples+  ghc-options -Wall -threaded+  if impl(ghc<7.6.1)+    ghc-options: -Werror+  build-depends:+    base,+    bound,+    prelude-extras,+    transformers++-- Verify the results of the examples+test-suite doctests+  type:    exitcode-stdio-1.0+  main-is: doctests.hs+  hs-source-dirs: tests+  ghc-options: -Wall -threaded+  if impl(ghc<7.6.1)+    ghc-options: -Werror+  build-depends:+    base,+    directory >= 1.0 && < 1.3,+    doctest   >= 0.9 && < 0.10,+    filepath,+    vector    == 0.9.*

@@ -1,5 +1,5 @@ {-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}-module Exp where+module Deriving where  import Data.List import Data.Foldable@@ -61,6 +61,9 @@  data P a = P { pattern :: [a] -> Pat Exp a, bindings :: [a] } +-- |+-- >>> lam (varp "x") (V "x")+-- Lam 1 VarP (Scope (V (B 0))) varp :: a -> P a varp a = P (const VarP) [a] @@ -70,6 +73,9 @@ asp :: a -> P a -> P a asp a (P p as) = P (\bs -> AsP (p (a:bs))) (a:as) +-- |+-- >>> lam (conp "Hello" [varp "x", wildp]) (V "y")+-- Lam 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V "y")))) conp :: String -> [P a] -> P a conp g ps = P (ConP g . go ps) (ps >>= bindings)   where@@ -81,6 +87,15 @@ viewp t (P p as) = P (\bs -> ViewP (abstract (`elemIndex` bs) t) (p bs)) as  -- | smart lam constructor+--+-- >>> let_ [("x",V "y"),("y",V "x" :@ V "y")] $ lam (varp "z") (V "z" :@ V "y")+-- Let 2 [Scope (V (B 1)),Scope (V (B 0) :@ V (B 1))] (Scope (Lam 1 VarP (Scope (V (B 0) :@ V (F (V (B 1)))))))+--+-- >>> lam (conp "F" [varp "x", viewp (V "x") $ varp "y"]) (V "y")+-- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (B 0))) VarP]) (Scope (V (B 1)))+--+-- >>> lam (conp "F" [varp "x", viewp (V "y") $ varp "y"]) (V "y")+-- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (F (V "y")))) VarP]) (Scope (V (B 1))) lam :: Eq a => P a -> Exp a -> Exp a lam (P p as) t = Lam (length as) (p []) (abstract (`elemIndex` as) t) @@ -91,26 +106,11 @@         abstr = abstract (`elemIndex` vs)  -- | smart alt constructor-alt :: Eq a => P a -> Exp a -> Alt Exp a-alt (P p as) t = Alt (length as) (p []) (abstract (`elemIndex` as) t)---- >>> let_ [("x",V "y"),("y",V "x" :@ V "y")] $ lam (varp "z") (V "z" :@ V "y")--- Let 2 [Scope (V (B 1)),Scope (V (B 0) :@ V (B 1))] (Scope (Lam 1 VarP (Scope (V (B 0) :@ V (F (V (B 1)))))))---- >>> lam (varp "x") (V "x")--- Lam 1 VarP (Scope (V (B 0)))---- >>> lam (conp "Hello" [varp "x", wildp]) (V "y")--- Lam 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V "y"))))-+-- -- >>> lam (varp "x") $ Case (V "x") [alt (conp "Hello" [varp "z",wildp]) (V "x"), alt (varp "y") (V "y")] -- Lam 1 VarP (Scope (Case (V (B 0)) [Alt 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V (B 0))))),Alt 1 VarP (Scope (V (B 0)))]))---- view patterns can reference name from earlier in the same scope--- >>> lam (conp "F" [varp "x", viewp (V "x") $ varp "y"]) (V "y")--- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (B 0))) VarP]) (Scope (V (B 1)))---- but like in ghc, they refuse to allow references to subsequent bindings in the scope--- >>> lam (conp "F" [varp "x", viewp (V "y") $ varp "y"]) (V "y")--- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (F (V "y")))) VarP]) (Scope (V (B 1)))+alt :: Eq a => P a -> Exp a -> Alt Exp a+alt (P p as) t = Alt (length as) (p []) (abstract (`elemIndex` as) t) +main :: IO ()+main = return ()

@@ -9,7 +9,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE TypeOperators #-}-module Exp where+module Overkill where  import Data.Vector as Vector hiding ((++), map) import Data.List as List@@ -189,8 +189,6 @@   ViewP e p >>>= f = ViewP (e >>= f) (p >>>= f)  -- ** Pats-- eqPats :: (Eq1 f, Eq a) => Pats bs f a -> Pats bs' f a -> Bool eqPats NilP      NilP      = True eqPats (p :> ps) (q :> qs) = eqPat p q && eqPats ps qs@@ -221,9 +219,7 @@   NilP >>>= _ = NilP   (p :> ps) >>>= f = (p >>>= f) :> (ps >>>= f) - -- ** Path into Pats- eqMPath :: MPath is -> MPath js -> Bool eqMPath (H m) (H n) = eqPath m n eqMPath (T p) (T q) = eqMPath p q@@ -244,8 +240,6 @@ -- instance Read (MPath is)  -- ** Path into Pat-- eqPath :: Path i -> Path j -> Bool eqPath V     V     = True eqPath L     L     = True@@ -282,6 +276,14 @@   showsPrec d (R m) = showParen (d > 10) $ showString "R " . showsPrec 11 m   showsPrec d (C p) = showParen (d > 10) $ showString "C " . showsPrec 11 p --- ghci> let_ [("x",Var "y"),("y",Var "x" :@ Var "y")] $ lam (varp "z") (Var "z" :@ Var "y")--- ghci> lam (varp "x") (Var "x")--- ghci> lam (conp "Hello" [varp "x", wildp])) (Var "y")+-- |+-- >>> let_ [("x",Var "y"),("y",Var "x" :@ Var "y")] $ lam (varp "z") (Var "z" :@ Var "y")+-- Let (fromList [Scope (Var (B 1)),Scope (Var (B 0) :@ Var (B 1))]) (Scope (Lam VarP (Scope (Var (B V) :@ Var (F (Var (B 1)))))))+--+-- >>> lam (varp "x") (Var "x")+-- Lam VarP (Scope (Var (B V)))+--+-- >>> lam (conp "Hello" [varp "x", wildp]) (Var "y")+-- Lam (ConP "Hello" (VarP :> WildP :> NilP)) (Scope (Var (F (Var "y"))))+main :: IO ()+main = return ()

@@ -27,7 +27,7 @@ -- | A smart constructor for Lam -- -- >>> lam "y" (lam "x" (V "x" :@ V "y"))--- Lam (Lam (V (B ()) :@ V (F (V (B ())))))+-- Lam (Scope (Lam (Scope (V (B ()) :@ V (F (V (B ()))))))) lam :: Eq a => a -> Exp a -> Exp a lam v b = Lam (abstract1 v b) @@ -95,7 +95,7 @@ -- -- Modified to use recursive let, because we can. ----- >>> nf cooked == lam "false" (lam "true" (V"false"))+-- >>> nf cooked == true -- True  true :: Exp String

@@ -9,44 +9,64 @@ -- Portability :  portable -- -- We represent the target language itself as an ideal monad supplied by the--- user, and provide a 'Scope' monad transformer for introducing bound +-- user, and provide a 'Scope' monad transformer for introducing bound -- variables in user supplied terms. Users supply a 'Monad' and 'Traversable' -- instance, and we traverse to find free variables, and use the 'Monad' to -- perform substitution that avoids bound variables. -- -- An untyped lambda calculus: ----- > import Bound--- > import Prelude.Extras+-- @+-- {-\# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable \#-}+-- import Bound+-- import Control.Applicative+-- import Control.Monad ('Control.Monad.ap')+-- import Prelude.Extras+-- import Data.Foldable+-- import Data.Traverable+-- @ ----- > infixl 9 :@--- > data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)--- >  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)+-- @+-- infixl 9 :\@+-- data Exp a = V a | Exp a :\@ Exp a | Lam ('Scope' () Exp a)+--   deriving ('Eq','Ord','Show','Read','Functor','Data.Foldable.Foldable','Data.Foldable.Traversable')+-- @ ----- > instance Eq1 Exp   where (==#)      = (==)--- > instance Ord1 Exp  where compare1   = compare--- > instance Show1 Exp where showsPrec1 = showsPrec--- > instance Read1 Exp where readsPrec1 = readsPrec--- > instance Applicative Exp where pure = V; (<*>) = ap+-- @+-- instance 'Prelude.Extras.Eq1' Exp   where ('Prelude.Extras.==#')      = ('==')+-- instance 'Prelude.Extras.Ord1' Exp  where 'Prelude.Extras.compare1'   = 'compare'+-- instance 'Prelude.Extras.Show1' Exp where 'Prelude.Extras.showsPrec1' = 'showsPrec'+-- instance 'Prelude.Extras.Read1' Exp where 'Prelude.Extras.readsPrec1' = 'readsPrec'+-- instance 'Control.Applicative.Applicative' Exp where 'Control.Applicative.pure' = V; ('<*>') = 'Control.Monad.ap'+-- @ ----- > instance Monad Exp where--- >   return = V--- >   V a      >>= f = f a--- >   (x :@ y) >>= f = (x >>= f) :@ (y >>= f)--- >   Lam e    >>= f = Lam (e >>>= f)--- >--- > lam :: Eq a => a -> Exp a -> Exp a--- > lam v b = Lam (abstract1 v b)+-- @+-- instance 'Monad' Exp where+--   'return' = V+--   V a      '>>=' f = f a+--   (x :\@ y) '>>=' f = (x '>>=' f) :\@ (y >>= f)+--   Lam e    '>>=' f = Lam (e '>>>=' f)+-- @ ----- > whnf :: Exp a -> Exp a--- > whnf (f :@ a) = case whnf f of--- >   Lam b -> whnf (instantiate1 a b)--- >   f'    -> f' :@ a--- > whnf e = e+-- @+-- lam :: 'Eq' a => a -> 'Exp' a -> 'Exp' a+-- lam v b = Lam ('abstract1' v b)+-- @ --+-- @+-- whnf :: 'Exp' a -> 'Exp' a+-- whnf (f :\@ a) = case whnf f of+--   Lam b -> whnf ('instantiate1' a b)+--   f'    -> f' :\@ a+-- whnf e = e+-- @+-- -- More exotic combinators for manipulating a 'Scope' can be imported from -- "Bound.Scope". --+-- You can also retain names in your bound variables by using 'Bound.Name.Name'+-- and the related combinators from "Bound.Name". They are not re-exported+-- from this module by default. ---------------------------------------------------------------------------- module Bound   (

@@ -12,6 +12,8 @@ -- Stability   :  experimental -- Portability :  portable --+-- This module provides the 'Bound' class, for performing substitution into+-- things that are not necessarily full monad transformers. ---------------------------------------------------------------------------- module Bound.Class   ( Bound(..)@@ -24,15 +26,22 @@  infixl 1 >>>= --- | Instances may or may not be monad transformers.+-- | Instances of 'Bound' may or may not be monad transformers. ----- If they are, then you can use @m >>>= f = m >>= lift . f@+-- If they are, then @m '>>>=' f ≡ m '>>=' 'lift' '.' f@ is required to hold, and is+-- in fact the default definition. If it is not a 'MonadTrans' instance, then+-- you have greater flexibility in how to implement this class. -- -- This is useful for types like expression lists, case alternatives, -- schemas, etc. that may not be expressions in their own right, but often--- contain one.-+-- contain expressions. class Bound t where+  -- | Perform substitution+  --+  -- If @t@ is an instance of @MonadTrans@ and you are compiling on GHC >= 7.4, then this+  -- gets the default definition:+  --+  -- @m '>>>=' f = m '>>=' 'lift' '.' f@   (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 704   default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) =>@@ -41,5 +50,8 @@ #endif  infixr 1 =<<<+-- | A flipped version of ('>>>=').+--+-- @('=<<<') = 'flip' ('>>>=')@ (=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c (=<<<) = flip (>>>=)

@@ -0,0 +1,162 @@+{-# LANGUAGE CPP #-}+#ifdef __GLASGOW_HASKELL__+{-# LANGUAGE DeriveDataTypeable #-}++# if __GLASGOW_HASKELL__ >= 704+{-# LANGUAGE DeriveGeneric #-}+# endif++#endif+-----------------------------------------------------------------------------+-- |+-- Module      :  Bound.Name+-- Copyright   :  (C) 2012 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  experimental+-- Portability :  portable+--+-- The problem with locally nameless approaches is that original names are+-- often useful for error reporting, or to allow for the user in an interactive+-- theorem prover to convey some hint about the domain. A @'Name' n b@ is a value+-- @b@ supplemented with a (discardable) name that may be useful for error+-- reporting purposes. In particular, this name does not participate in+-- comparisons for equality.+--+-- This module is /not/ exported from "Bound" by default. You need to explicitly+-- import it, due to the fact that 'Name' is a pretty common term in other+-- people's code.+----------------------------------------------------------------------------+module Bound.Name+  ( Name(..)+  , name+  , abstractName+  , abstract1Name+  , instantiateName+  , instantiate1Name+  ) where++import Bound.Scope+import Bound.Var+import Data.Foldable+import Data.Traversable+import Data.Monoid+import Data.Bifunctor+import Data.Bifoldable+import Data.Bitraversable+#ifdef __GLASGOW_HASKELL__+import Data.Data+# if __GLASGOW_HASKELL__ >= 704+import GHC.Generics+# endif+#endif+import Control.Applicative+import Control.Comonad+import Control.Monad (liftM)+import Prelude.Extras++-------------------------------------------------------------------------------+-- Names+-------------------------------------------------------------------------------++-- |+-- We track the choice of 'Name' @n@ as a forgettable property that does /not/ affect+-- the result of ('==') or 'compare'.+--+-- To compare names rather than values, use @('Data.Function.on' 'compare' 'name')@ instead.+data Name n b = Name n b deriving+  ( Show+  , Read+#ifdef __GLASGOW_HASKELL__+  , Typeable+  , Data+# if __GLASGOW_HASKELL__ >= 704+  , Generic+# endif+#endif+  )++-- | Extract the 'name'.+name :: Name n b -> n+name (Name n _) = n++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance Eq b => Eq (Name n b) where+  Name _ a == Name _ b = a == b++instance Ord b => Ord (Name n b) where+  Name _ a `compare` Name _ b = compare a b++instance Functor (Name n) where+  fmap f (Name n a) = Name n (f a)++instance Foldable (Name n) where+  foldMap f (Name _ a) = f a++instance Traversable (Name n) where+  traverse f (Name n a) = Name n <$> f a++instance Bifunctor Name where+  bimap f g (Name n a) = Name (f n) (g a)++instance Bifoldable Name where+  bifoldMap f g (Name n a) = f n `mappend` g a++instance Bitraversable Name where+  bitraverse f g (Name n a) = Name <$> f n <*> g a++instance Comonad (Name n) where+  extract (Name _ b) = b+  extend f w@(Name n _) = Name n (f w)++instance Eq1   (Name b) where (==#)      = (==)+instance Ord1  (Name b) where compare1   = compare+instance Show b => Show1 (Name b) where showsPrec1 = showsPrec+instance Read b => Read1 (Name b) where readsPrec1 = readsPrec++-- these are slightly too restrictive, but still safe+instance Eq2 Name   where (==##)     = (==)+instance Ord2 Name  where compare2   = compare+instance Show2 Name where showsPrec2 = showsPrec+instance Read2 Name where readsPrec2  = readsPrec++-------------------------------------------------------------------------------+-- Abstraction+-------------------------------------------------------------------------------++-- | Abstraction, capturing named bound variables.+abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f a+abstractName f t = Scope (liftM k t) where+  k a = case f a of+    Just b  -> B (Name a b)+    Nothing -> F (return a)+{-# INLINE abstractName #-}++-- | Abstract over a single variable+abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f a+abstract1Name a = abstractName (\b -> if a == b then Just () else Nothing)+{-# INLINE abstract1Name #-}++-------------------------------------------------------------------------------+-- Instantiation+-------------------------------------------------------------------------------++-- | Enter a scope, instantiating all bound variables, but discarding (comonadic)+-- meta data, like its name+instantiateName :: (Monad f, Comonad n) => (b -> f a) -> Scope (n b) f a -> f a+instantiateName k e = unscope e >>= \v -> case v of+  B b -> k (extract b)+  F a -> a+{-# INLINE instantiateName #-}+++-- | Enter a 'Scope' that binds one (named) variable, instantiating it.+--+-- @'instantiate1Name' = 'instantiate1'@+instantiate1Name :: Monad f => f a -> Scope n f a -> f a+instantiate1Name = instantiate1+{-# INLINE instantiate1Name #-}

@@ -8,6 +8,10 @@ -- Stability   :  experimental -- Portability :  portable --+-- This is the work-horse of the @bound@ library.+--+-- 'Scope' provides a single generalized de Bruijn level+-- and is often used inside of the definition of binders. ---------------------------------------------------------------------------- module Bound.Scope   ( Scope(..)@@ -51,6 +55,10 @@ import Prelude.Extras import Prelude hiding (foldr, mapM, mapM_) +-------------------------------------------------------------------------------+-- Scopes+-------------------------------------------------------------------------------+ -- | @'Scope' b f a@ is an @f@ expression with bound variables in @b@, -- and free variables in @a@ --@@ -72,6 +80,10 @@ -- newtype Scope b f a = Scope { unscope :: f (Var b (f a)) } +-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------+ instance Functor f => Functor (Scope b f) where   fmap f (Scope a) = Scope (fmap (fmap (fmap f)) a) @@ -122,8 +134,16 @@ instance Bound (Scope b) where   Scope m >>>= f = Scope (liftM (fmap (>>= f)) m) +-------------------------------------------------------------------------------+-- Abstraction+-------------------------------------------------------------------------------+ -- | Capture some free variables in an expression to yield -- a 'Scope' with bound variables in @b@+--+-- >>> :m + Data.List+-- >>> abstract (`elemIndex` "bar") "barry"+-- Scope [B 0,B 1,B 2,B 2,F "y"] abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a abstract f e = Scope (liftM k e) where   k y = case f y of@@ -131,33 +151,54 @@     Nothing -> F (return y) {-# INLINE abstract #-} +-- | Abstract over a single variable+--+-- >>> abstract1 'x' "xyz"+-- Scope [B (),F "y",F "z"]+abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a+abstract1 a = abstract (\b -> if a == b then Just () else Nothing)+{-# INLINE abstract1 #-}++-------------------------------------------------------------------------------+-- Instantiation+-------------------------------------------------------------------------------+ -- | Enter a scope, instantiating all bound variables+--+-- >>> :m + Data.List+-- >>> instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"+-- "abccy" instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a instantiate k e = unscope e >>= \v -> case v of   B b -> k b   F a -> a {-# INLINE instantiate #-} --- * Special purpose combinators---- | Abstract over a single variable-abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a-abstract1 a = abstract (\b -> if a == b then Just () else Nothing)-{-# INLINE abstract1 #-}- -- | Enter a 'Scope' that binds one variable, instantiating it-instantiate1 :: Monad f => f a -> Scope () f a -> f a+--+-- >>> instantiate1 "x" $ Scope [B (),F "y",F "z"]+-- "xyz"+instantiate1 :: Monad f => f a -> Scope n f a -> f a instantiate1 e = instantiate (const e) {-# INLINE instantiate1 #-} +-------------------------------------------------------------------------------+-- Traditional de Bruijn+-------------------------------------------------------------------------------+ -- | @'fromScope'@ quotients out the possible placements of 'F' in 'Scope' -- by distributing them all to the leaves. This yields a more traditional -- de Bruijn indexing scheme for bound variables. ----- > fromScope . toScope = id--- > fromScope . toScope . fromScope = fromScope+-- Since, ----- @('toScope' . 'fromScope')@ is idempotent+-- @'fromScope' '.' 'toScope' ≡ 'id'@+--+-- we know that+--+-- @'fromScope' '.' 'toScope' '.' 'fromScope' ≡ 'fromScope'@+--+-- and therefore @('toScope' . 'fromScope')@ is idempotent. fromScope :: Monad f => Scope b f a -> f (Var b a) fromScope (Scope s) = s >>= \v -> case v of   F e -> liftM F e@@ -171,21 +212,25 @@ toScope e = Scope (liftM (fmap return) e) {-# INLINE toScope #-} --- | Perform substitution on both bound and free variables in a 'Scope'+-------------------------------------------------------------------------------+-- Exotic Traversals of Bound Variables (not exported by default)+-------------------------------------------------------------------------------++-- | Perform substitution on both bound and free variables in a 'Scope'. splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c splat f unbind s = unscope s >>= \v -> case v of   B b -> unbind b   F ea -> ea >>= f {-# INLINE splat #-} --- Return a list of occurences of the variables bound by this scope+-- | Return a list of occurences of the variables bound by this 'Scope'. bindings :: Foldable f => Scope b f a -> [b] bindings (Scope s) = foldr f [] s where   f (B v) vs = v : vs   f _ vs     = vs {-# INLINE bindings #-} --- | Perform a change of variables on bound variables+-- | Perform a change of variables on bound variables. mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a mapBound f (Scope s) = Scope (fmap f' s) where   f' (B b) = B (f b)@@ -226,6 +271,7 @@ foldMapScope f g (Scope s) = foldMap (bifoldMap f (foldMap g)) s {-# INLINE foldMapScope #-} +-- | 'traverse_' the bound variables in a 'Scope'. traverseBound_ :: (Applicative g, Foldable f) =>                   (b -> g d) -> Scope b f a -> g () traverseBound_ f (Scope s) = traverse_ f' s@@ -233,7 +279,7 @@         f' _     = pure () {-# INLINE traverseBound_ #-} ---- | Traverse both the variables bound by this scope and any free variables.+-- | 'traverse' both the variables bound by this scope and any free variables. traverseScope_ :: (Applicative g, Foldable f) =>                   (b -> g d) -> (a -> g c) -> Scope b f a -> g () traverseScope_ f g (Scope s) = traverse_ (bitraverse_ f (traverse_ g)) s@@ -253,7 +299,7 @@ mapMScope_ f g (Scope s) = mapM_ (bimapM_ f (mapM_ g)) s {-# INLINE mapMScope_ #-} ---- | Traverse both bound and free variables+-- | Traverse both bound and free variables traverseBound :: (Applicative g, Traversable f) =>                  (b -> g c) -> Scope b f a -> g (Scope c f a) traverseBound f (Scope s) = Scope <$> traverse f' s where@@ -261,13 +307,13 @@   f' (F a) = pure (F a) {-# INLINE traverseBound #-} ---- | Traverse both bound and free variables+-- | Traverse both bound and free variables traverseScope :: (Applicative g, Traversable f) =>                  (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c) traverseScope f g (Scope s) = Scope <$> traverse (bitraverse f (traverse g)) s {-# INLINE traverseScope #-} ---- | mapM over both bound and free variables+-- | mapM over both bound and free variables mapMBound :: (Monad m, Traversable f) =>              (b -> m c) -> Scope b f a -> m (Scope c f a) mapMBound f (Scope s) = liftM Scope (mapM f' s) where@@ -275,7 +321,7 @@   f' (F a) = return (F a) {-# INLINE mapMBound #-} ---- | A 'traverseScope' that can be used when you only have a 'Monad'+-- | A 'traverseScope' that can be used when you only have a 'Monad' -- instance mapMScope :: (Monad m, Traversable f) =>              (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)

@@ -11,6 +11,7 @@ ---------------------------------------------------------------------------- module Bound.Term   ( substitute+  , substituteVar   , isClosed   , closed   ) where@@ -19,18 +20,44 @@ import Data.Traversable import Prelude hiding (all) --- | @'substitute' a p w@ replaces the free variable @a@ with @p@ in @w@+-- | @'substitute' a p w@ replaces the free variable @a@ with @p@ in @w@.+--+-- >>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]+-- ["goodnight","Gracie","!!!"] substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a substitute a p w = w >>= \b -> if a == b then p else return b {-# INLINE substitute #-} +-- | @'substituteVar' a b w@ replaces a free variable @a@ with another free variable @b@ in @w@.+--+-- >>> substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]+-- ["Bob","Bob","Charlie"]+substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a+substituteVar a p = fmap (\b -> if a == b then p else b)+{-# INLINE substituteVar #-}+ -- | If a term has no free variables, you can freely change the type of -- free variables it is parameterized on.+--+-- >>> closed [12]+-- Nothing+--+-- >>> closed ""+-- Just []+--+-- >>> :t closed ""+-- closed "" :: Maybe [b] closed :: Traversable f => f a -> Maybe (f b) closed = traverse (const Nothing) {-# INLINE closed #-}  -- | A closed term has no free variables.+--+-- >>> isClosed []+-- True+--+-- >>> isClosed [1,2,3]+-- False isClosed :: Foldable f => f a -> Bool isClosed = all (const False) {-# INLINE isClosed #-}

@@ -1,3 +1,13 @@+{-# LANGUAGE CPP #-}++#ifdef __GLASGOW_HASKELL__+{-# LANGUAGE DeriveDataTypeable #-}++# if __GLASGOW_HASKELL__ >= 704+{-# LANGUAGE DeriveGeneric #-}+# endif++#endif ----------------------------------------------------------------------------- -- | -- Module      :  Bound.Var@@ -13,26 +23,52 @@   ( Var(..)   ) where +import Control.Applicative+import Control.Monad (ap) import Data.Foldable import Data.Traversable import Data.Monoid (mempty) import Data.Bifunctor import Data.Bifoldable import Data.Bitraversable-import Control.Applicative-import Control.Monad (ap)+#ifdef __GLASGOW_HASKELL__+import Data.Data+# if __GLASGOW_HASKELL__ >= 704+import GHC.Generics+# endif+#endif import Prelude.Extras +----------------------------------------------------------------------------+-- Bound and Free Variables+----------------------------------------------------------------------------+ -- | \"I am not a number, I am a /free monad/!\" ----- A @Var b a@ is a variable that may either be \"bound\" or \"free\".+-- A @'Var' b a@ is a variable that may either be \"bound\" ('B') or \"free\" ('F'). ----- (It is also technically a free monad in the same near trivial sense as+-- (It is also technically a free monad in the same near-trivial sense as -- 'Either'.) data Var b a   = B b -- ^ this is a bound variable   | F a -- ^ this is a free variable-  deriving (Eq,Ord,Show,Read)+  deriving+  ( Eq+  , Ord+  , Show+  , Read+#ifdef __GLASGOW_HASKELL__+  , Data+  , Typeable+# if __GLASGOW_HASKELL__ >= 704+  , Generic+# endif+#endif+  )++----------------------------------------------------------------------------+-- Instances+----------------------------------------------------------------------------  instance Functor (Var b) where   fmap _ (B b) = B b

@@ -0,0 +1,32 @@+module Main where++import Test.DocTest+import System.Directory+import System.FilePath+import Control.Applicative+import Control.Monad+import Data.List++main :: IO ()+main = getSources >>= \sources -> doctest $+    "-iexamples"+  : "-isrc"+  : "-idist/build/autogen"+  : "-optP-include"+  : "-optPdist/build/autogen/cabal_macros.h"+  : sources++getSources :: IO [FilePath]+getSources = do+  examples <- go "examples"+  src <- go "src"+  return $ filter (isSuffixOf ".hs") (examples ++ src)+  where+    go dir = do+      (dirs, files) <- getFilesAndDirectories dir+      (files ++) . concat <$> mapM go dirs++getFilesAndDirectories :: FilePath -> IO ([FilePath], [FilePath])+getFilesAndDirectories dir = do+  c <- map (dir </>) . filter (`notElem` ["..", "."]) <$> getDirectoryContents dir+  (,) <$> filterM doesDirectoryExist c <*> filterM doesFileExist c