Phadej ghc 8.4

CHANGES.md

@@ -2,8 +2,11 @@
 
 ## NEXT
 
+## 0.8.0.1 
+
 - Support for "existential binders", see `tests/pos/ebind-*.fq` for example.
   This only works with `--eliminate`.
+- Move to GHC 8.4.3 
 
 ## 0.7.0.0
 

liquid-fixpoint.cabal

@@ -1,5 +1,5 @@
 name:                liquid-fixpoint
-version:             0.7.0.7
+version:             0.8.0.1
 Copyright:           2010-17 Ranjit Jhala, University of California, San Diego.
 synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 homepage:            https://github.com/ucsd-progsys/liquid-fixpoint
@@ -53,7 +53,7 @@ Executable fixpoint
   if flag(devel)
     ghc-options: -Werror
   hs-source-dirs: bin
-  Build-Depends: base >=4.8.1.0 && <5
+  Build-Depends: base >=4.9.1.0 && <5
                , liquid-fixpoint
 
 Library
@@ -85,7 +85,6 @@ Library
                    Language.Fixpoint.Graph.Partition,
                    Language.Fixpoint.Graph.Deps,
                    Language.Fixpoint.Graph,
-                   -- Language.Fixpoint.Congruence.Closure,
                    Language.Fixpoint.Defunctionalize,
                    Language.Fixpoint.Smt.Types,
                    Language.Fixpoint.Smt.Bitvector,
@@ -110,9 +109,13 @@ Library
                    Language.Fixpoint.Solver.Instantiate,
                    Language.Fixpoint.Solver.Sanitize,
                    Language.Fixpoint.Utils.Statistics,
-                   Language.Fixpoint.Solver.Solve
+                   Language.Fixpoint.Solver.Solve,
 
-  Build-Depends: base >=4.8.1.0 && <5
+                   Text.PrettyPrint.HughesPJ.Compat
+
+  Other-Modules: Paths_liquid_fixpoint
+
+  Build-Depends: base >=4.9.1.0 && <5
                , array
                , async
                , attoparsec
@@ -131,7 +134,7 @@ Library
                , intern
                , mtl
                , parsec
-               , pretty
+               , pretty >=1.1.3.1
                , boxes
                , parallel
                , process
@@ -148,8 +151,9 @@ Library
                , time
                , parallel-io
 
-  if impl(ghc >= 7.10.2)
-    Build-Depends: located-base
+  -- unconditionally depend on located-base
+  Build-Depends: located-base
+
   if !os(windows)
     Build-Depends: ascii-progress >= 0.3
     hs-source-dirs: unix
@@ -164,21 +168,23 @@ test-suite test
   if flag(devel)
     ghc-options:    -Werror
   main-is:          test.hs
-  build-depends:    base >= 4.8 && < 5,
+  Other-Modules:    Paths_liquid_fixpoint
+  build-depends:    base >= 4.9.1.0 && < 5,
                     directory,
                     filepath,
                     process,
                     stm >= 2.4,
                     containers >= 0.5,
-                    mtl >= 2.1,
-                    transformers >= 0.3,
+                    mtl >= 2.2.2,
+                    transformers >= 0.5,
                     tasty >= 0.10,
                     tasty-hunit,
-                    tasty-rerun >= 1.1,
+                    tasty-rerun >= 1.1.12,
                     tasty-ant-xml,
                     tasty-hunit >= 0.9,
                     text
 
+
 test-suite testparser
   default-language: Haskell98
   type:             exitcode-stdio-1.0
@@ -187,17 +193,40 @@ test-suite testparser
   if flag(devel)
     ghc-options:    -Werror
   main-is:          testParser.hs
-  build-depends:    base >= 4.8 && < 5,
+  build-depends:    base >= 4.9.1.0 && < 5,
                     directory,
                     filepath,
                     tasty >= 0.10,
                     tasty-hunit,
                     tasty-rerun >= 1.1,
                     tasty-ant-xml,
                     tasty-hunit >= 0.9,
-                    text
+                    text,
+                    liquid-fixpoint
   if flag(devel)
     hs-source-dirs:   tests src
+    other-modules:
+                 Language.Fixpoint.Misc
+                 Language.Fixpoint.Parse
+                 Language.Fixpoint.Smt.Bitvector
+                 Language.Fixpoint.Smt.Types
+                 Language.Fixpoint.Types
+                 Language.Fixpoint.Types.Config
+                 Language.Fixpoint.Types.Constraints
+                 Language.Fixpoint.Types.Environments
+                 Language.Fixpoint.Types.Errors
+                 Language.Fixpoint.Types.Names
+                 Language.Fixpoint.Types.PrettyPrint
+                 Language.Fixpoint.Types.Refinements
+                 Language.Fixpoint.Types.Sorts
+                 Language.Fixpoint.Types.Spans
+                 Language.Fixpoint.Types.Substitutions
+                 Language.Fixpoint.Types.Theories
+                 Language.Fixpoint.Types.Triggers
+                 Language.Fixpoint.Types.Utils
+                 Language.Fixpoint.Utils.Files
+                 Text.PrettyPrint.HughesPJ.Compat
+
     build-depends:
                  array
                , async

src/Language/Fixpoint/Graph/Deps.hs

@@ -28,6 +28,7 @@ module Language.Fixpoint.Graph.Deps (
 
 import           Prelude hiding (init)
 import           Data.Maybe                       (mapMaybe, fromMaybe)
+import           Data.Semigroup                   (Semigroup (..))
 import           Data.Tree (flatten)
 import           Language.Fixpoint.Misc
 import           Language.Fixpoint.Utils.Files
@@ -46,7 +47,7 @@ import qualified Data.HashMap.Strict                  as M
 import qualified Data.Graph                           as G
 import           Data.Function (on)
 import           Data.Hashable
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 import           Debug.Trace (trace)
 
 --------------------------------------------------------------------------------
@@ -289,9 +290,12 @@ instance PPrint (Elims a) where
     where
       ppSize     = pprint . S.size
 
+instance (Eq a, Hashable a) => Semigroup (Elims a) where
+  Deps d1 n1 <> Deps d2 n2 = Deps (S.union d1 d2) (S.union n1 n2)
+
 instance (Eq a, Hashable a) => Monoid (Elims a) where
-  mempty                            = Deps S.empty S.empty
-  mappend (Deps d1 n1) (Deps d2 n2) = Deps (S.union d1 d2) (S.union n1 n2)
+  mempty  = Deps S.empty S.empty
+  mappend = (<>)
 
 dCut, dNonCut :: (Hashable a) => a -> Elims a
 dNonCut v = Deps S.empty (S.singleton v)
@@ -551,7 +555,7 @@ instance PTable Stats where
 
 graphStats :: F.TaggedC c a => Config -> F.GInfo c a -> Stats
 graphStats cfg si = Stats {
-    stNumKVCuts   = S.size $ F.tracepp "CUTS:" (depCuts d)
+    stNumKVCuts   = S.size (depCuts d)
   , stNumKVNonLin = S.size  nlks
   , stNumKVTotal  = S.size (depCuts d) + S.size (depNonCuts d)
   , stIsReducible = isReducible si

src/Language/Fixpoint/Graph/Partition.hs

@@ -38,7 +38,8 @@ import qualified Data.HashMap.Strict                  as M
 -- import           Data.Function (on)
 import           Data.Maybe                     (fromMaybe)
 import           Data.Hashable
-import           Text.PrettyPrint.HughesPJ
+import           Data.Semigroup                 (Semigroup (..))
+import           Text.PrettyPrint.HughesPJ.Compat
 import           Data.List (sortBy)
 -- import qualified Data.HashSet              as S
 
@@ -55,12 +56,15 @@ data CPart c a = CPart { pws :: !(M.HashMap F.KVar (F.WfC a))
                        , pcm :: !(M.HashMap Integer (c a))
                        }
 
+instance Semigroup (CPart c a) where
+  l <> r = CPart { pws = pws l <> pws r
+                 , pcm = pcm l <> pcm r
+                 }
+
 instance Monoid (CPart c a) where
    mempty      = CPart mempty mempty
-   mappend l r = CPart { pws = pws l `mappend` pws r
-                       , pcm = pcm l `mappend` pcm r
-                       }
-
+   mappend     = (<>)
+
 --------------------------------------------------------------------------------
 -- | Multicore info ------------------------------------------------------------
 --------------------------------------------------------------------------------

src/Language/Fixpoint/Graph/Types.hs

@@ -50,7 +50,7 @@ module Language.Fixpoint.Graph.Types (
 
 import           GHC.Generics              (Generic)
 import           Data.Hashable
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 
 import           Language.Fixpoint.Misc         -- hiding (group)
 import           Language.Fixpoint.Types.PrettyPrint
@@ -73,8 +73,8 @@ data CVertex = KVar  !KVar    -- ^ real kvar vertex
 instance PPrint CVertex where
   pprintTidy _ (KVar k)  = doubleQuotes $ pprint $ kv k
   pprintTidy _ (EBind s)  = doubleQuotes $ pprint $ s
-  pprintTidy _ (Cstr i)  = text "id_" <> pprint i
-  pprintTidy _ (DKVar k) = pprint k   <> text "*"
+  pprintTidy _ (Cstr i)  = text "id_" <-> pprint i
+  pprintTidy _ (DKVar k) = pprint k   <-> text "*"
 
 
 instance Hashable CVertex

src/Language/Fixpoint/Misc.hs

@@ -18,30 +18,28 @@ import           Control.Arrow                    (second)
 import           Control.Monad                    (when, forM_, filterM)
 import qualified Data.HashMap.Strict              as M
 import qualified Data.List                        as L
+import qualified Data.HashSet                     as S
 import           Data.Tuple                       (swap)
 import           Data.Maybe
 import           Data.Array                       hiding (indices)
 import           Data.Function                    (on)
 import qualified Data.Graph                       as G
 import qualified Data.Tree                        as T
+
 import           Data.Unique
 import           Debug.Trace                      (trace)
 import           System.Console.ANSI
 import           System.Console.CmdArgs.Verbosity (whenLoud)
 import           System.Process                   (system)
 import           System.Directory                 (createDirectoryIfMissing)
 import           System.FilePath                  (takeDirectory)
-import           Text.PrettyPrint.HughesPJ        hiding (first)
+import           Text.PrettyPrint.HughesPJ.Compat
 import           System.IO                        (stdout, hFlush )
 import           System.Exit                      (ExitCode)
 import           Control.Concurrent.Async
 
-
-#ifdef MIN_VERSION_located_base
-import Prelude hiding (error, undefined)
-import GHC.Err.Located
+import Prelude hiding (undefined)
 import GHC.Stack
-#endif
 
 type (|->) a b = M.HashMap a b
 
@@ -58,6 +56,15 @@ traceShow s x = trace ("\nTrace: [" ++ s ++ "] : " ++ show x)  x
 hashMapToAscList :: Ord a => M.HashMap a b -> [(a, b)]
 hashMapToAscList = L.sortBy (compare `on` fst) . M.toList
 
+findNearest :: (Ord i, Num i) => i -> [(i, a)] -> Maybe a 
+findNearest key kvs = argMin [ (abs (key - k), v) | (k, v) <- kvs ]
+
+argMin :: (Ord k) => [(k, v)] -> Maybe v 
+argMin = fmap snd . headMb . L.sortBy (compare `on` fst)
+
+headMb :: [a] -> Maybe a 
+headMb []    = Nothing 
+headMb (x:_) = Just x
 ---------------------------------------------------------------
 -- | Unique Int -----------------------------------------------
 ---------------------------------------------------------------
@@ -139,10 +146,11 @@ wrap l r s = l ++ s ++ r
 repeats :: Int -> [a] -> [a]
 repeats n  = concat . replicate n
 
-#ifdef MIN_VERSION_located_base
-errorstar :: (?callStack :: CallStack) => String -> a
-#endif
 
+errorP :: String -> String -> a
+errorP p s = error (p ++ s)   
+
+errorstar :: (?callStack :: CallStack) => String -> a
 errorstar  = error . wrap (stars ++ "\n") (stars ++ "\n")
   where
     stars = repeats 3 $ wrapStars "ERROR"
@@ -159,15 +167,9 @@ thd3 (_,_,x) = x
 secondM :: Functor f => (b -> f c) -> (a, b) -> f (a, c)
 secondM act (x, y) = (x,) <$> act y
 
-#ifdef MIN_VERSION_located_base
 mlookup    :: (?callStack :: CallStack, Eq k, Show k, Hashable k) => M.HashMap k v -> k -> v
 safeLookup :: (?callStack :: CallStack, Eq k, Hashable k) => String -> k -> M.HashMap k v -> v
 mfromJust  :: (?callStack :: CallStack) => String -> Maybe a -> a
-#else
-mlookup    :: (Eq k, Show k, Hashable k) => M.HashMap k v -> k -> v
-safeLookup :: (Eq k, Hashable k) => String -> k -> M.HashMap k v -> v
-mfromJust  :: String -> Maybe a -> a
-#endif
 
 mlookup m k = fromMaybe err $ M.lookup k m
   where
@@ -206,19 +208,21 @@ hashNub = M.keys . M.fromList . fmap (, ())
 
 sortNub :: (Ord a) => [a] -> [a]
 sortNub = nubOrd . L.sort
-  where
-    nubOrd (x:t@(y:_))
-      | x == y    = nubOrd t
-      | otherwise = x : nubOrd t
-    nubOrd xs     = xs
+
+nubOrd :: (Eq a) => [a] -> [a]
+nubOrd (x:t@(y:_))
+  | x == y    = nubOrd t
+  | otherwise = x : nubOrd t
+nubOrd xs     = xs
+
+hashNubWith :: (Eq b, Hashable b) => (a -> b) -> [a] -> [a]
+hashNubWith f xs = M.elems $ M.fromList [ (f x, x) | x <- xs ]
 
 duplicates :: (Eq k, Hashable k) => [k] -> [k]
 duplicates xs = [ x | (x, n) <- count xs, 1 < n ]
 
-#ifdef MIN_VERSION_located_base
 safeZip :: (?callStack :: CallStack) => String -> [a] -> [b] -> [(a,b)]
 safeZipWith :: (?callStack :: CallStack) => String -> (a -> b -> c) -> [a] -> [b] -> [c]
-#endif
 
 safeZip msg xs ys
   | nxs == nys
@@ -241,21 +245,12 @@ safeZipWith msg f xs ys
 {-@ type ListNE a = {v:[a] | 0 < len v} @-}
 type ListNE a = [a]
 
-#ifdef MIN_VERSION_located_base
 safeHead   :: (?callStack :: CallStack) => String -> ListNE a -> a
 safeLast   :: (?callStack :: CallStack) => String -> ListNE a -> a
 safeInit   :: (?callStack :: CallStack) => String -> ListNE a -> [a]
 safeUncons :: (?callStack :: CallStack) => String -> ListNE a -> (a, [a])
 safeUnsnoc :: (?callStack :: CallStack) => String -> ListNE a -> ([a], a)
 safeFromList :: (?callStack :: CallStack, Eq k, Hashable k, Show k) => String -> [(k, v)] -> M.HashMap k v
-#else
-safeHead   :: String -> ListNE a -> a
-safeLast   :: String -> ListNE a -> a
-safeInit   :: String -> ListNE a -> [a]
-safeUncons :: String -> ListNE a -> (a, [a])
-safeUnsnoc :: String -> ListNE a -> ([a], a)
-safeFromList :: (Eq k, Hashable k, Show k) => String -> [(k, v)] -> M.HashMap k v
-#endif
 
 safeFromList msg kvs = applyNonNull (M.fromList kvs) err (dups kvs)
   where
@@ -288,7 +283,7 @@ applyNonNull _   f xs = f xs
 
 arrow, dcolon :: Doc
 arrow              = text "->"
-dcolon             = colon <> colon
+dcolon             = colon <-> colon
 
 intersperse :: Doc -> [Doc] -> Doc
 intersperse d ds   = hsep $ punctuate d ds
@@ -334,6 +329,10 @@ mapEither f (x:xs) = case f x of
                      where
                        (ys, zs) = mapEither f xs
 
+isRight :: Either a b -> Bool 
+isRight (Right _) = True 
+isRight _         = False
+
 componentsWith :: (Ord c) => (a -> [(b, c, [c])]) -> a -> [[b]]
 componentsWith eF x = map (fst3 . f) <$> vss
   where
@@ -436,3 +435,10 @@ revMapM f          = go []
   where
     go !acc []     = return (reverse acc)
     go !acc (x:xs) = do {!y <- f x; go (y:acc) xs}
+
+-- Null if first is a subset of second
+nubDiff :: (Eq a, Hashable a) => [a] -> [a] -> S.HashSet a 
+nubDiff a b = a' `S.difference` b'
+  where
+    a' = S.fromList a
+    b' = S.fromList b