{-# LANGUAGE CPP
           , RankNTypes
           , FlexibleContexts
           , GADTs
           , TypeFamilies
  #-}

----------------------------------------------------------------------
-- |
-- Module      :  Unbound.LocallyNameless.Alpha
-- License     :  BSD-like (see LICENSE)
-- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>
-- Portability :  GHC only (-XKitchenSink)
--
----------------------------------------------------------------------

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.Semigroup (Semigroup)
import qualified Data.Semigroup as Semigroup
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 almost never be called
--   directly.  Instead, use other methods provided by this module
--   which are defined in terms of @Alpha@ methods.
--
--   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
--
--   Occasionally, however, it may be useful to override the default
--   implementations of one or more @Alpha@ methods for a particular
--   type.  For example, consider a type like
--
--   > data Term = ...
--   >           | Annotation Stuff Term
--
--   where the @Annotation@ constructor of @Term@ associates some sort
--   of annotation with a term --- say, information obtained from a
--   parser about where in an input file the term came from.  This
--   information is needed to produce good error messages, but should
--   not be taken into consideration when, say, comparing two @Term@s
--   for alpha-equivalence.  In order to make 'aeq' ignore
--   annotations, you can override the implementation of @aeq'@ like
--   so:
--
--   > instance Alpha Term where
--   >   aeq' c (Annotation _ t1) t2 = aeq' c t1 t2
--   >   aeq' c t1 (Annotation _ t2) = aeq' c t1 t2
--   >   aeq' c t1 t2 = aeqR1 rep1 t1 t2
--
--   Note how the call to 'aeqR1' handles all the other cases generically.
--
--   If you use "Abstract" types (i.e. those with representations derived via
--   derive_abstract) then you must provide a definition of aeq' and
--   acompare'.  In these cases, Unbound has no information about the
--   structure of the type and cannot do anything sensible.

--      swaps'    -- identity function
--      fv'       -- const mempty
--      freshen'  -- identity function
--      lfreshen' -- identity function
--      open/close -- treat like constants

class (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 'acompare'.
  acompare' :: AlphaCtx -> a -> a -> Ordering
  acompare' = acompareR1 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

  -- | @isPat x@ dynamically checks whether @x@ can be used as a valid
  --   pattern.  The default instance returns @Just@ if at all
  --   possible.  If successful, returns a list of names bound by the
  --   pattern.
  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

-- | Type class for embedded terms (either @Embed@ or @Shift@).
class IsEmbed e where
  type Embedded e :: *

  -- | Construct an embedded term, which is an instance of 'Embed'
  --   with any number of enclosing 'Shift's.  That is, @embed@ can have
  --   any of the types
  --
  -- * @t -> Embed t@
  --
  -- * @t -> Shift (Embed t)@
  --
  -- * @t -> Shift (Shift (Embed t))@
  --
  -- and so on.
  embed   :: Embedded e -> e

  -- | Destruct an embedded term.  @unembed@ can have any of the types
  --
  -- * @Embed t -> t@
  --
  -- * @Shift (Embed t) -> t@
  --
  -- and so on.
  unembed :: e -> Embedded e

------------------------------------------------------------
--  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)


instance Semigroup FindResult where
  NamesSeen i <> NamesSeen j = NamesSeen (i + j)
  NamesSeen i <> Index j     = Index (i + j)
  Index j     <> _           = Index j

-- | @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
#if !MIN_VERSION_base(4,11,0)
  mappend = (Semigroup.<>)
#endif

-- | 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 }


instance Semigroup NthCont where
  (NthCont f) <> (NthCont g)
    = NthCont $ \i -> case f i of
        Found n     -> Found n
        CurIndex i' -> g i'

-- | @NthCont@ forms a monoid: function composition which
--   short-circuits once a result is found.
instance Monoid NthCont where
  mempty = NthCont $ \i -> CurIndex i
#if !MIN_VERSION_base(4,11,0)  
  mappend = (Semigroup.<>)
#endif

-- | 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")
                 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 }

-- | Toplevel alpha-contexts
initial :: AlphaCtx
initial = AC Term 0

-- | Call when going under a binder
incr :: AlphaCtx -> AlphaCtx
incr c = c { level = level c + 1 }

-- | Call when going in an embedding
decr :: AlphaCtx -> AlphaCtx
decr c = -- if level c == 0 then error "Too many outers"
         -- else
         c { level = level c - 1 }

-- | Call when entering a pattern
pat  :: AlphaCtx -> AlphaCtx
pat c  = c { mode = Pat }

-- | Call when entering a term embedded in a pattern
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       :: forall f. Collection f => AlphaCtx -> a -> f AnyName,
  freshenD  :: forall m. Fresh m => AlphaCtx -> a -> m (a, Perm AnyName),
  lfreshenD :: forall m b. LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b,
  aeqD      :: AlphaCtx -> a -> a -> Bool,
  acompareD :: AlphaCtx -> a -> a -> Ordering,
  closeD    :: forall b. Alpha b => AlphaCtx -> b -> a -> a,
  openD     :: forall b. Alpha b => AlphaCtx -> b -> a -> a,
  findpatD  :: a -> AnyName -> FindResult,
  nthpatD   :: a -> NthCont
  }

instance Alpha a => Sat (AlphaD a) where
  dict = AlphaD isPat isTerm isEmbed swaps' fv' freshen' lfreshen' aeq' -- match'
          acompare' close open findpatrec nthpatrec 

----------------------------------------------------------------------
-- Generic definitions for 'Alpha' methods.  (Note that all functions
-- that take representations end in 'R1'.)
----------------------------------------------------------------------

-- | Generic version of close
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

-- | Generic version of open
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

-- | Generic version of swaps
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

-- | Generic version of fv
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 where
          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
fvR1 _ = \ _ _ -> emptyC


{-
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)
-}

-- | Generic version of aeq
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 (Abstract1 _) = \ _ x y -> error "Must override aeq' for abstract types"
aeqR1 _        = \ _ _ _ -> False

-- | Generic list version of aeq
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

-- | Generic version of freshen
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)

-- | Generic list version of freshen
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 _ = \ _ _ -> mempty

findpatL :: MTup AlphaD l -> l -> AnyName -> FindResult
findpatL MNil Nil _              = 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 _ = \ _ -> 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 _ = \ _ -> 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 _ = \ _ -> 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  _ = \x y -> compare x y
acompareR1 Char1 _ = \x y -> compare x y
acompareR1 (Data1 _ 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 _ , Nothing) -> LT
                        (Nothing, Just _ ) -> GT
                        (Nothing, Nothing) -> loop rest
                 loop [] = error "acompareR1 found no constructors! Please report this as a bug."
             in loop cons
acompareR1 r1 _ = error ("acompare' not supported for " ++ show r1)

compareTupM :: MTup AlphaD l -> AlphaCtx -> l -> l -> Ordering
compareTupM MNil _ Nil Nil = EQ
compareTupM (x :+: xs) c (y :*: ys) (z :*: zs) =
   mappend (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' _ _ x = x

  aeq' c x y   | mode c == Term = x == y

  aeq' _ _ _   = 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' _ _ = 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 _) | mode c == Term && level c >= 0 =
      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 = mconcat [compare r1 r2, compare n1 n2]

  acompare' c (Bn r1 m1 n1) (Bn r2 m2 n2)
    | mode c == Term = mconcat [compare r1 r2, compare m1 m2, compare n1 n2]

  acompare' c (Nm _ _)   (Bn _ _ _) | mode c == Term = LT
  acompare' c (Bn _ _ _) (Nm _ _)   | mode c == Term = GT

  acompare' _ _          _                           = 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' _ _ _                  = 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"
       neq -> neq
  acompare' _ _ _           = 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 _)) =
    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 (Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card 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) =
      mappend (acompare' (pat c) p1 p2) (acompare' (incr c) t1 t2)

    findpatrec _ b = error $ "Binding used as a pattern"
    nthpatrec    b = error $ "Binding 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) =
      mappend (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 embeds as constants
instance Alpha t => Alpha (Embed t) where
   isPat (Embed t)   = if (isTerm t) then Just [] else Nothing
   isTerm _          = False
   isEmbed (Embed t) = isTerm t

   swaps' c pm (Embed t) =
     case mode c of
       Pat  -> Embed (swaps' (term c) pm t)
       Term -> Embed t

   fv' c (Embed t) =
     case mode c of
       Pat  -> fv' (term c) t
       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) = case mode c of
     Pat  -> Embed (close (term c) b x)
     Term -> error "close on Embed"

   open c b (Embed x) = case mode c of
     Pat  -> Embed (open (term c) b x)
     Term -> error "open on Embed"

   findpatrec _ _ = mempty
   nthpatrec _    = mempty

instance IsEmbed (Embed t) where
  type Embedded (Embed t) = t

  embed             = Embed
  unembed (Embed t) = t

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 _          = 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)

instance IsEmbed e => IsEmbed (Shift e) where
  type Embedded (Shift e) = Embedded e

  embed             = Shift . embed
  unembed (Shift e) = unembed e

-- 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)