diff options
Diffstat (limited to 'doc/examples')
| -rw-r--r-- | doc/examples/bitfield.sail | 8 | ||||
| -rw-r--r-- | doc/examples/enum.sail | 7 | ||||
| -rw-r--r-- | doc/examples/enum1.sail | 1 | ||||
| -rw-r--r-- | doc/examples/enum2.sail | 5 | ||||
| -rw-r--r-- | doc/examples/my_replicate_bits.sail | 52 | ||||
| -rw-r--r-- | doc/examples/struct.sail | 5 | ||||
| -rw-r--r-- | doc/examples/type_operator.sail | 5 |
7 files changed, 83 insertions, 0 deletions
diff --git a/doc/examples/bitfield.sail b/doc/examples/bitfield.sail new file mode 100644 index 00000000..a7e23738 --- /dev/null +++ b/doc/examples/bitfield.sail @@ -0,0 +1,8 @@ +bitfield cr : vector(8, dec, bit) = { + CR0 : 7 .. 4, + LT : 7, + GT : 6, + CR1 : 3 .. 2, + CR3 : 1 .. 0 +} +register CR : cr
\ No newline at end of file diff --git a/doc/examples/enum.sail b/doc/examples/enum.sail new file mode 100644 index 00000000..3abad2d3 --- /dev/null +++ b/doc/examples/enum.sail @@ -0,0 +1,7 @@ +enum Foo = Bar | Baz | quux + +enum Foo = { + Bar, + Baz, + quux +}
\ No newline at end of file diff --git a/doc/examples/enum1.sail b/doc/examples/enum1.sail new file mode 100644 index 00000000..7234e4d8 --- /dev/null +++ b/doc/examples/enum1.sail @@ -0,0 +1 @@ +enum Foo = Bar | Baz | quux diff --git a/doc/examples/enum2.sail b/doc/examples/enum2.sail new file mode 100644 index 00000000..b3856191 --- /dev/null +++ b/doc/examples/enum2.sail @@ -0,0 +1,5 @@ +enum Foo = { + Bar, + Baz, + quux +} diff --git a/doc/examples/my_replicate_bits.sail b/doc/examples/my_replicate_bits.sail new file mode 100644 index 00000000..bd45a32d --- /dev/null +++ b/doc/examples/my_replicate_bits.sail @@ -0,0 +1,52 @@ +default Order dec + +$include <prelude.sail> + +infixl 7 << +infixl 7 >> + +val operator << = "shiftl" : forall 'm. (bits('m), int) -> bits('m) +val "shiftl" : forall 'm. (bits('m), int) -> bits('m) + +val operator >> = { + ocaml: "shiftr_ocaml", + c: "shiftr_c", + lem: "shiftr_lem" +} : forall 'm. (bits('m), int) -> bits('m) + +val "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) + +overload operator | = {or_vec} + +val my_replicate_bits : forall 'n 'm, 'm >= 1 & 'n >= 1. (int('n), bits('m)) -> bits('n * 'm) + +function my_replicate_bits(n, xs) = { + ys = zeros(n * length(xs)); + foreach (i from 1 to n) { + ys = ys << length(xs); + ys = ys | zero_extend(xs, length(ys)) + }; + ys +} + +val my_replicate_bits_2 : forall 'n 'm, 'm >= 1 & 'n >= 1. (int('n), bits('m)) -> bits('n * 'm) + +function my_replicate_bits_2(n, xs) = { + ys = zeros('n * 'm); + foreach (i from 1 to n) { + ys = (ys << 'm) | zero_extend(xs, 'n * 'm) + }; + ys +} + +val cast extz : forall 'n 'm, 'm >= 'n. bits('n) -> bits('m) + +function extz(xs) = zero_extend(xs, 'm) + +val my_replicate_bits_3 : forall 'n 'm, 'm >= 1 & 'n >= 1. (int('n), bits('m)) -> bits('n * 'm) + +function my_replicate_bits_3(n, xs) = { + ys = zeros('n * 'm); + foreach (i from 1 to n) ys = ys << 'm | xs; + ys +}
\ No newline at end of file diff --git a/doc/examples/struct.sail b/doc/examples/struct.sail new file mode 100644 index 00000000..a7b267e9 --- /dev/null +++ b/doc/examples/struct.sail @@ -0,0 +1,5 @@ +struct Foo = { + bar : vector(4, dec, bit), + baz : int, + quux : range(0, 9) +}
\ No newline at end of file diff --git a/doc/examples/type_operator.sail b/doc/examples/type_operator.sail new file mode 100644 index 00000000..871c8e0e --- /dev/null +++ b/doc/examples/type_operator.sail @@ -0,0 +1,5 @@ +infix 3 ... + +type operator ... ('n : Int) ('m : Int) = range('n, 'm) + +let x : 3 ... 5 = 4
\ No newline at end of file |