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