never executed always true always false
1
2 module Conjure.Process.FiniteGivens
3 ( finiteGivens
4 , finiteGivensParam
5 ) where
6
7 import Conjure.Prelude
8 import Conjure.Bug
9 import Conjure.UserError
10 import Conjure.Language.Definition
11 import Conjure.Language.Constant
12 import Conjure.Language.Domain
13 import Conjure.Language.Pretty
14 import Conjure.Language.Instantiate ( instantiateExpression, instantiateDomain )
15 import Conjure.Language.ZeroVal ( zeroVal )
16 import Conjure.Language.Type
17 import Conjure.Process.Enumerate ( EnumerateDomain )
18
19
20 -- | givens should have finite domains. except ints.
21 -- this transformation introduces extra given ints to make them finite.
22 -- the values for the extra givens will be computed during translate-solution
23 finiteGivens ::
24 MonadFailDoc m =>
25 NameGen m =>
26 MonadLog m =>
27 MonadUserError m =>
28 EnumerateDomain m =>
29 (?typeCheckerMode :: TypeCheckerMode) =>
30 Model -> m Model
31 finiteGivens m = flip evalStateT 1 $ do
32 statements <- forM (mStatements m) $ \ st ->
33 case st of
34 Declaration (FindOrGiven Given name domain) -> do
35 (domain', extras, _) <- mkFinite domain
36 return $ [ Declaration $ FindOrGiven Given e (DomainInt TagInt []) | e <- extras ]
37 ++ [ Declaration $ FindOrGiven Given name domain' ]
38 _ -> return [st]
39 namegenst <- exportNameGenState
40 return m { mStatements = concat statements
41 , mInfo = (mInfo m) { miNameGenState = namegenst
42 , miNbExtraGivens = maybe 0 (\ n -> n - 1 ) (lookup "fin" namegenst)
43 }
44 }
45
46
47 finiteGivensParam ::
48 MonadFailDoc m =>
49 NameGen m =>
50 MonadLog m =>
51 MonadUserError m =>
52 EnumerateDomain m =>
53 (?typeCheckerMode :: TypeCheckerMode) =>
54 Model -> -- eprime
55 Model -> -- essence-param
56 [(Name, Constant)] -> -- some additional lettings
57 m (Model, [Name]) -- essence-param
58 finiteGivensParam eprimeModel essenceParam additionalLettings = flip evalStateT 1 $ do
59 let essenceGivenNames = eprimeModel |> mInfo |> miGivens
60 let essenceGivens = eprimeModel |> mInfo |> miOriginalDomains
61 let essenceLettings = extractLettings essenceParam
62 ++ eprimeModel |> mInfo |> miLettings
63 ++ [ (nm, Constant c) | (nm, c) <- additionalLettings ]
64 let nbExtraGivens = eprimeModel |> mInfo |> miNbExtraGivens
65 let expectedExtras = [ MachineName "fin" extraGiven []
66 | extraGiven <- [1..nbExtraGivens]
67 ]
68 extras <- fmap concat $ forM essenceGivenNames $ \ name -> do
69 logDebugVerbose $ "finiteGivensParam name" <+> pretty name
70 case (lookup name essenceGivens, lookup name essenceLettings) of
71 (Nothing, _) -> bug $ "Not found:" <+> pretty name
72 (_, Nothing) -> return []
73 (Just domain', Just expr) -> do
74 logDebugVerbose $ "finiteGivensParam domain' " <+> pretty domain'
75 domain <- failToUserError $ fmap Constant <$> instantiateDomain essenceLettings domain'
76 logDebugVerbose $ "finiteGivensParam domain " <+> pretty domain
77 logDebugVerbose $ "finiteGivensParam expr " <+> pretty expr
78 constant <- failToUserError $ instantiateExpression essenceLettings expr
79 logDebugVerbose $ "finiteGivensParam constant" <+> pretty constant
80 (_, _, f) <- mkFinite domain
81 outs <- f constant
82 logDebugVerbose $ "finiteGivensParam outs " <+> vcat (map pretty outs)
83 return outs
84 logDebugVerbose $ "finiteGivensParam extras " <+> vcat (map (pretty . show) extras)
85 return
86 ( essenceParam
87 { mStatements = [ Declaration (Letting name (Constant value))
88 | name <- expectedExtras
89 -- we are storing the number of "extra givens" in the model info.
90 -- also, defaulting their values to 0 if they do not come out of
91 -- the usual finiteGivens process.
92 -- the idea is: if they don't come out from that,
93 -- they must be a part of an emply collection, hence 0.
94 , let value = fromMaybe 0 (lookup name extras)
95 ]
96 ++ mStatements essenceParam
97 }
98 , expectedExtras
99 )
100
101
102 -- | given a domain, add it additional attributes to make it _smaller_
103 -- for example, this means adding a size attribute at the outer-most level
104 -- and adding a maxSize attribute at the inner levels.
105 mkFinite ::
106 MonadFailDoc m =>
107 MonadState Int m =>
108 NameGen m =>
109 MonadLog m =>
110 MonadUserError m =>
111 EnumerateDomain m =>
112 (?typeCheckerMode :: TypeCheckerMode) =>
113 Domain () Expression ->
114 m ( Domain () Expression -- "finite" domain
115 , [Name] -- extra givens
116 , Constant -> m [(Name, Constant)] -- value calculator for the extra givens
117 ) -- input is a list of values for the domain
118 mkFinite d@DomainTuple{} = mkFiniteOutermost d
119 mkFinite d@DomainRecord{} = mkFiniteOutermost d
120 mkFinite d@DomainVariant{} = mkFiniteOutermost d
121 mkFinite d@DomainMatrix{} = mkFiniteOutermost d
122 mkFinite d@DomainSet{} = mkFiniteOutermost d
123 mkFinite d@DomainMSet{} = mkFiniteOutermost d
124 mkFinite d@DomainSequence{} = mkFiniteOutermost d
125 mkFinite d@DomainPermutation{} = mkFiniteOutermost d
126 mkFinite d@DomainFunction{} = mkFiniteOutermost d
127 mkFinite d@DomainRelation{} = mkFiniteOutermost d
128 mkFinite d@DomainPartition{} = mkFiniteOutermost d
129 mkFinite d = return (d, [], const (return []))
130
131
132 -- TODO add permutation support
133 mkFiniteOutermost ::
134 MonadFailDoc m =>
135 MonadState Int m =>
136 NameGen m =>
137 MonadLog m =>
138 MonadUserError m =>
139 EnumerateDomain m =>
140 (?typeCheckerMode :: TypeCheckerMode) =>
141 Domain () Expression ->
142 m ( Domain () Expression
143 , [Name]
144 , Constant -> m [(Name, Constant)]
145 )
146 mkFiniteOutermost (DomainTuple inners) = do
147 mids <- mapM mkFiniteInner inners
148 return
149 ( DomainTuple (map fst3 mids)
150 , concatMap snd3 mids
151 , \ constant -> do
152 logDebug $ "mkFiniteOutermost DomainTuple" <+> pretty constant
153 xs <- failToUserError $ viewConstantTuple constant
154 let innerFs = map thd3 mids
155 innerValues <- sequence [ innerF [x] | (innerF, x) <- zip innerFs xs ]
156 return (concat innerValues)
157 )
158 mkFiniteOutermost (DomainRecord (sortOn fst -> inners)) = do
159 mids <- mapM (mkFiniteInner . snd) inners
160 return
161 ( DomainRecord (zip (map fst inners) (map fst3 mids))
162 , concatMap snd3 mids
163 , \ constant -> do
164 logDebug $ "mkFiniteOutermost DomainRecord" <+> pretty constant
165 xs' <- failToUserError $ viewConstantRecord constant
166 let
167 xs :: [Constant]
168 xs = map snd $ sortOn fst xs'
169 let innerFs = map thd3 mids
170 innerValues <- sequence [ innerF [x] | (innerF, x) <- zip innerFs xs ]
171 return (concat innerValues)
172 )
173 mkFiniteOutermost (DomainVariant inners) = do
174 mids <- mapM (mkFiniteInner . snd) inners
175 return
176 ( DomainVariant (zip (map fst inners) (map fst3 mids))
177 , concatMap snd3 mids
178 , \ constant -> do
179 logDebug $ "mkFiniteOutermost DomainVariant" <+> pretty constant
180 xs' <- failToUserError $ viewConstantVariant constant
181 xs :: [Constant] <- sequence
182 [ case xs' of
183 (_, nm', c') | nm == nm' -> return c'
184 _ -> failToUserError $ instantiateDomain [] d >>= zeroVal
185 | (nm, d) <- inners ]
186 let innerFs = map thd3 mids
187 innerValues <- sequence [ innerF [x] | (innerF, x) <- zip innerFs xs ]
188 return (concat innerValues)
189 )
190 mkFiniteOutermost (DomainMatrix index inner) = do
191 (inner', innerExtras, innerF) <- mkFiniteInner inner
192 return
193 ( DomainMatrix index inner'
194 , innerExtras
195 , \ constant -> do
196 logDebug $ "mkFiniteOutermost DomainMatrix" <+> pretty constant
197 (_, matr) <- failToUserError $ viewConstantMatrix constant
198 innerValues <- innerF matr
199 return innerValues
200 )
201 mkFiniteOutermost (DomainSet () attr@(SetAttr SizeAttr_Size{}) inner) = do
202 (inner', innerExtras, innerF) <- mkFiniteInner inner
203 return
204 ( DomainSet () attr inner'
205 , innerExtras
206 , \ constant -> do
207 logDebug $ "mkFiniteOutermost DomainSet" <+> pretty constant
208 set <- failToUserError $ viewConstantSet constant
209 innerValues <- innerF set
210 return innerValues
211 )
212 mkFiniteOutermost (DomainSet () _ inner) = do
213 s <- nextName "fin"
214 (inner', innerExtras, innerF) <- mkFiniteInner inner
215 return
216 ( DomainSet () (SetAttr (SizeAttr_Size (fromName s))) inner'
217 , s:innerExtras
218 , \ constant -> do
219 logDebug $ "mkFiniteOutermost DomainSet" <+> pretty constant
220 set <- failToUserError $ viewConstantSet constant
221 let setSize = genericLength set
222 innerValues <- innerF set
223 return $ innerValues ++ [(s, ConstantInt TagInt setSize)]
224 )
225 mkFiniteOutermost (DomainMSet () attr@(MSetAttr SizeAttr_Size{} _) inner) = do
226 (inner', innerExtras, innerF) <- mkFiniteInner inner
227 return
228 ( DomainMSet () attr inner'
229 , innerExtras
230 , \ constant -> do
231 logDebug $ "mkFiniteOutermost DomainMSet" <+> pretty constant
232 set <- failToUserError $ viewConstantMSet constant
233 innerValues <- innerF set
234 return innerValues
235 )
236 mkFiniteOutermost (DomainMSet () (MSetAttr _ occurAttr) inner) = do
237 s <- nextName "fin"
238 (inner', innerExtras, innerF) <- mkFiniteInner inner
239 return
240 ( DomainMSet () (MSetAttr (SizeAttr_Size (fromName s)) occurAttr) inner'
241 , s:innerExtras
242 , \ constant -> do
243 logDebug $ "mkFiniteOutermost DomainMSet" <+> pretty constant
244 set <- failToUserError $ viewConstantMSet constant
245 let setSize = genericLength set
246 innerValues <- innerF set
247 return $ innerValues ++ [(s, ConstantInt TagInt setSize)]
248 )
249 mkFiniteOutermost (DomainSequence () attr@(SequenceAttr SizeAttr_Size{} _) inner) = do
250 (inner', innerExtras, innerF) <- mkFiniteInner inner
251 return
252 ( DomainSequence () attr inner'
253 , innerExtras
254 , \ constant -> do
255 logDebug $ "mkFiniteOutermost DomainSequence" <+> pretty constant
256 set <- failToUserError $ viewConstantSequence constant
257 innerValues <- innerF set
258 return innerValues
259 )
260 mkFiniteOutermost (DomainSequence () (SequenceAttr _ jectivityAttr) inner) = do
261 s <- nextName "fin"
262 (inner', innerExtras, innerF) <- mkFiniteInner inner
263 return
264 ( DomainSequence () (SequenceAttr (SizeAttr_Size (fromName s)) jectivityAttr) inner'
265 , s:innerExtras
266 , \ constant -> do
267 logDebug $ "mkFiniteOutermost DomainSequence" <+> pretty constant
268 set <- failToUserError $ viewConstantSequence constant
269 let setSize = genericLength set
270 innerValues <- innerF set
271 return $ innerValues ++ [(s, ConstantInt TagInt setSize)]
272 )
273 mkFiniteOutermost (DomainFunction () attr@(FunctionAttr SizeAttr_Size{} _ _) innerFr innerTo) = do
274 (innerFr', innerFrExtras, innerFrF) <- mkFiniteInner innerFr
275 (innerTo', innerToExtras, innerToF) <- mkFiniteInner innerTo
276 return
277 ( DomainFunction () attr innerFr' innerTo'
278 , innerFrExtras ++ innerToExtras
279 , \ constant -> do
280 logDebug $ "mkFiniteOutermost DomainFunction" <+-> pretty constant
281 function <- failToUserError $ viewConstantFunction constant
282 innerFrValues <- innerFrF (map fst function)
283 innerToValues <- innerToF (map snd function)
284 return $ innerFrValues ++ innerToValues
285 )
286 mkFiniteOutermost (DomainFunction () (FunctionAttr _ partialityAttr jectivityAttr) innerFr innerTo) = do
287 s <- nextName "fin"
288 (innerFr', innerFrExtras, innerFrF) <- mkFiniteInner innerFr
289 (innerTo', innerToExtras, innerToF) <- mkFiniteInner innerTo
290 return
291 ( DomainFunction ()
292 (FunctionAttr (SizeAttr_Size (fromName s)) partialityAttr jectivityAttr)
293 innerFr' innerTo'
294 , s : innerFrExtras ++ innerToExtras
295 , \ constant -> do
296 logDebug $ "mkFiniteOutermost DomainFunction" <+-> pretty constant
297 function <- failToUserError $ viewConstantFunction constant
298 let functionSize = genericLength function
299 innerFrValues <- innerFrF (map fst function)
300 innerToValues <- innerToF (map snd function)
301 return $ innerFrValues ++ innerToValues ++ [(s, ConstantInt TagInt functionSize)]
302 )
303 mkFiniteOutermost (DomainRelation () attr@(RelationAttr SizeAttr_Size{} _) inners) = do
304 (inners', innersExtras, innersF) <- unzip3 <$> mapM mkFiniteInner inners
305 return
306 ( DomainRelation () attr inners'
307 , concat innersExtras
308 , \ constant -> do
309 logDebug $ "mkFiniteOutermost DomainRelation" <+> pretty constant
310 relation <- failToUserError $ viewConstantRelation constant
311 innersValues <- zipWithM ($) innersF (transpose relation)
312 return (concat innersValues)
313 )
314 mkFiniteOutermost (DomainRelation () (RelationAttr _ binRelAttr) inners) = do
315 s <- nextName "fin"
316 (inners', innersExtras, innersF) <- unzip3 <$> mapM mkFiniteInner inners
317 return
318 ( DomainRelation ()
319 (RelationAttr (SizeAttr_Size (fromName s)) binRelAttr)
320 inners'
321 , s : concat innersExtras
322 , \ constant -> do
323 logDebug $ "mkFiniteOutermost DomainRelation" <+> pretty constant
324 relation <- failToUserError $ viewConstantRelation constant
325 let relationSize = genericLength relation
326 innersValues <- zipWithM ($) innersF (transpose relation)
327 return $ concat innersValues ++ [(s, ConstantInt TagInt relationSize)]
328 )
329 mkFiniteOutermost (DomainPartition () attr@(PartitionAttr SizeAttr_Size{} SizeAttr_Size{} _) inner) = do
330 (inner', innerExtras, innerF) <- mkFiniteInner inner
331 return
332 ( DomainPartition () attr inner'
333 , innerExtras
334 , \ constant -> do
335 logDebug $ "mkFiniteOutermost DomainPartition" <+> pretty constant
336 parts <- failToUserError $ viewConstantPartition constant
337 innerValues <- mapM innerF parts
338 return (concat innerValues)
339 )
340 mkFiniteOutermost (DomainPartition () (PartitionAttr _ _ isRegularAttr) inner) = do
341 numPartsFin <- nextName "fin"
342 partsSizeFin <- nextName "fin"
343 (inner', innerExtras, innerF) <- mkFiniteInner inner
344 return
345 ( DomainPartition ()
346 (PartitionAttr (SizeAttr_Size (fromName numPartsFin))
347 (SizeAttr_MaxSize (fromName partsSizeFin))
348 isRegularAttr)
349 inner'
350 , numPartsFin:partsSizeFin:innerExtras
351 , \ constant -> do
352 logDebug $ "mkFiniteOutermost DomainPartition" <+> pretty constant
353 parts <- failToUserError $ viewConstantPartition constant
354 let numPartsVal = genericLength parts
355 let partsSizeVal = maximum0 $ map genericLength parts
356 innerValues <- mapM innerF parts
357 return $ concat innerValues ++ [ (numPartsFin, ConstantInt TagInt numPartsVal)
358 , (partsSizeFin, ConstantInt TagInt partsSizeVal)
359 ]
360 )
361 mkFiniteOutermost d = return (d, [], const (return []))
362
363
364 -- TODO add permutation support
365 mkFiniteInner ::
366 MonadFailDoc m =>
367 MonadState Int m =>
368 NameGen m =>
369 MonadLog m =>
370 MonadUserError m =>
371 EnumerateDomain m =>
372 (?typeCheckerMode :: TypeCheckerMode) =>
373 Domain () Expression ->
374 m ( Domain () Expression
375 , [Name]
376 , [Constant] -> m [(Name, Constant)]
377 )
378 mkFiniteInner (DomainInt t []) = do
379 fr <- nextName "fin"
380 to <- nextName "fin"
381 return
382 ( DomainInt t [RangeBounded (fromName fr) (fromName to)]
383 , [fr, to]
384 , \ constants -> do
385 logDebug $ "mkFiniteInner DomainInt 1" <+-> fsep (map pretty constants)
386 ints <- failToUserError $ mapM viewConstantInt constants
387 return [ (fr, ConstantInt t (minimum0 ints))
388 , (to, ConstantInt t (maximum0 ints))
389 ]
390 )
391 mkFiniteInner (DomainInt t [RangeLowerBounded low]) = do
392 new <- nextName "fin"
393 return
394 ( DomainInt t [RangeBounded low (fromName new)]
395 , [new]
396 , \ constants -> do
397 logDebug $ "mkFiniteInner DomainInt 2" <+-> fsep (map pretty constants)
398 ints <- failToUserError $ mapM viewConstantInt constants
399 return [ (new, ConstantInt t (maximum0 ints)) ]
400 )
401 mkFiniteInner (DomainInt t [RangeUpperBounded upp]) = do
402 new <- nextName "fin"
403 return
404 ( DomainInt t [RangeBounded (fromName new) upp]
405 , [new]
406 , \ constants -> do
407 logDebug $ "mkFiniteInner DomainInt 3" <+-> fsep (map pretty constants)
408 ints <- failToUserError $ mapM viewConstantInt constants
409 return [ (new, ConstantInt t (minimum0 ints)) ]
410 )
411 mkFiniteInner (DomainTuple inners) = do
412 mids <- mapM mkFiniteInner inners
413 return
414 ( DomainTuple (map fst3 mids)
415 , concatMap snd3 mids
416 , \ constants -> do
417 logDebug $ "mkFiniteInner DomainTuple" <+-> vcat (map pretty constants)
418 xss <- failToUserError $ mapM viewConstantTuple constants
419 let innerFs = map thd3 mids
420 innerValues <- sequence [ innerF xs | (innerF, xs) <- zip innerFs (transpose xss) ]
421 return (concat innerValues)
422 )
423 mkFiniteInner (DomainRecord (sortOn fst -> inners)) = do
424 mids <- mapM (mkFiniteInner . snd) inners
425 return
426 ( DomainRecord (zip (map fst inners) (map fst3 mids))
427 , concatMap snd3 mids
428 , \ constants -> do
429 logDebug $ "mkFiniteInner DomainRecord" <+-> vcat (map pretty constants)
430 xss' :: [[(Name, Constant)]] <- failToUserError $ mapM viewConstantRecord constants
431 let
432 xss :: [[Constant]]
433 xss = map (map snd . sortOn fst) xss'
434 let innerFs = map thd3 mids
435 innerValues <- sequence [ innerF xs | (innerF, xs) <- zip innerFs (transpose xss) ]
436 return (concat innerValues)
437 )
438 mkFiniteInner (DomainVariant inners) = do
439 mids <- mapM (mkFiniteInner . snd) inners
440 return
441 ( DomainVariant (zip (map fst inners) (map fst3 mids))
442 , concatMap snd3 mids
443 , \ constants -> do
444 logDebug $ "mkFiniteInner DomainVariant" <+-> vcat (map pretty constants)
445 xss' <- failToUserError $ mapM viewConstantVariant constants
446 xss :: [[Constant]]
447 <- sequence
448 [ sequence
449 [ case xs' of
450 (_, nm', c') | nm == nm' -> return c'
451 _ -> failToUserError $ instantiateDomain [] d >>= zeroVal
452 | (nm, d) <- inners ]
453 | xs' <- xss' ]
454 let innerFs = map thd3 mids
455 innerValues <- sequence [ innerF xs | (innerF, xs) <- zip innerFs (transpose xss) ]
456 return (concat innerValues)
457 )
458 mkFiniteInner (DomainMatrix index inner) = do
459 (inner', innerExtras, innerF) <- mkFiniteInner inner
460 return
461 ( DomainMatrix index inner'
462 , innerExtras
463 , \ constants -> do
464 logDebug $ "mkFiniteInner DomainMatrix" <+-> vcat (map pretty constants)
465 xss <- failToUserError $ mapM viewConstantMatrix constants
466 innerF (concatMap snd xss)
467 )
468 mkFiniteInner (DomainSet () attr@(SetAttr SizeAttr_Size{}) inner) = do
469 (inner', innerExtras, innerF) <- mkFiniteInner inner
470 return
471 ( DomainSet () attr inner'
472 , innerExtras
473 , \ constants -> do
474 logDebug $ "mkFiniteInner DomainSet" <+-> vcat (map pretty constants)
475 sets <- failToUserError $ mapM viewConstantSet constants
476 innerF (concat sets)
477 )
478 mkFiniteInner (DomainSet () _ inner) = do
479 s <- nextName "fin"
480 (inner', innerExtras, innerF) <- mkFiniteInner inner
481 return
482 ( DomainSet () (SetAttr (SizeAttr_MaxSize (fromName s))) inner'
483 , s:innerExtras
484 , \ constants -> do
485 logDebug $ "mkFiniteInner DomainSet" <+-> vcat (map pretty constants)
486 sets <- failToUserError $ mapM viewConstantSet constants
487 let setMaxSize = maximum0 $ map genericLength sets
488 innerValues <- innerF (concat sets)
489 return $ innerValues ++ [(s, ConstantInt TagInt setMaxSize)]
490 )
491 mkFiniteInner (DomainMSet () attr@(MSetAttr SizeAttr_Size{} _) inner) = do
492 (inner', innerExtras, innerF) <- mkFiniteInner inner
493 return
494 ( DomainMSet () attr inner'
495 , innerExtras
496 , \ constants -> do
497 logDebug $ "mkFiniteInner DomainMSet" <+-> vcat (map pretty constants)
498 sets <- failToUserError $ mapM viewConstantMSet constants
499 innerF (concat sets)
500 )
501 mkFiniteInner (DomainMSet () (MSetAttr _ occurAttr) inner) = do
502 s <- nextName "fin"
503 (inner', innerExtras, innerF) <- mkFiniteInner inner
504 return
505 ( DomainMSet () (MSetAttr (SizeAttr_MaxSize (fromName s)) occurAttr) inner'
506 , s:innerExtras
507 , \ constants -> do
508 logDebug $ "mkFiniteInner DomainMSet" <+-> vcat (map pretty constants)
509 sets <- failToUserError $ mapM viewConstantMSet constants
510 let setMaxSize = maximum0 $ map genericLength sets
511 innerValues <- innerF (concat sets)
512 return $ innerValues ++ [(s, ConstantInt TagInt setMaxSize)]
513 )
514 mkFiniteInner (DomainSequence () attr@(SequenceAttr SizeAttr_Size{} _) inner) = do
515 (inner', innerExtras, innerF) <- mkFiniteInner inner
516 return
517 ( DomainSequence () attr inner'
518 , innerExtras
519 , \ constants -> do
520 logDebug $ "mkFiniteInner DomainSequence" <+-> vcat (map pretty constants)
521 seqs <- failToUserError $ mapM viewConstantSequence constants
522 innerF (concat seqs)
523 )
524 mkFiniteInner (DomainSequence () (SequenceAttr _ jectivityAttr) inner) = do
525 s <- nextName "fin"
526 (inner', innerExtras, innerF) <- mkFiniteInner inner
527 return
528 ( DomainSequence () (SequenceAttr (SizeAttr_MaxSize (fromName s)) jectivityAttr) inner'
529 , s:innerExtras
530 , \ constants -> do
531 logDebug $ "mkFiniteInner DomainSequence" <+-> vcat (map pretty constants)
532 seqs <- failToUserError $ mapM viewConstantSequence constants
533 let seqMaxSize = maximum0 $ map genericLength seqs
534 innerValues <- innerF (concat seqs)
535 return $ innerValues ++ [(s, ConstantInt TagInt seqMaxSize)]
536 )
537 mkFiniteInner (DomainFunction () attr@(FunctionAttr SizeAttr_Size{} _ _) innerFr innerTo) = do
538 (innerFr', innerFrExtras, innerFrF) <- mkFiniteInner innerFr
539 (innerTo', innerToExtras, innerToF) <- mkFiniteInner innerTo
540 return
541 ( DomainFunction () attr innerFr' innerTo'
542 , innerFrExtras ++ innerToExtras
543 , \ constants -> do
544 logDebug $ "mkFiniteInner DomainFunction" <+-> vcat (map pretty constants)
545 functions <- failToUserError $ mapM viewConstantFunction constants
546 innerFrValues <- innerFrF (map fst (concat functions))
547 innerToValues <- innerToF (map snd (concat functions))
548 return $ innerFrValues ++ innerToValues
549 )
550 mkFiniteInner (DomainFunction () (FunctionAttr _ partialityAttr jectivityAttr) innerFr innerTo) = do
551 s <- nextName "fin"
552 (innerFr', innerFrExtras, innerFrF) <- mkFiniteInner innerFr
553 (innerTo', innerToExtras, innerToF) <- mkFiniteInner innerTo
554 return
555 ( DomainFunction ()
556 (FunctionAttr (SizeAttr_MaxSize (fromName s)) partialityAttr jectivityAttr)
557 innerFr' innerTo'
558 , s : innerFrExtras ++ innerToExtras
559 , \ constants -> do
560 logDebug $ "mkFiniteInner DomainFunction" <+-> vcat (map pretty constants)
561 functions <- failToUserError $ mapM viewConstantFunction constants
562 let functionMaxSize = maximum0 $ map genericLength functions
563 innerFrValues <- innerFrF (map fst (concat functions))
564 innerToValues <- innerToF (map snd (concat functions))
565 return $ innerFrValues ++ innerToValues ++ [(s, ConstantInt TagInt functionMaxSize)]
566 )
567 mkFiniteInner (DomainRelation () attr@(RelationAttr SizeAttr_Size{} _) inners) = do
568 (inners', innersExtras, innersF) <- unzip3 <$> mapM mkFiniteInner inners
569 return
570 ( DomainRelation () attr inners'
571 , concat innersExtras
572 , \ constants -> do
573 logDebug $ "mkFiniteInner DomainRelation" <+-> vcat (map pretty constants)
574 relations <- failToUserError $ mapM viewConstantRelation constants
575 innersValues <- zipWithM ($) innersF (transpose $ concat relations)
576 return $ concat innersValues
577 )
578 mkFiniteInner (DomainRelation () (RelationAttr _ binRelAttr) inners) = do
579 s <- nextName "fin"
580 (inners', innersExtras, innersF) <- unzip3 <$> mapM mkFiniteInner inners
581 return
582 ( DomainRelation ()
583 (RelationAttr (SizeAttr_MaxSize (fromName s)) binRelAttr)
584 inners'
585 , s : concat innersExtras
586 , \ constants -> do
587 logDebug $ "mkFiniteInner DomainRelation" <+> vcat (map pretty constants)
588 relations <- failToUserError $ mapM viewConstantRelation constants
589 let relationMaxSize = maximum0 $ map genericLength relations
590 innersValues <- zipWithM ($) innersF (transpose $ concat relations)
591 return $ concat innersValues ++ [(s, ConstantInt TagInt relationMaxSize)]
592 )
593 mkFiniteInner (DomainPartition () attr@(PartitionAttr SizeAttr_Size{} SizeAttr_Size{} _) inner) = do
594 (inner', innerExtras, innerF) <- mkFiniteInner inner
595 return
596 ( DomainPartition () attr inner'
597 , innerExtras
598 , \ constants -> do
599 logDebug $ "mkFiniteInner DomainPartition" <+> vcat (map pretty constants)
600 parts <- failToUserError $ mapM viewConstantPartition constants
601 innersValues <- mapM innerF (concat parts)
602 return $ concat innersValues
603 )
604 mkFiniteInner (DomainPartition () (PartitionAttr _ _ isRegularAttr) inner) = do
605 numPartsFin <- nextName "fin"
606 partsSizeFin <- nextName "fin"
607 (inner', innerExtras, innerF) <- mkFiniteInner inner
608 return
609 ( DomainPartition ()
610 (PartitionAttr (SizeAttr_MaxSize (fromName numPartsFin))
611 (SizeAttr_MaxSize (fromName partsSizeFin))
612 isRegularAttr)
613 inner'
614 , numPartsFin:partsSizeFin:innerExtras
615 , \ constants -> do
616 logDebug $ "mkFiniteInner DomainPartition" <+> vcat (map pretty constants)
617 parts <- failToUserError $ mapM viewConstantPartition constants
618 let numPartsVal = maximum0 $ map genericLength parts
619 let partsSizeVal = maximum0 $ map genericLength parts
620 innerValues <- mapM innerF (concat parts)
621 return $ concat innerValues ++ [ (numPartsFin, ConstantInt TagInt numPartsVal)
622 , (partsSizeFin, ConstantInt TagInt partsSizeVal)
623 ]
624 )
625 mkFiniteInner d = return (d, [], const (return []))
626
627
628 -- specialised the type for minimum0 and maximum0, to avoid possible bugs
629 -- this function is always intended to be used with Integers
630 minimum0 :: [Integer] -> Integer
631 minimum0 [] = 0
632 minimum0 xs = minimum xs
633
634 maximum0 :: [Integer] -> Integer
635 maximum0 [] = 0
636 maximum0 xs = maximum xs