{-# LANGUAGE Unsafe #-}

-- | It provides a family of security monads for pure values.
module SecLib.TCB.Sec where

import Control.Applicative
import SecLib.Lattice


---
--- Sec Monad
---

-- | This monad denotes computations which produce values at security level @l@.
newtype Sec l a = MkSec a

instance Monad (Sec l) where
  return a = MkSec a

  MkSec a >>= k =
    MkSec (let MkSec b = k a in b)


instance Functor (Sec l) where
    -- | On purpose, @Sec l@ must not be a functor
    fmap = undefined

instance Applicative (Sec l) where
    pure  = return
    -- | @(<*>)@ cannot be used since @Sec l@ is not a functor
    (<*>) = undefined


-- | This function unlabels data (to be used only by trusted modules)
unsec :: Sec l a -> a
unsec (MkSec a) = a

---
--- Upgrading secure values
---

{- | It raises the security level of a value based on order-relationship expressed by the
security lattice.

This is the only operation which connects members of the @Sec l@ monad family.
-}
up :: Less l l' => Sec l a -> Sec l' a
up (MkSec a) = return a