diff options
| author | Thomas Bauereiss | 2017-08-02 16:04:38 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-08-02 16:04:38 +0100 |
| commit | dbf09ba3d706db3e7b121d11a42a6f193a0f4291 (patch) | |
| tree | 6aba7a9c9713d8f06d9dc859bdde823d14f6a990 /lib | |
| parent | 9f0394eb854f22d6d590ce465d620050dcb8661d (diff) | |
Tune vector_subrange
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/prelude.sail | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail index bac9532c..5f809f72 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -16,11 +16,13 @@ val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l overload vector_access [vector_access_inc; vector_access_dec] (* Type safe vector subrange *) +(* vector_subrange(v, m, o) returns the subvector of v with elements with + indices from m up to and *including* o. *) val forall Num 'n, Num 'l, Num 'm, Num '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 + (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,('o - 'm) + 1,inc,'a> effect pure vector_subrange_inc val forall Num 'n, Num 'l, Num 'm, Num '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 val forall Num 'n, Num 'l, Order 'ord. (vector<'n,'l,'ord,bit>, int, int) -> list<bit> effect pure vector_subrange_bl @@ -276,4 +278,3 @@ typedef option = const union forall Type 'a. { None; 'a Some } - |