|
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
|
