Support for printing (simple) notations with recursive binders in let…

…/match.

Printing notations with complex nesting of pattern-matching that
includes variables for recursive binders would typically require to
intertwin pattern-matching decompilation with search for notations.

interp/notation_ops.ml

@@ -965,6 +965,10 @@ let is_onlybinding_meta id metas =
   try match Id.List.assoc id metas with _,NtnTypeBinder _ -> true | _ -> false
   with Not_found -> false
 
+let is_onlybindinglist_meta id metas =
+  try match Id.List.assoc id metas with _,NtnTypeBinderList _ -> true | _ -> false
+  with Not_found -> false
+
 let is_onlybinding_pattern_like_meta isvar id metas =
   try match Id.List.assoc id metas with
     | _,NtnTypeBinder (NtnBinderParsedAsConstr (AsAnyPattern | AsStrictPattern)) -> true
@@ -1297,8 +1301,17 @@ let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1
   match DAst.get pat1, DAst.get pat2 with
   | PatVar _, PatVar (Name id2) when is_onlybinding_pattern_like_meta true id2 metas ->
       bind_binding_env alp sigma id2 [pat1]
+  | PatVar id1, PatVar (Name id2) when is_onlybindinglist_meta id2 metas ->
+      let t1 = DAst.make @@ GHole(Evar_kinds.BinderType id1,IntroAnonymous) in
+      bind_bindinglist_env alp sigma id2 [DAst.make @@ GLocalAssum (id1,Explicit,t1)]
   | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta false id2 metas ->
       bind_binding_env alp sigma id2 [pat1]
+  | _, PatVar (Name id2) when is_onlybindinglist_meta id2 metas ->
+      (* dummy data; should not be used anyway *)
+      let id1 = Namegen.next_ident_away (Id.of_string "x") Id.Set.empty in
+      let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id1),IntroAnonymous) in
+      let ids1 = [] in
+      bind_bindinglist_env alp sigma id2 [DAst.make @@ GLocalPattern (([pat1],ids1),id1,Explicit,t1)]
   | PatVar na1, PatVar na2 -> match_names metas acc na1 na2
   | _, PatVar Anonymous when allow_catchall -> acc
   | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
@@ -1462,11 +1475,12 @@ let rec match_ inner u alp metas sigma a1 a2 =
      match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2
   | GProd (na1,bk1,t1,b1), NProd (na2,t2,b2) ->
      match_extended_binders (not inner) u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2
-  | GLetIn (na1,b1,_,c1), NLetIn (na2,b2,None,c2)
-  | GLetIn (na1,b1,None,c1), NLetIn (na2,b2,_,c2) ->
-     match_binders u alp metas na1 na2 (match_in u alp metas sigma b1 b2) c1 c2
+  | GLetIn (na1,b1,t1,c1), NLetIn (na2,b2,None,c2)
+  | GLetIn (na1,b1,(None as t1),c1), NLetIn (na2,b2,_,c2) ->
+     let t = match t1 with Some t -> t | None -> DAst.make @@ GHole(Evar_kinds.BinderType na1,IntroAnonymous) in
+     match_extended_binders false u alp metas na1 na2 Explicit t (match_in u alp metas sigma b1 b2) c1 c2
   | GLetIn (na1,b1,Some t1,c1), NLetIn (na2,b2,Some t2,c2) ->
-     match_binders u alp metas na1 na2
+     match_extended_binders false u alp metas na1 na2 Explicit t1
        (match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2
   | GCases (sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2)
       when sty1 == sty2 && Int.equal (List.length tml1) (List.length tml2) ->

test-suite/output/Notations4.out

@@ -261,3 +261,32 @@ Notation "[[ _ ]]" is already defined at level 0 with arguments custom foo
 while it is now required to be at level 0 with arguments custom bar.
 lambda x y : nat, x + y = 0
      : nat -> nat -> Prop
+uncurryλ a b c => a + b + c
+     : unit * nat * nat * nat -> nat
+fun x : unit * nat * (nat * nat) =>
+match x with
+| (x0, y) =>
+    match y with
+    | (a, b) =>
+        let d := 1 in
+        match x0 with
+        | (x1, c) => let 'tt := x1 in a + b + c + d
+        end
+    end
+end
+     : unit * nat * (nat * nat) -> nat
+fun x : unit * nat * (nat * nat) =>
+match x with
+| (x0, (a, b)) => let d := 1 in match x0 with
+                                | (tt, c) => a + b + c + d
+                                end
+end
+     : unit * nat * (nat * nat) -> nat
+uncurryλ '(a, b) => a + b
+     : unit * (nat * nat) -> nat
+lets a b c := 0 in a + b + c
+     : nat
+let
+'(a, b) := (0, 0) in
+ lets d := 1 in let '(c, e) := (0, 0) in a + b + c + d + e
+     : nat

test-suite/output/Notations4.v

@@ -561,3 +561,36 @@ Notation "'lambda' x .. y , t" := (λ x .. y, t) (at level 200, x binder, y bind
 Check lambda x y, x+y=0.
 
 End RecursivePatternsArgumentsInRecursiveNotations.
+
+Module RecursivePatternsInMatch.
+
+Remove Printing Let prod.
+Unset Printing Matching.
+
+Notation "'uncurryλ' x1 .. xn => body"
+  := (fun x => match x with (pair x x1) => .. (match x with (pair x xn) => let 'tt := x in body end) .. end)
+     (at level 200, x1 binder, xn binder, right associativity).
+
+Check uncurryλ a b c => a + b + c.
+
+(* Check other forms of binders, but too complex interaction
+    with pattern-matching compaction for printing *)
+Check uncurryλ '(a,b) (d:=1) c => a + b + c + d.
+
+Set Printing Matching.
+Check uncurryλ '(a,b) (d:=1) c => a + b + c + d.
+
+(* This is a case where printing is easy though, relying on pattern-matching compaction *)
+Check uncurryλ '(a,b) => a + b.
+
+Notation "'lets' x1 .. xn := c 'in' body"
+  := (let x1 := c in .. (let xn := c in body) ..)
+     (at level 200, x1 binder, xn binder, right associativity).
+
+Check lets a b c := 0 in a + b + c.
+
+(* Check other forms of binders, but too complex interaction
+    with pattern-matching factorization for printing *)
+Check lets '(a,b) (d:=1) '(c,e) := (0,0) in a + b + c + d + e.
+
+End RecursivePatternsInMatch.