def
Lean.Elab.Command.elabMacroRulesAux
(doc? : Option Lean.Syntax)
(attrKind : Lean.Syntax)
(tk : Lean.Syntax)
(k : Lean.SyntaxNodeKind)
(alts : Array Lean.Syntax)
:
Equations
- Lean.Elab.Command.elabMacroRulesAux doc? attrKind tk k alts = do let alts ← Array.mapM (fun alt => let discr := alt; 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; let discr_3 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; let rhs := discr; let pats := { elemsAndSeps := Lean.Syntax.getArgs discr_2 }; let pat := Array.getOp pats.elemsAndSeps 0; let _do_jp := fun y => let quoted := Lean.Syntax.getQuotContent pat; let k' := Lean.Syntax.getKind quoted; if Lean.Elab.Command.checkRuleKind k' k = true then pure alt else if (k' == Lean.choiceKind) = true then match Array.find? (Lean.Syntax.getArgs quoted) fun quotAlt => Lean.Elab.Command.checkRuleKind (Lean.Syntax.getKind quotAlt) k with | none => Lean.throwErrorAt alt (Lean.toMessageData "invalid macro_rules alternative, expected syntax node kind '" ++ Lean.toMessageData k ++ Lean.toMessageData "'") | some quoted => let pat := Lean.Syntax.setArg pat 1 quoted; let pats := Array.set! pats.elemsAndSeps 0 pat; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.Syntax.SepArray.ofElems pats).elemsAndSeps), Lean.Syntax.atom info "=>", rhs]) else Lean.throwErrorAt alt (Lean.toMessageData "invalid macro_rules alternative, unexpected syntax node kind '" ++ Lean.toMessageData k' ++ Lean.toMessageData "'"); 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 := alt; Lean.Elab.throwUnsupportedSyntax) alts let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Elab.Command.aux_def #[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.macro #[Lean.Syntax.atom info "macro", Lean.mkIdent k]]], Lean.Syntax.atom info "]"]], Lean.Syntax.atom info "aux_def", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "macroRules") (Lean.addMacroScope mainModule `macroRules scp) [], Lean.mkIdentFrom tk k], Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Macro") (Lean.addMacroScope mainModule `Macro scp) [(`Lean.Macro, [])], Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.push (Array.append #[] alts) (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "throw") (Lean.addMacroScope mainModule `throw scp) [(`MonadExcept.throw, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "Lean.Macro.Exception.unsupportedSyntax") (Lean.addMacroScope mainModule `Lean.Macro.Exception.unsupportedSyntax scp) [(`Lean.Macro.Exception.unsupportedSyntax, [])]]]]))]]])
Equations
- Lean.Elab.Command.elabMacroRules = Lean.Elab.Command.adaptExpander fun stx => let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.macro_rules = true then let discr_1 := Lean.Syntax.getArg discr 0; let yes := fun x doc? => let discr_2 := Lean.Syntax.getArg discr 1; cond (Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.attrKind) (let discr_3 := Lean.Syntax.getArg discr 2; let discr_4 := Lean.Syntax.getArg discr 3; if Lean.Syntax.matchesNull discr_4 0 = true then let discr_5 := Lean.Syntax.getArg discr 4; if Lean.Syntax.isOfKind discr_5 `Lean.Parser.Term.matchAlts = true then let discr := Lean.Syntax.getArg discr_5 0; let alts := Lean.Syntax.getArgs discr; let tk := discr_3; let attrKind := discr_2; Lean.Elab.Command.expandNoKindMacroRulesAux alts "macro_rules" fun kind? alts => do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.macro_rules #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match doc? with | some doc? => #[doc?] | none => Array.empty)), attrKind, Lean.Syntax.atom (Option.getD (Lean.Syntax.getHeadInfo? tk) info) "macro_rules", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (let a := Lean.mkIdent <$> kind?; match a with | some a => #[Lean.Syntax.atom info "(", Lean.Syntax.atom info "kind", Lean.Syntax.atom info ":=", a, Lean.Syntax.atom info ")"] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] alts)]]) else let discr := Lean.Syntax.getArg discr 4; Lean.Elab.throwUnsupportedSyntax else let discr_5 := Lean.Syntax.getArg discr 3; if Lean.Syntax.matchesNull discr_5 5 = true then let discr_6 := Lean.Syntax.getArg discr_5 0; let discr_7 := Lean.Syntax.getArg discr_5 1; let discr_8 := Lean.Syntax.getArg discr_5 2; let discr_9 := Lean.Syntax.getArg discr_5 3; let discr_10 := Lean.Syntax.getArg discr_5 4; let discr_11 := Lean.Syntax.getArg discr 4; if Lean.Syntax.isOfKind discr_11 `Lean.Parser.Term.matchAlts = true then let discr := Lean.Syntax.getArg discr_11 0; if Lean.Syntax.matchesNull discr 1 = true then let discr_12 := Lean.Syntax.getArg discr 0; if Lean.Syntax.isOfKind discr_12 `Lean.Parser.Term.matchAlt = true then let discr_13 := Lean.Syntax.getArg discr_12 0; let discr_14 := Lean.Syntax.getArg discr_12 1; if Lean.Syntax.matchesNull discr_14 1 = true then let discr_15 := Lean.Syntax.getArg discr_14 0; cond (Lean.Syntax.isOfKind discr_15 `ident) (let discr := Lean.Syntax.getArg discr_12 2; let discr := Lean.Syntax.getArg discr_12 3; let rhs := discr; let x := discr_15; let kind := discr_9; let tk := discr_3; let attrKind := discr_2; do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Elab.Command.aux_def #[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.macro #[Lean.Syntax.atom info "macro", kind]]], Lean.Syntax.atom info "]"]], Lean.Syntax.atom info "aux_def", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.mkIdentFrom tk (Lean.Syntax.getId kind), kind], Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Macro") (Lean.addMacroScope mainModule `Macro scp) [(`Lean.Macro, [])], Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[x], Lean.Syntax.atom info "=>", rhs]]])) (let discr_16 := Lean.Syntax.getArg discr_14 0; let discr_17 := Lean.Syntax.getArg discr_12 2; let discr_18 := Lean.Syntax.getArg discr_12 3; let alts := Lean.Syntax.getArgs discr; let kind := discr_9; let tk := discr_3; let attrKind := discr_2; do let a ← Lean.Elab.Command.resolveSyntaxKind (Lean.Syntax.getId kind) Lean.Elab.Command.elabMacroRulesAux doc? attrKind tk a alts) else let discr_15 := Lean.Syntax.getArg discr_12 1; let discr_16 := Lean.Syntax.getArg discr_12 2; let discr_17 := Lean.Syntax.getArg discr_12 3; let alts := Lean.Syntax.getArgs discr; let kind := discr_9; let tk := discr_3; let attrKind := discr_2; do let a ← Lean.Elab.Command.resolveSyntaxKind (Lean.Syntax.getId kind) Lean.Elab.Command.elabMacroRulesAux doc? attrKind tk a alts else let discr_13 := Lean.Syntax.getArg discr 0; let alts := Lean.Syntax.getArgs discr; let kind := discr_9; let tk := discr_3; let attrKind := discr_2; do let a ← Lean.Elab.Command.resolveSyntaxKind (Lean.Syntax.getId kind) Lean.Elab.Command.elabMacroRulesAux doc? attrKind tk a alts else let discr := Lean.Syntax.getArg discr_11 0; let alts := Lean.Syntax.getArgs discr; let kind := discr_9; let tk := discr_3; let attrKind := discr_2; do let a ← Lean.Elab.Command.resolveSyntaxKind (Lean.Syntax.getId kind) Lean.Elab.Command.elabMacroRulesAux doc? attrKind tk a alts else let discr := Lean.Syntax.getArg discr 4; Lean.Elab.throwUnsupportedSyntax else let discr_6 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; Lean.Elab.throwUnsupportedSyntax) (let discr_3 := Lean.Syntax.getArg discr 1; let discr_4 := Lean.Syntax.getArg discr 2; let discr_5 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; Lean.Elab.throwUnsupportedSyntax); if Lean.Syntax.isNone discr_1 = true then yes () none else let discr_2 := discr_1; if Lean.Syntax.matchesNull discr_2 1 = true then let discr_3 := Lean.Syntax.getArg discr_2 0; cond (Lean.Syntax.isOfKind discr_3 `Lean.Parser.Command.docComment) (let doc? := discr_3; yes () (some doc?)) (let discr_4 := Lean.Syntax.getArg discr_2 0; let discr_5 := Lean.Syntax.getArg discr 0; let discr_6 := Lean.Syntax.getArg discr 1; let discr_7 := Lean.Syntax.getArg discr 2; let discr_8 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; Lean.Elab.throwUnsupportedSyntax) else let discr_3 := discr_1; let discr_4 := Lean.Syntax.getArg discr 0; let discr_5 := Lean.Syntax.getArg discr 1; let discr_6 := Lean.Syntax.getArg discr 2; let discr_7 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; Lean.Elab.throwUnsupportedSyntax else let discr := stx; Lean.Elab.throwUnsupportedSyntax