diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/c/pattern_concat_nest.expect | 2 | ||||
| -rw-r--r-- | test/c/pattern_concat_nest.sail | 44 |
2 files changed, 46 insertions, 0 deletions
diff --git a/test/c/pattern_concat_nest.expect b/test/c/pattern_concat_nest.expect new file mode 100644 index 00000000..b3bdd5e7 --- /dev/null +++ b/test/c/pattern_concat_nest.expect @@ -0,0 +1,2 @@ +works = 0b101 +doesnt = 0b010 diff --git a/test/c/pattern_concat_nest.sail b/test/c/pattern_concat_nest.sail new file mode 100644 index 00000000..92150e66 --- /dev/null +++ b/test/c/pattern_concat_nest.sail @@ -0,0 +1,44 @@ +default Order dec +type bits ('n : Int) = vector('n, dec, bit) + +union option ('a : Type) = {None : unit, Some : 'a} + +val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", c: "vector_subrange"} + : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm & 'm <= 'n. + (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) + +val bitvector_access = {ocaml: "access", lem: "access_vec_dec", c: "vector_access"} + : forall ('n : Int) ('m : Int), 0 <= 'm & 'm + 1 <= 'n. + (bits('n), atom('m)) -> bit + +overload vector_access = {bitvector_access} + +val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit"}: (bit, bit) -> bool + +overload operator == = { + eq_bit +} + +val and_bool = {ocaml: "and_bool", lem: "and_bool", smt: "and_bool", interpreter: "and_bool", c: "and_bool"}: (bool, bool) -> bool + + +//////////////////////////////////////////////////////////// + +val works : bits(8) -> bits(3) +function works bv = match bv { + a : bits(3) @ b : bits(2) @ 0b000 => a +} + +val doesnt : bits(8) -> bits(3) +function doesnt bv = match bv { + (a : bits(3) @ b : bits(2)) @ 0b000 => a +} + +val "print_bits" : forall 'n. (string, bits('n)) -> unit + +val main : unit -> unit + +function main() = { + print_bits("works = ", works(0b1010_0000)); + print_bits("doesnt = ", doesnt(0b0101_0000)); +}
\ No newline at end of file |
