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.
---
 src/type_check.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index 82bc92d8..08b6eb5a 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3882,7 +3882,11 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        | Measure_aux (Measure_some exp,l) ->
           Measure_aux (Measure_some (crule check_exp env exp int_typ),l)
      in
-     let checked_body = crule check_exp (add_opt_constraint (assert_constraint env true checked_cond) env) body unit_typ in
+     let nc = match loop_type with
+       | While -> assert_constraint env true checked_cond
+       | Until -> None
+     in
+     let checked_body = crule check_exp (add_opt_constraint nc env) body unit_typ in
      annot_exp (E_loop (loop_type, checked_measure, checked_cond, checked_body)) unit_typ
   | E_for (v, f, t, step, ord, body) ->
      begin
-- 
cgit v1.2.3