Merge branch 'sail2' into mappings

4 files changed, 40 insertions, 1 deletions

diff --git a/doc/examples/exn.sail b/doc/examples/exn.sail
new file mode 100644
index 00000000..de97e3f9
--- /dev/null
+++ b/doc/examples/exn.sail
@@ -0,0 +1,20 @@
+val print = {ocaml: "print_endline"} : string -> unit
+
+scattered union exception
+
+union clause exception = Epair : (range(0, 255), range(0, 255))
+
+union clause exception = Eunknown : string
+
+function main() : unit -> unit = {
+  try {
+    throw(Eunknown("foo"))
+  } catch {
+    Eunknown(msg) => print(msg),
+    _ => exit()
+  }
+}
+
+union clause exception = Eint : int
+
+end exception
diff --git a/doc/examples/list.sail b/doc/examples/list.sail
new file mode 100644
index 00000000..4eaeb67a
--- /dev/null
+++ b/doc/examples/list.sail
@@ -0,0 +1 @@
+let l : list(int) = 1 :: 2 :: 3 :: [||]
\ No newline at end of file
diff --git a/doc/examples/my_replicate_bits.sail b/doc/examples/my_replicate_bits.sail
index bd45a32d..c9972cd6 100644
--- a/doc/examples/my_replicate_bits.sail
+++ b/doc/examples/my_replicate_bits.sail
@@ -11,7 +11,8 @@ val "shiftl" : forall 'm. (bits('m), int) -> bits('m)
 val operator >> = {
   ocaml: "shiftr_ocaml",
   c: "shiftr_c",
-  lem: "shiftr_lem"
+  lem: "shiftr_lem",
+  _: "shiftr"
 } : forall 'm. (bits('m), int) -> bits('m)
 
 val "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
diff --git a/doc/examples/regref.sail b/doc/examples/regref.sail
new file mode 100644
index 00000000..268af295
--- /dev/null
+++ b/doc/examples/regref.sail
@@ -0,0 +1,17 @@
+default Order dec
+$include <prelude.sail>
+
+register X0 : bits(8)
+register X1 : bits(8)
+register X2 : bits(8)
+
+let X : vector(3, dec, register(bits(8))) = [ref X2, ref X1, ref X0]
+
+function main() : unit -> unit = {
+  X0 = 0xFF;
+  assert(X0 == 0xFF);
+  (*X[0]) = 0x11;
+  assert(X0 == 0x11);
+  (*ref X0) = 0x00;
+  assert(X0 == 0x00)
+}
\ No newline at end of file