Fix grouping for pattern synonyms
[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 -- 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 c [], PmExprEq t1 t2)
116 | c == trueDataCon -> solveComplexEq solver_state (t1, t2)
117 | c == falseDataCon -> Just (eq:standby, (unhandled, env))
118 (PmExprEq t1 t2, PmExprCon c [])
119 | c == trueDataCon -> solveComplexEq solver_state (t1, t2)
120 | c == falseDataCon -> 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 :: Id -> 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 -- | Simplify a complex equality.
146 simplifyComplexEq :: ComplexEq -> ComplexEq
147 simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2)
148
149 -- | Simplify an expression. The boolean indicates if there has been any
150 -- simplification or if the operation was a no-op.
151 simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
152 -- See Note [Deep equalities]
153 simplifyPmExpr e = case e of
154 PmExprCon c ts -> case mapAndUnzip simplifyPmExpr ts of
155 (ts', bs) -> (PmExprCon c ts', or bs)
156 PmExprEq t1 t2 -> simplifyEqExpr t1 t2
157 _other_expr -> (e, False) -- the others are terminals
158
159 -- | Simplify an equality expression. The equality is given in parts.
160 simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
161 -- See Note [Deep equalities]
162 simplifyEqExpr e1 e2 = case (e1, e2) of
163 -- Varables
164 (PmExprVar x, PmExprVar y)
165 | x == y -> (truePmExpr, True)
166
167 -- Literals
168 (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
169 -- See Note [Undecidable Equality for Overloaded Literals]
170 True -> (truePmExpr, True)
171 False -> (falsePmExpr, True)
172
173 -- Can potentially be simplified
174 (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
175 ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
176 ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
177 ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
178 (_, PmExprEq {}) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
179 ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
180 ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
181 ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
182
183 -- Constructors
184 (PmExprCon c1 ts1, PmExprCon c2 ts2)
185 | c1 == c2 ->
186 let (ts1', bs1) = mapAndUnzip simplifyPmExpr ts1
187 (ts2', bs2) = mapAndUnzip simplifyPmExpr ts2
188 (tss, _bss) = zipWithAndUnzip simplifyEqExpr ts1' ts2'
189 worst_case = PmExprEq (PmExprCon c1 ts1') (PmExprCon c2 ts2')
190 in if | not (or bs1 || or bs2) -> (worst_case, False) -- no progress
191 | all isTruePmExpr tss -> (truePmExpr, True)
192 | any isFalsePmExpr tss -> (falsePmExpr, True)
193 | otherwise -> (worst_case, False)
194 | otherwise -> (falsePmExpr, True)
195
196 -- We cannot do anything about the rest..
197 _other_equality -> (original, False)
198
199 where
200 original = PmExprEq e1 e2 -- reconstruct equality
201
202 -- | Apply an (un-flattened) substitution to a simple equality.
203 applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
204 applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2)
205
206 -- | Apply an (un-flattened) substitution to a variable.
207 varDeepLookup :: PmVarEnv -> Id -> PmExpr
208 varDeepLookup env x
209 | Just e <- Map.lookup x env = exprDeepLookup env e -- go deeper
210 | otherwise = PmExprVar x -- terminal
211 {-# INLINE varDeepLookup #-}
212
213 -- | Apply an (un-flattened) substitution to an expression.
214 exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
215 exprDeepLookup env (PmExprVar x) = varDeepLookup env x
216 exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
217 exprDeepLookup env (PmExprEq e1 e2) = PmExprEq (exprDeepLookup env e1)
218 (exprDeepLookup env e2)
219 exprDeepLookup _ other_expr = other_expr -- PmExprLit, PmExprOther
220
221 -- | External interface to the term oracle.
222 tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
223 tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs
224
225 -- | Type of a PmLit
226 pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :(
227 pmLitType (PmSLit lit) = hsLitType lit
228 pmLitType (PmOLit _ lit) = overLitType lit
229
230 {- Note [Deep equalities]
231 ~~~~~~~~~~~~~~~~~~~~~~~~~
232 Solving nested equalities is the most difficult part. The general strategy
233 is the following:
234
235 * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
236 (e1 ~ e2) and then treated recursively.
237
238 * Equalities of the form (False ~ (e1 ~ e2)) cannot be analyzed unless
239 we know more about the inner equality (e1 ~ e2). That's exactly what
240 `simplifyEqExpr' tries to do: It takes e1 and e2 and either returns
241 truePmExpr, falsePmExpr or (e1' ~ e2') in case it is uncertain. Note
242 that it is not e but rather e', since it may perform some
243 simplifications deeper.
244 -}