diff options
Diffstat (limited to 'test/ocaml/prelude.sail')
| -rw-r--r-- | test/ocaml/prelude.sail | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index 2526d109..cbe1927d 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -15,6 +15,10 @@ val extern forall Type 'a, Num 'n. vector<'n - 1, 'n, dec, 'a> -> [:'n:] effect val extern forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *). (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange = "subrange" +(* FIXME: rewriter shouldn't assume this exists *) +val extern forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *). + (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure bitvector_subrange_dec = "subrange" + val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int) -> 'a effect pure vector_access = "access" val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int, 'a) -> vector<'n - 1, 'n, dec, 'a> effect pure vector_update = "update" |