From 94e2f401263c7efc69f7d2b731827dc41bd8c1b8 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 2 Aug 2019 11:39:25 +0100
Subject: Fix up some edge cases with the bitvector/polyvector split Mostly in
 the Coq backend, plus a few testcases that use bitvector builtins on
 poly-vectors (which works on some backends, but not Coq). Also handle some
 additional list inclusion proofs in Coq.

---
 test/typecheck/pass/deinfix_plus.sail | 4 ++--
 test/typecheck/pass/int_synonym.sail  | 2 +-
 test/typecheck/pass/lexp_vec.sail     | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'test')

diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail
index 261e3b44..e6f499a5 100644
--- a/test/typecheck/pass/deinfix_plus.sail
+++ b/test/typecheck/pass/deinfix_plus.sail
@@ -1,10 +1,10 @@
 default Order inc
 
 val bv_add = {ocaml: "add_vec", lem: "add_vec", coq: "add_vec"}: forall ('n : Int).
-  (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit)
+  (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc)
 
 overload operator + = {bv_add}
 
-val test : (vector(3, inc, bit), vector(3, inc, bit)) -> vector(3, inc, bit)
+val test : (bitvector(3, inc), bitvector(3, inc)) -> bitvector(3, inc)
 
 function test (x, y) = x + y
diff --git a/test/typecheck/pass/int_synonym.sail b/test/typecheck/pass/int_synonym.sail
index 33bdaf0c..8438b330 100644
--- a/test/typecheck/pass/int_synonym.sail
+++ b/test/typecheck/pass/int_synonym.sail
@@ -3,7 +3,7 @@ default Order dec
 
 $include <flow.sail>
 
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
 
 type xlen : Int       = 64
 type xlen_bytes : Int = 8
diff --git a/test/typecheck/pass/lexp_vec.sail b/test/typecheck/pass/lexp_vec.sail
index 605c3855..b20da027 100644
--- a/test/typecheck/pass/lexp_vec.sail
+++ b/test/typecheck/pass/lexp_vec.sail
@@ -2,9 +2,9 @@ default Order dec
 
 $include <prelude.sail>
 
-register V : vector(1, dec, vector(32, dec, bit))
+register V : vector(1, dec, bitvector(32, dec))
 
-val zeros : forall 'n, 'n >= 0. unit -> vector('n, dec, bit)
+val zeros : forall 'n, 'n >= 0. unit -> bitvector('n, dec)
 
 function main() : unit -> unit = {
   V[0] = zeros()
-- 
cgit v1.2.3