102 lines
4.3 KiB
Text
102 lines
4.3 KiB
Text
/-
|
|
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
import Lean.Util.Sorry
|
|
|
|
namespace Lean
|
|
|
|
/--
|
|
The `MonadLog` interface for logging error messages.
|
|
-/
|
|
class MonadLog (m : Type → Type) extends MonadFileMap m where
|
|
/-- Return the current reference syntax being used to provide position information. -/
|
|
getRef : m Syntax
|
|
/-- The name of the file being processed. -/
|
|
getFileName : m String
|
|
/-- Return `true` if errors have been logged. -/
|
|
hasErrors : m Bool
|
|
/-- Log a new message. -/
|
|
logMessage : Message → m Unit
|
|
|
|
export MonadLog (getFileName logMessage)
|
|
|
|
instance (m n) [MonadLift m n] [MonadLog m] : MonadLog n where
|
|
getRef := liftM (MonadLog.getRef : m _)
|
|
getFileMap := liftM (getFileMap : m _)
|
|
getFileName := liftM (getFileName : m _)
|
|
hasErrors := liftM (MonadLog.hasErrors : m _)
|
|
logMessage := fun msg => liftM (logMessage msg : m _ )
|
|
|
|
variable [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
|
|
|
|
/--
|
|
Return the position (as `String.pos`) associated with the current reference syntax (i.e., the syntax object returned by `getRef`.)
|
|
-/
|
|
def getRefPos : m String.Pos := do
|
|
let ref ← MonadLog.getRef
|
|
return ref.getPos?.getD 0
|
|
|
|
/--
|
|
Return the line and column numbers associated with the current reference syntax (i.e., the syntax object returned by `getRef`.)
|
|
-/
|
|
def getRefPosition : m Position := do
|
|
let fileMap ← getFileMap
|
|
return fileMap.toPosition (← getRefPos)
|
|
|
|
/-- If `warningAsError` is set to `true`, then warning messages are treated as errors. -/
|
|
register_builtin_option warningAsError : Bool := {
|
|
defValue := false
|
|
descr := "treat warnings as errors"
|
|
}
|
|
|
|
/--
|
|
Log the message `msgData` at the position provided by `ref` with the given `severity`.
|
|
If `getRef` has position information but `ref` does not, we use `getRef`.
|
|
We use the `fileMap` to find the line and column numbers for the error message.
|
|
-/
|
|
def logAt (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity := MessageSeverity.error) : m Unit :=
|
|
unless severity == .error && msgData.hasSyntheticSorry do
|
|
let severity := if severity == .warning && warningAsError.get (← getOptions) then .error else severity
|
|
let ref := replaceRef ref (← MonadLog.getRef)
|
|
let pos := ref.getPos?.getD 0
|
|
let endPos := ref.getTailPos?.getD pos
|
|
let fileMap ← getFileMap
|
|
let msgData ← addMessageContext msgData
|
|
logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos, data := msgData, severity := severity }
|
|
|
|
/-- Log a new error message using the given message data. The position is provided by `ref`. -/
|
|
def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
|
|
logAt ref msgData MessageSeverity.error
|
|
|
|
/-- Log a new warning message using the given message data. The position is provided by `ref`. -/
|
|
def logWarningAt [MonadOptions m] (ref : Syntax) (msgData : MessageData) : m Unit := do
|
|
logAt ref msgData .warning
|
|
|
|
/-- Log a new information message using the given message data. The position is provided by `ref`. -/
|
|
def logInfoAt (ref : Syntax) (msgData : MessageData) : m Unit :=
|
|
logAt ref msgData MessageSeverity.information
|
|
|
|
/-- Log a new error/warning/information message using the given message data and `severity`. The position is provided by `getRef`. -/
|
|
def log (msgData : MessageData) (severity : MessageSeverity := MessageSeverity.error): m Unit := do
|
|
let ref ← MonadLog.getRef
|
|
logAt ref msgData severity
|
|
|
|
/-- Log a new error message using the given message data. The position is provided by `getRef`. -/
|
|
def logError (msgData : MessageData) : m Unit :=
|
|
log msgData MessageSeverity.error
|
|
|
|
/-- Log a new warning message using the given message data. The position is provided by `getRef`. -/
|
|
def logWarning [MonadOptions m] (msgData : MessageData) : m Unit := do
|
|
log msgData (if warningAsError.get (← getOptions) then .error else .warning)
|
|
|
|
/-- Log a new information message using the given message data. The position is provided by `getRef`. -/
|
|
def logInfo (msgData : MessageData) : m Unit :=
|
|
log msgData MessageSeverity.information
|
|
|
|
/-- Log the error message "unknown declaration" -/
|
|
def logUnknownDecl (declName : Name) : m Unit :=
|
|
logError m!"unknown declaration '{declName}'"
|
|
|
|
end Lean
|