content: {-# OPTIONS_HADDOCK show-extensions #-}
  -- |
  -- Module     : Unbound.Generics.LocallyNameless.Rebind
  -- Copyright  : (c) 2014, Aleksey Kliger
  -- License    : BSD3 (See LICENSE)
  -- Maintainer : Aleksey Kliger
  -- Stability  : experimental
  --
  -- The pattern @'Rebind' p1 p2@ binds the names in @p1@ and @p2@ just as @(p1, p2)@ would,
  -- however it additionally also brings the names of @p1@ into scope in @p2@.
  --
  {-# LANGUAGE DeriveGeneric #-}
  module Unbound.Generics.LocallyNameless.Rebind where
  
  import Control.Applicative ((<*>), (<$>))
  import Control.DeepSeq (NFData(..))
  import Data.Monoid ((<>), All(..))
  import GHC.Generics
  
  import Unbound.Generics.LocallyNameless.Alpha
  
  
  -- | @'Rebind' p1 p2@ is a pattern that binds the names of @p1@ and @p2@, and additionally
  -- brings the names of @p1@ into scope over @p2@.
  --
  -- This may be used, for example, to faithfully represent Scheme's @let*@ binding form, defined by:
  -- 
  -- >  (let* () body) ≙ body
  -- >  (let* ([v1, e1] binds ...) body) ≙ (let ([v1, e1]) (let* (binds ...) body))
  -- 
  -- using the following AST:
  --
  -- @
  -- type Var = Name Expr
  -- data Lets = EmptyLs
  --           | ConsLs (Rebind (Var, Embed Expr) Lets)
  -- data Expr = ...
  --           | LetStar (Bind Lets Expr)
  --           | ...
  -- @
  data Rebind p1 p2 = Rebnd p1 p2
                    deriving (Generic, Eq)
  
  instance (NFData p1, NFData p2) => NFData (Rebind p1 p2) where
    rnf (Rebnd p1 p2) = rnf p1 `seq` rnf p2 `seq` ()
  
  instance (Show p1, Show p2) => Show (Rebind p1 p2) where
    showsPrec paren (Rebnd p1 p2) =
      showParen (paren > 0) (showString "<<"
                             . showsPrec paren p1
                             . showString ">> "
                             . showsPrec 0 p2)
  
  instance (Alpha p1, Alpha p2) => Alpha (Rebind p1 p2) where
    isTerm _ = All False
  
    isPat (Rebnd p1 p2) = isPat p1 <> isPat p2
  
    swaps' ctx perm (Rebnd p1 p2) =
      Rebnd (swaps' ctx perm p1) (swaps' (incrLevelCtx ctx) perm p2)
  
    freshen' ctx (Rebnd p1 p2) =
      if isTermCtx ctx
      then error "freshen' on Rebind in Term mode"
      else do
        (p1', perm1) <- freshen' ctx p1
        (p2', perm2) <- freshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) perm1 p2)
        return (Rebnd p1' p2', perm1 <> perm2)
  
    lfreshen' ctx (Rebnd p q) cont =
      if isTermCtx ctx
      then error "lfreshen' on Rebind in Term mode"
      else
        lfreshen' ctx p $ \ p' pm1 ->
        lfreshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) pm1 q) $ \ q' pm2 ->
        cont (Rebnd p' q') (pm1 <> pm2)
  
  
    aeq' ctx (Rebnd p1 p2) (Rebnd q1 q2) =
      -- XXX TODO: Unbound had (aeq' ctx p2 q2) here.  But that doesn't seem right.
      aeq' ctx p1 q1 && aeq' (incrLevelCtx ctx) p2 q2
  
    fvAny' ctx afa (Rebnd p1 p2) = Rebnd <$> fvAny' ctx afa p1
                                         <*> fvAny' (incrLevelCtx ctx) afa p2
  
    open ctx b (Rebnd p1 p2) = Rebnd (open ctx b p1) (open (incrLevelCtx ctx) b p2)
    close ctx b (Rebnd p1 p2) = Rebnd (close ctx b p1) (close (incrLevelCtx ctx) b p2)
  
    acompare' ctx (Rebnd p1 p2) (Rebnd q1 q2) =
      acompare' ctx p1 q1 <> acompare' (incrLevelCtx ctx) p2 q2
  