From d7d968cead615471e62e615d8e9c68a6931da50b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Sep 2018 18:45:18 -0700
Subject: [PATCH] feat(library/init/lean/parser/basic): merge explicit and
 default (0) token precedences

---
 library/init/lean/parser/basic.lean       | 11 +++++++----
 library/init/lean/parser/declaration.lean |  6 +++---
 library/init/lean/parser/term.lean        |  6 +++---
 3 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean
index 275cf16af4..24cfdcfa75 100644
--- a/library/init/lean/parser/basic.lean
+++ b/library/init/lean/parser/basic.lean
@@ -110,12 +110,15 @@ def eoi : syntax_node_kind := ⟨`lean.parser.eoi⟩
 
 def mk_parser_state (tokens : list token_config) : except string parser_state :=
 do -- the only hardcoded tokens, because they are never directly mentioned by a `parser`
-   let builtin_tokens : list token_config := [⟨"/-", 0, none⟩, ⟨"--", 0, none⟩],
+   let builtin_tokens : list token_config := [{«prefix» := "/-"}, {«prefix» := "--"}],
    t ← (builtin_tokens ++ tokens).mfoldl (λ (t : trie token_config) tk,
      match t.find tk.prefix with
-     | some tk' := if tk.lbp = tk'.lbp then pure t else throw $
-       "invalid token '" ++ tk.prefix ++ "', has been defined with precendences " ++
-       to_string tk.lbp ++ " and " ++ to_string tk'.lbp
+     | some tk' := (match tk.lbp, tk'.lbp with
+       | l, 0  := pure $ t.insert tk.prefix tk
+       | 0, _  := pure t
+       | l, l' := if l = l' then pure t else throw $
+         "invalid token '" ++ tk.prefix ++ "', has been defined with precedences " ++
+         to_string l ++ " and " ++ to_string l')
      | none := pure $ t.insert tk.prefix tk)
      trie.mk,
    pure ⟨t, message_log.empty⟩
diff --git a/library/init/lean/parser/declaration.lean b/library/init/lean/parser/declaration.lean
index 1e02a67d8a..8b648fc391 100644
--- a/library/init/lean/parser/declaration.lean
+++ b/library/init/lean/parser/declaration.lean
@@ -77,8 +77,8 @@ node_choice! decl_val {
 @[derive has_tokens has_view]
 def infer_modifier.parser : command_parser :=
 node_choice! infer_modifier {
-  relaxed: try $ node! relaxed_infer_modifier ["{":max_prec, "}"],
-  strict: try $ node! strict_infer_modifier ["(":max_prec, ")"],
+  relaxed: try $ node! relaxed_infer_modifier ["{", "}"],
+  strict: try $ node! strict_infer_modifier ["(", ")"],
 }
 
 @[derive has_tokens has_view]
@@ -95,7 +95,7 @@ def structure_field.parser : command_parser :=
 node_choice! structure_field {
   -- TODO(Sebastian): this `try` is too coarse
   local_notation: try node! structure_notation [
-    "(":max_prec, «notation»: notation_like.parser, ")"],
+    "(", «notation»: notation_like.parser, ")"],
   field: term.bracketed_binder.parser,
 }
 
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 20dc3b5fa9..15d3299963 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -87,13 +87,13 @@ node! binder_content [
 @[derive has_tokens has_view]
 def bracketed_binder.parser : term_parser :=
 node_choice! bracketed_binder {
-  explicit: node! explicit_binder ["(":max_prec, content: node_choice! explicit_binder_content {
+  explicit: node! explicit_binder ["(", content: node_choice! explicit_binder_content {
     «notation»: command.notation_like.parser,
     other: binder_content.parser
   }, right: symbol ")"],
-  implicit: node! implicit_binder ["{":max_prec, content: binder_content.parser, "}"],
+  implicit: node! implicit_binder ["{", content: binder_content.parser, "}"],
   strict_implicit: node! strict_implicit_binder [
-    left: any_of [symbol "{{" max_prec, symbol "⦃" max_prec],
+    left: any_of [symbol "{{", symbol "⦃"],
     content: binder_content.parser,
     right: any_of [symbol "}}", symbol "⦄"]
   ],