From d750f3e9256bba43d2eca33f0a4e9ad52e33e72e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 25 Apr 2019 17:12:37 +0100
Subject: Get basic constructor monomorphisation working again - updates for
 type checking changes - handle a little more pattern matching in constant
 propagation - fix bug where false positive warnings were produced - ensure
 bitvectors in tuples are always monomorphised (to catch the case   where the
 bitvectors only appear alone with a constant size)

---
 test/mono/not-yet/union-exist        |  1 -
 test/mono/not-yet/union-exist_manual |  1 -
 test/mono/pass/union-exist           |  1 +
 test/mono/pass/union-exist_manual    |  1 +
 test/mono/union-exist.sail           | 25 ++++++++-----------------
 5 files changed, 10 insertions(+), 19 deletions(-)
 delete mode 100644 test/mono/not-yet/union-exist
 delete mode 100644 test/mono/not-yet/union-exist_manual
 create mode 100644 test/mono/pass/union-exist
 create mode 100644 test/mono/pass/union-exist_manual

(limited to 'test')

diff --git a/test/mono/not-yet/union-exist b/test/mono/not-yet/union-exist
deleted file mode 100644
index ebb89267..00000000
--- a/test/mono/not-yet/union-exist
+++ /dev/null
@@ -1 +0,0 @@
-union-exist.sail -auto_mono
diff --git a/test/mono/not-yet/union-exist_manual b/test/mono/not-yet/union-exist_manual
deleted file mode 100644
index d35c3d48..00000000
--- a/test/mono/not-yet/union-exist_manual
+++ /dev/null
@@ -1 +0,0 @@
-union-exist.sail -mono_split union-exist.sail:9:v
\ No newline at end of file
diff --git a/test/mono/pass/union-exist b/test/mono/pass/union-exist
new file mode 100644
index 00000000..ebb89267
--- /dev/null
+++ b/test/mono/pass/union-exist
@@ -0,0 +1 @@
+union-exist.sail -auto_mono
diff --git a/test/mono/pass/union-exist_manual b/test/mono/pass/union-exist_manual
new file mode 100644
index 00000000..54deb7d8
--- /dev/null
+++ b/test/mono/pass/union-exist_manual
@@ -0,0 +1 @@
+union-exist.sail -mono_split union-exist.sail:10:v
diff --git a/test/mono/union-exist.sail b/test/mono/union-exist.sail
index f1e01e75..ca953b3c 100644
--- a/test/mono/union-exist.sail
+++ b/test/mono/union-exist.sail
@@ -1,32 +1,23 @@
 default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
-val operator & = "and_bool" : (bool, bool) -> bool
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
-val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
-overload operator == = {eq_int, eq_vec}
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
-  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
-
+$include <prelude.sail>
 
 union myunion = {
-  MyConstr : {'n, 'n in {8,16}. (atom('n),bits('n))}
+  MyConstr : {'n, 'n in {8,16}. (int('n),bits('n))}
 }
 
 val make : bits(2) -> myunion
 
 function make(v) =
-  /* Can't mention these below without running into exp/nexp parsing conflict! */
-  let eight = 8 in let sixteen = 16 in
-  let r : {'n, 'n in {8,16}. (atom('n),bits('n))} = match v {
-    0b00 => (  eight,  0x12),
-    0b01 => (sixteen,0x1234),
-    0b10 => (  eight,  0x56),
-    0b11 => (sixteen,0x5678)
+  let r : {'n, 'n in {8,16}. (int('n),bits('n))} = match v {
+    0b00 => ( 8,  0x12),
+    0b01 => (16,0x1234),
+    0b10 => ( 8,  0x56),
+    0b11 => (16,0x5678)
   } in MyConstr(r)
 
 val use : myunion -> bits(32)
 
-function use(MyConstr((n,v) as (atom('n),bits('n)))) = extz(v)
+function use(MyConstr(n,v)) = sail_zero_extend(v,32)
 
 val run : unit -> unit effect {escape}
 
-- 
cgit v1.2.3