agda2lagda-0.2023.1.12: src/Main.hs

-- | agda2lagda
--
-- Translate line comments into ordinary text,
-- block comments into (LaTeX) comments,
-- and wrap regular Agda code into code delimiters (\begin{code}...\end{code}).

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RecordWildCards #-}

module Main where

import Control.Monad

import System.Directory (doesFileExist, createDirectoryIfMissing)
import System.FilePath  (takeDirectory)
import System.IO        (hPutStr, stderr)
import System.Exit      (exitFailure)

import LexicalStructure
import Options
import Render

main :: IO ()
main = do

  -- Parse options.

  opts@Options{..} <- options
  target@(language, format, mout) <- getTarget opts
  chat opts $ vocalizeOptions opts target

  -- Parse input.

  chat opts $ "Reading input...\n"
  items <- parseItems [] <$> maybe getContents readFile optInput

  -- Generate output.

  let result = case format of
        LaTeX    -> lagdaTex items
        Markdown -> lagdaMd language items

  -- Save to file or print to stdout.

  chat opts $ "Writing output...\n"
  case mout of
    Nothing      -> putStr result
    Just outFile -> do

      -- Do not overwrite existing file unless forced.
      unless optForce $ do
        ex <- doesFileExist outFile
        when ex $ do
          hPutStr stderr $ unlines
            [ unwords [ "Error: output file", outFile, "already exists." ]
            , "Use option --force to allow to overwrite existing files."
            , "Aborting."
            ]
          exitFailure

      createDirectoryIfMissing True $ takeDirectory outFile
      writeFile outFile result

  -- Done.

  chat opts $ unwords [ self, "terminated successfully.\n" ]

chat :: Options -> String -> IO ()
chat o msg = when (optVerbose o) $ hPutStr stderr msg

-- UNUSED:
-- -- | Checks where first file has been more recently modified than second file.
-- --   If first file does not exist, return 'False'
-- --   (its modification time is then taken to be minus infinity).
-- --
-- --   Precondition: second file exists.
-- newerThan :: FilePath -> FilePath -> IO Bool
-- newerThan f1 f2 = do
--   t2 <- getModificationTime f2
--   ((> t2) <$> getModificationTime t1)
--     `catch` \ e
--        | isPermissionError e || isDoesNotExistError e -> return False
--        | otherwise -> throw e