never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Horizontal.MSet where
4
5 import Conjure.Rules.Import
6
7
8 rule_Comprehension_Literal :: Rule
9 rule_Comprehension_Literal = "mset-comprehension-literal" `namedRule` theRule where
10 theRule (Comprehension body gensOrConds) = do
11 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
12 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
13 _ -> na "rule_Comprehension_Literal"
14 (TypeMSet tau, elems) <- match msetLiteral expr
15 let outLiteral = make matrixLiteral
16 (TypeMatrix (TypeInt TagInt) tau)
17 (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength elems))])
18 elems
19 let upd val old = lambdaToFunction pat old val
20 return
21 ( "Comprehension on mset literals"
22 , do
23 (iPat, i) <- quantifiedVar
24 return $ Comprehension (upd i body)
25 $ gocBefore
26 ++ [Generator (GenInExpr iPat outLiteral)]
27 ++ transformBi (upd i) gocAfter
28 )
29 theRule _ = na "rule_Comprehension_Literal"
30
31
32
33 -- freq(toMSet(flatten(m)), arg) ~~> sum([ toInt(arg = i) | i in mset ])
34 rule_Freq_toMSet_Flatten :: Rule
35 rule_Freq_toMSet_Flatten = "mset-freq-toMSet_Flatten" `namedRule` theRule where
36 theRule p = do
37 (mset, arg) <- match opFreq p
38 m <- match opToMSet mset >>= match opFlatten
39 indexDoms <- indexDomainsOf m
40 forM_ indexDoms $ \case
41 DomainAny{} -> na "rule_Comprehension_Flatten"
42 _ -> return ()
43 when (null indexDoms) $ na "rule_Comprehension_Flatten"
44 return
45 ( "Comprehension on a matrix flatten"
46 , do
47 (gens, is) <- unzip <$> sequence
48 [ do
49 (iPat, i) <- quantifiedVar
50 return (Generator (GenDomainNoRepr iPat d), i)
51 | d <- indexDoms
52 ]
53 let mis = make opMatrixIndexing m is
54 return $ make opSum $ Comprehension [essence| toInt(&arg = &mis) |] gens
55 )
56
57
58 rule_Comprehension_ToSet_Literal :: Rule
59 rule_Comprehension_ToSet_Literal = "mset-comprehension-toSet-literal" `namedRule` theRule where
60 theRule (Comprehension body gensOrConds) = do
61 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
62 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
63 _ -> na "rule_Comprehension_ToSet_Literal"
64 mset <- match opToSet expr
65 (TypeMSet tau, elems) <- match msetLiteral mset
66 let outLiteralDomain = mkDomainIntB 1 (fromInt $ genericLength elems)
67 let outLiteral = make matrixLiteral (TypeMatrix (TypeInt TagInt) tau) outLiteralDomain elems
68 let upd val old = lambdaToFunction pat old val
69 return
70 ( "Comprehension on toSet of mset literals"
71 , do
72 (iPat, i) <- quantifiedVar
73 (jPat, j) <- quantifiedVar
74 let iIndexed = [essence| &outLiteral[&i] |]
75 let jIndexed = [essence| &outLiteral[&j] |]
76 return $ Comprehension (upd iIndexed body)
77 $ gocBefore
78 ++ [ Generator (GenDomainNoRepr iPat outLiteralDomain)
79 , Condition [essence|
80 !(exists &jPat : &outLiteralDomain .
81 (&j < &i) /\ (&iIndexed = &jIndexed))
82 |]
83 ]
84 ++ transformBi (upd iIndexed) gocAfter
85 )
86 theRule _ = na "rule_Comprehension_ToSet_Literal"
87
88
89 rule_Comprehension_ToSet :: Rule
90 rule_Comprehension_ToSet = "mset-comprehension-toSet" `namedRule` theRule where
91 theRule (Comprehension body gensOrConds) = do
92 (gocBefore, (pat, iPat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
93 Generator (GenInExpr pat@(Single iPat) expr) -> return (pat, iPat, expr)
94 _ -> na "rule_Comprehension_ToSet"
95 mset <- match opToSet expr
96 TypeMSet{} <- typeOf mset
97 case tryMatch msetLiteral mset of
98 Just{} -> na "rule_Comprehension_ToSet: literal has a more specific rule"
99 Nothing -> return ()
100 innerDomain <- msetInnerDomain mset
101 let i = Reference iPat Nothing
102 return
103 ( "Comprehension on toSet of a multiset"
104 , return $ Comprehension body
105 $ gocBefore
106 ++ [ Generator (GenDomainNoRepr pat innerDomain)
107 , Condition [essence| freq(&mset, &i) > 0 |]
108 ]
109 ++ gocAfter
110 )
111 theRule _ = na "rule_Comprehension_ToSet"
112
113 msetInnerDomain mset = case tryMatch opUnion mset of
114 Just (x, y) -> do
115 xInner <- msetInnerDomain x
116 yInner <- msetInnerDomain y
117 domainUnion xInner yInner
118 Nothing -> do
119 DomainMSet _ _ inner <- domainOf mset
120 return inner
121
122
123 -- Is this argument of a toMSet guaranteed not to contain the same element twice?
124 duplicateFreeToMSetArg ::
125 (?typeCheckerMode :: TypeCheckerMode) =>
126 Expression -> Bool
127 duplicateFreeToMSetArg x = case (typeOf x :: Maybe Type) of
128 Just TypeSet{} -> True
129 Just TypeFunction{} -> True
130 Just TypeRelation{} -> True
131 _ -> case x of
132 -- a collection that has already been refined into a comprehension
133 -- generating each member of a domain at most once
134 Comprehension (Reference nm _) gensOrConds ->
135 case [ gen | Generator gen <- gensOrConds ] of
136 [GenDomainNoRepr (Single nm') _] -> nm == nm'
137 [GenDomainHasRepr nm' _] -> nm == nm'
138 _ -> False
139 _ -> False
140
141
142 -- Matches toMSet(x) union toMSet(y), where neither x nor y can contain duplicates.
143 -- Such a union has the same elements as the (much cheaper) union of the two
144 -- containers, so it is handled by the set union rule instead of by rule_Union.
145 tryMatchUnionOfSimpleToMSets ::
146 (?typeCheckerMode :: TypeCheckerMode) =>
147 Expression -> Maybe (Expression, Expression)
148 tryMatchUnionOfSimpleToMSets p = do
149 (x, y) <- match opUnion p
150 x' <- match opToMSet x
151 y' <- match opToMSet y
152 unless (duplicateFreeToMSetArg x' && duplicateFreeToMSetArg y') Nothing
153 return (x', y')
154
155
156 -- A multiset union contains max(freq(x, i), freq(y, i)) copies of each i.
157 -- Keep all copies from x, then add only the excess copies from y.
158 rule_Union :: Rule
159 rule_Union = "mset-union" `namedRule` theRule where
160 theRule (Comprehension body gensOrConds) = do
161 (gocBefore, (pat, iPat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
162 Generator (GenInExpr pat@(Single iPat) expr) -> return (pat, iPat, expr)
163 _ -> na "rule_Union"
164 (x, y) <- match opUnion expr
165 TypeMSet{} <- typeOf x
166 case tryMatchUnionOfSimpleToMSets expr of
167 Just{} -> na "rule_Union: set-union has a cheaper translation for this"
168 Nothing -> return ()
169 yMaxOccur <- msetMaxOccur y
170 let i = Reference iPat Nothing
171 return
172 ( "Horizontal rule for multiset union"
173 , do
174 (jPat, j) <- quantifiedVar
175 return $ make opFlatten $ AbstractLiteral $ AbsLitMatrix
176 (DomainInt TagInt [RangeBounded 1 2])
177 [ Comprehension body
178 $ gocBefore
179 ++ [ Generator (GenInExpr pat x) ]
180 ++ gocAfter
181 , Comprehension body
182 $ gocBefore
183 ++ [ Generator (GenInExpr pat [essence| toSet(&y) |])
184 , Generator (GenDomainNoRepr jPat (mkDomainIntB 1 yMaxOccur))
185 , Condition [essence| freq(&x, &i) < &j /\ &j <= freq(&y, &i) |]
186 ]
187 ++ gocAfter
188 ]
189 )
190 theRule _ = na "rule_Union"
191
192 -- an upper bound on the number of occurrences of a single element in the multiset
193 msetMaxOccur mset = case tryMatch opUnion mset of
194 Just (x, y) -> do
195 xMaxOccur <- msetMaxOccur x
196 yMaxOccur <- msetMaxOccur y
197 return [essence| max([&xMaxOccur, &yMaxOccur]) |]
198 Nothing -> case tryMatch opToMSet mset of
199 -- toMSet of a set, function or relation never repeats an element
200 Just inner -> do
201 tyInner <- typeOf inner
202 case tyInner of
203 TypeSet{} -> return 1
204 TypeFunction{} -> return 1
205 TypeRelation{} -> return 1
206 TypeMSet{} -> msetMaxOccur inner
207 _ -> msetMaxOccurFromDomain mset
208 Nothing -> msetMaxOccurFromDomain mset
209
210 msetMaxOccurFromDomain mset = do
211 DomainMSet _ (MSetAttr sizeAttr _) _ <- domainOf mset
212 case sizeAttr of
213 SizeAttr_Size size -> return size
214 SizeAttr_MaxSize size -> return size
215 SizeAttr_MinMaxSize _ size -> return size
216 _ -> failDoc "rule_Union maxOccur"
217
218
219 rule_Eq :: Rule
220 rule_Eq = "mset-eq" `namedRule` theRule where
221 theRule p = do
222 (x,y) <- match opEq p
223 TypeMSet{} <- typeOf x
224 TypeMSet{} <- typeOf y
225 return
226 ( "Horizontal rule for mset equality"
227 , do
228 (iPat, i) <- quantifiedVar
229 return
230 [essence|
231 (forAll &iPat in &x . freq(&x,&i) = freq(&y,&i)) /\
232 (forAll &iPat in &y . freq(&x,&i) = freq(&y,&i))
233 |]
234 )
235
236
237 rule_Neq :: Rule
238 rule_Neq = "mset-neq" `namedRule` theRule where
239 theRule [essence| &x != &y |] = do
240 TypeMSet{} <- typeOf x
241 TypeMSet{} <- typeOf y
242 return
243 ( "Horizontal rule for mset dis-equality"
244 , do
245 (iPat, i) <- quantifiedVar
246 return
247 [essence|
248 (exists &iPat in &x . freq(&x,&i) != freq(&y,&i)) \/
249 (exists &iPat in &y . freq(&x,&i) != freq(&y,&i))
250 |]
251 )
252 theRule _ = na "rule_Neq"
253
254
255 rule_SubsetEq :: Rule
256 rule_SubsetEq = "mset-subsetEq" `namedRule` theRule where
257 theRule p = do
258 (x,y) <- match opSubsetEq p
259 TypeMSet{} <- typeOf x
260 TypeMSet{} <- typeOf y
261 return
262 ( "Horizontal rule for mset subsetEq"
263 , do
264 (iPat, i) <- quantifiedVar
265 return [essence| forAll &iPat in &x . freq(&x,&i) <= freq(&y,&i) |]
266 )
267
268
269 rule_Subset :: Rule
270 rule_Subset = "mset-subset" `namedRule` theRule where
271 theRule [essence| &x subset &y |] = do
272 TypeMSet{} <- typeOf x
273 TypeMSet{} <- typeOf y
274 return
275 ( "Horizontal rule for mset subset"
276 , do
277 (iPat, i) <- quantifiedVar
278 return
279 [essence|
280 (forAll &iPat in &x . freq(&x,&i) <= freq(&y,&i)) /\
281 (exists &iPat in &x . freq(&x,&i) < freq(&y,&i))
282 |]
283 )
284 theRule _ = na "rule_Subset"
285
286
287 rule_Supset :: Rule
288 rule_Supset = "mset-supset" `namedRule` theRule where
289 theRule [essence| &a supset &b |] = do
290 TypeMSet{} <- typeOf a
291 TypeMSet{} <- typeOf b
292 return
293 ( "Horizontal rule for mset supset"
294 , return [essence| &b subset &a |]
295 )
296 theRule _ = na "rule_Supset"
297
298
299 rule_SupsetEq :: Rule
300 rule_SupsetEq = "mset-subsetEq" `namedRule` theRule where
301 theRule [essence| &a supsetEq &b |] = do
302 TypeMSet{} <- typeOf a
303 TypeMSet{} <- typeOf b
304 return
305 ( "Horizontal rule for mset supsetEq"
306 , return [essence| &b subsetEq &a |]
307 )
308 theRule _ = na "rule_SupsetEq"
309
310
311 rule_MaxMin :: Rule
312 rule_MaxMin = "mset-max-min" `namedRule` theRule where
313 theRule [essence| max(&s) |] = do
314 TypeMSet (TypeInt _) <- typeOf s
315 return
316 ( "Horizontal rule for mset max"
317 , case () of
318 _ | Just (_, xs) <- match msetLiteral s, length xs > 0 -> return $ make opMax $ fromList xs
319 _ -> do
320 (iPat, i) <- quantifiedVar
321 return [essence| max([&i | &iPat <- &s]) |]
322 )
323 theRule [essence| min(&s) |] = do
324 TypeMSet (TypeInt _) <- typeOf s
325 return
326 ( "Horizontal rule for mset min"
327 , case () of
328 _ | Just (_, xs) <- match msetLiteral s, length xs > 0 -> return $ make opMin $ fromList xs
329 _ -> do
330 (iPat, i) <- quantifiedVar
331 return [essence| min([&i | &iPat <- &s]) |]
332 )
333 theRule _ = na "rule_MaxMin"
334
335
336 -- freq(x union y, arg) ~~> max([freq(x, arg), freq(y, arg)])
337 rule_Freq_Union :: Rule
338 rule_Freq_Union = "mset-freq-union" `namedRule` theRule where
339 theRule p = do
340 (mset, arg) <- match opFreq p
341 (x, y) <- match opUnion mset
342 TypeMSet{} <- typeOf x
343 return
344 ( "Horizontal rule for frequency in a multiset union."
345 , return [essence| max([freq(&x, &arg), freq(&y, &arg)]) |]
346 )
347
348
349 -- freq(mset,arg) ~~> sum([ toInt(arg = i) | i in mset ])
350 rule_Freq :: Rule
351 rule_Freq = "mset-freq" `namedRule` theRule where
352 theRule p = do
353 (mset, arg) <- match opFreq p
354 case match opToMSet mset >>= match opFlatten of
355 Nothing -> return ()
356 Just{} -> na "There is a better rule for this: rule_Freq_toMSet_Flatten"
357 TypeMSet{} <- typeOf mset
358 -- avoid applying this rule when "mset" is of the form "toMSet of set"
359 case mset of
360 [essence| toMSet(&s) |] -> do
361 tyS <- typeOf s
362 case tyS of
363 TypeSet{} -> na "rule_Freq"
364 _ -> return ()
365 _ -> return ()
366 return
367 ( "Horizontal rule for mset-freq."
368 , do
369 (iPat, i) <- quantifiedVar
370 return [essence| sum &iPat in &mset . toInt(&i = &arg) |]
371 )
372
373
374 -- x in s ~~> or([ x = i | i in s ])
375 rule_In :: Rule
376 rule_In = "mset-in" `namedRule` theRule where
377 theRule p = do
378 (x,s) <- match opIn p
379 TypeMSet{} <- typeOf s
380 return
381 ( "Horizontal rule for mset-in."
382 , do
383 (iPat, i) <- quantifiedVar
384 return [essence| exists &iPat in &s . &i = &x |]
385 )
386
387
388 rule_Card :: Rule
389 rule_Card = "mset-card" `namedRule` theRule where
390 theRule p = do
391 s <- match opTwoBars p
392 TypeMSet{} <- typeOf s
393 return
394 ( "Horizontal rule for mset cardinality."
395 , do
396 (iPat, _) <- quantifiedVar
397 return [essence| sum &iPat in &s . 1 |]
398 )