content: module Agda2Hs.Render where
  
  import Control.Monad ( unless )
  import Control.Monad.IO.Class ( MonadIO(liftIO) )
  
  import Data.Function ( on )
  import Data.List ( sortBy, nub )
  import Data.Maybe ( fromMaybe, isNothing )
  import Data.Set ( Set )
  import qualified Data.Set as Set
  
  import System.FilePath ( takeDirectory )
  import System.Directory ( createDirectoryIfMissing )
  
  import Agda.Compiler.Backend
  
  import Agda.TypeChecking.Pretty
  import qualified Agda.Syntax.Concrete.Name as C
  import Agda.Syntax.Position
  import Agda.Syntax.TopLevelModuleName
  import Agda.Syntax.Common.Pretty ( prettyShow )
  
  import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
  
  import Agda2Hs.Compile
  import Agda2Hs.Compile.Types
  import Agda2Hs.Compile.Imports
  import Agda2Hs.Compile.Utils ( primModules, moduleFileName )
  import qualified Agda2Hs.Language.Haskell as Hs
  import Agda2Hs.Language.Haskell.Utils
    ( extToName, pp, moveToTop, insertParens )
  import Agda2Hs.Pragma ( getForeignPragmas )
  
  -- Rendering --------------------------------------------------------------
  
  type Block = Ranged [String]
  
  sortRanges :: [Ranged a] -> [a]
  sortRanges = map snd . sortBy (compare `on` rLine . fst)
  
  rLine :: Range -> Int
  rLine r = fromIntegral $ fromMaybe 0 $ posLine <$> rStart r
  
  renderBlocks :: [Block] -> String
  renderBlocks = unlines . map unlines . sortRanges . filter (not . null . snd)
  
  defBlock :: [Ranged [Hs.Decl ()]] -> [Block]
  defBlock def = [ (r, map (pp . insertParens) ds) | (r, ds) <- def ]
  
  renderLangExts :: [Hs.KnownExtension] -> String
  renderLangExts exts
    | null exts = ""
    | otherwise = pp (Hs.LanguagePragma () $ nub $ map extToName exts) ++ "\n"
  
  codePragmas :: [Ranged Code] -> [Block]
  codePragmas code = [ (r, map pp ps) | (r, (Hs.Module _ _ ps _ _, _)) <- code ]
  
  codeBlocks :: [Ranged Code] -> [Block]
  codeBlocks code = [(r, [uncurry Hs.exactPrint $ moveToTop $ noPragmas mcs]) | (r, mcs) <- code, nonempty mcs]
    where noPragmas (Hs.Module l h _ is ds, cs) = (Hs.Module l h [] is ds, cs)
          noPragmas m                           = m
          nonempty (Hs.Module _ _ _ is ds, cs) = not $ null is && null ds && null cs
          nonempty _                           = True
  
  -- Generating the files -------------------------------------------------------
  
  ensureDirectory :: FilePath -> IO ()
  ensureDirectory = createDirectoryIfMissing True . takeDirectory
  
  -- | Compile the full import list,
  -- with special handling for the @Prelude@ as prescribed by 'Options'.
  compileImportsWithPrelude
    :: Options -> String -> Imports -> TCM [Hs.ImportDecl ()]
  compileImportsWithPrelude opts mod imps = do
      -- if the prelude is supposed to be implicit,
      -- or the prelude imports have been fixed in the config file,
      -- we remove it from the list of imports
      let filteredImps =
            if not preludeImplicit && isNothing preludeImports
              then imps
              else filter ((/= Hs.prelude_mod ()) . importModule) imps
  
      -- then we try to add it back
      if (not preludeImplicit && isNothing preludeImports) || null preludeHiding
        then compileImports mod filteredImps
        else (preludeImportDecl preOpts:) <$> compileImports mod filteredImps
    where
      preOpts@PreludeOpts{..} = optPrelude opts
  
  -- | Render the @.hs@ module as a 'String' and write it to a file.
  writeModule :: GlobalEnv -> ModuleEnv -> IsMain -> TopLevelModuleName
              -> [(CompiledDef, CompileOutput)] -> TCM ModuleRes
  writeModule genv _ isMain m outs = do
    let opts = globalOptions genv
    code <- getForeignPragmas (optExtensions opts)
    let mod  = prettyShow m
        (cdefs, impss, extss) = unzip3 $ flip map outs $
          \(cdef, CompileOutput imps exts) -> (cdef, imps, exts)
        defs = concatMap defBlock cdefs ++ codeBlocks code
        imps = concat impss
        exts = concat extss
    unless (null code && null defs && isMain == NotMain) $ do
  
      let unlines' [] = []
          unlines' ss = unlines ss ++ "\n"
  
      autoImports <- unlines' . map Hs.prettyShowImportDecl
        <$> compileImportsWithPrelude opts mod imps
  
      -- The comments make it hard to generate and pretty print a full module
      hsFile <- moduleFileName opts m
  
      let output = concat
            [ renderLangExts exts
            , renderBlocks $ codePragmas code
            , "module " ++ mod ++ " where\n\n"
            , autoImports
            , renderBlocks defs
            ]
  
      reportSLn "" 1 $ "Writing " ++ hsFile
  
      liftIO $ ensureDirectory hsFile >> writeFile hsFile output
  