{-# LANGUAGE BlockArguments        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE TypeApplications      #-}

module Blagda
  ( module Blagda
  , module Blagda.Template
  , module Blagda.Types
  , loadMarkdown
  , rename
  ) where

import Blagda.Agda
import Blagda.Markdown
import Blagda.Template
import Blagda.Rename (rename)
import Blagda.Types
import Blagda.Utils (pattern Strs)
import Data.List
import Data.Map.Lazy (Map)
import Data.Text (Text)
import Development.Shake
import Development.Shake.FilePath
import Text.Pandoc


--  Loads our type lookup table into memory
parseFileTypes :: () -> Action (Map Text Text)
parseFileTypes :: () -> Action (Map Text Text)
parseFileTypes () = do
  Partial => [FilePath] -> Action ()
[FilePath] -> Action ()
need [FilePath
"_build/all-pages.agda"]
  FilePath -> IO (Map Text Text) -> Action (Map Text Text)
forall a. FilePath -> IO a -> Action a
traced FilePath
"loading types from iface" (IO (Map Text Text) -> Action (Map Text Text))
-> ((FilePath -> TCMT IO (Map Text Text)) -> IO (Map Text Text))
-> (FilePath -> TCMT IO (Map Text Text))
-> Action (Map Text Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> TCMT IO (Map Text Text)) -> IO (Map Text Text)
forall a. (FilePath -> TCMT IO a) -> IO a
runAgda ((FilePath -> TCMT IO (Map Text Text)) -> Action (Map Text Text))
-> (FilePath -> TCMT IO (Map Text Text)) -> Action (Map Text Text)
forall a b. (a -> b) -> a -> b
$
    FilePath -> FilePath -> TCMT IO (Map Text Text)
tcAndLoadPublicNames FilePath
"_build/all-pages.agda"


agdaHTML :: FilePath -> Action [FilePath]
agdaHTML :: FilePath -> Action [FilePath]
agdaHTML FilePath
dir = do
  [FilePath]
agda_files <- [FilePath] -> [FilePath]
forall a. Ord a => [a] -> [a]
sort ([FilePath] -> [FilePath])
-> Action [FilePath] -> Action [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> [FilePath] -> Action [FilePath]
getDirectoryFiles FilePath
dir [FilePath
"**/*.agda", FilePath
"**/*.lagda.md"]

  let
    toOut :: FilePath -> FilePath
toOut FilePath
x | FilePath -> FilePath
takeExtensions FilePath
x FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
".lagda.md"
            = FilePath -> FilePath
moduleName (FilePath -> FilePath
dropExtensions FilePath
x) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" -- (text page)"
    toOut FilePath
x = FilePath -> FilePath
moduleName (FilePath -> FilePath
dropExtensions FilePath
x) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" -- (code only)"

  -- build the index
  FilePath -> [FilePath] -> Action ()
forall (m :: * -> *).
(MonadIO m, Partial) =>
FilePath -> [FilePath] -> m ()
writeFileLines FilePath
"_build/all-pages.agda"
    ([FilePath] -> Action ()) -> [FilePath] -> Action ()
forall a b. (a -> b) -> a -> b
$ [FilePath
"open import " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
toOut FilePath
x | FilePath
x <- [FilePath]
agda_files]
     [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath
"import " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
x FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" -- (builtin)" | FilePath
x <- [FilePath]
builtinModules]

  -- get agda html
  -- cacheAction @String @() "agda" $

  [CmdOption] -> FilePath -> [FilePath] -> Action ()
forall r.
(Partial, CmdResult r) =>
[CmdOption] -> FilePath -> [FilePath] -> Action r
command @() [] FilePath
"agda"
    [ FilePath
"--html"
    , FilePath
"--html-dir=_build/html0"
    , FilePath
"--html-highlight=auto"
    , FilePath
"--local-interfaces"
    , FilePath
"--css=/css/agda-cats.css"
    , FilePath
"_build/all-pages.agda"
    ]

  [FilePath] -> Action [FilePath]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [FilePath]
agda_files


parseMetaString :: MetaValue -> Maybe Text
parseMetaString :: MetaValue -> Maybe Text
parseMetaString (MetaString Text
txt) = Text -> Maybe Text
forall a. a -> Maybe a
Just Text
txt
parseMetaString (MetaInlines (Strs Text
txt)) = Text -> Maybe Text
forall a. a -> Maybe a
Just Text
txt
parseMetaString MetaValue
_ = Maybe Text
forall a. Maybe a
Nothing