feat(library/init/lean/parser/notation): simple term language for precedences

library/init/lean/elaborator.lean

@@ -34,7 +34,7 @@ do cfg ← read,
 local attribute [instance] name.has_lt_quick
 
 def prec_to_nat (prec : option precedence.view) : nat :=
-(prec <&> λ p, p.prec.to_nat).get_or_else 0
+(prec <&> λ p, p.term.to_nat).get_or_else 0
 
 def command_parser_config.register_notation_tokens (spec : notation_spec.view) (cfg : command_parser_config) :
   except string command_parser_config :=
@@ -78,7 +78,9 @@ def postprocess_notation_spec (spec : notation_spec.view) : notation_spec.view :
 -- NOTE: should happen after copying precedences from reserved notation
 match spec with
 | {prefix_arg := none, rules := r@{symbol := notation_symbol.view.quoted sym@{prec := none, ..}, ..}::rs} :=
-  {spec with rules := {r with symbol := notation_symbol.view.quoted {sym with prec := some {prec := number.view.of_nat max_prec}}}::rs}
+  {spec with rules := {r with symbol := notation_symbol.view.quoted {sym with prec := some
+    {term := precedence_term.view.lit $ precedence_lit.view.num $ number.view.of_nat max_prec}
+  }}::rs}
 | _ := spec
 
 def reserve_notation.elaborate : elaborator :=
@@ -95,7 +97,7 @@ def reserve_notation.elaborate : elaborator :=
 
 def match_precedence : option precedence.view → option precedence.view → bool
 | none      (some rp) := tt
-| (some sp) (some rp) := sp.prec.to_nat = rp.prec.to_nat
+| (some sp) (some rp) := sp.term.to_nat = rp.term.to_nat
 | _         _         := ff
 
 /-- Check if a notation is compatible with a reserved notation, and if so, copy missing

library/init/lean/expander.lean

@@ -56,7 +56,7 @@ match k with
     rules := [{
       symbol := sym,
       transition := transition.view.arg {id := `b,
-        action := prec_to_action <$> precedence.view.prec <$> prec}}]}
+        action := prec_to_action <$> precedence.view.term <$> prec}}]}
 | mixfix.kind.view.postfix _ :=
   -- `postfix tk:prec` ~> `notation a tk:prec`
   pure {
@@ -65,9 +65,9 @@ match k with
 | mixfix.kind.view.infixr _ := do
   -- `infixr tk:prec` ~> `notation a tk:prec b:(prec-1)`
   act ← match prec with
-  | some prec := if prec.prec.to_nat = 0
+  | some prec := if prec.term.to_nat = 0
     then error (review «precedence» prec) "invalid `infixr` declaration, given precedence must greater than zero"
-    else pure $ some $ prec_to_action $ number.view.of_nat $ prec.prec.to_nat - 1
+    else pure $ some $ prec_to_action $ precedence_term.view.lit $ precedence_lit.view.num $ number.view.of_nat $ prec.term.to_nat - 1
   | none := pure none,
   pure {
     prefix_arg := `a,
@@ -82,7 +82,7 @@ match k with
     rules := [{
       symbol := sym,
       transition := transition.view.arg {id := `b,
-        action := prec_to_action <$> precedence.view.prec <$> prec}}]}
+        action := prec_to_action <$> precedence.view.term <$> prec}}]}
 
 def mixfix.transform : transformer :=
 λ stx, do

library/init/lean/parser/notation.lean

@@ -26,9 +26,38 @@ set_option class.instance_max_depth 100
 
 namespace «command»
 namespace notation_spec
+@[derive parser.has_tokens parser.has_view]
+def precedence_lit.parser : term_parser :=
+node_choice! precedence_lit {
+  num: number.parser,
+  max: symbol_or_ident "max",
+  -- TODO(Sebastian): `prec_of`?
+}
+
+def precedence_lit.view.to_nat : precedence_lit.view → nat
+| (precedence_lit.view.num n) := n.to_nat
+| (precedence_lit.view.max _) := max_prec
+
+@[derive parser.has_tokens parser.has_view]
+def precedence_term.parser : term_parser :=
+node_choice! precedence_term {
+  lit: precedence_lit.parser,
+  offset: node! precedence_offset ["(", lit: precedence_lit.parser,
+    op: node_choice! precedence_offset_op {" + ", " - "},
+    offset: number.parser,
+    ")",
+  ]
+}
+
+def precedence_term.view.to_nat : precedence_term.view → nat
+| (precedence_term.view.lit l) := l.to_nat
+| (precedence_term.view.offset o) := match o.op with
+  | (precedence_offset_op.view.«+» _) := o.lit.to_nat.add o.offset.to_nat
+  | (precedence_offset_op.view.«-» _) := o.lit.to_nat - o.offset.to_nat
+
 @[derive parser.has_tokens parser.has_view]
 def precedence.parser : term_parser :=
-node! «precedence» [":", prec: number.parser]/-TODO <|> expr-/
+node! «precedence» [":", term: precedence_term.parser]
 
 def quoted_symbol.parser : term_parser :=
 do (s, info) ← with_source_info $ take_until (= '`'),
@@ -74,8 +103,7 @@ node_choice! mixfix_symbol {
 @[derive parser.has_tokens parser.has_view]
 def action.parser : term_parser :=
 node! action [":", action: node_choice! action_kind {
-  prec: number.parser,
-  max: symbol_or_ident "max",
+  prec: try precedence_term.parser,
   prev: symbol_or_ident "prev",
   scoped: node! scoped_action [
     "(",