never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.UI.ParameterGenerator ( parameterGenerator ) where
4
5 import Conjure.Prelude
6 import Conjure.Bug
7 import Conjure.Language
8 import Conjure.Language.CategoryOf ( categoryOf, Category(..) )
9 import Conjure.Language.NameResolution ( resolveNames )
10 import Conjure.Language.Instantiate ( trySimplify )
11 import Conjure.Process.Enumerate ( EnumerateDomain )
12 import Conjure.Language.Expression.DomainSizeOf ( domainSizeOf )
13
14 -- text
15 import Data.Text ( pack )
16
17
18 -- | This doesn't do anything to do with correcting categories at the moment, it should.
19 -- An example:
20 -- given n : int(1..10)
21 -- given s : set (size n) of int(1..10)
22 -- Should output:
23 -- find n : int(1..10)
24 -- find s : set (minSize 1, maxSize 10) of int(1..10)
25 -- such that n = |s|
26 -- (Just dropping wrong category stuff from attribute list isn't acceptable, because mset.)
27 parameterGenerator ::
28 MonadLog m =>
29 MonadFailDoc m =>
30 MonadUserError m =>
31 EnumerateDomain m =>
32 NameGen m =>
33 (?typeCheckerMode :: TypeCheckerMode) =>
34 Integer -> -- MININT
35 Integer -> -- MAXINT
36 Model -> m ( ( Model -- generator model
37 , Model ) -- repair model
38 , [(Name, String)] -- classification for each given
39 )
40 parameterGenerator minIntValue maxIntValue model =
41 runStateAsWriterT $ runNameGen () (resolveNames model) >>= core >>= evaluateBounds2
42 where
43 core m = do
44 out <- forM (mStatements m) $ \ st -> case st of
45 Declaration (FindOrGiven Given nm dom) -> do
46 (dom', genDecls, genCons, repairCons) <- pgOnDomain (Reference nm Nothing) nm dom
47 let repairDecls = [ Declaration (FindOrGiven Find ("repaired_" `mappend` genDeclNm) genDeclDom)
48 | Declaration (FindOrGiven Given genDeclNm genDeclDom) <- genDecls
49 ]
50 let repairObjectiveParts =
51 [ [essence| |&b-&a| |]
52 | Declaration (FindOrGiven Given genDeclNm _) <- genDecls
53 , let a = Reference genDeclNm Nothing
54 , let b = Reference ("repaired_" `mappend` genDeclNm) Nothing
55 ]
56 let prependRepair (Reference n _) = Reference ("repaired_" `mappend` n) Nothing
57 prependRepair x = x
58 return ( genDecls
59 ++ [ Declaration (FindOrGiven Find nm dom') ]
60 ++ [ SuchThat genCons | not (null genCons) ]
61 , genDecls
62 ++ repairDecls
63 ++ [SuchThat (map (transform prependRepair) repairCons) | not (null repairCons)]
64 , repairObjectiveParts
65 )
66 Declaration (FindOrGiven Find _ _ ) -> return ([], [], [])
67 Declaration (Letting _ _) -> return ([st], [], [])
68 Declaration {} -> return ([st], [], [])
69 SearchOrder {} -> return ([], [], [])
70 SearchHeuristic {} -> return ([], [], [])
71 Where xs -> do
72 xs' <- mapM (transformM fixQuantified) xs
73 return ([SuchThat xs'], [], [])
74 Objective {} -> return ([], [], [])
75 SuchThat {} -> return ([], [], [])
76
77 let (generatorStmts, repairStmts, repairObjectiveParts) = mconcat out
78
79 return ( m { mStatements = generatorStmts }
80 , m { mStatements = repairStmts
81 ++ [Objective Minimising (make opSum (fromList repairObjectiveParts))] }
82 )
83
84 evaluateBounds2 (m1, m2) = do
85 m1' <- evaluateBounds m1
86 m2' <- evaluateBounds m2
87 return (inlineLettings m1', inlineLettings m2')
88
89 evaluateBounds m = do
90 let symbols = [("MININT", fromInt minIntValue), ("MAXINT", fromInt maxIntValue)]
91 let eval = transformBiM (trySimplify symbols)
92 stmtsEvaluated <- mapM eval (mStatements m)
93 return m { mStatements = stmtsEvaluated }
94
95
96 inlineLettings :: Model -> Model
97 inlineLettings model =
98 let
99 inline p@(Reference nm _) = do
100 x <- gets (lookup nm)
101 return (fromMaybe p x)
102 inline p = return p
103
104 statements = catMaybes
105 $ flip evalState []
106 $ forM (mStatements model)
107 $ \ st ->
108 case st of
109 Declaration (Letting nm x) -> modify ((nm,x) :) >> return Nothing
110 _ -> Just <$> transformBiM inline st
111 in
112 model { mStatements = statements }
113
114
115 fixQuantified ::
116 MonadUserError m =>
117 NameGen m =>
118 Expression ->
119 m Expression
120 fixQuantified (Comprehension body gocs) = do
121 gocs' <- forM gocs $ \ goc -> case goc of
122 Generator (GenDomainNoRepr (Single pat) domain) -> do
123 let go x d =
124 case d of
125 DomainInt t ranges -> do
126 boundsAndCons <- forM ranges $ \ range ->
127 case range of
128 RangeSingle s -> do
129 (fr', frCons) <-
130 if categoryOf s < CatParameter
131 then return (s, [])
132 else do
133 bound <- lowerBoundOfIntExpr s
134 return (bound, return [essence| &x = &s |])
135 (to', _) <-
136 if categoryOf s < CatParameter
137 then return (s, [])
138 else do
139 bound <- upperBoundOfIntExpr s
140 return (bound, [])
141 return ([fr'], [to'], frCons)
142 RangeBounded fr to -> do
143 (fr', frCons) <-
144 if categoryOf fr < CatParameter
145 then return (fr, [])
146 else do
147 bound <- lowerBoundOfIntExpr fr
148 return (bound, return [essence| &x >= &fr |])
149 (to', toCons) <-
150 if categoryOf to < CatParameter
151 then return (to, [])
152 else do
153 bound <- upperBoundOfIntExpr to
154 return (bound, return [essence| &x <= &to |])
155 return ([fr'], [to'], frCons ++ toCons)
156 _ -> userErr1 $ vcat [ "Open ranges are not supported:" <+> pretty range
157 , "In domain:" <+> pretty d
158 ]
159 let (froms, tos, cons) = mconcat boundsAndCons
160 let fr' = make opMin $ fromList froms
161 let to' = make opMax $ fromList tos
162 return (DomainInt t [RangeBounded fr' to'], cons)
163 DomainFunction r attr innerFr innerTo -> do
164 (jPat, j) <- quantifiedVar
165 (innerFr', consFr) <- go [essence| &j[1] |] innerFr
166 (innerTo', consTo) <- go [essence| &j[2] |] innerTo
167 let innerCons = make opAnd $ fromList $ consFr ++ consTo
168 return ( DomainFunction r attr innerFr' innerTo'
169 , return [essence| forAll &jPat in &x . &innerCons |]
170 )
171 _ -> return (d, [])
172
173 let patX = Reference pat Nothing
174 (dom', cons) <- go patX (expandDomainReference domain)
175 return $ [Generator (GenDomainNoRepr (Single pat) dom')]
176 ++ map Condition cons
177 _ -> return [goc]
178 return (Comprehension body (concat gocs'))
179 fixQuantified x = return x
180
181
182 pgOnDomain ::
183 MonadUserError m =>
184 NameGen m =>
185 MonadState [(Name, String)] m =>
186 Expression -> -- how do we refer to this top level variable
187 Name -> -- its name
188 Domain () Expression -> -- its domain
189 m ( Domain () Expression -- its modified domain for the find version
190 , [Statement] -- statements that define the necessary givens
191 , [Expression] -- constraints for the generator model
192 , [Expression] -- constraints for the repair model
193 )
194 pgOnDomain x nm (expandDomainReference -> dom) =
195
196 case dom of
197
198 DomainBool -> return4 dom [] [] []
199
200 DomainInt t _ -> do
201 lbX <- minOfIntDomain dom
202 ubX <- maxOfIntDomain dom
203 lb <- lowerBoundOfIntExpr lbX
204 ub <- upperBoundOfIntExpr ubX
205
206 let nmMin = nm `mappend` "_min"
207 sawTell [(nmMin, "i")]
208 let rmin = Reference nmMin Nothing
209
210 let nmMax = nm `mappend` "_max"
211 sawTell [(nmMax, "i")]
212 let rmax = Reference nmMax Nothing
213
214 return4
215 (DomainInt t [RangeBounded lb ub])
216 [ Declaration (FindOrGiven Given nmMin
217 (DomainInt t [RangeBounded lb ub]))
218 , Declaration (FindOrGiven Given nmMax
219 -- (DomainInt t [RangeBounded 0 [essence| min([5, (&ub - &lb) / 2]) |]]))
220 (DomainInt t [RangeBounded lb ub]))
221 ]
222 ( [ [essence| &x >= &rmin |]
223 , [essence| &x <= &rmax |]
224 ] ++
225 [ [essence| &x >= &lbX |]
226 | lb /= lbX
227 ] ++
228 [ [essence| &x <= &ubX |]
229 | ub /= ubX
230 ] )
231 ( [ [essence| &rmin <= &rmax |]
232 ] )
233
234 DomainRecord ds -> do
235 inners <- forM ds $ \ (nmRec, domRec) -> do
236 let iE = Reference nmRec Nothing
237 let ref = [essence| &x[&iE] |]
238 pgOnDomain ref (nm `mappend` (Name $ pack $ "_" ++ show (pretty nmRec))) domRec
239 return4
240 (DomainRecord (zip (map fst ds) (map fst4 inners)))
241 (concatMap snd4 inners)
242 (concatMap thd4 inners)
243 (concatMap fourth4 inners)
244
245 DomainTuple ds -> do
246 inners <- forM (zip [1..] ds) $ \ (i, d) -> do
247 let iE = fromInt i
248 let ref = [essence| &x[&iE] |]
249 pgOnDomain ref (nm `mappend` (Name $ pack $ "_tuple" ++ show i)) d
250 return4
251 (DomainTuple (map fst4 inners))
252 (concatMap snd4 inners)
253 (concatMap thd4 inners)
254 (concatMap fourth4 inners)
255
256 DomainMatrix indexDomain innerDomain | categoryOf indexDomain <= CatConstant -> do
257 (iPat, i) <- quantifiedVar
258 let liftCons c = [essence| forAll &iPat : &indexDomain . &c |]
259 let ref = [essence| &x[&i] |]
260 (innerDomain', declInner, consInner, repairStmts) <- pgOnDomain ref (nm `mappend` "_inner") innerDomain
261 return4
262 (DomainMatrix indexDomain innerDomain')
263 declInner
264 (map liftCons consInner)
265 repairStmts
266
267 DomainSequence r attr innerDomain -> do
268
269 let nmCardMin = nm `mappend` "_cardMin"
270 sawTell [(nmCardMin, "i")]
271 let cardMin = Reference nmCardMin Nothing
272
273 let nmCardMax = nm `mappend` "_cardMax"
274 sawTell [(nmCardMax, "i")]
275 let cardMax = Reference nmCardMax Nothing
276
277 (iPat, i) <- quantifiedVar
278 let liftCons c = [essence| forAll &iPat in &x . &c |]
279 (domInner, declInner, consInner, repairStmts) <- pgOnDomain [essence| &i[2] |] (nm `mappend` "_inner") innerDomain
280
281 (attrOut, sizeLb, sizeUb, cardDomain) <-
282 case attr of
283 SequenceAttr size jectivity -> do
284 (sizeOut, lb, ub, cardDomain) <-
285 case size of
286 SizeAttr_None ->
287 return ( SizeAttr_MaxSize maxInt, Nothing, Nothing
288 , DomainInt TagInt [RangeBounded minInt maxInt]
289 )
290 SizeAttr_Size a -> do
291 lb <- lowerBoundOfIntExpr a
292 ub <- upperBoundOfIntExpr a
293 return ( SizeAttr_MinMaxSize lb ub, Just a, Just a
294 , DomainInt TagInt [RangeBounded lb ub]
295 )
296 SizeAttr_MinSize a -> do
297 lb <- lowerBoundOfIntExpr a
298 return ( SizeAttr_MinMaxSize lb maxInt, Just a, Nothing
299 , DomainInt TagInt [RangeBounded lb maxInt]
300 )
301 SizeAttr_MaxSize a -> do
302 ub <- upperBoundOfIntExpr a
303 return ( SizeAttr_MaxSize ub, Nothing, Just a
304 , DomainInt TagInt [RangeBounded 0 ub]
305 )
306 SizeAttr_MinMaxSize a b -> do
307 lb <- lowerBoundOfIntExpr a
308 ub <- upperBoundOfIntExpr b
309 return ( SizeAttr_MinMaxSize lb ub, Just a, Just b
310 , DomainInt TagInt [RangeBounded lb ub]
311 )
312 return (SequenceAttr sizeOut jectivity, lb, ub, cardDomain)
313
314 let
315 newDecl =
316 [ Declaration (FindOrGiven Given nmCardMin cardDomain)
317 , Declaration (FindOrGiven Given nmCardMax cardDomain)
318 ]
319
320 let
321 cardinalityCons = return $ return
322 [essence|
323 |&x| >= &cardMin /\
324 |&x| <= &cardMax
325 |]
326
327 sizeLbCons =
328 case sizeLb of
329 Nothing -> return []
330 Just bound -> return $ return [essence| |&x| >= &bound |]
331
332 sizeUbCons =
333 case sizeUb of
334 Nothing -> return []
335 Just bound -> return $ return [essence| |&x| <= &bound |]
336
337 newCons <- concat <$> sequence [cardinalityCons, sizeLbCons, sizeUbCons]
338
339 return4
340 (DomainSequence r attrOut domInner)
341 (newDecl ++ declInner)
342 (newCons ++ map liftCons consInner)
343 repairStmts
344
345 DomainSet r attr innerDomain -> do
346
347 let nmCardMin = nm `mappend` "_cardMin"
348 sawTell [(nmCardMin, "i")]
349 let cardMin = Reference nmCardMin Nothing
350
351 let nmCardMax = nm `mappend` "_cardMax"
352 sawTell [(nmCardMax, "i")]
353 let cardMax = Reference nmCardMax Nothing
354
355 (iPat, i) <- quantifiedVar
356 let liftCons c = [essence| forAll &iPat in &x . &c |]
357 (domInner, declInner, consInner, repairStmts) <- pgOnDomain i (nm `mappend` "_inner") innerDomain
358
359 (attrOut, sizeLb, sizeUb, cardDomain) <-
360 case attr of
361 SetAttr size -> do
362 (sizeOut, lb, ub, cardDomain) <-
363 case size of
364 SizeAttr_None ->
365 return ( SizeAttr_MaxSize maxInt, Nothing, Nothing
366 , DomainInt TagInt [RangeBounded minInt maxInt]
367 )
368 SizeAttr_Size a -> do
369 lb <- lowerBoundOfIntExpr a
370 ub <- upperBoundOfIntExpr a
371 return ( SizeAttr_MinMaxSize lb ub, Just a, Just a
372 , DomainInt TagInt [RangeBounded lb ub]
373 )
374 SizeAttr_MinSize a -> do
375 lb <- lowerBoundOfIntExpr a
376 return ( SizeAttr_MinMaxSize lb maxInt, Just a, Nothing
377 , DomainInt TagInt [RangeBounded lb maxInt]
378 )
379 SizeAttr_MaxSize a -> do
380 ub <- upperBoundOfIntExpr a
381 return ( SizeAttr_MaxSize ub, Nothing, Just a
382 , DomainInt TagInt [RangeBounded 0 ub]
383 )
384 SizeAttr_MinMaxSize a b -> do
385 lb <- lowerBoundOfIntExpr a
386 ub <- upperBoundOfIntExpr b
387 return ( SizeAttr_MinMaxSize lb ub, Just a, Just b
388 , DomainInt TagInt [RangeBounded lb ub]
389 )
390 return (SetAttr sizeOut, lb, ub, cardDomain)
391
392 let
393 newDecl =
394 [ Declaration (FindOrGiven Given nmCardMin cardDomain)
395 , Declaration (FindOrGiven Given nmCardMax cardDomain)
396 ]
397
398 let
399 cardinalityCons = return $ return
400 [essence|
401 |&x| >= &cardMin /\
402 |&x| <= &cardMax
403 |]
404
405 sizeLbCons =
406 case sizeLb of
407 Nothing -> return []
408 Just bound -> return $ return [essence| |&x| >= &bound |]
409
410 sizeUbCons =
411 case sizeUb of
412 Nothing -> return []
413 Just bound -> return $ return [essence| |&x| <= &bound |]
414
415 newCons <- concat <$> sequence [cardinalityCons, sizeLbCons, sizeUbCons]
416
417 return4
418 (DomainSet r attrOut domInner)
419 (newDecl ++ declInner)
420 (newCons ++ map liftCons consInner)
421 repairStmts
422
423 DomainMSet r attr innerDomain -> do
424
425 let nmCardMin = nm `mappend` "_cardMin"
426 sawTell [(nmCardMin, "i")]
427 let cardMin = Reference nmCardMin Nothing
428
429 let nmCardMax = nm `mappend` "_cardMax"
430 sawTell [(nmCardMax, "i")]
431 let cardMax = Reference nmCardMax Nothing
432
433 (iPat, i) <- quantifiedVar
434 let liftCons c = [essence| forAll &iPat in &x . &c |]
435 (domInner, declInner, consInner, repairStmts) <- pgOnDomain i (nm `mappend` "_inner") innerDomain
436
437 (attrOut, sizeLb, sizeUb, cardDomain, occurLb, occurUb) <-
438 case attr of
439 MSetAttr sizeAttr occurAttr -> do
440 (sizeAttrOut, sizeLb, sizeUb, cardDomain) <-
441 case sizeAttr of
442 SizeAttr_None ->
443 return ( SizeAttr_MaxSize maxInt, Nothing, Nothing
444 , DomainInt TagInt [RangeBounded minInt maxInt]
445 )
446 SizeAttr_Size a -> do
447 lb <- lowerBoundOfIntExpr a
448 ub <- upperBoundOfIntExpr a
449 return ( SizeAttr_MinMaxSize lb ub, Just a, Just a
450 , DomainInt TagInt [RangeBounded lb ub]
451 )
452 SizeAttr_MinSize a -> do
453 lb <- lowerBoundOfIntExpr a
454 return ( SizeAttr_MinMaxSize lb maxInt, Just a, Nothing
455 , DomainInt TagInt [RangeBounded lb maxInt]
456 )
457 SizeAttr_MaxSize a -> do
458 ub <- upperBoundOfIntExpr a
459 return ( SizeAttr_MaxSize ub, Nothing, Just a
460 , DomainInt TagInt [RangeBounded 0 ub]
461 )
462 SizeAttr_MinMaxSize a b -> do
463 lb <- lowerBoundOfIntExpr a
464 ub <- upperBoundOfIntExpr b
465 return ( SizeAttr_MinMaxSize lb ub, Just a, Just b
466 , DomainInt TagInt [RangeBounded lb ub]
467 )
468 (occurAttrOut, occurLb, occurUb) <-
469 case occurAttr of
470 OccurAttr_None ->
471 return (OccurAttr_MaxOccur maxInt, Nothing, Nothing)
472 OccurAttr_MinOccur a -> do
473 lb <- lowerBoundOfIntExpr a
474 return (OccurAttr_MinMaxOccur lb maxInt, Just a, Nothing)
475 OccurAttr_MaxOccur a -> do
476 ub <- upperBoundOfIntExpr a
477 return (OccurAttr_MaxOccur ub, Nothing, Just a)
478 OccurAttr_MinMaxOccur a b -> do
479 lb <- lowerBoundOfIntExpr a
480 ub <- upperBoundOfIntExpr b
481 return (OccurAttr_MinMaxOccur lb ub, Just a, Just b)
482 return (MSetAttr sizeAttrOut occurAttrOut, sizeLb, sizeUb, cardDomain, occurLb, occurUb)
483
484 let
485 newDecl =
486 [ Declaration (FindOrGiven Given nmCardMin cardDomain)
487 , Declaration (FindOrGiven Given nmCardMax cardDomain)
488 ]
489
490 let
491 cardinalityCons = return $ return
492 [essence|
493 |&x| >= &cardMin /\
494 |&x| <= &cardMax
495 |]
496
497 sizeLbCons =
498 case sizeLb of
499 Nothing -> return []
500 Just bound -> return $ return [essence| |&x| >= &bound |]
501
502 sizeUbCons =
503 case sizeUb of
504 Nothing -> return []
505 Just bound -> return $ return [essence| |&x| <= &bound |]
506
507 occurLbCons =
508 case occurLb of
509 Nothing -> return []
510 Just bound -> return $ return $ liftCons [essence| freq(&x, &i) >= &bound |]
511
512 occurUbCons =
513 case occurUb of
514 Nothing -> return []
515 Just bound -> return $ return $ liftCons [essence| freq(&x, &i) <= &bound |]
516
517 newCons <- concat <$> sequence [cardinalityCons, sizeLbCons, sizeUbCons, occurLbCons, occurUbCons]
518
519 return4
520 (DomainMSet r attrOut domInner)
521 (newDecl ++ declInner)
522 (newCons ++ map liftCons consInner)
523 repairStmts
524
525 DomainFunction r attr innerDomainFr innerDomainTo -> do
526
527 let nmCardMin = nm `mappend` "_cardMin"
528 sawTell [(nmCardMin, "i")]
529 let cardMin = Reference nmCardMin Nothing
530
531 let nmCardMax = nm `mappend` "_cardMax"
532 sawTell [(nmCardMax, "i")]
533 let cardMax = Reference nmCardMax Nothing
534
535 (iPat, i) <- quantifiedVar
536 let liftCons c = [essence| forAll &iPat in &x . &c |]
537 (domFr, declFr, consFr, repairStmtsFr) <- pgOnDomain [essence| &i[1] |] (nm `mappend` "_defined") innerDomainFr
538 (domTo, declTo, consTo, repairStmtsTo) <- pgOnDomain [essence| &i[2] |] (nm `mappend` "_range") innerDomainTo
539
540 -- drop total, post constraint instead
541 (attrOut, sizeLb, sizeUb, cardDomain) <-
542 case attr of
543 FunctionAttr size PartialityAttr_Partial jectivity -> do
544 (sizeOut, lb, ub, cardDomain) <-
545 case size of
546 SizeAttr_None -> do
547 mdomSize <- runExceptT $ domainSizeOf innerDomainFr
548 case mdomSize of
549 Left{} ->
550 return ( SizeAttr_MaxSize maxInt, Nothing, Nothing
551 , DomainInt TagInt [RangeBounded minInt maxInt]
552 )
553 Right domSize -> do
554 domSizeUpp <- upperBoundOfIntExpr domSize
555 return ( SizeAttr_MaxSize maxInt, Nothing, Nothing
556 , DomainInt TagInt [RangeBounded 0 domSizeUpp]
557 )
558 SizeAttr_Size a -> do
559 lb <- lowerBoundOfIntExpr a
560 ub <- upperBoundOfIntExpr a
561 return ( SizeAttr_MinMaxSize lb ub, Just a, Just a
562 , DomainInt TagInt [RangeBounded lb ub]
563 )
564 SizeAttr_MinSize a -> do
565 lb <- lowerBoundOfIntExpr a
566 return ( SizeAttr_MinMaxSize lb maxInt, Just a, Nothing
567 , DomainInt TagInt [RangeBounded lb maxInt]
568 )
569 SizeAttr_MaxSize a -> do
570 ub <- upperBoundOfIntExpr a
571 return ( SizeAttr_MaxSize ub, Nothing, Just a
572 , DomainInt TagInt [RangeBounded 0 ub]
573 )
574 SizeAttr_MinMaxSize a b -> do
575 lb <- lowerBoundOfIntExpr a
576 ub <- upperBoundOfIntExpr b
577 return ( SizeAttr_MinMaxSize lb ub, Just a, Just b
578 , DomainInt TagInt [RangeBounded lb ub]
579 )
580 return (FunctionAttr sizeOut PartialityAttr_Partial jectivity, lb, ub, cardDomain)
581 FunctionAttr _size PartialityAttr_Total jectivity -> do
582 return (FunctionAttr SizeAttr_None PartialityAttr_Partial jectivity, Nothing, Nothing, bug "cardDomain not needed")
583
584 let isTotal = case attr of
585 FunctionAttr _ PartialityAttr_Total _ -> True
586 _ -> False
587 isPartial = not isTotal
588
589 let
590 newDecl | isTotal = []
591 | otherwise =
592 [ Declaration (FindOrGiven Given nmCardMin cardDomain)
593 , Declaration (FindOrGiven Given nmCardMax cardDomain)
594 ]
595
596 let
597 cardinalityCons | isTotal = return []
598 | otherwise = return $ return
599 [essence|
600 |&x| >= &cardMin /\
601 |&x| <= &cardMax
602 |]
603
604 totalityCons | isPartial = return []
605 | otherwise = do
606
607 let
608 go d = case d of
609 DomainInt{} -> do
610 dMin <- minOfIntDomain d
611 dMax <- maxOfIntDomain d
612 return (\ k -> [essence| (&k >= &dMin /\ &k <= &dMax) |] )
613 DomainTuple ds -> do
614 makers <- mapM go ds
615 return $ \ k -> make opAnd $ fromList
616 [ mk [essence| &k[&nExpr] |]
617 | (mk, n) <- zip makers [1..]
618 , let nExpr = fromInt n
619 ]
620 DomainSet _ _ inner -> do
621 (jPat, j) <- quantifiedVar
622 maker <- go inner
623 let innerCons = maker j
624 return $ \ k -> [essence| forAll &jPat in &k . &innerCons |]
625 DomainMSet _ _ inner -> do
626 (jPat, j) <- quantifiedVar
627 maker <- go inner
628 let innerCons = maker j
629 return $ \ k -> [essence| forAll &jPat in &k . &innerCons |]
630 _ -> bug $ "Unhandled domain (in function defined):" <+> vcat [pretty d, pretty (show d)]
631
632 mkCondition <- go innerDomainFr
633
634 let iCondition = mkCondition i
635
636 return $ return [essence|
637 forAll &iPat : &domFr .
638 &iCondition
639 <->
640 &i in defined(&x)
641 |]
642
643 sizeLbCons =
644 case sizeLb of
645 Nothing -> return []
646 Just bound -> return $ return [essence| |&x| >= &bound |]
647
648 sizeUbCons =
649 case sizeUb of
650 Nothing -> return []
651 Just bound -> return $ return [essence| |&x| <= &bound |]
652
653 -- only for bool domains (innerDomainTo)
654 let nmPercentageMax = nm `mappend` "_percentage_max"
655 let nmPercentageMin = nm `mappend` "_percentage_min"
656 let refPercentageMax = Reference nmPercentageMax Nothing
657 let refPercentageMin = Reference nmPercentageMin Nothing
658 sawTell [(nmPercentageMax, "i")]
659 sawTell [(nmPercentageMin, "i")]
660
661 let isToBool = case innerDomainTo of
662 DomainBool -> True
663 _ -> False
664
665 let declToBool =
666 [ Declaration (FindOrGiven Given nmPercentageMin (DomainInt TagInt [RangeBounded 0 100]))
667 , Declaration (FindOrGiven Given nmPercentageMax (DomainInt TagInt [RangeBounded 0 100]))
668 ]
669 let consToBool = make opAnd $ fromList
670 [ [essence| sum([ toInt(&i[2]) | &iPat <- &x ]) <= &refPercentageMax * |defined(&x)| / 100 |]
671 , [essence| sum([ toInt(&i[2]) | &iPat <- &x ]) >= &refPercentageMin * |defined(&x)| / 100 |]
672 ]
673
674 newCons <- concat <$> sequence [cardinalityCons, totalityCons, sizeLbCons, sizeUbCons]
675 let innerCons = concat $ concat
676 [ [consFr | isPartial ] -- only if the function is not total
677 , [consTo]
678 ]
679
680 let
681 appendToReferences suffix (Reference n _) = Reference (n `mappend` suffix) Nothing
682 appendToReferences _ n = n
683
684 let
685
686 definedBoundCons n d =
687 case d of
688 DomainInt{} -> do
689 let
690 defined_max = Reference (n `mappend` "_max") Nothing
691 defined_min = Reference (n `mappend` "_min") Nothing
692 defined_maxBound <- transform (appendToReferences "_max") <$> maxOfIntDomain d
693 defined_minBound <- transform (appendToReferences "_min") <$> minOfIntDomain d
694 return [ [essence| &defined_min >= &defined_minBound |]
695 , [essence| &defined_max <= &defined_maxBound |]
696 ]
697 DomainTuple ds ->
698 concatForM (zip allNats ds) $ \ (n', d') ->
699 definedBoundCons
700 (mconcat [n, "_tuple", Name (stringToText $ show n')])
701 d'
702 _ -> return []
703
704 definedGtCard =
705 case innerDomainFr of
706 DomainTuple ds ->
707 let
708 defined_min n =
709 Reference
710 (mconcat [nm, "_defined_tuple", Name (stringToText $ show n), "_min"])
711 Nothing
712 defined_max n =
713 Reference
714 (mconcat [nm, "_defined_tuple", Name (stringToText $ show n), "_max"])
715 Nothing
716 one n = let minn = defined_min n
717 maxn = defined_max n
718 in [essence| &maxn - &minn + 1 |]
719 multiplied = make opProduct $ fromList $ map one [1..length ds]
720 in
721 [essence| &multiplied >= &cardMax |]
722 _ ->
723 let
724 defined_max = Reference (nm `mappend` "_defined_max") Nothing
725 defined_min = Reference (nm `mappend` "_defined_min") Nothing
726 in
727 [essence| &defined_max - &defined_min + 1 >= &cardMax |]
728
729 definedBoundCons' <- definedBoundCons (nm `mappend` "_defined") innerDomainFr
730
731 let repairCons = [ [essence| &cardMin <= &cardMax |] | isPartial ]
732 ++ [ definedGtCard | isPartial ]
733 ++ concat [ definedBoundCons' | isPartial ]
734 ++ [ [essence| &refPercentageMax >= &refPercentageMin |] | isToBool ]
735
736 return4
737 (DomainFunction r attrOut domFr domTo)
738 (newDecl ++ concat [ declFr | isPartial ] ++ declTo ++ concat [ declToBool | isToBool ])
739 (newCons ++ map liftCons innerCons ++ concat [[consToBool] | isToBool ])
740 (repairCons ++ concat [ repairStmtsFr | isPartial ] ++ repairStmtsTo)
741
742 DomainRelation r attr innerDomains -> do
743
744 let nmCardMin = nm `mappend` "_cardMin"
745 sawTell [(nmCardMin, "i")]
746 let cardMin = Reference nmCardMin Nothing
747
748 let nmCardMax = nm `mappend` "_cardMax"
749 sawTell [(nmCardMax, "i")]
750 let cardMax = Reference nmCardMax Nothing
751
752 (iPat, i) <- quantifiedVar
753 let liftCons c = [essence| forAll &iPat in &x . &c |]
754
755 inners <- forM (zip [1..] innerDomains) $ \ (n, d) -> do
756 let nE = fromInt n
757 let ref = [essence| &i[&nE] |]
758 (d', decl, cons, repairStmts) <- pgOnDomain ref (nm `mappend` (Name $ pack $ "_relation" ++ show n)) d
759 return (d', decl, map liftCons cons, repairStmts)
760
761 let maxIntN = maxIntTimes (genericLength innerDomains)
762
763 (attrOut, sizeLb, sizeUb, cardDomain) <-
764 case attr of
765 RelationAttr size binRelAttr -> do
766 (sizeOut, lb, ub, cardDomain) <-
767 case size of
768 SizeAttr_None ->
769 return ( SizeAttr_MaxSize maxIntN, Nothing, Nothing
770 , DomainInt TagInt [RangeBounded minInt maxIntN]
771 )
772 SizeAttr_Size a -> do
773 lb <- lowerBoundOfIntExpr a
774 ub <- upperBoundOfIntExpr a
775 return ( SizeAttr_MinMaxSize lb ub, Just a, Just a
776 , DomainInt TagInt [RangeBounded lb ub]
777 )
778 SizeAttr_MinSize a -> do
779 lb <- lowerBoundOfIntExpr a
780 return ( SizeAttr_MinMaxSize lb maxIntN, Just a, Nothing
781 , DomainInt TagInt [RangeBounded lb maxIntN]
782 )
783 SizeAttr_MaxSize a -> do
784 ub <- upperBoundOfIntExpr a
785 return ( SizeAttr_MaxSize ub, Nothing, Just a
786 , DomainInt TagInt [RangeBounded 0 ub]
787 )
788 SizeAttr_MinMaxSize a b -> do
789 lb <- lowerBoundOfIntExpr a
790 ub <- upperBoundOfIntExpr b
791 return ( SizeAttr_MinMaxSize lb ub, Just a, Just b
792 , DomainInt TagInt [RangeBounded lb ub]
793 )
794 return (RelationAttr sizeOut binRelAttr, lb, ub, cardDomain)
795
796 let
797 newDecl =
798 [ Declaration (FindOrGiven Given nmCardMin cardDomain)
799 , Declaration (FindOrGiven Given nmCardMax cardDomain)
800 ]
801
802 let
803 cardinalityCons = return $ return
804 [essence|
805 |&x| >= &cardMin /\
806 |&x| <= &cardMax
807 |]
808
809 sizeLbCons =
810 case sizeLb of
811 Nothing -> return []
812 Just bound -> return $ return [essence| |&x| >= &bound |]
813
814 sizeUbCons =
815 case sizeUb of
816 Nothing -> return []
817 Just bound -> return $ return [essence| |&x| <= &bound |]
818
819 newCons <- concat <$> sequence [cardinalityCons, sizeLbCons, sizeUbCons]
820
821 return4
822 (DomainRelation r attrOut (map fst4 inners))
823 (newDecl ++ concatMap snd4 inners)
824 (newCons ++ concatMap thd4 inners)
825 (concatMap fourth4 inners)
826
827 _ -> userErr1 $ "Unhandled domain:" <++> vcat [ pretty dom
828 , pretty (show dom)
829 ]
830
831
832 -- helper functions
833
834 return4 :: Monad m => a -> b -> c -> d -> m (a,b,c,d)
835 return4 x y z w = return (x,y,z,w)
836
837 minInt :: Expression
838 minInt = Reference "MININT" Nothing
839
840 maxInt :: Expression
841 maxInt = Reference "MAXINT" Nothing
842
843 maxIntTimes :: Integer -> Expression
844 maxIntTimes n = let m = fromInt n in [essence| &maxInt ** &m |]
845
846
847 minOfIntDomain :: MonadUserError m => Domain () Expression -> m Expression
848 minOfIntDomain (DomainInt _ rs) = do
849 xs <- sortNub <$> mapM minOfIntRange rs
850 case xs of
851 [] -> return minInt
852 [x] -> return x
853 _ -> return $ make opMin $ fromList xs
854 minOfIntDomain d = userErr1 $ "Expected integer domain, but got:" <++> vcat [pretty d, pretty (show d)]
855
856 minOfIntRange :: Monad m => Range Expression -> m Expression
857 minOfIntRange (RangeSingle lb) = return lb
858 minOfIntRange (RangeLowerBounded lb) = return lb
859 minOfIntRange (RangeBounded lb _) = return lb
860 minOfIntRange _ = return minInt
861
862 lowerBoundOfIntExpr :: MonadUserError m => Expression -> m Expression
863 lowerBoundOfIntExpr x@Constant{} = return x
864 lowerBoundOfIntExpr x | x == minInt = return minInt
865 lowerBoundOfIntExpr x | x == maxInt = return maxInt
866 lowerBoundOfIntExpr (Reference _ (Just (DeclNoRepr Given _ dom _))) = minOfIntDomain dom
867 lowerBoundOfIntExpr (Reference _ (Just (Alias x))) = lowerBoundOfIntExpr x
868 lowerBoundOfIntExpr (Reference _ _) = return minInt
869 lowerBoundOfIntExpr (Op (MkOpMinus (OpMinus a b))) = do
870 aLower <- lowerBoundOfIntExpr a
871 bUpper <- upperBoundOfIntExpr b
872 return $ make opMinus aLower bUpper
873 lowerBoundOfIntExpr (Op (MkOpSum (OpSum x))) | Just xs <- listOut x = do
874 bounds <- mapM lowerBoundOfIntExpr xs
875 return $ make opSum $ fromList bounds
876 -- TODO: check for negatives
877 lowerBoundOfIntExpr (Op (MkOpProduct (OpProduct x))) | Just xs <- listOut x = do
878 bounds <- mapM lowerBoundOfIntExpr xs
879 return $ make opProduct $ fromList bounds
880 lowerBoundOfIntExpr (Op (MkOpMin (OpMin x))) | Just xs <- listOut x = do
881 bounds <- mapM lowerBoundOfIntExpr xs
882 return $ make opMin $ fromList bounds
883 lowerBoundOfIntExpr (Op (MkOpMin (OpMin (Comprehension body gocs)))) = do
884 body' <- lowerBoundOfIntExpr body
885 return $ make opMin $ Comprehension body' gocs
886 lowerBoundOfIntExpr (Op (MkOpMax (OpMax x))) | Just xs <- listOut x = do
887 bounds <- mapM lowerBoundOfIntExpr xs
888 return $ make opMin $ fromList bounds
889 lowerBoundOfIntExpr (Op (MkOpMax (OpMax (Comprehension body gocs)))) = do
890 body' <- lowerBoundOfIntExpr body
891 return $ make opMin $ Comprehension body' gocs
892 lowerBoundOfIntExpr (Op (MkOpNegate (OpNegate x))) = do
893 bound <- upperBoundOfIntExpr x
894 return (make opNegate bound)
895 lowerBoundOfIntExpr x = userErr1 $ "Cannot compute lower bound of integer expression:" <++> vcat [pretty x, pretty (show x)]
896
897
898 maxOfIntDomain :: MonadUserError m => Domain () Expression -> m Expression
899 maxOfIntDomain (DomainInt _ rs) = do
900 xs <- sortNub <$> mapM maxOfIntRange rs
901 case xs of
902 [] -> return maxInt
903 [x] -> return x
904 _ -> return $ make opMax $ fromList xs
905 maxOfIntDomain d = userErr1 $ "Expected integer domain, but got:" <++> pretty d
906
907 maxOfIntRange :: Monad m => Range Expression -> m Expression
908 maxOfIntRange (RangeSingle ub) = return ub
909 maxOfIntRange (RangeUpperBounded ub) = return ub
910 maxOfIntRange (RangeBounded _ ub) = return ub
911 maxOfIntRange _ = return maxInt
912
913 upperBoundOfIntExpr :: MonadUserError m => Expression -> m Expression
914 upperBoundOfIntExpr x@Constant{} = return x
915 upperBoundOfIntExpr x | x == minInt = return minInt
916 upperBoundOfIntExpr x | x == maxInt = return maxInt
917 upperBoundOfIntExpr (Reference _ (Just (DeclNoRepr Given _ dom _))) = maxOfIntDomain dom
918 upperBoundOfIntExpr (Reference _ (Just (Alias x))) = upperBoundOfIntExpr x
919 upperBoundOfIntExpr (Reference _ _) = return maxInt
920 upperBoundOfIntExpr (Op (MkOpMinus (OpMinus a b))) = do
921 aUpper <- upperBoundOfIntExpr a
922 bLower <- lowerBoundOfIntExpr b
923 return $ make opMinus aUpper bLower
924 upperBoundOfIntExpr (Op (MkOpSum (OpSum x))) | Just xs <- listOut x = do
925 bounds <- mapM upperBoundOfIntExpr xs
926 return $ make opSum $ fromList bounds
927 -- TODO: check for negatives
928 upperBoundOfIntExpr (Op (MkOpProduct (OpProduct x))) | Just xs <- listOut x = do
929 bounds <- mapM upperBoundOfIntExpr xs
930 return $ make opProduct $ fromList bounds
931 upperBoundOfIntExpr (Op (MkOpMin (OpMin x))) | Just xs <- listOut x = do
932 bounds <- mapM upperBoundOfIntExpr xs
933 return $ make opMax $ fromList bounds
934 upperBoundOfIntExpr (Op (MkOpMin (OpMin (Comprehension body gocs)))) = do
935 body' <- lowerBoundOfIntExpr body
936 return $ make opMax $ Comprehension body' gocs
937 upperBoundOfIntExpr (Op (MkOpMax (OpMax x))) | Just xs <- listOut x = do
938 bounds <- mapM upperBoundOfIntExpr xs
939 return $ make opMax $ fromList bounds
940 upperBoundOfIntExpr (Op (MkOpMax (OpMax (Comprehension body gocs)))) = do
941 body' <- lowerBoundOfIntExpr body
942 return $ make opMax $ Comprehension body' gocs
943 upperBoundOfIntExpr (Op (MkOpNegate (OpNegate x))) = do
944 bound <- lowerBoundOfIntExpr x
945 return (make opNegate bound)
946 upperBoundOfIntExpr x = userErr1 $ "Cannot compute upper bound of integer expression:" <++> vcat [pretty x, pretty (show x)]