{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE MultiWayIf #-}

import Control.Applicative
import Control.Monad
import Control.Monad.Except

import qualified Data.List as List
import qualified Data.List.NonEmpty as List1
import Data.List.NonEmpty ( pattern (:|) )
import Data.Maybe

import System.Directory
import System.Environment
import System.Exit
import System.FilePath
import System.FilePath.Find
import System.IO

headerFile     = "Header"
allOutputFile  = "Everything"
safeOutputFile = "EverythingSafe"
srcDir         = "src"

---------------------------------------------------------------------------
-- Files with a special status

-- | Checks whether a module is declared (un)safe

unsafeModules :: [FilePath]
unsafeModules = map modToFile
  [ "Codata.Musical.Colist"
  , "Codata.Musical.Colist.Base"
  , "Codata.Musical.Colist.Properties"
  , "Codata.Musical.Colist.Bisimilarity"
  , "Codata.Musical.Colist.Relation.Unary.All"
  , "Codata.Musical.Colist.Relation.Unary.All.Properties"
  , "Codata.Musical.Colist.Relation.Unary.Any"
  , "Codata.Musical.Colist.Relation.Unary.Any.Properties"
  , "Codata.Musical.Colist.Infinite-merge"
  , "Codata.Musical.Costring"
  , "Codata.Musical.Covec"
  , "Codata.Musical.Conversion"
  , "Codata.Musical.Stream"
  , "Data.Bytestring.Base"
  , "Data.Bytestring.Builder.Base"
  , "Data.Bytestring.Builder.Primitive"
  , "Data.Bytestring.IO"
  , "Data.Bytestring.IO.Primitive"
  , "Data.Bytestring.Primitive"
  , "Data.Word8.Base"
  , "Data.Word8.Literals"
  , "Data.Word8.Primitive"
  , "Data.Word64.Primitive"
  , "Data.Word8.Show"
  , "Data.Word64.Show"
  , "Debug.Trace"
  , "Effect.Monad.IO"
  , "Effect.Monad.IO.Instances"
  , "Foreign.Haskell"
  , "Foreign.Haskell.Coerce"
  , "Foreign.Haskell.Either"
  , "Foreign.Haskell.Maybe"
  , "Foreign.Haskell.List.NonEmpty"
  , "Foreign.Haskell.Pair"
  , "IO"
  , "IO.Base"
  , "IO.Categorical"
  , "IO.Handle"
  , "IO.Infinite"
  , "IO.Instances"
  , "IO.Effectful"
  , "IO.Finite"
  , "IO.Primitive"
  , "IO.Primitive.Core"
  , "IO.Primitive.Handle"
  , "IO.Primitive.Infinite"
  , "IO.Primitive.Finite"
  , "Relation.Binary.PropositionalEquality.TrustMe"
  , "System.Clock"
  , "System.Clock.Primitive"
  , "System.Directory"
  , "System.Directory.Primitive"
  , "System.Environment"
  , "System.Environment.Primitive"
  , "System.Exit"
  , "System.Exit.Primitive"
  , "System.FilePath.Posix"
  , "System.FilePath.Posix.Primitive"
  , "System.Process"
  , "System.Process.Primitive"
  , "System.Random"
  , "System.Random.Primitive"
  , "Test.Golden"
  , "Text.Pretty.Core"
  , "Text.Pretty"
  ] ++ sizedTypesModules

isUnsafeModule :: FilePath -> Bool
isUnsafeModule fp =
    unqualifiedModuleName fp == "Unsafe"
    || fp `elem` unsafeModules

-- | Checks whether a module is declared as using K

withKModules :: [FilePath]
withKModules = map modToFile
  [ "Axiom.Extensionality.Heterogeneous"
  , "Data.Star.BoundedVec"
  , "Data.Star.Decoration"
  , "Data.Star.Environment"
  , "Data.Star.Fin"
  , "Data.Star.Pointer"
  , "Data.Star.Vec"
  , "Data.String.Unsafe"
  , "Reflection.AnnotatedAST"
  , "Reflection.AnnotatedAST.Free"
  , "Relation.Binary.HeterogeneousEquality"
  , "Relation.Binary.HeterogeneousEquality.Core"
  , "Relation.Binary.HeterogeneousEquality.Quotients.Examples"
  , "Relation.Binary.HeterogeneousEquality.Quotients"
  , "Relation.Binary.PropositionalEquality.TrustMe"
  , "Text.Pretty.Core"
  , "Text.Pretty"
  , "Text.Regex.String.Unsafe"
  ]

isWithKModule :: FilePath -> Bool
isWithKModule =
  -- GA 2019-02-24: it is crucial to use an anonymous lambda
  -- here so that `withKModules` is shared between all calls
  -- to `isWithKModule`.
  \ fp -> unqualifiedModuleName fp == "WithK"
       || fp `elem` withKModules

sizedTypesModules :: [FilePath]
sizedTypesModules = map modToFile
  [ "Codata.Sized.Cofin"
  , "Codata.Sized.Cofin.Literals"
  , "Codata.Sized.Colist"
  , "Codata.Sized.Colist.Bisimilarity"
  , "Codata.Sized.Colist.Categorical"
  , "Codata.Sized.Colist.Effectful"
  , "Codata.Sized.Colist.Properties"
  , "Codata.Sized.Conat"
  , "Codata.Sized.Conat.Bisimilarity"
  , "Codata.Sized.Conat.Literals"
  , "Codata.Sized.Conat.Properties"
  , "Codata.Sized.Covec"
  , "Codata.Sized.Covec.Bisimilarity"
  , "Codata.Sized.Covec.Categorical"
  , "Codata.Sized.Covec.Effectful"
  , "Codata.Sized.Covec.Instances"
  , "Codata.Sized.Covec.Properties"
  , "Codata.Sized.Cowriter"
  , "Codata.Sized.Cowriter.Bisimilarity"
  , "Codata.Sized.Delay"
  , "Codata.Sized.Delay.Bisimilarity"
  , "Codata.Sized.Delay.Categorical"
  , "Codata.Sized.Delay.Effectful"
  , "Codata.Sized.Delay.Properties"
  , "Codata.Sized.M"
  , "Codata.Sized.M.Bisimilarity"
  , "Codata.Sized.M.Properties"
  , "Codata.Sized.Stream"
  , "Codata.Sized.Stream.Bisimilarity"
  , "Codata.Sized.Stream.Categorical"
  , "Codata.Sized.Stream.Effectful"
  , "Codata.Sized.Stream.Instances"
  , "Codata.Sized.Stream.Properties"
  , "Codata.Sized.Thunk"
  , "Data.Container.Fixpoints.Sized"
  , "Data.W.Sized"
  , "Data.Nat.PseudoRandom.LCG.Unsafe"
  , "Data.Tree.Binary.Show"
  , "Data.Tree.Rose"
  , "Data.Tree.Rose.Properties"
  , "Data.Tree.Rose.Show"
  , "Data.Trie"
  , "Data.Trie.NonEmpty"
  , "Relation.Unary.Sized"
  , "Size"
  , "Text.Tree.Linear"
  ]

isSizedTypesModule :: FilePath -> Bool
isSizedTypesModule =
  \ fp -> fp `elem` sizedTypesModules

unqualifiedModuleName :: FilePath -> String
unqualifiedModuleName = dropExtension . takeFileName

-- | Returns 'True' for all Agda files except for core modules.

isLibraryModule :: FilePath -> Bool
isLibraryModule f =
  takeExtension f `elem` [".agda", ".lagda"]
  && unqualifiedModuleName f /= "Core"

---------------------------------------------------------------------------
-- Analysing library files

type Exc = Except String

-- | Extracting the header.

-- It needs to have the form:
-- ------------------------------------------------------------------------
-- -- The Agda standard library
-- --
-- -- Description of the module
-- ------------------------------------------------------------------------

extractHeader :: FilePath -> [String] -> Exc [String]
extractHeader mod = extract
  where
  delimiter = all (== '-')

  extract :: [String] -> Exc [String]
  extract (d1 : "-- The Agda standard library" : "--" : ss)
    | delimiter d1
    , (info, d2 : rest) <- span ("-- " `List.isPrefixOf`) ss
    , delimiter d2
    = pure $ info
  extract (d1@(c:cs) : _)
    | not (delimiter d1)
      -- Andreas, issue #1510: there is a haunting of Prelude.last, so use List1.last instead.
      -- See https://gitlab.haskell.org/ghc/ghc/-/issues/19917.
      -- Update: The haunting is also resolved by 'throwError' instead of 'error',
      -- but still I dislike Prelude.last.
    , List1.last (c :| cs) == '\r'
    = throwError $ unwords
      [ mod
      , "contains \\r, probably due to git misconfiguration;"
      , "maybe set autocrf to input?"
      ]
  extract _ = throwError $ unwords
      [ mod
      , "is malformed."
      , "It needs to have a module header."
      , "Please see other existing files or consult HACKING.md."
      ]

-- | A crude classifier looking for lines containing options

data Safety = Unsafe | Safe deriving (Eq)
data Status = Deprecated | Active deriving (Eq)

classify :: FilePath -> [String] -> [String] -> Exc (Safety, Status)
classify fp hd ls
  -- We start with sanity checks
  | isUnsafe && safe          = throwError $ fp ++ contradiction "unsafe" "safe"
  | not (isUnsafe || safe)    = throwError $ fp ++ uncategorized "unsafe" "safe"
  | isWithK && cubicalC       = throwError $ fp ++ contradiction "as relying on K" "cubical-compatible"
  | isWithK && not withK      = throwError $ fp ++ missingWithK
  | not (isWithK || cubicalC) = throwError $ fp ++ uncategorized "as relying on K" "cubical-compatible"
  -- And then perform the actual classification
  | otherwise = do
      let safety = if | safe -> Safe
                      | isUnsafe -> Unsafe
                      | otherwise -> error "IMPOSSIBLE"
      let status = if deprecated then Deprecated else Active
      pure (safety, status)

  where

    -- based on declarations
    isWithK  = isWithKModule fp
    isUnsafe = isUnsafeModule fp

    -- based on detected OPTIONS
    safe        = option "--safe"
    withK       = option "--with-K"
    cubicalC    = option "--cubical-compatible"

    -- based on detected comment in header
    deprecated  = let detect = List.isSubsequenceOf "This module is DEPRECATED."
                  in any detect hd

    -- GA 2019-02-24: note that we do not reprocess the whole module for every
    -- option check: the shared @options@ definition ensures we only inspect a
    -- handful of lines (at most one, ideally)
    option str = let detect = List.isSubsequenceOf ["{-#", "OPTIONS", str, "#-}"]
                  in any detect options
    options    = words <$> filter (List.isInfixOf "OPTIONS") ls

    -- formatting error messages
    contradiction d o = unwords
      [ " is declared", d, "but uses the", "--" ++ o, "option." ]
    uncategorized d o = unwords
      [ " is not declared", d, "but not using the", "--" ++ o, "option either." ]

    missingWithK = " is declared as relying on K but not using the --with-K option."

-- | Analyse a file: extracting header and classifying it.

data LibraryFile = LibraryFile
  { filepath   :: FilePath -- ^ FilePath of the source file
  , header     :: [String] -- ^ All lines in the headers are already prefixed with \"-- \".
  , safety     :: Safety
  , status     :: Status   -- ^ Deprecation status options used by the module
  }

analyse :: FilePath -> IO LibraryFile
analyse fp = do
  ls <- lines <$> readFileUTF8 fp
  hd <- runExc $ extractHeader fp ls
  (sf, st) <- runExc $ classify fp hd ls
  return $ LibraryFile
    { filepath = fp
    , header   = hd
    , safety   = sf
    , status   = st
    }

checkFilePaths :: String -> [FilePath] -> IO ()
checkFilePaths cat fps = forM_ fps $ \ fp -> do
  b <- doesFileExist fp
  unless b $
    die $ fp ++ " is listed as " ++ cat ++ " but does not exist."

data Options = Options
  { includeDeprecated :: Bool
  , outputDirectory :: FilePath
  }

initOptions :: Options
initOptions = Options
  { includeDeprecated = False
  , outputDirectory = "."
  }

parseOptions :: [String] -> Options -> Maybe Options
parseOptions [] opts = pure opts
parseOptions ("--include-deprecated" : rest) opts
  = parseOptions rest (opts { includeDeprecated = True })
parseOptions ("--out-dir" : dir : rest) opts
  = parseOptions rest (opts { outputDirectory = dir })
parseOptions _ _ = Nothing

---------------------------------------------------------------------------
-- Collecting all non-Core library files, analysing them and generating
-- 2 files:
-- Everything.agda                 all the modules
-- EverythingSafe.agda             all the safe modules

main :: IO ()
main = do
  args <- getArgs
  Options{..} <- case parseOptions args initOptions of
    Just opts -> pure opts
    Nothing -> hPutStr stderr usage >> exitFailure

  checkFilePaths "unsafe" unsafeModules
  checkFilePaths "using K" withKModules

  header  <- readFileUTF8 headerFile
  modules <- filter isLibraryModule . List.sort <$>
               find always
                    (extension ==? ".agda" ||? extension ==? ".lagda")
                    srcDir
  libraryfiles <- (if includeDeprecated then id
    else (filter ((Deprecated /=) . status) <$>)) (mapM analyse modules)

  let mkModule str = "module " ++ str ++ " where"

  writeFileUTF8 (outputDirectory ++ "/" ++ allOutputFile ++ ".agda") $
    unlines [ header
            , "{-# OPTIONS --rewriting --guardedness --sized-types #-}\n"
            , mkModule allOutputFile
            , format libraryfiles
            ]

  writeFileUTF8 (outputDirectory ++ "/" ++ safeOutputFile ++ ".agda") $
    unlines [ header
            , "{-# OPTIONS --safe --guardedness #-}\n"
            , mkModule safeOutputFile
            , format $ filter ((Unsafe /=) . safety) libraryfiles
            ]

-- | Usage info.

usage :: String
usage = unlines
  [ "GenerateEverything: A utility program for Agda's standard library."
  , ""
  , "Usage: GenerateEverything"
  , ""
  , "This program should be run in the base directory of a clean checkout of"
  , "the library."
  , ""
  , "The program generates documentation for the library by extracting"
  , "headers from library modules. The output is written to " ++ allOutputFile
  , "with the file " ++ headerFile ++ " inserted verbatim at the beginning."
  , ""
  , "If the option --out-dir is used then the output is placed in the"
  , "subdirectory thus selected."
  ]


-- | Formats the extracted module information.

format :: [LibraryFile] -> String
format = unlines . concatMap fmt
  where
  fmt lf = "" : header lf ++ ["import " ++ fileToMod (filepath lf)]

-- | Translates back and forth between a file name and the corresponding module
--   name. We assume that the file name corresponds to an Agda module under
--   'srcDir'.

fileToMod :: FilePath -> String
fileToMod = map slashToDot . dropExtension . makeRelative srcDir
  where
  slashToDot c | isPathSeparator c = '.'
               | otherwise         = c

modToFile :: String -> FilePath
modToFile name = concat [ srcDir, [pathSeparator], map dotToSlash name, ".agda" ]
  where
  dotToSlash c | c == '.'  = pathSeparator
               | otherwise = c

-- | A variant of 'readFile' which uses the 'utf8' encoding.

readFileUTF8 :: FilePath -> IO String
readFileUTF8 f = do
  h <- openFile f ReadMode
  hSetEncoding h utf8
  s <- hGetContents h
  length s `seq` return s

-- | A variant of 'writeFile' which uses the 'utf8' encoding.

writeFileUTF8 :: FilePath -> String -> IO ()
writeFileUTF8 f s = withFile f WriteMode $ \h -> do
  hSetEncoding h utf8
  hPutStr h s

-- | Turning exceptions into fatal errors.

runExc :: Exc a -> IO a
runExc = either die return . runExcept