-- | The checker monad.
--
-- Responsible for throwing errors and accumulating warnings.

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE TypeFamilies #-}  -- for type equality ~

module BNFC.Check.Monad where

import BNFC.Prelude
import BNFC.CF
import BNFC.Types.Position
import BNFC.Types.Regex     (Regex)

import qualified BNFC.Abs as A

-- * Specification
---------------------------------------------------------------------------

-- | Monad for error reporting and warnings.

class Monad m => MonadCheck m where
  fatalError       :: FatalError       -> m a
  recoverableError :: RecoverableError -> m ()
  warn             :: Warning          -> m ()
  -- | Set the file position for subsequent errors.
  atPosition       :: ToPosition' p => p -> m a -> m a
  -- | Retrieve the stored position.
  askPosition      :: m Position'

  -- lift MonadCheck through monad transformers

  default fatalError
    :: (MonadTrans t, MonadCheck n, t n ~ m)
    => FatalError -> m a
  fatalError = lift . fatalError

  default recoverableError
    :: (MonadTrans t, MonadCheck n, t n ~ m)
    => RecoverableError -> m ()
  recoverableError = lift . recoverableError

  default warn
    :: (MonadTrans t, MonadCheck n, t n ~ m)
    => Warning -> m ()
  warn = lift . warn

  default atPosition
    :: (MonadTransControl t, MonadCheck n, t n ~ m)
    =>  ToPosition' p => p -> m a -> m a
  atPosition = liftThrough . atPosition

  default askPosition
    :: (MonadTrans t, MonadCheck n, t n ~ m)
    => m Position'
  askPosition = lift askPosition

instance MonadCheck m => MonadCheck (ExceptT e m)
instance MonadCheck m => MonadCheck (ReaderT r m)
instance MonadCheck m => MonadCheck (StateT s m)

-- * Warnings and errors
---------------------------------------------------------------------------

-- | Fatal errors (check cannot continue).

data FatalError  = FatalError
  --- Type checking expressions
  | UndefinedLabel LabelName
      -- ^ The given label isn't contained in the 'Signature'.
  | ListsDontInhabitType Type
      -- ^ A list expression was found at the given type, which isn't a 'ListType'.
  deriving Show

-- | Any of these errors allows to continue BNFC, but may result in undesired/illformed output.

data RecoverableError
  = DelimitersNotSupported
      -- ^ The pragma @delimiters@ has been removed in BNFC 2.9.
      --   Pragma is ignored.
  --- Pass 1 errors
  | IncompatibleDefinition ICat Position
      -- ^ E.g. trying to mix ordinary rules with list pragmas or @token@ definitions.
      --   Redefinition is ignored.
  | CoercionsOfCoerceCat
      -- ^ Trying to apply @coercions@ pragma to a 'CoerceCat', e.g. @coercions Exp3 2@.
      --   Pragma is ignored.
  -- Pass 2 errors
  | CoercionsOfBuiltinCat
      -- ^ Trying to apply @coercions@ pragma to a 'BuiltinCat', e.g. @coercions Integer 2@.
      --   Pragma is ignored.
  | CoercionsOfIdentCat
      -- ^ Trying to apply @coercions@ pragma to a 'IdentCat', e.g. @coercions Ident 2@.
      --   Pragma is ignored.
  | CoercionsOfTokenCat
      -- ^ Trying to apply @coercions@ pragma to a 'TokenCat', e.g. @coercions Id 2@.
      --   Pragma is ignored.
  --- Category resolution
  | UnknownCatName CatName
      -- ^ This base category is not defined.
  | CoerceBuiltinCat BuiltinCat
      -- ^ Tried to make a precedence variant of a builtin category, like @Char3@.
  | CoerceIdentCat IdentCat
      -- ^ Tried to make a precedence variant of an ident category, like @Ident3@.
  | CoerceListCat CatName
      -- ^ Tried to make a precedence variant of a list category, like @[Arg3]@.
  | CoerceTokenCat CatName
      -- ^ Tried to make a precedence variant of a token category, like @Id3@.
  --- Rule definition
  | DuplicateLabel LabelName Position
      -- ^ The label 'LabelName' has been defined already, at 'Position'.
  | DuplicateRHS Position
      -- ^ The same BNF rule already exists, at 'Position'.
  --- Type checking special labels
  | InvalidListRule LabelName
      -- ^ Cannot use ordinary or defined labels to construct a list category.
  | InvalidListLabel Type
      -- ^ List label to construct non-list category.
  | InvalidLabelNil  FunType
      -- ^ Invalid type for label @[]@.
  | InvalidLabelCons FunType
      -- ^ Invalid type for label @(:)@.
  | InvalidLabelSg   FunType
      -- ^ Invalid type for label @(:[])@.
  | InvalidLabelWild FunType
      -- ^ Invalid type for label @_@.
  --- Type checking expressions
  | IgnoringUndeclaredFunction
      -- ^ @define@ pragma with unused label is skipped, since we don't have its type.
  | NotEnoughParameters (List1 String1)
      -- ^ Type checker added missing parameters in a @define@.
  | DroppingSpuriousParameters (List1 A.Arg)
      -- ^ These parameters were ignored since they are too many, according to the type.
  | MissingArguments LabelName (List1 Type)
      -- ^ A constructor/function misses arguments of the given types.
  | DroppingSpuriousArguments LabelName (List1 A.Exp)
      -- ^ A constructor/function was given (these) more arguments than needed.
  | ExpectedVsInferredType Type Type
      -- ^ An expression of the first type was expected, but it has the second type.
  --- Token definitions
  | NullableToken CatName Regex
      -- ^ Defined @token@ category matches the empty string.
      -- Such a token can be produced by the lexer when nothing else can be produced,
      -- but then it can be produced infinitely often without making progress.
      -- This may result in a loop in the lexer.
      -- Token definition is kept.
  --- Comments
  | IllformedBlockComment
      -- ^ One of the delimiters of a block comment is empty.
  --- Layout
  | ConflictingUsesOfLayoutKeyword Keyword Position
      -- ^ A keyword appears both in @layout@ and @layout stop@.
      --   The redefinition is ignored.
  -- Final checks
  | EmptyGrammar
      -- ^ No entrypoints have been defined.
      --   This is an error that does not block any other checks,
      --   so it is "recoverable".
      --   But it makes flags failure of the check phase,
      --   because later phases (e.g. parser generation) will crash.
  deriving Show

-- | Any of these warnings drops the useless or redundant definition.

data Warning
  = FooWarning
  --- Error in some backends:
  | LabelClashesWithCategory LabelName Position
      -- ^ The label 'LabelName' clashes with a category of the same name defined at 'Position'.
  --- Coercions
  | IgnoringNullCoercions
      -- ^ @coercions _ 0@ does not add any rules.
  | NonUniformListRule Cat [Cat]
      -- ^ A list rule with different coercion levels of the base category.
      --   Cannot implement faithful printer for such rules.
  --- Type checking expressions
  | ParameterShouldBeLowerCase VarName
      -- ^ Grammar permits upper case parameters, but this isn't Haskell-style
      --   (which is the model for BNFC's expression syntax otherwise).
  | ShadowingParameter VarName
      -- ^ A parameter shadows a previous one.
  | ShadowedByParameter VarName
      -- ^ The given label is shadowed by a parameter, which looks confusing.
  --- Token definitions
  | EmptyToken CatName Regex
      -- ^ Defined @token@ category may not match anything.
  --- Comments
  | IgnoringEmptyLineComment
      -- ^ @comment ""@ is ignored.
  | IgnoringEmptyBlockComment
      -- ^ @comment "" ""@ is ignored.
  --- Layout
  | EmptyLayoutKeyword
      -- ^ @layout [stop] ""@ is simply ignored
  | UndefinedLayoutKeyword Keyword
      -- ^ @layout [stop] kw@ but @kw@ is not mentioned in the grammar.
  | DuplicateLayoutKeyword Keyword Position
      -- ^ This layout keyword already occurred in a pragma of the same kind.
  | DuplicateLayoutTop Position
      -- ^ @layout toplevel@ already appeared at 'Position'.
  deriving Show

-- * Types used only in the checker
---------------------------------------------------------------------------

-- | Intermediated form of categories.  (No builtins/token types recognized yet.)
type ICat = Cat' CatName

-- * Implementation
---------------------------------------------------------------------------

type PFatalError       = WithPosition' FatalError
type PRecoverableError = WithPosition' RecoverableError
type PWarning          = WithPosition' Warning
type PWarnErr          = WithPosition' (Either RecoverableError Warning)

type RecoverableErrors = [PRecoverableError]
type Warnings          = [PWarning]
type WarnErrs          = [PWarnErr]
  -- NB: We could choose a more efficient monoid, like difference lists.

-- | The LBNF checker monad.

newtype Check a = Check { unCheck :: ReaderT Position' (ExceptT PFatalError (Writer WarnErrs)) a }
  deriving (Functor, Applicative, Monad)

runCheck :: Check a -> (Warnings, RecoverableErrors, Either PFatalError a)
runCheck (Check m) = (ws, es, res)
  where
  (res, wes) = runWriter $ runExceptT $ m `runReaderT` Nothing
  (es, ws)   = partitionEithers $ map distributeF2 wes

instance MonadCheck Check where

  fatalError :: FatalError -> Check a
  fatalError e = Check $ do
    p <- ask
    throwError $ WithPosition' p e

  recoverableError :: RecoverableError -> Check ()
  recoverableError e = Check $ do
    p <- ask
    tell [WithPosition' p $ Left e]

  warn :: Warning -> Check ()
  warn w = Check $ do
    p <- ask
    tell [WithPosition' p $ Right w]

  atPosition :: ToPosition' p => p -> Check a -> Check a
  atPosition p (Check m) = Check $ local (const $ toPosition' p) m

  askPosition :: Check Position'
  askPosition = Check ask


-- -}