{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
module DCLabel.NanoEDSL ( -- * Operators
			  (.\/.), (./\.)
                        , (<>), (><)
                          -- * DCLabel creation
                        , newDC
                          -- * Privilege object creation
                        , newPriv, newTCBPriv
                        ) where

import DCLabel.Core

infixl 7 .\/.
infixl 6 ./\.

-- | Class used to create single-principal labels.
class Singleton a where 
      singleton :: a -> Label -- ^ Creates a singleton label.

instance Singleton Principal where 
      singleton p = MkLabel $ MkConj [ MkDisj [p] ]

instance Singleton String where 
      singleton s = MkLabel $ MkConj [ MkDisj [principal s] ]


-- | Class used to create disjunctions
class DisjunctionOf a b where
  (.\/.) :: a -> b -> Label

instance DisjunctionOf Principal Principal where
 p1 .\/. p2 = MkLabel $ MkConj [ MkDisj [p1,p2] ]

instance DisjunctionOf Principal Label where
 p .\/. l = (singleton p) `or_label` l 

instance DisjunctionOf Label Principal where
 l .\/. p = p .\/. l

instance DisjunctionOf Label Label where
 l1 .\/. l2 = l1 `or_label` l2

instance DisjunctionOf String String where
 s1 .\/. s2 = singleton s1 .\/. singleton s2

instance DisjunctionOf String Label where
  s .\/. l = singleton s .\/. l 

instance DisjunctionOf Label String where
  l .\/. p = p .\/. l  


-- | Class used to create conjunctions
class ConjunctionOf a b where
   (./\.) :: a -> b -> Label 

instance ConjunctionOf Principal Principal where
   p1 ./\. p2 = MkLabel $ MkConj [ MkDisj [p1], MkDisj [p2] ] 

instance ConjunctionOf Principal Label where
   p ./\. l = singleton p `and_label` l 

instance ConjunctionOf Label Principal where
   l ./\. p = p ./\. l 

instance ConjunctionOf Label Label where
   l1 ./\. l2 = l1 `and_label` l2 

-- | Instances usng strings and not principals
instance ConjunctionOf String String where
   s1 ./\. s2 = singleton s1 ./\. singleton s2 

instance ConjunctionOf String Label where
   s ./\. l = singleton s `and_label` l 

instance ConjunctionOf Label String where
   l ./\. s = s ./\. l 


-- | Empty label.
(<>) :: Label
(<>) = emptyLabel

-- | All label.
(><) :: Label
(><) = allLabel

---
--- Creating 'DCLabel's
---

-- | Class used to create 'DCLabel's.
class NewDC a b where
  newDC :: a -> b -> DCLabel -- ^ Given two elements create label.

instance NewDC Label Label where
  newDC l1 l2 = MkDCLabel l1 l2 

instance NewDC Principal Label where
  newDC p l = MkDCLabel (singleton p) l 

instance NewDC Label 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 Label where
  newDC p l = MkDCLabel (singleton p) l 

instance NewDC Label String where
  newDC l p = MkDCLabel l (singleton p) 

instance NewDC String String where
  newDC p1 p2 = MkDCLabel (singleton p1) (singleton p2) 

--
-- Creating 'Priv's and 'TCBPriv's.
--

-- | Class used to create 'Priv's and 'TCBPriv's.
class NewPriv a where
  -- ^ Given element create privilege.
  newPriv :: a -> Priv 
  -- ^ Given element create (maybe) trusted privileged object.
  newTCBPriv :: TCBPriv -> a -> Maybe TCBPriv
  newTCBPriv p = delegatePriv p . newPriv

instance NewPriv Label where
  newPriv = id

instance NewPriv Principal where
  newPriv p = singleton p

instance NewPriv String where
  newPriv p = singleton p