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/rewriter.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'src/rewriter.ml')

diff --git a/src/rewriter.ml b/src/rewriter.ml
index 77070025..5907c603 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -346,7 +346,14 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) =
 let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = 
   let rewrite_funcl (FCL_aux (FCL_Funcl(id,pexp),(l,annot))) =
     (FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),(l,annot)))
-  in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot))
+  in
+  let recopt = match recopt with
+    | Rec_aux (Rec_nonrec, l) -> Rec_aux (Rec_nonrec, l)
+    | Rec_aux (Rec_rec, l) -> Rec_aux (Rec_rec, l)
+    | Rec_aux (Rec_measure (pat,exp),l) ->
+       Rec_aux (Rec_measure (rewrite_pat rewriters pat, rewrite_exp rewriters exp),l)
+  in
+  FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot))
 
 let rewrite_def rewriters d = match d with
   | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), annot)) ->
-- 
cgit v1.2.3