-- | Basic data types for library management.

module Agda.Interaction.Library.Base where

import Agda.Utils.Lens

-- | A symbolic library name.
--
type LibName = String

-- | The special name @\".\"@ is used to indicated that the current directory
--   should count as a project root.
--
libNameForCurrentDir :: LibName
libNameForCurrentDir :: LibName
libNameForCurrentDir = LibName
"."

-- | Content of a @.agda-lib@ file.
--
data AgdaLibFile = AgdaLibFile
  { AgdaLibFile -> LibName
_libName     :: LibName     -- ^ The symbolic name of the library.
  , AgdaLibFile -> LibName
_libFile     :: FilePath    -- ^ Path to this @.agda-lib@ file (not content of the file).
  , AgdaLibFile -> [LibName]
_libIncludes :: [FilePath]  -- ^ Roots where to look for the modules of the library.
  , AgdaLibFile -> [LibName]
_libDepends  :: [LibName]   -- ^ Dependencies.
  }
  deriving (Int -> AgdaLibFile -> ShowS
[AgdaLibFile] -> ShowS
AgdaLibFile -> LibName
(Int -> AgdaLibFile -> ShowS)
-> (AgdaLibFile -> LibName)
-> ([AgdaLibFile] -> ShowS)
-> Show AgdaLibFile
forall a.
(Int -> a -> ShowS) -> (a -> LibName) -> ([a] -> ShowS) -> Show a
showList :: [AgdaLibFile] -> ShowS
$cshowList :: [AgdaLibFile] -> ShowS
show :: AgdaLibFile -> LibName
$cshow :: AgdaLibFile -> LibName
showsPrec :: Int -> AgdaLibFile -> ShowS
$cshowsPrec :: Int -> AgdaLibFile -> ShowS
Show)

emptyLibFile :: AgdaLibFile
emptyLibFile :: AgdaLibFile
emptyLibFile = AgdaLibFile :: LibName -> LibName -> [LibName] -> [LibName] -> AgdaLibFile
AgdaLibFile
  { _libName :: LibName
_libName     = LibName
""
  , _libFile :: LibName
_libFile     = LibName
""
  , _libIncludes :: [LibName]
_libIncludes = []
  , _libDepends :: [LibName]
_libDepends  = []
  }

-- | Lenses for AgdaLibFile

libName :: Lens' LibName AgdaLibFile
libName :: (LibName -> f LibName) -> AgdaLibFile -> f AgdaLibFile
libName LibName -> f LibName
f AgdaLibFile
a = LibName -> f LibName
f (AgdaLibFile -> LibName
_libName AgdaLibFile
a) f LibName -> (LibName -> AgdaLibFile) -> f AgdaLibFile
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ LibName
x -> AgdaLibFile
a { _libName :: LibName
_libName = LibName
x }

libFile :: Lens' FilePath AgdaLibFile
libFile :: (LibName -> f LibName) -> AgdaLibFile -> f AgdaLibFile
libFile LibName -> f LibName
f AgdaLibFile
a = LibName -> f LibName
f (AgdaLibFile -> LibName
_libFile AgdaLibFile
a) f LibName -> (LibName -> AgdaLibFile) -> f AgdaLibFile
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ LibName
x -> AgdaLibFile
a { _libFile :: LibName
_libFile = LibName
x }

libIncludes :: Lens' [FilePath] AgdaLibFile
libIncludes :: ([LibName] -> f [LibName]) -> AgdaLibFile -> f AgdaLibFile
libIncludes [LibName] -> f [LibName]
f AgdaLibFile
a = [LibName] -> f [LibName]
f (AgdaLibFile -> [LibName]
_libIncludes AgdaLibFile
a) f [LibName] -> ([LibName] -> AgdaLibFile) -> f AgdaLibFile
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ [LibName]
x -> AgdaLibFile
a { _libIncludes :: [LibName]
_libIncludes = [LibName]
x }

libDepends :: Lens' [LibName] AgdaLibFile
libDepends :: ([LibName] -> f [LibName]) -> AgdaLibFile -> f AgdaLibFile
libDepends [LibName] -> f [LibName]
f AgdaLibFile
a = [LibName] -> f [LibName]
f (AgdaLibFile -> [LibName]
_libDepends AgdaLibFile
a) f [LibName] -> ([LibName] -> AgdaLibFile) -> f AgdaLibFile
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ [LibName]
x -> AgdaLibFile
a { _libDepends :: [LibName]
_libDepends = [LibName]
x }