Lean.Elab.Util

source

def Lean.Syntax.prettyPrint (stx : Lean.Syntax) :

Lean.Format

Equations

Lean.Syntax.prettyPrint stx = match Lean.Syntax.reprint (Lean.Syntax.unsetTrailing stx) with | some str => Lean.format (String.toFormat str) | none => Lean.format stx

source

def Lean.MacroScopesView.format (view : Lean.MacroScopesView) (mainModule : Lean.Name) :

Lean.Format

Equations

Lean.MacroScopesView.format view mainModule = Lean.format (if List.isEmpty view.scopes = true then view.name else if (view.mainModule == mainModule) = true then List.foldl Lean.Name.mkNum (view.name ++ view.imported) view.scopes else List.foldl Lean.Name.mkNum (view.name ++ view.imported ++ view.mainModule) view.scopes)

source

def Lean.Elab.expandOptNamedPrio (stx : Lean.Syntax) :

Lean.MacroM Nat

Equations

Lean.Elab.expandOptNamedPrio stx = if Lean.Syntax.isNone stx = true then pure 1000 else let discr := Lean.Syntax.getOp stx 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.namedPrio = 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_4 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; let prio := discr_4; Lean.evalPrio prio else let discr := Lean.Syntax.getOp stx 0; Lean.Macro.throwUnsupported

source

structure Lean.Elab.MacroStackElem :

Type

before : Lean.Syntax
after : Lean.Syntax

source

@[inline]

abbrev Lean.Elab.MacroStack :

Type

Equations

Lean.Elab.MacroStack = List Lean.Elab.MacroStackElem

source

def Lean.Elab.getBetterRef (ref : Lean.Syntax) (macroStack : Lean.Elab.MacroStack) :

Lean.Syntax

Equations

Lean.Elab.getBetterRef ref macroStack = match Lean.Syntax.getPos? ref with | some x => ref | none => match List.find? (fun a => Lean.Syntax.getPos? a.before != none) macroStack with | some elem => elem.before | none => ref

source

constant Lean.Elab.pp.macroStack :

Lean.Option Bool

source

def Lean.Elab.addMacroStack {m : Type → Type} [inst : Monad m] [inst : Lean.MonadOptions m] (msgData : Lean.MessageData) (macroStack : Lean.Elab.MacroStack) :

m Lean.MessageData

Equations

Lean.Elab.addMacroStack msgData macroStack = do let a ← Lean.getOptions if (!Lean.Option.get a Lean.Elab.pp.macroStack) = true then pure msgData else match macroStack with | [] => pure msgData | stack@h:(top :: x) => let msgData := msgData ++ Lean.MessageData.ofFormat Lean.Format.line ++ Function.comp Lean.MessageData.ofFormat Lean.format "with resulting expansion" ++ Lean.indentD (Lean.MessageData.ofSyntax top.after); pure (List.foldl (fun msgData elem => msgData ++ Lean.MessageData.ofFormat Lean.Format.line ++ Function.comp Lean.MessageData.ofFormat Lean.format "while expanding" ++ Lean.indentD (Lean.MessageData.ofSyntax elem.before)) msgData stack)

source

def Lean.Elab.checkSyntaxNodeKind {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (k : Lean.Name) :

m Lean.Name

Equations

Lean.Elab.checkSyntaxNodeKind k = do let a ← Lean.getEnv if Lean.Parser.isValidSyntaxNodeKind a k = true then pure k else Lean.throwError (Lean.toMessageData "failed")

source

def Lean.Elab.checkSyntaxNodeKindAtNamespaces {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (k : Lean.Name) :

Lean.Name → m Lean.Name

Equations

Lean.Elab.checkSyntaxNodeKindAtNamespaces k (Lean.Name.str p x_1 x_2) = HOrElse.hOrElse (Lean.Elab.checkSyntaxNodeKind (Lean.Name.str p x_1 x_2 ++ k)) fun x => Lean.Elab.checkSyntaxNodeKindAtNamespaces k p
Lean.Elab.checkSyntaxNodeKindAtNamespaces k Lean.Name.anonymous = Lean.Elab.checkSyntaxNodeKind k
Lean.Elab.checkSyntaxNodeKindAtNamespaces k x = Lean.throwError (Lean.toMessageData "failed")

source

def Lean.Elab.checkSyntaxNodeKindAtCurrentNamespaces (k : Lean.Name) :

Lean.AttrM Lean.Name

Equations

Lean.Elab.checkSyntaxNodeKindAtCurrentNamespaces k = do let ctx ← read Lean.Elab.checkSyntaxNodeKindAtNamespaces k ctx.currNamespace

source

def Lean.Elab.syntaxNodeKindOfAttrParam (defaultParserNamespace : Lean.Name) (stx : Lean.Syntax) :

Lean.AttrM Lean.SyntaxNodeKind

Equations

Lean.Elab.syntaxNodeKindOfAttrParam defaultParserNamespace stx = do let k ← Lean.Attribute.Builtin.getId stx HOrElse.hOrElse (Lean.Elab.checkSyntaxNodeKindAtCurrentNamespaces k) fun x => HOrElse.hOrElse (Lean.Elab.checkSyntaxNodeKind (defaultParserNamespace ++ k)) fun x => Lean.throwError (Lean.toMessageData "invalid syntax node kind '" ++ Lean.toMessageData k ++ Lean.toMessageData "'")

source

@[implementedBy _private.Lean.Elab.Util.0.Lean.Elab.evalSyntaxConstantUnsafe]

constant Lean.Elab.evalSyntaxConstant (env : Lean.Environment) (opts : Lean.Options) (constName : Lean.Name) :

ExceptT String Id Lean.Syntax

source

unsafe def Lean.Elab.mkElabAttribute (γ : Type) (attrDeclName : Lean.Name) (attrBuiltinName : Lean.Name) (attrName : Lean.Name) (parserNamespace : Lean.Name) (typeName : Lean.Name) (kind : String) :

IO (Lean.KeyedDeclsAttribute γ)

Equations

Lean.Elab.mkElabAttribute γ attrDeclName attrBuiltinName attrName parserNamespace typeName kind = Lean.KeyedDeclsAttribute.init { builtinName := attrBuiltinName, name := attrName, descr := kind ++ " elaborator", valueTypeName := typeName, evalKey := fun x stx => Lean.Elab.syntaxNodeKindOfAttrParam parserNamespace stx, onAdded := fun builtin declName => if builtin = true then do let a ← Lean.getEnv let a ← liftM (Lean.findDocString? a declName) let _do_jp : Unit → Lean.AttrM Unit := fun y => do let a ← Lean.findDeclarationRanges? declName match a with | some declRanges => Lean.declareBuiltin (declName ++ `declRange) (Lean.mkAppN (Lean.mkConst `Lean.addBuiltinDeclarationRanges) #[Lean.toExpr declName, Lean.toExpr declRanges]) | x => pure PUnit.unit match a with | some doc => do let y ← Lean.declareBuiltin (declName ++ `docString) (Lean.mkAppN (Lean.mkConst `Lean.addBuiltinDocString) #[Lean.toExpr declName, Lean.toExpr doc]) _do_jp y | x => do let y ← pure PUnit.unit _do_jp y else pure PUnit.unit } attrDeclName

source

unsafe def Lean.Elab.mkMacroAttributeUnsafe :

IO (Lean.KeyedDeclsAttribute Lean.Macro)

Equations

Lean.Elab.mkMacroAttributeUnsafe = Lean.Elab.mkElabAttribute Lean.Macro `Lean.Elab.macroAttribute `builtinMacro `macro Lean.Name.anonymous `Lean.Macro "macro"

source

@[implementedBy Lean.Elab.mkMacroAttributeUnsafe]

constant Lean.Elab.mkMacroAttribute :

IO (Lean.KeyedDeclsAttribute Lean.Macro)

source

constant Lean.Elab.macroAttribute :

Lean.KeyedDeclsAttribute Lean.Macro

source

def Lean.Elab.expandMacroImpl? (env : Lean.Environment) :

Lean.Syntax → Lean.MacroM (Option (Lean.Name × Except Lean.Macro.Exception Lean.Syntax))

Equations

Lean.Elab.expandMacroImpl? env stx = do let r ← let col := Lean.KeyedDeclsAttribute.getEntries Lean.Elab.macroAttribute env (Lean.Syntax.getKind stx); forIn col { fst := none, snd := PUnit.unit } fun e r => let r := r.snd; do let r ← tryCatch (do let stx' ← Lean.withFreshMacroScope (Lean.KeyedDeclsAttribute.AttributeEntry.value e stx) pure (DoResultPR.return (e.toOLeanEntry.declName, Except.ok stx') PUnit.unit)) fun ex => match ex with | Lean.Macro.Exception.unsupportedSyntax => do let y ← pure () pure (DoResultPR.pure y PUnit.unit) | ex => pure (DoResultPR.return (e.toOLeanEntry.declName, Except.error ex) PUnit.unit) match r with | DoResultPR.pure a u => let x := u; do pure a pure (ForInStep.yield { fst := none, snd := PUnit.unit }) | DoResultPR.return b u => let x := u; pure (ForInStep.done { fst := some (some b), snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MacroM (Option (Lean.Name × Except Lean.Macro.Exception Lean.Syntax)) := fun y => pure none match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

source

class Lean.Elab.MonadMacroAdapter (m : Type → Type) :

Type

getCurrMacroScope : m Lean.MacroScope
getNextMacroScope : m Lean.MacroScope
setNextMacroScope : Lean.MacroScope → m Unit

Instances

source

instance Lean.Elab.instMonadMacroAdapter (m : Type → Type) (n : Type → Type) [inst : MonadLift m n] [inst : Lean.Elab.MonadMacroAdapter m] :

Lean.Elab.MonadMacroAdapter n

Equations

Lean.Elab.instMonadMacroAdapter m n = { getCurrMacroScope := liftM Lean.Elab.MonadMacroAdapter.getCurrMacroScope, getNextMacroScope := liftM Lean.Elab.MonadMacroAdapter.getNextMacroScope, setNextMacroScope := fun s => liftM (Lean.Elab.MonadMacroAdapter.setNextMacroScope s) }

source

def Lean.Elab.liftMacroM {α : Type} {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadMacroAdapter m] [inst : Lean.MonadEnv m] [inst : Lean.MonadRecDepth m] [inst : Lean.MonadError m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadTrace m] [inst : Lean.MonadOptions m] [inst : Lean.AddMessageContext m] (x : Lean.MacroM α) :

m α

Equations

Lean.Elab.liftMacroM x = do let env ← Lean.getEnv let currNamespace ← Lean.getCurrNamespace let openDecls ← Lean.getOpenDecls let methods : Lean.Macro.MethodsRef := Lean.Macro.mkMethods { expandMacro? := fun stx => do let a ← Lean.Elab.expandMacroImpl? env stx match a with | some (x, Except.ok stx) => pure (some stx) | x => pure none, getCurrNamespace := pure currNamespace, hasDecl := fun declName => pure (Lean.Environment.contains env declName), resolveNamespace? := fun n => pure (Lean.ResolveName.resolveNamespace? env currNamespace openDecls n), resolveGlobalName := fun n => pure (Lean.ResolveName.resolveGlobalName env currNamespace openDecls n) } let a ← Lean.getRef let a_1 ← Lean.Elab.MonadMacroAdapter.getCurrMacroScope let a_2 ← Lean.MonadRecDepth.getRecDepth let a_3 ← Lean.MonadRecDepth.getMaxRecDepth let a_4 ← Lean.Elab.MonadMacroAdapter.getNextMacroScope match x { methods := methods, mainModule := Lean.Environment.mainModule env, currMacroScope := a_1, currRecDepth := a_2, maxRecDepth := a_3, ref := a } { macroScope := a_4, traceMsgs := [] } with | EStateM.Result.error Lean.Macro.Exception.unsupportedSyntax x => Lean.Elab.throwUnsupportedSyntax | EStateM.Result.error (Lean.Macro.Exception.error ref msg) x => if (msg == Lean.maxRecDepthErrorMessage) = true then Lean.throwMaxRecDepthAt ref else Lean.throwErrorAt ref (Function.comp Lean.MessageData.ofFormat Lean.format msg) | EStateM.Result.ok a s => do Lean.Elab.MonadMacroAdapter.setNextMacroScope s.macroScope List.forM (List.reverse s.traceMsgs) fun x => match x with | (clsName, msg) => Lean.trace clsName fun x => Function.comp Lean.MessageData.ofFormat Lean.format msg pure a

source

@[inline]

def Lean.Elab.adaptMacro {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadMacroAdapter m] [inst : Lean.MonadEnv m] [inst : Lean.MonadRecDepth m] [inst : Lean.MonadError m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadTrace m] [inst : Lean.MonadOptions m] [inst : Lean.AddMessageContext m] (x : Lean.Macro) (stx : Lean.Syntax) :

m Lean.Syntax

Equations

Lean.Elab.adaptMacro x stx = Lean.Elab.liftMacroM (x stx)

source

def Lean.Elab.mkUnusedBaseName (baseName : Lean.Name) :

Lean.MacroM Lean.Name

Equations

Lean.Elab.mkUnusedBaseName baseName = do let currNamespace ← Lean.Macro.getCurrNamespace let a ← Lean.Macro.hasDecl (currNamespace ++ baseName) if a = true then (fun loop => loop 1) (Lean.Elab.mkUnusedBaseName.loop baseName currNamespace) else pure baseName

source

partial def Lean.Elab.mkUnusedBaseName.loop (baseName : Lean.Name) (currNamespace : Lean.Name) (idx : Nat) :

Lean.MacroM Lean.Name