From 1f421b865a87a161a82550443a0cf39aa2642d9c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 15 Apr 2019 12:08:28 +0100
Subject: Basic loop termination measures for Coq Currently only supports pure
 termination measures for loops with effects.

The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
---
 src/interpreter.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/interpreter.ml')

diff --git a/src/interpreter.ml b/src/interpreter.ml
index f01a3846..b198c59b 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -243,8 +243,8 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
   | E_if (exp, then_exp, else_exp) ->
      step exp >>= fun exp' -> wrap (E_if (exp', then_exp, else_exp))
 
-  | E_loop (While, exp, body) -> wrap (E_if (exp, E_aux (E_block [body; orig_exp], annot), exp_of_value V_unit))
-  | E_loop (Until, exp, body) -> wrap (E_block [body; E_aux (E_if (exp, exp_of_value V_unit, orig_exp), annot)])
+  | E_loop (While, _, exp, body) -> wrap (E_if (exp, E_aux (E_block [body; orig_exp], annot), exp_of_value V_unit))
+  | E_loop (Until, _, exp, body) -> wrap (E_block [body; E_aux (E_if (exp, exp_of_value V_unit, orig_exp), annot)])
 
   | E_assert (exp, msg) when is_true exp -> wrap unit_exp
   | E_assert (exp, msg) when is_false exp && is_value msg ->
-- 
cgit v1.2.3