module Data.Binding.Hobbits.Closed (
Cl(),
cl, clApply, unCl, noClosedNames,
mkClosed, Closed, unClosed
) where
import Data.Binding.Hobbits.Internal.Name
import Data.Binding.Hobbits.Internal.Mb
import Data.Binding.Hobbits.Internal.Closed
import Data.Binding.Hobbits.Mb
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 :: 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
TH.NameU {} -> return e
TH.NameL {} -> closed n >> return e
_ -> 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 ++ "'."
clApply :: Cl (a -> b) -> Cl a -> Cl b
clApply (Cl f) (Cl a) = Cl (f a)
clMbApply :: Cl (Mb ctx (a -> b)) -> Cl (Mb ctx a) ->
Cl (Mb ctx b)
clMbApply (Cl f) (Cl a) = Cl (mbApply f a)
noClosedNames :: Cl (Name a) -> b
noClosedNames (Cl n) =
case cmpName n n of
_ ->
error $
"... Clever girl!" ++
"The `noClosedNames' invariant has somehow been violated."
mkClosed = cl
type Closed = Cl
unClosed x = unCl x