{-# LANGUAGE TemplateHaskell, ViewPatterns, PolyKinds, GADTs, PatternGuards #-}

-- |
-- 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 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
  Closed(),
  -- * Operators involving 'Closed'
  unClosed, mkClosed, noClosedNames, clApply, clMbApply, clApplyCl, unsafeClose,
  -- * Typeclass for inherently closed types
  Closable(..)
) where

import Data.Proxy
import Data.Type.RList
import Data.Binding.Hobbits.Internal.Name
import Data.Binding.Hobbits.Internal.Mb
import Data.Binding.Hobbits.Internal.Closed
import Data.Binding.Hobbits.Mb

-- | @noClosedNames@ encodes the hobbits guarantee that no name can escape its
-- multi-binding.
noClosedNames :: Closed (Name a) -> b
noClosedNames :: Closed (Name a) -> b
noClosedNames (Closed Name a
n) =
  -- We compare n to itself to force evaluation, in case the body of
  -- the closed value is non-terminating...
  case Name a -> Name a -> Maybe (a :~: a)
forall k (a :: k) (b :: k). Name a -> Name b -> Maybe (a :~: b)
cmpName Name a
n Name a
n of
    Maybe (a :~: a)
_ ->
      [Char] -> b
forall a. HasCallStack => [Char] -> a
error ([Char] -> b) -> [Char] -> b
forall a b. (a -> b) -> a -> b
$
      [Char]
"... Clever girl!" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"The `noClosedNames' invariant has somehow been violated."

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

-- | Closed multi-bindings are also closed under application.
clMbApply :: Closed (Mb ctx (a -> b)) -> Closed (Mb ctx a) ->
             Closed (Mb ctx b)
clMbApply :: Closed (Mb ctx (a -> b)) -> Closed (Mb ctx a) -> Closed (Mb ctx b)
clMbApply (Closed Mb ctx (a -> b)
f) (Closed Mb ctx a
a) = Mb ctx b -> Closed (Mb ctx b)
forall a. a -> Closed a
Closed (Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
forall k (ctx :: RList k) a b.
Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
mbApply Mb ctx (a -> b)
f Mb ctx a
a)

-- | When applying a closed function, the argument can be viewed as locally
-- closed
clApplyCl :: Closed (Closed a -> b) -> Closed a -> Closed b
clApplyCl :: Closed (Closed a -> b) -> Closed a -> Closed b
clApplyCl (Closed Closed a -> b
f) Closed a
a = b -> Closed b
forall a. a -> Closed a
Closed (Closed a -> b
f Closed a
a)

-- | FIXME: this should not be possible!!
closeBug :: a -> Closed a
closeBug :: a -> Closed a
closeBug = $([| \x -> $(mkClosed [| x |]) |])

-- | Mark an object as closed without actually traversing it. This is unsafe if
-- the object does in fact contain any names.
unsafeClose :: a -> Closed a
unsafeClose :: a -> Closed a
unsafeClose = a -> Closed a
forall a. a -> Closed a
Closed

-- | Typeclass for inherently closed types
class Closable a where
  toClosed :: a -> Closed a

instance Closable Integer where
  toClosed :: Integer -> Closed Integer
toClosed Integer
i = Integer -> Closed Integer
forall a. a -> Closed a
Closed Integer
i

instance Closable (Member ctx a) where
  -- NOTE: this is actually definable with mkClosed, but this is more efficient
  toClosed :: Member ctx a -> Closed (Member ctx a)
toClosed Member ctx a
memb = Member ctx a -> Closed (Member ctx a)
forall a. a -> Closed a
Closed Member ctx a
memb

instance Closable (Proxy a) where
  toClosed :: Proxy a -> Closed (Proxy a)
toClosed Proxy a
Proxy = $(mkClosed [| Proxy |])

instance Closable (Closed a) where
  toClosed :: Closed a -> Closed (Closed a)
toClosed = Closed (Closed a -> Closed a) -> Closed a -> Closed (Closed a)
forall a b. Closed (Closed a -> b) -> Closed a -> Closed b
clApplyCl $(mkClosed [| id |])

instance Closable Bool where
  toClosed :: Bool -> Closed Bool
toClosed Bool
True = $(mkClosed [| True |])
  toClosed Bool
False = $(mkClosed [| False |])

instance Closable Char where
  toClosed :: Char -> Closed Char
toClosed = Char -> Closed Char
forall a. a -> Closed a
unsafeClose

instance Closable Int where
  toClosed :: Int -> Closed Int
toClosed = Int -> Closed Int
forall a. a -> Closed a
unsafeClose

instance Closable a => Closable [a] where
  toClosed :: [a] -> Closed [a]
toClosed [] = $(mkClosed [| [] |])
  toClosed (a
a:[a]
as) =
    $(mkClosed [| (:) |]) Closed (a -> [a] -> [a]) -> Closed a -> Closed ([a] -> [a])
forall a b. Closed (a -> b) -> Closed a -> Closed b
`clApply` a -> Closed a
forall a. Closable a => a -> Closed a
toClosed a
a Closed ([a] -> [a]) -> Closed [a] -> Closed [a]
forall a b. Closed (a -> b) -> Closed a -> Closed b
`clApply` [a] -> Closed [a]
forall a. Closable a => a -> Closed a
toClosed [a]
as

-- | Object-level reification of the 'Closable' typeclass
data IsClosable a where IsClosable :: Closable a => IsClosable a

-- | Type functors @f@ where @f a@ is always 'Closable' for any @a@
class ClosableAny1 f where
  closableAny1 :: f a -> IsClosable (f a)

-- | Helper function to use the proof returned by 'closableAny1'
toClosedAny1 :: ClosableAny1 f => f a -> Closed (f a)
toClosedAny1 :: f a -> Closed (f a)
toClosedAny1 f a
x | IsClosable (f a)
IsClosable <- f a -> IsClosable (f a)
forall k (f :: k -> *) (a :: k).
ClosableAny1 f =>
f a -> IsClosable (f a)
closableAny1 f a
x = f a -> Closed (f a)
forall a. Closable a => a -> Closed a
toClosed f a
x

instance ClosableAny1 Proxy where
  closableAny1 :: Proxy a -> IsClosable (Proxy a)
closableAny1 Proxy a
_ = IsClosable (Proxy a)
forall a. Closable a => IsClosable a
IsClosable

instance ClosableAny1 (Member ctx) where
  closableAny1 :: Member ctx a -> IsClosable (Member ctx a)
closableAny1 Member ctx a
_ = IsClosable (Member ctx a)
forall a. Closable a => IsClosable a
IsClosable

instance ClosableAny1 f => Closable (RAssign f ctx) where
  toClosed :: RAssign f ctx -> Closed (RAssign f ctx)
toClosed RAssign f ctx
MNil = $(mkClosed [| MNil |])
  toClosed (RAssign f c
xs :>: f a
x) =
    $(mkClosed [| (:>:) |]) Closed (RAssign f c -> f a -> RAssign f (c ':> a))
-> Closed (RAssign f c) -> Closed (f a -> RAssign f (c ':> a))
forall a b. Closed (a -> b) -> Closed a -> Closed b
`clApply` RAssign f c -> Closed (RAssign f c)
forall a. Closable a => a -> Closed a
toClosed RAssign f c
xs Closed (f a -> RAssign f (c ':> a))
-> Closed (f a) -> Closed (RAssign f (c ':> a))
forall a b. Closed (a -> b) -> Closed a -> Closed b
`clApply` f a -> Closed (f a)
forall k (f :: k -> *) (a :: k).
ClosableAny1 f =>
f a -> Closed (f a)
toClosedAny1 f a
x