def
Lean.Elab.Term.Quotation.resolveSectionVariable
(sectionVars : Lean.NameMap Lean.Name)
(id : Lean.Name)
:
Equations
- Lean.Elab.Term.Quotation.resolveSectionVariable sectionVars id = let extractionResult := Lean.extractMacroScopes id; (fun loop => loop extractionResult.name []) (Lean.Elab.Term.Quotation.resolveSectionVariable.loop sectionVars extractionResult)
def
Lean.Elab.Term.Quotation.resolveSectionVariable.loop
(sectionVars : Lean.NameMap Lean.Name)
(extractionResult : Lean.MacroScopesView)
:
Equations
- Lean.Elab.Term.Quotation.resolveSectionVariable.loop sectionVars extractionResult (Lean.Name.str p s x_2) x = let id := Lean.MacroScopesView.review { name := Lean.Name.str p s x_2, imported := extractionResult.imported, mainModule := extractionResult.mainModule, scopes := extractionResult.scopes }; match Lean.NameMap.find? sectionVars id with | some newId => [(newId, x)] | none => Lean.Elab.Term.Quotation.resolveSectionVariable.loop sectionVars extractionResult p (s :: x)
- Lean.Elab.Term.Quotation.resolveSectionVariable.loop sectionVars extractionResult x x = []
Equations
- Lean.Elab.Term.Quotation.ArrayStxBuilder.build x = match x with | Sum.inl elems => Lean.quote elems | Sum.inr arr => arr
def
Lean.Elab.Term.Quotation.ArrayStxBuilder.push
(b : Lean.Elab.Term.Quotation.ArrayStxBuilder)
(elem : Lean.Syntax)
:
Equations
- Lean.Elab.Term.Quotation.ArrayStxBuilder.push b elem = match b with | Sum.inl elems => Sum.inl (Array.push elems elem) | Sum.inr arr => Sum.inr (Lean.Syntax.mkCApp `Array.push #[arr, elem])
def
Lean.Elab.Term.Quotation.ArrayStxBuilder.append
(b : Lean.Elab.Term.Quotation.ArrayStxBuilder)
(arr : Lean.Syntax)
(appendName : optParam Lean.Name `Array.append)
:
Equations
- Lean.Elab.Term.Quotation.ArrayStxBuilder.append b arr appendName = Sum.inr (Lean.Syntax.mkCApp appendName #[Lean.Elab.Term.Quotation.ArrayStxBuilder.build b, arr])
Equations
- Lean.Elab.Term.Quotation.stxQuot.expand stx = do let stx ← Lean.Elab.Term.Quotation.quoteSyntax (Lean.Syntax.getQuotContent 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 "Bind.bind") (Lean.addMacroScope mainModule `Bind.bind scp) [(`Bind.bind, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "MonadRef.mkInfoFromRefPos") (Lean.addMacroScope mainModule `MonadRef.mkInfoFromRefPos scp) [(`Lean.MonadRef.mkInfoFromRefPos, [])], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[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 "info") (Lean.addMacroScope mainModule `info scp) []], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Bind.bind") (Lean.addMacroScope mainModule `Bind.bind scp) [(`Bind.bind, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "getCurrMacroScope") (Lean.addMacroScope mainModule `getCurrMacroScope scp) [(`Lean.MonadQuotation.getCurrMacroScope, [])], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[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 "scp") (Lean.addMacroScope mainModule `scp scp) []], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Bind.bind") (Lean.addMacroScope mainModule `Bind.bind scp) [(`Bind.bind, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "getMainModule") (Lean.addMacroScope mainModule `getMainModule scp) [(`Lean.MonadQuotation.getMainModule, [])], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[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 "mainModule") (Lean.addMacroScope mainModule `mainModule scp) []], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[stx]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]])
Equations
- Lean.Elab.Term.Quotation.commandElab_stx_quot__ = Lean.ParserDescr.node `Lean.Elab.Term.Quotation.commandElab_stx_quot__ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "elab_stx_quot") (Lean.ParserDescr.parser `Lean.Parser.Term.ident))
- unconditional: Lean.Elab.Term.Quotation.HeadCheck
- shape: Lean.SyntaxNodeKind → Option Nat → Lean.Elab.Term.Quotation.HeadCheck
- slice: Nat → Nat → Lean.Elab.Term.Quotation.HeadCheck
- other: Lean.Syntax → Lean.Elab.Term.Quotation.HeadCheck
Equations
- Lean.Elab.Term.Quotation.match_syntax.expand stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.match = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 0 = true then let discr_3 := Lean.Syntax.getArg discr 2; match OptionM.run (Array.sequenceMap (Array.getSepElems (Lean.Syntax.getArgs discr_3)) fun x => let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.matchDiscr = true then let discr_4 := Lean.Syntax.getArg discr 0; if Lean.Syntax.matchesNull discr_4 0 = true then let discr := Lean.Syntax.getArg discr 1; let discrs := discr; some discrs else let discr_5 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; none else let discr := x; none) with | some discrs => 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 discr_6 := Lean.Syntax.getArg discr 5; if Lean.Syntax.isOfKind discr_6 `Lean.Parser.Term.matchAlts = true then let discr := Lean.Syntax.getArg discr_6 0; match OptionM.run (Array.sequenceMap (Lean.Syntax.getArgs discr) fun x => let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.matchAlt = true then let discr_7 := Lean.Syntax.getArg discr 0; let discr_8 := Lean.Syntax.getArg discr 1; match OptionM.run (Array.sequenceMap (Array.getSepElems (Lean.Syntax.getArgs discr_8)) fun x => let discr := x; let patss := discr; some patss) with | some patss => let discr_9 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; let rhss := discr; some (patss, rhss) | none => let discr_9 := Lean.Syntax.getArg discr 1; let discr_10 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; none else let discr := x; none) with | some tuples => let rhss := Array.map (fun x => match x with | (patss, rhss) => rhss) tuples; let patss := Array.map (fun x => match x with | (patss, rhss) => patss) tuples; let _do_jp := fun y => do let stx ← Lean.Elab.Term.Quotation.compileStxMatch (Array.toList discrs) (Array.toList (Array.zip (Array.map (fun a => Array.toList a) patss) rhss)) let cls : Lean.Name := `Elab.match_syntax.result let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.TermElabM Lean.Syntax := fun y => pure stx if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData stx ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y; if (!Array.any patss (fun a => Array.any a (fun x => let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.namedPattern = true then let discr_7 := Lean.Syntax.getArg discr 0; let discr_8 := Lean.Syntax.getArg discr 1; let discr_9 := Lean.Syntax.getArg discr 2; if Lean.Syntax.matchesNull discr_9 0 = true then let discr := Lean.Syntax.getArg discr 3; let pat := discr; let id := discr_7; Lean.Syntax.isQuot pat else let discr_10 := Lean.Syntax.getArg discr 2; let discr_11 := Lean.Syntax.getArg discr 3; let pat := discr; Lean.Syntax.isQuot pat else let discr := x; let pat := discr; Lean.Syntax.isQuot pat) 0 (Array.size a)) 0 (Array.size patss)) = true then do let y ← Lean.Elab.throwUnsupportedSyntax _do_jp y else do let y ← pure PUnit.unit _do_jp y | none => let discr := Lean.Syntax.getArg discr_6 0; Lean.Elab.throwUnsupportedSyntax else let discr := Lean.Syntax.getArg discr 5; Lean.Elab.throwUnsupportedSyntax else let discr_5 := Lean.Syntax.getArg discr 3; let discr_6 := Lean.Syntax.getArg discr 4; let discr := Lean.Syntax.getArg discr 5; Lean.Elab.throwUnsupportedSyntax | none => 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 := Lean.Syntax.getArg discr 5; Lean.Elab.throwUnsupportedSyntax 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 := Lean.Syntax.getArg discr 5; Lean.Elab.throwUnsupportedSyntax else let discr := stx; Lean.Elab.throwUnsupportedSyntax