diff options
| author | Alasdair Armstrong | 2017-07-12 15:12:04 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-07-12 15:12:04 +0100 |
| commit | 1f09cfcd9703b0a10a0c73883dc4718a2d8275e8 (patch) | |
| tree | e3f07d0fde1f7cd7d1a6350816eb2ac72d6425bb /lib | |
| parent | 73c960dab16124dde513344777551b0bc4eacb88 (diff) | |
Fixed parser to parse 2** nexp expressions properly
This introduces some shift/reduce and reduce/reduce conflicts, but I don't think these matter.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/prelude.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail index f3637945..17b49980 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -16,7 +16,7 @@ val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec + (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec overload vector_subrange [vector_subrange_inc; vector_subrange_dec] @@ -39,7 +39,7 @@ overload (deinfix ^^) [duplicate; duplicate_bits] val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord. vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz -val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord. +val cast forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord. vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts overload EXTZ [extz] |