1-- | 2-- Module : Cryptol.ModuleSystem.Base 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8-- 9-- This is the main driver---it provides entry points for the 10-- various passes. 11 12{-# LANGUAGE FlexibleContexts #-} 13{-# LANGUAGE ImplicitParams #-} 14{-# LANGUAGE RecordWildCards #-} 15 16module Cryptol.ModuleSystem.Base where 17 18import Cryptol.ModuleSystem.Env (DynamicEnv(..)) 19import Cryptol.ModuleSystem.Fingerprint 20import Cryptol.ModuleSystem.Interface 21import Cryptol.ModuleSystem.Monad 22import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap) 23import Cryptol.ModuleSystem.Env (lookupModule 24 , LoadedModule(..) 25 , meCoreLint, CoreLint(..) 26 , ModContext(..) 27 , ModulePath(..), modulePathLabel) 28import qualified Cryptol.Eval as E 29import qualified Cryptol.Eval.Concrete as Concrete 30import Cryptol.Eval.Concrete (Concrete(..)) 31import qualified Cryptol.ModuleSystem.NamingEnv as R 32import qualified Cryptol.ModuleSystem.Renamer as R 33import qualified Cryptol.Parser as P 34import qualified Cryptol.Parser.Unlit as P 35import Cryptol.Parser.AST as P 36import Cryptol.Parser.NoPat (RemovePatterns(removePatterns)) 37import Cryptol.Parser.NoInclude (removeIncludesModule) 38import Cryptol.Parser.Position (HasLoc(..), Range, emptyRange) 39import qualified Cryptol.TypeCheck as T 40import qualified Cryptol.TypeCheck.AST as T 41import qualified Cryptol.TypeCheck.PP as T 42import qualified Cryptol.TypeCheck.Sanity as TcSanity 43 44import Cryptol.Transform.AddModParams (addModParams) 45import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName 46 , preludeReferenceName, interactiveName, modNameChunks 47 , notParamInstModName, isParamInstModName ) 48import Cryptol.Utils.PP (pretty) 49import Cryptol.Utils.Panic (panic) 50import Cryptol.Utils.Logger(logPutStrLn, logPrint) 51 52import Cryptol.Prelude ( preludeContents, floatContents, arrayContents 53 , suiteBContents, primeECContents, preludeReferenceContents ) 54import Cryptol.Transform.MonoValues (rewModule) 55 56import qualified Control.Exception as X 57import Control.Monad (unless,when) 58import Data.Maybe (fromMaybe) 59import Data.Monoid ((<>)) 60import Data.Text.Encoding (decodeUtf8') 61import System.Directory (doesFileExist, canonicalizePath) 62import System.FilePath ( addExtension 63 , isAbsolute 64 , joinPath 65 , (</>) 66 , normalise 67 , takeDirectory 68 , takeFileName 69 ) 70import qualified System.IO.Error as IOE 71import qualified Data.Map as Map 72 73import Prelude () 74import Prelude.Compat hiding ( (<>) ) 75 76 77-- Renaming -------------------------------------------------------------------- 78 79rename :: ModName -> R.NamingEnv -> R.RenameM a -> ModuleM a 80rename modName env m = do 81 (res,ws) <- liftSupply $ \ supply -> 82 case R.runRenamer supply modName env m of 83 (Right (a,supply'),ws) -> ((Right a,ws),supply') 84 (Left errs,ws) -> ((Left errs,ws),supply) 85 86 renamerWarnings ws 87 case res of 88 Right r -> return r 89 Left errs -> renamerErrors errs 90 91-- | Rename a module in the context of its imported modules. 92renameModule :: P.Module PName 93 -> ModuleM (IfaceDecls,R.NamingEnv,P.Module Name) 94renameModule m = do 95 (decls,menv) <- importIfaces (map thing (P.mImports m)) 96 (declsEnv,rm) <- rename (thing (mName m)) menv (R.renameModule m) 97 return (decls,declsEnv,rm) 98 99 100-- NoPat ----------------------------------------------------------------------- 101 102-- | Run the noPat pass. 103noPat :: RemovePatterns a => a -> ModuleM a 104noPat a = do 105 let (a',errs) = removePatterns a 106 unless (null errs) (noPatErrors errs) 107 return a' 108 109 110-- Parsing --------------------------------------------------------------------- 111 112parseModule :: ModulePath -> ModuleM (Fingerprint, P.Module PName) 113parseModule path = do 114 getBytes <- getByteReader 115 116 bytesRes <- case path of 117 InFile p -> io (X.try (getBytes p)) 118 InMem _ bs -> pure (Right bs) 119 120 bytes <- case bytesRes of 121 Right bytes -> return bytes 122 Left exn -> 123 case path of 124 InFile p 125 | IOE.isDoesNotExistError exn -> cantFindFile p 126 | otherwise -> otherIOError p exn 127 InMem p _ -> panic "parseModule" 128 [ "IOError for in-memory contetns???" 129 , "Label: " ++ show p 130 , "Exception: " ++ show exn ] 131 132 txt <- case decodeUtf8' bytes of 133 Right txt -> return txt 134 Left e -> badUtf8 path e 135 136 let cfg = P.defaultConfig 137 { P.cfgSource = case path of 138 InFile p -> p 139 InMem l _ -> l 140 , P.cfgPreProc = P.guessPreProc (modulePathLabel path) 141 } 142 143 case P.parseModule cfg txt of 144 Right pm -> let fp = fingerprint bytes 145 in fp `seq` return (fp, pm) 146 Left err -> moduleParseError path err 147 148 149-- Modules --------------------------------------------------------------------- 150 151-- | Load a module by its path. 152loadModuleByPath :: FilePath -> ModuleM T.Module 153loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do 154 let fileName = takeFileName path 155 foundPath <- findFile fileName 156 (fp, pm) <- parseModule (InFile foundPath) 157 let n = thing (P.mName pm) 158 159 -- Check whether this module name has already been loaded from a different file 160 env <- getModuleEnv 161 -- path' is the resolved, absolute path, used only for checking 162 -- whether it's already been loaded 163 path' <- io (canonicalizePath foundPath) 164 165 case lookupModule n env of 166 -- loadModule will calculate the canonical path again 167 Nothing -> doLoadModule False (FromModule n) (InFile foundPath) fp pm 168 Just lm 169 | path' == loaded -> return (lmModule lm) 170 | otherwise -> duplicateModuleName n path' loaded 171 where loaded = lmModuleId lm 172 173 174-- | Load a module, unless it was previously loaded. 175loadModuleFrom :: Bool {- ^ quiet mode -} -> ImportSource -> ModuleM (ModulePath,T.Module) 176loadModuleFrom quiet isrc = 177 do let n = importedModule isrc 178 mb <- getLoadedMaybe n 179 case mb of 180 Just m -> return (lmFilePath m, lmModule m) 181 Nothing -> 182 do path <- findModule n 183 errorInFile path $ 184 do (fp, pm) <- parseModule path 185 m <- doLoadModule quiet isrc path fp pm 186 return (path,m) 187 188-- | Load dependencies, typecheck, and add to the eval environment. 189doLoadModule :: 190 Bool {- ^ quiet mode: true suppresses the "loading module" message -} -> 191 ImportSource -> 192 ModulePath -> 193 Fingerprint -> 194 P.Module PName -> 195 ModuleM T.Module 196doLoadModule quiet isrc path fp pm0 = 197 loading isrc $ 198 do let pm = addPrelude pm0 199 loadDeps pm 200 201 unless quiet $ withLogger logPutStrLn 202 ("Loading module " ++ pretty (P.thing (P.mName pm))) 203 tcm <- optionalInstantiate =<< checkModule isrc path pm 204 205 -- extend the eval env, unless a functor. 206 tbl <- Concrete.primTable <$> getEvalOptsAction 207 let ?evalPrim = \i -> Right <$> Map.lookup i tbl 208 callStacks <- getCallStacks 209 let ?callStacks = callStacks 210 unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv Concrete tcm) 211 loadedModule path fp tcm 212 213 return tcm 214 where 215 optionalInstantiate tcm 216 | isParamInstModName (importedModule isrc) = 217 if T.isParametrizedModule tcm then 218 case addModParams tcm of 219 Right tcm1 -> return tcm1 220 Left xs -> failedToParameterizeModDefs (T.mName tcm) xs 221 else notAParameterizedModule (T.mName tcm) 222 | otherwise = return tcm 223 224 225 226 227 228-- | Rewrite an import declaration to be of the form: 229-- 230-- > import foo as foo [ [hiding] (a,b,c) ] 231fullyQualified :: P.Import -> P.Import 232fullyQualified i = i { iAs = Just (iModule i) } 233 234-- | Find the interface referenced by an import, and generate the naming 235-- environment that it describes. 236importIface :: P.Import -> ModuleM (IfaceDecls,R.NamingEnv) 237importIface imp = 238 do Iface { .. } <- getIface (T.iModule imp) 239 return (ifPublic, R.interpImport imp ifPublic) 240 241-- | Load a series of interfaces, merging their public interfaces. 242importIfaces :: [P.Import] -> ModuleM (IfaceDecls,R.NamingEnv) 243importIfaces is = mconcat `fmap` mapM importIface is 244 245moduleFile :: ModName -> String -> FilePath 246moduleFile n = addExtension (joinPath (modNameChunks n)) 247 248 249-- | Discover a module. 250findModule :: ModName -> ModuleM ModulePath 251findModule n = do 252 paths <- getSearchPath 253 loop (possibleFiles paths) 254 where 255 loop paths = case paths of 256 257 path:rest -> do 258 b <- io (doesFileExist path) 259 if b then return (InFile path) else loop rest 260 261 [] -> handleNotFound 262 263 handleNotFound = 264 case n of 265 m | m == preludeName -> pure (InMem "Cryptol" preludeContents) 266 | m == floatName -> pure (InMem "Float" floatContents) 267 | m == arrayName -> pure (InMem "Array" arrayContents) 268 | m == suiteBName -> pure (InMem "SuiteB" suiteBContents) 269 | m == primeECName -> pure (InMem "PrimeEC" primeECContents) 270 | m == preludeReferenceName -> pure (InMem "Cryptol::Reference" preludeReferenceContents) 271 _ -> moduleNotFound n =<< getSearchPath 272 273 -- generate all possible search paths 274 possibleFiles paths = do 275 path <- paths 276 ext <- P.knownExts 277 return (path </> moduleFile n ext) 278 279-- | Discover a file. This is distinct from 'findModule' in that we 280-- assume we've already been given a particular file name. 281findFile :: FilePath -> ModuleM FilePath 282findFile path | isAbsolute path = do 283 -- No search path checking for absolute paths 284 b <- io (doesFileExist path) 285 if b then return path else cantFindFile path 286findFile path = do 287 paths <- getSearchPath 288 loop (possibleFiles paths) 289 where 290 loop paths = case paths of 291 path':rest -> do 292 b <- io (doesFileExist path') 293 if b then return (normalise path') else loop rest 294 [] -> cantFindFile path 295 possibleFiles paths = map (</> path) paths 296 297-- | Add the prelude to the import list if it's not already mentioned. 298addPrelude :: P.Module PName -> P.Module PName 299addPrelude m 300 | preludeName == P.thing (P.mName m) = m 301 | preludeName `elem` importedMods = m 302 | otherwise = m { mImports = importPrelude : mImports m } 303 where 304 importedMods = map (P.iModule . P.thing) (P.mImports m) 305 importPrelude = P.Located 306 { P.srcRange = emptyRange 307 , P.thing = P.Import 308 { iModule = preludeName 309 , iAs = Nothing 310 , iSpec = Nothing 311 } 312 } 313 314-- | Load the dependencies of a module into the environment. 315loadDeps :: P.Module name -> ModuleM () 316loadDeps m = 317 do mapM_ loadI (P.mImports m) 318 mapM_ loadF (P.mInstance m) 319 where 320 loadI i = do (_,m1) <- loadModuleFrom False (FromImport i) 321 when (T.isParametrizedModule m1) $ importParamModule $ T.mName m1 322 loadF f = do _ <- loadModuleFrom False (FromModuleInstance f) 323 return () 324 325 326 327-- Type Checking --------------------------------------------------------------- 328 329-- | Typecheck a single expression, yielding a renamed parsed expression, 330-- typechecked core expression, and a type schema. 331checkExpr :: P.Expr PName -> ModuleM (P.Expr Name,T.Expr,T.Schema) 332checkExpr e = do 333 334 fe <- getFocusedEnv 335 let params = mctxParams fe 336 decls = mctxDecls fe 337 names = mctxNames fe 338 339 -- run NoPat 340 npe <- noPat e 341 342 -- rename the expression with dynamic names shadowing the opened environment 343 re <- rename interactiveName names (R.rename npe) 344 345 -- merge the dynamic and opened environments for typechecking 346 prims <- getPrimMap 347 let act = TCAction { tcAction = T.tcExpr, tcLinter = exprLinter 348 , tcPrims = prims } 349 (te,s) <- typecheck act re params decls 350 351 return (re,te,s) 352 353-- | Typecheck a group of declarations. 354-- 355-- INVARIANT: This assumes that NoPat has already been run on the declarations. 356checkDecls :: [P.TopDecl PName] -> ModuleM (R.NamingEnv,[T.DeclGroup]) 357checkDecls ds = do 358 fe <- getFocusedEnv 359 let params = mctxParams fe 360 decls = mctxDecls fe 361 names = mctxNames fe 362 363 -- introduce names for the declarations before renaming them 364 declsEnv <- liftSupply (R.namingEnv' (map (R.InModule interactiveName) ds)) 365 rds <- rename interactiveName (declsEnv `R.shadowing` names) 366 (traverse R.rename ds) 367 368 prims <- getPrimMap 369 let act = TCAction { tcAction = T.tcDecls, tcLinter = declsLinter 370 , tcPrims = prims } 371 ds' <- typecheck act rds params decls 372 return (declsEnv,ds') 373 374-- | Generate the primitive map. If the prelude is currently being loaded, this 375-- should be generated directly from the naming environment given to the renamer 376-- instead. 377getPrimMap :: ModuleM PrimMap 378getPrimMap = 379 do env <- getModuleEnv 380 let mkPrims = ifacePrimMap . lmInterface 381 mp `alsoPrimFrom` m = 382 case lookupModule m env of 383 Nothing -> mp 384 Just lm -> mkPrims lm <> mp 385 386 case lookupModule preludeName env of 387 Just prel -> return $ mkPrims prel 388 `alsoPrimFrom` floatName 389 Nothing -> panic "Cryptol.ModuleSystem.Base.getPrimMap" 390 [ "Unable to find the prelude" ] 391 392-- | Load a module, be it a normal module or a functor instantiation. 393checkModule :: ImportSource -> ModulePath -> P.Module PName -> ModuleM T.Module 394checkModule isrc path m = 395 case P.mInstance m of 396 Nothing -> checkSingleModule T.tcModule isrc path m 397 Just fmName -> do tf <- getLoaded (thing fmName) 398 checkSingleModule (T.tcModuleInst tf) isrc path m 399 400 401-- | Typecheck a single module. If the module is an instantiation 402-- of a functor, then this just type-checks the instantiating parameters. 403-- See 'checkModule' 404checkSingleModule :: 405 Act (P.Module Name) T.Module {- ^ how to check -} -> 406 ImportSource {- ^ why are we loading this -} -> 407 ModulePath {- path -} -> 408 P.Module PName {- ^ module to check -} -> 409 ModuleM T.Module 410checkSingleModule how isrc path m = do 411 412 -- check that the name of the module matches expectations 413 let nm = importedModule isrc 414 unless (notParamInstModName nm == thing (P.mName m)) 415 (moduleNameMismatch nm (mName m)) 416 417 -- remove includes first; we only do this for actual files. 418 -- it is less clear what should happen for in-memory things, and since 419 -- this is a more-or-less obsolete feature, we are just not doing 420 -- ot for now. 421 e <- case path of 422 InFile p -> do 423 r <- getByteReader 424 io (removeIncludesModule r p m) 425 InMem {} -> pure (Right m) 426 427 nim <- case e of 428 Right nim -> return nim 429 Left ierrs -> noIncludeErrors ierrs 430 431 -- remove pattern bindings 432 npm <- noPat nim 433 434 -- rename everything 435 (tcEnv,declsEnv,scm) <- renameModule npm 436 437 -- when generating the prim map for the typechecker, if we're checking the 438 -- prelude, we have to generate the map from the renaming environment, as we 439 -- don't have the interface yet. 440 prims <- if thing (mName m) == preludeName 441 then return (R.toPrimMap declsEnv) 442 else getPrimMap 443 444 -- typecheck 445 let act = TCAction { tcAction = how 446 , tcLinter = moduleLinter (P.thing (P.mName m)) 447 , tcPrims = prims } 448 449 450 tcm0 <- typecheck act scm noIfaceParams tcEnv 451 452 let tcm = tcm0 -- fromMaybe tcm0 (addModParams tcm0) 453 454 liftSupply (`rewModule` tcm) 455 456data TCLinter o = TCLinter 457 { lintCheck :: 458 o -> T.InferInput -> Either (Range, TcSanity.Error) [TcSanity.ProofObligation] 459 , lintModule :: Maybe P.ModName 460 } 461 462 463exprLinter :: TCLinter (T.Expr, T.Schema) 464exprLinter = TCLinter 465 { lintCheck = \(e',s) i -> 466 case TcSanity.tcExpr i e' of 467 Left err -> Left err 468 Right (s1,os) 469 | TcSanity.same s s1 -> Right os 470 | otherwise -> Left ( fromMaybe emptyRange (getLoc e') 471 , TcSanity.TypeMismatch "exprLinter" s s1 472 ) 473 , lintModule = Nothing 474 } 475 476declsLinter :: TCLinter [ T.DeclGroup ] 477declsLinter = TCLinter 478 { lintCheck = \ds' i -> case TcSanity.tcDecls i ds' of 479 Left err -> Left err 480 Right os -> Right os 481 482 , lintModule = Nothing 483 } 484 485moduleLinter :: P.ModName -> TCLinter T.Module 486moduleLinter m = TCLinter 487 { lintCheck = \m' i -> case TcSanity.tcModule i m' of 488 Left err -> Left err 489 Right os -> Right os 490 , lintModule = Just m 491 } 492 493type Act i o = i -> T.InferInput -> IO (T.InferOutput o) 494 495data TCAction i o = TCAction 496 { tcAction :: Act i o 497 , tcLinter :: TCLinter o 498 , tcPrims :: PrimMap 499 } 500 501typecheck :: 502 (Show i, Show o, HasLoc i) => TCAction i o -> i -> 503 IfaceParams -> IfaceDecls -> ModuleM o 504typecheck act i params env = do 505 506 let range = fromMaybe emptyRange (getLoc i) 507 input <- genInferInput range (tcPrims act) params env 508 out <- io (tcAction act i input) 509 510 case out of 511 512 T.InferOK nameMap warns seeds supply' o -> 513 do setNameSeeds seeds 514 setSupply supply' 515 typeCheckWarnings nameMap warns 516 menv <- getModuleEnv 517 case meCoreLint menv of 518 NoCoreLint -> return () 519 CoreLint -> case lintCheck (tcLinter act) o input of 520 Right as -> 521 let ppIt l = mapM_ (logPrint l . T.pp) 522 in withLogger ppIt as 523 Left err -> panic "Core lint failed:" [show err] 524 return o 525 526 T.InferFailed nameMap warns errs -> 527 do typeCheckWarnings nameMap warns 528 typeCheckingFailed nameMap errs 529 530-- | Generate input for the typechecker. 531genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM T.InferInput 532genInferInput r prims params env = do 533 seeds <- getNameSeeds 534 monoBinds <- getMonoBinds 535 cfg <- getSolverConfig 536 solver <- getTCSolver 537 supply <- getSupply 538 searchPath <- getSearchPath 539 callStacks <- getCallStacks 540 541 -- TODO: include the environment needed by the module 542 return T.InferInput 543 { T.inpRange = r 544 , T.inpVars = Map.map ifDeclSig (ifDecls env) 545 , T.inpTSyns = ifTySyns env 546 , T.inpNewtypes = ifNewtypes env 547 , T.inpAbstractTypes = ifAbstractTypes env 548 , T.inpNameSeeds = seeds 549 , T.inpMonoBinds = monoBinds 550 , T.inpCallStacks = callStacks 551 , T.inpSolverConfig = cfg 552 , T.inpSearchPath = searchPath 553 , T.inpSupply = supply 554 , T.inpPrimNames = prims 555 , T.inpParamTypes = ifParamTypes params 556 , T.inpParamConstraints = ifParamConstraints params 557 , T.inpParamFuns = ifParamFuns params 558 , T.inpSolver = solver 559 } 560 561 562-- Evaluation ------------------------------------------------------------------ 563 564evalExpr :: T.Expr -> ModuleM Concrete.Value 565evalExpr e = do 566 env <- getEvalEnv 567 denv <- getDynEnv 568 evopts <- getEvalOptsAction 569 let tbl = Concrete.primTable evopts 570 let ?evalPrim = \i -> Right <$> Map.lookup i tbl 571 let ?range = emptyRange 572 callStacks <- getCallStacks 573 let ?callStacks = callStacks 574 575 io $ E.runEval mempty (E.evalExpr Concrete (env <> deEnv denv) e) 576 577evalDecls :: [T.DeclGroup] -> ModuleM () 578evalDecls dgs = do 579 env <- getEvalEnv 580 denv <- getDynEnv 581 evOpts <- getEvalOptsAction 582 let env' = env <> deEnv denv 583 let tbl = Concrete.primTable evOpts 584 let ?evalPrim = \i -> Right <$> Map.lookup i tbl 585 callStacks <- getCallStacks 586 let ?callStacks = callStacks 587 588 deEnv' <- io $ E.runEval mempty (E.evalDecls Concrete dgs env') 589 let denv' = denv { deDecls = deDecls denv ++ dgs 590 , deEnv = deEnv' 591 } 592 setDynEnv denv' 593