#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)
#endif
module DCLabel.NanoEDSL (
(.\/.), (./\.)
, (<>), (><)
, singleton
, newDC
, NewPriv, newPriv, newTCBPriv
) where
import DCLabel.Core
import qualified Data.ByteString as B
import qualified Data.ByteString.Char8 as C
infixl 7 .\/.
infixl 6 ./\.
class Singleton a where
singleton :: a -> Component
instance Singleton Principal where
singleton p = MkComponent $ MkConj [ MkDisj [p] ]
instance Singleton String where
singleton s = singleton (C.pack s)
instance Singleton B.ByteString where
singleton s = MkComponent $ MkConj [ MkDisj [principal s] ]
class DisjunctionOf a b where
(.\/.) :: a -> b -> Component
instance DisjunctionOf Principal Principal where
p1 .\/. p2 = MkComponent $ MkConj [ MkDisj [p1,p2] ]
instance DisjunctionOf Principal Component where
p .\/. l = (singleton p) `or_component` l
instance DisjunctionOf Component Principal where
l .\/. p = p .\/. l
instance DisjunctionOf Component Component where
l1 .\/. l2 = l1 `or_component` l2
instance DisjunctionOf String String where
s1 .\/. s2 = singleton s1 .\/. singleton s2
instance DisjunctionOf String Component where
s .\/. l = singleton s .\/. l
instance DisjunctionOf Component String where
l .\/. p = p .\/. l
class ConjunctionOf a b where
(./\.) :: a -> b -> Component
instance ConjunctionOf Principal Principal where
p1 ./\. p2 = MkComponent $ MkConj [ MkDisj [p1], MkDisj [p2] ]
instance ConjunctionOf Principal Component where
p ./\. l = singleton p `and_component` l
instance ConjunctionOf Component Principal where
l ./\. p = p ./\. l
instance ConjunctionOf Component Component where
l1 ./\. l2 = l1 `and_component` l2
instance ConjunctionOf String String where
s1 ./\. s2 = singleton s1 ./\. singleton s2
instance ConjunctionOf String Component where
s ./\. l = singleton s `and_component` l
instance ConjunctionOf Component String where
l ./\. s = s ./\. l
instance ConjunctionOf Disj Disj where
d1 ./\. d2 = MkComponent $ MkConj [ d1, d2 ]
instance ConjunctionOf Disj Component where
d ./\. l = (MkComponent $ MkConj [d]) `and_component` l
instance ConjunctionOf Component Disj where
l ./\. d = d ./\. l
instance ConjunctionOf Principal Disj where
p ./\. d = singleton p ./\. d
instance ConjunctionOf Disj Principal where
d ./\. p = p ./\. d
instance ConjunctionOf String Disj where
p ./\. d = singleton p ./\. d
instance ConjunctionOf Disj String where
d ./\. p = p ./\. d
(<>) :: Component
(<>) = emptyComponent
(><) :: Component
(><) = allComponent
class NewDC a b where
newDC :: a -> b -> DCLabel
instance NewDC Component Component where
newDC l1 l2 = MkDCLabel l1 l2
instance NewDC Principal Component where
newDC p l = MkDCLabel (singleton p) l
instance NewDC Component Principal where
newDC l p = MkDCLabel l (singleton p)
instance NewDC Principal Principal where
newDC p1 p2 = MkDCLabel (singleton p1) (singleton p2)
instance NewDC String Component where
newDC p l = MkDCLabel (singleton p) l
instance NewDC Component String where
newDC l p = MkDCLabel l (singleton p)
instance NewDC String String where
newDC p1 p2 = MkDCLabel (singleton p1) (singleton p2)
class NewPriv a where
newPriv :: a -> Priv
newTCBPriv :: TCBPriv -> a -> Maybe TCBPriv
newTCBPriv p = delegatePriv p . newPriv
instance NewPriv Component where
newPriv = id
instance NewPriv Principal where
newPriv p = singleton p
instance NewPriv String where
newPriv p = singleton p