-----------------------------------------------------------------------------
-- |
-- Module  :  ForSyDe.Shallow.Model
-- Copyright   :  (c) ForSyDe Group, KTH 2007-2008
-- License     :  BSD-style (see the file LICENSE)
-- 
-- Maintainer  :  forsyde-dev@ict.kth.se
-- Stability   :  experimental
-- Portability :  portable
--
-- This module contains the data structure and access
-- functions for the memory model.
-----------------------------------------------------------------------------
module ForSyDe.Shallow.Utility.Memory (
  Memory (..), Access (..), 
  MemSize, Adr, newMem, memState, memOutput
  ) where

import ForSyDe.Shallow.Core.Vector
import ForSyDe.Shallow.Core.AbsentExt

type Adr     =  Int
type MemSize =  Int

-- | The data type 'Memory' is modeled as a vector. 
data Memory a = Mem Adr (Vector (AbstExt a)) 
              deriving (Memory a -> Memory a -> Bool
(Memory a -> Memory a -> Bool)
-> (Memory a -> Memory a -> Bool) -> Eq (Memory a)
forall a. Eq a => Memory a -> Memory a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Memory a -> Memory a -> Bool
$c/= :: forall a. Eq a => Memory a -> Memory a -> Bool
== :: Memory a -> Memory a -> Bool
$c== :: forall a. Eq a => Memory a -> Memory a -> Bool
Eq, Int -> Memory a -> ShowS
[Memory a] -> ShowS
Memory a -> String
(Int -> Memory a -> ShowS)
-> (Memory a -> String) -> ([Memory a] -> ShowS) -> Show (Memory a)
forall a. Show a => Int -> Memory a -> ShowS
forall a. Show a => [Memory a] -> ShowS
forall a. Show a => Memory a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Memory a] -> ShowS
$cshowList :: forall a. Show a => [Memory a] -> ShowS
show :: Memory a -> String
$cshow :: forall a. Show a => Memory a -> String
showsPrec :: Int -> Memory a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Memory a -> ShowS
Show)

-- | The data type 'Access' defines two access patterns.
data Access a = Read Adr -- ^ 'Read adr' reads an address from the memory.
              | Write Adr a -- ^ 'Write Adr a' writes a value into an address.
              deriving (Access a -> Access a -> Bool
(Access a -> Access a -> Bool)
-> (Access a -> Access a -> Bool) -> Eq (Access a)
forall a. Eq a => Access a -> Access a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Access a -> Access a -> Bool
$c/= :: forall a. Eq a => Access a -> Access a -> Bool
== :: Access a -> Access a -> Bool
$c== :: forall a. Eq a => Access a -> Access a -> Bool
Eq, Int -> Access a -> ShowS
[Access a] -> ShowS
Access a -> String
(Int -> Access a -> ShowS)
-> (Access a -> String) -> ([Access a] -> ShowS) -> Show (Access a)
forall a. Show a => Int -> Access a -> ShowS
forall a. Show a => [Access a] -> ShowS
forall a. Show a => Access a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Access a] -> ShowS
$cshowList :: forall a. Show a => [Access a] -> ShowS
show :: Access a -> String
$cshow :: forall a. Show a => Access a -> String
showsPrec :: Int -> Access a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Access a -> ShowS
Show)

-- | The function 'newMem' creates a new memory, where the number of
-- entries is given by a parameter.
newMem :: MemSize -> Memory a

-- | The function 'memState' gives the new state of the memory, after
-- an access to a memory. A 'Read' operation leaves the memory
-- unchanged.
memState :: Memory a -> Access a -> Memory a


-- | The function 'memOutput' gives the output of the memory after an
-- access to the memory. A 'Write' operation gives an absent value as
-- output.
memOutput :: Memory a -> Access a -> AbstExt a

-- Implementation

newMem :: Int -> Memory a
newMem Int
size = Int -> Vector (AbstExt a) -> Memory a
forall a. Int -> Vector (AbstExt a) -> Memory a
Mem Int
size (Int -> AbstExt a -> Vector (AbstExt a)
forall a b. (Num a, Eq a) => a -> b -> Vector b
copyV Int
size AbstExt a
forall a. AbstExt a
Abst)

writeMem :: Memory a -> (Int, a) -> Memory a
writeMem :: Memory a -> (Int, a) -> Memory a
writeMem (Mem Int
size Vector (AbstExt a)
vs) (Int
i, a
x) 
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
size Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0  =  Int -> Vector (AbstExt a) -> Memory a
forall a. Int -> Vector (AbstExt a) -> Memory a
Mem Int
size (Vector (AbstExt a) -> Int -> AbstExt a -> Vector (AbstExt a)
forall a. Vector a -> Int -> a -> Vector a
replaceV Vector (AbstExt a)
vs Int
i (a -> AbstExt a
forall a. a -> AbstExt a
abstExt a
x))
  | Bool
otherwise           =  Int -> Vector (AbstExt a) -> Memory a
forall a. Int -> Vector (AbstExt a) -> Memory a
Mem Int
size Vector (AbstExt a)
vs

readMem           :: Memory a -> Int -> (AbstExt a)
readMem :: Memory a -> Int -> AbstExt a
readMem (Mem Int
size Vector (AbstExt a)
vs) Int
i   
   | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
size Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0  =  Vector (AbstExt a)
vs Vector (AbstExt a) -> Int -> AbstExt a
forall a b. Integral a => Vector b -> a -> b
`atV` Int
i
   | Bool
otherwise           =  AbstExt a
forall a. AbstExt a
Abst

memState :: Memory a -> Access a -> Memory a
memState Memory a
mem (Read Int
_)     =  Memory a
mem
memState Memory a
mem (Write Int
i a
x)  =  Memory a -> (Int, a) -> Memory a
forall a. Memory a -> (Int, a) -> Memory a
writeMem Memory a
mem (Int
i, a
x)

memOutput :: Memory a -> Access a -> AbstExt a
memOutput Memory a
mem (Read Int
i)     =  Memory a -> Int -> AbstExt a
forall a. Memory a -> Int -> AbstExt a
readMem Memory a
mem Int
i
memOutput Memory a
_   (Write Int
_ a
_)  =  AbstExt a
forall a. AbstExt a
Abst