From 4f20163965e7c336f28740628fa9d64528006861 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 11 Dec 2018 11:54:36 +0000
Subject: Initial attempt at using termination measures in Coq This only
 applies to recursive functions and uses the termination measure merely as a
 limit to the recursive call depth, rather than proving the measure correct.

---
 src/parser.mly | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/parser.mly')

diff --git a/src/parser.mly b/src/parser.mly
index bb5aa5f1..9385c148 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -125,6 +125,8 @@ let doc_vs doc (VS_aux (v, l)) = VS_aux (v, Documented (doc, l))
 
 let qi_id_of_kopt (KOpt_aux (kopt_aux, l) as kopt) = QI_aux (QI_id kopt, l)
 
+let mk_recr r n m = (Rec_aux(r, loc n m))
+
 let mk_recn = (Rec_aux((Rec_nonrec), Unknown))
 let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown))
 let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
@@ -1216,9 +1218,15 @@ type_unions:
   | type_union Comma type_unions
     { $1 :: $3 }
 
+rec_measure:
+  | Lcurly pat EqGt exp Rcurly
+    { mk_recr (Rec_measure ($2, $4)) $startpos $endpos }
+
 fun_def:
   | Function_ funcls
     { let funcls, tannot = $2 in mk_fun (FD_function (mk_recn, tannot, mk_eannotn, funcls)) $startpos $endpos }
+  | Function_ rec_measure funcls
+    { let funcls, tannot = $3 in mk_fun (FD_function ($2, tannot, mk_eannotn, funcls)) $startpos $endpos }
 
 fun_def_list:
   | fun_def
-- 
cgit v1.2.3