content: {-# OPTIONS_HADDOCK show-extensions #-}
  -- |
  -- Module     : Unbound.Generics.LocallyNameless.Bind
  -- Copyright  : (c) 2014, Aleksey Kliger
  -- License    : BSD3 (See LICENSE)
  -- Maintainer : Aleksey Kliger
  -- Stability  : experimental
  --
  -- The fundamental binding form.  The type @'Bind' p t@ allows you to
  -- place a pattern @p@ in a term @t@ such that the names in the
  -- pattern scope over the term.  Use 'Unbound.Generics.LocallyNameless.Operations.bind'
  -- and 'Unbound.Generics.LocallyNameless.Operations.unbind' and 'Unbound.Generics.LocallyNameless.Operations.lunbind'
  -- to work with @'Bind' p t@
  {-# LANGUAGE DeriveGeneric #-}
  module Unbound.Generics.LocallyNameless.Bind (
    -- * Name binding
    Bind(..)
    ) where
  
  import Control.Applicative (Applicative(..), (<$>))
  import Control.DeepSeq (NFData(..))
  import Data.Monoid ((<>), All(..))
  
  import GHC.Generics (Generic)
  
  import Unbound.Generics.LocallyNameless.Alpha
  
  -- | A term of type @'Bind' p t@ is a term that binds the free
  -- variable occurrences of the variables in pattern @p@ in the term
  -- @t@.  In the overall term, those variables are now bound. See also
  -- 'Unbound.Generics.LocallyNameless.Operations.bind' and
  -- 'Unbound.Generics.LocallyNameless.Operations.unbind' and
  -- 'Unbound.Generics.LocallyNameless.Operations.lunbind'
  data Bind p t = B p t
                deriving (Generic)
  
  instance (NFData p, NFData t) => NFData (Bind p t) where
    rnf (B p t) = rnf p `seq` rnf t `seq` ()
  
  instance (Show p, Show t) => Show (Bind p t) where
    showsPrec prec (B p t) =
      showParen (prec > 0) (showString "<"
                            . showsPrec prec p
                            . showString "> "
                            . showsPrec 0 t)
  
  instance (Alpha p, Alpha t) => Alpha (Bind p t) where
  
    aeq' ctx (B p1 t1) (B p2 t2) =
      aeq' (patternCtx ctx) p1 p2
      && aeq' (incrLevelCtx ctx) t1 t2
  
    fvAny' ctx nfn (B p t) = B <$> fvAny' (patternCtx ctx) nfn p
                               <*> fvAny' (incrLevelCtx ctx) nfn t
  
    isPat _ = inconsistentDisjointSet
  
    isTerm (B p t) = (All $ isConsistentDisjointSet $ isPat p) <> isTerm t
  
    close ctx b (B p t) =
      B (close (patternCtx ctx) b p) (close (incrLevelCtx ctx) b t)
  
    open ctx b (B p t) =
      B (open (patternCtx ctx) b p) (open (incrLevelCtx ctx) b t)
  
    nthPatFind b = error $ "Binding " ++ show b ++ " used as a pattern"
    namePatFind b = error $ "Binding " ++ show b ++ " used as a pattern"
  
    swaps' ctx perm (B p t) =
      B (swaps' (patternCtx ctx) perm p)
        (swaps' (incrLevelCtx ctx) perm t)
  
    freshen' ctx (B p t) = do
      (p', perm1) <- freshen' (patternCtx ctx) p
      (t', perm2) <- freshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) perm1 t)
      return (B p' t', perm1 <> perm2)
    {-# INLINE freshen' #-}
  
    lfreshen' ctx (B p t) cont =
      lfreshen' (patternCtx ctx) p $ \p' pm1 ->
      lfreshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) pm1 t) $ \t' pm2 ->
      cont (B p' t') (pm1 <> pm2)
  
    acompare' ctx (B p1 t1) (B p2 t2) =
      acompare' (patternCtx ctx) p1 p2 <> acompare' (incrLevelCtx ctx) t1 t2
  