diff options
Diffstat (limited to 'doc/examples')
| -rw-r--r-- | doc/examples/exn.sail | 20 | ||||
| -rw-r--r-- | doc/examples/list.sail | 1 | ||||
| -rw-r--r-- | doc/examples/my_replicate_bits.sail | 3 | ||||
| -rw-r--r-- | doc/examples/regref.sail | 17 |
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 |
