1-- | 2-- Module : Cryptol.ModuleSystem.Monad 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8 9{-# LANGUAGE FlexibleContexts #-} 10{-# LANGUAGE DeriveAnyClass #-} 11{-# LANGUAGE DeriveGeneric #-} 12{-# LANGUAGE OverloadedStrings #-} 13module Cryptol.ModuleSystem.Monad where 14 15import Cryptol.Eval (EvalEnv,EvalOpts(..)) 16 17import qualified Cryptol.Backend.Monad as E 18 19import Cryptol.ModuleSystem.Env 20import Cryptol.ModuleSystem.Fingerprint 21import Cryptol.ModuleSystem.Interface 22import Cryptol.ModuleSystem.Name (FreshM(..),Supply) 23import Cryptol.ModuleSystem.Renamer (RenamerError(),RenamerWarning()) 24import qualified Cryptol.Parser as Parser 25import qualified Cryptol.Parser.AST as P 26import Cryptol.Parser.Position (Located) 27import Cryptol.Utils.Panic (panic) 28import qualified Cryptol.Parser.NoPat as NoPat 29import qualified Cryptol.Parser.NoInclude as NoInc 30import qualified Cryptol.TypeCheck as T 31import qualified Cryptol.TypeCheck.AST as T 32import qualified Cryptol.TypeCheck.Solver.SMT as SMT 33 34import Cryptol.Parser.Position (Range) 35import Cryptol.Utils.Ident (interactiveName, noModuleName) 36import Cryptol.Utils.PP 37import Cryptol.Utils.Logger(Logger) 38 39import qualified Control.Monad.Fail as Fail 40import Control.Monad.IO.Class 41import Control.Exception (IOException) 42import Data.ByteString (ByteString) 43import Data.Function (on) 44import Data.Map (Map) 45import Data.Maybe (isJust) 46import Data.Text.Encoding.Error (UnicodeException) 47import MonadLib 48import System.Directory (canonicalizePath) 49 50import GHC.Generics (Generic) 51import Control.DeepSeq 52 53import Prelude () 54import Prelude.Compat 55 56 57-- Errors ---------------------------------------------------------------------- 58 59data ImportSource 60 = FromModule P.ModName 61 | FromImport (Located P.Import) 62 | FromModuleInstance (Located P.ModName) 63 deriving (Show, Generic, NFData) 64 65instance Eq ImportSource where 66 (==) = (==) `on` importedModule 67 68instance PP ImportSource where 69 ppPrec _ is = case is of 70 FromModule n -> text "module name" <+> pp n 71 FromImport li -> text "import of module" <+> pp (P.iModule (P.thing li)) 72 FromModuleInstance l -> 73 text "instantiation of module" <+> pp (P.thing l) 74 75importedModule :: ImportSource -> P.ModName 76importedModule is = 77 case is of 78 FromModule n -> n 79 FromImport li -> P.iModule (P.thing li) 80 FromModuleInstance l -> P.thing l 81 82 83data ModuleError 84 = ModuleNotFound P.ModName [FilePath] 85 -- ^ Unable to find the module given, tried looking in these paths 86 | CantFindFile FilePath 87 -- ^ Unable to open a file 88 | BadUtf8 ModulePath UnicodeException 89 -- ^ Bad UTF-8 encoding in while decoding this file 90 | OtherIOError FilePath IOException 91 -- ^ Some other IO error occurred while reading this file 92 | ModuleParseError ModulePath Parser.ParseError 93 -- ^ Generated this parse error when parsing the file for module m 94 | RecursiveModules [ImportSource] 95 -- ^ Recursive module group discovered 96 | RenamerErrors ImportSource [RenamerError] 97 -- ^ Problems during the renaming phase 98 | NoPatErrors ImportSource [NoPat.Error] 99 -- ^ Problems during the NoPat phase 100 | NoIncludeErrors ImportSource [NoInc.IncludeError] 101 -- ^ Problems during the NoInclude phase 102 | TypeCheckingFailed ImportSource T.NameMap [(Range,T.Error)] 103 -- ^ Problems during type checking 104 | OtherFailure String 105 -- ^ Problems after type checking, eg. specialization 106 | ModuleNameMismatch P.ModName (Located P.ModName) 107 -- ^ Module loaded by 'import' statement has the wrong module name 108 | DuplicateModuleName P.ModName FilePath FilePath 109 -- ^ Two modules loaded from different files have the same module name 110 | ImportedParamModule P.ModName 111 -- ^ Attempt to import a parametrized module that was not instantiated. 112 | FailedToParameterizeModDefs P.ModName [T.Name] 113 -- ^ Failed to add the module parameters to all definitions in a module. 114 | NotAParameterizedModule P.ModName 115 116 | ErrorInFile ModulePath ModuleError 117 -- ^ This is just a tag on the error, indicating the file containing it. 118 -- It is convenient when we had to look for the module, and we'd like 119 -- to communicate the location of pthe problematic module to the handler. 120 121 deriving (Show) 122 123instance NFData ModuleError where 124 rnf e = case e of 125 ModuleNotFound src path -> src `deepseq` path `deepseq` () 126 CantFindFile path -> path `deepseq` () 127 BadUtf8 path ue -> rnf (path, ue) 128 OtherIOError path exn -> path `deepseq` exn `seq` () 129 ModuleParseError source err -> source `deepseq` err `deepseq` () 130 RecursiveModules mods -> mods `deepseq` () 131 RenamerErrors src errs -> src `deepseq` errs `deepseq` () 132 NoPatErrors src errs -> src `deepseq` errs `deepseq` () 133 NoIncludeErrors src errs -> src `deepseq` errs `deepseq` () 134 TypeCheckingFailed nm src errs -> nm `deepseq` src `deepseq` errs `deepseq` () 135 ModuleNameMismatch expected found -> 136 expected `deepseq` found `deepseq` () 137 DuplicateModuleName name path1 path2 -> 138 name `deepseq` path1 `deepseq` path2 `deepseq` () 139 OtherFailure x -> x `deepseq` () 140 ImportedParamModule x -> x `deepseq` () 141 FailedToParameterizeModDefs x xs -> x `deepseq` xs `deepseq` () 142 NotAParameterizedModule x -> x `deepseq` () 143 ErrorInFile x y -> x `deepseq` y `deepseq` () 144 145instance PP ModuleError where 146 ppPrec prec e = case e of 147 148 ModuleNotFound src path -> 149 text "[error]" <+> 150 text "Could not find module" <+> pp src 151 $$ 152 hang (text "Searched paths:") 153 4 (vcat (map text path)) 154 $$ 155 text "Set the CRYPTOLPATH environment variable to search more directories" 156 157 CantFindFile path -> 158 text "[error]" <+> 159 text "can't find file:" <+> text path 160 161 BadUtf8 path _ue -> 162 text "[error]" <+> 163 text "bad utf-8 encoding:" <+> pp path 164 165 OtherIOError path exn -> 166 hang (text "[error]" <+> 167 text "IO error while loading file:" <+> text path <.> colon) 168 4 (text (show exn)) 169 170 ModuleParseError _source err -> Parser.ppError err 171 172 RecursiveModules mods -> 173 hang (text "[error] module imports form a cycle:") 174 4 (vcat (map pp (reverse mods))) 175 176 RenamerErrors _src errs -> vcat (map pp errs) 177 178 NoPatErrors _src errs -> vcat (map pp errs) 179 180 NoIncludeErrors _src errs -> vcat (map NoInc.ppIncludeError errs) 181 182 TypeCheckingFailed _src nm errs -> vcat (map (T.ppNamedError nm) errs) 183 184 ModuleNameMismatch expected found -> 185 hang (text "[error]" <+> pp (P.srcRange found) <.> char ':') 186 4 (vcat [ text "File name does not match module name:" 187 , text "Saw:" <+> pp (P.thing found) 188 , text "Expected:" <+> pp expected 189 ]) 190 191 DuplicateModuleName name path1 path2 -> 192 hang (text "[error] module" <+> pp name <+> 193 text "is defined in multiple files:") 194 4 (vcat [text path1, text path2]) 195 196 OtherFailure x -> text x 197 198 ImportedParamModule p -> 199 text "[error] Import of a non-instantiated parameterized module:" <+> pp p 200 201 FailedToParameterizeModDefs x xs -> 202 hang (text "[error] Parameterized module" <+> pp x <+> 203 text "has polymorphic parameters:") 204 4 (hsep $ punctuate comma $ map pp xs) 205 206 NotAParameterizedModule x -> 207 text "[error] Module" <+> pp x <+> text "does not have parameters." 208 209 ErrorInFile _ x -> ppPrec prec x 210 211moduleNotFound :: P.ModName -> [FilePath] -> ModuleM a 212moduleNotFound name paths = ModuleT (raise (ModuleNotFound name paths)) 213 214cantFindFile :: FilePath -> ModuleM a 215cantFindFile path = ModuleT (raise (CantFindFile path)) 216 217badUtf8 :: ModulePath -> UnicodeException -> ModuleM a 218badUtf8 path ue = ModuleT (raise (BadUtf8 path ue)) 219 220otherIOError :: FilePath -> IOException -> ModuleM a 221otherIOError path exn = ModuleT (raise (OtherIOError path exn)) 222 223moduleParseError :: ModulePath -> Parser.ParseError -> ModuleM a 224moduleParseError path err = 225 ModuleT (raise (ModuleParseError path err)) 226 227recursiveModules :: [ImportSource] -> ModuleM a 228recursiveModules loaded = ModuleT (raise (RecursiveModules loaded)) 229 230renamerErrors :: [RenamerError] -> ModuleM a 231renamerErrors errs = do 232 src <- getImportSource 233 ModuleT (raise (RenamerErrors src errs)) 234 235noPatErrors :: [NoPat.Error] -> ModuleM a 236noPatErrors errs = do 237 src <- getImportSource 238 ModuleT (raise (NoPatErrors src errs)) 239 240noIncludeErrors :: [NoInc.IncludeError] -> ModuleM a 241noIncludeErrors errs = do 242 src <- getImportSource 243 ModuleT (raise (NoIncludeErrors src errs)) 244 245typeCheckingFailed :: T.NameMap -> [(Range,T.Error)] -> ModuleM a 246typeCheckingFailed nameMap errs = do 247 src <- getImportSource 248 ModuleT (raise (TypeCheckingFailed src nameMap errs)) 249 250moduleNameMismatch :: P.ModName -> Located P.ModName -> ModuleM a 251moduleNameMismatch expected found = 252 ModuleT (raise (ModuleNameMismatch expected found)) 253 254duplicateModuleName :: P.ModName -> FilePath -> FilePath -> ModuleM a 255duplicateModuleName name path1 path2 = 256 ModuleT (raise (DuplicateModuleName name path1 path2)) 257 258importParamModule :: P.ModName -> ModuleM a 259importParamModule x = ModuleT (raise (ImportedParamModule x)) 260 261failedToParameterizeModDefs :: P.ModName -> [T.Name] -> ModuleM a 262failedToParameterizeModDefs x xs = 263 ModuleT (raise (FailedToParameterizeModDefs x xs)) 264 265notAParameterizedModule :: P.ModName -> ModuleM a 266notAParameterizedModule x = ModuleT (raise (NotAParameterizedModule x)) 267 268-- | Run the computation, and if it caused and error, tag the error 269-- with the given file. 270errorInFile :: ModulePath -> ModuleM a -> ModuleM a 271errorInFile file (ModuleT m) = ModuleT (m `handle` h) 272 where h e = raise $ case e of 273 ErrorInFile {} -> e 274 _ -> ErrorInFile file e 275 276-- Warnings -------------------------------------------------------------------- 277 278data ModuleWarning 279 = TypeCheckWarnings T.NameMap [(Range,T.Warning)] 280 | RenamerWarnings [RenamerWarning] 281 deriving (Show, Generic, NFData) 282 283instance PP ModuleWarning where 284 ppPrec _ w = case w of 285 TypeCheckWarnings nm ws -> vcat (map (T.ppNamedWarning nm) ws) 286 RenamerWarnings ws -> vcat (map pp ws) 287 288warn :: [ModuleWarning] -> ModuleM () 289warn = ModuleT . put 290 291typeCheckWarnings :: T.NameMap -> [(Range,T.Warning)] -> ModuleM () 292typeCheckWarnings nameMap ws 293 | null ws = return () 294 | otherwise = warn [TypeCheckWarnings nameMap ws] 295 296renamerWarnings :: [RenamerWarning] -> ModuleM () 297renamerWarnings ws 298 | null ws = return () 299 | otherwise = warn [RenamerWarnings ws] 300 301 302-- Module System Monad --------------------------------------------------------- 303 304data RO m = 305 RO { roLoading :: [ImportSource] 306 , roEvalOpts :: m EvalOpts 307 , roCallStacks :: Bool 308 , roFileReader :: FilePath -> m ByteString 309 , roTCSolver :: SMT.Solver 310 } 311 312emptyRO :: ModuleInput m -> RO m 313emptyRO minp = 314 RO { roLoading = [] 315 , roEvalOpts = minpEvalOpts minp 316 , roCallStacks = minpCallStacks minp 317 , roFileReader = minpByteReader minp 318 , roTCSolver = minpTCSolver minp 319 } 320 321newtype ModuleT m a = ModuleT 322 { unModuleT :: ReaderT (RO m) 323 (StateT ModuleEnv 324 (ExceptionT ModuleError 325 (WriterT [ModuleWarning] m))) a 326 } 327 328instance Monad m => Functor (ModuleT m) where 329 {-# INLINE fmap #-} 330 fmap f m = ModuleT (fmap f (unModuleT m)) 331 332instance Monad m => Applicative (ModuleT m) where 333 {-# INLINE pure #-} 334 pure x = ModuleT (pure x) 335 336 {-# INLINE (<*>) #-} 337 l <*> r = ModuleT (unModuleT l <*> unModuleT r) 338 339instance Monad m => Monad (ModuleT m) where 340 {-# INLINE return #-} 341 return x = ModuleT (return x) 342 343 {-# INLINE (>>=) #-} 344 m >>= f = ModuleT (unModuleT m >>= unModuleT . f) 345 346instance Fail.MonadFail m => Fail.MonadFail (ModuleT m) where 347 {-# INLINE fail #-} 348 fail = ModuleT . raise . OtherFailure 349 350instance MonadT ModuleT where 351 {-# INLINE lift #-} 352 lift = ModuleT . lift . lift . lift . lift 353 354instance Monad m => FreshM (ModuleT m) where 355 liftSupply f = ModuleT $ 356 do me <- get 357 let (a,s') = f (meSupply me) 358 set $! me { meSupply = s' } 359 return a 360 361instance MonadIO m => MonadIO (ModuleT m) where 362 liftIO m = lift $ liftIO m 363 364 365data ModuleInput m = 366 ModuleInput 367 { minpCallStacks :: Bool 368 , minpEvalOpts :: m EvalOpts 369 , minpByteReader :: FilePath -> m ByteString 370 , minpModuleEnv :: ModuleEnv 371 , minpTCSolver :: SMT.Solver 372 } 373 374runModuleT :: 375 Monad m => 376 ModuleInput m -> 377 ModuleT m a -> 378 m (Either ModuleError (a, ModuleEnv), [ModuleWarning]) 379runModuleT minp m = 380 runWriterT 381 $ runExceptionT 382 $ runStateT (minpModuleEnv minp) 383 $ runReaderT (emptyRO minp) 384 $ unModuleT m 385 386type ModuleM = ModuleT IO 387 388runModuleM :: 389 ModuleInput IO -> 390 ModuleM a -> 391 IO (Either ModuleError (a,ModuleEnv),[ModuleWarning]) 392runModuleM = runModuleT 393 394 395io :: BaseM m IO => IO a -> ModuleT m a 396io m = ModuleT (inBase m) 397 398getByteReader :: Monad m => ModuleT m (FilePath -> m ByteString) 399getByteReader = ModuleT $ do 400 RO { roFileReader = readFileBytes } <- ask 401 return readFileBytes 402 403getCallStacks :: Monad m => ModuleT m Bool 404getCallStacks = ModuleT (roCallStacks <$> ask) 405 406readBytes :: Monad m => FilePath -> ModuleT m ByteString 407readBytes fn = do 408 fileReader <- getByteReader 409 ModuleT $ lift $ lift $ lift $ lift $ fileReader fn 410 411getModuleEnv :: Monad m => ModuleT m ModuleEnv 412getModuleEnv = ModuleT get 413 414getTCSolver :: Monad m => ModuleT m SMT.Solver 415getTCSolver = ModuleT (roTCSolver <$> ask) 416 417setModuleEnv :: Monad m => ModuleEnv -> ModuleT m () 418setModuleEnv = ModuleT . set 419 420modifyModuleEnv :: Monad m => (ModuleEnv -> ModuleEnv) -> ModuleT m () 421modifyModuleEnv f = ModuleT $ do 422 env <- get 423 set $! f env 424 425getLoadedMaybe :: P.ModName -> ModuleM (Maybe LoadedModule) 426getLoadedMaybe mn = ModuleT $ 427 do env <- get 428 return (lookupModule mn env) 429 430isLoaded :: P.ModName -> ModuleM Bool 431isLoaded mn = isJust <$> getLoadedMaybe mn 432 433loadingImport :: Located P.Import -> ModuleM a -> ModuleM a 434loadingImport = loading . FromImport 435 436loadingModule :: P.ModName -> ModuleM a -> ModuleM a 437loadingModule = loading . FromModule 438 439loadingModInstance :: Located P.ModName -> ModuleM a -> ModuleM a 440loadingModInstance = loading . FromModuleInstance 441 442-- | Push an "interactive" context onto the loading stack. A bit of a hack, as 443-- it uses a faked module name 444interactive :: ModuleM a -> ModuleM a 445interactive = loadingModule interactiveName 446 447loading :: ImportSource -> ModuleM a -> ModuleM a 448loading src m = ModuleT $ do 449 ro <- ask 450 let ro' = ro { roLoading = src : roLoading ro } 451 452 -- check for recursive modules 453 when (src `elem` roLoading ro) (raise (RecursiveModules (roLoading ro'))) 454 455 local ro' (unModuleT m) 456 457-- | Get the currently focused import source. 458getImportSource :: ModuleM ImportSource 459getImportSource = ModuleT $ do 460 ro <- ask 461 case roLoading ro of 462 is : _ -> return is 463 _ -> return (FromModule noModuleName) 464 465getIface :: P.ModName -> ModuleM Iface 466getIface mn = 467 do env <- ModuleT get 468 case lookupModule mn env of 469 Just lm -> return (lmInterface lm) 470 Nothing -> panic "ModuleSystem" ["Interface not available", show (pp mn)] 471 472getLoaded :: P.ModName -> ModuleM T.Module 473getLoaded mn = ModuleT $ 474 do env <- get 475 case lookupModule mn env of 476 Just lm -> return (lmModule lm) 477 Nothing -> panic "ModuleSystem" ["Module not available", show (pp mn) ] 478 479getNameSeeds :: ModuleM T.NameSeeds 480getNameSeeds = ModuleT (meNameSeeds `fmap` get) 481 482getSupply :: ModuleM Supply 483getSupply = ModuleT (meSupply `fmap` get) 484 485getMonoBinds :: ModuleM Bool 486getMonoBinds = ModuleT (meMonoBinds `fmap` get) 487 488setMonoBinds :: Bool -> ModuleM () 489setMonoBinds b = ModuleT $ do 490 env <- get 491 set $! env { meMonoBinds = b } 492 493setNameSeeds :: T.NameSeeds -> ModuleM () 494setNameSeeds seeds = ModuleT $ do 495 env <- get 496 set $! env { meNameSeeds = seeds } 497 498setSupply :: Supply -> ModuleM () 499setSupply supply = ModuleT $ 500 do env <- get 501 set $! env { meSupply = supply } 502 503unloadModule :: (LoadedModule -> Bool) -> ModuleM () 504unloadModule rm = ModuleT $ do 505 env <- get 506 set $! env { meLoadedModules = removeLoadedModule rm (meLoadedModules env) } 507 508loadedModule :: ModulePath -> Fingerprint -> T.Module -> ModuleM () 509loadedModule path fp m = ModuleT $ do 510 env <- get 511 ident <- case path of 512 InFile p -> unModuleT $ io (canonicalizePath p) 513 InMem l _ -> pure l 514 515 set $! env { meLoadedModules = addLoadedModule path ident fp m (meLoadedModules env) } 516 517modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM () 518modifyEvalEnv f = ModuleT $ do 519 env <- get 520 let evalEnv = meEvalEnv env 521 evalEnv' <- inBase $ E.runEval mempty (f evalEnv) 522 set $! env { meEvalEnv = evalEnv' } 523 524getEvalEnv :: ModuleM EvalEnv 525getEvalEnv = ModuleT (meEvalEnv `fmap` get) 526 527getEvalOptsAction :: ModuleM (IO EvalOpts) 528getEvalOptsAction = ModuleT (roEvalOpts `fmap` ask) 529 530getEvalOpts :: ModuleM EvalOpts 531getEvalOpts = 532 do act <- getEvalOptsAction 533 liftIO act 534 535getNewtypes :: ModuleM (Map T.Name T.Newtype) 536getNewtypes = ModuleT (loadedNewtypes <$> get) 537 538getFocusedModule :: ModuleM (Maybe P.ModName) 539getFocusedModule = ModuleT (meFocusedModule `fmap` get) 540 541setFocusedModule :: P.ModName -> ModuleM () 542setFocusedModule n = ModuleT $ do 543 me <- get 544 set $! me { meFocusedModule = Just n } 545 546getSearchPath :: ModuleM [FilePath] 547getSearchPath = ModuleT (meSearchPath `fmap` get) 548 549-- | Run a 'ModuleM' action in a context with a prepended search 550-- path. Useful for temporarily looking in other places while 551-- resolving imports, for example. 552withPrependedSearchPath :: [FilePath] -> ModuleM a -> ModuleM a 553withPrependedSearchPath fps m = ModuleT $ do 554 env0 <- get 555 let fps0 = meSearchPath env0 556 set $! env0 { meSearchPath = fps ++ fps0 } 557 x <- unModuleT m 558 env <- get 559 set $! env { meSearchPath = fps0 } 560 return x 561 562getFocusedEnv :: ModuleM ModContext 563getFocusedEnv = ModuleT (focusedEnv `fmap` get) 564 565getDynEnv :: ModuleM DynamicEnv 566getDynEnv = ModuleT (meDynEnv `fmap` get) 567 568setDynEnv :: DynamicEnv -> ModuleM () 569setDynEnv denv = ModuleT $ do 570 me <- get 571 set $! me { meDynEnv = denv } 572 573setSolver :: T.SolverConfig -> ModuleM () 574setSolver cfg = ModuleT $ do 575 me <- get 576 set $! me { meSolverConfig = cfg } 577 578getSolverConfig :: ModuleM T.SolverConfig 579getSolverConfig = ModuleT $ do 580 me <- get 581 return (meSolverConfig me) 582 583-- | Usefule for logging. For example: @withLogger logPutStrLn "Hello"@ 584withLogger :: (Logger -> a -> IO b) -> a -> ModuleM b 585withLogger f a = do l <- getEvalOpts 586 io (f (evalLogger l) a) 587