Add while-loops to Lem backend

4 files changed, 87 insertions, 0 deletions

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
+}
+