Equations
-
Lean.Elab.Command.expandMacro x = let discr := x;
if Lean.Syntax.isOfKind discr `Lean.Parser.Command.macro = 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;
let yes := fun x prec? =>
let discr_5 := Lean.Syntax.getArg discr 4;
let yes := fun x name? =>
let discr_6 := Lean.Syntax.getArg discr 5;
let yes := fun x prio? =>
let discr_7 := Lean.Syntax.getArg discr 6;
let discr_8 := Lean.Syntax.getArg discr 7;
if Lean.Syntax.isOfKind discr_8 `Lean.Parser.Command.macroTail = true then
let discr := Lean.Syntax.getArg discr_8 0;
let discr := Lean.Syntax.getArg discr_8 1;
let discr_9 := Lean.Syntax.getArg discr_8 2;
let discr_10 := Lean.Syntax.getArg discr_8 3;
let rhs := discr_10;
let cat := discr;
let args := Lean.Syntax.getArgs discr_7;
let tk := discr_3;
let attrKind := discr_2;
do
let prio ← Lean.evalOptPrio prio?
let a ← Array.mapM Lean.Elab.Command.expandMacroArg args
let x : Array Lean.Syntax × Array Lean.Syntax := Array.unzip a
match x with
| (stxParts, patArgs) =>
let _do_jp := fun name => do
let a ← Lean.Macro.getCurrNamespace
let pat : Lean.Syntax := Lean.mkNode (a ++ name) patArgs
let a ← Lean.mkIdentFromRef name
let stxCmd ←
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.syntax
#[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) "syntax",
Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[]
(match prec? with
| some prec? =>
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.precedence
#[Lean.Syntax.atom info ":", prec?]]
| none => Array.empty)),
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedName
#[Lean.Syntax.atom info "(", Lean.Syntax.atom info "name",
Lean.Syntax.atom info ":=", a, Lean.Syntax.atom info ")"]],
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namedPrio
#[Lean.Syntax.atom info "(", Lean.Syntax.atom info "priority",
Lean.Syntax.atom info ":=", Lean.quote prio, Lean.Syntax.atom info ")"]],
Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[] (Array.map (fun stxParts => stxParts) stxParts)),
Lean.Syntax.atom info ":", cat])
let _do_jp : Lean.Syntax → Lean.MacroM Lean.Syntax := fun macroRulesCmd =>
pure (Lean.mkNullNode #[stxCmd, macroRulesCmd])
if (Array.size (Lean.Syntax.getArgs rhs) == 1) = true then
let rhs := Lean.Syntax.getOp rhs 0;
do
let y ←
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)),
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind
#[Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.atom (Option.getD (Lean.Syntax.getHeadInfo? tk) info) "macro_rules",
Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts
#[Lean.Syntax.node Lean.SourceInfo.none `null
#[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.quot
#[Lean.Syntax.atom info "`(", pat, Lean.Syntax.atom info ")"]],
Lean.Syntax.atom info "=>", rhs]]]])
_do_jp y
else
let rhsBody := Lean.Syntax.getOp rhs 1;
do
let y ←
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)),
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind
#[Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.atom (Option.getD (Lean.Syntax.getHeadInfo? tk) info) "macro_rules",
Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts
#[Lean.Syntax.node Lean.SourceInfo.none `null
#[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.quot
#[Lean.Syntax.atom info "`(", pat, Lean.Syntax.atom info ")"]],
Lean.Syntax.atom info "=>",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.quot
#[Lean.Syntax.atom info "`(", rhsBody,
Lean.Syntax.atom info ")"]]]]])
_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.Command.mkNameFromParserSyntax (Lean.Syntax.getId cat) (Lean.mkNullNode stxParts)
_do_jp y
else
let discr := Lean.Syntax.getArg discr 7;
Lean.Macro.throwUnsupported;
if Lean.Syntax.isNone discr_6 = true then yes () none
else
let discr_7 := discr_6;
if Lean.Syntax.matchesNull discr_7 1 = true then
let discr_8 := Lean.Syntax.getArg discr_7 0;
if Lean.Syntax.isOfKind discr_8 `Lean.Parser.Command.namedPrio = true then
let discr := Lean.Syntax.getArg discr_8 0;
let discr := Lean.Syntax.getArg discr_8 1;
let discr := Lean.Syntax.getArg discr_8 2;
let discr := Lean.Syntax.getArg discr_8 3;
let discr_9 := Lean.Syntax.getArg discr_8 4;
let prio? := discr;
yes () (some prio?)
else
let discr_9 := Lean.Syntax.getArg discr_7 0;
let discr_10 := Lean.Syntax.getArg discr 5;
let discr_11 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Macro.throwUnsupported
else
let discr_8 := discr_6;
let discr_9 := Lean.Syntax.getArg discr 5;
let discr_10 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Macro.throwUnsupported;
if Lean.Syntax.isNone discr_5 = true then yes () none
else
let discr_6 := discr_5;
if Lean.Syntax.matchesNull discr_6 1 = true then
let discr_7 := Lean.Syntax.getArg discr_6 0;
if Lean.Syntax.isOfKind discr_7 `Lean.Parser.Command.namedName = true then
let discr := Lean.Syntax.getArg discr_7 0;
let discr := Lean.Syntax.getArg discr_7 1;
let discr := Lean.Syntax.getArg discr_7 2;
let discr := Lean.Syntax.getArg discr_7 3;
let discr_8 := Lean.Syntax.getArg discr_7 4;
let name? := discr;
yes () (some name?)
else
let discr_8 := Lean.Syntax.getArg discr_6 0;
let discr_9 := Lean.Syntax.getArg discr 4;
let discr_10 := Lean.Syntax.getArg discr 5;
let discr_11 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Macro.throwUnsupported
else
let discr_7 := discr_5;
let discr_8 := Lean.Syntax.getArg discr 4;
let discr_9 := Lean.Syntax.getArg discr 5;
let discr_10 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Macro.throwUnsupported;
if Lean.Syntax.isNone discr_4 = true then yes () none
else
let discr_5 := discr_4;
if Lean.Syntax.matchesNull discr_5 1 = true then
let discr_6 := Lean.Syntax.getArg discr_5 0;
if Lean.Syntax.isOfKind discr_6 `Lean.Parser.precedence = true then
let discr := Lean.Syntax.getArg discr_6 0;
let discr := Lean.Syntax.getArg discr_6 1;
let prec? := discr;
yes () (some prec?)
else
let discr_7 := Lean.Syntax.getArg discr_5 0;
let discr_8 := Lean.Syntax.getArg discr 3;
let discr_9 := Lean.Syntax.getArg discr 4;
let discr_10 := Lean.Syntax.getArg discr 5;
let discr_11 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Macro.throwUnsupported
else
let discr_6 := discr_4;
let discr_7 := Lean.Syntax.getArg discr 3;
let discr_8 := Lean.Syntax.getArg discr 4;
let discr_9 := Lean.Syntax.getArg discr 5;
let discr_10 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Macro.throwUnsupported)
(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_8 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Macro.throwUnsupported);
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_9 := Lean.Syntax.getArg discr 4;
let discr_10 := Lean.Syntax.getArg discr 5;
let discr_11 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Macro.throwUnsupported)
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_8 := Lean.Syntax.getArg discr 4;
let discr_9 := Lean.Syntax.getArg discr 5;
let discr_10 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Macro.throwUnsupported
else
let discr := x;
Lean.Macro.throwUnsupported