Skip to content

Commit

Permalink
Merge branch 'master' of github.com:ekmett/bound
Browse files Browse the repository at this point in the history
  • Loading branch information
ekmett committed Jul 25, 2016
2 parents 0df8000 + a5ae503 commit 9bd4849
Show file tree
Hide file tree
Showing 15 changed files with 462 additions and 111 deletions.
11 changes: 8 additions & 3 deletions .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,10 @@ matrix:
addons: {apt: {packages: [cabal-install-1.16,ghc-7.6.3], sources: [hvr-ghc]}}
- env: CABALVER=1.18 GHCVER=7.8.4
addons: {apt: {packages: [cabal-install-1.18,ghc-7.8.4], sources: [hvr-ghc]}}
- env: CABALVER=1.22 GHCVER=7.10.1
addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.1],sources: [hvr-ghc]}}
- env: CABALVER=1.22 GHCVER=7.10.3
addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.3],sources: [hvr-ghc]}}
- env: CABALVER=1.24 GHCVER=8.0.1
addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1],sources: [hvr-ghc]}}
- env: CABALVER=head GHCVER=head
addons: {apt: {packages: [cabal-install-head,ghc-head], sources: [hvr-ghc]}}

Expand All @@ -20,17 +22,20 @@ matrix:
before_install:
- export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
- export CABAL=cabal-$CABALVER
- echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"
- $CABAL --version
- ghc-pkg list | grep Cabal

install:
- travis_retry $CABAL update
- $CABAL install "Cabal == $CABALVER.*"
# - $CABAL install "Cabal == $CABALVER.*"
- $CABAL install --enable-tests --only-dependencies

script:
- $CABAL configure -v2 --enable-tests
- $CABAL build
- $CABAL test
- $CABAL haddock
- $CABAL sdist
- export SRC_TGZ=$($CABAL info . | awk '{print $2 ".tar.gz";exit}') ;
cd dist/;
Expand Down
39 changes: 33 additions & 6 deletions README.markdown
Original file line number Diff line number Diff line change
Expand Up @@ -17,20 +17,16 @@ See [the documentation](http://hackage.haskell.org/package/bound) on hackage for
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
import Bound
import Prelude.Extras
import Control.Applicative
import Control.Monad
import Data.Functor.Classes
import Data.Foldable
import Data.Traversable

infixl 9 :@
data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
deriving (Eq,Show,Functor,Foldable,Traversable)

instance Eq1 Exp
instance Ord1 Exp
instance Show1 Exp
instance Read1 Exp
instance Applicative Exp where pure = V; (<*>) = ap

instance Monad Exp where
Expand All @@ -47,6 +43,37 @@ whnf (f :@ a) = case whnf f of
Lam b -> whnf (instantiate1 a b)
f' -> f' :@ a
whnf e = e

-- Unfortunately we have to write these instances by hand, for now.
--
-- https://mail.haskell.org/pipermail/libraries/2016-January/026536.html
-- https://github.com/haskell-compat/deriving-compat/issues/3
instance Eq1 Exp where
liftEq g (V a) (V b) = g a b
liftEq g (a :@ a') (b :@ b') = liftEq g a b && liftEq g a' b'
liftEq g (Lam a) (Lam b) = liftEq g a b
liftEq _ _ _ = False

instance Show1 Exp where
liftShowsPrec g _ d (V a) =
showParen (d >= 11)
$ showString "V "
. g 11 a
liftShowsPrec g h d (a :@ b) =
showParen (d >= 10)
$ liftShowsPrec g h 10 a
. showString " :@ "
. liftShowsPrec g h 10 b
liftShowsPrec g h d (Lam a) =
showParen (d >= 11)
$ showString "Lam "
. liftShowsPrec g h 11 a

main :: IO ()
main = do
let term = lam 'x' (V 'x') :@ V 'y'
print term -- Lam (Scope (V (B ()))) :@ V 'y'
print $ whnf term -- V 'y'
```

There are longer examples in the [examples/ folder](https://github.com/ekmett/bound/tree/master/examples).
Expand Down
4 changes: 4 additions & 0 deletions Setup.lhs
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,10 @@ generateBuildModule verbosity pkg lbi = do
createDirectoryIfMissingVerbose verbosity True dir
rewriteFile (dir </> "Build_" ++ testName suite ++ ".hs") $ unlines
[ "module Build_" ++ testName suite ++ " where"
, ""
, "autogen_dir :: String"
, "autogen_dir = " ++ show dir
, ""
, "deps :: [String]"
, "deps = " ++ (show $ formatdeps (testDeps libcfg suitecfg))
]
Expand Down
58 changes: 46 additions & 12 deletions bound.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ description:
and we traverse to find free variables, and use the Monad to perform
substitution that avoids bound variables.
.
Slides describing and motivating this approach to name binding are available
Slides describing and motivating this approach to name binding are available
online at:
.
<http://www.slideshare.net/ekmett/bound-making-de-bruijn-succ-less>
Expand All @@ -30,7 +30,7 @@ description:
With generalized de Bruijn term you can 'lift' whole trees instead of just
applying 'succ' to individual variables, weakening the all variables bound
by a scope and greatly speeding up instantiation. By giving binders more
structure we permit easy simultaneous substitution and further speed up
structure we permit easy simultaneous substitution and further speed up
instantiation.

extra-source-files:
Expand Down Expand Up @@ -108,18 +108,52 @@ test-suite Simple
transformers,
transformers-compat

test-suite Overkill
type: exitcode-stdio-1.0
main-is: Overkill.hs
hs-source-dirs: examples
ghc-options: -Wall -threaded -main-is Overkill
build-depends:
base,
bound,
transformers,
transformers-compat,
vector
if !impl(ghc >= 7.8)
buildable: False

test-suite Deriving
type: exitcode-stdio-1.0
main-is: Deriving.hs
hs-source-dirs: examples
ghc-options: -Wall -threaded -main-is Deriving
build-depends:
base,
bound,
transformers,
transformers-compat

test-suite Imperative
type: exitcode-stdio-1.0
main-is: Imperative.hs
hs-source-dirs: examples
ghc-options: -Wall -threaded -main-is Imperative
build-depends:
base,
bound,
transformers,
transformers-compat,
void

test-suite doctests
type: exitcode-stdio-1.0
main-is: doctests.hs
hs-source-dirs: tests
if impl(ghc>=8)
buildable: False
else
ghc-options: -Wall -threaded
build-depends:
base,
directory >= 1.0 && < 1.3,
doctest >= 0.9 && < 0.10,
filepath,
vector >= 0.9 && < 0.11
ghc-options: -Wall -threaded
build-depends:
base,
directory >= 1.0 && < 1.3,
doctest >= 0.9 && < 0.12,
filepath,
vector >= 0.9 && < 0.12,
void
38 changes: 31 additions & 7 deletions examples/Deriving.hs
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
{-# LANGUAGE CPP, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
module Deriving where

import Data.List
import Data.Foldable
import Data.Traversable
import Control.Monad
import Control.Applicative
import Prelude.Extras
import Data.Functor.Classes
import Bound

infixl 9 :@
Expand All @@ -17,7 +17,7 @@ data Exp a
| Lam {-# UNPACK #-} !Int (Pat Exp a) (Scope Int Exp a)
| Let {-# UNPACK #-} !Int [Scope Int Exp a] (Scope Int Exp a)
| Case (Exp a) [Alt Exp a]
deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
deriving (Eq,Functor,Foldable,Traversable)

instance Applicative Exp where
pure = V
Expand All @@ -31,10 +31,18 @@ instance Monad Exp where
Let n bs e >>= f = Let n (map (>>>= f) bs) (e >>>= f)
Case e as >>= f = Case (e >>= f) (map (>>>= f) as)

#if MIN_VERSION_transformers(0,5,0) || !MIN_VERSION_transformers(0,4,0)
instance Eq1 Exp where
liftEq eq (V a) (V b) = eq a b
liftEq eq (a :@ a') (b :@ b') = liftEq eq a b && liftEq eq a' b'
liftEq eq (Lam n p e) (Lam n' p' e') = n == n' && liftEq eq p p' && liftEq eq e e'
liftEq eq (Let n bs e) (Let n' bs' e') = n == n' && liftEq (liftEq eq) bs bs' && liftEq eq e e'
liftEq eq (Case e as) (Case e' as') = liftEq eq e e' && liftEq (liftEq eq) as as'
liftEq _ _ _ = False
#else
instance Eq1 Exp
instance Ord1 Exp
instance Show1 Exp
instance Read1 Exp
#endif
-- And "similarly" for Ord1, Show1 and Read1

data Pat f a
= VarP
Expand All @@ -44,6 +52,16 @@ data Pat f a
| ViewP (Scope Int f a) (Pat f a)
deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)

#if MIN_VERSION_transformers(0,5,0) || !MIN_VERSION_transformers(0,4,0)
instance (Eq1 f, Monad f) => Eq1 (Pat f) where
liftEq _ VarP VarP = True
liftEq _ WildP WildP = True
liftEq eq (AsP p) (AsP p') = liftEq eq p p'
liftEq eq (ConP g ps) (ConP g' ps') = g == g' && liftEq (liftEq eq) ps ps'
liftEq eq (ViewP e p) (ViewP e' p') = liftEq eq e e' && liftEq eq p p'
liftEq _ _ _ = False
#endif

instance Bound Pat where
VarP >>>= _ = VarP
WildP >>>= _ = WildP
Expand All @@ -52,7 +70,13 @@ instance Bound Pat where
ViewP e p >>>= f = ViewP (e >>>= f) (p >>>= f)

data Alt f a = Alt {-# UNPACK #-} !Int (Pat f a) (Scope Int f a)
deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
deriving (Eq,Functor,Foldable,Traversable)

#if MIN_VERSION_transformers(0,5,0) || !MIN_VERSION_transformers(0,4,0)
instance (Eq1 f, Monad f) => Eq1 (Alt f) where
liftEq eq (Alt n p b) (Alt n' p' b') =
n == n' && liftEq eq p p' && liftEq eq b b'
#endif

instance Bound Alt where
Alt n p b >>>= f = Alt n (p >>>= f) (b >>>= f)
Expand Down
Loading

0 comments on commit 9bd4849

Please sign in to comment.