/- Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich, Leonardo de Moura Message type used by the Lean frontend -/ prelude import Lean.Data.Position import Lean.Data.OpenDecl import Lean.MetavarContext import Lean.Environment import Lean.Util.PPExt import Lean.Util.Sorry namespace Lean def mkErrorStringWithPos (fileName : String) (pos : Position) (msg : String) (endPos : Option Position := none) : String := let endPos := match endPos with | some endPos => s!"-{endPos.line}:{endPos.column}" | none => "" s!"{fileName}:{pos.line}:{pos.column}{endPos}: {msg}" inductive MessageSeverity where | information | warning | error deriving Inhabited, BEq, ToJson, FromJson structure MessageDataContext where env : Environment mctx : MetavarContext lctx : LocalContext opts : Options /-- A naming context is the information needed to shorten names in pretty printing. It gives the current namespace and the list of open declarations. -/ structure NamingContext where currNamespace : Name openDecls : List OpenDecl structure TraceData where /-- Trace class, e.g. `Elab.step`. -/ cls : Name /-- Start time in seconds; 0 if unknown to avoid `Option` allocation. -/ startTime : Float := 0 /-- Stop time in seconds; 0 if unknown to avoid `Option` allocation. -/ stopTime : Float := startTime /-- Whether trace node defaults to collapsed in the infoview. -/ collapsed : Bool := true /-- Optional tag shown in `trace.profiler.output` output after the trace class name. -/ tag : String := "" /-- Structured message data. We use it for reporting errors, trace messages, etc. -/ inductive MessageData where /-- Eagerly formatted text with info annotations. This constructor is inspected in various hacks. -/ | ofFormatWithInfos : FormatWithInfos → MessageData | ofGoal : MVarId → MessageData /-- A widget instance. In `ofWidget wi alt`, the nested message `alt` should approximate the contents of the widget without itself using `ofWidget wi _`. This is used as fallback in environments that cannot display user widgets. `alt` may nest any structured message, for example `ofGoal` to approximate a tactic state widget, and, if necessary, even other widget instances (for which approximations are computed recursively). -/ | ofWidget : Widget.WidgetInstance → MessageData → MessageData /-- `withContext ctx d` specifies the pretty printing context `(env, mctx, lctx, opts)` for the nested expressions in `d`. -/ | withContext : MessageDataContext → MessageData → MessageData | withNamingContext : NamingContext → MessageData → MessageData /-- Lifted `Format.nest` -/ | nest : Nat → MessageData → MessageData /-- Lifted `Format.group` -/ | group : MessageData → MessageData /-- Lifted `Format.compose` -/ | compose : MessageData → MessageData → MessageData /-- Tagged sections. `Name` should be viewed as a "kind", and is used by `MessageData` inspector functions. Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/ | tagged : Name → MessageData → MessageData | trace (data : TraceData) (msg : MessageData) (children : Array MessageData) /-- A lazy message. The provided thunk will not be run until it is about to be displayed. This can save computation in cases where the message may never be seen. The `Dynamic` value is expected to be a `MessageData`, which is a workaround for the positivity restriction. If the thunked message is produced for a term that contains a synthetic sorry, `hasSyntheticSorry` should return `true`. This is used to filter out certain messages. -/ | ofLazy (f : Option PPContext → IO Dynamic) (hasSyntheticSorry : MetavarContext → Bool) deriving Inhabited, TypeName namespace MessageData /-- Eagerly formatted text. -/ def ofFormat (fmt : Format) : MessageData := .ofFormatWithInfos ⟨fmt, .empty⟩ /-- Lazy message data production, with access to the context as given by a surrounding `MessageData.withContext` (which is expected to exist). -/ def lazy (f : PPContext → IO MessageData) (hasSyntheticSorry : MetavarContext → Bool := fun _ => false) : MessageData := .ofLazy (hasSyntheticSorry := hasSyntheticSorry) fun ctx? => do let msg ← match ctx? with | .none => pure (.ofFormat "(invalid MessageData.lazy, missing context)") -- see `addMessageContext` | .some ctx => f ctx return Dynamic.mk msg variable (p : Name → Bool) in /-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag` is true. This does not descend into lazily generated subtress (`.ofLazy`); message tags of interest (like those added by `logLinter`) are expected to be near the root of the `MessageData`, and not hidden inside `.ofLazy`. -/ partial def hasTag : MessageData → Bool | withContext _ msg => hasTag msg | withNamingContext _ msg => hasTag msg | nest _ msg => hasTag msg | group msg => hasTag msg | compose msg₁ msg₂ => hasTag msg₁ || hasTag msg₂ | tagged n msg => p n || hasTag msg | trace data msg msgs => p data.cls || hasTag msg || msgs.any hasTag | _ => false /-- An empty message. -/ def nil : MessageData := ofFormat Format.nil def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext := { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts, currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls } def ofSyntax (stx : Syntax) : MessageData := -- discard leading/trailing whitespace let stx := stx.copyHeadTailInfoFrom .missing .ofLazy (fun ctx? => do let msg ← ofFormat <$> match ctx? with | .none => pure stx.formatStx | .some ctx => ppTerm ctx ⟨stx⟩ -- HACK: might not be a term return Dynamic.mk msg) (fun _ => false) def ofExpr (e : Expr) : MessageData := .ofLazy (fun ctx? => do let msg ← ofFormatWithInfos <$> match ctx? with | .none => pure (format (toString e)) | .some ctx => ppExprWithInfos ctx e return Dynamic.mk msg) (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry) def ofLevel (l : Level) : MessageData := .ofLazy (fun ctx? => do let msg ← ofFormat <$> match ctx? with | .none => pure (format l) | .some ctx => ppLevel ctx l return Dynamic.mk msg) (fun _ => false) /-- Simply formats the name. See `MessageData.ofConstName` for richer messages. -/ def ofName (n : Name) : MessageData := ofFormat (format n) /-- Represents a constant name such that hovering and "go to definition" works. If there is no such constant in the environment, the name is simply formatted, but sanitized if it is a hygienic name. Use `MessageData.ofName` if hovers are undesired. If `fullNames` is true, then pretty prints as if `pp.fullNames` is true. Otherwise, pretty prints using the current user setting for `pp.fullNames`. -/ def ofConstName (constName : Name) (fullNames : Bool := false) : MessageData := .ofLazy (fun ctx? => do let msg ← ofFormatWithInfos <$> match ctx? with | .none => pure (format constName) | .some ctx => let ctx := if fullNames then { ctx with opts := ctx.opts.insert `pp.fullNames fullNames } else ctx ppConstNameWithInfos ctx constName return Dynamic.mk msg) (fun _ => false) partial def hasSyntheticSorry (msg : MessageData) : Bool := visit none msg where visit (mctx? : Option MetavarContext) : MessageData → Bool | ofLazy _ f => f (mctx?.getD {}) | withContext ctx msg => visit ctx.mctx msg | withNamingContext _ msg => visit mctx? msg | nest _ msg => visit mctx? msg | group msg => visit mctx? msg | compose msg₁ msg₂ => visit mctx? msg₁ || visit mctx? msg₂ | tagged _ msg => visit mctx? msg | trace _ msg msgs => visit mctx? msg || msgs.any (visit mctx?) | _ => false partial def formatAux : NamingContext → Option MessageDataContext → MessageData → IO Format | _, _, ofFormatWithInfos fmt => return fmt.1 | _, none, ofGoal mvarId => return "goal " ++ format (mkMVar mvarId) | nCtx, some ctx, ofGoal mvarId => ppGoal (mkPPContext nCtx ctx) mvarId | nCtx, ctx, ofWidget _ d => formatAux nCtx ctx d | nCtx, _, withContext ctx d => formatAux nCtx ctx d | _, ctx, withNamingContext nCtx d => formatAux nCtx ctx d | nCtx, ctx, tagged _ d => formatAux nCtx ctx d | nCtx, ctx, nest n d => Format.nest n <$> formatAux nCtx ctx d | nCtx, ctx, compose d₁ d₂ => return (← formatAux nCtx ctx d₁) ++ (← formatAux nCtx ctx d₂) | nCtx, ctx, group d => Format.group <$> formatAux nCtx ctx d | nCtx, ctx, trace data header children => do let mut msg := f!"[{data.cls}]" if data.startTime != 0 then msg := f!"{msg} [{data.stopTime - data.startTime}]" msg := f!"{msg} {(← formatAux nCtx ctx header).nest 2}" let children ← children.mapM (formatAux nCtx ctx) return .nest 2 (.joinSep (msg::children.toList) "\n") | nCtx, ctx?, ofLazy pp _ => do let dyn ← pp (ctx?.map (mkPPContext nCtx)) let some msg := dyn.get? MessageData | panic! s!"MessageData.ofLazy: expected MessageData in Dynamic, got {dyn.typeName}" formatAux nCtx ctx? msg protected def format (msgData : MessageData) : IO Format := formatAux { currNamespace := Name.anonymous, openDecls := [] } none msgData protected def toString (msgData : MessageData) : IO String := do return toString (← msgData.format) instance : Append MessageData := ⟨compose⟩ instance : Coe String MessageData := ⟨ofFormat ∘ format⟩ instance : Coe Format MessageData := ⟨ofFormat⟩ instance : Coe Level MessageData := ⟨ofLevel⟩ instance : Coe Expr MessageData := ⟨ofExpr⟩ instance : Coe Name MessageData := ⟨ofName⟩ instance : Coe Syntax MessageData := ⟨ofSyntax⟩ instance : Coe MVarId MessageData := ⟨ofGoal⟩ instance : Coe (Option Expr) MessageData := ⟨fun o => match o with | none => "none" | some e => ofExpr e⟩ partial def arrayExpr.toMessageData (es : Array Expr) (i : Nat) (acc : MessageData) : MessageData := if h : i < es.size then let e := es.get ⟨i, h⟩; let acc := if i == 0 then acc ++ ofExpr e else acc ++ ", " ++ ofExpr e; toMessageData es (i+1) acc else acc ++ "]" instance : Coe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩ /-- Wrap the given message in `l` and `r`. See also `Format.bracket`. -/ def bracket (l : String) (f : MessageData) (r : String) : MessageData := group (nest l.length <| l ++ f ++ r) /-- Wrap the given message in parentheses `()`. -/ def paren (f : MessageData) : MessageData := bracket "(" f ")" /-- Wrap the given message in square brackets `[]`. -/ def sbracket (f : MessageData) : MessageData := bracket "[" f "]" /-- Append the given list of messages with the given separator. -/ def joinSep : List MessageData → MessageData → MessageData | [], _ => Format.nil | [a], _ => a | a::as, sep => a ++ sep ++ joinSep as sep /-- Write the given list of messages as a list, separating each item with `,\n` and surrounding with square brackets. -/ def ofList : List MessageData → MessageData | [] => "[]" | xs => sbracket <| joinSep xs (ofFormat "," ++ Format.line) /-- See `MessageData.ofList`. -/ def ofArray (msgs : Array MessageData) : MessageData := ofList msgs.toList /-- Puts `MessageData` into a comma-separated list with `"or"` at the back (no Oxford comma). Best used on non-empty lists; returns `"– none –"` for an empty list. -/ def orList (xs : List MessageData) : MessageData := match xs with | [] => "– none –" | [x] => "'" ++ x ++ "'" | _ => joinSep (xs.dropLast.map (fun x => "'" ++ x ++ "'")) ", " ++ " or '" ++ xs.getLast! ++ "'" /-- Puts `MessageData` into a comma-separated list with `"and"` at the back (no Oxford comma). Best used on non-empty lists; returns `"– none –"` for an empty list. -/ def andList (xs : List MessageData) : MessageData := match xs with | [] => "– none –" | [x] => x | _ => joinSep xs.dropLast ", " ++ " and " ++ xs.getLast! instance : Coe (List MessageData) MessageData := ⟨ofList⟩ instance : Coe (List Expr) MessageData := ⟨fun es => ofList <| es.map ofExpr⟩ end MessageData /-- A `BaseMessage` is a richly formatted piece of information emitted by Lean. They are rendered by client editors in the infoview and in diagnostic windows. There are two varieties in the Lean core: * `Message`: Uses structured, effectful `MessageData` for formatting content. * `SerialMessage`: Stores pure `String` data. Obtained by running the effectful `Message.serialize`. -/ structure BaseMessage (α : Type u) where fileName : String pos : Position endPos : Option Position := none /-- If `true`, report range as given; see `msgToInteractiveDiagnostic`. -/ keepFullRange : Bool := false severity : MessageSeverity := MessageSeverity.error caption : String := "" /-- The content of the message. -/ data : α deriving Inhabited, ToJson, FromJson /-- A `Message` is a richly formatted piece of information emitted by Lean. They are rendered by client editors in the infoview and in diagnostic windows. -/ abbrev Message := BaseMessage MessageData /-- A `SerialMessage` is a `Message` whose `MessageData` has been eagerly serialized and is thus appropriate for use in pure contexts where the effectful `MessageData.toString` cannot be used. -/ abbrev SerialMessage := BaseMessage String namespace SerialMessage @[inline] def toMessage (msg : SerialMessage) : Message := {msg with data := msg.data} protected def toString (msg : SerialMessage) (includeEndPos := false) : String := Id.run do let mut str := msg.data let endPos := if includeEndPos then msg.endPos else none unless msg.caption == "" do str := msg.caption ++ ":\n" ++ str match msg.severity with | .information => pure () | .warning => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "warning: " ++ str | .error => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "error: " ++ str if str.isEmpty || str.back != '\n' then str := str ++ "\n" return str instance : ToString SerialMessage := ⟨SerialMessage.toString⟩ end SerialMessage namespace Message @[inline] def serialize (msg : Message) : IO SerialMessage := do return {msg with data := ← msg.data.toString} protected def toString (msg : Message) (includeEndPos := false) : IO String := do -- Remark: The inline here avoids a new message allocation when `msg` is shared return inline <| (← msg.serialize).toString includeEndPos protected def toJson (msg : Message) : IO Json := do -- Remark: The inline here avoids a new message allocation when `msg` is shared return inline <| toJson (← msg.serialize) end Message /-- A persistent array of messages. In the Lean elaborator, we use a fresh message log per command but may also report diagnostics at various points inside a command, which will empty `unreported` and updated `hadErrors` accordingly (see `CoreM.getAndEmptyMessageLog`). -/ structure MessageLog where /-- If true, there was an error in the log previously that has already been reported to the user and removed from the log. Thus we say that in the current context (usually the current command), we "have errors" if either this flag is set or there is an error in `msgs`; see `MessageLog.hasErrors`. If we have errors, we suppress some error messages that are often the result of a previous error. -/ /- Design note: We considered introducing a `hasErrors` field instead that already includes the presence of errors in `msgs` but this would not be compatible with e.g. `MessageLog.errorsToWarnings`. -/ hadErrors : Bool := false /-- The list of messages not already reported, in insertion order. -/ unreported : PersistentArray Message := {} /-- Set of message kinds that have been added to the log. For example, we have the kind `unsafe.exponentiation.warning` for warning messages associated with the configuration option `exponentiation.threshold`. We don't produce a warning if the kind is already in the following set. -/ reportedKinds : NameSet := {} deriving Inhabited namespace MessageLog def empty : MessageLog := {} @[deprecated "renamed to `unreported`; direct access should in general be avoided in favor of \ using `MessageLog.toList/toArray`" (since := "2024-05-22")] def msgs : MessageLog → PersistentArray Message := unreported def hasUnreported (log : MessageLog) : Bool := !log.unreported.isEmpty def add (msg : Message) (log : MessageLog) : MessageLog := { log with unreported := log.unreported.push msg } protected def append (l₁ l₂ : MessageLog) : MessageLog := { hadErrors := l₁.hadErrors || l₂.hadErrors, unreported := l₁.unreported ++ l₂.unreported } instance : Append MessageLog := ⟨MessageLog.append⟩ def hasErrors (log : MessageLog) : Bool := log.hadErrors || log.unreported.any (·.severity matches .error) def errorsToWarnings (log : MessageLog) : MessageLog := { unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) } def getInfoMessages (log : MessageLog) : MessageLog := { unreported := log.unreported.filter fun m => match m.severity with | MessageSeverity.information => true | _ => false } def forM {m : Type → Type} [Monad m] (log : MessageLog) (f : Message → m Unit) : m Unit := log.unreported.forM f /-- Converts the unreported messages to a list, oldest message first. -/ def toList (log : MessageLog) : List Message := log.unreported.toList /-- Converts the unreported messages to an array, oldest message first. -/ def toArray (log : MessageLog) : Array Message := log.unreported.toArray end MessageLog def MessageData.nestD (msg : MessageData) : MessageData := MessageData.nest 2 msg def indentD (msg : MessageData) : MessageData := MessageData.nestD (Format.line ++ msg) def indentExpr (e : Expr) : MessageData := indentD e class AddMessageContext (m : Type → Type) where /-- Without context, a `MessageData` object may be missing information (e.g. hover info) for pretty printing, or may print an error. Hence, `addMessageContext` should be called on all constructed `MessageData` (e.g. via `m!`) before taking it out of context (e.g. leaving `MetaM` or `CoreM`). -/ addMessageContext : MessageData → m MessageData export AddMessageContext (addMessageContext) instance (m n) [MonadLift m n] [AddMessageContext m] : AddMessageContext n where addMessageContext := fun msg => liftM (addMessageContext msg : m _) def addMessageContextPartial {m} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData := do let env ← getEnv let opts ← getOptions return MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msgData def addMessageContextFull {m} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData := do let env ← getEnv let mctx ← getMCtx let lctx ← getLCtx let opts ← getOptions return MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData class ToMessageData (α : Type) where toMessageData : α → MessageData export ToMessageData (toMessageData) def stringToMessageData (str : String) : MessageData := let lines := str.split (· == '\n') let lines := lines.map (MessageData.ofFormat ∘ format) MessageData.joinSep lines (MessageData.ofFormat Format.line) instance [ToFormat α] : ToMessageData α := ⟨MessageData.ofFormat ∘ format⟩ instance : ToMessageData Expr := ⟨MessageData.ofExpr⟩ instance : ToMessageData Level := ⟨MessageData.ofLevel⟩ instance : ToMessageData Name := ⟨MessageData.ofName⟩ instance : ToMessageData String := ⟨stringToMessageData⟩ instance : ToMessageData Syntax := ⟨MessageData.ofSyntax⟩ instance : ToMessageData (TSyntax k) := ⟨(MessageData.ofSyntax ·)⟩ instance : ToMessageData Format := ⟨MessageData.ofFormat⟩ instance : ToMessageData MVarId := ⟨MessageData.ofGoal⟩ @[default_instance] instance : ToMessageData MessageData := ⟨id⟩ instance [ToMessageData α] : ToMessageData (List α) := ⟨fun as => MessageData.ofList <| as.map toMessageData⟩ instance [ToMessageData α] : ToMessageData (Array α) := ⟨fun as => toMessageData as.toList⟩ instance [ToMessageData α] : ToMessageData (Subarray α) := ⟨fun as => toMessageData as.toArray.toList⟩ instance [ToMessageData α] : ToMessageData (Option α) := ⟨fun | none => "none" | some e => "some (" ++ toMessageData e ++ ")"⟩ instance [ToMessageData α] [ToMessageData β] : ToMessageData (α × β) := ⟨fun (a, b) => .paren <| toMessageData a ++ "," ++ Format.line ++ toMessageData b⟩ instance : ToMessageData (Option Expr) := ⟨fun | none => "" | some e => toMessageData e⟩ syntax:max "m!" interpolatedStr(term) : term macro_rules | `(m! $interpStr) => do interpStr.expandInterpolatedStr (← `(MessageData)) (← `(toMessageData)) def toMessageList (msgs : Array MessageData) : MessageData := indentD (MessageData.joinSep msgs.toList m!"\n\n") namespace KernelException private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData := MessageData.withContext { env := env, mctx := {}, lctx := lctx, opts := opts } msg def toMessageData (e : KernelException) (opts : Options) : MessageData := match e with | unknownConstant env constName => mkCtx env {} opts m!"(kernel) unknown constant '{constName}'" | alreadyDeclared env constName => mkCtx env {} opts m!"(kernel) constant has already been declared '{.ofConstName constName true}'" | declTypeMismatch env decl givenType => mkCtx env {} opts <| let process (n : Name) (expectedType : Expr) : MessageData := m!"(kernel) declaration type mismatch, '{n}' has type{indentExpr givenType}\nbut it is expected to have type{indentExpr expectedType}"; match decl with | Declaration.defnDecl { name := n, type := type, .. } => process n type | Declaration.thmDecl { name := n, type := type, .. } => process n type | _ => "(kernel) declaration type mismatch" -- TODO fix type checker, type mismatch for mutual decls does not have enough information | declHasMVars env constName _ => mkCtx env {} opts m!"(kernel) declaration has metavariables '{.ofConstName constName true}'" | declHasFVars env constName _ => mkCtx env {} opts m!"(kernel) declaration has free variables '{.ofConstName constName true}'" | funExpected env lctx e => mkCtx env lctx opts m!"(kernel) function expected{indentExpr e}" | typeExpected env lctx e => mkCtx env lctx opts m!"(kernel) type expected{indentExpr e}" | letTypeMismatch env lctx n _ _ => mkCtx env lctx opts m!"(kernel) let-declaration type mismatch '{n}'" | exprTypeMismatch env lctx e _ => mkCtx env lctx opts m!"(kernel) type mismatch at{indentExpr e}" | appTypeMismatch env lctx e fnType argType => mkCtx env lctx opts m!"application type mismatch{indentExpr e}\nargument has type{indentExpr argType}\nbut function has type{indentExpr fnType}" | invalidProj env lctx e => mkCtx env lctx opts m!"(kernel) invalid projection{indentExpr e}" | thmTypeIsNotProp env constName type => mkCtx env {} opts m!"(kernel) type of theorem '{.ofConstName constName true}' is not a proposition{indentExpr type}" | other msg => m!"(kernel) {msg}" | deterministicTimeout => "(kernel) deterministic timeout" | excessiveMemory => "(kernel) excessive memory consumption detected" | deepRecursion => "(kernel) deep recursion detected" | interrupted => "(kernel) interrupted" end KernelException end Lean