liquidhaskell-boot 0.9.2.8.0 → 0.9.4.7.0
raw patch · 22 files changed
+302/−253 lines, 22 filesdep ~Cabaldep ~ghcdep ~liquid-fixpoint
Dependency ranges changed: Cabal, ghc, liquid-fixpoint
Files
- ghc-api-tests/GhcApiTests.hs +73/−21
- liquidhaskell-boot.cabal +5/−5
- src-ghc/Liquid/GHC/API.hs +33/−19
- src-ghc/Liquid/GHC/API/Extra.hs +34/−17
- src/Language/Haskell/Liquid/Bare/Elaborate.hs +3/−2
- src/Language/Haskell/Liquid/Constraint/Generate.hs +1/−8
- src/Language/Haskell/Liquid/Constraint/Termination.hs +39/−21
- src/Language/Haskell/Liquid/GHC/Interface.hs +15/−15
- src/Language/Haskell/Liquid/GHC/Logging.hs +13/−15
- src/Language/Haskell/Liquid/GHC/Misc.hs +20/−53
- src/Language/Haskell/Liquid/GHC/Plugin.hs +14/−14
- src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs +11/−10
- src/Language/Haskell/Liquid/Termination/Structural.hs +5/−8
- src/Language/Haskell/Liquid/Transforms/ANF.hs +3/−2
- src/Language/Haskell/Liquid/Types/Errors.hs +4/−4
- src/Language/Haskell/Liquid/Types/Generics.hs +3/−18
- src/Language/Haskell/Liquid/Types/PrettyPrint.hs +6/−13
- src/Language/Haskell/Liquid/Types/RefType.hs +2/−2
- src/Language/Haskell/Liquid/Types/Specs.hs +15/−1
- src/Language/Haskell/Liquid/Types/Types.hs +2/−3
- src/Language/Haskell/Liquid/Types/Variance.hs +0/−1
- src/Language/Haskell/Liquid/UX/DiffCheck.hs +1/−1
ghc-api-tests/GhcApiTests.hs view
@@ -7,6 +7,8 @@ , Expr(..) , Alt(..) , AltCon(..)+ , LitNumType(..)+ , Literal(..) , apiCommentsParsedSource , occNameString , pAT_ERROR_ID@@ -17,15 +19,20 @@ import Test.Tasty.Runners.AntXML import qualified GHC as GHC+import qualified GHC.Builtin.Names as GHC+import qualified GHC.Builtin.Types as GHC import qualified GHC.Core as GHC import qualified GHC.Data.EnumSet as EnumSet import qualified GHC.Data.FastString as GHC import qualified GHC.Data.StringBuffer as GHC import qualified GHC.Parser as Parser import qualified GHC.Parser.Lexer as GHC-import qualified GHC.Types.Name.Occurrence as GHC+import qualified GHC.Types.Id as GHC+import qualified GHC.Types.Name as GHC import qualified GHC.Types.SrcLoc as GHC import qualified GHC.Unit.Module.ModGuts as GHC+import qualified GHC.Utils.Error as GHC+import qualified GHC.Utils.Outputable as GHC import GHC.Paths (libdir) @@ -39,6 +46,7 @@ testGroup "GHC API" [ testCase "apiComments" testApiComments , testCase "caseDesugaring" testCaseDesugaring+ , testCase "numericLiteralDesugaring" testNumLitDesugaring ] -- Tests that Liquid.GHC.API.Extra.apiComments can retrieve the comments in@@ -78,13 +86,22 @@ parseMod str filepath = do let location = GHC.mkRealSrcLoc (GHC.mkFastString filepath) 1 1 buffer = GHC.stringToStringBuffer str- popts = GHC.mkParserOpts EnumSet.empty EnumSet.empty False True True True+ popts = GHC.mkParserOpts EnumSet.empty diagOpts [] False True True True parseState = GHC.initParserState popts buffer location case GHC.unP Parser.parseModule parseState of GHC.POk _ result -> return result _ -> fail "Unexpected parser error" + diagOpts = GHC.DiagOpts+ { GHC.diag_warning_flags = EnumSet.empty+ , GHC.diag_fatal_warning_flags = EnumSet.empty+ , GHC.diag_warn_is_error = True+ , GHC.diag_reverse_errors = False+ , GHC.diag_max_errors = Nothing+ , GHC.diag_ppr_ctx = GHC.defaultSDocContext+ } + -- | Tests that case expressions desugar as Liquid Haskell expects. testCaseDesugaring :: IO () testCaseDesugaring = do@@ -121,26 +138,61 @@ -> e3 == pAT_ERROR_ID _ -> False - coreProgram <- compileToCore inputSource+ coreProgram <- compileToCore "CaseDesugaring" inputSource unless (isExpectedDesugaring coreProgram) $ fail $ unlines $ "Unexpected desugaring:" : map showPprQualified coreProgram- where- compileToCore inputSource = do- now <- getCurrentTime- GHC.runGhc (Just libdir) $ do- df1 <- GHC.getSessionDynFlags- GHC.setSessionDynFlags df1- let target = GHC.Target {- GHC.targetId = GHC.TargetFile "CaseDesugaring.hs" Nothing- , GHC.targetAllowObjCode = False- , GHC.targetContents = Just (GHC.stringToStringBuffer inputSource, now)- }- GHC.setTargets [target]- void $ GHC.load GHC.LoadAllTargets - dsMod <- GHC.getModSummary (GHC.mkModuleName "CaseDesugaring")- >>= GHC.parseModule- >>= GHC.typecheckModule- >>= GHC.desugarModule- return $ GHC.mg_binds $ GHC.dm_core_module dsMod+-- | Tests that numeric literal expressions desugar as Liquid Haskell expects.+testNumLitDesugaring :: IO ()+testNumLitDesugaring = do+ let inputSource = unlines+ [ "module NumLitDesugaring where"+ , "f :: Num a => a"+ , "f = 1"+ ]++ fBind (GHC.NonRec b _e) =+ occNameString (GHC.occName b) == "f"+ fBind _ = False++ -- Expected desugaring:+ --+ -- NumLitDesugaring.f+ -- = \@a dict -> fromInteger @a dict (GHC.Num.Integer.IS 1#)+ --+ isExpectedDesugaring p = case find fBind p of+ Just (GHC.NonRec _ e0)+ | Lam _a (Lam _dict (App fromIntegerApp (App (Var vIS) lit))) <- e0+ , App (App (Var vFromInteger) _aty) _numDict <- fromIntegerApp+ , GHC.idName vFromInteger == GHC.fromIntegerName+ , GHC.nameStableString (GHC.idName vIS) == GHC.nameStableString GHC.integerISDataConName+ , Lit (LitNumber LitNumInt 1) <- lit+ -> True+ _ -> False++ coreProgram <- compileToCore "NumLitDesugaring" inputSource+ unless (isExpectedDesugaring coreProgram) $+ fail $ unlines $+ "Unexpected desugaring:" : map showPprQualified coreProgram++compileToCore :: String -> String -> IO [GHC.CoreBind]+compileToCore modName inputSource = do+ now <- getCurrentTime+ GHC.runGhc (Just libdir) $ do+ df1 <- GHC.getSessionDynFlags+ GHC.setSessionDynFlags df1+ let target = GHC.Target {+ GHC.targetId = GHC.TargetFile (modName ++ ".hs") Nothing+ , GHC.targetUnitId = GHC.homeUnitId_ df1+ , GHC.targetAllowObjCode = False+ , GHC.targetContents = Just (GHC.stringToStringBuffer inputSource, now)+ }+ GHC.setTargets [target]+ void $ GHC.load GHC.LoadAllTargets++ dsMod <- GHC.getModSummary (GHC.mkModuleName modName)+ >>= GHC.parseModule+ >>= GHC.typecheckModule+ >>= GHC.desugarModule+ return $ GHC.mg_binds $ GHC.dm_core_module dsMod
liquidhaskell-boot.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell-boot-version: 0.9.2.8.0+version: 0.9.4.7.0 synopsis: Liquid Types for Haskell description: This package provides a plugin to verify Haskell programs. But most likely you should be using the [liquidhaskell package](https://hackage.haskell.org/package/liquidhaskell)@@ -13,7 +13,7 @@ category: Language homepage: https://github.com/ucsd-progsys/liquidhaskell build-type: Simple-tested-with: GHC == 9.2.8+tested-with: GHC == 9.4.7 data-files: include/CoreToLogic.lg syntax/liquid.css@@ -126,7 +126,7 @@ , aeson , binary , bytestring >= 0.10- , Cabal < 3.7+ , Cabal < 3.9 , cereal , cmdargs >= 0.10 , containers >= 0.5@@ -136,14 +136,14 @@ , filepath >= 1.3 , fingertree >= 0.1 , exceptions < 0.11- , ghc ^>= 9.2+ , ghc ^>= 9.4 , ghc-boot , ghc-paths >= 0.1 , ghc-prim , gitrev , hashable >= 1.3 && < 1.5 , hscolour >= 1.22- , liquid-fixpoint == 0.9.2.5+ , liquid-fixpoint == 0.9.4.7 , mtl >= 2.1 , optparse-applicative < 0.18 , githash
src-ghc/Liquid/GHC/API.hs view
@@ -59,7 +59,6 @@ , LexicalFixity(Prefix) , Located , LocatedN- , Logger , ModIface_(mi_anns, mi_exports, mi_globals, mi_module) , ModLocation(ml_hs_file) , ModSummary(ms_hspp_file, ms_hspp_opts, ms_location, ms_mod)@@ -319,7 +318,9 @@ , pAT_ERROR_ID ) import GHC.Core.Predicate as Ghc (getClassPredTys_maybe, getClassPredTys, isEvVarType, isEqPrimPred, isEqPred, isClassPred, isDictId, mkClassPred)-import GHC.Core.Subst as Ghc (deShadowBinds, emptySubst, extendCvSubst)+import GHC.Core.Reduction as Ghc+ ( Reduction(Reduction) )+import GHC.Core.Subst as Ghc (emptySubst, extendCvSubst) import GHC.Core.TyCo.Rep as Ghc ( AnonArgFlag(VisArg) , ArgFlag(Required)@@ -370,7 +371,7 @@ , isPromotedDataCon , isTupleTyCon , isVanillaAlgTyCon- , mkKindTyCon+ , mkPrimTyCon , newTyConRhs , tyConBinders , tyConDataCons_maybe@@ -420,12 +421,14 @@ , fsLit , mkFastString , mkFastStringByteString- , sLit+ , mkPtrString , uniq , unpackFS ) import GHC.Data.Pair as Ghc ( Pair(Pair) )+import GHC.Driver.Config.Diagnostic as Ghc+ ( initDiagOpts ) import GHC.Driver.Main as Ghc ( hscDesugar , hscTcRcLookupName@@ -433,8 +436,7 @@ import GHC.Driver.Phases as Ghc (Phase(StopLn)) import GHC.Driver.Pipeline as Ghc (compileFile) import GHC.Driver.Session as Ghc- ( WarnReason(NoReason)- , getDynFlags+ ( getDynFlags , gopt_set , updOptLevel , xopt_set@@ -448,6 +450,7 @@ , fromSerialized , toSerialized , defaultPlugin+ , emptyPlugins , Plugin(..) , CommandLineOption , purePlugin@@ -458,11 +461,12 @@ import GHC.Core.Opt.OccurAnal as Ghc ( occurAnalysePgm ) import GHC.Driver.Env as Ghc- ( HscEnv(hsc_EPS, hsc_HPT, hsc_dflags, hsc_plugins, hsc_static_plugins) )+ ( HscEnv(hsc_mod_graph, hsc_unit_env, hsc_dflags, hsc_plugins) )+import GHC.Driver.Errors as Ghc+ ( printMessages ) import GHC.Driver.Ppr as Ghc ( showPpr , showSDoc- , showSDocDump ) import GHC.HsToCore.Expr as Ghc ( dsLExpr )@@ -471,13 +475,14 @@ , loadInterface ) import GHC.Rename.Expr as Ghc (rnLExpr)+import GHC.Rename.Names as Ghc (renamePkgQual)+import GHC.Tc.Errors.Types as Ghc+ ( TcRnMessage(TcRnUnknownMessage) ) import GHC.Tc.Gen.App as Ghc (tcInferSigma) import GHC.Tc.Gen.Bind as Ghc (tcValBinds) import GHC.Tc.Gen.Expr as Ghc (tcInferRho) import GHC.Tc.Module as Ghc- ( getModuleInterface- , tcRnLookupRdrName- )+ ( getModuleInterface ) import GHC.Tc.Solver as Ghc ( InferMode(NoRestrictions) , captureTopConstraints@@ -503,14 +508,17 @@ , failWithTc , initIfaceTcRn , liftIO- , mkLongErrAt+ , addErrAt+ , addErrs , pushTcLevelM- , reportError- , reportErrors+ , reportDiagnostic+ , reportDiagnostics ) import GHC.Tc.Utils.TcType as Ghc (tcSplitDFunTy, tcSplitMethodTy) import GHC.Tc.Utils.Zonk as Ghc ( zonkTopLExpr )+import GHC.Types.PkgQual as Ghc+ ( PkgQual(NoPkgQual) ) import GHC.Types.Annotations as Ghc ( AnnPayload , AnnTarget(ModuleTarget)@@ -539,9 +547,12 @@ ( CostCentre(cc_loc) ) import GHC.Types.Error as Ghc- ( Messages- , DecoratedSDoc+ ( Messages(getMessages)+ , MessageClass(MCDiagnostic)+ , DiagnosticReason(WarningWithoutFlag) , MsgEnvelope(errMsgSpan)+ , errorsOrFatalWarningsFound+ , mkPlainError ) import GHC.Types.Fixity as Ghc ( Fixity(Fixity) )@@ -560,7 +571,7 @@ import GHC.Types.Id.Info as Ghc ( CafInfo(NoCafRefs) , IdDetails(DataConWorkId, DataConWrapId, RecSelId, VanillaId)- , IdInfo(occInfo, unfoldingInfo)+ , IdInfo(occInfo, realUnfoldingInfo) , cafInfo , inlinePragInfo , mayHaveCafRefs@@ -660,8 +671,11 @@ , extendVarSetList , unitVarSet )+import GHC.Unit.Env as Ghc+ ( UnitEnv(ue_eps), ue_hpt ) import GHC.Unit.External as Ghc ( ExternalPackageState (eps_ann_env)+ , ExternalUnitCache(euc_eps) ) import GHC.Unit.Finder as Ghc ( FindResult(Found, NoPackage, FoundMultiple, NotFound)@@ -693,7 +707,7 @@ , mg_usages ) )-import GHC.Utils.Error as Ghc (withTiming)-import GHC.Utils.Logger as Ghc (putLogMsg)+import GHC.Utils.Error as Ghc (pprLocMsgEnvelope, withTiming)+import GHC.Utils.Logger as Ghc (Logger(logFlags), putLogMsg) import GHC.Utils.Outputable as Ghc hiding ((<>)) import GHC.Utils.Panic as Ghc (panic, throwGhcException, throwGhcExceptionIO)
src-ghc/Liquid/GHC/API/Extra.hs view
@@ -11,18 +11,17 @@ , dataConSig , desugarModuleIO , fsToUnitId- , getDependenciesModuleNames , isPatErrorAlt , lookupModSummary , modInfoLookupNameIO , moduleInfoTc- , moduleUnitId , parseModuleIO , qualifiedNameFS , relevantModules , renderWithStyle , showPprQualified , showSDocQualified+ , strictNothing , thisPackage , tyConRealArity , typecheckModuleIO@@ -35,6 +34,7 @@ import Data.Generics (extQ) import Data.Foldable (asum) import Data.List (foldl', sortOn)+import qualified Data.Map as Map import qualified Data.Set as S import GHC.Core as Ghc import GHC.Core.Coercion as Ghc@@ -44,6 +44,7 @@ import GHC.Data.FastString as Ghc import qualified GHC.Data.EnumSet as EnumSet import GHC.Data.Maybe+import qualified GHC.Data.Strict import GHC.Driver.Env import GHC.Driver.Main import GHC.Driver.Session as Ghc@@ -54,7 +55,12 @@ import GHC.Types.Unique (getUnique) import GHC.Types.Unique.FM -import GHC.Unit.Module.Deps as Ghc (Dependencies(dep_mods))+import GHC.Unit.Module.Deps as Ghc (Dependencies(dep_direct_mods))+import GHC.Unit.Module.Graph as Ghc+ ( NodeKey(NodeKey_Module)+ , ModNodeKeyWithUid(ModNodeKeyWithUid)+ , mgTransDeps+ ) import GHC.Unit.Module.ModDetails (md_types) import GHC.Unit.Module.ModSummary (isBootSummary) import GHC.Utils.Outputable as Ghc hiding ((<>))@@ -67,9 +73,6 @@ fsToUnitId :: FastString -> UnitId fsToUnitId = toUnitId . fsToUnit -moduleUnitId :: Module -> UnitId-moduleUnitId = toUnitId . moduleUnit- thisPackage :: DynFlags -> UnitId thisPackage = homeUnitId_ @@ -83,8 +86,17 @@ Nothing -> acc Just ks -> go (acc + 1) ks -getDependenciesModuleNames :: Dependencies -> [ModuleNameWithIsBoot]-getDependenciesModuleNames = dep_mods+getDependenciesModuleNames :: ModuleGraph -> UnitId -> Dependencies -> [ModuleNameWithIsBoot]+getDependenciesModuleNames mg unitId deps =+ mapMaybe nodeKeyToModuleName $ S.toList $ S.unions $ catMaybes+ [ Map.lookup k tdeps+ | (_, m) <- S.toList $ dep_direct_mods deps+ , let k = NodeKey_Module $ ModNodeKeyWithUid m unitId+ ]+ where+ tdeps = mgTransDeps mg+ nodeKeyToModuleName (NodeKey_Module (ModNodeKeyWithUid m _)) = Just m+ nodeKeyToModuleName _ = Nothing renderWithStyle :: DynFlags -> SDoc -> PprStyle -> String renderWithStyle dynflags sdoc style = Ghc.renderWithContext (Ghc.initSDocContext dynflags style) sdoc@@ -95,13 +107,13 @@ = (dataConUnivAndExTyCoVars dc, dataConTheta dc, map irrelevantMult $ dataConOrigArgTys dc, dataConOrigResTy dc) -- | The collection of dependencies and usages modules which are relevant for liquidHaskell-relevantModules :: ModGuts -> S.Set Module-relevantModules modGuts = used `S.union` dependencies+relevantModules :: ModuleGraph -> ModGuts -> S.Set Module+relevantModules mg modGuts = used `S.union` dependencies where dependencies :: S.Set Module dependencies = S.fromList $ map (toModule . gwib_mod) . filter ((NotBoot ==) . gwib_isBoot)- . getDependenciesModuleNames $ deps+ . getDependenciesModuleNames mg thisUnitId $ deps deps :: Dependencies deps = mg_deps modGuts@@ -109,8 +121,10 @@ thisModule :: Module thisModule = mg_module modGuts + thisUnitId = moduleUnitId thisModule+ toModule :: ModuleName -> Module- toModule = unStableModule . mkStableModule (moduleUnitId thisModule)+ toModule = unStableModule . mkStableModule thisUnitId used :: S.Set Module used = S.fromList $ foldl' collectUsage mempty . mg_usages $ modGuts@@ -192,7 +206,7 @@ -- TODO: take into account anchor_op, which only matters if the source was -- pre-processed by an exact-print-aware tool.- toRealSrc (L a e) = L (RealSrcSpan (anchor a) Nothing) e+ toRealSrc (L a e) = L (RealSrcSpan (anchor a) strictNothing) e spanToLineColumn = fmap (\s -> (srcSpanStartLine s, srcSpanStartCol s)) . srcSpanToRealSrcSpan@@ -221,10 +235,9 @@ Just tyThing -> return (Just tyThing) Nothing -> lookupType hscEnv name -moduleInfoTc :: HscEnv -> ModSummary -> TcGblEnv -> IO ModuleInfoLH-moduleInfoTc hscEnv ms tcGblEnv = do- let hsc_env_tmp = hscEnv { hsc_dflags = ms_hspp_opts ms }- details <- md_types <$> liftIO (makeSimpleDetails hsc_env_tmp tcGblEnv)+moduleInfoTc :: HscEnv -> TcGblEnv -> IO ModuleInfoLH+moduleInfoTc hscEnv tcGblEnv = do+ details <- md_types <$> liftIO (makeSimpleDetails (hsc_logger hscEnv) tcGblEnv) pure ModuleInfoLH { minflh_type_env = details } -- | Tells if a case alternative calls to patError@@ -271,3 +284,7 @@ myQualify :: Ghc.PrintUnqualified myQualify = Ghc.neverQualify { Ghc.queryQualifyName = Ghc.alwaysQualifyNames } -- { Ghc.queryQualifyName = \_ _ -> Ghc.NameNotInScope1 }+++strictNothing :: GHC.Data.Strict.Maybe a+strictNothing = GHC.Data.Strict.Nothing
src/Language/Haskell/Liquid/Bare/Elaborate.hs view
@@ -568,7 +568,7 @@ mkHsTyConApp :: IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs-mkHsTyConApp tyconId tyargs = nlHsTyConApp Prefix tyconId (map HsValArg tyargs)+mkHsTyConApp tyconId tyargs = nlHsTyConApp NotPromoted Prefix tyconId (map HsValArg tyargs) -- | Embed fixpoint expressions into parsed haskell expressions. -- It allows us to bypass the GHC parser and use arbitrary symbols@@ -688,10 +688,11 @@ specTypeToLHsType = flip (ghylo (distPara @SpecType) distAna) (fmap pure . project) $ \case RVarF (RTV tv) _ -> nlHsTyVar+ NotPromoted -- (GM.notracePpr ("varRdr" ++ F.showpp (F.symbol tv)) $ getRdrName tv) (symbolToRdrNameNs tvName (F.symbol tv)) RFunF _ _ (tin, tin') (_, tout) _- | isClassType tin -> noLocA $ HsQualTy Ghc.noExtField (Just (noLocA [tin'])) tout+ | isClassType tin -> noLocA $ HsQualTy Ghc.noExtField (noLocA [tin']) tout | otherwise -> nlHsFunTy tin' tout RAllTF (ty_var_value -> (RTV tv)) (_, t) _ -> noLocA $ HsForAllTy Ghc.noExtField
src/Language/Haskell/Liquid/Constraint/Generate.hs view
@@ -14,7 +14,7 @@ -- | This module defines the representation of Subtyping and WF Constraints, -- and the code for syntax-directed constraint generation. -module Language.Haskell.Liquid.Constraint.Generate ( generateConstraints, generateConstraintsWithEnv, caseEnv, consE ) where+module Language.Haskell.Liquid.Constraint.Generate ( generateConstraints, caseEnv, consE ) where import Prelude hiding (error) import GHC.Stack ( CallStack )@@ -61,13 +61,6 @@ generateConstraints info = {-# SCC "ConsGen" #-} execState act $ initCGI cfg info where act = do { γ <- initEnv info; consAct γ cfg info }- cfg = getConfig info--generateConstraintsWithEnv :: TargetInfo -> CGInfo -> CGEnv -> CGInfo----------------------------------------------------------------------------------generateConstraintsWithEnv info cgi γ = {-# SCC "ConsGenEnv" #-} execState act cgi- where- act = consAct γ cfg info cfg = getConfig info consAct :: CGEnv -> Config -> TargetInfo -> CG ()
src/Language/Haskell/Liquid/Constraint/Termination.hs view
@@ -22,10 +22,6 @@ import Control.Applicative (liftA2) import Control.Monad.State ( gets, forM, foldM ) import Text.PrettyPrint.HughesPJ ( (<+>), text )-import GHC.Types.Var (Var)-import GHC.Types.Name (NamedThing, getSrcSpan)-import GHC.Core.TyCon (TyCon)-import GHC.Core (Bind, CoreExpr, bindersOf) import qualified Language.Haskell.Liquid.GHC.Misc as GM import qualified Language.Fixpoint.Types as F import Language.Fixpoint.Types.PrettyPrint (PPrint)@@ -40,9 +36,11 @@ toRTypeRep, structuralTerm, bkArrowDeep, mkArrow, bkUniv, bkArrow, fromRTypeRep) import Language.Haskell.Liquid.Types.RefType (isDecreasing, makeDecrType, makeLexRefa, makeNumEnv) import Language.Haskell.Liquid.Misc (safeFromLeft, replaceN, (<->), zip4, safeFromJust, fst5)+import qualified Liquid.GHC.API as GHC data TCheck = TerminationCheck | StrataCheck | NoCheck+ deriving Show mkTCheck :: Bool -> Bool -> TCheck mkTCheck tc is@@ -50,7 +48,7 @@ | tc = TerminationCheck | otherwise = NoCheck -doTermCheck :: Config -> Bind Var -> CG Bool+doTermCheck :: Config -> GHC.Bind GHC.Var -> CG Bool doTermCheck cfg bind = do lazyVs <- gets specLazy termVs <- gets specTmVars@@ -59,9 +57,9 @@ return $ chk && not skip where nocheck = if typeclass cfg then GM.isEmbeddedDictVar else GM.isInternal- xs = bindersOf bind+ xs = GHC.bindersOf bind -makeTermEnvs :: CGEnv -> [(Var, [F.Located F.Expr])] -> [(Var, CoreExpr)]+makeTermEnvs :: CGEnv -> [(GHC.Var, [F.Located F.Expr])] -> [(GHC.Var, GHC.CoreExpr)] -> [SpecType] -> [SpecType] -> [CGEnv] makeTermEnvs γ xtes xes ts ts' = setTRec γ . zip xs <$> rts@@ -78,7 +76,7 @@ rts = zipWith (addObligation OTerm) ts' <$> rss (xs, ces) = unzip xes mkSub ys ys' = F.mkSubst [(x, F.EVar y) | (x, y) <- zip ys ys']- collectArgs' = GM.collectArguments . length . ty_binds . toRTypeRep+ collectArgs' = collectArguments . length . ty_binds . toRTypeRep err x = "Constant: makeTermEnvs: no terminating expression for " ++ GM.showPpr x addObligation :: Oblig -> SpecType -> RReft -> SpecType@@ -92,7 +90,7 @@ -- | TERMINATION TYPE ---------------------------------------------------------- -------------------------------------------------------------------------------- -makeDecrIndex :: (Var, Template SpecType, [Var]) -> CG (Maybe Int)+makeDecrIndex :: (GHC.Var, Template SpecType, [GHC.Var]) -> CG (Maybe Int) makeDecrIndex (x, Assumed t, args) = do dindex <- makeDecrIndexTy x t args case dindex of@@ -105,14 +103,14 @@ Right i -> return $ Just i makeDecrIndex _ = return Nothing -makeDecrIndexTy :: Var -> SpecType -> [Var] -> CG (Either (TError t) Int)+makeDecrIndexTy :: GHC.Var -> SpecType -> [GHC.Var] -> CG (Either (TError t) Int) makeDecrIndexTy x st args = do autosz <- gets autoSize return $ case dindex autosz of Nothing -> Left msg Just i -> Right i where- msg = ErrTermin (getSrcSpan x) [F.pprint x] (text "No decreasing parameter")+ msg = ErrTermin (GHC.getSrcSpan x) [F.pprint x] (text "No decreasing parameter") trep = toRTypeRep $ unOCons st ts = ty_args trep tvs = zip ts args@@ -122,7 +120,7 @@ dindex autosz = L.findIndex (p autosz) tvs recType :: F.Symbolic a- => S.HashSet TyCon+ => S.HashSet GHC.TyCon -> (([a], Maybe Int), (t, Maybe Int, SpecType)) -> SpecType recType _ ((_, Nothing), (_, Nothing, t)) = t@@ -133,20 +131,20 @@ xts = zip (ty_binds trep) (ty_args trep) trep = toRTypeRep $ unOCons t -checkIndex :: (NamedThing t, PPrint t, PPrint a)+checkIndex :: (GHC.NamedThing t, PPrint t, PPrint a) => (t, [a], Template (RType c tv r), Maybe Int) -> CG (Maybe (RType c tv r)) checkIndex (_, _, _, Nothing ) = return Nothing checkIndex (x, vs, t, Just index) = safeLogIndex msg1 vs index >> safeLogIndex msg2 ts index where- loc = getSrcSpan x+ loc = GHC.getSrcSpan x ts = ty_args $ toRTypeRep $ unOCons $ unTemplate t msg1 = ErrTermin loc [xd] (text "No decreasing" <+> F.pprint index <-> text "-th argument on" <+> xd <+> text "with" <+> F.pprint vs) msg2 = ErrTermin loc [xd] (text "No decreasing parameter") xd = F.pprint x makeRecType :: (Enum a1, Eq a1, Num a1, F.Symbolic a)- => S.HashSet TyCon+ => S.HashSet GHC.TyCon -> SpecType -> Maybe a -> Maybe (F.Symbol, SpecType)@@ -180,8 +178,8 @@ | otherwise = return $ Just $ ls !! n -- RJ: AAAAAAARGHHH!!!!!! THIS CODE IS HORRIBLE!!!!!!!!!-consCBSizedTys :: (Bool -> CGEnv -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType)) ->- CGEnv -> [(Var, CoreExpr)] -> CG CGEnv+consCBSizedTys :: (Bool -> CGEnv -> (GHC.Var, GHC.CoreExpr, Template SpecType) -> CG (Template SpecType)) ->+ CGEnv -> [(GHC.Var, GHC.CoreExpr)] -> CG CGEnv consCBSizedTys consBind γ xes = do ts' <- forM xes $ \(x, e) -> varTemplate γ (x, Just e) autoenv <- gets autoSize@@ -200,14 +198,14 @@ allowTC = typeclass (getConfig γ) (vars, es) = unzip xes dxs = F.pprint <$> vars- collectArgs' = GM.collectArguments . length . ty_binds . toRTypeRep . unOCons . unTemplate+ collectArgs' = collectArguments . length . ty_binds . toRTypeRep . unOCons . unTemplate checkEqTypes :: [Maybe SpecType] -> CG [SpecType] checkEqTypes x = checkAllVsHead err1 toRSort (catMaybes x) err1 = ErrTermin loc dxs $ text "The decreasing parameters should be of same type" checkSameLens :: [Maybe Int] -> CG [Maybe Int] checkSameLens = checkAllVsHead err2 length err2 = ErrTermin loc dxs $ text "All Recursive functions should have the same number of decreasing parameters"- loc = getSrcSpan (head vars)+ loc = GHC.getSrcSpan (head vars) checkAllVsHead :: Eq b => Error -> (a -> b) -> [a] -> CG [a] checkAllVsHead _ _ [] = return []@@ -215,8 +213,28 @@ | all (== f x) (f <$> xs) = return (x:xs) | otherwise = addWarning err >> return [] -consCBWithExprs :: (Bool -> CGEnv -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType)) ->- CGEnv -> [(Var, CoreExpr)] -> CG CGEnv+-- See Note [Shape of normalized terms] in+-- Language.Haskell.Liquid.Transforms.ANF+collectArguments :: Int -> GHC.CoreExpr -> [GHC.Var]+collectArguments n e = take n (vs' ++ vs)+ where+ (vs', e') = collectValBinders' $ snd $ GHC.collectTyBinders e+ vs = fst $ GHC.collectBinders $ ignoreLetBinds e'++collectValBinders' :: GHC.CoreExpr -> ([GHC.Var], GHC.CoreExpr)+collectValBinders' = go []+ where+ go tvs (GHC.Lam b e) | GHC.isTyVar b = go tvs e+ go tvs (GHC.Lam b e) | GHC.isId b = go (b:tvs) e+ go tvs (GHC.Tick _ e) = go tvs e+ go tvs e = (reverse tvs, e)++ignoreLetBinds :: GHC.Expr b -> GHC.Expr b+ignoreLetBinds (GHC.Let (GHC.NonRec _ _) e') = ignoreLetBinds e'+ignoreLetBinds e = e++consCBWithExprs :: (Bool -> CGEnv -> (GHC.Var, GHC.CoreExpr, Template SpecType) -> CG (Template SpecType)) ->+ CGEnv -> [(GHC.Var, GHC.CoreExpr)] -> CG CGEnv consCBWithExprs consBind γ xes = do ts0 <- forM xes $ \(x, e) -> varTemplate γ (x, Just e) texprs <- gets termExprs
src/Language/Haskell/Liquid/GHC/Interface.hs view
@@ -122,7 +122,7 @@ f (Rec xes) = any eqFd (fst <$> xes) eqFd x = varName x == varName fd deps = concatMap unfoldDep unfolds- unfolds = unfoldingInfo . idInfo <$> concatMap bindersOf cbs'+ unfolds = realUnfoldingInfo . idInfo <$> concatMap bindersOf cbs' unfoldDep :: Unfolding -> [Id] unfoldDep (DFunUnfolding _ _ e) = concatMap exprDep e@@ -190,8 +190,8 @@ -- for this module; we will use this to create our name-resolution environment -- (see `Bare.Resolve`) ----------------------------------------------------------------------------------------lookupTyThings :: HscEnv -> ModSummary -> TcGblEnv -> IO [(Name, Maybe TyThing)]-lookupTyThings hscEnv modSum tcGblEnv = forM names (lookupTyThing hscEnv modSum tcGblEnv)+lookupTyThings :: HscEnv -> TcGblEnv -> IO [(Name, Maybe TyThing)]+lookupTyThings hscEnv tcGblEnv = forM names (lookupTyThing hscEnv tcGblEnv) where names :: [Ghc.Name] names = liftM2 (++)@@ -199,32 +199,32 @@ (fmap is_dfun_name . tcg_insts) tcGblEnv -- | Lookup a single 'Name' in the GHC environment, yielding back the 'Name' alongside the 'TyThing', -- if one is found.-lookupTyThing :: HscEnv -> ModSummary -> TcGblEnv -> Name -> IO (Name, Maybe TyThing)-lookupTyThing hscEnv modSum tcGblEnv n = do+lookupTyThing :: HscEnv -> TcGblEnv -> Name -> IO (Name, Maybe TyThing)+lookupTyThing hscEnv tcGblEnv n = do mty <- runMaybeT $ MaybeT (Ghc.hscTcRcLookupName hscEnv n) `mplus` MaybeT (- do mi <- moduleInfoTc hscEnv modSum tcGblEnv+ do mi <- moduleInfoTc hscEnv tcGblEnv modInfoLookupNameIO hscEnv mi n ) return (n, mty) -availableTyThings :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [TyThing]-availableTyThings hscEnv modSum tcGblEnv avails =+availableTyThings :: HscEnv -> TcGblEnv -> [AvailInfo] -> IO [TyThing]+availableTyThings hscEnv tcGblEnv avails = fmap catMaybes $- mapM (fmap snd . lookupTyThing hscEnv modSum tcGblEnv) $+ mapM (fmap snd . lookupTyThing hscEnv tcGblEnv) $ availableNames avails -- | Returns all the available (i.e. exported) 'TyCon's (type constructors) for the input 'Module'.-availableTyCons :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [Ghc.TyCon]-availableTyCons hscEnv modSum tcGblEnv avails =- fmap (\things -> [tyCon | (ATyCon tyCon) <- things]) (availableTyThings hscEnv modSum tcGblEnv avails)+availableTyCons :: HscEnv -> TcGblEnv -> [AvailInfo] -> IO [Ghc.TyCon]+availableTyCons hscEnv tcGblEnv avails =+ fmap (\things -> [tyCon | (ATyCon tyCon) <- things]) (availableTyThings hscEnv tcGblEnv avails) -- | Returns all the available (i.e. exported) 'Var's for the input 'Module'.-availableVars :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [Ghc.Var]-availableVars hscEnv modSum tcGblEnv avails =- fmap (\things -> [var | (AnId var) <- things]) (availableTyThings hscEnv modSum tcGblEnv avails)+availableVars :: HscEnv -> TcGblEnv -> [AvailInfo] -> IO [Ghc.Var]+availableVars hscEnv tcGblEnv avails =+ fmap (\things -> [var | (AnId var) <- things]) (availableTyThings hscEnv tcGblEnv avails) availableNames :: [AvailInfo] -> [Name] availableNames =
src/Language/Haskell/Liquid/GHC/Logging.hs view
@@ -9,10 +9,11 @@ to pay the price of a pretty-printing \"roundtrip\". -} -module Language.Haskell.Liquid.GHC.Logging (- fromPJDoc+module Language.Haskell.Liquid.GHC.Logging+ ( addTcRnUnknownMessage+ , addTcRnUnknownMessages+ , fromPJDoc , putWarnMsg- , mkLongErrAt ) where import qualified Liquid.GHC.API as GHC@@ -27,23 +28,20 @@ -- | Like the original 'putLogMsg', but internally converts the input 'Doc' (from the \"pretty\" library) -- into GHC's internal 'SDoc'. putLogMsg :: GHC.Logger- -> GHC.DynFlags- -> GHC.WarnReason -> GHC.Severity -> GHC.SrcSpan -> Maybe GHC.PprStyle -> PJ.Doc -> IO ()-putLogMsg logger dynFlags reason sev srcSpan _mbStyle =- GHC.putLogMsg logger dynFlags reason sev srcSpan . GHC.text . PJ.render+putLogMsg logger sev srcSpan _mbStyle =+ GHC.putLogMsg logger (GHC.logFlags logger) (GHC.MCDiagnostic sev GHC.WarningWithoutFlag) srcSpan . GHC.text . PJ.render -defaultErrStyle :: GHC.DynFlags -> GHC.PprStyle-defaultErrStyle _dynFlags = GHC.defaultErrStyle+putWarnMsg :: GHC.Logger -> GHC.SrcSpan -> PJ.Doc -> IO ()+putWarnMsg logger srcSpan doc =+ putLogMsg logger GHC.SevWarning srcSpan (Just GHC.defaultErrStyle) doc -putWarnMsg :: GHC.Logger -> GHC.DynFlags -> GHC.SrcSpan -> PJ.Doc -> IO ()-putWarnMsg logger dynFlags srcSpan doc =- putLogMsg logger dynFlags GHC.NoReason GHC.SevWarning srcSpan (Just $ defaultErrStyle dynFlags) doc+addTcRnUnknownMessage :: GHC.SrcSpan -> PJ.Doc -> GHC.TcRn ()+addTcRnUnknownMessage srcSpan = GHC.addErrAt srcSpan . GHC.TcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc --- | Like GHC's 'mkLongErrAt', but it builds the final 'ErrMsg' out of two \"HughesPJ\"'s 'Doc's.-mkLongErrAt :: GHC.SrcSpan -> PJ.Doc -> PJ.Doc -> GHC.TcRn (GHC.MsgEnvelope GHC.DecoratedSDoc)-mkLongErrAt srcSpan msg extra = GHC.mkLongErrAt srcSpan (fromPJDoc msg) (fromPJDoc extra)+addTcRnUnknownMessages :: [(GHC.SrcSpan, PJ.Doc)] -> GHC.TcRn ()+addTcRnUnknownMessages = GHC.addErrs . map (fmap (GHC.TcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc))
src/Language/Haskell/Liquid/GHC/Misc.hs view
@@ -28,11 +28,10 @@ import Liquid.GHC.API as Ghc hiding ( L , sourceName , showPpr- , showSDocDump , panic , showSDoc )-import qualified Liquid.GHC.API as Ghc (GenLocated (L), showSDoc, panic, showSDocDump)+import qualified Liquid.GHC.API as Ghc (GenLocated (L), showSDoc, panic) import Data.Char (isLower, isSpace, isUpper)@@ -46,7 +45,7 @@ import qualified Data.Text.Encoding as T import qualified Data.Text as T import Control.Arrow (second)-import Control.Monad ((>=>), foldM)+import Control.Monad ((>=>), foldM, when) import qualified Text.PrettyPrint.HughesPJ as PJ import Language.Fixpoint.Types hiding (L, panic, Loc (..), SrcSpan, Constant, SESearch (..)) import qualified Language.Fixpoint.Types as F@@ -74,7 +73,7 @@ tickSrcSpan :: CoreTickish -> SrcSpan tickSrcSpan (ProfNote cc _ _) = cc_loc cc-tickSrcSpan (SourceNote ss _) = RealSrcSpan ss Nothing+tickSrcSpan (SourceNote ss _) = RealSrcSpan ss strictNothing tickSrcSpan _ = noSrcSpan --------------------------------------------------------------------------------@@ -112,7 +111,7 @@ -- FIXME: reusing uniques like this is really dangerous stringTyConWithKind :: Kind -> Char -> Int -> String -> TyCon-stringTyConWithKind k c n s = Ghc.mkKindTyCon name [] k [] name+stringTyConWithKind k c n s = Ghc.mkPrimTyCon name [] k [] where name = mkInternalName (mkUnique c n) occ noSrcSpan occ = mkTcOcc s@@ -201,7 +200,7 @@ -- { Ghc.queryQualifyName = \_ _ -> Ghc.NameNotInScope1 } showSDocDump :: Ghc.SDoc -> String-showSDocDump = Ghc.showSDocDump Ghc.defaultSDocContext+showSDocDump = Ghc.renderWithContext Ghc.defaultSDocContext instance Outputable a => Outputable (S.HashSet a) where ppr = ppr . S.toList@@ -246,7 +245,7 @@ p' = srcSpanSourcePosE sp sourcePos2SrcSpan :: SourcePos -> SourcePos -> SrcSpan-sourcePos2SrcSpan p p' = RealSrcSpan (packRealSrcSpan f (unPos l) (unPos c) (unPos l') (unPos c')) Nothing+sourcePos2SrcSpan p p' = RealSrcSpan (packRealSrcSpan f (unPos l) (unPos c) (unPos l') (unPos c')) strictNothing where (f, l, c) = F.sourcePosElts p (_, l', c') = F.sourcePosElts p'@@ -327,40 +326,6 @@ namedPanic x msg = panic (Just (getSrcSpan x)) msg ----------------------------------------------------------------------------------- | Manipulating CoreExpr ----------------------------------------------------------------------------------------------------------------------------------------collectArguments :: Int -> CoreExpr -> [Var]-collectArguments n e = if length xs > n then take n xs else xs- where- (vs', e') = collectValBinders' $ snd $ collectTyBinders e- vs = fst $ collectBinders $ ignoreLetBinds e'- xs = vs' ++ vs--{--collectTyBinders :: CoreExpr -> ([Var], CoreExpr)-collectTyBinders expr- = go [] expr- where- go tvs (Lam b e) | isTyVar b = go (b:tvs) e- go tvs e = (reverse tvs, e)--}--collectValBinders' :: Ghc.Expr Var -> ([Var], Ghc.Expr Var)-collectValBinders' = go []- where- go tvs (Lam b e) | isTyVar b = go tvs e- go tvs (Lam b e) | isId b = go (b:tvs) e- go tvs (Tick _ e) = go tvs e- go tvs e = (reverse tvs, e)--ignoreLetBinds :: Ghc.Expr t -> Ghc.Expr t-ignoreLetBinds (Let (NonRec _ _) e')- = ignoreLetBinds e'-ignoreLetBinds e- = e---------------------------------------------------------------------------------- -- | Predicates on CoreExpr and DataCons --------------------------------------- -------------------------------------------------------------------------------- @@ -420,7 +385,7 @@ lookupRdrName :: HscEnv -> ModuleName -> RdrName -> IO (Maybe Name) lookupRdrName hsc_env mod_name rdr_name = do -- First find the package the module resides in by searching exposed packages and home modules- found_module <- findImportedModule hsc_env mod_name Nothing+ found_module <- findImportedModule hsc_env mod_name NoPkgQual case found_module of Found _ mod' -> do -- Find the exports of the module@@ -438,7 +403,7 @@ -- XXX [gre] -> return (Just (gre_name gre)) [] -> return Nothing _ -> Ghc.panic "lookupRdrNameInModule"- Nothing -> throwCmdLineErrorS dflags $ Ghc.hsep [Ghc.ptext (sLit "Could not determine the exports of the module"), ppr mod_name]+ Nothing -> throwCmdLineErrorS dflags $ Ghc.hsep [Ghc.ptext (Ghc.mkPtrString "Could not determine the exports of the module"), ppr mod_name] err' -> throwCmdLineErrorS dflags $ cannotFindModule hsc_env mod_name err' where dflags = hsc_dflags hsc_env throwCmdLineErrorS dflags' = throwCmdLineError . Ghc.showSDoc dflags'@@ -460,12 +425,6 @@ -- | Symbol Conversions -------------------------------------------------------- -------------------------------------------------------------------------------- -symbolTyConWithKind :: Kind -> Char -> Int -> Symbol -> TyCon-symbolTyConWithKind k x i n = stringTyConWithKind k x i (symbolString n)--symbolTyCon :: Char -> Int -> Symbol -> TyCon-symbolTyCon x i n = stringTyCon x i (symbolString n)- symbolTyVar :: Symbol -> TyVar symbolTyVar = stringTyVar . symbolString @@ -719,9 +678,6 @@ synTyConRhs_maybe :: TyCon -> Maybe Type synTyConRhs_maybe = Ghc.synTyConRhs_maybe -tcRnLookupRdrName :: HscEnv -> Ghc.LocatedN RdrName -> IO (Messages DecoratedSDoc, Maybe [Name])-tcRnLookupRdrName = Ghc.tcRnLookupRdrName- showCBs :: Bool -> [CoreBind] -> String showCBs untidy | untidy =@@ -919,7 +875,18 @@ -- Ignore the dictionary bindings evbs' <- simplifyInteractive residual full_expr <- zonkTopLExpr (mkHsDictLet (EvBinds evbs') (mkHsDictLet evbs tc_expr))- initDsTc $ dsLExpr full_expr+ (ds_msgs, me) <- initDsTc $ dsLExpr full_expr++ logger <- getLogger+ diag_opts <- initDiagOpts <$> getDynFlags+ liftIO $ printMessages logger diag_opts ds_msgs++ case me of+ Nothing -> failM+ Just e -> do+ when (errorsOrFatalWarningsFound ds_msgs)+ failM+ return e newtype HashableType = HashableType {getHType :: Type}
src/Language/Haskell/Liquid/GHC/Plugin.hs view
@@ -27,7 +27,7 @@ , filterReportErrorsWith , defaultFilterReporter , reduceFilters )-import qualified Language.Haskell.Liquid.GHC.Logging as LH (fromPJDoc)+import qualified Language.Haskell.Liquid.GHC.Logging as LH (addTcRnUnknownMessages) import Language.Haskell.Liquid.GHC.Plugin.Types import Language.Haskell.Liquid.GHC.Plugin.Util as Util@@ -127,7 +127,7 @@ liquidPluginGo summary gblEnv = do logger <- getLogger dynFlags <- getDynFlags- withTiming logger dynFlags (text "LiquidHaskell" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ do+ withTiming logger (text "LiquidHaskell" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ do if gopt Opt_Haddock dynFlags then do -- Warn the user@@ -136,7 +136,7 @@ ] let srcLoc = mkSrcLoc (mkFastString $ ms_hspp_file summary) 1 1 let warning = mkWarning (mkSrcSpan srcLoc srcLoc) msg- liftIO $ printWarning logger dynFlags warning+ liftIO $ printWarning logger warning pure gblEnv else do newGblEnv <- typecheckHook summary gblEnv@@ -229,9 +229,9 @@ -- would lead to a loop if we didn't remove the plugin when calling the type -- checker. typechecked <- liftIO $ typecheckModuleIO (dropPlugins env) (LH.ignoreInline parsed)- resolvedNames <- liftIO $ LH.lookupTyThings env modSummary tcGblEnv- availTyCons <- liftIO $ LH.availableTyCons env modSummary tcGblEnv (tcg_exports tcGblEnv)- availVars <- liftIO $ LH.availableVars env modSummary tcGblEnv (tcg_exports tcGblEnv)+ resolvedNames <- liftIO $ LH.lookupTyThings env tcGblEnv+ availTyCons <- liftIO $ LH.availableTyCons env tcGblEnv (tcg_exports tcGblEnv)+ availVars <- liftIO $ LH.availableVars env tcGblEnv (tcg_exports tcGblEnv) unoptimisedGuts <- liftIO $ desugarModuleIO env modSummary typechecked @@ -244,7 +244,7 @@ thisModule :: Module thisModule = tcg_mod tcGblEnv - dropPlugins hsc_env = hsc_env { hsc_plugins = [], hsc_static_plugins = [] }+ dropPlugins hsc_env = hsc_env { hsc_plugins = emptyPlugins } serialiseSpec :: Module -> TcGblEnv -> LiquidLib -> TcM TcGblEnv serialiseSpec thisModule tcGblEnv liquidLib = do@@ -277,8 +277,9 @@ processInputSpec :: Config -> PipelineData -> ModSummary -> TcGblEnv -> BareSpec -> TcM (Either LiquidCheckException TcGblEnv) processInputSpec cfg pipelineData modSummary tcGblEnv inputSpec = do+ hscEnv <- env_top <$> getEnv debugLog $ " Input spec: \n" ++ show inputSpec- debugLog $ "Relevant ===> \n" ++ unlines (renderModule <$> S.toList (relevantModules modGuts))+ debugLog $ "Relevant ===> \n" ++ unlines (renderModule <$> S.toList (relevantModules (hsc_mod_graph hscEnv) modGuts)) logicMap :: LogicMap <- liftIO LH.makeLogicMap @@ -291,7 +292,7 @@ , lhModuleSummary = modSummary , lhModuleTcData = pdTcData pipelineData , lhModuleGuts = pdUnoptimisedCore pipelineData- , lhRelevantModules = relevantModules modGuts+ , lhRelevantModules = relevantModules (hsc_mod_graph hscEnv) modGuts } -- liftIO $ putStrLn ("liquidHaskellCheck 6: " ++ show isIg)@@ -378,11 +379,11 @@ errorLogger :: FilePath -> [Filter] -> OutputResult -> TcM () errorLogger file filters outputResult = do LH.filterReportErrorsWith- FilterReportErrorsArgs { msgReporter = GHC.reportErrors+ FilterReportErrorsArgs { errorReporter = \errs ->+ LH.addTcRnUnknownMessages [(sp, e) | (sp, e) <- errs] , filterReporter = LH.defaultFilterReporter file , failure = GHC.failM , continue = pure ()- , pprinter = \(spn, e) -> mkLongErrAt spn (LH.fromPJDoc e) O.empty , matchingFilters = LH.reduceFilters (\(src, doc) -> PJ.render doc ++ " at " ++ LH.showPpr src) filters , filters = filters }@@ -499,7 +500,6 @@ targetSrc <- liftIO $ makeTargetSrc moduleCfg file lhModuleTcData modGuts hscEnv logger <- getLogger- dynFlags <- getDynFlags -- See https://github.com/ucsd-progsys/liquidhaskell/issues/1711 -- Due to the fact the internals can throw exceptions from pure code at any point, we need to@@ -516,10 +516,10 @@ (case result of -- Print warnings and errors, aborting the compilation. Left diagnostics -> do- liftIO $ mapM_ (printWarning logger dynFlags) (allWarnings diagnostics)+ liftIO $ mapM_ (printWarning logger) (allWarnings diagnostics) reportErrs $ allErrors diagnostics Right (warnings, targetSpec, liftedSpec) -> do- liftIO $ mapM_ (printWarning logger dynFlags) warnings+ liftIO $ mapM_ (printWarning logger) warnings let targetInfo = TargetInfo targetSrc targetSpec debugLog $ "bareSpec ==> " ++ show bareSpec
src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs view
@@ -64,14 +64,14 @@ -- ^ Any relevant module fetched during dependency-discovery. -> TcM [SpecFinderResult] findRelevantSpecs lhAssmPkgExcludes hscEnv mods = do- eps <- liftIO $ readIORef (hsc_EPS hscEnv)+ eps <- liftIO $ readIORef (euc_eps $ ue_eps $ hsc_unit_env hscEnv) foldM (loadRelevantSpec eps) mempty mods where loadRelevantSpec :: ExternalPackageState -> [SpecFinderResult] -> Module -> TcM [SpecFinderResult] loadRelevantSpec eps !acc currentModule = do res <- liftIO $ runMaybeT $- lookupInterfaceAnnotations eps (hsc_HPT hscEnv) currentModule+ lookupInterfaceAnnotations eps (ue_hpt $ hsc_unit_env hscEnv) currentModule case res of Nothing -> do mAssm <- loadModuleLHAssumptionsIfAny currentModule@@ -81,18 +81,19 @@ loadModuleLHAssumptionsIfAny m | isImportExcluded m = return Nothing | otherwise = do- let assModName = assumptionsModuleName m+ let assumptionsModName = assumptionsModuleName m -- loadInterface might mutate the EPS if the module is -- not already loaded- res <- liftIO $ findImportedModule hscEnv assModName Nothing+ res <- liftIO $ findImportedModule hscEnv assumptionsModName NoPkgQual case res of- Found _ assMod -> do- _ <- initIfaceTcRn $ loadInterface "liquidhaskell assumptions" assMod ImportBySystem+ Found _ assumptionsMod -> do+ _ <- initIfaceTcRn $ loadInterface "liquidhaskell assumptions" assumptionsMod ImportBySystem -- read the EPS again- eps2 <- liftIO $ readIORef (hsc_EPS hscEnv)+ eps2 <- liftIO $ readIORef (euc_eps $ ue_eps $ hsc_unit_env hscEnv) -- now look up the assumptions- liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 assMod- FoundMultiple{} -> failWithTc $ cannotFindModule hscEnv assModName res+ liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 assumptionsMod+ FoundMultiple{} -> failWithTc $ TcRnUnknownMessage $ mkPlainError [] $+ cannotFindModule hscEnv assumptionsModName res _ -> return Nothing isImportExcluded m =@@ -162,7 +163,7 @@ lookupLiquidBaseModule :: ModuleName -> IO (Maybe StableModule) lookupLiquidBaseModule mn = do- res <- findExposedPackageModule env mn (Just "liquidhaskell")+ res <- findImportedModule env mn (renamePkgQual (hsc_unit_env env) mn (Just "liquidhaskell")) case res of Found _ mdl -> pure $ Just (toStableModule mdl) _ -> pure Nothing
src/Language/Haskell/Liquid/Termination/Structural.hs view
@@ -23,7 +23,7 @@ import Data.Foldable (fold) terminationVars :: TargetInfo -> [Var]-terminationVars info = failingBinds info >>= allBoundVars+terminationVars info = failingBinds info >>= allLetBoundVars failingBinds :: TargetInfo -> [CoreBind] failingBinds info = filter (hasErrors . checkBind) structBinds@@ -37,13 +37,10 @@ checkBind :: CoreBind -> Result () checkBind bind = do- srcCallInfo <- getCallInfoBind emptyEnv (deShadowBind bind)+ srcCallInfo <- getCallInfoBind emptyEnv bind let structCallInfo = fmap toStructCall <$> srcCallInfo fold $ mapWithFun structDecreasing structCallInfo -deShadowBind :: CoreBind -> CoreBind-deShadowBind bind = head $ deShadowBinds [bind]- findStructBinds :: HashSet Var -> CoreProgram -> [CoreBind] findStructBinds structFuns program = filter isStructBind program where@@ -51,9 +48,9 @@ isStructBind (Rec []) = False isStructBind (Rec ((f,_):xs)) = f `HS.member` structFuns || isStructBind (Rec xs) -allBoundVars :: CoreBind -> [Var]-allBoundVars (NonRec v e) = v : (nextBinds e >>= allBoundVars)-allBoundVars (Rec binds) = map fst binds ++ (map snd binds >>= nextBinds >>= allBoundVars)+allLetBoundVars :: CoreBind -> [Var]+allLetBoundVars (NonRec v e) = v : (nextBinds e >>= allLetBoundVars)+allLetBoundVars (Rec binds) = map fst binds ++ (map snd binds >>= nextBinds >>= allLetBoundVars) nextBinds :: CoreExpr -> [CoreBind] nextBinds = \case
src/Language/Haskell/Liquid/Transforms/ANF.hs view
@@ -255,8 +255,9 @@ -- Note [Shape of normalized terms] ----- The termination checker in Termination.collectArguments expects the type--- binders to come before lets:+-- The termination checker in+-- Language.Haskell.Liquid.Constraint.Termination.collectArguments expects the+-- type binders to come before lets: -- -- > \ (@a) -> let ... in \ b c d -> ... --
src/Language/Haskell/Liquid/Types/Errors.hs view
@@ -90,7 +90,7 @@ import qualified Language.Fixpoint.Misc as Misc import qualified Language.Haskell.Liquid.Misc as Misc import Language.Haskell.Liquid.Misc ((<->))-import Language.Haskell.Liquid.Types.Generics+import Language.Haskell.Liquid.Types.Generics() type ParseError = P.ParseError String Void @@ -726,7 +726,7 @@ instance FromJSON SrcSpan where parseJSON (Object v) = do tag <- v .: "realSpan" if tag- then RealSrcSpan <$> v .: "spanInfo" <*> pure Nothing+ then RealSrcSpan <$> v .: "spanInfo" <*> pure strictNothing else return noSrcSpan parseJSON _ = mempty @@ -1082,8 +1082,8 @@ sourceErrors :: String -> SourceError -> [TError t] sourceErrors s =- concatMap errMsgErrors . bagToList . srcErrorMessages+ concatMap errMsgErrors . bagToList . getMessages . srcErrorMessages where errMsgErrors e = [ ErrGhc (errMsgSpan e) msg ] where- msg = text s $+$ nest 4 (text (show e))+ msg = text s $+$ nest 4 (text $ showSDocQualified (pprLocMsgEnvelope e))
src/Language/Haskell/Liquid/Types/Generics.hs view
@@ -1,33 +1,18 @@-{- | Geriving instances, generically.- This module shares some of the underlying ideas and implementations of the- [generic-data](https://hackage.haskell.org/package/generic-data-0.8.1.0/docs/Generic-Data.html)- package, allowing us to derive a bunch of instances using the underlying 'Generic' implementation,- but in a more declarative way.-- In particular we introduc the 'Generically' newtype wrapper to be used with '-XDerivingVia' to make- derivation explicit. For example:--@- data Foo = Foo- deriving Generic- deriving Eq via Generically Foo-@+{- | Deriving instances of Hashable and Binary, generically. -} -{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-orphans #-} -module Language.Haskell.Liquid.Types.Generics where+module Language.Haskell.Liquid.Types.Generics() where import GHC.Generics import Data.Hashable import Data.Binary import Data.Hashable.Generic import Data.Function--newtype Generically a = Generically a deriving Generic -- * 'Hashable'
src/Language/Haskell/Liquid/Types/PrettyPrint.hs view
@@ -41,7 +41,6 @@ ) where -import Control.Monad (void) import qualified Data.HashMap.Strict as M import qualified Data.List as L -- (sort) import qualified Data.Set as Set@@ -62,7 +61,7 @@ , srcSpanStartLine , srcSpanStartCol )-import Language.Haskell.Liquid.GHC.Logging (mkLongErrAt)+import Language.Haskell.Liquid.GHC.Logging import Language.Haskell.Liquid.GHC.Misc import Language.Haskell.Liquid.Misc import Language.Haskell.Liquid.Types.Types@@ -98,8 +97,6 @@ -------------------------------------------------------------------------------- -- | A whole bunch of PPrint instances follow ---------------------------------- ---------------------------------------------------------------------------------instance PPrint (Ghc.MsgEnvelope Ghc.DecoratedSDoc) where- pprintTidy _ = text . show instance PPrint SourceError where pprintTidy _ = text . show@@ -458,11 +455,11 @@ filterReportErrors :: forall e' a. (Show e', F.PPrint e') => FilePath -> Ghc.TcRn a -> Ghc.TcRn a -> [Filter] -> F.Tidy -> [TError e'] -> Ghc.TcRn a filterReportErrors path failure continue filters k = filterReportErrorsWith- FilterReportErrorsArgs { msgReporter = Ghc.reportErrors+ FilterReportErrorsArgs { errorReporter = \errs ->+ addTcRnUnknownMessages [(pos err, ppError k empty err) | err <- errs] , filterReporter = defaultFilterReporter path , failure = failure , continue = continue- , pprinter = \err -> mkLongErrAt (pos err) (ppError k empty err) mempty , matchingFilters = reduceFilters renderer filters , filters = filters }@@ -494,7 +491,7 @@ FilterReportErrorsArgs { -- | Report the @msgs@ to the monad (usually IO)- msgReporter :: [msg] -> m ()+ errorReporter :: [e] -> m () , -- | Report unmatched @filters@ to the monad filterReporter :: [filter] -> m ()@@ -505,9 +502,6 @@ -- | Continuation for when there are no unmatched errors or filters continue :: m a ,- -- | Compute a representation of the given error; does not report the error- pprinter :: e -> m msg- , -- | Yields the filters that map a given error. Must only yield -- filters in the @filters@ field. matchingFilters :: e -> [filter]@@ -533,15 +527,14 @@ filterReporter unmatchedFilters failure else do- msgs <- traverse (pprinter . fst) unmatchedErrors- void $ msgReporter msgs+ errorReporter $ map fst unmatchedErrors failure -- | Report errors via GHC's API stating the given `Filter`s did not get -- matched. Does nothing if the list of filters is empty. defaultFilterReporter :: FilePath -> [Filter] -> Ghc.TcRn () defaultFilterReporter _ [] = pure ()-defaultFilterReporter path fs = Ghc.reportError =<< mkLongErrAt srcSpan (vcat $ leaderMsg : (nest 4 <$> filterMsgs)) empty+defaultFilterReporter path fs = addTcRnUnknownMessage srcSpan (vcat $ leaderMsg : (nest 4 <$> filterMsgs)) where leaderMsg :: Doc leaderMsg = text "Could not match the following expected errors with actual thrown errors:"
src/Language/Haskell/Liquid/Types/RefType.hs view
@@ -1721,8 +1721,8 @@ -- Why do we return the strictness of the data-con arguments? -- Answer: see Note [Record evaluated-ness in worker/wrapper] deepSplitProductType fam_envs ty- | let (co, ty1) = topNormaliseType_maybe fam_envs ty- `orElse` (mkRepReflCo ty, ty)+ | let Reduction co ty1 = topNormaliseType_maybe fam_envs ty+ `orElse` Reduction (mkRepReflCo ty) ty , Just (tc, tc_args) <- splitTyConApp_maybe ty1 , Just con <- tyConSingleDataCon_maybe tc , let arg_tys = dataConInstArgTys con tc_args
src/Language/Haskell/Liquid/Types/Specs.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingVia #-}+{-# LANGUAGE StandaloneDeriving #-} {-# OPTIONS_GHC -Wno-orphans #-} @@ -76,7 +77,6 @@ import qualified Data.HashMap.Strict as M import Data.HashMap.Strict (HashMap) import Language.Haskell.Liquid.Types.Types-import Language.Haskell.Liquid.Types.Generics import Language.Haskell.Liquid.Types.Variance import Language.Haskell.Liquid.Types.Bounds import Liquid.GHC.API hiding (text, (<+>))@@ -198,6 +198,7 @@ , gsImps :: ![(F.Symbol, F.Sort)] -- ^ Imported Environment , gsConfig :: !Config }+ deriving Show instance HasConfig TargetSpec where getConfig = gsConfig@@ -209,6 +210,7 @@ , gsLvars :: !(S.HashSet Var) -- ^ Variables that should be checked "lazily" in the environment they are used , gsCMethods :: ![Var] -- ^ Refined Class methods }+ deriving Show instance Semigroup GhcSpecVars where sv1 <> sv2 = SpVar@@ -225,6 +227,7 @@ { gsQualifiers :: ![F.Qualifier] -- ^ Qualifiers in Source/Spec files e.g tests/pos/qualTest.hs , gsRTAliases :: ![F.Located SpecRTAlias] -- ^ Refinement type aliases (only used for qualifiers) }+ deriving Show data GhcSpecSig = SpSig { gsTySigs :: ![(Var, LocSpecType)] -- ^ Asserted Reftypes@@ -238,6 +241,7 @@ , gsRelation :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)] , gsAsmRel :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)] }+ deriving Show instance Semigroup GhcSpecSig where x <> y = SpSig@@ -270,6 +274,8 @@ , gsMeasures :: ![Measure SpecType DataCon] -- ^ Measure definitions , gsUnsorted :: ![UnSortedExpr] }+ deriving Show+ data GhcSpecNames = SpNames { gsFreeSyms :: ![(F.Symbol, Var)] -- ^ List of `Symbol` free in spec and corresponding GHC var, eg. (Cons, Cons#7uz) from tests/pos/ex1.hs , gsDconsP :: ![F.Located DataCon] -- ^ Predicated Data-Constructors, e.g. see tests/pos/Map.hs@@ -278,7 +284,11 @@ , gsADTs :: ![F.DataDecl] -- ^ ADTs extracted from Haskell 'data' definitions , gsTyconEnv :: !TyConMap }+ deriving Show +deriving instance Show TyConP+deriving instance Show TyConMap+ data GhcSpecTerm = SpTerm { gsStTerm :: !(S.HashSet Var) -- ^ Binders to CHECK by structural termination , gsAutosize :: !(S.HashSet TyCon) -- ^ Binders to IGNORE during termination checking@@ -286,6 +296,7 @@ , gsFail :: !(S.HashSet (F.Located Var)) -- ^ Binders to fail type checking , gsNonStTerm :: !(S.HashSet Var) -- ^ Binders to CHECK using REFINEMENT-TYPES/termination metrics }+ deriving Show instance Semigroup GhcSpecTerm where t1 <> t2 = SpTerm@@ -309,6 +320,7 @@ , gsRewrites :: S.HashSet (F.Located Var) , gsRewritesWith :: M.HashMap Var [Var] }+ deriving Show instance Semigroup GhcSpecRefl where x <> y = SpRefl@@ -331,6 +343,7 @@ { gsLawDefs :: ![(Class, [(Var, LocSpecType)])] , gsLawInst :: ![LawInstance] }+ deriving Show data LawInstance = LawInstance { lilName :: Class@@ -339,6 +352,7 @@ , lilEqus :: [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))] , lilPos :: SrcSpan }+ deriving Show type VarOrLocSymbol = Either Var LocSymbol type BareMeasure = Measure LocBareType F.LocSymbol
src/Language/Haskell/Liquid/Types/Types.hs view
@@ -293,7 +293,6 @@ import qualified Language.Fixpoint.Types as F -import Language.Haskell.Liquid.Types.Generics import Language.Haskell.Liquid.GHC.Misc import Language.Haskell.Liquid.GHC.Logging as GHC import Language.Haskell.Liquid.Types.Variance@@ -1996,8 +1995,8 @@ -- | Printing Warnings --------------------------------------------------------- -------------------------------------------------------------------------------- -printWarning :: Logger -> DynFlags -> Warning -> IO ()-printWarning logger dyn (Warning srcSpan doc) = GHC.putWarnMsg logger dyn srcSpan doc+printWarning :: Logger -> Warning -> IO ()+printWarning logger (Warning srcSpan doc) = GHC.putWarnMsg logger srcSpan doc -------------------------------------------------------------------------------- -- | Error Data Type -----------------------------------------------------------
src/Language/Haskell/Liquid/Types/Variance.hs view
@@ -24,7 +24,6 @@ import qualified Language.Fixpoint.Types as F -import Language.Haskell.Liquid.Types.Generics import qualified Language.Haskell.Liquid.GHC.Misc as GM import Liquid.GHC.API as Ghc hiding (text)
src/Language/Haskell/Liquid/UX/DiffCheck.hs view
@@ -540,7 +540,7 @@ isCheckedRealSpan cm = not . null . (`IM.search` cm) . srcSpanStartLine adjustSpan :: LMap -> SrcSpan -> Maybe SrcSpan-adjustSpan lm (RealSrcSpan rsp _) = RealSrcSpan <$> adjustReal lm rsp <*> pure Nothing+adjustSpan lm (RealSrcSpan rsp _) = RealSrcSpan <$> adjustReal lm rsp <*> pure strictNothing adjustSpan _ sp = Just sp adjustReal :: LMap -> RealSrcSpan -> Maybe RealSrcSpan