/-
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.Environment
import Lean.MetavarContext
import Lean.Message
import Lean.Util.PPGoal

namespace Lean
namespace Meta

abbrev ExceptionContext := MessageDataContext

inductive Bug
| overwritingExprMVar (mvarId : Name)

inductive Exception
| unknownConst         (constName : Name) (ctx : ExceptionContext)
| unknownFVar          (fvarId : FVarId) (ctx : ExceptionContext)
| unknownExprMVar      (mvarId : MVarId) (ctx : ExceptionContext)
| unknownLevelMVar     (mvarId : MVarId) (ctx : ExceptionContext)
| unexpectedBVar       (bvarIdx : Nat)
| functionExpected     (f a : Expr) (ctx : ExceptionContext)
| typeExpected         (type : Expr) (ctx : ExceptionContext)
| incorrectNumOfLevels (constName : Name) (constLvls : List Level) (ctx : ExceptionContext)
| invalidProjection    (structName : Name) (idx : Nat) (s : Expr) (ctx : ExceptionContext)
| revertFailure        (toRevert : Array Expr) (decl : LocalDecl) (ctx : ExceptionContext)
| readOnlyMVar         (mvarId : MVarId) (ctx : ExceptionContext)
| isLevelDefEqStuck    (u v : Level) (ctx : ExceptionContext)
| isExprDefEqStuck     (t s : Expr) (ctx : ExceptionContext)
| letTypeMismatch      (fvarId : FVarId) (ctx : ExceptionContext)
| appTypeMismatch      (f a : Expr) (ctx : ExceptionContext)
| notInstance          (e : Expr) (ctx : ExceptionContext)
| appBuilder           (op : Name) (msg : MessageData) (ctx : ExceptionContext)
| synthInstance        (inst : Expr) (ctx : ExceptionContext)
| tactic               (ref : Syntax) (tacticName : Name) (mvarId : MVarId) (msg : MessageData) (ctx : ExceptionContext)
| generalizeTelescope  (es : Array Expr) (ctx : ExceptionContext)
| kernel               (ex : KernelException) (opts : Options)
| bug                  (b : Bug) (ctx : ExceptionContext)
| other                (ref : Syntax) (msg : MessageData)

namespace Exception
instance : Inhabited Exception := ⟨other Syntax.missing ""⟩

def getRef : Exception → Syntax
| tactic ref _ _ _ _ => ref
| other ref _        => ref
| _                  => Syntax.missing

-- TODO: improve, use (to be implemented) pretty printer
def toStr : Exception → String
| unknownConst c _              => "unknown constant '" ++ toString c ++ "'"
| unknownFVar fvarId _          => "unknown free variable '" ++ toString fvarId ++ "'"
| unknownExprMVar mvarId _      => "unknown metavariable '" ++ toString mvarId ++ "'"
| unknownLevelMVar mvarId _     => "unknown universe level metavariable '" ++ toString mvarId ++ "'"
| unexpectedBVar bvarIdx        => "unexpected loose bound variable #" ++ toString bvarIdx
| functionExpected fType args _ => "function expected"
| typeExpected _ _              => "type expected"
| incorrectNumOfLevels c lvls _ => "incorrect number of universe levels for '" ++ toString c ++ "' " ++ toString lvls
| invalidProjection _ _ _ _     => "invalid projection"
| revertFailure _ _ _           => "revert failure"
| readOnlyMVar _ _              => "try to assign read only metavariable"
| isLevelDefEqStuck _ _ _       => "isDefEq is stuck"
| isExprDefEqStuck _ _ _        => "isDefEq is stuck"
| letTypeMismatch _ _           => "type mismatch at let-expression"
| appTypeMismatch _ _ _         => "application type mismatch"
| notInstance _ _               => "type class instance expected"
| appBuilder _ _ _              => "application builder failure"
| synthInstance _ _             => "type class instance synthesis failed"
| tactic _ tacName _ _ _        => "tactic '" ++ toString tacName ++ "' failed"
| generalizeTelescope _ _       => "generalize telescope"
| kernel _ _                    => "kernel exception"
| bug _ _                       => "bug"
| other _ s                     => toString $ fmt s

instance : HasToString Exception := ⟨toStr⟩

def mkCtx (ctx : ExceptionContext) (m : MessageData) : MessageData :=
MessageData.withContext ctx m

/-- Generate trace message that is suitable for tracing crawlers -/
def toTraceMessageData : Exception → MessageData
| unknownConst c ctx              => mkCtx ctx $ `unknownConst ++ " " ++ c
| unknownFVar fvarId ctx          => mkCtx ctx $ `unknownFVar ++ " " ++ fvarId
| unknownExprMVar mvarId ctx      => mkCtx ctx $ `unknownExprMVar ++ " " ++ mkMVar mvarId
| unknownLevelMVar mvarId ctx     => mkCtx ctx $ `unknownLevelMVar ++ " " ++ mkLevelMVar mvarId
| unexpectedBVar bvarIdx          => `unexpectedBVar ++ " " ++ mkBVar bvarIdx
| functionExpected f a ctx        => mkCtx ctx $ `functionExpected ++ " " ++ mkApp f a
| typeExpected t ctx              => mkCtx ctx $ `typeExpected ++ " " ++ t
| incorrectNumOfLevels c lvls ctx => mkCtx ctx $ `incorrectNumOfLevels ++ " " ++ mkConst c lvls
| invalidProjection s i e ctx     => mkCtx ctx $ `invalidProjection ++ " " ++ mkProj s i e
| revertFailure xs decl ctx       => mkCtx ctx $ `revertFailure -- TODO improve
| readOnlyMVar mvarId ctx         => mkCtx ctx $ `readOnlyMVar ++ " " ++ mkMVar mvarId
| isLevelDefEqStuck u v ctx       => mkCtx ctx $ `isLevelDefEqStuck ++ " " ++ u ++ " =?= " ++ v
| isExprDefEqStuck t s ctx        => mkCtx ctx $ `isExprDefEqStuck ++ " " ++ t ++ " =?= " ++ s
| letTypeMismatch fvarId ctx      => mkCtx ctx $ `letTypeMismatch ++ " " ++ mkFVar fvarId
| appTypeMismatch f a ctx         => mkCtx ctx $ `appTypeMismatch ++ " " ++ mkApp f a
| notInstance i ctx               => mkCtx ctx $ `notInstance ++ " " ++ i
| appBuilder op msg ctx           => mkCtx ctx $ `appBuilder ++ " " ++ op ++ " " ++ msg
| synthInstance inst ctx          => mkCtx ctx $ `synthInstance ++ " " ++ inst
| tactic _ tacName mvarId msg ctx => mkCtx ctx $ `tacticFailure ++ " " ++ tacName ++ " " ++ msg
| generalizeTelescope es ctx      => mkCtx ctx $ `generalizeTelescope ++ " " ++ es
| kernel ex opts                  => ex.toMessageData opts
| bug _ _                         => "internal bug" -- TODO improve
| other _ s                       => s

end Exception

end Meta
end Lean