<div dir="ltr"><div><div>Hi all,<br><br></div>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.<br><br></div>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.<br><br><div>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).<br><br></div><div>Concretely, I have a set up like this:<br><br></div><div>Datatype`cell = <| ... ; program: prog; ... |>`; (* prog is from CakeML's astTheory *)<br><br></div><div>Define`next_state cell =<br></div><div>  let encoded = encode cell.data in<br></div><div></div><div><br>  let output = run_eval_prog ... cell.time_limit ... encoded ... cell.program in<br>  (* run_eval_prog is from CakeML's interpTheory *)<br></div><div><br>  let decoded = decode output in<br></div><div><br>  <| ... := decoded.data; program := decoded.program; ... |>`;<br><br><br></div><div>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.<br><br></div><div>My questions for the list are:<br><br></div><div>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?<br><br></div><div>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?<br><br></div><div>Thanks for reading. My guess is I'll have to try a few approaches, but I'd appreciate any comments.<br></div><div>Ramana<br></div></div>