bound (empty) → 0.1

raw patch · 11 files changed

+745/−0 lines, 11 filesdep +basedep +bifunctorsdep +prelude-extrassetup-changed

Dependencies added: base, bifunctors, prelude-extras, transformers

Files

.travis.yml +1/−0
Bound.hs +22/−0
Bound/Class.hs +34/−0
Bound/Scope.hs +147/−0
Bound/Term.hs +33/−0
Bound/Var.hs +74/−0
LICENSE +30/−0
Setup.lhs +7/−0
bound.cabal +37/−0
examples/Exp.hs +308/−0
examples/Simple.hs +52/−0

+ .travis.yml view

@@ -0,0 +1,1 @@+language: haskell

+ Bound.hs view

@@ -0,0 +1,22 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Bound+-- Copyright   :  (C) 2012 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  experimental+-- Portability :  portable+--+----------------------------------------------------------------------------+module Bound+  ( module Bound.Var+  , module Bound.Class+  , module Bound.Scope+  , module Bound.Term+  ) where++import Bound.Var+import Bound.Class+import Bound.Scope+import Bound.Term

+ Bound/Class.hs view

@@ -0,0 +1,34 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Bound.Class+-- Copyright   :  (C) 2012 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  experimental+-- Portability :  portable+--+----------------------------------------------------------------------------+module Bound.Class+  ( Bound(..)+  , (=<<<)+  ) where++infixl 1 >>>=++-- | This may or may not be a monad transformer,+--+-- If it is, then you can use @m >>>= f = m >>= lift . f@+--+-- 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.++class Bound t where+  (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c+  -- default (>>>=) :: MonadTrans t, Monad f) => t f a -> (a -> f c) -> t f c+  -- m >>>= f = m >>= lift . f++infixr 1 =<<<+(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c+(=<<<) = flip (>>>=)

+ Bound/Scope.hs view

@@ -0,0 +1,147 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Bound.Scope+-- Copyright   :  (C) 2012 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  experimental+-- Portability :  portable+--+----------------------------------------------------------------------------+module Bound.Scope+  ( Scope(..)+  -- * Abstraction+  , abstract, abstract1+  -- * Instantiation+  , instantiate, instantiate1+  -- * Substitution+  , splat+  -- * Quotienting+  , fromScope+  , toScope+  ) where++import Data.Foldable+import Data.Traversable+import Control.Monad+import Control.Monad.Trans.Class+import Control.Applicative+import Prelude.Extras+import Bound.Class+import Bound.Var++-- | @Scope b f a@ is a an @f@ expression with bound variables in @b@, and free variables in @a@+--+-- This stores bound variables as their generalized de Bruijn representation,+-- in that the succ's for variable ids are allowed to occur anywhere within the tree+-- permitting /O(1)/ weakening and allowing more sharing opportunities. +-- Here the deBruijn 0 is represented by the 'B' constructor of 'Var', while the +-- de Bruijn 'succ' (which may be applied to an entire tree!) is handled by 'F'.+--+-- NB: equality and comparison quotient out the distinct 'F' placements allowed by +-- the choice of a generalized de Bruijn representation and return the same result as a traditional de Bruijn+-- representation would.++newtype Scope b f a = Scope { unscope :: f (Var b (f a)) }++instance Functor f => Functor (Scope b f) where+  fmap f (Scope a) = Scope (fmap (fmap (fmap f)) a)++-- | @toList@ is provides a list (with duplicates) of the free variables+instance Foldable f => Foldable (Scope b f) where+  foldMap f (Scope a) = foldMap (foldMap (foldMap f)) a++instance Traversable f => Traversable (Scope b f) where+  traverse f (Scope a) = Scope <$> traverse (traverse (traverse f)) a++-- | The monad permits substitution on free variables, while preserving bound variables+instance Monad f => Monad (Scope b f) where+  return a = Scope (return (F (return a)))+  Scope e >>= f = Scope $ e >>= \v -> case v of+    B b -> return (B b)+    F ea -> ea >>= unscope . f++instance MonadTrans (Scope b) where+  lift m = Scope (return (F m))++instance (Monad f, Eq b, Eq1 f, Eq a) => Eq  (Scope b f a) where (==) = (==#)+instance (Monad f, Eq b, Eq1 f)       => Eq1 (Scope b f)   where+  a ==# b = liftM Lift2 (fromScope a) ==# liftM Lift2 (fromScope b)+  -- a ==# b = mangleScope a ==# mangleScope b++instance (Monad f, Ord b, Ord1 f, Ord a) => Ord  (Scope b f a) where compare = compare1+instance (Monad f, Ord b, Ord1 f)        => Ord1 (Scope b f) where+  compare1 a b = liftM Lift2 (fromScope a) `compare1` liftM Lift2 (fromScope b)+  -- compare1 a b = compare1 (mangleScope a) (mangleScope b)++mangleScope :: Functor f => Scope b f a -> f (Lift2 Var b (Lift1 f a))+mangleScope (Scope a) = fmap (Lift2 . fmap Lift1) a+{-# INLINE mangleScope #-}++unmangleScope :: Functor f => f (Lift2 Var b (Lift1 f a)) -> Scope b f a+unmangleScope a = Scope (fmap (fmap lower1 . lower2) a)+{-# INLINE unmangleScope #-}+++instance (Functor f, Show b, Show1 f, Show a) => Show  (Scope b f a) where showsPrec = showsPrec1+instance (Functor f, Show b, Show1 f)         => Show1 (Scope b f)   where+  showsPrec1 d a = showParen (d > 10) $ showString "Scope " . showsPrec1 11 (mangleScope a)++instance (Functor f, Read b, Read1 f, Read a) => Read  (Scope b f a) where readsPrec = readsPrec1+instance (Functor f, Read b, Read1 f)         => Read1 (Scope b f) where+  readPrec1 = liftM unmangleScope readPrec1++instance Bound (Scope b) where+  m >>>= f = m >>= lift . f++-- | Capture some free variables in an expression to yield a Scope with bound variables+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+    Just z  -> B z+    Nothing -> F (return y)+{-# INLINE abstract #-}++-- | 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, instantiating all bound variables+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 #-}++-- | Enter a scope with one bound variable, instantiating it+instantiate1 :: Monad f => f a -> Scope () f a -> f a+instantiate1 e = instantiate (\ () -> e)+{-# INLINE instantiate1 #-}+++-- | @fromScope@ quotients out the possible placements of F in Scope+-- distributing them all to the leaves. This yields a traditional deBruijn+-- indexing scheme for bound variables.+--+-- > fromScope . toScope = id+-- > fromScope . toScope . fromScope = fromScope+--+-- @(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+  B b -> return (B b)+{-# INLINE fromScope #-}++toScope :: Monad f => f (Var b a) -> Scope b f a+toScope e = Scope (liftM (fmap return) e)+{-# INLINE toScope #-}++-- | 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 #-}

+ Bound/Term.hs view

@@ -0,0 +1,33 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Bound.Term+-- Copyright   :  (C) 2012 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  experimental+-- Portability :  portable+--+----------------------------------------------------------------------------+module Bound.Term+  ( substitute+  , isClosed+  , closed+  ) where++import Data.Traversable+import Data.Maybe (isJust)++-- | @substitute p a w@ replaces the free variable @a@ with @p@ in @w@+substitute :: (Monad f, Eq a) => f a -> a -> f a -> f a+substitute p a w = w >>= \b -> if a == b then p else return b+{-# INLINE substitute #-}++-- | If a term has no free variables, you can freely change the type of free variables it uses+closed :: Traversable f => f a -> Maybe (f b)+closed = traverse (const Nothing)+{-# INLINE closed #-}++isClosed :: Traversable f => f a -> Bool+isClosed = isJust . closed+{-# INLINE isClosed #-}

+ Bound/Var.hs view

@@ -0,0 +1,74 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Bound.Var+-- Copyright   :  (C) 2012 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  experimental+-- Portability :  portable+--+----------------------------------------------------------------------------+module Bound.Var (Var(..)) where++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)+import Prelude.Extras+import Text.Read++-- | "I am not a number, I am a /free monad/!"+--+-- @Var b a@ represents variables that may either be "bound" (@B@) or "free" (@F@)+data Var b a+  = B b -- this is a bound variable+  | F a -- this is a free variable+  deriving (Eq,Ord,Show,Read)++instance Functor (Var b) where+  fmap _ (B b) = B b+  fmap f (F a) = F (f a)++instance Foldable (Var b) where+  foldMap f (F a) = f a+  foldMap _ _ = mempty++instance Traversable (Var b) where+  traverse f (F a) = F <$> f a+  traverse _ (B b) = pure (B b)++instance Applicative (Var b) where+  pure = F+  (<*>) = ap++instance Monad (Var b) where+  return = F+  F a  >>= f = f a+  B b >>= _ = B b++instance Bifunctor Var where+  bimap f _ (B b) = B (f b)+  bimap _ g (F a) = F (g a)++instance Bifoldable Var where+  bifoldMap f _ (B b) = f b+  bifoldMap _ g (F a) = g a++instance Bitraversable Var where+  bitraverse f _ (B b) = B <$> f b+  bitraverse _ g (F a) = F <$> g a++instance Eq2 Var   where (==##)     = (==)+instance Ord2 Var  where compare2   = compare+instance Show2 Var where showsPrec2 = showsPrec+instance Read2 Var where readPrec2  = readPrec++instance Eq b   => Eq1   (Var b) where (==#)      = (==)+instance Ord b  => Ord1  (Var b) where compare1   = compare+instance Show b => Show1 (Var b) where showsPrec1 = showsPrec+instance Read b => Read1 (Var b) where readPrec1  = readPrec

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright 2012 Edward Kmett++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.++2. 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.++3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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.

+ Setup.lhs view

@@ -0,0 +1,7 @@+#!/usr/bin/runhaskell+> module Main (main) where++> import Distribution.Simple++> main :: IO ()+> main = defaultMain

+ bound.cabal view

@@ -0,0 +1,37 @@+name:          bound+category:      Language, Compilers/Interpreters+version:       0.1+license:       BSD3+cabal-version: >= 1.6+license-file:  LICENSE+author:        Edward A. Kmett+maintainer:    Edward A. Kmett <ekmett@gmail.com>+stability:     experimental+homepage:      http://github.com/ekmett/bound/+bug-reports:   http://github.com/ekmett/bound/issues+copyright:     Copyright (C) 2012 Edward A. Kmett+synopsis:      Combinators for manipulating locally-nameless generalized de Bruijn terms+description:   Combinators for manipulating locally-nameless generalized de Bruijn terms++build-type:    Simple+extra-source-files: .travis.yml examples/Simple.hs examples/Exp.hs++source-repository head+  type: git+  location: git://github.com/ekmett/bound.git++library+  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.Scope+    Bound.Term+    Bound.Var++  ghc-options: -Wall

+ examples/Exp.hs view

@@ -0,0 +1,308 @@+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE TypeOperators #-}+module Exp where+++import Data.Vector as Vector hiding ((++), map)+import Data.List as List+import Data.Foldable+import Data.Traversable+import Data.Monoid (Monoid(..))+import Control.Monad+import Control.Monad.Trans.Class+import Control.Applicative+import Prelude hiding (foldr)+import Prelude.Extras+import GHC.Prim (Constraint(..))+import Unsafe.Coerce+import Bound++-- ghci> 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)))))))+--+-- ghc> lam (varp "x") (Var "x")+-- ghc> lam (conp "Hello" [varp "x", wildp])) (Var "y")++infixl 9 :@+infixr 5 :>++-- little orphan instances+instance Show1 Vector where showsPrec1 = showsPrec+instance Eq1 Vector where (==#) = (==)++data Exp a+  = Var a+  | Exp a :@ Exp a+  | forall (b :: Index). Lam (Pat b Exp a) (Scope (Path b) Exp a)+  | Let (Vector (Scope Int Exp a)) (Scope Int Exp a)+  -- | Case (Exp a) [Alt Exp a]++data Alt f a = forall b. Alt (Pat b f a) (Scope (Path b) Exp a)++data Index = VarI | WildI | AsI Index | ConI [Index]++data Pat :: Index -> (* -> *) -> * -> * where+  VarP  ::                             Pat VarI f a+  WildP ::                             Pat WildI f a+  AsP   :: Pat i f a                -> Pat (AsI i) f a+  ConP  :: String    -> Pats bs f a -> Pat (ConI bs) f a+  ViewP :: f a       -> Pat b f a   -> Pat b f a -- TODO: allow references to earlier variables++data Pats :: [Index] -> (* -> *) -> * -> * where+  NilP  :: Pats '[] f a+  (:>) :: Pat b f a -> Pats bs f a -> Pats (b ': bs) f a++data Path :: Index -> * where+  V :: Path VarI+  L :: Path (AsI a)+  R :: Path a -> Path (AsI a)+  C :: MPath as -> Path (ConI as)++data MPath :: [Index] -> * where+  H :: Path a   -> MPath (a ':as)+  T :: MPath as -> MPath (a ':as)++instance Functor Exp where+  fmap = fmapDefault++instance Foldable Exp where+  foldMap = foldMapDefault++instance Applicative Exp where+  pure = Var+  (<*>) = ap++instance Traversable Exp where+  traverse f (Var a)    = Var <$> f a+  traverse f (x :@ y)   = (:@) <$> traverse f x <*> traverse f y+  traverse f (Lam p e)  = Lam <$> traverse f p <*> traverse f e+  traverse f (Let bs e) = Let <$> traverse (traverse f) bs <*> traverse f e++instance Monad Exp where+  return         = Var+  Var a    >>= f = f a+  (x :@ y) >>= f = (x >>= f) :@ (y >>= f)+  Lam p e  >>= f = Lam (p >>>= f) (e >>>= f)+  Let bs e >>= f = Let (fmap (>>>= f) bs) (e >>>= f)+ -- Case e as >>= f = Case (e >>= f) (fmap (>>>= f) as)++instance Eq a => Eq (Exp a) where (==) = (==#)+instance Eq1 Exp where+  Var a     ==# Var b     = a == b+  (a :@ b)  ==# (c :@ d)  = a ==# c && b ==# d+  Lam ps a  ==# Lam qs b  = eqPat ps qs && a ==# unsafeCoerce b -- eqPat proves equal shape+  Let as a  ==# Let bs b  = as == bs && a ==# b+ -- Case e as ==# Case f bs = e ==# f && as == bs+  _         ==# _         = False++instance Show a => Show (Exp a) where showsPrec = showsPrec1+instance Show1 Exp where+  showsPrec1 d (Var a)    = showParen (d > 10) $ showString "Var " . showsPrec 11 a+  showsPrec1 d (a :@ b)   = showParen (d > 9) $ showsPrec1 9 a . showString " :@ " . showsPrec1 10 b+  showsPrec1 d (Lam ps b) = showParen (d > 10) $ showString "Lam " . showsPrec1 11 ps . showChar ' ' . showsPrec1 11 b+  showsPrec1 d (Let bs b) = showParen (d > 10) $ showString "Let " . showsPrec1 11 bs . showChar ' ' . showsPrec1 11 b++{-+instance Eq1 f => Eq1 (Alt f) where+  Alt p s ==# Alt q t = eqPat p q && s == unsafeCoerce t++instance (Eq1 f, Eq a) => Eq (Alt f) where (==) = (==#)++instance Show1 f => Show1 (Alt f) where+  showsPrec d (Alt p s) = showsPrec d (Alt p s)+-}+++-- * smart lam++-- ** smart patterns++data P a = forall b. P (Pat b Exp a) [a] (a -> Maybe (Path b))++varp :: Eq a => a -> P a+varp a = P VarP [a] (\v -> if a == v then Just V else Nothing)++wildp :: P a+wildp = P WildP [] (const Nothing)++asp :: Eq a => a -> P a -> P a+asp a (P p as f) = P (AsP p) (a:as) $ \v -> case f v of+  Just b              -> Just (R b)+  Nothing | a == v    -> Just L+          | otherwise -> Nothing++data Ps a = forall bs. Ps (Pats bs Exp a) [a] (a -> Maybe (MPath bs))++conp :: String -> [P a] -> P a+conp g ps = case go ps of+  Ps qs as f -> P (ConP g qs) as (fmap C . f)+  where+    go :: [P a] -> Ps a+    go [] = Ps NilP [] (const Nothing)+    go (P p as f : xs) = case go xs of+      Ps ps ass g -> Ps (p :> ps) (as ++ ass) $ \v ->+        T <$> g v <|> H <$> f v++-- * smart lam+lam :: P a -> Exp a -> Exp a+lam (P p _ f) t = Lam p (abstract f t)++-- * smart let+let_ :: Eq a => [(a, Exp a)] -> Exp a -> Exp a+let_ bs b = Let (Vector.fromList $ map (abstr . snd) bs) (abstr b)+  where vs  = map fst bs+        abstr = abstract (`List.elemIndex` vs)++-- * Pat++-- ** A Kind of Shape++eqPat :: (Eq1 f, Eq a) => Pat b f a -> Pat b' f a -> Bool+eqPat VarP        VarP        = True+eqPat WildP       WildP       = True+eqPat (AsP p)     (AsP q)     = eqPat p q+eqPat (ConP g ps) (ConP h qs) = g == h  && eqPats ps qs+eqPat (ViewP e p) (ViewP f q) = e ==# f && eqPat p q++instance Eq1 f   => Eq1 (Pat b f)        where (==#) = eqPat+instance (Eq1 f, Eq a) => Eq (Pat b f a) where (==) = eqPat++instance Show1 f => Show1 (Pat b f) where showsPrec1 = showsPrec+instance (Show1 f, Show a) => Show (Pat b f a) where+  showsPrec _ VarP        = showString "VarP"+  showsPrec _ WildP       = showString "WildP"+  showsPrec d (AsP p)     = showParen (d > 10) $ showString "AsP " . showsPrec 11 p+  showsPrec d (ConP g ps) = showParen (d > 10) $ showString "ConP " . showsPrec 11 g . showChar ' ' . showsPrec 11 ps+  showsPrec d (ViewP e p) = showParen (d > 10) $ showString "ViewP " . showsPrec1 11 e . showChar ' ' . showsPrec 11 p++instance Functor f => Functor (Pat b f) where+  fmap _ VarP = VarP+  fmap _ WildP = WildP+  fmap f (AsP p) = AsP (fmap f p)+  fmap f (ConP g ps) = ConP g (fmap f ps)+  fmap f (ViewP e p) = ViewP (fmap f e) (fmap f p)++instance Foldable f => Foldable (Pat b f) where+  foldMap f (AsP p)     = foldMap f p+  foldMap f (ConP g ps) = foldMap f ps+  foldMap f (ViewP e p) = foldMap f e `mappend` foldMap f p+  foldMap _ _           = mempty++instance Traversable f => Traversable (Pat b f) where+  traverse _ VarP = pure VarP+  traverse _ WildP = pure WildP+  traverse f (AsP p) = AsP <$> traverse f p+  traverse f (ConP g ps) = ConP g <$> traverse f ps+  traverse f (ViewP e p) = ViewP <$> traverse f e <*> traverse f p++instance Bound (Pat b) where+  VarP      >>>= _ = VarP+  WildP     >>>= _ = WildP+  AsP p     >>>= f = AsP (p >>>= f)+  ConP g ps >>>= f = ConP g (ps >>>= f)+  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+eqPats _         _         = False++instance Eq1 f         => Eq1 (Pats bs f)   where (==#) = eqPats+instance (Eq1 f, Eq a) => Eq  (Pats bs f a) where (==)  = eqPats++instance (Show1 f, Show a) => Show (Pats bs f a) where showsPrec = showsPrec1+instance Show1 f => Show1 (Pats bs f) where+  showsPrec1 _ NilP      = showString "NilP"+  showsPrec1 d (p :> ps) = showParen (d > 5) $+    showsPrec1 6 p . showString " :> " . showsPrec1 5 ps++instance Functor f => Functor (Pats bs f) where+  fmap _ NilP = NilP+  fmap f (p :> ps) = fmap f p :> fmap f ps++instance Foldable f => Foldable (Pats bs f) where+  foldMap f (p :> ps) = foldMap f p `mappend` foldMap f ps+  foldMap _ _    = mempty++instance Traversable f => Traversable (Pats bs f) where+  traverse f NilP = pure NilP+  traverse f (p :> ps) = (:>) <$> traverse f p <*> traverse f ps++instance Bound (Pats bs) where+  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+eqMPath _     _     = False+instance Eq (MPath is) where (==) = eqMPath++compareMPath :: MPath is -> MPath js -> Ordering+compareMPath (H m) (H n) = comparePath m n+compareMPath (H _) (T _) = LT+compareMPath (T p) (T q) = compareMPath p q+compareMPath (T _) (H _) = GT+instance Ord (MPath is) where compare = compareMPath++instance Show (MPath is) where+  showsPrec d (H m) = showParen (d > 10) $ showString "H " . showsPrec 11 m+  showsPrec d (T p) = showParen (d > 10) $ showString "T " . showsPrec 11 p++-- instance Read (MPath is)++-- ** Path into Pat+++eqPath :: Path i -> Path j -> Bool+eqPath V     V     = True+eqPath L     L     = True+eqPath (R m) (R n) = eqPath m n+eqPath (C p) (C q) = eqMPath p q+eqPath _     _     = False++instance Eq (Path i) where (==) = eqPath++comparePath :: Path i -> Path j -> Ordering+comparePath V     V     = EQ+comparePath V     _     = LT+comparePath L     V     = GT+comparePath L     L     = EQ+comparePath L     _     = LT+comparePath (R _) V     = GT+comparePath (R _) L     = GT+comparePath (R m) (R n) = comparePath m n+comparePath (R _) (C _) = LT+comparePath (C p) (C q) = compareMPath p q+comparePath (C _) _     = GT++instance Ord (Path i) where+  compare V     V     = EQ+  compare L     L     = EQ+  compare L     _     = LT+  compare (R _) L     = GT+  compare (R m) (R n) = compare m n+  compare (C p) (C q) = compare p q++instance Show (Path i) where+  showsPrec _ V     = showString "V"+  showsPrec _ L     = showString "L"+  showsPrec d (R m) = showParen (d > 10) $ showString "R " . showsPrec 11 m+  showsPrec d (C p) = showParen (d > 10) $ showString "C " . showsPrec 11 p++

+ examples/Simple.hs view

@@ -0,0 +1,52 @@+module Simple where++import Data.Foldable+import Data.Traversable+import Control.Monad+import Control.Applicative+import Prelude hiding (foldr)+import Prelude.Extras+import Bound++-- \ x -> x+-- ghci> lam "x" (Var "x")+-- Lam (Var (Bound ()))++-- \ x -> x y+-- ghci> lam "x" (Var "x" :@ Var "y")+-- Lam (Var (Bound ()) :@ Var (Free (Var "y")))++-- \ y -> \x -> x y+-- ghci> lam "y" (lam "x" (Var "x" :@ Var "y"))+-- Lam (Lam (Var (Bound ()) :@ Var (Free (Var (Bound ())))))++infixl 9 :@++data Exp a = Var a | Exp a :@ Exp a | Lam (Scope () Exp a)+  deriving (Eq,Ord,Show,Read)+++lam :: Eq a => a -> Exp a -> Exp a+lam v b = Lam (abstract1 v b)++instance Eq1 Exp      where (==#)      = (==)+instance Ord1 Exp     where compare1   = compare+instance Show1 Exp    where showsPrec1 = showsPrec+instance Read1 Exp    where readsPrec1 = readsPrec+instance Functor Exp  where fmap       = fmapDefault+instance Foldable Exp where foldMap    = foldMapDefault++instance Applicative Exp where+  pure  = Var+  (<*>) = ap++instance Traversable Exp where+  traverse f (Var a)  = Var <$> f a+  traverse f (x :@ y) = (:@) <$> traverse f x <*> traverse f y+  traverse f (Lam e)  = Lam <$> traverse f e++instance Monad Exp where+  return         = Var+  Var a    >>= f = f a+  (x :@ y) >>= f = (x >>= f) :@ (y >>= f)+  Lam e    >>= f = Lam (e >>>= f)