def
Lean.Elab.Command.withExpectedType
(expectedType? : Option Lean.Expr)
(x : Lean.Expr → Lean.Elab.TermElabM Lean.Expr)
:
Equations
- Lean.Elab.Command.withExpectedType expectedType? x = do Lean.Elab.Term.tryPostponeIfNoneOrMVar expectedType? let discr ← pure expectedType? match discr with | some expectedType => x expectedType | x => Lean.throwError (Lean.toMessageData "expected type must be known")
def
Lean.Elab.Command.elabElabRulesAux
(doc? : Option Lean.Syntax)
(attrKind : Lean.Syntax)
(k : Lean.SyntaxNodeKind)
(cat? : Option Lean.Syntax)
(expty? : Option Lean.Syntax)
(alts : Array Lean.Syntax)
:
Equations
-
Lean.Elab.Command.elabElabRulesAux doc? attrKind k cat? expty? 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 elab_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 elab_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 _do_jp : Lean.Name → Lean.Elab.Command.CommandElabM Lean.Syntax := fun catName =>
match expty? with
| some expId =>
if (catName == `term) = true then do
let a ← Lean.mkIdentFromRef k
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
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind
#[Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Attr.simple
#[Lean.Syntax.ident info (String.toSubstring "termElab")
(Lean.addMacroScope mainModule `termElab scp) [],
Lean.Syntax.node Lean.SourceInfo.none `null #[a]]]],
Lean.Syntax.atom info "]"]],
Lean.Syntax.atom info "aux_def",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.ident info (String.toSubstring "elabRules")
(Lean.addMacroScope mainModule `elabRules scp) [],
Lean.mkIdent k],
Lean.Syntax.atom info ":",
Lean.Syntax.ident info (String.toSubstring "Lean.Elab.Term.TermElab")
(Lean.addMacroScope mainModule `Lean.Elab.Term.TermElab scp) [(`Lean.Elab.Term.TermElab, [])],
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
#[Lean.Syntax.ident info (String.toSubstring "stx") (Lean.addMacroScope mainModule `stx scp)
[],
Lean.Syntax.ident info (String.toSubstring "expectedType?")
(Lean.addMacroScope mainModule `expectedType? scp) []],
Lean.Syntax.atom info "=>",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app
#[Lean.Syntax.ident info (String.toSubstring "Lean.Elab.Command.withExpectedType")
(Lean.addMacroScope mainModule `Lean.Elab.Command.withExpectedType scp)
[(`Lean.Elab.Command.withExpectedType, [])],
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.ident info (String.toSubstring "expectedType?")
(Lean.addMacroScope mainModule `expectedType? scp) [],
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 #[expId],
Lean.Syntax.atom info "=>",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.match
#[Lean.Syntax.atom info "match",
Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr
#[Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.ident info (String.toSubstring "stx")
(Lean.addMacroScope mainModule `stx scp) []]],
Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.atom info "with",
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.ident info
(String.toSubstring "throwUnsupportedSyntax")
(Lean.addMacroScope mainModule `throwUnsupportedSyntax scp)
[(`Lean.Elab.throwUnsupportedSyntax, [])]]))]]]]]]]]])
else
Lean.throwErrorAt expId
(Lean.toMessageData "syntax category '" ++ Lean.toMessageData catName ++ Lean.toMessageData "' does not support expected type specification")
| x =>
if (catName == `term) = true then do
let a ← Lean.mkIdentFromRef k
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
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind
#[Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Attr.simple
#[Lean.Syntax.ident info (String.toSubstring "termElab")
(Lean.addMacroScope mainModule `termElab scp) [],
Lean.Syntax.node Lean.SourceInfo.none `null #[a]]]],
Lean.Syntax.atom info "]"]],
Lean.Syntax.atom info "aux_def",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.ident info (String.toSubstring "elabRules")
(Lean.addMacroScope mainModule `elabRules scp) [],
Lean.mkIdent k],
Lean.Syntax.atom info ":",
Lean.Syntax.ident info (String.toSubstring "Lean.Elab.Term.TermElab")
(Lean.addMacroScope mainModule `Lean.Elab.Term.TermElab scp) [(`Lean.Elab.Term.TermElab, [])],
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
#[Lean.Syntax.ident info (String.toSubstring "stx") (Lean.addMacroScope mainModule `stx scp)
[],
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.match
#[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr
#[Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.ident info (String.toSubstring "stx")
(Lean.addMacroScope mainModule `stx scp) []]],
Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with",
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.ident info (String.toSubstring "throwUnsupportedSyntax")
(Lean.addMacroScope mainModule `throwUnsupportedSyntax scp)
[(`Lean.Elab.throwUnsupportedSyntax, [])]]))]]]]])
else
if (catName == `command) = true then do
let a ← Lean.mkIdentFromRef k
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
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind
#[Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Attr.simple
#[Lean.Syntax.ident info (String.toSubstring "commandElab")
(Lean.addMacroScope mainModule `commandElab scp) [],
Lean.Syntax.node Lean.SourceInfo.none `null #[a]]]],
Lean.Syntax.atom info "]"]],
Lean.Syntax.atom info "aux_def",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.ident info (String.toSubstring "elabRules")
(Lean.addMacroScope mainModule `elabRules scp) [],
Lean.mkIdent k],
Lean.Syntax.atom info ":",
Lean.Syntax.ident info (String.toSubstring "Lean.Elab.Command.CommandElab")
(Lean.addMacroScope mainModule `Lean.Elab.Command.CommandElab scp)
[(`Lean.Elab.Command.CommandElab, [])],
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.ident info (String.toSubstring "throwUnsupportedSyntax")
(Lean.addMacroScope mainModule `throwUnsupportedSyntax scp)
[(`Lean.Elab.throwUnsupportedSyntax, [])]]))]]])
else
if (catName == `tactic) = true then do
let a ← Lean.mkIdentFromRef k
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
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.attrKind
#[Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Attr.simple
#[Lean.Syntax.ident info (String.toSubstring "tactic")
(Lean.addMacroScope mainModule `tactic scp) [],
Lean.Syntax.node Lean.SourceInfo.none `null #[a]]]],
Lean.Syntax.atom info "]"]],
Lean.Syntax.atom info "aux_def",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.ident info (String.toSubstring "elabRules")
(Lean.addMacroScope mainModule `elabRules scp) [],
Lean.mkIdent k],
Lean.Syntax.atom info ":",
Lean.Syntax.ident info (String.toSubstring "Lean.Elab.Tactic.Tactic")
(Lean.addMacroScope mainModule `Lean.Elab.Tactic.Tactic scp) [(`Lean.Elab.Tactic.Tactic, [])],
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.ident info (String.toSubstring "throwUnsupportedSyntax")
(Lean.addMacroScope mainModule `throwUnsupportedSyntax scp)
[(`Lean.Elab.throwUnsupportedSyntax, [])]]))]]])
else
Lean.throwError
(Lean.toMessageData "unsupported syntax category '" ++ Lean.toMessageData catName ++ Lean.toMessageData "'")
match cat?, expty? with
| some cat, x => do
let y ← pure (Lean.Syntax.getId cat)
_do_jp y
| x, some x_1 => do
let y ← pure `term
_do_jp y
| x, x_1 => do
let y ←
Lean.throwError
(Lean.toMessageData "invalid elab_rules command, specify category using `elab_rules :
...`" ) _do_jp y
Equations
- Lean.Elab.Command.elabElabRules = Lean.Elab.Command.adaptExpander fun stx => let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.elab_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; let yes := fun x cat? => let discr_6 := Lean.Syntax.getArg discr 5; let yes := fun x expty? => let discr_7 := Lean.Syntax.getArg discr 6; if Lean.Syntax.isOfKind discr_7 `Lean.Parser.Term.matchAlts = true then let discr := Lean.Syntax.getArg discr_7 0; let alts := Lean.Syntax.getArgs discr; let attrKind := discr_2; Lean.Elab.Command.expandNoKindMacroRulesAux alts "elab_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.elab_rules #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match doc? with | some doc? => #[doc?] | none => Array.empty)), attrKind, Lean.Syntax.atom info "elab_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 `null (Array.append #[] (match cat? with | some cat? => #[Lean.Syntax.atom info ":", cat?] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match expty? with | some expty? => #[Lean.Syntax.atom info "<=", expty?] | 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 6; Lean.Elab.throwUnsupportedSyntax; 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 := Lean.Syntax.getArg discr_7 0; let discr := Lean.Syntax.getArg discr_7 1; let expty? := discr; yes () (some expty?) else let discr_8 := discr_6; let discr_9 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; Lean.Elab.throwUnsupportedSyntax; if Lean.Syntax.isNone discr_5 = true then yes () none else let discr_6 := discr_5; if Lean.Syntax.matchesNull discr_6 2 = true then let discr := Lean.Syntax.getArg discr_6 0; let discr := Lean.Syntax.getArg discr_6 1; let cat? := discr; yes () (some cat?) else let discr_7 := discr_5; let discr_8 := Lean.Syntax.getArg discr 4; let discr_9 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; 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; let yes := fun x cat? => let discr_12 := Lean.Syntax.getArg discr 5; let yes := fun x expty? => let discr_13 := Lean.Syntax.getArg discr 6; if Lean.Syntax.isOfKind discr_13 `Lean.Parser.Term.matchAlts = true then let discr := Lean.Syntax.getArg discr_13 0; let alts := Lean.Syntax.getArgs discr; let kind := discr_9; let attrKind := discr_2; do let a ← Lean.Elab.Command.resolveSyntaxKind (Lean.Syntax.getId kind) Lean.Elab.Command.elabElabRulesAux doc? attrKind a cat? expty? alts else let discr := Lean.Syntax.getArg discr 6; Lean.Elab.throwUnsupportedSyntax; if Lean.Syntax.isNone discr_12 = true then yes () none else let discr_13 := discr_12; if Lean.Syntax.matchesNull discr_13 2 = true then let discr := Lean.Syntax.getArg discr_13 0; let discr := Lean.Syntax.getArg discr_13 1; let expty? := discr; yes () (some expty?) else let discr_14 := discr_12; let discr_15 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; Lean.Elab.throwUnsupportedSyntax; if Lean.Syntax.isNone discr_11 = true then yes () none else let discr_12 := discr_11; if Lean.Syntax.matchesNull discr_12 2 = true then let discr := Lean.Syntax.getArg discr_12 0; let discr := Lean.Syntax.getArg discr_12 1; let cat? := discr; yes () (some cat?) else let discr_13 := discr_11; let discr_14 := Lean.Syntax.getArg discr 4; let discr_15 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; Lean.Elab.throwUnsupportedSyntax else 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; 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_6 := Lean.Syntax.getArg discr 4; let discr_7 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; 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_9 := Lean.Syntax.getArg discr 4; let discr_10 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; 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_8 := Lean.Syntax.getArg discr 4; let discr_9 := Lean.Syntax.getArg discr 5; let discr := Lean.Syntax.getArg discr 6; Lean.Elab.throwUnsupportedSyntax else let discr := stx; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Command.expandElab x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.elab = 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.elabTail = 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 yes := fun x expectedType? => let discr_10 := Lean.Syntax.getArg discr_8 3; let discr_11 := Lean.Syntax.getArg discr_8 4; let rhs := discr_11; let cat := discr; let args := Lean.Syntax.getArgs discr_7; let attrKind := discr_2; do let prio ← Lean.evalOptPrio prio? let catName : Lean.Name := Lean.Syntax.getId cat 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 info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `null #[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 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], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.elab_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 info "elab_rules", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", cat], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match expectedType? with | some expectedType? => #[Lean.Syntax.atom info "<=", expectedType?] | none => Array.empty)), 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]]]]]); 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; if Lean.Syntax.isNone discr_9 = true then yes () none else let discr := discr_9; if Lean.Syntax.matchesNull discr 2 = true then let discr_10 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let expectedType? := discr; yes () (some expectedType?) else let discr := discr_9; let discr := Lean.Syntax.getArg discr_8 2; let discr := Lean.Syntax.getArg discr_8 3; let discr := Lean.Syntax.getArg discr_8 4; Lean.Macro.throwUnsupported 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