-- 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.Read.Read LibRISCV.RegIdx
instance GHC.Enum.Enum LibRISCV.RegIdx
instance GHC.Show.Show LibRISCV.RegIdx
instance GHC.Enum.Bounded LibRISCV.RegIdx
instance GHC.Ix.Ix LibRISCV.RegIdx
instance GHC.Classes.Eq LibRISCV.RegIdx
instance GHC.Classes.Ord 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] :: Decoding v v
[DecodeRS2] :: Decoding v v
[DecodeRD] :: Decoding v v
[DecodeImmI] :: Decoding v v
[DecodeImmS] :: Decoding v v
[DecodeImmB] :: Decoding v v
[DecodeImmU] :: Decoding v v
[DecodeImmJ] :: Decoding v v
[DecodeShamt] :: Decoding v v
[SetInstr] :: v -> Decoding v ()
[WithInstrType] :: Proxy v -> (InstructionType -> b) -> Decoding v b
withInstrType :: forall v_a3xq b_a3xr. forall effs_a5ao. Member (Decoding v_a3xq) effs_a5ao => Proxy v_a3xq -> (InstructionType -> b_a3xr) -> Eff effs_a5ao b_a3xr
setInstr :: forall v_a3xp. forall effs_a5an. Member (Decoding v_a3xp) effs_a5an => v_a3xp -> Eff effs_a5an ()
decodeShamt :: forall v_a3xo. forall effs_a5am. Member (Decoding v_a3xo) effs_a5am => Eff effs_a5am v_a3xo
decodeImmJ :: forall v_a3xn. forall effs_a5al. Member (Decoding v_a3xn) effs_a5al => Eff effs_a5al v_a3xn
decodeImmU :: forall v_a3xm. forall effs_a5ak. Member (Decoding v_a3xm) effs_a5ak => Eff effs_a5ak v_a3xm
decodeImmB :: forall v_a3xl. forall effs_a5aj. Member (Decoding v_a3xl) effs_a5aj => Eff effs_a5aj v_a3xl
decodeImmS :: forall v_a3xk. forall effs_a5ai. Member (Decoding v_a3xk) effs_a5ai => Eff effs_a5ai v_a3xk
decodeImmI :: forall v_a3xj. forall effs_a5ah. Member (Decoding v_a3xj) effs_a5ah => Eff effs_a5ah v_a3xj
decodeRD :: forall v_a3xi. forall effs_a5ag. Member (Decoding v_a3xi) effs_a5ag => Eff effs_a5ag v_a3xi
decodeRS2 :: forall v_a3xh. forall effs_a5af. Member (Decoding v_a3xh) effs_a5af => Eff effs_a5af v_a3xh
decodeRS1 :: forall v_a3xg. forall effs_a5ae. Member (Decoding v_a3xg) effs_a5ae => Eff effs_a5ae v_a3xg


-- | 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. (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] :: Expr v -> ExprEval v Bool
[IsFalse] :: Expr v -> ExprEval v Bool
[Eval] :: Expr v -> ExprEval v v
eval :: forall v_a7YT. forall effs_a800. Member (ExprEval v_a7YT) effs_a800 => Expr v_a7YT -> Eff effs_a800 v_a7YT
defaultEval :: MonadIO m => (v -> Bool, Expr v -> v) -> ExprEval v ~> m

-- | Like <a>ifM</a> but with internal expression evaluation.
ifExprM :: forall v r 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. Member (ExprEval v) r => Expr v -> Eff r () -> Eff r ()

-- | Like <a>unlessM</a> but with internal expression evaluation.
unlessExprM :: forall v r. 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 :: 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_a9PQ. Member LogInstructionFetch effs_a9PQ => InstructionType -> Eff effs_a9PQ ()


-- | 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 :: 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 :: 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 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 :: MArray t a IO => Address -> Word32 -> IO (Memory t a)

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

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

-- | Load a half (16-bit) from memory at the given address.
loadHalf :: (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 :: (MArray t a IO, WordStorage b a) => Memory t a -> Address -> IO b

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

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

-- | Store a word (32-bit) in memory.
storeWord :: (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 :: 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.WordStorage GHC.Word.Word32 GHC.Word.Word8
instance LibRISCV.Effects.Operations.Default.Machine.Memory.WordStorage 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.HalfStorage Data.BitVector.BV 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 a
RegisterFile :: IORef Word32 -> t RegIdx a -> RegisterFile t a

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

-- | The underlying array to store the register values.
[regs] :: RegisterFile t 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 :: MArray t a IO => a -> IO (RegisterFile t a)

-- | Dump the current register file state as a <a>String</a>.
dumpRegs :: 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 :: 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 :: MArray t a IO => RegisterFile t a -> RegIdx -> a -> IO ()

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

-- | Write a new program counter value.
writePC :: 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] :: v -> Operations v v
[WriteRegister] :: v -> v -> Operations v ()
[Load] :: Size -> v -> Operations v v
[Store] :: Size -> v -> v -> Operations v ()
[WritePC] :: v -> Operations v ()
[ReadPC] :: Operations v v
[Exception] :: v -> String -> Operations v ()
[Ecall] :: v -> Operations v ()
[Ebreak] :: v -> Operations v ()
ebreak :: forall v_aaEP. forall effs_aaJJ. Member (Operations v_aaEP) effs_aaJJ => v_aaEP -> Eff effs_aaJJ ()
ecall :: forall v_aaEO. forall effs_aaJI. Member (Operations v_aaEO) effs_aaJI => v_aaEO -> Eff effs_aaJI ()
exception :: forall v_aaEN. forall effs_aaJH. Member (Operations v_aaEN) effs_aaJH => v_aaEN -> String -> Eff effs_aaJH ()
readPC :: forall v_aaEM. forall effs_aaJG. Member (Operations v_aaEM) effs_aaJG => Eff effs_aaJG v_aaEM
writePC :: forall v_aaEL. forall effs_aaJF. Member (Operations v_aaEL) effs_aaJF => v_aaEL -> Eff effs_aaJF ()
store :: forall v_aaEK. forall effs_aaJE. Member (Operations v_aaEK) effs_aaJE => Size -> v_aaEK -> v_aaEK -> Eff effs_aaJE ()
load :: forall v_aaEJ. forall effs_aaJD. Member (Operations v_aaEJ) effs_aaJD => Size -> v_aaEJ -> Eff effs_aaJD v_aaEJ
writeRegister :: forall v_aaEI. forall effs_aaJC. Member (Operations v_aaEI) effs_aaJC => v_aaEI -> v_aaEI -> Eff effs_aaJC ()
readRegister :: forall v_aaEH. forall effs_aaJB. Member (Operations v_aaEH) effs_aaJB => v_aaEH -> Eff effs_aaJB v_aaEH
instance GHC.Show.Show LibRISCV.Effects.Operations.Language.Size
instance GHC.Classes.Eq 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 :: 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 = 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 v r. (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. (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. (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. (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. (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. (Member (ExprEval v) r, Member (Operations v) r) => Expr v -> Eff r ()
