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 $ \ goc -> case goc of
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 $ \ goc -> case goc of
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 -- TODO: what to do with the conditions?
191 -- should we `dontCare unless condition`?
192 -- discard for now
193 (_conditions, generators) <- fmap mconcat $ forM gensOrConds $ \ goc -> case goc of
194 Condition{} -> return ([goc], [])
195 ComprehensionLetting{} -> return ([], [goc])
196 Generator (GenDomainHasRepr _ _) -> return ([], [goc])
197 _ -> na "rule_LiftVars"
198
199 let patRefs = [ Reference patName Nothing | Generator (GenDomainHasRepr patName _domain) <- generators ]
200 let indexDomains = [domain | Generator (GenDomainHasRepr _patName domain) <- generators ]
201
202 let upd (Reference nm _) | nm `elem` map fst decls
203 = let r = Reference nm Nothing
204 in make opMatrixIndexing r patRefs
205 upd r = r
206
207 let declsLifted =
208 [ Declaration (FindOrGiven LocalFind nm domLifted)
209 | (nm, dom) <- decls
210 , let domLifted = foldr (\ i j -> DomainMatrix (forgetRepr i) j ) dom indexDomains
211 ]
212
213 let consLifted =
214 [ make opAnd $ Comprehension c generators
215 | c <- transformBi upd cons
216 ]
217
218 return
219 ( "Bubbling up auxiliary variables through a comprehension."
220 , return $ WithLocals (Comprehension (transform upd body) (transformBi upd gensOrConds))
221 (AuxiliaryVars (declsLifted ++ [SuchThat consLifted]))
222 )
223 theRule WithLocals{} = na "rule_LiftVars"
224 theRule Reference{} = na "rule_LiftVars"
225
226 -- special handling of AuxiliaryVars-bubbles on the rhs of an implication
227 theRule p
228 | Just (a, WithLocals b (AuxiliaryVars locals@(_:_))) <- match opImply p
229 = do
230 let
231 decls = [ l | l@(Declaration (FindOrGiven LocalFind _ _)) <- locals ]
232
233 cons = make opAnd $ fromList $ concat [ xs | SuchThat xs <- locals ]
234
235 dontCares = make opAnd $ fromList [ make opDontCare (Reference nm Nothing)
236 | Declaration (FindOrGiven LocalFind nm _) <- locals
237 ]
238
239 p' = [essence| and([ &a -> (&b /\ &cons)
240 , !&a -> &dontCares
241 ])
242 |]
243
244 return
245 ( "Bubbling up auxiliary variables, rhs of imply."
246 , return $ WithLocals p' (AuxiliaryVars decls)
247 )
248
249 theRule p = do
250 let
251 f (WithLocals y (AuxiliaryVars locals@(_:_))) = do
252 tell locals
253 return y
254 f x = return x
255 (p', collected) <- runWriterT (descendM f p)
256 when (null collected) $
257 na "rule_LiftVars doesn't have any bubbly children"
258 return
259 ( "Bubbling up auxiliary variables."
260 , return $ WithLocals p' (AuxiliaryVars collected)
261 )