feat: nicer syntax for unification hints

lean4-mode/lean4-syntax.el

@@ -20,7 +20,7 @@
     "try" "catch" "finally" "where" "rec" "mut" "forall" "fun"
     "exists" "if" "then" "else" "from" "init_quot" "return"
     "mutual" "def" "run_cmd" "declare_syntax_cat" "syntax" "macro_rules" "macro"
-    "initialize" "builtin_initialize" "induction" "cases" "generalizing")
+    "initialize" "builtin_initialize" "induction" "cases" "generalizing" "unif_hint")
   "lean keywords ending with 'word' (not symbol)")
 (defconst lean4-keywords1-regexp
   (eval `(rx word-start (or ,@lean4-keywords1) word-end)))

src/Init/Core.lean

@@ -1038,16 +1038,4 @@ constant reduceNat (n : Nat) : Nat := n
 axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b
 axiom ofReduceNat (a b : Nat) (h : reduceNat a = b)    : a = b
 
-structure UnificationConstraint where
-  {α : Type u}
-  lhs : α
-  rhs : α
-
-infix:50 " ≟ "   => UnificationConstraint.mk
-infix:50 " =?= " => UnificationConstraint.mk
-
-structure UnificationHint where
-  constraints : List UnificationConstraint.{u}
-  pattern     : UnificationConstraint.{u}
-
 end Lean

src/Init/NotationExtra.lean

@@ -57,6 +57,30 @@ def expandBrackedBinders (combinatorDeclName : Name) (bracketedExplicitBinders :
   let combinator := mkIdentFrom (← getRef) combinatorDeclName
   expandBrackedBindersAux combinator #[bracketedExplicitBinders] body
 
+structure UnificationConstraint.{u} where
+  {α : Type u}
+  lhs : α
+  rhs : α
+
+structure UnificationHint.{u} where
+  constraints : List UnificationConstraint.{u}
+  pattern     : UnificationConstraint.{u}
+
+syntax unifConstraint := term:50 (" =?= " <|> " ≟ ") term:50
+syntax unifConstraintElem := colGe unifConstraint ", "?
+
+syntax "unif_hint " bracketedBinder* " where " withPosition(unifConstraintElem*) ("|-" <|> "⊢ ") unifConstraint : command
+
+macro_rules
+  | `(unif_hint $bs* where $cs* |- $p) => do
+    let mut csNew ← `([])
+    for c in cs.reverse do
+      csNew ← `((UnificationConstraint.mk $(c[0][0]) $(c[0][2])) :: $csNew)
+    `(@[unificationHint] def hint $bs:explicitBinder* : UnificationHint := {
+        constraints := $csNew
+        pattern := UnificationConstraint.mk $(p[0]) $(p[2])
+      })
+
 end Lean
 
 open Lean

tests/lean/run/unihint.lean

@@ -1,5 +1,3 @@
-open Lean
-
 structure S where
   carrier : Type
   mul : carrier → carrier → carrier
@@ -12,15 +10,11 @@ def Int.S : S where
   carrier := Int
   mul := (· * ·)
 
-@[unificationHint]
-def NatHint (s : S) : UnificationHint where
- pattern := s.carrier =?= Nat
- constraints := [ s =?= Nat.S ]
+unif_hint (s : S) where
+  s =?= Nat.S ⊢ s.carrier =?= Nat
 
-@[unificationHint]
-def IntHint (s : S) : UnificationHint where
- pattern := s.carrier =?= Int
- constraints := [ s =?= Int.S ]
+unif_hint (s : S) where
+  s =?= Int.S ⊢ s.carrier =?= Int
 
 def mul {s : S} (a b : s.carrier) : s.carrier :=
   s.mul a b
@@ -43,10 +37,8 @@ def sext (x : BV s) (n : Nat) : BV (s+n) :=
 def bvmul (x y : BV w) : BV w :=
   x
 
-@[unificationHint]
-def add64Eq128Hint (x : Nat) : UnificationHint where
- pattern := Nat.add 64 x =?= 128
- constraints := [ x =?= 64 ]
+unif_hint (x : Nat) where
+  x =?= 64 ⊢ Nat.add 64 x =?= 128
 
 set_option pp.all false