diff options
| author | Thomas Bauereiss | 2017-12-12 18:27:04 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-12-12 19:20:04 +0000 |
| commit | 4597e503131395df087b1aa9a600a96be5a960ed (patch) | |
| tree | 32c91e1de62e92bc51b86d233f3f4037259c1448 /lib | |
| parent | 154e4871694a57faaf5e27b4f8a8957e40bf4182 (diff) | |
Add a few helper functions for bit lists
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/prelude.sail | 4 | ||||
| -rw-r--r-- | lib/prelude_wrappers.sail | 8 |
2 files changed, 6 insertions, 6 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail index a7f6fb2f..1f8f3e75 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -90,13 +90,13 @@ overload (deinfix ^^) [duplicate; duplicate_bits; duplicate_to_list; duplicate_b val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz -val extern forall Num 'm, Num 'p, Order 'ord. +val forall Num 'm, Num 'p, Order 'ord. list<bit> -> vector<'p, 'm, 'ord, bit> effect pure extz_bl val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts -val extern forall Num 'm, Num 'p, Order 'ord. +val forall Num 'm, Num 'p, Order 'ord. list<bit> -> vector<'p, 'm, 'ord, bit> effect pure exts_bl (* If we want an automatic bitvector extension, then this is the function to diff --git a/lib/prelude_wrappers.sail b/lib/prelude_wrappers.sail index 37b20f43..4dc15077 100644 --- a/lib/prelude_wrappers.sail +++ b/lib/prelude_wrappers.sail @@ -60,9 +60,9 @@ function forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. (vector<'p, 'm, 'ord, bit>) extz (v) = extz' (sizeof 'p, sizeof 'm, v) val extern forall Num 'm, Num 'p, Order 'ord. - ([:'p:], [:'m:], list<bit>) -> vector<'p, 'm, 'ord, bit> effect pure extz_bl' = "extz_bl" + ([:'p:], [:'m:], list<bit>) -> vector<'p, 'm, 'ord, bit> effect pure cast_bl_vec = "cast_bl_vec" function forall Num 'm, Num 'p, Order 'ord. - (vector<'p, 'm, 'ord, bit>) extz_bl (v) = extz_bl' (sizeof 'p, sizeof 'm, v) + (vector<'p, 'm, 'ord, bit>) extz_bl (v) = cast_bl_vec (sizeof 'p, sizeof 'm, v) val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. ([:'p:], [:'m:], vector<'o, 'n, 'ord, bit>) -> vector<'p, 'm, 'ord, bit> effect pure exts' = "exts" @@ -70,9 +70,9 @@ function forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. (vector<'p, 'm, 'ord, bit>) exts (v) = exts' (sizeof 'p, sizeof 'm, v) val extern forall Num 'm, Num 'p, Order 'ord. - ([:'p:], [:'m:], list<bit>) -> vector<'p, 'm, 'ord, bit> effect pure exts_bl' = "exts_bl" + ([:'p:], [:'m:], list<bit>) -> vector<'p, 'm, 'ord, bit> effect pure cast_bl_svec = "cast_bl_svec" function forall Num 'm, Num 'p, Order 'ord. - vector<'p, 'm, 'ord, bit> exts_bl (v) = exts_bl' (sizeof 'p, sizeof 'm, v) + vector<'p, 'm, 'ord, bit> exts_bl (v) = cast_bl_svec (sizeof 'p, sizeof 'm, v) val extern forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o. ([:'p:], [:'o:], vector<'n, 'm, 'ord, 'a>) -> vector<'p, 'o, 'ord, 'a> effect pure mask' = "extz" |