Fix Uncovered set of literal patterns
[ghc.git] / compiler / deSugar / TmOracle.hs
1 {-
2 Author: George Karachalias <george.karachalias@cs.kuleuven.be>
3
4 The term equality oracle. The main export of the module is function `tmOracle'.
5 -}
6
7 {-# LANGUAGE CPP, MultiWayIf #-}
8
9 module TmOracle (
10
11 -- re-exported from PmExpr
12 PmExpr(..), PmLit(..), SimpleEq, ComplexEq, PmVarEnv, falsePmExpr,
13 eqPmLit, filterComplex, isNotPmExprOther, runPmPprM, lhsExprToPmExpr,
14 hsExprToPmExpr, pprPmExprWithParens,
15
16 -- the term oracle
17 tmOracle, TmState, initialTmState, solveOneEq, extendSubst, canDiverge,
18
19 -- misc.
20 toComplex, exprDeepLookup, pmLitType, flattenPmVarEnv
21 ) where
22
23 #include "HsVersions.h"
24
25 import GhcPrelude
26
27 import PmExpr
28
29 import Id
30 import Name
31 import Type
32 import HsLit
33 import TcHsSyn
34 import MonadUtils
35 import Util
36 import Outputable
37
38 import NameEnv
39
40 {-
41 %************************************************************************
42 %* *
43 The term equality oracle
44 %* *
45 %************************************************************************
46 -}
47
48 -- | The type of substitutions.
49 type PmVarEnv = NameEnv PmExpr
50
51 -- | The environment of the oracle contains
52 -- 1. A Bool (are there any constraints we cannot handle? (PmExprOther)).
53 -- 2. A substitution we extend with every step and return as a result.
54 type TmOracleEnv = (Bool, PmVarEnv)
55
56 -- | Check whether a constraint (x ~ BOT) can succeed,
57 -- given the resulting state of the term oracle.
58 canDiverge :: Name -> TmState -> Bool
59 canDiverge x (standby, (_unhandled, env))
60 -- If the variable seems not evaluated, there is a possibility for
61 -- constraint x ~ BOT to be satisfiable.
62 | PmExprVar y <- varDeepLookup env x -- seems not forced
63 -- If it is involved (directly or indirectly) in any equality in the
64 -- worklist, we can assume that it is already indirectly evaluated,
65 -- as a side-effect of equality checking. If not, then we can assume
66 -- that the constraint is satisfiable.
67 = not $ any (isForcedByEq x) standby || any (isForcedByEq y) standby
68 -- Variable x is already in WHNF so the constraint is non-satisfiable
69 | otherwise = False
70
71 where
72 isForcedByEq :: Name -> ComplexEq -> Bool
73 isForcedByEq y (e1, e2) = varIn y e1 || varIn y e2
74
75 -- | Check whether a variable is in the free variables of an expression
76 varIn :: Name -> PmExpr -> Bool
77 varIn x e = case e of
78 PmExprVar y -> x == y
79 PmExprCon _ es -> any (x `varIn`) es
80 PmExprLit _ -> False
81 PmExprEq e1 e2 -> (x `varIn` e1) || (x `varIn` e2)
82 PmExprOther _ -> False
83
84 -- | Flatten the DAG (Could be improved in terms of performance.).
85 flattenPmVarEnv :: PmVarEnv -> PmVarEnv
86 flattenPmVarEnv env = mapNameEnv (exprDeepLookup env) env
87
88 -- | The state of the term oracle (includes complex constraints that cannot
89 -- progress unless we get more information).
90 type TmState = ([ComplexEq], TmOracleEnv)
91
92 -- | Initial state of the oracle.
93 initialTmState :: TmState
94 initialTmState = ([], (False, emptyNameEnv))
95
96 -- | Solve a complex equality (top-level).
97 solveOneEq :: TmState -> ComplexEq -> Maybe TmState
98 solveOneEq solver_env@(_,(_,env)) complex
99 = solveComplexEq solver_env -- do the actual *merging* with existing state
100 $ simplifyComplexEq -- simplify as much as you can
101 $ applySubstComplexEq env complex -- replace everything we already know
102
103 -- | Solve a complex equality.
104 -- Nothing => definitely unsatisfiable
105 -- Just tms => I have added the complex equality and added
106 -- it to the tmstate; the result may or may not be
107 -- satisfiable
108 solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
109 solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
110 -- We cannot do a thing about these cases
111 (PmExprOther _,_) -> Just (standby, (True, env))
112 (_,PmExprOther _) -> Just (standby, (True, env))
113
114 (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
115 -- See Note [Undecidable Equality for Overloaded Literals]
116 True -> Just solver_state
117 False -> Nothing
118
119 (PmExprCon c1 ts1, PmExprCon c2 ts2)
120 | c1 == c2 -> foldlM solveComplexEq solver_state (zip ts1 ts2)
121 | otherwise -> Nothing
122 (PmExprCon _ [], PmExprEq t1 t2)
123 | isTruePmExpr e1 -> solveComplexEq solver_state (t1, t2)
124 | isFalsePmExpr e1 -> Just (eq:standby, (unhandled, env))
125 (PmExprEq t1 t2, PmExprCon _ [])
126 | isTruePmExpr e2 -> solveComplexEq solver_state (t1, t2)
127 | isFalsePmExpr e2 -> Just (eq:standby, (unhandled, env))
128
129 (PmExprVar x, PmExprVar y)
130 | x == y -> Just solver_state
131 | otherwise -> extendSubstAndSolve x e2 solver_state
132
133 (PmExprVar x, _) -> extendSubstAndSolve x e2 solver_state
134 (_, PmExprVar x) -> extendSubstAndSolve x e1 solver_state
135
136 (PmExprEq _ _, PmExprEq _ _) -> Just (eq:standby, (unhandled, env))
137
138 _ -> WARN( True, text "solveComplexEq: Catch all" <+> ppr eq )
139 Just (standby, (True, env)) -- I HATE CATCH-ALLS
140
141 -- | Extend the substitution and solve the (possibly updated) constraints.
142 extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState
143 extendSubstAndSolve x e (standby, (unhandled, env))
144 = foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed)
145 where
146 -- Apply the substitution to the worklist and partition them to the ones
147 -- that had some progress and the rest. Then, recurse over the ones that
148 -- had some progress. Careful about performance:
149 -- See Note [Representation of Term Equalities] in deSugar/Check.hs
150 (changed, unchanged) = partitionWith (substComplexEq x e) standby
151 new_incr_state = (unchanged, (unhandled, extendNameEnv env x e))
152
153 -- | When we know that a variable is fresh, we do not actually have to
154 -- check whether anything changes, we know that nothing does. Hence,
155 -- `extendSubst` simply extends the substitution, unlike what
156 -- `extendSubstAndSolve` does.
157 extendSubst :: Id -> PmExpr -> TmState -> TmState
158 extendSubst y e (standby, (unhandled, env))
159 | isNotPmExprOther simpl_e
160 = (standby, (unhandled, extendNameEnv env x simpl_e))
161 | otherwise = (standby, (True, env))
162 where
163 x = idName y
164 simpl_e = fst $ simplifyPmExpr $ exprDeepLookup env e
165
166 -- | Simplify a complex equality.
167 simplifyComplexEq :: ComplexEq -> ComplexEq
168 simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2)
169
170 -- | Simplify an expression. The boolean indicates if there has been any
171 -- simplification or if the operation was a no-op.
172 simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
173 -- See Note [Deep equalities]
174 simplifyPmExpr e = case e of
175 PmExprCon c ts -> case mapAndUnzip simplifyPmExpr ts of
176 (ts', bs) -> (PmExprCon c ts', or bs)
177 PmExprEq t1 t2 -> simplifyEqExpr t1 t2
178 _other_expr -> (e, False) -- the others are terminals
179
180 -- | Simplify an equality expression. The equality is given in parts.
181 simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
182 -- See Note [Deep equalities]
183 simplifyEqExpr e1 e2 = case (e1, e2) of
184 -- Varables
185 (PmExprVar x, PmExprVar y)
186 | x == y -> (truePmExpr, True)
187
188 -- Literals
189 (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
190 -- See Note [Undecidable Equality for Overloaded Literals]
191 True -> (truePmExpr, True)
192 False -> (falsePmExpr, True)
193
194 -- Can potentially be simplified
195 (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
196 ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
197 ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
198 ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
199 (_, PmExprEq {}) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
200 ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
201 ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
202 ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
203
204 -- Constructors
205 (PmExprCon c1 ts1, PmExprCon c2 ts2)
206 | c1 == c2 ->
207 let (ts1', bs1) = mapAndUnzip simplifyPmExpr ts1
208 (ts2', bs2) = mapAndUnzip simplifyPmExpr ts2
209 (tss, _bss) = zipWithAndUnzip simplifyEqExpr ts1' ts2'
210 worst_case = PmExprEq (PmExprCon c1 ts1') (PmExprCon c2 ts2')
211 in if | not (or bs1 || or bs2) -> (worst_case, False) -- no progress
212 | all isTruePmExpr tss -> (truePmExpr, True)
213 | any isFalsePmExpr tss -> (falsePmExpr, True)
214 | otherwise -> (worst_case, False)
215 | otherwise -> (falsePmExpr, True)
216
217 -- We cannot do anything about the rest..
218 _other_equality -> (original, False)
219
220 where
221 original = PmExprEq e1 e2 -- reconstruct equality
222
223 -- | Apply an (un-flattened) substitution to a simple equality.
224 applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
225 applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2)
226
227 -- | Apply an (un-flattened) substitution to a variable.
228 varDeepLookup :: PmVarEnv -> Name -> PmExpr
229 varDeepLookup env x
230 | Just e <- lookupNameEnv env x = exprDeepLookup env e -- go deeper
231 | otherwise = PmExprVar x -- terminal
232 {-# INLINE varDeepLookup #-}
233
234 -- | Apply an (un-flattened) substitution to an expression.
235 exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
236 exprDeepLookup env (PmExprVar x) = varDeepLookup env x
237 exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
238 exprDeepLookup env (PmExprEq e1 e2) = PmExprEq (exprDeepLookup env e1)
239 (exprDeepLookup env e2)
240 exprDeepLookup _ other_expr = other_expr -- PmExprLit, PmExprOther
241
242 -- | External interface to the term oracle.
243 tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
244 tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs
245
246 -- | Type of a PmLit
247 pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :(
248 pmLitType (PmSLit lit) = hsLitType lit
249 pmLitType (PmOLit _ lit) = overLitType lit
250
251 {- Note [Deep equalities]
252 ~~~~~~~~~~~~~~~~~~~~~~~~~
253 Solving nested equalities is the most difficult part. The general strategy
254 is the following:
255
256 * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
257 (e1 ~ e2) and then treated recursively.
258
259 * Equalities of the form (False ~ (e1 ~ e2)) cannot be analyzed unless
260 we know more about the inner equality (e1 ~ e2). That's exactly what
261 `simplifyEqExpr' tries to do: It takes e1 and e2 and either returns
262 truePmExpr, falsePmExpr or (e1' ~ e2') in case it is uncertain. Note
263 that it is not e but rather e', since it may perform some
264 simplifications deeper.
265 -}