From 414cfd64702be920c9d96514e3802bc950b5ea0b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 7 Dec 2018 13:38:59 +0100
Subject: Clean the representation of recursive annotation in Constrexpr

We make clearer which arguments are optional and which are mandatory.
Some of these representations are tricky because of small differences
between Program and Function, which share the same infrastructure.

As a side-effect of this cleanup, Program Fixpoint can now be used with
e.g. {measure (m + n) R}. Previously, parentheses were required around
R.
---
 parsing/g_constr.mlg | 14 +++++++-------
 parsing/pcoq.mli     |  2 +-
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 0586dda555..7786155092 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -56,10 +56,10 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr =
   (id,ann,bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr =
-  let _ = Option.map (fun { CAst.loc = aloc } ->
+  Option.iter (fun { CAst.loc = aloc } ->
     CErrors.user_err ?loc:aloc
       ~hdr:"Constr:mk_cofixb"
-      (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
+      (Pp.str"Annotation forbidden in cofix expression.")) ann;
   let ty = match tyc with
       Some ty -> ty
     | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in
@@ -440,10 +440,10 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   fixannot:
-    [ [ "{"; IDENT "struct"; id=identref; "}" -> { (Some id, CStructRec) }
-    | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> { (id, CWfRec rel) }
+    [ [ "{"; IDENT "struct"; id=identref; "}" -> { CStructRec id }
+    | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CWfRec(id,rel) }
     | "{"; IDENT "measure"; m=constr; id=OPT identref;
-	rel=OPT constr; "}" -> { (id, CMeasureRec (m,rel)) }
+        rel=OPT constr; "}" -> { CMeasureRec (id,m,rel) }
     ] ]
   ;
   impl_name_head:
@@ -452,9 +452,9 @@ GRAMMAR EXTEND Gram
   binders_fixannot:
     [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot ->
           { (assum na :: fst bl), snd bl }
-      | f = fixannot -> { [], f }
+      | f = fixannot -> { [], Some (CAst.make ~loc f) }
       | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl }
-      | -> { [], (None, CStructRec) }
+      | -> { [], None }
     ] ]
   ;
   open_binders:
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 5d8897cb47..84d19730fa 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -191,7 +191,7 @@ module Constr :
     val binder : local_binder_expr list Entry.t (* closed_binder or variable *)
     val binders : local_binder_expr list Entry.t (* list of binder *)
     val open_binders : local_binder_expr list Entry.t
-    val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t
+    val binders_fixannot : (local_binder_expr list * recursion_order_expr CAst.t option) Entry.t
     val typeclass_constraint : (lname * bool * constr_expr) Entry.t
     val record_declaration : constr_expr Entry.t
     val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t
-- 
cgit v1.2.3