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