-- | Example secure computations involving pure values and side-effects. To see how to run the computationts defined here, please check the module "SafeExample". 
module Example where

import SecLib.Untrustworthy 
import SecLib.LatticeLH 

import Data.Maybe

low :: Sec L String
low = return "public data" 

high :: Sec H String
high = return "secret key" 

-- | Combines public and secret data. The result is secret.
comb :: Sec H String
comb = do h <- high 
          l <- up low
          return (h ++ l)

-- | Some interaction on the terminal. 
hello :: SecIO L () 
hello = do  putStrLnSecIO scr "Hello!"
            putStrLnSecIO scr "What is your name?"
            name <- getLineSecIO scr 
            putStrLnSecIO scr $ "Hi, " ++ name ++ "!"
       
  
-- | Return true if the input matches the stored password. The resulting value is secret.
high_check :: SecIO L (Sec H Bool)
high_check = do putStrLnSecIO scr "What is your password?"
                name <- getLineSecIO scr 
                return $ do key   <- high 
                            input <- return name 
                            return $ key == input 



-- | Return true if the input matches the stored password. The resulting value is public. The function waits for an escape hatch hable to compare the secret key and the input of the user and release the result. Observe the use of declassification. 
low_check :: (Sec H (String, String) -> SecIO L (Sec L Bool)) 
             -> SecIO L Bool
low_check escape = do putStrLnSecIO scr "What is your password?"
                      seci <- getLineSecIO scr

                      -- It puts in a pair the secret and the input 
                      let pair = do i <- return seci 
                                    k <- high 
                                    return (k,i)

                      -- Pass the pair to the escape hatch
                      secbool <- escape pair 
                      return $ public $ secbool