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