[CakeML] Embedding a CakeML interpreter in a HOL program

[Ramana Kumar]

Hi all,

I have an application in which I want to formalise a system that includes,
as a subsystem, a mechanism for running CakeML programs that take some
input data and produce some output data. The system is a cellular automaton
game in which cells may contain CakeML programs (amongst other things), and
the next state of the cell can depend on the output of the program when it
is given information about the current state of the cell as input.

I am writing the next-state function for cells in this game as a function
in HOL (i.e., a shallowly embedded algorithm). I intend to keep this
function within the obviously-computable subset of HOL, so that it may
later be extracted to CakeML or elsewhere.

The input/output data for the programs is first-order, but I would rather
avoid serialising it as bytes if I can get away with it (and instead just
use CakeML values).

Concretely, I have a set up like this:

Datatype`cell = <| ... ; program: prog; ... |>`; (* prog is from CakeML's
astTheory *)

Define`next_state cell =
  let encoded = encode cell.data in

  let output = run_eval_prog ... cell.time_limit ... encoded ...
cell.program in
  (* run_eval_prog is from CakeML's interpTheory *)

  let decoded = decode output in

  <| ... := decoded.data; program := decoded.program; ... |>`;


As can be seen above, in my shallow embedding I have CakeML ASTs as part of
the cell state, and I also want the CakeML program to return a new AST to
be used for the next state of the cell. So, I at least need the entire
"prog" type to be translated into CakeML and to be available in the
environment passed to the interpreter (run_eval_prog). Additionally, there
are some other datatypes in my particular setup that I would want available
for manipulation by the programs in the cells. I hope to use CakeML's
translator to automate as much as I can.

My questions for the list are:

What should be the (internal) type of cell.program? In my shallow embedding
its type is prog. But the type in CakeML could be a function, data -> data
* prog, or it could be of type data -> unit and run in an environment where
it expects to set a reference of type (data * prog) ref. Or it could be of
type unit and simply generate an io_trace that reads and writes the data I
need (including serialisation to/from bytes). Which of these is likely to
be easier to work with? Are there other alternatives?

How can I write the encode and decode functions above to play nicely with
CakeML's translator? In some cases I'm going to want to generate the
contents of cell.program using the translator, which means I'll need my
encode and decode functions to map into/out of exactly the deeply embedded
datatypes as generated by the translator. Is there any nice way to set this
up?

Thanks for reading. My guess is I'll have to try a few approaches, but I'd
appreciate any comments.
Ramana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20150917/bdd439fc/attachment.html>