Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experiments

6 files changed, 97 insertions, 1 deletions

diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh
index 4454aa48..481ff80f 100755
--- a/test/ocaml/run_tests.sh
+++ b/test/ocaml/run_tests.sh
@@ -43,7 +43,7 @@ function finish_suite {
     fail=0
 }
 
-SAILLIBDIR="$DIR"
+SAILLIBDIR="$DIR/../../lib/"
 
 printf "<testsuites>\n" >> $DIR/tests.xml
 
diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail
new file mode 100644
index 00000000..a477cd97
--- /dev/null
+++ b/test/typecheck/pass/nzcv.sail
@@ -0,0 +1,9 @@
+default Order dec
+
+val bit[4] -> unit effect pure test
+
+function test nzcv =
+{
+  (N,Z,C,V) := nzcv;
+  ()
+}
diff --git a/test/typecheck/pass/while_MM.sail b/test/typecheck/pass/while_MM.sail
new file mode 100644
index 00000000..e6916edd
--- /dev/null
+++ b/test/typecheck/pass/while_MM.sail
@@ -0,0 +1,23 @@
+default Order dec
+
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
+    ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add"
+val extern (int, int) -> int effect pure add_int = "add"
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure add_vec_int
+overload (deinfix +) [add_vec_int; add_range; add_int]
+
+val extern bool -> bool effect pure bool_not = "not"
+
+val cast forall Num 'n, Num 'l. [:0:] -> vector<'n,'l,dec,bit> effect pure cast_0_vec_dec
+
+register (bit[64]) COUNT
+register (bool) INT
+
+function (unit) test () = {
+  COUNT := 0;
+  while (bool_not(INT)) do {
+    COUNT := COUNT + 1;
+  }
+}
+
diff --git a/test/typecheck/pass/while_MP.sail b/test/typecheck/pass/while_MP.sail
new file mode 100644
index 00000000..05d396e2
--- /dev/null
+++ b/test/typecheck/pass/while_MP.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val extern (int, int) -> int effect pure add_int = "add"
+overload (deinfix +) [add_vec_int; add_range; add_int]
+
+val extern bool -> bool effect pure bool_not = "not"
+
+register (bool) INT
+
+function (int) test () = {
+  (int) count := 0;
+  while (bool_not(INT)) do {
+    count := count + 1;
+  };
+  return count;
+}
+
diff --git a/test/typecheck/pass/while_PM.sail b/test/typecheck/pass/while_PM.sail
new file mode 100644
index 00000000..b03a87dc
--- /dev/null
+++ b/test/typecheck/pass/while_PM.sail
@@ -0,0 +1,23 @@
+default Order dec
+
+val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt"
+val extern (int, int) -> bool effect pure lt_int = "lt"
+overload (deinfix <) [lt_range_atom; lt_int]
+
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
+    ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add"
+val extern (int, int) -> int effect pure add_int = "add"
+overload (deinfix +) [add_range; add_int]
+
+val extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, int) -> bit effect pure vector_access = "bitvector_access_dec"
+
+register (bit[64]) GPR00
+
+function (unit) test ((bit) b) = {
+  (int) i := 0;
+  while (i < 64) do {
+    GPR00[i] := b;
+    i := i + 1;
+  }
+}
+
diff --git a/test/typecheck/pass/while_PP.sail b/test/typecheck/pass/while_PP.sail
new file mode 100644
index 00000000..454cc9ac
--- /dev/null
+++ b/test/typecheck/pass/while_PP.sail
@@ -0,0 +1,24 @@
+default Order dec
+
+val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt"
+val extern (int, int) -> bool effect pure lt_int = "lt"
+overload (deinfix <) [lt_range_atom; lt_int]
+
+val (int, int) -> int effect pure mult_int
+overload (deinfix * ) [mult_int]
+
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
+    ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add"
+val extern (int, int) -> int effect pure add_int = "add"
+overload (deinfix +) [add_range; add_int]
+
+function (int) test ((int) n) = {
+  (int) i := 1;
+  (int) j := 1;
+  while (i < n) do {
+    j := i * j;
+    i := i + 1;
+  };
+  j
+}
+