{-# LANGUAGE TemplateHaskell #-}

-- |
-- Module      : Data.Binding.Hobbits.Closed
-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
--
-- License     : BSD3
--
-- Maintainer  : emw4@rice.edu
-- Stability   : experimental
-- Portability : GHC
--
-- This module uses Template Haskell to distinguish closed terms, so that the
-- library can trust such functions to not contain any @Name@ values in their
-- closure.

module Data.Binding.Hobbits.Closed (
  -- * Abstract types
  Cl(),
  -- * Operators involving 'Cl'
  cl, clApply, unCl, mbApplyCl, mbLiftClosed, noClosedNames,
  -- * Synonyms
  mkClosed, Closed, unClosed
) where

import Data.Binding.Hobbits.Internal (Name, Mb(..), Cl(..))

import Data.Binding.Hobbits.NuElim

import Language.Haskell.TH (Q, Exp(..), Type(..))
import qualified Language.Haskell.TH as TH
import qualified Language.Haskell.TH.ExpandSyns as TH

import qualified Data.Generics as SYB
import qualified Language.Haskell.TH.Syntax as TH





-- | @cl@ is used with Template Haskell quotations to create closed terms of
-- type 'Cl'. A quoted expression is closed if all of the names occuring in it
-- are
--
--   1) bound globally or
--   2) bound within the quotation or
--   3) also of type 'Cl'.
cl :: Q Exp -> Q Exp
cl e = AppE (ConE 'Cl) `fmap` e >>= SYB.everywhereM (SYB.mkM w) where
  w e@(VarE n@(TH.Name _ flav)) = case flav of
    TH.NameG {} -> return e -- bound globally
    TH.NameU {} -> return e -- bound locally within this quotation
    TH.NameL {} -> closed n >> return e -- bound locally outside this quotation
    _ -> fail $ "`cl' does not allow dynamically bound names: `"
      ++ show n ++ "'."
  w e = return e

  closed n = do
    i <- TH.reify n
    case i of
      TH.VarI _ ty _ _ -> TH.expandSyns ty >>= w
        where
          w (AppT (ConT m) _) | m == ''Cl = return ()
          w (ForallT _ _ ty) = w ty
          w _ = fail $ "`cl` requires non-global variables to have type `Cl'.\n\t`"
            ++ show (TH.ppr n) ++ "' does not. It's type is:\n\t `"
            ++ show (TH.ppr ty) ++ "'."
      _ -> fail $ "hobbits Panic -- could not reify `" ++ show n ++ "'."





-- | Closed terms are closed (sorry) under application.
clApply :: Cl (a -> b) -> Cl a -> Cl b
-- could be defined with cl were it not for the GHC stage restriction
clApply (Cl f) (Cl a) = Cl (f a)

-- | Closed multi-bindings are also closed under application.
clMbApply :: (NuElim a, NuElim b) => Cl (Mb ctx (a -> b)) -> Cl (Mb ctx a) ->
             Cl (Mb ctx b)
clMbApply (Cl f) (Cl a) = Cl (mbApply f a)

-- | @mbLiftClosed@ is safe because closed terms don't contain names.
mbLiftClosed :: Mb ctx (Cl a) -> Cl a
mbLiftClosed (MkMb _ a) = a

-- | @noClosedNames@ encodes the hobbits guarantee that no name can escape its
-- multi-binding.
noClosedNames :: Cl (Name a) -> b
noClosedNames _ = error $ "... Clever girl!" ++
  "The `noClosedNames' invariant has somehow been violated."

-- | @mbApplyCl@ @f@ @b@ applies a closed function @f@ to the body of
-- multi-binding @b@. For example:
--
-- > mbApplyCl $(cl [| f |]) (nu $ \n -> n)   =   nu f
mbApplyCl :: Cl (a -> b) -> Mb ctx a -> Mb ctx b
mbApplyCl f (MkMb names i) = MkMb names (unCl f i)



-- | @mkClosed = cl@
mkClosed = cl

-- | @Closed = Cl@
type Closed = Cl

-- | @unClosed = unCl@
unClosed x = unCl x