module Data.Binding.Hobbits.Closed (
Cl(),
cl, clApply, unCl, mbApplyCl, mbLiftClosed, noClosedNames,
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 :: 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 :: (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 :: Mb ctx (Cl a) -> Cl a
mbLiftClosed (MkMb _ a) = a
noClosedNames :: Cl (Name a) -> b
noClosedNames _ = error $ "... Clever girl!" ++
"The `noClosedNames' invariant has somehow been violated."
mbApplyCl :: Cl (a -> b) -> Mb ctx a -> Mb ctx b
mbApplyCl f (MkMb names i) = MkMb names (unCl f i)
mkClosed = cl
type Closed = Cl
unClosed x = unCl x