{-# LANGUAGE TemplateHaskell
           , ScopedTypeVariables
           , FlexibleInstances
           , FlexibleContexts
           , MultiParamTypeClasses
           , EmptyDataDecls
  #-}

----------------------------------------------------------------------
-- |
-- Module      :  Unbound.LocallyNameless.Types
-- License     :  BSD-like (see LICENSE)
--
-- Maintainer  :  Brent Yorgey <byorgey@cis.upenn.edu>
-- Stability   :  experimental
-- Portability :  GHC only
--
-- Special type combinators for specifying binding structure.
----------------------------------------------------------------------

module Unbound.LocallyNameless.Types
       ( GenBind(..), Bind, SetBind, SetPlusBind
       , Rebind(..)
       , Rec(..)
       , TRec(..)
       , Embed(..)
       , Shift(..)
       , module Unbound.LocallyNameless.Name

       -- * Pay no attention to the man behind the curtain

       -- | These type representation objects are exported so they can be
       --   referenced by auto-generated code.  Please pretend they do not
       --   exist.

       , rGenBind, rRebind, rEmbed, rRec, rShift
       ) where

import Generics.RepLib
import Unbound.LocallyNameless.Name

import Data.Binary
import Control.Applicative (pure, (<$>), (<*>))

------------------------------------------------------------
-- Basic types
------------------------------------------------------------
-- Note: can't use DataKinds here because RepLib does not support
-- representations of them.

-- | Type level flag for binder that allows permutation
data RelaxedOrder
-- | Type level flag for binder that does not allow permutation
data StrictOrder

-- | Type level flag for binder that allows extra unused variables
data RelaxedCard
-- | Type level flag for binder that does not allow weakening
data StrictCard

--------------------------------------------------  
-- Bind
--------------------------------------------------

-- | Generic binding combinator for a pattern @p@ within a term @t@.
-- Flexible over the order and cardinality of the variables bound
-- in the pattern
data GenBind order card p t = B p t

  
-- | The most fundamental combinator for expressing binding structure
--   is 'Bind'.  The /term type/ @Bind p t@ represents a pattern @p@
--   paired with a term @t@, where names in @p@ are bound within @t@.
--
--   Like 'Name', 'Bind' is also abstract. You can create bindings
--   using 'bind' and take them apart with 'unbind' and friends.
type Bind p t        = GenBind StrictOrder StrictCard p t



-- | A variant of 'Bind' where alpha-equivalence allows multiple
-- variables bound in the same pattern to be reordered
type SetBind p t     = GenBind RelaxedOrder StrictCard p t
-- | A variant of 'Bind' where alpha-equivalence allows multiple
-- variables bound in the same pattern to be reordered, and
-- allows the binding of unused variables
-- For example,  \{ a b c } . a b `aeq` \ { b a } . a b
type SetPlusBind p t = GenBind RelaxedOrder RelaxedCard p t

instance (Show a, Show b) => Show (GenBind order card a b) where
  showsPrec p (B a b) = showParen (p>0)
      (showString "bind " . showsPrec 11 a . showsPrec 11 b)

--------------------------------------------------
-- Rebind
--------------------------------------------------

-- | @Rebind@ allows for /nested/ bindings.  If @p1@ and @p2@ are
--   pattern types, then @Rebind p1 p2@ is also a pattern type,
--   similar to the pattern type @(p1,p2)@ except that @p1@
--   /scopes over/ @p2@.  That is, names within terms embedded in @p2@
--   may refer to binders in @p1@.
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 "rebind " . showsPrec 11 a . showsPrec 11 b)

-- Rec
--------------------------------------------------

-- | If @p@ is a pattern type, then @Rec p@ is also a pattern type,
-- which is /recursive/ in the sense that @p@ may bind names in terms
-- embedded within itself.  Useful for encoding e.g. 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': the only difference is
--   that whereas @'Rec' p@ is a pattern type, @TRec p@
--   is a /term type/.  It is isomorphic to @'Bind' ('Rec' p) ()@.
--
--   Note that @TRec@ corresponds to Pottier's /abstraction/ construct
--   from alpha-Caml.  In this context, @'Embed' t@ corresponds to
--   alpha-Caml's @inner t@, and @'Shift' ('Embed' t)@ corresponds to
--   alpha-Caml's @outer t@.
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
--------------------------------------------------

-- | @Embed@ allows for terms to be /embedded/ within patterns.  Such
--   embedded terms do not bind names along with the rest of the
--   pattern.  For examples, see the tutorial or examples directories.
--
--   If @t@ is a /term type/, then @Embed t@ is a /pattern type/.
--
--   @Embed@ is not abstract since it involves no binding, and hence
--   it is safe to manipulate directly.  To create and destruct
--   @Embed@ terms, you may use the @Embed@ constructor directly.
--   (You may also use the functions 'embed' and 'unembed', which
--   additionally can construct or destruct any number of enclosing
--   'Shift's at the same time.)
newtype Embed t = Embed t deriving Eq

instance Show a => Show (Embed a) where
  showsPrec _ (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 _ (Shift a) = showString "{" . showsPrec 0 a . showString "}"

-- Pay no attention...

$(derive [''GenBind, ''Embed, ''Rebind, ''Rec, ''Shift])

$(derive [''RelaxedOrder, ''StrictOrder, ''RelaxedCard, ''StrictCard])


-- Data.Binary instances for Name and Bind
----------------------------------------------------

instance Rep a => Binary (Name a) where
  put (Nm _ (s,i)) = do put (0 :: Word8)
                        put s
                        put i
  put (Bn _ i j)   = do put (1 :: Word8)
                        put i
                        put j
  
  get = do tag <- getWord8
           case tag of
              0 -> Nm <$> pure rep <*> get
              1 -> Bn <$> pure rep <*> get <*> get

instance (Binary p, Binary t) => Binary (GenBind order card p t) where
  put (B p t) = do put p ; put t
  get = B <$> get <*> get

instance (Binary p1, Binary p2) => Binary (Rebind p1 p2) where
  put (R p1 p2) = do put p1 ; put p2
  get = R <$> get <*> get
  
instance (Binary p) => Binary (Embed p) where
  put (Embed p) = put p
  get = Embed <$> get