module ChipModel where
import Monad(liftM)
import State
import qualified FunFM as FM
import Algorithms
import Memories
import MemMonads
import Protected
import Nat
import MemoryState

type Channel = Nat
type Packet = (Channel,Data)
type Regs = FM.FM RegFile
type ChipState = (Memory,Regs)

type Algs = Channel -> Alg

chip :: Algs -> ChipState -> [Packet] -> [Packet]
chip algs state ps = fst (runS (manyPackets algs ps) state)

{-P: {-#cert:Separation#-}  {-#cert:ISaySeparation#-}
assert Separation =
   All algs . All ch . All state . All ps . 
   {pick ch (chip algs state ps)} === {chip algs state (pick ch ps)}

pick :: Channel -> [Packet] -> [Packet]
pick ch = filter (sameChannel ch)

sameChannel :: Channel -> Packet -> Bool
sameChannel ch p = fst p == ch
-}

manyPackets :: Algs -> [Packet] -> StateM ChipState [Packet]
manyPackets algs = mapM (onePacket algs)

onePacket :: Algs -> Packet ->  StateM ChipState Packet
onePacket algs (chan,ws) =
  do regfile <- liftM (\regs->FM.lookup regs chan) (inSnd load)
     (ws',regfile') <- inFst (doPacket (algs chan) ws regfile)
     finishPacket chan ws' regfile'

doPacket :: Alg -> Data -> RegFile -> StateM Memory (Data,RegFile)
doPacket alg ws regf = 
  do r <- mallocM (len ws)
     update (storeList (base r) ws)
     let code = alg (base r) regf
     doPacket2 code r regf

doPacket2 :: Code -> Range -> RegFile -> StateM Memory (Data,RegFile)
doPacket2 code r regf = saferun >>= doPacket3 r
  where
    saferun = runProtected regf (inRange r) run
    run = runAlg code

doPacket3 :: Range -> RegFile -> StateM Memory (Data,RegFile)
doPacket3 r regf' =
  do ws <- liftM (loadRange r) load
     freeM r
     return (ws,regf')

finishPacket :: Channel -> Data -> RegFile -> StateM ChipState Packet
finishPacket ch ws regf =
  do inSnd (update (FM.update ch regf))
     return (ch,ws)

initRegs :: Regs
initRegs = FM.empty initRegFile

initChip :: ChipState
initChip = (initMem,initRegs)

{-P:
property StateIndependent =
  {| m | All s1 . All s2 . {fst (runS m s1)} === {fst (runS m s2)} |}

property GoodAlg =
  {| alg | All ws . All regf . StateIndependent {doPacket alg ws regf} |}

regfile :: Channel -> ChipState -> RegFile
regfile ch state = FM.lookup (snd state) ch

property Invariant =
  {| state1, state2, ch | {regfile ch state1} === {regfile ch state2} |}

assert CondSeparation = {-#cert:CondSeparation#-} {-#cert:ISayCondSeparation#-} 
   All algs . All ch . All state1 . All state2 . All ps . 
   GoodAlg {algs ch} ==>
   Invariant state1 state2 ch ==>
   {pick ch (chip algs state1 ps)} === {chip algs state2 (pick ch ps)}

{-#cert:AllGoodAlg#-} {-#cert:ISayAllGoodAlg#-}
assert AllGoodAlg = All alg . GoodAlg alg

{-#cert:SameState#-} {-#cert:ISaySameState#-}
assert SameState = All state . All ch . Invariant state state ch
-}