From 5b6051b15ea92b40d1207c2ac55adebf703eb231 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 20 May 2021 15:20:15 +0200
Subject: [PATCH] feat: revise `have` syntax

---
 src/Lean/Elab/BuiltinNotation.lean | 19 ++++++++++---------
 src/Lean/Parser/Term.lean          | 12 +++++++++---
 2 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index c21c02569e..c635b6df6c 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -62,20 +62,21 @@ open Meta
   | _                                  => Macro.throwUnsupported
 
 @[builtinMacro Lean.Parser.Term.have] def expandHave : Macro := fun stx =>
-  let mkId (x? : Option Syntax) : Syntax :=
-    x?.getD <| mkIdentFrom stx `this
+  let thisId := mkIdentFrom stx `this
   match stx with
-  | `(have $[$x :]? $type from $val $[;]? $body)              => let x := mkId x; `(let_fun $x : $type := $val; $body)
-  | `(have $[$x :]? $type by%$b $tac:tacticSeq $[;]? $body)   => `(have $[$x :]? $type from by%$b $tac:tacticSeq; $body)
-  | `(have $x:ident : $type:term := $val $[;]? $body)         => `(let_fun $x:ident : $type:term := $val; $body)
-  | `(have $x:ident := $val:term $[;]? $body)                 => `(let_fun $x:ident := $val:term ; $body)
+  | `(have $x $bs* $[: $type]? := $val $[;]? $body)           => `(let_fun $x $bs* $[: $type]? := $val; $body)
+  | `(have : $type := $val $[;]? $body)                       => `(have $thisId : $type := $val; $body)
+  | `(have $x $bs* $[: $type]? $alts:matchAlts $[;]? $body)   => `(let_fun $x $bs* $[: $type]? $alts:matchAlts; $body)
+  | `(have : $type $alts:matchAlts $[;]? $body)               => `(have $thisId : $type $alts:matchAlts; $body)
   | `(have $pattern:term := $val:term $[;]? $body)            => `(let_fun $pattern:term := $val:term ; $body)
   | _                                                         => Macro.throwUnsupported
 
 @[builtinMacro Lean.Parser.Term.suffices] def expandSuffices : Macro
-  | `(suffices $[$x :]? $type from $val $[;]? $body)            => `(have $[$x :]? $type from $body; $val)
-  | `(suffices $[$x :]? $type by%$b $tac:tacticSeq $[;]? $body) => `(have $[$x :]? $type from $body; by%$b $tac:tacticSeq)
-  | _                                                           => Macro.throwUnsupported
+  | `(suffices $x:ident : $type from $val $[;]? $body)            => `(have $x : $type := $body; $val)
+  | `(suffices $type:term from $val $[;]? $body)                  => `(have : $type := $body; $val)
+  | `(suffices $x:ident : $type by%$b $tac:tacticSeq $[;]? $body) => `(have $x : $type := $body; by%$b $tac:tacticSeq)
+  | `(suffices $type:term by%$b $tac:tacticSeq $[;]? $body)       => `(have $type := $body; by%$b $tac:tacticSeq)
+  | _                                                             => Macro.throwUnsupported
 
 open Lean.Parser in
 private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax := do
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 2dd3ac4847..631495b573 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -71,9 +71,6 @@ def parenSpecial : Parser := optional (tupleTail <|> typeAscription)
 @[builtinTermParser] def anonymousCtor := leading_parser "⟨" >> sepBy termParser ", " >> "⟩"
 def optIdent : Parser := optional (atomic (ident >> " : "))
 def fromTerm   := leading_parser " from " >> termParser
-def haveAssign := leading_parser " := " >> termParser
-def haveDecl   := leading_parser optIdent >> termParser >> (haveAssign <|> fromTerm <|> byTactic)
-@[builtinTermParser] def «have» := leading_parser:leadPrec withPosition ("have " >> haveDecl) >> optSemicolon termParser
 def sufficesDecl := leading_parser optIdent >> termParser >> (fromTerm <|> byTactic)
 @[builtinTermParser] def «suffices» := leading_parser:leadPrec withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
 @[builtinTermParser] def «show»     := leading_parser:leadPrec "show " >> termParser >> (fromTerm <|> byTactic)
@@ -170,6 +167,15 @@ def letDecl     := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFoll
 @[builtinTermParser] def «let_fun»     := leading_parser:leadPrec withPosition ((symbol "let_fun " <|> "let_λ") >> letDecl) >> optSemicolon termParser
 @[builtinTermParser] def «let_delayed» := leading_parser:leadPrec withPosition ("let_delayed " >> letDecl) >> optSemicolon termParser
 
+-- like `let_fun` but with optional name
+def haveIdLhs    := nodeWithAntiquot "haveIdLhs" `Lean.Parser.Term.haveIdLhs      <| ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
+def haveNoIdLhs  := nodeWithAntiquot "haveNoIdLhs" `Lean.Parser.Term.haveNoIdLhs  <| typeSpec
+def haveLhs      := haveIdLhs <|> haveNoIdLhs
+def haveIdDecl   := nodeWithAntiquot "haveIdDecl"   `Lean.Parser.Term.haveIdDecl   $ atomic (haveLhs >> " := ") >> termParser
+def haveEqnsDecl := nodeWithAntiquot "haveEqnsDecl" `Lean.Parser.Term.haveEqnsDecl $ haveLhs >> matchAlts
+def haveDecl     := nodeWithAntiquot "haveDecl" `Lean.Parser.Term.haveDecl (haveIdDecl <|> letPatDecl <|> haveEqnsDecl)
+@[builtinTermParser] def «have» := leading_parser:leadPrec withPosition ("have " >> haveDecl) >> optSemicolon termParser
+
 def «scoped» := leading_parser "scoped "
 def «local»  := leading_parser "local "
 def attrKind := leading_parser optional («scoped» <|> «local»)