Equations
- Lean.Elab.Command.expandMacroArg stx = (fun mkSplicePat => do let a ← Lean.expandMacros stx let _do_jp : Option Lean.Syntax × Lean.Syntax × Lean.Syntax → Lean.MacroM (Lean.Syntax × Lean.Syntax) := fun discr => let x := discr; match x with | (id?, id, stx) => let _do_jp := fun pat => pure (stx, pat); let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Syntax.atom = true then let discr_1 := Lean.Syntax.getArg discr 0; cond (Lean.Syntax.isOfKind discr_1 `strLit) (let s := discr_1; do let a ← Lean.Elab.Command.strLitToPattern s let y ← pure (Lean.mkNode `token_antiquot #[a, Lean.mkAtom "%", Lean.mkAtom "$", id]) _do_jp y) (let discr := Lean.Syntax.getArg discr 0; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none)) else let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Syntax.nonReserved = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; cond (Lean.Syntax.isOfKind discr_2 `strLit) (let s := discr_2; do let a ← Lean.Elab.Command.strLitToPattern s let y ← pure (Lean.mkNode `token_antiquot #[a, Lean.mkAtom "%", Lean.mkAtom "$", id]) _do_jp y) (let discr := Lean.Syntax.getArg discr 1; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none)) else let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Syntax.unary = true then let discr_1 := Lean.Syntax.getArg discr 0; if Lean.Syntax.matchesIdent discr_1 `optional = true then let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; if Lean.Syntax.matchesNull discr_3 1 = true then let discr_4 := Lean.Syntax.getArg discr_3 0; let discr := Lean.Syntax.getArg discr 3; let stx := discr_4; do let y ← pure (mkSplicePat `optional id "?") _do_jp y else let discr_4 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none) else let discr_2 := Lean.Syntax.getArg discr 0; if Lean.Syntax.matchesIdent discr_2 `many = true then let discr_3 := Lean.Syntax.getArg discr 1; let discr_4 := Lean.Syntax.getArg discr 2; if Lean.Syntax.matchesNull discr_4 1 = true then let discr_5 := Lean.Syntax.getArg discr_4 0; let discr := Lean.Syntax.getArg discr 3; let stx := discr_5; do let y ← pure (mkSplicePat `many id "*") _do_jp y else let discr_5 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none) else let discr_3 := Lean.Syntax.getArg discr 0; if Lean.Syntax.matchesIdent discr_3 `many1 = true then let discr_4 := Lean.Syntax.getArg discr 1; let discr_5 := Lean.Syntax.getArg discr 2; if Lean.Syntax.matchesNull discr_5 1 = true then let discr_6 := Lean.Syntax.getArg discr_5 0; let discr := Lean.Syntax.getArg discr 3; let stx := discr_6; do let y ← pure (mkSplicePat `many id "*") _do_jp y else let discr_6 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none) else 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 := Lean.Syntax.getArg discr 3; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none) else let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Syntax.sepBy = 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_5 := Lean.Syntax.getArg discr 3; cond (Lean.Syntax.isOfKind discr_5 `strLit) (let discr_6 := Lean.Syntax.getArg discr 4; let yes := fun x stxsep => let discr_7 := Lean.Syntax.getArg discr 5; let yes := fun x => let discr := Lean.Syntax.getArg discr 6; let sep := discr_5; let stx := discr_3; do let y ← pure (mkSplicePat `sepBy id (Option.get! (Lean.Syntax.isStrLit? sep) ++ "*")) _do_jp y; if Lean.Syntax.isNone discr_7 = true then yes () else let discr_8 := discr_7; if Lean.Syntax.matchesNull discr_8 2 = true then let discr := Lean.Syntax.getArg discr_8 0; let discr := Lean.Syntax.getArg discr_8 1; yes () else let discr_9 := discr_7; let discr_10 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none); if Lean.Syntax.isNone discr_6 = true then yes () none else let discr_7 := discr_6; if Lean.Syntax.matchesNull discr_7 2 = true then let discr_8 := Lean.Syntax.getArg discr_7 0; let discr_9 := Lean.Syntax.getArg discr_7 1; if Lean.Syntax.matchesNull discr_9 1 = true then let discr := Lean.Syntax.getArg discr_9 0; let stxsep := discr; yes () (some stxsep) else let discr_10 := Lean.Syntax.getArg discr_7 1; let discr_11 := Lean.Syntax.getArg discr 4; let discr_12 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none) else let discr_8 := discr_6; let discr_9 := Lean.Syntax.getArg discr 4; let discr_10 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none)) (let discr_6 := Lean.Syntax.getArg discr 3; let discr_7 := Lean.Syntax.getArg discr 4; let discr_8 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none)) else 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_6 := Lean.Syntax.getArg discr 4; let discr_7 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none) else let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Syntax.sepBy1 = 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_5 := Lean.Syntax.getArg discr 3; cond (Lean.Syntax.isOfKind discr_5 `strLit) (let discr_6 := Lean.Syntax.getArg discr 4; let yes := fun x stxsep => let discr_7 := Lean.Syntax.getArg discr 5; let yes := fun x => let discr := Lean.Syntax.getArg discr 6; let sep := discr_5; let stx := discr_3; do let y ← pure (mkSplicePat `sepBy id (Option.get! (Lean.Syntax.isStrLit? sep) ++ "*")) _do_jp y; if Lean.Syntax.isNone discr_7 = true then yes () else let discr_8 := discr_7; if Lean.Syntax.matchesNull discr_8 2 = true then let discr := Lean.Syntax.getArg discr_8 0; let discr := Lean.Syntax.getArg discr_8 1; yes () else let discr_9 := discr_7; let discr_10 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none); if Lean.Syntax.isNone discr_6 = true then yes () none else let discr_7 := discr_6; if Lean.Syntax.matchesNull discr_7 2 = true then let discr_8 := Lean.Syntax.getArg discr_7 0; let discr_9 := Lean.Syntax.getArg discr_7 1; if Lean.Syntax.matchesNull discr_9 1 = true then let discr := Lean.Syntax.getArg discr_9 0; let stxsep := discr; yes () (some stxsep) else let discr_10 := Lean.Syntax.getArg discr_7 1; let discr_11 := Lean.Syntax.getArg discr 4; let discr_12 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none) else let discr_8 := discr_6; let discr_9 := Lean.Syntax.getArg discr 4; let discr_10 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none)) (let discr_6 := Lean.Syntax.getArg discr 3; let discr_7 := Lean.Syntax.getArg discr 4; let discr_8 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none)) else 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_6 := Lean.Syntax.getArg discr 4; let discr_7 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none) else let discr := stx; match id? with | some id => do let y ← pure (Lean.Syntax.mkAntiquotNode id 0 none) _do_jp y | none => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Syntax.unary #[Lean.Syntax.ident info (String.toSubstring "group") (Lean.addMacroScope mainModule `group scp) [], Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx], Lean.Syntax.atom info ")"]) pure (a, Lean.Syntax.mkAntiquotNode id 0 none) let discr : Lean.Syntax := a if Lean.Syntax.isOfKind discr `Lean.Parser.Command.macroArg = true then let discr_1 := Lean.Syntax.getArg discr 0; if Lean.Syntax.matchesNull discr_1 2 = true then let discr_2 := Lean.Syntax.getArg discr_1 0; cond (Lean.Syntax.isOfKind discr_2 `ident) (let discr_3 := Lean.Syntax.getArg discr_1 1; let discr := Lean.Syntax.getArg discr 1; let stx := discr; let id := discr_2; do let y ← pure (some id, id, stx) _do_jp y) (let discr_3 := Lean.Syntax.getArg discr_1 0; let discr_4 := Lean.Syntax.getArg discr_1 1; let discr := Lean.Syntax.getArg discr 1; do let y ← Lean.Macro.throwUnsupported _do_jp y) else let discr_2 := Lean.Syntax.getArg discr 0; if Lean.Syntax.matchesNull discr_2 0 = true then let discr := Lean.Syntax.getArg discr 1; let stx := discr; do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.ident info (String.toSubstring "x") (Lean.addMacroScope mainModule `x scp) []) let y ← pure (none, a, stx) _do_jp y else let discr_3 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; do let y ← Lean.Macro.throwUnsupported _do_jp y else let discr := a; do let y ← Lean.Macro.throwUnsupported _do_jp y) Lean.Elab.Command.expandMacroArg.mkSplicePat
def
Lean.Elab.Command.expandMacroArg.mkSplicePat
(kind : Lean.SyntaxNodeKind)
(id : Lean.Syntax)
(suffix : String)
:
Equations
- Lean.Elab.Command.expandMacroArg.mkSplicePat kind id suffix = Lean.mkNullNode #[Lean.Syntax.mkAntiquotSuffixSpliceNode kind (Lean.Syntax.mkAntiquotNode id 0 none) suffix]