Basic interface for configuration evaluation

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

Equations

• Lean.Elab.ConfigEval.evalTermWithRef stx = Lean.withRef stx.raw (Prod.fst <$> Lean.Elab.ConfigEval.evalTerm stx)

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

Evaluate stx using either evalExpr.

Equations

• One or more equations did not get rendered due to their size.

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

Evaluate stx using either evalStx or evalExpr.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• item.isAnonymous = item.optionComps.isEmpty

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

Equations

• item.root = match item.optionComps with | c :: tail => c | x => Lean.Syntax.missing

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

Equations

• item.getRootStr = match item.root.getId with | pre.str s => s | x => ""

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

Equations

• item.prevRoot? = item.prevOptionComps[0]?

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

Equations

• item.prevRoot = match item.prevOptionComps with | c :: tail => c | x => Lean.Syntax.missing

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.

Equations

• item.getCurrOptionName = List.foldl Lean.Name.appendCore Lean.Name.anonymous (List.map (fun (x : Lean.Syntax) => x.getId) item.optionComps)

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[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 α

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.ConfigEval.EvalConfigItem.defaultOnErr cfg cfgItem cfgType? = (fun (__r : Unit) => if cfgItem.hasMissing = true then pure cfg else Lean.Elab.throwUnsupportedSyntax) ()

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Lean.Elab.ConfigEval.runConfigElab mx = (Lean.Elab.withSaveInfoContext mx).run'.run'

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• eval.setConfigs' init cfgs onErr logExceptions = if cfgs.isEmpty = true then pure init else Lean.Elab.ConfigEval.runConfigElab (eval.setConfigs init cfgs onErr logExceptions)