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