never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Horizontal.Function where
4
5 import Conjure.Rules.Import
6
7 -- uniplate
8 import Data.Generics.Uniplate.Zipper as Zipper ( up, hole )
9
10
11 rule_Comprehension_Literal :: Rule
12 rule_Comprehension_Literal = "function-comprehension-literal" `namedRule` theRule where
13 theRule (Comprehension body gensOrConds) = do
14 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \case
15 Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDefs [opToSet,opToMSet,opToRelation] expr)
16 _ -> na "rule_Comprehension_Literal"
17 (TypeFunction fr to, elems) <- match functionLiteral expr
18 let outLiteral = make matrixLiteral
19 (TypeMatrix (TypeInt TagInt) (TypeTuple [fr,to]))
20 (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength elems))])
21 [ AbstractLiteral (AbsLitTuple [a,b])
22 | (a,b) <- elems
23 ]
24 let upd val old = lambdaToFunction pat old val
25 return
26 ( "Comprehension on function literals"
27 , do
28 (iPat, i) <- quantifiedVar
29 return $ Comprehension (upd i body)
30 $ gocBefore
31 ++ [Generator (GenInExpr iPat outLiteral)]
32 ++ transformBi (upd i) gocAfter
33 )
34 theRule _ = na "rule_Comprehension_Literal"
35
36
37 rule_Eq :: Rule
38 rule_Eq = "function-eq" `namedRule` theRule where
39 theRule [essence| &x = &y |] = do
40 case x of WithLocals{} -> na "bubble-delay" ; _ -> return ()
41 case y of WithLocals{} -> na "bubble-delay" ; _ -> return ()
42 TypeFunction{} <- typeOf x
43 TypeFunction{} <- typeOf y
44 return
45 ( "Horizontal rule for function equality"
46 , do
47 (iPat, i) <- quantifiedVar
48 return [essence|
49 (forAll &iPat in &x . &y(&i[1]) = &i[2])
50 /\
51 (forAll &iPat in &y . &x(&i[1]) = &i[2])
52 |]
53 )
54 theRule _ = na "rule_Eq"
55
56
57 rule_Neq :: Rule
58 rule_Neq = "function-neq" `namedRule` theRule where
59 theRule [essence| &x != &y |] = do
60 case x of WithLocals{} -> na "bubble-delay" ; _ -> return ()
61 case y of WithLocals{} -> na "bubble-delay" ; _ -> return ()
62 TypeFunction{} <- typeOf x
63 TypeFunction{} <- typeOf y
64 return
65 ( "Horizontal rule for function dis-equality"
66 , do
67 (iPat, i) <- quantifiedVar
68 return [essence|
69 (exists &iPat in &x . !(&i in &y))
70 \/
71 (exists &iPat in &y . !(&i in &x))
72 |]
73 )
74 theRule _ = na "rule_Neq"
75
76
77 rule_SubsetEq :: Rule
78 rule_SubsetEq = "function-subsetEq" `namedRule` theRule where
79 theRule [essence| &x subsetEq &y |] = do
80 case x of WithLocals{} -> na "bubble-delay" ; _ -> return ()
81 case y of WithLocals{} -> na "bubble-delay" ; _ -> return ()
82 TypeFunction{} <- typeOf x
83 TypeFunction{} <- typeOf y
84 return
85 ( "Horizontal rule for function subsetEq"
86 , do
87 (iPat, i) <- quantifiedVar
88 return [essence|
89 (forAll &iPat in &x . &y(&i[1]) = &i[2])
90 |]
91 )
92 theRule _ = na "rule_SubsetEq"
93
94
95 rule_Subset :: Rule
96 rule_Subset = "function-subset" `namedRule` theRule where
97 theRule [essence| &x subset &y |] = do
98 case x of WithLocals{} -> na "bubble-delay" ; _ -> return ()
99 case y of WithLocals{} -> na "bubble-delay" ; _ -> return ()
100 TypeFunction{} <- typeOf x
101 TypeFunction{} <- typeOf y
102 return
103 ( "Horizontal rule for function subset"
104 , return [essence| &x subsetEq &y /\ &x != &y |]
105 )
106 theRule _ = na "rule_Subset"
107
108
109 rule_Supset :: Rule
110 rule_Supset = "function-supset" `namedRule` theRule where
111 theRule [essence| &x supset &y |] = do
112 case x of WithLocals{} -> na "bubble-delay" ; _ -> return ()
113 case y of WithLocals{} -> na "bubble-delay" ; _ -> return ()
114 TypeFunction{} <- typeOf x
115 TypeFunction{} <- typeOf y
116 return
117 ( "Horizontal rule for function supset"
118 , return [essence| &y subset &x |]
119 )
120 theRule _ = na "rule_Supset"
121
122
123 rule_SupsetEq :: Rule
124 rule_SupsetEq = "function-subsetEq" `namedRule` theRule where
125 theRule [essence| &x supsetEq &y |] = do
126 case x of WithLocals{} -> na "bubble-delay" ; _ -> return ()
127 case y of WithLocals{} -> na "bubble-delay" ; _ -> return ()
128 TypeFunction{} <- typeOf x
129 TypeFunction{} <- typeOf y
130 return
131 ( "Horizontal rule for function supsetEq"
132 , return [essence| &y subsetEq &x |]
133 )
134 theRule _ = na "rule_SupsetEq"
135
136
137 rule_Inverse :: Rule
138 rule_Inverse = "function-inverse" `namedRule` theRule where
139 theRule [essence| inverse(&a, &b) |] = do
140 case a of WithLocals{} -> na "bubble-delay" ; _ -> return ()
141 case b of WithLocals{} -> na "bubble-delay" ; _ -> return ()
142 TypeFunction{} <- typeOf a
143 TypeFunction{} <- typeOf b
144 return
145 ( "Horizontal rule for function inverse"
146 , do
147 (iPat, i) <- quantifiedVar
148 return
149 [essence|
150 (forAll &iPat in &a . &b(&i[2]) = &i[1])
151 /\
152 (forAll &iPat in &b . &a(&i[2]) = &i[1])
153 |]
154 )
155 theRule _ = na "rule_Inverse"
156
157
158 rule_Comprehension_PreImage :: Rule
159 rule_Comprehension_PreImage = "function-preImage" `namedRule` theRule where
160 theRule (Comprehension body gensOrConds) = do
161 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
162 Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDefs [opToSet,opToMSet] expr)
163 _ -> na "rule_Comprehension_PreImage"
164 (func, img) <- match opPreImage expr
165 TypeFunction{} <- typeOf func
166 let upd val old = lambdaToFunction pat old val
167 return
168 ( "Mapping over the preImage of a function"
169 , do
170 (jPat, j) <- quantifiedVar
171 let val = [essence| &j[1] |]
172 return $
173 Comprehension
174 (upd val body)
175 $ gocBefore
176 ++ [ Generator (GenInExpr jPat func)
177 , Condition [essence| &j[2] = &img |]
178 ]
179 ++ transformBi (upd val) gocAfter
180 )
181 theRule _ = na "rule_Comprehension_PreImage"
182
183
184 rule_Card :: Rule
185 rule_Card = "function-cardinality" `namedRule` theRule where
186 theRule [essence| |&f| |] = do
187 TypeFunction{} <- typeOf f
188 dom <- domainOf f
189 return
190 ( "Function cardinality"
191 , case dom of
192 DomainFunction _ (FunctionAttr (SizeAttr_Size n) _ _) _ _
193 -> return n
194 DomainFunction _ (FunctionAttr _ _ jectivity) _ innerTo
195 | jectivity `elem` [JectivityAttr_Surjective, JectivityAttr_Bijective]
196 -> domainSizeOf innerTo
197 DomainFunction _ (FunctionAttr _ PartialityAttr_Total _) innerFr _
198 -> domainSizeOf innerFr
199 _ -> return [essence| |toSet(&f)| |]
200 )
201 theRule _ = na "rule_Card"
202
203
204 rule_Comprehension_Defined :: Rule
205 rule_Comprehension_Defined = "function-defined" `namedRule` theRule where
206 theRule (Comprehension body gensOrConds) = do
207 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
208 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
209 _ -> na "rule_Comprehension_Defined"
210 func <- match opDefined expr
211 TypeFunction{} <- typeOf func
212 let upd val old = lambdaToFunction pat old val
213 return
214 ( "Mapping over defined(f)"
215 , do
216 (iPat, i) <- quantifiedVar
217 let i1 = [essence| &i[1] |]
218 return $
219 Comprehension
220 (upd i1 body)
221 $ gocBefore
222 ++ [ Generator (GenInExpr iPat func) ]
223 ++ transformBi (upd i1) gocAfter
224 )
225 theRule _ = na "rule_Comprehension_Defined"
226
227
228 rule_Comprehension_Range :: Rule
229 rule_Comprehension_Range = "function-range" `namedRuleZ` theRule where
230
231 theRule z p = do
232 should <- shouldRemoveDuplicates z
233 if should
234 then theRule_shouldRemoveDuplicates p
235 else theRule_noRemoveDuplicates p
236
237 -- keep going up, until finding a quantifier
238 -- when found, return whether this quantifier requires us to remove duplicates or not
239 -- if none exists, do not apply the rule.
240 -- (or maybe we should call bug right ahead, it can't be anything else.)
241 shouldRemoveDuplicates z0 =
242 case Zipper.up z0 of
243 Nothing -> na "rule_Comprehension_Range shouldRemoveDuplicates 1"
244 Just z -> do
245 let h = Zipper.hole z
246 case ( match opAnd h, match opOr h, match opSum h
247 , match opMin h, match opMax h ) of
248 (Just{}, _, _, _, _) -> return False
249 (_, Just{}, _, _, _) -> return False
250 (_, _, Just{}, _, _) -> return True
251 (_, _, _, Just{}, _) -> return False
252 (_, _, _, _, Just{}) -> return False
253 _ -> na "rule_Comprehension_Range shouldRemoveDuplicates 2"
254 -- case Zipper.up z of
255 -- Nothing -> na "queryQ"
256 -- Just u -> queryQ u
257
258 theRule_shouldRemoveDuplicates (Comprehension body gensOrConds) = do
259
260 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \case
261 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
262 _ -> na "rule_Comprehension_Range"
263 func <- match opRange expr
264 TypeFunction{} <- typeOf func
265 DomainFunction _ attrs _domFr domTo <- domainOf func
266 let upd val old = lambdaToFunction pat old val
267 let
268 isInjective =
269 case attrs of
270 FunctionAttr _ _ JectivityAttr_Injective -> True
271 FunctionAttr _ _ JectivityAttr_Bijective -> True
272 _ -> False
273
274 -- the range is already alldiff
275 caseInjective = do
276 (iPat, i) <- quantifiedVar
277 let i2 = [essence| &i[2] |]
278 return $
279 Comprehension
280 (upd i2 body)
281 $ gocBefore
282 ++ [ Generator (GenInExpr iPat func) ]
283 ++ transformBi (upd i2) gocAfter
284
285 -- this is the expensive case: introduce an aux set for the range to make it alldiff
286 caseNonInjective = do
287 (auxName, aux) <- auxiliaryVar
288 (jPat, j) <- quantifiedVar
289 (kPat, k) <- quantifiedVar
290 (lPat, l) <- quantifiedVar
291 let k2 = [essence| &k[2] |]
292 let l2 = [essence| &l[2] |]
293 return $ WithLocals
294 (Comprehension
295 (upd j body)
296 $ gocBefore
297 ++ [ Generator (GenInExpr jPat aux) ]
298 ++ transformBi (upd j) gocAfter)
299 (AuxiliaryVars
300 [ Declaration (FindOrGiven LocalFind auxName (DomainSet def def (forgetRepr domTo)))
301 , SuchThat
302 [ make opAnd $ Comprehension
303 [essence| &k2 in &aux |]
304 [ Generator (GenInExpr kPat func) ]
305 , make opAnd $
306 Comprehension
307 (make opOr $ Comprehension
308 [essence| &l2 = &k |]
309 [ Generator (GenInExpr lPat func) ]
310 )
311 [ Generator (GenInExpr kPat aux) ]
312 ]
313 ])
314
315 when isInjective $
316 unless (null [ () | DomainAny{} <- universe domTo ]) $
317 na "Cannot compute the domain of range(f)"
318
319 return
320 ( "Mapping over range(f)"
321 , if isInjective
322 then caseInjective
323 else caseNonInjective
324 )
325 theRule_shouldRemoveDuplicates _ = na "rule_Comprehension_Range"
326
327 theRule_noRemoveDuplicates (Comprehension body gensOrConds) = do
328 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \case
329 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
330 _ -> na "rule_Comprehension_Range"
331 func <- match opRange expr
332 TypeFunction{} <- typeOf func
333 let upd val old = lambdaToFunction pat old val
334 return
335 ( "Mapping over range(f)"
336 , do
337 (iPat, i) <- quantifiedVar
338 let i2 = [essence| &i[2] |]
339 return $ Comprehension (upd i2 body)
340 $ gocBefore
341 ++ [Generator (GenInExpr iPat func)]
342 ++ transformBi (upd i2) gocAfter
343 )
344 theRule_noRemoveDuplicates _ = na "rule_Comprehension_Range"
345
346
347 -- TODO: What about duplicates for sum, product, etc?
348 rule_Param_DefinedRange :: Rule
349 rule_Param_DefinedRange = "param-DefinedRange-of-function" `namedRule` theRule where
350 theRule p = do
351 unless (categoryOf p == CatParameter) $ na "rule_Param_DefinedRange"
352 (_reducerType, _, mk, p2) <- match opReducer p
353 (index, f) <- case p2 of
354 [essence| defined(&f) |] -> return (1, f)
355 [essence| range(&f) |] -> return (2, f)
356 _ -> na "rule_Param_DefinedRange"
357 return
358 ( "rule_Param_DefinedRange"
359 , do
360 (iPat, i) <- quantifiedVar
361 return $ mk $ [essence| [ &i[&index] | &iPat <- &f ] |]
362 )
363
364
365 rule_Comprehension_Defined_Size :: Rule
366 rule_Comprehension_Defined_Size = "function-defined-size" `namedRule` theRule where
367 theRule [essence| size(defined(&func), &n) |] = do
368 DomainFunction _ _ domFr _domTo <- domainOf func
369 return
370 ( "size(defined(func), n)"
371 , do
372 (auxName, aux) <- auxiliaryVar
373 (kPat, k) <- quantifiedVar
374 (lPat, l) <- quantifiedVar
375 let k1 = [essence| &k[1] |]
376 let l1 = [essence| &l[1] |]
377 return $ WithLocals
378 (fromBool True)
379 (AuxiliaryVars
380 [ Declaration (FindOrGiven LocalFind auxName
381 (DomainSet def (SetAttr (SizeAttr_Size n)) (forgetRepr domFr)))
382 , SuchThat
383 [ make opAnd $ Comprehension
384 [essence| &k1 in &aux |]
385 [ Generator (GenInExpr kPat func) ]
386 , make opAnd $
387 Comprehension
388 (make opOr $ Comprehension
389 [essence| &l1 = &k |]
390 [ Generator (GenInExpr lPat func) ]
391 )
392 [ Generator (GenInExpr kPat aux) ]
393 ]
394 ])
395 )
396 theRule _ = na "rule_Comprehension_Defined_Size"
397
398
399 rule_Comprehension_Range_Size :: Rule
400 rule_Comprehension_Range_Size = "function-range-size" `namedRule` theRule where
401 theRule [essence| size(range(&func), &n) |] = do
402 DomainFunction _ _ _domFr domTo <- domainOf func
403 return
404 ( "size(range(func), n)"
405 , do
406 (auxName, aux) <- auxiliaryVar
407 (kPat, k) <- quantifiedVar
408 (lPat, l) <- quantifiedVar
409 let k2 = [essence| &k[2] |]
410 let l2 = [essence| &l[2] |]
411 return $ WithLocals
412 (fromBool True)
413 (AuxiliaryVars
414 [ Declaration (FindOrGiven LocalFind auxName
415 (DomainSet def (SetAttr (SizeAttr_Size n)) (forgetRepr domTo)))
416 , SuchThat
417 [ make opAnd $ Comprehension
418 [essence| &k2 in &aux |]
419 [ Generator (GenInExpr kPat func) ]
420 , make opAnd $
421 Comprehension
422 (make opOr $ Comprehension
423 [essence| &l2 = &k |]
424 [ Generator (GenInExpr lPat func) ]
425 )
426 [ Generator (GenInExpr kPat aux) ]
427 ]
428 ])
429 )
430 theRule _ = na "rule_Comprehension_Range_Size"
431
432
433 rule_In :: Rule
434 rule_In = "function-in" `namedRule` theRule where
435 theRule [essence| &x in &f |] = do
436 TypeFunction{} <- typeOf f
437 return
438 ( "Function membership to function image."
439 , return [essence| &f(&x[1]) = &x[2] |]
440 )
441 theRule _ = na "rule_In"
442
443
444 rule_Restrict_Image :: Rule
445 rule_Restrict_Image = "function-restrict-image" `namedRule` theRule where
446 theRule p = do
447 (func', arg) <- match opImage p
448 (func , dom) <- match opRestrict func'
449 TypeFunction{} <- typeOf func
450 return
451 ( "Function image on a restricted function."
452 , do
453 (iPat, i) <- quantifiedVar
454 let bob = [essence| exists &iPat : &dom . &i = &arg |]
455 return $ WithLocals (make opImage func arg) (DefinednessConstraints [bob])
456 )
457
458
459 rule_Restrict_Comprehension :: Rule
460 rule_Restrict_Comprehension = "function-restrict-comprehension" `namedRule` theRule where
461 theRule (Comprehension body gensOrConds) = do
462 (gocBefore, (iPat, iPatName, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
463 Generator (GenInExpr iPat@(Single iPatName) expr) -> return (iPat, iPatName, expr)
464 _ -> na "rule_Restrict_Comprehension"
465 (func, dom) <- match opRestrict expr
466 TypeFunction{} <- typeOf func
467 return
468 ( "Mapping over restrict(func, dom)"
469 , do
470 (jPat, j) <- quantifiedVar
471 let i = Reference iPatName Nothing
472 return $ Comprehension body
473 $ gocBefore
474 ++ [ Generator (GenInExpr iPat func)
475 , Condition [essence| exists &jPat : &dom . &j = &i[1] |]
476 ]
477 ++ gocAfter
478 )
479 theRule _ = na "rule_Restrict_Comprehension"
480
481
482 -- image(f,x) can be nasty for non-total functions.
483 -- 1. if f is a total function, it can readily be replaced by a set expression.
484 -- 2.1. if f isn't total, and if the return type is right, it will always end up as a generator for a comprehension.
485 -- a vertical rule is needed for such cases.
486 -- 2.2. if the return type is not "right", i.e. it is a bool or an int, i.e. sth we cannot quantify over,
487 -- the vertical rule is harder.
488
489
490 -- | f(x) : bool ~~> or([ b | (a,b) <- f, a = x])
491 rule_Image_Bool :: Rule
492 rule_Image_Bool = "function-image-bool" `namedRule` theRule where
493 theRule p = do
494 (func, arg) <- match opImage p
495 case match opRestrict func of
496 Nothing -> return ()
497 Just{} -> na "rule_Image_Bool" -- do not use this rule for restricted functions
498 TypeFunction _ TypeBool <- typeOf func
499 return
500 ( "Function image, bool."
501 , do
502 (iPat, i) <- quantifiedVar
503 return $ make opOr $ Comprehension [essence| &i[2] |]
504 [ Generator (GenInExpr iPat func)
505 , Condition [essence| &i[1] = &arg |]
506 ]
507 )
508
509
510 -- | f(x)[i] : bool ~~> or([ b[i] | (a,b) <- f, a = x]) "matrix indexing"
511 rule_Image_BoolMatrixIndexed :: Rule
512 rule_Image_BoolMatrixIndexed = "function-image-BoolMatrixIndexed" `namedRule` theRule where
513 theRule p = do
514 (matrix, indices) <- match opMatrixIndexing p
515 (func, arg) <- match opImage matrix
516 TypeFunction _ (TypeMatrix _ TypeBool) <- typeOf func
517 return
518 ( "Function image, matrix of bool."
519 , do
520 (iPat, i) <- quantifiedVar
521 let i2 = make opMatrixIndexing [essence| &i[2] |] indices
522 return $ make opOr $ Comprehension i2
523 [ Generator (GenInExpr iPat func)
524 , Condition [essence| &i[1] = &arg |]
525 ]
526 )
527
528
529 -- | f(x)[i] : bool ~~> or([ b[i] | (a,b) <- f, a = x]) "tuple indexing"
530 rule_Image_BoolTupleIndexed :: Rule
531 rule_Image_BoolTupleIndexed = "function-image-BoolTupleIndexed" `namedRule` theRule where
532 theRule p = do
533 (matrix, index) <- match opIndexing p
534 (func, arg) <- match opImage matrix
535 TypeFunction _ (TypeTuple ts) <- typeOf func
536 iInt <- match constantInt index
537 case atMay ts (fromInteger (iInt-1)) of
538 Just TypeBool -> return ()
539 _ -> na "rule_Image_BoolTupleIndexed"
540 return
541 ( "Function image, tuple of bool."
542 , do
543 (iPat, i) <- quantifiedVar
544 let i2 = make opIndexing [essence| &i[2] |] index
545 return $ make opOr $ Comprehension i2
546 [ Generator (GenInExpr iPat func)
547 , Condition [essence| &i[1] = &arg |]
548 ]
549 )
550
551
552 -- | f(x) : int ~~> sum([ b | (a,b) <- f, a = x])
553 rule_Image_Int :: Rule
554 rule_Image_Int = "function-image-int" `namedRule` theRule where
555 theRule p = do
556 (func, arg) <- match opImage p
557 case match opRestrict func of
558 Nothing -> return ()
559 Just{} -> na "rule_Image_Int" -- do not use this rule for restricted functions
560 TypeFunction _ (TypeInt _) <- typeOf func
561 return
562 ( "Function image, int."
563 , do
564 (iPat, i) <- quantifiedVar
565 let val = make opSum $ Comprehension [essence| &i[2] |]
566 [ Generator (GenInExpr iPat func)
567 , Condition [essence| &i[1] = &arg |]
568 ]
569 let isDefined = [essence| &arg in defined(&func) |]
570 return $ WithLocals val (DefinednessConstraints [isDefined])
571 )
572
573
574 -- | f(x)[i] : int ~~> sum([ b[i] | (a,b) <- f, a = x]) "matrix indexing"
575 rule_Image_IntMatrixIndexed :: Rule
576 rule_Image_IntMatrixIndexed = "function-image-IntMatrixIndexed" `namedRule` theRule where
577 theRule p = do
578 (matrix, indices) <- match opMatrixIndexing p
579 (func, arg) <- match opImage matrix
580 TypeFunction _ (TypeMatrix _ (TypeInt _)) <- typeOf func
581 return
582 ( "Function image, matrix of int."
583 , do
584 (iPat, i) <- quantifiedVar
585 let i2 = make opMatrixIndexing [essence| &i[2] |] indices
586 let val = make opSum $ Comprehension i2
587 [ Generator (GenInExpr iPat func)
588 , Condition [essence| &i[1] = &arg |]
589 ]
590 let isDefined = [essence| &arg in defined(&func) |]
591 return $ WithLocals val (DefinednessConstraints [isDefined])
592 )
593
594
595 -- | f(x)[i] : int ~~> sum([ b[i] | (a,b) <- f, a = x]) "tuple indexing"
596 rule_Image_IntTupleIndexed :: Rule
597 rule_Image_IntTupleIndexed = "function-image-IntTupleIndexed" `namedRule` theRule where
598 theRule p = do
599 (matrix, index) <- match opIndexing p
600 (func, arg) <- match opImage matrix
601 TypeFunction _ (TypeTuple ts) <- typeOf func
602 iInt <- match constantInt index
603 case atMay ts (fromInteger (iInt-1)) of
604 Just (TypeInt _) -> return ()
605 _ -> na "rule_Image_IntTupleIndexed"
606 return
607 ( "Function image, tuple of int."
608 , do
609 (iPat, i) <- quantifiedVar
610 let i2 = make opIndexing [essence| &i[2] |] index
611 let val = make opSum $ Comprehension i2
612 [ Generator (GenInExpr iPat func)
613 , Condition [essence| &i[1] = &arg |]
614 ]
615 let isDefined = [essence| &arg in defined(&func) |]
616 return $ WithLocals val (DefinednessConstraints [isDefined])
617 )
618
619
620 -- | [ ..i.. | i <- f(x), ..i.. ] ~~>
621 -- [ ..j.. | (a,b) <- f, a = i, j <- b, ..j.. ]
622 rule_Comprehension_Image :: Rule
623 rule_Comprehension_Image = "function-image-comprehension" `namedRule` theRule where
624 theRule (Comprehension body gensOrConds) = do
625 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
626 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
627 _ -> na "rule_Comprehension_Image"
628 (mkModifier, expr2) <- match opModifier expr
629 (func, arg) <- match opImage expr2
630 TypeFunction{} <- typeOf func
631 case match opRestrict func of
632 Nothing -> return ()
633 Just{} -> na "rule_Comprehension_Image" -- do not use this rule for restricted functions
634 let upd val old = lambdaToFunction pat old val
635 return
636 ( "Mapping over the image of a function"
637 , do
638 (iPat, i) <- quantifiedVar
639 (jPat, j) <- quantifiedVar
640 return $ Comprehension
641 (upd j body)
642 $ gocBefore
643 ++ [ Generator (GenInExpr iPat func)
644 , Condition [essence| &i[1] = &arg |]
645 , Generator (GenInExpr jPat (mkModifier [essence| &i[2] |]))
646 ]
647 ++ transformBi (upd j) gocAfter
648 )
649 theRule _ = na "rule_Comprehension_Image"
650
651
652 -- | [ ..i.. | i <- imageSet(f,x), ..i.. ] ~~>
653 -- [ ..b.. | (a,b) <- f, a = i, ..b.. ]
654 rule_Comprehension_ImageSet :: Rule
655 rule_Comprehension_ImageSet = "function-imageSet-comprehension" `namedRule` theRule where
656 theRule (Comprehension body gensOrConds) = do
657 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
658 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
659 _ -> na "rule_Comprehension_ImageSet"
660 (mkModifier, expr2) <- match opModifierNoP expr
661 (func, arg) <- match opImageSet expr2
662 TypeFunction{} <- typeOf func
663 case match opRestrict func of
664 Nothing -> return ()
665 Just{} -> na "rule_Comprehension_ImageSet" -- do not use this rule for restricted functions
666 let upd val old = lambdaToFunction pat old val
667 return
668 ( "Mapping over the imageSet of a function"
669 , do
670 (iPat, i) <- quantifiedVar
671 return $ Comprehension
672 (upd [essence| &i[2] |] body)
673 $ gocBefore
674 ++ [ Generator (GenInExpr iPat (mkModifier func))
675 , Condition [essence| &i[1] = &arg |]
676 ]
677 ++ transformBi (upd [essence| &i[2] |]) gocAfter
678 )
679 theRule _ = na "rule_Comprehension_ImageSet"
680
681
682 -- | f(x) <=lex m ~~> and([ b <=lex m | (a,b) <- f, a = x])
683 rule_Image_Matrix_LexLhs :: Rule
684 rule_Image_Matrix_LexLhs = "function-image-matrix-lexlhs" `namedRule` theRule where
685 theRule p = do
686 (mkLex, (lhs,rhs)) <- match opLex p
687 (func, arg) <- match opImage lhs
688 TypeFunction{} <- typeOf func
689 return
690 ( "Function image, matrix as an argument to a lex operator."
691 , do
692 (iPat, i) <- quantifiedVar
693 let val = make opAnd $ Comprehension (mkLex [essence| &i[2] |] rhs)
694 [ Generator (GenInExpr iPat func)
695 , Condition [essence| &i[1] = &arg |]
696 ]
697 let isDefined = [essence| &arg in defined(&func) |]
698 return $ WithLocals val (DefinednessConstraints [isDefined])
699 )
700
701
702 -- | f(x) <=lex m ~~> and([ b <=lex m | (a,b) <- f, a = x])
703 rule_Image_Matrix_LexRhs :: Rule
704 rule_Image_Matrix_LexRhs = "function-image-matrix-lexrhs" `namedRule` theRule where
705 theRule p = do
706 (mkLex, (lhs,rhs)) <- match opLex p
707 (func, arg) <- match opImage rhs
708 TypeFunction{} <- typeOf func
709 return
710 ( "Function image, matrix as an argument to a lex operator."
711 , do
712 (iPat, i) <- quantifiedVar
713 let val = make opAnd $ Comprehension (mkLex lhs [essence| &i[2] |])
714 [ Generator (GenInExpr iPat func)
715 , Condition [essence| &i[1] = &arg |]
716 ]
717 let isDefined = [essence| &arg in defined(&func) |]
718 return $ WithLocals val (DefinednessConstraints [isDefined])
719 )
720
721
722 rule_Defined_Intersect :: Rule
723 rule_Defined_Intersect = "function-Defined-intersect" `namedRule` theRule where
724 theRule (Comprehension body gensOrConds) = do
725 (gocBefore, (pat, iPat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
726 Generator (GenInExpr pat@(Single iPat) expr) -> return (pat, iPat, expr)
727 _ -> na "rule_Defined_Intersect"
728 f <- match opDefined expr
729 (x, y) <- match opIntersect f
730 tx <- typeOf x
731 case tx of
732 TypeFunction{} -> return ()
733 _ -> failDoc "type incompatibility in intersect operator"
734 let i = Reference iPat Nothing
735 return
736 ( "Horizontal rule for function intersection"
737 , return $
738 Comprehension body
739 $ gocBefore
740 ++ [ Generator (GenInExpr pat (make opDefined x))
741 , Condition [essence| (&i, image(&x,&i)) in &y |]
742 ]
743 ++ gocAfter
744 )
745 theRule _ = na "rule_Defined_Intersect"
746
747
748 rule_DefinedOrRange_Union :: Rule
749 rule_DefinedOrRange_Union = "function-DefinedOrRange-union" `namedRule` theRule where
750 theRule (Comprehension body gensOrConds) = do
751 (gocBefore, (pat, iPat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
752 Generator (GenInExpr pat@(Single iPat) expr) -> return (pat, iPat, expr)
753 _ -> na "rule_DefinedOrRange_Union"
754 (mk, f) <- match opDefinedOrRange expr
755 (x, y) <- match opUnion f
756 tx <- typeOf x
757 case tx of
758 TypeFunction{} -> return ()
759 _ -> failDoc "type incompatibility in union operator"
760 let mkx = mk x
761 let mky = mk y
762 let i = Reference iPat Nothing
763 return
764 ( "Horizontal rule for function union"
765 , return $ make opFlatten $ AbstractLiteral $ AbsLitMatrix
766 (DomainInt TagInt [RangeBounded 1 2])
767 [ Comprehension body
768 $ gocBefore
769 ++ [ Generator (GenInExpr pat mkx) ]
770 ++ gocAfter
771 , Comprehension body
772 $ gocBefore
773 ++ [ Generator (GenInExpr pat mky)
774 , Condition [essence| !(&i in &mkx) |]
775 ]
776 ++ gocAfter
777 ]
778 )
779 theRule _ = na "rule_DefinedOrRange_Union"
780
781
782 rule_DefinedOrRange_Difference :: Rule
783 rule_DefinedOrRange_Difference = "function-DefinedOrRange-difference" `namedRule` theRule where
784 theRule (Comprehension body gensOrConds) = do
785 (gocBefore, (pat, iPat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
786 Generator (GenInExpr pat@(Single iPat) expr) -> return (pat, iPat, expr)
787 _ -> na "rule_DefinedOrRange_Difference"
788 (mk, f) <- match opDefinedOrRange expr
789 (x, y) <- match opMinus f
790 tx <- typeOf x
791 case tx of
792 TypeFunction{} -> return ()
793 _ -> failDoc "type incompatibility in difference operator"
794 let mkx = mk x
795 let mky = mk y
796 let i = Reference iPat Nothing
797 return
798 ( "Horizontal rule for function difference"
799 , return $
800 Comprehension body
801 $ gocBefore
802 ++ [ Generator (GenInExpr pat mkx)
803 , Condition [essence| !(&i in &mky) |]
804 ]
805 ++ gocAfter
806 )
807 theRule _ = na "rule_DefinedOrRange_Difference"
808
809