diff options
| author | Alasdair Armstrong | 2017-12-14 16:04:06 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-12-14 16:04:06 +0000 |
| commit | 2162c6586b8024789875c2e619b09ba8348e72e0 (patch) | |
| tree | 52cdadf43453a20c5f48b259f925d15294acf056 /lib | |
| parent | fcb7b8dff4fb0ae308d900b7e53bfba56850cdfd (diff) | |
| parent | 4597e503131395df087b1aa9a600a96be5a960ed (diff) | |
Merge remote-tracking branch 'origin/experiments' into interactive
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" |