1-- | Basic data types for library management.
2
3module Agda.Interaction.Library.Base where
4
5import Control.Arrow ( first , second )
6import Control.DeepSeq
7import Control.Monad.Except
8import Control.Monad.State
9import Control.Monad.Writer
10
11import Data.Char ( isDigit )
12import Data.Data ( Data )
13import qualified Data.List as List
14import Data.Map (Map)
15import qualified Data.Map as Map
16import Data.Text ( Text )
17
18import GHC.Generics (Generic)
19
20import System.Directory
21import System.FilePath
22
23import Agda.Interaction.Options.Warnings
24
25import Agda.Utils.FileName
26import Agda.Utils.Lens
27import Agda.Utils.Pretty
28
29-- | A symbolic library name.
30--
31type LibName = String
32
33data LibrariesFile = LibrariesFile
34  { lfPath   :: FilePath
35      -- ^ E.g. @~/.agda/libraries@.
36  , lfExists :: Bool
37       -- ^ The libraries file might not exist,
38       --   but we may print its assumed location in error messages.
39  } deriving (Show)
40
41-- | A symbolic executable name.
42--
43type ExeName = Text
44
45data ExecutablesFile = ExecutablesFile
46  { efPath   :: FilePath
47      -- ^ E.g. @~/.agda/executables@.
48  , efExists :: Bool
49       -- ^ The executables file might not exist,
50       --   but we may print its assumed location in error messages.
51  } deriving (Show, Data, Generic)
52
53-- | The special name @\".\"@ is used to indicated that the current directory
54--   should count as a project root.
55--
56libNameForCurrentDir :: LibName
57libNameForCurrentDir = "."
58
59-- | A file can either belong to a project located at a given root
60--   containing one or more .agda-lib files, or be part of the default
61--   project.
62data ProjectConfig
63  = ProjectConfig
64    { configRoot         :: FilePath
65    , configAgdaLibFiles :: [FilePath]
66    }
67  | DefaultProjectConfig
68  deriving Generic
69
70-- | Content of a @.agda-lib@ file.
71--
72data AgdaLibFile = AgdaLibFile
73  { _libName     :: LibName     -- ^ The symbolic name of the library.
74  , _libFile     :: FilePath    -- ^ Path to this @.agda-lib@ file (not content of the file).
75  , _libIncludes :: [FilePath]  -- ^ Roots where to look for the modules of the library.
76  , _libDepends  :: [LibName]   -- ^ Dependencies.
77  , _libPragmas  :: [String]    -- ^ Default pragma options for all files in the library.
78  }
79  deriving (Show, Generic)
80
81emptyLibFile :: AgdaLibFile
82emptyLibFile = AgdaLibFile
83  { _libName     = ""
84  , _libFile     = ""
85  , _libIncludes = []
86  , _libDepends  = []
87  , _libPragmas  = []
88  }
89
90-- | Lenses for AgdaLibFile
91
92libName :: Lens' LibName AgdaLibFile
93libName f a = f (_libName a) <&> \ x -> a { _libName = x }
94
95libFile :: Lens' FilePath AgdaLibFile
96libFile f a = f (_libFile a) <&> \ x -> a { _libFile = x }
97
98libIncludes :: Lens' [FilePath] AgdaLibFile
99libIncludes f a = f (_libIncludes a) <&> \ x -> a { _libIncludes = x }
100
101libDepends :: Lens' [LibName] AgdaLibFile
102libDepends f a = f (_libDepends a) <&> \ x -> a { _libDepends = x }
103
104libPragmas :: Lens' [String] AgdaLibFile
105libPragmas f a = f (_libPragmas a) <&> \ x -> a { _libPragmas = x }
106
107
108------------------------------------------------------------------------
109-- * Library warnings and errors
110------------------------------------------------------------------------
111
112type LineNumber = Int
113
114data LibPositionInfo = LibPositionInfo
115  { libFilePos :: Maybe FilePath -- ^ Name of @libraries@ file
116  , lineNumPos :: LineNumber     -- ^ Line number in @libraries@ file.
117  , filePos    :: FilePath       -- ^ Library file
118  }
119  deriving (Show, Data, Generic)
120
121data LibWarning = LibWarning (Maybe LibPositionInfo) LibWarning'
122  deriving (Show, Data, Generic)
123
124-- | Library Warnings.
125data LibWarning'
126  = UnknownField String
127  | ExeNotFound ExecutablesFile FilePath
128      -- ^ Raised when a trusted executable can not be found.
129  | ExeNotExecutable ExecutablesFile FilePath
130      -- ^ Raised when a trusted executable does not have the executable permission.
131  deriving (Show, Data, Generic)
132
133data LibError = LibError (Maybe LibPositionInfo) LibError'
134
135libraryWarningName :: LibWarning -> WarningName
136libraryWarningName (LibWarning c (UnknownField{})) = LibUnknownField_
137libraryWarningName (LibWarning c (ExeNotFound{})) = ExeNotFoundWarning_
138libraryWarningName (LibWarning c (ExeNotExecutable{})) = ExeNotExecutableWarning_
139
140-- | Collected errors while processing library files.
141--
142data LibError'
143  = LibNotFound LibrariesFile LibName
144      -- ^ Raised when a library name could not successfully be resolved
145      --   to an @.agda-lib@ file.
146      --
147  | AmbiguousLib LibName [AgdaLibFile]
148      -- ^ Raised when a library name is defined in several @.agda-lib files@.
149  | OtherError String
150      -- ^ Generic error.
151  deriving (Show)
152
153-- | Cache locations of project configurations and parsed .agda-lib files
154type LibState =
155  ( Map FilePath ProjectConfig
156  , Map FilePath AgdaLibFile
157  )
158
159-- | Collects 'LibError's and 'LibWarning's.
160--
161type LibErrorIO = WriterT [Either LibError LibWarning] (StateT LibState IO)
162
163-- | Throws 'Doc' exceptions, still collects 'LibWarning's.
164type LibM = ExceptT Doc (WriterT [LibWarning] (StateT LibState IO))
165
166warnings :: MonadWriter [Either LibError LibWarning] m => [LibWarning] -> m ()
167warnings = tell . map Right
168
169warnings' :: MonadWriter [Either LibError LibWarning] m => [LibWarning'] -> m ()
170warnings' = tell . map (Right . LibWarning Nothing)
171
172-- UNUSED Liang-Ting Chen 2019-07-16
173--warning :: MonadWriter [Either LibError LibWarning] m => LibWarning -> m ()
174--warning = warnings . pure
175
176raiseErrors' :: MonadWriter [Either LibError LibWarning] m => [LibError'] -> m ()
177raiseErrors' = tell . map (Left . (LibError Nothing))
178
179raiseErrors :: MonadWriter [Either LibError LibWarning] m => [LibError] -> m ()
180raiseErrors = tell . map Left
181
182getCachedProjectConfig
183  :: (MonadState LibState m, MonadIO m)
184  => FilePath -> m (Maybe ProjectConfig)
185getCachedProjectConfig path = do
186  path <- liftIO $ canonicalizePath path
187  cache <- gets fst
188  return $ Map.lookup path cache
189
190storeCachedProjectConfig
191  :: (MonadState LibState m, MonadIO m)
192  => FilePath -> ProjectConfig -> m ()
193storeCachedProjectConfig path conf = do
194  path <- liftIO $ canonicalizePath path
195  modify $ first $ Map.insert path conf
196
197getCachedAgdaLibFile
198  :: (MonadState LibState m, MonadIO m)
199  => FilePath -> m (Maybe AgdaLibFile)
200getCachedAgdaLibFile path = do
201  path <- liftIO $ canonicalizePath path
202  gets $ Map.lookup path . snd
203
204storeCachedAgdaLibFile
205  :: (MonadState LibState m, MonadIO m)
206  => FilePath -> AgdaLibFile -> m ()
207storeCachedAgdaLibFile path lib = do
208  path <- liftIO $ canonicalizePath path
209  modify $ second $ Map.insert path lib
210
211------------------------------------------------------------------------
212-- * Prettyprinting errors and warnings
213------------------------------------------------------------------------
214
215formatLibPositionInfo :: LibPositionInfo -> String -> Doc
216formatLibPositionInfo (LibPositionInfo libFile lineNum file) err = text $
217  let loc | Just lf <- libFile = lf ++ ":" ++ show lineNum ++ ": "
218          | otherwise = ""
219  in if "Failed to read" `List.isPrefixOf` err
220     then loc
221     else file ++ ":" ++ (if all isDigit (take 1 err) then "" else " ")
222
223-- | Pretty-print 'LibError'.
224formatLibError :: [AgdaLibFile] -> LibError -> Doc
225formatLibError installed (LibError mc e) = prefix <+> body where
226  prefix = case mc of
227    Nothing                      -> ""
228    Just c | OtherError err <- e -> formatLibPositionInfo c err
229    _                            -> ""
230
231  body = case e of
232    LibNotFound file lib -> vcat $
233      [ text $ "Library '" ++ lib ++ "' not found."
234      , sep [ "Add the path to its .agda-lib file to"
235            , nest 2 $ text $ "'" ++ lfPath file ++ "'"
236            , "to install."
237            ]
238      , "Installed libraries:"
239      ] ++
240      map (nest 2)
241         (if null installed then ["(none)"]
242          else [ sep [ text $ _libName l, nest 2 $ parens $ text $ _libFile l ]
243               | l <- installed ])
244
245    AmbiguousLib lib tgts -> vcat $
246      sep [ text $ "Ambiguous library '" ++ lib ++ "'."
247            , "Could refer to any one of"
248          ]
249        : [ nest 2 $ text (_libName l) <+> parens (text $ _libFile l) | l <- tgts ]
250
251
252    OtherError err -> text err
253
254instance Pretty LibWarning where
255  pretty (LibWarning mc w) = prefix <+> pretty w
256    where
257      prefix = case mc of
258        Nothing -> ""
259        Just c  -> formatLibPositionInfo c ""
260
261
262instance Pretty LibWarning' where
263  pretty (UnknownField s) = text $ "Unknown field '" ++ s ++ "'"
264  pretty (ExeNotFound file exe) = text $ "Executable '" ++ exe ++ "' not found."
265  pretty (ExeNotExecutable file exe) = text $ "Executable '" ++ exe ++ "' not executable."
266
267------------------------------------------------------------------------
268-- NFData instances
269------------------------------------------------------------------------
270
271instance NFData ExecutablesFile
272instance NFData ProjectConfig
273instance NFData AgdaLibFile
274instance NFData LibPositionInfo
275instance NFData LibWarning
276instance NFData LibWarning'
277