{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- | The reserved packaged final-prelude source and its authority-free parser.
module Felix.Prelude
    ( ReservedPreludeSourceInput
    , reservedPreludeSourceInput
    , loadReservedPreludeSourceInput
    , emptyBootstrapSourceInput
    , reservedPreludeSourceOwner
    , reservedPreludeSourceLabel
    , reservedPreludeSourceCanonicalPath
    , reservedPreludeSourceBytes
    , reservedPreludeSourceText
    , rejectOrdinaryPreludeSourceGraph
    , preludeDiagnosticLabel
    , PreludeLoadError(..)
    , renderPreludeLoadError
    , PreludeParseError(..)
    , renderPreludeParseError
    , ReservedParsedPrelude
    , reservedParsedPreludeInput
    , reservedParsedPreludeModule
    , parseReservedPreludeSource
    ) where

import Base
import Felix.Module
import Felix.Parse
import Felix.Parsed.Identity qualified as Parsed
import Felix.Source
import Felix.Source.Graph
import Report.Location
import Syntax.Adapt (SyntaxMaterializationError)
import Syntax.Interface
import Syntax.Pragma

import Control.Exception (IOException, displayException, try)
import Data.ByteString (ByteString)
import Data.ByteString qualified as ByteString
import Data.Text qualified as Text
import Data.Text.Encoding qualified as Text
import Data.Text.Encoding.Error (UnicodeException)
import Paths_felix qualified as Paths


data ReservedPreludeSourceInput = ReservedPreludeSourceInput
    !ModuleName
    !FilePath
    !(Maybe CanonicalPath)
    !ByteString
    !Text

reservedPreludeSourceInput
    :: ByteString
    -> Either UnicodeException ReservedPreludeSourceInput
reservedPreludeSourceInput bytes =
    ReservedPreludeSourceInput
        preludeModuleName
        preludeDiagnosticLabel
        Nothing
        bytes
        <$> Text.decodeUtf8' bytes

data PreludeLoadError
    = PreludeSourceReadFailed !FilePath !Text
    | PreludeSourceCanonicalizationFailed !FilePath !SourceError
    | PreludeSourceUtf8Failed !UnicodeException

instance Show PreludeLoadError where
    show = Text.unpack . renderPreludeLoadError

renderPreludeLoadError :: PreludeLoadError -> Text
renderPreludeLoadError = \case
    PreludeSourceReadFailed path failure ->
        Text.pack path
            <> ": unable to read packaged final prelude: "
            <> failure
    PreludeSourceCanonicalizationFailed path failure ->
        Text.pack path
            <> ": unable to resolve packaged final prelude: "
            <> renderSourceError failure
    PreludeSourceUtf8Failed failure ->
        preludeErrorPrefix
            <> "malformed UTF-8: "
            <> Text.pack (displayException failure)

loadReservedPreludeSourceInput
    :: IO (Either PreludeLoadError ReservedPreludeSourceInput)
loadReservedPreludeSourceInput = do
    path <- Paths.getDataFileName "data/felix-prelude.tex"
    canonicalized <- canonicalizeExistingSourcePath path
    case canonicalized of
        Left failure ->
            pure
                (Left
                    (PreludeSourceCanonicalizationFailed path failure))
        Right canonical -> do
            loaded <- try
                (ByteString.readFile
                    (canonicalPathFilePath canonical))
                :: IO (Either IOException ByteString)
            pure case loaded of
                Left failure ->
                    Left
                        (PreludeSourceReadFailed
                            path
                            (Text.pack (displayException failure)))
                Right bytes ->
                    case Text.decodeUtf8' bytes of
                        Left failure ->
                            Left (PreludeSourceUtf8Failed failure)
                        Right sourceText ->
                            Right
                                (ReservedPreludeSourceInput
                                    preludeModuleName
                                    preludeDiagnosticLabel
                                    (Just canonical)
                                    bytes
                                    sourceText)

-- | Empty final-prelude input used only by focused compiler fixtures.
--
-- Production verification always calls 'loadReservedPreludeSourceInput'.
emptyBootstrapSourceInput :: ReservedPreludeSourceInput
emptyBootstrapSourceInput =
    ReservedPreludeSourceInput
        preludeModuleName
        preludeDiagnosticLabel
        Nothing
        ByteString.empty
        Text.empty

reservedPreludeSourceOwner
    :: ReservedPreludeSourceInput
    -> ModuleName
reservedPreludeSourceOwner
        (ReservedPreludeSourceInput owner _label _canonical _bytes _text) =
    owner

reservedPreludeSourceLabel
    :: ReservedPreludeSourceInput
    -> FilePath
reservedPreludeSourceLabel
        (ReservedPreludeSourceInput _owner label _canonical _bytes _text) =
    label

reservedPreludeSourceCanonicalPath
    :: ReservedPreludeSourceInput
    -> Maybe CanonicalPath
reservedPreludeSourceCanonicalPath
        (ReservedPreludeSourceInput _owner _label canonical _bytes _text) =
    canonical

reservedPreludeSourceBytes
    :: ReservedPreludeSourceInput
    -> ByteString
reservedPreludeSourceBytes
        (ReservedPreludeSourceInput _owner _label _canonical bytes _text) =
    bytes

reservedPreludeSourceText :: ReservedPreludeSourceInput -> Text
reservedPreludeSourceText
        (ReservedPreludeSourceInput
            _owner _label _canonical _bytes sourceText) =
    sourceText

-- | Reject an ordinary source graph containing the physical packaged
-- prelude. Synthetic reserved inputs deliberately have no physical path.
rejectOrdinaryPreludeSourceGraph
    :: ReservedPreludeSourceInput
    -> ResolvedSourceGraph
    -> Either SourceError ()
rejectOrdinaryPreludeSourceGraph sourceInput graph =
    case reservedPreludeSourceCanonicalPath sourceInput of
        Nothing ->
            Right ()
        Just reservedPath ->
            case listToMaybe
                    [ source
                    | node <- sourceGraphNodes graph
                    , let source = sourceNodeResolved node
                    , resolvedSourceCanonicalPath source == reservedPath
                    ] of
                Nothing ->
                    Right ()
                Just source ->
                    Left (PackagedPreludeSelectedAsOrdinarySource source)

preludeDiagnosticLabel :: FilePath
preludeDiagnosticLabel =
    "<felix-prelude>"

data PreludeParseError
    = PreludeLocationRegistrationFailed !LocationRegistrationError
    | PreludeSyntaxPragmaFailed !SyntaxPragmaError
    | PreludeImportNotSupported ![FilePath]
    | PreludeLexicalScanFailed !LexicalScanError
    | PreludeSyntaxDeclarationFailed !SyntaxDeclarationError
    | PreludeLexiconCollision !LexiconCollision
    | PreludeSyntaxDeltaFailed !CanonicalSyntaxCollision
    | PreludeSyntaxInterfaceFailed !SyntaxInterfaceError
    | PreludeSyntaxMaterializationFailed !SyntaxMaterializationError
    | PreludeParseFailed !ParseException
    | PreludeFreshInputFailed !FreshModuleInputError
    | PreludeParsedModuleKeyFailed !Parsed.ParsedModuleKeyError
    | PreludeParseInvariantFailed !Text

instance Show PreludeParseError where
    show = Text.unpack . renderPreludeParseError

renderPreludeParseError :: PreludeParseError -> Text
renderPreludeParseError = \case
    PreludeLocationRegistrationFailed FileIdSpaceExhausted ->
        preludeErrorPrefix
            <> "could not register source locations: file identifier space exhausted"
    PreludeSyntaxPragmaFailed failure ->
        renderSyntaxPragmaError failure
    PreludeImportNotSupported imports ->
        preludeErrorPrefix
            <> "imports are not supported"
            <> case imports of
                [] -> ""
                _ ->
                    ": "
                        <> Text.intercalate
                            ", "
                            (Text.pack . show <$> imports)
    PreludeLexicalScanFailed failure ->
        Text.pack (show failure)
    PreludeSyntaxDeclarationFailed failure ->
        Text.pack (show failure)
    PreludeLexiconCollision collision ->
        Text.pack (show collision)
    PreludeSyntaxDeltaFailed collision ->
        preludeErrorPrefix
            <> "syntax delta has conflicting entries for pattern "
            <> Text.pack (show (canonicalCollisionPattern collision))
            <> ": "
            <> Text.pack
                (show (toList (canonicalCollisionEntries collision)))
    PreludeSyntaxInterfaceFailed failure ->
        preludeErrorPrefix <> renderSyntaxInterfaceError failure
    PreludeSyntaxMaterializationFailed failure ->
        preludeErrorPrefix <> renderSyntaxMaterializationError failure
    PreludeParseFailed failure ->
        preludeErrorPrefix <> Text.pack (show failure)
    PreludeFreshInputFailed failure ->
        preludeErrorPrefix <> renderFreshModuleInputError failure
    PreludeParsedModuleKeyFailed failure ->
        preludeErrorPrefix <> renderParsedModuleKeyError failure
    PreludeParseInvariantFailed failure ->
        preludeErrorPrefix <> "parse invariant failed: " <> failure

preludeErrorPrefix :: Text
preludeErrorPrefix =
    Text.pack preludeDiagnosticLabel <> ": "

renderSyntaxInterfaceError :: SyntaxInterfaceError -> Text
renderSyntaxInterfaceError = \case
    DuplicateDirectSyntaxInterface duplicate ->
        "duplicate direct syntax input " <> Text.pack (show duplicate)
    UnexpectedBaseSyntaxInterface actual expected ->
        "base syntax interface mismatch: expected "
            <> Text.pack (show expected)
            <> ", got "
            <> Text.pack (show actual)
    SyntaxInterfaceIdMismatch asserted computed ->
        "syntax interface identity mismatch: asserted "
            <> Text.pack (show asserted)
            <> ", computed "
            <> Text.pack (show computed)

renderFreshModuleInputError :: FreshModuleInputError -> Text
renderFreshModuleInputError = \case
    FreshModuleTextDoesNotMatchBytes ->
        "decoded source text does not match its source bytes"
    FreshPhysicalOwnerMismatch expected actual ->
        "physical source owner mismatch: expected "
            <> Text.pack (show expected)
            <> ", got "
            <> Text.pack (show actual)
    FreshPhysicalLocationPathMismatch expected actual ->
        "physical source location mismatch: expected "
            <> Text.pack (show expected)
            <> ", got "
            <> Text.pack (show actual)

renderParsedModuleKeyError :: Parsed.ParsedModuleKeyError -> Text
renderParsedModuleKeyError = \case
    Parsed.DuplicateParsedDirectSyntaxInput duplicate ->
        "parsed module has duplicate direct syntax input "
            <> Text.pack (show duplicate)

data ReservedParsedPrelude = ReservedParsedPrelude
    !FreshModuleInput
    !IdentifiedParsedModule

reservedParsedPreludeInput
    :: ReservedParsedPrelude
    -> FreshModuleInput
reservedParsedPreludeInput (ReservedParsedPrelude input _parsed) =
    input

reservedParsedPreludeModule
    :: ReservedParsedPrelude
    -> IdentifiedParsedModule
reservedParsedPreludeModule (ReservedParsedPrelude _input parsed) =
    parsed

-- | Parse reserved final-prelude input through the ordinary fresh-source path.
parseReservedPreludeSource
    :: ReservedPreludeSourceInput
    -> IO (Either PreludeParseError ReservedParsedPrelude)
parseReservedPreludeSource sourceInput = do
    registered <-
        registerFilePathWithDisplay
            label
            label
    case registered of
        Left err ->
            pure (Left (PreludeLocationRegistrationFailed err))
        Right fileId ->
            parseRegistered fileId
  where
    parseRegistered fileId =
        pure
            (case parseReservedFreshModule
                    (reservedPreludeSourceOwner sourceInput)
                    fileId
                    label
                    (reservedPreludeSourceBytes sourceInput)
                    (reservedPreludeSourceText sourceInput) of
                Left failure ->
                    Left (fromReservedParseError failure)
                Right (input, parsed) ->
                    Right (ReservedParsedPrelude input parsed))

    label = reservedPreludeSourceLabel sourceInput

fromReservedParseError
    :: ReservedModuleParseError
    -> PreludeParseError
fromReservedParseError = \case
    ReservedModuleSyntaxPragmaError failure ->
        PreludeSyntaxPragmaFailed failure
    ReservedModuleImportError imports ->
        PreludeImportNotSupported imports
    ReservedModuleLexicalScanError failure ->
        PreludeLexicalScanFailed failure
    ReservedModuleSyntaxDeclarationError failure ->
        PreludeSyntaxDeclarationFailed failure
    ReservedModuleLexiconCollision collision ->
        PreludeLexiconCollision collision
    ReservedModuleSyntaxInterfaceError failure ->
        PreludeSyntaxInterfaceFailed failure
    ReservedModuleSyntaxMaterializationError failure ->
        PreludeSyntaxMaterializationFailed failure
    ReservedModuleParseException failure ->
        PreludeParseFailed failure
    ReservedModuleFreshInputError failure ->
        PreludeFreshInputFailed failure
    ReservedModuleParsedKeyError failure ->
        PreludeParsedModuleKeyFailed failure
    ReservedModuleInvariantError message ->
        PreludeParseInvariantFailed message