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@DomainFunction{} = mkFiniteOutermost d
126 mkFinite d@DomainRelation{} = mkFiniteOutermost d
127 mkFinite d@DomainPartition{} = mkFiniteOutermost d
128 mkFinite d = return (d, [], const (return []))
129
130
131 mkFiniteOutermost ::
132 MonadFailDoc m =>
133 MonadState Int m =>
134 NameGen m =>
135 MonadLog m =>
136 MonadUserError m =>
137 EnumerateDomain m =>
138 (?typeCheckerMode :: TypeCheckerMode) =>
139 Domain () Expression ->
140 m ( Domain () Expression
141 , [Name]
142 , Constant -> m [(Name, Constant)]
143 )
144 mkFiniteOutermost (DomainTuple inners) = do
145 mids <- mapM mkFiniteInner inners
146 return
147 ( DomainTuple (map fst3 mids)
148 , concatMap snd3 mids
149 , \ constant -> do
150 logDebug $ "mkFiniteOutermost DomainTuple" <+> pretty constant
151 xs <- failToUserError $ viewConstantTuple constant
152 let innerFs = map thd3 mids
153 innerValues <- sequence [ innerF [x] | (innerF, x) <- zip innerFs xs ]
154 return (concat innerValues)
155 )
156 mkFiniteOutermost (DomainRecord (sortOn fst -> inners)) = do
157 mids <- mapM (mkFiniteInner . snd) inners
158 return
159 ( DomainRecord (zip (map fst inners) (map fst3 mids))
160 , concatMap snd3 mids
161 , \ constant -> do
162 logDebug $ "mkFiniteOutermost DomainRecord" <+> pretty constant
163 xs' <- failToUserError $ viewConstantRecord constant
164 let
165 xs :: [Constant]
166 xs = map snd $ sortOn fst xs'
167 let innerFs = map thd3 mids
168 innerValues <- sequence [ innerF [x] | (innerF, x) <- zip innerFs xs ]
169 return (concat innerValues)
170 )
171 mkFiniteOutermost (DomainVariant inners) = do
172 mids <- mapM (mkFiniteInner . snd) inners
173 return
174 ( DomainVariant (zip (map fst inners) (map fst3 mids))
175 , concatMap snd3 mids
176 , \ constant -> do
177 logDebug $ "mkFiniteOutermost DomainVariant" <+> pretty constant
178 xs' <- failToUserError $ viewConstantVariant constant
179 xs :: [Constant] <- sequence
180 [ case xs' of
181 (_, nm', c') | nm == nm' -> return c'
182 _ -> failToUserError $ instantiateDomain [] d >>= zeroVal
183 | (nm, d) <- inners ]
184 let innerFs = map thd3 mids
185 innerValues <- sequence [ innerF [x] | (innerF, x) <- zip innerFs xs ]
186 return (concat innerValues)
187 )
188 mkFiniteOutermost (DomainMatrix index inner) = do
189 (inner', innerExtras, innerF) <- mkFiniteInner inner
190 return
191 ( DomainMatrix index inner'
192 , innerExtras
193 , \ constant -> do
194 logDebug $ "mkFiniteOutermost DomainMatrix" <+> pretty constant
195 (_, matr) <- failToUserError $ viewConstantMatrix constant
196 innerValues <- innerF matr
197 return innerValues
198 )
199 mkFiniteOutermost (DomainSet () attr@(SetAttr SizeAttr_Size{}) inner) = do
200 (inner', innerExtras, innerF) <- mkFiniteInner inner
201 return
202 ( DomainSet () attr inner'
203 , innerExtras
204 , \ constant -> do
205 logDebug $ "mkFiniteOutermost DomainSet" <+> pretty constant
206 set <- failToUserError $ viewConstantSet constant
207 innerValues <- innerF set
208 return innerValues
209 )
210 mkFiniteOutermost (DomainSet () _ inner) = do
211 s <- nextName "fin"
212 (inner', innerExtras, innerF) <- mkFiniteInner inner
213 return
214 ( DomainSet () (SetAttr (SizeAttr_Size (fromName s))) inner'
215 , s:innerExtras
216 , \ constant -> do
217 logDebug $ "mkFiniteOutermost DomainSet" <+> pretty constant
218 set <- failToUserError $ viewConstantSet constant
219 let setSize = genericLength set
220 innerValues <- innerF set
221 return $ innerValues ++ [(s, ConstantInt TagInt setSize)]
222 )
223 mkFiniteOutermost (DomainMSet () attr@(MSetAttr SizeAttr_Size{} _) inner) = do
224 (inner', innerExtras, innerF) <- mkFiniteInner inner
225 return
226 ( DomainMSet () attr inner'
227 , innerExtras
228 , \ constant -> do
229 logDebug $ "mkFiniteOutermost DomainMSet" <+> pretty constant
230 set <- failToUserError $ viewConstantMSet constant
231 innerValues <- innerF set
232 return innerValues
233 )
234 mkFiniteOutermost (DomainMSet () (MSetAttr _ occurAttr) inner) = do
235 s <- nextName "fin"
236 (inner', innerExtras, innerF) <- mkFiniteInner inner
237 return
238 ( DomainMSet () (MSetAttr (SizeAttr_Size (fromName s)) occurAttr) inner'
239 , s:innerExtras
240 , \ constant -> do
241 logDebug $ "mkFiniteOutermost DomainMSet" <+> pretty constant
242 set <- failToUserError $ viewConstantMSet constant
243 let setSize = genericLength set
244 innerValues <- innerF set
245 return $ innerValues ++ [(s, ConstantInt TagInt setSize)]
246 )
247 mkFiniteOutermost (DomainSequence () attr@(SequenceAttr SizeAttr_Size{} _) inner) = do
248 (inner', innerExtras, innerF) <- mkFiniteInner inner
249 return
250 ( DomainSequence () attr inner'
251 , innerExtras
252 , \ constant -> do
253 logDebug $ "mkFiniteOutermost DomainSequence" <+> pretty constant
254 set <- failToUserError $ viewConstantSequence constant
255 innerValues <- innerF set
256 return innerValues
257 )
258 mkFiniteOutermost (DomainSequence () (SequenceAttr _ jectivityAttr) inner) = do
259 s <- nextName "fin"
260 (inner', innerExtras, innerF) <- mkFiniteInner inner
261 return
262 ( DomainSequence () (SequenceAttr (SizeAttr_Size (fromName s)) jectivityAttr) inner'
263 , s:innerExtras
264 , \ constant -> do
265 logDebug $ "mkFiniteOutermost DomainSequence" <+> pretty constant
266 set <- failToUserError $ viewConstantSequence constant
267 let setSize = genericLength set
268 innerValues <- innerF set
269 return $ innerValues ++ [(s, ConstantInt TagInt setSize)]
270 )
271 mkFiniteOutermost (DomainFunction () attr@(FunctionAttr SizeAttr_Size{} _ _) innerFr innerTo) = do
272 (innerFr', innerFrExtras, innerFrF) <- mkFiniteInner innerFr
273 (innerTo', innerToExtras, innerToF) <- mkFiniteInner innerTo
274 return
275 ( DomainFunction () attr innerFr' innerTo'
276 , innerFrExtras ++ innerToExtras
277 , \ constant -> do
278 logDebug $ "mkFiniteOutermost DomainFunction" <+-> pretty constant
279 function <- failToUserError $ viewConstantFunction constant
280 innerFrValues <- innerFrF (map fst function)
281 innerToValues <- innerToF (map snd function)
282 return $ innerFrValues ++ innerToValues
283 )
284 mkFiniteOutermost (DomainFunction () (FunctionAttr _ partialityAttr jectivityAttr) innerFr innerTo) = do
285 s <- nextName "fin"
286 (innerFr', innerFrExtras, innerFrF) <- mkFiniteInner innerFr
287 (innerTo', innerToExtras, innerToF) <- mkFiniteInner innerTo
288 return
289 ( DomainFunction ()
290 (FunctionAttr (SizeAttr_Size (fromName s)) partialityAttr jectivityAttr)
291 innerFr' innerTo'
292 , s : innerFrExtras ++ innerToExtras
293 , \ constant -> do
294 logDebug $ "mkFiniteOutermost DomainFunction" <+-> pretty constant
295 function <- failToUserError $ viewConstantFunction constant
296 let functionSize = genericLength function
297 innerFrValues <- innerFrF (map fst function)
298 innerToValues <- innerToF (map snd function)
299 return $ innerFrValues ++ innerToValues ++ [(s, ConstantInt TagInt functionSize)]
300 )
301 mkFiniteOutermost (DomainRelation () attr@(RelationAttr SizeAttr_Size{} _) inners) = do
302 (inners', innersExtras, innersF) <- unzip3 <$> mapM mkFiniteInner inners
303 return
304 ( DomainRelation () attr inners'
305 , concat innersExtras
306 , \ constant -> do
307 logDebug $ "mkFiniteOutermost DomainRelation" <+> pretty constant
308 relation <- failToUserError $ viewConstantRelation constant
309 innersValues <- zipWithM ($) innersF (transpose relation)
310 return (concat innersValues)
311 )
312 mkFiniteOutermost (DomainRelation () (RelationAttr _ binRelAttr) inners) = do
313 s <- nextName "fin"
314 (inners', innersExtras, innersF) <- unzip3 <$> mapM mkFiniteInner inners
315 return
316 ( DomainRelation ()
317 (RelationAttr (SizeAttr_Size (fromName s)) binRelAttr)
318 inners'
319 , s : concat innersExtras
320 , \ constant -> do
321 logDebug $ "mkFiniteOutermost DomainRelation" <+> pretty constant
322 relation <- failToUserError $ viewConstantRelation constant
323 let relationSize = genericLength relation
324 innersValues <- zipWithM ($) innersF (transpose relation)
325 return $ concat innersValues ++ [(s, ConstantInt TagInt relationSize)]
326 )
327 mkFiniteOutermost (DomainPartition () attr@(PartitionAttr SizeAttr_Size{} SizeAttr_Size{} _) inner) = do
328 (inner', innerExtras, innerF) <- mkFiniteInner inner
329 return
330 ( DomainPartition () attr inner'
331 , innerExtras
332 , \ constant -> do
333 logDebug $ "mkFiniteOutermost DomainPartition" <+> pretty constant
334 parts <- failToUserError $ viewConstantPartition constant
335 innerValues <- mapM innerF parts
336 return (concat innerValues)
337 )
338 mkFiniteOutermost (DomainPartition () (PartitionAttr _ _ isRegularAttr) inner) = do
339 numPartsFin <- nextName "fin"
340 partsSizeFin <- nextName "fin"
341 (inner', innerExtras, innerF) <- mkFiniteInner inner
342 return
343 ( DomainPartition ()
344 (PartitionAttr (SizeAttr_Size (fromName numPartsFin))
345 (SizeAttr_MaxSize (fromName partsSizeFin))
346 isRegularAttr)
347 inner'
348 , numPartsFin:partsSizeFin:innerExtras
349 , \ constant -> do
350 logDebug $ "mkFiniteOutermost DomainPartition" <+> pretty constant
351 parts <- failToUserError $ viewConstantPartition constant
352 let numPartsVal = genericLength parts
353 let partsSizeVal = maximum0 $ map genericLength parts
354 innerValues <- mapM innerF parts
355 return $ concat innerValues ++ [ (numPartsFin, ConstantInt TagInt numPartsVal)
356 , (partsSizeFin, ConstantInt TagInt partsSizeVal)
357 ]
358 )
359 mkFiniteOutermost d = return (d, [], const (return []))
360
361
362 mkFiniteInner ::
363 MonadFailDoc m =>
364 MonadState Int m =>
365 NameGen m =>
366 MonadLog m =>
367 MonadUserError m =>
368 EnumerateDomain m =>
369 (?typeCheckerMode :: TypeCheckerMode) =>
370 Domain () Expression ->
371 m ( Domain () Expression
372 , [Name]
373 , [Constant] -> m [(Name, Constant)]
374 )
375 mkFiniteInner (DomainInt t []) = do
376 fr <- nextName "fin"
377 to <- nextName "fin"
378 return
379 ( DomainInt t [RangeBounded (fromName fr) (fromName to)]
380 , [fr, to]
381 , \ constants -> do
382 logDebug $ "mkFiniteInner DomainInt 1" <+-> fsep (map pretty constants)
383 ints <- failToUserError $ mapM viewConstantInt constants
384 return [ (fr, ConstantInt t (minimum0 ints))
385 , (to, ConstantInt t (maximum0 ints))
386 ]
387 )
388 mkFiniteInner (DomainInt t [RangeLowerBounded low]) = do
389 new <- nextName "fin"
390 return
391 ( DomainInt t [RangeBounded low (fromName new)]
392 , [new]
393 , \ constants -> do
394 logDebug $ "mkFiniteInner DomainInt 2" <+-> fsep (map pretty constants)
395 ints <- failToUserError $ mapM viewConstantInt constants
396 return [ (new, ConstantInt t (maximum0 ints)) ]
397 )
398 mkFiniteInner (DomainInt t [RangeUpperBounded upp]) = do
399 new <- nextName "fin"
400 return
401 ( DomainInt t [RangeBounded (fromName new) upp]
402 , [new]
403 , \ constants -> do
404 logDebug $ "mkFiniteInner DomainInt 3" <+-> fsep (map pretty constants)
405 ints <- failToUserError $ mapM viewConstantInt constants
406 return [ (new, ConstantInt t (minimum0 ints)) ]
407 )
408 mkFiniteInner (DomainTuple inners) = do
409 mids <- mapM mkFiniteInner inners
410 return
411 ( DomainTuple (map fst3 mids)
412 , concatMap snd3 mids
413 , \ constants -> do
414 logDebug $ "mkFiniteInner DomainTuple" <+-> vcat (map pretty constants)
415 xss <- failToUserError $ mapM viewConstantTuple constants
416 let innerFs = map thd3 mids
417 innerValues <- sequence [ innerF xs | (innerF, xs) <- zip innerFs (transpose xss) ]
418 return (concat innerValues)
419 )
420 mkFiniteInner (DomainRecord (sortOn fst -> inners)) = do
421 mids <- mapM (mkFiniteInner . snd) inners
422 return
423 ( DomainRecord (zip (map fst inners) (map fst3 mids))
424 , concatMap snd3 mids
425 , \ constants -> do
426 logDebug $ "mkFiniteInner DomainRecord" <+-> vcat (map pretty constants)
427 xss' :: [[(Name, Constant)]] <- failToUserError $ mapM viewConstantRecord constants
428 let
429 xss :: [[Constant]]
430 xss = map (map snd . sortOn fst) xss'
431 let innerFs = map thd3 mids
432 innerValues <- sequence [ innerF xs | (innerF, xs) <- zip innerFs (transpose xss) ]
433 return (concat innerValues)
434 )
435 mkFiniteInner (DomainVariant inners) = do
436 mids <- mapM (mkFiniteInner . snd) inners
437 return
438 ( DomainVariant (zip (map fst inners) (map fst3 mids))
439 , concatMap snd3 mids
440 , \ constants -> do
441 logDebug $ "mkFiniteInner DomainVariant" <+-> vcat (map pretty constants)
442 xss' <- failToUserError $ mapM viewConstantVariant constants
443 xss :: [[Constant]]
444 <- sequence
445 [ sequence
446 [ case xs' of
447 (_, nm', c') | nm == nm' -> return c'
448 _ -> failToUserError $ instantiateDomain [] d >>= zeroVal
449 | (nm, d) <- inners ]
450 | xs' <- xss' ]
451 let innerFs = map thd3 mids
452 innerValues <- sequence [ innerF xs | (innerF, xs) <- zip innerFs (transpose xss) ]
453 return (concat innerValues)
454 )
455 mkFiniteInner (DomainMatrix index inner) = do
456 (inner', innerExtras, innerF) <- mkFiniteInner inner
457 return
458 ( DomainMatrix index inner'
459 , innerExtras
460 , \ constants -> do
461 logDebug $ "mkFiniteInner DomainMatrix" <+-> vcat (map pretty constants)
462 xss <- failToUserError $ mapM viewConstantMatrix constants
463 innerF (concatMap snd xss)
464 )
465 mkFiniteInner (DomainSet () attr@(SetAttr SizeAttr_Size{}) inner) = do
466 (inner', innerExtras, innerF) <- mkFiniteInner inner
467 return
468 ( DomainSet () attr inner'
469 , innerExtras
470 , \ constants -> do
471 logDebug $ "mkFiniteInner DomainSet" <+-> vcat (map pretty constants)
472 sets <- failToUserError $ mapM viewConstantSet constants
473 innerF (concat sets)
474 )
475 mkFiniteInner (DomainSet () _ inner) = do
476 s <- nextName "fin"
477 (inner', innerExtras, innerF) <- mkFiniteInner inner
478 return
479 ( DomainSet () (SetAttr (SizeAttr_MaxSize (fromName s))) inner'
480 , s:innerExtras
481 , \ constants -> do
482 logDebug $ "mkFiniteInner DomainSet" <+-> vcat (map pretty constants)
483 sets <- failToUserError $ mapM viewConstantSet constants
484 let setMaxSize = maximum0 $ map genericLength sets
485 innerValues <- innerF (concat sets)
486 return $ innerValues ++ [(s, ConstantInt TagInt setMaxSize)]
487 )
488 mkFiniteInner (DomainMSet () attr@(MSetAttr SizeAttr_Size{} _) inner) = do
489 (inner', innerExtras, innerF) <- mkFiniteInner inner
490 return
491 ( DomainMSet () attr inner'
492 , innerExtras
493 , \ constants -> do
494 logDebug $ "mkFiniteInner DomainMSet" <+-> vcat (map pretty constants)
495 sets <- failToUserError $ mapM viewConstantMSet constants
496 innerF (concat sets)
497 )
498 mkFiniteInner (DomainMSet () (MSetAttr _ occurAttr) inner) = do
499 s <- nextName "fin"
500 (inner', innerExtras, innerF) <- mkFiniteInner inner
501 return
502 ( DomainMSet () (MSetAttr (SizeAttr_MaxSize (fromName s)) occurAttr) inner'
503 , s:innerExtras
504 , \ constants -> do
505 logDebug $ "mkFiniteInner DomainMSet" <+-> vcat (map pretty constants)
506 sets <- failToUserError $ mapM viewConstantMSet constants
507 let setMaxSize = maximum0 $ map genericLength sets
508 innerValues <- innerF (concat sets)
509 return $ innerValues ++ [(s, ConstantInt TagInt setMaxSize)]
510 )
511 mkFiniteInner (DomainSequence () attr@(SequenceAttr SizeAttr_Size{} _) inner) = do
512 (inner', innerExtras, innerF) <- mkFiniteInner inner
513 return
514 ( DomainSequence () attr inner'
515 , innerExtras
516 , \ constants -> do
517 logDebug $ "mkFiniteInner DomainSequence" <+-> vcat (map pretty constants)
518 seqs <- failToUserError $ mapM viewConstantSequence constants
519 innerF (concat seqs)
520 )
521 mkFiniteInner (DomainSequence () (SequenceAttr _ jectivityAttr) inner) = do
522 s <- nextName "fin"
523 (inner', innerExtras, innerF) <- mkFiniteInner inner
524 return
525 ( DomainSequence () (SequenceAttr (SizeAttr_MaxSize (fromName s)) jectivityAttr) inner'
526 , s:innerExtras
527 , \ constants -> do
528 logDebug $ "mkFiniteInner DomainSequence" <+-> vcat (map pretty constants)
529 seqs <- failToUserError $ mapM viewConstantSequence constants
530 let seqMaxSize = maximum0 $ map genericLength seqs
531 innerValues <- innerF (concat seqs)
532 return $ innerValues ++ [(s, ConstantInt TagInt seqMaxSize)]
533 )
534 mkFiniteInner (DomainFunction () attr@(FunctionAttr SizeAttr_Size{} _ _) innerFr innerTo) = do
535 (innerFr', innerFrExtras, innerFrF) <- mkFiniteInner innerFr
536 (innerTo', innerToExtras, innerToF) <- mkFiniteInner innerTo
537 return
538 ( DomainFunction () attr innerFr' innerTo'
539 , innerFrExtras ++ innerToExtras
540 , \ constants -> do
541 logDebug $ "mkFiniteInner DomainFunction" <+-> vcat (map pretty constants)
542 functions <- failToUserError $ mapM viewConstantFunction constants
543 innerFrValues <- innerFrF (map fst (concat functions))
544 innerToValues <- innerToF (map snd (concat functions))
545 return $ innerFrValues ++ innerToValues
546 )
547 mkFiniteInner (DomainFunction () (FunctionAttr _ partialityAttr jectivityAttr) innerFr innerTo) = do
548 s <- nextName "fin"
549 (innerFr', innerFrExtras, innerFrF) <- mkFiniteInner innerFr
550 (innerTo', innerToExtras, innerToF) <- mkFiniteInner innerTo
551 return
552 ( DomainFunction ()
553 (FunctionAttr (SizeAttr_MaxSize (fromName s)) partialityAttr jectivityAttr)
554 innerFr' innerTo'
555 , s : innerFrExtras ++ innerToExtras
556 , \ constants -> do
557 logDebug $ "mkFiniteInner DomainFunction" <+-> vcat (map pretty constants)
558 functions <- failToUserError $ mapM viewConstantFunction constants
559 let functionMaxSize = maximum0 $ map genericLength functions
560 innerFrValues <- innerFrF (map fst (concat functions))
561 innerToValues <- innerToF (map snd (concat functions))
562 return $ innerFrValues ++ innerToValues ++ [(s, ConstantInt TagInt functionMaxSize)]
563 )
564 mkFiniteInner (DomainRelation () attr@(RelationAttr SizeAttr_Size{} _) inners) = do
565 (inners', innersExtras, innersF) <- unzip3 <$> mapM mkFiniteInner inners
566 return
567 ( DomainRelation () attr inners'
568 , concat innersExtras
569 , \ constants -> do
570 logDebug $ "mkFiniteInner DomainRelation" <+-> vcat (map pretty constants)
571 relations <- failToUserError $ mapM viewConstantRelation constants
572 innersValues <- zipWithM ($) innersF (transpose $ concat relations)
573 return $ concat innersValues
574 )
575 mkFiniteInner (DomainRelation () (RelationAttr _ binRelAttr) inners) = do
576 s <- nextName "fin"
577 (inners', innersExtras, innersF) <- unzip3 <$> mapM mkFiniteInner inners
578 return
579 ( DomainRelation ()
580 (RelationAttr (SizeAttr_MaxSize (fromName s)) binRelAttr)
581 inners'
582 , s : concat innersExtras
583 , \ constants -> do
584 logDebug $ "mkFiniteInner DomainRelation" <+> vcat (map pretty constants)
585 relations <- failToUserError $ mapM viewConstantRelation constants
586 let relationMaxSize = maximum0 $ map genericLength relations
587 innersValues <- zipWithM ($) innersF (transpose $ concat relations)
588 return $ concat innersValues ++ [(s, ConstantInt TagInt relationMaxSize)]
589 )
590 mkFiniteInner (DomainPartition () attr@(PartitionAttr SizeAttr_Size{} SizeAttr_Size{} _) inner) = do
591 (inner', innerExtras, innerF) <- mkFiniteInner inner
592 return
593 ( DomainPartition () attr inner'
594 , innerExtras
595 , \ constants -> do
596 logDebug $ "mkFiniteInner DomainPartition" <+> vcat (map pretty constants)
597 parts <- failToUserError $ mapM viewConstantPartition constants
598 innersValues <- mapM innerF (concat parts)
599 return $ concat innersValues
600 )
601 mkFiniteInner (DomainPartition () (PartitionAttr _ _ isRegularAttr) inner) = do
602 numPartsFin <- nextName "fin"
603 partsSizeFin <- nextName "fin"
604 (inner', innerExtras, innerF) <- mkFiniteInner inner
605 return
606 ( DomainPartition ()
607 (PartitionAttr (SizeAttr_MaxSize (fromName numPartsFin))
608 (SizeAttr_MaxSize (fromName partsSizeFin))
609 isRegularAttr)
610 inner'
611 , numPartsFin:partsSizeFin:innerExtras
612 , \ constants -> do
613 logDebug $ "mkFiniteInner DomainPartition" <+> vcat (map pretty constants)
614 parts <- failToUserError $ mapM viewConstantPartition constants
615 let numPartsVal = maximum0 $ map genericLength parts
616 let partsSizeVal = maximum0 $ map genericLength parts
617 innerValues <- mapM innerF (concat parts)
618 return $ concat innerValues ++ [ (numPartsFin, ConstantInt TagInt numPartsVal)
619 , (partsSizeFin, ConstantInt TagInt partsSizeVal)
620 ]
621 )
622 mkFiniteInner d = return (d, [], const (return []))
623
624
625 -- specialised the type for minimum0 and maximum0, to avoid possible bugs
626 -- this function is always intended to be used with Integers
627 minimum0 :: [Integer] -> Integer
628 minimum0 [] = 0
629 minimum0 xs = minimum xs
630
631 maximum0 :: [Integer] -> Integer
632 maximum0 [] = 0
633 maximum0 xs = maximum xs