never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Horizontal.Set where
4
5 import Conjure.Rules.Import
6 import Conjure.Rules.Horizontal.MSet ( tryMatchUnionOfSimpleToMSets )
7 import Conjure.Process.Sanity ( isInfinite )
8
9 rule_Comprehension_Literal :: Rule
10 rule_Comprehension_Literal = "set-comprehension-literal" `namedRule` theRule where
11 theRule (Comprehension body gensOrConds) = do
12 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
13 Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDefs [opToSet, opToMSet] expr)
14 Generator (GenInExpr pat@AbsPatSet{} expr) -> return (pat, matchDefs [opToSet, opToMSet] expr)
15 _ -> na "rule_Comprehension_Literal"
16 (TypeSet tau, elems) <- match setLiteral expr
17 let outLiteral = make matrixLiteral
18 (TypeMatrix (TypeInt TagInt) tau)
19 (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength elems))])
20 elems
21 return
22 ( "Comprehension on set literals"
23 , return $ Comprehension body
24 $ gocBefore
25 ++ [Generator (GenInExpr pat outLiteral)]
26 ++ gocAfter
27 )
28 theRule _ = na "rule_Comprehension_Literal"
29
30
31 rule_Eq :: Rule
32 rule_Eq = "set-eq" `namedRule` theRule where
33 theRule p = do
34 (x,y) <- match opEq p
35 TypeSet{} <- typeOf x
36 TypeSet{} <- typeOf y
37 return
38 ( "Horizontal rule for set equality"
39 , return $ make opAnd $ fromList
40 [ make opSubsetEq x y
41 , make opSubsetEq y x
42 ]
43 )
44
45
46 rule_Neq :: Rule
47 rule_Neq = "set-neq" `namedRule` theRule where
48 theRule [essence| &x != &y |] = do
49 TypeSet{} <- typeOf x
50 TypeSet{} <- typeOf y
51 return
52 ( "Horizontal rule for set dis-equality"
53 , do
54 (iPat, i) <- quantifiedVar
55 return [essence|
56 (exists &iPat in &x . !(&i in &y))
57 \/
58 (exists &iPat in &y . !(&i in &x))
59 |]
60 )
61 theRule _ = na "rule_Neq"
62
63
64 rule_SubsetEq :: Rule
65 rule_SubsetEq = "set-subsetEq" `namedRule` theRule where
66 theRule p = do
67 (x,y) <- match opSubsetEq p
68 TypeSet{} <- typeOf x
69 TypeSet{} <- typeOf y
70 return
71 ( "Horizontal rule for set subsetEq"
72 , do
73 (iPat, i) <- quantifiedVar
74 return [essence| forAll &iPat in &x . &i in &y |]
75 )
76
77
78 rule_Subset :: Rule
79 rule_Subset = "set-subset" `namedRule` theRule where
80 theRule [essence| &a subset &b |] = do
81 TypeSet{} <- typeOf a
82 TypeSet{} <- typeOf b
83 return
84 ( "Horizontal rule for set subset"
85 , return [essence| &a subsetEq &b /\ &a != &b |]
86 )
87 theRule _ = na "rule_Subset"
88
89
90 rule_Supset :: Rule
91 rule_Supset = "set-supset" `namedRule` theRule where
92 theRule [essence| &a supset &b |] = do
93 TypeSet{} <- typeOf a
94 TypeSet{} <- typeOf b
95 return
96 ( "Horizontal rule for set supset"
97 , return [essence| &b subset &a |]
98 )
99 theRule _ = na "rule_Supset"
100
101
102 rule_SupsetEq :: Rule
103 rule_SupsetEq = "set-subsetEq" `namedRule` theRule where
104 theRule [essence| &a supsetEq &b |] = do
105 TypeSet{} <- typeOf a
106 TypeSet{} <- typeOf b
107 return
108 ( "Horizontal rule for set supsetEq"
109 , return [essence| &b subsetEq &a |]
110 )
111 theRule _ = na "rule_SupsetEq"
112
113
114 rule_Intersect :: Rule
115 rule_Intersect = "set-intersect" `namedRule` theRule where
116 theRule (Comprehension body gensOrConds) = do
117 (gocBefore, (pat, iPat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
118 Generator (GenInExpr pat@(Single iPat) expr) ->
119 return (pat, iPat, matchDefs [opToSet,opToMSet,opToRelation] expr)
120 _ -> na "rule_Intersect"
121 (mkModifier, s) <- match opModifier expr
122 (x, y) <- match opIntersect s
123 tx <- typeOf x
124 case tx of
125 TypeSet{} -> return ()
126 TypeMSet{} -> return ()
127 TypeFunction{} -> return ()
128 TypeRelation{} -> return ()
129 _ -> failDoc "type incompatibility in intersect operator"
130 let i = Reference iPat Nothing
131 return
132 ( "Horizontal rule for set intersection"
133 , return $
134 Comprehension body
135 $ gocBefore
136 ++ [ Generator (GenInExpr pat (mkModifier x))
137 , Condition [essence| &i in &y |]
138 ]
139 ++ gocAfter
140 )
141 theRule _ = na "rule_Intersect"
142
143
144 rule_Union :: Rule
145 rule_Union = "set-union" `namedRule` theRule where
146 theRule (Comprehension body gensOrConds) = do
147 (gocBefore, (pat, iPat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
148 Generator (GenInExpr pat@(Single iPat) expr) -> return (pat, iPat, expr)
149 _ -> na "rule_Union"
150 (mkModifier, s) <- match opModifier expr
151 (x, y) <- match opUnion s
152 tx <- typeOf x
153 case tx of
154 TypeSet{} -> return ()
155 -- a multiset union only agrees with a set union when neither side
156 -- can contain duplicates, rule_Union in Horizontal.MSet handles the rest
157 TypeMSet{} -> case tryMatchUnionOfSimpleToMSets s of
158 Just{} -> return ()
159 Nothing -> na "rule_Union: multiset union"
160 TypeFunction{} -> return ()
161 TypeRelation{} -> return ()
162 _ -> failDoc "type incompatibility in union operator"
163 let i = Reference iPat Nothing
164 return
165 ( "Horizontal rule for set union"
166 , return $ make opFlatten $ AbstractLiteral $ AbsLitMatrix
167 (DomainInt TagInt [RangeBounded 1 2])
168 [ Comprehension body
169 $ gocBefore
170 ++ [ Generator (GenInExpr pat (mkModifier x)) ]
171 ++ gocAfter
172 , Comprehension body
173 $ gocBefore
174 ++ [ Generator (GenInExpr pat (mkModifier y))
175 , Condition [essence| !(&i in &x) |]
176 ]
177 ++ gocAfter
178 ]
179 )
180 theRule _ = na "rule_Union"
181
182
183 rule_Difference :: Rule
184 rule_Difference = "set-difference" `namedRule` theRule where
185 theRule (Comprehension body gensOrConds) = do
186 (gocBefore, (pat, iPat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
187 Generator (GenInExpr pat@(Single iPat) expr) -> return (pat, iPat, expr)
188 _ -> na "rule_Difference"
189 (mkModifier, s) <- match opModifier expr
190 (x, y) <- match opMinus s
191 tx <- typeOf x
192 case tx of
193 TypeSet{} -> return ()
194 TypeMSet{} -> return ()
195 TypeFunction{} -> return ()
196 TypeRelation{} -> return ()
197 _ -> failDoc "type incompatibility in difference operator"
198 let i = Reference iPat Nothing
199 return
200 ( "Horizontal rule for set difference"
201 , return $
202 Comprehension body
203 $ gocBefore
204 ++ [ Generator (GenInExpr pat (mkModifier x))
205 , Condition [essence| !(&i in &y) |]
206 ]
207 ++ gocAfter
208 )
209 theRule _ = na "rule_Difference"
210
211
212 rule_PowerSet_Difference :: Rule
213 rule_PowerSet_Difference = "set-powerSet-difference" `namedRule` theRule where
214 theRule (Comprehension body gensOrConds) = do
215 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
216 Generator (GenInExpr pat expr) -> return (pat, expr)
217 _ -> na "rule_PowerSet_Difference"
218 setExpr <- match opPowerSet expr
219 (x, y) <- match opMinus setExpr
220 let patAsExpr = patternToExpr pat
221 return
222 ( "Horizontal rule for set powerSet difference"
223 , return $
224 Comprehension body
225 $ gocBefore
226 ++ [ Generator (GenInExpr pat (make opPowerSet x))
227 , Condition [essence| !(&patAsExpr subsetEq &y) |]
228 ]
229 ++ gocAfter
230 )
231 theRule _ = na "rule_PowerSet_Difference"
232
233
234 rule_PowerSet_Comprehension :: Rule
235 rule_PowerSet_Comprehension = "set-powerSet-comprehension" `namedRule` theRule where
236 theRule (Comprehension body gensOrConds) = do
237 (gocBefore, (patName, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
238 Generator (GenInExpr (Single patName) expr) -> return (patName, expr)
239 _ -> na "rule_PowerSet_Comprehension"
240 s <- match opPowerSet expr
241 sDom <- domainOf s
242 let sDom' =
243 -- only keep the maxsize attribute
244 case sDom of
245 DomainSet () (SetAttr sAttr) sInner ->
246 let
247 sAttr' =
248 case sAttr of
249 SizeAttr_None -> SizeAttr_None
250 SizeAttr_Size x -> SizeAttr_MaxSize x
251 SizeAttr_MinSize _ -> SizeAttr_None
252 SizeAttr_MaxSize x -> SizeAttr_MaxSize x
253 SizeAttr_MinMaxSize _ x -> SizeAttr_MaxSize x
254 in
255 DomainSet () (SetAttr sAttr') sInner
256 _ -> sDom
257 let pat = Single patName
258 let patAsExpr = Reference patName Nothing
259 return
260 ( "Horizontal rule for set-comprehension over powerSet"
261 , return $
262 Comprehension body
263 $ gocBefore
264 ++ [ Generator (GenDomainNoRepr pat sDom')
265 , Condition [essence| &patAsExpr subsetEq &s |]
266 ]
267 ++ gocAfter
268 )
269 theRule _ = na "rule_PowerSet_Comprehension"
270
271
272 rule_MaxMin :: Rule
273 rule_MaxMin = "set-max-min" `namedRule` theRule where
274 theRule [essence| max(&s) |] = do
275 TypeSet (TypeInt _) <- typeOf s
276 return
277 ( "Horizontal rule for set max"
278 , case () of
279 _ | Just (_, xs) <- match setLiteral s, length xs > 0 -> return $ make opMax $ fromList xs
280 _ -> do
281 (iPat, i) <- quantifiedVar
282 return [essence| max([&i | &iPat <- &s]) |]
283 )
284 theRule [essence| min(&s) |] = do
285 TypeSet (TypeInt _) <- typeOf s
286 return
287 ( "Horizontal rule for set min"
288 , case () of
289 _ | Just (_, xs) <- match setLiteral s, length xs > 0 -> return $ make opMin $ fromList xs
290 _ -> do
291 (iPat, i) <- quantifiedVar
292 return [essence| min([&i | &iPat <- &s]) |]
293 )
294 theRule _ = na "rule_MaxMin"
295
296
297 -- x in s ~~> or([ x = i | i in s ])
298 rule_In :: Rule
299 rule_In = "set-in" `namedRule` theRule where
300 theRule p = do
301 (x,s) <- match opIn p
302 TypeSet{} <- typeOf s
303 -- do not apply this rule to quantified variables
304 -- or else we might miss the opportunity to apply a more specific vertical rule
305 if referenceToComprehensionVar s
306 then na "rule_In"
307 else return ()
308 return
309 ( "Horizontal rule for set-in."
310 , do
311 (iPat, i) <- quantifiedVar
312 return [essence| exists &iPat in &s . &i = &x |]
313 )
314
315
316 rule_Card :: Rule
317 rule_Card = "set-card" `namedRule` theRule where
318 theRule p = do
319 s <- match opTwoBars p
320 case s of
321 Domain{} -> na "rule_Card"
322 _ -> return ()
323 TypeSet{} <- typeOf s
324 return
325 ( "Horizontal rule for set cardinality."
326 , do
327 mdom <- runMaybeT $ domainOf s
328 case mdom of
329 Just (DomainSet _ (SetAttr (SizeAttr_Size n)) _) -> return n
330 _ -> do
331 (iPat, _) <- quantifiedVar
332 return [essence| sum &iPat in &s . 1 |]
333 )
334
335
336 rule_CardViaFreq :: Rule
337 rule_CardViaFreq = "set-card-via-freq" `namedRule` theRule where
338 theRule [essence| freq(toMSet(&s),&x) |] = do
339 case s of
340 Domain{} -> na "rule_CardViaFreq"
341 _ -> return ()
342 TypeSet{} <- typeOf s
343 return
344 ( "Horizontal rule for set cardinality."
345 , return [essence| toInt(&x in &s) |]
346 )
347 theRule _ = na "rule_CardViaFreq"
348
349
350 rule_Param_MinOfSet :: Rule
351 rule_Param_MinOfSet = "param-min-of-set" `namedRule` theRule where
352 theRule [essence| min(&s) |] = do
353 TypeSet (TypeInt _) <- typeOf s
354 unless (categoryOf s == CatParameter) $ na "rule_Param_MinOfSet"
355 isDomainExpr s
356 DomainSet _ _ inner <- domainOf s
357 case inner of
358 DomainInt _ rs | isInfinite rs -> na "rule_Param_MaxOfSet"
359 _ -> return ()
360 return
361 ( "min of a parameter set"
362 , case inner of
363 DomainInt _ [RangeBounded l _] -> return l
364 _ -> do
365 (iPat, i) <- quantifiedVar
366 return [essence| min([ &i | &iPat : &inner ]) |]
367 )
368 theRule _ = na "rule_Param_MinOfSet"
369
370
371 rule_Param_MaxOfSet :: Rule
372 rule_Param_MaxOfSet = "param-max-of-set" `namedRule` theRule where
373 theRule [essence| max(&s) |] = do
374 TypeSet (TypeInt _) <- typeOf s
375 unless (categoryOf s == CatParameter) $ na "rule_Param_MaxOfSet"
376 isDomainExpr s
377 DomainSet _ _ inner <- domainOf s
378 case inner of
379 DomainInt _ rs | isInfinite rs -> na "rule_Param_MaxOfSet"
380 _ -> return ()
381 return
382 ( "max of a parameter set"
383 , case inner of
384 DomainInt _ [RangeBounded _ u] -> return u
385 _ -> do
386 (iPat, i) <- quantifiedVar
387 return [essence| max([ &i | &iPat : &inner ]) |]
388 )
389 theRule _ = na "rule_Param_MaxOfSet"
390
391
392 rule_Param_Card :: Rule
393 rule_Param_Card = "param-card-of-set" `namedRule` theRule where
394 theRule [essence| |&s| |] = do
395 TypeSet (TypeInt _) <- typeOf s
396 unless (categoryOf s == CatParameter) $ na "rule_Param_Card"
397 DomainSet _ (SetAttr (SizeAttr_Size n)) _ <- domainOf s
398 return
399 ( "cardinality of a parameter set"
400 , return n
401 )
402 theRule _ = na "rule_Param_Card"