Merge pull request #2441 from ucsd-progsys/fd/refactorings

Various small refactorings

liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs

@@ -670,6 +670,7 @@ import GHC.Types.Name.Reader          as Ghc
     , getRdrName
     , globalRdrEnvElts
     , greName
+    , isLocalGRE
     , lookupGRE
     , lookupGRE_Name
     , mkQual

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs

@@ -16,24 +16,17 @@ module Language.Haskell.Liquid.Bare (
   -- * Creating a TargetSpec
   -- $creatingTargetSpecs
     makeTargetSpec
-
-  -- * Loading and Saving lifted specs from/to disk
-  , loadLiftedSpec
-  , saveLiftedSpec
   ) where
 
 import           Control.Monad                              (forM, mplus, when)
 import qualified Control.Exception                          as Ex
-import qualified Data.Binary                                as B
 import           Data.IORef (newIORef)
 import qualified Data.Maybe                                 as Mb
 import qualified Data.List                                  as L
 import qualified Data.HashMap.Strict                        as M
 import qualified Data.HashSet                               as S
 import           Text.PrettyPrint.HughesPJ                  hiding (first, (<>)) -- (text, (<+>))
 import           System.FilePath                            (dropExtension)
-import           System.Directory                           (doesFileExist)
-import           System.Console.CmdArgs.Verbosity           (whenLoud)
 import           Language.Fixpoint.Utils.Files              as Files
 import           Language.Fixpoint.Misc                     as Misc
 import           Language.Fixpoint.Types                    hiding (dcFields, DataDecl, Error, panic)
@@ -71,35 +64,6 @@ import Data.Hashable (Hashable)
 import Data.Bifunctor (bimap, first)
 import Data.Function (on)
 
---------------------------------------------------------------------------------
--- | De/Serializing Spec files
---------------------------------------------------------------------------------
-
-loadLiftedSpec :: Config -> FilePath -> IO (Maybe Ms.BareSpec)
-loadLiftedSpec cfg srcF
-  | noLiftedImport cfg = putStrLn "No LIFTED Import" >> return Nothing
-  | otherwise          = do
-      let specF = extFileName BinSpec srcF
-      ex  <- doesFileExist specF
-      whenLoud $ putStrLn $ "Loading Binary Lifted Spec: " ++ specF ++ " " ++ "for source-file: " ++ show srcF ++ " " ++ show ex
-      lSp <- if ex
-               then Just <$> B.decodeFile specF
-               else {- warnMissingLiftedSpec srcF specF >> -} return Nothing
-      Ex.evaluate lSp
-
--- warnMissingLiftedSpec :: FilePath -> FilePath -> IO ()
--- warnMissingLiftedSpec srcF specF = do
---   incDir <- Misc.getIncludeDir
---   unless (Misc.isIncludeFile incDir srcF)
---     $ Ex.throw (errMissingSpec srcF specF)
-
-saveLiftedSpec :: FilePath -> Ms.BareSpec -> IO ()
-saveLiftedSpec srcF lspec = do
-  ensurePath specF
-  B.encodeFile specF lspec
-  -- print (errorP "DIE" "HERE" :: String)
-  where
-    specF = extFileName BinSpec srcF
 
 {- $creatingTargetSpecs
 
@@ -128,43 +92,15 @@ makeTargetSpec :: Config
 makeTargetSpec cfg localVars lmap targetSrc bareSpec dependencies = do
   let targDiagnostics     = Bare.checkTargetSrc cfg targetSrc
   let depsDiagnostics     = mapM (Bare.checkBareSpec . snd) legacyDependencies
-  let bareSpecDiagnostics = Bare.checkBareSpec legacyBareSpec
+  let bareSpecDiagnostics = Bare.checkBareSpec bareSpec
   case targDiagnostics >> depsDiagnostics >> bareSpecDiagnostics of
    Left d | noErrors d -> secondPhase (allWarnings d)
    Left d              -> return $ Left d
    Right ()            -> secondPhase mempty
   where
     secondPhase :: [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
     secondPhase phaseOneWarns = do
-
-      -- we should be able to setContext regardless of whether
-      -- we use the ghc api. However, ghc will complain
-      -- if the filename does not match the module name
-      -- when (typeclass cfg) $ do
-      --   Ghc.setContext [iimport |(modName, _) <- allSpecs legacyBareSpec,
-      --                   let iimport = if isTarget modName
-      --                                 then Ghc.IIModule (getModName modName)
-      --                                 else Ghc.IIDecl (Ghc.simpleImportDecl (getModName modName))]
-      --   void $ Ghc.execStmt
-      --     "let {infixr 1 ==>; True ==> False = False; _ ==> _ = True}"
-      --     Ghc.execOptions
-      --   void $ Ghc.execStmt
-      --     "let {infixr 1 <=>; True <=> False = False; _ <=> _ = True}"
-      --     Ghc.execOptions
-      --   void $ Ghc.execStmt
-      --     "let {infix 4 ==; (==) :: a -> a -> Bool; _ == _ = undefined}"
-      --     Ghc.execOptions
-      --   void $ Ghc.execStmt
-      --     "let {infix 4 /=; (/=) :: a -> a -> Bool; _ /= _ = undefined}"
-      --     Ghc.execOptions
-      --   void $ Ghc.execStmt
-      --     "let {infixl 7 /; (/) :: Num a => a -> a -> a; _ / _ = undefined}"
-      --     Ghc.execOptions
-      --   void $ Ghc.execStmt
-      --     "let {len :: [a] -> Int; len _ = undefined}"
-      --     Ghc.execOptions
-
-      diagOrSpec <- makeGhcSpec cfg localVars (fromTargetSrc targetSrc) lmap legacyBareSpec legacyDependencies
+      diagOrSpec <- makeGhcSpec cfg localVars (fromTargetSrc targetSrc) lmap bareSpec legacyDependencies
       case diagOrSpec of
         Left d -> return $ Left d
         Right (warns, ghcSpec) -> do
@@ -178,9 +114,6 @@ makeTargetSpec cfg localVars lmap targetSrc bareSpec dependencies = do
     legacyDependencies :: [(ModName, Ms.BareSpec)]
     legacyDependencies = map toLegacyDep . M.toList . getDependencies $ dependencies
 
-    legacyBareSpec :: Ms.BareSpec
-    legacyBareSpec = fromBareSpec bareSpec
-
     -- Assumptions about local functions that are not exported aren't useful for
     -- other modules.
     removeUnexportedLocalAssumptions :: LiftedSpec -> Ghc.TcRn LiftedSpec
@@ -329,6 +262,9 @@ makeGhcSpec0 cfg session tcg instEnvs localVars src lmap targetSpec dependencySp
                 , rinstance = specInstances
                   -- Preserve rinstances.
                 , asmReflectSigs = Ms.asmReflectSigs mySpec
+                , reflects = Ms.reflects mySpec0
+                , cmeasures = Ms.cmeasures targetSpec
+                , embeds = Ms.embeds targetSpec
                 }
     })
   where
@@ -434,16 +370,7 @@ makeLiftedSpec0 :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareS
                 -> Ms.BareSpec
 makeLiftedSpec0 cfg src embs lmap mySpec = mempty
   { Ms.ealiases  = lmapEAlias . snd <$> Bare.makeHaskellInlines (typeclass cfg) src embs lmap mySpec
-  , Ms.reflects  = Ms.reflects mySpec
   , Ms.dataDecls = Bare.makeHaskellDataDecls cfg name mySpec tcs
-  , Ms.embeds    = Ms.embeds mySpec
-  -- We do want 'embeds' to survive and to be present into the final 'LiftedSpec'. The
-  -- caveat is to decide which format is more appropriate. We obviously cannot store
-  -- them as a 'TCEmb TyCon' as serialising a 'TyCon' would be fairly exponsive. This
-  -- needs more thinking.
-  , Ms.cmeasures = Ms.cmeasures mySpec
-  -- We do want 'cmeasures' to survive and to be present into the final 'LiftedSpec'. The
-  -- caveat is to decide which format is more appropriate. This needs more thinking.
   }
   where
     tcs          = uniqNub (_gsTcs src ++ refTcs)
@@ -549,7 +476,7 @@ makeSpecQual _cfg env tycEnv measEnv _rtEnv specs = SpQual
                    ++ (fst <$> Bare.meSyms measEnv)
                    ++ (fst <$> Bare.meClassSyms measEnv)
 
-makeQualifiers :: Bare.Env -> Bare.TycEnv -> (ModName, Ms.Spec ty bndr) -> [F.Qualifier]
+makeQualifiers :: Bare.Env -> Bare.TycEnv -> (ModName, Ms.Spec ty) -> [F.Qualifier]
 makeQualifiers env tycEnv (modn, spec)
   = fmap        (Bare.qualifyTopDummy env        modn)
   . Mb.mapMaybe (resolveQParams       env tycEnv modn)
@@ -647,7 +574,7 @@ makeRewrite env spec =
 makeRewriteWith :: Bare.Env -> Ms.BareSpec -> Bare.Lookup (M.HashMap Ghc.Var [Ghc.Var])
 makeRewriteWith env spec = M.fromList <$> makeRewriteWith' env spec
 
-makeRewriteWith' :: Bare.Env -> Spec ty bndr -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
+makeRewriteWith' :: Bare.Env -> Spec ty -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
 makeRewriteWith' env spec =
   forM (M.toList $ Ms.rewriteWith spec) $ \(x, xs) -> do
     xv  <- Bare.lookupGhcIdLHName env x

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs

@@ -1054,11 +1054,7 @@ addSymSort _ _ _ t
   = t
 
 addSymSortRef :: (PPrint s) => Ghc.SrcSpan -> s -> RPVar -> SpecProp -> Int -> SpecProp
-addSymSortRef sp rc p r i
-  | isPropPV p
-  = addSymSortRef' sp rc i p r
-  | otherwise
-  = panic Nothing "addSymSortRef: malformed ref application"
+addSymSortRef sp rc p r i = addSymSortRef' sp rc i p r
 
 addSymSortRef' :: (PPrint s) => Ghc.SrcSpan -> s -> Int -> RPVar -> SpecProp -> SpecProp
 addSymSortRef' _ _ _ p (RProp s (RVar v r)) | isDummy v

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/ToBare.hs

@@ -85,5 +85,5 @@ txPV :: (c1 -> c2) -> (tv1 -> tv2) -> PVU c1 tv1 -> PVU c2 tv2
 txPV cF vF (PV sym k y txes) = PV sym k' y txes'
   where
     txes'                  = [ (tx t, x, e) | (t, x, e) <- txes]
-    k'                     = tx <$> k
+    k'                     = tx k
     tx                     = txRType cF vF

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs

@@ -976,18 +976,14 @@ varAnn γ x t
 -- | Helpers: Creating Fresh Refinement -------------------------------
 -----------------------------------------------------------------------
 freshPredRef :: CGEnv -> CoreExpr -> PVar RSort -> CG SpecProp
-freshPredRef γ e (PV _ (PVProp rsort) _ as)
+freshPredRef γ e (PV _ rsort _ as)
   = do t    <- freshTyType (typeclass (getConfig γ))  PredInstE e (toType False rsort)
        args <- mapM (const fresh) as
        let targs = [(x, s) | (x, (s, y, z)) <- zip args as, F.EVar y == z ]
        γ' <- foldM (+=) γ [("freshPredRef", x, ofRSort τ) | (x, τ) <- targs]
        addW $ WfC γ' t
        return $ RProp targs t
 
-freshPredRef _ _ (PV _ PVHProp _ _)
-  = todo Nothing "EFFECTS:freshPredRef"
-
-
 --------------------------------------------------------------------------------
 -- | Helpers: Creating Refinement Types For Various Things ---------------------
 --------------------------------------------------------------------------------

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs

@@ -22,7 +22,7 @@ import qualified Language.Fixpoint.Types                 as F
 import qualified  Language.Haskell.Liquid.GHC.Misc        as LH
 import qualified Language.Haskell.Liquid.UX.CmdLine      as LH
 import qualified Language.Haskell.Liquid.GHC.Interface   as LH
-import           Language.Haskell.Liquid.LHNameResolution (collectTypeAliases, resolveLHNames)
+import           Language.Haskell.Liquid.LHNameResolution (resolveLHNames)
 import qualified Language.Haskell.Liquid.Liquid          as LH
 import qualified Language.Haskell.Liquid.Types.PrettyPrint as LH ( filterReportErrors
                                                                  , filterReportErrorsWith
@@ -400,7 +400,7 @@ liquidHaskellCheckWithConfig
   :: Config -> PipelineData -> ModSummary -> TcM (Either LiquidCheckException LiquidLib)
 liquidHaskellCheckWithConfig cfg pipelineData modSummary = do
   -- Parse the spec comments stored in the pipeline data.
-  let inputSpec = toBareSpec . snd $
+  let inputSpec = snd $
         hsSpecificationP (moduleName thisModule) (pdSpecComments pipelineData)
 
   processInputSpec cfg pipelineData modSummary inputSpec
@@ -430,7 +430,7 @@ checkLiquidHaskellContext lhContext = do
       let bareSpec = lhInputSpec lhContext
           file = LH.modSummaryHsFile $ lhModuleSummary lhContext
 
-      withPragmas (lhGlobalCfg lhContext) file (Ms.pragmas $ fromBareSpec bareSpec) $ \moduleCfg ->  do
+      withPragmas (lhGlobalCfg lhContext) file (Ms.pragmas bareSpec) $ \moduleCfg ->  do
         let filters = getFilters moduleCfg
         -- Report the outcome of the checking
         LH.reportResult (errorLogger file filters) moduleCfg [giTarget (giSrc pmrTargetInfo)] out
@@ -458,7 +458,7 @@ errorLogger file filters outputResult = do
     (LH.orMessages outputResult)
 
 isIgnore :: BareSpec -> Bool
-isIgnore (MkBareSpec sp) = any ((== "--skip-module") . F.val) (pragmas sp)
+isIgnore sp = any ((== "--skip-module") . F.val) (pragmas sp)
 
 --------------------------------------------------------------------------------
 -- | Working with bare & lifted specs ------------------------------------------
@@ -521,9 +521,9 @@ processModule LiquidHaskellContext{..} = do
   -- (cfr. 'allowExtResolution').
   let file            = LH.modSummaryHsFile lhModuleSummary
 
-  _                   <- liftIO $ LH.checkFilePragmas $ Ms.pragmas (fromBareSpec bareSpec0)
+  _                   <- liftIO $ LH.checkFilePragmas $ Ms.pragmas bareSpec0
 
-  withPragmas lhGlobalCfg file (Ms.pragmas $ fromBareSpec bareSpec0) $ \moduleCfg -> do
+  withPragmas lhGlobalCfg file (Ms.pragmas bareSpec0) $ \moduleCfg -> do
     dependencies <- loadDependencies moduleCfg (S.toList lhRelevantModules)
 
     debugLog $ "Found " <> show (HM.size $ getDependencies dependencies) <> " dependencies:"
@@ -544,13 +544,13 @@ processModule LiquidHaskellContext{..} = do
     -- call 'evaluate' to force any exception and catch it, if we can.
 
     tcg <- getGblEnv
-    let rtAliases = collectTypeAliases thisModule bareSpec0 (HM.toList $ getDependencies dependencies)
-        localVars = makeLocalVars preNormalizedCore
+    let localVars = makeLocalVars preNormalizedCore
         eBareSpec = resolveLHNames
+          thisModule
           localVars
-          rtAliases
           (tcg_rdr_env tcg)
           bareSpec0
+          dependencies
     result <-
       case eBareSpec of
         Left errors -> pure $ Left $ mkDiagnostics [] errors