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, 18 insertions, 0 deletions

diff --git a/test/coq/pass/while_MM_terminating.sail b/test/coq/pass/while_MM_terminating.sail
new file mode 100644
index 00000000..e3bca7f5
--- /dev/null
+++ b/test/coq/pass/while_MM_terminating.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+register COUNT : int
+
+register INT : bool
+
+function test () -> unit = {
+  COUNT = 0;
+  while not_bool(INT) do {
+    COUNT = COUNT + 1;
+    if COUNT > 5 then
+      INT = true
+  }
+}
+
+termination_measure test while (5 - COUNT)