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

{-
   Statically tracking `ticks'

   A `tick' may be an operation to read a byte from a hardware register,
   or to write such a byte. A computation may read a byte and chose
   a subcomputation depending on the value of that byte. These 
   sub-computations may read further bytes. It is important that any sequence
   of sub-computations within one processing cycle has read the same
   number of bytes, so the protocol is obeyed and a frame is fully
   consumed. We should get this guarantee statically.
   Of course one may say we should read all bytes in a buffer... But:
   that requires a memory buffer, and a double-scan of data (first
   read and write into the buffer, then read from the buffer).
   The embedded device (for which we generate the code for, via code-
   generating combinators) may be under-powered for such buffering.


   The second application is to permit different paths through the code
   within one processing cycle differ in the number of ticks. But we want
   to accumulate the max number of ticks. So we can statically determine
   the worst `time complexity' of the code. When we generate the code,
   we may as well associate a number of ticks with a generated instruction
   (and hence, with its generator). So, we can statically estimate the
   worst-case time complexity and determine if our computation might
   fit within allocated time budget. 
   Loops are no problem: all iterations in embedded systems must be
   bound in the number of steps. We can use IntBounded for representing
   the loop counter, and so estimate the max latency of a loop.
  
-}


module RealTime where

import BinaryNumber
import Areas (Ix, (<<=), toIxN, Succ, ixPred)

import Prelude hiding (succ, max)

-- Introduction.
-- This code is based on tagging (monadic) computation with ticks.
-- We need a simple variable-state monad (transformer)
-- The following is excerpted from a message posted on the Haskell
-- mailing list on Dec 17, 2006.
-- However, our implementation here is different: the `state' is emphemeral
-- (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)

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


-- some syntactic sugar

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

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

-- The first example: balanced ticks across the branches

-- Our state is the number of ticks. Define the command that increments
-- the tick

-- tickL m = vsget >== vsput . succ +>> glift m
-- The following is the same as above. However, it makes it clear
-- there are no run-time computations.
tickL :: (Monad m, Succ si so) => m v -> VST m si so v
tickL = VST


-- Define the command that `reads a byte'. We tag this command as
-- `tickable', that is, advancing the tick counter

tread_byte :: Succ si so => VST IO si so Int
tread_byte = tickL (do
		    putStrLn "Read byte"
		    return 1)		-- the value of the read byte


-- Sample computation:
-- We read a byte. We branch upon the byte value. In one branch, we
-- read the second byte and branch again. In some branches, we have
-- to add dummy reads to balance the reading in other branches. If
-- we miss those, the compiler complaints.
-- A do notation for `monadish' would have been nice.


-- It was quite difficult to balance those things...
tex1 = 
  tread_byte >== 
   \b1 -> if b1 > 10 then branch1 b1 
             else branch2 b1 +>> tread_byte +>> tread_byte
 where
  branch1 b = tread_byte >== \b2 ->
	        if b2 > 10 then branch4 b2 +>> branch2 b2 else branch3 b2
  branch2 b = tread_byte +>> tread_byte
  branch3 b = tread_byte +>> glift (putStrLn "branch3") +>> tread_byte
	      +>> tread_byte
  branch4 b = tread_byte

runst :: forall m so v. Monad m => VST m N0 so v -> m (so,v)
runst m = runVST m >>= return . (,) (undefined::so)

rundy m = runst m >>= (
           \ (so,r) -> putStrLn $ "ticks " ++ show (toInt so) ++ 
	                          " result: " ++ show r)

te1 = runst tex1
{- It takes 5 ticks. The compiler has figured that out
*RealTime> :t te1
te1 :: IO (U (U B1 B0) B1, Int)
-}

te2 = rundy tex1


-- The second example: worst-case complexity

-- Needed a new branching combinator

data Else = Else

gif tst th Else el = vsputL (if tst then runVST th else runVST el) si sm
  where (si1,st) = gets th		-- these aren't actually run!
        (si2,se) = gets el
        sm = max st se
	si = if True then si1 else si2
        gets :: VST m si so v -> (si,so); gets = undefined


-- now, branches are not balanced


tex2 () = 
  tread_byte >== (
   \b1 -> gif (b1 > 10) (branch1 b1)
              Else (branch2 b1 +>> tread_byte +>> tread_byte))
 where
  branch1 b = tread_byte >== (\b2 ->
	        gif (b2 > 10) (branch4 b2 +>> branch2 b2)
			      Else (branch3 b2))
  branch2 b = tread_byte +>> tread_byte
  branch3 b = glift (putStrLn "branch3") +>> tread_byte
  branch4 b = tread_byte +>> tread_byte

te3 = runst (tex2 ())
{- The worst-case complexity through the branches
*RealTime> :t te3
te3 :: IO (U (U B1 B1) B0, Int)
-}

te4 = rundy (tex2 ())


-- The third example: worst-case complexity in the presence of loops

-- First, we read a byte from the register. If it is less than 10,
-- we read that many more bytes. Otherwise, we just read one more
-- byte. Compute the worst-time complexity.

nat10 = add nat2 nat8			-- type-level numerals

tex3 () = 
  tread_byte >== \b1 ->
   gmaybe (branch2 b1) (loop b1) (toIxN nat10 b1)
 where
   branch2 _ = tread_byte
   loop b ix = foldTM branch1 b ix
   branch1 b = glift (putStrLn "branch1")  +>> tread_byte +>> tread_byte

-- FoldM with an upper-bound tick accumulation. That code should be
-- in the security kernel.
foldTM :: (Monad m, NatE n, Succ n' n, Add si diff so',
	   Mul diff n' grand_diff, Add si grand_diff so) => 
	  (v -> VST m si so' v) -> v -> Ix n -> VST m si so v
foldTM f seed ix = VST( loop seed (ixPred ix) )
 where loop seed ixm 
	  = maybe (return seed) (loop' seed) ((minBound `asTypeOf` ix) <<= ixm)
       loop' seed ix = do seed' <- runVST (f seed); loop seed' (ixPred ix)
			 

gmaybe onnothing onjust mv 
    = vsputL (maybe (runVST onnothing) (runVST . onjust) mv) si sm
  where (si1,st) = gets onnothing		-- these aren't actually run!
        (si2,se) = gets (onjust undefined)
        sm = max st se
	si = if True then si1 else si2
        gets :: VST m si so v -> (si,so); gets = undefined

te5 = runst (tex3 ())
{- The worst-case complexity through the branches
*RealTime> :t te5
te5 :: IO (U (U (U B1 B0) B1) B0, Int)
-}

te7 = rundy (tex3 ())