{-# 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 AreaTests where

import Areas
import Control.Monad

-- First is just a simple example of a structured memory area



-- define the type of our area: a pair of pairs.
-- TH can be used for a more convenient notation. We avoid the syntactic
-- sugar for clarity

-- When we used the following definition, we get a type error!
-- BEA_Int16 is misaligned: it must be at the 2-byte boundary
-- type AreaT = Pair AInt8 (Pair BEA_Int16 AWord8)

type AreaT = Pair BEA_Int16 (Pair AWord8 AInt8)

data TestArea = TestArea		-- label
-- Assign properties: these are like area declarations in STMA
-- TH can generate those, from a STMA-like syntax
instance Property TestArea APInHeap HTrue
instance Property TestArea APARef (ARef N4 AreaT)
instance Property TestArea APReadOnly HFalse
instance Property TestArea APOverlayOK HTrue

test1 = with_area TestArea (\ap ->
	do
        -- If we forget to define ReadOnly property on the area,
	-- we get the type error right here!
	write_area (afst ap) 1
        -- the following raises the expected error. Good!
	-- write_area (asnd (afst ap)) 2

	write_area (afst (asnd ap)) 2
	v1 <- read_area (afst ap)
	v2 <- read_area (afst (asnd ap))
	v3 <- read_area (asnd (asnd ap))
	return (v1,v2,v3)
        )

arr_to_list arrp = loop i0
  where
  i0 = minBound `asTypeOf` (arr_index . aref_area $ arrp)
  im = maxBound `asTypeOf` (arr_index . aref_area $ arrp)
  loop ix = do
	    v <- read_area (arrp @@ ix)
	    maybe (return [v]) (liftM (v:) . loop) (ixSucc ix <<= im)

list_to_arr lst arrp = loop lst i0
  where
  i0 = minBound `asTypeOf` (arr_index . aref_area $ arrp)
  im = maxBound `asTypeOf` (arr_index . aref_area $ arrp)
  loop [] ix = return ()
  loop (h:t) ix = do
	    write_area (arrp @@ ix) h
	    maybe (return ()) (loop t) (ixSucc ix <<= im)

test2 = with_area TestArea (\ap ->
	do
	write_area (afst ap) 1
	write_area (afst (asnd ap)) 2
	write_area (asnd (asnd ap)) 3
			    
        -- the following can succeed only when we assert the overlay property
        let bp1 = as_read_only $ as_bytes ap
	bl1 <- arr_to_list bp1

        -- The following is a type error: can't write to a RO array
	-- list_to_arr [1,2,3,4] bp1

        -- make an emphemeral writable view
        list_to_arr [1,2,3,4] (as_bytes ap)

        let ap2 = as_area bp1 (undefined::LEA_Int16) nat0
	w0 <- read_area ap2

        -- apo2 was created from a ReadOnly array, so writing is not OK
	-- The overlayed area inherits the properties of its base
	-- write_area ap2 0

        -- The following raises a type error due to the wrong alignment
	-- w1 <- read_area (as_area ap (undefined::LEA_Int16) nat1)

	w2 <- read_area (as_area ap (undefined::LEA_Int16) nat2)
        
	return (bl1,w0,w2)
        ) >>= print
-- ([0,1,2,3],513,1027)


-- Testing stored indices

-- We define a structural area, whose first byte is an index
-- to an array of what follows.
-- If we use the following by mistake, we get a type error
-- when we try to use the index with an array
-- type ARIT = Pair (IntBounded N4 AWord8) (Array N2 AInt8)
type ARIT = Pair (IntBounded N4 AWord8) (Array N4 AInt8)

data ARIA = ARIA		-- label
-- Assign properties: 
instance Property ARIA APInHeap HTrue
instance Property ARIA APARef (ARef N4 ARIT)
instance Property ARIA APReadOnly HFalse

test3 = with_area ARIA (\ap ->
	do
	let ir = afst ap
	    ar = asnd ap
	write_area ir minBound
	i0 <- read_area ir
	write_area (ar @@ i0) 0

        -- increment the index, and if it is in range, write it down
	-- The type system will nbot let us forget about the range check
	maybe (return ()) (write_area ir) 
		  (ixSucc i0 <<= maxBound `asTypeOf` i0)
	i1 <- read_area ir
	return (i0,i1)
        ) >>= print