{- |
Module: Agda.Unused.Types.Root

Data types representing public entry points for an Agda project.
-}
module Agda.Unused.Types.Root

  ( -- * Types

    Root(..)
  , Roots(..)

    -- * Construction

  , fromList

  ) where

import Agda.Unused.Types.Name
  (QName)

import Data.Either
  (lefts, rights)

-- | A public entry point for an Agda project.
data Root
  = Root
  { Root -> QName
rootFile
    :: QName
    -- ^ A module name.
  , Root -> Maybe [QName]
rootNames
    :: Maybe [QName]
    -- ^ Identifier names. An value of 'Nothing' represents all names in scope.
  } deriving Int -> Root -> ShowS
[Root] -> ShowS
Root -> String
(Int -> Root -> ShowS)
-> (Root -> String) -> ([Root] -> ShowS) -> Show Root
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Root] -> ShowS
$cshowList :: [Root] -> ShowS
show :: Root -> String
$cshow :: Root -> String
showsPrec :: Int -> Root -> ShowS
$cshowsPrec :: Int -> Root -> ShowS
Show

-- | A collection of public entry points for an Agda project.
data Roots
  = Roots
  { Roots -> [Root]
rootsCheck
    :: [Root]
    -- ^ Modules to check.
  , Roots -> [QName]
rootsIgnore
    :: [QName]
    -- ^ Modules to ignore.
  } deriving Int -> Roots -> ShowS
[Roots] -> ShowS
Roots -> String
(Int -> Roots -> ShowS)
-> (Roots -> String) -> ([Roots] -> ShowS) -> Show Roots
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Roots] -> ShowS
$cshowList :: [Roots] -> ShowS
show :: Roots -> String
$cshow :: Roots -> String
showsPrec :: Int -> Roots -> ShowS
$cshowsPrec :: Int -> Roots -> ShowS
Show

-- | Construct a collection of roots from a list of elements.
fromList
  :: [Either QName Root]
  -> Roots
fromList :: [Either QName Root] -> Roots
fromList rs :: [Either QName Root]
rs
  = [Root] -> [QName] -> Roots
Roots ([Either QName Root] -> [Root]
forall a b. [Either a b] -> [b]
rights [Either QName Root]
rs) ([Either QName Root] -> [QName]
forall a b. [Either a b] -> [a]
lefts [Either QName Root]
rs)