-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A versatile, flexible and executable formal model for the RISC-V architecture.
--   
--   A formal model for the <a>RISC-V</a> <i>Instruction Set
--   Architecture</i> (ISA). Contrary to other Haskell RISC-V ISA models,
--   like <a>GRIFT</a> or <a>riscv-semantics</a>, LibRISCV is specifically
--   tailored to the creation of custom ISA interpreters. To this end, it
--   is designed for flexibility, allowing a versatile representation of
--   instruction operands. For example, instruction operands can be
--   <a>SMT</a> expressions for <a>symbolic execution</a> of binary code.
--   
--   LibRISCV abstractly describes instruction semantics using an
--   <i>Embedded Domain Specific Language</i> (EDSL) with <a>free(r)
--   monads</a>. This Haskell library is intended to build custom
--   interpreters for this free monad. The entry point for this purpose is
--   the <a>LibRISCV.Semantics.buildAST</a> function which obtains the free
--   monad AST based on an entry address. The entry address can be obtained
--   from a provided ELF loader implementation, this <a>Loader</a> module
--   is also responsible for loading binary instructions into a provided
--   memory implementation. Refer to provided example interpreters in the
--   <a>GitHub repository</a> for practical usage instruction. More
--   detailed information on LibRISCV and its concepts is also available in
--   a <a>TFP'23 publication</a>.
@package libriscv
@version 0.1.0.0

module LibRISCV

-- | Representation of a 32-bit addresses for RV32.
type Address = Word32

-- | Align an <a>Address</a> on the next word boundary.
align :: Address -> Address

-- | Type to represent an index for the register file.
--   
--   <pre>
--   &gt;&gt;&gt; toEnum 12 :: RegIdx
--   A2
--   
--   &gt;&gt;&gt; toEnum 31 :: RegIdx
--   T6
--   
--   &gt;&gt;&gt; fromEnum (minBound :: RegIdx)
--   0
--   </pre>
data RegIdx
Zero :: RegIdx
RA :: RegIdx
SP :: RegIdx
GP :: RegIdx
TP :: RegIdx
T0 :: RegIdx
T1 :: RegIdx
T2 :: RegIdx
FP :: RegIdx
S1 :: RegIdx
A0 :: RegIdx
A1 :: RegIdx
A2 :: RegIdx
A3 :: RegIdx
A4 :: RegIdx
A5 :: RegIdx
A6 :: RegIdx
A7 :: RegIdx
S2 :: RegIdx
S3 :: RegIdx
S4 :: RegIdx
S5 :: RegIdx
S6 :: RegIdx
S7 :: RegIdx
S8 :: RegIdx
S9 :: RegIdx
S10 :: RegIdx
S11 :: RegIdx
T3 :: RegIdx
T4 :: RegIdx
T5 :: RegIdx
T6 :: RegIdx
instance GHC.Enum.Bounded LibRISCV.RegIdx
instance GHC.Enum.Enum LibRISCV.RegIdx
instance GHC.Classes.Eq LibRISCV.RegIdx
instance GHC.Ix.Ix LibRISCV.RegIdx
instance GHC.Classes.Ord LibRISCV.RegIdx
instance GHC.Read.Read LibRISCV.RegIdx
instance GHC.Show.Show LibRISCV.RegIdx


-- | Implementation of common command-line arguments using
--   <a>optparse-applicative</a>.
module LibRISCV.CmdLine

-- | <a>BasicArgs</a> can be combined/extended with additional parsers
--   using the <a>&lt;*&gt;</a> applicative operator provided by
--   <a>Options.Applicative</a>.
data BasicArgs
BasicArgs :: Word32 -> Word32 -> Bool -> Bool -> String -> BasicArgs

-- | Start address of the general-purpose memory.
[memAddr] :: BasicArgs -> Word32

-- | Size of the memory in bytes.
[memSize] :: BasicArgs -> Word32

-- | Whether to enable instruction tracing.
[trace] :: BasicArgs -> Bool

-- | Whether to print all register values at the end.
[putRegs] :: BasicArgs -> Bool

-- | Path to ELf file which should be executed.
[file] :: BasicArgs -> String

-- | <a>Options.Applicative</a> parser for <a>BasicArgs</a>.
basicArgs :: Parser BasicArgs


-- | Implements an effect for instruction decoding. Specifically, the
--   effect is only used to describe obtaining of instruction operands. The
--   instruction opcode is determined seperatly using code generated from
--   the existing <a>riscv-opcodes</a> tool. The decoding effect is
--   stateful and operates on a current instruction word specified via
--   <a>setInstr</a>, thereby avoiding the need to pass the current
--   instruction word to every decoding function.
module LibRISCV.Effects.Decoding.Language
data Decoding v r
[DecodeRS1] :: forall v. Decoding v v
[DecodeRS2] :: forall v. Decoding v v
[DecodeRD] :: forall v. Decoding v v
[DecodeImmI] :: forall v. Decoding v v
[DecodeImmS] :: forall v. Decoding v v
[DecodeImmB] :: forall v. Decoding v v
[DecodeImmU] :: forall v. Decoding v v
[DecodeImmJ] :: forall v. Decoding v v
[DecodeShamt] :: forall v. Decoding v v
[SetInstr] :: forall v. v -> Decoding v ()
[WithInstrType] :: forall v r. Proxy v -> (InstructionType -> r) -> Decoding v r
decodeRS1 :: forall v (effs :: [Type -> Type]). Member (Decoding v) effs => Eff effs v
decodeRS2 :: forall v (effs :: [Type -> Type]). Member (Decoding v) effs => Eff effs v
decodeRD :: forall v (effs :: [Type -> Type]). Member (Decoding v) effs => Eff effs v
decodeImmI :: forall v (effs :: [Type -> Type]). Member (Decoding v) effs => Eff effs v
decodeImmS :: forall v (effs :: [Type -> Type]). Member (Decoding v) effs => Eff effs v
decodeImmB :: forall v (effs :: [Type -> Type]). Member (Decoding v) effs => Eff effs v
decodeImmU :: forall v (effs :: [Type -> Type]). Member (Decoding v) effs => Eff effs v
decodeImmJ :: forall v (effs :: [Type -> Type]). Member (Decoding v) effs => Eff effs v
decodeShamt :: forall v (effs :: [Type -> Type]). Member (Decoding v) effs => Eff effs v
setInstr :: forall v (effs :: [Type -> Type]). Member (Decoding v) effs => v -> Eff effs ()
withInstrType :: forall v b (effs :: [Type -> Type]). Member (Decoding v) effs => Proxy v -> (InstructionType -> b) -> Eff effs b


-- | Provides the default (concrete) interpretation for the decoding
--   effect. This implementation assumes that the <a>Decodable</a> type
--   class can be implemented for the underlying type parameter, that is,
--   it must be possible to convert the type to a fixed-width concrete
--   integer.
module LibRISCV.Effects.Decoding.Default.Interpreter

-- | Decoder state used to implement the stateful <a>SetInstr</a>
--   constructor of the <a>Decoding</a> effect.
type DecoderState = IORef Word32

-- | Type class used to perform conversion from/to a fixed-with concrete
--   integer.
class Decodable a

-- | Convert from a fixed-with integer to the underlying value type of the
--   interpreter.
fromWord :: Decodable a => Word32 -> a

-- | Convert from the underlying value type to a fixed-with integer.
toWord :: Decodable a => a -> Word32

-- | Concrete implementation of the decoding effect.
defaultDecoding :: forall v (m :: Type -> Type). (Decodable v, MonadIO m) => DecoderState -> Decoding v ~> m
instance LibRISCV.Effects.Decoding.Default.Interpreter.Decodable Data.BitVector.BV


-- | Defines the expression abstraction to express arithmetic and logic
--   operations within the formal description of RISC-V instructions. The
--   abstraction is just a non-monadic algebraic data type called
--   <a>Expr</a>. In addition to the the data type definition, this module
--   also provides several smart constructors for utilzing the expression
--   lanuage, these are generated using template-haskell.
module LibRISCV.Effects.Expressions.Expr
data Expr a

-- | Create a new <a>Expr</a> from a given immediate value.
FromImm :: a -> Expr a

-- | Create an expression from a concrete <a>Integer</a>, treating it as a
--   fixed-width two's complement value of the size (in bits) specified by
--   the first argument to the constructor.
FromInt :: Int -> Integer -> Expr a

-- | Zero extend an expression by adding the given amount of bits to it,
--   for example, an 8-bit value can be zero-extended to 32-bit by passing
--   24 as the first argument.
ZExt :: Int -> Expr a -> Expr a

-- | Same as <a>ZExt</a> but performs sign-extension instead of
--   zero-extension.
SExt :: Int -> Expr a -> Expr a

-- | Extract a specified amount of bits from an expression. The first
--   argument specifies the first bit which should be extracted, the second
--   specifies the amount of bits to extract.
Extract :: Int -> Int -> Expr a -> Expr a
Add :: Expr a -> Expr a -> Expr a
Sub :: Expr a -> Expr a -> Expr a
Eq :: Expr a -> Expr a -> Expr a
Slt :: Expr a -> Expr a -> Expr a
Sge :: Expr a -> Expr a -> Expr a
Ult :: Expr a -> Expr a -> Expr a
Uge :: Expr a -> Expr a -> Expr a
And :: Expr a -> Expr a -> Expr a
Or :: Expr a -> Expr a -> Expr a
Xor :: Expr a -> Expr a -> Expr a
LShl :: Expr a -> Expr a -> Expr a
LShr :: Expr a -> Expr a -> Expr a
AShr :: Expr a -> Expr a -> Expr a
Mul :: Expr a -> Expr a -> Expr a
UDiv :: Expr a -> Expr a -> Expr a
SDiv :: Expr a -> Expr a -> Expr a
URem :: Expr a -> Expr a -> Expr a
SRem :: Expr a -> Expr a -> Expr a
xor :: a -> a -> Expr a

-- | Extract shamt value from an expression (lower 5 bits).
regShamt :: Int -> Expr a -> Expr a
and :: a -> a -> Expr a
or :: a -> a -> Expr a
mul :: a -> a -> Expr a
eq :: a -> a -> Expr a
ashr :: a -> a -> Expr a
sge :: a -> a -> Expr a
slt :: a -> a -> Expr a
sdiv :: a -> a -> Expr a
srem :: a -> a -> Expr a
zextImm :: Int -> a -> Expr a
sextImm :: Int -> a -> Expr a
addImm :: a -> a -> Expr a
subImm :: a -> a -> Expr a
eqImm :: a -> a -> Expr a
sltImm :: a -> a -> Expr a
sgeImm :: a -> a -> Expr a
ultImm :: a -> a -> Expr a
ugeImm :: a -> a -> Expr a
andImm :: a -> a -> Expr a
orImm :: a -> a -> Expr a
xorImm :: a -> a -> Expr a
lshlImm :: a -> a -> Expr a
lshrImm :: a -> a -> Expr a
ashrImm :: a -> a -> Expr a
mulImm :: a -> a -> Expr a
udivImm :: a -> a -> Expr a
sdivImm :: a -> a -> Expr a
uremImm :: a -> a -> Expr a
sremImm :: a -> a -> Expr a
add :: a -> a -> Expr a
sub :: a -> a -> Expr a
ult :: a -> a -> Expr a
uge :: a -> a -> Expr a
lshl :: a -> a -> Expr a
lshr :: a -> a -> Expr a
udiv :: a -> a -> Expr a
urem :: a -> a -> Expr a


-- | Implements an effect for <i>evaluation</i> of the <a>Expr</a>
--   abstraction.
module LibRISCV.Effects.Expressions.Language
data ExprEval v r
[IsTrue] :: forall v. Expr v -> ExprEval v Bool
[IsFalse] :: forall v. Expr v -> ExprEval v Bool
[Eval] :: forall v. Expr v -> ExprEval v v
eval :: forall v (effs :: [Type -> Type]). Member (ExprEval v) effs => Expr v -> Eff effs v
defaultEval :: forall (m :: Type -> Type) v. MonadIO m => (v -> Bool, Expr v -> v) -> ExprEval v ~> m

-- | Like <a>ifM</a> but with internal expression evaluation.
ifExprM :: forall v (r :: [Type -> Type]) v'. Member (ExprEval v) r => Expr v -> Eff r v' -> Eff r v' -> Eff r v'

-- | Like <a>whenM</a> but with internal expression evaluation.
whenExprM :: forall v (r :: [Type -> Type]). Member (ExprEval v) r => Expr v -> Eff r () -> Eff r ()

-- | Like <a>unlessM</a> but with internal expression evaluation.
unlessExprM :: forall v (r :: [Type -> Type]). Member (ExprEval v) r => Expr v -> Eff r () -> Eff r ()


-- | Provides the default (concrete) evaluation of the expression
--   abstraction.
module LibRISCV.Effects.Expressions.Default.Interpreter

-- | Evaluate an <a>Expr</a> abstraction which encapsulates a concrete
--   <a>BV</a>.
evalE :: Expr BV -> BV

-- | Concrete implementation of the <a>ExprEval</a> effect.
defaultEval :: forall (m :: Type -> Type) v. MonadIO m => (v -> Bool, Expr v -> v) -> ExprEval v ~> m


-- | Implements the logging effect for instruction tracing. This effect is
--   primarly intended to be used for debugging.
module LibRISCV.Effects.Logging.Language
data LogInstructionFetch r
[LogFetched] :: InstructionType -> LogInstructionFetch ()
logFetched :: forall (effs :: [Type -> Type]). Member LogInstructionFetch effs => InstructionType -> Eff effs ()


-- | Provides the default interpretation for the logging effect.
module LibRISCV.Effects.Logging.Default.Interpreter

-- | The default effectful logging interpreter which writes the
--   <a>InstructionType</a> of a fetched instruction to standard output,
--   before executing it. This is particularly useful for debugging but is
--   quite verbose in the common case.
defaultLogging :: forall (m :: Type -> Type). MonadIO m => LogInstructionFetch ~> m

-- | A stub implementation of an effectful interpreter which ignores any
--   logging effects entirely. Should be used when no debugging output is
--   desired.
noLogging :: forall (m :: Type -> Type). Monad m => LogInstructionFetch ~> m


-- | Provides an implementatio of a byte-addressable memory, intended for
--   internal usage in interpreters for the <a>Operations</a> effect.
module LibRISCV.Effects.Operations.Default.Machine.Memory

-- | Representation of a byte-addressable memory. The type is parameterized
--   over an array implementation (such as <a>IOUArray</a>) and a generic
--   value type (used to represent instruction operands).
data Memory (t :: Type -> Type -> Type) a

-- | Since the memory is byte-addressable it requires converting values of
--   a larger size to bytes. This type class is responsible for a
--   conversion of 16-bit values (halfs). That is, it converts halfs to
--   bytes (and vice versa) in little endian.
class HalfStorage halfType byteType

-- | Convert a list of two bytes to a single half.
toHalf :: HalfStorage halfType byteType => [byteType] -> halfType

-- | Convert a single half to a list of two bytes.
halfToBytes :: HalfStorage halfType byteType => halfType -> [byteType]

-- | Similar to <a>HalfStorage</a> but handles conversion of 32-bit values
--   (words).
class WordStorage wordType byteType

-- | Convert a list of four bytes to a single word.
toWord :: WordStorage wordType byteType => [byteType] -> wordType

-- | Convert a single word to a list of four bytes.
wordToBytes :: WordStorage wordType byteType => wordType -> [byteType]

-- | Create a new memory of the given size starting at the given address.
mkMemory :: forall (t :: Type -> Type -> Type) a. MArray t a IO => Address -> Word32 -> IO (Memory t a)

-- | Returns the size of the memory in bytes.
memSize :: forall (t :: Type -> Type -> Type) a. MArray t a IO => Memory t a -> IO Word32

-- | Load a single byte from memory at the given address.
loadByte :: forall (t :: Type -> Type -> Type) a. MArray t a IO => Memory t a -> Address -> IO a

-- | Load a half (16-bit) from memory at the given address.
loadHalf :: forall (t :: Type -> Type -> Type) a b. (MArray t a IO, HalfStorage b a) => Memory t a -> Address -> IO b

-- | Load a word (32-bit) from memory at the given address.
loadWord :: forall (t :: Type -> Type -> Type) a b. (MArray t a IO, WordStorage b a) => Memory t a -> Address -> IO b

-- | Store a single byte in memory.
storeByte :: forall (t :: Type -> Type -> Type) a. MArray t a IO => Memory t a -> Address -> a -> IO ()

-- | Store a half (16-bit) in memory.
storeHalf :: forall (t :: Type -> Type -> Type) a b. (MArray t a IO, HalfStorage b a) => Memory t a -> Address -> b -> IO ()

-- | Store a word (32-bit) in memory.
storeWord :: forall (t :: Type -> Type -> Type) a b. (MArray t a IO, WordStorage b a) => Memory t a -> Address -> b -> IO ()

-- | Write a <a>ByteString</a> to memory in little endian byteorder.
--   Expects a function to convert single bytes (<a>Word8</a>) to the
--   chosen value representation, a <a>Memory</a>, as well the
--   <a>Address</a> where the string should be stored and the
--   <a>ByteString</a> itself.
storeByteString :: forall (t :: Type -> Type -> Type) a. MArray t a IO => (Word8 -> a) -> Memory t a -> Address -> ByteString -> IO ()

-- | Converts a list of bytes to a <a>Word32</a> in little endian.
mkWord :: [Word8] -> Word32

-- | Split a 32-bit word into four octets in little endian.
mkBytes :: Word32 -> [Word8]
instance LibRISCV.Effects.Operations.Default.Machine.Memory.HalfStorage Data.BitVector.BV GHC.Word.Word8
instance LibRISCV.Effects.Operations.Default.Machine.Memory.HalfStorage GHC.Word.Word16 GHC.Word.Word8
instance LibRISCV.Effects.Operations.Default.Machine.Memory.WordStorage Data.BitVector.BV GHC.Word.Word8
instance LibRISCV.Effects.Operations.Default.Machine.Memory.WordStorage GHC.Word.Word32 GHC.Word.Word8


-- | Provides a polymorphic implementation of a register file. This module
--   is intended to be used internally by interpreters for the
--   <a>Operations</a> effect. This register file implementation also
--   provides facilities for storing a concrete program counter.
module LibRISCV.Effects.Operations.Default.Machine.Register

-- | Register file addressed by <a>RegIdx</a>. The type is parameterized
--   over an array implementation (such as <a>IOUArray</a>) and a generic
--   value type (used to represent instruction operands).
data RegisterFile (t :: Type -> Type -> Type) a
RegisterFile :: IORef Word32 -> t RegIdx a -> RegisterFile (t :: Type -> Type -> Type) a

-- | The current program counter (always concrete in this implementation).
[pc] :: RegisterFile (t :: Type -> Type -> Type) a -> IORef Word32

-- | The underlying array to store the register values.
[regs] :: RegisterFile (t :: Type -> Type -> Type) a -> t RegIdx a

-- | Create a new register file, initializing all registers with the given
--   default value. This value <i>must</i> represent the zero value in the
--   chosen value type.
mkRegFile :: forall (t :: Type -> Type -> Type) a. MArray t a IO => a -> IO (RegisterFile t a)

-- | Dump the current register file state as a <a>String</a>.
dumpRegs :: forall (t :: Type -> Type -> Type) a. MArray t a IO => (a -> ShowS) -> RegisterFile t a -> IO String

-- | Read register value at given register index. For the <a>Zero</a>
--   register index, the zero/default value (as passed to <a>mkRegFile</a>
--   is always returned.
readRegister :: forall (t :: Type -> Type -> Type) a. MArray t a IO => RegisterFile t a -> RegIdx -> IO a

-- | Write register at given register index. Writes to the <a>Zero</a>
--   register are ignored.
writeRegister :: forall (t :: Type -> Type -> Type) a. MArray t a IO => RegisterFile t a -> RegIdx -> a -> IO ()

-- | Returs the current program counter value.
readPC :: forall (t :: Type -> Type -> Type) a. RegisterFile t a -> IO Word32

-- | Write a new program counter value.
writePC :: forall (t :: Type -> Type -> Type) a. RegisterFile t a -> Word32 -> IO ()


-- | Implements an effect for interactions with the architectural state,
--   upon which instructions are executed (register file, memory, program
--   counter, etc.).
module LibRISCV.Effects.Operations.Language

-- | Abstraction for expressing a 8-, 16-, or 32-bit size.
data Size
Byte :: Size
Half :: Size
Word :: Size

-- | Returns the size in bits (either 8, 16, or 32).
bitSize :: Size -> Int
data Operations v r
[ReadRegister] :: forall v. v -> Operations v v
[WriteRegister] :: forall v. v -> v -> Operations v ()
[Load] :: forall v. Size -> v -> Operations v v
[Store] :: forall v. Size -> v -> v -> Operations v ()
[WritePC] :: forall v. v -> Operations v ()
[ReadPC] :: forall v. Operations v v
[Exception] :: forall v. v -> String -> Operations v ()
[Ecall] :: forall v. v -> Operations v ()
[Ebreak] :: forall v. v -> Operations v ()
readRegister :: forall v (effs :: [Type -> Type]). Member (Operations v) effs => v -> Eff effs v
writeRegister :: forall v (effs :: [Type -> Type]). Member (Operations v) effs => v -> v -> Eff effs ()
load :: forall v (effs :: [Type -> Type]). Member (Operations v) effs => Size -> v -> Eff effs v
store :: forall v (effs :: [Type -> Type]). Member (Operations v) effs => Size -> v -> v -> Eff effs ()
writePC :: forall v (effs :: [Type -> Type]). Member (Operations v) effs => v -> Eff effs ()
readPC :: forall v (effs :: [Type -> Type]). Member (Operations v) effs => Eff effs v
exception :: forall v (effs :: [Type -> Type]). Member (Operations v) effs => v -> String -> Eff effs ()
ecall :: forall v (effs :: [Type -> Type]). Member (Operations v) effs => v -> Eff effs ()
ebreak :: forall v (effs :: [Type -> Type]). Member (Operations v) effs => v -> Eff effs ()
instance GHC.Classes.Eq LibRISCV.Effects.Operations.Language.Size
instance GHC.Show.Show LibRISCV.Effects.Operations.Language.Size


-- | Implements the default (concrete) interpreter for the
--   <a>Operations</a> effect.
module LibRISCV.Effects.Operations.Default.Interpreter

-- | Representation of the concrete architectural state of the interpreter.
data ArchState
ArchState :: RegisterFile IOUArray Int32 -> Memory IOUArray Word8 -> ArchState

-- | Register file implementation of the architectural state.
[getReg] :: ArchState -> RegisterFile IOUArray Int32

-- | Memory implementation of the architectural state.
[getMem] :: ArchState -> Memory IOUArray Word8

-- | Create a new <a>ArchState</a> based on a memory start address and a
--   memory size.
mkArchState :: Address -> Word32 -> IO ArchState

-- | Write a textual representation of the <a>ArchState</a> to standard
--   output.
dumpState :: ArchState -> IO ()

-- | Implements concrete interpretation of the <a>Operations</a> effect
--   based on a <a>BV</a> value representation.
defaultInstructions :: forall (m :: Type -> Type). MonadIO m => ArchState -> Operations BV ~> m


-- | An implementation of an <i>Executable Loadable Format</i> (ELF)
--   loader. The module is responsible for loading instructions into a
--   provided memory implementation and obtaining the entry point for the
--   executable.
module LibRISCV.Loader

-- | Read an ELF from a given <a>FilePath</a>.
readElf :: FilePath -> IO Elf

-- | Load a <a>ByteString</a> into memory at a given address.
type LoadFunc (m :: Type -> Type) = Address -> ByteString -> m ()

-- | Load all loadable segments of an ELF file into memory. An addition to
--   the <a>Elf</a> file, it requires an implementation of a
--   <a>LoadFunc</a> which is responsible for converting a
--   <a>ByteString</a> to the internal value representation.
loadElf :: Monad m => Elf -> LoadFunc m -> m ()

-- | Return the entry point from the ELF header.
startAddr :: MonadCatch m => Elf -> m Word32


-- | Functions for interacting with the free monad abstraction used to
--   formally describe the semantics of RISC-V instructions.
module LibRISCV.Semantics

-- | Obtain the free monad AST for a program loaded into memory, e.g.
--   through the provided ELF <a>Loader</a> implementation. The function
--   takes one argument which corresponds to an address in memory at which
--   program execution will start. An instruction word will be loaded from
--   this address, decoded, and executed.
buildAST :: forall (w :: Nat) v (r :: [Type -> Type]). (KnownNat w, Member (Operations v) r, Member LogInstructionFetch r, Member (Decoding v) r, Member (ExprEval v) r) => v -> Eff r ()

-- | Write to a register in the register file. The function takes a
--   register index and a value which should be written to the register
--   (represented as an <a>Expr</a>). This function is primarly useful to
--   initialize special registers, e.g. setting the stack pointer to a
--   meaningful value at the very beginning of the free monad AST.
writeRegister :: forall v (r :: [Type -> Type]). (Member (ExprEval v) r, Member (Operations v) r) => v -> Expr v -> Eff r ()

-- | Obtain the current value for a register in the register file. The
--   functions takes a register index (encapsulated in an <a>Expr</a>) and
--   returns the value of this register.
readRegister :: forall v (r :: [Type -> Type]). (Member (ExprEval v) r, Member (Operations v) r) => Expr v -> Eff r v

-- | Load a fixed-size value from memory. The function takes two arguments:
--   The <a>Size</a> of the value to load and the start address of the
--   value in memory (represented as an <a>Expr</a>).
load :: forall v (r :: [Type -> Type]). (Member (ExprEval v) r, Member (Operations v) r) => Size -> Expr v -> Eff r v

-- | Store a fixed-size value in memory. The arguments are: The <a>Size</a>
--   of the value, the start address where the value should be stored, and
--   the value itself. The latter two are encapuslated in the <a>Expr</a>
--   abstraction.
store :: forall v (r :: [Type -> Type]). (Member (ExprEval v) r, Member (Operations v) r) => Size -> Expr v -> Expr v -> Eff r ()

-- | Change the current value of the <i>Program Counter</i> (PC). The new
--   value is the only function argument and is represented as an
--   <a>Expr</a>.
writePC :: forall v (r :: [Type -> Type]). (Member (ExprEval v) r, Member (Operations v) r) => Expr v -> Eff r ()
