From 4c39126f0a0a97152f67a3a5e7c86db860f48e39 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 24 Apr 2020 21:52:37 +0200
Subject: Fix #12159 (Numeral Notations do not play well with multiple scopes
 for the same inductive)

Numeral Notations now play better with multiple scopes for the same
inductive. Previously, when multiple numeral notations where defined
for the same inductive, only the last one was considered for
printing. Now, we proceed as follows
1. keep only uninterpreters that produce an output (first
   List.map_filter)
2. keep only uninterpretation for scopes that either have a scope
   delimiter or are open (second List.map_filter)
3. the final selection is made according to the order of open scopes,
   (find_uninterpretation) or or according to the last defined
   notation if no appropriate scope is open (head of list at the end)
---
 test-suite/output/bug_12159.out | 28 ++++++++++++++++++++++++++++
 test-suite/output/bug_12159.v   | 39 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 67 insertions(+)
 create mode 100644 test-suite/output/bug_12159.out
 create mode 100644 test-suite/output/bug_12159.v

(limited to 'test-suite')

diff --git a/test-suite/output/bug_12159.out b/test-suite/output/bug_12159.out
new file mode 100644
index 0000000000..7f47c47e32
--- /dev/null
+++ b/test-suite/output/bug_12159.out
@@ -0,0 +1,28 @@
+f 1%B
+     : unit
+f 0
+     : unit
+1%B
+     : unit
+0
+     : unit
+1%B
+     : unit
+1
+     : unit
+1
+     : unit
+0
+     : unit
+1
+     : unit
+0%A
+     : unit
+1
+     : unit
+0%A
+     : unit
+0
+     : unit
+0
+     : unit
diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v
new file mode 100644
index 0000000000..91d66f7f4c
--- /dev/null
+++ b/test-suite/output/bug_12159.v
@@ -0,0 +1,39 @@
+Declare Scope A.
+Declare Scope B.
+Delimit Scope A with A.
+Delimit Scope B with B.
+Definition to_unit (v : Decimal.uint) : option unit
+  := match Nat.of_uint v with O => Some tt | _ => None end.
+Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
+Definition of_unit' (v : unit) : Decimal.uint := Nat.to_uint 1.
+Numeral Notation unit to_unit of_unit : A.
+Numeral Notation unit to_unit of_unit' : B.
+Definition f x : unit := x.
+Check f tt.
+Arguments f x%A.
+Check f tt.
+Check tt.
+Open Scope A.
+Check tt.
+Close Scope A.
+Check tt.
+Open Scope B.
+Check tt.
+Undelimit Scope B.
+Check tt.
+Open Scope A.
+Check tt.
+Close Scope A.
+Check tt.
+Close Scope B.
+Check tt.
+Open Scope B.
+Check tt.
+Notation "1" := true.
+Check tt.
+Open Scope A.
+Check tt.
+Declare Scope C.
+Notation "0" := false : C.
+Open Scope C.
+Check tt.  (* gives 0 but should now be 0%A *)
-- 
cgit v1.2.3