From 3ec7f6d6373b6b8b5011daecbcf712f5a9d2dc7c Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 27 Mar 2020 01:19:40 +0000
Subject: Be more careful when flow-typing loops

Asserting constraints from the loop condition in the body is fine for
while-loops, but doesn't make sense for until-loops.
---
 test/typecheck/pass/repeat_constraint.sail      | 9 +++++++++
 test/typecheck/pass/repeat_constraint/v1.expect | 6 ++++++
 test/typecheck/pass/repeat_constraint/v1.sail   | 9 +++++++++
 3 files changed, 24 insertions(+)
 create mode 100644 test/typecheck/pass/repeat_constraint.sail
 create mode 100644 test/typecheck/pass/repeat_constraint/v1.expect
 create mode 100644 test/typecheck/pass/repeat_constraint/v1.sail

(limited to 'test/typecheck')

diff --git a/test/typecheck/pass/repeat_constraint.sail b/test/typecheck/pass/repeat_constraint.sail
new file mode 100644
index 00000000..6d63f2e8
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint.sail
@@ -0,0 +1,9 @@
+$include <flow.sail>
+
+val main : unit -> unit
+
+function main() = {
+  repeat {
+    _not_prove(constraint(false));
+  } until (false);
+}
diff --git a/test/typecheck/pass/repeat_constraint/v1.expect b/test/typecheck/pass/repeat_constraint/v1.expect
new file mode 100644
index 00000000..9d561e11
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint/v1.expect
@@ -0,0 +1,6 @@
+Type error:
+[repeat_constraint/v1.sail]:7:4-29
+7 |    _prove(constraint(false));
+  |    ^-----------------------^
+  | Cannot prove false
+  | 
diff --git a/test/typecheck/pass/repeat_constraint/v1.sail b/test/typecheck/pass/repeat_constraint/v1.sail
new file mode 100644
index 00000000..5dd2f513
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint/v1.sail
@@ -0,0 +1,9 @@
+$include <flow.sail>
+
+val main : unit -> unit
+
+function main() = {
+  repeat {
+    _prove(constraint(false));
+  } until (false);
+}
-- 
cgit v1.2.3