6e5cd5fcc0
@Kha I kept `TokenInfo` as is. That is, the `lbp` field is still `Option Nat`. I changed my mind because we have the combinator `NonReservedSymbol`. It feels weird to have a combinator that does not create a keyword, but sets the `lbp`. Recall that it is used at `Lean/Parser/Tactic.lean`. Other observations: - We use symbols in auxiliary constructions (e.g., `mkAntiquot`). It feels weird to set their `lbp` there. - It felt weird to specify the `lbp` in places such as ``` def structCtor := parser! ident >> optional inferMod >> symbol " :: " 67 ``` - We have a few parsing rules where the same symbol appears twice. It is funny to set the `lbp` twice. Note that the approach we discussed yesterday (retrieving the `lbp` from the `Environment`) would not work here.
58 lines
3.4 KiB
Text
58 lines
3.4 KiB
Text
/-
|
|
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura, Sebastian Ullrich
|
|
-/
|
|
prelude
|
|
import Lean.Parser.Term
|
|
|
|
namespace Lean
|
|
namespace Parser
|
|
namespace Tactic
|
|
|
|
def underscoreFn : ParserFn :=
|
|
fun c s =>
|
|
let s := symbolFn "_" c s;
|
|
let stx := s.stxStack.back;
|
|
let s := s.popSyntax;
|
|
s.pushSyntax $ mkIdentFrom stx `_
|
|
|
|
@[inline] def underscore : Parser :=
|
|
{ fn := underscoreFn,
|
|
info := mkAtomicInfo "ident" }
|
|
|
|
def ident' : Parser := ident <|> underscore
|
|
|
|
@[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> optional ident'
|
|
@[builtinTacticParser] def «intros» := parser! nonReservedSymbol "intros " >> many ident'
|
|
@[builtinTacticParser] def «revert» := parser! nonReservedSymbol "revert " >> many1 ident
|
|
@[builtinTacticParser] def «clear» := parser! nonReservedSymbol "clear " >> many1 ident
|
|
@[builtinTacticParser] def «subst» := parser! nonReservedSymbol "subst " >> many1 ident
|
|
@[builtinTacticParser] def «assumption» := parser! nonReservedSymbol "assumption"
|
|
@[builtinTacticParser] def «apply» := parser! nonReservedSymbol "apply " >> termParser
|
|
@[builtinTacticParser] def «exact» := parser! nonReservedSymbol "exact " >> termParser
|
|
@[builtinTacticParser] def «refine» := parser! nonReservedSymbol "refine " >> termParser
|
|
@[builtinTacticParser] def «case» := parser! nonReservedSymbol "case " >> ident >> tacticParser
|
|
@[builtinTacticParser] def «allGoals» := parser! nonReservedSymbol "allGoals " >> tacticParser
|
|
@[builtinTacticParser] def «skip» := parser! nonReservedSymbol "skip"
|
|
@[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
|
|
@[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticParser
|
|
@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 50 >> symbol " = " 50 >> ident
|
|
def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
|
|
def inductionAlt : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> (Term.hole <|> Term.namedHole <|> tacticParser)
|
|
def inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|")
|
|
def withAlts : Parser := optional (" with " >> inductionAlts)
|
|
def usingRec : Parser := optional (" using " >> ident)
|
|
def generalizingVars := optional (" generalizing " >> many1 ident)
|
|
@[builtinTacticParser] def «induction» := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> withAlts
|
|
@[builtinTacticParser] def «cases» := parser! nonReservedSymbol "cases " >> majorPremise >> withAlts
|
|
def withIds : Parser := optional (" with " >> many1 ident')
|
|
@[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds
|
|
@[builtinTacticParser] def paren := parser! symbol "(" appPrec >> nonEmptySeq >> ")"
|
|
@[builtinTacticParser] def nestedTacticBlock := parser! symbol "begin " appPrec >> seq >> "end"
|
|
@[builtinTacticParser] def nestedTacticBlockCurly := parser! symbol "{" appPrec >> seq >> "}"
|
|
@[builtinTacticParser] def orelse := tparser! symbol " <|> " 2 >> tacticParser 1
|
|
|
|
end Tactic
|
|
end Parser
|
|
end Lean
|