Make AST after rewriting for Lem backend type-checkable

- Add support for some internal nodes to type checker
- Add more explicit type annotations during rewriting
- Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer;
  these will be resolved by the type checker during rewriting now

2 files changed, 30 insertions, 1 deletions

diff --git a/lib/prelude.sail b/lib/prelude.sail
index 8cc1b86d..92bfb180 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -10,12 +10,16 @@ val forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec
 (* Vector access can't actually be properly polymorphic on vector
    direction because of the ranges being different for each type, so
    we overload it instead *)
+val forall Num 'n, 'n >= 0. (vector<'n - 1,'n,dec,bit>, [|0:'n - 1|]) -> bit effect pure bitvector_access_dec_norm
+val forall Num 'n, 'n >= 0. (vector<0,'n,inc,bit>, [|0:'n - 1|]) -> bit effect pure bitvector_access_inc_norm
+val forall Num 'n, Type 'a, 'n >= 0. (vector<'n - 1,'n,dec,'a>, [|0:'n - 1|]) -> 'a effect pure vector_access_dec_norm
+val forall Num 'n, Type 'a, 'n >= 0. (vector<0,'n,inc,'a>, [|0:'n - 1|]) -> 'a effect pure vector_access_inc_norm
 val extern forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
 val extern forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
 val extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec
 val extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc
 
-overload vector_access [bitvector_access_inc; bitvector_access_dec; vector_access_inc; vector_access_dec]
+overload vector_access [bitvector_access_dec_norm; bitvector_access_dec; bitvector_access_inc_norm; bitvector_access_inc; vector_access_inc_norm; vector_access_inc; vector_access_dec_norm; vector_access_dec]
 
 (* Type safe vector subrange *)
 (* vector_subrange(v, m, o) returns the subvector of v with elements with
@@ -57,6 +61,15 @@ val extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l
 
 overload vector_update [bitvector_update_dec; bitvector_update_inc; vector_update_dec; vector_update_inc]
 
+(* Vector subrange update *)
+
+val extern forall Num 'n, Num 'l, Num 'i, Num 'j, Num 'o, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [:'i:], [:'j:], vector<'o,'i - 'j + 1,dec,'a>) -> vector<'n,'l,dec,'a> effect pure vector_update_subrange_dec
+val extern forall Num 'n, Num 'l, Num 'i, Num 'j, Num 'o, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [:'i:], [:'j:], vector<'o,'j - 'i + 1,inc,'a>) -> vector<'n,'l,inc,'a> effect pure vector_update_subrange_inc
+val extern forall Num 'n, Num 'l, Num 'i, Num 'j, Num 'o, 'l >= 0. (vector<'n,'l,dec,bit>, [:'i:], [:'j:], vector<'o,'i - 'j + 1,dec,bit>) -> vector<'n,'l,dec,bit> effect pure bitvector_update_subrange_dec
+val extern forall Num 'n, Num 'l, Num 'i, Num 'j, Num 'o, 'l >= 0. (vector<'n,'l,inc,bit>, [:'i:], [:'j:], vector<'o,'j - 'i + 1,inc,bit>) -> vector<'n,'l,dec,bit> effect pure bitvector_update_subrange_inc
+
+overload vector_update_subrange [bitvector_update_subrange_dec; bitvector_update_subrange_inc; vector_update_subrange_dec; vector_update_subrange_inc]
+
 (* Implicit register dereferencing *)
 val cast extern forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref
 
diff --git a/lib/prelude_wrappers.sail b/lib/prelude_wrappers.sail
index 7fd6eac6..37b20f43 100644
--- a/lib/prelude_wrappers.sail
+++ b/lib/prelude_wrappers.sail
@@ -14,6 +14,10 @@ val extern forall Num 'n, Num 'l, 'l >= 0. ([:'n:], vector<'n,'l,dec,bit>, [|'n
 function forall Num 'n, Num 'l, 'l >= 0. bit bitvector_access_dec ((vector<'n,'l,dec,bit>) v, i) = bitvector_access_dec' (sizeof 'n, v, i)
 val extern forall Num 'n, Num 'l, 'l >= 0. ([:'n:], vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc' = "bitvector_access_inc"
 function forall Num 'n, Num 'l, 'l >= 0. bit bitvector_access_inc ((vector<'n,'l,inc,bit>) v, i) = bitvector_access_inc' (sizeof 'n, v, i)
+function forall Num 'n, 'n >= 0. bit bitvector_access_dec_norm ((vector<'n - 1,'n,dec,bit>) v, i) = bitvector_access_dec' (sizeof 'n - 1, v, i)
+function forall Num 'n, 'n >= 0. bit bitvector_access_inc_norm ((vector<0,'n,inc,bit>) v, i) = bitvector_access_inc' (0, v, i)
+function forall Num 'n, Type 'a, 'n >= 0. 'a vector_access_dec_norm ((vector<'n - 1,'n,dec,'a>) v, i) = vector_access_dec' (sizeof 'n - 1, v, i)
+function forall Num 'n, Type 'a, 'n >= 0. 'a vector_access_inc_norm ((vector<0,'n,inc,'a>) v, i) = vector_access_inc' (0, v, i)
 
 (* Vector subrange *)
 
@@ -37,6 +41,18 @@ val extern forall Num 'n, Num 'l, Num 'm, Num 'o, 'n >= 'm, 'm >= 'o, 'o >= 'n -
   ([:'n:], vector<'n,'l,dec,bit>, [:'m:], [:'o:]) -> vector<'m,('m - 'o) + 1,dec,bit> effect pure bitvector_subrange_dec' = "bitvector_subrange_dec"
 function bitvector_subrange_dec (v, i, j) = bitvector_subrange_dec' (sizeof 'n, v, i, j)
 
+(* Vector subrange update *)
+
+val extern forall Num 'n, Num 'l, Num 'i, Num 'j, Num 'o, Type 'a, 'l >= 0. ([:'n:], vector<'n,'l,dec,'a>, [:'i:], [:'j:], vector<'o,'i - 'j + 1,dec,'a>) -> vector<'n,'l,dec,'a> effect pure vector_update_subrange_dec' = "vector_update_subrange_dec"
+val extern forall Num 'n, Num 'l, Num 'i, Num 'j, Num 'o, Type 'a, 'l >= 0. ([:'n:], vector<'n,'l,inc,'a>, [:'i:], [:'j:], vector<'o,'j - 'i + 1,inc,'a>) -> vector<'n,'l,inc,'a> effect pure vector_update_subrange_inc' = "vector_update_subrange_inc"
+val extern forall Num 'n, Num 'l, Num 'i, Num 'j, Num 'o, 'l >= 0. ([:'n:], vector<'n,'l,dec,bit>, [:'i:], [:'j:], vector<'o,'i - 'j + 1,dec,bit>) -> vector<'n,'l,dec,bit> effect pure bitvector_update_subrange_dec' = "bitvector_update_subrange_dec"
+val extern forall Num 'n, Num 'l, Num 'i, Num 'j, Num 'o, 'l >= 0. ([:'n:], vector<'n,'l,inc,bit>, [:'i:], [:'j:], vector<'o,'j - 'i + 1,inc,bit>) -> vector<'n,'l,dec,bit> effect pure bitvector_update_subrange_inc' = "bitvector_update_subrange_inc"
+
+function vector_update_subrange_dec (v, i, j, v') = vector_update_subrange_dec' (sizeof 'n, v, i, j, v')
+function vector_update_subrange_inc (v, i, j, v') = vector_update_subrange_inc' (sizeof 'n, v, i, j, v')
+function bitvector_update_subrange_dec (v, i, j, v') = bitvector_update_subrange_dec' (sizeof 'n, v, i, j, v')
+function bitvector_update_subrange_inc (v, i, j, v') = bitvector_update_subrange_inc' (sizeof 'n, v, i, j, v')
+
 (* Bitvector extension *)
 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 extz' = "extz"