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 DomainFunction _ _ (DomainInt _ [RangeBounded lb ub]) innerDom -> do
385 let size = [essence| &ub - &lb + 1 |]
386 let bucketSize = [essence| &size / 10 |]
387 nm <- nextName "q"
388 let pat = Single nm
389 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
390
391 liftMatrix (Reference n _) | n == nm = [essence| &x(&ref) |]
392 liftMatrix p = p
393
394 innerConstraints <- transformBi liftMatrix <$> innerStreamliner ref
395 concatForM [0..9] $ \ (bucketInt :: Integer) -> let bucket = fromInt bucketInt in
396 forM innerConstraints $ \ (innerConstraint, grps) ->
397 attachGroup (("FunctionByBucket-" ++ show bucketInt) : grps) [essence|
398 forAll &pat : int(&lb + &bucket * &bucketSize .. min([&ub, &lb + (&bucket+1) * &bucketSize])) . &innerConstraint
399 |]
400 _ -> noStreamliner
401
402
403
404 matrixByColBucket ::
405 MonadFailDoc m =>
406 NameGen m =>
407 (?typeCheckerMode :: TypeCheckerMode) =>
408 StreamlinerGen m -> StreamlinerGen m
409 matrixByColBucket innerStreamliner x = do
410 dom <- expandDomainReference <$> domainOf x
411 case dom of
412 DomainMatrix outerIndex (DomainMatrix (DomainInt _ [RangeBounded lb ub]) innerDom) -> do
413 let size = [essence| &ub - &lb + 1 |]
414 let bucketSize = [essence| &size / 10 |]
415
416 nmO <- nextName "q"
417 let patO = Single nmO
418 let refO = Reference nmO Nothing
419
420 nm <- nextName "q"
421 let pat = Single nm
422 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
423
424 liftMatrix (Reference n _) | n == nm = [essence| &x[&refO, &ref] |]
425 liftMatrix p = p
426
427 innerConstraints <- transformBi liftMatrix <$> innerStreamliner ref
428 concatForM [0..9] $ \ (bucketInt :: Integer) -> let bucket = fromInt bucketInt in
429 forM innerConstraints $ \ (innerConstraint, grps) ->
430 attachGroup (("MatrixByColBucket-" ++ show bucketInt) : grps) [essence|
431 forAll &patO : &outerIndex .
432 forAll &pat : int(&lb + &bucket * &bucketSize .. min([&ub, &lb + (&bucket+1) * &bucketSize])) .
433 &innerConstraint
434 |]
435 _ -> noStreamliner
436
437
438 ------------------------------------------------------------------------------
439 -- Sets and MSets
440 ------------------------------------------------------------------------------
441
442
443 setAll ::
444 MonadFailDoc m =>
445 NameGen m =>
446 (?typeCheckerMode :: TypeCheckerMode) =>
447 StreamlinerGen m -> StreamlinerGen m
448 setAll innerStreamliner x = do
449 dom <- expandDomainReference <$> domainOf x
450 let minnerDom =
451 case dom of
452 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
453 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
454 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
455 _ -> Nothing
456 case minnerDom of
457 Just (innerDom, newTag) -> do
458 nm <- nextName "q"
459 -- traceM $ show $ "setAll nm" <+> pretty nm
460 let pat = Single nm
461 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
462 innerConstraints <- innerStreamliner ref
463 -- traceM $ show $ "maybeInnerConstraint" <+> vcat (map pretty innerConstraints)
464 forM innerConstraints $ \ (innerConstraint, grps) ->
465 attachGroup (newTag: grps) [essence| forAll &pat in &x . &innerConstraint |]
466 _ -> noStreamliner
467
468
469 setAtMostOne ::
470 MonadFailDoc m =>
471 NameGen m =>
472 (?typeCheckerMode :: TypeCheckerMode) =>
473 StreamlinerGen m -> StreamlinerGen m
474 setAtMostOne innerStreamliner x = do
475 dom <- expandDomainReference <$> domainOf x
476 let minnerDom =
477 case dom of
478 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
479 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
480 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
481 _ -> Nothing
482 case minnerDom of
483 Just (innerDom, newTag) -> do
484 nm <- nextName "q"
485 let pat = Single nm
486 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
487 innerConstraints <- innerStreamliner ref
488 forM innerConstraints $ \ (innerConstraint, grps) ->
489 attachGroup (newTag: grps) [essence| 1 >= sum &pat in &x . toInt(&innerConstraint) |]
490 _ -> noStreamliner
491
492
493 setHalf ::
494 MonadFailDoc m =>
495 NameGen m =>
496 (?typeCheckerMode :: TypeCheckerMode) =>
497 StreamlinerGen m -> StreamlinerGen m
498 setHalf innerStreamliner x = do
499 dom <- expandDomainReference <$> domainOf x
500 let minnerDom =
501 case dom of
502 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
503 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
504 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
505 _ -> Nothing
506 case minnerDom of
507 Just (innerDom, newTag) -> do
508 let size = [essence| |&x| |]
509 nm <- nextName "q"
510 let pat = Single nm
511 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
512 innerConstraints <- innerStreamliner ref
513 forM innerConstraints $ \ (innerConstraint, grps) ->
514 attachGroup (newTag: grps) [essence| &size / 2 = (sum &pat in &x . toInt(&innerConstraint)) |]
515 _ -> noStreamliner
516
517
518 setApproxHalf ::
519 MonadFailDoc m =>
520 NameGen m =>
521 (?typeCheckerMode :: TypeCheckerMode) =>
522 StreamlinerGen m -> StreamlinerGen m
523 setApproxHalf innerStreamliner x = do
524 dom <- expandDomainReference <$> domainOf x
525 let minnerDom =
526 case dom of
527 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
528 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
529 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
530 _ -> Nothing
531 case minnerDom of
532 Just (innerDom, newTag) -> do
533 let size = [essence| |&x| |]
534 nm <- nextName "q"
535 let pat = Single nm
536 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
537 innerConstraints <- innerStreamliner ref
538 forM innerConstraints $ \ (innerConstraint, grps) ->
539 attachGroup (newTag: grps) [essence|
540 (&size/2) + 1 >= (sum &pat in &x . toInt(&innerConstraint)) /\
541 (&size/2 -1) <= (sum &pat in &x . toInt(&innerConstraint))
542 |]
543 _ -> noStreamliner
544
545
546 setMoreThanHalf ::
547 MonadFailDoc m =>
548 NameGen m =>
549 (?typeCheckerMode :: TypeCheckerMode) =>
550 StreamlinerGen m -> StreamlinerGen m
551 setMoreThanHalf innerStreamliner x = do
552 dom <- expandDomainReference <$> domainOf x
553 let minnerDom =
554 case dom of
555 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
556 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
557 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
558 _ -> Nothing
559 case minnerDom of
560 Just (innerDom, newTag) -> do
561 let size = [essence| |&x| |]
562 nm <- nextName "q"
563 let pat = Single nm
564 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
565 innerConstraints <- innerStreamliner ref
566 forM innerConstraints $ \ (innerConstraint, grps) ->
567 attachGroup (newTag: grps) [essence|
568 (&size/2) <= (sum &pat in &x . toInt(&innerConstraint))
569 |]
570 _ -> noStreamliner
571
572
573 setLessThanHalf ::
574 MonadFailDoc m =>
575 NameGen m =>
576 (?typeCheckerMode :: TypeCheckerMode) =>
577 StreamlinerGen m -> StreamlinerGen m
578 setLessThanHalf innerStreamliner x = do
579 dom <- expandDomainReference <$> domainOf x
580 let minnerDom =
581 case dom of
582 DomainSet _ _ innerDom -> Just (innerDom, "SetCardinality")
583 DomainMSet _ _ innerDom -> Just (innerDom, "MSetCardinality")
584 DomainRelation _ _ innerDoms -> Just (DomainTuple innerDoms, "RelationCardinality")
585 _ -> Nothing
586 case minnerDom of
587 Just (innerDom, newTag) -> do
588 let size = [essence| |&x| |]
589 nm <- nextName "q"
590 let pat = Single nm
591 ref = Reference nm (Just (DeclNoRepr Find nm innerDom NoRegion))
592 innerConstraints <- innerStreamliner ref
593 forM innerConstraints $ \ (innerConstraint, grps) ->
594 attachGroup (newTag: grps) [essence|
595 (&size/2) >= (sum &pat in &x . toInt(&innerConstraint))
596 |]
597 _ -> noStreamliner
598
599
600 relationCardinality ::
601 MonadFailDoc m =>
602 NameGen m =>
603 (?typeCheckerMode :: TypeCheckerMode) =>
604 StreamlinerGen m
605 relationCardinality x = do
606 dom <- expandDomainReference <$> domainOf x
607 case dom of
608 DomainRelation _ _ inners -> do
609 let maxCard = make opProduct $ fromList [ [essence| |`&i`| |] | i <- inners ]
610 sequence
611 [ case lowerOrUpper of
612 "lowerBound" -> return ([essence| |&x| >= &maxCard / &slice |], [grp])
613 "upperBound" -> return ([essence| |&x| <= &maxCard / &slice |], [grp])
614 _ -> bug "relationCardinality"
615 | slice <- [1,2,4,8,16,32]
616 , lowerOrUpper <- ["LowerBound","UpperBound"]
617 , let grp = "RelationCardinality-" ++ lowerOrUpper
618 ]
619 _ -> noStreamliner
620
621
622 binRelAttributes ::
623 MonadFailDoc m =>
624 NameGen m =>
625 (?typeCheckerMode :: TypeCheckerMode) =>
626 StreamlinerGen m
627 binRelAttributes x = do
628 dom <- expandDomainReference <$> domainOf x
629 case dom of
630 -- we don't insist on inner1 == inner2 any more
631 DomainRelation _ _ [inner1, inner2] -> sequence
632 [ do
633 out <- case softness of
634 Nothing -> mkBinRelCons (BinaryRelationAttrs (S.singleton attr)) inner x
635 Just s -> mkBinRelConsSoft maxNum s (BinaryRelationAttrs (S.singleton attr)) inner x
636 return (make opAnd (fromList out), [grp])
637 | inner <- [inner1, inner2]
638 , (attr, maxNum) <- [ ( BinRelAttr_Reflexive , [essence| |`&inner`| |] )
639 , ( BinRelAttr_Irreflexive , [essence| |`&inner`| |] )
640 , ( BinRelAttr_Coreflexive , [essence| |`&inner`| * |`&inner`| |] )
641 , ( BinRelAttr_Symmetric , [essence| |`&inner`| * |`&inner`| |] )
642 , ( BinRelAttr_AntiSymmetric , [essence| |`&inner`| * |`&inner`| |] )
643 , ( BinRelAttr_ASymmetric , [essence| |`&inner`| * |`&inner`| |] )
644 , ( BinRelAttr_Transitive , [essence| |`&inner`| * |`&inner`| * |`&inner`| |] )
645 , ( BinRelAttr_Total , [essence| |`&inner`| * |`&inner`| |] )
646 , ( BinRelAttr_Connex , [essence| |`&inner`| * |`&inner`| |] )
647 , ( BinRelAttr_Euclidean , [essence| |`&inner`| * |`&inner`| * |`&inner`| |] )
648 , ( BinRelAttr_Serial , [essence| |`&inner`| |] )
649 , ( BinRelAttr_Equivalence , [essence| |`&inner`| * |`&inner`| * |`&inner`| |] )
650 , ( BinRelAttr_PartialOrder , [essence| |`&inner`| * |`&inner`| * |`&inner`| |] )
651 ]
652 , let grp = show attr
653 , softness <- [Nothing, Just 2, Just 4, Just 8, Just 16, Just 32]
654 ]
655 _ -> noStreamliner
656
657
658 ------------------------------------------------------------------------------
659 -- Functions and Sequences
660 ------------------------------------------------------------------------------
661
662
663 monotonicallyIncreasing ::
664 MonadFailDoc m =>
665 NameGen m =>
666 (?typeCheckerMode :: TypeCheckerMode) =>
667 StreamlinerGen m
668 monotonicallyIncreasing x = do
669 -- traceM $ show $ "Monotonically Increasing [1]" <+> pretty x
670 dom <- expandDomainReference <$> domainOf x
671 -- traceM $ show $ "Monotonically Increasing [2]" <+> pretty dom
672 let
673 applicable = case dom of
674 DomainFunction _ _ DomainInt{} DomainInt{} -> True
675 DomainSequence _ _ DomainInt{} -> True
676 _ -> False
677 if applicable
678 then do
679 (iPat, i) <- quantifiedVar
680 (jPat, j) <- quantifiedVar
681 mkStreamliner "FuncIncreaseDecrease" [essence|
682 forAll &iPat in defined(&x) .
683 forAll &jPat in defined(&x) .
684 &i < &j -> &x(&i) <= &x(&j)
685 |]
686 else noStreamliner
687
688
689 monotonicallyDecreasing ::
690 MonadFailDoc m =>
691 NameGen m =>
692 (?typeCheckerMode :: TypeCheckerMode) =>
693 StreamlinerGen m
694 monotonicallyDecreasing x = do
695 dom <- expandDomainReference <$> domainOf x
696 let
697 applicable = case dom of
698 DomainFunction _ _ DomainInt{} DomainInt{} -> True
699 DomainSequence _ _ DomainInt{} -> True
700 _ -> False
701 if applicable
702 then do
703 -- traceM $ show $ "Monotonically Decreasing"
704 (iPat, i) <- quantifiedVar
705 (jPat, j) <- quantifiedVar
706 mkStreamliner "FuncIncreaseDecrease" [essence|
707 forAll &iPat in defined(&x) .
708 forAll &jPat in defined(&x) .
709 &i < &j -> &x(&i) >= &x(&j)
710 |]
711 else noStreamliner
712
713
714 smallestFirst ::
715 MonadFailDoc m =>
716 NameGen m =>
717 (?typeCheckerMode :: TypeCheckerMode) =>
718 StreamlinerGen m
719 smallestFirst x = do
720 dom <- expandDomainReference <$> domainOf x
721 let
722 applicable = case dom of
723 DomainFunction _ _ DomainInt{} DomainInt{} -> True
724 DomainSequence _ _ DomainInt{} -> True
725 _ -> False
726 if applicable
727 then do
728 -- traceM $ show $ "Smallest First"
729 (ipat, i) <- quantifiedVar
730 mkStreamliner "FuncIncreaseDecrease" [essence|
731 forAll &ipat in defined(&x) .
732 &x(min(defined(&x))) <= &x(&i)
733 |]
734 else noStreamliner
735
736
737 largestFirst ::
738 MonadFailDoc m =>
739 NameGen m =>
740 (?typeCheckerMode :: TypeCheckerMode) =>
741 StreamlinerGen m
742 largestFirst x = do
743 dom <- expandDomainReference <$> domainOf x
744 let
745 applicable = case dom of
746 DomainFunction _ _ DomainInt{} DomainInt{} -> True
747 DomainSequence _ _ DomainInt{} -> True
748 _ -> False
749 if applicable
750 then do
751 -- traceM $ show $ "Largest First"
752 (ipat, i) <- quantifiedVar
753 mkStreamliner "FuncIncreaseDecrease" [essence|
754 forAll &ipat in defined(&x) .
755 &x(max(defined(&x))) >= &x(&i)
756 |]
757 else noStreamliner
758
759
760 commutative ::
761 MonadFailDoc m =>
762 NameGen m =>
763 (?typeCheckerMode :: TypeCheckerMode) =>
764 StreamlinerGen m
765 commutative x = do
766 dom <- expandDomainReference <$> domainOf x
767 case dom of
768 DomainFunction () _ (DomainTuple [a, b]) c -> do
769 if (a==b) && (b==c)
770 then do
771 (ipat, i) <- quantifiedVar
772 (jpat, j) <- quantifiedVar
773 mkStreamliner "FuncCommutative" [essence|
774 forAll (&ipat,&jpat) in defined(&x) .
775 &x((&i,&j)) = &x((&j,&i))
776 |]
777 else noStreamliner
778 _ -> noStreamliner
779
780
781 nonCommutative ::
782 MonadFailDoc m =>
783 NameGen m =>
784 (?typeCheckerMode :: TypeCheckerMode) =>
785 StreamlinerGen m
786 nonCommutative x = do
787 dom <- expandDomainReference <$> domainOf x
788 case dom of
789 DomainFunction () _ (DomainTuple [a, b]) c -> do
790 if (a==b) && (b==c)
791 then do
792 (ipat, i) <- quantifiedVar
793 (jpat, j) <- quantifiedVar
794 mkStreamliner "FuncCommutative" [essence|
795 forAll (&ipat,&jpat) in defined(&x) .
796 &x((&i,&j)) != &x((&j,&i))
797 |]
798 else noStreamliner
799 _ -> noStreamliner
800
801
802 associative ::
803 MonadFailDoc m =>
804 NameGen m =>
805 (?typeCheckerMode :: TypeCheckerMode) =>
806 StreamlinerGen m
807 associative x = do
808 dom <- expandDomainReference <$> domainOf x
809 case dom of
810 DomainFunction () _ (DomainTuple [a, b]) c -> do
811 if (a==b) && (b==c)
812 then do
813 (ipat, i) <- quantifiedVar
814 (jpat, j) <- quantifiedVar
815 (kpat, k) <- quantifiedVar
816 mkStreamliner "FuncAssociative" [essence|
817 forAll &ipat, &jpat, &kpat in defined(&x) .
818 &x((&x((&i,&j)), &k)) = &x((&i, &x((&j, &k))))
819 |]
820 else noStreamliner
821 _ -> noStreamliner
822
823
824
825 onTuple ::
826 MonadFailDoc m =>
827 NameGen m =>
828 (?typeCheckerMode :: TypeCheckerMode) =>
829 Integer -> StreamlinerGen m -> StreamlinerGen m
830 onTuple n innerStreamliner x = do
831 dom <- expandDomainReference <$> domainOf x
832 case dom of
833 DomainTuple ds | n >= 1 && n <= genericLength ds -> do
834 nm <- nextName "q"
835 let ref = Reference nm (Just (DeclNoRepr Find nm (ds `genericIndex` (n-1)) NoRegion))
836 innerConstraints <- innerStreamliner ref
837
838 let
839 nE = fromInt n
840 replaceRef (Reference nm2 _) | nm2 == nm = [essence| &x[&nE] |]
841 replaceRef p = p
842
843 return [ (transform replaceRef cons, grps)
844 | (cons, grps) <- innerConstraints
845 ]
846
847 _ -> noStreamliner
848
849
850 onRange ::
851 MonadFailDoc m =>
852 NameGen m =>
853 (?typeCheckerMode :: TypeCheckerMode) =>
854 StreamlinerGen m -> StreamlinerGen m
855 onRange innerStreamliner x = do
856 -- traceM $ show $ "onRange" <+> pretty x
857 dom <- expandDomainReference <$> domainOf x
858 -- traceM $ show $ "onRange dom" <+> pretty dom
859 let
860 minnerDomTo = case dom of
861 DomainFunction _ _ DomainInt{} innerDomTo -> return innerDomTo
862 DomainSequence _ _ innerDomTo -> return innerDomTo
863 _ -> Nothing
864 case minnerDomTo of
865 Just innerDomTo -> do
866
867 let rangeSetDomain = DomainSet () def innerDomTo
868
869 nm <- nextName "q"
870 let ref = Reference nm (Just (DeclNoRepr Find nm rangeSetDomain NoRegion))
871 innerConstraints <- innerStreamliner ref
872
873 let
874 replaceWithRangeOfX (Reference n _) | n == nm = [essence| range(&x) |]
875 replaceWithRangeOfX p = p
876
877 -- traceM $ show $ "innerConstraints 1" <+> vcat (map pretty innerConstraints)
878 -- traceM $ show $ "innerConstraints 2" <+> vcat (map pretty (transformBi replaceWithRangeOfX innerConstraints))
879
880 return [ (transform replaceWithRangeOfX cons, grps)
881 | (cons, grps) <- innerConstraints
882 ]
883
884 _ -> noStreamliner
885
886
887 onDefined ::
888 MonadFailDoc m =>
889 NameGen m =>
890 (?typeCheckerMode :: TypeCheckerMode) =>
891 StreamlinerGen m -> StreamlinerGen m
892 onDefined innerStreamliner x = do
893 -- traceM $ show $ "Defined" <+> pretty x
894 dom <- expandDomainReference <$> domainOf x
895 -- traceM $ show $ "Defined dom" <+> pretty dom
896 -- So we get the range and then we apply and then apply the rule to the range of the function
897 let
898 minnerDomFr = case dom of
899 DomainFunction _ _ innerDomFr _ -> return innerDomFr
900 _ -> Nothing
901
902 case minnerDomFr of
903 Just innerDomFr -> do
904
905 let rangeSetDomain = DomainSet () def innerDomFr
906
907 nm <- nextName "q"
908 let ref = Reference nm (Just (DeclNoRepr Find nm rangeSetDomain NoRegion))
909 innerConstraints <- innerStreamliner ref
910
911 let
912 replaceWithRangeOfX (Reference n _) | n == nm = [essence| defined(&x) |]
913 replaceWithRangeOfX p = p
914
915 -- traceM $ show $ "innerConstraints 1" <+> vcat (map pretty innerConstraints)
916 -- traceM $ show $ "innerConstraints 2" <+> vcat (map pretty (transformBi replaceWithRangeOfX innerConstraints))
917
918 return [ (transform replaceWithRangeOfX cons, grps)
919 | (cons, grps) <- innerConstraints
920 ]
921
922 _ -> noStreamliner
923
924
925 -- diagonal :: (MonadFailDoc m, NameGen m) => StreamlinerGen m -> StreamlinerGen m
926 -- diagonal innerStreamliner x = do
927 -- traceM $ show $ "diagnoal" <+> pretty x
928 -- dom <- expandDomainReference <$> domainOf x
929 -- case dom of
930 -- DomainFunction () _ (DomainTuple [a, b]) domto-> do
931 -- case (a == b) of
932 -- True -> do
933 -- nm <- nextname "fx"
934 -- let auxfunction = domainfunction () def a domto
935 -- ref = reference nm (just (declnorepr find nm auxfunction noregion))
936
937 -- i <- nextname "q"
938 -- (ipat, i) <- quantifiedvar
939
940 -- innerconstraints <- innerstreamliner ref
941 -- return $ attachGroup grps [essence| find &ref: function &a --> &domto such that forall &ipat: &a. (&i, &i) in defined(&x) -> &ref(&i) = &x((&i,&i)),
942 -- forall &ipat: &a . &i in defined(&ref) -> &ref(&i) = &x((&i,&i)) |]
943 -- False -> do
944 -- noStreamliner
945 -- _ -> noStreamliner
946
947 --
948 -- prefix :: (MonadFailDoc m, NameGen m) => StreamlinerGen m -> StreamlinerGen m
949 -- prefix innerStreamliner x = do
950 -- traceM $ show $ "prefix"
951 -- dom <- expandDomainReference <$> domainOf x
952 -- case dom of
953 -- DomainFunction () _ (DomainInt [RangeBounded lb up]) innerDomTo -> do
954 -- case x of
955 -- Reference nm (Just (DeclNoRepr Find _ domain NoRegion)) -> do
956
957 -- innerConstraints <- innerStreamliner x
958
959 -- let
960 -- replaceWithRangeOfX (Reference n _) | n == nm = [essence| restrict(&x,`int(&lb..(&up-1))`) |]
961 -- replaceWithRangeOfX p = p
962
963 -- -- traceM $ show $ "innerConstraints 1" <+> vcat (map pretty innerConstraints)
964 -- -- traceM $ show $ "innerConstraints 2" <+> vcat (map pretty (transformBi replaceWithRangeOfX innerConstraints))
965
966 -- return (transformBi replaceWithRangeOfX innerConstraints)
967 -- _ -> noStreamliner
968
969 -- _ -> noStreamliner
970 --
971
972 -- postfix :: (MonadFailDoc m, NameGen m) => StreamlinerGen m -> StreamlinerGen m
973 -- postfix innerStreamliner x = do
974 -- traceM $ show $ "postfix"
975 -- dom <- expandDomainReference <$> domainOf x
976 -- case dom of
977 -- DomainFunction () _ (DomainInt [RangeBounded lb up]) innerDomTo -> do
978 -- case x of
979 -- Reference nm (Just (DeclNoRepr Find _ domain NoRegion)) -> do
980
981 -- innerConstraints <- innerStreamliner x
982
983 -- let
984 -- replaceWithRangeOfX (Reference n _) | n == nm = [essence| restrict(&x,`int((&lb+1)..&up)`) |]
985 -- replaceWithRangeOfX p = p
986
987 -- -- traceM $ show $ "innerConstraints 1" <+> vcat (map pretty innerConstraints)
988 -- -- traceM $ show $ "innerConstraints 2" <+> vcat (map pretty (transformBi replaceWithRangeOfX innerConstraints))
989
990 -- return (transformBi replaceWithRangeOfX innerConstraints)
991 -- _ -> noStreamliner
992
993 -- _ -> noStreamliner
994
995
996 ------------------------------------------------------------------------------
997 -- Partitions
998 ------------------------------------------------------------------------------
999
1000
1001 parts ::
1002 MonadFailDoc m =>
1003 NameGen m =>
1004 (?typeCheckerMode :: TypeCheckerMode) =>
1005 StreamlinerGen m -> StreamlinerGen m
1006 parts innerStreamliner x = do
1007 dom <- expandDomainReference <$> domainOf x
1008 case dom of
1009 DomainPartition _ _ partitionDomain -> do
1010 -- traceM $ show $ "partition"
1011 nm <- nextName "q"
1012 let setDomain = DomainSet () def (DomainSet () def partitionDomain)
1013 ref = Reference nm (Just (DeclNoRepr Find nm setDomain NoRegion))
1014
1015 innerConstraints <- innerStreamliner ref
1016
1017 let
1018 replaceWithRangeOfX (Reference n _) | n == nm = [essence| parts(&x) |]
1019 replaceWithRangeOfX p = p
1020
1021 return [ (transform replaceWithRangeOfX cons, grps)
1022 | (cons, grps) <- innerConstraints
1023 ]
1024
1025 _ -> noStreamliner
1026
1027
1028 quasiRegular ::
1029 MonadFailDoc m =>
1030 NameGen m =>
1031 (?typeCheckerMode :: TypeCheckerMode) =>
1032 StreamlinerGen m
1033 quasiRegular x = do
1034 dom <- expandDomainReference <$> domainOf x
1035 case dom of
1036 DomainPartition{} -> do
1037 mkStreamliner "PartitionRegular" [essence|
1038 minPartSize(&x, |participants(&x)| / |parts(&x)| - 1) /\
1039 maxPartSize(&x, |participants(&x)|/ |parts(&x)| + 1)
1040 |]
1041 _ -> noStreamliner