{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

{-
  Handle-based IO with the statically assured open/close protocol:
  -- one may perform i/o only when the handle is opened
  -- once the handle is closed, it stays closed
  -- one cannot close the handle more than once
  -- at the end of the program, all handles are closed.

There is no requirement that the opening/closing of handles must be
properly nested. That is, it is not necessary to close handles in the
inverse order they have been opened. As shown in the last example
(suggested by Ken), we open one file (e.g., the configuration file) to
read the name of the main file, close the configuration file and
continue working with the second file. There are no limitation as to
how many handles may be opened or kept open concurrently.

This is the simplified version of the code in multi-handle-io.hs,
without regions. Everything is static, which means we can't form
recursive computations.


Alas, although this approach can work out in the absence of
exceptions, it crumbles when any exceptions arise, and the latter is
inevitable.  See the comments in multi-handle-io.hs for details.

But see SafeHandles.hs for a hybrid solution, which is still better
than System.IO.

Joint work with Chung-chieh Shan.

-}

module MultiHandle0 where

import System.IO
import Control.Monad (liftM2)
import Control.Exception (try, throwIO)

-- ======================================================================
-- Security kernel below


-- ----------------------------------------------------------------------
-- safe handle and the TSIO monad

-- The TSIO monad is a (ST s)-like monad with a state whose type
-- may vary from action to action (see class Monadish below). 
-- The state can informally be described as
--
-- kind State = (Counter, ActiveLabels)
-- kind Counter = Peano numeral for producing handle labels
-- kind ActiveLabels = [Label]  -- labels of the open handles
-- kind Label = Peano numeral
--
-- Since we don't have kind declarations in Haskell, we have to emulate
-- above using Peano numerals and heterogeneous lists built with the type
-- constant N and the binary type constructor C h t. This reminds one
-- of emulating data structures in Scheme/Lisp using only cons, car, cdr, nil
-- and pair?.

-- Handles can be opened and closed at will, in any order. 
-- A created handle is labeled with the new label, which is inserted in 
-- the active label list. The tshClose operation removes the label 
-- from the list.

-- TSIO is operationally indistinguishable from IO. All of its state
-- is phantom.
newtype TSIO s si so a = TSIO {unTSIO :: IO a}
tsio_in  :: TSIO s si so a -> si; tsio_in  = undefined
tsio_out :: TSIO s si so a -> so; tsio_out = undefined
tsio_s   :: TSIO s si so a -> s;  tsio_s   = undefined
tsio :: (StateOK si, StateOK so) => IO a -> s -> si -> so -> TSIO s si so a
tsio m _ _ _ = TSIO m

instance Monadish (TSIO s) where
  gret      = TSIO . return
  gbind m f = TSIO (unTSIO m >>= unTSIO . f)

instance Monad (TSIO s p p) where
  return = gret
  (>>=)  = gbind


-- lift into the TSIO monad
glift :: IO v -> TSIO s si si v
glift = TSIO


-- A handle is labeled by the eigenvariable and by the label.
-- The eigenvariable is opaque and merely prevents the escape of the handle.
-- The label lets us tell if the handle is active. It is far easier
-- to manipulate Peano numerals than eigenvariables (there is no
-- equality predicate on eigenvariables)
newtype TSHandle s l = TSHandle Handle
shandle :: Handle -> s -> l -> TSHandle s l
shandle h _ _ = TSHandle h
shandle_l :: TSHandle s l -> (s,l); shandle_l = undefined

-- Well-formedness predicate for the state, or, the description of
-- the kind state. Not exported.
-- It is used only internally, to add `static kinding' to the type-level
-- programs below
class StateOK s
-- Add: in any list of active labels, all labels are unique.
instance Nat0 counter => StateOK (counter, activeLabels)

-- Run the TSIO computation
-- In the resulting state, the list of active labels should be empty:
-- all handles must be closed. The resulting counter can be any, qc
runTSIO :: (forall s. TSIO s (Z,N) (qc,N) a) -> IO a
runTSIO m = unTSIO m  -- somehow, eta-expansion is needed here

-- low-level primitive to work with TSHandles. They are certainly not exported.
new_shandle ioh = r
 where
 r         = tsio (ioh >>= \h ->return (shandle h s cnt)) undefined undefined so
 s         = tsio_s r
 so        = (newcnt,newlst)
 newcnt    = inc cnt
 newlst    = C cnt lst
 (cnt,lst) = tsio_in r

-- Check that the handle is current. 
check_shandle sh@(TSHandle h) f = r
  where
  (s,l)  = shandle_l sh
  r  = tsio (f h) s undefined so
  so = tsio_in r
  (_,activelabels) = so
  -- If the label can be removed, it means it is present.
  _ = apply RemL (l,activelabels)


-- Remove the handle from the list of active. 
remove_shandle sh@(TSHandle h) f = r
  where
  (s,l)  = shandle_l sh
  r = tsio (f h) s undefined (cnt,activelabels')
  (cnt,activelabels) = tsio_in r
  activelabels' = apply RemL (l,activelabels)

test1 = runTSIO (glift (print "yes") +>>
	        (gret "yes again")) >>= print


-- All errors are considered fatal. See the paper
tshOpen fname mode = new_shandle (openFile fname mode)
tshClose sh = remove_shandle sh close
 where close h = do
		 hPutStrLn stderr $ "Closing " ++ show h
		 hClose h

-- regular handle operations
tshIsEOF sh    = check_shandle sh hIsEOF 
tshGetLine sh  = check_shandle sh hGetLine
tshPutStrLn sh = check_shandle sh . flip hPutStrLn

tshReport :: StateOK p => String -> TSIO s p p ()
tshReport str = TSIO (hPutStrLn stderr str)


-- The Final combinator
infixl 1 +>>>
(+>>>) :: TSIO s p q a -> TSIO s q r b -> TSIO s p r b
m1 +>>> m2 = TSIO (do
		   r1 <- try (unTSIO m1)
		   r2 <- unTSIO m2 
		   either throwIO (const (return r2)) r1)


test12 () = tshOpen "/etc/motd" ReadMode        >==
	    \h1 -> tshOpen "/dev/null" ReadMode >==
	    \h2 -> tshGetLine h1

-- Note the inferred type: two handles are open
-- Therefore, the following leads to a type error: non-closed handles left
-- test2r = runTSIO (test2 ())

-- The following is accepted (the constraint resolution is delayed due
-- to the polymorphic type, the error is reported below)
test13 () = tshOpen "/etc/motd" ReadMode >==
	    \h1 -> tshOpen "/dev/null" ReadMode >==
	    \h2 -> 
	       tshClose h1 +>>
	       tshClose h2 +>>
	       tshGetLine h1

-- The following is again a type error: although all the handles are closed,
-- we attempted to read from a closed handle (h1)
-- test3r = runTSIO (test3 ())

-- Here, the error is reported more immediately
{-
test13' = runTSIO (tshOpen "/etc/motd" ReadMode >==
	    \h1 -> tshOpen "/dev/null" ReadMode >==
	    \h2 -> 
	       tshClose h1 +>>
	       tshClose h2 +>>
	       tshGetLine h1)
-}

-- Here, we see non-nesting: h1 is opened before h2 and is closed before h2
test14 () = tshOpen "/etc/motd" ReadMode >==
	    \h1 -> tshOpen "/dev/null" ReadMode >==
	    \h2 -> 
	       tshClose h1 +>>
	       tshClose h2 +>>
	       gret "OK"
test14r = runTSIO (test14 ())

test15 () = tshOpen "/etc/motd" ReadMode >==
	    \h1 -> tshOpen "/dev/null" ReadMode >==
	    \h2 -> tshGetLine h1 >==
	      \l->
	       tshClose h2 +>>
	       -- tshClose h1 +>>	-- can't close the handle twice
	       tshClose h1 +>>
	       gret l
test15r = runTSIO (test15 ())

-- Standard tests from SafeHandlesTest.hs

test4 h1 h2 = do
	      d1 <- tshGetLine h1
	      tshPutStrLn h2 d1


{- Ken's test:
A programming example using the enumerator (rather than cursor) pattern to
    (1) read a file name from a file
    (2) open that file and zip the two files' contents together
thus assuring that the files are accessed correctly and resources
disposed of completely.
-}


till condition iteration = loop where
  loop = do b <- condition
            if b then return () else iteration >> loop

test3 = runTSIO (
  tshOpen "/tmp/SafeHandles.hs" ReadMode >== \h1 ->
  test3_internal h1 >== \h3 ->
  -- once we closed h2, we write the rest of h1 into h3
  till (tshIsEOF h1)
       (tshGetLine h1 >>= tshPutStrLn h3) >>
  tshReport "test3 done" +>>
  tshClose h1 +>>			-- if we omit it, error is reported
  tshClose h3				-- if we omit it, error is reported
  )

-- The following shows that we do not have to put all IO code in
-- one big function. We can spread it out. The inferred type for the
-- following is _region-polymorphic_.
test3_internal h1 = 
  tshOpen "/tmp/ex-file.conf" ReadMode >== \h2 ->
		-- read the fname from the config file
  tshGetLine h2 >== \fname ->
  tshOpen fname WriteMode >== \h3 ->
  -- zip h2 and h1 into h3
  tshPutStrLn h3 fname >>
  till (liftM2 (||) (tshIsEOF h2) (tshIsEOF h1))
       (tshGetLine h2 >>= tshPutStrLn h3 >>
        tshGetLine h1 >>= tshPutStrLn h3) >>
  tshReport "Finished zipping h1 and h2" +>>
  tshClose h2 +>>
  gret h3


-- The problem however remains if the second tshOpen throws an exception
-- Then h1 is not closed...
test_exc = runTSIO (
   tshOpen "/etc/motd" ReadMode >== \h1 ->
   tshGetLine h1 >== \l1 ->
   tshOpen "/etc/hosts" ReadMode >== \h2 ->  -- ReadMode is deliberate!
   tshPutStrLn h2 l1 +>>>		     -- must cause an error
   tshClose h1 +>>
   tshPutStrLn h2 l1 +>>>
   tshClose h2)


-- ----------------------------------------------------------------------
-- Parameterized, state-changing Monad-like

class Monadish m where
    gret :: a -> m p p a
    gbind :: m p q a -> (a -> m q r b) -> m p r b

-- Inject regular monads to be monadish things too
newtype MW m p q a = MW{ unMW:: m a }

instance Monad m => Monadish (MW m) where
    gret = MW . return
    gbind (MW m) f = MW (m >>= unMW . f)

-- some syntactic sugar

infixl 1 +>>
vm1 +>> vm2 = gbind vm1 (const vm2)

infixl 1 >==
m >== f = gbind m f



-- ----------------------------------------------------------------------
-- Peano numerals, used to label handles
-- We only require the successor and comparison operations

data Z
data S a
inc :: a -> S a
inc = undefined

class Nat0 n
instance Nat0 Z
instance Nat0 n => Nat0 (S n)

data HTrue
data HFalse

__ = __

-- n1 ==  n2 --> HTrue
-- otherwise --> HFalse
class EQN n1 n2 r | n1 n2 -> r
instance EQN Z Z HTrue
instance EQN Z (S n) HFalse
instance EQN (S n) Z HFalse
instance EQN n1 n2 r => EQN (S n1) (S n2) r

eqn :: EQN n1 n2 r => n1 -> n2 -> r; eqn = undefined

n0 :: Z = __
n1 = inc n0
n2 = inc n1
n3 = inc n2

test_eqn1 = eqn n0 n1
test_eqn2 = eqn n1 n1
test_eqn3 = eqn n2 n1

-- ----------------------------------------------------------------------
-- A bit of HList

data N     = N
data C a b = C a b

-- A heterogeneous apply operator

class Apply f a r | f a -> r where
  apply :: f -> a -> r
  apply = undefined			-- In case we use Apply for
                                        -- type-level computations only

-- Normal function application

instance Apply (x -> y) x y where
  apply f x = f x

-- Identity
data Id = Id

instance Apply Id x x where
  apply _ x = x

-- Type-level computation
-- remove a label from a list of labels

data Closure f arg			-- not exported

data RemL = RemL
instance (EQN l e bf, Apply (Closure RemL bf) (l,(C e r)) w) 
    => Apply RemL (l,(C e r)) w
instance Apply (Closure RemL HTrue) (l,(C l r)) r
instance Apply RemL (l,r) w => Apply (Closure RemL HFalse) (l,(C e r)) (C e w)

test_Reml1 = apply RemL (n0,(C n0 N))
-- Type error
-- test_Reml2 = apply RemL (n3,(C n0 (C n1 (C n2 N))))
test_Reml3 = apply RemL (n0,(C n0 (C n1 (C n2 N))))
test_Reml4 = apply RemL (n1,(C n0 (C n1 (C n2 N))))
test_Reml5 = apply RemL (n2,(C n0 (C n1 (C n2 N))))

-- Find an element in a heterogenous list satisfying a given predicate
-- The element must be present
newtype FindL f = FindL f
instance (Apply pred e bf, Apply (Closure (FindL pred) bf) (C e r) w)
    => Apply (FindL pred) (C e r) w
instance Apply (Closure (FindL pred) HTrue) (C e r) e
instance Apply (FindL pred) r w 
    => Apply (Closure (FindL pred) HFalse) (C e r) w

test_Findl1 = apply (FindL (EqtoN n1)) (C n0 (C n1 (C n2 N)))

newtype EqtoN n = EqtoN n
instance EQN n1 n2 r => Apply (EqtoN n1) n2 r