Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested…

… applications in notations

Reviewed-by: ejgallego
Ack-by: maximedenes

doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst

@@ -0,0 +1,8 @@
+- **Fixed:**
+  Issues in the presence of notations recursively referring to another
+  applicative notations, such as missing scope propagation, or failure
+  to use a notation for printing
+  (`#12960 <https://github.com/coq/coq/pull/12960>`_,
+  fixes `#9403 <https://github.com/coq/coq/issues/9403>`_
+  and `#10803 <https://github.com/coq/coq/issues/10803>`_,
+  by Hugo Herbelin).

interp/notation_ops.ml

@@ -187,7 +187,7 @@ let apply_cases_pattern ?loc (ids_disjpat,id) c =
 let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_status_fun) e nc =
   let lt x = DAst.make ?loc x in lt @@ match nc with
   | NVar id -> GVar id
-  | NApp (a,args) -> let e = h.no e in GApp (f e a, List.map (f e) args)
+  | NApp (a,args) -> let e = h.no e in DAst.get (mkGApp (f e a) (List.map (f e) args))
   | NList (x,y,iter,tail,swap) ->
       let t = f e tail in let it = f e iter in
       let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in

test-suite/output/bug_10803.out

@@ -0,0 +1,10 @@
+a !
+     : Foo
+where
+?y : [ |- nat]
+a !
+     : Foo
+a
+     : Foo -> Foo
+a !
+     : Foo

test-suite/output/bug_10803.v

@@ -0,0 +1,14 @@
+Inductive Foo := foo.
+Declare Scope foo_scope.
+Delimit Scope foo_scope with foo.
+Bind Scope foo_scope with Foo.
+Notation "'!'" := foo : foo_scope.
+Definition of_foo {x : nat} {y : nat} (f : Foo) := f.
+Notation a := (@of_foo O).
+Notation b := (@a).
+Check a !.
+Check @a O !.
+Check @b O.
+Check @b O !. (* was failing *)
+(* All are printed "a !", without making explicit the "0", which is
+   incidentally disputable *)

test-suite/output/bug_9403.out

@@ -0,0 +1,6 @@
+1 subgoal
+
+  X : tele
+  α, β, γ1, γ2 : X → Prop
+  ============================
+  accessor α β γ1 → accessor α β (λ.. x : X, γ1 x ∨ γ2 x)

test-suite/output/bug_9403.v

@@ -0,0 +1,99 @@
+(* Uselessly long but why not *)
+
+From Coq Require Export Utf8.
+
+Local Set Universe Polymorphism.
+
+Module tele.
+(** Telescopes *)
+Inductive tele : Type :=
+  | TeleO : tele
+  | TeleS {X} (binder : X → tele) : tele.
+
+Arguments TeleS {_} _.
+
+(** The telescope version of Coq's function type *)
+Fixpoint tele_fun (TT : tele) (T : Type) : Type :=
+  match TT with
+  | TeleO => T
+  | TeleS b => ∀ x, tele_fun (b x) T
+  end.
+
+Notation "TT -t> A" :=
+  (tele_fun TT A) (at level 99, A at level 200, right associativity).
+
+(** An eliminator for elements of [tele_fun].
+    We use a [fix] because, for some reason, that makes stuff print nicer
+    in the proofs in iris:bi/lib/telescopes.v *)
+Definition tele_fold {X Y} {TT : tele} (step : ∀ {A : Type}, (A → Y) → Y) (base : X → Y)
+  : (TT -t> X) → Y :=
+  (fix rec {TT} : (TT -t> X) → Y :=
+     match TT as TT return (TT -t> X) → Y with
+     | TeleO => λ x : X, base x
+     | TeleS b => λ f, step (λ x, rec (f x))
+     end) TT.
+Arguments tele_fold {_ _ !_} _ _ _ /.
+
+(** A sigma-like type for an "element" of a telescope, i.e. the data it
+  takes to get a [T] from a [TT -t> T]. *)
+Inductive tele_arg : tele → Type :=
+| TargO : tele_arg TeleO
+(* the [x] is the only relevant data here *)
+| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder).
+
+Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T :=
+  λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T :=
+     match a in tele_arg TT return (TT -t> T) → T with
+     | TargO => λ t : T, t
+     | TargS x a => λ f, rec a (f x)
+     end) TT a f.
+Arguments tele_app {!_ _} _ !_ /.
+
+Coercion tele_arg : tele >-> Sortclass.
+Local Coercion tele_app : tele_fun >-> Funclass.
+
+(** Operate below [tele_fun]s with argument telescope [TT]. *)
+Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U :=
+  match TT as TT return (TT → U) → TT -t> U with
+  | TeleO => λ F, F TargO
+  | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *)
+                  tele_bind (λ a, F (TargS x a))
+  end.
+Arguments tele_bind {_ !_} _ /.
+
+(** Notation-compatible telescope mapping *)
+(* This adds (tele_app ∘ tele_bind), which is an identity function, around every
+   binder so that, after simplifying, this matches the way we typically write
+   notations involving telescopes. *)
+Notation "t $ r" := (t r)
+  (at level 65, right associativity, only parsing).
+Notation "'λ..' x .. y , e" :=
+  (tele_app $ tele_bind (λ x, .. (tele_app $ tele_bind (λ y, e)) .. ))
+  (at level 200, x binder, y binder, right associativity,
+   format "'[  ' 'λ..'  x  ..  y ']' ,  e").
+
+(** Telescopic quantifiers *)
+Definition texist {TT : tele} (Ψ : TT → Prop) : Prop :=
+  tele_fold ex (λ x, x) (tele_bind Ψ).
+Arguments texist {!_} _ /.
+
+Notation "'∃..' x .. y , P" := (texist (λ x, .. (texist (λ y, P)) .. ))
+  (at level 200, x binder, y binder, right associativity,
+  format "∃..  x  ..  y ,  P").
+End tele.
+Import tele.
+
+(* This is like Iris' accessors, but in Prop.  Just to play with telescopes. *)
+Definition accessor {X : tele} (α β γ : X → Prop) : Prop :=
+  ∃.. x, α x ∧ (β x → γ x).
+
+(* Working with abstract telescopes. *)
+Section tests.
+Context {X : tele}.
+Implicit Types α β γ : X → Prop.
+
+Lemma acc_mono_disj α β γ1 γ2 :
+  accessor α β γ1 → accessor α β (λ.. x, γ1 x ∨ γ2 x).
+Show.
+Abort.
+End tests.