diff options
| author | Thomas Bauereiss | 2020-02-24 19:34:02 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2020-02-24 20:43:10 +0000 |
| commit | 65228f7ea61535fa8961dcb8ce8f030e7359c479 (patch) | |
| tree | b5b6e975bbdbd0ae47f428b29caa69c62db85ab3 /lib | |
| parent | f75f4b66028305d77205fe0f8ef0aa78c8660ada (diff) | |
Allow overloading of subrange builtins for non-bitvectors
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/vector_dec.sail | 8 | ||||
| -rw-r--r-- | lib/vector_inc.sail | 8 |
2 files changed, 12 insertions, 4 deletions
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 6014ab8c..2a9e96f0 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -173,7 +173,7 @@ val or_vec = { overload operator | = {or_vec} -val vector_subrange = { +val subrange_bits = { ocaml: "subrange", interpreter: "subrange", lem: "subrange_vec_dec", @@ -182,7 +182,9 @@ val vector_subrange = { } : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n. (bits('n), int('m), int('o)) -> bits('m - 'o + 1) -val vector_update_subrange = { +overload vector_subrange = {subrange_bits} + +val update_subrange_bits = { ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_dec", @@ -190,6 +192,8 @@ val vector_update_subrange = { coq: "update_subrange_vec_dec" } : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), int('m), int('o), bits('m - ('o - 1))) -> bits('n) +overload vector_update_subrange = {update_subrange_bits} + val sail_shiftleft = "shiftl" : forall 'n ('ord : Order). (bitvector('n, 'ord), int) -> bitvector('n, 'ord) effect pure diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail index 381ae6bc..05f5c57f 100644 --- a/lib/vector_inc.sail +++ b/lib/vector_inc.sail @@ -108,7 +108,7 @@ val add_bits_int = { overload operator + = {add_bits, add_bits_int} -val vector_subrange = { +val subrange_bits = { ocaml: "subrange", interpreter: "subrange", lem: "subrange_vec_inc", @@ -117,7 +117,9 @@ val vector_subrange = { } : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'm <= 'o < 'n. (bits('n), atom('m), atom('o)) -> bits('o - 'm + 1) -val vector_update_subrange = { +overload vector_subrange = {subrange_bits} + +val update_subrange_bits = { ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_inc", @@ -125,6 +127,8 @@ val vector_update_subrange = { coq: "update_subrange_vec_inc" } : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) +overload vector_update_subrange = {update_subrange_bits} + // Some ARM specific builtins /* |