More work on ocaml backend.

Works for basic examples with arbitrary register types, so for example we can compile:

val extern string -> unit effect pure print = "print_endline"

val unit -> string effect pure hello_world

function hello_world () = {
  return "Hello, World!";
  "Unreachable"
}

val unit -> unit effect {wreg, rreg} main

register string REG

function main () = {
  REG := "Hello, Sail!";
  print(REG);
  REG := hello_world ();
  print(REG);
  return ()
}

into

open Sail_lib;;

let zhello_world () = with_return (fun r ->
  begin r.return "Hello, World!"; "Unreachable" end);;

let zREG : (string) ref = ref (undefined_string ());;

let zmain () = with_return (fun r ->
  begin
    zREG := "Hello, Sail!";
    print_endline !zREG;
    zREG := zhello_world ();
    print_endline !zREG;
    r.return ()
  end);;

let initialize_registers () = with_return (fun r -> zREG := undefined_string ());;

with the arbitrary register types and early returns being handled
appropriately, given a suitable implementation for Sail_lib

0 files changed, 0 insertions, 0 deletions