-- | Diagnostics related to execution of metaprograms.
module Mikan.TypeChecking.Unquote.Errors where

import Control.DeepSeq

import Data.Map.Strict qualified as Map
import Data.Text qualified as Text

import GHC.Generics

import Mikan.Interaction.Library.Base

import Mikan.Syntax.Common.Pretty qualified as P
import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Internal as I
import Mikan.Syntax.Common

import Mikan.TypeChecking.Monad.Diagnostic
import Mikan.TypeChecking.Monad.Closure
import Mikan.TypeChecking.Monad.Base
import Mikan.TypeChecking.Pretty

import Mikan.Utils.Singleton

-- | An error raised during execution of a metaprogram.
data UnquoteError
  = BlockedOnMeta TCState Blocker
  | CannotDeclareHiddenFunction QName
      -- ^ Attempt to @unquoteDecl@ with 'Hiding' other than 'NotHidden'.
  | CommitAfterDef
  | ConInsteadOfDef QName String String
  | DefineDataNotData QName
  | DefInsteadOfCon QName String String
  | EscapingVariable (Closure Term)
      -- ^ Given meta-program produces unbound variable under @extendContext@.
  | FreshNameWhileElaborating
  | MissingDeclaration QName
  | MissingDefinition QName
  | NakedUnquote
  | NonCanonical String I.Term
  | PatLamWithoutClauses I.Term
  | StaleMeta TopLevelModuleName MetaId
      -- ^ Attempt to unquote a serialized meta.
  | TooManyParameters Nat A.Expr
      -- ^ Attempt to shave of 'Nat' many parameters from function type 'A.Expr'.
  | UnboundName QName
  deriving (Int -> UnquoteError -> ShowS
[UnquoteError] -> ShowS
UnquoteError -> String
(Int -> UnquoteError -> ShowS)
-> (UnquoteError -> String)
-> ([UnquoteError] -> ShowS)
-> Show UnquoteError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnquoteError -> ShowS
showsPrec :: Int -> UnquoteError -> ShowS
$cshow :: UnquoteError -> String
show :: UnquoteError -> String
$cshowList :: [UnquoteError] -> ShowS
showList :: [UnquoteError] -> ShowS
Show, (forall x. UnquoteError -> Rep UnquoteError x)
-> (forall x. Rep UnquoteError x -> UnquoteError)
-> Generic UnquoteError
forall x. Rep UnquoteError x -> UnquoteError
forall x. UnquoteError -> Rep UnquoteError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. UnquoteError -> Rep UnquoteError x
from :: forall x. UnquoteError -> Rep UnquoteError x
$cto :: forall x. Rep UnquoteError x -> UnquoteError
to :: forall x. Rep UnquoteError x -> UnquoteError
Generic)

-- | Error when trying to call an external executable during reflection.
data ExecError
  = ExeNotTrusted ExeName ExeMap
      -- ^ The given executable is not listed as trusted.
  | ExeNotFound ExeName FilePath
      -- ^ The given executable could not be found under the given path.
  | ExeNotExecutable ExeName FilePath
      -- ^ The given file path does not have executable permissions.
  deriving (Int -> ExecError -> ShowS
[ExecError] -> ShowS
ExecError -> String
(Int -> ExecError -> ShowS)
-> (ExecError -> String)
-> ([ExecError] -> ShowS)
-> Show ExecError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExecError -> ShowS
showsPrec :: Int -> ExecError -> ShowS
$cshow :: ExecError -> String
show :: ExecError -> String
$cshowList :: [ExecError] -> ShowS
showList :: [ExecError] -> ShowS
Show, (forall x. ExecError -> Rep ExecError x)
-> (forall x. Rep ExecError x -> ExecError) -> Generic ExecError
forall x. Rep ExecError x -> ExecError
forall x. ExecError -> Rep ExecError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ExecError -> Rep ExecError x
from :: forall x. ExecError -> Rep ExecError x
$cto :: forall x. Rep ExecError x -> ExecError
to :: forall x. Rep ExecError x -> ExecError
Generic)

instance NFData UnquoteError
instance NFData ExecError

instance PrettyTCM UnquoteError where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => UnquoteError -> m Doc
prettyTCM = \case

    BlockedOnMeta TCState
_ Blocker
m -> [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 -> [m Doc]) -> String -> [m Doc]
forall a b. (a -> b) -> a -> b
$ String
"Unquote failed because of unsolved meta variables."

    CannotDeclareHiddenFunction QName
f -> [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 declare hidden function" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f ]

    UnquoteError
CommitAfterDef -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Cannot use commitTC after declaring new definitions"

    ConInsteadOfDef QName
x String
def String
con -> [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
"Use " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
con String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" instead of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
def String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" for constructor") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x]

    DefineDataNotData QName
x -> [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
$
      [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is not declared as a datatype or record, or it already has a definition."

    DefInsteadOfCon QName
x String
def String
con -> [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
"Use " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
def String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" instead of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
con String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" for non-constructor")
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x]

    EscapingVariable Closure Term
v -> Closure Term -> (Term -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure Term
v \ Term
v ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat [m Doc
"Local variable '", Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Term
var Int
0), m Doc
"' escaping in result of extendContext:"]
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v

    UnquoteError
FreshNameWhileElaborating -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Generating new names in an edit-time macro is not supported"

    MissingDeclaration QName
x -> [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
"Missing declaration for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x ]

    MissingDefinition QName
x -> [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
"Missing definition for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x ]

    UnquoteError
NakedUnquote -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"`unquote' must be applied to a term"

    NonCanonical String
kind Term
t ->
      String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String
"Cannot unquote non-canonical " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
kind)
      m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t)

    PatLamWithoutClauses Term
_ -> [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 unquote pattern lambda without clauses. Use a single `absurd-clause` for absurd lambdas."

    StaleMeta TopLevelModuleName
m MetaId
x ->
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ m Doc
"Cannot unquote stale metavariable"
        , TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
m m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"._" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Word64 -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (MetaId -> Word64
metaId MetaId
x)
        ]

    TooManyParameters Int
npars Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ [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
"Cannot shave", [Int -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
npars], String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"parameters off type" ]
      , Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e
      ]

    UnboundName QName
x -> [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
"Unbound name:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x]

instance Diagnostic UnquoteError where
  diagnosticReason :: UnquoteError -> DiagnosticReason
diagnosticReason UnquoteError
_ = DiagnosticReason
DiagError
  diagnosticString :: UnquoteError -> String
diagnosticString = \case
    BlockedOnMeta               {} -> String
"Unquote.BlockedOnMeta"
    CannotDeclareHiddenFunction {} -> String
"Unquote.CannotDeclareHiddenFunction"
    CommitAfterDef              {} -> String
"Unquote.CommitAfterDef"
    ConInsteadOfDef             {} -> String
"Unquote.ConInsteadOfDef"
    DefineDataNotData           {} -> String
"Unquote.DefineDataNotData"
    DefInsteadOfCon             {} -> String
"Unquote.DefInsteadOfCon"
    EscapingVariable            {} -> String
"Unquote.EscapingVariable"
    FreshNameWhileElaborating   {} -> String
"Unquote.FreshNameWhileElaborating"
    MissingDeclaration          {} -> String
"Unquote.MissingDeclaration"
    MissingDefinition           {} -> String
"Unquote.MissingDefinition"
    NakedUnquote                {} -> String
"Unquote.NakedUnquote"
    NonCanonical                {} -> String
"Unquote.NonCanonical"
    PatLamWithoutClauses        {} -> String
"Unquote.PatLamWithoutClauses"
    StaleMeta                   {} -> String
"Unquote.StaleMeta"
    TooManyParameters           {} -> String
"Unquote.TooManyParameters"
    UnboundName                 {} -> String
"Unquote.UnboundName"

instance PrettyTCM ExecError where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => ExecError -> m Doc
prettyTCM = \case
    ExeNotTrusted ExeName
exe ExeMap
exes -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      ([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
"Could not find"
         , ExeName -> [m Doc]
forall (m :: * -> *) a. (MonadPretty m, Pretty a) => a -> [m Doc]
q ExeName
exe
         , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"in list of trusted executables:"
         ]) m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
      [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"  - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExeName -> String
Text.unpack ExeName
exe | ExeName
exe <- ExeMap -> [ExeName]
forall k a. Map k a -> [k]
Map.keys ExeMap
exes ]

    ExeNotFound ExeName
exe String
fp -> [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
"Could not find file"
      , String -> [m Doc]
forall (m :: * -> *) a. (MonadPretty m, Pretty a) => a -> [m Doc]
q String
fp
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"for trusted executable"
      , String -> [m Doc]
forall (m :: * -> *) a. (MonadPretty m, Pretty a) => a -> [m Doc]
q String
fp
      ]

    ExeNotExecutable ExeName
exe String
fp -> [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
      [ [ m Doc
"File" ]
      , String -> [m Doc]
forall (m :: * -> *) a. (MonadPretty m, Pretty a) => a -> [m Doc]
q String
fp
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"for trusted executable"
      , ExeName -> [m Doc]
forall (m :: * -> *) a. (MonadPretty m, Pretty a) => a -> [m Doc]
q ExeName
exe
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"does not have permission to execute"
      ]

    where
      q :: (MonadPretty m, P.Pretty a) => a -> [m Doc]
      q :: forall (m :: * -> *) a. (MonadPretty m, Pretty a) => a -> [m Doc]
q = m Doc -> [m Doc]
forall el coll. Singleton el coll => el -> coll
singleton (m Doc -> [m Doc]) -> (a -> m Doc) -> a -> [m Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
quotes (m Doc -> m Doc) -> (a -> m Doc) -> a -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty

instance Diagnostic ExecError where
  diagnosticReason :: ExecError -> DiagnosticReason
diagnosticReason ExecError
_ = DiagnosticReason
DiagError
  diagnosticString :: ExecError -> String
diagnosticString = \case
    ExeNotTrusted    {} -> String
"Exec.ExeNotTrusted"
    ExeNotFound      {} -> String
"Exec.ExeNotFound"
    ExeNotExecutable {} -> String
"Exec.ExeNotExecutable"