/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Util.Sorry
import Lean.Message

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
