packages feed

unbound (empty) → 0.2

raw patch · 33 files changed

+6645/−0 lines, 33 filesdep +RepLibdep +basedep +containerssetup-changed

Dependencies added: RepLib, base, containers, mtl, transformers

Files

+ LICENSE view
@@ -0,0 +1,30 @@+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.
+ README view
@@ -0,0 +1,12 @@+-----------------------------------------------------------------------------+-- +-- Copyright   :  (c) 2010-2011, Unbound team (see LICENSE)+-- License     :  BSD3+-- +-- Maintainer  :  sweirich@cis.upenn.edu, byorgey@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+-- See http://code.google.com/p/replib/ for more information.+-----------------------------------------------------------------------------+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Unbound/LocallyNameless.hs view
@@ -0,0 +1,93 @@+
+----------------------------------------------------------------------
+-- |
+-- Module      :  Unbound.LocallyNameless
+-- License     :  BSD-like (see LICENSE)
+--
+-- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>
+-- Stability   :  experimental
+-- Portability :  non-portable (-XKitchenSink)
+--
+-- A generic implementation of name binding functions using a locally
+-- nameless representation.  Datatypes with binding can be defined
+-- using the 'Name' and 'Bind' types.  Expressive patterns for binding
+-- come from the 'Embed' and 'Rebind' types.
+--
+-- Important classes are:
+--
+--   * 'Alpha' -- the class of types and patterns that include binders,
+--
+--   * 'Subst' -- for subtitution functions.
+--
+-- Name generation is controlled via monads which implement the
+-- 'Fresh' and 'LFresh' classes.
+----------------------------------------------------------------------
+
+module Unbound.LocallyNameless
+  ( -- * Basic types
+    Name, AnyName(..), Bind, Embed(..), Rebind, Rec, TRec, Shift(..),
+
+    -- ** Utilities
+    integer2Name, string2Name, s2n, makeName,
+    name2Integer, name2String, anyName2Integer, anyName2String,
+    name1,name2,name3,name4,name5,name6,name7,name8,name9,name10,
+    translate,
+
+    -- * The 'Alpha' class
+    Alpha(..),
+    swaps, swapsEmbeds, swapsBinders,
+    aeq, aeqBinders,
+    acompare,
+
+    -- * Variable calculations
+    Collection(..), Multiset(..),
+    fv, fvAny, patfv, patfvAny, binders, bindersAny,
+
+    -- * Binding operations
+    bind, unsafeUnbind,
+
+    -- * The 'Fresh' class
+    Fresh(..), freshen,
+    unbind, unbind2, unbind3,
+
+    FreshM, runFreshM,
+    FreshMT, runFreshMT,
+
+    -- * The 'LFresh' class
+    LFresh(..),
+    lfreshen,
+    lunbind, lunbind2, lunbind3,
+
+    LFreshM, runLFreshM, getAvoids,
+    LFreshMT, runLFreshMT,
+
+    -- * Rebinding operations
+    rebind, unrebind,
+
+    -- * Rec operations
+    rec, unrec,
+    trec, untrec, luntrec,
+
+    -- XXX export embed, unembed, shift, unshift.
+    -- XXX should embed/unembed work for Shifts as well?
+
+    -- * Substitution
+    Subst(..), SubstName(..),
+
+    -- * Pay no attention to the man behind the curtain
+    -- $paynoattention
+    rName, rBind, rRebind, rEmbed, rRec, rShift
+) where
+
+import Unbound.LocallyNameless.Name
+import Unbound.LocallyNameless.Fresh
+import Unbound.LocallyNameless.Types
+import Unbound.LocallyNameless.Alpha
+import Unbound.LocallyNameless.Subst
+import Unbound.LocallyNameless.Ops
+import Unbound.Util
+
+-- $paynoattention
+-- These type representation objects are exported so they can be
+-- referenced by auto-generated code.  Please pretend they do not
+-- exist.
+ Unbound/LocallyNameless/Alpha.hs view
@@ -0,0 +1,794 @@+{-# LANGUAGE RankNTypes
+           , FlexibleContexts
+           , GADTs
+  #-}
+
+----------------------------------------------------------------------
+-- |
+-- Module      :  Unbound.LocallyNameless.Alpha
+-- License     :  BSD-like (see LICENSE)
+--
+----------------------------------------------------------------------
+
+module Unbound.LocallyNameless.Alpha where
+
+import Generics.RepLib hiding (GT)
+import Unbound.PermM
+import Unbound.LocallyNameless.Types
+import Unbound.LocallyNameless.Fresh
+import Unbound.Util
+
+import Data.List (intersect)
+import Data.Maybe (isJust)
+
+import Data.Monoid
+
+------------------------------------------------------------
+-- Overview
+--
+-- We have two classes of types:
+--    Terms (which contain variables) and
+--    Patterns (which contain binders)
+--
+-- Terms include
+--    Names
+--    Bind p t when p is a Pattern and t is a Term
+--    Standard type constructors (Unit, (,), Maybe, [], etc)
+--
+-- Patterns include
+--    Names
+--    Embed t when t is a Term
+--    Rebind p q when p and q are both Patterns
+--    Rec p when p is a pattern
+--    Shift a when a is an Embed or some number of Shifts wrapped around Embed
+--    Standard type constructors (Unit, (,), Maybe, [], etc)
+--
+-- Terms support a number of operations, including alpha-equivalence,
+-- free variables, swapping, etc.  Because Patterns occur in terms, so
+-- they too support the same operations, but only for the annotations
+-- inside them.
+-- Therefore, both Terms and Patterns are instances of the "Alpha" type class
+-- which lists these operations.  However, some types (such as [Name])
+-- are both Terms and Patterns, and the behavior of the operations
+-- is different when we use [Name] as a term and [Name] as a pattern.
+-- Therefore, we index each of the operations with a mode that tells us
+-- what version we should be defining.
+--
+-- [SCW: could we use multiparameter type classes? Alpha m t]
+--
+-- Patterns also support a few extra operations that Terms do not
+-- for dealing with the binding variables.
+--     These are used to find the index of names inside patterns.
+------------------------------------------------------------
+
+------------------------------------------------------------
+-- The Alpha class
+------------------------------------------------------------
+
+-- | The 'Alpha' type class is for types which may contain names.  The
+--   'Rep1' constraint means that we can only make instances of this
+--   class for types that have generic representations (which can be
+--   automatically derived by RepLib.)
+--
+--   Note that the methods of 'Alpha' should never be called directly!
+--   Instead, use other methods provided by this module which are
+--   defined in terms of 'Alpha' methods. (The only reason they are
+--   exported is to make them available to automatically-generated
+--   code.)
+--
+--   Most of the time, the default definitions of these methods will
+--   suffice, so you can make an instance for your data type by simply
+--   declaring
+--
+--   > instance Alpha MyType
+--
+class (Show a, Rep1 AlphaD a) => Alpha a where
+
+  -- | See 'swaps'.
+  swaps' :: AlphaCtx -> Perm AnyName -> a -> a
+  swaps' = swapsR1 rep1
+
+  -- | See 'fv'.
+  fv' :: Collection f => AlphaCtx -> a -> f AnyName
+  fv' = fvR1 rep1
+
+  -- | See 'lfreshen'.
+  lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
+  lfreshen' = lfreshenR1 rep1
+
+  -- | See 'freshen'.
+  freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
+  freshen' = freshenR1 rep1
+
+  -- | See 'aeq'.
+  aeq' :: AlphaCtx -> a -> a -> Bool
+  aeq' = aeqR1 rep1
+
+{-
+  -- | See 'match'.
+  match'   :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)
+  match'   = matchR1 rep1
+-}
+
+  -- | Replace free names by bound names.
+  close :: Alpha b => AlphaCtx -> b -> a -> a
+  close = closeR1 rep1
+
+  -- | Replace bound names by free names.
+  open :: Alpha b => AlphaCtx -> b -> a -> a
+  open = openR1 rep1
+
+  -- | See 'acompare'.
+  acompare' :: AlphaCtx -> a -> a -> Ordering
+  acompare' = acompareR1 rep1
+
+  -- | @isPat x@ dynamically checks whether @x@ can be used as a valid
+  --   pattern.  The default instance returns @True@ if at all
+  --   possible.
+  isPat :: a -> Maybe [AnyName]
+  isPat = isPatR1 rep1
+
+  -- | @isTerm x@ dynamically checks whether @x@ can be used as a
+  --   valid term. The default instance returns @True@ if at all
+  --   possible.
+  isTerm :: a -> Bool
+  isTerm = isTermR1 rep1
+
+  -- | @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
+  ---------------- PATTERN OPERATIONS ----------------------------
+
+  -- | @'nthpatrec' p n@ looks up the @n@th name in the pattern @p@
+  -- (zero-indexed), returning the number of names encountered if not
+  -- found.
+  nthpatrec :: a -> NthCont
+  nthpatrec = nthpatR1 rep1
+
+  -- | Find the (first) index of the name in the pattern if one
+  --   exists; otherwise, return the number of names encountered
+  --   instead.
+  findpatrec :: a -> AnyName -> FindResult
+  findpatrec = findpatR1 rep1
+
+------------------------------------------------------------
+--  Pattern operation internals
+------------------------------------------------------------
+
+-- | The result of a 'findpatrec' operation.
+data FindResult = Index Integer      -- ^ The (first) index of the name we
+                                     --   sought
+                | NamesSeen Integer  -- ^ We haven't found the name
+                                     --   (yet), but have seen this many
+                                     --   others while looking for it
+  deriving (Eq, Ord, Show)
+
+-- | @FindResult@ forms a monoid which combines information from
+--   several 'findpatrec' operations.  @mappend@ takes the leftmost
+--   'Index', and combines the number of names seen to the left of it
+--   so we can correctly compute its global index.
+instance Monoid FindResult where
+  mempty = NamesSeen 0
+  NamesSeen i `mappend` NamesSeen j = NamesSeen (i + j)
+  NamesSeen i `mappend` Index j     = Index (i + j)
+  Index j     `mappend` _           = Index j
+
+-- | Find the (first) index of the name in the pattern, if it exists.
+findpat :: Alpha a => a -> AnyName -> Maybe Integer
+findpat x n = case findpatrec x n of
+                   Index i     -> Just i
+                   NamesSeen _ -> Nothing
+
+
+-- | The result of an 'nthpatrec' operation.
+data NthResult = Found AnyName    -- ^ The name found at the given
+                                  --   index.
+               | CurIndex Integer -- ^ We haven't yet reached the
+                                  --   required index; this is the
+                                  --   index into the remainder of the
+                                  --   pattern (which decreases as we
+                                  --   traverse the pattern).
+
+-- | A continuation which takes the remaining index and searches for
+--   that location in a pattern, yielding a name or a remaining index
+--   if the end of the pattern was reached too soon.
+newtype NthCont = NthCont { runNthCont :: Integer -> NthResult }
+
+-- | @NthCont@ forms a monoid: function composition which
+--   short-circuits once a result is found.
+instance Monoid NthCont where
+  mempty = NthCont $ \i -> CurIndex i
+  (NthCont f) `mappend` (NthCont g)
+    = NthCont $ \i -> case f i of
+                        Found n     -> Found n
+                        CurIndex i' -> g i'
+
+-- | If we see a name, check whether the index is 0: if it is, we've
+--   found the name we're looking for, otherwise continue with a
+--   decremented index.
+nthName :: AnyName -> NthCont
+nthName nm = NthCont $ \i -> if i == 0
+                               then Found nm
+                               else CurIndex (i-1)
+
+-- | @'nthpat' b n@ looks up up the @n@th name in the pattern @b@
+-- (zero-indexed).  PRECONDITION: the number of names in the pattern
+-- must be at least @n@.
+nthpat :: Alpha a => a -> Integer -> AnyName
+nthpat x i = case runNthCont (nthpatrec x) i of
+                 CurIndex j -> error
+                   ("BUG: pattern index " ++ show i ++
+                    " out of bounds by " ++ show j ++ "in" ++ show x)
+                 Found nm   -> nm
+
+------------------------------------------------------------
+--  AlphaCtx
+------------------------------------------------------------
+
+-- An AlphaCtx records the current mode (Term/Pat) and current level,
+-- and gets passed along during operations which need to keep track of
+-- the mode and/or level.
+
+-- | Many of the operations in the 'Alpha' class take an 'AlphaCtx':
+-- stored information about the iteration as it progresses. This type
+-- is abstract, as classes that override these operations should just pass
+-- the context on.
+data AlphaCtx = AC { mode :: Mode , level :: Integer }
+
+initial :: AlphaCtx
+initial = AC Term 0
+
+incr :: AlphaCtx -> AlphaCtx
+incr c = c { level = level c + 1 }
+
+decr :: AlphaCtx -> AlphaCtx
+decr c = if level c == 0 then error "Too many outers"
+         else c { level = level c - 1 }
+
+
+pat  :: AlphaCtx -> AlphaCtx
+pat c  = c { mode = Pat }
+
+term  :: AlphaCtx -> AlphaCtx
+term c  = c { mode = Term }
+
+-- | A mode is basically a flag that tells us whether we should be
+--   looking at the names in the term, or if we are in a pattern and
+--   should /only/ be looking at the names in the annotations. The
+--   standard mode is to use 'Term'; many functions do this by default.
+data Mode = Term | Pat deriving (Show, Eq, Read)
+
+-- | Open a term using the given pattern.
+openT :: (Alpha p, Alpha t) => p -> t -> t
+openT = open initial
+
+-- | @openP p1 p2@ opens the pattern @p2@ using the pattern @p1@.
+openP :: (Alpha p1, Alpha p2) => p1 -> p2 -> p2
+openP = open (pat initial)
+
+-- | Close a term using the given pattern.
+closeT :: (Alpha p, Alpha t) => p -> t -> t
+closeT = close initial
+
+-- | @closeP p1 p2@ closes the pattern @p2@ using the pattern @p1@.
+closeP :: (Alpha p1, Alpha p2) => p1 -> p2 -> p2
+closeP = close (pat initial)
+
+-- | Class constraint hackery to allow us to override the default
+--   definitions for certain classes.  'AlphaD' is essentially a
+--   reified dictionary for the 'Alpha' class.
+data AlphaD a = AlphaD {
+  isPatD    :: a -> Maybe [AnyName],
+  isTermD   :: a -> Bool,
+  isEmbedD  :: a -> Bool,
+  swapsD    :: AlphaCtx -> Perm AnyName -> a -> a,
+  fvD       :: Collection f => AlphaCtx -> a -> f AnyName,
+  freshenD  :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName),
+  lfreshenD :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b,
+  aeqD      :: AlphaCtx -> a -> a -> Bool,
+  -- matchD    :: AlphaCtx -> a -> a -> Maybe (Perm AnyName),
+  closeD    :: Alpha b => AlphaCtx -> b -> a -> a,
+  openD     :: Alpha b => AlphaCtx -> b -> a -> a,
+  findpatD  :: a -> AnyName -> FindResult,
+  nthpatD   :: a -> NthCont,
+  acompareD :: AlphaCtx -> a -> a -> Ordering
+  }
+
+instance Alpha a => Sat (AlphaD a) where
+  dict = AlphaD isPat isTerm isEmbed swaps' fv' freshen' lfreshen' aeq' -- match'
+           close open findpatrec nthpatrec acompare'
+
+----------------------------------------------------------------------
+-- Generic definitions for 'Alpha' methods.  (Note that all functions
+-- that take representations end in 'R1'.)
+----------------------------------------------------------------------
+
+closeR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a
+closeR1 (Data1 _ cons) = \i a d ->
+   case (findCon cons d) of
+      Val c rec kids ->
+        to c (map_l (\z -> closeD z i a) rec kids)
+closeR1 _               = \_ _ d -> d
+
+
+openR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a
+openR1 (Data1 _ cons) = \i a d ->
+   case (findCon cons d) of
+      Val c rec kids ->
+        to c (map_l (\z -> openD z i a) rec kids)
+openR1 _               = \_ _ d -> d
+
+
+swapsR1 :: R1 AlphaD a -> AlphaCtx -> Perm AnyName -> a -> a
+swapsR1 (Data1 _ cons)  = \ p x d ->
+  case (findCon cons d) of
+    Val c rec kids -> to c (map_l (\z -> swapsD z p x) rec kids)
+swapsR1 _               = \ _ _ d -> d
+
+
+fvR1 :: Collection f => R1 (AlphaD) a -> AlphaCtx -> a -> f AnyName
+fvR1 (Data1 _ cons) = \ p  d ->
+  case (findCon cons d) of
+    Val _ rec kids -> fv1 rec p kids
+fvR1 _ = \ _ _ -> emptyC
+
+fv1 :: Collection f => MTup (AlphaD) l -> AlphaCtx -> l -> f AnyName
+fv1 MNil _ Nil = emptyC
+fv1 (r :+: rs) p (p1 :*: t1) =
+   fvD r p p1 `union` fv1 rs p t1
+
+{-
+matchR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)
+matchR1 (Data1 _ cons) = loop cons where
+   loop (Con emb reps : rest) p x y =
+     case (from emb x, from emb y) of
+      (Just p1, Just p2) -> match1 reps p p1 p2
+      (Nothing, Nothing) -> loop rest p x y
+      (_,_)              -> Nothing
+   loop [] _ _ _ = error "Impossible"
+matchR1 Int1 = \ _ x y -> if x == y then Just empty else Nothing
+matchR1 Integer1 = \ _ x y -> if x == y then Just empty else Nothing
+matchR1 Char1 = \ _ x y -> if x == y then Just empty else Nothing
+matchR1 _ = \ _ _ _ -> Nothing
+
+match1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Maybe (Perm AnyName)
+match1 MNil _ Nil Nil = Just empty
+match1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) = do
+  l1 <- matchD r c p1 p2
+  l2 <- match1 rs c t1 t2
+  (l1 `join` l2)
+-}
+
+aeqR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Bool
+aeqR1 (Data1 _ cons) = loop cons where
+   loop (Con emb reps : rest) p x y =
+     case (from emb x, from emb y) of
+      (Just p1, Just p2) -> aeq1 reps p p1 p2
+      (Nothing, Nothing) -> loop rest p x y
+      (_,_)              -> False
+   loop [] _ _ _ = error "Impossible"
+aeqR1 Int1     = \ _ x y ->  x == y
+aeqR1 Integer1 = \ _ x y -> x == y
+aeqR1 Char1    = \ _ x y -> x == y
+aeqR1 _        = \ _ _ _ -> False
+
+aeq1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Bool
+aeq1 MNil _ Nil Nil = True
+aeq1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) = do
+  aeqD r c p1 p2 && aeq1 rs c t1 t2
+
+freshenR1 :: Fresh m => R1 (AlphaD) a -> AlphaCtx -> a -> m (a,Perm AnyName)
+freshenR1 (Data1 _ cons) = \ p d ->
+   case findCon cons d of
+     Val c rec kids -> do
+       (l, p') <- freshenL rec p kids
+       return (to c l, p')
+freshenR1 _ = \ _ n -> return (n, empty)
+
+freshenL :: Fresh m => MTup (AlphaD) l -> AlphaCtx -> l -> m (l, Perm AnyName)
+freshenL MNil _ Nil = return (Nil, empty)
+freshenL (r :+: rs) p (t :*: ts) = do
+  (xs, p2) <- freshenL rs p ts
+  (x, p1) <- freshenD r p (swapsD r p p2 t)
+  return ( x :*: xs, p1 <> p2)
+
+lfreshenR1 :: LFresh m => R1 AlphaD a -> AlphaCtx -> a ->
+              (a -> Perm AnyName -> m b) -> m b
+lfreshenR1 (Data1 _ cons) = \p d f ->
+   case findCon cons d of
+     Val c rec kids -> lfreshenL rec p kids (\ l p' -> f (to c l) p')
+lfreshenR1 _ = \ _ n f -> f n empty
+
+lfreshenL :: LFresh m => MTup (AlphaD) l -> AlphaCtx -> l ->
+              (l -> Perm AnyName -> m b) -> m b
+lfreshenL MNil _ Nil f = f Nil empty
+lfreshenL (r :+: rs) p (t :*: ts) f =
+  lfreshenL rs p ts ( \ y p2 ->
+  lfreshenD r p (swapsD r p p2 t) ( \ x p1 ->
+     f (x :*: y) (p1 <> p2)))
+
+
+findpatR1 :: R1 AlphaD b -> b -> AnyName -> FindResult
+findpatR1 (Data1 dt cons) = \ d n ->
+   case findCon cons d of
+     Val c rec kids -> findpatL rec kids n
+findpatR1 _ = \ x n -> mempty
+
+findpatL :: MTup AlphaD l -> l -> AnyName -> FindResult
+findpatL MNil Nil n              = mempty
+findpatL (r :+: rs) (t :*: ts) n = findpatD r t n <> findpatL rs ts n
+
+nthpatR1 :: R1 AlphaD b -> b -> NthCont
+nthpatR1 (Data1 dt cons) = \ d ->
+   case findCon cons d of
+     Val c rec kids -> nthpatL rec kids
+nthpatR1 _ = \ x -> mempty
+
+nthpatL :: MTup AlphaD l -> l -> NthCont
+nthpatL MNil Nil              = mempty
+nthpatL (r :+: rs) (t :*: ts) = nthpatD r t <> nthpatL rs ts
+
+combine :: Maybe [AnyName] -> Maybe [AnyName] -> Maybe [AnyName]
+combine (Just ns1) (Just ns2) | ns1 `intersect` ns2 == [] =
+                                  Just (ns1 ++ ns2)
+combine _ _ = Nothing
+
+isPatR1 :: R1 AlphaD b -> b -> Maybe [AnyName]
+isPatR1 (Data1 dt cons) = \ d ->
+   case findCon cons d of
+     Val c rec kids ->
+       foldl_l (\ c b a -> combine (isPatD c a) b) (Just []) rec kids
+isPatR1 _ = \ d -> Just []
+
+isTermR1 :: R1 AlphaD b -> b -> Bool
+isTermR1 (Data1 dt cons) = \ d ->
+   case findCon cons d of
+     Val c rec kids -> foldl_l (\ c b a -> isTermD c a && b) True rec kids
+isTermR1 _ = \ d -> True
+
+-- Exactly like the generic Ord instance defined in Generics.RepLib.PreludeLib,
+-- except that the comparison operation takes an AlphaCtx
+
+acompareR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Ordering
+acompareR1 Int1  c = \x y -> compare x y
+acompareR1 Char1 c = \x y -> compare x y
+acompareR1 (Data1 str cons) c = \x y ->
+             let loop (Con emb rec : rest) =
+                     case (from emb x, from emb y) of
+                        (Just t1, Just t2) -> compareTupM rec c t1 t2
+                        (Just t1, Nothing) -> LT
+                        (Nothing, Just t2) -> GT
+                        (Nothing, Nothing) -> loop rest
+             in loop cons
+acompareR1 r1 c = error ("compareR1 not supported for " ++ show r1)
+
+lexord         :: Ordering -> Ordering -> Ordering
+lexord LT ord  =  LT
+lexord EQ ord  =  ord
+lexord GT ord  =  GT
+
+compareTupM :: MTup AlphaD l -> AlphaCtx -> l -> l -> Ordering
+compareTupM MNil c Nil Nil = EQ
+compareTupM (x :+: xs) c (y :*: ys) (z :*: zs) =
+   lexord (acompareD x c y z) (compareTupM xs c ys zs)
+
+
+------------------------------------------------------------
+-- Specific Alpha instances for the binding combinators:
+--      Name, Bind, Embed, Rebind, Rec, Shift
+-----------------------------------------------------------
+
+-- In the Name instance, if the mode is Term then the operation
+-- observes the name. In Pat mode the name is a binder, so the name is
+-- usually ignored.
+instance Rep a => Alpha (Name a) where
+
+  -- Both bound and free names are valid terms.
+  isTerm _ = True
+
+  -- Only free names are valid as patterns, which serve as binders.
+  isPat n@(Nm _ _) = Just [AnyName n]
+  isPat _          = Nothing
+
+  fv' c n@(Nm _ _)  | mode c == Term = singleton (AnyName n)
+  fv' _ _                            = emptyC
+
+  swaps' c p x | mode c == Term =
+                     case apply p (AnyName x) of
+                       AnyName y ->
+                         case gcastR (getR y) (getR x) y of
+                           Just y' -> y'
+                           Nothing -> error "Internal error in swaps': sort mismatch"
+  swaps' c p x | mode c == Pat  = x
+
+  aeq' _ x y   | x == y         = True
+  aeq' c n1 n2 | mode c == Term = False
+  aeq' c _ _   | mode c == Pat  = True
+
+{-
+  match' _ x  y   | x == y         = Just empty
+  match' c n1 n2  | mode c == Term = Just $ single (AnyName n1) (AnyName n2)
+  match' c _ _    | mode c == Pat  = Just empty
+-}
+
+  freshen' c nm | mode c == Pat  = do x <- fresh nm
+                                      return (x, single (AnyName nm) (AnyName x))
+  freshen' c nm | mode c == Term = error "freshen' on Name in Term mode"
+
+  lfreshen' c nm f = case mode c of
+     Pat  -> do x <- lfresh nm
+                avoid [AnyName x] $ f x (single (AnyName nm) (AnyName x))
+     Term -> error "lfreshen' on Name in Term mode"
+
+  open c a (Bn r j x) | mode c == Term && level c == j =
+    case nthpat a x of
+      AnyName nm -> case gcastR (getR nm) r nm of
+        Just nm' -> nm'
+        Nothing  -> error "Internal error in open: sort mismatch"
+  open _ _ n = n
+
+  close c a nm@(Nm r n) | mode c == Term =
+      case findpat a (AnyName nm) of
+        Just x  -> Bn r (level c) x
+        Nothing -> nm
+  close _ _ n = n
+
+  findpatrec nm1 (AnyName nm2) =
+    case gcastR (getR nm1) (getR nm2) nm1 of
+      Just nm1' -> if nm1' == nm2 then Index 0 else NamesSeen 1
+      Nothing   -> NamesSeen 1
+
+  nthpatrec = nthName . AnyName
+
+  acompare' c (Nm r1 n1)    (Nm r2 n2)
+    | mode c == Term = lexord (compare r1 r2) (compare n1 n2)
+
+  acompare' c (Bn r1 m1 n1) (Bn r2 m2 n2)
+    | mode c == Term = lexord (compare r1 r2) (lexord (compare m1 m2) (compare n1 n2))
+
+  acompare' c (Nm _ _)   (Bn _ _ _) | mode c == Term = LT
+  acompare' c (Bn _ _ _) (Nm _ _)   | mode c == Term = GT
+  acompare' c _          _          | mode c == Pat = EQ
+
+instance Alpha AnyName  where
+
+  isTerm _ = True
+
+  isPat n@(AnyName (Nm _ _)) = Just [n]
+  isPat _                    = Nothing
+
+  fv' c n@(AnyName (Nm _ _))  | mode c == Term = singleton n
+  fv' _ _                                      = emptyC
+
+  swaps' c p x = case mode c of
+                   Term -> apply p x
+                   Pat  -> x
+
+  aeq' _ x y | x == y         = True
+  aeq' c _ _ | mode c == Term = False
+  aeq' c _ _ | mode c == Pat  = True
+
+{-
+  match' _ x y | x == y          = Just empty
+  match' c (AnyName n1) (AnyName n2)
+    | mode c == Term =
+      case gcastR (getR n1) (getR n2) n1 of
+        Just n1' -> Just $ single (AnyName n1) (AnyName n2)
+        Nothing  -> Nothing
+  match' c _ _           | mode c == Pat   = Just empty
+-}
+
+  acompare' _ x y | x == y          = EQ
+  acompare' c (AnyName n1) (AnyName n2)
+    | mode c == Term =
+      case compareR (getR n1) (getR n2) of
+       EQ ->  case gcastR (getR n1) (getR n2) n1 of
+          Just n1' -> acompare' c n1' n2
+          Nothing  -> error "impossible"
+       otherwise -> otherwise
+  acompare' c _ _           | mode c == Pat   = EQ
+
+
+  freshen' c (AnyName nm) = case mode c of
+     Pat  -> do x <- fresh nm
+                return (AnyName x, single (AnyName nm) (AnyName x))
+     Term -> error "freshen' on AnyName in Term mode"
+
+  lfreshen' c (AnyName nm) f = case mode c of
+     Pat  -> do x <- lfresh nm
+                avoid [AnyName x] $ f (AnyName x) (single (AnyName nm) (AnyName x))
+     Term -> error "lfreshen' on AnyName in Term mode"
+
+  open c a (AnyName (Bn _ j x)) | level c == j = nthpat a x
+  open _ _ n = n
+
+  close c a nm@(AnyName (Nm r n)) =
+    case findpat a nm of
+      Just x  -> AnyName (Bn r (level c) x)
+      Nothing -> nm
+
+  close _ _ n = n
+
+  findpatrec nm1 nm2 | nm1 == nm2 = Index 0
+  findpatrec _ _ = NamesSeen 1
+
+  nthpatrec = nthName
+
+instance (Alpha p, Alpha t) => Alpha (Bind p t) where
+    isPat _ = Nothing
+    isTerm (B p t) = isJust (isPat p) && isTerm t
+
+    swaps' c pm (B p t) =
+        (B (swaps' (pat c) pm p)
+           (swaps' (incr c) pm t))
+
+    fv' c (B p t) = fv' (pat c) p `union` fv' (incr c) t
+
+    freshen' c (B p t) = do
+      (p', pm1) <- freshen' (pat c) p
+      (t', pm2) <- freshen' (incr c) (swaps' (incr c) pm1 t)
+      return (B p' t', pm1 <> pm2)
+
+    lfreshen' c (B p t) f =
+      lfreshen' (pat c) p (\ p' pm1 ->
+      lfreshen' (incr c) (swaps' (incr c) pm1 t) (\ t' pm2 ->
+      f (B p' t') (pm1 <> pm2)))
+
+    aeq' c (B p1 t1) (B p2 t2) = do
+      aeq' (pat c) p1 p2  && aeq' (incr c) t1 t2
+
+{-
+    match' c (B p1 t1) (B p2 t2) = do
+      pp <- match' (pat c) p1 p2
+      pt <- match' (incr c) t1 t2
+      -- need to make sure that all permutations of
+      -- bound variables at this
+      -- level are the identity
+      (pp `join` pt)
+-}
+
+    open  c a (B p t)    = B (open (pat c) a p)  (open  (incr c) a t)
+    close c a (B p t)    = B (close (pat c) a p) (close (incr c) a t)
+
+    --  Comparing two binding terms.
+    acompare' c (B p1 t1) (B p2 t2) =
+      lexord (acompare' (pat c) p1 p2) (acompare' (incr c) t1 t2)
+
+    findpatrec _ b = error $ "Binding " ++ show b ++ " used as a pattern"
+    nthpatrec    b = error $ "Binding " ++ show b ++ " used as a pattern"
+
+instance (Alpha p, Alpha q) => Alpha (Rebind p q) where
+  isTerm _ = False
+  isPat (R p q) = combine (isPat p) (isPat q)
+
+  swaps' c pm (R p q) = R (swaps' c pm p) (swaps' (incr c) pm q)
+
+  fv' c (R p q) =  fv' c p `union` fv' (incr c) q
+
+  lfreshen' c (R p q) g
+    | mode c == Term = error "lfreshen' on Rebind in Term mode"
+    | otherwise =
+        lfreshen' c p $ \ p' pm1 ->
+        lfreshen' (incr c) (swaps' (incr c) pm1 q) $ \ q' pm2 ->
+        g (R p' q') (pm1 <> pm2)
+
+  freshen' c (R p q)
+    | mode c == Term = error "freshen' on Rebind in Term mode"
+    | otherwise = do
+        (p', pm1) <- freshen' c p
+        (q', pm2) <- freshen' (incr c) (swaps' (incr c) pm1 q)
+        return (R p' q', pm1 <> pm2)
+
+  aeq' c (R p1 q1) (R p2 q2 ) = do
+      aeq' c p1 p2 && aeq' c q1 q2
+
+{-
+  match' c (R p1 q1) (R p2 q2) = do
+     pp <- match' c p1 p2
+     pq <- match' (incr c)  q1 q2
+     (pp `join` pq)
+-}
+
+  acompare' c (R a1 a2) (R b1 b2) =
+      lexord (acompare' c a1 b1) (acompare' (incr c) a2 b2)
+
+
+  open c a (R p q)  = R (open c a p) (open (incr c) a q)
+  close c a (R p q) = R (close c a p) (close (incr c) a q)
+
+  findpatrec (R p q) nm = findpatrec p nm <> findpatrec q nm
+
+  nthpatrec (R p q) = nthpatrec p <> nthpatrec q
+
+
+instance Alpha p => Alpha (Rec p) where
+   {-  default defs of these work if we don't care about incrs
+
+   fv' c (Rec a) = fv' c a
+   aeq' c (Rec a) (Rec b) = aeq' c a b
+   acompare' c (Rec a) (Rec b) = acompare' c a b
+   swaps' p pm (Rec a) = Rec (swaps' p pm a)
+   findpatrec (Rec a) nm = findpatrec a nm
+   nthpatrec (Rec a)  i  = nthpatrec a i
+
+   -}
+   isPat (Rec p) = isPat p
+   isTerm _ = False
+
+   open  c a (Rec p) = Rec (open  (incr c) a p)
+   close c a (Rec p) = Rec (close (incr c) a p)
+
+
+-- note: for Embeds, when the mode is "term" then we are
+-- implementing the "binding" version of the function
+-- and we generally should treat the annots as constants
+instance Alpha t => Alpha (Embed t) where
+   isPat (Embed t)   = if (isTerm t) then Just [] else Nothing
+   isTerm t          = False
+   isEmbed (Embed t) = isTerm t
+
+   swaps' c pm (Embed t) | mode c == Pat  = Embed (swaps' (term c) pm t)
+   swaps' c pm (Embed t) | mode c == Term = Embed t
+
+   fv' c (Embed t) | mode c == Pat  = fv' (term c) t
+   fv' c _         | mode c == Term = emptyC
+
+   freshen' c p | mode c == Term = error "freshen' called on a term"
+                | otherwise      = return (p, empty)
+
+   lfreshen' c p f         | mode c == Term = error "lfreshen' called on a term"
+                           | otherwise      = f p empty
+
+   aeq' c (Embed x) (Embed y) = aeq' (term c) x y
+
+   acompare' c (Embed x) (Embed y) = acompare' (term c) x y
+
+{-
+   match' c (Embed x) (Embed y) | mode c == Pat  = match' (term c) x y
+   match' c (Embed x) (Embed y) | mode c == Term =
+                                    if x `aeq` y
+                                    then Just empty
+                                    else Nothing
+-}
+
+   close c b (Embed x) | mode c == Pat  = Embed (close (term c) b x)
+                       | mode c == Term = error "close on Embed"
+
+   open c b (Embed x) | mode c == Pat  = Embed (open (term c) b x)
+                      | mode c == Term = error "open on Embed"
+
+   findpatrec _ _ = mempty
+   nthpatrec _    = mempty
+
+instance Alpha a => Alpha (Shift a) where
+
+  -- The contents of Shift may only be an Embed or another Shift.
+  isPat (Shift a)   = if (isEmbed a) then Just [] else Nothing
+  isTerm a          = False
+  isEmbed (Shift a) = isEmbed a
+
+  close c b (Shift x) = Shift (close (decr c) b x)
+  open  c b (Shift x) = Shift (open  (decr c) b x)
+
+
+-- Instances for other types use the default definitions.
+instance Alpha Bool
+instance Alpha Float
+instance Alpha ()
+instance Alpha a => Alpha [a]
+instance Alpha Int
+instance Alpha Integer
+instance Alpha Double
+instance Alpha Char
+instance Alpha a => Alpha (Maybe 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)
+
+instance (Rep a) => Alpha (R a)
+ Unbound/LocallyNameless/Fresh.hs view
@@ -0,0 +1,284 @@+{-# LANGUAGE TypeSynonymInstances
+           , FlexibleInstances
+           , FlexibleContexts
+           , GeneralizedNewtypeDeriving
+           , OverlappingInstances
+           , MultiParamTypeClasses
+           , UndecidableInstances
+  #-}
+----------------------------------------------------------------------
+-- |
+-- Module      :  Unbound.LocallyNameless.Fresh
+-- License     :  BSD-like (see LICENSE)
+--
+-- Maintainer  :  Brent Yorgey <byorgey@cis.upenn.edu>
+-- Stability   :  experimental
+-- Portability :  unportable (GHC 7 only)
+--
+-- The 'Fresh' and 'LFresh' classes, which govern monads with fresh
+-- name generation capabilities, and the FreshM(T) and LFreshM(T)
+-- monad (transformers) which provide useful default implementations.
+----------------------------------------------------------------------
+
+module Unbound.LocallyNameless.Fresh
+  ( -- * The 'Fresh' class
+
+    Fresh(..),
+
+    FreshM(..), runFreshM, contFreshM,
+    FreshMT(..), runFreshMT, contFreshMT,
+
+    -- * The 'LFresh' class
+
+    LFresh(..),
+
+    LFreshM(..), runLFreshM, contLFreshM, getAvoids,
+    LFreshMT(..), runLFreshMT, contLFreshMT
+
+  ) where
+
+import Generics.RepLib
+import Unbound.LocallyNameless.Name
+
+import Data.Set (Set)
+import qualified Data.Set as S
+
+import Data.Monoid
+
+import Control.Monad.Reader
+import qualified Control.Monad.State as St
+import Control.Monad.Identity
+import Control.Applicative (Applicative)
+
+import Control.Monad.Trans.Cont
+import Control.Monad.Trans.Error
+import Control.Monad.Trans.Identity
+import Control.Monad.Trans.List
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Reader (ReaderT)
+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.IO.Class as IC
+
+------------------------------------------------------------
+-- Fresh
+------------------------------------------------------------
+
+-- | Type class for monads which can generate new globally unique
+--   'Name's based on a given 'Name'.
+class Monad m => Fresh m where
+  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, Monad, St.MonadState Integer, MonadPlus, MonadIO)
+
+-- | Run a 'FreshMT' computation starting in an empty context.
+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 Monad m => Fresh (FreshMT m) where
+  fresh (Nm r (s,_)) = FreshMT $ do
+    n <- St.get
+    St.put (n+1)
+    return $ Nm r (s,n)
+
+-- | 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 in an empty context.
+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
+
+-- Instances for applying monad transformers to Fresh monads
+
+instance Fresh m => Fresh (ContT r m) where
+  fresh = lift . fresh
+
+instance (Error e, Fresh m) => Fresh (ErrorT e m) where
+  fresh = lift . fresh
+
+instance Fresh m => Fresh (IdentityT m) where
+  fresh = lift . fresh
+
+instance Fresh m => Fresh (ListT m) where
+  fresh = lift . fresh
+
+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
+
+-- Instances for applying FreshMT to other monads
+
+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
+
+---------------------------------------------------
+-- LFresh
+---------------------------------------------------
+
+-- XXX todo: generalize 'avoid' to take an arbitrary term/pattern?
+-- would make the modules recursive though...
+-- | This is the class of monads that support freshness in an
+--   (implicit) local scope.  Generated names are fresh for the current
+--   local scope, but not globally fresh.
+class Monad m => LFresh m where
+  -- | Pick a new name that is fresh for the current (implicit) scope.
+  lfresh  :: Rep a => Name a -> m (Name a)
+  -- | Avoid the given names when freshening in the subcomputation.
+  avoid   :: [AnyName] -> m a -> m a
+
+-- | A simple reader monad instance for 'LFresh'.
+instance LFresh (Reader Integer) where
+  lfresh (Nm r (s,j)) = do { n <- ask; return (Nm r (s, max j (n+1))) }
+  avoid []          = id
+  avoid names       = local (max k)
+    where k = maximum (map anyName2Integer names)
+
+-- | The LFresh monad transformer.  Keeps track of a set of names to
+-- avoid, and when asked for a fresh one will choose the first unused
+-- numerical name.
+newtype LFreshMT m a = LFreshMT { unLFreshMT :: ReaderT (Set AnyName) m a }
+  deriving (Functor, Applicative, Monad, MonadReader (Set AnyName), MonadIO, MonadPlus)
+
+-- | 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
+
+-- | Get the set of names currently being avoided.
+getAvoids :: Monad m => LFreshMT m (Set AnyName)
+getAvoids = LFreshMT ask
+
+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
+
+-- | 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
+
+instance (Error e, LFresh m) => LFresh (ErrorT e m) where
+  lfresh = lift . lfresh
+  avoid  = mapErrorT . avoid
+
+instance LFresh m => LFresh (IdentityT m) where
+  lfresh = lift . lfresh
+  avoid  = mapIdentityT . avoid
+
+instance LFresh m => LFresh (ListT m) where
+  lfresh = lift . lfresh
+  avoid  = mapListT . avoid
+
+instance LFresh m => LFresh (MaybeT m) where
+  lfresh = lift . lfresh
+  avoid  = mapMaybeT . avoid
+
+instance LFresh m => LFresh (ReaderT r m) where
+  lfresh = lift . lfresh
+  avoid  = mapReaderT . avoid
+
+instance LFresh m => LFresh (Lazy.StateT s m) where
+  lfresh = lift . lfresh
+  avoid  = Lazy.mapStateT . avoid
+
+instance LFresh m => LFresh (Strict.StateT s m) where
+  lfresh = lift . lfresh
+  avoid  = Strict.mapStateT . avoid
+
+instance (Monoid w, LFresh m) => LFresh (Lazy.WriterT w m) where
+  lfresh = lift . lfresh
+  avoid  = Lazy.mapWriterT . avoid
+
+instance (Monoid w, LFresh m) => LFresh (Strict.WriterT w m) where
+  lfresh = lift . lfresh
+  avoid  = Strict.mapWriterT . avoid
+
+-- 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
+ Unbound/LocallyNameless/Name.hs view
@@ -0,0 +1,148 @@+{-# LANGUAGE RankNTypes
+           , TemplateHaskell
+           , GADTs
+           , UndecidableInstances
+           , FlexibleInstances
+           , FlexibleContexts
+           , MultiParamTypeClasses
+           , ScopedTypeVariables
+  #-}
+----------------------------------------------------------------------
+-- |
+-- Module      :  Unbound.LocallyNameless.Name
+-- License     :  BSD-like (see LICENSE)
+--
+-- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>
+-- Stability   :  experimental
+-- Portability :  XXX
+--
+-- XXX write me
+----------------------------------------------------------------------
+
+module Unbound.LocallyNameless.Name where
+-- XXX todo make explicit export list
+
+import Generics.RepLib
+
+$(derive_abstract [''R])
+-- The above only works with GHC 7.
+
+-- | 'Name's are things that get bound.  This type is intentionally
+--   abstract; to create a 'Name' you can use 'string2Name' or
+--   'integer2Name'. The type parameter is a tag, or /sort/, which tells
+--   us what sorts of things this name may stand for. The sort must
+--   be an instance of the 'Rep' type class.
+data Name a
+  = Nm (R a) (String, Integer)   -- free names
+  | Bn (R a) Integer Integer     -- bound names / binding level + pattern index
+   deriving (Eq, Ord)
+
+$(derive [''Name])
+
+-- | A name with a hidden (existentially quantified) sort.
+data AnyName = forall a. Rep a => AnyName (Name a)
+
+isBound :: Name a -> Bool
+isBound (Nm _ _) = False
+isBound (Bn _ _ _) = True
+
+isFree :: Name a -> Bool
+isFree (Nm _ _) = True
+isFree (Bn _ _ _) = False
+
+-- AnyName has an existential in it, so we cannot create a complete
+-- representation for it, unfortunately.
+
+$(derive_abstract [''AnyName])
+
+instance Show AnyName where
+  show (AnyName n1) = show n1
+
+instance Eq AnyName where
+   (AnyName n1) == (AnyName n2) =
+      case gcastR (getR n1) (getR n2) n1 of
+           Just n1' -> n1' == n2
+           Nothing  -> False
+
+instance Ord AnyName where
+   compare (AnyName n1) (AnyName n2) =
+       case compareR (getR n1) (getR n2) of
+         EQ  -> case gcastR (getR n1) (getR n2) n1 of
+           Just n1' -> compare n1' n2
+           Nothing  -> error "Panic: equal types are not equal in Ord AnyName instance!"
+         ord -> ord
+
+------------------------------------------------------------
+-- Utilities
+------------------------------------------------------------
+
+-- some convenient names for testing
+name1, name2, name3, name4, name5, name6, name7, name8, name9, name10, name11
+  :: Rep a => Name a
+name1 = integer2Name 1
+name2 = integer2Name 2
+name3 = integer2Name 3
+name4 = integer2Name 4
+name5 = integer2Name 5
+name6 = integer2Name 6
+name7 = integer2Name 7
+name8 = integer2Name 8
+name9 = integer2Name 9
+name10 = integer2Name 10
+name11 = integer2Name 11
+
+--instance Read Name where
+--  read s = error "FIXME"
+
+instance Show (Name a) where
+  show (Nm _ ("",n)) = "_" ++ (show n)
+  show (Nm _ (x,0))  = x
+  show (Nm _ (x,n))  = x ++ (show n)
+  show (Bn _ x y)    =  show x ++ "@" ++ show y
+
+-- | Get the integer index of a 'Name'.
+name2Integer :: Name a -> Integer
+name2Integer (Nm _ (_,x)) = x
+name2Integer (Bn _ _ _)   = error "Internal Error: cannot call name2Integer for bound names"
+
+-- | Get the string part of a 'Name'.
+name2String :: Name a -> String
+name2String (Nm _ (s,_)) = s
+name2String (Bn _ _ _)   = error "Internal Error: cannot call name2Integer for bound names"
+
+-- | Get the integer index of an 'AnyName'.
+anyName2Integer :: AnyName -> Integer
+anyName2Integer (AnyName nm) = name2Integer nm
+
+-- | Get the string part of an 'AnyName'.
+anyName2String :: AnyName -> String
+anyName2String (AnyName nm) = name2String nm
+
+toSortedName :: Rep a => AnyName -> Maybe (Name a)
+toSortedName (AnyName n) = gcastR (getR n) rep n
+
+-- | Create a 'Name' from an 'Integer'.
+integer2Name :: Rep a => Integer -> Name a
+integer2Name n = makeName "" n
+
+-- | Create a 'Name' from a 'String'.
+string2Name :: Rep a => String -> Name a
+string2Name s = makeName s 0
+
+-- | Convenient synonym for 'string2Name'.
+s2n :: Rep a => String -> Name a
+s2n = string2Name
+
+-- | Create a 'Name' from a @String@ and an @Integer@ index.
+makeName :: Rep a => String -> Integer -> Name a
+makeName s i = Nm rep (s,i)
+
+-- | Determine the sort of a 'Name'.
+getR :: Name a -> R a
+getR (Nm r _)   = r
+getR (Bn r _ _) = r
+
+-- | Change the sort of a name
+translate :: (Rep b) => Name a -> Name b
+translate (Nm _ x) = Nm rep x
+translate (Bn _ x y) = Bn rep x y
+ Unbound/LocallyNameless/Ops.hs view
@@ -0,0 +1,249 @@+module Unbound.LocallyNameless.Ops where++import Generics.RepLib++import Unbound.LocallyNameless.Types+import Unbound.LocallyNameless.Alpha+import Unbound.LocallyNameless.Fresh+import Unbound.Util+import Unbound.PermM++import Control.Monad (liftM)+import qualified Text.Read as R++----------------------------------------------------------+-- Binding operations+----------------------------------------------------------++-- | A smart constructor for binders, also sometimes known as+-- \"close\".+bind :: (Alpha c, Alpha b) => b -> c -> Bind b c+bind b c = B b (closeT b c)++-- | A destructor for binders that does /not/ guarantee fresh+--   names for the binders.+unsafeUnbind :: (Alpha a, Alpha b) => Bind a b -> (a,b)+unsafeUnbind (B a b) = (a, openT a b)++instance (Alpha a, Alpha b, Read a, Read b) => Read (Bind a b) where+         readPrec = R.parens $ (R.prec app_prec $ do+                                  R.Ident "<" <- R.lexP+                                  m1 <- R.step R.readPrec+                                  R.Ident ">" <- R.lexP+                                  m2 <- R.step R.readPrec+                                  return (bind m1 m2))+           where app_prec = 10++         readListPrec = R.readListPrecDefault++----------------------------------------------------------+-- Rebinding operations+----------------------------------------------------------++-- | Constructor for binding in patterns.+rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b+rebind a b = R a (closeP a b)++-- | Compare for alpha-equality.+instance (Alpha a, Alpha b, Eq b) => Eq (Rebind a b) where+   b1 == b2 = b1 `aeqBinders` b2++-- | Destructor for `Rebind`.  It does not need a monadic context for+--   generating fresh names, since `Rebind` can only occur in the+--   pattern of a `Bind`; hence a previous call to `open` must have+--   already freshened the names at this point.+unrebind :: (Alpha a, Alpha b) => Rebind a b -> (a, b)+unrebind (R a b) = (a, openP a b)++----------------------------------------------------------+-- Rec operations+----------------------------------------------------------++rec :: (Alpha a) => a -> Rec a+rec a = Rec (closeP a a) where++unrec :: (Alpha a) => Rec a -> a+unrec (Rec a) = openP a a++----------------------------------------------------------+-- TRec operations+----------------------------------------------------------++trec :: Alpha p => p -> TRec p+trec p = TRec $ bind (rec p) ()++untrec :: (Fresh m, Alpha p) => TRec p -> m p+untrec (TRec b) = (unrec . fst) `liftM` unbind b++luntrec :: (LFresh m, Alpha p) => TRec p -> m p+luntrec (TRec b) = lunbind b $ return . unrec . fst++----------------------------------------------------------+-- Wrappers for operations in the Alpha class+----------------------------------------------------------++-- | Determine alpha-equivalence of terms.+aeq :: Alpha t => t -> t -> Bool+aeq t1 t2 = aeq' initial t1 t2++-- | Determine (alpha-)equivalence of patterns.  Do they bind the same+--   variables and have alpha-equal annotations?+aeqBinders :: Alpha p => p -> p -> Bool+aeqBinders p1 p2 = aeq' initial p1 p2++-- | An alpha-respecting total order on terms involving binders.+acompare :: Alpha t => t -> t -> Ordering+acompare x y = acompare' initial x y+++-- | Calculate the free variables (of any sort) contained in a term.+fvAny :: (Alpha t, Collection f) => t -> f AnyName+fvAny = fv' initial++-- | Calculate the free variables of a particular sort contained in a+--   term.+fv :: (Rep a, Alpha t, Collection f) => t -> f (Name a)+fv = filterC+   . cmap toSortedName+   . fvAny++-- | Calculate the variables (of any sort) that occur freely within+--   pattern annotations (but are not bound by the pattern).+patfvAny :: (Alpha p, Collection f) => p -> f AnyName+patfvAny = fv' (pat initial)++-- | Calculate the variables of a particular sort that occur freely in+--   pattern annotations (but are not bound by the pattern).+patfv :: (Rep a, Alpha p, Collection f) => p -> f (Name a)+patfv = filterC+      . cmap toSortedName+      . patfvAny++-- | Calculate the binding variables (of any sort) in a pattern.+bindersAny :: (Alpha p, Collection f) => p -> f AnyName+bindersAny = fvAny++-- | Calculate the binding variables (of a particular sort) in a+--   pattern.+binders :: (Rep a, Alpha p, Collection f) => p -> f (Name a)+binders = fv+++-- | Apply a permutation to a term.+swaps :: Alpha a => Perm AnyName -> a -> a+swaps = swaps' initial++-- | Apply a permutation to the binding variables in a pattern.+-- Embedded terms are left alone by the permutation.+swapsBinders :: Alpha a => Perm AnyName -> a -> a+swapsBinders = swaps' initial++-- | Apply a permutation to the annotations in a pattern. Binding+-- names are left alone by the permutation.+swapsEmbeds :: Alpha a => Perm AnyName -> a -> a+swapsEmbeds = swaps' (pat initial)+++-- | \"Locally\" freshen a pattern replacing all binding names with+--  new names that have not already been used. The second argument is+-- a continuation, which takes the renamed term and a permutation that+-- specifies how the pattern has been renamed.+lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b+lfreshen = lfreshen' (pat initial)++-- | 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' (pat initial)++{-+-- | Compare two terms and produce a permutation of their 'Name's that+-- will make them alpha-equivalent to each other.  Return 'Nothing' if+-- no such renaming is possible.  Note that two terms are+-- alpha-equivalent if the empty permutation is returned.+match   :: Alpha a => a -> a -> Maybe (Perm AnyName)+match   = match' initial++-- | Compare two patterns, ignoring the names of binders, and produce+-- a permutation of their annotations to make them alpha-equivalent+-- to eachother. Return 'Nothing' if no such renaming is possible.+matchEmbeds :: Alpha a => a -> a -> Maybe (Perm AnyName)+matchEmbeds = match' (pat initial)++-- | Compare two patterns for equality and produce a permutation of+-- their binding 'Names' to make them alpha-equivalent to each other+-- (Free 'Name's that appear in annotations must match exactly). Return+-- 'Nothing' if no such renaming is possible.+matchBinders ::  Alpha a => a -> a -> Maybe (Perm AnyName)+matchBinders = match' initial+-}++------------------------------------------------------------+-- Opening binders+------------------------------------------------------------++-- | Unbind (also known as \"open\") is the destructor for+-- bindings. It ensures that the names in the binding are fresh.+unbind  :: (Fresh m, Alpha p, Alpha t) => Bind p t -> m (p,t)+unbind (B p t) = do+      (p', _) <- freshen p+      return (p', openT p' t)++-- | Unbind two terms with the same fresh names, provided the+--   binders have the same number of binding 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 (fvAny p1) (fvAny p2) of+         Just pm -> do+           (p1', pm') <- freshen p1+           return $ Just (p1', openT p1' t1,+                          swaps (pm' <> pm) p2, openT p1' t2)+         Nothing -> return Nothing++-- | Unbind three terms with the same fresh names, provided the+--   binders have the same number of binding variables.+unbind3  :: (Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) =>+            Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 ->  m (Maybe (p1,t1,p2,t2,p3,t3))+unbind3 (B p1 t1) (B p2 t2) (B p3 t3) = do+      case ( mkPerm (fvAny p1) (fvAny p2)+           , mkPerm (fvAny p1) (fvAny p3) ) of+         (Just pm12, Just pm13) -> do+           (p1', p') <- freshen p1+           return $ Just (p1', openT p1' t1,+                          swaps (p' <> pm12) p2, openT p1' t2,+                          swaps (p' <> pm13) p3, openT p1' t3)+         _ -> return Nothing++-- | Destruct a binding in an 'LFresh' monad.+lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c+lunbind (B p t) g =+  lfreshen p (\x _ -> g (x, openT x t))+++-- | Unbind two terms with the same fresh names, provided the+--   binders have the same number of binding variables.+lunbind2  :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) =>+            Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1,t1,p2,t2) -> m r) -> m r+lunbind2 (B p1 t1) (B p2 t2) g =+  case mkPerm (fvAny p1) (fvAny p2) of+    Just pm1 ->+      lfreshen p1 (\p1' pm2 -> g $ Just (p1', openT p1' t1,+                                         swaps (pm2 <> pm1) p2, openT p1' t2))+    Nothing -> g Nothing++-- | Unbind three terms with the same fresh names, provided the+--   binders have the same number of binding variables.+lunbind3 :: (LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) =>+            Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 ->+            (Maybe (p1,t1,p2,t2,p3,t3) -> m r) ->+            m r+lunbind3 (B p1 t1) (B p2 t2) (B p3 t3) g =+  case ( mkPerm (fvAny p1) (fvAny p2)+       , mkPerm (fvAny p1) (fvAny p3) ) of+         (Just pm12, Just pm13) ->+           lfreshen p1 (\p1' pm' -> g $ Just (p1', openT p1' t1,+                                              swaps (pm' <> pm12) p2, openT p1' t2,+                                              swaps (pm' <> pm13) p3, openT p1' t3))+         _ -> g Nothing
+ Unbound/LocallyNameless/Subst.hs view
@@ -0,0 +1,114 @@+{-# LANGUAGE MultiParamTypeClasses+           , FlexibleContexts+           , FlexibleInstances+           , TypeFamilies+           , GADTs+           , ScopedTypeVariables+  #-}++module Unbound.LocallyNameless.Subst where++import Data.List (find)++import Generics.RepLib+import Unbound.LocallyNameless.Types+import Unbound.LocallyNameless.Alpha++------------------------------------------------------------+-- Substitution+------------------------------------------------------------++-- | See 'isvar'.+data SubstName a b where+  SubstName :: (a ~ b) => Name a -> SubstName a b++-- | The 'Subst' class governs capture-avoiding substitution.  To+--   derive this class, you only need to indicate where the variables+--   are in the data type, by overriding the method 'isvar'.+class (Rep1 (SubstD b) a) => Subst b a where++  -- | If the argument is a variable, return its name wrapped in the+  --   'SubstName' constructor.  Return 'Nothing' for non-variable+  --   arguments.  The default implementation always returns+  --   'Nothing'.+  isvar :: a -> Maybe (SubstName a b)+  isvar x = Nothing++  -- | @'subst' nm sub tm@ substitutes @sub@ for @nm@ in @tm@.+  subst :: Name b -> b -> a -> a+  subst n u x | isFree n =+     case (isvar x :: Maybe (SubstName a b)) of+        Just (SubstName m) -> if  m == n then u else x+        Nothing -> substR1 rep1 n u x+  subst m u x = error $ "Cannot substitute for bound variable " ++ show m++  -- | Perform several simultaneous substitutions.+  substs :: [(Name b, b)] -> a -> a+  substs ss x+    | all (isFree . 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 -> substsR1 rep1 ss x+    | otherwise =+      error $ "Cannot substitute for bound variable in: " ++ show (map fst ss)++-- | Reified class dictionary for 'Subst'.+data SubstD b a = SubstD {+  isvarD  :: a -> Maybe (SubstName a b),+  substD  ::  Name b -> b -> a -> a ,+  substsD :: [(Name b, b)] -> a -> a+}++instance Subst b a => Sat (SubstD b a) where+  dict = SubstD isvar subst substs++substDefault :: Rep1 (SubstD b) a => Name b -> b -> a -> a+substDefault = substR1 rep1++substR1 :: R1 (SubstD b) a -> Name b -> b -> a -> a+substR1 (Data1 dt cons) = \ x y d ->+  case (findCon cons d) of+  Val c rec kids ->+      let z = map_l (\ w -> substD w x y) rec kids+      in (to c z)+substR1 r               = \ x y c -> c++substsR1 :: R1 (SubstD b) a -> [(Name b, b)] -> a -> a+substsR1 (Data1 dt cons) = \ s d ->+  case (findCon cons d) of+  Val c rec kids ->+      let z = map_l (\ w -> substsD w s) rec kids+      in (to c z)+substsR1 r               = \ s c -> c++instance Subst b Int+instance Subst b Bool+instance Subst b ()+instance Subst b Char+instance Subst b Integer+instance Subst b Float+instance Subst b Double++instance Subst b AnyName+instance Rep a => Subst b (R a)+instance Rep a => Subst b (Name a)++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 (Subst c b, Subst c a, Alpha a,Alpha b) =>+    Subst c (Bind a b)+instance (Subst c b, Subst c a, Alpha a, Alpha b) =>+    Subst c (Rebind a b)++instance (Subst c a) => Subst c (Embed a)+instance (Alpha a, Subst c a) => Subst c (Rec a)
+ Unbound/LocallyNameless/Test.hs view
@@ -0,0 +1,154 @@+{-# LANGUAGE TemplateHaskell+           , MultiParamTypeClasses+           , FlexibleInstances+           , FlexibleContexts+           , ScopedTypeVariables+           , UndecidableInstances+  #-}++module Generics.RepLib.Bind.LocallyNameless.Test where++import qualified Data.Set as S++import Generics.RepLib hiding (GT)+import Generics.RepLib.Bind.LocallyNameless+import Generics.RepLib.Bind.LocallyNameless.Alpha+import Generics.RepLib.Bind.LocallyNameless.Name+import Generics.RepLib.Bind.PermM++-------------------- TESTING CODE --------------------------------+data Exp = V (Name Exp)+         | A Exp Exp+         | L (Bind (Name Exp) Exp) deriving (Show)++$(derive [''Exp])++instance Alpha Exp+instance Subst Exp Exp where+   isvar (V n) = Just (SubstName n)+   isvar _     = Nothing++nameA, nameB, nameC :: Name Exp+nameA = integer2Name 1+nameB = integer2Name 2+nameC = integer2Name 3++assert :: String -> Bool -> IO ()+assert s True = return ()+assert s False = print ("Assertion " ++ s ++ " failed")++do_tests :: IO ()+do_tests = do+   tests_aeq+   tests_fv+   tests_big+   tests_nth+   tests_acompare++perm = single nameA nameB++naeq x y = not (aeq x y)++tests_aeq = do+   assert "a1" $ (bind nameA nameA) `naeq` (bind nameA nameB)+   assert "a2" $ (bind nameA nameA) `aeq` (bind nameA nameA)+   assert "a3" $ (bind nameA nameA) `aeq` (bind nameB nameB)+   assert "a4" $ (bind nameA nameB) `naeq` (bind nameB nameA)+   assert "a5" $ (bind (nameA, Embed nameB) nameA) `naeq`+                 (bind (nameA, Embed nameC) nameA)+   assert "a6" $ (bind (nameA, Embed nameB) nameA) `aeq`+                 (bind (nameA, Embed nameB) nameA)+   assert "a7" $ (bind (nameA, Embed nameB) nameA) `aeq`+                 (bind (nameB, Embed nameB) nameB)+   assert "a8" $ rebind nameA nameB `naeq` rebind nameB nameB+   assert "a9" $ rebind nameA nameA `naeq` rebind nameB nameB+   assert "a9" $ (bind (rebind nameA (Embed nameA)) nameA) `aeq`+                 (bind (rebind nameB (Embed nameB)) nameB)+   assert "a10" $ bind (rebind (nameA, Embed nameA) ()) nameA `aeq`+                  bind (rebind (nameB, Embed nameA) ()) nameB+   assert "a11" $ bind (rebind (nameA, Embed nameA) ()) nameA `naeq`+                  bind (rebind (nameB, Embed nameB) ()) nameB+   assert "a12" $ bind (Embed nameA) () `naeq` bind (Embed nameB) ()+   assert "a13" $ bind (Embed nameA) () `aeq` bind (Embed nameA) ()+   assert "a14" $ bind (rebind (Embed nameA) ()) () `naeq`+                  bind (rebind (Embed nameB) ()) ()+   assert "a15" $ (rebind (nameA, Embed nameA) ()) `naeq`+                  (rebind (name4, Embed nameC) ())+   assert "a16" $ bind (nameA, nameB) nameA `naeq` bind (nameB, nameA) nameA+   assert "a17" $ bind (nameA, nameB) nameA `naeq` bind (nameA, nameB) nameB+   assert "a18" $ (nameA, nameA) `naeq` (nameA, nameB)+--   assert "a19" $ match (nameA, nameA) (nameB, nameC) == Nothing++emptyNE :: S.Set (Name Exp)+emptyNE = S.empty++tests_fv = do+   assert "f1" $ fv (bind nameA nameA) == emptyNE+   assert "f2" $ fv' (pat initial) (bind nameA nameA) == S.empty+   assert "f4" $ fv (bind nameA nameB) == S.singleton nameB+   assert "f5" $ fv (bind (nameA, Embed nameB) nameA) == S.singleton nameB+   assert "f7" $ fv (bind (nameB, Embed nameB) nameB) == S.singleton nameB+   assert "f8" $ fv (rebind nameA nameB) == S.fromList [nameA, nameB]+   assert "f9" $ fv' (pat initial) (rebind nameA nameA) == S.empty+   assert "f3" $ fv (bind (rebind nameA (Embed nameA)) nameA) == emptyNE+   assert "f10" $ fv (rebind (nameA, Embed nameA) ()) == S.singleton nameA+   assert "f11" $ fv' (pat initial) (rebind (nameA, Embed nameA) ()) == S.singleton (AnyName nameA)+   assert "f12" $ fv (bind (Embed nameA) ()) == S.singleton nameA+   assert "f14" $ fv (rebind (Embed nameA) ()) == emptyNE++mkbig :: [Name Exp] -> Exp -> Exp+mkbig (n : names) body =+    L (bind n (mkbig names (A (V n) body)))+mkbig [] body = body++big1 = mkbig (map integer2Name (take 100 [1 ..])) (V name11)+big2 = mkbig (map integer2Name (take 101 [1 ..])) (V name11)+++tests_nth = do+  assert "n1" $ nthpat ([nameA],nameB) 0 == AnyName nameA+  assert "n2" $ nthpat ([nameA],nameB) 1 == AnyName nameB+  assert "n3" $ nthpat (nameA, nameB) 0 == AnyName nameA+  assert "p1" $ findpat ([nameA],nameB) (AnyName nameA) == Just 0+  assert "p2" $ findpat ([nameA],nameB) (AnyName nameB) == Just 1+  assert "p3" $ findpat ([nameA],nameB) (AnyName nameC) == Nothing++tests_big = do+   assert "b1" $ big1 `naeq` big2+   assert "b2" $ fv big1 == emptyNE+   assert "b3" $ big1 `aeq` subst name11 (V name11) big1++tests_acompare = do+   -- Names compare in the obvious way.+   assert "ac1" $ acompare nameA nameB == LT+   assert "ac2" $ acompare nameB nameB == EQ+   assert "ac3" $ acompare nameB nameA == GT+   -- structured date compares lexicographically+   assert "ac4" $ acompare (A (V nameA) (V nameA)) (A (V nameA) (V nameA)) == EQ+   assert "ac5" $ acompare (A (V nameA) (V nameA)) (A (V nameA) (V nameB)) == LT+   assert "ac6" $ acompare (A (V nameA) (V nameB)) (A (V nameA) (V nameA)) == GT+   assert "ac7" $ acompare (A (V nameA) (V nameA)) (A (V nameB) (V nameA)) == LT+   assert "ac8" $ acompare (A (V nameB) (V nameA)) (A (V nameA) (V nameA)) == GT+   assert "ac9" $ acompare (A (V nameB) (V nameA)) (A (V nameA) (V nameB)) == GT+   -- comparison goes under binders, alpha-respectingly.+   assert "ac10" $ acompare (bind nameA (A (V nameA) (V nameA))) (bind nameA (A (V nameA) (V nameA))) == EQ+   assert "ac11" $ acompare (bind nameA (A (V nameA) (V nameA))) (bind nameA (A (V nameA) (V nameB))) == GT+   assert "ac12" $ acompare (bind nameC (A (V nameC) (V nameA))) (bind nameA (A (V nameA) (V nameB))) == LT+   -- non-matching binders handled alpha-respectingly.+   assert "ac13" $ acompare (bind [nameA] nameA) (bind [nameA,nameB] nameA)+                 ==  acompare (bind [nameC] nameC) (bind [nameA,nameB] nameA)+   assert "ac14" $ acompare (bind [nameA,nameB] nameA) (bind [nameA] nameA)+                 ==  acompare (bind [nameC,nameB] nameC) (bind [nameA] nameA)+   -- non-binding stuff in patterns gets compared+   assert "ac15" $ acompare (Embed nameA) (Embed nameB) == LT+   assert "ac16" $ acompare (bind (nameC, Embed nameA) (A (V nameC) (V nameC)))+                            (bind (nameC, Embed nameB) (A (V nameC) (V nameC))) == LT+   assert "ac17" $ acompare (bind (nameC, Embed nameA) (A (V nameB) (V nameB)))+                          (bind (nameC, Embed nameB) (A (V nameA) (V nameA))) == LT+   -- TODO: do we need anything special for rebind? For AnyName?++-- properties+-- if match t1 t2 = Some p then swaps p t1 = t2++main :: IO ()+main = do_tests
+ Unbound/LocallyNameless/Types.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE TemplateHaskell+           , ScopedTypeVariables+           , FlexibleInstances+           , FlexibleContexts+           , MultiParamTypeClasses+  #-}++module Unbound.LocallyNameless.Types+       ( Bind(..)+       , Rebind(..)+       , Rec(..)+       , TRec(..)+       , Embed(..)+       , Shift(..)+       , module Unbound.LocallyNameless.Name++       -- * Pay no attention to the man behind the curtain+       -- $paynoattention+       , rBind, rRebind, rEmbed, rRec, rShift+       ) where++import Generics.RepLib+import Unbound.LocallyNameless.Name++------------------------------------------------------------+-- Basic types+------------------------------------------------------------++-- Bind+--------------------------------------------------++-- | The type of a binding.  We can 'Bind' an @a@ object in a @b@+--   object if we can create \"fresh\" @a@ objects, and @a@ objects+--   can occur unbound in @b@ objects. Often @a@ is 'Name' but that+--   need not be the case.+--+--   Like 'Name', 'Bind' is also abstract. You can create bindings+--   using 'bind' and take them apart with 'unbind' and friends.+data Bind p t = B p t++instance (Show a, Show b) => Show (Bind a b) where+  showsPrec p (B a b) = showParen (p>0)+      (showString "<" . showsPrec p a . showString "> " . showsPrec 0 b)++-- XXX todo: make sure everything has write Read and Eq instances?++-- Rebind+--------------------------------------------------++-- | 'Rebind' supports \"telescopes\" --- that is, patterns where+--   bound variables appear in multiple subterms.+data Rebind p1 p2 = R p1 p2++instance (Show a, Show b) => Show (Rebind a b) where+  showsPrec p (R a b) = showParen (p>0)+      (showString "<<" . showsPrec p a . showString ">> " . showsPrec 0 b)++-- Rec+--------------------------------------------------++-- | 'Rec' supports recursive patterns --- that is, patterns where+-- any variables anywhere in the pattern are bound in the pattern+-- itself.  Useful for lectrec (and Agda's dot notation).+data Rec p = Rec p++instance Show a => Show (Rec a) where+  showsPrec _ (Rec a) = showString "[" . showsPrec 0 a . showString "]"++-- TRec+--------------------------------------------------++-- | 'TRec' is a standalone variant of 'Rec' -- that is, if @p@ is a+--   pattern type then @TRec p@ is a term type.  It is isomorphic to+--   @Bind (Rec p) ()@.++newtype TRec p = TRec (Bind (Rec p) ())++instance Show a => Show (TRec a) where+  showsPrec _ (TRec (B (Rec p) ())) = showString "[" . showsPrec 0 p . showString "]"+++-- Embed+--------------------------------------------------++-- XXX improve this doc+-- | An annotation is a \"hole\" in a pattern where variables can be+--   used, but not bound. For example, patterns may include type+--   annotations, and those annotations can reference variables+--   without binding them.  Annotations do nothing special when they+--   appear elsewhere in terms.+newtype Embed t = Embed t deriving Eq++instance Show a => Show (Embed a) where+  showsPrec p (Embed a) = showString "{" . showsPrec 0 a . showString "}"++-- Shift+--------------------------------------------------++-- | Shift the scope of an embedded term one level outwards.+newtype Shift p = Shift p deriving Eq++instance Show a => Show (Shift a) where+  showsPrec p (Shift a) = showString "{" . showsPrec 0 a . showString "}"++-- $paynoattention+-- These type representation objects are exported so they can be+-- referenced by auto-generated code.  Please pretend they do not+-- exist.++$(derive [''Bind, ''Embed, ''Rebind, ''Rec, ''Shift])+
+ Unbound/Nominal.hs view
@@ -0,0 +1,70 @@+----------------------------------------------------------------------
+-- |
+-- Module      :  Unbound.Nominal
+-- License     :  BSD-like (see LICENSE)
+--
+-- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>
+-- Stability   :  experimental
+-- Portability :  non-portable (-XKitchenSink)
+--
+-- Generic implementation of name binding functions, based on the library
+-- RepLib. This version uses a nominal representation of binding structure.
+--
+-- DISCLAIMER: this module probably contains bugs and may be
+-- slower than "Unbound.LocallyNameless".  At this point
+-- we recommend it only for the curious or intrepid.
+--
+-- Datatypes with binding defined using the 'Name' and 'Bind' types.
+-- Important classes are
+--     'Alpha' -- the class of types that include binders.
+-- These classes are generic, and default implementations exist for all
+-- representable types. This file also defines a third generic class,
+--     'Subst' -- for subtitution functions.
+--
+--------------------------------------------------------------------------
+module Unbound.Nominal
+  (-- * Basic types
+    Name,  AnyName(..), Bind, Embed(..), Rebind, Rec, Shift,
+
+    -- ** Utilities
+    integer2Name, string2Name, name2Integer, name2String, makeName,
+    name1,name2,name3,name4,name5,name6,name7,name8,name9,name10,
+    translate,
+
+    -- * The 'Alpha' class
+    Alpha(..),
+    swaps, -- is a bit wonky
+    match,
+    binders, patfv, fv,
+    aeq,
+
+    -- * Binding operations
+    bind, unsafeUnbind,
+
+    -- * The 'Fresh' class
+    Fresh(..), freshen,
+    unbind, unbind2, unbind3,
+
+    -- * The 'LFresh' class
+    HasNext(..), LFresh(..),
+    lfreshen,
+    lunbind, lunbind2, lunbind3,
+
+    -- * Rebinding operations
+    rebind, reopen,
+
+    -- * Rec operations
+    rec, unrec,
+
+    -- * Substitution
+    Subst(..),
+
+   -- * Advanced
+   AlphaCtx, matchR1,
+
+   -- * Pay no attention to the man behind the curtain
+   -- $paynoattention
+   rName, rBind, rRebind, rEmbed, rRec, rShift) where
+
+import Unbound.Nominal.Name
+import Unbound.Nominal.Internal
+ Unbound/Nominal/Internal.hs view
@@ -0,0 +1,977 @@+{-# LANGUAGE FlexibleInstances, UndecidableInstances, FlexibleContexts, MultiParamTypeClasses, TemplateHaskell, TypeOperators, ScopedTypeVariables, TypeSynonymInstances, RankNTypes, GADTs, EmptyDataDecls, StandaloneDeriving #-}
+
+----------------------------------------------------------------------
+-- |
+-- Module      :  Unbound.Nominal.Internal
+-- License     :  BSD-like (see LICENSE)
+--
+--------------------------------------------------------------------------
+module Unbound.Nominal.Internal where
+
+import Generics.RepLib
+import Unbound.Nominal.Name
+import Unbound.PermM
+
+import qualified Data.List as List
+import qualified Text.Read as R
+import Data.Set (Set)
+import Data.Maybe
+import qualified Data.Set as S
+import Prelude hiding (or)
+import Data.Monoid
+import qualified Control.Monad as Monad
+import Control.Monad.Reader (Reader,ask,local,runReader)
+import System.IO.Unsafe (unsafePerformIO)
+
+(<>) :: Monoid m => m -> m -> m
+(<>) = mappend
+
+---------------------------------------------------
+
+$(derive_abstract [''R])
+-- The above only works with GHC 7.
+
+
+-- | Type of a binding.  Morally, the type a should be in the
+-- class 'Pattern' and the type b should be in the class 'Alpha'.
+-- The Pattern class contains the constructor and a safe
+-- destructor for these types.
+-- We can Bind an "a" object in a "b" object if we
+-- can create "fresh" a objects, and Names can be
+-- swapped in "b" objects. Often "a" is Name
+-- but that need not be the case.
+data Bind a b = B a b
+
+-- | An annotation is a 'hole' in a pattern where variables
+-- can be used, but not bound. For example patterns may include
+-- type annotations, and those annotations can reference variables
+-- without binding them.
+-- Annotations do nothing special when they appear elsewhere in terms
+newtype Embed a = Embed a deriving (Read, Eq)
+
+-- | Shift the scope of an embedded term one level outwards.
+newtype Shift a = Shift a deriving Eq
+
+-- | Rebinding is for telescopes --- i.e. to support patterns that
+-- also bind variables that appear later
+data Rebind a b = R a (Bind [AnyName] b)
+
+-- | 'Rec' supports recursive patterns --- that is, patterns where
+-- any variables anywhere in the pattern are bound in the pattern
+-- itself.  Useful for lectrec (and Agda's dot notation).
+data Rec a = Rec a
+
+$(derive [''Bind, ''Name, ''Embed, ''Rebind, ''Rec, ''Shift])
+
+----------------------------------------------------------
+-- Binding operations & instances
+----------------------------------------------------------
+
+-- | Smart constructor for binders
+bind :: (Alpha b,Alpha c) => b -> c -> Bind b c
+bind a b = B a b
+
+-- | A destructor for binders that does not guarantee fresh
+-- names for the binders.
+unsafeUnbind :: Bind a b -> (a,b)
+unsafeUnbind (B a b) = (a,b)
+
+instance (Show a, Show b) => Show (Bind a b) where
+  showsPrec p (B a b) = showParen (p>0)
+      (showString "<" . showsPrec p a . showString "> " . showsPrec 0 b)
+
+instance (Alpha a, Alpha b, Read a, Read b) => Read (Bind a b) where
+         readPrec = R.parens $ (R.prec app_prec $ do
+                                  R.Ident "B" <- R.lexP
+                                  m1 <- R.step R.readPrec
+                                  m2 <- R.step R.readPrec
+                                  return (bind m1 m2))
+           where app_prec = 10
+
+         readListPrec = R.readListPrecDefault
+
+----------------------------------------------------------
+-- Rebinding operations
+----------------------------------------------------------
+
+-- | Constructor for binding in patterns
+rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b
+rebind a b = R a (bind (binders a) b)
+
+instance (Alpha a, Show a, Show b) => Show (Rebind a b) where
+  showsPrec p (R a (B a' b)) =  showParen (p>0)
+      (showString "<<" . showsPrec p a . sa' . showString ">> " . showsPrec 0 b)
+   where sa' =  if binders' initial a == a' then showString ""
+                  else showString "/" . showsPrec p a'
+
+-- | destructor for binding patterns, the external names
+-- should have already
+-- been freshen'ed. We swap the internal names so that they use the
+-- external names
+reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b)
+reopen (R a1 (B names b)) = (a1, swaps p b) where
+   p = fromJust $ Monad.foldM join empty
+          (zipWith single (binders' initial a1) names)
+
+----------------------------------------------------------
+-- Rec operations
+----------------------------------------------------------
+
+rec :: (Alpha a) => a -> Rec a
+rec a = Rec a where
+
+unrec :: (Alpha a) => Rec a -> a
+unrec (Rec a) = a
+
+instance Show a => Show (Rec a) where
+  showsPrec p (Rec a) = showString "[" . showsPrec 0 a . showString "]"
+
+----------------------------------------------------------
+-- Embed
+----------------------------------------------------------
+instance (Show a) => Show (Embed a) where
+  showsPrec p (Embed a) =
+      (showString "{" . showsPrec 0 a . showString "}")
+
+----------------------------------------------------------
+-- Wrappers for operations in the Alpha class
+----------------------------------------------------------
+
+aeq :: Alpha a => a -> a -> Bool
+aeq t1 t2 = -- aeq' initial t1 t2
+  case match t1 t2 of
+              Just p -> isid p
+              _       -> False
+
+
+-- | calculate the free variables of the term
+fv :: (Rep b, Alpha a) => a -> Set (Name b)
+fv = S.map fromJust . S.filter isJust . S.map toSortedName . fv' initial
+
+-- | List the binding variables in a pattern
+binders :: (Rep b, Alpha b) => b -> [AnyName]
+binders = binders' initial
+
+-- | Set of variables that occur freely in annotations (not binding)
+patfv :: (Rep a, Alpha b) => b -> Set (Name a)
+patfv = S.map fromJust . S.filter isJust . S.map toSortedName . fv' (pat initial)
+
+-- | The method "swaps" applys a permutation to all free variables
+-- in the term.
+swaps :: Alpha a => Perm AnyName -> a -> a
+swaps = swaps' initial
+
+-- | Apply a permutation to the binding variables in a pattern.
+--   Embedded terms are left alone by the permutation.
+swapsBinders :: Alpha a => Perm AnyName -> a -> a
+swapsBinders = swaps' initial
+
+-- | Apply a permutation to the annotations in a pattern. Binding
+-- names are left alone by the permutation.
+swapsEmbeds :: Alpha a => Perm AnyName -> a -> a
+swapsEmbeds = swaps' (pat initial)
+
+
+-- | "Locally" freshen an object
+lfreshen :: Alpha a => LFresh m => a -> (a -> Perm AnyName -> m b) -> m b
+lfreshen = lfreshen' initial
+
+-- | A pattern of type "b" can be freshened if a new
+-- copy of "b" can be produced where all old *binding* Names
+-- in "b" are replaced with new fresh Names, and the
+-- permutation reports which Names were swapped by others.
+freshen :: (Fresh m, Alpha a) => a -> m (a, Perm AnyName)
+freshen = freshen' initial
+
+-- | Match compares two data structures and produces a permutation
+-- of their Names that will make them alpha-equivalent to
+-- eachother. (Names that appear in annotations must match exactly.)
+-- Also note that two terms are alpha-equivalent when the empty
+-- permutation is returned.
+match   :: Alpha a => a -> a -> Maybe (Perm AnyName)
+match   = match' initial
+
+
+-- | Compare two patterns, ignoring the names of binders, and produce
+-- a permutation of their annotations to make them alpha-equivalent
+-- to eachother. Return 'Nothing' if no such renaming is possible.
+matchEmbeds :: Alpha a => a -> a -> Maybe (Perm AnyName)
+matchEmbeds = match' (pat initial)
+
+-- | Compare two patterns for equality and produce a permutation of
+-- their binding 'Names' to make them alpha-equivalent to each other
+-- ('Name's that appear in annotations must match exactly). Return
+-- 'Nothing' if no such renaming is possible.
+matchBinders ::  Alpha a => a -> a -> Maybe (Perm AnyName)
+matchBinders = match' initial
+
+---------------------------------------------------------------
+-- | Many of the operations in the 'Alpha' class take an 'AlphaCtx':
+-- stored information about the iteration as it progresses. This type
+-- is abstract, as classes that override these operations should just pass
+-- the context on.
+data AlphaCtx = Term | Pat deriving (Show, Eq, Read)
+
+initial :: AlphaCtx
+initial = Term
+
+pat  :: AlphaCtx -> AlphaCtx
+pat c  = Pat
+
+term  :: AlphaCtx -> AlphaCtx
+term c  = Term
+
+mode :: AlphaCtx -> AlphaCtx
+mode = id
+
+------------------------------------------------------------
+-- The Alpha class
+------------------------------------------------------------
+-- | The Alpha class is for all terms that may contain binders
+-- The 'Rep1' class constraint means that we can only
+-- make instances of this class for types that have
+-- generic representations. (Derive these using TH and
+-- RepLib.)
+
+class (Rep1 (AlphaD) a) => Alpha a where
+
+  aeq' :: AlphaCtx -> a -> a -> Bool
+  aeq' = aeqR1 rep1
+
+  -- | swap everything, including bound and free variables,
+  -- parts in annots, etc.
+  swapall' :: AlphaCtx -> Perm AnyName -> a -> a
+  swapall' = swapallR1 rep1
+
+  -- | The method "swaps'" applys a compound permutation
+  swaps' :: AlphaCtx -> Perm AnyName -> a -> a
+  swaps' = swapsR1 rep1
+
+  -- | calculate the free variables (aka support)
+  fv' :: AlphaCtx -> a -> Set AnyName
+  fv' = fvR1 rep1
+
+  -- | list the binding variables in a pattern, in order
+  binders' :: AlphaCtx -> a -> [AnyName]
+  binders' = bindersR1 rep1
+
+  -- | Match' compares two data structures and produces a
+  -- permutation of their free variables that will make them
+  -- alpha-equivalent to eachother.
+  match' :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)
+  match' = matchR1 rep1
+
+  -- | An object of type "a" can be freshened if a new
+  -- copy of "a" can be produced where all old Names
+  -- in "a" are replaced with new fresh Names, and the
+  -- permutation reports which names were swapped by others.
+  freshen' :: Fresh m => AlphaCtx -> a -> m (a,Perm AnyName)
+  freshen' = freshenR1 rep1
+
+  -- | See 'lfreshen'
+  lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
+  lfreshen' = lfreshenR1 rep1
+
+
+-- class constraint hackery to allow us to override the
+-- default definitions for certain classes
+data AlphaD a = AlphaD {
+  aeqD     :: AlphaCtx -> a -> a -> Bool,
+  swapallD   :: AlphaCtx -> (Perm AnyName) -> a -> a,
+  swapsD   :: AlphaCtx -> (Perm AnyName) -> a -> a,
+  fvD      :: AlphaCtx -> a -> Set AnyName,
+  bindersD :: AlphaCtx -> a -> [AnyName],
+
+  matchD   :: AlphaCtx -> a -> a -> Maybe (Perm AnyName),
+  freshenD :: forall m. Fresh m => AlphaCtx -> a -> m (a,Perm AnyName),
+  lfreshenD :: forall b m. LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
+ }
+
+instance Alpha a => Sat (AlphaD a) where
+  dict = AlphaD aeq' swapall' swaps' fv' binders' match' freshen' lfreshen'
+
+-- Generic definitions of the class functions.
+-- (All functions that take representations end
+-- in 'R1')
+aeqR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Bool
+aeqR1 (Data1 _ cons) = loop cons where
+  loop (Con emb reps : rest) p x y =
+    case (from emb x, from emb y) of
+      (Just p1, Just p2) -> aeq1 reps p p1 p2
+      (Nothing, Nothing) -> loop rest p x y
+      (_,_)              -> False
+  loop [] _ _ _ = error "Impossible"
+aeqR1 Int1 = \ _ x y -> x == y
+aeqR1 Integer1 = \ _ x y -> x == y
+aeqR1 Char1 = \ _ x y -> x == y
+aeqR1 _ = \ _ _ _ -> error "Cannot aeq this type"
+
+aeq1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Bool
+aeq1 MNil _ Nil Nil = True
+aeq1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) =
+  aeqD r c p1 p2 && aeq1 rs c t1 t2
+
+swapsR1 :: R1 (AlphaD) a -> AlphaCtx -> (Perm AnyName) -> a -> a
+swapsR1 Char1           = \ _ _ c -> c
+swapsR1 Int1            = \ _ _ c -> c
+swapsR1 Float1          = \ _ _ c -> c
+swapsR1 Integer1        = \ _ _ c -> c
+swapsR1 (Data1 _ cons)  = \ p x d ->
+  case (findCon cons d) of
+  Val c rec kids -> to c (map_l (\z -> swapsD z p x) rec kids)
+swapsR1 r               = error ("Cannot swap type " ++ (show r))
+
+
+swapallR1 :: R1 (AlphaD) a -> AlphaCtx -> (Perm AnyName) -> a -> a
+swapallR1 Char1           = \ _ _ c -> c
+swapallR1 Int1            = \ _ _ c -> c
+swapallR1 Float1          = \ _ _ c -> c
+swapallR1 Integer1        = \ _ _ c -> c
+swapallR1 (Data1 _ cons)  = \ p x d ->
+  case (findCon cons d) of
+  Val c rec kids -> to c (map_l (\z -> swapallD z p x) rec kids)
+swapallR1 r               = error ("Cannot swap type " ++ (show r))
+
+fvR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> Set AnyName
+fvR1 (Data1 _ cons) = \ p  d ->
+  case (findCon cons d) of
+    Val _ rec kids -> fv1 rec p kids
+fvR1 _ = \ _ _ -> S.empty
+
+fv1 :: MTup (AlphaD) l -> AlphaCtx -> l -> Set AnyName
+fv1 MNil _ Nil = S.empty
+fv1 (r :+: rs) p (p1 :*: t1) =
+   fvD r p p1 `S.union` fv1 rs p t1
+
+bindersR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> [AnyName]
+bindersR1 (Data1 _ cons) = \ p  d ->
+  case (findCon cons d) of
+    Val _ rec kids -> binders1 rec p kids
+bindersR1 _ = \ _ _ -> []
+
+binders1 :: MTup (AlphaD) l -> AlphaCtx -> l -> [AnyName]
+binders1 MNil _ Nil = []
+binders1 (r :+: rs) p (p1 :*: t1) =
+   bindersD r p p1 ++ binders1 rs p t1
+
+
+matchR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)
+matchR1 (Data1 _ cons) = loop cons where
+  loop (Con emb reps : rest) p x y =
+    case (from emb x, from emb y) of
+      (Just p1, Just p2) -> match1 reps p p1 p2
+      (Nothing, Nothing) -> loop rest p x y
+      (_,_)              -> Nothing
+  loop [] _ _ _ = error "Impossible"
+matchR1 Int1 = \ _ x y -> if x == y then Just empty else Nothing
+matchR1 Integer1 = \ _ x y -> if x == y then Just empty else Nothing
+matchR1 Char1 = \ _ x y -> if x == y then Just empty else Nothing
+matchR1 _ = \ _ _ _ -> Nothing
+
+match1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Maybe (Perm AnyName)
+match1 MNil _ Nil Nil = Just empty
+match1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) = do
+  l1 <- matchD r c p1 p2
+  l2 <- match1 rs c t1 t2
+  (l1 `join` l2)
+
+
+freshenR1 :: R1 (AlphaD) a -> Fresh m => AlphaCtx -> a -> m (a,Perm AnyName)
+freshenR1 (Data1 _ cons) = \ p d ->
+   case findCon cons d of
+     Val c rec kids -> do
+       (l, p') <- freshenL rec p kids
+       return (to c l, p')
+freshenR1 _ = \ _ n -> return (n, empty)
+
+freshenL :: Fresh m => MTup (AlphaD) l -> AlphaCtx -> l -> m (l, Perm AnyName)
+freshenL MNil _ Nil = return (Nil, empty)
+freshenL (r :+: rs) p (t :*: ts) = do
+  (xs, p2) <- freshenL rs p ts
+  (x, p1) <- freshenD r p (swapsD r p p2 t)
+  return ( x :*: xs, p1 <> p2)
+
+lfreshenR1 :: LFresh m => R1 AlphaD a -> AlphaCtx -> a ->
+              (a -> Perm AnyName -> m b) -> m b
+lfreshenR1 (Data1 _ cons) = \p d f ->
+   case findCon cons d of
+     Val c rec kids -> lfreshenL rec p kids (\ l p' -> f (to c l) p')
+lfreshenR1 _ = \ _ n f -> f n empty
+
+lfreshenL :: LFresh m => MTup (AlphaD) l -> AlphaCtx -> l ->
+              (l -> Perm AnyName -> m b) -> m b
+lfreshenL MNil _ Nil f = f Nil empty
+lfreshenL (r :+: rs) p (t :*: ts) f =
+  lfreshenL rs p ts ( \ y p2 ->
+  lfreshenD r p (swapsD r p p2 t) ( \ x p1 ->
+     f (x :*: y) (p1 <> p2)))
+
+
+instance (Rep a) => Alpha (Name a) where
+  fv' c n@(Nm _ _)  | mode c == Term = S.singleton (AnyName n)
+  fv' c n           | mode c == Pat  = S.empty
+
+  binders' c n@(Nm _ _)  | mode c == Term = [AnyName n]
+  binders' c n           | mode c == Pat  = []
+
+  swapall' c p x =
+      case apply p (AnyName x) of
+       AnyName y ->
+        case cast y of
+          Just y' -> y'
+          Nothing -> error "Internal error in swaps': sort mismatch"
+
+  swaps' c p x | mode c == Term =
+      case apply p (AnyName x) of
+       AnyName y ->
+        case cast y of
+          Just y' -> y'
+          Nothing -> error "Internal error in swaps': sort mismatch"
+  swaps' c p x | mode c == Pat = x
+
+  aeq' c x y = x == y
+
+  match' c x y  | x == y         = Just empty
+  match' c x y  | mode c == Term =
+    Just $ single (AnyName x) (AnyName y)
+  match' c _ _  | mode c == Pat  = Just empty
+
+  freshen' c nm = case mode c of
+     Term -> do x <- fresh nm
+                return (x, single (AnyName nm) (AnyName x))
+     Pat  -> return (nm, empty)
+
+  lfreshen' c nm f = case mode c of
+     Term -> do x <- lfresh nm
+                avoid [AnyName x] $
+                  f x (single (AnyName nm) (AnyName x))
+     Pat  -> f nm empty
+
+
+instance Alpha AnyName  where
+
+  fv' Term n = S.singleton n
+  fv' Pat n  = S.empty
+
+  binders' Term n = [n]
+  binders' Pat n  = []
+
+  swapall' c p x = apply p x
+
+  swaps' Term p x = apply p x
+  swaps' Pat perm x = x
+
+  aeq' c x y = x == y
+
+  match' Term x y = if x == y then Just empty else Just (single x y)
+  match' Pat x y = Just empty
+
+  freshen' Term (AnyName nm) = do { x <- fresh nm; return(AnyName x,
+                                  (single (AnyName nm) (AnyName x))) }
+  freshen' Pat nm = return (nm, empty)
+
+  lfreshen' c (AnyName nm) f = case mode c of
+     Term -> do { x <- lfresh nm; avoid [AnyName x] $ f (AnyName x)
+                     (single (AnyName nm) (AnyName x)) }
+     Pat  -> f (AnyName nm) empty
+
+instance (Alpha a, Alpha b) => Alpha (Bind a b) where
+    -- default definition of swapall
+
+    -- to swap in a binder, swap the free variables in the
+    -- pattern, then remove the binders from the permutation
+    -- and swap in the body
+    -- ? why don't we just swap everywhere? we need to be
+    -- able to freshen patterns with annotations
+    swaps' p pm (B x y) =
+        B (swaps' (pat p) pm x) (swaps' p pm' y) where
+            pm' = restrict pm (binders x)
+
+    -- free variables of a binder are the free variables in
+    -- the annotations in the pattern plus the free variables
+    -- of the body, minus the binders.
+    fv' p (B x y) = fv' Pat x `S.union` (fv' p y S.\\ fv' Term x)
+
+    binders' p (B x y) = binders' Pat x ++
+                         (binders' p y List.\\ binders' Term x)
+
+    -- default definition of freshen'
+{-
+    freshen' p (B x y) = do
+--       (x', p1)  <- freshen' (all p) x -- freshen the binders & annots
+       (y', p3) <- freshen' p (swaps' p p1 y) -- freshen body
+       return (B x' y', p1 <> p3)
+-}
+
+    lfreshen' c (B x y) f =
+      avoid (S.elems $ fv' c x) $
+        lfreshen' (pat c) x (\ x' pm1 ->
+        lfreshen' c (swaps' c pm1 y) (\ y' pm2 ->
+        f (B x' y') (pm1 <> pm2)))
+
+    -- this version of aeq seems to work
+    aeq' p (B x1 y1) (B x2 y2)
+       -- if the binders match, compare the patterns & bodies
+       | bx1 == bx2 = aeq' p x1 x2 && aeq' p y1 y2
+       -- if any binders of the first appear freely in the
+       -- second body, not aeq
+       | (S.fromList bx1) `S.intersection`
+         (fv' Term y2 S.\\ fv' Term y1) /= S.empty = False
+       -- otherwise swap the binding variables in the pattern
+       -- and *all* of the variables in the body
+       | True = aeq' p x1 (swaps' Term pm x2) &&
+                aeq' p y1 (swapall' Term pm y2)
+     where bx1 = binders' Term x1
+           bx2 = binders' Term x2
+           pm  = foldl (<>) empty (zipWith single bx1 bx2)
+
+
+    -- basic idea of match
+    -- if binders x1 == binders x2 then
+        --- match the annots in x1 and x2 and match the bodies y1 y2
+    -- if binders x1 /= binders x2 then
+        -- make sure binders of x1 are not free in the body of y2
+        -- swap (x1,x2) in y2
+        -- match the annots & match the bodies
+        -- make sure none of the binders escapes in the resulting match
+    -- ingredients:
+        -- match the binders, ignoring the annots
+        -- match the annots, ignoring the binders
+        -- list the binding variables
+    match' p (B x1 y1) (B x2 y2)
+      |  bx1 == bx2 = do
+            pm1 <- match' Pat x1 x2
+            pm2 <- match' p y1 y2
+            pm1 `join` pm2
+      | (S.fromList bx1) `S.intersection`
+        (fv' Term y2 S.\\ fv' Term y1)
+            /= S.empty = Nothing
+      | True = do
+            -- make sure that we can match up the binders
+            -- this will fail if there are repeated vars
+            pm <- Monad.foldM join empty (zipWith single bx1 bx2)
+            let x2' = swaps' initial pm x2
+            let y2' = swapall' initial pm y2
+            pm1 <- match' Pat x1 x2'
+            pm2 <- match' p   y1 y2'
+            -- note pm2 should not permute binders
+            -- (see a16) Dropping would give us "set binding"
+            if S.fromList bx1 `S.intersection`
+               S.fromList (support pm2) /= S.empty
+              then Nothing
+              else pm1 `join` pm2
+       where bx1 = binders' Term x1
+             bx2 = binders' Term x2
+
+instance (Alpha a, Alpha b) => Alpha (Rebind a b) where
+
+   -- free variables of the external binder
+   -- plus free vars of the annots in the binder
+   -- plus free vars of the body minus any
+   --     binding vars of internal binder
+   fv' p (R x (B ns y)) = fv' p x `S.union`
+      (fv' p y S.\\ S.fromList ns)
+
+   binders' p (R x (B ns y)) = binders' p x ++
+      (binders' p y List.\\ ns)
+
+
+   swaps' Term pm (R x (B ns y)) =
+      R (swaps' Term pm x) (B ns (swaps' Term pm' y)) where
+            pm' = restrict pm ns
+
+   match' p (R x1 (B n1 y1)) (R x2 (B n2 y2)) = do
+      px  <- match' p x1 x2   -- external names
+      pb  <- match' p (B n1 y1) (B n2 y2)
+      px `join` pb
+
+   freshen' p (R x (B x1 y)) = do
+      (x', pm1) <- freshen' p x
+      (y', pm2) <- freshen' p (swaps' p pm1 y)
+      return (R x (B x1 y'), pm1 <> pm2)
+
+
+instance (Eq a, Alpha a) => Alpha (Embed a) where
+
+   swaps' Pat  pm (Embed t) = Embed (swaps' Term pm t)
+   swaps' Term pm (Embed t) = Embed t
+
+   fv' Pat (Embed t)        = fv' Term t
+   fv' Term _               = S.empty
+
+   binders' Pat (Embed t)   = binders' Term t
+   binders' Term _          = []
+
+
+   freshen' Pat (Embed t)  = do
+     (t', p) <- freshen' Term t
+     return (Embed t', p)
+   freshen' Term a       = return (a, empty)
+
+   match' Pat (Embed x) (Embed y)  = match' Term x y
+   match' Term (Embed x) (Embed y) = if x `aeq` y
+                                    then Just empty
+                                    else Nothing
+
+-- Instances for other types (mostly) use the default definitions.
+instance Alpha Bool where
+instance Alpha Float where
+instance Alpha () where
+instance Alpha a => Alpha [a] where
+instance Alpha Int where
+instance Alpha Integer where
+instance Alpha Double where
+instance Alpha Char where
+instance Alpha a => Alpha (Maybe a) where
+instance (Alpha a,Alpha b) => Alpha (Either a b) where
+instance (Alpha a,Alpha b) => Alpha (a,b) where
+instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c) where
+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)
+instance (Rep a) => Alpha (R a) where
+
+
+-- Definitions of the class members for abstract types.
+{-
+abs_swaps' :: Alpha a => AlphaCtx -> Perm Name -> a -> a
+abs_swaps' _ p s = s
+abs_fv' :: Alpha a => AlphaCtx -> a -> [Name]
+abs_fv' _ s = []
+abs_freshen' :: (Fresh m, Alpha a) => AlphaCtx -> a -> m (a, Perm Name)
+abs_freshen' _ b = return (b, empty)
+abs_match' :: (Eq a, Alpha a) => AlphaCtx -> a -> a -> Maybe (Perm Name)
+abs_match' _ x1 x2 = if x1 == x2 then Just empty else Nothing
+-}
+
+-------------------------------------------------------
+-- | A monad "m" supports the nextInteger operation if it
+-- can generate new fresh integers
+
+class Monad m => HasNext m where
+  nextInteger :: m Integer
+  resetNext   :: Integer -> m ()
+
+-- | A monad "m" supports the "fresh" operation if it
+-- can generate a new unique names.
+
+class (Monad m, HasNext m) => Fresh m where
+  fresh :: Name a -> m (Name a)
+  fresh (Nm r (s,j)) = do { i <- nextInteger; return (Nm r (s,i)) }
+
+instance HasNext m => Fresh m where
+  fresh (Nm r (s,j)) = do { n <- nextInteger; return (Nm r (s,n)) }
+
+-- | Unbind is the destructor of a binding. It ensures that
+-- the names in the binding b are fresh.
+unbind  :: (Alpha b,Fresh m,Alpha c) => Bind b c -> m (b,c)
+unbind (B x y) = do
+    (x',perm) <- freshen x
+    return(x', swaps perm y)
+
+-- | Destruct two bindings simultanously, if they match, using the
+-- same list of fresh names
+unbind2  :: (Fresh m,Alpha b,Alpha c, Alpha d) =>
+   Bind b c -> Bind b d -> m (Maybe (b,c,d))
+unbind2 (B x1 y1) (B x2 y2) = do
+   (x1', perm1) <- freshen x1
+   case match x1' x2 of
+      (Just perm2) ->
+         return $ Just (x1', swaps perm1 y1, swaps perm2 y2)
+      Nothing -> return Nothing
+
+unbind3  :: (Fresh m,Alpha b,Alpha c, Alpha d, Alpha e) =>
+   Bind b c -> Bind b d -> Bind b e -> m (Maybe (b,c,d,e))
+unbind3 (B x1 y1) (B x2 y2) (B x3 y3) = do
+   (x1', perm1) <- freshen x1
+   case (match x1' x2, match x1' x3) of
+      (Just perm2, Just perm3) ->
+         return $ Just (x1', swaps perm1 y1, swaps perm2 y2, swaps perm3 y3)
+      _ -> return Nothing
+
+-----------------------------------------------------------------
+-- | Locally fresh monad
+-- This is the class of
+-- monads that support freshness in an (implicit) local scope.  Names
+-- drawn are fresh for this particular scope, but not globally fresh.
+-- This class has a basic instance based on the reader monad.
+class Monad m => LFresh m where
+  -- | pick a new name that is fresh for the current (implicit) scope.
+  lfresh  :: Rep a => Name a -> m (Name a)
+  -- | avoid these names when freshening in the subcomputation.
+  avoid   :: [AnyName] -> m a -> m a
+
+-- | Reader monad instance for local freshness class.
+instance LFresh (Reader Integer) where
+  lfresh (Nm r (s,j)) = do { n <- ask; return (Nm r (s, max j (n+1))) }
+  avoid []          = id
+  avoid names       = local (max k) where
+        k = maximum (map anyName2Integer names)
+
+-- | Destruct a binding in the LFresh monad.
+lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> m (a, b)
+lunbind (B a b) =
+  avoid (S.elems $ fv' initial b) $ error "UNIMP"
+
+
+lunbind2  :: (LFresh m, Alpha b, Alpha c, Alpha d) =>
+            Bind b c -> Bind b d -> m (Maybe (b,c,d))
+lunbind2 (B b1 c) (B b2 d) = do
+      case match b1 b2 of
+         Just _ -> do
+           (b', c') <- lunbind (B b1 c)
+           return $ error "UNIMP"
+         Nothing -> return Nothing
+
+lunbind3  :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) =>
+            Bind b c -> Bind b d -> Bind b e ->  m (Maybe (b,c,d,e))
+lunbind3 (B b1 c) (B b2 d) (B b3 e) = do
+      case (match b1 b2, match b1 b3) of
+         (Just _, Just _) -> do
+           (b', c') <- lunbind (B b1 c)
+           return $ error "UNIMP"
+         _ -> return Nothing
+
+
+---------------------------------------------------------------
+
+-- | Capture-avoiding substitution, in a monad so that we can rename
+-- variables at binding locations and avoid capture
+
+subst :: (Alpha a, Alpha b, Subst b a) => Name b -> b -> a -> a
+subst n u x =
+ runReader (avoid ([AnyName n] ++ (S.elems $ fv' initial u)++(S.elems $ fv' initial x)) $ lsubst n u x) (0 :: Integer)
+
+substs :: (Alpha a, Alpha b, Subst b a) => [Name b] -> [b] -> a -> a
+substs ns us x =
+ runReader (avoid ((map AnyName ns) ++ (concatMap (S.elems . (fv' initial)) us)++(S.elems $ fv' initial x)) $ lsubsts ns us x)
+     (0 :: Integer)
+
+
+class (Rep1 (SubstD b) a) => Subst b a where
+  isvar :: a -> Maybe (Name b, b -> a)
+  isvar x = Nothing
+
+  lsubst :: LFresh m => Name b -> b -> a -> m a
+  lsubst n u x =
+      case isvar x of
+        Just (m, f) | m == n -> return (f u)
+        Just (_, _) -> return x
+        Nothing -> substR1 rep1 n u x
+
+
+  lsubsts :: LFresh m => [Name b] -> [b] -> a -> m a
+  lsubsts ns us x =
+      case isvar x of
+        Just (m, f) -> case m `List.elemIndex` ns of
+                    Just i  -> return (f (us !! i))
+                    Nothing -> return x
+        Nothing -> substsR1 rep1 ns us x
+
+
+data SubstD b a = SubstD {
+   substD  :: LFresh m => Name b -> b -> a -> m a
+  ,substsD :: LFresh m => [Name b] -> [b] -> a -> m a
+}
+
+instance Subst b a => Sat (SubstD b a) where
+  dict = SubstD lsubst lsubsts
+
+substR1 :: LFresh m => R1 (SubstD b) a -> Name b -> b -> a -> m a
+substR1 (Data1 _ cons) = \ x y d ->
+  case (findCon cons d) of
+  Val c rec kids -> do
+      w <- mapM_l (\z -> substD z x y) rec kids
+      return (to c w)
+substR1 _               = \ _ _ c -> return c
+
+substsR1 :: LFresh m => R1 (SubstD b) a -> [Name b] -> [b] -> a -> m a
+substsR1 (Data1 _ cons) = \ x y d ->
+  case (findCon cons d) of
+  Val c rec kids -> do
+      z <- mapM_l (\ w -> substsD w x y) rec kids
+      return (to c z)
+substsR1 _               = \ _ _ c -> return c
+
+instance Subst c AnyName where
+
+instance Subst b Int where
+instance Subst b Bool where
+instance Subst b () where
+instance Subst b Char where
+instance Subst b Integer where
+instance Subst b Float where
+instance Subst b Double where
+instance (Subst c a, Subst c b) => Subst c (a,b) where
+instance (Subst c a, Subst c b, Subst c d) => Subst c (a,b,d) where
+instance (Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a,b,d,e) where
+instance (Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a,b,d,e,f) where
+
+instance (Subst c a) => Subst c [a] where
+instance (Subst c a) => Subst c (Maybe a) where
+instance (Subst c a, Subst c b) => Subst c (Either a b) where
+
+instance Rep a => Subst b (R a) where
+instance Rep a => Subst b (Name a) where
+
+
+instance (Subst c a, Alpha a, Subst c b, Alpha b) =>
+    Subst c (Bind a b) where
+  lsubst n u (B a b) =
+      lfreshen' Term a ( \ a' p -> do
+         let b' = swapall' Term p b
+         a'' <- lsubst n u a'
+         b'' <- lsubst n u b'
+         return (B a'' b''))
+
+  lsubsts n u (B a b) =
+      lfreshen' Term a ( \ a' p -> do
+         a'' <- lsubsts n u a'
+         let b' = swaps' Pat p (swaps' Term p b)
+         b'' <- lsubsts n u b'
+         return (B a'' b''))
+
+instance (Subst c b, Subst c a, Alpha a, Alpha b) =>
+    Subst c (Rebind a b) where
+instance (Subst c a) => Subst c (Embed a) where
+
+
+-------------------- TESTING CODE --------------------------------
+data Exp = V (Name Exp)
+         | A Exp Exp
+         | L (Bind (Name Exp) Exp) deriving (Show)
+
+$(derive [''Exp])
+
+instance Alpha Exp
+instance Subst Exp Exp where
+   isvar (V n) = Just (n, id)
+   isvar _     = Nothing
+
+-- deriving instance Eq Exp
+-- deriving instance Ord Exp
+
+nameA, nameB, nameC :: Name Exp
+nameA = string2Name "A"
+nameB = string2Name "B"
+nameC = string2Name "C"
+
+assert :: String -> Bool -> IO ()
+assert s True = return ()
+assert s False = print ("Assertion " ++ s ++ " failed")
+
+do_tests :: ()
+do_tests =
+   unsafePerformIO $ do
+   tests_aeq
+   tests_fv
+   tests_big
+   tests_subst
+
+perm = single (AnyName nameA)(AnyName nameB)
+
+naeq x y = not (aeq x y)
+
+a10a = bind (rebind (nameA, Embed nameC) ()) nameA
+a10b = bind (rebind (nameB, Embed nameC) ()) nameB
+
+a10c = bind (rebind (nameA, Embed nameA) ()) nameA
+a10d = bind (rebind (nameB, Embed nameA) ()) nameB
+
+tests_aeq = do
+   assert "a1" $ (bind nameA nameA) `naeq` (bind nameA nameB)
+   assert "a2" $ (bind nameA nameA) `aeq` (bind nameA nameA)
+   assert "a3" $ (bind nameA nameA) `aeq` (bind nameB nameB)
+   assert "a4" $ (bind nameA nameB) `naeq` (bind nameB nameA)
+   assert "a5" $ (bind (nameA, Embed nameB) nameA) `naeq`
+                 (bind (nameA, Embed nameC) nameA)
+   assert "a6" $ (bind (nameA, Embed nameB) nameA) `aeq`
+                 (bind (nameA, Embed nameB) nameA)
+   assert "a7" $ (bind (nameA, Embed nameB) nameA) `aeq`
+                 (bind (nameB, Embed nameB) nameB)
+   assert "a8" $ rebind nameA nameB `naeq` rebind nameB nameB
+   assert "a9" $ rebind nameA nameA `naeq` rebind nameB nameB
+   assert "a9a" $ (bind (rebind nameA (Embed nameA)) nameA) `aeq`
+                  (bind (rebind nameB (Embed nameB)) nameB)
+   assert "a10" $ bind (rebind (nameA, Embed nameA) ()) nameA `aeq`
+                  bind (rebind (nameB, Embed nameA) ()) nameB
+   assert "a10a" $ a10a `aeq` a10b
+   assert "a11" $ bind (rebind (nameA, Embed nameA) ()) nameA `naeq`
+                  bind (rebind (nameB, Embed nameB) ()) nameB
+   assert "a12" $ bind (Embed nameA) () `naeq` bind (Embed nameB) ()
+   assert "a13" $ bind (Embed nameA) () `aeq` bind (Embed nameA) ()
+   assert "a14" $ bind (rebind (Embed nameA) ()) () `naeq`
+                  bind (rebind (Embed nameB) ()) ()
+   assert "a15" $ (rebind (nameA, Embed nameA) ()) `naeq`
+                  (rebind (name4, Embed nameC) ())
+   assert "a16" $ bind (nameA, nameB) nameA `naeq`
+                  bind (nameB, nameA) nameA
+   assert "a17" $ bind (nameA, nameB) nameA `naeq` bind (nameA, nameB) nameB
+   assert "a18" $ (nameA, nameA) `naeq` (nameA, nameB)
+   assert "a19" $ match (nameA, nameA) (nameB, nameC) == Nothing
+   assert "a20" $ (L (bind name2 (L (bind name3 (L (bind name4  (A (V name2) (A (V name3) (V name4))))))))) `aeq`  (L (bind name1 (L (bind name2 (L (bind name3  (A (V name1) (A (V name2) (V name3)))))))))
+
+emptyNE :: Set (Name Exp)
+emptyNE = S.empty
+
+tests_fv = do
+   assert "f1" $ fv (bind nameA nameA) == emptyNE
+   assert "f2" $ fv' Pat (bind nameA nameA) == S.empty
+   assert "f3" $ fv (bind (rebind nameA (Embed nameA)) nameA) == emptyNE
+   assert "f4" $ fv (bind nameA nameB) == S.singleton nameB
+   assert "f5" $ fv (bind (nameA, Embed nameB) nameA) == S.singleton nameB
+   assert "f7" $ fv (bind (nameB, Embed nameB) nameB) == S.singleton nameB
+   assert "f8" $ fv (rebind nameA nameB) == S.fromList [nameA, nameB]
+   assert "f9" $ fv' Pat (rebind nameA nameA) == S.empty
+   assert "f9a" $ fv (rebind nameA (Embed nameA)) == S.singleton nameA
+   assert "f9b" $ fv' Pat (rebind nameA (Embed nameA)) == S.empty
+   assert "f10" $ fv (rebind (nameA, Embed nameA) ()) == S.singleton nameA
+   assert "f11" $ fv' Pat (rebind (nameA, Embed nameA) ()) == S.singleton (AnyName nameA)
+   assert "f10a" $ fv (rebind (nameA, Embed nameB) ()) == S.singleton nameA
+   assert "f11a" $ fv' Pat (rebind (nameA, Embed nameB) ()) == S.singleton (AnyName nameB)
+
+
+   assert "f12" $ fv (bind (Embed nameA) ()) == S.singleton nameA
+   assert "f12a" $ fv' Pat (bind (Embed nameA) ()) == S.singleton (AnyName nameA)
+
+   assert "f14" $ fv (rebind (Embed nameA) ()) == emptyNE
+   assert "f14a" $ fv' Pat (rebind (Embed nameA) ()) == S.singleton (AnyName nameA)
+
+tests_subst = do
+   assert "s1" $ subst nameA (V nameB) (V nameA) `aeq` (V nameB)
+   assert "s2" $ subst nameA (V nameB) (V nameC) `aeq` (V nameC)
+   assert "s3" $ subst nameA (V nameB) (L (bind nameA (V nameA))) `aeq`
+                                       (L (bind nameA (V nameA)))
+
+   assert "s4" $ subst nameA (V nameB) (L (bind nameB (V nameB))) `aeq`
+                                       (L (bind nameA (V nameA)))
+
+   assert "s5" $ subst nameA (V nameB) (L (bind nameC (V nameA))) `aeq`
+                                       (L (bind nameC (V nameB)))
+
+   assert "s6" $ subst nameA (V nameA) (L (bind nameC (V nameA))) `aeq`
+                                       (L (bind nameC (V nameA)))
+
+   assert "s7" $ subst nameA (V nameA) (L (bind nameA (V nameB))) `aeq`
+                                       (L (bind nameA (V nameB)))
+   assert "s9" $ subst name1 (V name1)
+                  (L (bind name1 (L (bind name2 (L (bind name3
+                           (A (V name1) (A (V name2) (V name3))))))))) `aeq`
+                  (L (bind name1 (L (bind name2 (L (bind name3
+                           (A (V name1) (A (V name2) (V name3)))))))))
+
+
+mkbig :: [Name Exp] -> Exp -> Exp
+mkbig (n : names) body =
+    L (bind n (mkbig names (A (V n) body)))
+mkbig [] body = body
+
+big1 = mkbig (map integer2Name (take 100 [1 ..])) (V name11)
+big2 = mkbig (map integer2Name (take 101 [1 ..])) (V name11)
+
+tests_big = do
+   assert "b1" $ big1 `naeq` big2
+   assert "b2" $ fv big1 == emptyNE
+   assert "b3" $ big1 `aeq` subst name11 (V name11) big1
+
+
+ Unbound/Nominal/Name.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE RankNTypes
+           , TemplateHaskell
+           , GADTs
+           , FlexibleInstances
+           , MultiParamTypeClasses
+  #-}
+----------------------------------------------------------------------
+-- |
+-- Module      :  Unbound.Nominal.Name
+-- License     :  BSD-like (see LICENSE)
+--
+-- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>
+-- Stability   :  experimental
+-- Portability :  XXX
+--
+-- XXX write me
+----------------------------------------------------------------------
+
+module Unbound.Nominal.Name where
+-- XXX todo make explicit export list
+
+import Generics.RepLib
+
+-- | 'Name's are things that get bound.  This type is intentionally
+--   abstract; to create a 'Name' you can use 'string2Name' or
+--   'integer2Name'. The type parameter is a tag, or /sort/, which tells
+--   us what sorts of things this name may stand for. The sort must
+--   be an instance of the 'Rep' type class.
+data Name a
+  = Nm (R a) (String, Integer)   -- free names
+   deriving (Eq, Ord)
+
+-- | A name with a hidden (existentially quantified) sort.
+data AnyName = forall a. Rep a => AnyName (Name a)
+
+-- AnyName has an existential in it, so we cannot create a complete
+-- representation for it, unfortunately.
+
+$(derive_abstract [''AnyName])
+
+instance Show AnyName where
+  show (AnyName n1) = show n1
+
+instance Eq AnyName where
+   (AnyName n1) == (AnyName n2) =
+      case gcastR (getR n1) (getR n2) n1 of
+           Just n1' -> n1' == n2
+           Nothing  -> False
+
+instance Ord AnyName where
+   compare (AnyName n1) (AnyName n2) =
+       case compareR (getR n1) (getR n2) of
+         EQ  -> case gcastR (getR n1) (getR n2) n1 of
+           Just n1' -> compare n1' n2
+           Nothing  -> error "Panic: equal types are not equal in Ord AnyName instance!"
+         ord -> ord
+
+------------------------------------------------------------
+-- Utilities
+------------------------------------------------------------
+
+-- some convenient names for testing
+name1, name2, name3, name4, name5, name6, name7, name8, name9, name10, name11
+  :: Rep a => Name a
+name1 = integer2Name 1
+name2 = integer2Name 2
+name3 = integer2Name 3
+name4 = integer2Name 4
+name5 = integer2Name 5
+name6 = integer2Name 6
+name7 = integer2Name 7
+name8 = integer2Name 8
+name9 = integer2Name 9
+name10 = integer2Name 10
+name11 = integer2Name 11
+
+--instance Read Name where
+--  read s = error "FIXME"
+
+instance Show (Name a) where
+  show (Nm _ ("",n)) = "_" ++ (show n)
+  show (Nm _ (x,0))  = x
+  show (Nm _ (x,n))  = x ++ (show n)
+
+-- | Get the integer index of a 'Name'.
+name2Integer :: Name a -> Integer
+name2Integer (Nm _ (_,x)) = x
+
+
+-- | Get the string part of a 'Name'.
+name2String :: Name a -> String
+name2String (Nm _ (s,_)) = s
+
+
+-- | Get the integer index of an 'AnyName'.
+anyName2Integer :: AnyName -> Integer
+anyName2Integer (AnyName nm) = name2Integer nm
+
+-- | Get the string part of an 'AnyName'.
+anyName2String :: AnyName -> String
+anyName2String (AnyName nm) = name2String nm
+
+toSortedName :: Rep a => AnyName -> Maybe (Name a)
+toSortedName (AnyName n) = gcastR (getR n) rep n
+
+-- | Create a 'Name' from an 'Integer'.
+integer2Name :: Rep a => Integer -> Name a
+integer2Name n = makeName "" n
+
+-- | Create a 'Name' from a 'String'.
+string2Name :: Rep a => String -> Name a
+string2Name s = makeName s 0
+
+-- | Convenient synonym for 'string2Name'.
+s2n :: Rep a => String -> Name a
+s2n = string2Name
+
+-- | Create a 'Name' from a @String@ and an @Integer@ index.
+makeName :: Rep a => String -> Integer -> Name a
+makeName s i = Nm rep (s,i)
+
+-- | Determine the sort of a 'Name'.
+getR :: Name a -> R a
+getR (Nm r _)   = r
+
+
+-- | Change the sort of a name
+translate :: (Rep b) => Name a -> Name b
+translate (Nm _ x) = Nm rep x
+
+ Unbound/PermM.hs view
@@ -0,0 +1,133 @@+----------------------------------------------------------------------+-- |+-- Module      :  Unbound.Perm+-- Copyright   :  ???+-- License     :  BSD+--+-- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>+-- Stability   :  experimental+-- Portability :  portable+--+-- A slow, but hopefully correct implementation of permutations.+--+----------------------------------------------------------------------++module Unbound.PermM (+    Perm, single, compose, apply, support, isid, join, empty, restrict, mkPerm+  ) where++import Data.Monoid+import Data.List+import Data.Map (Map)+import qualified Data.Map as Map+import System.IO.Unsafe++(<>) :: Monoid m => m -> m -> m+(<>) = mappend++newtype Perm a = Perm (Map a a)++instance Ord a => Eq (Perm a) where+  (Perm p1) == (Perm p2) =+    all (\x -> Map.findWithDefault x x p1 == Map.findWithDefault x x p2) (Map.keys p1) &&+    all (\x -> Map.findWithDefault x x p1 == Map.findWithDefault x x p2) (Map.keys p2)++instance Show a => Show (Perm a) where+  show (Perm p) = show p++apply :: Ord a => Perm a -> a -> a+apply (Perm p) x = Map.findWithDefault x x p++single :: Ord a => a -> a -> Perm a+single x y = if x == y then Perm Map.empty else+    Perm (Map.insert x y (Map.insert y x Map.empty))++empty :: Perm a+empty = Perm Map.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 (Map.fromList ([ (x,Map.findWithDefault y y b) | (x,y) <- Map.toList a]+         ++ [ (x, Map.findWithDefault x x b) | x <- Map.keys b, Map.notMember x a]))++instance Ord a => Monoid (Perm a) where+  mempty  = empty+  mappend = compose++-- | isid -- do all keys map to themselves?+isid :: Ord a => Perm a -> Bool+isid (Perm p) =+     Map.foldrWithKey (\ a b r -> r && a == b) True p++-- | Join two permutation. Fail if the two permutations map the same+-- name to two different variables.+join :: Ord a => Perm a -> Perm a -> Maybe (Perm a)+join (Perm p1) (Perm p2) =+     let overlap = Map.intersectionWith (==) p1 p2 in+     if Map.fold (&&) True overlap then+       Just (Perm (Map.union p1 p2))+       else Nothing++support :: Ord a => Perm a -> [a]+support (Perm p) = [ x | x <- Map.keys p, Map.findWithDefault x x p /= x]++restrict :: Ord a => Perm a -> [a] -> Perm a+restrict (Perm p) l = Perm (foldl' (\p' k -> Map.delete k p') p l)++-- | @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 = foldl' (\mp p -> mp >>= join p)+                                    (Just empty)+                                    (zipWith single xs ys)+  | otherwise = Nothing++---------------------------------------------------------------------+seteq :: Ord a => [a] -> [a] -> Bool+seteq x y = nub (sort x) == nub (sort y)+++assert :: String -> Bool -> IO ()+assert s True = return ()+assert s False = print ("Assertion " ++ s ++ " failed")++do_tests :: ()+do_tests =+   unsafePerformIO $ do+     tests_apply+     tests_isid+     tests_support+     tests_join++tests_join = do+  assert "j1" $ join empty (empty :: Perm Int) == Just empty+  assert "j2" $ join (single 1 2) empty == Just (single 1 2)+  assert "j3" $ join (single 1 2) (single 2 1) == Just (single 1 2)+  assert "j4" $ join (single 1 2) (single 1 3) == Nothing++tests_apply = do+  assert "a1" $ apply empty 1 == 1+  assert "a2" $ apply (single 1 2) 1 == 2+  assert "a3" $ apply (single 2 1) 1 == 2+  assert "a4" $ apply ((single 1 2) <> (single 2 1)) 1 == 1++tests_isid = do+  assert "i1" $ isid (empty :: Perm Int) == True+  assert "i2" $ isid (single 1 2) == False+  assert "i3" $ isid (single 1 1) == True+  assert "i4" $ isid ((single 1 2) <> (single 1 2)) == True+  assert "i5" $ isid ((single 1 2) <> (single 2 1)) == True+  assert "i6" $ isid ((single 1 2) <> (single 3 2)) == False++tests_support = do+  assert "s1" $ support (empty :: Perm Int) `seteq` []+  assert "s2" $ support (single 1 2) `seteq` [1,2]+  assert "s3" $ support (single 1 1) `seteq` []+  assert "s4" $ support ((single 1 2) <> (single 1 2)) `seteq` []+  assert "s5" $ support ((single 1 2) <> (single 2 1)) `seteq` []+  assert "s6" $ support ((single 1 2) <> (single 3 2)) `seteq` [1,2,3]
+ Unbound/Util.hs view
@@ -0,0 +1,72 @@+module Unbound.Util where++import Data.Maybe (catMaybes)+import Data.Monoid+import qualified Data.Foldable as F++import qualified Data.Set as S+import qualified Data.Map as M++------------------------------------------------------------+-- Convenient Monoid syntax+------------------------------------------------------------++(<>) :: Monoid m => m -> m -> m+(<>) = mappend++------------------------------------------------------------+-- Collections+------------------------------------------------------------++-- | Collections are foldable types that support empty, singleton,+--   union, and map operations.  The result of a free variable+--   calculation may be any collection.  Instances are provided for+--   lists and sets.+class F.Foldable f => Collection f where+  emptyC    :: f a+  singleton :: a -> f a+  union     :: Ord a => f a -> f a -> f a+  cmap      :: (Ord a, Ord b) => (a -> b) -> f a -> f b++-- | Combine a list of containers into one.+unions :: (Ord a, Collection f) => [f a] -> f a+unions = foldr union emptyC++-- | Create a collection from a list of elements.+fromList :: (Ord a, Collection f) => [a] -> f a+fromList = unions . map singleton++-- | Remove the @Nothing@s from a collection.+filterC :: (Collection f, Ord a) => f (Maybe a) -> f a+filterC = fromList . catMaybes . F.toList++-- | Lists are containers under concatenation.  Lists preserve+--   ordering and multiplicity of elements.+instance Collection [] where+  emptyC    = []+  singleton = (:[])+  union     = (++)+  cmap      = map++-- | A simple representation of multisets.+newtype Multiset a = Multiset (M.Map a Int)++instance F.Foldable Multiset where+  fold (Multiset m) = M.foldrWithKey (\a n x -> mconcat (x : replicate n a)) mempty m++-- | Multisets are containers which preserve multiplicity but not+--   ordering.+instance Collection Multiset where+  emptyC                              = Multiset M.empty+  singleton                           = Multiset . flip M.singleton 1+  (Multiset m1) `union` (Multiset m2) = Multiset $ M.unionWith (+) m1 m2+  cmap f (Multiset m)                 = Multiset $ M.mapKeys f m++-- | Sets are containers under union, which preserve only occurrence,+--   not multiplicity or ordering.+instance Collection S.Set where+  emptyC    = S.empty+  singleton = S.singleton+  union     = S.union+  cmap      = S.map+
+ examples/Basic.hs view
@@ -0,0 +1,185 @@+-- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Main+-- Copyright   :  (c) The University of Pennsylvania, 2006+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+-- A file demonstrating the use of RepLib+--+-----------------------------------------------------------------------------++module Basic where++import Generics.RepLib+import Language.Haskell.TH+++-- For each datatype that we define, we need to also create its representation.+-- The template Haskell function derive does this automatically for+-- each type.++data Tree a = Leaf a | Node (Tree a) (Tree a)+$(derive [''Tree])++data Day = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday++$(derive [''Day])++-- Note, for mutually recursive datatypes, use "derive" and give list+-- of type names.++-- Note also that the functions of RepLib can cooperate with the+-- traditional 'deriving' mechanism+data Company   = C [Dept]                 deriving (Eq, Ord, Show)+data Dept      = D String Manager [CUnit] deriving (Eq, Ord, Show)+data Manager   = M Employee               deriving (Eq, Ord, Show)+data CUnit     = PU Employee | DU Dept    deriving (Eq, Ord, Show)+data Employee  = E Person Salary          deriving (Eq, Ord, Show)+data Person    = P String                 deriving (Eq, Ord, Show)+data Salary    = S Float                  deriving (Eq, Ord, Show)++$(derive+    [''Company,+     ''Dept,+     ''CUnit,+     ''Employee,+ 	  ''Manager,+ 	  ''Person,+ 	  ''Salary])+++--+-- Some sample data for these types+--+t1 :: Tree Int+t1 = Node (Node (Leaf 3) (Leaf 4)) (Node (Leaf 5) (Leaf 6))++t2 :: Tree Int+t2 = Node (Node (Leaf 0) (Leaf 7)) (Leaf 20)++s1 :: Company+s1 = C [D "Types" (M (E (P "Stephanie") (S 1000.0)))+            [PU (E (P "Michael") (S 50)),+             PU (E (P "Samuel") (S 50)),+             PU (E (P "Theodore") (S 50))],+        D "Terms" (M (E (P "Stephanie") (S 200)))+            [DU (D "Shipping" (M (E (P "Alice") (S 3000)))+                [])]]+++--+-- Prelude operations.+--+-- Note that we didn't derive Eq, Ord, Bounded or Show for "Day" and "Tree". We can+-- do that now with operations from RepLib.PreludeLib.++-- for Day+instance Eq Day      where+  (==) = eqR1 rep1+instance Ord Day     where+  compare = compareR1 rep1+instance Bounded Day where+  minBound = minBoundR1 rep1+  maxBound = maxBoundR1 rep1+instance Show Day    where+  showsPrec = showsPrecR1 rep1++-- for Tree+instance (Rep a, Eq a) => Eq (Tree a)     where (==) = eqR1 rep1+instance (Rep a, Show a) => Show (Tree a) where showsPrec = showsPrecR1 rep1+instance (Rep a, Ord a) => Ord (Tree a)   where compare = compareR1 rep1++-- Besides the prelude operations, RepLib provides a number of other+-- type-indexed operations.++--+-- Instances for RepLib.Lib operations+--++-- Generate creates arbitrary elements of a type, up to a certain depth.+instance Generate Day+instance Generate a => Generate (Tree a)+instance Generate Company+instance Generate Dept+instance Generate Manager+instance Generate CUnit+instance Generate Employee+instance Generate Person+instance Generate Salary+++-- Sum adds together all of the Ints in a datastructure+instance GSum a => GSum (Tree a)+instance GSum Company+instance GSum Dept+instance GSum Manager+instance GSum CUnit+instance GSum Employee+instance GSum Person+instance GSum Salary++-- Shrink creates smaller versions of a data structure.+instance Shrink a => Shrink (Tree a)++--+-- SYB Style operations+--+-- RepLib also supports many of the combinators from the SYB library. For example,+-- we can include the following code from the "Paradise" benchmark that gives everyone+-- in the company a raise.++-- Increase salary by percentage+increase :: Float -> Company -> Company+increase k = everywhere (mkT (incS k))++-- "interesting" code for increase+incS :: Float -> Salary -> Salary+incS k (S s) = S (s * (1+k))+++--+-- Generalized folds+--+-- finally, we define generalized versions of fold left and+-- fold right for the Tree type constructor.+instance Fold Tree where+  foldRight op = rreduceR1 (rTree1 (RreduceD { rreduceD = op })+                                   (RreduceD { rreduceD = foldRight op}))+  foldLeft  op = lreduceR1 (rTree1 (LreduceD { lreduceD = op })+                                   (LreduceD { lreduceD = foldLeft op }))++assert :: String -> Bool -> IO ()+assert s True  = return ()+assert s False = print ("Assertion " ++ s ++ " failed")+++main = do+   assert "m1" (minBound == Monday)+   assert "m2" (maxBound == Sunday)++   assert "e1" (t1 == Node (Node (Leaf 3) (Leaf 4)) (Node (Leaf 5) (Leaf 6)))++   assert "o3" (Monday < Tuesday)+   assert "o4" (not (t1 < t2))+--+   assert "g1" (generate 7 == [Monday,Tuesday,Wednesday,Thursday,Friday,Saturday,Sunday])+   assert "g2" ((generate 3 :: [Tree Int]) == [Leaf 0,Leaf 1,Leaf 2,Node (Leaf 0) (Leaf 0),Node (Leaf 0) (Leaf 1),Node (Leaf 0) (Node (Leaf 0) (Leaf 0)),Node (Leaf 1) (Leaf 0),Node (Leaf 1) (Leaf 1),Node (Leaf 1) (Node (Leaf 0) (Leaf 0)),Node (Node (Leaf 0) (Leaf 0)) (Leaf 0),Node (Node (Leaf 0) (Leaf 0)) (Leaf 1),Node (Node (Leaf 0) (Leaf 0)) (Node (Leaf 0) (Leaf 0))])++--+   assert "s1" (subtrees t1 == [Node (Leaf 3) (Leaf 4),Node (Leaf 5) (Leaf 6)])+   assert "s2" (gsum t1 == 18)+   assert "s3" (gsum t2 == 27)+--+   assert "i1" (increase 0.1 s1 == C [D "Types" (M (E (P "Stephanie") (S 1100.0))) [PU (E (P "Michael") (S 55.0)),PU (E (P "Samuel") (S 55.0)),PU (E (P "Theodore") (S 55.0))],D "Terms" (M (E (P "Stephanie") (S 220.0))) [DU (D "Shipping" (M (E (P "Alice") (S 3300.0))) [])]])++   assert "i2" (s1 < (increase 0.2 s1))+--+   assert "f1" (gproduct t1 == 360)+   assert "f2" (count t1 == 4)+
+ examples/DepCalc.hs view
@@ -0,0 +1,292 @@+{-# LANGUAGE PatternGuards+           , MultiParamTypeClasses+           , TemplateHaskell+           , ScopedTypeVariables+           , FlexibleInstances+           , FlexibleContexts+           , UndecidableInstances+  #-}++{- A "simple" core dependent calculus.++term     M ::= x | * | \D. M | M [N] | Pi D. B+             | T | c+             | case M with y of [ c [x] => N ]++tele     D ::= . | x:A, D++ctx      G ::= . | G, x:A++judgement forms:+    G |- D wf         telescope wellformedness+    G |- [ M ] : D    check a list of terms against a telescope+    G |- chk M : A    check that term M has type A+    G |- inf M : A    infer the type of M (which is A)+    G |- A == B       check that A & B are equal++typing rules:++     telescope well formedness   (checkTele)++     G |-chk A : *    G,x:A |- D wf+     ----------------------------- cons+     G |- x:A, D wf++     ------------- nil+     G |- [] wf++     list of terms vs a telescope   (checks)++     G |-chk N : A    (G |- [N] : D)[x |-> N]+     -------------------------------------- cons+     G |- N, [N] : x:A,D++     -------------- nil+     G |- [] : .++     terms (check && infer)++     x:A \in G+     -----------+     G |- inf x : A++     G |- D wf        G, D |- chk B : *+     --------------------------------+     G |- inf Pi D.B : *++     G |- D wf        G, D |- inf M : B+     -------------------------------+     G |- inf \D.M : Pi D. B++     G |- inf M : Pi D.B      G |- [N] : D+     ---------------------------------------+     G |- inf M [N] : B [ D |-> [N] ]+       ** note: simultaneous substitution for the domain **++     ----------+     G |- inf * : *++     G |- inf  M : A    G |- A == B+     ----------------------------+     G |- chk  M : B++     A = Pi D . *+     T : A \in Sigma+     ---------------------+     G |- inf T : A++     c: A \in Sigma+     A = Pi D. Pi D'. T [x]+     dom(D) = [x]+     -------------+     G |- inf c : A++     G |- inf M : T [ P ]+     G |- chk A : *+     for each i,+         ci : Pi D. Pi Di. T [x] \in Sigma  where dom(D) = [x]+         G, Di[ D |-> [P] ], y : M = C [w] |- chk N : A+    ------------------------------------------------------+     G |-inf case M in A with y of [ c [w] => N ] : A++-}+++import Generics.RepLib+import Generics.RepLib.Bind.LocallyNameless++import Data.Monoid+import Control.Monad+import Control.Monad.Trans.Error++data TyCon    -- tags for the names of type constructors+data DataCon  -- and data constructors so that we don't get them+              -- confused with variables++-- initial context of data and type constructors+sigmaData :: [(Name DataCon, Exp)]+sigmaData = undefined++sigmaTy  :: [(Name TyCon, Exp)]+sigmaTy = undefined++teq :: Name TyCon+teq = string2Name "=="++data Exp = EVar (Name Exp)+         | EStar+         | ELam (Bind Tele Exp)+         | EApp Exp [Exp]+         | EPi (Bind Tele Exp)+         | ETyCon (Name TyCon)+         | EDataCon (Name DataCon)+         | ECase Exp Exp (Bind (Name Exp)+                    [(Name DataCon,Bind [Name Exp] Exp)])+  deriving Show++data Tele = Empty+          | Cons (Rebind (Name Exp, Annot Exp) Tele)+  deriving Show++type Ctx  = [ (Name Exp, Exp) ]++$(derive [''TyCon, ''DataCon, ''Exp, ''Tele])++instance Alpha Exp+instance Alpha Tele++instance Subst Exp Exp where+  isvar (EVar v) = Just (SubstName v)+  isvar _        = Nothing++instance Subst Exp Tele++------------------------------------------------++-- for examples++evar :: String -> Exp+evar = EVar . string2Name++elam :: [(String, Exp)] -> Exp -> Exp+elam t b = ELam (bind (mkTele t) b)++epi :: [(String, Exp)] -> Exp -> Exp+epi t b = EPi (bind (mkTele t) b)++earr :: Exp -> Exp -> Exp+earr t1 t2 = epi [("_", t1)] t2++eapp :: Exp -> Exp -> Exp+eapp a b = EApp a [b]++mkTele :: [(String, Exp)] -> Tele+mkTele []          = Empty+mkTele ((x,e) : t) = Cons (rebind (string2Name x, Annot e) (mkTele t))++{- Polymorphic identity function -}++pid :: Exp+pid = elam [("A", EStar), ("x", evar "A")] (evar "x")++{-+ELam (<(Cons (<<(A,{EStar})>> Cons (<<(x,{EVar 0@0})>> Empty)))> EVar 0@1)+-}++{- Polymorphic identity type: -}+sid :: Exp+sid = epi [("A", EStar), ("x", evar "A")] (evar "A")++{-+EPi (<(Cons (<<(A,{EStar})>> Cons (<<(x,{EVar 0@0})>> Empty)))> EVar 0@0)+-}++{- Polymorphic identity type: -}+sid2 :: Exp+sid2 = epi [("B", EStar), ("y", evar "B")] (evar "B")+++----------------------------------------------------------+-- Type checker++type M = ErrorT String FreshM+ok = return ()++runM :: M a -> a+runM m = case (runFreshM (runErrorT m)) of+   Left s  -> error s+   Right a -> a++lookUp :: Name a -> [(Name a, b)] -> M b+lookUp n []     = throwError $ "Not in scope: " ++ show n+lookUp v ((x,a):t') | v == x    = return a+                    | otherwise = lookUp v t'++unPi :: Ctx -> Exp -> M (Bind Tele Exp)+unPi g (EPi bnd) = return bnd+unPi g e         = throwError $ "Expected pi type, got " ++ show e ++ " instead"++unVar :: Exp -> M (Name Exp)+unVar (EVar x) = return x+unVar e        = throwError $ "Expected variable, got " ++ show e ++ " instead"++unTApp :: Ctx -> Exp -> M (Name TyCon, [Exp])+unTApp _ (EApp (ETyCon n) args) = return (n, args)+unTApp _ e = throwError $ "Expected datatype, got " ++ show e++ " instead"++-- Check a telescope and push it onto the context+checkTele :: Ctx -> Tele -> M Ctx+checkTele g Empty = return g+checkTele g (Cons rb) = do+  let ((x,Annot t), tele) = unrebind rb+  a <- infer g t+  check g a EStar+  checkTele ((x,t) : g) tele++infer :: Ctx -> Exp -> M Exp+infer g (EVar x)  = lookUp x g+infer _ EStar     = return EStar+infer g (ELam bnd) = do+    (delta, m) <- unbind bnd+    g' <- checkTele g delta+    b <- infer g' m+    return . EPi $ bind delta b+infer g (EApp m ns) = do+    bnd <- (unPi g) =<< infer g m+    (delta, b) <- unbind bnd+    checks g ns delta  --- ensures that the length ns == length (binders delta)+    return $ substs (zip (binders delta) ns) b+infer g (EPi bnd) = do+    (delta, b) <- unbind bnd+    g' <- checkTele g delta+    check g' b EStar+    return EStar+infer g (ETyCon n) = do+    bnd <- (unPi g) =<< lookUp n sigmaTy+    (delta, t) <- unbind bnd+    checkEq g t EStar+    return $ EPi bnd+infer g (EDataCon c) = do+  bnd <- (unPi g) =<< lookUp c sigmaData+  (delta, t) <- unbind bnd+  bnd' <- unPi g t+  (delta', EApp (ETyCon _) vars) <- unbind bnd'+  vs <- mapM unVar vars+  if vs == binders delta then return $ EPi bnd+     else throwError $ "incorrect result type for " ++ show (EDataCon c)+infer g (ECase m a bnd) = do+   check g a EStar+   (y, brs) <- unbind bnd+   t <- infer g m+   (n, ps)  <- unTApp g t+   _ <- mapM (checkBr y ps) brs+   return a+    where+      checkBr y ps (c,bnd) = do+         cbnd <- (unPi g) =<< lookUp c sigmaData+         (delta, rest) <- unbind cbnd+         cbnd' <- unPi g rest+         Just (deltai, _, ws, n) <- unbind2 cbnd' bnd+         g' <- checkTele g (substs (zip (binders delta) ps) deltai)+         let g'' = (y, EApp (ETyCon teq) [m, (EApp (EDataCon c) (map EVar ws))]): g'+         check g' n a++check :: Ctx -> Exp -> Exp -> M ()+check g m a = do+  b <- infer g m+  checkEq g b a++checks :: Ctx -> [Exp] -> Tele -> M ()+checks _ [] Empty = ok+checks g (e:es) (Cons rb) = do+  let ((x, Annot a), t') = unrebind rb+  check g e a+  checks (subst x e g) (subst x e es) (subst x e t')+checks _ _ _ = throwError $ "Unequal number of parameters and arguments"+++-- A conservative, inexpressive notion of equality, just for the sake+-- of the example.+checkEq :: Ctx -> Exp -> Exp -> M ()+checkEq _ e1 e2 = if aeq e1 e2 then return () else throwError $ "Couldn't match: " ++ show e1 ++ " " ++ show e2+
+ examples/F.hs view
@@ -0,0 +1,140 @@+{-# LANGUAGE TemplateHaskell, +             ScopedTypeVariables,+             FlexibleInstances,+             MultiParamTypeClasses,+             FlexibleContexts,+             UndecidableInstances, +             GADTs #-}++module F where++import Generics.RepLib+import Generics.RepLib.Bind.LocallyNameless+import Control.Monad+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++data Tm = TmVar TmName+        | Lam (Bind (TmName, Annot Ty) Tm) +        | TLam (Bind TyName Tm)+        | App Tm Tm+        | TApp Tm Ty+   deriving Show++$(derive [''Ty, ''Tm])++------------------------------------------------------  +instance Alpha Ty where   +instance Alpha Tm where++instance Subst Tm Ty where+instance Subst Tm Tm where+  isvar (TmVar x) = Just (SubstName x)+  isvar _  = Nothing+instance Subst Ty Ty where+  isvar (TyVar x) = Just (SubstName x)+  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 (TyVar a) (bind x (TmVar x))))++-- All a. a -> a+polyidty :: Ty+polyidty = All (bind a (Arr (TyVar a) (TyVar a)))+++-----------------------------------------------------------------+-- Typechecker+-----------------------------------------------------------------+type Delta = [ TyName ]+type Gamma = [ (TmName, Ty) ]++data Ctx = Ctx { getDelta :: Delta , getGamma :: Gamma }+emptyCtx = Ctx { getDelta = [], getGamma = [] }++type M = ErrorT String FreshM++runM :: M a -> a +runM m = case (runFreshM (runErrorT m)) of+   Left s  -> error s+   Right a -> a ++checkTyVar :: Ctx -> TyName -> M ()+checkTyVar g v = do +    if List.elem v (getDelta g) then +      return ()+    else +      throwError "NotFound" ++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 x) = +   checkTyVar g x +tcty g  (All b) = do +   (x, ty') <- unbind b+   tcty (extendTy x g) ty'+tcty g  (Arr t1 t2) = do +   tcty g  t1 +   tcty g  t2++ti :: Ctx -> Tm -> M Ty+ti g (TmVar x) = lookupTmVar g x +ti g (Lam ty1 bnd) = do +  (x, t) <- unbind bnd+  tcty g ty1+  ty2 <- ti (extendTm x ty1 g) t+  return (Arr ty1 ty2)+ti g (App t1 t2) = do +  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 +  (x, t) <- unbind bnd+  ty <- ti (extendTy x g) t+  return (All (bind x ty))+ti g (TApp t ty) = do+  tyt <- ti g t+  case tyt of+   (All b) -> do +      tcty g  ty +      (n1, ty1) <- unbind b+      return $ subst n1 ty ty1+
+ examples/LC-smallstep.hs view
@@ -0,0 +1,94 @@+-- Untyped lambda calculus, with small-step evaluation and an example parser++{-# LANGUAGE PatternGuards+           , MultiParamTypeClasses+           , TemplateHaskell+           , ScopedTypeVariables+           , FlexibleInstances+           , FlexibleContexts+           , UndecidableInstances+  #-}+import Control.Applicative+import Control.Arrow+import Control.Monad++import Control.Monad.Trans.Maybe++import Text.Parsec hiding ((<|>))+import qualified Text.Parsec.Token as P+import Text.Parsec.Language (haskellDef)++import Generics.RepLib.Bind.LocallyNameless+import Generics.RepLib++data Term = Var (Name Term)+          | App Term Term+          | Lam (Bind (Name Term) Term)+  deriving Show++$(derive [''Term])++instance Alpha Term+instance Subst Term Term where+  isvar (Var v) = Just (SubstName v)+  isvar _       = Nothing++done :: MonadPlus m => m a+done = mzero++step :: Term -> MaybeT FreshM Term+step (Var _) = done+step (Lam _) = done+step (App (Lam b) t2) = do+  (x,t1) <- unbind b+  return $ subst x t2 t1+step (App t1 t2) =+      App <$> step t1 <*> pure t2+  <|> App <$> pure t1 <*> step t2++tc :: Monad m => (a -> MaybeT m a) -> (a -> m a)+tc f a = do+  ma' <- runMaybeT (f a)+  case ma' of+    Just a' -> tc f a'+    Nothing -> return a++eval :: Term -> Term+eval x = runFreshM (tc step x)++-- Some example terms++lam :: String -> Term -> Term+lam x t = Lam $ bind (string2Name x) t++var :: String -> Term+var = Var . string2Name++idT = lam "y" (var "y")++foo = lam "z" (var "y")++trueT  = lam "x" (lam "y" (var "x"))+falseT = lam "x" (lam "x" (var "x"))++-- A small parser for Terms+lexer = P.makeTokenParser haskellDef+parens   = P.parens lexer+brackets = P.brackets lexer+ident    = P.identifier lexer++parseTerm = parseAtom `chainl1` (pure App)++parseAtom = parens parseTerm+        <|> var <$> ident+        <|> lam <$> (brackets ident) <*> parseTerm++runTerm :: String -> Either ParseError Term+runTerm = (id +++ eval) . parse parseTerm ""++{- example, 2 + 3 = 5:++    *Main> runTerm "([m][n][s][z] m s (n s z)) ([s] [z] s (s z)) ([s][z] s (s (s z))) s z"+    Right (App (Var s) (App (Var s) (App (Var s) (App (Var s) (App (Var s) (Var z))))))++-}
+ examples/LC.hs view
@@ -0,0 +1,142 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,+    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving+ #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  LC+-- Copyright   :  (c) The University of Pennsylvania, 2010+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+--+--+-----------------------------------------------------------------------------++-- | A very simple example demonstration of the binding library+-- based on the untyped lambda calculus.+module LC where++import Generics.RepLib+import Generics.RepLib.Bind.LocallyNameless+import Control.Monad.Reader (Reader, runReader)+import Data.Set as S++-- | A Simple datatype for the Lambda Calculus+data Exp = Var (Name Exp)+         | Lam (Bind (Name Exp) Exp)+         | App Exp Exp+  deriving Show++-- Use RepLib to derive representation types+$(derive [''Exp])++-- | With representation types, tbe default implementation of Alpha+-- provides alpha-equivalence and free variable calculation.+instance Alpha Exp++-- | The subst class uses generic programming to implement capture+-- avoiding substitution. It just needs to know where the variables+-- are.+instance Subst Exp Exp where+   isvar (Var x) = Just (SubstName x)+   isvar _       = Nothing+++-- | All new functions should be defined in a monad that can generate+-- locally fresh names. ++type M a = FreshM a++-- | Beta-Eta equivalence for lambda calculus terms.+-- If the terms have a normal form+-- then the algorithm will terminate. Otherwise, the algorithm may+-- loop for certain inputs.+(=~) :: Exp -> Exp -> M Bool+e1 =~ e2 | e1 `aeq` e2 = return True+e1 =~ e2 = do+    e1' <- red e1+    e2' <- red e2+    if e1' `aeq` e1 && e2' `aeq` e2+      then return False+      else e1' =~ e2'+++-- | Parallel beta-eta reduction for lambda calculus terms.+-- Do as many reductions as possible in one step, while still ensuring+-- termination.+red :: Exp -> M Exp+red (App e1 e2) = do+  e1' <- red e1+  e2' <- red e2+  case e1' of+    -- look for a beta-reduction+    Lam bnd -> do+        (x, e1'') <- unbind bnd+        return $ subst x e2' e1''+    otherwise -> return $ App e1' e2'+red (Lam bnd) = do+   (x, e) <- unbind bnd+   e' <- red e+   case e of+     -- look for an eta-reduction+     App e1 (Var y) | y == x && x `S.notMember` fv e1 -> return e1+     otherwise -> return (Lam (bind x e'))+red (Var x) = return $ (Var x)+++---------------------------------------------------------------------+-- Some testing code to demonstrate this library in action.++assert :: String -> Bool -> IO ()+assert s True  = return ()+assert s False = print ("Assertion " ++ s ++ " failed")++assertM :: String -> M Bool -> IO ()+assertM s c =+  if (runFreshM c) then return ()+  else print ("Assertion " ++ s ++ " failed")++x :: Name Exp+x = string2Name "x"++y :: Name Exp+y = string2Name "y"++z :: Name Exp+z = string2Name "z"++s :: Name Exp+s = string2Name "s"++lam :: Name Exp -> Exp -> Exp+lam x y = Lam (bind x y)++zero  = lam s (lam z (Var z))+one   = lam s (lam z (App (Var s) (Var z)))+two   = lam s (lam z (App (Var s) (App (Var s) (Var z))))+three = lam s (lam z (App (Var s) (App (Var s) (App (Var s) (Var z)))))++plus = lam x (lam y (lam s (lam z (App (App (Var x) (Var s)) (App (App (Var y) (Var s)) (Var z))))))++true = lam x (lam y (Var x))+false = lam x (lam y (Var y))+if_ x y z = (App (App x y) z)++main :: IO ()+main = do+  -- \x.x == \x.y+  assert "a1" $ lam x (Var x) `aeq` lam y (Var y)+  -- \x.x /= \x.y+  assert "a2" $ not (lam x (Var y) `aeq` lam x (Var x))+  -- \x.(\y.x) (\y.y) == \y.y+  assertM "be1" $ lam x (App (lam y (Var x)) (lam y (Var y))) =~ (lam y (Var y))+  -- \x. f x === f+  assertM "be2" $ lam x (App (Var y) (Var x)) =~ Var y+  assertM "be3" $ if_ true (Var x) (Var y) =~ Var x+  assertM "be4" $ if_ false (Var x) (Var y) =~ Var y+  assertM "be5" $ App (App plus one) two =~ three+
+ examples/LCRec.hs view
@@ -0,0 +1,156 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,+    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving+ #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  LC+-- Copyright   :  (c) The University of Pennsylvania, 2010+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+--+--+-----------------------------------------------------------------------------++-- | A very simple example demonstration of the binding library+-- based on the untyped lambda calculus.+module LCRec where++import Generics.RepLib+import Generics.RepLib.Bind.LocallyNameless+import Control.Monad.Reader (Reader, runReader)+import Data.Set as S+import Data.List as L++-- | A Simple datatype for the Lambda Calculus+data Exp = Var (Name Exp)+         | Lam (Bind (Name Exp) Exp)+         | App Exp Exp+         | Letrec (Bind (Rec [(Name Exp, Annot Exp)]) Exp)+  deriving Show++-- Use RepLib to derive representation types+$(derive [''Exp])++-- | With representation types, tbe default implementation of Alpha+-- provides alpha-equivalence and free variable calculation.+instance Alpha Exp++-- | The subst class uses generic programming to implement capture+-- avoiding substitution. It just needs to know where the variables+-- are.+instance Subst Exp Exp where+   isvar (Var x) = Just (SubstName x)+   isvar _       = Nothing+++-- | All new functions should be defined in a monad that can generate+-- locally fresh names. ++type M a = FreshM a++-- | Beta-Eta equivalence for lambda calculus terms.+-- If the terms have a normal form+-- then the algorithm will terminate. Otherwise, the algorithm may+-- loop for certain inputs.+(=~) :: Exp -> Exp -> M Bool+e1 =~ e2 | e1 `aeq` e2 = return True+e1 =~ e2 = do+    e1' <- red e1+    e2' <- red e2+    if e1' `aeq` e1 && e2' `aeq` e2+      then return False+      else e1' =~ e2'+++-- | Parallel beta-eta reduction for lambda calculus terms.+-- Do as many reductions as possible in one step, while still ensuring+-- termination.+red :: Exp -> M Exp+red (App e1 e2) = do+  e1' <- red e1+  e2' <- red e2+  case e1' of+    -- look for a beta-reduction+    Lam bnd -> do+        (x, e1'') <- unbind bnd+        return $ subst x e2' e1''+    otherwise -> return $ App e1' e2'+red (Lam bnd) = do+   (x, e) <- unbind bnd+   e' <- red e+   case e of+     -- look for an eta-reduction+     App e1 (Var y) | y == x && x `S.notMember` fv e1 -> return e1+     otherwise -> return (Lam (bind x e'))+red (Var x) = return $ (Var x)+red (Letrec bnd) = do +  (r, body) <- unbind bnd+  -- get the variable definitions+  let vars = unrec r+  -- substitute them all (once) throughout the body, iteratively+  let newbody = foldr (\ (x,Annot rhs) body -> subst x rhs body) body vars+  let fvs = fv newbody+  -- garbage collect, if possible+  if (L.any (\ (x,_) -> x `S.member` fvs) vars) then+    return $ Letrec (bind (rec vars) newbody)+  else return newbody++---------------------------------------------------------------------+-- Some testing code to demonstrate this library in action.++assert :: String -> Bool -> IO ()+assert s True  = return ()+assert s False = print ("Assertion " ++ s ++ " failed")++assertM :: String -> M Bool -> IO ()+assertM s c =+  if (runFreshM c) then return ()+  else print ("Assertion " ++ s ++ " failed")++x :: Name Exp+x = string2Name "x"++y :: Name Exp+y = string2Name "y"++z :: Name Exp+z = string2Name "z"++s :: Name Exp+s = string2Name "s"++lam :: Name Exp -> Exp -> Exp+lam x y = Lam (bind x y)++zero  = lam s (lam z (Var z))+one   = lam s (lam z (App (Var s) (Var z)))+two   = lam s (lam z (App (Var s) (App (Var s) (Var z))))+three = lam s (lam z (App (Var s) (App (Var s) (App (Var s) (Var z)))))++plus = lam x (lam y (lam s (lam z (App (App (Var x) (Var s)) (App (App (Var y) (Var s)) (Var z))))))++true = lam x (lam y (Var x))+false = lam x (lam y (Var y))+if_ x y z = (App (App x y) z)++e = Letrec (bind (rec [(y, Annot(Var x)), (x, Annot (Var z))]) (Var y))++main :: IO ()+main = do+  -- \x.x == \x.y+  assert "a1" $ lam x (Var x) `aeq` lam y (Var y)+  -- \x.x /= \x.y+  assert "a2" $ not (lam x (Var y) `aeq` lam x (Var x))+  -- \x.(\y.x) (\y.y) == \y.y+  assertM "be1" $ lam x (App (lam y (Var x)) (lam y (Var y))) =~ (lam y (Var y))+  -- \x. f x === f+  assertM "be2" $ lam x (App (Var y) (Var x)) =~ Var y+  assertM "be3" $ if_ true (Var x) (Var y) =~ Var x+  assertM "be4" $ if_ false (Var x) (Var y) =~ Var y+  assertM "be5" $ App (App plus one) two =~ three+
+ examples/LF.hs view
@@ -0,0 +1,825 @@+{- Type checker for LF, based on algorithm in Harper and Pfennig, "On+   Equivalence and Canonical Forms in the LF Type Theory", ACM+   Transactions on Computational Logic, 2000.+-}++{-# LANGUAGE TemplateHaskell+           , ScopedTypeVariables+           , FlexibleInstances+           , MultiParamTypeClasses+           , FlexibleContexts+           , UndecidableInstances+           , TypeSynonymInstances+           , TypeFamilies+           , GeneralizedNewtypeDeriving+           , NoMonomorphismRestriction+  #-}++{- TODO:+   1. [ ] Fix parser to deal with infix type operators+   2. [ ] test on contents of qbf/+   3. [ ] tune for speed?+-}++module Main where++import Prelude hiding (lookup)++import Generics.RepLib.Bind.LocallyNameless+import Generics.RepLib.Bind.Fresh (contLFreshM)+import Generics.RepLib++import Text.Parsec hiding ((<|>))+import qualified Text.Parsec.Token as P+import Text.Parsec.Language (haskellDef)+import Text.Parsec.String+import qualified Text.Parsec.Expr as PE++import Text.PrettyPrint (Doc, (<+>), (<>), colon, comma, text, render, empty, integer, nest, vcat, ($+$))+import qualified Text.PrettyPrint as PP++import Control.Monad.Error+import Control.Monad.Reader+import Control.Monad.Identity+import Control.Applicative hiding (many)++import qualified Data.Map as M+import qualified Data.Set as S+import Data.List (sortBy, groupBy)+import Data.Function (on)+import Data.Ord (comparing)++import System.Environment++------------------------------+-- Syntax --------------------+------------------------------++-- Kinds+data Kind = KPi (Bind (Name Tm, Annot Ty) Kind) -- {x:ty} k+          | Type                                -- type+  deriving Show++-- Types, also called "Families"+data Ty   = TyPi (Bind (Name Tm, Annot Ty) Ty)  -- {x:ty} ty+          | TyApp Ty Tm                         -- ty tm+          | TyConst (Name Ty)                   -- a+  deriving Show++-- Terms, also called "Objects"+data Tm   = Lam (Bind (Name Tm, Annot Ty) Tm)   -- [x:ty] tm+          | TmApp Tm Tm                         -- tm tm+          | TmVar (Name Tm)                     -- x+  deriving Show+  -- Harper and Pfennig distinguish between term *variables* and term+  -- *constants*, but for our purposes there is no need to distinguish+  -- between them.++$(derive [''Kind, ''Ty, ''Tm])++instance Alpha Kind+instance Alpha Ty+instance Alpha Tm++-- There are no term variables in types or kinds, so we can just+-- use the default structural Subst instances.+instance Subst Tm Kind+instance Subst Tm Ty++-- For Tm we must implement isvar so the Subst instance knows about+-- term variables.+instance Subst Tm Tm where+  isvar (TmVar v) = Just (SubstName v)+  isvar _         = Nothing++-- A declaration is either+--   * a type constant declaration (a name and a kind),+--   * a term constant declaration (with optional type and definition), or+--   * a fixity/precedence declaration.+data Decl = DeclTy (Name Ty) Kind+          | DeclTm (Name Tm) (Maybe Ty) (Maybe Tm)+          | DeclInfix Op+  deriving Show++data Op = Op Assoc Integer (Name Tm)+  deriving Show++data Assoc = L | R+  deriving Show++-- A program is a sequence of declarations.+type Prog = [Decl]++--------------------+-- Erasure ---------+--------------------++-- Simple kinds and types (no dependency)+data SKind = SKType+           | SKArr STy SKind+  deriving (Eq, Show)+data STy   = STyConst (Name Ty)+           | STyArr STy STy+  deriving (Eq, Show)  -- structural equality is OK here, since there+                       -- are no bound variables.  Otherwise we could+                       -- use 'aeq' from+                       -- Generics.RepLib.Bind.LocallyNameless.++$(derive [''SKind, ''STy])++class Erasable t where+  type Erased t :: *+  erase :: t -> Erased t++instance Erasable Kind where+  type Erased Kind = SKind+  erase Type = SKType+  erase (KPi b) = SKArr (erase ty) (erase k)+    where ((_, Annot ty), k) = unsafeUnbind b+          -- this is actually safe since we ignore the name+          -- and promise to erase it from k.++instance Erasable Ty where+  type Erased Ty = STy+  erase (TyPi b)      = STyArr (erase t1) (erase t2)+    where ((_, Annot t1), t2) = unsafeUnbind b+  erase (TyApp ty _)  = erase ty+  erase (TyConst c)   = STyConst c++instance Erasable Tm where+  type Erased Tm = Tm+  erase t = t++instance (Erasable a, Erasable b) => Erasable (a,b) where+  type Erased (a,b) = (Erased a, Erased b)+  erase (x,y) = (erase x, erase y)++------------------------------+-- Signatures/contexts -------+------------------------------++data Context tm ty = C (M.Map (Name Tm) tm) (M.Map (Name Ty) ty)++emptyCtx :: Context tm ty+emptyCtx = C M.empty M.empty++extendTm :: Name Tm -> tm -> Context tm ty -> Context tm ty+extendTm x t (C tm ty) = C (M.insert x t tm) ty++extendTy :: Name Ty -> ty -> Context tm ty -> Context tm ty+extendTy x k (C tm ty) = C tm (M.insert x k ty)++lookupTm :: Name Tm -> TcM (Context tm ty) tm+lookupTm x = ask >>= \(C tm _) -> embedMaybe (text $ "Not in scope: term variable " ++ show x)+                                  (M.lookup x tm)++lookupTy :: Name Ty -> TcM (Context tm ty) ty+lookupTy x = ask >>= \(C _ ty) -> embedMaybe (text $ "Not in scope: type constant " ++ show x)+                                  (M.lookup x ty)++embedMaybe :: Doc -> Maybe a -> TcM ctx a+embedMaybe errMsg m = case m of+  Just a  -> return a+  Nothing -> err errMsg++addTrace :: Doc -> TcM ctx String+addTrace msg = do+  chks  <- getChkContext+  trace <- vcat <$> mapM ppr chks+  return . PP.render $ msg $+$ trace++embedEither :: (MonadError String m) => Either String a -> m a+embedEither = either throwError return++instance Erasable a => Erasable (M.Map k a) where+  type Erased (M.Map k a) = M.Map k (Erased a)+  erase = M.map erase++instance (Erasable tm, Erasable ty) => Erasable (Context tm ty) where+  type Erased (Context tm ty) = Context (Erased tm) (Erased ty)+  erase (C tm ty) = C (erase tm) (erase ty)++instance (Erasable a) => Erasable (Maybe a) where+  type Erased (Maybe a) = Maybe (Erased a)+  erase = fmap erase++type Ctx  = Context (Ty, Maybe Tm) Kind+type SCtx = Erased Ctx++withTmBinding :: (MonadReader (Context (tm, Maybe Tm) ty) m, LFresh m)+              => Name Tm -> tm -> m r -> m r+withTmBinding x b = do+  avoid [AnyName x] . local (extendTm x (b, Nothing))++withTmDefn :: (MonadReader (Context tm ty) m, LFresh m)+           => Name Tm -> tm -> m r -> m r+withTmDefn x b = do+  avoid [AnyName x] . local (extendTm x b)++withTyBinding :: (MonadReader (Context tm ty) m, LFresh m)+              => Name Ty -> ty -> m r -> m r+withTyBinding x b = do+  avoid [AnyName x] . local (extendTy x b)++-----------------------+-- Error reporting ----+-----------------------++-- Keep track of what we're in the middle of checking.+data Check = TyCheck Tm+           | KCheck Ty+           | SCheck Kind+           | TmEq Tm Tm STy+           | TyEq Ty Ty SKind+           | KEq Kind Kind+           | DeclCheck Decl++------------------------------+-- Typechecking monad --------+------------------------------++newtype TcM ctx a = TcM { unTcM :: ErrorT String (ReaderT ctx (ReaderT [Check] LFreshM)) a }+  deriving (Functor, Applicative, Monad, MonadReader ctx, MonadPlus, MonadError String, LFresh)++getTcMAvoids :: TcM ctx (S.Set AnyName)+getTcMAvoids = TcM . lift . lift . lift $ getAvoids++getChkContext :: TcM ctx [Check]+getChkContext = TcM . lift . lift $ ask++-- | Continue a TcM computation, given a binding context, a checking+--   context, and a set of names to avoid.+contTcM :: TcM ctx a -> ctx -> [Check] -> S.Set AnyName -> Either String a+contTcM (TcM m) c chks nms = flip contLFreshM nms . flip runReaderT chks . flip runReaderT c . runErrorT $ m++-- | Run a TcM computation in an empty context.+runTcM :: TcM (Context tm ty) a -> Either String a+runTcM m = contTcM m emptyCtx [] S.empty++-- | Run a subcomputation with an erased context.+withErasedCtx :: TcM SCtx a -> TcM Ctx a+withErasedCtx m = do+  c <- ask+  chks <- getChkContext+  nms <- getTcMAvoids+  embedEither $ contTcM m (erase c) chks nms++-- | Run a subcomputation with another check pushed on the checking+--   context stack.+whileChecking :: Check -> TcM ctx a -> TcM ctx a+whileChecking chk m = do+  c <- ask+  chks <- getChkContext+  nms <- getTcMAvoids+  embedEither $ contTcM m c (chk:chks) nms++ensure errMsg b = if b then return () else errMsg >>= err++err msg = addTrace msg >>= throwError++matchErr :: Pretty a => a -> a -> TcM ctx Doc+matchErr x y = do+  x' <- ppr x+  y' <- ppr y+  return $ text "Cannot match" <+> x' <+> text "with" <+> y'++unTyPi (TyPi bnd) = return bnd+unTyPi t = ppr t >>= \t' -> err $ text "Expected pi type, got" <+> t' <+> text "instead"++unKPi (KPi bnd) = return bnd+unKPi t = ppr t >>= \t' -> err $ text "Expected pi kind, got" <+> t' <+> text "instead"++isType Type = return ()+isType t = ppr t >>= \t' -> err $ text "Expected Type, got" <+> t' <+> text "instead"++------------------------------+-- Weak head reduction -------+------------------------------++-- Reduce a term to weak-head normal form, or return it unchanged if+-- it is not head-reducible.  Works in erased or unerased contexts.+whr :: Tm -> TcM (Context (t, Maybe Tm) ty) Tm+whr (TmVar a) = (do+  (_, Just defn) <- lookupTm a+  whr defn)+  `mplus`+  return (TmVar a)++whr (TmApp (Lam b) m1) =+  lunbind b $ \((x,_),m2) ->+    whr $ subst x m1 m2++whr (TmApp m1 m2) = do+  m1' <- whr m1+  case m1' of+    Lam _ -> whr (TmApp m1' m2)+    _     -> return $ TmApp m1' m2++whr t = return t++------------------------------+-- Term equality -------------+------------------------------++-- Type-directed term equality.  In context Delta, is M <==> N at+-- simple type tau?+tmEq :: Tm -> Tm -> STy -> TcM SCtx ()+tmEq m n t = whileChecking (TmEq m n t) $ tmEqWhr m n t++tmEqWhr :: Tm -> Tm -> STy -> TcM SCtx ()+tmEqWhr m n t = do+  m' <- whr m+  n' <- whr n+  whileChecking (TmEq m' n' t) $ tmEq' m' n' t -- XXX++  -- XXX todo: might be nice to have 'lfresh' and 'lfreshen', the+  -- first NOT taking an argument++  -- XXX todo: need nicer way of doing "string2Name"+-- Type-directed term equality on terms in WHNF+tmEq' :: Tm -> Tm -> STy -> TcM SCtx ()+tmEq' m n (STyArr t1 t2) = do+  x <- lfresh (string2Name "_x")+  withTmBinding x t1 $+    tmEq (TmApp m (TmVar x)) (TmApp n (TmVar x)) t2+tmEq' m n a@(STyConst {}) = do+  a' <- tmEqS m n+  ensure (matchErr a a') $ a == a'++-- Structural term equality.  Check whether two terms in WHNF are+-- structurally equal, and return their "approximate type" if so.+tmEqS :: Tm -> Tm -> TcM SCtx STy++tmEqS (TmVar a) (TmVar b) = do+  ensure (matchErr a b) $ a == b+  (tyA,_) <- lookupTm a  -- XXX+  return tyA++tmEqS (TmApp m1 m2) (TmApp n1 n2) = do+  ty <- tmEqS m1 n1+  case ty of+    STyArr t2 t1 -> do+      tmEq m2 n2 t2+      return t1+    _            -> do+      ty' <- ppr ty+      err $+        text "Left-hand side of an application has type" <+> ty' <> text "; expecting an arrow type"++tmEqS t1 t2 = err $ text "Term mismatch"++------------------------------+-- Type equality -------------+------------------------------++-- Kind-directed type equality.+tyEq :: Ty -> Ty -> SKind -> TcM SCtx ()+tyEq ty1 ty2 k = whileChecking (TyEq ty1 ty2 k) $ tyEq' ty1 ty2 k++tyEq' (TyPi bnd1) (TyPi bnd2) SKType =  -- XXX+  lunbind2 bnd1 bnd2 $ \(Just ((x, Annot a1), a2, (_, Annot b1), b2)) -> do+    tyEq a1 b1 SKType+    withTmBinding x (erase a1) $ tyEq a2 b2 SKType++tyEq' a b SKType = do+  t <- tyEqS a b+  ensure (matchErr t SKType) $ t == SKType++tyEq' a b (SKArr t k) = do+  x <- lfresh (string2Name "_x")+  withTmBinding x t $ tyEq (TyApp a (TmVar x)) (TyApp b (TmVar x)) k++-- Structural type equality.+tyEqS :: Ty -> Ty -> TcM SCtx SKind+tyEqS (TyConst a) (TyConst b) = do+  ensure (matchErr a b) $ a == b+  lookupTy a++tyEqS (TyApp a m) (TyApp b n) = do+  SKArr t k <- tyEqS a b  -- XXX+  tmEq m n t+  return k++tyEqS t1 t2 = do+  t1' <- ppr t1+  t2' <- ppr t2+  err $ text "Types are not equal: " <+> t1' <> comma <+> t2'++------------------------------+-- Kind equality -------------+------------------------------++-- Algorithmic kind equality.+kEq :: Kind -> Kind -> TcM SCtx ()++kEq Type Type = return ()++kEq k1@(KPi bnd1) k2@(KPi bnd2) = whileChecking (KEq k1 k2) $+  lunbind bnd1 $ \((x, Annot a), k) ->+  lunbind bnd2 $ \((_, Annot b), l) -> do+    tyEq a b SKType+    withTmBinding x (erase a) $ kEq k l++kEq k1 k2 = do+  k1' <- ppr k1+  k2' <- ppr k2+  err $ text "Kinds are not equal:" <+> k1' <> comma <+> k2'++------------------------------+-- Type checking -------------+------------------------------++-- Compute the type of a term.+tyCheck :: Tm -> TcM Ctx Ty+tyCheck tm = whileChecking (TyCheck tm) $ tyCheck' tm++tyCheck' :: Tm -> TcM Ctx Ty+tyCheck' t@(TmVar x)     = liftM fst $ lookupTm x+tyCheck' t@(TmApp m1 m2) = do+  bnd <- unTyPi =<< tyCheck m1+  a2  <- tyCheck m2+  lunbind bnd $ \((x, Annot a2'), a1) -> do+    withErasedCtx $ tyEq a2' a2 SKType+    return $ subst x m2 a1+tyCheck' t@(Lam bnd) =+  lunbind bnd $ \((x, Annot a1), m2) -> do+    isType =<< kCheck a1+    a2   <- withTmBinding x a1 $ tyCheck m2+    return $ TyPi (bind (x, Annot a1) a2)++-- Compute the kind of a type.+kCheck :: Ty -> TcM Ctx Kind+kCheck ty = whileChecking (KCheck ty) $ kCheck' ty++kCheck' :: Ty -> TcM Ctx Kind+kCheck' (TyConst a) = lookupTy a+kCheck' (TyApp a m) = do+  bnd <- unKPi =<< kCheck a+  b   <- tyCheck m+  lunbind bnd $ \((x, Annot b'), k) -> do+    withErasedCtx $ tyEq b' b SKType+    return $ subst x m k+kCheck' (TyPi bnd) =+  lunbind bnd $ \((x, Annot a1), a2) -> do+    isType =<< kCheck a1+    isType =<< (withTmBinding x a1 $ kCheck a2)+    return Type++-- Check the validity of a kind.+sortCheck :: Kind -> TcM Ctx ()+sortCheck k = whileChecking (SCheck k) $ sortCheck' k++sortCheck' :: Kind -> TcM Ctx ()+sortCheck' Type      = return ()+sortCheck' (KPi bnd) =+  lunbind bnd $ \((x, Annot a), k) -> do+    isType =<< kCheck a+    withTmBinding x a $ sortCheck k++------------------------------------------------------------+--  Parser  ------------------------------------------------+------------------------------------------------------------++type OpList = [Op]++mkOp :: Op -> PE.Operator String OpList Identity Tm+mkOp (Op a _ nm) = PE.Infix (TmApp . TmApp (TmVar nm) <$ sym (name2String nm))+                            (assoc a)+  where assoc L = PE.AssocLeft+        assoc R = PE.AssocRight++mkOpTable :: OpList -> PE.OperatorTable String OpList Identity Tm+mkOpTable = map (map mkOp) . groupBy ((==) `on` prec) . sortBy (flip $ comparing prec)+  where prec (Op _ n _) = n++type LFParser = Parsec String OpList++lfParseTest :: Show a => LFParser a -> String -> IO ()+lfParseTest p = print . runParser p [] ""++------------------------------+-- Lexing --------------------+------------------------------++startStuff = letter   <|> oneOf "!#$%&*+/<=>?@\\^|-~"+endStuff   = alphaNum <|> oneOf "!#$%&*+/<=>?@\\^|-~"++reservedNames = ["type", "infix", "right", "left"]+             ++ [":", "=", ".", "->", "%", "{", "}", "(", ")"]+++langDef = haskellDef { P.reservedNames   = reservedNames+                     , P.reservedOpNames = reservedNames+                     , P.identStart      = startStuff+                     , P.identLetter     = endStuff+                     , P.opStart         = startStuff+                     , P.opLetter        = endStuff+                     }++lexer    = P.makeTokenParser langDef++parens   = P.parens     lexer+braces   = P.braces     lexer+brackets = P.brackets   lexer+sym      = P.symbol     lexer+op       = P.reservedOp lexer+reserved = P.reserved   lexer+natural  = P.natural    lexer++var      = string2Name <$> P.identifier lexer++------------------------------+-- Terms ---------------------+------------------------------++parseTm :: LFParser Tm+parseTm = parseTmExpr `chainl1` (pure TmApp)++parseTmExpr :: LFParser Tm+parseTmExpr = do+  ops <- getState+  PE.buildExpressionParser (mkOpTable ops) parseAtom++parseAtom :: LFParser Tm+parseAtom = parens parseTm+        <|> TmVar <$> var+        <|> Lam <$> (+              bind+                <$> brackets ((,) <$> var+                                  <*> (Annot <$> (sym ":" *> parseTy))+                             )+                <*> parseTm+              )++------------------------------+-- Types ---------------------+------------------------------++parseTy :: LFParser Ty+parseTy  =+      -- ty ::=++      -- [x:ty] ty+      TyPi <$> (bind+         <$> braces ((,) <$> var+                         <*> (Annot <$> (sym ":" *> parseTy))+                    )+         <*> parseTy)++      -- te -> ty+  <|> try (TyPi <$> (bind+             <$> ((,) (string2Name "_") . Annot <$> parseTyExpr)+             <*> (op "->" *> parseTy)+          ))++      -- te+  <|> parseTyExpr++  -- XXX this does not handle type expressions built using infix type operators!+parseTyExpr :: LFParser Ty+  -- te ::= ta [tm ...]+parseTyExpr = foldl TyApp <$> parseTyAtom <*> many parseAtom++parseTyAtom :: LFParser Ty+parseTyAtom =+      -- ta ::=++      -- (ty)+      parens parseTy++      -- x+  <|> TyConst <$> var++------------------------------+-- Kinds ---------------------+------------------------------++parseKind :: LFParser Kind+parseKind =+      -- k ::=++      -- {x:ty} k+      KPi <$> (bind+       <$> braces ((,) <$> var+                       <*> (Annot <$> (sym ":" *> parseTy))+                  )+       <*> parseKind)++      -- ka -> k+  <|> try (KPi <$> (bind+             <$> ((,) (string2Name "_") . Annot <$> parseTyExpr)+             <*> (op "->" *> parseKind)+          ))++      -- ka+  <|> parseKindAtom++parseKindAtom :: LFParser Kind+parseKindAtom =+      -- ka ::=++      -- (k)+      parens parseKind++      -- Type+  <|> try (Type <$ reserved "type")++------------------------------+-- Declarations --------------+------------------------------++parseDecl :: LFParser Decl+parseDecl = declBody <* sym "."+ where+  declBody =+        DeclInfix <$> (Op <$> (sym "%" *> reserved "infix" *> rl)+                          <*> natural+                          <*> var)++    <|> try (DeclTy <$> var+                    <*> (sym ":" *> parseKind))++    <|> try (DeclTm <$> var+                    <*> (sym ":" *> (Just <$> parseTy))+                    <*> optionMaybe (sym "=" *> parseTm))++    <|>      DeclTm <$> var+                    <*> pure Nothing+                    <*> (sym "=" *> (Just <$> parseTm))+  rl = (L <$ reserved "left") <|> (R <$ reserved "right")++------------------------------+-- Programs ------------------+------------------------------++parseProg :: LFParser Prog+parseProg =+      -- stop at eof+      [] <$ eof++  <|> do d <- parseDecl  -- parse a single decl+         case d of       -- add fixity declarations to the state+           DeclInfix op -> modifyState (op:)+           _ -> return ()++         (d:) <$> parseProg  -- parse the rest of the program++----------------------------------------+-- Pretty-printing ---------------------+----------------------------------------++class Pretty p where+  ppr :: (LFresh m, Functor m) => p -> m Doc++instance Pretty (Name a) where+  ppr = return . text . show++dot = text "."++instance Pretty Decl where+  ppr (DeclTy t k) = do+    t' <- ppr t+    k' <- ppr k+    return $ t' <+> colon <+> k' <> dot+  ppr (DeclTm x mty mdef) = do+    x'   <- ppr x+    tyf  <- case mty of+              Nothing -> return id+              Just ty -> do ty' <- ppr ty+                            return (<+> (colon <+> ty'))+    deff <- case mdef of+              Nothing -> return id+              Just def -> do def' <- ppr def+                             return (<+> (text "=" <+> def'))+    return $ (deff . tyf $ x') <> dot+  ppr (DeclInfix op) = do+    op' <- ppr op+    return $ op' <> dot++instance Pretty Op where+  ppr (Op assoc prec op) = do+    op' <- ppr op+    return $+      text "%infix"+        <+> text (case assoc of L -> "left"; R -> "right")+        <+> integer prec+        <+> op'++instance Pretty Kind where+  ppr Type = return $ text "type"+  ppr (KPi bnd) = lunbind bnd $ \((x, Annot ty), k) -> do+    x'  <- ppr x+    ty' <- ppr ty+    k'  <- ppr k+    if x `S.member` fv k+      then return $ PP.braces (x' <> colon <> ty') <+> k'+      else return $ PP.parens ty' <+> text "->" <+> k'++instance Pretty Ty where+  ppr (TyApp ty tm) = do+    ty' <- ppr ty+    tm' <- ppr tm+    return $ ty' <+> PP.parens tm'+  ppr (TyConst c) = ppr c+  ppr (TyPi bnd) = lunbind bnd $ \((x, Annot ty1), ty2) -> do+    x' <- ppr x+    ty1' <- ppr ty1+    ty2' <- ppr ty2+    if x `S.member` fv ty2+      then return $ PP.braces (x' <> colon <> ty1') <+> ty2'+      else return $ PP.parens ty1' <+> text "->" <+> ty2'++instance Pretty STy where+  ppr sty = ppr (uneraseTy sty)++uneraseTy (STyConst c) = TyConst c+uneraseTy (STyArr t1 t2) = TyPi (bind (string2Name "_", Annot (uneraseTy t1)) (uneraseTy t2))++uneraseK SKType = Type+uneraseK (SKArr sty sk) = KPi (bind (string2Name "_", Annot (uneraseTy sty)) (uneraseK sk))++instance Pretty SKind where+  ppr sk = ppr (uneraseK sk)++instance Pretty Tm where+  ppr (TmVar x) = ppr x+  ppr (TmApp tm1 tm2) = do+    tm1' <- ppr tm1+    tm2' <- ppr tm2+    return $ tm1' <+> PP.parens tm2'+  ppr (Lam bnd) = lunbind bnd $ \((x, Annot ty), tm) -> do+    x' <- ppr x+    ty' <- ppr ty+    tm' <- ppr tm+    return $ PP.brackets (x' <> colon <> ty') <+> tm'++instance Pretty Check where+  ppr (TyCheck tm) =+    (text "While checking the type of:" <+>) <$> ppr tm+  ppr (KCheck ty) =+    (text "While checking the kind of:" <+>) <$> ppr ty+  ppr (SCheck k) =+    (text "While checking the sort of:" <+>) <$> ppr k+  ppr (TmEq m n ty) = do+    m' <- ppr m+    n' <- ppr n+    ty' <- ppr ty+    return $  text "While checking that terms:"+          $+$ nest 4 (m' $+$ n')+          $+$ nest 2 (text "are equal at type")+          $+$ nest 4 ty'+  ppr (TyEq t1 t2 k) = do+    t1' <- ppr t1+    t2' <- ppr t2+    k'  <- ppr k+    return $  text "While checking that types:"+          $+$ nest 4 (t1' $+$ t2')+          $+$ nest 2 (text "are equal at kind")+          $+$ nest 4 k'+  ppr (KEq k1 k2) = do+    k1' <- ppr k1+    k2' <- ppr k2+    return $ text "While checking equality of kinds:"+          $+$ nest 4 (k1' $+$ k2')+  ppr (DeclCheck decl) = do+    d' <- ppr decl+    return $ text "While checking the declaration:" $+$ nest 4 d'++------------------------------+-- Typechecking programs -----+------------------------------++checkProg :: Prog -> TcM Ctx ()+checkProg [] = return ()+checkProg (DeclInfix _ : ds) = checkProg ds+checkProg (d@(DeclTy nm k) : ds) = do+  whileChecking (DeclCheck d) $ sortCheck k+  withTyBinding nm k $ checkProg ds+checkProg ((DeclTm nm Nothing Nothing):_) = do+  throwError $ "Term " ++ show nm+    ++ " has no type or definition! (This shouldn't happen.)"+checkProg (d@(DeclTm nm (Just ty) Nothing) : ds) = do+  whileChecking (DeclCheck d) $ isType =<< kCheck ty+  withTmBinding nm ty $ checkProg ds+checkProg (d@(DeclTm nm Nothing (Just def)) : ds) = do+  ty <- whileChecking (DeclCheck d) $ tyCheck def+  withTmDefn nm (ty, Just def) $ checkProg ds+checkProg (d@(DeclTm nm (Just ty) (Just def)) : ds) = do+  whileChecking (DeclCheck d) $ do+    isType =<< kCheck ty+    ty'  <- tyCheck def+    withErasedCtx $ tyEq ty ty' SKType+  withTmDefn nm (ty, Just def) $ checkProg ds++checkLF :: [FilePath] -> IO ()+checkLF fileNames = do+  files <- mapM readFile fileNames+  case runParser parseProg [] "" (concat files) of+    Left err   -> print err+    Right prog -> do+      -- putStrLn . unlines . map render . runLFreshM . mapM ppr $ prog+      putStrLn . either ("Error: "++) (const "OK!") . runTcM . checkProg $ prog++main = do+  fileNames <- getArgs+  checkLF fileNames
+ examples/Main.hs view
@@ -0,0 +1,31 @@+-- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances +{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Main+-- Copyright   :  (c) The University of Pennsylvania, 2006+-- License     :  BSD+-- +-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Testsuite+--+-----------------------------------------------------------------------------++module Main where++import qualified Basic+import qualified LC+import qualified STLC+import qualified Abstract+++main = do+     Basic.main+     LC.main+     STLC.main+     Abstract.main+     print "Tests completed"+
+ examples/STLC.hs view
@@ -0,0 +1,193 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,+    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving+ #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  STLC+-- Copyright   :  (c) The University of Pennsylvania, 2010+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+--+--+-----------------------------------------------------------------------------++module STLC where++import Generics.RepLib+import Generics.RepLib.Bind.LocallyNameless+import Control.Monad.Reader+import Data.Set as S++data Ty = TInt | TUnit | Arr Ty Ty+  deriving (Show, Eq)+data Exp = Lit Int | Var Name | Lam (Bind Name Exp) | App Exp Ty Exp | EUnit+  deriving Show++-- Use RepLib to derive representation types+$(derive [''Ty,''Exp])++-- With representation types, default implementations of these+-- classes are available.+instance Alpha Ty where+instance Alpha Exp where++instance Subst Exp Ty where+instance Subst Exp Exp where+   isvar (Var x) = Just (SubstName x)+   isvar _       = Nothing++-- Equivalence for expressions is alpha equivalence. So we can't derive Eq+-- until we've made it a member of the Alpha class+deriving instance Eq Exp++type Ctx = [(Name, Ty)]++-- A monad that can generate locally fresh names+type M a = Reader Integer a++-- A type checker for STLC terms+tc :: Ctx -> Exp -> Ty -> M Bool+tc g (Var n) ty =+  case lookup n g of+    Just ty' -> return (ty == ty')+    Nothing  -> return False+tc g (Lam bnd) (Arr t1 t2) = do+  lunbind bnd $ \ (x , e) ->+    tc ((x,t1) : g) e t2+tc g (App e1 t1 e2) t2= do+  b1 <- tc g e1 (Arr t1 t2)+  b2 <- tc g e2 t1+  return $ b1 && b2+tc g EUnit TUnit = return True+tc g (Lit i) TInt = return True+tc g e t = return False+++-- beta-eta equivalence, from Karl Crary's ATTAPL chapter+-- assumes both terms type check+algeq :: Exp -> Exp -> Ty -> M Bool+algeq e1 e2 TInt  = do+  e1' <- wh e1+  e2' <- wh e2+  patheq e1' e2'+algeq e1 e2 TUnit = return True+algeq e1 e2 (Arr t1 t2) = do+  x <- lfresh name1+  algeq (App e1 t1 (Var x)) (App e2 t1 (Var x)) t2++-- path equivalence (for terms in weak-head normal form)+patheq :: Exp -> Exp -> M Bool+patheq (Var x) (Var y) | x == y = return True+patheq (Lit x) (Lit y) | x == y = return True+patheq (App e1 ty e2) (App e1' ty' e2') | ty == ty' = do+ b1 <- patheq e1 e1'+ b2 <- algeq e2 e2' ty+ return $ b1 && b2+patheq _ _ = return False++-- weak-head reduction+wh :: Exp -> M Exp+wh (App e1 ty e2) = do+   e1' <- wh e1+   case e1' of+     Lam bnd ->+       lunbind bnd $ \ (x, e1') ->+       wh (subst x e2 e1')+     _ -> return $ App e1' ty e2+wh e = return e++--- A different equivalence algorithm, based on reduce and compare.+--- (Doesn't support eta equivalences for the unit type.)++-- Parallel beta-eta reduction, prefers beta reductions to+-- eta reductions+red :: Exp -> M Exp+red (App e1 t e2) = do+  e1' <- red e1+  e2' <- red e2+  case e1' of+    Lam bnd ->+      lunbind bnd $ \ (x, e1'') ->+        return $ subst x e2' e1''+    _ -> return $ App e1' t e2'+red (Lam bnd) =+   lunbind bnd $ \ (x, e) -> do+    e' <- red e+    case e of+     -- look for an eta-reduction+     App e1 t (Var y) | y == x && x `S.notMember` fv e1 -> return e1+     otherwise -> return e+red e = return $ e++-- Reduce both sides until you find a match.+redcomp :: Exp -> Exp -> M Bool+redcomp e1 e2 = if e1 == e2 then return True                                         else do+    e1' <- red e1+    e2' <- red e2+    if e1' == e1 && e2' == e2+      then return False+      else redcomp e1' e2'++---------------------------------------------------------------------+-- TDPE ???+{-+data RExp a where+   RVar  :: Name a -> RExp a+   RLam  :: (Bind (Name b) (Exp b)) -> Exp (a -> b)+   RApp  :: RExp (a -> b) -> (RExp a) -> RExp b+   RUnit :: RExp ()++reify   :: (Fresh m, Rep a) => Exp a -> m a+reify e = case rep of+           Unit -> return ()+           (Arr a b) -> do+              e' <- reflect x --here's the rub!+              return $ \ x -> reify (RApp e e')++reflect :: (Fresh m, Rep a) => a -> m (RExp a)+reflect m = case rep of+   Unit -> return RUnit+   (Arr a b) -> do+      x <- fresh "x"+      e' <- reflect (m (reify (RVar x)))+      return $ RLam (bind x e')+-}+---------------------------------------------------------------------++assert :: String -> Bool -> IO ()+assert s True  = return ()+assert s False = print ("Assertion " ++ s ++ " failed")++assertM :: (a -> Bool) -> String -> M a -> IO ()+assertM f s c =+  if f (runReader c (0 :: Integer)) then return ()+  else print ("Assertion " ++ s ++ " failed")+++main :: IO ()+main = do+  -- \x.x == \x.y+  assert "a1" $ Lam (bind name1 (Var name1)) == Lam (bind name2 (Var name2))+  -- \x.x /= \x.y+  assert "a2" $ Lam (bind name1 (Var name2)) /= Lam (bind name1 (Var name1))+  -- [] |- \x. x : () -> ()+  assertM id "tc1" $ tc [] (Lam (bind name1 (Var name1))) (Arr TUnit TUnit)+  -- [] |- \x. x ()  : (Unit -> Int) -> Int+  assertM id "tc2" $ tc []+     (Lam (bind name1+        (App (Var name1) TUnit EUnit))) (Arr (Arr TUnit TInt) TInt)+  -- \x. x  === \x. () :: Unit -> Unit+  assertM id "be1" $+     algeq (Lam (bind name1 (Var name1)))+           (Lam (bind name2 EUnit))+           (Arr TUnit TUnit)+  -- \x. f x === f  :: Int -> Int+  assertM id "be2" $+     algeq (Lam (bind name1 (App (Var name2) TInt (Var name1))))+           (Var name2)+           (Arr TInt TInt)
+ examples/UnifyExp.hs view
@@ -0,0 +1,161 @@+{-# OPTIONS -fglasgow-exts #-}+{-# OPTIONS -fallow-undecidable-instances #-}+{-# OPTIONS -fallow-overlapping-instances #-}+{-# OPTIONS -fth #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  UnifyExp+-- Copyright   :  (c) Ben Kavanagh 2008+-- License     :  BSD+--+-- Maintainer  :  ben.kavanagh@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- A file demonstrating the use of Generics.Replib.Unify+--+-----------------------------------------------------------------------------++module UnifyExp+where++import Generics.RepLib+import Generics.RepLib.Unify+import Test.HUnit+import Control.Monad.Error++++data Exp = Var Int+	 | Plus Exp Exp+	 | K String+	 deriving (Show, Eq)+$(derive [''Exp])++instance HasVar Int Exp where+    is_var (Var i) = Just i+    is_var _ = Nothing+    var = Var++-- A = "f" ==> [(A, "f")]+test1 :: Maybe [(Int, Exp)]+test1 = solveUnification [(Var 1, K "f")]+++-- A = "f" + A  ==>   fails occurs check+test2 :: Maybe [(Int, Exp)]+test2 = solveUnification [(Var 1, Plus (K "f") (Var 1))]+++-- A + B = B + B ==> A = B+test3 :: Maybe [(Int, Exp)]+test3 = solveUnification [(Plus (Var 1) (Var 2), Plus (Var 2) (Var 2))]++-- A + B = B + C ==> [(A, C), (B, C)]+test4 :: Maybe [(Int, Exp)]+test4 = solveUnification [(Plus (Var 1) (Var 2), Plus (Var 2) (Var 3))]+++++data Term = TVar Int+	  | K2 String+	  | App Term Term+	 deriving (Show, Eq)+$(derive [''Term])++instance HasVar Int Term where+    is_var (TVar i) = Just i+    is_var _ = Nothing+    var = TVar++-- There are two ways to override the unify [Char] [Char] problem. the first is to implement+-- unify and only offer the case for K2, defaulting to generic unify in other cases. The other+-- is to implement unify for String using equality, overriding the default Cons/Nil case handling+++-- special instance of unify for String+-- Writing an instance for String which leaves 'special' term 'a' abstract has a problem with case a = String,+-- which leads to overlap with a a case.. So we can only specialise String for a known 'special' term (here Term)+instance (Eq n, Show n, HasVar n Term) => Unify n Term String where+    unifyStep _ x y = if x == y+		      then return ()+		      else throwError $ strMsg ("unify failed when testing equality for " ++ show x ++ " = " ++ show y)+++++-- f(g(A)) = f(B)  ==>   [(B, g(A))]+test5 :: Maybe [(Int, Term)]+test5 = solveUnification [(App (K2 "f") (App (K2 "g") (TVar 1)), App (K2 "f") (TVar 2))]+++-- f(g(A), A) = f(B, xyz) ==> [(A, xyz), (B, g(xyz))]+test6 :: Maybe [(Int, Term)]+test6 = solveUnification [(App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1), App (App (K2 "f") (TVar 2)) (K2 "xyz"))]++-- f(A) = f(B, C) ==> fail. constructor mismatch. App vs K2. This is in essence an 'arity' failure.+-- in a term datatype that had Application as an arity plus list, the arity would not be equal and would call failure.+-- I'm not sure the error message would be adequate. Perhaps I could use a typeclass/newtype to get better error messages+-- on equality failures.+test7 :: Maybe [(Int, Term)]+test7 = solveUnification [(App (K2 "f") (TVar 1),  App (App (K2 "f") (TVar 2)) (TVar 3))]++-- f(A) = f(B) ==> [(A, B)]+test8 :: Maybe [(Int, Term)]+test8 = solveUnification [(App (K2 "f") (TVar 1), App (K2 "f") (TVar 2))]++-- A = B, B = abc  ==>  [(B, abc), (A, abc)]+test9 :: Maybe [(Int, Term)]+test9 = solveUnification [(TVar 1, TVar 2), (TVar 2, K2 "abc")]++-- A = abc, xyz = X, A = X  ==>  fails with built in equality since we effectively ask abc = xyz+test10 :: Maybe [(Int, Term)]+test10 = solveUnification [(TVar 1, K2 "abc"), (K2 "xyz", TVar 2), (TVar 1, TVar 2)]++++-- Test that unification works with surrounding term structure (other datatypes) which are closed, i.e. they have no free variables.+data OuterTerm =  K3 String+	       | Inner Term+	       | App3 OuterTerm OuterTerm+	 deriving (Show, Eq)+$(derive [''OuterTerm])+++-- H(f(g(A), A)) = H(f(B, xyz)) ==> [(A, xyz), (B, g(xyz))]  where H is outer+test11 :: Maybe [(Int, Term)]+test11 = solveUnification'+	   (undefined :: Proxy (Int, Term))+	   [(App3 (K3 "H") (Inner $ App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1)),+	     App3 (K3 "H") (Inner $ App (App (K2 "f") (TVar 2)) (K2 "xyz")))]+++-- H(f(g(A), A)) = H(f(B, xyz)) ==> [(A, xyz), (B, g(xyz))]  where H is outer+test12 :: Maybe [(Int, Term)]+test12 = solveUnification'+	   (undefined :: Proxy (Int, Term))+	   [(App3 (K3 "H") (Inner $ App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1)),+	     App3 (K3 "I") (Inner $ App (App (K2 "f") (TVar 2)) (K2 "xyz")))]+++++-- todo. fix tests so that errors are tested properly.+tests = test [ test1 ~?= Just [(1,K "f")],+	       test2 ~?= error "***Exception: occurs check failed",+	       test3 ~?= Just [(1,Var 2)],+	       test4 ~?= Just [(1,Var 3),(2,Var 3)],+	       test5 ~?= Just [(2,App (K2 "g") (TVar 1))],+	       test6 ~?= Just [(2,App (K2 "g") (K2 "xyz")),(1,K2 "xyz")],+	       test7 ~?= error "*** Exception: constructor mismatch",+	       test8 ~?= Just [(1,TVar 2)],+	       test9 ~?= Just [(2,K2 "abc"),(1,K2 "abc")],+	       test10 ~?= error "*** Exception: unify failed in built in equality",+	       test11 ~?= Just [(2,App (K2 "g") (K2 "xyz")),(1,K2 "xyz")],+	       test12 ~?= error "*** Exception: unify failed when testing equality for \"H\" = \"I\""]+++main = runTestTT tests+
+ examples/abstract.hs view
@@ -0,0 +1,179 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,+    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving+ #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  LC+-- Copyright   :  (c) The University of Pennsylvania, 2010+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+--+--+-----------------------------------------------------------------------------++-- | This example demonstrates how to use abstract types as part of+-- the syntax of the untyped lambda calculus+--+-- Suppose we wish to include Source positions in our Abstract Syntax+--+module Abstract where++import Generics.RepLib+import Generics.RepLib.Bind.LocallyNameless+import Generics.RepLib.Bind.PermM+import qualified Data.Set as S++import Control.Monad.Reader (Reader, runReader)+++-- We import the type SourcePos, but it is an abstract data type+-- all we know about it is that it is an instance of the Eq, Show and Ord classes.+import Text.ParserCombinators.Parsec.Pos (SourcePos, newPos)++-- Since we don't know the structure of the type, we create an "abstract"+-- representation for it. This defines rSourcePos :: R SourcePos and makes+-- SourcePos an instance of the Rep and Rep1 type classes.+--+-- Right now, this line triggers a warning because the TemplateHaskell code+-- does not work well with type abbreviations. The warning is safe to ignore.+$(derive_abstract [''SourcePos])++-- | A Simple datatype for the Lambda Calculus that includes source position+-- information+data Exp = Var SourcePos (Name Exp)+         | Lam (Bind (Name Exp) Exp)+         | App Exp Exp+  deriving Show++$(derive [''Exp])++-- To make Exp an instance of Alpha, we also need SourcePos to be an+-- instance of Alpha, because it appears inside the Exp type.  When we+-- do so, we override the default definition of aeq'.  There are a+-- few reasonable choices for this:+--+-- (1) match no source positions together  --- default definition+--      aeq' c s1 s2 = False+-- (2) match all source positions together+--      aeq' c s1 s2 = True+-- (3) only match equal source positions together+--      aeq' c s1 s2 = s1 == s2 +--      +--+-- Below, we choose option (2) because we would like+-- (alpha-)equivalence for Exp to ignore the source position+-- information. Two free variables with the same name but with+-- different source positions should be equal.+--+-- The other defaults for Alpha are fine.+instance Alpha SourcePos where+   aeq' c s1 s2 = True+   acompare' c s1 s2 = EQ+   match' c s1 s2 = Just empty++instance Alpha Exp where++instance Subst Exp SourcePos where+instance Subst Exp Exp where+   isvar (Var _ x) = Just (SubstName x)+   isvar _       = Nothing++type M a = Reader Integer a++-- | Beta-Eta equivalence for lambda calculus terms.+(=~) :: Exp -> Exp -> M Bool+e1 =~ e2 | e1 `aeq` e2 = return True+e1 =~ e2 = do+    e1' <- red e1+    e2' <- red e2+    if e1' `aeq` e1 && e2' `aeq` e2+      then return False+      else e1' =~ e2'+++-- | Parallel beta-eta reduction for lambda calculus terms.+-- Do as many reductions as possible in one step, while still ensuring+-- termination.+red :: Exp -> M Exp+red (App e1 e2) = do+  e1' <- red e1+  e2' <- red e2+  case e1' of+    -- look for a beta-reduction+    Lam bnd ->+      lunbind bnd $ \ (x, e1'') ->+        return $ subst x e2' e1''+    otherwise -> return $ App e1' e2'+red (Lam bnd) = lunbind bnd $ \ (x, e) -> do+   e' <- red e+   case e of+     -- look for an eta-reduction+     App e1 (Var _ y) | y `aeq` x && x `S.notMember` fv e1 -> return e1+     otherwise -> return (Lam (bind x e'))+red v = return $ v++++---------------------------------------------------------------------+-- Some testing code to demonstrate this library in action.++assert :: String -> Bool -> IO ()+assert s True  = return ()+assert s False = print ("Assertion " ++ s ++ " failed")++assertM :: String -> M Bool -> IO ()+assertM s c =+  if (runReader c (0 :: Integer)) then return ()+  else print ("Assertion " ++ s ++ " failed")++x :: Name Exp+x = string2Name "x"++y :: Name Exp+y = string2Name "y"++z :: Name Exp+z = string2Name "z"++s :: Name Exp+s = string2Name "s"++sp = newPos "Foo" 1 2+sp2 = newPos "Bar" 3 4++lam :: Name Exp -> Exp -> Exp+lam x y = Lam (bind x y)++var :: Name Exp -> Exp+var n = Var sp n++zero  = lam s (lam z (var z))+one   = lam s (lam z (App (var s) (var z)))+two   = lam s (lam z (App (var s) (App (var s) (var z))))+three = lam s (lam z (App (var s) (App (var s) (App (var s) (var z)))))++plus = lam x (lam y (lam s (lam z (App (App (var x) (var s)) (App (App (var y) (var s)) (var z))))))++true = lam x (lam y (var x))+false = lam x (lam y (var y))+if_ x y z = (App (App x y) z)++main :: IO ()+main = do+  -- \x.x `aeq` \x.y, no matter what the source positions are+  assert "a1" $ lam x (var x) `aeq` lam y (Var sp2 y)+  -- \x.x /= \x.y+  assert "a2" $ not(lam x (var y) `aeq` lam x (var x))+  -- \x.(\y.x) (\y.y) `aeq` \y.y+  assertM "be1" $ lam x (App (lam y (var x)) (lam y (var y))) =~ (lam y (var y))+  -- \x. f x `aeq` f+  assertM "be2" $ lam x (App (var y) (var x)) =~ var y+  assertM "be3" $ if_ true (var x) (var y) =~ var x+  assertM "be4" $ if_ false (var x) (var y) =~ var y+  assertM "be5" $ App (App plus one) two =~ three+
+ examples/functor.hs view
@@ -0,0 +1,112 @@+{-# LANGUAGE TemplateHaskell, +             ScopedTypeVariables,+             FlexibleInstances,+             MultiParamTypeClasses,+             FlexibleContexts,+             UndecidableInstances, +             GADTs #-}++module Functor where++import Generics.RepLib hiding (Int)+import Generics.RepLib.Bind.LocallyNameless+import Control.Monad+import Control.Monad.Trans.Error+import Data.List as List++{- So we can't actually do modules like I was thinking of. +   Substitution in modules only "delays" capture not avoids it.+ -}++type TyName = Name Type+type ModName = Name Module ++data Type = TyVar TyName+          | Int+          | Bool+          | Path Module TyName+   deriving Show++data ModDef =  TyDef TyName (Maybe (Annot Type))+            |  ModDef ModName Module +                 -- here is the question. For submodules should +                 -- it be Annot Module or just Module?  For the +                 -- former, then the "binding" names of the submodule+                 -- could be bound by the outer module. For the latter+                 -- a submodule can't use the same name as the outer +                 -- module.+   deriving Show+data Module =  Struct  (Rec [ModDef])+            |  Functor (Bind TyName Module)+            |  ModApp Module Type+            |  ModVar (Name Module)+   deriving Show++$(derive [''Type, ''ModDef, ''Module])++------------------------------------------------------  +instance Alpha Type where   +instance Alpha Module where+instance Alpha ModDef where++instance Subst Module Type where++instance Subst Module ModDef+instance Subst Module Module where+  isvar (ModVar x) = Just (SubstName x)+  isvar _ = Nothing++instance Subst Type Module where+instance Subst Type ModDef where+instance Subst Type Type where+  isvar (TyVar x) = Just (SubstName x)+  isvar _ = Nothing++t :: TyName+t = string2Name "t"++u :: TyName+u = string2Name "u"++x :: TyName+x = string2Name "x"++g :: ModName+g = string2Name "G"++f :: Module+f = Functor (bind x  +             (Struct (rec [TyDef t (Just (Annot Bool)), +             TyDef u (Just (Annot (TyVar x)))])))++m :: Module+m = Struct (rec [TyDef t (Just (Annot Int)), +                 ModDef g (ModApp f (TyVar t))])+++red :: Fresh m => Module -> m Module +red (ModApp m1 t) = do +  m1' <- red m1+  case m1' of +    Functor bnd -> do +       (x, m1'') <- unbind bnd+       red (subst x t m1'')+    _ -> return (ModApp m1 t)+red (Struct s) = do +    defs <- mapM redDef (unrec s)+    return (Struct (rec defs))  +red m = return m++redDef :: Fresh m => ModDef -> m ModDef+redDef (ModDef f m) = do +  m' <- red m+  return (ModDef f m')+redDef d = return d++m3 = Struct (rec [TyDef t Nothing, +                  TyDef u (Just (Annot (TyVar t)))])++m2 :: Module+m2 = runFreshM (red m)+       +
+ examples/functor2.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE TemplateHaskell, +             ScopedTypeVariables,+             FlexibleInstances,+             MultiParamTypeClasses,+             FlexibleContexts,+             UndecidableInstances, +             GADTs #-}++module Functor2 where++import Generics.RepLib hiding (Int)+import Generics.RepLib.Bind.LocallyNameless+import Control.Monad+import Control.Monad.Trans.Error+import Data.List as List++{- This is the right way to formalize modules and functors+ -}++type TyName = Name Type+type ModName = Name Module ++data Type = TyVar TyName+          | Int+          | Bool+          | Path Module String+   deriving Show++data ModDef =  TyDef  TyName  (Maybe (Annot Type))+            |  ModDef ModName (Annot Module) ++   deriving Show+data Module =  Struct  (Bind (Rec [(String,ModDef)]) ())+            |  Functor (Bind TyName Module)+            |  ModApp Module Type+            |  ModVar (Name Module)+   deriving Show++$(derive [''Type, ''ModDef, ''Module])++------------------------------------------------------  +instance Alpha Type where   +instance Alpha Module where+instance Alpha ModDef where++instance Subst Module Type where++instance Subst Module ModDef+instance Subst Module Module where+  isvar (ModVar x) = Just (SubstName x)+  isvar _ = Nothing++instance Subst Type Module where+instance Subst Type ModDef where+instance Subst Type Type where+  isvar (TyVar x) = Just (SubstName x)+  isvar _ = Nothing+++t :: TyName+t = string2Name "t"++u :: TyName+u = string2Name "u"++x :: TyName+x = string2Name "x"++g :: ModName+g = string2Name "G"++f :: Module+f = Functor (bind x  +             (Struct (bind (rec +                  [("t", TyDef t (Just (Annot Bool))),+                   ("u", TyDef u (Just (Annot (TyVar x))))]) ())))++m :: Module+m = Struct (bind (rec [("t", TyDef t (Just (Annot Int))), +                       ("g", ModDef g (Annot (ModApp f (TyVar t))))]) ())+++red :: Fresh m => Module -> m Module +red (ModApp m1 t) = do +  m1' <- red m1+  case m1' of +    Functor bnd -> do +       (x, m1'') <- unbind bnd+       red (subst x t m1'')+    _ -> return (ModApp m1 t)+red (Struct s) = do +    (r,()) <- unbind s+    defs <- mapM redDef (unrec r)+    return (Struct (bind (rec defs) ()))  +red m = return m++redDef :: Fresh m => (String,ModDef) -> m (String,ModDef)+redDef (s,ModDef f (Annot m)) = do +  m' <- red m+  return (s,ModDef f (Annot m'))+redDef d = return d++m2 :: Module+m2 = runFreshM (red m)+       +
+ examples/issue15.hs view
@@ -0,0 +1,13 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,+    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving+ #-}++module Issue15 where++import Generics.RepLib+import qualified Generics.RepLib.Bind.LocallyNameless as LN++data Foo = Foo (LN.Name Foo)++$(derive [''Foo])
+ tutorial/Makefile view
@@ -0,0 +1,5 @@+# To get pandoc, use+#   cabal install -fhighlighting pandoc++Tutorial.html : Tutorial.lhs+	pandoc -f markdown+lhs -t html+lhs -s -o Tutorial.html Tutorial.lhs
+ tutorial/Tutorial.lhs view
@@ -0,0 +1,595 @@+Programming with binders using RepLib+=====================================++*Names* are the bane of every language implementation: they play an+unavoidable, central role, yet are tedious to deal with and surprisingly+tricky to get right. ++RepLib includes a flexible and powerful library for programming with+names and binders, which makes programming with binders easy and+painless.  Built on top of RepLib's generic programming framework, it+does a lot of work behind the scenes to provide you with a seamless,+"it just works" experience.++This literate Haskell tutorial will walk you through the basics of+using the library.++The untyped lambda calculus+---------------------------++Let's start by writing a simple untyped lambda calculus+interpreter. This will illustrate the basic functionality of the+binding library.++**Preliminaries**++First, we need to enable lots of wonderful GHC extensions:++> {-# LANGUAGE MultiParamTypeClasses+>            , TemplateHaskell+>            , ScopedTypeVariables+>            , FlexibleInstances+>            , FlexibleContexts+>            , UndecidableInstances+>   #-}++You may be worried by `UndecidableInstances`.  Sadly, this is+necessary in order to typecheck the code generated by RepLib. Rest+assured, however, that the instances generated by RepLib *are*+decidable; it's just that GHC can't prove it. ++Now for some imports: ++> import Generics.RepLib+> import Generics.RepLib.Bind.LocallyNameless++We import the RepLib library as well as the locally nameless+implementation of the binding library.  (RepLib also provides a nominal+version in `Generics.RepLib.Bind.Nominal`.  At the moment these are+simply two different implementations providing essentially the same+interface.  The locally nameless version is more mature, but you are+welcome to experiment with using the nominal version in its place.)++A few other imports we'll need for this particular example:++> import Control.Applicative+> import Control.Arrow ((+++))+> import Control.Monad+> import Control.Monad.Trans.Maybe+> import Control.Monad.Trans.Error+>+> import Text.Parsec hiding ((<|>), Empty)+> import qualified Text.Parsec.Token as P+> import Text.Parsec.Language (haskellDef)+>+> import qualified Text.PrettyPrint as PP+> import Text.PrettyPrint (Doc, (<+>))++**Representing terms**++We now declare a `Term` data type to represent lambda calculus terms.++> data Term = Var (Name Term)+>           | App Term Term+>           | Lam (Bind (Name Term) Term)+>   deriving Show++The `App` constructor is straightforward, but the other two+constructors are worth looking at in detail.++First, the `Var` constructor holds a `Name Term`.  `Name` is an+abstract type for representing names provided by RepLib.  `Name`s are+indexed by the sorts of things to which they can refer (or more+precisely, the sorts of things which can be substituted for them).+Here, a variable is simply a name for some `Term`, so we use the type+`Name Term`.++Lambdas are where names are *bound*, so we use the special `Bind` type+also provided by RepLib.  Something of type `Bind p b` represents a+pair consisting of a *pattern* `p` and a *body* `b`.  The pattern may+bind names which occur in `b`.  Here is where the power of generic+programming comes into play: we may use (almost) any types at all as+patterns and bodies, and RepLib will be able to handle it with very+little extra guidance from us.++In this particular case, a lambda simply binds a single name, so the+pattern is just a `Name Term`, and the body is just another `Term`.++Now we tell RepLib to automatically derive a bunch of+behind-the-scenes, boilerplate instances for `Term`:++> $(derive [''Term])++There are just a couple more things we need to do.  First, we make+`Term` an instance of `Alpha`, which provides most of the methods we+will need for working with the variables and binders within `Term`s.++> instance Alpha Term++What, no method definitions?  Nope!  In this case (and in most cases)+the default implementations, written in terms of those generic+instances we had RepLib derive for us, work just fine.  But in special+situations it's possible to override specific methods in the `Alpha`+class with our own implementations.++We only need to provide one more thing: a `Subst Term Term`+instance. In general, an instance for `Subst b a` means that we can+use the `subst` function to substitute things of type `b` for `Name`s+occurring in things of type `a`.  The only method we must implement+ourselves is `isvar`, which has the type++    isvar :: a -> Maybe (SubstName a b)++The documentation for `isvar` states "If the argument is a variable,+return its name wrapped with the 'SubstName' constructor. Return+`Nothing` for non-variable arguments."  Even the most sophisticated+generic programming library can't read our minds: we have to tell it+which values of our data type are variables (*i.e.* things that can be+substituted for).  For `Term` this is not hard:++> instance Subst Term Term where+>   isvar (Var v) = Just (SubstName v)+>   isvar _       = Nothing++That's all!++**Trying things out**++Now that we've got the necessary preliminaries set up, what can we do+with this?  First, let's define some convenient helper functions:++> lam :: String -> Term -> Term+> lam x t = Lam $ bind (string2Name x) t+>+> var :: String -> Term+> var = Var . string2Name++Notice that `string2Name` allows us to create a `Name` from a+`String`, and `bind` allows us to construct bindings.++We can test things out at the `ghci` prompt like so:++    *Main> lam "x" (lam "y" (var "x"))+    Lam (<x> Lam (<y> Var 1@0))++The `1@0` is a *de Bruijn index*, which refers to the 0th variable of+the 1st (counting outwards from 0) enclosing binding site; that is, to+`x`.  Recall that the left-hand side of a `Bind` can be an arbitrary+data structure potentially containing multiple names (a *pattern*),+like a pair or a list; hence the need for the index after the `@`.  Of+course, in this particular example we only ever bind one name at once,+so the index after the `@` will always be zero.++We can check that substitution works as we expect. Substituting for+`x` in a term where `x` does not occur free has no effect:++    *Main> subst (string2Name "x") (var "z") (lam "x" (var "x"))+    Lam (<x> Var 0@0)+    +If `x` does occur free, the substitution takes place as expected:++    *Main> subst (string2Name "x") (var "z") (lam "y" (var "x"))+    Lam (<y> Var z)++Finally, substitution is capture-avoiding:++    *Main> subst (string2Name "x") (var "y") (lam "y" (var "x"))+    Lam (<y> Var y)++It may look at first glance like `y` has been incorrectly captured, but+the fact that it has a *name* means it is free: if it had been+captured we would see `Lam (<y> Var 0@0)`.++**Evaluation**++The first thing we want to do is write an evaluator for our lambda+calculus.  Of course there are many ways to do this; for the sake of+simplicity and illustration, we will write an evaluator based on a+small-step, call-by-value operational semantics.++> -- A convenient synonym for mzero+> done :: MonadPlus m => m a+> done = mzero+>+> step :: Term -> MaybeT FreshM Term+> step (Var _) = done+> step (Lam _) = done+> step (App (Lam b) t2) = do+>   (x,t1) <- unbind b+>   return $ subst x t2 t1+> step (App t1 t2) =+>       App <$> step t1 <*> pure t2+>   <|> App <$> pure t1 <*> step t2++We define a `step` function with the type `Term -> MaybeT FreshM+Term`.  `FreshM` is a monad provided by the binding library to handle+fresh name generation.  It's fairly simple but works just fine in many+situations.  (If you need to, you can create your own custom monad,+make it an instance of the `Fresh` class, and use it in place of+`FreshM`.)  In order to signal whether a reduction step has taken+place, we add failure capability with the `MaybeT` monad transformer.+We may freely intermix `FreshM` (which also comes in a transformer+variant, `FreshMT`) with all the standard monad transformers found in+the `transformers` package.++`step` tries to reduce the given term one step if possible.  Variables+and lambdas cannot be reduced at all, so in those cases we signal that+we are done. If the input term is an application of a lambda to+another term, we must do a beta-reduction.  We first use `unbind` to+destruct the binding inside the `Lam` constructor; it automatically+chooses a fresh name for the bound variable and gives us back a pair+of the variable and body.  We then call `subst` to perform the+appropriate substitution.++Otherwise, we must have an application of something other than a+lambda.  In this case we try reducing first the left-hand and then the+right-hand term.++Finally, we define an `eval` function as the transitive closure of+`step`, and run it with `runFreshM`:++> tc :: (Monad m, Functor m) => (a -> MaybeT m a) -> (a -> m a)+> tc f a = do+>   ma' <- runMaybeT (f a)+>   case ma' of+>     Just a' -> tc f a'+>     Nothing -> return a+>+> eval :: Term -> Term+> eval x = runFreshM (tc step x)++**Parsing**++We can use [Parsec](http://hackage.haskell.org/package/parsec) to+write a tiny parser for our lambda calculus:++> lexer = P.makeTokenParser haskellDef+> parens   = P.parens lexer+> brackets = P.brackets lexer+> ident    = P.identifier lexer+> +> parseTerm = parseAtom `chainl1` (pure App)+> +> parseAtom = parens parseTerm+>         <|> var <$> ident+>         <|> lam <$> (brackets ident) <*> parseTerm+> +> runTerm :: String -> Either ParseError Term+> runTerm = (id +++ eval) . parse parseTerm ""++In fact, there's nothing particularly special about this parser with+respect to the binding library: we just get to reuse our `var` and+`lam` functions from before, with the result that strings like `"([x]+[y] x) x"` are parsed into terms with all the scoping properly+resolved.++To check that it works, let's compute 2 + 3:++    *Main> runTerm "([m][n][s][z] m s (n s z)) ([s] [z] s (s z)) ([s][z] s (s (s z))) s z"+    Right (App (Var s) (App (Var s) (App (Var s) (App (Var s) (App (Var s) (Var z))))))++2 + 3 is still 5, and all is right with the world.++**Pretty-printing and LFresh**++Now we want to write a pretty-printer for our lambda calculus (to use+in our fantastic type checking error messages, once we get around to+adding an amazing, sophisticated type system).  Here's a first attempt:++> class Pretty' p where+>   ppr' :: (Applicative m, Fresh m) => p -> m Doc+>+> instance Pretty' Term where+>   ppr' (Var x)     = return . PP.text . show $ x+>   ppr' (App t1 t2) = PP.parens <$> ((<+>) <$> ppr' t1 <*> ppr' t2)+>   ppr' (Lam b)     = do+>     (x, t) <- unbind b+>     ((PP.brackets . PP.text . show $ x) <+>) <$> ppr' t++However, there's a problem:++    *Main> runFreshM $ ppr' (lam "x" (lam "y" (lam "z" (var "y"))))+    [x] [y1] [z2] y1++Ugh, what are those numbers doing there?  The problem is that `unbind`+always generates a new globally fresh name no matter what other names+are or aren't in scope.  This is fine for evaluation, but for+pretty-printing terms that include bound names it's rather ugly.  For+nicer printing we'll need something a bit more sophisticated.++That something is the `LFresh` type class, which gives a slightly+different interface for generating *locally fresh* names (as opposed+to `Fresh` which generates globally fresh names).  A standard+`LFreshM` monad is provided (along with a corresponding transformer,+`LFreshMT`) which is an instance of `LFresh`.++    class Monad m => LFresh m where+      -- | Pick a new name that is fresh for the current (implicit) scope.+      lfresh  :: Rep a => Name a -> m (Name a)+      -- | Avoid the given names when freshening in the subcomputation.+      avoid   :: [AnyName] -> m a -> m a++Monads which are instances of `LFresh` maintain a set of names that+are to be avoided. `lfresh` generates a name which is guaranteed not+to be in the set, and `avoid` runs a subcomputation with some+additional names that should be avoided.  You probably won't need to+call these methods explicitly very often; more useful are some methods+built on top of these such as `lunbind`:++    lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> ((a, b) -> m c) -> m c++`lunbind` corresponds to `unbind` but works in an `LFresh` context.+It destructs a binding, avoiding only names curently in scope, and+runs a subcomputation while additionally avoiding the chosen name(s).++Let's rewrite our pretty-printer in terms of `LFresh`.  The only+change we need to make is to use a continuation-passing style for the+call to `lunbind` in place of the normal monadic sequencing used with+`unbind`.++> class Pretty p where+>   ppr :: (Applicative m, LFresh m) => p -> m Doc+>+> instance Pretty Term where+>   ppr (Var x)     = return . PP.text . show $ x+>   ppr (App t1 t2) = PP.parens <$> ((<+>) <$> ppr t1 <*> ppr t2)+>   ppr (Lam b)     =+>     lunbind b $ \(x,t) ->+>       ((PP.brackets . PP.text . show $ x) <+>) <$> ppr t++Let's try it:++    *Main> runLFreshM $ ppr (lam "x" (lam "y" (lam "z" (var "y"))))+    [x] [y] [z] y+  +    *Main> runLFreshM $ ppr (lam "x" (lam "y" (lam "y" (var "y"))))+    [x] [y] [y1] y1+  +Much better!++A simple dependent calculus+---------------------------++To illustrate some of the more advanced features of RepLib's binding+library, let's consider a simple dependent calculus, defined as+follows:++[XXX put ott output here or something?  How to present the calculus?]++This is about a simple as we can get while retaining dependency of+types on terms, but it is already rather interesting with regards to+binding structure.  The main point of interest is the way that+*telescopes* work: in a term such as++[XXX \[A:*, B:A -> *, x:A, t:A -> B x]. t x]++every variable bound in the telescope is in scope not only in the body+of the abstraction but also in the type annotations of later bindings+in the telescope.  For example, `x` shows up both in the type of `t`+and in the body of the abstraction.++We can imagine a way to encode this using only `Bind`, but it would be+rather ugly. [XXX explain why it would be ugly: subtrees etc., doesn't+correspond to way we have imagined the syntax, etc.]++Instead, we can define a type `Exp` of expressions like this:++> data Exp = EVar (Name Exp)+>          | EStar+>          | ELam (Bind Tele Exp)+>          | EApp Exp [Exp]+>          | EPi (Bind Tele Exp)+>   deriving Show++There's nothing remarkable about this yet; the definition of `Exp`+corresponds exactly to the grammar we gave for expressions earlier,+and refers to a data type `Tele` of telescopes.  However, we can+already see that the definition of `Tele` will have to be somewhat+interesting: `ELam` and `EPi` declare telescopes as patterns which+bind variables within the body (an `Exp`), but as we noted before,+telescopes also have their own internal binding structure.++> data Tele = Empty+>           | Cons (Rebind (Name Exp, Annot Exp) Tele)+>   deriving Show++A telescope can be empty, of course, or else it is a variable binding+like `(x:A)` followed by another telescope, in which the variable is+bound.  However, it won't do to use `Bind`: the variable is bound *not+only* in the following telescope, but *also* in the body of the+abstraction which forms the outer context.  So instead of `Bind` we+use `Rebind`. `Rebind p b` specifies that the pattern `p` is bound in+the body `b`, but is *also* made available to be bound in another+outer context.  (Of course, that outer context might itself be a+`Rebind`, in which case the same variable would be bound in yet+another outer context, and so on.)++We are not quite done: `Rebind (Name Exp, Exp) Tele` would not be+correct, since this would specify that any variables occurring in the+`Exp` are bound in the telescope (and also in the outer context), but+this is not correct.  The `Exp` is a type annotation for the name, and+any names occurring in it are actually *references* to previously+bound names, not binding sites themselves.  For this purpose the+`Annot` wrapper is provided, which specifies that the wrapped type --+which would otherwise be considered a binding pattern -- is only an+annotation whose names refer back to previous bindings.++Pop quiz: why would++    | Cons (Rebind (Name Exp) (Annot Exp, Tele))++also be incorrect?++(Answer: because then variables would be bound within their own type+annotations.)++Now for some instances: we derive generic representations for `Exp`+and `Tele`, and make them both instances of `Alpha`. We also define a+`Subst` instance so we can substitute expressions for variables in+other expressions.++> $(derive [''Exp, ''Tele])+>+> instance Alpha Exp+> instance Alpha Tele++> instance Subst Exp Exp where+>   isvar (EVar v) = Just (SubstName v)+>   isvar _        = Nothing++We also need to be able to substitute expressions for variables+occurring in telescopes.  However, since telescopes do not contain+free expression variables directly (only binding sites, which are+never the target of a substitution), the default definition of `isvar+= const Nothing` is all we need, and the generic programming framework+takes care of the rest.++> instance Subst Exp Tele++We define some convenient smart constructors as before:++> evar :: String -> Exp+> evar = EVar . string2Name+> +> elam :: [(String, Exp)] -> Exp -> Exp+> elam t b = ELam (bind (mkTele t) b)+> +> epi :: [(String, Exp)] -> Exp -> Exp+> epi t b = EPi (bind (mkTele t) b)+>+> earr :: Exp -> Exp -> Exp+> earr t1 t2 = epi [("_", t1)] t2+> +> eapp :: Exp -> Exp -> Exp+> eapp a b = EApp a [b]+> +> mkTele :: [(String, Exp)] -> Tele+> mkTele []          = Empty+> mkTele ((x,e) : t) = Cons (rebind (string2Name x, Annot e) (mkTele t))++These are fairly straightforward, and we note only the second case of+`mkTele`, where we use `rebind` for creating a `Rebind` structure, and+wrap `e` in an `Annot` constructor.++We can test things out so far by creating a few example terms.  Here+is the polymorphic identity function:++    *Main> elam [("A", EStar), ("x", evar "A")] (evar "x")+    ELam (<(Cons (<<(A,{EStar})>> Cons (<<(x,{EVar 0@0})>> Empty)))> EVar 0@1)++Inside the `ELam` we have the whole telescope inside angle brackets+(indicating the entire thing is a binding pattern), followed by the+body of the lambda, `EVar 0@1`, indicating it is a reference to the+first enclosing binding pattern (that is, the telescope), and+specifically to the second variable bound within the pattern (that is,+`x`).  Within the telescope, there is a binding for `A` with an+annotation (in curly braces) of `EStar`, followed by a binding for+`x`, with an annotation of `EVar 0@0` -- that is, `A`.++    *Main> :{+    *Main| elam [ ("A", EStar)+    *Main|      , ("B", earr (evar "A") EStar)+    *Main|      , ("x", evar "A")+    *Main|      , ("t", earr (evar "A") (eapp (evar "B") (evar "x")))+    *Main|      ]+    *Main|   (eapp (evar "t") (evar "x"))+    *Main| :}+    +    ELam (<(Cons (<<(A,{EStar})>> +            Cons (<<(B,{EPi (<(Cons (<<(_,{EVar 0@0})>> Empty))> +                          EStar)})>> +            Cons (<<(x,{EVar 1@0})>> +            Cons (<<(t,{EPi (<(Cons (<<(_,{EVar 2@0})>> Empty))> +                          EApp (EVar 2@0) [EVar 1@0])})>> +            Empty)))))> +      EApp (EVar 0@3) [EVar 0@2])++We will also need functions for appending two telescopes, and for+looking up a name in a telescope.  Both these functions illustrate the+use of `unrebind`, which opens a `Rebind` structure similarly to the+way that `unbind` opens `Bind`s.  However, it is different in one+important respect: while the output of `unbind` must be in a monad for+fresh name generation, the output of `unrebind` is pure.  This is+because `Rebind`s can only ever occur within an enclosing `Bind`, so+by the time we get around to opening a `Rebind`, fresh names have+already been chosen for the binders by a call to `unbind`, and they+need not be freshened again.++We also define a monad `M` which will serve as the context for our+type checker.++> appTele :: Tele -> Tele -> Tele+> appTele Empty     t2 = t2+> appTele (Cons rb) t2 = Cons (rebind p (appTele t1' t2))+>   where (p, t1') = unrebind rb+> +> type M = ErrorT String LFreshM+>+> lookUp :: Name Exp -> Tele -> M Exp+> lookUp n Empty     = throwError $ "Not in scope: " ++ show n+> lookUp v (Cons rb) | v == x    = return a+>                    | otherwise = lookUp v t'+>   where ((x, Annot a), t') = unrebind rb++(We also note in passing that `appTele` and `lookUp` would be perfect+opportunities to use GHC's `ViewPatterns`, but for simplicity's sake+we leave this fun to the reader.)++We can now write a type checker for our toy language.  From the point+of view of the binding library, there's nothing too remarkable about+it: we use `lunbind` to take apart binders when inferring the types of+lambdas, applications, and pis, and use substitution both when+checking the types of argument lists (`checkList`) and when+substituting the arguments to an application into the type of the+result (`multiSubst`).++> unPi :: Exp -> M (Bind Tele Exp)+> unPi (EPi bnd) = return bnd+> unPi e         = throwError $ "Expected pi type, got " ++ show e ++ " instead"+> +> infer :: Tele -> Exp -> M Exp+> infer g (EVar x)  = lookUp x g+> infer _ EStar     = return EStar+> infer g (ELam bnd) = do+>   lunbind bnd $ \(delta, m) -> do+>     b <- infer (g `appTele` delta) m+>     return . EPi $ bind delta b+> infer g (EApp m ns) = do+>   bnd <- unPi =<< infer g m+>   lunbind bnd $ \(delta, b) -> do+>     checkList g ns delta+>     multiSubst delta ns b+> infer g (EPi bnd) = do+>   lunbind bnd $ \(delta, b) -> do+>     check (g `appTele` delta) b EStar+>     return EStar+> +> check :: Tele -> Exp -> Exp -> M ()+> check g m a = do+>   b <- infer g m+>   checkEq b a+> +> checkList :: Tele -> [Exp] -> Tele -> M ()+> checkList _ [] Empty = ok+> checkList g (e:es) (Cons rb) = do+>   let ((x, Annot a), t') = unrebind rb+>   check g e a+>   checkList (subst x e g) (subst x e es) (subst x e t')+> checkList _ _ _ = throwError $ "Unequal number of parameters and arguments"+> +> multiSubst :: Tele -> [Exp] -> Exp -> M Exp+> multiSubst Empty     [] e = return e+> multiSubst (Cons rb) (e1:es) e = multiSubst t' es e'+>   where ((x,_), t') = unrebind rb+>         e' = subst x e1 e+> multiSubst _ _ _ = throwError $ "Unequal lengths in multiSubst" -- shouldn't happen+> +> -- A conservative, inexpressive notion of equality, just for the sake+> -- of the example.+> checkEq :: Exp -> Exp -> M ()+> checkEq e1 e2 = if aeq e1 e2 +>                   then return () +>                   else throwError $ "Couldn't match: " ++ show e1 ++ " " ++ show e2++XXX insert type *checking* example (checking pi-type of a lambda) as+illustration of unbind2
+ unbound.cabal view
@@ -0,0 +1,43 @@+name:           unbound+version:        0.2+license:        BSD3+license-file:   LICENSE+build-type:     Simple+cabal-version:  >= 1.6+tested-with:    GHC == 7.0.1+author:         Stephanie Weirich+maintainer:     Brent Yorgey <byorgey@cis.upenn.edu>+		Chris Casinghino <ccasin@cis.upenn.edu>+                Stephanie Weirich <sweirich@cis.upenn.edu>+homepage:       http://code.google.com/p/replib/+category:       Language, Generics, Compilers/Interpreters+extra-source-files: README, +                    examples/*.hs,+                    tutorial/Makefile,+                    tutorial/Tutorial.lhs,+                    Unbound/LocallyNameless/Test.hs+synopsis:       Generic support for programming with names and binders++description:    Specify the binding structure of your data type with an+                expressive set of type combinators, and Unbound+                handles the rest!  Automatically derives+                alpha-equivalence, free variable calculation,+                capture-avoiding substitution, and more.+Library+  build-depends: base >= 4.3 && < 5,+                 RepLib >= 0.4.0,+                 mtl >= 2.0 && < 2.1, transformers >= 0.2.2.0 && < 0.2.3,+                 containers >= 0.3 && < 0.5+  exposed-modules:+    Unbound.LocallyNameless,+    Unbound.LocallyNameless.Name,+    Unbound.LocallyNameless.Fresh,+    Unbound.LocallyNameless.Types,+    Unbound.LocallyNameless.Alpha,+    Unbound.LocallyNameless.Subst,+    Unbound.LocallyNameless.Ops,+    Unbound.Nominal,+    Unbound.Nominal.Name,+    Unbound.Nominal.Internal,+    Unbound.PermM,+    Unbound.Util