Fix some more test cases

10 files changed, 68 insertions, 18 deletions

diff --git a/lib/prelude_wrappers.sail b/lib/prelude_wrappers.sail
index 4568f6ab..1d85b4ff 100644
--- a/lib/prelude_wrappers.sail
+++ b/lib/prelude_wrappers.sail
@@ -1,5 +1,5 @@
-val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
-val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,inc,bit> effect pure to_vec_inc
+val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,inc,bit> effect pure to_vec_inc
 function forall Num 'n, Num 'm. (vector<'m - 1,'m,dec,bit>) to_vec (n) = to_vec_dec ((sizeof 'm) - 1, sizeof 'm, n)
 
 function forall Num 'm. (vector<'m - 1,'m,dec,bit>) to_svec (n) = to_vec_dec ((sizeof 'm) - 1, sizeof 'm, n)
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index e2c8c0ac..1bfb19aa 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -530,14 +530,19 @@ let doc_exp_lem, doc_let_lem =
             if contains_bitvector_typ t && not (contains_t_pp_var t)
             then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
             else (epp, aexp_needed) in
-          if aexp_needed then parens (align taepp) else taepp
+          if aexp_needed then parens (align taepp) else taepp*)
        | Id_aux (Id "length",_) ->
+          (* Another temporary hack: The sizeof rewriting introduces calls to
+             "length", and the disambiguation between the length function on
+             bitvectors and vectors of other element types should be done by
+             the type checker, but type checking after rewriting steps is
+             currently broken. *)
           let [arg] = args in
           let targ = typ_of arg in
-          let call = if is_bitvector_typ targ then "bvlength" else "length" in
+          let call = if mwords && is_bitvector_typ targ then "bvlength" else "length" in
           let epp = separate space [string call;expY arg] in
           if aexp_needed then parens (align epp) else epp
-       | Id_aux (Id "bool_not", _) ->
+       (*)| Id_aux (Id "bool_not", _) ->
           let [a] = args in
           let epp = align (string "~" ^^ expY a) in
           if aexp_needed then parens (align epp) else epp *)
@@ -709,7 +714,9 @@ let doc_exp_lem, doc_let_lem =
         | _ -> parens (separate_map comma expN exps))
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
        let recordtyp = match annot with
-         | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
+         | Some (env, Typ_aux (Typ_id tid,_), _)
+         | Some (env, Typ_aux (Typ_app (tid, _), _), _)
+           when Env.is_record tid env ->
            tid
          | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        let epp = anglebars (space ^^ (align (separate_map
@@ -717,9 +724,11 @@ let doc_exp_lem, doc_let_lem =
                                           (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in
        if aexp_needed then parens epp else epp
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
-       let (E_aux (_, (_, eannot))) = e in
-       let recordtyp = match eannot with
-         | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
+       (* let (E_aux (_, (_, eannot))) = e in *)
+       let recordtyp = match annot with
+         | Some (env, Typ_aux (Typ_id tid,_), _)
+         | Some (env, Typ_aux (Typ_app (tid, _), _), _)
+           when Env.is_record tid env ->
            tid
          | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps))
diff --git a/src/rewriter.ml b/src/rewriter.ml
index d6a6aa2f..62ea6be7 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -2220,8 +2220,9 @@ let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) =
     (lhs, (fun exp -> rhs (E_aux (E_vector_update_subrange (lexp_to_exp lexp, e1, e2, exp), annot))))
   | LEXP_field (lexp, id) ->
     let (lhs, rhs) = rewrite_local_lexp lexp in
+    let (LEXP_aux (_, recannot)) = lexp in
     let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
-    (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), annot))))
+    (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), recannot))))
   | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le))
 
 (*Expects to be called after rewrite_defs; thus the following should not appear:
@@ -2946,6 +2947,18 @@ let rewrite_defs_letbind_effects  =
       let _ = reset_fresh_name_counter () in
       FCL_aux (FCL_Funcl (id,pat,n_exp_term newreturn exp),annot)
     in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),fdannot) in
+  let rewrite_def rewriters = function
+    | DEF_val (LB_aux (lb, annot)) ->
+      let rewrap lb = DEF_val (LB_aux (lb, annot)) in
+      begin
+        match lb with
+        | LB_val_implicit (pat, exp) ->
+          rewrap (LB_val_implicit (pat, n_exp_term (effectful exp) exp))
+        | LB_val_explicit (ts, pat, exp) ->
+          rewrap (LB_val_explicit (ts, pat, n_exp_term (effectful exp) exp))
+      end
+    | DEF_fundef fdef -> DEF_fundef (rewrite_fun rewriters fdef)
+    | d -> d in
   rewrite_defs_base
     {rewrite_exp = rewrite_exp
     ; rewrite_pat = rewrite_pat
diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail
index 83313ac7..cc84130f 100644
--- a/test/typecheck/pass/lexp_memory.sail
+++ b/test/typecheck/pass/lexp_memory.sail
@@ -48,7 +48,10 @@ val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'or
 
 overload (deinfix ==) [eq_vec]
 
-val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec
+val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+
+val cast forall Nat 'n, Nat 'l. [|0:1|] -> vector<'n,'l,dec,bit> effect pure cast_01_vec
+function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_01_vec i = to_vec_dec (sizeof 'n, sizeof 'l, i)
 val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned
 val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref
 
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
index 7808b2c0..0160dd8a 100644
--- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
+++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
@@ -1,5 +1,10 @@
-val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec
-val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec
+val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec
+val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec
+
+val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+
+function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i)
+function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i)
 
 default Order dec
 
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
index 26f161e2..847bca60 100644
--- a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
+++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
@@ -1,6 +1,11 @@
-val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec
-val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec
+val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec
+val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec
     
+val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+
+function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i)
+function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i)
+
 default Order dec
 
 typedef CauseReg = register bits [ 31 : 0 ] {
diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail
index 7bc7370b..af0b5ba2 100644
--- a/test/typecheck/pass/set_mark.sail
+++ b/test/typecheck/pass/set_mark.sail
@@ -1,5 +1,10 @@
 
-val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec
+val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+
+val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec
+function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i)
+
+default Order dec
 
 function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x
 
diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail
index cabfb1af..591c17ad 100644
--- a/test/typecheck/pass/set_mark2.sail
+++ b/test/typecheck/pass/set_mark2.sail
@@ -1,4 +1,10 @@
-val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec
+
+val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+
+val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec
+function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i)
+
+default Order dec
 
 function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x
 
diff --git a/test/typecheck/pass/varity.sail b/test/typecheck/pass/varity.sail
index d196f777..750d70eb 100644
--- a/test/typecheck/pass/varity.sail
+++ b/test/typecheck/pass/varity.sail
@@ -3,6 +3,10 @@ val int -> unit effect pure f1
 val (int, int) -> unit effect pure f2
 val (int, int, int) -> unit effect pure f3
 
+function f1 (i1) = ()
+function f2 (i1, i2) = ()
+function f3 (i1, i2, i3) = ()
+
 overload f [f1; f2; f3]
 
 val unit -> unit effect pure test
diff --git a/test/typecheck/pass/vector_synonym_cast.sail b/test/typecheck/pass/vector_synonym_cast.sail
index f1de42e9..bd0acaa6 100644
--- a/test/typecheck/pass/vector_synonym_cast.sail
+++ b/test/typecheck/pass/vector_synonym_cast.sail
@@ -1,7 +1,7 @@
 
 typedef vecsyn = vector<0,1,dec,bit>
 
-val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure adjust_dec
+val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure norm_dec
 
 val vector<1,1,dec,bit> -> vecsyn effect pure test