| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Added a test case for this behavior
|
|
For example,
val test = { ocaml: "test_ocaml" } : unit -> unit
will only be external for OCaml. For other backends, it will have to be
defined.
|
|
For example:
val test = { ocaml: "test_ocaml", lem: "test_lem" } : unit -> unit
val main : unit -> unit
function main () = {
test ();
}
for a backend not explicitly provided, the extern name would be simply
"test" in this case, i.e. the string version of the id.
Also fixed some bugs in the ocaml backend.
|
|
|
|
|
|
|
|
Cleaned up the option list in sail.ml
|
|
Fixed an issue in ast.ml with uneccessary type variables
|
|
|
|
Menhir pretty printer can now print enough sail to be useful with ASL parser
Fixity declarations are now preserved in the AST
Menhir parser now runs without the Pre-lexer
Ocaml backend now supports variant typedefs, as the machinery to
generate arbitrary instances of variant types has been added to the
-undefined_gen flag
|
|
|
|
|
|
|
|
just LB_val in AST
also rename functions in rewriter.ml appropriately.
|
|
|
|
|
|
syntactically correct ocaml
|
|
files into runable executable.
|
|
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
|
