🚨 Add -Wmissing-import-lists to package.yaml

lsrcz · Sep 28, 2023 · 477eed9 · 477eed9
1 parent 4bb96dd
commit 477eed9
Show file tree

Hide file tree

Showing 108 changed files with 3,158 additions and 607 deletions.
diff --git a/grisette.cabal b/grisette.cabal
@@ -126,7 +126,7 @@ library
       Paths_grisette
   hs-source-dirs:
       src
-  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields
+  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields
   build-depends:
       QuickCheck >=2.13.2 && <2.15
     , array >=0.5.4 && <0.6
@@ -161,7 +161,7 @@ test-suite doctest
       Paths_grisette
   hs-source-dirs:
       doctest
-  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields
+  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields
   build-depends:
       Glob
     , QuickCheck >=2.13.2 && <2.15
@@ -215,7 +215,7 @@ test-suite spec
       Paths_grisette
   hs-source-dirs:
       test
-  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields
+  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields
   build-depends:
       QuickCheck >=2.13.2 && <2.15
     , array >=0.5.4 && <0.6

diff --git a/package.yaml b/package.yaml
@@ -18,44 +18,46 @@ license-file: LICENSE
 github: lsrcz/grisette
 copyright: "2021-2023 Sirui Lu"
 extra-source-files:
-- CHANGELOG.md
-- README.md
+  - CHANGELOG.md
+  - README.md
 tested-with:
-- GHC == 8.10.7
-- GHC == 9.0.2
-- GHC == 9.2.8
-- GHC == 9.4.5
-- GHC == 9.6.2
+  - GHC == 8.10.7
+  - GHC == 9.0.2
+  - GHC == 9.2.8
+  - GHC == 9.4.5
+  - GHC == 9.6.2
 
 dependencies:
-- base >= 4.14 && < 5
-- intern >= 0.9.2 && < 0.10
-- hashable >= 1.2.3 && < 1.5
-- mtl >= 2.2.2 && < 2.4
-- transformers >= 0.5.6 && < 0.7
-- generic-deriving >= 1.14.1 && < 1.15
-- bytestring >= 0.10.12 && < 0.12
-- unordered-containers >= 0.2.11 && < 0.3
-- template-haskell >= 2.16 && < 2.21
-- deepseq >= 1.4.4 && < 1.5
-- hashtables >= 1.2.3.4 && < 1.4
-- loch-th >= 0.2.2 && < 0.3
-- th-compat >= 0.1.2 && < 0.2
-- call-stack >= 0.1 && < 0.5
-- array >= 0.5.4 && < 0.6
-- sbv >= 8.11 && < 10.3
-- parallel >= 3.2.2.0 && < 3.3
-- text >= 1.2.4.1 && < 2.1
-- QuickCheck >= 2.13.2 && < 2.15
-- prettyprinter >= 1.5.0 && < 1.8
+  - base >= 4.14 && < 5
+  - intern >= 0.9.2 && < 0.10
+  - hashable >= 1.2.3 && < 1.5
+  - mtl >= 2.2.2 && < 2.4
+  - transformers >= 0.5.6 && < 0.7
+  - generic-deriving >= 1.14.1 && < 1.15
+  - bytestring >= 0.10.12 && < 0.12
+  - unordered-containers >= 0.2.11 && < 0.3
+  - template-haskell >= 2.16 && < 2.21
+  - deepseq >= 1.4.4 && < 1.5
+  - hashtables >= 1.2.3.4 && < 1.4
+  - loch-th >= 0.2.2 && < 0.3
+  - th-compat >= 0.1.2 && < 0.2
+  - call-stack >= 0.1 && < 0.5
+  - array >= 0.5.4 && < 0.6
+  - sbv >= 8.11 && < 10.3
+  - parallel >= 3.2.2.0 && < 3.3
+  - text >= 1.2.4.1 && < 2.1
+  - QuickCheck >= 2.13.2 && < 2.15
+  - prettyprinter >= 1.5.0 && < 1.8
 
-flags: {
-  fast: {
-    description: "Compile with O2 optimization",
-    manual: False,
-    default: True,
+flags:
+  {
+    fast:
+      {
+        description: "Compile with O2 optimization",
+        manual: False,
+        default: True,
+      },
   }
-}
 
 when:
   - condition: flag(fast)
@@ -72,6 +74,7 @@ ghc-options:
   - -Wincomplete-record-updates
   - -Wmissing-export-lists
   - -Wmissing-home-modules
+  - -Wmissing-import-lists
   - -Wpartial-fields
 
 library:
@@ -94,4 +97,3 @@ tests:
       - grisette
       - doctest >= 0.18.2 && < 0.22
       - Glob
-
diff --git a/src/Grisette.hs b/src/Grisette.hs
@@ -1,5 +1,8 @@
+-- Disable this warning because we are re-exporting things.
+{-# OPTIONS_GHC -Wno-missing-import-lists #-}
+
 -- |
--- Module      :   Grisette.Core
+-- Module      :   Grisette
 -- Copyright   :   (c) Sirui Lu 2021-2023
 -- License     :   BSD-3-Clause (see the LICENSE file)
 --

diff --git a/src/Grisette/Backend/SBV.hs b/src/Grisette/Backend/SBV.hs
@@ -1,3 +1,6 @@
+-- Disable this warning because we are re-exporting things.
+{-# OPTIONS_GHC -Wno-missing-import-lists #-}
+
 -- |
 -- Module      :   Grisette.Backend.SBV
 -- Copyright   :   (c) Sirui Lu 2021-2023
@@ -34,3 +37,14 @@ where
 
 import qualified Data.SBV as SBV
 import Grisette.Backend.SBV.Data.SMT.Solving
+  ( ApproximationConfig (..),
+    ExtraConfig (..),
+    GrisetteSMTConfig (..),
+    SolvingFailure (..),
+    approx,
+    clearApprox,
+    clearTimeout,
+    precise,
+    withApprox,
+    withTimeout,
+  )
diff --git a/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs b/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
@@ -32,32 +32,123 @@ module Grisette.Backend.SBV.Data.SMT.Lowering
   )
 where
 
-import Data.Bifunctor
+import Data.Bifunctor (Bifunctor (bimap, first, second))
 import Data.Bits
-import Data.Dynamic
-import Data.Foldable
-import Data.Kind
-import Data.Maybe
+  ( Bits (complement, rotate, shift, xor, (.&.), (.|.)),
+  )
+import Data.Dynamic (Typeable, fromDyn, toDyn)
+import Data.Foldable (Foldable (foldl'), asum)
+import Data.Kind (Type)
+import Data.Maybe (fromMaybe)
 import qualified Data.SBV as SBV
 import qualified Data.SBV.Control as SBVC
 import qualified Data.SBV.Internals as SBVI
 import Data.Type.Equality (type (~~))
-import Data.Typeable
+import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))
 import GHC.Exts (sortWith)
-import GHC.Stack
+import GHC.Stack (HasCallStack)
 import GHC.TypeNats
+  ( KnownNat,
+    Nat,
+    natVal,
+    type (+),
+    type (-),
+    type (<=),
+  )
 import {-# SOURCE #-} Grisette.Backend.SBV.Data.SMT.Solving
+  ( ApproximationConfig (Approx, NoApprox),
+    ExtraConfig (integerApprox),
+    GrisetteSMTConfig (GrisetteSMTConfig),
+    TermTy,
+  )
 import Grisette.Backend.SBV.Data.SMT.SymBiMap
-import Grisette.Core.Data.BV
+  ( SymBiMap,
+    addBiMap,
+    addBiMapIntermediate,
+    emptySymBiMap,
+    findStringToSymbol,
+    lookupTerm,
+    sizeBiMap,
+  )
+import Grisette.Core.Data.BV (IntN (IntN, unIntN), WordN (WordN))
 import Grisette.Core.Data.Class.ModelOps
+  ( ModelOps (emptyModel, insertValue),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+    symTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
+  ( SomeTerm (SomeTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SomeTypedSymbol (SomeTypedSymbol),
+    SupportedPrim (withPrim),
+    Term
+      ( AbsNumTerm,
+        AddNumTerm,
+        AndBitsTerm,
+        AndTerm,
+        BVConcatTerm,
+        BVExtendTerm,
+        BVSelectTerm,
+        BVToSignedTerm,
+        BVToUnsignedTerm,
+        BinaryTerm,
+        ComplementBitsTerm,
+        ConTerm,
+        DivBoundedIntegralTerm,
+        DivIntegralTerm,
+        EqvTerm,
+        GeneralFunApplyTerm,
+        ITETerm,
+        LENumTerm,
+        LTNumTerm,
+        ModBoundedIntegralTerm,
+        ModIntegralTerm,
+        NotTerm,
+        OrBitsTerm,
+        OrTerm,
+        QuotBoundedIntegralTerm,
+        QuotIntegralTerm,
+        RemBoundedIntegralTerm,
+        RemIntegralTerm,
+        RotateBitsTerm,
+        ShiftBitsTerm,
+        SignumNumTerm,
+        SymTerm,
+        TabularFunApplyTerm,
+        TernaryTerm,
+        TimesNumTerm,
+        UMinusNumTerm,
+        UnaryTerm,
+        XorBitsTerm
+      ),
+    TypedSymbol (IndexedSymbol),
+    buildGeneralFun,
+    someTypedSymbol,
+    withSymbolSupported,
+    type (-->),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
-import Grisette.IR.SymPrim.Data.Prim.Model as PM
+  ( introSupportedPrimConstraint,
+  )
+import Grisette.IR.SymPrim.Data.Prim.Model as PM (Model)
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalEqvTerm,
+    pevalITETerm,
+  )
 import Grisette.IR.SymPrim.Data.TabularFun
+  ( type (=->) (TabularFun),
+  )
 import Grisette.Utils.Parameterized
+  ( KnownProof (KnownProof),
+    LeqProof (LeqProof),
+    unsafeAxiom,
+    unsafeKnownProof,
+    unsafeLeqProof,
+    withKnownProof,
+  )
 import qualified Type.Reflection as R
 
 translateTypeError :: (HasCallStack) => R.TypeRep a -> b

diff --git a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
@@ -37,33 +37,59 @@ module Grisette.Backend.SBV.Data.SMT.Solving
   )
 where
 
-import Control.DeepSeq
-import Control.Exception
+import Control.DeepSeq (NFData)
+import Control.Exception (handle)
 import Control.Monad.IO.Class (liftIO)
 import qualified Data.HashSet as S
-import Data.Hashable
-import Data.Kind
+import Data.Hashable (Hashable)
+import Data.Kind (Type)
 import Data.List (partition)
-import Data.Maybe
+import Data.Maybe (fromJust)
 import qualified Data.SBV as SBV
 import Data.SBV.Control (Query)
 import qualified Data.SBV.Control as SBVC
-import GHC.TypeNats
+import GHC.TypeNats (KnownNat, Nat)
 import Grisette.Backend.SBV.Data.SMT.Lowering
-import Grisette.Core.Data.BV
-import Grisette.Core.Data.Class.Bool
+  ( SymBiMap,
+    lowerSinglePrim,
+    lowerSinglePrimCached,
+    parseModel,
+  )
+import Grisette.Core.Data.BV (IntN, WordN)
+import Grisette.Core.Data.Class.Bool (LogicalOp (nots, (&&~)))
 import Grisette.Core.Data.Class.CEGISSolver
-import Grisette.Core.Data.Class.Evaluate
+  ( CEGISCondition (CEGISCondition),
+    CEGISSolver (cegisMultiInputs),
+  )
+import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ExtractSymbolics
+  ( ExtractSymbolics (extractSymbolics),
+  )
 import Grisette.Core.Data.Class.ModelOps
-import Grisette.Core.Data.Class.Solvable
-import Grisette.Core.Data.Class.Solver
+  ( ModelOps (exact, exceptFor),
+    SymbolSetOps (isEmptySet),
+  )
+import Grisette.Core.Data.Class.Solvable (Solvable (con))
+import Grisette.Core.Data.Class.Solver (Solver (solve, solveAll, solveMulti))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SomeTypedSymbol (SomeTypedSymbol),
+    Term,
+    type (-->),
+  )
 import Grisette.IR.SymPrim.Data.Prim.Model as PM
+  ( Model,
+    SymbolSet (unSymbolSet),
+    equation,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
-import Grisette.IR.SymPrim.Data.SymPrim
-import Grisette.IR.SymPrim.Data.TabularFun
+  ( pevalNotTerm,
+    pevalOrTerm,
+  )
+import Grisette.IR.SymPrim.Data.SymPrim (SymBool (SymBool))
+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
 import Language.Haskell.TH.Syntax (Lift)
 
 -- $setup

diff --git a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot
@@ -13,12 +13,14 @@ module Grisette.Backend.SBV.Data.SMT.Solving
   )
 where
 
-import Data.Kind
+import Data.Kind (Type)
 import qualified Data.SBV as SBV
-import GHC.TypeNats
-import Grisette.Core.Data.BV
+import GHC.TypeNats (KnownNat, Nat)
+import Grisette.Core.Data.BV (IntN, WordN)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-import Grisette.IR.SymPrim.Data.TabularFun
+  ( type (-->),
+  )
+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
 
 type Aux :: Bool -> Nat -> Type
 type family Aux o n where

diff --git a/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs b/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs
@@ -19,11 +19,15 @@ module Grisette.Backend.SBV.Data.SMT.SymBiMap
   )
 where
 
-import Data.Dynamic
+import Data.Dynamic (Dynamic)
 import qualified Data.HashMap.Strict as M
-import GHC.Stack
+import GHC.Stack (HasCallStack)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
+  ( SomeTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SomeTypedSymbol,
+  )
 
 data SymBiMap = SymBiMap
   { biMapToSBV :: M.HashMap SomeTerm Dynamic,