diff options
| author | Thomas Bauereiss | 2020-03-27 01:19:40 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2020-04-10 13:22:11 +0100 |
| commit | 3ec7f6d6373b6b8b5011daecbcf712f5a9d2dc7c (patch) | |
| tree | 33957d9e6a1c32e7a94e30b24bab0129acf8de6a /src | |
| parent | 8d28bb30b0ff1812fa0ad58147d42cddde3099da (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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 |