Merge remote-tracking branch 'github/pr/83'
[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 solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
104 solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
105 -- We cannot do a thing about these cases
106 (PmExprOther _,_) -> Just (standby, (True, env))
107 (_,PmExprOther _) -> Just (standby, (True, env))
108
109 (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
110 -- See Note [Undecidable Equality for Overloaded Literals]
111 True -> Just solver_state
112 False -> Nothing
113
114 (PmExprCon c1 ts1, PmExprCon c2 ts2)
115 | c1 == c2 -> foldlM solveComplexEq solver_state (zip ts1 ts2)
116 | otherwise -> Nothing
117 (PmExprCon _ [], PmExprEq t1 t2)
118 | isTruePmExpr e1 -> solveComplexEq solver_state (t1, t2)
119 | isFalsePmExpr e1 -> Just (eq:standby, (unhandled, env))
120 (PmExprEq t1 t2, PmExprCon _ [])
121 | isTruePmExpr e2 -> solveComplexEq solver_state (t1, t2)
122 | isFalsePmExpr e2 -> Just (eq:standby, (unhandled, env))
123
124 (PmExprVar x, PmExprVar y)
125 | x == y -> Just solver_state
126 | otherwise -> extendSubstAndSolve x e2 solver_state
127
128 (PmExprVar x, _) -> extendSubstAndSolve x e2 solver_state
129 (_, PmExprVar x) -> extendSubstAndSolve x e1 solver_state
130
131 (PmExprEq _ _, PmExprEq _ _) -> Just (eq:standby, (unhandled, env))
132
133 _ -> Just (standby, (True, env)) -- I HATE CATCH-ALLS
134
135 -- | Extend the substitution and solve the (possibly updated) constraints.
136 extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState
137 extendSubstAndSolve x e (standby, (unhandled, env))
138 = foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed)
139 where
140 -- Apply the substitution to the worklist and partition them to the ones
141 -- that had some progress and the rest. Then, recurse over the ones that
142 -- had some progress. Careful about performance:
143 -- See Note [Representation of Term Equalities] in deSugar/Check.hs
144 (changed, unchanged) = partitionWith (substComplexEq x e) standby
145 new_incr_state = (unchanged, (unhandled, extendNameEnv env x e))
146
147 -- | When we know that a variable is fresh, we do not actually have to
148 -- check whether anything changes, we know that nothing does. Hence,
149 -- `extendSubst` simply extends the substitution, unlike what
150 -- `extendSubstAndSolve` does.
151 extendSubst :: Id -> PmExpr -> TmState -> TmState
152 extendSubst y e (standby, (unhandled, env))
153 | isNotPmExprOther simpl_e
154 = (standby, (unhandled, extendNameEnv env x simpl_e))
155 | otherwise = (standby, (True, env))
156 where
157 x = idName y
158 simpl_e = fst $ simplifyPmExpr $ exprDeepLookup env e
159
160 -- | Simplify a complex equality.
161 simplifyComplexEq :: ComplexEq -> ComplexEq
162 simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2)
163
164 -- | Simplify an expression. The boolean indicates if there has been any
165 -- simplification or if the operation was a no-op.
166 simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
167 -- See Note [Deep equalities]
168 simplifyPmExpr e = case e of
169 PmExprCon c ts -> case mapAndUnzip simplifyPmExpr ts of
170 (ts', bs) -> (PmExprCon c ts', or bs)
171 PmExprEq t1 t2 -> simplifyEqExpr t1 t2
172 _other_expr -> (e, False) -- the others are terminals
173
174 -- | Simplify an equality expression. The equality is given in parts.
175 simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
176 -- See Note [Deep equalities]
177 simplifyEqExpr e1 e2 = case (e1, e2) of
178 -- Varables
179 (PmExprVar x, PmExprVar y)
180 | x == y -> (truePmExpr, True)
181
182 -- Literals
183 (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
184 -- See Note [Undecidable Equality for Overloaded Literals]
185 True -> (truePmExpr, True)
186 False -> (falsePmExpr, True)
187
188 -- Can potentially be simplified
189 (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
190 ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
191 ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
192 ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
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
198 -- Constructors
199 (PmExprCon c1 ts1, PmExprCon c2 ts2)
200 | c1 == c2 ->
201 let (ts1', bs1) = mapAndUnzip simplifyPmExpr ts1
202 (ts2', bs2) = mapAndUnzip simplifyPmExpr ts2
203 (tss, _bss) = zipWithAndUnzip simplifyEqExpr ts1' ts2'
204 worst_case = PmExprEq (PmExprCon c1 ts1') (PmExprCon c2 ts2')
205 in if | not (or bs1 || or bs2) -> (worst_case, False) -- no progress
206 | all isTruePmExpr tss -> (truePmExpr, True)
207 | any isFalsePmExpr tss -> (falsePmExpr, True)
208 | otherwise -> (worst_case, False)
209 | otherwise -> (falsePmExpr, True)
210
211 -- We cannot do anything about the rest..
212 _other_equality -> (original, False)
213
214 where
215 original = PmExprEq e1 e2 -- reconstruct equality
216
217 -- | Apply an (un-flattened) substitution to a simple equality.
218 applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
219 applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2)
220
221 -- | Apply an (un-flattened) substitution to a variable.
222 varDeepLookup :: PmVarEnv -> Name -> PmExpr
223 varDeepLookup env x
224 | Just e <- lookupNameEnv env x = exprDeepLookup env e -- go deeper
225 | otherwise = PmExprVar x -- terminal
226 {-# INLINE varDeepLookup #-}
227
228 -- | Apply an (un-flattened) substitution to an expression.
229 exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
230 exprDeepLookup env (PmExprVar x) = varDeepLookup env x
231 exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
232 exprDeepLookup env (PmExprEq e1 e2) = PmExprEq (exprDeepLookup env e1)
233 (exprDeepLookup env e2)
234 exprDeepLookup _ other_expr = other_expr -- PmExprLit, PmExprOther
235
236 -- | External interface to the term oracle.
237 tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
238 tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs
239
240 -- | Type of a PmLit
241 pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :(
242 pmLitType (PmSLit lit) = hsLitType lit
243 pmLitType (PmOLit _ lit) = overLitType lit
244
245 {- Note [Deep equalities]
246 ~~~~~~~~~~~~~~~~~~~~~~~~~
247 Solving nested equalities is the most difficult part. The general strategy
248 is the following:
249
250 * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
251 (e1 ~ e2) and then treated recursively.
252
253 * Equalities of the form (False ~ (e1 ~ e2)) cannot be analyzed unless
254 we know more about the inner equality (e1 ~ e2). That's exactly what
255 `simplifyEqExpr' tries to do: It takes e1 and e2 and either returns
256 truePmExpr, falsePmExpr or (e1' ~ e2') in case it is uncertain. Note
257 that it is not e but rather e', since it may perform some
258 simplifications deeper.
259 -}