max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: revise have syntax

Browse source
This commit is contained in:
Sebastian Ullrich 2021-05-20 15:20:15 +02:00 • committed by Leonardo de Moura
parent a4de54eaf0
commit 5b6051b15e
2 changed files with 19 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/Lean/Elab/BuiltinNotation.lean
View file

@ -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

12
src/Lean/Parser/Term.lean
View file

@ -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»)