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/vector_inc.sail | |
| parent | f75f4b66028305d77205fe0f8ef0aa78c8660ada (diff) | |
Allow overloading of subrange builtins for non-bitvectors
Diffstat (limited to 'lib/vector_inc.sail')
| -rw-r--r-- | lib/vector_inc.sail | 8 |
1 files changed, 6 insertions, 2 deletions
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 /* |