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

-- Strongly typed memory areas. The implementation of the library

{- 
 Rewriting the examples and snippets from
     Strongly Typed Memory Areas
     Programming Systems-Level Data Structures in a Functional Language
     Iavor S. Diatchki Mark P. Jones, Haskell Workshop 2006
 in real Haskell. The paper is to be referred to as STMA.

 We use Haskell FFI to manipulate `raw' pointers to `raw' memory areas.
-}


module Areas (
	      ARef,		-- the data constructor is not exported
	      Ref, aref_area, aref_al,
	      SizeOf(..), size_of,
	      -- pre-defined primitive areas
	      AInt8, AWord8, BEA_Int16, LEA_Int16, AInt16, AWord16,

              -- ValIn,			-- members not exported!
	      realign, 

              -- pairs
	      Pair, PAIR(..), afst_sig, afst, asnd_sig, asnd,

              -- arrays
              INDEXABLE(..), Array, mk_array_t, aref_sig, (@@), array_offset,
	      as_bytes, as_area,

	      -- indices
	      Ix, IxPlus, IxMinus, 	-- data costructors not exported!
	      fromIx, toIx, toIxN, (<<=), ixPlus, ixMinus, ixSucc, ixPred,
              IntBounded,               -- data costructors not exported!

              HTrue, HFalse,

              Property, AtArea,
	      -- pre-defined properties
	      APReadOnly, APInHeap, APARef, APOverlayOK, APFixedAddr,
	      as_read_only,

	      -- area allocators
	      new_area, with_area, read_area, write_area, area_at,
	      module BinaryNumber
	     ) where

import BinaryNumber
import Prelude hiding (gcd, succ)

import Foreign
import Foreign.Storable as FFIS
import Foreign.C


-- The universal class to make writing overloaded functions easier
class Apply f x y | f x -> y where
    apply :: f -> x -> y; apply = undefined

-- An area is the description of a memory area.
-- Note the difference between `Areas' and `areas' of the STMA paper.
-- The former is a kind, describing the layout etc. of a memory area.
-- The latter is a declaration for a reference to the memory of that
-- kind, as well as some properties.
-- We distinguish primitive Areas (Int8), structural areas (pairs and
-- other structures), array areas and labeled/attributed Areas.
-- The latter is an Area with a label, which lets us find area
-- attributes such as ReadOnly, allocation policy, etc.

-- The (implicitly, non-zero) pointer to some memory area.
-- 'area' is the label of the area.
-- The data constructor is not exported.
newtype ARef alignment area = ARef (Ptr Word8)
type Ref area = ARef N1 area

aref_area :: ARef al area -> area; aref_area = undefined
aref_al   :: ARef al area -> al;   aref_al = undefined
-- the following is NOT exported
cast_aref :: Ptr Word8 -> alignment -> area -> ARef alignment area
cast_aref p _ _ = ARef p

-- All areas are the members of the class SizeOf (see STMA paper).
-- The class relates an area label with the size of the data, in bytes.
-- One may say that SizeOf is the predicate for the kind area.

class NatE n => SizeOf area n | area -> n where -- just like in STMA
    memCopy :: ARef al area -> ARef al' area -> IO ()
    memCopy p@(ARef pfrom) (ARef pto) = 
       copyBytes pto pfrom (toInt . size_of . aref_area $ p)
    memZero :: Ref area -> IO ()
    memZero = undefined

size_of :: SizeOf area n => area -> n; size_of = undefined

-- ------------------------------------------------------------------------
-- Pre-defined primitive areas

data AInt8				-- signed byte
data AWord8				-- unsigned byte
data AInt16				-- signed native 16-bit int
data BEA_Int16				-- signed big-endian 16-bit int
type LEA_Int16 = AInt16			-- signed little-endian 16-bit int
data AWord16				-- unsigned native 16-bit int
    -- many more can be defined likewise

instance SizeOf AInt8 N1 where
    memCopy (ARef pfrom) (ARef pto) = peek pfrom >>= poke pto
    memZero (ARef pto) = poke pto 0

instance SizeOf AWord8 N1 where
    memCopy (ARef pfrom) (ARef pto) = peek pfrom >>= poke pto
    memZero (ARef pto) = poke pto 0

instance SizeOf AInt16 N2 where
    memCopy (ARef pfrom) (ARef pto) = 
	peek ((castPtr pfrom)::Ptr Int16) >>= poke ((castPtr pto)::Ptr Int16)
    memZero (ARef pto) = poke ((castPtr pto)::Ptr Int16) 0

instance SizeOf AWord16 N2 where
    memCopy (ARef pfrom) (ARef pto) = 
	peek ((castPtr pfrom)::Ptr Word16) >>= poke ((castPtr pto)::Ptr Word16)
    memZero (ARef pto) = poke ((castPtr pto)::Ptr Word16) 0

instance SizeOf BEA_Int16 N2 where
    memCopy (ARef pfrom) (ARef pto) = 
	peek ((castPtr pfrom)::Ptr Word16) >>= poke ((castPtr pto)::Ptr Word16)
    memZero (ARef pto) = poke ((castPtr pto)::Ptr Word16) 0

-- All primitive areas are the members of the class ValIn (see STMA paper).
-- The class relates an area label with the type of the values it contains.
-- It also establishes the minimal requirement on the alignment, so that
-- appropriate instructions to access memory could be used

class ValIn area primval minalignment | area -> primval minalignment where
    readRef  :: GCD al minalignment minalignment =>
		ARef al area -> IO primval
    writeRef :: GCD al minalignment minalignment =>
		ARef al area -> primval -> IO ()

instance ValIn AInt8  Int8  N1 where
    readRef  (ARef p) = peek . castPtr $ p
    writeRef (ARef p) = poke . castPtr $ p

instance ValIn AWord8 Word8 N1 where
    readRef  (ARef p) = peek . castPtr $ p
    writeRef (ARef p) = poke . castPtr $ p

instance ValIn AWord16 Word16 N2 where
    readRef  (ARef p) = peek . castPtr $ p
    writeRef (ARef p) = poke . castPtr $ p
instance ValIn AInt16  Int16 N2 where
    readRef  (ARef p) = peek . castPtr $ p
    writeRef (ARef p) = poke . castPtr $ p

-- Most significant byte first
instance ValIn BEA_Int16 Int16 N2 where
    readRef  (ARef p) = 
	do
	(bh::Word16) <- peek ((castPtr p)::Ptr Word8)
			>>= return . fromIntegral
	(bl::Word16) <- peek ((p `plusPtr` 1)::Ptr Word8)
			>>= return . fromIntegral
	return . fromIntegral $ (bh `shiftL` 16) .|. bl
    writeRef  (ARef p) v =
	do
	let (uv::Word16) = fromIntegral v
	poke p (fromIntegral (uv `shiftR` 8))
	poke ((p `plusPtr` 1)::Ptr Word8) (fromIntegral uv)

	

-- ------------------------------------------------------------------------
-- Static pointer arithmetics: given (ARef al1 area1) and 
-- area2 that is a part of area1 at the `offset',
-- compute (ARef al2 area2).
-- We check that Sizeof(area1) >= offset + SizeOf(area2) and
-- we compute the correct alignment al2

-- We can statically program either at the type level, or the term level.
-- That is, we specify the computation either with constraints,
-- or via the familiar-looking term computations. The result is the same:
-- no run-time computations.
{-
aref_offset :: (SizeOf area1 n1, SizeOf area2 n2, Nat0E offset,
		Add n2 offset n2offset, NLessEq n2offset n1,
		GCD offset al1 al2)
	       => ARef al1 area1 -> area2 -> offset -> ARef al2 area2
-}
aref_offset r@(ARef p1) area2 offset = 
    cast_aref (p1 `plusPtr` (toInt offset)) alignment area2
  where
    alignment = gcd offset (aref_al r)
    () = assert_leq (add offset (size_of area2)) (size_of area1)
    area1 = aref_area r
  


-- from the STMA paper
realign :: GCD a b b => ARef a t -> ARef b t
realign (ARef p) = ARef p

-- ------------------------------------------------------------------------
-- Structural values

-- Pairs: Pair s t declares an area s followed by an area t

data Pair area1 area2

-- To be able to treat attributed and unattributed pairs uniformly
class PAIR a a1 a2 | a -> a1 a2 where
    pair_fst :: a -> a1; pair_fst = undefined
    pair_snd :: a -> a2; pair_snd = undefined

instance PAIR (Pair a1 a2) a1 a2

-- The following declaration makes sure that in order for `Pair area1 area2'
-- to define an area, both area1 and area2 must. Recall that
-- SizeOf is the kind predicate for the `area' kind.
instance (NatE n, SizeOf area1 n1, SizeOf area2 n2, Add n1 n2 n)
    => SizeOf (Pair area1 area2) n

-- components of a pair

-- Here, we use the trick of partial signatures, to avoid enumerating
-- all the constraints.
-- The following definition does not have to be trusted, because aref_offset
-- is.
afst_sig :: PAIR a a1 a2 => ARef al a -> ARef al a1; afst_sig = undefined
afst p | False = afst_sig p
afst p = aref_offset p (pair_fst $ aref_area p) nat0

asnd_sig :: PAIR a a1 a2 => ARef al a -> ARef al' a2; asnd_sig = undefined
asnd p | False = asnd_sig p
asnd p = aref_offset p (pair_snd pair) (size_of $ pair_fst pair)
  where pair = aref_area p

-- more complex structures (such as the ones in the STMA paper) can
-- be defined similarly: as pairs of pairs of pairs, ...
-- with TH providing convenient syntactic sugar.


-- ------------------------------------------------------------------------
-- Arrays


-- The kind predicate for arrays. The constraint dictate that the kind
-- indexable is a kind of Areas
class (NatE count, SizeOf a totalsize)
    => INDEXABLE a count base totalsize | a -> count base totalsize where
    arr_count :: a -> count; arr_count = undefined
    arr_base  :: a -> base;  arr_base  = undefined
    arr_index :: a -> Ix count; arr_index = undefined

-- An example of mixed term-type-level programming. Some constraints
-- are specified at the type level, via a _partial_ signature. The rest
-- of the constrints is inferred from terms.
aref_sig :: INDEXABLE arr count base totalsize => 
	    ARef al arr -> Ix count -> ARef al' base
aref_sig = undefined
infixl 5 @@
r @@ i | False = aref_sig r i
r@(ARef p) @@ (Ix i) = cast_aref (p `plusPtr` (i*toInt base_size)) al base
  where
  base = arr_base (aref_area r)
  base_size = size_of base
  al = gcd (aref_al r) base_size


data Array count area
mk_array_t :: count -> area -> Array count area; mk_array_t = undefined

-- This instance says that Array is of a kind AREA
instance (NatE m, SizeOf area n, Mul count n m)
    => SizeOf (Array count area) m

instance (NatE count, NatE totalsize, SizeOf area n, Mul count n totalsize)
    => INDEXABLE (Array count area) count area totalsize


-- The same as aref_offset, only the offset in elements rather than
-- in bytes. This is useful for sub-ranging an array.
-- The constraints of aref_offset make sure the sub-array is within
-- the original array.
array_offset r arr2 elem_offset = aref_offset r arr2 byte_offset
  where
  elem_size = size_of . arr_base . aref_area $ r
  byte_offset = mul elem_size elem_offset



-- ------------------------------------------------------------------------
-- Indices. 
-- The design follows our `lightweight static capabilities'
-- rather than STMA. Our design is more general and does not require
-- any weird `patterns'.


-- Ix n is a non-negative integer less than n. The static numeral
-- n is the least upper bound for the index.
newtype NatE n => Ix n = Ix Int
    deriving (Ord, Eq, Show)

-- This is a positive integer. We are only sure about its greatest lower bound
-- (zero); we can't say anything about the upper bound. The value of
-- IxPlus is the result of adding a positive quantity to an Ix value.
newtype IxPlus = IxPlus Int
    deriving (Ord, Eq, Show)

-- This is an integer less than the positive number n. We are only sure
-- about its upper bound, n. We can't say anything about the lower bound. 
-- The value of IxMinux is the result of subtracting a positive quantity
-- from an Ix value.
newtype NatE n => IxMinus n = IxMinus Int
    deriving (Ord, Eq, Show)


-- index/integer conversions
class FROMIX x where fromIx :: x -> Int
instance NatE n => FROMIX (Ix n) where fromIx (Ix x) = x
instance FROMIX IxPlus where fromIx (IxPlus x) = x
instance NatE n => FROMIX (IxMinus n) where fromIx (IxMinus x) = x

instance NatE n => Bounded (Ix n) where
    minBound = Ix 0			-- also part of the trusted kernel
    maxBound = Ix . Prelude.pred . toInt $ (undefined::n)

-- The following makes the dynamic check and blesses the integer to be an
-- index
toIx :: forall n. NatE n => Int -> Maybe (Ix n)
toIx = toIxN (undefined::n)
toIxN :: NatE n => n -> Int -> Maybe (Ix n)
toIxN n x = if x >= 0 && x < upbound then Just $ Ix x else Nothing
  where upbound = toInt n

-- index comparisons
infix 4 <<=

-- Also part of the trusted kernel. See KMP-deptype.hs
-- Recovering of the bounds

class IXCMP i1 i2 i3 | i1 i2 -> i3 where
    (<<=) :: i1 -> i2 -> Maybe i3

instance NatE n => IXCMP IxPlus (Ix n) (Ix n) where
    (IxPlus i1) <<= (Ix i2) = if i1 <= i2 then Just $ Ix i1 else Nothing

instance NatE n => IXCMP (Ix n) (IxMinus n) (Ix n) where
    (Ix i1) <<= (IxMinus i2) = if i1 <= i2 then Just $ Ix i2 else Nothing

instance NatE n => IXCMP (IxPlus) (IxMinus n) (Ix n,Ix n) where
    (IxPlus i1) <<= (IxMinus i2) = 
	if i1 <= i2 then Just $ (Ix i1,Ix i2) else Nothing

ixPlus:: (NatE n, NatE m) => Ix n -> m -> IxPlus
ixPlus (Ix i) m = IxPlus $ i + toInt m

ixMinus:: (NatE n, NatE m) => Ix n -> m -> IxMinus n
ixMinus (Ix i) m = IxMinus $ i - toInt m

ixSucc i = ixPlus  i nat1
ixPred i = ixMinus i nat1

-- The type of integers with the statically known bounds: 0 <= x < n
-- Here 'a' is the type like Word8, Word16, etc. The data constructor
-- is not exported. The constraint is to make sure that 'n' does not
-- exceed what 'a' can represent. The application of this type is
-- for indices stored as Word8, etc. data in areas.
newtype IntBoundedOK n a => IntBounded n a = IntBounded a

class NatE n => IntBoundedOK n a
instance (NatE n, NLessEq n (U (U (U (U (U (U (U (U B1 B0) B0) B0) B0) B0) B0) B0) B0))
    => IntBoundedOK n AWord8

instance (IntBoundedOK n area, SizeOf area size)
    => SizeOf (IntBounded n area) size

instance (Integral t, ValIn area t al) 
    => ValIn (IntBounded n area) (Ix n) al where
    readRef  r@(ARef p) = readRef (cast_aref p (aref_al r) (undefined::area))
			  >>= return . Ix . fromIntegral
    writeRef r@(ARef p) (Ix x) 
	= writeRef (cast_aref p (aref_al r) (undefined::area))
	           (fromIntegral x)


-- ------------------------------------------------------------------------
-- Attributed Areas: Areas with associated properties. We asscociate a label
-- with an area. The latter is used as a key to look up the values of
-- various properties.
-- The following is essentially a type record --
-- something that the STMA paper wanted but did not attain.
-- Note our implementation presupposes that area properties must be
-- pre-declared. And still, the set of the properties is open and
-- extensible!

-- Later on, we need to think of possibly fuller integrating the type records
-- into our design. For example, instead of a class SizeOf, have a
-- SizeOf property.

data AtArea label area			-- an area with attributes

data HTrue				-- Boolean kind
data HFalse
class HBool a where toBool :: a -> Bool -- the bool kind predicate
instance HBool HTrue where toBool _ = True
instance HBool HFalse where toBool _ = False


-- We assert that an area labeled `label' has the named `property' of `value'
class Property label property value | label property -> value

-- define some property names (could be defined in a separate module...)
data APReadOnly
data APInHeap
data APARef

cast_aref_unattr :: ARef al (AtArea label area) -> ARef al area
cast_aref_unattr (ARef p) = ARef p

instance SizeOf area n => SizeOf (AtArea label area) n where
    memCopy from to = 
	memCopy (cast_aref_unattr from) (cast_aref_unattr to)

instance ValIn area t minal => ValIn (AtArea label area) t minal where
    readRef  r = readRef  (cast_aref_unattr r)
    writeRef r = writeRef (cast_aref_unattr r)

instance PAIR a a1 a2 => PAIR (AtArea l a) (AtArea l a1) (AtArea l a2)

instance INDEXABLE a count base size 
    => INDEXABLE (AtArea l a) count (AtArea l base) size


instance Property area p v => Property (Array count area) p v

instance Property label p v => Property (AtArea label area) p v

-- Read-only trait
data ROTrait x
instance Property (ROTrait x) APReadOnly HTrue
-- The following really needs overlapping instances. Bummer...
-- instance Property x p v => Property (ROTrait x) p v

instance Property x APARef v => Property (ROTrait x) APARef v
instance Property x APInHeap v => Property (ROTrait x) APInHeap v
instance Property x APOverlayOK v 
    => Property (ROTrait x) APOverlayOK v

-- should probably be a method so it could act on primitive areas,
-- not necessarily arrays
as_read_only:: ARef al (Array count (AtArea l area)) -> 
	       ARef al (Array count (AtArea (ROTrait l) area))
as_read_only (ARef p) = ARef p

-- ------------------------------------------------------------------------
-- Area alocations and operations.
-- The following are the only procedures that create ARefs
-- These procedure create and consumed labeled areas.

-- Allocate a new area via malloc. To make sure the memory is freed
-- (and only once) we should use the state-changing monad. Alternatively,
-- our ARef could store ForeignPtr rather than just Ptr.

-- The procedures new_area and with_area only work with areas that have
-- the attribute APInHeap

new_area :: forall label al area n.
	    (Property label APARef (ARef al area),
	     SizeOf area n, 
	     Property label APInHeap HTrue) => 
	 label -> IO (ARef al (AtArea label area))
new_area l = mallocBytes (toInt (undefined::n)) >>= return . ARef

-- The same only the memory is allocated temporarily and then freed
-- This is useful for debugging
with_area :: forall label al area n b.
	    (Property label APARef (ARef al area),
	     SizeOf area n, 
	     Property label APInHeap HTrue) => 
	 label -> (ARef al (AtArea label area) -> IO b) -> IO b
with_area l f = allocaBytes (toInt (undefined::n)) (f . ARef)

-- Allocating an area over the existing area. These allocators are
-- operationally identity: the don't do anything but change the
-- interpretation/annotation of the area reference.
-- Some areas, like those that include pointers and references, may
-- prohibit overlays, which may compromise their data. Thus, an area
-- that permits re-interpretation/overlay must have the corresponding
-- property.
-- As usual, when we allocate one area on the top of another, we make sure
-- the second area fits.

data APOverlayOK

-- The simplest overlay: cast an area as an array of bytes (AWord8 areas)
as_bytes :: (Property area APOverlayOK HTrue,
	     SizeOf area size)
	    => ARef al area -> ARef al (Array size (AtArea area AWord8))
as_bytes (ARef p) = ARef p


-- Overlay `area2' over the `area' at `offset'.
-- The original area must permit the overlay and be sufficiently big.
-- The alignment is computed.
as_area_sig :: Property area APOverlayOK HTrue =>
	       ARef al area -> area2 -> offset -> ARef al' (AtArea area area2)
as_area_sig = undefined
as_area r area2 offset | False = as_area_sig r area2 offset
as_area r area2 offset = cast_aref p (aref_al r') undefined
  where r'@(ARef p) = aref_offset r area2 offset 

-- Add the procedure to allocate at a specified address. Need to use FFI.
-- Place an area at the specified fixed address. The address can be
-- obtained via a foreign declaration such as
-- foreign import ccall "errno.h &errno" errno :: Ptr CInt
-- foreign import ccall "&foo_symbol"   foo   :: Ptr Word8
-- In the latter case, one has to link with a C file that contains
--  char foo_symbol [AREA_SIZE];
-- Alternatively, one may use a linker (ld) option -defsym
-- to associate foo_symbol with any desired location.
-- We check that the supplied Ptr has the correct alignment.
-- The area to associate with a fixed pointer must have an attribute
-- APFixedAddr True and APInHeap False.

data APFixedAddr
area_at :: forall label al area n.
	    (Property label APARef (ARef al area),
	     NatE al, SizeOf area n, 
	     Property label APFixedAddr HTrue,
	     Property label APInHeap HFalse) => 
	 label -> Ptr Word8 -> ARef al (AtArea label area)
area_at l ptr = if ptr == ptr_al then ARef ptr
		else error "Supplied ptr is misaligned for the area"
  where ptr_al = alignPtr ptr (toInt (undefined::al))
  

-- Reading and writing areas. Should only work for primitive areas
read_area :: (ValIn area primval minal, GCD al minal minal)
	     => (ARef al (AtArea label area)) -> IO primval
read_area = readRef


write_area :: (ValIn area primval minal, GCD al minal minal,
	       Property label APReadOnly HFalse)
	     => (ARef al (AtArea label area)) -> primval -> IO ()
write_area = writeRef