Basic interface for configuration evaluation

def Lean.Elab.ConfigEval.evalTermWithRef {α : Type} [EvalTerm α] (stx : Term) : TermElabM α

def Lean.Elab.ConfigEval.evalExprWithElab {α : Type} [EvalExpr α] (stx : Term) : TermElabM α

Evaluate stx using either evalExpr.

def Lean.Elab.ConfigEval.evalTermOrExprWithElab {α : Type} [EvalTerm α] [EvalExpr α] (stx : Term) : TermElabM α

Evaluate stx using either evalStx or evalExpr.

@[inline]

def Lean.Elab.ConfigEval.EvalTerm.evalTermWithInfo {α : Type} (expectedType? : Option Expr) (f : Term → TermElabM (α × Expr)) (stx : Term) : TermElabM (α × Expr)

@[inline]

def Lean.Elab.ConfigEval.EvalTerm.evalTermWithInfo' {α : Type} [ToExpr α] (f : Term → TermElabM α) : Term → TermElabM (α × Expr)

Like evalTermWithInfo, but uses an existing ToExpr instance for expectedType? and for constructing the expression.

def Lean.Elab.ConfigEval.EvalExpr.withWHNF {α : Type} (f : Expr → MetaM α) (e : Expr) (errMsg : MessageData) : MetaM α

Evaluates f e, and if that does throwUnsupportedExpr, evaluates f (← whnf e). If either throw another exception, aborts immediately with that exception. If both do throwUnsupportedExpr, then this generates an exception.

def Lean.Elab.ConfigEval.ConfigItem.isAnonymous (item : ConfigItem) : Bool

def Lean.Elab.ConfigEval.ConfigItem.root (item : ConfigItem) : Syntax

def Lean.Elab.ConfigEval.ConfigItem.getRootStr (item : ConfigItem) : String

def Lean.Elab.ConfigEval.ConfigItem.prevRoot? (item : ConfigItem) : Option Syntax

def Lean.Elab.ConfigEval.ConfigItem.prevRoot (item : ConfigItem) : Syntax

def Lean.Elab.ConfigEval.ConfigItem.getCurrOptionName (item : ConfigItem) : Name

Gets the current name of the option after any shifting. For example, if an option is named a.b.c.d and there is a handler for a.b.*, then the handler receives a ConfigItem whose current option name is c.d.

def Lean.Elab.ConfigEval.ConfigItem.shift (item : ConfigItem) : ConfigItem

Drops the first component of the optionName, returning the new config item. The first component is stored at the front of prevOptionComps.

def Lean.Elab.ConfigEval.ConfigItem.checkNotBool (item : ConfigItem) : TermElabM Unit

def Lean.Elab.ConfigEval.ConfigItem.throwInvalidOption {α : Type} (item : ConfigItem) (structName? : Option Name) : TermElabM α

def Lean.Elab.ConfigEval.ConfigItem.throwCannotSetOption {α : Type} (item : ConfigItem) (structName? : Option Name) : TermElabM α

def Lean.Elab.ConfigEval.ConfigItem.addConstInfo (item : ConfigItem) (projFn : Name) : TermElabM Unit

def Lean.Elab.ConfigEval.ConfigItem.addCompletionInfo (item : ConfigItem) (structName : Name) : TermElabM Unit

@[specialize #[]]

partial def Lean.Elab.ConfigEval.foldConfigM {α : Type} {m : Type → Type} [Monad m] [MonadRef m] (init : α) (cfg : Syntax) (k : α → ConfigItem → m α) (onErr : α → Syntax → m α) : m α

Interprets cfg as configuration item or list of configuration items.

Items are interpreted in a way that allows user-defined configurations. Nearly anything that looks like configuration items or lists of configuration items will be interpreted. We're expecting an item that has one of the following formats:

• "(" ident/atom ":=" syntax ")"
• "+" ident/atom
• "-" ident/atom

The specification:

• A null node is a list of configurations
• A one-argument node is considered to be a wrapper like optConfig or configItem.
• A node with at two arguments starting with a "+"/"-" atom and whose second argument is an ident or atom is a posConfigItem/negConfigItem
• A node with at most five arguments starting with a "(" atom and whose second argument is an ident or atom is a valConfigItem. The fourth argument is the value, and it is allowed to have arbitary syntax (it does not need to be a Term).
• A bare atom is considered to be a "+" option.

We trust that any atoms are valid as idents. The atom will be parsed using String.toName to form the name. (Small optimization: if the name doesn't contain ., we use Name.mkSimple to skip parsing. Atoms must not contain numerals or «» escapes.)

On interpretation error, onErr is called with the current configuration object and the offending syntax item. It may process the item itself or otherwise throw an error. We leave it to onErr to decide what to do for items containing Syntax.missing.

@[specialize #[]]

partial def Lean.Elab.ConfigEval.foldConfigsM {α : Type} {m : Type → Type} [Monad m] [MonadRef m] (init : α) (cfgs : Array Syntax) (k : α → ConfigItem → m α) (onErr : α → Syntax → m α) : m α

Like foldConfigM but takes an array of configurations or configuration items.

def Lean.Elab.ConfigEval.EvalConfigItem.trySet {α : Type} (eval : EvalConfigItem α) (config : α) (item : ConfigItem) (logExceptions : Bool) : TermElabM α

def Lean.Elab.ConfigEval.EvalConfigItem.defaultOnErr {α : Type} (cfg : α) (cfgItem : Syntax) (cfgType? : Option Expr := none) : TermElabM α

Default onErr handler. If the cfgItem contains .missing, we assume an error has already been reported by the parser and return cfg. Otherwise, we throw an unsupported syntax exception.

If cfgType? is present, then it adds completion info when the identifier is missing.

def Lean.Elab.ConfigEval.EvalConfigItem.setConfig {α : Type} (eval : EvalConfigItem α) (init : α) (cfg : Syntax) (onErr : α → Syntax → TermElabM α := fun (cfg : α) (cfgItem : Syntax) => defaultOnErr cfg cfgItem) (logExceptions : Bool := false) : TermElabM α

Applies the configuration cfg to init using eval.set. If logExceptions is true, then catches and logs exceptions.

The onErr callback is used for invalid configuration syntax.

Note: this should be run from within runConfigElab.

def Lean.Elab.ConfigEval.EvalConfigItem.setConfigs {α : Type} (eval : EvalConfigItem α) (init : α) (cfgs : Array Syntax) (onErr : α → Syntax → TermElabM α := fun (cfg : α) (cfgItem : Syntax) => defaultOnErr cfg cfgItem) (logExceptions : Bool := false) : TermElabM α

Applies the configuration cfg to init using eval.set. If logExceptions is true, then catches and logs exceptions.

The onErr callback is used for invalid configuration syntax.

Note: this should be run from within runConfigElab.

def Lean.Elab.ConfigEval.runConfigElab {α : Type} (mx : TermElabM α) : CoreM α

Runs mx using a fresh meta and term state. This should be used around any configuration elaboration.

def Lean.Elab.ConfigEval.EvalConfigItem.setConfig' {α : Type} (eval : EvalConfigItem α) (init : α) (cfg : Syntax) (onErr : α → Syntax → TermElabM α := fun (cfg : α) (cfgItem : Syntax) => defaultOnErr cfg cfgItem) (logExceptions : Bool := false) : CoreM α

Calls EvalConfigItem.setConfig' from within runConfigElab.

def Lean.Elab.ConfigEval.EvalConfigItem.setConfigs' {α : Type} (eval : EvalConfigItem α) (init : α) (cfgs : Array Syntax) (onErr : α → Syntax → TermElabM α := fun (cfg : α) (cfgItem : Syntax) => defaultOnErr cfg cfgItem) (logExceptions : Bool := false) : CoreM α

Calls EvalConfigItem.setConfigs' from within runConfigElab.