From e1a2b0d2a88e4797d714ad0cb941c3cbf019720b Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Sat, 4 Apr 2020 17:20:06 +0100
Subject: Tweak types of loop combinators for prover combinators

Split the variable (tuple) type into an input and output type.  They are
meant to be the same, but due to the way function types are
instantiated, unification can fail in the case of existential types, as
in the added test case (when trying to generate Lem definitions from
it).  The output of the loop will be checked against the expected type,
though, due to a type annotation outside the loop added by the rewrite
pass for variable updates.
---
 test/typecheck/pass/floor_pow2.sail | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test/typecheck/pass/floor_pow2.sail

(limited to 'test')

diff --git a/test/typecheck/pass/floor_pow2.sail b/test/typecheck/pass/floor_pow2.sail
new file mode 100644
index 00000000..fa8680cf
--- /dev/null
+++ b/test/typecheck/pass/floor_pow2.sail
@@ -0,0 +1,17 @@
+$include <arith.sail>
+
+val "pow2" : forall 'n, 'n >= 0. int('n) -> int(2 ^ 'n)
+
+val floor_pow2 : forall ('x : Int), 'x >= 0. int('x) -> int
+
+function floor_pow2 x = {
+    if x == 0 then {
+        return(0);
+    } else {
+        n : {'n, 'n >= 1. int('n)} = 1;
+        while x >= pow2(n) do {
+            n = n + 1
+        };
+        return(pow2(n - 1))
+    }
+}
-- 
cgit v1.2.3