From ca0e42c0ff9e5cebb734bcb59065a4f55ae4aa4e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 28 Jul 2020 23:47:11 +0200
Subject: In recursive notations, accept partial application over the recursive
 pattern.

This allows e.g. to support a notation of the form "x <== y <== z <= t"
standing for "x <= y /\ y <= z /\ z <= t".
---
 interp/notation.ml     |  4 ++++
 interp/notation_ops.ml | 11 ++++++++++-
 2 files changed, 14 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index 948ebe9640..1a361dc1a6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -391,6 +391,10 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NBinderList (_,_,NApp (NRef ref,args),_,_) ->
       RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
   | NRef ref -> RefKey(canonical_gr ref), NotAppNotation
+  | NApp (NList (_,_,NApp (NRef ref,args),_,_), args') ->
+      RefKey (canonical_gr ref), AppBoundedNotation (List.length args + List.length args')
+  | NApp (NList (_,_,NApp (_,args),_,_), args') ->
+      Oth, AppBoundedNotation (List.length args + List.length args')
   | NApp (_,args) -> Oth, AppBoundedNotation (List.length args)
   | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation
   | _ -> Oth, NotAppNotation
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 2e3fa0aa0e..7cb3ca25ee 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -275,6 +275,12 @@ type found_variables = {
 let add_id r id = r := { !r with vars = id :: (!r).vars }
 let add_name r = function Anonymous -> () | Name id -> add_id r id
 
+let mkNApp1 (g,a) =
+  match g with
+  (* Ensure flattening of nested applicative nodes *)
+  | NApp (g,args') -> NApp (g,args'@[a])
+  | _ -> NApp (g,[a])
+
 let is_gvar id c = match DAst.get c with
 | GVar id' -> Id.equal id id'
 | _ -> false
@@ -443,7 +449,10 @@ let notation_constr_and_vars_of_glob_constr recvars a =
         aux' c
   and aux' x = DAst.with_val (function
   | GVar id -> if not (Id.equal id ldots_var) then add_id found id; NVar id
-  | GApp (g,args) -> NApp (aux g, List.map aux args)
+  | GApp (g,[]) -> NApp (aux g,[]) (* Encoding @foo *)
+  | GApp (g,args) ->
+     (* Treat applicative notes as binary nodes *)
+     let a,args = List.sep_last args in mkNApp1 (aux (DAst.make (GApp (g, args))), aux a)
   | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
   | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
   | GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c)
-- 
cgit v1.2.3