@[inline]
@[inline]
def
Lean.Elab.Term.Quotation.withNewLocal
{α : Type}
(l : Lean.Name)
(x : Lean.Elab.Term.Quotation.PrecheckM α)
:
Equations
- Lean.Elab.Term.Quotation.withNewLocal l x = withReader (fun ctx => { quotLCtx := Lean.NameSet.insert ctx.quotLCtx l }) x
def
Lean.Elab.Term.Quotation.withNewLocals
{α : Type}
(ls : Array Lean.Name)
(x : Lean.Elab.Term.Quotation.PrecheckM α)
:
Equations
- Lean.Elab.Term.Quotation.withNewLocals ls x = withReader (fun ctx => { quotLCtx := Array.foldl Lean.NameSet.insert ctx.quotLCtx ls 0 (Array.size ls) }) x
Equations
- Lean.Elab.Term.Quotation.mkPrecheckAttribute = Lean.KeyedDeclsAttribute.init { builtinName := `builtinQuotPrecheck, name := `quotPrecheck, descr := "Register a double backtick syntax quotation pre-check.\n\n[quotPrecheck k] registers a declaration of type `Lean.Elab.Term.Quotation.Precheck` for the `SyntaxNodeKind` `k`.\nIt should implement eager name analysis on the passed syntax by throwing an exception on unbound identifiers,\nand calling `precheck` recursively on nested terms, potentially with an extended local context (`withNewLocal`).\nMacros without registered precheck hook are unfolded, and identifier-less syntax is ultimately assumed to be well-formed.", valueTypeName := `Lean.Elab.Term.Quotation.Precheck, evalKey := fun builtin stx => Lean.Attribute.Builtin.getId stx, onAdded := fun builtin declName => pure () } `Lean.Elab.Term.Quotation.precheckAttribute
Equations
- Lean.Elab.Term.Quotation.runPrecheck stx = do let opts ← Lean.getOptions if (Lean.Option.get opts Lean.Elab.Term.Quotation.quotPrecheck && Lean.Option.get opts Lean.Elab.Term.Quotation.hygiene) = true then ReaderT.run (Lean.Elab.Term.Quotation.precheck stx) { quotLCtx := ∅ } else pure PUnit.unit
Equations
- Lean.Elab.Term.Quotation.precheckIdent stx = match stx with | Lean.Syntax.ident info rawVal val preresolved => let _do_jp := fun y => do let a ← Lean.resolveGlobalName val let _do_jp : PUnit → Lean.Elab.Term.Quotation.PrecheckM Unit := fun y => do let a ← read let _do_jp : PUnit → Lean.Elab.Term.Quotation.PrecheckM Unit := fun y => let _do_jp := fun rs => do let r ← forIn rs { fst := none, snd := PUnit.unit } fun x r => match x with | (e, x) => let r := r.snd; match e with | Lean.Expr.fvar fvarId x => do let a ← Lean.getOptions let a_1 ← liftM (Lean.Elab.Term.Quotation.isSectionVariable e) if (Lean.Option.get a Lean.Elab.Term.Quotation.quotPrecheck.allowSectionVars && a_1) = true then pure (ForInStep.done { fst := some PUnit.unit, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) | x => do pure () pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.Elab.Term.Quotation.PrecheckM Unit := fun y => Lean.throwError (Lean.toMessageData "unknown identifier '" ++ Lean.toMessageData val ++ Lean.toMessageData "' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.") match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a; do let y ← tryCatch (liftM (Lean.Elab.Term.resolveName stx val [] [] none)) fun x => pure [] _do_jp y if Lean.NameSet.contains a.quotLCtx val = true then pure PUnit.unit else do let y ← pure PUnit.unit _do_jp y match a with | x :: x_1 => pure PUnit.unit | x => do let y ← pure PUnit.unit _do_jp y; if (!List.isEmpty preresolved) = true then pure PUnit.unit else do let y ← pure PUnit.unit _do_jp y | x => Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Term.Quotation.precheckApp x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let args := Lean.Syntax.getArgs discr; let f := discr_1; do Lean.Elab.Term.Quotation.precheck f let r ← forIn args PUnit.unit fun arg r => let discr := arg; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.namedArgument = true then let discr_2 := Lean.Syntax.getArg discr 0; 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; let e := discr_5; let n := discr_3; do Lean.Elab.Term.Quotation.precheck e pure (ForInStep.yield PUnit.unit) else let discr := arg; let e := discr; do Lean.Elab.Term.Quotation.precheck e pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit else let discr := x; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Term.Quotation.precheckParen x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.paren = 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 := Lean.Syntax.getArg discr 2; pure () else let discr_3 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_3 2 = true then let discr_4 := Lean.Syntax.getArg discr_3 0; let discr_5 := Lean.Syntax.getArg discr_3 1; 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.Term.typeAscription = true then let discr_7 := Lean.Syntax.getArg discr_6 0; let discr_8 := Lean.Syntax.getArg discr_6 1; let discr := Lean.Syntax.getArg discr 2; let type := discr_8; let e := discr_4; do Lean.Elab.Term.Quotation.precheck e Lean.Elab.Term.Quotation.precheck type else let discr_7 := Lean.Syntax.getArg discr_5 0; if Lean.Syntax.isOfKind discr_7 `Lean.Parser.Term.tupleTail = true then let discr_8 := Lean.Syntax.getArg discr_7 0; let discr_9 := Lean.Syntax.getArg discr_7 1; let discr := Lean.Syntax.getArg discr 2; let es := { elemsAndSeps := Lean.Syntax.getArgs discr_9 }; let e := discr_4; do Lean.Elab.Term.Quotation.precheck e Array.forM Lean.Elab.Term.Quotation.precheck (Lean.Syntax.SepArray.getElems es) 0 (Array.size (Lean.Syntax.SepArray.getElems es)) else let discr_8 := Lean.Syntax.getArg discr_5 0; let discr := Lean.Syntax.getArg discr 2; Lean.Elab.throwUnsupportedSyntax else let discr_6 := Lean.Syntax.getArg discr_3 1; if Lean.Syntax.matchesNull discr_6 0 = true then let discr := Lean.Syntax.getArg discr 2; let e := discr_4; Lean.Elab.Term.Quotation.precheck e else let discr_7 := Lean.Syntax.getArg discr_3 1; let discr := Lean.Syntax.getArg discr 2; Lean.Elab.throwUnsupportedSyntax else let discr_4 := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr 2; Lean.Elab.throwUnsupportedSyntax else let discr := x; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Term.Quotation.elabPrecheckedQuot stx expectedType? = let singleQuot := Lean.Syntax.getOp stx 1; do Lean.Elab.Term.Quotation.runPrecheck (Lean.Syntax.getQuotContent singleQuot) Lean.Elab.Term.adaptExpander (fun x => pure singleQuot) stx expectedType?