-- This is the main file for the chip model

--#include "State.alfa"

--#include "Alfa/Natural.alfa"

--#include "Memories.alfa"

--#include "Algorithms.alfa"

--#include "Protected.alfa"

package ChipModel
  (FM::Set -> Set)
  (fm::FiniteMaps.FiniteMap FM Natural.Nat)
  (Word::Set)
  (RegFile::Set)
 where
  open Tuples  use  Pair,  Unit,  unit,  pair,  fst,  snd,  swap,  curry
  open Types  use  Bool,  Maybe
  open Lists  use  List,  length
  open Monads
   use  Monad,  return,  (>>=),  (>>),  liftM,  ap,  liftM2,  sequence_,
        sequence,  mapM
  open State
   use  StateM,  inst,  load,  store,  update,  inFst,  inSnd,  uncurry
  open Memories FM fm Word
   use  Addr,  Memory,  Data,  storeList,  loadRange,  empty,  nullPtr,
        lookupM,  updateM,  Range,  malloc,  free
  public open Algorithms FM fm Word RegFile  use  Code,  Alg,  runAlg
  open MemMonads  use  MemMonad
  open Protected
   use  maybe,  EnvEx,  Protect,  protect,  mmprot,  runProtected
  open Natural  use  Nat,  natLt
  Channel = Nat
  Packet = Pair Channel Data
  Regs = FM RegFile
  ChipState = Pair Memory Regs
  mm :: MemMonad (StateM Memory) Addr Word
    = struct {
        monad = inst Memory;
        rd =
          \(a::Addr) ->
          liftM
            Memory
            Word
            (StateM Memory)
            monad
            (\(m::Memory) -> lookupM m a)
            (load Memory);
        wr = \(a::Addr) -> \(w::Word) -> update Memory (updateM a w);}
  mallocM (n::Nat) :: StateM Memory Range
    = malloc n
  freeM (r::Range) :: StateM Memory Unit
    = \(m::Memory) -> Pair@_ unit (free r m)
  mmp :: MemMonad (Protect (StateM Memory) Addr) Addr Word
    = mmprot (StateM Memory) Addr Word mm
  Algs :: Set
    = Channel -> Alg
  finishPacket (ch::Channel)(ws::Data)(regf::RegFile)
    :: StateM ChipState Packet
    = (>>)
        (StateM ChipState)
        Unit
        Packet
        (inst ChipState)
        (inSnd Memory Regs Unit (update Regs (fm.update RegFile ch regf)))
        (return Packet (StateM ChipState) (inst ChipState) (Pair@_ ch ws))
  doPacket3 (r::Range)(regf'::RegFile)
    :: StateM Memory (Pair Data RegFile)
    = (>>=)
        (List Word)
        (Pair Data RegFile)
        (StateM Memory)
        (State.inst Memory)
        (liftM
           Memory
           (List Word)
           (StateM Memory)
           (State.inst Memory)
           (loadRange r)
           (load Memory))
        (\(ws'::List Word) ->
         return
           (Pair Data RegFile)
           (StateM Memory)
           (State.inst Memory)
           (Pair@_ ws' regf'))
  doPacket2 (code::Code)(r::Range)(regf::RegFile)
    :: StateM Memory (Pair Data RegFile)
    = let run :: Protect (StateM Memory) Addr RegFile
            = runAlg (Protect (StateM Memory) Addr) mmp code
          saferun :: StateM Memory RegFile
            = runProtected
                (StateM Memory)
                Addr
                Word
                RegFile
                mm
                regf
                (\(a::Addr) -> natLt a r.base)
                run
      in  (>>=)
            RegFile
            (Pair Data RegFile)
            (StateM Memory)
            (inst Memory)
            saferun
            (doPacket3 r)
  doPacket1 (code::Code)(ws::Data)(regf::RegFile)(r::Range)
    :: StateM Memory (Pair Data RegFile)
    = (>>)
        (StateM Memory)
        Unit
        (Pair Data RegFile)
        (inst Memory)
        (update Memory (storeList r.base ws))
        (doPacket2 code r regf)
  doPacket (alg::Alg)(ws::Data)(regf::RegFile)
    :: StateM Memory (Pair Data RegFile)
    = (>>=)
        Range
        (Pair Data RegFile)
        (\(A::Set) -> (h::Memory) -> Tuples.Pair A Memory)
        (inst Memory)
        (mallocM (length Word ws))
        (\(r::Range) -> doPacket1 (alg r.base regf) ws regf r)
  onePacket (algs::Algs)(chan::Channel)(ws::Data)
    :: StateM ChipState Packet
    = (>>=)
        RegFile
        Packet
        (StateM ChipState)
        (inst ChipState)
        (liftM
           Regs
           RegFile
           (StateM ChipState)
           (inst ChipState)
           (\(regs::Regs) -> fm.lookup RegFile regs chan)
           (inSnd Memory Regs Regs (load Regs)))
        (\(regfile::RegFile) ->
         (>>=)
           (Pair Data RegFile)
           Packet
           (StateM ChipState)
           (inst ChipState)
           (inFst
              Memory
              Regs
              (Pair Data RegFile)
              (doPacket (algs chan) ws regfile))
           (uncurry Data RegFile (StateM ChipState Packet) (finishPacket chan)))
  manyPackets (algs::Algs)(ps::List Packet)
    :: StateM ChipState (List Packet)
    = mapM
        Packet
        Packet
        (\(A::Set) -> (h::ChipState) -> Pair A ChipState)
        (inst ChipState)
        (uncurry
           Channel
           Data
           ((h::ChipState) -> Pair Packet ChipState)
           (onePacket algs))
        ps
  abstract initChip :: ChipState
    = Pair@_ (empty ?) ?
  chip (algs::Algs)(state::ChipState)(ps::List Packet) :: List Packet
    = fst (List Packet) ChipState (manyPackets algs ps state)
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
 #-}