never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Process.Streamlining
4 ( streamlining
5 , streamliningToStdout
6 ) where
7
8 import Conjure.Prelude
9 import Conjure.Bug
10 import Conjure.Language
11 import Conjure.Compute.DomainOf ( domainOf )
12 import Conjure.Representations.Common ( mkBinRelCons, mkBinRelConsSoft )
13
14 -- containers
15 import Data.Set as S ( singleton )
16
17
18 streamliningToStdout ::
19 MonadFailDoc m =>
20 MonadLog m =>
21 MonadUserError m =>
22 NameGen m =>
23 MonadIO m =>
24 (?typeCheckerMode :: TypeCheckerMode) =>
25 Model -> m ()
26 streamliningToStdout model = do
27 let
28 whitespace '\t' = ' '
29 whitespace '\n' = ' '
30 whitespace ch = ch
31
32 showStr :: String -> Doc
33 showStr = pretty . show
34
35 streamliners <- streamlining model
36
37 liftIO $ print $ prettyList prBraces ","
38 [ showStr (show i) <> ":" <+> prBraces (vcat
39 [ showStr "onVariable" <> ":" <+> showStr (show (pretty nm)) <> ","
40 , showStr "groups" <> ":" <+> prettyList prBrackets "," (map showStr (nub groups)) <> ","
41 , showStr "constraint" <> ":" <+> showStr (map whitespace $ show $ pretty cons)
42 ])
43 | (i, (nm, (cons, groups))) <- zip allNats streamliners
44 ]
45 traceM $ show $ "Number of streamliners: " <+> pretty (length streamliners)
46
47
48 streamlining ::
49 MonadFailDoc m =>
50 MonadLog m =>
51 MonadUserError m =>
52 NameGen m =>
53 (?typeCheckerMode :: TypeCheckerMode) =>
54 Model -> m [(Name, Streamliner)]
55 streamlining model = do
56 concatForM (mStatements model) $ \case
57 Declaration (FindOrGiven Find nm domain) -> do
58 let ref = Reference nm (Just (DeclNoRepr Find nm domain NoRegion))
59 streamliners <- streamlinersForSingleVariable ref
60 -- traceM $ show $ vcat [ "Streamliners for --" <+> pretty statement
61 -- , vcat [ nest 4 (vcat (pretty x : map pretty gs)) | (x,gs) <- streamliners ]
62 -- ]
63 return [ (nm, s) | s <- streamliners ]
64 _ -> noStreamliner
65
66
67 type StreamlinerGroup = String
68
69 type Streamliner = (Expression, [StreamlinerGroup])
70
71 type StreamlinerGen m = Expression -> m [Streamliner]
72
73 mkStreamliner
74 :: Monad m
75 => StreamlinerGroup -- the group label
76 -> Expression -- the streamlining constraint
77 -> m [Streamliner]
78 mkStreamliner grp x = return [(x, [grp])]
79
80 noStreamliner :: Monad m => m [a]
81 noStreamliner = return []
82
83 attachGroup
84 :: Monad m
85 => [StreamlinerGroup]
86 -> Expression
87 -> m Streamliner
88 attachGroup grps x = return (x, grps)
89
90
91 -- given a reference to a top level variable, produce a list of all applicable streamliners
92 streamlinersForSingleVariable ::
93 MonadFailDoc m =>
94 NameGen m =>
95 (?typeCheckerMode :: TypeCheckerMode) =>
96 StreamlinerGen m
97 streamlinersForSingleVariable x = concatMapM ($ x)
98 [ intOdd
99 , intEven
100 , intLowerHalf
101 , intUpperHalf
102
103 , onTuple 1 streamlinersForSingleVariable
104 , onTuple 2 streamlinersForSingleVariable
105 , onTuple 3 streamlinersForSingleVariable
106 , onTuple 4 streamlinersForSingleVariable
107
108 , matrixByRowBucket streamlinersForSingleVariable
109 , matrixByColBucket streamlinersForSingleVariable
110
111 , matrixAll streamlinersForSingleVariable
112 , matrixHalf streamlinersForSingleVariable
113 , matrixAtMostOne streamlinersForSingleVariable
114 , matrixApproxHalf streamlinersForSingleVariable
115 , matrixMoreThanHalf streamlinersForSingleVariable
116 , matrixLessThanHalf streamlinersForSingleVariable
117
118 , setAll streamlinersForSingleVariable
119 , setHalf streamlinersForSingleVariable
120 , setAtMostOne streamlinersForSingleVariable
121 , setApproxHalf streamlinersForSingleVariable
122 , setMoreThanHalf streamlinersForSingleVariable
123 , setLessThanHalf streamlinersForSingleVariable
124
125 , relationCardinality
126
127 , binRelAttributes
128
129 , monotonicallyIncreasing
130 , monotonicallyDecreasing
131 , smallestFirst
132 , largestFirst
133 , commutative
134 , nonCommutative
135 , associative
136 , onRange streamlinersForSingleVariable
137 , onDefined streamlinersForSingleVariable
138 -- , diagonal streamlinersForSingleVariable
139 -- , prefix streamlinersForSingleVariable
140 -- , postfix streamlinersForSingleVariable
141
142 , parts streamlinersForSingleVariable
143 , quasiRegular
144
145 ]
146
147
148 ------------------------------------------------------------------------------
149 -- Integers
150 ------------------------------------------------------------------------------
151
152
153 -- given an integer expression (which can be a reference to a decision variable),
154 -- generate a constraint forcing it to be odd
155 intOdd ::
156 MonadFailDoc m =>
157 (?typeCheckerMode :: TypeCheckerMode) =>
158 StreamlinerGen m
159 intOdd x = do
160 ty <- typeOf x
161 if typeUnify ty (TypeInt TagInt)
162 then mkStreamliner "IntOddEven" [essence| &x % 2 = 1 |]
163 else noStreamliner
164
165
166 intEven ::
167 MonadFailDoc m =>
168 (?typeCheckerMode :: TypeCheckerMode) =>
169 StreamlinerGen m
170 intEven x = do
171 ty <- typeOf x
172 if typeUnify ty (TypeInt TagInt)
173 then mkStreamliner "IntOddEven" [essence| &x % 2 = 0 |]
174 else noStreamliner
175
176
177 intLowerHalf ::
178 MonadFailDoc m =>
179 NameGen m =>
180 (?typeCheckerMode :: TypeCheckerMode) =>
181 StreamlinerGen m
182 intLowerHalf x = do
183 ty <- typeOf x
184 dom <- expandDomainReference <$> domainOf x
185 case dom of
186 DomainInt _ [RangeBounded _lower upper] -> do
187 -- traceM $ show $ "DomainInt " <+> pretty (lower, upper)
188 if typeUnify ty (TypeInt TagInt)
189 then mkStreamliner "IntLowHigh" [essence| &x <= 1 + (&upper -1) /2 |]
190 else noStreamliner
191 _ -> noStreamliner
192
193
194 intUpperHalf ::
195 MonadFailDoc m =>
196 NameGen m =>
197 (?typeCheckerMode :: TypeCheckerMode) =>
198 StreamlinerGen m
199 intUpperHalf x = do
200 ty <- typeOf x
201 dom <- expandDomainReference <$> domainOf x
202 case dom of
203 DomainInt _ [RangeBounded _lower upper] -> do
204 -- traceM $ show $ "DomainInt " <+> pretty (lower, upper)
205 if typeUnify ty (TypeInt TagInt)
206 then mkStreamliner "IntLowHigh" [essence| &x > 1 + (&upper -1) /2 |]
207 else noStreamliner
208 _ -> noStreamliner
209
210
211 ------------------------------------------------------------------------------
212 -- Matrices
213 ------------------------------------------------------------------------------
214
215
216 matrixAll ::
217 MonadFailDoc m =>
218 NameGen m =>
219 (?typeCheckerMode :: TypeCheckerMode) =>
220 StreamlinerGen m -> StreamlinerGen m
221 matrixAll innerStreamliner x = do
222 dom <- expandDomainReference <$> domainOf x
223 case dom of
224 DomainMatrix indexDom innerDom -> do
225 nm <- nextName "q"
226 -- traceM $ show $ "matrixAll nm" <+> pretty nm
227 let pat = Single nm
228 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
229
230 liftMatrix (Reference n _) | n == nm = [essence| &x[&ref] |]
231 liftMatrix p = p
232
233 innerConstraints <- transformBi liftMatrix <$> innerStreamliner ref
234 -- traceM $ show $ "maybeInnerConstraint" <+> vcat (map pretty innerConstraints)
235 forM innerConstraints $ \ (innerConstraint, grps) ->
236 attachGroup ("MatrixCardinality": grps) [essence| forAll &pat : &indexDom . &innerConstraint |]
237 _ -> noStreamliner
238
239
240 matrixAtMostOne ::
241 MonadFailDoc m =>
242 NameGen m =>
243 (?typeCheckerMode :: TypeCheckerMode) =>
244 StreamlinerGen m -> StreamlinerGen m
245 matrixAtMostOne innerStreamliner x = do
246 dom <- expandDomainReference <$> domainOf x
247 case dom of
248 DomainMatrix indexDom innerDom -> do
249 nm <- nextName "q"
250 let pat = Single nm
251 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
252
253 liftMatrix (Reference n _) | n == nm = [essence| &x[&ref] |]
254 liftMatrix p = p
255
256 innerConstraints <- transformBi liftMatrix <$> innerStreamliner ref
257 forM innerConstraints $ \ (innerConstraint, grps) ->
258 attachGroup ("MatrixCardinality": grps) [essence| 1 >= sum &pat : &indexDom . toInt(&innerConstraint) |]
259 _ -> noStreamliner
260
261
262 matrixHalf :: MonadFailDoc m =>
263 NameGen m =>
264 (?typeCheckerMode :: TypeCheckerMode) =>
265 StreamlinerGen m -> StreamlinerGen m
266 matrixHalf innerStreamliner x = do
267 dom <- expandDomainReference <$> domainOf x
268 case dom of
269 DomainMatrix indexDom innerDom -> do
270 let size = [essence| |`&indexDom`| |]
271 nm <- nextName "q"
272 let pat = Single nm
273 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
274
275 liftMatrix (Reference n _) | n == nm = [essence| &x[&ref] |]
276 liftMatrix p = p
277
278 innerConstraints <- transformBi liftMatrix <$> innerStreamliner ref
279 forM innerConstraints $ \ (innerConstraint, grps) ->
280 attachGroup ("MatrixCardinality": grps) [essence| &size / 2 = (sum &pat : &indexDom . toInt(&innerConstraint)) |]
281 _ -> noStreamliner
282
283
284 matrixApproxHalf ::
285 MonadFailDoc m =>
286 NameGen m =>
287 (?typeCheckerMode :: TypeCheckerMode) =>
288 StreamlinerGen m -> StreamlinerGen m
289 matrixApproxHalf innerStreamliner x = do
290 dom <- expandDomainReference <$> domainOf x
291 case dom of
292 DomainMatrix indexDom innerDom -> do
293 let size = [essence| |`&indexDom`| |]
294 nm <- nextName "q"
295 let pat = Single nm
296 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
297
298 liftMatrix (Reference n _) | n == nm = [essence| &x[&ref] |]
299 liftMatrix p = p
300
301 innerConstraints <- transformBi liftMatrix <$> innerStreamliner ref
302 forM innerConstraints $ \ (innerConstraint, grps) ->
303 attachGroup ("MatrixCardinality": grps) [essence|
304 (&size/2) + 1 >= (sum &pat : &indexDom . toInt(&innerConstraint)) /\
305 (&size/2 -1) <= (sum &pat : &indexDom . toInt(&innerConstraint))
306 |]
307 _ -> noStreamliner
308
309
310 matrixMoreThanHalf ::
311 MonadFailDoc m =>
312 NameGen m =>
313 (?typeCheckerMode :: TypeCheckerMode) =>
314 StreamlinerGen m -> StreamlinerGen m
315 matrixMoreThanHalf innerStreamliner x = do
316 dom <- expandDomainReference <$> domainOf x
317 case dom of
318 DomainMatrix indexDom innerDom -> do
319 let size = [essence| |`&indexDom`| |]
320 nm <- nextName "q"
321 let pat = Single nm
322 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
323
324 liftMatrix (Reference n _) | n == nm = [essence| &x[&ref] |]
325 liftMatrix p = p
326
327 innerConstraints <- transformBi liftMatrix <$> innerStreamliner ref
328 forM innerConstraints $ \ (innerConstraint, grps) ->
329 attachGroup ("MatrixCardinality": grps) [essence|
330 (&size/2) <= (sum &pat : &indexDom . toInt(&innerConstraint))
331 |]
332 _ -> noStreamliner
333
334
335 matrixLessThanHalf ::
336 MonadFailDoc m =>
337 NameGen m =>
338 (?typeCheckerMode :: TypeCheckerMode) =>
339 StreamlinerGen m -> StreamlinerGen m
340 matrixLessThanHalf innerStreamliner x = do
341 dom <- expandDomainReference <$> domainOf x
342 case dom of
343 DomainMatrix indexDom innerDom -> do
344 let size = [essence| |`&indexDom`| |]
345 nm <- nextName "q"
346 let pat = Single nm
347 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
348
349 liftMatrix (Reference n _) | n == nm = [essence| &x[&ref] |]
350 liftMatrix p = p
351
352 innerConstraints <- transformBi liftMatrix <$> innerStreamliner ref
353 forM innerConstraints $ \ (innerConstraint, grps) ->
354 attachGroup ("MatrixCardinality": grps) [essence|
355 (&size/2) >= (sum &pat : &indexDom . toInt(&innerConstraint))
356 |]
357 _ -> noStreamliner
358
359
360 matrixByRowBucket ::
361 MonadFailDoc m =>
362 NameGen m =>
363 (?typeCheckerMode :: TypeCheckerMode) =>
364 StreamlinerGen m -> StreamlinerGen m
365 matrixByRowBucket innerStreamliner x = do
366 dom <- expandDomainReference <$> domainOf x
367 case dom of
368 DomainMatrix (DomainInt _ [RangeBounded lb ub]) innerDom@(DomainMatrix _ DomainInt{}) -> do
369 let size = [essence| &ub - &lb + 1 |]
370 let bucketSize = [essence| &size / 10 |]
371 nm <- nextName "q"
372 let pat = Single nm
373 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
374
375 liftMatrix (Reference n _) | n == nm = [essence| &x[&ref] |]
376 liftMatrix p = p
377
378 innerConstraints <- transformBi liftMatrix <$> innerStreamliner ref
379 concatForM [0..9] $ \ (bucketInt :: Integer) -> let bucket = fromInt bucketInt in
380 forM innerConstraints $ \ (innerConstraint, grps) ->
381 attachGroup (("MatrixByRowBucket-" ++ show bucketInt) : grps) [essence|
382 forAll &pat : int(&lb + &bucket * &bucketSize .. min([&ub, &lb + (&bucket+1) * &bucketSize])) . &innerConstraint
383 |]
384 _ -> noStreamliner
385
386
387
388 matrixByColBucket ::
389 MonadFailDoc m =>
390 NameGen m =>
391 (?typeCheckerMode :: TypeCheckerMode) =>
392 StreamlinerGen m -> StreamlinerGen m
393 matrixByColBucket innerStreamliner x = do
394 dom <- expandDomainReference <$> domainOf x
395 case dom of
396 DomainMatrix outerIndex (DomainMatrix (DomainInt _ [RangeBounded lb ub]) innerDom) -> do
397 let size = [essence| &ub - &lb + 1 |]
398 let bucketSize = [essence| &size / 10 |]
399
400 nmO <- nextName "q"
401 let patO = Single nmO
402 let refO = Reference nmO Nothing
403
404 nm <- nextName "q"
405 let pat = Single nm
406 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
407
408 liftMatrix (Reference n _) | n == nm = [essence| &x[&refO, &ref] |]
409 liftMatrix p = p
410
411 innerConstraints <- transformBi liftMatrix <$> innerStreamliner ref
412 concatForM [0..9] $ \ (bucketInt :: Integer) -> let bucket = fromInt bucketInt in
413 forM innerConstraints $ \ (innerConstraint, grps) ->
414 attachGroup (("MatrixByColBucket-" ++ show bucketInt) : grps) [essence|
415 forAll &patO : &outerIndex .
416 forAll &pat : int(&lb + &bucket * &bucketSize .. min([&ub, &lb + (&bucket+1) * &bucketSize])) .
417 &innerConstraint
418 |]
419 _ -> noStreamliner
420
421
422 ------------------------------------------------------------------------------
423 -- Sets and MSets
424 ------------------------------------------------------------------------------
425
426
427 setAll ::
428 MonadFailDoc m =>
429 NameGen m =>
430 (?typeCheckerMode :: TypeCheckerMode) =>
431 StreamlinerGen m -> StreamlinerGen m
432 setAll innerStreamliner x = do
433 dom <- expandDomainReference <$> domainOf x
434 let minnerDom =
435 case dom of
436 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
437 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
438 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
439 _ -> Nothing
440 case minnerDom of
441 Just (innerDom, newTag) -> do
442 nm <- nextName "q"
443 -- traceM $ show $ "setAll nm" <+> pretty nm
444 let pat = Single nm
445 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
446 innerConstraints <- innerStreamliner ref
447 -- traceM $ show $ "maybeInnerConstraint" <+> vcat (map pretty innerConstraints)
448 forM innerConstraints $ \ (innerConstraint, grps) ->
449 attachGroup (newTag: grps) [essence| forAll &pat in &x . &innerConstraint |]
450 _ -> noStreamliner
451
452
453 setAtMostOne ::
454 MonadFailDoc m =>
455 NameGen m =>
456 (?typeCheckerMode :: TypeCheckerMode) =>
457 StreamlinerGen m -> StreamlinerGen m
458 setAtMostOne innerStreamliner x = do
459 dom <- expandDomainReference <$> domainOf x
460 let minnerDom =
461 case dom of
462 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
463 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
464 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
465 _ -> Nothing
466 case minnerDom of
467 Just (innerDom, newTag) -> do
468 nm <- nextName "q"
469 let pat = Single nm
470 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
471 innerConstraints <- innerStreamliner ref
472 forM innerConstraints $ \ (innerConstraint, grps) ->
473 attachGroup (newTag: grps) [essence| 1 >= sum &pat in &x . toInt(&innerConstraint) |]
474 _ -> noStreamliner
475
476
477 setHalf ::
478 MonadFailDoc m =>
479 NameGen m =>
480 (?typeCheckerMode :: TypeCheckerMode) =>
481 StreamlinerGen m -> StreamlinerGen m
482 setHalf innerStreamliner x = do
483 dom <- expandDomainReference <$> domainOf x
484 let minnerDom =
485 case dom of
486 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
487 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
488 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
489 _ -> Nothing
490 case minnerDom of
491 Just (innerDom, newTag) -> do
492 let size = [essence| |&x| |]
493 nm <- nextName "q"
494 let pat = Single nm
495 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
496 innerConstraints <- innerStreamliner ref
497 forM innerConstraints $ \ (innerConstraint, grps) ->
498 attachGroup (newTag: grps) [essence| &size / 2 = (sum &pat in &x . toInt(&innerConstraint)) |]
499 _ -> noStreamliner
500
501
502 setApproxHalf ::
503 MonadFailDoc m =>
504 NameGen m =>
505 (?typeCheckerMode :: TypeCheckerMode) =>
506 StreamlinerGen m -> StreamlinerGen m
507 setApproxHalf innerStreamliner x = do
508 dom <- expandDomainReference <$> domainOf x
509 let minnerDom =
510 case dom of
511 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
512 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
513 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
514 _ -> Nothing
515 case minnerDom of
516 Just (innerDom, newTag) -> do
517 let size = [essence| |&x| |]
518 nm <- nextName "q"
519 let pat = Single nm
520 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
521 innerConstraints <- innerStreamliner ref
522 forM innerConstraints $ \ (innerConstraint, grps) ->
523 attachGroup (newTag: grps) [essence|
524 (&size/2) + 1 >= (sum &pat in &x . toInt(&innerConstraint)) /\
525 (&size/2 -1) <= (sum &pat in &x . toInt(&innerConstraint))
526 |]
527 _ -> noStreamliner
528
529
530 setMoreThanHalf ::
531 MonadFailDoc m =>
532 NameGen m =>
533 (?typeCheckerMode :: TypeCheckerMode) =>
534 StreamlinerGen m -> StreamlinerGen m
535 setMoreThanHalf innerStreamliner x = do
536 dom <- expandDomainReference <$> domainOf x
537 let minnerDom =
538 case dom of
539 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
540 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
541 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
542 _ -> Nothing
543 case minnerDom of
544 Just (innerDom, newTag) -> do
545 let size = [essence| |&x| |]
546 nm <- nextName "q"
547 let pat = Single nm
548 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
549 innerConstraints <- innerStreamliner ref
550 forM innerConstraints $ \ (innerConstraint, grps) ->
551 attachGroup (newTag: grps) [essence|
552 (&size/2) <= (sum &pat in &x . toInt(&innerConstraint))
553 |]
554 _ -> noStreamliner
555
556
557 setLessThanHalf ::
558 MonadFailDoc m =>
559 NameGen m =>
560 (?typeCheckerMode :: TypeCheckerMode) =>
561 StreamlinerGen m -> StreamlinerGen m
562 setLessThanHalf innerStreamliner x = do
563 dom <- expandDomainReference <$> domainOf x
564 let minnerDom =
565 case dom of
566 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
567 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
568 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
569 _ -> Nothing
570 case minnerDom of
571 Just (innerDom, newTag) -> do
572 let size = [essence| |&x| |]
573 nm <- nextName "q"
574 let pat = Single nm
575 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
576 innerConstraints <- innerStreamliner ref
577 forM innerConstraints $ \ (innerConstraint, grps) ->
578 attachGroup (newTag: grps) [essence|
579 (&size/2) >= (sum &pat in &x . toInt(&innerConstraint))
580 |]
581 _ -> noStreamliner
582
583
584 relationCardinality ::
585 MonadFailDoc m =>
586 NameGen m =>
587 (?typeCheckerMode :: TypeCheckerMode) =>
588 StreamlinerGen m
589 relationCardinality x = do
590 dom <- expandDomainReference <$> domainOf x
591 case dom of
592 DomainRelation _ _ inners -> do
593 let maxCard = make opProduct $ fromList [ [essence| |`&i`| |] | i <- inners ]
594 sequence
595 [ case lowerOrUpper of
596 "lowerBound" -> return ([essence| |&x| >= &maxCard / &slice |], [grp])
597 "upperBound" -> return ([essence| |&x| <= &maxCard / &slice |], [grp])
598 _ -> bug "relationCardinality"
599 | slice <- [1,2,4,8,16,32]
600 , lowerOrUpper <- ["LowerBound","UpperBound"]
601 , let grp = "RelationCardinality-" ++ lowerOrUpper
602 ]
603 _ -> noStreamliner
604
605
606 binRelAttributes ::
607 MonadFailDoc m =>
608 NameGen m =>
609 (?typeCheckerMode :: TypeCheckerMode) =>
610 StreamlinerGen m
611 binRelAttributes x = do
612 dom <- expandDomainReference <$> domainOf x
613 case dom of
614 -- we don't insist on inner1 == inner2 any more
615 DomainRelation _ _ [inner1, inner2] -> sequence
616 [ do
617 out <- case softness of
618 Nothing -> mkBinRelCons (BinaryRelationAttrs (S.singleton attr)) inner x
619 Just s -> mkBinRelConsSoft maxNum s (BinaryRelationAttrs (S.singleton attr)) inner x
620 return (make opAnd (fromList out), [grp])
621 | inner <- [inner1, inner2]
622 , (attr, maxNum) <- [ ( BinRelAttr_Reflexive , [essence| |`&inner`| |] )
623 , ( BinRelAttr_Irreflexive , [essence| |`&inner`| |] )
624 , ( BinRelAttr_Coreflexive , [essence| |`&inner`| * |`&inner`| |] )
625 , ( BinRelAttr_Symmetric , [essence| |`&inner`| * |`&inner`| |] )
626 , ( BinRelAttr_AntiSymmetric , [essence| |`&inner`| * |`&inner`| |] )
627 , ( BinRelAttr_ASymmetric , [essence| |`&inner`| * |`&inner`| |] )
628 , ( BinRelAttr_Transitive , [essence| |`&inner`| * |`&inner`| * |`&inner`| |] )
629 , ( BinRelAttr_Total , [essence| |`&inner`| * |`&inner`| |] )
630 , ( BinRelAttr_Connex , [essence| |`&inner`| * |`&inner`| |] )
631 , ( BinRelAttr_Euclidean , [essence| |`&inner`| * |`&inner`| * |`&inner`| |] )
632 , ( BinRelAttr_Serial , [essence| |`&inner`| |] )
633 , ( BinRelAttr_Equivalence , [essence| |`&inner`| * |`&inner`| * |`&inner`| |] )
634 , ( BinRelAttr_PartialOrder , [essence| |`&inner`| * |`&inner`| * |`&inner`| |] )
635 ]
636 , let grp = show attr
637 , softness <- [Nothing, Just 2, Just 4, Just 8, Just 16, Just 32]
638 ]
639 _ -> noStreamliner
640
641
642 ------------------------------------------------------------------------------
643 -- Functions and Sequences
644 ------------------------------------------------------------------------------
645
646
647 monotonicallyIncreasing ::
648 MonadFailDoc m =>
649 NameGen m =>
650 (?typeCheckerMode :: TypeCheckerMode) =>
651 StreamlinerGen m
652 monotonicallyIncreasing x = do
653 -- traceM $ show $ "Monotonically Increasing [1]" <+> pretty x
654 dom <- expandDomainReference <$> domainOf x
655 -- traceM $ show $ "Monotonically Increasing [2]" <+> pretty dom
656 let
657 applicable = case dom of
658 DomainFunction _ _ DomainInt{} DomainInt{} -> True
659 DomainSequence _ _ DomainInt{} -> True
660 _ -> False
661 if applicable
662 then do
663 (iPat, i) <- quantifiedVar
664 (jPat, j) <- quantifiedVar
665 mkStreamliner "FuncIncreaseDecrease" [essence|
666 forAll &iPat in defined(&x) .
667 forAll &jPat in defined(&x) .
668 &i < &j -> &x(&i) <= &x(&j)
669 |]
670 else noStreamliner
671
672
673 monotonicallyDecreasing ::
674 MonadFailDoc m =>
675 NameGen m =>
676 (?typeCheckerMode :: TypeCheckerMode) =>
677 StreamlinerGen m
678 monotonicallyDecreasing x = do
679 dom <- expandDomainReference <$> domainOf x
680 let
681 applicable = case dom of
682 DomainFunction _ _ DomainInt{} DomainInt{} -> True
683 DomainSequence _ _ DomainInt{} -> True
684 _ -> False
685 if applicable
686 then do
687 -- traceM $ show $ "Monotonically Decreasing"
688 (iPat, i) <- quantifiedVar
689 (jPat, j) <- quantifiedVar
690 mkStreamliner "FuncIncreaseDecrease" [essence|
691 forAll &iPat in defined(&x) .
692 forAll &jPat in defined(&x) .
693 &i < &j -> &x(&i) >= &x(&j)
694 |]
695 else noStreamliner
696
697
698 smallestFirst ::
699 MonadFailDoc m =>
700 NameGen m =>
701 (?typeCheckerMode :: TypeCheckerMode) =>
702 StreamlinerGen m
703 smallestFirst x = do
704 dom <- expandDomainReference <$> domainOf x
705 let
706 applicable = case dom of
707 DomainFunction _ _ DomainInt{} DomainInt{} -> True
708 DomainSequence _ _ DomainInt{} -> True
709 _ -> False
710 if applicable
711 then do
712 -- traceM $ show $ "Smallest First"
713 (ipat, i) <- quantifiedVar
714 mkStreamliner "FuncIncreaseDecrease" [essence|
715 forAll &ipat in defined(&x) .
716 &x(min(defined(&x))) <= &x(&i)
717 |]
718 else noStreamliner
719
720
721 largestFirst ::
722 MonadFailDoc m =>
723 NameGen m =>
724 (?typeCheckerMode :: TypeCheckerMode) =>
725 StreamlinerGen m
726 largestFirst x = do
727 dom <- expandDomainReference <$> domainOf x
728 let
729 applicable = case dom of
730 DomainFunction _ _ DomainInt{} DomainInt{} -> True
731 DomainSequence _ _ DomainInt{} -> True
732 _ -> False
733 if applicable
734 then do
735 -- traceM $ show $ "Largest First"
736 (ipat, i) <- quantifiedVar
737 mkStreamliner "FuncIncreaseDecrease" [essence|
738 forAll &ipat in defined(&x) .
739 &x(max(defined(&x))) >= &x(&i)
740 |]
741 else noStreamliner
742
743
744 commutative ::
745 MonadFailDoc m =>
746 NameGen m =>
747 (?typeCheckerMode :: TypeCheckerMode) =>
748 StreamlinerGen m
749 commutative x = do
750 dom <- expandDomainReference <$> domainOf x
751 case dom of
752 DomainFunction () _ (DomainTuple [a, b]) c -> do
753 if (a==b) && (b==c)
754 then do
755 (ipat, i) <- quantifiedVar
756 (jpat, j) <- quantifiedVar
757 mkStreamliner "FuncCommutative" [essence|
758 forAll (&ipat,&jpat) in defined(&x) .
759 &x((&i,&j)) = &x((&j,&i))
760 |]
761 else noStreamliner
762 _ -> noStreamliner
763
764
765 nonCommutative ::
766 MonadFailDoc m =>
767 NameGen m =>
768 (?typeCheckerMode :: TypeCheckerMode) =>
769 StreamlinerGen m
770 nonCommutative x = do
771 dom <- expandDomainReference <$> domainOf x
772 case dom of
773 DomainFunction () _ (DomainTuple [a, b]) c -> do
774 if (a==b) && (b==c)
775 then do
776 (ipat, i) <- quantifiedVar
777 (jpat, j) <- quantifiedVar
778 mkStreamliner "FuncCommutative" [essence|
779 forAll (&ipat,&jpat) in defined(&x) .
780 &x((&i,&j)) != &x((&j,&i))
781 |]
782 else noStreamliner
783 _ -> noStreamliner
784
785
786 associative ::
787 MonadFailDoc m =>
788 NameGen m =>
789 (?typeCheckerMode :: TypeCheckerMode) =>
790 StreamlinerGen m
791 associative x = do
792 dom <- expandDomainReference <$> domainOf x
793 case dom of
794 DomainFunction () _ (DomainTuple [a, b]) c -> do
795 if (a==b) && (b==c)
796 then do
797 (ipat, i) <- quantifiedVar
798 (jpat, j) <- quantifiedVar
799 (kpat, k) <- quantifiedVar
800 mkStreamliner "FuncAssociative" [essence|
801 forAll &ipat, &jpat, &kpat in defined(&x) .
802 &x((&x((&i,&j)), &k)) = &x((&i, &x((&j, &k))))
803 |]
804 else noStreamliner
805 _ -> noStreamliner
806
807
808
809 onTuple ::
810 MonadFailDoc m =>
811 NameGen m =>
812 (?typeCheckerMode :: TypeCheckerMode) =>
813 Integer -> StreamlinerGen m -> StreamlinerGen m
814 onTuple n innerStreamliner x = do
815 dom <- expandDomainReference <$> domainOf x
816 case dom of
817 DomainTuple ds | n >= 1 && n <= genericLength ds -> do
818 nm <- nextName "q"
819 let ref = Reference nm (Just (DeclNoRepr Find nm (ds `genericIndex` (n-1)) NoRegion))
820 innerConstraints <- innerStreamliner ref
821
822 let
823 nE = fromInt n
824 replaceRef (Reference nm2 _) | nm2 == nm = [essence| &x[&nE] |]
825 replaceRef p = p
826
827 return [ (transform replaceRef cons, grps)
828 | (cons, grps) <- innerConstraints
829 ]
830
831 _ -> noStreamliner
832
833
834 onRange ::
835 MonadFailDoc m =>
836 NameGen m =>
837 (?typeCheckerMode :: TypeCheckerMode) =>
838 StreamlinerGen m -> StreamlinerGen m
839 onRange innerStreamliner x = do
840 -- traceM $ show $ "onRange" <+> pretty x
841 dom <- expandDomainReference <$> domainOf x
842 -- traceM $ show $ "onRange dom" <+> pretty dom
843 let
844 minnerDomTo = case dom of
845 DomainFunction _ _ DomainInt{} innerDomTo -> return innerDomTo
846 DomainSequence _ _ innerDomTo -> return innerDomTo
847 _ -> Nothing
848 case minnerDomTo of
849 Just innerDomTo -> do
850
851 let rangeSetDomain = DomainSet () def innerDomTo
852
853 nm <- nextName "q"
854 let ref = Reference nm (Just (DeclNoRepr Find nm rangeSetDomain NoRegion))
855 innerConstraints <- innerStreamliner ref
856
857 let
858 replaceWithRangeOfX (Reference n _) | n == nm = [essence| range(&x) |]
859 replaceWithRangeOfX p = p
860
861 -- traceM $ show $ "innerConstraints 1" <+> vcat (map pretty innerConstraints)
862 -- traceM $ show $ "innerConstraints 2" <+> vcat (map pretty (transformBi replaceWithRangeOfX innerConstraints))
863
864 return [ (transform replaceWithRangeOfX cons, grps)
865 | (cons, grps) <- innerConstraints
866 ]
867
868 _ -> noStreamliner
869
870
871 onDefined ::
872 MonadFailDoc m =>
873 NameGen m =>
874 (?typeCheckerMode :: TypeCheckerMode) =>
875 StreamlinerGen m -> StreamlinerGen m
876 onDefined innerStreamliner x = do
877 -- traceM $ show $ "Defined" <+> pretty x
878 dom <- expandDomainReference <$> domainOf x
879 -- traceM $ show $ "Defined dom" <+> pretty dom
880 -- So we get the range and then we apply and then apply the rule to the range of the function
881 let
882 minnerDomFr = case dom of
883 DomainFunction _ _ innerDomFr _ -> return innerDomFr
884 _ -> Nothing
885
886 case minnerDomFr of
887 Just innerDomFr -> do
888
889 let rangeSetDomain = DomainSet () def innerDomFr
890
891 nm <- nextName "q"
892 let ref = Reference nm (Just (DeclNoRepr Find nm rangeSetDomain NoRegion))
893 innerConstraints <- innerStreamliner ref
894
895 let
896 replaceWithRangeOfX (Reference n _) | n == nm = [essence| defined(&x) |]
897 replaceWithRangeOfX p = p
898
899 -- traceM $ show $ "innerConstraints 1" <+> vcat (map pretty innerConstraints)
900 -- traceM $ show $ "innerConstraints 2" <+> vcat (map pretty (transformBi replaceWithRangeOfX innerConstraints))
901
902 return [ (transform replaceWithRangeOfX cons, grps)
903 | (cons, grps) <- innerConstraints
904 ]
905
906 _ -> noStreamliner
907
908
909 -- diagonal :: (MonadFailDoc m, NameGen m) => StreamlinerGen m -> StreamlinerGen m
910 -- diagonal innerStreamliner x = do
911 -- traceM $ show $ "diagnoal" <+> pretty x
912 -- dom <- expandDomainReference <$> domainOf x
913 -- case dom of
914 -- DomainFunction () _ (DomainTuple [a, b]) domto-> do
915 -- case (a == b) of
916 -- True -> do
917 -- nm <- nextname "fx"
918 -- let auxfunction = domainfunction () def a domto
919 -- ref = reference nm (just (declnorepr find nm auxfunction noregion))
920
921 -- i <- nextname "q"
922 -- (ipat, i) <- quantifiedvar
923
924 -- innerconstraints <- innerstreamliner ref
925 -- return $ attachGroup grps [essence| find &ref: function &a --> &domto such that forall &ipat: &a. (&i, &i) in defined(&x) -> &ref(&i) = &x((&i,&i)),
926 -- forall &ipat: &a . &i in defined(&ref) -> &ref(&i) = &x((&i,&i)) |]
927 -- False -> do
928 -- noStreamliner
929 -- _ -> noStreamliner
930
931 --
932 -- prefix :: (MonadFailDoc m, NameGen m) => StreamlinerGen m -> StreamlinerGen m
933 -- prefix innerStreamliner x = do
934 -- traceM $ show $ "prefix"
935 -- dom <- expandDomainReference <$> domainOf x
936 -- case dom of
937 -- DomainFunction () _ (DomainInt [RangeBounded lb up]) innerDomTo -> do
938 -- case x of
939 -- Reference nm (Just (DeclNoRepr Find _ domain NoRegion)) -> do
940
941 -- innerConstraints <- innerStreamliner x
942
943 -- let
944 -- replaceWithRangeOfX (Reference n _) | n == nm = [essence| restrict(&x,`int(&lb..(&up-1))`) |]
945 -- replaceWithRangeOfX p = p
946
947 -- -- traceM $ show $ "innerConstraints 1" <+> vcat (map pretty innerConstraints)
948 -- -- traceM $ show $ "innerConstraints 2" <+> vcat (map pretty (transformBi replaceWithRangeOfX innerConstraints))
949
950 -- return (transformBi replaceWithRangeOfX innerConstraints)
951 -- _ -> noStreamliner
952
953 -- _ -> noStreamliner
954 --
955
956 -- postfix :: (MonadFailDoc m, NameGen m) => StreamlinerGen m -> StreamlinerGen m
957 -- postfix innerStreamliner x = do
958 -- traceM $ show $ "postfix"
959 -- dom <- expandDomainReference <$> domainOf x
960 -- case dom of
961 -- DomainFunction () _ (DomainInt [RangeBounded lb up]) innerDomTo -> do
962 -- case x of
963 -- Reference nm (Just (DeclNoRepr Find _ domain NoRegion)) -> do
964
965 -- innerConstraints <- innerStreamliner x
966
967 -- let
968 -- replaceWithRangeOfX (Reference n _) | n == nm = [essence| restrict(&x,`int((&lb+1)..&up)`) |]
969 -- replaceWithRangeOfX p = p
970
971 -- -- traceM $ show $ "innerConstraints 1" <+> vcat (map pretty innerConstraints)
972 -- -- traceM $ show $ "innerConstraints 2" <+> vcat (map pretty (transformBi replaceWithRangeOfX innerConstraints))
973
974 -- return (transformBi replaceWithRangeOfX innerConstraints)
975 -- _ -> noStreamliner
976
977 -- _ -> noStreamliner
978
979
980 ------------------------------------------------------------------------------
981 -- Partitions
982 ------------------------------------------------------------------------------
983
984
985 parts ::
986 MonadFailDoc m =>
987 NameGen m =>
988 (?typeCheckerMode :: TypeCheckerMode) =>
989 StreamlinerGen m -> StreamlinerGen m
990 parts innerStreamliner x = do
991 dom <- expandDomainReference <$> domainOf x
992 case dom of
993 DomainPartition _ _ partitionDomain -> do
994 -- traceM $ show $ "partition"
995 nm <- nextName "q"
996 let setDomain = DomainSet () def (DomainSet () def partitionDomain)
997 ref = Reference nm (Just (DeclNoRepr Find nm setDomain NoRegion))
998
999 innerConstraints <- innerStreamliner ref
1000
1001 let
1002 replaceWithRangeOfX (Reference n _) | n == nm = [essence| parts(&x) |]
1003 replaceWithRangeOfX p = p
1004
1005 return [ (transform replaceWithRangeOfX cons, grps)
1006 | (cons, grps) <- innerConstraints
1007 ]
1008
1009 _ -> noStreamliner
1010
1011
1012 quasiRegular ::
1013 MonadFailDoc m =>
1014 NameGen m =>
1015 (?typeCheckerMode :: TypeCheckerMode) =>
1016 StreamlinerGen m
1017 quasiRegular x = do
1018 dom <- expandDomainReference <$> domainOf x
1019 case dom of
1020 DomainPartition{} -> do
1021 mkStreamliner "PartitionRegular" [essence|
1022 minPartSize(&x, |participants(&x)| / |parts(&x)| - 1) /\
1023 maxPartSize(&x, |participants(&x)|/ |parts(&x)| + 1)
1024 |]
1025 _ -> noStreamliner