From 0795b6eade586ae33c2527689d76e6e11ba77e8e Mon Sep 17 00:00:00 2001 From: Vierkantor Date: Fri, 1 May 2020 10:14:42 +0000 Subject: [PATCH] feat(src/frontends): order notation by priority in pretty-printer If you have a notation for a special case, e.g. `finset.sum finset.univ`, and a notation for a general case, e.g. `finset.sum`, you can now give the special-cased notation a higher priority to ensure it is used by the pretty-printer when applicable. When deciding how to pretty-print an expression, Lean looks up the notations associated to the head of the expression. It tries them one-by-one until it finds a notation that matches the expression. The order in which they are tried used to be the definition order. This PR changes this ordering to have higher-priority notations first. Although `notation_entry.priority()` is also used by the parser, it doesn't seem to be set at all in mathlib. I expect that there will be no conflicts between the usage of `priority` in the parser and in the pretty-printer. --- src/frontends/lean/parser_config.cpp | 4 ++- tests/lean/notation_pp_priority.lean | 28 +++++++++++++++++++ .../notation_pp_priority.lean.expected.out | 4 +++ 3 files changed, 35 insertions(+), 1 deletion(-) create mode 100644 tests/lean/notation_pp_priority.lean create mode 100644 tests/lean/notation_pp_priority.lean.expected.out diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index e5a91fb19f..3a3e369e11 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -202,9 +202,11 @@ transition read_transition(deserializer & d) { return transition(n, a, pp); } +struct notation_prio_fn { unsigned operator()(notation_entry const & v) const { return v.priority(); } }; + struct notation_state { typedef rb_map, mpz_cmp_fn> num_map; - typedef head_map head_to_entries; + typedef head_map_prio head_to_entries; parse_table m_nud; parse_table m_led; num_map m_num_map; diff --git a/tests/lean/notation_pp_priority.lean b/tests/lean/notation_pp_priority.lean new file mode 100644 index 0000000000..3ffa212099 --- /dev/null +++ b/tests/lean/notation_pp_priority.lean @@ -0,0 +1,28 @@ +prelude + +import init.data.nat.basic + +noncomputable theory + +constant some_type : Type +constants foo bar : some_type + +/- + Test that notation with a high priority is used by the pretty-printer, + regardless of the order in which they are declared. +-/ +section + notation [priority 2000] `high_before_low` := foo + notation [priority 1] `low_after_high` := foo + + def test_high_before_low := foo + #print test_high_before_low +end + +section + notation [priority 1] `low_before_high` := bar + notation [priority 2000] `high_after_low` := bar + + def test_high_after_low := bar + #print test_high_after_low +end diff --git a/tests/lean/notation_pp_priority.lean.expected.out b/tests/lean/notation_pp_priority.lean.expected.out new file mode 100644 index 0000000000..25ec306096 --- /dev/null +++ b/tests/lean/notation_pp_priority.lean.expected.out @@ -0,0 +1,4 @@ +noncomputable def test_high_before_low : some_type := +high_before_low +noncomputable def test_high_after_low : some_type := +high_after_low