{-# 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.

More elaborated version of the code in multi-handle-io0.hs.
Recursive IO computations are now possible.


Alas, although this approach can work out in the absence of
exceptions, it crumbles when any exceptions arise, and the latter is
inevitable.  Let's consider the code

newRgn $
  do
  h1 <- shOpenFile "file1"
  c1 <- shReadChar
  h2 <- shOpenFile "file2"
  shPutChar h2 c1
  shClose h1
  shPutChar h2 c1
  shClose h2

According to static guarantees, the open/close protocol is obeyed:
when `newRgn' computation finished, all handles opened with the region
are closed. Suppose an exception arose at the first shPutChar. Where
to put an exception handler? At newRgn? How would the handler know
that both h1 and h2 need to be closed? And if an exception arose at
the second shPutChar, then only h2 has to be closed. How would the
handler know that, given that IO exceptions don't contain the type of
the monad where they arose? Furthermore, how would an exception
handler (at newRgn) get hold of the handles to close, given that both
h1 and h2 names are out of scope at that point?

One attempt to save the day is to wrap an exception handler around
_every_ monadic operation, and to pack into the exception the state of
the monad (which is known only statically and erased at run-time -- so
we need a reification, something like Typeable) along with applicable
handles. But that is clearly not a scalable or efficient solution. The
point of an exception is that a handler is placed only at certain
points in a computation. If we check for an exception after each and
every operation, we essentially prohibit exceptions. Alas, in Haskell
exceptions are omni-present.

Thus we reach the conclusion that in the presence of exceptions (which
may occur, in principle, at any point in execution -- even so when IO
is concerned) we cannot get by with purely static gurantees. Some
dynamic checks are necessary -- which defeats this whole approach
because the conventional IO with handles already does the dynamic
check for the validity of a handle.

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

Joint work with Chung-chieh Shan.

-}

module MultiHandle where

import System.IO


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


-- ----------------------------------------------------------------------
-- safe handle and the SIO monad

-- The SIO monad is a VST IO monad where the state is a (heterogeneous)
-- list, which can informally be described as
--
-- kind State = [RegionD]
-- kind RegionD = (Mark, RegionLabel, Counter, ActiveLabels)
-- kind Mark = eigenvariable unque to the region
-- kind Counter = Peano numeral for producing handle labels
-- kind ActiveLabels = [Label]  -- labels of the open handles
-- kind Label = Peano numeral
-- kind RegionLabel = Label -- label for the region. The top region
--                             has label Z
--
-- 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?.
--
-- We permit a sequence of properly nested regions. 
-- Each region describes the set of handles created in that region.
-- An open handle is valid in any child region.
-- Within a region, handles can be opened and closed at will,
-- in any order. One can close handles in the parent region.
-- When the region exits, all handles opened in that region must be closed.
-- A created handle is labeled with the label of the active
-- region and inserted in that region's active label list.
-- 
-- Why we need regions: to be able to write iterative (generally recursive)
-- programs that open handles.
-- The type system then guarantees that one cannot create unbounded
-- amount of open handles. When used with recursive code, the type
-- system will prevent the user to close handles in the parent region.
-- That is good: otherwise, we can't guarantee that each handle is closed
-- exactly once.

type SIO si so v = VST IO si so v
sio_in  :: SIO si so v -> si; sio_in  = undefined
sio_out :: SIO si so v -> so; sio_out = undefined
sio :: (StateOK si, StateOK so) => IO v -> si -> so -> SIO si so v
sio = undefined



-- A handle is labeled by the eignevariable and by the label of the
-- region it is created in, as well as the label within that region
-- The eignevariable is opaque and merely prevents the escape of the handle.
-- The region label is a numeral and lets us locate the region
newtype SHandle s rl l = SHandle Handle
shandle :: Handle -> s -> rl -> l -> SHandle s rl l
shandle h _ _ _ = SHandle h
shandle_l :: SHandle s rl l -> (rl,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				-- non-empty list of regionD
instance RegionDOK regionD => StateOK (C regionD N)
instance (RegionDOK regionD, StateOK r) => StateOK (C regionD r)
class RegionDOK r
-- Add: in any list of active labels, all labels are unique.
instance (Nat0 regionLabel, Nat0 counter) 
    => RegionDOK (mark,regionLabel, counter, activeLabels)

-- create the top region and run a computation in it
-- The resulting state of the computation should be empty as well:
-- all nested regions must be disposed of, and all handles are closed
runSIO :: (forall s. SIO (C (s,Z,Z,N) N) (C (s,Z,any,N) N) v) -> IO v
runSIO m = runVST m  -- somehow, eta-expansion is needed here

-- Create a new region and run a computation there. When the region
-- is over, its list of active handle labels must be empty, i.e., N
-- The signature is a bit unwieldy. We don't have 
-- the `as' construct as in OCaml. Also, we have to write the signature in
-- full because of the higher-rank type.
-- There aren't many such signatures, however.
newRegion :: (forall r. 
	      SIO (C (r,S reglabel,Z,N)
		     (C (s,reglabel,cnt,active) rest))
	          (C (r,S reglabel,any,N)
		     (C (s,reglabel,cnt,active') rest'))
	          v) -> 
     SIO (C (s,reglabel,cnt,active) rest)   -- input state
         (C (s,reglabel,cnt,active') rest') -- result state, some handles
	                                    -- may be closed there
         v
newRegion m = VST (runVST m)

-- low-level primitive to work with SHandles. They are certainly not exported.
new_shandle h = r
 where
 r = sio (return (shandle h s reglabel cnt)) undefined so
 so = C (s,reglabel,newcnt,newlst) rest
 newcnt = inc cnt
 newlst = C cnt lst
 C (s,reglabel,cnt,lst) rest = sio_in r

-- Check that the handle is current. 
check_shandle sh@(SHandle h) f = r
  where
  r = sio (f h) undefined so
  so = sio_in r
  (reglabel, l)  = shandle_l sh
  (m,_,_,activelabels) = apply (FindL (RegLabelQ reglabel)) so
  -- If the label can be removed, it means it is present.
  _ = apply RemL (l,activelabels)


{-
-- Remove the handle from the list of current. 
remove_shandle sh@(SHandle h) f = r
  where
  r = sio (f h) undefined so
  so = sio_in r
  (reglabel, l)  = shandle_l sh
  (m,_,_,activelabels) = apply (FindL (RegLabelQ reglabel)) so
  -- If the label can be removed, it means it is present.
  _ = apply RemL (l,activelabels)
-}

newtype RegLabelQ n = RegLabelQ n
instance EQN n n2 r => Apply (RegLabelQ n) (m,n2,c,ls) r


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


-- regular handle operations
shIsEOF sh = check_shandle sh hIsEOF 

-- shClose:: Handle -> IO ()
-- hFileSize:: Handle -> IO Integer
-- hFlush :: Handle -> IO ()
-- hPutStr :: Handle -> String -> IO ()
-- hPutChar :: Handle -> Char -> IO ()
-- hGetChar :: Handle -> IO Char
-- example with closing the file in the error handler
-- When opening a file, catch the exception and re-raise it by wrapping
-- into `IO error during file open exc'. So, the upward error handler can know
-- when to close the handle and when not.
-- openFile :: FilePath -> IOMode -> IO Handle



-- ----------------------------------------------------------------------
-- Variable state monad transformer
-- The state is variable and purely phantom
-- (type-level only). That at the run-time, our state-changing `monad'
-- is the same as the underlying, base monad.

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

-- Introduce the variable-type phantom state. It is operationally
-- indistinguishable from the base monad m.

newtype VST m si so v = VST{runVST:: m v}

-- lift into the VST monad
glift :: Monad m => m v -> VST m si si v
glift = VST

-- Pure type-level computation (attribution)
vsputL :: Monad m => m v -> si -> so -> VST m si so v
vsputL m _ _ = VST m



instance Monad m => Monadish (VST m) where
  gret = VST . return
  gbind (VST m) f = VST (m >>= runVST . f)

vsget :: forall m si. Monad m => VST m si si si
vsget = VST (return (undefined::si))
vsput :: Monad m => so -> VST m si so ()
vsput x = VST (return ())

-- ----------------------------------------------------------------------
-- 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

{-
-- problem with polymorphic recursion...
reml l (C e rest) = cond (eqn e l) (Id,rest) (f, (e,l,rest))
  where
  f (e,l,r) = C e (reml l r)


class Cond t th el w where
    cond :: t -> th -> el -> w
    cond = undefined

instance (Apply f arg r, TypeCast r w) => Cond HTrue (f,arg) el w where
instance (Apply f arg r, TypeCast r w) => Cond HFalse th (f,arg) w where

test_reml1 = reml n0 (C n0 N)
-- Type error
-- test_reml2 = reml n1 (C n0 N)
test_reml3 = reml n0 (C n0 (C n1 (C n2 N)))
-- *SafeHadles> :t test_reml3
-- test_reml3 :: C (S Z) (C (S (S Z)) N)

-- test_reml4 = reml n1 (C n0 (C n1 (C n2 N)))
-- test_reml5 = reml n2 (C n0 (C n1 (C n2 N)))
-}