-- | The list of data files Agda uses.
--
-- Because of TemplateHaskell state restrictions, this cannot be define in ''Agda.Setup''.

module Agda.Setup.DataFiles where

-- | A data file path relative to the project root.

dataPath :: FilePath -> FilePath
dataPath :: [Char] -> [Char]
dataPath = ([Char]
"src/data/" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++)
-- Do we need to bother with </> for Windows?
-- dataPath f = "src" </> "data" </> f

-- | Agda's embedded data files.

-- KEEP IN SYNC with the list in Agda.cabal under extra-source-files!
dataFiles :: [FilePath]
dataFiles :: [[Char]]
dataFiles =
  ([Char] -> [Char]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
emacsModeDir [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"/") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) [[Char]]
emacsLispFiles [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++
  -- N.B.: agda2-mode-pkg.el is not part of emacsLispFiles as it need not be compiled.
  [ [Char]
"emacs-mode/agda2-mode-pkg.el"
  , [Char]
"html/Agda.css"
  , [Char]
"html/highlight-hover.js"
  , [Char]
"JS/agda-rts.mjs"
  , [Char]
"JS/agda-rts.js"
  , [Char]
"JS/agda-rts.amd.js"
  , [Char]
"latex/agda.sty"
  , [Char]
"latex/postprocess-latex.pl"
  , [Char]
"lib/prim/agda-builtins.agda-lib"
  , [Char]
"lib/prim/Agda/Builtin/Bool.agda"
  , [Char]
"lib/prim/Agda/Builtin/Char.agda"
  , [Char]
"lib/prim/Agda/Builtin/Char/Properties.agda"
  , [Char]
"lib/prim/Agda/Builtin/Coinduction.agda"
  , [Char]
"lib/prim/Agda/Builtin/Cubical/Path.agda"
  , [Char]
"lib/prim/Agda/Builtin/Cubical/Sub.agda"
  , [Char]
"lib/prim/Agda/Builtin/Cubical/Glue.agda"
  , [Char]
"lib/prim/Agda/Builtin/Cubical/Equiv.agda"
  , [Char]
"lib/prim/Agda/Builtin/Cubical/HCompU.agda"
  , [Char]
"lib/prim/Agda/Builtin/Equality.agda"
  , [Char]
"lib/prim/Agda/Builtin/Equality/Erase.agda"
  , [Char]
"lib/prim/Agda/Builtin/Equality/Rewrite.agda"
  , [Char]
"lib/prim/Agda/Builtin/Float.agda"
  , [Char]
"lib/prim/Agda/Builtin/Float/Properties.agda"
  , [Char]
"lib/prim/Agda/Builtin/FromNat.agda"
  , [Char]
"lib/prim/Agda/Builtin/FromNeg.agda"
  , [Char]
"lib/prim/Agda/Builtin/FromString.agda"
  , [Char]
"lib/prim/Agda/Builtin/IO.agda"
  , [Char]
"lib/prim/Agda/Builtin/Int.agda"
  , [Char]
"lib/prim/Agda/Builtin/List.agda"
  , [Char]
"lib/prim/Agda/Builtin/Maybe.agda"
  , [Char]
"lib/prim/Agda/Builtin/Nat.agda"
  , [Char]
"lib/prim/Agda/Builtin/Reflection.agda"
  , [Char]
"lib/prim/Agda/Builtin/Reflection/External.agda"
  , [Char]
"lib/prim/Agda/Builtin/Reflection/Properties.agda"
  , [Char]
"lib/prim/Agda/Builtin/Sigma.agda"
  , [Char]
"lib/prim/Agda/Builtin/Size.agda"
  , [Char]
"lib/prim/Agda/Builtin/Strict.agda"
  , [Char]
"lib/prim/Agda/Builtin/String.agda"
  , [Char]
"lib/prim/Agda/Builtin/String/Properties.agda"
  , [Char]
"lib/prim/Agda/Builtin/TrustMe.agda"
  , [Char]
"lib/prim/Agda/Builtin/Unit.agda"
  , [Char]
"lib/prim/Agda/Builtin/Word.agda"
  , [Char]
"lib/prim/Agda/Builtin/Word/Properties.agda"
  , [Char]
"lib/prim/Agda/Primitive.agda"
  , [Char]
"lib/prim/Agda/Primitive/Cubical.agda"
  , [Char]
"MAlonzo/src/MAlonzo/RTE.hs"
  , [Char]
"MAlonzo/src/MAlonzo/RTE/Float.hs"
  ]

-- | The subdirectory in the Agda data directory containing the emacs mode.

emacsModeDir :: FilePath
emacsModeDir :: [Char]
emacsModeDir = [Char]
"emacs-mode"

-- | The Agda mode's Emacs Lisp files, given in the order in which
-- they should be compiled.

emacsLispFiles :: [FilePath]
emacsLispFiles :: [[Char]]
emacsLispFiles =
  [ [Char]
"agda2-abbrevs.el"
  , [Char]
"annotation.el"
  , [Char]
"agda2-queue.el"
  , [Char]
"eri.el"
  , [Char]
"agda2.el"
  , [Char]
"agda-input.el"
  , [Char]
"agda2-highlight.el"
  , [Char]
"agda2-mode.el"
  ]
  -- N.B.: We also ship agda2-mode-pkg.el for melpa,
  -- but this is not part of the emacs mode and need not be compiled.