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