Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-experiments

2 files changed, 21 insertions, 0 deletions

diff --git a/test/ocaml/hello_world/expect b/test/ocaml/hello_world/expect
new file mode 100644
index 00000000..3df47a31
--- /dev/null
+++ b/test/ocaml/hello_world/expect
@@ -0,0 +1,2 @@
+Hello, Sail!
+Hello, World!
diff --git a/test/ocaml/hello_world/hello_world.sail b/test/ocaml/hello_world/hello_world.sail
new file mode 100644
index 00000000..d96429f2
--- /dev/null
+++ b/test/ocaml/hello_world/hello_world.sail
@@ -0,0 +1,19 @@
+
+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 ()
+}