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).

1 files changed, 23 insertions, 15 deletions

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 8efd66f0..5ab93cbc 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -136,19 +136,29 @@ Definition Zwf_guarded (z:Z) : Acc (Zwf 0) z :=
   end).
 
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
-                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec whileM vars cond body =
-  cond vars >>= fun cond_val ->
-  if cond_val then
-    body vars >>= fun vars -> whileM vars cond body
-  else return vars
-
-val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
-                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec untilM vars cond body =
-  body vars >>= fun vars ->
-  cond vars >>= fun cond_val ->
-  if cond_val then return vars else untilM vars cond body
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*)
+Fixpoint whileMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E :=
+  if Z_ge_dec limit 0 then
+    cond vars >>= fun cond_val =>
+    if cond_val then
+      body vars >>= fun vars => whileMT' (limit - 1) vars cond body (_limit_reduces acc)
+    else returnm vars
+  else Fail "Termination limit reached".
+
+Definition whileMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E :=
+  whileMT' limit vars cond body (Zwf_guarded limit).
+
+(*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*)
+Fixpoint untilMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E :=
+  if Z_ge_dec limit 0 then
+    body vars >>= fun vars =>
+    cond vars >>= fun cond_val =>
+    if cond_val then returnm vars else untilMT' (limit - 1) vars cond body (_limit_reduces acc)
+  else Fail "Termination limit reached".
+
+Definition untilMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E :=
+  untilMT' limit vars cond body (Zwf_guarded limit).
 
 (*let write_two_regs r1 r2 vec =
   let is_inc =
@@ -171,8 +181,6 @@ let rec untilM vars cond body =
     else slice vec (start_vec - size_r1) (start_vec - size_vec) in
   write_reg r1 r1_v >> write_reg r2 r2_v*)
 
-*)
-
 (* If we need to build an existential after a monadic operation, assume that
    we can do it entirely from the type. *)