C snapshot with user-definable monad operations

[aa755]

Is there a way to obtain a C snapshot of the Arm model where the implementation of the monad in the POL2019 paper (sec 4.2, copied below) is user-definable, instead of hard coding the processor state as a struct and specific implementations the monad operations?

type monad 'r 'a 'e =
| Done of 'a
| Read_mem of read_kind * address * nat * (list mem_byte -> monad 'r 'a 'e)
| Write_ea of write_kind * address * nat * monad 'r 'a 'e
| Write_memv of list mem_byte * (bool -> monad 'r 'a 'e)
...
| Barrier of barrier_kind * monad 'r 'a 'e
| Read_reg of register_name * ('r -> monad 'r 'a 'e)
| Write_reg of register_name * 'r * monad 'r 'a 'e
| Undefined of (bool -> monad 'r 'a 'e)
| Exception of 'e (* Exception thrown *)

Doing so would make the C snapshot more generally usable.