{-# LANGUAGE TemplateHaskell, ViewPatterns #-}

-- |
-- Module      : Data.Binding.Hobbits.Closed
-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
--
-- License     : BSD3
--
-- Maintainer  : emw4@rice.edu
-- Stability   : experimental
-- Portability : GHC
--
-- This module defines the type @'Cl' a@ of closed objects of type
-- @a@. Note that, in order to ensure adequacy of the Hobbits
-- name-binding approach, this representation is hidden from the user,
-- and so this file should never be imported directly by the user.
--

module Data.Binding.Hobbits.Internal.Closed where

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

{-| The type @Closed a@ represents a closed term of type @a@, i.e., an expression
of type @a@ with no free (Haskell) variables.  Since this cannot be checked
directly in the Haskell type system, the @Closed@ data type is hidden, and the
user can only create closed terms using Template Haskell, through the 'mkClosed'
operator. -}
newtype Closed a =
  Closed {
  -- | Extract the value of a 'Closed' object
  Closed a -> a
unClosed :: a
  }

-- | Extract the type of an 'Info' object
reifyNameType :: TH.Name -> Q Type
reifyNameType :: Name -> Q Type
reifyNameType Name
n =
  Name -> Q Info
TH.reify Name
n Q Info -> (Info -> Q Type) -> Q Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Info
i ->
  case Info
i of
    TH.VarI Name
_ Type
ty Maybe Dec
_ -> Type -> Q Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
    Info
_ -> String -> Q Type
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q Type) -> String -> Q Type
forall a b. (a -> b) -> a -> b
$ String
"hobbits Panic -- could not reify `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'."

-- | @mkClosed@ is used with Template Haskell quotations to create closed terms
-- of type 'Closed'. A quoted expression is closed if all of the names occuring in
-- it are either:
--
--   1) bound globally or
--   2) bound within the quotation or
--   3) also of type 'Closed'.
mkClosed :: Q Exp -> Q Exp
mkClosed :: Q Exp -> Q Exp
mkClosed Q Exp
e = Exp -> Exp -> Exp
AppE (Name -> Exp
ConE 'Closed) (Exp -> Exp) -> Q Exp -> Q Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Q Exp
e Q Exp -> (Exp -> Q Exp) -> Q Exp
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GenericM Q -> GenericM Q
forall (m :: * -> *). Monad m => GenericM m -> GenericM m
SYB.everywhereM ((Exp -> Q Exp) -> a -> Q a
forall (m :: * -> *) a b.
(Monad m, Typeable a, Typeable b) =>
(b -> m b) -> a -> m a
SYB.mkM Exp -> Q Exp
w) where
  w :: Exp -> Q Exp
w e :: Exp
e@(VarE n :: Name
n@(TH.Name OccName
_ NameFlavour
flav)) = case NameFlavour
flav of
    TH.NameG {} -> Exp -> Q Exp
forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e -- bound globally
    TH.NameU {} -> Exp -> Q Exp
forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e -- bound locally within this quotation
    TH.NameL {} -> Name -> Q ()
closed Name
n Q () -> Q Exp -> Q Exp
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Exp -> Q Exp
forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e -- bound locally outside this quotation
    NameFlavour
_ -> String -> Q Exp
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q Exp) -> String -> Q Exp
forall a b. (a -> b) -> a -> b
$ String
"`mkClosed' does not allow dynamically bound names: `"
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'."
  w Exp
e = Exp -> Q Exp
forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e

  closed :: Name -> Q ()
closed Name
n = do
    Type
ty <- Name -> Q Type
reifyNameType Name
n
    Type -> Q Type
TH.expandSyns Type
ty Q Type -> (Type -> Q ()) -> Q ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Type -> Q ()
forall (m :: * -> *) a. (MonadFail m, Ppr a) => a -> Type -> m ()
w Type
ty
      where
        w :: a -> Type -> m ()
w a
_ (AppT (ConT Name
m) Type
_) | Name
m Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Closed = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        w a
top_ty (ForallT [TyVarBndr]
_ Cxt
_ Type
ty') = a -> Type -> m ()
w a
top_ty Type
ty'
        w a
top_ty Type
_ =
          String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"`mkClosed` requires non-global variables to have type `Closed'.\n\t`"
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. Ppr a => a -> Doc
TH.ppr Name
n) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' does not. It's type is:\n\t `"
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (a -> Doc
forall a. Ppr a => a -> Doc
TH.ppr a
top_ty) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'."