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/parse_ast.ml | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'src/parse_ast.ml')

diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 818c9340..896a860d 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -238,7 +238,14 @@ and fpat =
 
 type loop = While | Until
 
-type 
+type measure_aux =  (* optional termination measure for a loop *)
+ | Measure_none
+ | Measure_some of exp
+
+and measure = 
+ | Measure_aux of measure_aux * l
+
+and
 exp_aux =  (* Expression *)
    E_block of (exp) list (* block (parsing conflict with structs?) *)
  | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *)
@@ -251,7 +258,7 @@ exp_aux =  (* Expression *)
  | E_app_infix of exp * id * exp (* infix function application *)
  | E_tuple of (exp) list (* tuple *)
  | E_if of exp * exp * exp (* conditional *)
- | E_loop of loop * exp * exp
+ | E_loop of loop * measure * exp * exp
  | E_for of id * exp * exp * exp * atyp * exp (* loop *)
  | E_vector of (exp) list (* vector (indexed from 0) *)
  | E_vector_access of exp * exp (* vector access *)
@@ -489,6 +496,10 @@ dec_spec =
    DEC_aux of dec_spec_aux * l
 
 
+type loop_measure = 
+ | Loop of loop * exp
+
+
 type 
 scattered_def = 
    SD_aux of scattered_def_aux * l
@@ -509,6 +520,7 @@ def =  (* Top-level definition *)
  | DEF_default of default_typing_spec (* default kind and type assumptions *)
  | DEF_scattered of scattered_def (* scattered definition *)
  | DEF_measure of id * pat * exp (* separate termination measure declaration *)
+ | DEF_loop_measures of id * loop_measure list (* separate termination measure declaration *)
  | DEF_reg_dec of dec_spec (* register declaration *)
  | DEF_pragma of string * string * l
  | DEF_internal_mutrec of fundef list
-- 
cgit v1.2.3