never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.BubbleUp where
4
5 import Conjure.Rules.Import
6
7
8 rule_MergeNested :: Rule
9 rule_MergeNested = "bubble-up-merge-nested" `namedRule` theRule where
10 theRule (WithLocals (WithLocals body (DefinednessConstraints locals1)) (DefinednessConstraints locals2)) =
11 return
12 ( "Merging nested bubbles"
13 , return $ WithLocals body (DefinednessConstraints (locals1 ++ locals2))
14 )
15 theRule (WithLocals (WithLocals body (AuxiliaryVars locals1)) (AuxiliaryVars locals2)) =
16 return
17 ( "Merging nested bubbles"
18 , return $ WithLocals body (AuxiliaryVars (locals1 ++ locals2))
19 )
20 theRule _ = na "rule_MergeNested"
21
22
23 rule_ToAnd :: Rule
24 rule_ToAnd = "bubble-to-and" `namedRule` theRule where
25 theRule (WithLocals x (AuxiliaryVars [])) = return ("Empty bubble is no bubble", return x)
26 theRule (WithLocals x (DefinednessConstraints [])) = return ("Empty bubble is no bubble", return x)
27 theRule (WithLocals x (DefinednessConstraints cons))
28 | let isTrueCons (Constant (ConstantBool True)) = True
29 isTrueCons _ = False
30 , all isTrueCons cons
31 = return ("Trivially defined", return x)
32 theRule (WithLocals x (DefinednessConstraints cons))
33 | let isFalseCons (Constant (ConstantBool False)) = True
34 isFalseCons _ = False
35 , any isFalseCons cons
36 , length cons > 1
37 = return ( "Trivially undefined"
38 , return (WithLocals x (DefinednessConstraints [Constant (ConstantBool False)]))
39 )
40 theRule (WithLocals x (DefinednessConstraints locals@(_:_))) = do
41 TypeBool <- typeOf x
42 let out = make opAnd $ fromList (x:locals)
43 return
44 ( "Converting a bubble into a conjunction."
45 , return out
46 )
47 theRule _ = na "rule_BubbleToAnd"
48
49
50 rule_ToMultiply_HeadOfIntComprehension :: Rule
51 rule_ToMultiply_HeadOfIntComprehension = "bubble-to-multiply-HeadOfIntComprehension" `namedRule` theRule where
52 theRule p = do
53 (_, _, mk, Comprehension (WithLocals x (DefinednessConstraints cons)) gocs) <- match opReducer p
54 TypeInt _ <- typeOf x
55 let conjunct = make opAnd (fromList cons)
56 let x' = [essence| &x * toInt(&conjunct) |]
57 let out = mk $ Comprehension x' gocs
58 return
59 ( "Converting a bubble into a multiplication."
60 , return out
61 )
62
63
64 rule_NotBoolYet :: Rule
65 rule_NotBoolYet = "bubble-up-NotBoolYet" `namedRule` theRule where
66 theRule WithLocals{}
67 = na "rule_NotBoolYet WithLocals"
68
69 theRule [essence| catchUndef(&x, &_) |]
70 | WithLocals _ (DefinednessConstraints _) <- x
71 = na "rule_NotBoolYet WithLocals"
72
73
74 -- if anything in a comprehension is undefined, the whole comprehension is undefined
75 -- this is for the non-bool case.
76 theRule (Comprehension (WithLocals body (DefinednessConstraints locals@(_:_))) gensOrConds) = do
77
78 ty <- typeOf body
79 case ty of
80 TypeBool -> na "rule_NotBoolYet"
81 _ -> return ()
82
83 forM_ gensOrConds $ \case
84 Generator GenDomainHasRepr{} -> return ()
85 Generator {} -> na "rule_NotBoolYet" -- no other generators, only GenDomainHasRepr
86 Condition {} -> return ()
87 ComprehensionLetting {} -> na "rule_NotBoolYet" -- no lettings
88
89 let localsLifted =
90 [ make opAnd $ Comprehension c gensOrConds
91 | c <- locals
92 ]
93
94 return
95 ( "Bubbling up (through comprehension), not reached a relational context yet."
96 , return $ WithLocals (Comprehension body gensOrConds) (DefinednessConstraints localsLifted)
97 )
98
99 theRule (Comprehension x gensOrConds) = do
100 let (gensOrConds', Any changed) = mconcat
101 [ case goc of
102 Generator (GenInExpr pat (WithLocals y (DefinednessConstraints cons)))
103 -> (Generator (GenInExpr pat y) : map Condition cons, Any True)
104 _ -> ([goc], Any False)
105 | goc <- gensOrConds
106 ]
107 unless changed (na "rule_NotBoolYet")
108 return
109 ( "Bubbling up, attached to a generator inside a comprehension"
110 , return $ Comprehension x gensOrConds'
111 )
112
113 theRule p = do
114 let
115 f x@(WithLocals y (DefinednessConstraints locals@(_:_))) = do
116 ty <- typeOf y
117 case ty of
118 TypeBool -> return x -- do not bubble-up if it is attached to a bool
119 _ -> tell locals >> return y
120 f x = return x
121 (p', collected) <- runWriterT (descendM f p)
122 when (null collected) $
123 na "rule_NotBoolYet doesn't have any bubbly children"
124 return
125 ( "Bubbling up, not reached a relational context yet."
126 , return $ WithLocals p' (DefinednessConstraints collected)
127 )
128
129
130 rule_ConditionInsideGeneratorDomain :: Rule
131 rule_ConditionInsideGeneratorDomain = "bubble-up-ConditionInsideGeneratorDomain" `namedRule` theRule where
132
133 theRule (Comprehension body gensOrConds) = do
134 (gocBefore, (goc', newConditions), gocAfter) <- matchFirst gensOrConds $ \case
135 Generator (GenDomainHasRepr pat domain@DomainInt{}) -> do
136 let
137 f (WithLocals x (DefinednessConstraints cons)) = do
138 tell cons
139 f x
140 f x = return x
141 (domain', newConditions) <- runWriterT (transformBiM f domain)
142 let goc' = Generator (GenDomainHasRepr pat domain')
143 if null newConditions
144 then na "rule_ConditionInsideGeneratorDomain"
145 else return (goc', newConditions)
146 _ -> na "rule_ConditionInsideGeneratorDomain"
147 return
148 ( "Bubbling up definedness constraints inside a generator domain."
149 , return $ Comprehension body
150 $ gocBefore
151 ++ [goc']
152 ++ map Condition newConditions
153 ++ gocAfter
154 )
155 theRule _ = na "rule_ConditionInsideGeneratorDomain"
156
157
158 rule_LiftVars :: Rule
159 rule_LiftVars = "bubble-up-LiftVars" `namedRule` theRule where
160
161 theRule [essence| catchUndef(&x, &ifUndefVal) |]
162 | WithLocals body (DefinednessConstraints cons) <- x = do
163 let ifDef = make opAnd (fromList cons)
164 return
165 ( ""
166 , return [essence| [ catchUndef(&body, &ifUndefVal)
167 , &ifUndefVal
168 ; int(0..1)
169 ] [ toInt(!&ifDef) ]
170 |]
171 )
172
173 theRule (Comprehension (WithLocals body locals) gensOrConds)
174 | and [ case goc of
175 Condition{} -> True
176 ComprehensionLetting{} -> True
177 _ -> False
178 | goc <- gensOrConds
179 ] -- if gensOrConds do not contain generators
180 = return
181 ( "Bubbling up when a comprehension doesn't contain any generators."
182 , return $ WithLocals (Comprehension body gensOrConds) locals
183 )
184
185 theRule (Comprehension (WithLocals body (AuxiliaryVars locals@(_:_))) gensOrConds) = do
186
187 let decls = [ (nm,dom) | Declaration (FindOrGiven LocalFind nm dom) <- locals ]
188 let cons = concat [ xs | SuchThat xs <- locals ]
189
190 (_conditions, generators) <- fmap mconcat $ forM gensOrConds $ \ goc -> case goc of
191 Condition{} -> return ([goc], [])
192 ComprehensionLetting{} -> return ([], [goc])
193 Generator (GenDomainHasRepr _ _) -> return ([], [goc])
194 _ -> na "rule_LiftVars"
195
196 let gensOrConds_dontCare = [ case goc of
197 Condition c -> Condition (make opNot c)
198 _ -> goc
199 | goc <- gensOrConds
200 ]
201
202 let patRefs = [ Reference patName Nothing | Generator (GenDomainHasRepr patName _domain) <- generators ]
203 let indexDomains = [domain | Generator (GenDomainHasRepr _patName domain) <- generators ]
204
205 let upd (Reference nm _) | nm `elem` map fst decls
206 = let r = Reference nm Nothing
207 in make opMatrixIndexing r patRefs
208 upd r = r
209
210 let declsLifted =
211 [ Declaration (FindOrGiven LocalFind nm domLifted)
212 | (nm, dom) <- decls
213 , let domLifted = foldr (DomainMatrix . forgetRepr) dom indexDomains
214 ]
215 let declsLiftedNames =
216 [ nm
217 | (nm, _dom) <- decls
218 ]
219
220 -- traceM $ show $ "declsLifted" <+> vcat (map pretty declsLifted)
221
222 let consLifted =
223 [ make opAnd $ Comprehension c gensOrConds
224 | c <- transformBi upd cons
225 ]
226
227 -- traceM $ show $ "consLifted" <+> vcat (map pretty consLifted)
228 -- traceM $ show $ "head lifted 1" <+> pretty body
229 -- traceM $ show $ "head lifted 2" <+> pretty (transform upd body)
230
231 let referencesInCons = nub [ r | r@(Reference _ (Just (DeclHasRepr {}))) <- concatMap universe cons]
232 let referencesInBody = nub [ r | r@(Reference _ (Just (DeclHasRepr {}))) <- universe body]
233 -- traceM $ show $ "referencesInBody" <+> vcat (map pretty referencesInBody)
234
235 let pr :: Name -> String = show . pretty
236
237 -- the name is a prefix of a name that's defined in the decls, but not identical
238 let unrefinedInBody = [ name | Reference name _ <- referencesInBody
239 , or [ pr name `isPrefixOf` pr declName && pr declName /= pr name | declName <- declsLiftedNames ]
240 ]
241
242 let unrefinedInCons = [ name | Reference name _ <- referencesInCons
243 , or [ pr name `isPrefixOf` pr declName && pr declName /= pr name | declName <- declsLiftedNames ]
244 ]
245
246 let dontCareCons = make opAnd $ fromList [ make opDontCare (Reference r Nothing) | r <- declsLiftedNames ]
247
248 -- traceM $ show $ "unrefinedInBody" <+> vcat (map pretty unrefinedInBody)
249 -- traceM $ show $ "unrefinedInCons" <+> vcat (map pretty unrefinedInCons)
250
251 when (not (null unrefinedInBody) || not (null unrefinedInCons)) $ na "rule_LiftVars"
252
253 return
254 ( "Bubbling up auxiliary variables through a comprehension."
255 , return $ WithLocals (make opConcatenate $ fromList [ Comprehension (transform upd body) (transformBi upd gensOrConds)
256 , Comprehension (transform upd dontCareCons) (transformBi upd gensOrConds_dontCare)
257 ])
258 (AuxiliaryVars (declsLifted ++ [SuchThat consLifted]))
259 )
260
261 -- this is to deal with when an AuxiliaryVars expression is in the generator
262 theRule (Comprehension body gensOrConds) = do
263
264 (gocBefore, (pat, expr, locals), gocAfter) <- matchFirst gensOrConds $ \case
265 Generator (GenInExpr pat (WithLocals expr (AuxiliaryVars locals))) ->
266 return (pat, expr, locals)
267 _ -> na "rule_LiftVars"
268
269 return
270 ( "Bubbling up auxiliary variables through a comprehension's generator."
271 , return $ WithLocals
272 (Comprehension body (gocBefore ++ [Generator (GenInExpr pat expr)] ++ gocAfter))
273 (AuxiliaryVars locals)
274 )
275
276 theRule WithLocals{} = na "rule_LiftVars"
277 theRule Reference{} = na "rule_LiftVars"
278
279 -- special handling of AuxiliaryVars-bubbles on the rhs of an implication
280 theRule p
281 | Just (a, WithLocals b (AuxiliaryVars locals@(_:_))) <- match opImply p
282 = do
283 let
284 decls = [ l | l@(Declaration (FindOrGiven LocalFind _ _)) <- locals ]
285
286 cons = make opAnd $ fromList $ concat [ xs | SuchThat xs <- locals ]
287
288 dontCares = make opAnd $ fromList [ make opDontCare (Reference nm Nothing)
289 | Declaration (FindOrGiven LocalFind nm _) <- locals
290 ]
291
292 p' = [essence| and([ &a -> (&b /\ &cons)
293 , !&a -> &dontCares
294 ])
295 |]
296
297 return
298 ( "Bubbling up auxiliary variables, rhs of imply."
299 , return $ WithLocals p' (AuxiliaryVars decls)
300 )
301
302 theRule p = do
303 let
304 f (WithLocals y (AuxiliaryVars locals@(_:_))) = do
305 tell locals
306 return y
307 f x = return x
308 (p', collected) <- runWriterT (descendM f p)
309 when (null collected) $
310 na "rule_LiftVars doesn't have any bubbly children"
311 return
312 ( "Bubbling up auxiliary variables."
313 , return $ WithLocals p' (AuxiliaryVars collected)
314 )