diff --git a/README.md b/README.md index 7322c6ad23..fe7cd5c5cd 100644 --- a/README.md +++ b/README.md @@ -339,33 +339,17 @@ patter synonym to deal with changes in type constructors. Currently, no. Only one version of GHC is supported and that is the one that can be tested with `./scripts/test/test_plugin.sh`. -# GHC Plugin Development FAQs - -## Why is the GHC.Interface using slightly different types than the GHC.Plugin module? - -Mostly for backward-compatibility and for historical reasons. Types like [BareSpec][] used to be type alias -rather than `newtype`s, and things were slightly renamed to reflect better purpose when the support for the -plugin was added. While doing so we also added a compatibility layer in the form of some `optics` that can be used -to map back and forth (sometimes in a partial way) between old and new data structures. When in doubt, -**consider the GHC.Plugin as the single source of truth, and prefer whichever data structure the latter is -using**. - [GHC.API]: liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs [Plugin]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs [GHC.Plugin]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs [GHC.Interface]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs [SpecFinder]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs -[BareSpec]: liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L362 [LiftedSpec]: liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L559 [TargetSrc]: liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L158 -[Ghc monad]: https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:Ghc -[HscEnv]: https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:HscEnv -[DynFlags]: https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:DynFlags -[GhcMonad]: https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:GhcMonad [typechecking phase]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L211-L226 [ghcide]: https://github.com/haskell/ghcide [findRelevantSpecs]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs#L65 -[core binds]: https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC-Core.html#t:CoreBind +[core binds]: https://hackage.haskell.org/package/ghc-9.4.7/docs/GHC-Core.html#t:CoreBind [configureGhcTargets]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L254 [processTargetModule]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L483 [processModule]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L509 diff --git a/docs/mkDocs/docs/install.md b/docs/mkDocs/docs/install.md index 5fefbd3d76..4ea62eeb72 100644 --- a/docs/mkDocs/docs/install.md +++ b/docs/mkDocs/docs/install.md @@ -19,7 +19,8 @@ LiquidHaskell itself is installed&enabled by adding it as a dependency in your p Depending on your version of GHC, you might want to use a build of LiquidHaskell from github or from Hackage. -* `ghc-9.2.8`: use LiquidHaskell from github +* `ghc-9.4.7`: use LiquidHaskell from github +* `ghc-9.2.8`: use liquidhaskell-0.9.2.8.0 from Hackage * `ghc-9.2.5`: use liquidhaskell-0.9.2.5.0 from Hackage * `ghc-9.0.2`: use liquidhaskell-0.9.0.2.1 and liquid-base-0.4.15.1.0 from Hackage * `ghc-8.10.7`: use liquidhaskell-0.8.10.7 and liquid-base-0.4.15.0.0 from Hackage diff --git a/liquid-fixpoint b/liquid-fixpoint index 1ccf4b3962..c253dc1932 160000 --- a/liquid-fixpoint +++ b/liquid-fixpoint @@ -1 +1 @@ -Subproject commit 1ccf4b3962b4c3a3f4c17537280ec70edfa85c3e +Subproject commit c253dc1932f06ed64fcc62d356f30256abaf83cd diff --git a/liquid-platform/liquid-platform.cabal b/liquid-platform/liquid-platform.cabal index 2072e6b410..32266de259 100644 --- a/liquid-platform/liquid-platform.cabal +++ b/liquid-platform/liquid-platform.cabal @@ -28,7 +28,7 @@ executable liquidhaskell build-depends: base >= 4.15.1.0 && < 5 , containers >= 0.6.4.1 && < 0.7 , liquid-prelude >= 0.9.2.8 - , liquid-vector >= 0.12.3.1.2 + , liquid-vector >= 0.13.1.0 , liquidhaskell >= 0.9.2.8 , liquidhaskell-boot >= 0.9.2.8 , filepath diff --git a/liquid-vector/liquid-vector.cabal b/liquid-vector/liquid-vector.cabal index 931eaa1a3f..0284b32ada 100644 --- a/liquid-vector/liquid-vector.cabal +++ b/liquid-vector/liquid-vector.cabal @@ -1,6 +1,6 @@ cabal-version: 1.24 name: liquid-vector -version: 0.12.3.1.2 +version: 0.13.1.0 synopsis: LiquidHaskell specs for the vector package description: LiquidHaskell specs for the vector package. license: BSD3 @@ -19,7 +19,7 @@ library exposed-modules: Data.Vector_LHAssumptions hs-source-dirs: src build-depends: base < 5 - , vector >= 0.12.3.1 && < 0.14 + , vector >= 0.13.1.0 && < 0.14 , liquidhaskell >= 0.9.2.8 default-language: Haskell2010 default-extensions: PackageImports diff --git a/liquidhaskell-boot/ghc-api-tests/GhcApiTests.hs b/liquidhaskell-boot/ghc-api-tests/GhcApiTests.hs index e7f8777036..a6146c3341 100644 --- a/liquidhaskell-boot/ghc-api-tests/GhcApiTests.hs +++ b/liquidhaskell-boot/ghc-api-tests/GhcApiTests.hs @@ -7,6 +7,8 @@ import Liquid.GHC.API , Expr(..) , Alt(..) , AltCon(..) + , LitNumType(..) + , Literal(..) , apiCommentsParsedSource , occNameString , pAT_ERROR_ID @@ -17,13 +19,16 @@ import Test.Tasty.HUnit 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 @@ -41,6 +46,7 @@ testTree = testGroup "GHC API" [ testCase "apiComments" testApiComments , testCase "caseDesugaring" testCaseDesugaring + , testCase "numericLiteralDesugaring" testNumLitDesugaring ] -- Tests that Liquid.GHC.API.Extra.apiComments can retrieve the comments in @@ -132,27 +138,61 @@ testCaseDesugaring = do -> 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.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 "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 diff --git a/stack.yaml b/stack.yaml index ba47bca9fa..1fee9bb10c 100644 --- a/stack.yaml +++ b/stack.yaml @@ -27,7 +27,6 @@ extra-deps: - smtlib-backends-process-0.3 - git: https://github.com/qnikst/ghc-timings-report commit: 45ef3498e35897712bde8e002ce18df6d55f8b15 -- vector-0.12.3.1 # for tests - strip-ansi-escape-0.1.0.0@sha256:08f2ed93b16086a837ec46eab7ce8d27cf39d47783caaeb818878ea33c2ff75f,1628 diff --git a/stack.yaml.lock b/stack.yaml.lock index 79704e5ccb..f4854060a5 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -36,13 +36,6 @@ packages: original: commit: 45ef3498e35897712bde8e002ce18df6d55f8b15 git: https://github.com/qnikst/ghc-timings-report -- completed: - hackage: vector-0.12.3.1@sha256:39141f312871b7c793a63be76635999e84d442aa3290aec59f30638ec0bf23a7,8218 - pantry-tree: - sha256: c4f50de0598ce416df3a8f01ad7f23d8f1282ef3c5c531d67afe15b1e14a5d8d - size: 3842 - original: - hackage: vector-0.12.3.1 - completed: hackage: strip-ansi-escape-0.1.0.0@sha256:08f2ed93b16086a837ec46eab7ce8d27cf39d47783caaeb818878ea33c2ff75f,1628 pantry-tree: diff --git a/tests/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/Optimal.hs b/tests/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/Optimal.hs index d9b4fba70e..c794b4aa54 100644 --- a/tests/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/Optimal.hs +++ b/tests/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/Optimal.hs @@ -66,8 +66,8 @@ sort2ByOffset cmp a off = sort2ByIndex cmp a off (off + 1) @-} sort2ByIndex :: (PrimMonad m, MVector v e) => Comparison e -> v (PrimState m) e -> Int -> Int -> m () -sort2ByIndex cmp a i j = UNSAFE_CHECK(checkIndex) "sort2ByIndex" i (length a) - $ UNSAFE_CHECK(checkIndex) "sort2ByIndex" j (length a) $ do +sort2ByIndex cmp a i j = UNSAFE_CHECK(checkIndex) i (length a) + $ UNSAFE_CHECK(checkIndex) j (length a) $ do a0 <- unsafeRead a i a1 <- unsafeRead a j case cmp a0 a1 of @@ -99,9 +99,9 @@ sort3ByOffset cmp a off = sort3ByIndex cmp a off (off + 1) (off + 2) @-} sort3ByIndex :: (PrimMonad m, MVector v e) => Comparison e -> v (PrimState m) e -> Int -> Int -> Int -> m () -sort3ByIndex cmp a i j k = UNSAFE_CHECK(checkIndex) "sort3ByIndex" i (length a) - $ UNSAFE_CHECK(checkIndex) "sort3ByIndex" j (length a) - $ UNSAFE_CHECK(checkIndex) "sort3ByIndex" k (length a) $ do +sort3ByIndex cmp a i j k = UNSAFE_CHECK(checkIndex) i (length a) + $ UNSAFE_CHECK(checkIndex) j (length a) + $ UNSAFE_CHECK(checkIndex) k (length a) $ do a0 <- unsafeRead a i a1 <- unsafeRead a j a2 <- unsafeRead a k @@ -151,10 +151,10 @@ sort4ByOffset cmp a off = sort4ByIndex cmp a off (off + 1) (off + 2) (off + 3) @-} sort4ByIndex :: (PrimMonad m, MVector v e) => Comparison e -> v (PrimState m) e -> Int -> Int -> Int -> Int -> m () -sort4ByIndex cmp a i j k l = UNSAFE_CHECK(checkIndex) "sort4ByIndex" i (length a) - $ UNSAFE_CHECK(checkIndex) "sort4ByIndex" j (length a) - $ UNSAFE_CHECK(checkIndex) "sort4ByIndex" k (length a) - $ UNSAFE_CHECK(checkIndex) "sort4ByIndex" l (length a) $ do +sort4ByIndex cmp a i j k l = UNSAFE_CHECK(checkIndex) i (length a) + $ UNSAFE_CHECK(checkIndex) j (length a) + $ UNSAFE_CHECK(checkIndex) k (length a) + $ UNSAFE_CHECK(checkIndex) l (length a) $ do a0 <- unsafeRead a i a1 <- unsafeRead a j a2 <- unsafeRead a k diff --git a/tests/benchmarks/vector-algorithms-0.5.4.2/include/vector.h b/tests/benchmarks/vector-algorithms-0.5.4.2/include/vector.h index a8666c570c..b41ab65c53 100644 --- a/tests/benchmarks/vector-algorithms-0.5.4.2/include/vector.h +++ b/tests/benchmarks/vector-algorithms-0.5.4.2/include/vector.h @@ -11,7 +11,7 @@ import qualified Data.Vector.Internal.Check as Ck #define ERROR(f) (Ck.f __FILE__ __LINE__) #define ASSERT (Ck.assert __FILE__ __LINE__) #define ENSURE (Ck.f __FILE__ __LINE__) -#define CHECK(f) (Ck.f __FILE__ __LINE__) +#define CHECK(f) (Ck.f) #define BOUNDS_ERROR(f) (ERROR(f) Ck.Bounds) #define BOUNDS_ASSERT (ASSERT Ck.Bounds) diff --git a/tests/errors/SplitSubtype.hs b/tests/errors/SplitSubtype.hs index 4e6e20fe8e..8476d9fef0 100644 --- a/tests/errors/SplitSubtype.hs +++ b/tests/errors/SplitSubtype.hs @@ -1,4 +1,4 @@ -{-@ LIQUID "--expect-error-containing=| VV > 5}" @-} +{-@ LIQUID "--expect-error-containing=> 5}" @-} module SplitSubtype where {-@ foo :: {v:Int | v > 0 && v > 5 && v < 10 } -> Int @-}