packages feed

liquidhaskell-boot 0.9.8.2 → 0.9.10.1

raw patch · 20 files changed

+167/−69 lines, 20 filesdep +ghc-internaldep ~basedep ~ghcdep ~tasty

Dependencies added: ghc-internal

Dependency ranges changed: base, ghc, tasty, tasty-hunit, template-haskell, unordered-containers

Files

liquidhaskell-boot.cabal view
@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               liquidhaskell-boot-version:            0.9.8.2+version:            0.9.10.1 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.8.2+tested-with:        GHC == 9.10.1  extra-source-files: tests/specfiles/pos/*.spec @@ -137,13 +137,13 @@                     , filepath             >= 1.3                     , fingertree           >= 0.1                     , exceptions           < 0.11-                    , ghc                  ^>= 9.8+                    , ghc                  ^>= 9.10                     , ghc-boot                     , ghc-prim                     , gitrev                     , hashable             >= 1.3 && < 1.5                     , hscolour             >= 1.22-                    , liquid-fixpoint      == 0.9.6.3+                    , liquid-fixpoint      == 0.9.6.3.1                     , mtl                  >= 2.1                     , optparse-applicative < 0.19                     , githash@@ -169,6 +169,23 @@    if flag(devel)     ghc-options:      -Wall -Werror++test-suite wiredin-tests+  type:             exitcode-stdio-1.0+  main-is:          WiredInTests.hs+  hs-source-dirs:   tests+  build-depends:    base+                  , ghc-internal+                  , ghc-prim+                  , liquidhaskell-boot+                  , tasty+                  , tasty-ant-xml+                  , tasty-hunit+                  , template-haskell+                  , unordered-containers+  default-language: Haskell2010+  if flag(devel)+    ghc-options:      -W -Werror  test-suite ghc-api-tests   type:             exitcode-stdio-1.0
src-ghc/Liquid/GHC/API.hs view
@@ -67,6 +67,7 @@     , ModuleName     , Name     , NamedThing+    , NamespaceSpecifier (NoNamespaceSpecifier)     , ParsedModule (pm_mod_summary, pm_parsed_source)     , PredType     , RealSrcLoc@@ -163,21 +164,20 @@     , Unique     , and_RDR     , bindMName-    , dATA_FOLDABLE+    , gHC_INTERNAL_DATA_FOLDABLE     , eqClassKey     , eqClassName     , ge_RDR     , gt_RDR     , fractionalClassKey     , fractionalClassKeys-    , gHC_REAL+    , gHC_INTERNAL_REAL     , getUnique     , hasKey     , isStringClassName     , itName     , le_RDR     , lt_RDR-    , minus_RDR     , negateName     , not_RDR     , numericClassKeys
src-ghc/Liquid/GHC/API/Extra.hs view
@@ -13,6 +13,7 @@   , fsToUnitId   , isPatErrorAlt   , lookupModSummary+  , minus_RDR   , modInfoLookupNameIO   , moduleInfoTc   , parseModuleIO@@ -20,6 +21,7 @@   , relevantModules   , renderWithStyle   , showPprQualified+  , showPprDebug   , showSDocQualified   , splitDollarApp   , strictNothing@@ -35,10 +37,10 @@ import Data.Data (Data, gmapQr) import Data.Generics (extQ) import Data.Foldable                  (asum)-import Data.List                      (foldl', sortOn)+import Data.List                      (sortOn) import qualified Data.Map as Map import qualified Data.Set as S-import GHC.Builtin.Names ( dollarIdKey )+import GHC.Builtin.Names ( dollarIdKey, minusName ) import GHC.Core                       as Ghc import GHC.Core.Coercion              as Ghc import GHC.Core.DataCon               as Ghc@@ -53,6 +55,7 @@ import GHC.Driver.Session             as Ghc import GHC.Tc.Types import GHC.Types.Name                 (isSystemName, nameModule_maybe, occNameFS)+import GHC.Types.Name.Reader          (nameRdrName) import GHC.Types.SrcLoc               as Ghc import GHC.Types.TypeEnv import GHC.Types.Unique               (getUnique, hasKey)@@ -288,7 +291,18 @@ myQualify = Ghc.neverQualify { Ghc.queryQualifyName = Ghc.alwaysQualifyNames } -- { Ghc.queryQualifyName = \_ _ -> Ghc.NameNotInScope1 } +showPprDebug :: Outputable a => a -> String+showPprDebug = showSDocDebug . ppr +showSDocDebug :: Ghc.SDoc -> String+showSDocDebug = Ghc.renderWithContext ctx+  where+    style = Ghc.mkUserStyle myQualify Ghc.AllTheWay+    ctx = Ghc.defaultSDocContext {+        sdocStyle = style+      , sdocPprDebug = True+      }+ strictNothing :: GHC.Data.Strict.Maybe a strictNothing = GHC.Data.Strict.Nothing @@ -314,3 +328,6 @@ untick :: CoreExpr -> CoreExpr untick (Tick _ e) = untick e untick e = e++minus_RDR :: RdrName+minus_RDR = nameRdrName minusName
src/Language/Haskell/Liquid/Bare/Elaborate.hs view
@@ -563,7 +563,7 @@   mkHsTyConApp ::  IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs-mkHsTyConApp tyconId tyargs = nlHsTyConApp NotPromoted Prefix tyconId (map HsValArg tyargs)+mkHsTyConApp tyconId tyargs = nlHsTyConApp NotPromoted Prefix tyconId (map (HsValArg noExtField) tyargs)  -- | Embed fixpoint expressions into parsed haskell expressions. --   It allows us to bypass the GHC parser and use arbitrary symbols@@ -601,7 +601,7 @@ --   (nlHsVar (varQual_RDR dATA_FOLDABLE (fsLit "and"))) --   (nlList $ fixExprToHsExpr env <$> es) fixExprToHsExpr env (F.POr es) = mkHsApp-  (nlHsVar (varQual_RDR dATA_FOLDABLE (fsLit "or")))+  (nlHsVar (varQual_RDR gHC_INTERNAL_DATA_FOLDABLE (fsLit "or")))   (nlList $ fixExprToHsExpr env <$> es) fixExprToHsExpr env (F.PIff e0 e1) = mkHsApp   (mkHsApp (nlHsVar (mkVarUnqual (mkFastString "<=>"))) (fixExprToHsExpr env e0)@@ -623,9 +623,9 @@ constantToHsExpr :: F.Constant -> LHsExpr GhcPs -- constantToHsExpr (F.I c) = noLoc (HsLit NoExt (HsInt NoExt (mkIntegralLit c))) constantToHsExpr (F.I i) =-  noLocA (HsOverLit noAnn (mkHsIntegral (mkIntegralLit i)))+  noLocA (HsOverLit noExtField (mkHsIntegral (mkIntegralLit i))) constantToHsExpr (F.R d) =-  noLocA (HsOverLit noAnn (mkHsFractional (mkTHFractionalLit (toRational d))))+  noLocA (HsOverLit noExtField (mkHsFractional (mkTHFractionalLit (toRational d)))) constantToHsExpr _ =   todo Nothing "constantToHsExpr: Not sure how to handle constructor L" 
src/Language/Haskell/Liquid/Constraint/Monad.hs view
@@ -23,11 +23,17 @@ -------------------------------------------------------------------------------- addC :: SubC -> String -> CG () ---------------------------------------------------------------------------------addC c@(SubC γ t1 t2) _msg-  | toType False t1 /= toType False t2-  = panic (Just $ getLocation γ) $ "addC: malformed constraint:\n" ++ _msg ++ showpp t1 ++ "\n <: \n" ++ showpp t2-  | otherwise-  = modify $ \s -> s { hsCs  = c : hsCs s }+addC c@(SubC γ t1 t2) _msg =+  let tt1 = toType False t1+      tt2 = toType False t2+   in if tt1 /= tt2 then+        panic (Just $ getLocation γ) $+          "addC: malformed constraint:\n" ++ _msg ++ "\n---------\n" +++          showpp tt1 +++          "\n <: \n" +++          showpp tt2+      else+        modify $ \s -> s { hsCs  = c : hsCs s }   addC c _msg
src/Language/Haskell/Liquid/GHC/CoreToLogic.hs view
@@ -22,13 +22,13 @@   , "define Data.Set.Internal.isSubsetOf x y   = (Set_sub x y)"   , "define Data.Set.Internal.fromList xs      = (listElts xs)"   , ""-  , "define GHC.Real.fromIntegral x = (x)"+  , "define GHC.Internal.Real.fromIntegral x = (x)"   , ""   , "define GHC.Types.True                 = (true)"-  , "define GHC.Real.div x y               = (x / y)"-  , "define GHC.Real.mod x y               = (x mod y)"+  , "define GHC.Internal.Real.div x y      = (x / y)"+  , "define GHC.Internal.Real.mod x y      = (x mod y)"   , "define GHC.Classes.not x              = (~ x)"-  , "define GHC.Base.$ f x                 = (f x)"+  , "define GHC.Internal.Base.$ f x        = (f x)"   , ""   , "define Language.Haskell.Liquid.Bag.get k m   = (Map_select m k)"   , "define Language.Haskell.Liquid.Bag.put k m   = (Map_store m k (1 + (Map_select m k)))"
src/Language/Haskell/Liquid/GHC/Misc.hs view
@@ -24,6 +24,7 @@  import           Data.String import qualified Data.List as L+import           Data.Word (Word64) import           Debug.Trace  import           Prelude                                    hiding (error)@@ -104,11 +105,11 @@         name = mkInternalName (mkUnique 'x' uid) occ noSrcSpan         occ = mkVarOcc (T.unpack (symbolText sym)) -stringTyCon :: Char -> Int -> String -> TyCon+stringTyCon :: Char -> Word64 -> String -> TyCon stringTyCon = stringTyConWithKind anyTy  -- FIXME: reusing uniques like this is really dangerous-stringTyConWithKind :: Kind -> Char -> Int -> String -> TyCon+stringTyConWithKind :: Kind -> Char -> Word64 -> String -> TyCon stringTyConWithKind k c n s = Ghc.mkPrimTyCon name [] k []   where     name          = mkInternalName (mkUnique c n) occ noSrcSpan@@ -507,15 +508,15 @@   where     tailName msg = symbol . safeLast msg -splitModuleUnique :: Symbol -> (Symbol, Int)-splitModuleUnique x = (dropModuleNamesAndUnique x, base62ToI (takeModuleUnique x))+splitModuleUnique :: Symbol -> (Symbol, Word64)+splitModuleUnique x = (dropModuleNamesAndUnique x, base62ToW (takeModuleUnique x)) -base62ToI :: Symbol -> Int-base62ToI s =  fromMaybe (errorstar "base62ToI Out Of Range") $ go (F.symbolText s)+base62ToW :: Symbol -> Word64+base62ToW s =  fromMaybe (errorstar "base62ToW Out Of Range") $ go (F.symbolText s)   where-    digitToI :: OM.Map Char Int-    digitToI = OM.fromList $ zip (['0'..'9'] ++ ['a'..'z'] ++ ['A'..'Z']) [0..]-    f acc (flip OM.lookup digitToI -> x) = (acc * 62 +) <$> x+    digitToW :: OM.Map Char Word64+    digitToW = OM.fromList $ zip (['0'..'9'] ++ ['a'..'z'] ++ ['A'..'Z']) [0..]+    f acc (flip OM.lookup digitToW -> x) = (acc * 62 +) <$> x     go = foldM f 0 . T.unpack  @@ -918,7 +919,8 @@   -- undef <- lookupUndef   wiredIns <- mkWiredIns   -- snd <$> tcValBinds Ghc.NotTopLevel (binds undef wiredIns) (sigs wiredIns) m-  snd <$> tcValBinds Ghc.NotTopLevel [] (sigs wiredIns) m+  (_, _, a) <- tcValBinds Ghc.NotTopLevel [] (sigs wiredIns) m+  return a   where   -- lookupUndef = do@@ -939,7 +941,7 @@   --   ) wiredIns    sigs wiredIns = concatMap (\w ->-      let inf = maybeToList $ (\(fPrec, fDir) -> Ghc.L locSpanAnn $ Ghc.FixSig Ghc.noAnn $ Ghc.FixitySig Ghc.noExtField [Ghc.L locSpanAnn (tcWiredInName w)] $ Ghc.Fixity Ghc.NoSourceText fPrec fDir) <$> tcWiredInFixity w in+      let inf = maybeToList $ (\(fPrec, fDir) -> Ghc.L locSpanAnn $ Ghc.FixSig Ghc.noAnn $ Ghc.FixitySig Ghc.NoNamespaceSpecifier [Ghc.L locSpanAnn (tcWiredInName w)] $ Ghc.Fixity Ghc.NoSourceText fPrec fDir) <$> tcWiredInFixity w in       let t =             let ext' = [] in             [Ghc.L locSpanAnn $ TypeSig Ghc.noAnn [Ghc.L locSpanAnn (tcWiredInName w)] $ HsWC ext' $ Ghc.L locSpanAnn $ HsSig Ghc.noExtField (HsOuterImplicit ext') $ tcWiredInType w]@@ -1001,7 +1003,7 @@     return $ TcWiredIn n Nothing ty  prependGHCRealQual :: FastString -> RdrName-prependGHCRealQual = varQual_RDR gHC_REAL+prependGHCRealQual = varQual_RDR gHC_INTERNAL_REAL  isFromGHCReal :: NamedThing a => a -> Bool-isFromGHCReal x = Ghc.nameModule (Ghc.getName x) == gHC_REAL+isFromGHCReal x = Ghc.nameModule (Ghc.getName x) == gHC_INTERNAL_REAL
src/Language/Haskell/Liquid/GHC/Plugin/Types.hs view
@@ -29,7 +29,6 @@     ) where  import           Data.Binary                             as B-import           Data.Foldable import           GHC.Generics                      hiding ( moduleName )  import qualified Data.HashSet        as HS
src/Language/Haskell/Liquid/GHC/TypeRep.hs view
@@ -117,11 +117,11 @@   = AppCo (subst x tx c1) (subst x tx c2) substCoercion x tx (FunCo r afl afr cN c1 c2)   = FunCo r afl afr cN (subst x tx c1) (subst x tx c2) -- TODO(adinapoli) Is this the correct substitution?-substCoercion x tx (ForAllCo y c1 c2)+substCoercion x tx (ForAllCo y f1 f2 c1 c2)   | symbol x == symbol y -  = ForAllCo y c1 c2+  = ForAllCo y f1 f2 c1 c2   | otherwise -  = ForAllCo y (subst x tx c1) (subst x tx c2)+  = ForAllCo y f1 f2 (subst x tx c1) (subst x tx c2) substCoercion _ _ (CoVarCo y)   = CoVarCo y  substCoercion x tx (AxiomInstCo co bi cs)
src/Language/Haskell/Liquid/Parse.hs view
@@ -32,7 +32,7 @@ import           Data.Data import qualified Data.Maybe                             as Mb -- (isNothing, fromMaybe) import           Data.Char                              (isSpace, isAlphaNum)-import           Data.List                              (foldl', partition)+import           Data.List                              (partition) import           GHC                                    (ModuleName, mkModuleName) import qualified Text.PrettyPrint.HughesPJ              as PJ import           Text.PrettyPrint.HughesPJ.Compat       ((<+>))
src/Language/Haskell/Liquid/Transforms/ANF.hs view
@@ -11,6 +11,7 @@  module Language.Haskell.Liquid.Transforms.ANF (anormalize) where +import           Data.Word (Word64) import           Debug.Trace (trace) import           Prelude                          hiding (error) import           Language.Haskell.Liquid.GHC.TypeRep@@ -369,7 +370,7 @@   let sp = Sp.srcSpan (aeSrcSpan γ)   return (mkUserLocal (anfOcc i) u Ghc.ManyTy t sp) -anfOcc :: Int -> OccName+anfOcc :: Word64 -> OccName anfOcc = mkVarOccFS . GM.symbolFastString . F.intSymbol F.anfPrefix  data AnfEnv = AnfEnv
src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs view
@@ -427,9 +427,9 @@  makeApp :: Expr -> LogicMap -> Located Symbol-> [Expr] -> Expr makeApp _ _ f [e]-  | val f == symbol ("GHC.Num.negate" :: String)+  | val f == symbol ("GHC.Internal.Num.negate" :: String)   = ENeg e-  | val f == symbol ("GHC.Num.fromInteger" :: String)+  | val f == symbol ("GHC.Internal.Num.fromInteger" :: String)   , ECon c <- e   = ECon c   | (modName, sym) <- GM.splitModuleName (val f)@@ -443,7 +443,7 @@   -- Hack for typeclass support. (overriden == without Eq constraint defined at Ghci)   | (modName, sym) <- GM.splitModuleName (val f)   , symbol ("Ghci" :: String) `isPrefixOfSym` modName-  , Just op <- M.lookup (mappendSym (symbol ("GHC.Num." :: String)) sym) bops+  , Just op <- M.lookup (mappendSym (symbol ("GHC.Internal.Num." :: String)) sym) bops   = EBin op e1 e2  makeApp def lmap f es@@ -493,9 +493,9 @@                   ]   where     numSymbol :: String -> Symbol-    numSymbol =  symbol . (++) "GHC.Num."+    numSymbol =  symbol . (++) "GHC.Internal.Num."     realSymbol :: String -> Symbol-    realSymbol =  symbol . (++) "GHC.Real."+    realSymbol =  symbol . (++) "GHC.Internal.Real."  splitArgs :: Bool -> C.Expr t -> (C.Expr t, [C.Arg t]) splitArgs allowTC exprt = (exprt', reverse args)
src/Language/Haskell/Liquid/Transforms/Rec.hs view
@@ -13,6 +13,7 @@ import           Control.Monad.State import qualified Data.HashMap.Strict                  as M import           Data.Hashable+import           Data.Word (Word64) import           Liquid.GHC.API      as Ghc hiding (panic) import           Language.Haskell.Liquid.GHC.Misc import           Language.Haskell.Liquid.GHC.Play@@ -109,7 +110,7 @@  type TE = State TrEnv -data TrEnv = Tr { freshIndex  :: !Int+data TrEnv = Tr { freshIndex  :: !Word64                 , _loc        :: SrcSpan                 } @@ -235,8 +236,8 @@ class Freshable a where   fresh :: a -> TE a -instance Freshable Int where-  fresh _ = freshInt+instance Freshable Word64 where+  fresh _ = freshWord64  instance Freshable Unique where   fresh _ = freshUnique@@ -244,15 +245,15 @@ instance Freshable Var where   fresh v = fmap (setVarUnique v) freshUnique -freshInt :: MonadState TrEnv m => m Int-freshInt+freshWord64 :: MonadState TrEnv m => m Word64+freshWord64   = do s <- get        let n = freshIndex s        put s{freshIndex = n+1}        return n  freshUnique :: MonadState TrEnv m => m Unique-freshUnique = fmap (mkUnique 'X') freshInt+freshUnique = fmap (mkUnique 'X') freshWord64   mapNonRec :: (b -> [Bind b] -> [Bind b]) -> [Bind b] -> [Bind b]
src/Language/Haskell/Liquid/Types/Names.hs view
@@ -13,7 +13,7 @@  --  defined in include/GHC/Base.hs functionComposisionSymbol :: Symbol-functionComposisionSymbol = symbol ("GHC.Base.." :: String)+functionComposisionSymbol = symbol ("GHC.Internal.Base.." :: String)   selfSymbol :: Symbol
src/Language/Haskell/Liquid/Types/RefType.hs view
@@ -133,7 +133,6 @@                                                                       , text                                                                       ) import           Language.Haskell.Liquid.GHC.TypeRep () -- Eq Type instance-import Data.List (foldl')   
src/Language/Haskell/Liquid/Types/Types.hs view
@@ -285,7 +285,7 @@ import qualified Data.List                              as L import           Data.Maybe                             (mapMaybe) import           Data.Function                          (on)-import           Data.List                              as L (foldl', nub, null)+import           Data.List                              as L (nub, null) import           Data.Text                              (Text) import           Text.PrettyPrint.HughesPJ              hiding (first, (<>)) import           Text.Printf
src/Language/Haskell/Liquid/Types/Visitors.hs view
@@ -15,7 +15,7 @@  import           Data.Hashable -import           Data.List                        (foldl', (\\), delete)+import           Data.List                        ((\\), delete) import qualified Data.HashSet                     as S import           Prelude                          hiding (error) import           Language.Fixpoint.Misc
src/Language/Haskell/Liquid/UX/QuasiQuoter.hs view
@@ -16,7 +16,6 @@   where  import Data.Data-import Data.List  import qualified Data.Text as T 
src/Language/Haskell/Liquid/WiredIn.hs view
@@ -23,6 +23,7 @@         -- * Deriving classes        , isDerivedInstance+       , derivingClasses        ) where  import Prelude                                hiding (error)@@ -199,23 +200,26 @@ isDerivedInstance :: Ghc.ClsInst -> Bool -------------------------------------------------------------------------------- isDerivedInstance i = F.notracepp ("IS-DERIVED: " ++ F.showpp classSym)-                    $ S.member classSym derivingClasses+                    $ S.member classSym derivingClassesSet   where     classSym        = F.symbol . Ghc.is_cls $ i -derivingClasses :: S.HashSet F.Symbol-derivingClasses = S.fromList+derivingClassesSet :: S.HashSet F.Symbol+derivingClassesSet = S.fromList $ map F.symbol derivingClasses++derivingClasses :: [String]+derivingClasses =   [ "GHC.Classes.Eq"   , "GHC.Classes.Ord"-  , "GHC.Enum.Enum"-  , "GHC.Show.Show"-  , "GHC.Read.Read"-  , "GHC.Base.Monad"-  , "GHC.Base.Applicative"-  , "GHC.Base.Functor"-  , "Data.Foldable.Foldable"-  , "Data.Traversable.Traversable"-  , "GHC.Real.Fractional"+  , "GHC.Internal.Enum.Enum"+  , "GHC.Internal.Show.Show"+  , "GHC.Internal.Read.Read"+  , "GHC.Internal.Base.Monad"+  , "GHC.Internal.Base.Applicative"+  , "GHC.Internal.Base.Functor"+  , "GHC.Internal.Data.Foldable.Foldable"+  , "GHC.Internal.Data.Traversable.Traversable"+  , "GHC.Internal.Real.Fractional"   -- , "GHC.Enum.Bounded"   -- , "GHC.Base.Monoid"   ]
+ tests/WiredInTests.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TemplateHaskell #-}++import           Control.Monad (forM, when)+import qualified Language.Haskell.TH as TH+import qualified Language.Haskell.TH.Syntax as TH+import           Test.Tasty+import           Test.Tasty.HUnit+import           Test.Tasty.Runners.AntXML++import Language.Haskell.Liquid.WiredIn (derivingClasses)++import qualified GHC.Classes+import qualified GHC.Internal.Base+import qualified GHC.Internal.Data.Foldable+import qualified GHC.Internal.Data.Traversable+import qualified GHC.Internal.Enum+import qualified GHC.Internal.Read+import qualified GHC.Internal.Real+import qualified GHC.Internal.Show++main :: IO ()+main =+  defaultMainWithIngredients (antXMLRunner:defaultIngredients) testTree++testTree :: TestTree+testTree =+    testGroup "WiredIn names"+      [ testCase "derivingClasses" testDerivingClasses+      ]++testDerivingClasses :: IO ()+testDerivingClasses = do+    let xs = $((TH.lift . concat =<<) $ forM derivingClasses $ \s -> do+               mName <- TH.lookupTypeName s+               case mName of+                 Nothing ->+                   pure [s ++ " is not in scope"]+                 Just n ->+                   case TH.nameModule n of+                     Nothing ->+                       pure [s ++ " doesn't have a module qualifier"]+                     Just m+                       | actual == s ->+                         pure []+                       | otherwise ->+                         pure [s ++ " is defined at another place: " ++ actual]+                       where+                         actual = m ++ "." ++ TH.nameBase n+             ) :: [String]+    when (not $ null xs) $+      assertFailure $ unlines xs+