-- A data type to represent algorithms in a way that makes all memory access observable:

--#include "Memories.alfa"

--#include "MemMonads.alfa"

package Algorithms (FM::Set -> Set)(fm::FiniteMaps.FiniteMap FM Natural.Nat)(Word::Set)(RegFile::Set)  where
  open Memories FM fm Word  use  Addr
  open MemMonads  use  MemMonad
  open Monads  use  return,  (>>=),  (>>)
  Code :: Set
    = data Done (regf::RegFile) | Read (addr::Addr) (cont::Word -> Code) | Write (addr::Addr) (word::Word) (cont::Code)
  Alg :: Set
    = Addr -> RegFile -> Code
  runAlg (M::Set -> Set)(mm::MemMonad M Addr Word)(c::Code) :: M RegFile
    = case c of {
        (Done regf) -> return RegFile M mm.monad regf;
        (Read addr cont) -> (>>=) Word RegFile M mm.monad (mm.rd addr) (\(w::Word) -> runAlg M mm (cont w));
        (Write addr word cont) -> (>>) M Tuples.Unit RegFile mm.monad (mm.wr addr word) (runAlg M mm cont);}
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
var "runAlg" hide 1
 #-}