liquidhaskell-boot 0.9.6.3 → 0.9.8.1
raw patch · 25 files changed
+340/−284 lines, 25 filesdep ~Cabaldep ~Diffdep ~ghc
Dependency ranges changed: Cabal, Diff, ghc, ghc-paths
Files
- ghc-api-tests/GhcApiTests.hs +65/−15
- include/CoreToLogic.lg +0/−49
- liquidhaskell-boot.cabal +7/−9
- src-ghc/Liquid/GHC/API.hs +15/−16
- src-ghc/Liquid/GHC/API/Extra.hs +27/−1
- src/Language/Haskell/Liquid/Bare/Check.hs +1/−0
- src/Language/Haskell/Liquid/Bare/Expand.hs +1/−0
- src/Language/Haskell/Liquid/CSS.hs +114/−0
- src/Language/Haskell/Liquid/Constraint/Generate.hs +1/−0
- src/Language/Haskell/Liquid/Constraint/Init.hs +1/−0
- src/Language/Haskell/Liquid/Constraint/Termination.hs +1/−0
- src/Language/Haskell/Liquid/GHC/CoreToLogic.hs +54/−0
- src/Language/Haskell/Liquid/GHC/Interface.hs +6/−6
- src/Language/Haskell/Liquid/GHC/Logging.hs +5/−1
- src/Language/Haskell/Liquid/GHC/Misc.hs +3/−33
- src/Language/Haskell/Liquid/GHC/Plugin.hs +6/−0
- src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs +1/−0
- src/Language/Haskell/Liquid/Measure.hs +1/−0
- src/Language/Haskell/Liquid/Misc.hs +1/−21
- src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +1/−0
- src/Language/Haskell/Liquid/Transforms/Rewrite.hs +5/−22
- src/Language/Haskell/Liquid/Types/Errors.hs +1/−0
- src/Language/Haskell/Liquid/UX/Annotate.hs +21/−5
- src/Language/Haskell/Liquid/UX/QuasiQuoter.hs +2/−1
- syntax/liquid.css +0/−105
ghc-api-tests/GhcApiTests.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE ViewPatterns #-} import Control.Monad import Data.List (find)@@ -10,9 +11,12 @@ , LitNumType(..) , Literal(..) , apiCommentsParsedSource+ , gopt_set , occNameString , pAT_ERROR_ID , showPprQualified+ , splitDollarApp+ , untick ) import Test.Tasty import Test.Tasty.HUnit@@ -32,7 +36,6 @@ 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) @@ -47,6 +50,8 @@ [ testCase "apiComments" testApiComments , testCase "caseDesugaring" testCaseDesugaring , testCase "numericLiteralDesugaring" testNumLitDesugaring+ , testCase "dollarDesugaring" testDollarDesugaring+ , testCase "localBindingsDesugaring" testLocalBindingsDesugaring ] -- Tests that Liquid.GHC.API.Extra.apiComments can retrieve the comments in@@ -86,22 +91,12 @@ parseMod str filepath = do let location = GHC.mkRealSrcLoc (GHC.mkFastString filepath) 1 1 buffer = GHC.stringToStringBuffer str- popts = GHC.mkParserOpts EnumSet.empty diagOpts [] False True True True+ popts = GHC.mkParserOpts EnumSet.empty GHC.emptyDiagOpts [] 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@@ -130,7 +125,7 @@ -- isExpectedDesugaring p = case find fBind p of Just (GHC.NonRec _ e0)- | Lam x (Case (Var x') _ _ [alt0, _alt1]) <- e0+ | Lam x (untick -> Case (Var x') _ _ [alt0, _alt1]) <- e0 , x == x' , Alt DEFAULT [] e1 <- alt0 , Case e2 _ _ [] <- e1@@ -144,6 +139,8 @@ "Unexpected desugaring:" : map showPprQualified coreProgram -- | Tests that numeric literal expressions desugar as Liquid Haskell expects.+--+-- https://github.com/ucsd-progsys/liquidhaskell/issues/2237 testNumLitDesugaring :: IO () testNumLitDesugaring = do let inputSource = unlines@@ -163,7 +160,7 @@ -- isExpectedDesugaring p = case find fBind p of Just (GHC.NonRec _ e0)- | Lam _a (Lam _dict (App fromIntegerApp (App (Var vIS) lit))) <- e0+ | Lam _a (Lam _dict (untick -> 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@@ -176,12 +173,65 @@ fail $ unlines $ "Unexpected desugaring:" : map showPprQualified coreProgram +-- | Tests that dollar sign desugars as Liquid Haskell expects.+testDollarDesugaring :: IO ()+testDollarDesugaring = do+ let inputSource = unlines+ [ "module DollarDesugaring where"+ , "f :: ()"+ , "f = (\\_ -> ()) $ 'a'"+ ]++ fBind (GHC.NonRec b _e) =+ occNameString (GHC.occName b) == "f"+ fBind _ = False++ isExpectedDesugaring p = case find fBind p of+ Just (GHC.NonRec _ e0)+ | Just (Lam _ _, App _ (Lit (LitChar 'a'))) <- splitDollarApp e0+ -> True+ _ -> False++ coreProgram <- compileToCore "DollarDesugaring" inputSource+ unless (isExpectedDesugaring coreProgram) $+ fail $ unlines $+ "Unexpected desugaring:" : map showPprQualified coreProgram++-- | Test that local bindings are preserved.+testLocalBindingsDesugaring :: IO ()+testLocalBindingsDesugaring = do+ let inputSource = unlines+ [ "module LocalBindingsDesugaring where"+ , "f :: ()"+ , "f = z"+ , " where"+ , " z = ()"+ ]++ fBind (GHC.NonRec b _e) =+ occNameString (GHC.occName b) == "f"+ fBind _ = False++ isExpectedDesugaring p = case find fBind p of+ Just (GHC.NonRec _ (Let (GHC.NonRec b _) _))+ -> occNameString (GHC.occName b) == "z"+ _ -> False++ coreProgram <- compileToCore "LocalBindingsDesugaring" 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+ GHC.setSessionDynFlags $ df1+ { GHC.backend = GHC.interpreterBackend+ }+ `gopt_set` GHC.Opt_InsertBreakpoints let target = GHC.Target { GHC.targetId = GHC.TargetFile (modName ++ ".hs") Nothing , GHC.targetUnitId = GHC.homeUnitId_ df1
− include/CoreToLogic.lg
@@ -1,49 +0,0 @@-define Data.Set.Base.singleton x = (Set_sng x)-define Data.Set.Base.union x y = (Set_cup x y)-define Data.Set.Base.intersection x y = (Set_cap x y)-define Data.Set.Base.difference x y = (Set_dif x y)-define Data.Set.Base.empty = (Set_empty 0)-define Data.Set.Base.null x = (Set_emp x)-define Data.Set.Base.member x xs = (Set_mem x xs)-define Data.Set.Base.isSubsetOf x y = (Set_sub x y)-define Data.Set.Base.fromList xs = (listElts xs)--define Data.Set.Internal.singleton x = (Set_sng x)-define Data.Set.Internal.union x y = (Set_cup x y)-define Data.Set.Internal.intersection x y = (Set_cap x y)-define Data.Set.Internal.difference x y = (Set_dif x y)-define Data.Set.Internal.empty = (Set_empty 0)-define Data.Set.Internal.null x = (Set_emp x)-define Data.Set.Internal.member x xs = (Set_mem x xs)-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.Types.True = (true)-define GHC.Real.div x y = (x / y)-define GHC.Real.mod x y = (x mod y)-define GHC.Classes.not x = (~ x)-define GHC.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)))-define Language.Haskell.Liquid.Bag.union m n = (Map_union m n)-define Language.Haskell.Liquid.Bag.empty = (Map_default 0)--define Data.Map.Base.insert k v m = (Map_store m k v)-define Data.Map.Base.select k v = (Map_select m k)--define Language.Haskell.Liquid.String.stringEmp = (stringEmp)-define Data.RString.RString.stringEmp = (stringEmp)-define String.stringEmp = (stringEmp)-define Main.mempty = (mempty)-define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)-define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)-define ProofCombinators.cast x y = (y)-define Liquid.ProofCombinators.cast x y = (y)-define Control.Parallel.Strategies.withStrategy s x = (x)--define Language.Haskell.Liquid.Equational.eq x y = (y)--define GHC.CString.unpackCString# x = x
liquidhaskell-boot.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell-boot-version: 0.9.6.3+version: 0.9.8.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,10 +13,7 @@ category: Language homepage: https://github.com/ucsd-progsys/liquidhaskell build-type: Simple-tested-with: GHC == 9.6.3--data-files: include/CoreToLogic.lg- syntax/liquid.css+tested-with: GHC == 9.8.1 source-repository head type: git@@ -47,6 +44,7 @@ Language.Haskell.Liquid.Bare.Slice Language.Haskell.Liquid.Bare.Typeclass Language.Haskell.Liquid.Bare.Elaborate+ Language.Haskell.Liquid.CSS Language.Haskell.Liquid.Constraint.Constraint Language.Haskell.Liquid.Constraint.Env Language.Haskell.Liquid.Constraint.Fresh@@ -63,6 +61,7 @@ Liquid.GHC.API Liquid.GHC.API.Extra Liquid.GHC.API.StableModule+ Language.Haskell.Liquid.GHC.CoreToLogic Language.Haskell.Liquid.GHC.Interface Language.Haskell.Liquid.GHC.Logging Language.Haskell.Liquid.GHC.Misc@@ -122,11 +121,11 @@ hs-source-dirs: src src-ghc build-depends: base >= 4.11.1.0 && < 5- , Diff >= 0.3 && < 0.5+ , Diff >= 0.3 && < 0.6 , aeson , binary , bytestring >= 0.10- , Cabal < 3.11+ , Cabal , cereal , cmdargs >= 0.10 , containers >= 0.5@@ -136,9 +135,8 @@ , filepath >= 1.3 , fingertree >= 0.1 , exceptions < 0.11- , ghc ^>= 9.6+ , ghc ^>= 9.8 , ghc-boot- , ghc-paths >= 0.1 , ghc-prim , gitrev , hashable >= 1.3 && < 1.5
src-ghc/Liquid/GHC/API.hs view
@@ -31,6 +31,7 @@ ( Opt_DeferTypedHoles , Opt_Haddock , Opt_ImplicitImportQualified+ , Opt_InsertBreakpoints , Opt_KeepRawTokenStream , Opt_PIC )@@ -163,7 +164,6 @@ , and_RDR , bindMName , dATA_FOLDABLE- , dollarIdKey , eqClassKey , eqClassName , ge_RDR@@ -431,6 +431,7 @@ import GHC.Driver.Config.Diagnostic as Ghc ( initDiagOpts , initDsMessageOpts+ , initIfaceMessageOpts ) import GHC.Driver.Main as Ghc ( hscDesugar@@ -474,19 +475,22 @@ ) import GHC.HsToCore.Expr as Ghc ( dsLExpr )+import GHC.Iface.Errors.Ppr as Ghc+ ( missingInterfaceErrorDiagnostic ) import GHC.Iface.Load as Ghc- ( cannotFindModule+ ( WhereFrom(ImportBySystem)+ , cannotFindModule , loadInterface ) import GHC.Rename.Expr as Ghc (rnLExpr)-import GHC.Rename.Names as Ghc (renamePkgQual)+import GHC.Rename.Names as Ghc+ ( renamePkgQual+ ) import GHC.Tc.Errors.Types as Ghc ( mkTcRnUnknownMessage ) 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 ) import GHC.Tc.Solver as Ghc ( InferMode(NoRestrictions) , captureTopConstraints@@ -498,7 +502,6 @@ , TcGblEnv(tcg_anns, tcg_exports, tcg_insts, tcg_mod, tcg_rdr_env, tcg_rn_imports) , TcM , TcRn- , WhereFrom(ImportBySystem) ) import GHC.Tc.Types.Evidence as Ghc ( TcEvBinds(EvBinds) )@@ -519,7 +522,7 @@ , reportDiagnostics ) import GHC.Tc.Utils.TcType as Ghc (tcSplitDFunTy, tcSplitMethodTy)-import GHC.Tc.Utils.Zonk as Ghc+import GHC.Tc.Zonk.Type as Ghc ( zonkTopLExpr ) import GHC.Types.PkgQual as Ghc ( PkgQual(NoPkgQual) )@@ -532,7 +535,6 @@ import GHC.Types.Avail as Ghc ( AvailInfo(Avail, AvailTC) , availNames- , greNameMangledName ) import GHC.Types.Basic as Ghc ( Arity@@ -553,9 +555,11 @@ import GHC.Types.Error as Ghc ( Messages(getMessages) , MessageClass(MCDiagnostic)- , Diagnostic(defaultDiagnosticOpts)+ , Diagnostic , DiagnosticReason(WarningWithoutFlag) , MsgEnvelope(errMsgSpan)+ , ResolvedDiagnosticReason(ResolvedDiagnosticReason)+ , defaultDiagnosticOpts , errorsOrFatalWarningsFound , mkPlainError )@@ -610,15 +614,10 @@ , stableNameCmp ) import GHC.Types.Name.Reader as Ghc- ( ImpDeclSpec(ImpDeclSpec, is_as, is_dloc, is_mod, is_qual)- , ImportSpec(ImpSpec)- , ImpItemSpec(ImpAll)+ ( ImpItemSpec(ImpAll) , getRdrName , globalRdrEnvElts- , gresFromAvails- , greMangledName- , lookupGRE_RdrName- , mkGlobalRdrEnv+ , greName , mkQual , mkVarUnqual , mkUnqual
src-ghc/Liquid/GHC/API/Extra.hs view
@@ -21,10 +21,12 @@ , renderWithStyle , showPprQualified , showSDocQualified+ , splitDollarApp , strictNothing , thisPackage , tyConRealArity , typecheckModuleIO+ , untick ) where import Control.Monad.IO.Class@@ -36,6 +38,7 @@ import Data.List (foldl', sortOn) import qualified Data.Map as Map import qualified Data.Set as S+import GHC.Builtin.Names ( dollarIdKey ) import GHC.Core as Ghc import GHC.Core.Coercion as Ghc import GHC.Core.DataCon as Ghc@@ -52,7 +55,7 @@ import GHC.Types.Name (isSystemName, nameModule_maybe, occNameFS) import GHC.Types.SrcLoc as Ghc import GHC.Types.TypeEnv-import GHC.Types.Unique (getUnique)+import GHC.Types.Unique (getUnique, hasKey) import GHC.Types.Unique.FM import GHC.Unit.Module.Deps as Ghc (Dependencies(dep_direct_mods))@@ -288,3 +291,26 @@ strictNothing :: GHC.Data.Strict.Maybe a strictNothing = GHC.Data.Strict.Nothing++splitDollarApp :: CoreExpr -> Maybe (CoreExpr, CoreExpr)+splitDollarApp e+ -- matches `$ t1 t2 t3 t4 f a`+ | App e1 a <- untick e+ , App e2 f <- untick e1+ , App e3 t4 <- untick e2+ , App e4 t3 <- untick e3+ , App e5 t2 <- untick e4+ , App d t1 <- untick e5+ , Var v <- untick d+ , v `hasKey` dollarIdKey+ , Type _ <- untick t1+ , Type _ <- untick t2+ , Type _ <- untick t3+ , Type _ <- untick t4+ = Just (f, a)+ | otherwise+ = Nothing++untick :: CoreExpr -> CoreExpr+untick (Tick _ e) = untick e+untick e = e
src/Language/Haskell/Liquid/Bare/Check.hs view
@@ -3,6 +3,7 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -Wno-x-partial #-} module Language.Haskell.Liquid.Bare.Check ( checkTargetSpec
src/Language/Haskell/Liquid/Bare/Expand.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -Wno-x-partial #-} module Language.Haskell.Liquid.Bare.Expand ( -- * Create alias expansion environment
+ src/Language/Haskell/Liquid/CSS.hs view
@@ -0,0 +1,114 @@+{-# LANGUAGE OverloadedStrings #-}+module Language.Haskell.Liquid.CSS where++import Data.Text (Text)+import qualified Data.Text as Text++syntax :: Text+syntax = Text.unlines+ [ ".hs-linenum {"+ , " color: #B2B2B2;"+ , " font-style: italic;"+ , "}"+ , ""+ , ".hs-error {"+ , " background-color: #FF8585 ;"+ , "}"+ , ""+ , ".hs-keyglyph {"+ , " color: #007020"+ , "}"+ , ""+ , ".hs-keyword {"+ , " color: #007020;"+ , " // font-weight: bold;"+ , "}"+ , ""+ , ".hs-comment, .hs-comment a {color: green;}"+ , ""+ , ".hs-str, .hs-chr {color: teal;}"+ , ""+ , ".hs-conid { "+ , " color: #902000; /* color: #00FFFF; color: #0E84B5; */"+ , " //font-weight: bold; "+ , "}"+ , ""+ , ".hs-definition { "+ , " color: #06287E "+ , " /* font-weight: bold; */ "+ , "}"+ , ""+ , ".hs-varid, .hs-varop, .hs-layout {"+ , " color: black; "+ , "}"+ , ""+ , ".hs-num {"+ , " color: #40A070;"+ , "}"+ , ""+ , ".hs-conop {"+ , " color: #902000; "+ , "}"+ , ""+ , ".hs-cpp {"+ , " color: orange;"+ , "}"+ , ""+ , ".hs-sel {}"+ , ""+ , "a.annot {"+ , " position:relative; "+ , " color:#000;"+ , " text-decoration:none; "+ , " white-space: pre; "+ , "}"+ , ""+ , "a.annot:hover { "+ , " z-index:25; "+ , " background-color: #D8D8D8;"+ , "}"+ , ""+ , "a.annot span.annottext{display: none}"+ , ""+ , "a.annot:hover span.annottext{ "+ , " "+ , " border-radius: 5px 5px;"+ , " "+ , " -moz-border-radius: 5px; "+ , " -webkit-border-radius: 5px; "+ , " "+ , " box-shadow: 5px 5px 5px rgba(0, 0, 0, 0.1); "+ , " -webkit-box-shadow: 5px 5px rgba(0, 0, 0, 0.1);"+ , " -moz-box-shadow: 5px 5px rgba(0, 0, 0, 0.1); "+ , ""+ , " white-space:pre;"+ , " display:block;"+ , " position: absolute; "+ , " left: 1em; top: 2em; "+ , " z-index: 99;"+ , " margin-left: 5; "+ , " background: #FFFFAA; "+ , " border: 3px solid #FFAD33;"+ , " padding: 0.8em 1em;"+ , "}"+ , ""+ , "code {"+ , " /* font-weight: bold; */"+ , " background-color: rgb(250, 250, 250);"+ , " border: 1px solid rgb(200, 200, 200);"+ , " padding-left: 4px;"+ , " padding-right: 4px;"+ , "}"+ , ""+ , "pre {"+ , " background-color: #f0f0f0;"+ , " border-top: 1px solid #ccc;"+ , " border-bottom: 1px solid #ccc;"+ , " padding: 5px;"+ , " // font-size: 120%;"+ , " // font-family: Bitstream Vera Sans Mono,monospace;"+ , " display: block;"+ , " overflow: visible;"+ , "}"+ ]+
src/Language/Haskell/Liquid/Constraint/Generate.hs view
@@ -10,6 +10,7 @@ {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}+{-# OPTIONS_GHC -Wno-x-partial #-} -- | This module defines the representation of Subtyping and WF Constraints, -- and the code for syntax-directed constraint generation.
src/Language/Haskell/Liquid/Constraint/Init.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -Wno-x-partial #-} -- | This module defines the representation of Subtyping and WF Constraints, -- and the code for syntax-directed constraint generation.
src/Language/Haskell/Liquid/Constraint/Termination.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE TupleSections #-}+{-# OPTIONS_GHC -Wno-x-partial #-} -- | This module defines code for generating termination constraints. module Language.Haskell.Liquid.Constraint.Termination (
+ src/Language/Haskell/Liquid/GHC/CoreToLogic.hs view
@@ -0,0 +1,54 @@+module Language.Haskell.Liquid.GHC.CoreToLogic where++coreToLogic :: String+coreToLogic = unlines+ [ "define Data.Set.Base.singleton x = (Set_sng x)"+ , "define Data.Set.Base.union x y = (Set_cup x y)"+ , "define Data.Set.Base.intersection x y = (Set_cap x y)"+ , "define Data.Set.Base.difference x y = (Set_dif x y)"+ , "define Data.Set.Base.empty = (Set_empty 0)"+ , "define Data.Set.Base.null x = (Set_emp x)"+ , "define Data.Set.Base.member x xs = (Set_mem x xs)"+ , "define Data.Set.Base.isSubsetOf x y = (Set_sub x y)"+ , "define Data.Set.Base.fromList xs = (listElts xs)"+ , ""+ , "define Data.Set.Internal.singleton x = (Set_sng x)"+ , "define Data.Set.Internal.union x y = (Set_cup x y)"+ , "define Data.Set.Internal.intersection x y = (Set_cap x y)"+ , "define Data.Set.Internal.difference x y = (Set_dif x y)"+ , "define Data.Set.Internal.empty = (Set_empty 0)"+ , "define Data.Set.Internal.null x = (Set_emp x)"+ , "define Data.Set.Internal.member x xs = (Set_mem x xs)"+ , "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.Types.True = (true)"+ , "define GHC.Real.div x y = (x / y)"+ , "define GHC.Real.mod x y = (x mod y)"+ , "define GHC.Classes.not x = (~ x)"+ , "define GHC.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)))"+ , "define Language.Haskell.Liquid.Bag.union m n = (Map_union m n)"+ , "define Language.Haskell.Liquid.Bag.empty = (Map_default 0)"+ , ""+ , "define Data.Map.Base.insert k v m = (Map_store m k v)"+ , "define Data.Map.Base.select k v = (Map_select m k)"+ , ""+ , "define Language.Haskell.Liquid.String.stringEmp = (stringEmp)"+ , "define Data.RString.RString.stringEmp = (stringEmp)"+ , "define String.stringEmp = (stringEmp)"+ , "define Main.mempty = (mempty)"+ , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)"+ , "define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)"+ , "define ProofCombinators.cast x y = (y)"+ , "define Liquid.ProofCombinators.cast x y = (y)"+ , "define Control.Parallel.Strategies.withStrategy s x = (x)"+ , ""+ , "define Language.Haskell.Liquid.Equational.eq x y = (y)"+ , ""+ , "define GHC.CString.unpackCString# x = x"+ ]
src/Language/Haskell/Liquid/GHC/Interface.hs view
@@ -13,6 +13,7 @@ {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wwarn=deprecations #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}+{-# OPTIONS_GHC -Wno-x-partial #-} module Language.Haskell.Liquid.GHC.Interface ( @@ -75,6 +76,7 @@ import Text.PrettyPrint.HughesPJ hiding (first, (<>)) import Language.Fixpoint.Types hiding (err, panic, Error, Result, Expr) import qualified Language.Fixpoint.Misc as Misc+import qualified Language.Haskell.Liquid.GHC.CoreToLogic as CoreToLogic import Language.Haskell.Liquid.GHC.Misc import Language.Haskell.Liquid.GHC.Types (MGIModGuts(..)) import Language.Haskell.Liquid.GHC.Play@@ -195,7 +197,7 @@ where names :: [Ghc.Name] names = liftM2 (++)- (fmap Ghc.greMangledName . Ghc.globalRdrEnvElts . tcg_rdr_env)+ (fmap Ghc.greName . Ghc.globalRdrEnvElts . tcg_rdr_env) (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.@@ -229,8 +231,8 @@ availableNames :: [AvailInfo] -> [Name] availableNames = concatMap $ \case- Avail n -> [Ghc.greNameMangledName n]- AvailTC n ns -> n : map Ghc.greNameMangledName ns+ Avail n -> [n]+ AvailTC n ns -> n : ns _dumpTypeEnv :: TypecheckedModule -> IO () _dumpTypeEnv tm = do@@ -351,9 +353,7 @@ makeLogicMap :: IO LogicMap makeLogicMap = do- lg <- Misc.getCoreToLogicPath- lspec <- Misc.sayReadFile lg- case parseSymbolToLogic lg lspec of+ case parseSymbolToLogic "CoreToLogic.coreToLogic" CoreToLogic.coreToLogic of Left peb -> do hPutStrLn stderr (errorBundlePretty peb) panic Nothing "makeLogicMap failed"
src/Language/Haskell/Liquid/GHC/Logging.hs view
@@ -34,7 +34,11 @@ -> PJ.Doc -> IO () putLogMsg logger sev srcSpan _mbStyle =- GHC.putLogMsg logger (GHC.logFlags logger) (GHC.MCDiagnostic sev GHC.WarningWithoutFlag Nothing) srcSpan . GHC.text . PJ.render+ GHC.putLogMsg+ logger+ (GHC.logFlags logger)+ (GHC.MCDiagnostic sev (GHC.ResolvedDiagnosticReason GHC.WarningWithoutFlag) Nothing)+ srcSpan . GHC.text . PJ.render putWarnMsg :: GHC.Logger -> GHC.SrcSpan -> PJ.Doc -> IO () putWarnMsg logger srcSpan doc =
src/Language/Haskell/Liquid/GHC/Misc.hs view
@@ -14,6 +14,7 @@ {-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1. {-# OPTIONS_GHC -Wno-orphans #-}+{-# OPTIONS_GHC -Wno-x-partial #-} -- | This module contains a wrappers and utility functions for -- accessing GHC module information. It should NEVER depend on@@ -28,7 +29,7 @@ import Prelude hiding (error) import Liquid.GHC.API as Ghc hiding (L, line, sourceName, showPpr, panic, showSDoc)-import qualified Liquid.GHC.API as Ghc (GenLocated (L), showSDoc, panic)+import qualified Liquid.GHC.API as Ghc (GenLocated (L)) import Data.Char (isLower, isSpace, isUpper)@@ -53,7 +54,7 @@ isAnonBinder :: Ghc.TyConBinder -> Bool-isAnonBinder (Bndr _ (AnonTCB _)) = True+isAnonBinder (Bndr _ AnonTCB) = True isAnonBinder (Bndr _ _) = False mkAlive :: Var -> Id@@ -377,37 +378,6 @@ uniqueHash :: Uniquable a => Int -> a -> Int uniqueHash i = hashWithSalt i . getKey . getUnique---- slightly modified version of DynamicLoading.lookupRdrNameInModule-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 NoPkgQual- case found_module of- Found _ mod' -> do- -- Find the exports of the module- (_, mb_iface) <- getModuleInterface hsc_env mod'- case mb_iface of- Just iface -> do- -- Try and find the required name in the exports- let decl_spec = ImpDeclSpec { is_mod = mod_name, is_as = mod_name- , is_qual = False, is_dloc = noSrcSpan }- provenance = Just $ ImpSpec decl_spec ImpAll- env = case mi_globals iface of- Nothing -> mkGlobalRdrEnv (gresFromAvails provenance (mi_exports iface))- Just e -> e- case lookupGRE_RdrName rdr_name env of--- XXX [gre] -> return (Just (gre_name gre))- [] -> return Nothing- _ -> Ghc.panic "lookupRdrNameInModule"- 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'- throwCmdLineError = throwGhcException . CmdLineError---- qualImportDecl :: ModuleName -> ImportDecl name--- qualImportDecl mn = (simpleImportDecl mn) { ideclQualified = True } ignoreInline :: ParsedModule -> ParsedModule ignoreInline x = x {pm_parsed_source = go <$> pm_parsed_source x}
src/Language/Haskell/Liquid/GHC/Plugin.hs view
@@ -169,6 +169,12 @@ `gopt_set` Opt_PIC `gopt_set` Opt_DeferTypedHoles `gopt_set` Opt_KeepRawTokenStream+ -- Opt_InsertBreakpoints is used during desugaring to prevent the+ -- simple optimizer from inlining local bindings to which we might want+ -- to attach specifications.+ --+ -- https://gitlab.haskell.org/ghc/ghc/-/issues/24386+ `gopt_set` Opt_InsertBreakpoints `xopt_set` MagicHash `xopt_set` DeriveGeneric `xopt_set` StandaloneDeriving
src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs view
@@ -93,6 +93,7 @@ -- now look up the assumptions liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 assumptionsMod FoundMultiple{} -> failWithTc $ mkTcRnUnknownMessage $ mkPlainError [] $+ missingInterfaceErrorDiagnostic (initIfaceMessageOpts $ hsc_dflags hscEnv) $ cannotFindModule hscEnv assumptionsModName res _ -> return Nothing
src/Language/Haskell/Liquid/Measure.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TupleSections #-}+{-# OPTIONS_GHC -Wno-x-partial #-} module Language.Haskell.Liquid.Measure ( -- * Specifications
src/Language/Haskell/Liquid/Misc.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE DoAndIfThenElse #-}+{-# OPTIONS_GHC -Wno-x-partial #-} module Language.Haskell.Liquid.Misc where @@ -7,9 +8,7 @@ import Control.Monad.State import Control.Arrow (first)-import System.FilePath import System.Directory (getModificationTime, doesFileExist)-import System.Environment (getExecutablePath) import qualified Control.Exception as Ex --(evaluate, catch, IOException) import qualified Data.HashSet as S@@ -25,7 +24,6 @@ import qualified Text.PrettyPrint.HughesPJ as PJ -- (char, Doc) import Text.Printf import Language.Fixpoint.Misc-import Paths_liquidhaskell_boot type Nat = Int @@ -157,24 +155,6 @@ unzip4 = go [] [] [] [] where go a1 a2 a3 a4 ((x1,x2,x3,x4):xs) = go (x1:a1) (x2:a2) (x3:a3) (x4:a4) xs go a1 a2 a3 a4 [] = (reverse a1, reverse a2, reverse a3, reverse a4)---getCssPath :: IO FilePath-getCssPath = getDataFileName $ "syntax" </> "liquid.css"--getCoreToLogicPath :: IO FilePath-getCoreToLogicPath = do- let fileName = "CoreToLogic.lg"-- -- Try to find it first at executable path- exePath <- dropFileName <$> getExecutablePath- let atExe = exePath </> fileName- exists <- doesFileExist atExe-- if exists then- return atExe- else- getDataFileName ("include" </> fileName) {-@ type ListN a N = {v:[a] | len v = N} @-} {-@ type ListL a L = ListN a (len L) @-}
src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -Wno-orphans #-}+{-# OPTIONS_GHC -Wno-x-partial #-} module Language.Haskell.Liquid.Transforms.CoreToLogic ( coreToDef
src/Language/Haskell/Liquid/Transforms/Rewrite.hs view
@@ -56,21 +56,11 @@ simplifyCore = not . noSimplifyCore undollar :: RewriteRule-undollar = go - where - go e - -- matches `$ t1 t2 t3 f a` - | App e1 a <- untick e- , App e2 f <- untick e1- , App e3 t3 <- untick e2 - , App e4 t2 <- untick e3 - , App d t1 <- untick e4 - , Var v <- untick d - , v `hasKey` dollarIdKey- , Type _ <- untick t1- , Type _ <- untick t2- , Type _ <- untick t3- = Just $ App f a +undollar = go+ where+ go e+ | Just (f, a) <- splitDollarApp e+ = Just $ App f a go (Tick t e) = Tick t <$> go e go (Let (NonRec x ex) e)@@ -95,13 +85,6 @@ goAlt (Alt c bs e) = Alt c bs <$> go e-- - --untick :: CoreExpr -> CoreExpr -untick (Tick _ e) = untick e -untick e = e tidyTuples :: RewriteRule tidyTuples ce = Just $ evalState (go ce) []
src/Language/Haskell/Liquid/Types/Errors.hs view
@@ -10,6 +10,7 @@ {-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1. {-# OPTIONS_GHC -Wno-orphans #-} -- PPrint and aeson instances.+{-# OPTIONS_GHC -Wno-x-partial #-} -- | This module contains the *types* related creating Errors. -- It depends only on Fixpoint and basic haskell libraries,
src/Language/Haskell/Liquid/UX/Annotate.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}+{-# OPTIONS_GHC -Wno-x-partial #-} --------------------------------------------------------------------------- -- | This module contains the code that uses the inferred types to generate@@ -20,6 +21,7 @@ ) where import Data.Hashable+import qualified Data.Text.IO as Text import Data.String import GHC ( SrcSpan (..) , srcSpanStartCol@@ -39,10 +41,12 @@ import Data.Aeson import Control.Arrow hiding ((<+>)) -- import Control.Applicative ((<$>))-import Control.Monad (when, forM_)+import Control.Exception (catchJust)+import Control.Monad (guard, when, forM_)+import GHC.IO.Exception (IOErrorType(ResourceBusy), ioe_type) import System.Exit (ExitCode (..))-import System.FilePath (takeFileName, dropFileName, (</>))+import System.FilePath (dropFileName, (</>)) import System.Directory (findExecutable) import qualified System.Directory as Dir import qualified Data.List as L@@ -51,6 +55,7 @@ import qualified Data.Text as T import qualified Data.HashMap.Strict as M import qualified Language.Haskell.Liquid.Misc as Misc+import qualified Language.Haskell.Liquid.CSS as CSS import qualified Language.Haskell.Liquid.UX.ACSS as ACSS import Language.Haskell.HsColour.Classify import Language.Fixpoint.Utils.Files@@ -129,6 +134,17 @@ Dir.createDirectoryIfMissing False $ tempDirectory tgt Dir.copyFile src tgt +-- | Creates the parent directory and tries to writes the file.+-- Might not write to the file if someone else is writing to it+-- already.+writeFileCreateParentDirIfMissing :: T.Text -> FilePath -> IO ()+writeFileCreateParentDirIfMissing s tgt = do+ Dir.createDirectoryIfMissing False $ tempDirectory tgt+ catchJust+ (\e -> guard (ioe_type e == ResourceBusy))+ (Text.writeFile tgt s)+ (const (return ()))+ writeFilesOrStrings :: FilePath -> [Either FilePath String] -> IO () writeFilesOrStrings tgtFile = mapM_ $ either (`copyFileCreateParentDirIfMissing` tgtFile) (tgtFile `appendFile`) @@ -137,9 +153,9 @@ src <- Misc.sayReadFile srcF let lhs = isExtFile LHs srcF let body = {-# SCC "hsannot" #-} ACSS.hsannot False (Just tokAnnot) lhs (src, annm)- cssFile <- getCssPath- copyFileCreateParentDirIfMissing cssFile (dropFileName htmlF </> takeFileName cssFile)- renderHtml (pandocF && lhs) htmlF srcF (takeFileName cssFile) body+ let cssFile = "syntax.css"+ writeFileCreateParentDirIfMissing CSS.syntax (dropFileName htmlF </> cssFile)+ renderHtml (pandocF && lhs) htmlF srcF cssFile body renderHtml :: Bool -> FilePath -> String -> String -> String -> IO () renderHtml True = renderPandoc
src/Language/Haskell/Liquid/UX/QuasiQuoter.hs view
@@ -3,6 +3,7 @@ {-# LANGUAGE TemplateHaskellQuotes #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -Wno-x-partial #-} module Language.Haskell.Liquid.UX.QuasiQuoter -- (@@ -91,7 +92,7 @@ lsym = F.atLoc rta n name = symbolName n n = rtName (val rta)- tvs = (\a -> PlainTV (symbolName a) ()) <$> rtTArgs (val rta)+ tvs = (\a -> PlainTV (symbolName a) BndrReq) <$> rtTArgs (val rta) mkSpecDecs _ = Right []
− syntax/liquid.css
@@ -1,105 +0,0 @@-.hs-linenum {- color: #B2B2B2; - font-style: italic;-}--.hs-error {- background-color: #FF8585 ;-}--.hs-keyglyph {- color: #007020-}--.hs-keyword {- color: #007020;- // font-weight: bold;-}--.hs-comment, .hs-comment a {color: green;}--.hs-str, .hs-chr {color: teal;}--.hs-conid { - color: #902000; /* color: #00FFFF; color: #0E84B5; */- //font-weight: bold; -}--.hs-definition { - color: #06287E - /* font-weight: bold; */ -}--.hs-varid, .hs-varop, .hs-layout {- color: black; -}--.hs-num {- color: #40A070;-}--.hs-conop {- color: #902000; -}--.hs-cpp {- color: orange;-}--.hs-sel {}--a.annot {- position:relative; - color:#000;- text-decoration:none; - white-space: pre; -}--a.annot:hover { - z-index:25; - background-color: #D8D8D8;-}--a.annot span.annottext{display: none}--a.annot:hover span.annottext{ - - border-radius: 5px 5px;- - -moz-border-radius: 5px; - -webkit-border-radius: 5px; - - box-shadow: 5px 5px 5px rgba(0, 0, 0, 0.1); - -webkit-box-shadow: 5px 5px rgba(0, 0, 0, 0.1);- -moz-box-shadow: 5px 5px rgba(0, 0, 0, 0.1); -- white-space:pre;- display:block;- position: absolute; - left: 1em; top: 2em; - z-index: 99;- margin-left: 5; - background: #FFFFAA; - border: 3px solid #FFAD33;- padding: 0.8em 1em;-}--code {- /* font-weight: bold; */- background-color: rgb(250, 250, 250); - border: 1px solid rgb(200, 200, 200);- padding-left: 4px;- padding-right: 4px;-}--pre {- background-color: #f0f0f0;- border-top: 1px solid #ccc;- border-bottom: 1px solid #ccc;- padding: 5px;- // font-size: 120%;- // font-family: Bitstream Vera Sans Mono,monospace;- display: block;- overflow: visible;-}-