{-# LANGUAGE OverloadedStrings #-}
module Agda.Interaction.Command.Reload where

import Agda.Interaction.Imports
  ( CheckResult, Mode (..), crInterface, crMode, crWarnings
  , typeCheckMain, parseSource
  )
import Agda.Interaction.FindFile (SourceFile (..))
import Agda.Interaction.Options (optOnlyScopeChecking)
import Agda.Syntax.Translation.ConcreteToAbstract (importPrimitives)
import Agda.TypeChecking.Errors (applyFlagsToTCWarnings, prettyError)
import Agda.TypeChecking.Monad.Base
  (ModuleCheckMode (..), TypeError (..), TCM, commandLineOptions, iInsideScope, typeError)
import Agda.TypeChecking.Monad.State (setScope)
import Agda.Utils.FileName (AbsolutePath)
import Agda.Utils.Null (unlessNullM)
import Control.Monad.Except (MonadError(..), unless)
import Data.ByteString (ByteString)

import Proof.Assistant.Helpers (toBS)

reload :: Maybe AbsolutePath -> TCM ByteString
reload :: Maybe AbsolutePath -> TCM ByteString
reload Maybe AbsolutePath
Nothing = ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
"Failed to type check."
reload (Just AbsolutePath
file) = do
  CheckResult
checked <- AbsolutePath -> TCM CheckResult
checkFile AbsolutePath
file
  ScopeInfo -> TCM ()
setScope (ScopeInfo -> TCM ()) -> ScopeInfo -> TCM ()
forall a b. (a -> b) -> a -> b
$ Interface -> ScopeInfo
iInsideScope (CheckResult -> Interface
crInterface CheckResult
checked)
  [Declaration]
_ <- ScopeM [Declaration]
importPrimitives
  ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
"Type checked succesfully."
  TCM ByteString -> (TCErr -> TCM ByteString) -> TCM ByteString
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e -> do
    String
s <- TCErr -> TCMT IO String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
prettyError TCErr
e
    ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> TCM ByteString) -> ByteString -> TCM ByteString
forall a b. (a -> b) -> a -> b
$ ByteString
"Failed. " ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> String -> ByteString
toBS String
s

checkFile :: AbsolutePath -> TCM CheckResult
checkFile :: AbsolutePath -> TCM CheckResult
checkFile AbsolutePath
inputFile = do
  CommandLineOptions
opts <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  let mode :: Mode
mode =
        if CommandLineOptions -> Bool
optOnlyScopeChecking CommandLineOptions
opts
          then Mode
ScopeCheck
          else Mode
TypeCheck

  CheckResult
result <- Mode -> Source -> TCM CheckResult
typeCheckMain Mode
mode (Source -> TCM CheckResult) -> TCMT IO Source -> TCM CheckResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SourceFile -> TCMT IO Source
parseSource (AbsolutePath -> SourceFile
SourceFile AbsolutePath
inputFile)

  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (CheckResult -> ModuleCheckMode
crMode CheckResult
result ModuleCheckMode -> ModuleCheckMode -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleCheckMode
ModuleScopeChecked) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO [TCWarning] -> ([TCWarning] -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM ([TCWarning] -> TCMT IO [TCWarning]
forall (m :: * -> *). HasOptions m => [TCWarning] -> m [TCWarning]
applyFlagsToTCWarnings (CheckResult -> [TCWarning]
crWarnings CheckResult
result)) (([TCWarning] -> TCM ()) -> TCM ())
-> ([TCWarning] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ [TCWarning]
ws ->
      TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> TypeError
NonFatalErrors [TCWarning]
ws

  CheckResult -> TCM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
result