summaryrefslogtreecommitdiff
path: root/compiler/utils
diff options
context:
space:
mode:
authorSebastian Graf <sebastian.graf@kit.edu>2019-05-16 18:49:02 +0200
committerMarge Bot <ben+marge-bot@smart-cactus.org>2019-09-16 13:33:05 -0400
commit7915afc6bb9539a4534db99aeb6616a6d145918a (patch)
tree41b7c731d20754b2ce9f73488b7aaeff7ec80565 /compiler/utils
parentb5ae3868db62228e7a75a9f1f66a9b05a4cf3277 (diff)
downloadhaskell-7915afc6bb9539a4534db99aeb6616a6d145918a.tar.gz
Encode shape information in `PmOracle`
Previously, we had an elaborate mechanism for selecting the warnings to generate in the presence of different `COMPLETE` matching groups that, albeit finely-tuned, produced wrong results from an end user's perspective in some cases (#13363). The underlying issue is that at the point where the `ConVar` case has to commit to a particular `COMPLETE` group, there's not enough information to do so and the status quo was to just enumerate all possible complete sets nondeterministically. The `getResult` function would then pick the outcome according to metrics defined in accordance to the user's guide. But crucially, it lacked knowledge about the order in which affected clauses appear, leading to the surprising behavior in #13363. In !1010 we taught the term oracle to reason about literal values a variable can certainly not take on. This MR extends that idea to `ConLike`s and thereby fixes #13363: Instead of committing to a particular `COMPLETE` group in the `ConVar` case, we now split off the matching constructor incrementally and record the newly covered case as a refutable shape in the oracle. Whenever the set of refutable shapes covers any `COMPLETE` set, the oracle recognises vacuosity of the uncovered set. This patch goes a step further: Since at this point the information in value abstractions is merely a cut down representation of what the oracle knows, value abstractions degenerate to a single `Id`, the semantics of which is determined by the oracle state `Delta`. Value vectors become lists of `[Id]` given meaning to by a single `Delta`, value set abstractions (of which the uncovered set is an instance) correspond to a union of `Delta`s which instantiate the same `[Id]` (akin to models of formula). Fixes #11528 #13021, #13363, #13965, #14059, #14253, #14851, #15753, #17096, #17149 ------------------------- Metric Decrease: ManyAlternatives T11195 -------------------------
Diffstat (limited to 'compiler/utils')
-rw-r--r--compiler/utils/Binary.hs1
-rw-r--r--compiler/utils/ListSetOps.hs9
-rw-r--r--compiler/utils/ListT.hs79
-rw-r--r--compiler/utils/Outputable.hs2
-rw-r--r--compiler/utils/Util.hs15
5 files changed, 12 insertions, 94 deletions
diff --git a/compiler/utils/Binary.hs b/compiler/utils/Binary.hs
index 7a3b7a1472..164549fe58 100644
--- a/compiler/utils/Binary.hs
+++ b/compiler/utils/Binary.hs
@@ -935,7 +935,6 @@ putTypeRep bh (Fun arg res) = do
put_ bh (3 :: Word8)
putTypeRep bh arg
putTypeRep bh res
-putTypeRep _ _ = fail "Binary.putTypeRep: Impossible"
getSomeTypeRep :: BinHandle -> IO SomeTypeRep
getSomeTypeRep bh = do
diff --git a/compiler/utils/ListSetOps.hs b/compiler/utils/ListSetOps.hs
index 8078d5603e..a8b717df00 100644
--- a/compiler/utils/ListSetOps.hs
+++ b/compiler/utils/ListSetOps.hs
@@ -14,7 +14,7 @@ module ListSetOps (
Assoc, assoc, assocMaybe, assocUsing, assocDefault, assocDefaultUsing,
-- Duplicate handling
- hasNoDups, removeDups, findDupsEq, insertNoDup,
+ hasNoDups, removeDups, findDupsEq,
equivClasses,
-- Indexing
@@ -178,10 +178,3 @@ findDupsEq _ [] = []
findDupsEq eq (x:xs) | null eq_xs = findDupsEq eq xs
| otherwise = (x :| eq_xs) : findDupsEq eq neq_xs
where (eq_xs, neq_xs) = partition (eq x) xs
-
--- | \( O(n) \). @'insertNoDup' x xs@ treats @xs@ as a set, inserting @x@ only
--- when an equal element couldn't be found in @xs@.
-insertNoDup :: (Eq a) => a -> [a] -> [a]
-insertNoDup x set
- | elem x set = set
- | otherwise = x:set
diff --git a/compiler/utils/ListT.hs b/compiler/utils/ListT.hs
deleted file mode 100644
index 66e52ed9f4..0000000000
--- a/compiler/utils/ListT.hs
+++ /dev/null
@@ -1,79 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-
--------------------------------------------------------------------------
--- |
--- Module : Control.Monad.Logic
--- Copyright : (c) Dan Doel
--- License : BSD3
---
--- Maintainer : dan.doel@gmail.com
--- Stability : experimental
--- Portability : non-portable (multi-parameter type classes)
---
--- A backtracking, logic programming monad.
---
--- Adapted from the paper
--- /Backtracking, Interleaving, and Terminating
--- Monad Transformers/, by
--- Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry
--- (<http://www.cs.rutgers.edu/~ccshan/logicprog/ListT-icfp2005.pdf>).
--------------------------------------------------------------------------
-
-module ListT (
- ListT(..),
- runListT,
- select,
- fold
- ) where
-
-import GhcPrelude
-
-import Control.Applicative
-
-import Control.Monad
-import Control.Monad.Fail as MonadFail
-
--------------------------------------------------------------------------
--- | A monad transformer for performing backtracking computations
--- layered over another monad 'm'
-newtype ListT m a =
- ListT { unListT :: forall r. (a -> m r -> m r) -> m r -> m r }
- deriving (Functor)
-
-select :: Monad m => [a] -> ListT m a
-select xs = foldr (<|>) mzero (map pure xs)
-
-fold :: ListT m a -> (a -> m r -> m r) -> m r -> m r
-fold = runListT
-
--------------------------------------------------------------------------
--- | Runs a ListT computation with the specified initial success and
--- failure continuations.
-runListT :: ListT m a -> (a -> m r -> m r) -> m r -> m r
-runListT = unListT
-
-instance Applicative (ListT f) where
- pure a = ListT $ \sk fk -> sk a fk
- f <*> a = ListT $ \sk fk -> unListT f (\g fk' -> unListT a (sk . g) fk') fk
-
-instance Alternative (ListT f) where
- empty = ListT $ \_ fk -> fk
- f1 <|> f2 = ListT $ \sk fk -> unListT f1 sk (unListT f2 sk fk)
-
-instance Monad (ListT m) where
- m >>= f = ListT $ \sk fk -> unListT m (\a fk' -> unListT (f a) sk fk') fk
-#if !MIN_VERSION_base(4,13,0)
- fail = MonadFail.fail
-#endif
-
-instance MonadFail.MonadFail (ListT m) where
- fail _ = ListT $ \_ fk -> fk
-
-instance MonadPlus (ListT m) where
- mzero = ListT $ \_ fk -> fk
- m1 `mplus` m2 = ListT $ \sk fk -> unListT m1 sk (unListT m2 sk fk)
diff --git a/compiler/utils/Outputable.hs b/compiler/utils/Outputable.hs
index a5306faaa4..cd3e2a5f5b 100644
--- a/compiler/utils/Outputable.hs
+++ b/compiler/utils/Outputable.hs
@@ -1205,7 +1205,7 @@ pprTraceM str doc = pprTrace str doc (pure ())
-- | @pprTraceWith desc f x@ is equivalent to @pprTrace desc (f x) x@.
-- This allows you to print details from the returned value as well as from
-- ambient variables.
-pprTraceWith :: Outputable a => String -> (a -> SDoc) -> a -> a
+pprTraceWith :: String -> (a -> SDoc) -> a -> a
pprTraceWith desc f x = pprTrace desc (f x) x
-- | @pprTraceIt desc x@ is equivalent to @pprTrace desc (ppr x) x@
diff --git a/compiler/utils/Util.hs b/compiler/utils/Util.hs
index 51812cca75..d6cea5ca8d 100644
--- a/compiler/utils/Util.hs
+++ b/compiler/utils/Util.hs
@@ -14,6 +14,9 @@ module Util (
ghciTablesNextToCode,
isWindowsHost, isDarwinHost,
+ -- * Miscellaneous higher-order functions
+ applyWhen, nTimes,
+
-- * General list processing
zipEqual, zipWithEqual, zipWith3Equal, zipWith4Equal,
zipLazy, stretchZipWith, zipWithAndUnzip, zipAndUnzip,
@@ -57,9 +60,6 @@ module Util (
takeList, dropList, splitAtList, split,
dropTail, capitalise,
- -- * For loop
- nTimes,
-
-- * Sorting
sortWith, minWith, nubSort, ordNub,
@@ -222,12 +222,17 @@ isDarwinHost = False
{-
************************************************************************
* *
-\subsection{A for loop}
+\subsection{Miscellaneous higher-order functions}
* *
************************************************************************
-}
--- | Compose a function with itself n times. (nth rather than twice)
+-- | Apply a function iff some condition is met.
+applyWhen :: Bool -> (a -> a) -> a -> a
+applyWhen True f x = f x
+applyWhen _ _ x = x
+
+-- | A for loop: Compose a function with itself n times. (nth rather than twice)
nTimes :: Int -> (a -> a) -> (a -> a)
nTimes 0 _ = id
nTimes 1 f = f