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