def
Lean.mkErrorStringWithPos
(fileName : String)
(pos : Lean.Position)
(msg : String)
(endPos : optParam (Option Lean.Position) none)
:
Equations
- Lean.mkErrorStringWithPos fileName pos msg endPos = let endPos := match endPos with | some endPos => toString "-" ++ toString endPos.line ++ toString ":" ++ toString endPos.column ++ toString "" | none => ""; toString "" ++ toString fileName ++ toString ":" ++ toString pos.line ++ toString ":" ++ toString pos.column ++ toString "" ++ toString endPos ++ toString ": " ++ toString msg ++ toString ""
- information: Lean.MessageSeverity
- warning: Lean.MessageSeverity
- error: Lean.MessageSeverity
Equations
- Lean.instBEqMessageSeverity = { beq := [anonymous] }
Equations
- Lean.instInhabitedMessageSeverity = { default := Lean.MessageSeverity.information }
- env : Lean.Environment
- mctx : Lean.MetavarContext
- lctx : Lean.LocalContext
- opts : Lean.Options
- ofFormat: Lean.Format → Lean.MessageData
- ofSyntax: Lean.Syntax → Lean.MessageData
- ofExpr: Lean.Expr → Lean.MessageData
- ofLevel: Lean.Level → Lean.MessageData
- ofName: Lean.Name → Lean.MessageData
- ofGoal: Lean.MVarId → Lean.MessageData
- withContext: Lean.MessageDataContext → Lean.MessageData → Lean.MessageData
- withNamingContext: Lean.NamingContext → Lean.MessageData → Lean.MessageData
- nest: Nat → Lean.MessageData → Lean.MessageData
- group: Lean.MessageData → Lean.MessageData
- compose: Lean.MessageData → Lean.MessageData → Lean.MessageData
- tagged: Lean.Name → Lean.MessageData → Lean.MessageData
- node: Array Lean.MessageData → Lean.MessageData
Equations
- Lean.instInhabitedMessageData = { default := Lean.MessageData.ofFormat default }
Equations
- Lean.MessageData.instantiateMVars msg = (fun visit => visit msg { depth := 0, mvarCounter := 0, lDepth := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }) Lean.MessageData.instantiateMVars.visit
partial def
Lean.MessageData.instantiateMVars.visit
(msg : Lean.MessageData)
(mctx : Lean.MetavarContext)
:
Equations
- Lean.MessageData.isNil x = match x with | Lean.MessageData.ofFormat Lean.Format.nil => true | x => false
Equations
- Lean.MessageData.isNest x = match x with | Lean.MessageData.nest x x_1 => true | x => false
Equations
- Lean.MessageData.mkPPContext nCtx ctx = { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts, currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls }
Equations
- Lean.MessageData.format msgData = Lean.MessageData.formatAux { currNamespace := Lean.Name.anonymous, openDecls := [] } none msgData
Equations
- Lean.MessageData.toString msgData = do let a ← Lean.MessageData.format msgData pure (toString a)
Equations
- Lean.MessageData.instAppendMessageData = { append := Lean.MessageData.compose }
Equations
- Lean.MessageData.instCoeStringMessageData = { coe := Lean.MessageData.ofFormat ∘ Lean.format }
Equations
Equations
Equations
Equations
Equations
Equations
Equations
- Lean.MessageData.instCoeOptionExprMessageData = { coe := fun o => match o with | none => Function.comp Lean.MessageData.ofFormat Lean.format "none" | some e => Lean.MessageData.ofExpr e }
partial def
Lean.MessageData.arrayExpr.toMessageData
(es : Array Lean.Expr)
(i : Nat)
(acc : Lean.MessageData)
:
Equations
- Lean.MessageData.instCoeArrayExprMessageData = { coe := fun es => Lean.MessageData.arrayExpr.toMessageData es 0 (Function.comp Lean.MessageData.ofFormat Lean.format "#[") }
Equations
- Lean.MessageData.bracket l f r = Lean.MessageData.group (Lean.MessageData.nest (String.length l) (Function.comp Lean.MessageData.ofFormat Lean.format l ++ f ++ Function.comp Lean.MessageData.ofFormat Lean.format r))
Equations
- Lean.MessageData.paren f = Lean.MessageData.bracket "(" f ")"
Equations
- Lean.MessageData.sbracket f = Lean.MessageData.bracket "[" f "]"
Equations
- Lean.MessageData.joinSep [] x = Lean.MessageData.ofFormat Lean.Format.nil
- Lean.MessageData.joinSep [a] x = a
- Lean.MessageData.joinSep (a :: as) x = a ++ x ++ Lean.MessageData.joinSep as x
Equations
- Lean.MessageData.ofList x = match x with | [] => Function.comp Lean.MessageData.ofFormat Lean.format "[]" | xs => Lean.MessageData.sbracket (Lean.MessageData.joinSep xs (Lean.MessageData.ofFormat (Std.Format.text ",") ++ Lean.MessageData.ofFormat Lean.Format.line))
Equations
- Lean.MessageData.ofArray msgs = Lean.MessageData.ofList (Array.toList msgs)
Equations
Equations
- Lean.MessageData.instCoeListExprMessageData = { coe := fun es => Lean.MessageData.ofList (List.map Lean.MessageData.ofExpr es) }
- fileName : String
- pos : Lean.Position
- endPos : Option Lean.Position
- severity : Lean.MessageSeverity
- caption : String
- data : Lean.MessageData
Equations
- Lean.instInhabitedMessage = { default := { fileName := default, pos := default, endPos := default, severity := default, caption := default, data := default } }
Equations
- Lean.Message.toString msg includeEndPos = do let str ← Lean.MessageData.toString msg.data let endPos : Option Lean.Position := if includeEndPos = true then msg.endPos else none let _do_jp : String → PUnit → IO String := fun str y => let _do_jp := fun str y => let _do_jp := fun str y => pure str; if (String.isEmpty str || String.back str != Char.ofNat 10) = true then let str := str ++ "\n"; do let y ← pure PUnit.unit _do_jp str y else do let y ← pure PUnit.unit _do_jp str y; match msg.severity with | Lean.MessageSeverity.information => do let y ← pure () _do_jp str y | Lean.MessageSeverity.warning => let str := Lean.mkErrorStringWithPos msg.fileName msg.pos "warning: " endPos ++ str; do let y ← pure PUnit.unit _do_jp str y | Lean.MessageSeverity.error => let str := Lean.mkErrorStringWithPos msg.fileName msg.pos "error: " endPos ++ str; do let y ← pure PUnit.unit _do_jp str y if (msg.caption == "") = true then do let y ← pure PUnit.unit _do_jp str y else let str := msg.caption ++ ":\n" ++ str; do let y ← pure PUnit.unit _do_jp str y
Equations
- Lean.instInhabitedMessageLog = { default := { msgs := default } }
Equations
- Lean.MessageLog.empty = { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }
Equations
- Lean.MessageLog.isEmpty log = Std.PersistentArray.isEmpty log.msgs
Equations
- Lean.MessageLog.add msg log = { msgs := Std.PersistentArray.push log.msgs msg }
Equations
- Lean.MessageLog.append l₁ l₂ = { msgs := l₁.msgs ++ l₂.msgs }
Equations
- Lean.MessageLog.instAppendMessageLog = { append := Lean.MessageLog.append }
Equations
- Lean.MessageLog.hasErrors log = Std.PersistentArray.any log.msgs fun m => match m.severity with | Lean.MessageSeverity.error => true | x => false
Equations
- Lean.MessageLog.errorsToWarnings log = { msgs := Std.PersistentArray.map (fun m => match m.severity with | Lean.MessageSeverity.error => { fileName := m.fileName, pos := m.pos, endPos := m.endPos, severity := Lean.MessageSeverity.warning, caption := m.caption, data := m.data } | x => m) log.msgs }
Equations
- Lean.MessageLog.getInfoMessages log = { msgs := Std.PersistentArray.filter log.msgs fun m => match m.severity with | Lean.MessageSeverity.information => true | x => false }
def
Lean.MessageLog.forM
{m : Type → Type}
[inst : Monad m]
(log : Lean.MessageLog)
(f : Lean.Message → m Unit)
:
m Unit
Equations
- Lean.MessageLog.forM log f = Std.PersistentArray.forM log.msgs f
Equations
- Lean.MessageLog.toList log = List.reverse (Std.PersistentArray.foldl log.msgs (fun acc msg => msg :: acc) [])
Equations
- Lean.MessageData.nestD msg = Lean.MessageData.nest 2 msg
Equations
Equations
- addMessageContext : Lean.MessageData → m Lean.MessageData
instance
Lean.instAddMessageContext
(m : Type → Type)
(n : Type → Type)
[inst : MonadLift m n]
[inst : Lean.AddMessageContext m]
:
Equations
- Lean.instAddMessageContext m n = { addMessageContext := fun msg => liftM (Lean.addMessageContext msg) }
def
Lean.addMessageContextPartial
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadOptions m]
(msgData : Lean.MessageData)
:
Equations
- Lean.addMessageContextPartial msgData = do let env ← Lean.getEnv let opts ← Lean.getOptions pure (Lean.MessageData.withContext { env := env, mctx := { depth := 0, mvarCounter := 0, lDepth := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, lctx := { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, opts := opts } msgData)
def
Lean.addMessageContextFull
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadMCtx m]
[inst : Lean.MonadLCtx m]
[inst : Lean.MonadOptions m]
(msgData : Lean.MessageData)
:
Equations
- Lean.addMessageContextFull msgData = do let env ← Lean.getEnv let mctx ← Lean.getMCtx let lctx ← Lean.getLCtx let opts ← Lean.getOptions pure (Lean.MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData)
- toMessageData : α → Lean.MessageData
Instances
- Lean.instToMessageData
- Lean.instToMessageDataFormat
- Lean.instToMessageDataOption
- Lean.instToMessageDataOptionExpr
- Lean.instToMessageDataSyntax
- Lean.instToMessageDataExpr
- Lean.instToMessageDataMessageData
- Lean.instToMessageDataList
- Lean.instToMessageDataSubarray
- Lean.Meta.instToMessageDataSimpLemma
- Lean.instToMessageDataArray
- Lean.instToMessageDataMVarId
- Lean.instToMessageDataName
- Lean.instToMessageDataString
- Lean.instToMessageDataLevel
Equations
- Lean.stringToMessageData str = let lines := String.split str fun a => a == Char.ofNat 10; let lines := List.map (Lean.MessageData.ofFormat ∘ Lean.format) lines; Lean.MessageData.joinSep lines (Lean.MessageData.ofFormat Lean.Format.line)
Equations
- Lean.instToMessageData = { toMessageData := Lean.MessageData.ofFormat ∘ Lean.format }
Equations
- Lean.instToMessageDataExpr = { toMessageData := Lean.MessageData.ofExpr }
Equations
- Lean.instToMessageDataLevel = { toMessageData := Lean.MessageData.ofLevel }
Equations
- Lean.instToMessageDataName = { toMessageData := Lean.MessageData.ofName }
Equations
- Lean.instToMessageDataString = { toMessageData := Lean.stringToMessageData }
Equations
- Lean.instToMessageDataSyntax = { toMessageData := Lean.MessageData.ofSyntax }
Equations
- Lean.instToMessageDataFormat = { toMessageData := Lean.MessageData.ofFormat }
Equations
- Lean.instToMessageDataMVarId = { toMessageData := Lean.MessageData.ofGoal }
Equations
- Lean.instToMessageDataMessageData = { toMessageData := id }
Equations
- Lean.instToMessageDataList = { toMessageData := fun as => Lean.MessageData.ofList (List.map Lean.toMessageData as) }
Equations
- Lean.instToMessageDataArray = { toMessageData := fun as => Lean.toMessageData (Array.toList as) }
Equations
- Lean.instToMessageDataSubarray = { toMessageData := fun as => Lean.toMessageData (Array.toList (Subarray.toArray as)) }
Equations
- Lean.instToMessageDataOption = { toMessageData := fun x => match x with | none => Function.comp Lean.MessageData.ofFormat Lean.format "none" | some e => Function.comp Lean.MessageData.ofFormat Lean.format "some (" ++ Lean.toMessageData e ++ Function.comp Lean.MessageData.ofFormat Lean.format ")" }
Equations
-
Lean.instToMessageDataOptionExpr = { toMessageData := fun x =>
match x with
| none => Function.comp Lean.MessageData.ofFormat Lean.format "
" | some e => Lean.toMessageData e }
Equations
- Lean.termM!_ = Lean.ParserDescr.node `Lean.termM!_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "m!") (Lean.ParserDescr.unary `interpolatedStr (Lean.ParserDescr.cat `term 0)))
Equations
- Lean.KernelException.toMessageData e opts = match e with | Lean.KernelException.unknownConstant env constName => Lean.KernelException.mkCtx env { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } opts (Lean.toMessageData "(kernel) unknown constant '" ++ Lean.toMessageData constName ++ Lean.toMessageData "'") | Lean.KernelException.alreadyDeclared env constName => Lean.KernelException.mkCtx env { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } opts (Lean.toMessageData "(kernel) constant has already been declared '" ++ Lean.toMessageData constName ++ Lean.toMessageData "'") | Lean.KernelException.declTypeMismatch env decl givenType => let process := fun n expectedType => Lean.toMessageData "(kernel) declaration type mismatch, '" ++ Lean.toMessageData n ++ Lean.toMessageData "' has type" ++ Lean.toMessageData (Lean.indentExpr givenType) ++ Lean.toMessageData "\nbut it is expected to have type" ++ Lean.toMessageData (Lean.indentExpr expectedType) ++ Lean.toMessageData ""; match decl with | Lean.Declaration.defnDecl { toConstantVal := { name := n, levelParams := x, type := type }, value := x_1, hints := x_2, safety := x_3 } => process n type | Lean.Declaration.thmDecl { toConstantVal := { name := n, levelParams := x, type := type }, value := x_1 } => process n type | x => Function.comp Lean.MessageData.ofFormat Lean.format "(kernel) declaration type mismatch" | Lean.KernelException.declHasMVars env constName x => Lean.KernelException.mkCtx env { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } opts (Lean.toMessageData "(kernel) declaration has metavariables '" ++ Lean.toMessageData constName ++ Lean.toMessageData "'") | Lean.KernelException.declHasFVars env constName x => Lean.KernelException.mkCtx env { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } opts (Lean.toMessageData "(kernel) declaration has free variables '" ++ Lean.toMessageData constName ++ Lean.toMessageData "'") | Lean.KernelException.funExpected env lctx e => Lean.KernelException.mkCtx env lctx opts (Lean.toMessageData "(kernel) function expected" ++ Lean.toMessageData (Lean.indentExpr e) ++ Lean.toMessageData "") | Lean.KernelException.typeExpected env lctx e => Lean.KernelException.mkCtx env lctx opts (Lean.toMessageData "(kernel) type expected" ++ Lean.toMessageData (Lean.indentExpr e) ++ Lean.toMessageData "") | Lean.KernelException.letTypeMismatch env lctx n x x_1 => Lean.KernelException.mkCtx env lctx opts (Lean.toMessageData "(kernel) let-declaration type mismatch '" ++ Lean.toMessageData n ++ Lean.toMessageData "'") | Lean.KernelException.exprTypeMismatch env lctx e x => Lean.KernelException.mkCtx env lctx opts (Lean.toMessageData "(kernel) type mismatch at" ++ Lean.toMessageData (Lean.indentExpr e) ++ Lean.toMessageData "") | Lean.KernelException.appTypeMismatch env lctx e fnType argType => Lean.KernelException.mkCtx env lctx opts (Lean.toMessageData "application type mismatch" ++ Lean.toMessageData (Lean.indentExpr e) ++ Lean.toMessageData "\nargument has type" ++ Lean.toMessageData (Lean.indentExpr argType) ++ Lean.toMessageData "\nbut function has type" ++ Lean.toMessageData (Lean.indentExpr fnType) ++ Lean.toMessageData "") | Lean.KernelException.invalidProj env lctx e => Lean.KernelException.mkCtx env lctx opts (Lean.toMessageData "(kernel) invalid projection" ++ Lean.toMessageData (Lean.indentExpr e) ++ Lean.toMessageData "") | Lean.KernelException.other msg => Lean.toMessageData "(kernel) " ++ Lean.toMessageData msg ++ Lean.toMessageData ""