Equations
- Lean.Elab.Term.expandOptPrecedence stx = if Lean.Syntax.isNone stx = true then pure none else do let a ← Lean.evalPrec (Lean.Syntax.getOp (Lean.Syntax.getOp stx 0) 1) pure (some a)
- catName : Lean.Name
- first : Bool
- leftRec : Bool
- behavior : Lean.Parser.LeadingIdentBehavior
@[inline]
Equations
- Lean.Elab.Term.checkLeftRec stx = do let ctx ← read let _do_jp : PUnit → Lean.Elab.Term.ToParserDescrM Bool := fun y => let cat := Lean.Name.eraseMacroScopes (Lean.Syntax.getId (Lean.Syntax.getOp stx 0)); let _do_jp := fun y => do let prec? ← Lean.Elab.liftMacroM (Lean.Elab.Term.expandOptPrecedence (Lean.Syntax.getOp stx 1)) let _do_jp : PUnit → Lean.Elab.Term.ToParserDescrM Bool := fun y => do Lean.Elab.Term.markAsTrailingParser (Option.getD prec? 0) pure true if ctx.leftRec = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwErrorAt (Lean.Syntax.getOp stx 3) (Lean.toMessageData "invalid occurrence of '" ++ Lean.toMessageData cat ++ Lean.toMessageData "', parser algorithm does not allow this form of left recursion") _do_jp y; if (cat == ctx.catName) = true then do let y ← pure PUnit.unit _do_jp y else pure false if (ctx.first && Lean.Syntax.getKind stx == `Lean.Parser.Syntax.cat) = true then do let y ← pure PUnit.unit _do_jp y else pure false
Equations
- Lean.Elab.Term.toParserDescr stx catName = (fun processSeq resolveParserName ensureNoPrec processSepBy1 isValidAtom processNonReserved => do let env ← Lean.getEnv let behavior : Lean.Parser.LeadingIdentBehavior := Lean.Parser.leadingIdentBehavior env catName StateRefT'.run (process stx { catName := catName, first := true, leftRec := true, behavior := behavior }) none) Lean.Elab.Term.toParserDescr.process Lean.Elab.Term.toParserDescr.processSeq Lean.Elab.Term.toParserDescr.resolveParserName Lean.Elab.Term.toParserDescr.ensureNoPrec Lean.Elab.Term.toParserDescr.processParserCategory Lean.Elab.Term.toParserDescr.processNullaryOrCat Lean.Elab.Term.toParserDescr.processUnary Lean.Elab.Term.toParserDescr.processBinary Lean.Elab.Term.toParserDescr.processSepBy Lean.Elab.Term.toParserDescr.processSepBy1 Lean.Elab.Term.toParserDescr.isValidAtom Lean.Elab.Term.toParserDescr.processAtom Lean.Elab.Term.toParserDescr.processNonReserved
Equations
- Lean.Elab.Term.toParserDescr.resolveParserName parserName = do let r ← tryCatch (do let candidates ← Lean.Elab.resolveGlobalConstWithInfos parserName let env ← Lean.getEnv let y ← pure (List.filterMap (fun c => match Lean.Environment.find? env c with | none => none | some info => match Lean.ConstantInfo.type info with | Lean.Expr.const (Lean.Name.str (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Lean" x_2) "Parser" x_3) "TrailingParser" x_4) x x_1 => some (c, false) | Lean.Expr.const (Lean.Name.str (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Lean" x_2) "Parser" x_3) "Parser" x_4) x x_1 => some (c, false) | Lean.Expr.const (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Lean" x_2) "ParserDescr" x_3) x x_1 => some (c, true) | Lean.Expr.const (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Lean" x_2) "TrailingParserDescr" x_3) x x_1 => some (c, true) | x => none) candidates) pure (DoResultPR.pure y PUnit.unit)) fun x => pure (DoResultPR.return [] PUnit.unit) match r with | DoResultPR.pure a u => let x := u; pure a | DoResultPR.return b u => let x := u; pure b
Equations
- Lean.Elab.Term.toParserDescr.ensureNoPrec stx = if Lean.Syntax.isNone (Lean.Syntax.getOp stx 1) = true then pure PUnit.unit else Lean.throwErrorAt (Lean.Syntax.getOp stx 1) (Lean.toMessageData "unexpected precedence")
Equations
- Lean.Elab.Term.toParserDescr.processParserCategory stx = let catName := Lean.Name.eraseMacroScopes (Lean.Syntax.getId (Lean.Syntax.getOp stx 0)); do let a ← read let a_1 ← read let _do_jp : PUnit → Lean.Elab.Term.ToParserDescrM Lean.Syntax := fun y => do let prec? ← Lean.Elab.liftMacroM (Lean.Elab.Term.expandOptPrecedence (Lean.Syntax.getOp stx 1)) let prec : Nat := Option.getD prec? 0 let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ParserDescr.cat") (Lean.addMacroScope mainModule `ParserDescr.cat scp) [(`Lean.ParserDescr.cat, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote catName, Lean.quote prec]]) if (a.first && catName == a_1.catName) = true then do let y ← Lean.throwErrorAt stx (Lean.toMessageData "invalid atomic left recursive syntax") _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Elab.Term.toParserDescr.processNullaryOrCat stx = do let a ← Lean.Elab.Term.toParserDescr.resolveParserName (Lean.Syntax.getOp stx 0) match a with | [(c, true)] => do Lean.Elab.Term.toParserDescr.ensureNoPrec stx pure (Lean.mkIdentFrom stx c) | [(c, false)] => do Lean.Elab.Term.toParserDescr.ensureNoPrec stx let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ParserDescr.parser") (Lean.addMacroScope mainModule `ParserDescr.parser scp) [(`Lean.ParserDescr.parser, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote c]]) | cs@h:(x :: x_1 :: x_2) => Lean.throwError (Lean.toMessageData "ambiguous parser declaration " ++ Lean.toMessageData (List.map (fun a => a.fst) cs) ++ Lean.toMessageData "") | [] => let id := Lean.Name.eraseMacroScopes (Lean.Syntax.getId (Lean.Syntax.getOp stx 0)); do let a ← Lean.getEnv if Lean.Parser.isParserCategory a id = true then Lean.Elab.Term.toParserDescr.processParserCategory stx else do let a ← liftM (Lean.Parser.isParserAlias id) if a = true then do Lean.Elab.Term.toParserDescr.ensureNoPrec stx liftM (Lean.Parser.ensureConstantParserAlias id) let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ParserDescr.const") (Lean.addMacroScope mainModule `ParserDescr.const scp) [(`Lean.ParserDescr.const, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote id]]) else Lean.throwError (Lean.toMessageData "unknown parser declaration/category/alias '" ++ Lean.toMessageData id ++ Lean.toMessageData "'")
Equations
- Lean.Elab.Term.toParserDescr.isValidAtom s = (!String.isEmpty s && String.getOp s 0 != Char.ofNat 39 && String.getOp s 0 != Char.ofNat 34 && !(String.getOp s 0 == Char.ofNat 96 && (String.bsize s == 1 || Lean.isIdFirst (String.getOp s 1) || Lean.isIdBeginEscape (String.getOp s 1))) && !Char.isDigit (String.getOp s 0))
Equations
- Lean.Elab.Term.toParserDescr.processAtom stx = match Lean.Syntax.isStrLit? (Lean.Syntax.getOp stx 0) with | some atom => let _do_jp := fun y => do let a ← read let a_1 ← read if (a.behavior != Lean.Parser.LeadingIdentBehavior.default && a_1.first) = true then do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ParserDescr.nonReservedSymbol") (Lean.addMacroScope mainModule `ParserDescr.nonReservedSymbol scp) [(`Lean.ParserDescr.nonReservedSymbol, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote atom, Lean.Syntax.ident info (String.toSubstring "false") (Lean.addMacroScope mainModule `false scp) [(`Bool.false, [])]]]) else do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ParserDescr.symbol") (Lean.addMacroScope mainModule `ParserDescr.symbol scp) [(`Lean.ParserDescr.symbol, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote atom]]); if Lean.Elab.Term.toParserDescr.isValidAtom atom = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwErrorAt stx (Lean.toMessageData "invalid atom") _do_jp y | none => Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Term.toParserDescr.processNonReserved stx = match Lean.Syntax.isStrLit? (Lean.Syntax.getOp stx 1) with | some atom => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ParserDescr.nonReservedSymbol") (Lean.addMacroScope mainModule `ParserDescr.nonReservedSymbol scp) [(`Lean.ParserDescr.nonReservedSymbol, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote atom, Lean.Syntax.ident info (String.toSubstring "false") (Lean.addMacroScope mainModule `false scp) [(`Bool.false, [])]]]) | none => Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Command.elabDeclareSyntaxCat stx = let catName := Lean.Syntax.getId (Lean.Syntax.getOp stx 1); let catBehavior := if Lean.Syntax.isNone (Lean.Syntax.getOp stx 2) = true then Lean.Parser.LeadingIdentBehavior.default else if (Lean.Syntax.getKind (Lean.Syntax.getOp (Lean.Syntax.getOp stx 2) 3) == `Lean.Parser.Command.catBehaviorBoth) = true then Lean.Parser.LeadingIdentBehavior.both else Lean.Parser.LeadingIdentBehavior.symbol; let attrName := Lean.Name.appendAfter catName "Parser"; do let env ← Lean.getEnv let env ← liftM (Lean.Parser.registerParserCategory env attrName catName catBehavior) Lean.setEnv env Lean.Elab.Command.declareSyntaxCatQuotParser catName
Equations
- Lean.Elab.Command.mkNameFromParserSyntax catName stx = (fun visit appendCatName => Lean.Elab.mkUnusedBaseName (Lean.Name.mkSimple (appendCatName (visit stx "")))) Lean.Elab.Command.mkNameFromParserSyntax.visit (Lean.Elab.Command.mkNameFromParserSyntax.appendCatName catName)
Equations
- Lean.Elab.Command.mkNameFromParserSyntax.appendCatName catName str = match catName with | Lean.Name.str x s x_1 => s ++ str | x => str
Equations
- Lean.Elab.Command.resolveSyntaxKind k = do let a ← Lean.getCurrNamespace HOrElse.hOrElse (Lean.Elab.checkSyntaxNodeKindAtNamespaces k a) fun x => Lean.throwError (Lean.toMessageData "invalid syntax node kind '" ++ Lean.toMessageData k ++ Lean.toMessageData "'")
Equations
- Lean.Elab.Command.elabSyntax stx = do let discr ← pure stx let discr_1 : Lean.Syntax := discr if Lean.Syntax.isOfKind discr_1 `Lean.Parser.Command.syntax = true then let discr := Lean.Syntax.getArg discr_1 0; let yes := fun x doc? => let discr := Lean.Syntax.getArg discr_1 1; cond (Lean.Syntax.isOfKind discr `Lean.Parser.Term.attrKind) (let discr_2 := Lean.Syntax.getArg discr_1 2; let discr_3 := Lean.Syntax.getArg discr_1 3; let yes := fun x prec? => let discr_4 := Lean.Syntax.getArg discr_1 4; let yes := fun x name? => let discr_5 := Lean.Syntax.getArg discr_1 5; let yes := fun x prio? => let discr_6 := Lean.Syntax.getArg discr_1 6; match OptionM.run (Array.sequenceMap (Lean.Syntax.getArgs discr_6) fun x => let discr := x; let ps := discr; some ps) with | some ps => let discr_7 := Lean.Syntax.getArg discr_1 7; let discr_8 := Lean.Syntax.getArg discr_1 8; let catStx := discr_8; let attrKind := discr; let cat := Lean.Name.eraseMacroScopes (Lean.Syntax.getId catStx); do let a ← Lean.getEnv let _do_jp : PUnit → Lean.Elab.Command.CommandElabM Unit := fun y => let syntaxParser := Lean.mkNullNode ps; let precDefault := if Lean.Elab.Command.isAtomLikeSyntax syntaxParser = true then Lean.Parser.maxPrec else Lean.Parser.leadPrec; let _do_jp := fun prec => let _do_jp := fun name => do let prio ← Lean.Elab.liftMacroM (Lean.evalOptPrio prio?) let a ← Lean.getCurrNamespace let stxNodeKind : Lean.Name := a ++ name let catParserId : Lean.Syntax := Lean.mkIdentFrom stx (Lean.Name.appendAfter cat "Parser") let discr ← Lean.Elab.Command.runTermElabM none fun x => Lean.Elab.Term.toParserDescr syntaxParser cat let x : Lean.Syntax × Option Nat := discr match x with | (val, lhsPrec?) => let declName := Lean.mkIdentFrom stx name; let _do_jp := fun d => do Lean.Elab.trace `Elab fun x => Lean.MessageData.ofSyntax d Lean.Elab.Command.withMacroExpansion stx d (Lean.Elab.Command.elabCommand d); match lhsPrec? with | some lhsPrec => do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declaration #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declModifiers #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match doc? with | some doc? => #[doc?] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attributes #[Lean.Syntax.atom info "@[", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrInstance #[attrKind, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Attr.simple #[catParserId, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote prio]]]], Lean.Syntax.atom info "]"]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.def #[Lean.Syntax.atom info "def", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declId #[declName, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.optDeclSig #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Lean.TrailingParserDescr") (Lean.addMacroScope mainModule `Lean.TrailingParserDescr scp) [(`Lean.TrailingParserDescr, [])]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ParserDescr.trailingNode") (Lean.addMacroScope mainModule `ParserDescr.trailingNode scp) [(`Lean.ParserDescr.trailingNode, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote stxNodeKind, Lean.quote prec, Lean.quote lhsPrec, val]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]) _do_jp y | x => do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declaration #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declModifiers #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match doc? with | some doc? => #[doc?] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attributes #[Lean.Syntax.atom info "@[", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrInstance #[attrKind, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Attr.simple #[catParserId, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote prio]]]], Lean.Syntax.atom info "]"]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.def #[Lean.Syntax.atom info "def", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declId #[declName, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.optDeclSig #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Lean.ParserDescr") (Lean.addMacroScope mainModule `Lean.ParserDescr scp) [(`Lean.ParserDescr, [])]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ParserDescr.node") (Lean.addMacroScope mainModule `ParserDescr.node scp) [(`Lean.ParserDescr.node, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote stxNodeKind, Lean.quote prec, val]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]) _do_jp y; match name? with | some name => do let y ← pure (Lean.Syntax.getId name) _do_jp y | none => do let y ← Lean.Elab.liftMacroM (Lean.Elab.Command.mkNameFromParserSyntax cat syntaxParser) _do_jp y; match prec? with | some prec => do let y ← Lean.Elab.liftMacroM (Lean.evalPrec prec) _do_jp y | none => do let y ← pure precDefault _do_jp y if Lean.Parser.isParserCategory a cat = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwErrorAt catStx (Lean.toMessageData "unknown category '" ++ Lean.toMessageData cat ++ Lean.toMessageData "'") _do_jp y | none => let discr := Lean.Syntax.getArg discr_1 6; let discr := Lean.Syntax.getArg discr_1 7; let discr := Lean.Syntax.getArg discr_1 8; Lean.Elab.throwUnsupportedSyntax; if Lean.Syntax.isNone discr_5 = true then yes () none else let discr := discr_5; if Lean.Syntax.matchesNull discr 1 = true then let discr_6 := Lean.Syntax.getArg discr 0; if Lean.Syntax.isOfKind discr_6 `Lean.Parser.Command.namedPrio = true then let discr := Lean.Syntax.getArg discr_6 0; let discr := Lean.Syntax.getArg discr_6 1; let discr := Lean.Syntax.getArg discr_6 2; let discr := Lean.Syntax.getArg discr_6 3; let discr_7 := Lean.Syntax.getArg discr_6 4; let prio? := discr; yes () (some prio?) else let discr := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr_1 5; let discr := Lean.Syntax.getArg discr_1 6; let discr := Lean.Syntax.getArg discr_1 7; let discr := Lean.Syntax.getArg discr_1 8; Lean.Elab.throwUnsupportedSyntax else let discr := discr_5; let discr := Lean.Syntax.getArg discr_1 5; let discr := Lean.Syntax.getArg discr_1 6; let discr := Lean.Syntax.getArg discr_1 7; let discr := Lean.Syntax.getArg discr_1 8; Lean.Elab.throwUnsupportedSyntax; if Lean.Syntax.isNone discr_4 = true then yes () none else let discr := discr_4; if Lean.Syntax.matchesNull discr 1 = true then let discr_5 := Lean.Syntax.getArg discr 0; if Lean.Syntax.isOfKind discr_5 `Lean.Parser.Command.namedName = true then let discr := Lean.Syntax.getArg discr_5 0; let discr := Lean.Syntax.getArg discr_5 1; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_5 3; let discr_6 := Lean.Syntax.getArg discr_5 4; let name? := discr; yes () (some name?) else let discr := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr_1 4; let discr := Lean.Syntax.getArg discr_1 5; let discr := Lean.Syntax.getArg discr_1 6; let discr := Lean.Syntax.getArg discr_1 7; let discr := Lean.Syntax.getArg discr_1 8; Lean.Elab.throwUnsupportedSyntax else let discr := discr_4; let discr := Lean.Syntax.getArg discr_1 4; let discr := Lean.Syntax.getArg discr_1 5; let discr := Lean.Syntax.getArg discr_1 6; let discr := Lean.Syntax.getArg discr_1 7; let discr := Lean.Syntax.getArg discr_1 8; Lean.Elab.throwUnsupportedSyntax; if Lean.Syntax.isNone discr_3 = true then yes () none else let discr := discr_3; if Lean.Syntax.matchesNull discr 1 = true then let discr_4 := Lean.Syntax.getArg discr 0; if Lean.Syntax.isOfKind discr_4 `Lean.Parser.precedence = true then let discr := Lean.Syntax.getArg discr_4 0; let discr := Lean.Syntax.getArg discr_4 1; let prec? := discr; yes () (some prec?) else let discr := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr_1 3; let discr := Lean.Syntax.getArg discr_1 4; let discr := Lean.Syntax.getArg discr_1 5; let discr := Lean.Syntax.getArg discr_1 6; let discr := Lean.Syntax.getArg discr_1 7; let discr := Lean.Syntax.getArg discr_1 8; Lean.Elab.throwUnsupportedSyntax else let discr := discr_3; let discr := Lean.Syntax.getArg discr_1 3; let discr := Lean.Syntax.getArg discr_1 4; let discr := Lean.Syntax.getArg discr_1 5; let discr := Lean.Syntax.getArg discr_1 6; let discr := Lean.Syntax.getArg discr_1 7; let discr := Lean.Syntax.getArg discr_1 8; Lean.Elab.throwUnsupportedSyntax) (let discr := Lean.Syntax.getArg discr_1 1; let discr := Lean.Syntax.getArg discr_1 2; let discr := Lean.Syntax.getArg discr_1 3; let discr := Lean.Syntax.getArg discr_1 4; let discr := Lean.Syntax.getArg discr_1 5; let discr := Lean.Syntax.getArg discr_1 6; let discr := Lean.Syntax.getArg discr_1 7; let discr := Lean.Syntax.getArg discr_1 8; Lean.Elab.throwUnsupportedSyntax); if Lean.Syntax.isNone discr = true then yes () none else let discr_2 := discr; if Lean.Syntax.matchesNull discr_2 1 = true then let discr := Lean.Syntax.getArg discr_2 0; cond (Lean.Syntax.isOfKind discr `Lean.Parser.Command.docComment) (let doc? := discr; yes () (some doc?)) (let discr := Lean.Syntax.getArg discr_2 0; let discr := Lean.Syntax.getArg discr_1 0; let discr := Lean.Syntax.getArg discr_1 1; let discr := Lean.Syntax.getArg discr_1 2; let discr := Lean.Syntax.getArg discr_1 3; let discr := Lean.Syntax.getArg discr_1 4; let discr := Lean.Syntax.getArg discr_1 5; let discr := Lean.Syntax.getArg discr_1 6; let discr := Lean.Syntax.getArg discr_1 7; let discr := Lean.Syntax.getArg discr_1 8; Lean.Elab.throwUnsupportedSyntax) else let discr := discr; let discr := Lean.Syntax.getArg discr_1 0; let discr := Lean.Syntax.getArg discr_1 1; let discr := Lean.Syntax.getArg discr_1 2; let discr := Lean.Syntax.getArg discr_1 3; let discr := Lean.Syntax.getArg discr_1 4; let discr := Lean.Syntax.getArg discr_1 5; let discr := Lean.Syntax.getArg discr_1 6; let discr := Lean.Syntax.getArg discr_1 7; let discr := Lean.Syntax.getArg discr_1 8; Lean.Elab.throwUnsupportedSyntax else let discr := discr; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Command.elabSyntaxAbbrev stx = do let discr ← pure stx let discr_1 : Lean.Syntax := discr if Lean.Syntax.isOfKind discr_1 `Lean.Parser.Command.syntaxAbbrev = true then let discr := Lean.Syntax.getArg discr_1 0; let yes := fun x doc? => let discr := Lean.Syntax.getArg discr_1 1; let discr := Lean.Syntax.getArg discr_1 2; cond (Lean.Syntax.isOfKind discr `ident) (let discr_2 := Lean.Syntax.getArg discr_1 3; let discr_3 := Lean.Syntax.getArg discr_1 4; match OptionM.run (Array.sequenceMap (Lean.Syntax.getArgs discr_3) fun x => let discr := x; let ps := discr; some ps) with | some ps => let declName := discr; do let discr ← Lean.Elab.Command.runTermElabM none fun x => Lean.Elab.Term.toParserDescr (Lean.mkNullNode ps) Lean.Name.anonymous let x : Lean.Syntax × Option Nat := discr match x with | (val, x) => do let a ← Lean.getCurrNamespace let stxNodeKind : Lean.Name := a ++ Lean.Syntax.getId declName let stx' ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declaration #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declModifiers #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match doc? with | some doc? => #[doc?] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.def #[Lean.Syntax.atom info "def", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declId #[declName, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.optDeclSig #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Lean.ParserDescr") (Lean.addMacroScope mainModule `Lean.ParserDescr scp) [(`Lean.ParserDescr, [])]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ParserDescr.nodeWithAntiquot") (Lean.addMacroScope mainModule `ParserDescr.nodeWithAntiquot scp) [(`Lean.ParserDescr.nodeWithAntiquot, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote (toString (Lean.Syntax.getId declName)), Lean.quote stxNodeKind, val]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]) Lean.Elab.Command.withMacroExpansion stx stx' (Lean.Elab.Command.elabCommand stx') | none => let discr := Lean.Syntax.getArg discr_1 4; Lean.Elab.throwUnsupportedSyntax) (let discr := Lean.Syntax.getArg discr_1 2; let discr := Lean.Syntax.getArg discr_1 3; let discr := Lean.Syntax.getArg discr_1 4; Lean.Elab.throwUnsupportedSyntax); if Lean.Syntax.isNone discr = true then yes () none else let discr_2 := discr; if Lean.Syntax.matchesNull discr_2 1 = true then let discr := Lean.Syntax.getArg discr_2 0; cond (Lean.Syntax.isOfKind discr `Lean.Parser.Command.docComment) (let doc? := discr; yes () (some doc?)) (let discr := Lean.Syntax.getArg discr_2 0; let discr := Lean.Syntax.getArg discr_1 0; let discr := Lean.Syntax.getArg discr_1 1; let discr := Lean.Syntax.getArg discr_1 2; let discr := Lean.Syntax.getArg discr_1 3; let discr := Lean.Syntax.getArg discr_1 4; Lean.Elab.throwUnsupportedSyntax) else let discr := discr; let discr := Lean.Syntax.getArg discr_1 0; let discr := Lean.Syntax.getArg discr_1 1; let discr := Lean.Syntax.getArg discr_1 2; let discr := Lean.Syntax.getArg discr_1 3; let discr := Lean.Syntax.getArg discr_1 4; Lean.Elab.throwUnsupportedSyntax else let discr := discr; Lean.Elab.throwUnsupportedSyntax
def
Lean.Elab.Command.checkRuleKind
(given : Lean.SyntaxNodeKind)
(expected : Lean.SyntaxNodeKind)
:
Equations
- Lean.Elab.Command.inferMacroRulesAltKind x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.matchAlt = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 1 = true then let discr_3 := Lean.Syntax.getArg discr_2 0; let discr_4 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; let rhs := discr; let pat := discr_3; let _do_jp := fun y => let quoted := Lean.Syntax.getQuotContent pat; pure (Lean.Syntax.getKind quoted); if (!Lean.Syntax.isQuot pat) = true then do let y ← Lean.Elab.throwUnsupportedSyntax _do_jp y else do let y ← pure PUnit.unit _do_jp y else let discr_3 := Lean.Syntax.getArg discr 1; let discr_4 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; Lean.Elab.throwUnsupportedSyntax else let discr := x; Lean.Elab.throwUnsupportedSyntax
def
Lean.Elab.Command.expandNoKindMacroRulesAux
(alts : Array Lean.Syntax)
(cmdName : String)
(mkCmd : Option Lean.Name → Array Lean.Syntax → Lean.Elab.Command.CommandElabM Lean.Syntax)
:
Equations
- Lean.Elab.Command.expandNoKindMacroRulesAux alts cmdName mkCmd = do let k ← Lean.Elab.Command.inferMacroRulesAltKind (Array.getOp alts 0) let _do_jp : Lean.SyntaxNodeKind → PUnit → Lean.Elab.Command.CommandElabM Lean.Syntax := fun k y => if (k == Lean.choiceKind) = true then Lean.throwErrorAt (Array.getOp alts 0) (Lean.toMessageData "invalid " ++ Lean.toMessageData cmdName ++ Lean.toMessageData " alternative, multiple interpretations for pattern (solution: specify node kind using `" ++ Lean.toMessageData cmdName ++ Lean.toMessageData " (kind := ...) ...`)") else do let altsK ← Array.filterM (fun alt => do let a ← Lean.Elab.Command.inferMacroRulesAltKind alt pure (Lean.Elab.Command.checkRuleKind a k)) alts 0 (Array.size alts) let altsNotK ← Array.filterM (fun alt => do let a ← Lean.Elab.Command.inferMacroRulesAltKind alt pure !Lean.Elab.Command.checkRuleKind a k) alts 0 (Array.size alts) if Array.isEmpty altsNotK = true then mkCmd (some k) altsK else do let a ← mkCmd (some k) altsK let a_1 ← mkCmd none altsNotK pure (Lean.mkNullNode #[a, a_1]) if (Lean.Name.isStr k && Lean.Name.getString! k == "antiquot") = true then let k := Lean.Name.getPrefix k; do let y ← pure PUnit.unit _do_jp k y else do let y ← pure PUnit.unit _do_jp k y
Equations
- Lean.Elab.Command.strLitToPattern stx = match Lean.Syntax.isStrLit? stx with | some str => pure (Lean.mkAtomFrom stx str) | none => Lean.Macro.throwUnsupported