Remove unused import in deSugar/TmOracle.hs
[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 canDiverge, eqPmLit, filterComplex, isNotPmExprOther, runPmPprM,
14 pprPmExprWithParens, lhsExprToPmExpr, hsExprToPmExpr,
15
16 -- the term oracle
17 tmOracle, TmState, initialTmState,
18
19 -- misc.
20 exprDeepLookup, pmLitType, flattenPmVarEnv
21 ) where
22
23 #include "HsVersions.h"
24
25 import PmExpr
26
27 import Id
28 import TysWiredIn
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 Id 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 :: Id -> 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 :: Id -> 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 :: Id -> 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 True -> Just solver_state
109 False -> Nothing
110
111 (PmExprCon c1 ts1, PmExprCon c2 ts2)
112 | c1 == c2 -> foldlM solveComplexEq solver_state (zip ts1 ts2)
113 | otherwise -> Nothing
114 (PmExprCon c [], PmExprEq t1 t2)
115 | c == trueDataCon -> solveComplexEq solver_state (t1, t2)
116 | c == falseDataCon -> Just (eq:standby, (unhandled, env))
117 (PmExprEq t1 t2, PmExprCon c [])
118 | c == trueDataCon -> solveComplexEq solver_state (t1, t2)
119 | c == falseDataCon -> Just (eq:standby, (unhandled, env))
120
121 (PmExprVar x, PmExprVar y)
122 | x == y -> Just solver_state
123 | otherwise -> extendSubstAndSolve x e2 solver_state
124
125 (PmExprVar x, _) -> extendSubstAndSolve x e2 solver_state
126 (_, PmExprVar x) -> extendSubstAndSolve x e1 solver_state
127
128 (PmExprEq _ _, PmExprEq _ _) -> Just (eq:standby, (unhandled, env))
129
130 _ -> Just (standby, (True, env)) -- I HATE CATCH-ALLS
131
132 -- | Extend the substitution and solve the (possibly updated) constraints.
133 extendSubstAndSolve :: Id -> PmExpr -> TmState -> Maybe TmState
134 extendSubstAndSolve x e (standby, (unhandled, env))
135 = foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed)
136 where
137 -- Apply the substitution to the worklist and partition them to the ones
138 -- that had some progress and the rest. Then, recurse over the ones that
139 -- had some progress.
140 (changed, unchanged) = partitionWith (substComplexEq x e) standby
141 new_incr_state = (unchanged, (unhandled, Map.insert x e env))
142
143 -- | Simplify a complex equality.
144 simplifyComplexEq :: ComplexEq -> ComplexEq
145 simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2)
146
147 -- | Simplify an expression. The boolean indicates if there has been any
148 -- simplification or if the operation was a no-op.
149 simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
150 -- See Note [Deep equalities]
151 simplifyPmExpr e = case e of
152 PmExprCon c ts -> case mapAndUnzip simplifyPmExpr ts of
153 (ts', bs) -> (PmExprCon c ts', or bs)
154 PmExprEq t1 t2 -> simplifyEqExpr t1 t2
155 _other_expr -> (e, False) -- the others are terminals
156
157 -- | Simplify an equality expression. The equality is given in parts.
158 simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
159 -- See Note [Deep equalities]
160 simplifyEqExpr e1 e2 = case (e1, e2) of
161 -- Varables
162 (PmExprVar x, PmExprVar y)
163 | x == y -> (truePmExpr, True)
164
165 -- Literals
166 (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
167 True -> (truePmExpr, True)
168 False -> (falsePmExpr, True)
169
170 -- Can potentially be simplified
171 (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
172 ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
173 ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
174 ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
175 (_, PmExprEq {}) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
176 ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
177 ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
178 ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
179
180 -- Constructors
181 (PmExprCon c1 ts1, PmExprCon c2 ts2)
182 | c1 == c2 ->
183 let (ts1', bs1) = mapAndUnzip simplifyPmExpr ts1
184 (ts2', bs2) = mapAndUnzip simplifyPmExpr ts2
185 (tss, _bss) = zipWithAndUnzip simplifyEqExpr ts1' ts2'
186 worst_case = PmExprEq (PmExprCon c1 ts1') (PmExprCon c2 ts2')
187 in if | not (or bs1 || or bs2) -> (worst_case, False) -- no progress
188 | all isTruePmExpr tss -> (truePmExpr, True)
189 | any isFalsePmExpr tss -> (falsePmExpr, True)
190 | otherwise -> (worst_case, False)
191 | otherwise -> (falsePmExpr, True)
192
193 -- We cannot do anything about the rest..
194 _other_equality -> (original, False)
195
196 where
197 original = PmExprEq e1 e2 -- reconstruct equality
198
199 -- | Apply an (un-flattened) substitution to a simple equality.
200 applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
201 applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2)
202
203 -- | Apply an (un-flattened) substitution to a variable.
204 varDeepLookup :: PmVarEnv -> Id -> PmExpr
205 varDeepLookup env x
206 | Just e <- Map.lookup x env = exprDeepLookup env e -- go deeper
207 | otherwise = PmExprVar x -- terminal
208 {-# INLINE varDeepLookup #-}
209
210 -- | Apply an (un-flattened) substitution to an expression.
211 exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
212 exprDeepLookup env (PmExprVar x) = varDeepLookup env x
213 exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
214 exprDeepLookup env (PmExprEq e1 e2) = PmExprEq (exprDeepLookup env e1)
215 (exprDeepLookup env e2)
216 exprDeepLookup _ other_expr = other_expr -- PmExprLit, PmExprOther
217
218 -- | External interface to the term oracle.
219 tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
220 tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs
221
222 -- | Type of a PmLit
223 pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :(
224 pmLitType (PmSLit lit) = hsLitType lit
225 pmLitType (PmOLit _ lit) = overLitType lit
226
227 {- Note [Deep equalities]
228 ~~~~~~~~~~~~~~~~~~~~~~~~~
229 Solving nested equalities is the most difficult part. The general strategy
230 is the following:
231
232 * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
233 (e1 ~ e2) and then treated recursively.
234
235 * Equalities of the form (False ~ (e1 ~ e2)) cannot be analyzed unless
236 we know more about the inner equality (e1 ~ e2). That's exactly what
237 `simplifyEqExpr' tries to do: It takes e1 and e2 and either returns
238 truePmExpr, falsePmExpr or (e1' ~ e2') in case it is uncertain. Note
239 that it is not e but rather e', since it may perform some
240 simplifications deeper.
241 -}