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

{- 
  Strongly typed memory areas. The videoRAM example from
     Strongly Typed Memory Areas
     Programming Systems-Level Data Structures in a Functional Language
     Iavor S. Diatchki Mark P. Jones, Haskell Workshop 2006
 rewritten in real Haskell. The paper is to be referred to as STMA.
-}

module VideoRAM where

import Areas
import Control.Monad
import Foreign.Ptr
import Data.Int (Int8, Int16)
import Prelude hiding (div)

type N5  = U (U B1 B0) B1
type N6  = U (U B1 B1) B0
type N80 = U (U (U (U N5 B0) B0) B0) B0
type N25 = U (U N6 B0) B1

-- This is just like in the STMA paper:
--   type Screen = Array 25 (Array 20 ScreenChar)
type ScreenCharT = Pair AWord8 AWord8 -- attribute and char proper
scrchar_attr r = afst r
scrchar_char r = asnd r

type ScreenT   = Array N25 (Array N80 ScreenCharT)

data Screen = Screen
instance Property Screen APInHeap HTrue
instance Property Screen APARef (ARef N8 ScreenT)
instance Property Screen APReadOnly HFalse
instance Property Screen APOverlayOK HTrue

type SmallScreenT   = Array N5 (Array N80 ScreenCharT)

-- we can place the Screen area at a fixed absolute address
data ScreenAbs = ScreenAbs
instance Property ScreenAbs APInHeap HFalse
instance Property ScreenAbs APARef (ARef N8 ScreenT)
instance Property ScreenAbs APReadOnly HFalse
instance Property ScreenAbs APFixedAddr HTrue

-- Don't execute the following test, unless you're really on the DOS machine
videoRAM = area_at ScreenAbs (nullPtr `plusPtr` 0xb8000)
{-
*VideoRAM> :t videoRAM
testv0 :: ARef N8 (AtArea ScreenAbs ScreenT)
-}

-- Implementing the VideoRAM API, as in the STMA paper


-- Provide a reference to a character at the location (i,j) of the screen
-- The attribute of a character is not affected
attrAt i j = vram_attr_at videoRAM i j
charAt i j = vram_char_at videoRAM i j
{- The inferred type is kind of nice. Nice computed alignment.
*VideoRAM> :t charAt
charAt :: Ix N25 -> Ix N80 -> ARef B1 (AtArea ScreenAbs AWord8)
-}

vram_attr_at vram i j = scrchar_attr $ vram @@ i @@ j 
vram_char_at vram i j = scrchar_char $ vram @@ i @@ j 


forEachIx proc = loop minBound
  where
  loop ix = do
	    proc ix
	    maybe (return ()) (loop) (ixSucc ix <<= maxBound `asTypeOf` ix)

  
-- The first implementation of clearing the screen: double loop over
-- rows and columns. Not very efficient...

vram_cls vram =
    forEachIx (\r -> 
      forEachIx (\c -> write_cell (vram @@ r @@ c)))
 where write_cell cell = 
	   do
	   write_area (scrchar_attr cell) 0x07  -- white on black attribute
	   write_area (scrchar_char cell) 0x20  -- space character

-- The second implementation: cast the vram as a single array
-- We could have use as_bytes to treat the area as an array of bytes.
-- But we want a bit more structure: when we clean the area, we not 
-- necessarily wish to set attr to the same value as a char
-- So, we cast the Screen to a 1D array of BEA_Int16.

-- In the following, we assume the check that 0x7020 indeed fits within
-- Int16 is performed at _compile time_. Or, alternatively, the value
-- will be `narrowed' to fit (see GHC.Prim.narrow16Int#). Again at
-- compile time, because the value is literal.
-- Of course we can be more explicit, and use bounded integer operations
--  bounded_int :: IntBoundedOK n a => n -> a
-- We use the former method here.
blank :: Int16
blank = 0x7020   -- space on white background

{-
vram_cls' vram = forEachIx (\i -> write_area (vram' @@ i) blank)
  where
  vram' = as_area vram 
	    -- we get the type error here, if we forget div by 2
	    -- (mk_array_t (size_of . aref_area $ vram) (undefined::BEA_Int16))
	    (mk_array_t (div (size_of . aref_area $ vram) nat2)
	     (undefined::BEA_Int16))
	    nat0  -- offset; if we set it to nat1, we get another type error
-}

vram_cls' vram = forEachIx (\i -> write_area (vram' @@ i) blank)
  where
  vram' = as_area vram 
	    (mk_array_t undefined (undefined::BEA_Int16))
	    nat0  -- offset; if we set it to nat1, we get another type error
  _ = (size_of (aref_area vram)) `asTypeOf` (size_of (aref_area vram'))


testv1 = with_area Screen (\vram ->
	do
        let i1 = maxBound `asTypeOf` (arr_index . aref_area $ vram)
	let rp = vram @@ i1
        let i2 = maxBound `asTypeOf` (arr_index . aref_area $ rp)
	let cr = rp @@ i2
	write_area (afst cr) 1
	-- the following leads to an error: offset is too large
	-- let small_vram = array_offset vram (undefined::SmallScreenT) 
	--		  (undefined::N25)
	{-
	let small_vram = array_offset vram (undefined::SmallScreenT)
			  (undefined::N6)
	-- the following really takes a while...
        let i3 = maxBound `asTypeOf` (arr_index . aref_area $ small_vram)
	return (show i1, show i2, show i3)
	-}

        --vram_cls vram
        vram_cls' vram

        -- select a specific character
        let sr = 5; sc = 10
        let Just sri = toIx sr; Just sci = toIx sc
	let cell = vram @@ sri @@ sci
	sattr <- read_area (scrchar_attr cell)
	schar <- read_area (scrchar_char cell)
	return (sattr, schar)
        ) >>= print