-- | Diagnostics raised during interactive use.
module Mikan.Interaction.Errors
  ( InteractionError(..)
  )
  where

import Control.DeepSeq

import GHC.Generics

import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Concrete qualified as C
import Mikan.Syntax.Common.Pretty (prettyShow)
import Mikan.Syntax.Common

import Mikan.TypeChecking.Monad.Diagnostic
import Mikan.TypeChecking.Pretty

-- | Errors raised in @--interaction@ mode.
data InteractionError
  = CannotGive A.Expr
    -- ^ Failure of the 'give' interactive tactic.
  | CannotRefine String
    -- ^ Failure of the 'refine' interactive tactic.
  | CaseSplitError Doc
    -- ^ Failure of the 'makeCase' interactive tactic.
  | ExpectedIdentifier C.Expr
    -- ^ Expected the given expression to be an identifier.
  | ExpectedApplication
    -- ^ Expected an argument of the form @f e1 e2 .. en@.
  | NoActionForInteractionPoint InteractionId
    -- ^ Interaction point has not been reached during type checking.
  | NoSuchInteractionPoint InteractionId
    -- ^ 'InteractionId' does not resolve to an 'InteractionPoint'.
  | UnexpectedWhere
    -- ^ @where@ not allowed in hole.
  deriving (Int -> InteractionError -> ShowS
[InteractionError] -> ShowS
InteractionError -> String
(Int -> InteractionError -> ShowS)
-> (InteractionError -> String)
-> ([InteractionError] -> ShowS)
-> Show InteractionError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InteractionError -> ShowS
showsPrec :: Int -> InteractionError -> ShowS
$cshow :: InteractionError -> String
show :: InteractionError -> String
$cshowList :: [InteractionError] -> ShowS
showList :: [InteractionError] -> ShowS
Show, (forall x. InteractionError -> Rep InteractionError x)
-> (forall x. Rep InteractionError x -> InteractionError)
-> Generic InteractionError
forall x. Rep InteractionError x -> InteractionError
forall x. InteractionError -> Rep InteractionError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. InteractionError -> Rep InteractionError x
from :: forall x. InteractionError -> Rep InteractionError x
$cto :: forall x. Rep InteractionError x -> InteractionError
to :: forall x. Rep InteractionError x -> InteractionError
Generic)

instance NFData InteractionError

instance Diagnostic InteractionError where
  diagnosticReason :: InteractionError -> DiagnosticReason
diagnosticReason InteractionError
_ = DiagnosticReason
DiagError
  diagnosticString :: InteractionError -> String
diagnosticString = \case
    CannotGive{}                  -> String
"Interaction.CannotGive"
    CannotRefine{}                -> String
"Interaction.CannotRefine"
    CaseSplitError{}              -> String
"Interaction.CaseSplitError"
    ExpectedIdentifier{}          -> String
"Interaction.ExpectedIdentifier"
    ExpectedApplication{}         -> String
"Interaction.ExpectedApplication"
    NoActionForInteractionPoint{} -> String
"Interaction.NoActionForInteractionPoint"
    NoSuchInteractionPoint{}      -> String
"Interaction.NoSuchInteractionPoint"
    UnexpectedWhere{}             -> String
"Interaction.UnexpectedWhere"

instance PrettyTCM InteractionError where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => InteractionError -> m Doc
prettyTCM = \case
    CannotGive Expr
e       -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Failed to give" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e ]

    CannotRefine String
s     -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot refine" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
s

    CaseSplitError Doc
doc -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
doc

    ExpectedIdentifier Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Expected identifier, but found:"
      , m Doc -> [m Doc]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m Doc -> [m Doc]) -> m Doc -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e
      ]

    InteractionError
ExpectedApplication -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Expected an argument of the form f e1 e2 .. en"

    NoActionForInteractionPoint InteractionId
ii -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"No type nor action available for hole " String -> ShowS
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Pretty a => a -> String
prettyShow InteractionId
ii String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
      , String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"Possible cause: the hole has not been reached during type checking (do you see yellow?)"
      ]

    NoSuchInteractionPoint InteractionId
ii ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ m Doc
"Unknown", m Doc
"interaction", m Doc
"point", InteractionId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => InteractionId -> m Doc
prettyTCM InteractionId
ii ]

    InteractionError
UnexpectedWhere -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"`where' clauses are not supported in holes"