never executed always true always false
1 {-# LANGUAGE Rank2Types #-}
2 {-# LANGUAGE TupleSections #-}
3 {-# LANGUAGE QuasiQuotes #-}
4 {-# LANGUAGE RecordWildCards #-}
5 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
6 {-# HLINT ignore "Use camelCase" #-}
7
8 module Conjure.UI.Model
9 ( outputModels
10 , Strategy(..), Config(..), parseStrategy
11 , nbUses
12 , modelRepresentationsJSON
13 , timedF
14 , evaluateModel -- unused, exporting to suppress warning
15 , prologue
16 ) where
17
18 import Conjure.Prelude
19 import Conjure.Bug
20 import Conjure.UserError
21 import Conjure.Language.Definition
22 import Conjure.Language.Expression.Internal.Generated ()
23 import Conjure.Language.Domain
24 import Conjure.Language.Type
25 import Conjure.Language.Pretty
26 import Conjure.Language.CategoryOf
27 import Conjure.Language.TypeOf
28 import Conjure.Compute.DomainOf
29 import Conjure.Language.DomainSizeOf
30 import Conjure.Language.Lenses
31 import Conjure.Language.TH ( essence )
32 import Conjure.Language.Expression.Op
33 import Conjure.Language.ModelStats ( modelInfo )
34 import Conjure.Language.Instantiate ( instantiateExpression, trySimplify )
35 import Conjure.Process.Sanity ( sanityChecks )
36 import Conjure.Process.Enums ( removeEnumsFromModel )
37 import Conjure.Process.Unnameds ( removeUnnamedsFromModel )
38 import Conjure.Process.FiniteGivens ( finiteGivens )
39 import Conjure.Process.LettingsForComplexInDoms ( lettingsForComplexInDoms
40 , inlineLettingDomainsForDecls
41 , removeDomainLettings
42 )
43 import Conjure.Process.AttributeAsConstraints ( attributeAsConstraints, mkAttributeToConstraint )
44 import Conjure.Process.InferAttributes ( inferAttributes )
45 import Conjure.Process.DealWithCuts ( dealWithCuts )
46 import Conjure.Process.Enumerate ( EnumerateDomain )
47 import Conjure.Language.NameResolution ( resolveNames, resolveNamesX )
48 import Conjure.UI.TypeCheck ( typeCheckModel, typeCheckModel_StandAlone )
49 import Conjure.UI ( OutputFormat(..) )
50 import Conjure.UI.IO ( writeModel )
51 import Conjure.UI.NormaliseQuantified ( distinctQuantifiedVars
52 , renameQuantifiedVarsToAvoidShadowing
53 , normaliseQuantifiedVariables
54 , normaliseQuantifiedVariablesS
55 , normaliseQuantifiedVariablesE
56 )
57
58
59 import Conjure.Representations
60 ( downX, downX1, downD, reprOptions, getStructurals
61 , symmetryOrdering
62 , reprsStandardOrderNoLevels, reprsStandardOrder, reprsSparseOrder
63 )
64
65 import Conjure.Rules.Definition
66
67 import qualified Conjure.Rules.Vertical.Tuple as Vertical.Tuple
68 import qualified Conjure.Rules.Vertical.Record as Vertical.Record
69 import qualified Conjure.Rules.Vertical.Variant as Vertical.Variant
70 import qualified Conjure.Rules.Vertical.Matrix as Vertical.Matrix
71
72 import qualified Conjure.Rules.Horizontal.Set as Horizontal.Set
73 import qualified Conjure.Rules.Vertical.Set.Explicit as Vertical.Set.Explicit
74 import qualified Conjure.Rules.Vertical.Set.ExplicitVarSizeWithDummy as Vertical.Set.ExplicitVarSizeWithDummy
75 import qualified Conjure.Rules.Vertical.Set.ExplicitVarSizeWithFlags as Vertical.Set.ExplicitVarSizeWithFlags
76 import qualified Conjure.Rules.Vertical.Set.ExplicitVarSizeWithMarker as Vertical.Set.ExplicitVarSizeWithMarker
77 import qualified Conjure.Rules.Vertical.Set.Occurrence as Vertical.Set.Occurrence
78
79 import qualified Conjure.Rules.Horizontal.MSet as Horizontal.MSet
80 import qualified Conjure.Rules.Vertical.MSet.Occurrence as Vertical.MSet.Occurrence
81 import qualified Conjure.Rules.Vertical.MSet.ExplicitWithFlags as Vertical.MSet.ExplicitWithFlags
82 import qualified Conjure.Rules.Vertical.MSet.ExplicitWithRepetition as Vertical.MSet.ExplicitWithRepetition
83
84 import qualified Conjure.Rules.Horizontal.Function as Horizontal.Function
85 import qualified Conjure.Rules.Vertical.Function.Function1D as Vertical.Function.Function1D
86 import qualified Conjure.Rules.Vertical.Function.Function1DPartial as Vertical.Function.Function1DPartial
87 import qualified Conjure.Rules.Vertical.Function.FunctionND as Vertical.Function.FunctionND
88 import qualified Conjure.Rules.Vertical.Function.FunctionNDPartial as Vertical.Function.FunctionNDPartial
89 import qualified Conjure.Rules.Vertical.Function.FunctionNDPartialDummy as Vertical.Function.FunctionNDPartialDummy
90 import qualified Conjure.Rules.Vertical.Function.FunctionAsRelation as Vertical.Function.FunctionAsRelation
91
92 import qualified Conjure.Rules.Horizontal.Sequence as Horizontal.Sequence
93 import qualified Conjure.Rules.Vertical.Sequence.ExplicitBounded as Vertical.Sequence.ExplicitBounded
94
95 import qualified Conjure.Rules.Horizontal.Relation as Horizontal.Relation
96 import qualified Conjure.Rules.Vertical.Relation.RelationAsMatrix as Vertical.Relation.RelationAsMatrix
97 import qualified Conjure.Rules.Vertical.Relation.RelationAsSet as Vertical.Relation.RelationAsSet
98
99 import qualified Conjure.Rules.Horizontal.Partition as Horizontal.Partition
100 import qualified Conjure.Rules.Vertical.Partition.PartitionAsSet as Vertical.Partition.PartitionAsSet
101 import qualified Conjure.Rules.Vertical.Partition.Occurrence as Vertical.Partition.Occurrence
102 import qualified Conjure.Rules.Transform as Transform
103
104 import qualified Conjure.Rules.BubbleUp as BubbleUp
105 import qualified Conjure.Rules.DontCare as DontCare
106 import qualified Conjure.Rules.TildeOrdering as TildeOrdering
107
108 -- base
109 import System.IO ( hFlush, stdout )
110 import Data.IORef ( IORef, newIORef, readIORef, writeIORef, modifyIORef )
111 import System.IO.Unsafe ( unsafePerformIO )
112
113 -- uniplate
114 import Data.Generics.Uniplate.Zipper ( hole, replaceHole )
115 import Data.Generics.Uniplate.Zipper as Zipper ( right, up )
116
117 -- pipes
118 import Pipes ( Pipe, Producer, await, yield, (>->), cat )
119 import qualified Pipes.Prelude as Pipes ( foldM )
120
121 import qualified Data.Aeson.Types as JSON -- aeson
122 import qualified Data.Aeson.KeyMap as KM
123 import qualified Data.HashMap.Strict as M -- containers
124 import qualified Data.Vector as V -- vector
125
126 -- containers
127 import qualified Data.Set as S
128
129 -- text
130 import qualified Data.Text as T ( stripPrefix )
131
132
133 outputModels ::
134 forall m .
135 MonadIO m =>
136 MonadFailDoc m =>
137 MonadLog m =>
138 NameGen m =>
139 EnumerateDomain m =>
140 MonadUserError m =>
141 (?typeCheckerMode :: TypeCheckerMode) =>
142 Maybe Int -> -- portfolioSize
143 S.Set Int -> -- modelHashesBefore
144 String -> -- modelNamePrefix
145 Config ->
146 Model ->
147 m (S.Set Int) -- hash values, identifying the models
148 outputModels portfolioSize modelHashesBefore modelNamePrefix config model = do
149
150 liftIO $ writeIORef recordedResponses (responses config)
151 liftIO $ writeIORef recordedResponsesRepresentation (responsesRepresentation config)
152
153 -- Savile Row does not support ' characters in identifiers
154 -- We could implement a workaround where we insert a marker (like __PRIME__) for each ' character
155 -- and recover these after a solution is found.
156 -- But this will be too hairy, instead we will reject such identifiers for now.
157 -- If somebody really needs to use a ' character as part of an identifier, we can revisit this decision.
158 let
159 primeyIdentifiers = catMaybes
160 [ if '\'' `elem` textToString identifier
161 then Just identifier
162 else Nothing
163 | Declaration decl <- mStatements model
164 , Name identifier <- universeBi decl
165 ]
166 unless (null primeyIdentifiers) $ userErr1 $ vcat
167 ["Identifiers cannot contain a quotation mark character in them:" <+> prettyList id "," primeyIdentifiers]
168
169 let dir = outputDirectory config
170
171 unless (estimateNumberOfModels config) $
172 liftIO $ createDirectoryIfMissing True dir
173
174 let
175 limitModelsIfEstimating :: Pipe LogOrModel LogOrModel m ()
176 limitModelsIfEstimating =
177 if estimateNumberOfModels config
178 then limitModelsNeeded 1
179 else Pipes.cat
180
181 limitModelsIfNeeded :: Pipe LogOrModel LogOrModel m ()
182 limitModelsIfNeeded = maybe Pipes.cat limitModelsNeeded (limitModels config)
183
184 limitModelsNeeded :: Int -> Pipe LogOrModel LogOrModel m ()
185 limitModelsNeeded 0 = return ()
186 limitModelsNeeded n = do
187 x <- Pipes.await
188 Pipes.yield x
189 case x of
190 Left {} -> limitModelsNeeded n -- yielded a log, still n models to produce
191 Right{} -> limitModelsNeeded (n-1) -- yielded a model, produce n-1 more models
192
193 limitModelsPortfolioSize :: Pipe LogOrModel LogOrModel m ()
194 limitModelsPortfolioSize =
195 case portfolioSize of
196 Nothing -> Pipes.cat
197 Just s -> do
198 nb <- liftIO (readIORef nbGeneratedModels)
199 if nb < s
200 then do
201 x <- Pipes.await
202 Pipes.yield x
203 limitModelsPortfolioSize
204 else do
205 log LogInfo $ "Stopping, generated" <+> pretty nb <+> "models."
206 return ()
207
208 each (modelHashes, i) logOrModel =
209 case logOrModel of
210 Left (l,msg) -> do
211 log l msg
212 return (modelHashes, i)
213 Right eprime -> do
214 let newHash = eprime { mInfo = def, mStatements = sort (mStatements eprime) }
215 |> normaliseQuantifiedVariables
216 |> hash
217 let gen =
218 if modelNamePrefix `elem` ["01_compact", "02_sparse"]
219 then modelNamePrefix
220 else modelNamePrefix ++
221 if smartFilenames config
222 then [ choice
223 | (_question, choice, numOptions) <-
224 eprime |> mInfo |> miTrailCompact
225 , numOptions > 1
226 ] |> map (('_':) . show)
227 |> concat
228 else padLeft 6 '0' (show i)
229 let filename = dir </> gen ++ ".eprime"
230 if S.member newHash modelHashes
231 then do
232 log LogInfo $ "Skipping duplicate model (" <> pretty filename <> ")"
233 return (modelHashes, i)
234 else do
235 if estimateNumberOfModels config
236 then do
237 let
238 estimate :: Integer
239 estimate = product $ 1 : [ toInteger numOptions
240 | (_question, _choice, numOptions) <-
241 eprime |> mInfo |> miTrailCompact
242 ]
243 log LogInfo $ "These options would generate at least"
244 <+> pretty estimate
245 <+> (if estimate == 1 then "model" else "models") <> "."
246 else do
247 case portfolioSize of
248 Nothing -> return ()
249 Just _ -> log LogInfo $ "Saved model in:" <+> pretty filename
250 writeModel (lineWidth config) Plain (Just filename) eprime
251 liftIO $ modifyIORef nbGeneratedModels (+1)
252 let modelHashes' = S.insert newHash modelHashes
253 return (modelHashes', i+1)
254
255 let ?typeCheckerMode = RelaxedIntegerTags
256
257 Pipes.foldM each
258 (return (modelHashesBefore, numberingStart config))
259 (\ (modelHashes, _nbModels) -> return modelHashes )
260 (toCompletion config model
261 >-> limitModelsIfNeeded
262 >-> limitModelsIfEstimating
263 >-> limitModelsPortfolioSize)
264
265
266 toCompletion :: forall m .
267 MonadIO m =>
268 MonadFailDoc m =>
269 NameGen m =>
270 EnumerateDomain m =>
271 (?typeCheckerMode :: TypeCheckerMode) =>
272 Config ->
273 Model ->
274 Producer LogOrModel m ()
275 toCompletion config m = do
276 m2 <- let ?typeCheckerMode = StronglyTyped in prologue m
277 namegenst <- exportNameGenState
278 let m2Info = mInfo m2
279 let m3 = m2 { mInfo = m2Info { miStrategyQ = strategyQ config
280 , miStrategyA = strategyA config
281 , miNameGenState = namegenst
282 } }
283 logDebug $ modelInfo m3
284 loopy (StartOver m3)
285 where
286 driver :: Driver
287 driver = strategyToDriver config
288
289 loopy :: ModelWIP -> Producer LogOrModel m ()
290 loopy modelWIP = do
291 logDebug $ "[loop]" <+> pretty ((modelWIPOut modelWIP) {mInfo = def})
292 qs <- remainingWIP config modelWIP
293 if null qs
294 then do
295 let model = modelWIPOut modelWIP
296 model' <- epilogue model
297 yield (Right model')
298 else do
299 nextModels <- driver qs
300 mapM_ loopy nextModels
301
302
303 modelRepresentationsJSON ::
304 MonadFailDoc m =>
305 NameGen m =>
306 EnumerateDomain m =>
307 MonadLog m =>
308 (?typeCheckerMode :: TypeCheckerMode) =>
309 Model -> m JSONValue
310 modelRepresentationsJSON model = do
311 reprs <- modelRepresentations model
312 return $ JSON.Array $ V.fromList
313 [ JSON.Object $ KM.fromList
314 [ "name" ~~ r name
315 , "representations" ~~ representationsJSON
316 ]
317 | (name, domains) <- reprs
318 , let representationsJSON = JSON.Array $ V.fromList
319 [ JSON.Object $ KM.fromList
320 [ "description" ~~ r d
321 , "answer" ~~ toJSON i
322 ]
323 | (i, d) <- zip allNats domains
324 ]
325 ]
326 where
327 (~~) :: JSON.Key -> JSONValue -> (JSON.Key, JSONValue)
328 x ~~ y = ( x, y)
329 r s = JSON.String $ stringToText $ render 100000 $ pretty s
330
331
332 modelRepresentations ::
333 MonadFailDoc m =>
334 NameGen m =>
335 EnumerateDomain m =>
336 MonadLog m =>
337 (?typeCheckerMode :: TypeCheckerMode) =>
338 Model -> m [(Name, [Domain HasRepresentation Expression])]
339 modelRepresentations model0 = do
340 model <- prologue model0
341 concatForM (mStatements model) $ \case
342 Declaration (FindOrGiven _ name domain) -> do
343 domOpts <- reprOptions reprsStandardOrderNoLevels domain
344 return [(name, domOpts)]
345 _ -> return []
346
347
348 -- | If a rule is applied at a position P, the MonadZipper will be retained focused at that location
349 -- and new rules will be tried using P as the top of the zipper-tree.
350 -- The whole model (containing P too) will be tried later for completeness.
351 remainingWIP ::
352 MonadFailDoc m =>
353 MonadLog m =>
354 NameGen m =>
355 EnumerateDomain m =>
356 (?typeCheckerMode :: TypeCheckerMode) =>
357 Config ->
358 ModelWIP ->
359 m [Question]
360 remainingWIP config (StartOver model)
361 | Just modelZipper <- mkModelZipper model = do
362 qs <- remaining config modelZipper (mInfo model)
363 return qs
364 | otherwise = return []
365 remainingWIP config wip@(TryThisFirst modelZipper info) = do
366 qs <- remaining config modelZipper info
367 case (null qs, Zipper.right modelZipper, Zipper.up modelZipper) of
368 (False, _, _) -> return qs -- not null, return
369 (_, Just r, _) -> remainingWIP config (TryThisFirst r info) -- there is a sibling to the right
370 (_, _, Just u) -> remainingWIP config (TryThisFirst u info) -- there is a parent
371 _ -> remainingWIP config (StartOver (modelWIPOut wip)) -- we are done here,
372 -- start-over the whole model in case
373 -- something on the left needs attention.
374
375
376 remaining ::
377 MonadFailDoc m =>
378 MonadLog m =>
379 NameGen m =>
380 EnumerateDomain m =>
381 (?typeCheckerMode :: TypeCheckerMode) =>
382 Config ->
383 ModelZipper ->
384 ModelInfo ->
385 m [Question]
386 remaining config modelZipper minfo = do
387 -- note: the call to getQuestions can update the NameGen state
388 importNameGenState (minfo |> miNameGenState)
389 questions <- getQuestions config modelZipper
390 namegenst0 <- exportNameGenState
391 forM questions $ \ (focus, answers0) -> do
392 answers1 <- forM answers0 $ \ (ruleName, RuleResult{..}) -> do
393 importNameGenState namegenst0
394 ruleResultExpr <- ruleResult
395 -- ruleResultExpr <- fmap fixRelationProj ruleResult -- TODO: do we need the fixRelationProj?
396 let fullModelBeforeHook = replaceHole ruleResultExpr focus
397 let mtyBefore = typeOf (hole focus)
398 let mtyAfter = typeOf ruleResultExpr
399 case (mtyBefore, mtyAfter) of
400 (Right tyBefore, Right tyAfter) ->
401 unless (typesUnify [tyBefore, tyAfter]) $
402 bug $ vcat
403 [ "Rule application changes type:" <+> pretty ruleName
404 , "Before:" <+> pretty (hole focus)
405 , "After :" <+> pretty ruleResultExpr
406 , "Type before:" <+> pretty (show tyBefore)
407 , "Type after :" <+> pretty (show tyAfter)
408 ]
409 (Left msg, _) -> bug $ vcat
410 [ "Type error before rule application:" <+> pretty ruleName
411 , "Before:" <+> pretty (hole focus)
412 , "After :" <+> pretty ruleResultExpr
413 , "Error :" <+> pretty msg
414 ]
415 (_, Left msg) -> bug $ vcat
416 [ "Type error after rule application:" <+> pretty ruleName
417 , "Before:" <+> pretty (hole focus)
418 , "After :" <+> pretty ruleResultExpr
419 , "Error :" <+> pretty msg
420 ]
421
422 fullModelAfterHook <- case ruleResultHook of
423 Nothing -> do
424 namegenst <- exportNameGenState
425 return (TryThisFirst fullModelBeforeHook minfo { miNameGenState = namegenst })
426 Just hook -> do
427 namegenst1 <- exportNameGenState
428 let m1 = fromModelZipper fullModelBeforeHook minfo { miNameGenState = namegenst1 }
429 m2 <- hook m1
430 namegenst2 <- exportNameGenState
431 let m3 = m2 { mInfo = (mInfo m2) { miNameGenState = namegenst2 } }
432 return (StartOver m3)
433
434 return
435 ( Answer
436 { aText = ruleName <> ":" <+> ruleResultDescr
437 , aRuleName = ruleName
438 , aBefore = hole focus
439 , aAnswer = ruleResultExpr
440 , aFullModel = fullModelAfterHook
441 }
442 , ruleResultType
443 )
444 let qTypes = map snd answers1
445 qType' <- case qTypes of
446 [] -> bug "No applicable rules"
447 (t:ts) ->
448 if all (t==) ts
449 then return t
450 else bug "Rules of different rule kinds applicable, this is a bug."
451 return Question
452 { qType = qType'
453 , qHole = hole focus
454 , qAscendants = drop 1 (ascendants focus)
455 , qAnswers = map fst answers1
456 }
457
458
459 -- | Computes all applicable questions.
460 -- strategyQ == PickFirst is special-cased for performance.
461 getQuestions ::
462 MonadLog m =>
463 MonadFailDoc m =>
464 NameGen m =>
465 EnumerateDomain m =>
466 (?typeCheckerMode :: TypeCheckerMode) =>
467 Config ->
468 ModelZipper ->
469 m [(ModelZipper, [(Doc, RuleResult m)])]
470 getQuestions config modelZipper | strategyQ config == PickFirst = maybeToList <$>
471 let
472 loopLevels :: Monad m => [m (Maybe a)] -> m (Maybe a)
473 loopLevels [] = return Nothing
474 loopLevels (a:as) = do bs <- a
475 case bs of
476 Nothing -> loopLevels as
477 Just {} -> return bs
478
479 processLevel :: (MonadFailDoc m, MonadLog m, NameGen m, EnumerateDomain m)
480 => [Rule]
481 -> m (Maybe (ModelZipper, [(Doc, RuleResult m)]))
482 processLevel rulesAtLevel =
483 let
484 go [] = return Nothing
485 go (x:xs) = do
486 ys <- applicableRules config rulesAtLevel x
487 if null ys
488 then go xs
489 else return (Just (x, ys))
490 in
491 go (allContextsExceptReferences modelZipper)
492 in
493 loopLevels (map processLevel (allRules config))
494 getQuestions config modelZipper =
495 let
496 loopLevels :: Monad m => [m [a]] -> m [a]
497 loopLevels [] = return []
498 loopLevels (a:as) = do bs <- a
499 if null bs
500 then loopLevels as
501 else return bs
502
503 processLevel :: (MonadFailDoc m, MonadLog m, NameGen m, EnumerateDomain m)
504 => [Rule]
505 -> m [(ModelZipper, [(Doc, RuleResult m)])]
506 processLevel rulesAtLevel =
507 fmap catMaybes $ forM (allContextsExceptReferences modelZipper) $ \ x -> do
508 ys <- applicableRules config rulesAtLevel x
509 return $ if null ys
510 then Nothing
511 else Just (x, ys)
512 in
513 loopLevels (map processLevel (allRules config))
514
515
516 strategyToDriver :: Config -> Driver
517 strategyToDriver config questions = do
518 let optionsQ =
519 [ (doc, q)
520 | (n, q) <- zip allNats questions
521 , let doc =
522 vcat $ ("Question" <+> pretty n <> ":" <+> pretty (qHole q))
523 : [ nest 4 ("Context #" <> pretty i <> ":" <+> pretty c)
524 | (i,c) <- zip allNats (qAscendants q)
525 -- if logLevel < LogDebugVerbose, only show a select few levels
526 , logLevel config == LogDebugVerbose || i `elem` [1,3,5,10,25]
527 ]
528 ]
529 pickedQs <- executeStrategy (bug "strategyToDriver no Question") optionsQ (strategyQ config)
530 fmap concat $ forM pickedQs $ \ (pickedQNumber, pickedQDescr, pickedQ) -> do
531 let optionsA =
532 [ (doc, a)
533 | (n, a) <- zip allNats (qAnswers pickedQ)
534 , let doc = nest 4 $ "Answer" <+> pretty n <> ":" <+>
535 if "choose-repr" `isPrefixOf` show (aRuleName a)
536 then pretty (aText a)
537 else vcat [ pretty (aText a)
538 , sep [pretty (qHole pickedQ), "~~>", pretty (aAnswer a)]
539 ]
540 ]
541 let strategyA' = case qType pickedQ of
542 ChooseRepr -> representations
543 ChooseRepr_Find{} -> representationsFinds
544 ChooseRepr_Given{} -> representationsGivens
545 ChooseRepr_Auxiliary -> representationsAuxiliaries
546 ChooseRepr_Quantified -> representationsQuantifieds
547 ChooseRepr_Cut{} -> representationsCuts
548 ExpressionRefinement -> strategyA
549 pickedAs <- executeAnswerStrategy config pickedQ optionsA (strategyA' config)
550 return
551 [ theModel
552 | (pickedANumber, pickedADescr, pickedA) <- pickedAs
553 , let upd = addToTrail
554 config
555 (strategyQ config) pickedQNumber pickedQDescr pickedQ
556 (strategyA' config) pickedANumber (length optionsA) pickedADescr pickedA
557 , let theModel = updateModelWIPInfo upd (aFullModel pickedA)
558 ]
559
560
561 recordedResponses :: IORef (Maybe [Int])
562 {-# NOINLINE recordedResponses #-}
563 recordedResponses = unsafePerformIO (newIORef Nothing)
564
565 recordedResponsesRepresentation :: IORef (Maybe [(Name, Int)])
566 {-# NOINLINE recordedResponsesRepresentation #-}
567 recordedResponsesRepresentation = unsafePerformIO (newIORef Nothing)
568
569 nbGeneratedModels :: IORef Int
570 {-# NOINLINE nbGeneratedModels #-}
571 nbGeneratedModels = unsafePerformIO (newIORef 0)
572
573
574 executeStrategy :: (MonadIO m, MonadLog m) => Question -> [(Doc, a)] -> Strategy -> m [(Int, Doc, a)]
575 executeStrategy _ [] _ = bug "executeStrategy: nothing to choose from"
576 executeStrategy _ [(doc, option)] (viewAuto -> (_, True)) = do
577 logDebug ("Picking the only option:" <+> doc)
578 return [(1, doc, option)]
579 executeStrategy question options@((doc, option):_) (viewAuto -> (strategy, _)) =
580 case strategy of
581 Auto _ -> bug "executeStrategy: Auto"
582 PickFirst -> do
583 logDebug ("Picking the first option:" <+> doc)
584 return [(1, doc, option)]
585 Sparse -> do
586 logDebug ("Picking the first option (in sparse order):" <+> doc)
587 return [(1, doc, option)]
588 PickAll -> return [ (i,d,o) | (i,(d,o)) <- zip [1..] options ]
589 Interactive -> liftIO $ do
590 putStrLn $ render 80 $ vcat (map fst options)
591 recordedResponsesRepresentation' <- readIORef recordedResponsesRepresentation
592 let
593 nextRecordedResponse :: IO (Maybe Int)
594 nextRecordedResponse = do
595 mres <- readIORef recordedResponses
596 case mres of
597 Just (next:rest) -> do
598 writeIORef recordedResponses (Just rest)
599 return (Just next)
600 _ -> return Nothing
601
602 nextRecordedResponseRepresentation :: Name -> Maybe Int
603 nextRecordedResponseRepresentation nm =
604 case recordedResponsesRepresentation' of
605 Nothing -> Nothing
606 Just mres -> lookup nm mres
607
608 pickIndex :: IO Int
609 pickIndex = do
610 let useStoredReprResponse =
611 case qType question of
612 ChooseRepr_Find nm -> Just nm
613 ChooseRepr_Given nm -> Just nm
614 ChooseRepr_Cut nm -> Just nm
615 _ -> Nothing
616 let storedReprResponse =
617 case useStoredReprResponse of
618 Just nm -> nextRecordedResponseRepresentation nm
619 Nothing -> Nothing
620 case storedReprResponse of
621 Just recorded -> do
622 putStrLn ("Response: " ++ show recorded)
623 unless (recorded >= 1 && recorded <= length options) $
624 userErr1 $ vcat [ "Recorded response out of range."
625 , nest 4 $ "Expected a value between 1 and" <+> pretty (length options)
626 , nest 4 $ "But got: " <+> pretty recorded
627 ]
628 return recorded
629 Nothing -> do
630 mrecorded <- nextRecordedResponse
631 case mrecorded of
632 Just recorded -> do
633 putStrLn ("Response: " ++ show recorded)
634 unless (recorded >= 1 && recorded <= length options) $
635 userErr1 $ vcat [ "Recorded response out of range."
636 , nest 4 $ "Expected a value between 1 and" <+> pretty (length options)
637 , nest 4 $ "But got: " <+> pretty recorded
638 ]
639 return recorded
640 Nothing -> do
641 putStr "Pick option: "
642 hFlush stdout
643 line <- getLine
644 case (line, readMay line) of
645 ("", _) -> return 1
646 (_, Just lineInt) | lineInt >= 1 && lineInt <= length options -> return lineInt
647 (_, Nothing) -> do
648 putStrLn "Enter an integer value."
649 pickIndex
650 (_, Just _) -> do
651 print $ pretty $ "Enter a value between 1 and" <+> pretty (length options)
652 pickIndex
653
654 pickedIndex <- pickIndex
655 let (pickedDescr, picked) = at options (pickedIndex - 1)
656 return [(pickedIndex, pickedDescr, picked)]
657 AtRandom -> do
658 let nbOptions = length options
659 pickedIndex <- liftIO $ randomRIO (1, nbOptions)
660 let (pickedDescr, picked) = at options (pickedIndex - 1)
661 logDebug ("Randomly picking option #" <> pretty pickedIndex <+> "out of" <+> pretty nbOptions)
662 return [(pickedIndex, pickedDescr, picked)]
663 Compact -> bug "executeStrategy: Compact"
664
665
666 executeAnswerStrategy :: (MonadIO m, MonadLog m)
667 => Config -> Question -> [(Doc, Answer)] -> Strategy -> m [(Int, Doc, Answer)]
668 executeAnswerStrategy _ _ [] _ = bug "executeStrategy: nothing to choose from"
669 executeAnswerStrategy _ _ [(doc, option)] (viewAuto -> (_, True)) = do
670 logDebug ("Picking the only option:" <+> doc)
671 return [(1, doc, option)]
672 executeAnswerStrategy config question options st@(viewAuto -> (strategy, _)) = do
673 let
674 -- if the trail log does not tell us what to do
675 cacheMiss =
676 case strategy of
677 Compact -> do
678 let (n,(doc,c)) = minimumBy (compactCompareAnswer `on` (snd . snd)) (zip [1..] options)
679 return [(n, doc, c)]
680 _ -> executeStrategy question options st
681
682 case M.lookup (hashQuestion question) (followTrail config) of
683 Just aHash -> do
684 case [ (n, doc, option) | (n, (doc, option)) <- zip [1..] options, hashAnswer option == aHash ] of
685 [a] -> do
686 return [a]
687 _ -> cacheMiss
688 Nothing -> cacheMiss
689
690
691 compactCompareAnswer :: Answer -> Answer -> Ordering
692 compactCompareAnswer = comparing (expressionDepth . aAnswer)
693 where
694 expressionDepth :: Data a => a -> Int
695 expressionDepth x = 1 + maximum (0 : map expressionDepth (children x))
696
697
698 addToTrail
699 :: Config
700 -> Strategy -> Int -> Doc -> Question
701 -> Strategy -> Int -> Int -> Doc -> Answer
702 -> ModelInfo -> ModelInfo
703 addToTrail Config{..}
704 questionStrategy questionNumber questionDescr theQuestion
705 answerStrategy answerNumber answerNumbers answerDescr theAnswer
706 oldInfo = newInfo
707 where
708 ruleDescr = aText theAnswer
709 oldExpr = aBefore theAnswer
710 newExpr = aAnswer theAnswer
711 newInfo = oldInfo { miTrailCompact = (questionNumber, answerNumber, answerNumbers)
712 : miTrailCompact oldInfo
713 , miTrailGeneralised = (hashQuestion theQuestion, hashAnswer theAnswer)
714 : miTrailGeneralised oldInfo
715 , miTrailVerbose = if verboseTrail
716 then theA : theQ : miTrailVerbose oldInfo
717 else []
718 , miTrailRewrites = if rewritesTrail
719 then theRewrite : miTrailRewrites oldInfo
720 else []
721 }
722 theQ = Decision
723 { dDescription = map (stringToText . renderWide)
724 $ ("Question #" <> pretty questionNumber)
725 : (" (Using strategy:" <+> pretty (show questionStrategy) <> ")")
726 : map pretty (lines (renderWide questionDescr))
727 , dDecision = questionNumber
728 , dNumOptions = Nothing
729 }
730 theA = Decision
731 { dDescription = map (stringToText . renderWide)
732 $ ("Answer #" <> pretty answerNumber <+> "out of" <+> pretty (show answerNumbers))
733 : (" (Using strategy:" <+> pretty (show answerStrategy) <> ")")
734 : map pretty (lines (renderWide answerDescr))
735 , dDecision = answerNumber
736 , dNumOptions = Just answerNumbers
737 }
738 theRewrite = TrailRewrites
739 { trRule = stringToText $ renderWide ruleDescr
740 , trBefore = map stringToText $ lines $ renderWide $ pretty oldExpr
741 , trAfter = map stringToText $ lines $ renderWide $ pretty newExpr
742 }
743
744
745 hashQuestion :: Question -> Int
746 hashQuestion q = hash (qType q, qHole q, qAscendants q)
747
748
749 hashAnswer :: Answer -> Int
750 hashAnswer a = hash (aBefore a, renderWide (aRuleName a), aAnswer a)
751
752
753 -- | Add a true-constraint, for every decision variable (whether it is used or not in the model) and
754 -- for every parameter (that is not used in the model).
755 -- A true-constraint has no effect, other than forcing Conjure to produce a representation.
756 -- It can be used to make sure that a declaration doesn't get lost (if it isn't used anywhere in the model)
757 -- It can also be used to produce "extra" representations (if it is used in the model)
758 addTrueConstraints :: Model -> Model
759 addTrueConstraints m =
760 let
761 mkTrueConstraint forg nm dom = Op $ MkOpTrue $ OpTrue (Reference nm (Just (DeclNoRepr forg nm dom NoRegion)))
762 trueConstraints = [ mkTrueConstraint forg nm d
763 | (Declaration (FindOrGiven forg nm d), after) <- withAfter (mStatements m)
764 , forg == Find || (forg == Given && nbUses nm after == 0)
765 ]
766 in
767 m { mStatements = mStatements m ++ [SuchThat trueConstraints] }
768
769
770 reverseTrails :: Model -> Model
771 reverseTrails m =
772 let
773 oldInfo = mInfo m
774 newInfo = oldInfo { miTrailCompact = reverse (miTrailCompact oldInfo)
775 , miTrailVerbose = reverse (miTrailVerbose oldInfo)
776 , miTrailRewrites = reverse (miTrailRewrites oldInfo)
777 }
778 in
779 m { mInfo = newInfo }
780
781
782 oneSuchThat :: Model -> Model
783 oneSuchThat m = m { mStatements = onStatements (mStatements m)
784 |> nubBy ((==) `on` normaliseQuantifiedVariablesS) }
785
786 where
787
788 onStatements :: [Statement] -> [Statement]
789 onStatements xs =
790 let
791 (suchThats0, objectives, others) = xs |> map collect |> mconcat
792 suchThats = suchThats0
793 |> map breakConjunctions -- break top level /\'s
794 |> mconcat
795 |> filter (/= Constant (ConstantBool True)) -- remove top level true's
796 |> nubBy ((==) `on` normaliseQuantifiedVariablesE) -- uniq
797 in
798 others ++ objectives ++ [SuchThat (combine suchThats)]
799
800 collect :: Statement -> ( [Expression] -- SuchThats
801 , [Statement] -- Objectives
802 , [Statement] -- other statements
803 )
804 collect (SuchThat s) = (s, [], [])
805 collect s@Objective{} = ([], [s], [])
806 collect s = ([], [], [s])
807
808 combine :: [Expression] -> [Expression]
809 combine xs = if null xs
810 then [Constant (ConstantBool True)]
811 else xs
812
813 breakConjunctions :: Expression -> [Expression]
814 breakConjunctions p@(Op (MkOpAnd (OpAnd x))) =
815 case listOut x of
816 Nothing -> [p] -- doesn't contain a list
817 Just xs -> concatMap breakConjunctions xs
818 breakConjunctions x = [x]
819
820
821 emptyMatrixLiterals :: Model -> Model
822 emptyMatrixLiterals model =
823 let
824 f (TypeList ty) = TypeMatrix (TypeInt TagInt) ty
825 f x = x
826 in
827 model { mStatements = mStatements model |> transformBi f }
828
829
830 expandDomainReferences :: Model -> Model
831 expandDomainReferences = transformBi (expandDomainReference :: Domain () Expression -> Domain () Expression)
832
833
834 -- | Add a default search order (branching on [...])
835 -- to include all the primary variables and none of the aux variables that will potentailly be generated by Conjure.
836 -- Do not change the model if it already contains a SearchOrder in it.
837 addSearchOrder :: Model -> Model
838 addSearchOrder model
839 | let hasSearchOrder = not $ null [ () | SearchOrder{} <- mStatements model ]
840 , hasSearchOrder = model
841 | otherwise =
842 let finds = [ nm | Declaration (FindOrGiven Find nm _domain) <- mStatements model ]
843 in model { mStatements = mStatements model ++ [SearchOrder (map BranchingOn finds)] }
844
845
846 inlineDecVarLettings :: Model -> Model
847 inlineDecVarLettings model =
848 let
849 inline p@(Reference nm _) = do
850 x <- gets (lookup nm)
851 return (fromMaybe p x)
852 inline p = return p
853
854 statements = catMaybes
855 $ flip evalState []
856 $ forM (mStatements model)
857 $ \ st ->
858 case st of
859 Declaration (Letting nm x)
860 | categoryOf x == CatDecision
861 -> modify ((nm,x) :) >> return Nothing
862 -- The following doesn't work when the identifier is used in a domain
863 -- Declaration (Letting nm x@Reference{})
864 -- -> modify ((nm,x) :) >> return Nothing
865 _ -> Just <$> transformBiM inline st
866 in
867 model { mStatements = statements }
868
869
870 dropTagForSR ::
871 MonadFailDoc m =>
872 (?typeCheckerMode :: TypeCheckerMode) =>
873 Model -> m Model
874 dropTagForSR m = do
875 let
876 replacePredSucc [essence| pred(&x) |] = do
877 ty <- typeOf x
878 case ty of
879 TypeBool{} -> return [essence| false |]
880 -- since True becomes False
881 -- False becomes out-of-bounds, hence False
882 TypeInt{} -> do
883 let xTagInt = reTag TagInt x
884 return [essence| &xTagInt - 1 |]
885 _ -> bug "predSucc"
886 replacePredSucc [essence| succ(&x) |] = do
887 ty <- typeOf x
888 case ty of
889 TypeBool{} -> return [essence| !&x |]
890 -- since False becomes True
891 -- True becomes out-of-bounds, hence False
892 -- "succ" is exactly "negate" on bools
893 TypeInt{} -> do
894 let xTagInt = reTag TagInt x
895 return [essence| &xTagInt + 1 |]
896 _ -> bug "predSucc"
897 -- replacePredSucc [essence| &a .< &b |] = return [essence| &a < &b |]
898 -- replacePredSucc [essence| &a .<= &b |] = return [essence| &a <= &b |]
899 replacePredSucc x = return x
900
901 st <- transformBiM replacePredSucc (mStatements m)
902 return m { mStatements = transformBi (\ _ -> TagInt) st }
903
904
905 updateDeclarations ::
906 MonadUserError m =>
907 MonadFailDoc m =>
908 NameGen m =>
909 EnumerateDomain m =>
910 (?typeCheckerMode :: TypeCheckerMode) =>
911 Model -> m Model
912 updateDeclarations model = do
913 let
914 representations = model |> mInfo |> miRepresentations
915
916 onEachStatement (inStatement, afters) =
917 case inStatement of
918 Declaration (FindOrGiven forg nm _) -> do
919 let
920 -- the refined domains for the high level declaration
921 domains = [ d | (n, d) <- representations, n == nm ]
922 nub <$> concatMapM (onEachDomain forg nm) domains
923 Declaration (GivenDomainDefnEnum name) -> return
924 [ Declaration (FindOrGiven Given (name `mappend` "_EnumSize") (DomainInt TagInt [])) ]
925 Declaration (Letting nm x) -> do
926 let
927 usedAfter :: Bool
928 usedAfter = nbUses nm afters > 0
929
930 nbComplexLiterals :: Int
931 nbComplexLiterals = sum
932 [ case y of
933 Constant (ConstantAbstract AbsLitMatrix{}) -> 0
934 Constant ConstantAbstract{} -> 1
935 AbstractLiteral AbsLitMatrix{} -> 0
936 AbstractLiteral{} -> 1
937 _ -> 0
938 | y <- universe x ]
939
940 isRefined :: Bool
941 isRefined = nbComplexLiterals == 0
942 return [inStatement | and [usedAfter, isRefined]]
943 Declaration LettingDomainDefnEnum{} -> return []
944 Declaration LettingDomainDefnUnnamed{} -> return []
945 SearchOrder orders -> do
946 orders' <- forM orders $ \case
947 BranchingOn nm -> do
948 let domains = [ d | (n, d) <- representations, n == nm ]
949 -- last one is the representation of what's in true(?)
950 -- put that first!
951 let reorder xs =
952 case reverse xs of
953 [] -> []
954 (y:ys) -> y : reverse ys
955 outNames <- concatMapM (onEachDomainSearch nm) (reorder domains)
956 return $ map BranchingOn $ nub outNames
957 Cut{} -> bug "updateDeclarations, Cut shouldn't be here"
958 return [ SearchOrder (concat orders') ]
959 _ -> return [inStatement]
960
961 onEachDomain forg nm domain =
962 runExceptT (downD (nm, domain)) >>= \case
963 Left err -> bug err
964 Right outs -> forM outs $ \ (n, d) -> do
965 d' <- transformBiM (trySimplify []) $ forgetRepr d
966 return $ Declaration (FindOrGiven forg n d')
967
968 onEachDomainSearch nm domain =
969 runExceptT (downD (nm, domain)) >>= \case
970 Left err -> bug err
971 Right outs -> return [ n
972 | (n, _) <- outs
973 ]
974
975 statements <- concatMapM onEachStatement (withAfter (mStatements model))
976 return model { mStatements = statements }
977
978
979 -- | checking whether any `Reference`s with `DeclHasRepr`s are left in the model
980 checkIfAllRefined :: MonadFailDoc m => Model -> m Model
981 checkIfAllRefined m | Just modelZipper <- mkModelZipper m = do -- we exclude the mInfo here
982 let returnMsg x = return
983 $ ""
984 : ("Not refined:" <+> pretty (hole x))
985 : [ nest 4 ("Context #" <> pretty i <> ":" <+> pretty c)
986 | (i, c) <- zip allNats (drop 1 (ascendants x))
987 ]
988
989 fails <- fmap (nubBy (\a b->show a == show b) . concat) $ forM (allContextsExceptReferences modelZipper) $ \ x ->
990 case hole x of
991 Reference _ (Just (DeclHasRepr _ _ dom))
992 | not (isPrimitiveDomain dom) ->
993 return $ ""
994 : ("Not refined:" <+> pretty (hole x))
995 : ("Domain :" <+> pretty dom)
996 : [ nest 4 ("Context #" <> pretty i <> ":" <+> pretty c)
997 | (i, c) <- zip allNats (drop 1 (ascendants x))
998 ]
999 Constant (ConstantAbstract AbsLitMatrix{}) -> return []
1000 Constant ConstantAbstract{} -> returnMsg x
1001 AbstractLiteral AbsLitMatrix{} -> return []
1002 AbstractLiteral{} -> returnMsg x
1003 WithLocals{} -> returnMsg x
1004 Comprehension _ stmts -> do
1005 decisionConditions <-
1006 fmap catMaybes $ forM stmts $ \ stmt -> case stmt of
1007 Condition c ->
1008 if categoryOf c >= CatDecision
1009 then return (Just c)
1010 else return Nothing
1011 _ -> return Nothing
1012 comprehensionLettings <-
1013 fmap catMaybes $ forM stmts $ \ stmt -> case stmt of
1014 ComprehensionLetting{} -> return (Just stmt)
1015 _ -> return Nothing
1016 unsupportedGenerator <-
1017 fmap catMaybes $ forM stmts $ \ stmt -> case stmt of
1018 Generator GenInExpr{} -> return (Just stmt)
1019 _ -> return Nothing
1020 let msgs = [ "decision expressions as conditions"
1021 | not (null decisionConditions) ]
1022 ++ [ "local lettings"
1023 | not (null comprehensionLettings) ]
1024 ++ [ "unsupported generators"
1025 | not (null unsupportedGenerator) ]
1026 let msg = "Comprehension contains" <+> prettyListDoc id "," msgs <> "."
1027 case msgs of
1028 [] -> return []
1029 _ -> return $ [ msg ]
1030 ++ [ nest 4 (pretty (hole x)) ]
1031 ++ [ nest 4 ("Context #" <> pretty i <> ":" <+> pretty c)
1032 | (i, c) <- zip allNats (drop 1 (ascendants x))
1033 ]
1034 [essence| &_ .< &_ |] ->
1035 return ["", ("Not refined:" <+> pretty (hole x))]
1036 [essence| &_ .<= &_ |] ->
1037 return ["", ("Not refined:" <+> pretty (hole x))]
1038 _ -> return []
1039 unless (null fails) (bug (vcat fails))
1040 return m
1041 checkIfAllRefined m = return m
1042
1043
1044 -- | checking whether any undefined values creeped into the final model
1045 checkIfHasUndefined :: MonadFailDoc m => Model -> m Model
1046 checkIfHasUndefined m | Just modelZipper <- mkModelZipper m = do
1047 let returnMsg x = return
1048 $ ""
1049 : ("Undefined value in the final model:" <+> pretty (hole x))
1050 : [ nest 4 ("Context #" <> pretty i <> ":" <+> pretty c)
1051 | (i, c) <- zip allNats (drop 1 (ascendants x))
1052 ]
1053
1054 fails <- fmap concat $ forM (allContextsExceptReferences modelZipper) $ \ x ->
1055 case hole x of
1056 Constant ConstantUndefined{} -> returnMsg x
1057 _ -> return []
1058 unless (null fails) (bug (vcat fails))
1059 return m
1060 checkIfHasUndefined m = return m
1061
1062
1063 topLevelBubbles ::
1064 MonadFailDoc m =>
1065 MonadUserError m =>
1066 NameGen m =>
1067 (?typeCheckerMode :: TypeCheckerMode) =>
1068 Model -> m Model
1069 topLevelBubbles m = do
1070 let
1071 onStmt (SuchThat xs) = onExprs xs
1072 onStmt (Where xs) = concatMapM onWheres xs
1073 onStmt (Objective obj (WithLocals h locals)) =
1074 case locals of
1075 AuxiliaryVars locs -> ( locs ++ [Objective obj h] ) |> onStmts
1076 DefinednessConstraints locs -> ( [SuchThat locs] ++ [Objective obj h] ) |> onStmts
1077 onStmt (Declaration decl) =
1078 let
1079 f (WithLocals h locs) = tell [locs] >> return h
1080 f x = return x
1081
1082 (decl', locals) = runWriter (transformBiM f decl)
1083
1084 conv :: InBubble -> [Statement]
1085 conv (AuxiliaryVars locs) = locs
1086 conv (DefinednessConstraints locs) = [SuchThat locs]
1087
1088 newStmts :: [Statement]
1089 newStmts = concatMap conv locals
1090 in
1091 if null newStmts
1092 then return [Declaration decl]
1093 else onStmts (newStmts ++ [Declaration decl'])
1094 onStmt s = return [s]
1095
1096 -- a where that has a bubble at the top-most level will be replaced
1097 -- with a Comprehension. this is to avoid creating a where with decision variables inside.
1098 onWheres (WithLocals h (DefinednessConstraints locals)) =
1099 return $ map (Where . return) (locals ++ [h])
1100 onWheres (WithLocals h (AuxiliaryVars locals)) = do
1101 let (localfinds, gens) = mconcat
1102 [ case local of
1103 Declaration (FindOrGiven LocalFind nm dom) ->
1104 ([nm], [Generator (GenDomainNoRepr (Single nm) dom)])
1105 SuchThat xs ->
1106 ([], map Condition xs)
1107 _ -> bug ("topLevelBubbles.onWheres:" <+> pretty local)
1108 | local <- locals
1109 ]
1110 let forgetReprsOfLocalFinds (Reference nm _) | nm `elem` localfinds = Reference nm Nothing
1111 forgetReprsOfLocalFinds x = descend forgetReprsOfLocalFinds x
1112 let out = Comprehension h gens
1113 out' <- resolveNamesX (forgetReprsOfLocalFinds out)
1114 return [Where [out']]
1115 onWheres x = return [Where [x]]
1116
1117 onExpr (WithLocals h (AuxiliaryVars locals)) = ( locals ++ [SuchThat [h]]) |> onStmts
1118 onExpr (WithLocals h (DefinednessConstraints locals)) = ([SuchThat locals] ++ [SuchThat [h]]) |> onStmts
1119 onExpr x = return [SuchThat [x]]
1120
1121 onStmts = concatMapM onStmt
1122 onExprs = concatMapM onExpr
1123
1124 statements' <- onStmts (mStatements m)
1125 return m { mStatements = statements' }
1126
1127
1128 sliceThemMatrices ::
1129 Monad m =>
1130 (?typeCheckerMode :: TypeCheckerMode) =>
1131 Model -> m Model
1132 sliceThemMatrices model = do
1133 let
1134 -- nothing stays with a matrix type
1135 -- we are doing this top down
1136 -- when we reach a matrix-typed expression, we know it needs to be sliced
1137 -- we descend otherwise
1138 -- we also descend into components of the matrix-typed expression during slicing
1139 onExpr :: Monad m => Expression -> m Expression
1140 onExpr p = do
1141 let computeExistingSlices t =
1142 case match opSlicing t of
1143 Nothing -> return 0
1144 Just (t', _, _) -> (+1) <$> computeExistingSlices t'
1145 let isIndexedMatrix = do
1146 (m, is) <- match opMatrixIndexing p
1147 tyM <- typeOf m
1148 nSlices <- computeExistingSlices m
1149 return (m, nSlices, is, tyM)
1150 case isIndexedMatrix of
1151 Nothing -> descendM onExpr p
1152 Just (m, existingSlices, is, tyM) -> do
1153 let nestingLevel (TypeMatrix _ a) = 1 + nestingLevel a
1154 nestingLevel (TypeList a) = 1 + nestingLevel a
1155 nestingLevel _ = 0 :: Int
1156 -- "is" is the number of existing indices
1157 -- "nestingLevel" is the nesting level of the original matrix
1158 -- "existingSlices" is the number of existing slices
1159 let howMany = nestingLevel tyM - existingSlices - length is
1160 let unroll a 0 = a
1161 unroll a i = make opSlicing (unroll a (i-1)) Nothing Nothing
1162 m' <- descendM onExpr m
1163 is' <- mapM onExpr is
1164 let p' = make opMatrixIndexing m' is'
1165 return $ unroll p' howMany
1166
1167 statements <- descendBiM onExpr (mStatements model)
1168 return model { mStatements = statements }
1169
1170
1171 removeExtraSlices :: Monad m => Model -> m Model
1172 removeExtraSlices model = do
1173 let
1174 -- a slice at the end of a chain of slices & indexings
1175 -- does no good in Essence and should be removed
1176 onExpr :: Monad m => Expression -> m Expression
1177 onExpr (match opSlicing -> Just (m,_,_)) = onExpr m
1178 onExpr p@(match opIndexing -> Just _) = return p
1179 onExpr p = descendM onExpr p
1180
1181 statements <- descendBiM onExpr (mStatements model)
1182 return model { mStatements = statements }
1183
1184
1185 removeUnderscores :: Monad m => Model -> m Model
1186 removeUnderscores model = do
1187 let
1188 -- SR doesn't support identifiers that start with _
1189 -- we replace them with UNDERSCORE_
1190 onName :: Name -> Name
1191 onName (Name t) =
1192 case T.stripPrefix "_" t of
1193 Nothing -> Name t
1194 Just t' -> Name (mappend "UNDERSCORE__" t')
1195 onName n = n
1196
1197 return $ transformBi onName model
1198
1199
1200 lexSingletons :: (?typeCheckerMode :: TypeCheckerMode)
1201 => Monad m
1202 => Model -> m Model
1203 lexSingletons model = do
1204 let onExpr :: (?typeCheckerMode :: TypeCheckerMode)
1205 => Monad m => Expression -> m Expression
1206 onExpr [essence| &l <lex &r |] =
1207 case (matchSingleton l, matchSingleton r) of
1208 (Nothing, Nothing) -> return [essence| &l <lex &r |]
1209 (Just ls, Just rs) -> return [essence| &ls < &rs |]
1210 _ -> bug $ "lexSingleton: match inconsistent"
1211 onExpr [essence| &l <=lex &r |] =
1212 case (matchSingleton l, matchSingleton r) of
1213 (Nothing, Nothing) -> return [essence| &l <=lex &r |]
1214 (Just ls, Just rs) -> return [essence| &ls <= &rs |]
1215 _ -> bug $ "lexSingleton: match inconsistent"
1216 onExpr x = return x
1217 matchSingleton :: (?typeCheckerMode :: TypeCheckerMode)
1218 => Expression -> Maybe Expression
1219 matchSingleton (match matrixLiteral -> Just (TypeMatrix _ TypeInt{},_,[s])) =
1220 Just s
1221 matchSingleton _ = Nothing
1222 statements <- transformBiM onExpr (mStatements model)
1223 return model { mStatements = statements }
1224
1225
1226 logDebugIdModel :: MonadLog m => Doc -> Model -> m Model
1227 logDebugIdModel msg a = logDebug (msg <++> pretty (a {mInfo = def})) >> return a
1228
1229 prologue ::
1230 MonadFailDoc m =>
1231 MonadLog m =>
1232 NameGen m =>
1233 EnumerateDomain m =>
1234 (?typeCheckerMode :: TypeCheckerMode) =>
1235 Model -> m Model
1236 prologue model = do
1237 void $ typeCheckModel_StandAlone model
1238 return model >>= logDebugIdModel "[input]"
1239 >>= removeUnderscores >>= logDebugIdModel "[removeUnderscores]"
1240 >>= return . addSearchOrder >>= logDebugIdModel "[addSearchOrder]"
1241 >>= attributeAsConstraints >>= logDebugIdModel "[attributeAsConstraints]"
1242 >>= inferAttributes >>= logDebugIdModel "[inferAttributes]"
1243 >>= inlineLettingDomainsForDecls >>= logDebugIdModel "[inlineLettingDomainsForDecls]"
1244 >>= lettingsForComplexInDoms >>= logDebugIdModel "[lettingsForComplexInDoms]"
1245 >>= distinctQuantifiedVars >>= logDebugIdModel "[distinctQuantifiedVars]"
1246 >>= return . initInfo >>= logDebugIdModel "[initInfo]"
1247 >>= removeUnnamedsFromModel >>= logDebugIdModel "[removeUnnamedsFromModel]"
1248 >>= removeEnumsFromModel >>= logDebugIdModel "[removeEnumsFromModel]"
1249 >>= finiteGivens >>= logDebugIdModel "[finiteGivens]"
1250 >>= renameQuantifiedVarsToAvoidShadowing
1251 >>= logDebugIdModel "[renameQuantifiedVarsToAvoidShadowing]"
1252 >>= resolveNames >>= logDebugIdModel "[resolveNames]"
1253 >>= return . initInfo_Lettings >>= logDebugIdModel "[initInfo_Lettings]"
1254 >>= removeDomainLettings >>= logDebugIdModel "[removeDomainLettings]"
1255 >>= typeCheckModel >>= logDebugIdModel "[typeCheckModel]"
1256 >>= categoryChecking >>= logDebugIdModel "[categoryChecking]"
1257 >>= sanityChecks >>= logDebugIdModel "[sanityChecks]"
1258 >>= dealWithCuts >>= logDebugIdModel "[dealWithCuts]"
1259 >>= removeExtraSlices >>= logDebugIdModel "[removeExtraSlices]"
1260 -- >>= evaluateModel >>= logDebugIdModel "[evaluateModel]"
1261 >>= return . addTrueConstraints >>= logDebugIdModel "[addTrueConstraints]"
1262
1263
1264 epilogue ::
1265 MonadFailDoc m =>
1266 MonadLog m =>
1267 NameGen m =>
1268 EnumerateDomain m =>
1269 (?typeCheckerMode :: TypeCheckerMode) =>
1270 Model -> m Model
1271 epilogue model = return model
1272 >>= logDebugIdModel "[epilogue]"
1273 >>= lexSingletons >>= logDebugIdModel "[lexSingletons]"
1274 >>= resolveNames >>= logDebugIdModel "[resolveNames]"
1275 >>= updateDeclarations >>= logDebugIdModel "[updateDeclarations]"
1276 >>= return . inlineDecVarLettings >>= logDebugIdModel "[inlineDecVarLettings]"
1277 >>= topLevelBubbles >>= logDebugIdModel "[topLevelBubbles]"
1278 >>= checkIfAllRefined >>= logDebugIdModel "[checkIfAllRefined]"
1279 >>= checkIfHasUndefined >>= logDebugIdModel "[checkIfHasUndefined]"
1280 >>= sliceThemMatrices >>= logDebugIdModel "[sliceThemMatrices]"
1281 >>= dropTagForSR >>= logDebugIdModel "[dropTagForSR]"
1282 >>= return . emptyMatrixLiterals >>= logDebugIdModel "[emptyMatrixLiterals]"
1283 >>= return . expandDomainReferences
1284 >>= logDebugIdModel "[expandDomainReferences]"
1285 >>= return . reverseTrails >>= logDebugIdModel "[reverseTrails]"
1286 >>= return . oneSuchThat >>= logDebugIdModel "[oneSuchThat]"
1287 >>= return . languageEprime >>= logDebugIdModel "[languageEprime]"
1288
1289
1290 applicableRules :: forall m n .
1291 MonadUserError n =>
1292 MonadFailDoc n =>
1293 MonadLog n =>
1294 NameGen n =>
1295 EnumerateDomain n =>
1296 MonadUserError m =>
1297 MonadLog m =>
1298 NameGen m =>
1299 EnumerateDomain m =>
1300 MonadFailDoc m =>
1301 (?typeCheckerMode :: TypeCheckerMode) =>
1302 Config ->
1303 [Rule] ->
1304 ModelZipper ->
1305 n [(Doc, RuleResult m)]
1306 applicableRules Config{..} rulesAtLevel x = do
1307 let logAttempt = if logRuleAttempts then logInfo else const (return ())
1308 let logFail = if logRuleFails then logInfo else const (return ())
1309 let logSuccess = if logRuleSuccesses then logInfo else const (return ())
1310
1311 mys <- sequence [ do logAttempt ("attempting rule" <+> rName r <+> "on" <+> pretty (hole x))
1312 applied <- runExceptT $ runReaderT (rApply r x (hole x)) x
1313 return (rName r, applied)
1314 | r <- rulesAtLevel ]
1315 forM_ mys $ \ (rule, my) ->
1316 case my of
1317 Left failed -> unless ("N/A" `isPrefixOf` show failed) $ logFail $ vcat
1318 [ " rule failed:" <+> rule
1319 , " on:" <+> pretty (hole x)
1320 , " message:" <+> failed
1321 ]
1322 Right ys -> logSuccess $ vcat
1323 [ "rule applied:" <+> rule
1324 , " on:" <+> pretty (hole x)
1325 , " message:" <+> vcat (map ruleResultDescr ys)
1326 ]
1327 return [ (name, res {ruleResult = ruleResult'})
1328 | (name, Right ress) <- mys
1329 , res <- ress
1330 , let ruleResult' = do
1331 rResult <- ruleResult res
1332 case (hole x, rResult) of
1333 (Reference nm1 _, Reference nm2 _)
1334 | show name /= "choose-repr"
1335 , nm1 == nm2 -> bug $ vcat
1336 [ "Rule applied inside a Reference."
1337 , "Rule :" <+> pretty name
1338 , "Rule input :" <+> pretty (hole x)
1339 , "Rule output :" <+> pretty rResult
1340 , "Rule input (show):" <+> pretty (show (hole x))
1341 , "Rule output (show):" <+> pretty (show rResult)
1342 ]
1343 _ -> return ()
1344 merr <- runExceptT (resolveNamesX rResult)
1345 case merr of
1346 Left err -> bug $ vcat
1347 [ "Name resolution failed after rule application."
1348 , "Rule :" <+> pretty name
1349 , "Rule input :" <+> pretty (hole x)
1350 , "Rule output :" <+> pretty rResult
1351 , "Rule input (show):" <+> pretty (show (hole x))
1352 , "Rule output (show):" <+> pretty (show rResult)
1353 , "The error :" <+> err
1354 ]
1355 Right r -> return r
1356 ]
1357
1358
1359 allRules :: (?typeCheckerMode :: TypeCheckerMode) => Config -> [[Rule]]
1360 allRules config =
1361 [ Transform.rules_Transform
1362 , [ rule_FullEvaluate
1363 ]
1364 , [ rule_PartialEvaluate
1365 ]
1366 ] ++ paramRules ++
1367 [ [ rule_ChooseRepr config
1368 , rule_ChooseReprForComprehension config
1369 , rule_ChooseReprForLocals config
1370 ]
1371 ] ++ bubbleUpRules ++
1372 [ [ rule_Eq
1373 , rule_Neq
1374 , rule_Comprehension_Cardinality
1375 , rule_Flatten_Cardinality
1376 ]
1377 , verticalRules
1378 , horizontalRules
1379 ] ++ otherRules
1380 ++ delayedRules
1381
1382
1383 -- | For information that can be readily pulled out from parameters.
1384 -- Some things are easier when everything involved is a param.
1385 -- These rules aren't necessary for correctness, but they can help remove some verbose expressions from the output.
1386 -- Make Savile Row happier so it makes us happier. :)
1387 paramRules :: [[Rule]]
1388 paramRules =
1389 [ [ Horizontal.Set.rule_Param_MinOfSet
1390 , Horizontal.Set.rule_Param_MaxOfSet
1391 , Horizontal.Set.rule_Param_Card
1392 ]
1393 , [ Horizontal.Function.rule_Param_DefinedRange
1394 , Horizontal.Relation.rule_Param_Card
1395 ]
1396 ]
1397
1398 verticalRules :: [Rule]
1399 verticalRules =
1400 [ Vertical.Tuple.rule_Tuple_Eq
1401 , Vertical.Tuple.rule_Tuple_Neq
1402 , Vertical.Tuple.rule_Tuple_Leq
1403 , Vertical.Tuple.rule_Tuple_Lt
1404 , Vertical.Tuple.rule_Tuple_TildeLeq
1405 , Vertical.Tuple.rule_Tuple_TildeLt
1406 , Vertical.Tuple.rule_Tuple_Index
1407
1408 , Vertical.Record.rule_Record_Eq
1409 , Vertical.Record.rule_Record_Neq
1410 , Vertical.Record.rule_Record_Leq
1411 , Vertical.Record.rule_Record_Lt
1412 , Vertical.Record.rule_Record_Index
1413
1414 , Vertical.Variant.rule_Variant_Eq
1415 , Vertical.Variant.rule_Variant_Neq
1416 , Vertical.Variant.rule_Variant_Leq
1417 , Vertical.Variant.rule_Variant_Lt
1418 , Vertical.Variant.rule_Variant_Index
1419 , Vertical.Variant.rule_Variant_Active
1420
1421 , Vertical.Matrix.rule_Comprehension_Literal
1422 , Vertical.Matrix.rule_Comprehension
1423 , Vertical.Matrix.rule_Comprehension_Flatten
1424 , Vertical.Matrix.rule_ModifierAroundIndexedMatrixLiteral
1425 , Vertical.Matrix.rule_Comprehension_LiteralIndexed
1426 , Vertical.Matrix.rule_Comprehension_Nested
1427 , Vertical.Matrix.rule_Comprehension_Hist
1428 , Vertical.Matrix.rule_Comprehension_ToSet_Matrix
1429 , Vertical.Matrix.rule_Comprehension_ToSet_List
1430 , Vertical.Matrix.rule_Comprehension_ToSet_List_DuplicateFree
1431 , Vertical.Matrix.rule_Matrix_Eq
1432 , Vertical.Matrix.rule_Matrix_Neq
1433 , Vertical.Matrix.rule_Matrix_Leq_Primitive
1434 , Vertical.Matrix.rule_Matrix_Leq_Decompose
1435 , Vertical.Matrix.rule_Matrix_Lt_Primitive
1436 , Vertical.Matrix.rule_Matrix_Lt_Decompose
1437 , Vertical.Matrix.rule_IndexingIdentical
1438 , Vertical.Matrix.rule_ExpandSlices
1439 , Vertical.Matrix.rule_Freq
1440
1441 , Vertical.Set.Explicit.rule_Min
1442 , Vertical.Set.Explicit.rule_Max
1443 , Vertical.Set.Explicit.rule_Card
1444 , Vertical.Set.Explicit.rule_Comprehension
1445 , Vertical.Set.Explicit.rule_PowerSet_Comprehension
1446 , Vertical.Set.Explicit.rule_In
1447 , Vertical.Set.ExplicitVarSizeWithDummy.rule_Comprehension
1448 , Vertical.Set.ExplicitVarSizeWithDummy.rule_PowerSet_Comprehension
1449 , Vertical.Set.ExplicitVarSizeWithFlags.rule_Comprehension
1450 , Vertical.Set.ExplicitVarSizeWithFlags.rule_PowerSet_Comprehension
1451 , Vertical.Set.ExplicitVarSizeWithMarker.rule_Card
1452 , Vertical.Set.ExplicitVarSizeWithMarker.rule_Comprehension
1453 , Vertical.Set.ExplicitVarSizeWithMarker.rule_PowerSet_Comprehension
1454 , Vertical.Set.Occurrence.rule_Comprehension
1455 , Vertical.Set.Occurrence.rule_PowerSet_Comprehension
1456 , Vertical.Set.Occurrence.rule_In
1457
1458 , Vertical.MSet.Occurrence.rule_Comprehension
1459 , Vertical.MSet.Occurrence.rule_Freq
1460
1461 , Vertical.MSet.ExplicitWithFlags.rule_Comprehension
1462 , Vertical.MSet.ExplicitWithFlags.rule_Freq
1463
1464 , Vertical.MSet.ExplicitWithRepetition.rule_Comprehension
1465
1466 , Vertical.Function.Function1D.rule_Comprehension
1467 , Vertical.Function.Function1D.rule_Comprehension_Defined
1468 , Vertical.Function.Function1D.rule_Image
1469
1470 , Vertical.Function.Function1DPartial.rule_Comprehension
1471 , Vertical.Function.Function1DPartial.rule_PowerSet_Comprehension
1472 , Vertical.Function.Function1DPartial.rule_Image_NotABool
1473 , Vertical.Function.Function1DPartial.rule_Image_Bool
1474 , Vertical.Function.Function1DPartial.rule_InDefined
1475 , Vertical.Function.Function1DPartial.rule_DefinedEqDefined
1476
1477 , Vertical.Function.FunctionND.rule_Comprehension
1478 , Vertical.Function.FunctionND.rule_Comprehension_Defined
1479 , Vertical.Function.FunctionND.rule_Image
1480
1481 , Vertical.Function.FunctionNDPartial.rule_Comprehension
1482 , Vertical.Function.FunctionNDPartial.rule_Image_NotABool
1483 , Vertical.Function.FunctionNDPartial.rule_Image_Bool
1484 , Vertical.Function.FunctionNDPartial.rule_InDefined
1485
1486 , Vertical.Function.FunctionNDPartialDummy.rule_Comprehension
1487 , Vertical.Function.FunctionNDPartialDummy.rule_Image
1488 , Vertical.Function.FunctionNDPartialDummy.rule_InDefined
1489
1490 , Vertical.Function.FunctionAsRelation.rule_Comprehension
1491 -- , Vertical.Function.FunctionAsRelation.rule_PowerSet_Comprehension
1492 , Vertical.Function.FunctionAsRelation.rule_Image_Eq
1493 , Vertical.Function.FunctionAsRelation.rule_InDefined
1494 , Vertical.Function.FunctionAsRelation.rule_InToSet
1495
1496 , Vertical.Sequence.ExplicitBounded.rule_Comprehension
1497 , Vertical.Sequence.ExplicitBounded.rule_Card
1498 , Vertical.Sequence.ExplicitBounded.rule_Image_Bool
1499 , Vertical.Sequence.ExplicitBounded.rule_Image_NotABool
1500 , Vertical.Sequence.ExplicitBounded.rule_Leq
1501 , Vertical.Sequence.ExplicitBounded.rule_Lt
1502
1503 , Vertical.Relation.RelationAsMatrix.rule_Comprehension
1504 , Vertical.Relation.RelationAsMatrix.rule_Image
1505
1506 , Vertical.Relation.RelationAsSet.rule_Comprehension
1507 , Vertical.Relation.RelationAsSet.rule_PowerSet_Comprehension
1508 , Vertical.Relation.RelationAsSet.rule_Card
1509 , Vertical.Relation.RelationAsSet.rule_In
1510
1511 , Vertical.Partition.PartitionAsSet.rule_Comprehension
1512 , Vertical.Partition.Occurrence.rule_Comprehension
1513
1514 ]
1515
1516 horizontalRules :: [Rule]
1517 horizontalRules =
1518 [ Horizontal.Set.rule_Comprehension_Literal
1519 , Horizontal.Set.rule_Eq
1520 , Horizontal.Set.rule_Neq
1521 , Horizontal.Set.rule_Subset
1522 , Horizontal.Set.rule_SubsetEq
1523 , Horizontal.Set.rule_Supset
1524 , Horizontal.Set.rule_SupsetEq
1525 , Horizontal.Set.rule_In
1526 , Horizontal.Set.rule_Card
1527 , Horizontal.Set.rule_CardViaFreq
1528 , Horizontal.Set.rule_Intersect
1529 , Horizontal.Set.rule_Union
1530 , Horizontal.Set.rule_Difference
1531 , Horizontal.Set.rule_PowerSet_Comprehension
1532 , Horizontal.Set.rule_PowerSet_Difference
1533 , Horizontal.Set.rule_MaxMin
1534
1535 , Horizontal.MSet.rule_Comprehension_Literal
1536 , Horizontal.MSet.rule_Freq_toMSet_Flatten
1537 , Horizontal.MSet.rule_Comprehension_ToSet_Literal
1538 , Horizontal.MSet.rule_Eq
1539 , Horizontal.MSet.rule_Neq
1540 , Horizontal.MSet.rule_Subset
1541 , Horizontal.MSet.rule_SubsetEq
1542 , Horizontal.MSet.rule_Supset
1543 , Horizontal.MSet.rule_SupsetEq
1544 , Horizontal.MSet.rule_Freq
1545 , Horizontal.MSet.rule_In
1546 , Horizontal.MSet.rule_Card
1547 , Horizontal.MSet.rule_MaxMin
1548
1549 , Horizontal.Function.rule_Comprehension_Literal
1550 , Horizontal.Function.rule_Image_Bool
1551 , Horizontal.Function.rule_Image_BoolMatrixIndexed
1552 , Horizontal.Function.rule_Image_BoolTupleIndexed
1553 , Horizontal.Function.rule_Image_Int
1554 , Horizontal.Function.rule_Image_IntMatrixIndexed
1555 , Horizontal.Function.rule_Image_IntTupleIndexed
1556 , Horizontal.Function.rule_Image_Matrix_LexLhs
1557 , Horizontal.Function.rule_Image_Matrix_LexRhs
1558
1559 , Horizontal.Function.rule_Comprehension_Image
1560 , Horizontal.Function.rule_Comprehension_ImageSet
1561 , Horizontal.Function.rule_Eq
1562 , Horizontal.Function.rule_Neq
1563 , Horizontal.Function.rule_Subset
1564 , Horizontal.Function.rule_SubsetEq
1565 , Horizontal.Function.rule_Supset
1566 , Horizontal.Function.rule_SupsetEq
1567 , Horizontal.Function.rule_Inverse
1568 , Horizontal.Function.rule_Card
1569 , Horizontal.Function.rule_Comprehension_PreImage
1570 , Horizontal.Function.rule_Comprehension_Defined
1571 , Horizontal.Function.rule_Comprehension_Range
1572 , Horizontal.Function.rule_In
1573 , Horizontal.Function.rule_Restrict_Image
1574 , Horizontal.Function.rule_Restrict_Comprehension
1575 , Horizontal.Function.rule_Comprehension_Defined_Size
1576 , Horizontal.Function.rule_Comprehension_Range_Size
1577 , Horizontal.Function.rule_Defined_Intersect
1578 , Horizontal.Function.rule_DefinedOrRange_Union
1579 , Horizontal.Function.rule_DefinedOrRange_Difference
1580
1581 , Horizontal.Sequence.rule_Comprehension_Literal
1582 , Horizontal.Sequence.rule_Image_Bool
1583 , Horizontal.Sequence.rule_Image_Int
1584 , Horizontal.Sequence.rule_Comprehension_Image
1585 , Horizontal.Sequence.rule_Image_Literal_Bool
1586 , Horizontal.Sequence.rule_Image_Literal_Int
1587 , Horizontal.Sequence.rule_Eq_Literal
1588 , Horizontal.Sequence.rule_Eq
1589 , Horizontal.Sequence.rule_Eq_Comprehension
1590 , Horizontal.Sequence.rule_Neq
1591 , Horizontal.Sequence.rule_Subset
1592 , Horizontal.Sequence.rule_SubsetEq
1593 , Horizontal.Sequence.rule_Supset
1594 , Horizontal.Sequence.rule_SupsetEq
1595 , Horizontal.Sequence.rule_Card
1596 , Horizontal.Sequence.rule_Comprehension_PreImage
1597 , Horizontal.Sequence.rule_Comprehension_Defined
1598 , Horizontal.Sequence.rule_Comprehension_Range
1599 , Horizontal.Sequence.rule_In
1600 , Horizontal.Sequence.rule_Restrict_Image
1601 , Horizontal.Sequence.rule_Restrict_Comprehension
1602 , Horizontal.Sequence.rule_Substring
1603 , Horizontal.Sequence.rule_Subsequence
1604
1605 , Horizontal.Relation.rule_Comprehension_Literal
1606 , Horizontal.Relation.rule_Comprehension_Projection
1607 , Horizontal.Relation.rule_PowerSet_Comprehension
1608 , Horizontal.Relation.rule_Image
1609 , Horizontal.Relation.rule_In
1610 , Horizontal.Relation.rule_Eq
1611 , Horizontal.Relation.rule_Neq
1612 , Horizontal.Relation.rule_Subset
1613 , Horizontal.Relation.rule_SubsetEq
1614 , Horizontal.Relation.rule_Supset
1615 , Horizontal.Relation.rule_SupsetEq
1616 , Horizontal.Relation.rule_Card
1617
1618 , Horizontal.Partition.rule_Comprehension_Literal
1619 , Horizontal.Partition.rule_Eq
1620 , Horizontal.Partition.rule_Neq
1621 , Horizontal.Partition.rule_Together
1622 , Horizontal.Partition.rule_Apart
1623 , Horizontal.Partition.rule_Party
1624 , Horizontal.Partition.rule_Participants
1625 , Horizontal.Partition.rule_Card
1626 , Horizontal.Partition.rule_In
1627
1628 ]
1629
1630
1631 bubbleUpRules :: [[Rule]]
1632 bubbleUpRules =
1633 [
1634 [ BubbleUp.rule_MergeNested
1635 , BubbleUp.rule_ToAnd
1636 , BubbleUp.rule_ToMultiply_HeadOfIntComprehension
1637 , BubbleUp.rule_ConditionInsideGeneratorDomain
1638 , BubbleUp.rule_LiftVars
1639 ]
1640 ,
1641 [ BubbleUp.rule_NotBoolYet
1642 ]
1643 ]
1644
1645
1646 otherRules :: [[Rule]]
1647 otherRules =
1648 [
1649 [ rule_Xor_To_Sum ]
1650 ,
1651 [ TildeOrdering.rule_BoolInt
1652 , TildeOrdering.rule_MSet
1653 , TildeOrdering.rule_ViaMSet
1654 , TildeOrdering.rule_TildeLeq
1655 ]
1656 ,
1657 [ DontCare.rule_Bool
1658 , DontCare.rule_Int
1659 , DontCare.rule_Tuple
1660 , DontCare.rule_Record
1661 , DontCare.rule_Variant
1662 , DontCare.rule_Matrix
1663 , DontCare.rule_Abstract
1664 ]
1665 ,
1666 [ rule_TrueIsNoOp
1667 , rule_FlattenOf1D
1668 , rule_Decompose_AllDiff
1669 , rule_Decompose_AllDiff_MapToSingleInt
1670
1671 , rule_GeneratorsFirst
1672 ]
1673 ,
1674 [ rule_DomainCardinality
1675 , rule_DomainMinMax
1676
1677 , rule_ComplexAbsPat
1678
1679 , rule_AttributeToConstraint
1680
1681 , rule_QuantifierShift
1682 , rule_QuantifierShift2
1683 , rule_QuantifierShift3
1684
1685 ]
1686
1687 , [ rule_Comprehension_Simplify
1688 ]
1689
1690 , [ rule_InlineConditions
1691 , rule_InlineConditions_AllDiff
1692 , rule_InlineConditions_MaxMin
1693 ]
1694 ]
1695
1696 -- | These rules depend on other rules firing first.
1697 delayedRules :: [[Rule]]
1698 delayedRules =
1699 [
1700 [ Vertical.Matrix.rule_Comprehension_Singleton
1701 , Vertical.Matrix.rule_Comprehension_SingletonDomain
1702 , Vertical.Matrix.rule_Concatenate_Singleton
1703 , Vertical.Matrix.rule_MatrixIndexing
1704 ]
1705 , [ rule_ReducerToComprehension
1706 ]
1707 , [ rule_DotLtLeq
1708 , rule_Flatten_Lex
1709 ]
1710 ]
1711
1712
1713 rule_ChooseRepr :: (?typeCheckerMode :: TypeCheckerMode) => Config -> Rule
1714 rule_ChooseRepr config = Rule "choose-repr" (const theRule) where
1715
1716 theRule (Reference nm (Just (DeclNoRepr forg _ inpDom region))) | forg `elem` [Find, Given, CutFind] = do
1717 let reprsWhichOrder
1718 | (forg, representationsGivens config) == (Given, Sparse) = reprsSparseOrder
1719 | (forg, representationsFinds config) == (Find , Sparse) = reprsSparseOrder
1720 | representationLevels config == False = reprsStandardOrderNoLevels
1721 | otherwise = reprsStandardOrder
1722 domOpts <- reprOptions reprsWhichOrder inpDom
1723 when (null domOpts) $
1724 bug $ "No representation matches this beast:" <++> pretty inpDom
1725 let options =
1726 [ RuleResult { ruleResultDescr = msg
1727 , ruleResultType = case forg of
1728 Find -> ChooseRepr_Find nm
1729 Given -> ChooseRepr_Given nm
1730 CutFind -> ChooseRepr_Cut nm
1731 _ -> bug "rule_ChooseRepr ruleResultType"
1732 , ruleResult = return out
1733 , ruleResultHook = Just hook
1734 }
1735 | thisDom <- domOpts
1736 , let msg = "Choosing representation for" <+> pretty nm <> ":" <++> pretty thisDom
1737 , let out = Reference nm (Just (DeclHasRepr forg nm thisDom))
1738 , let hook = mkHook (channelling config) forg nm thisDom region
1739 ]
1740 return options
1741 theRule _ = na "rule_ChooseRepr"
1742
1743 mkHook
1744 :: ( MonadLog m
1745 , MonadFail m
1746 , MonadFailDoc m
1747 , NameGen m
1748 , EnumerateDomain m
1749 )
1750 => Bool
1751 -> FindOrGiven
1752 -> Name
1753 -> Domain HasRepresentation Expression
1754 -> Region
1755 -> Model
1756 -> m Model
1757 mkHook useChannelling -- whether to use channelling or not
1758 forg -- find or given
1759 name -- name of the original declaration
1760 domain -- domain with representation selected
1761 region -- the region of the Reference we are working on
1762 model = do
1763 let
1764
1765 representations = model |> mInfo |> miRepresentations
1766 representationsTree = model |> mInfo |> miRepresentationsTree
1767 |> concatMap (\ (n, ds) -> map (n,) ds )
1768
1769 usedBefore = (name, reprTree domain) `elem` representationsTree
1770
1771 mkStructurals :: (MonadLog m, MonadFailDoc m, NameGen m, EnumerateDomain m)
1772 => m [Expression]
1773 mkStructurals = do
1774 let ref = Reference name (Just (DeclHasRepr forg name domain))
1775 logDebugVerbose $ "Generating structural constraints for:" <+> vcat [pretty ref, pretty domain]
1776 structurals <- getStructurals downX1 domain >>= \ gen -> gen ref
1777 logDebugVerbose $ "Before name resolution:" <+> vcat (map pretty structurals)
1778 resolved <- mapM resolveNamesX structurals -- re-resolving names
1779 logDebugVerbose $ "After name resolution:" <+> vcat (map pretty resolved)
1780 return resolved
1781
1782 addStructurals :: (MonadLog m, MonadFailDoc m, NameGen m, EnumerateDomain m)
1783 => Model -> m Model
1784 addStructurals
1785 | forg == Given = return
1786 | usedBefore = return
1787 | otherwise = \ m -> do
1788 structurals <- mkStructurals
1789 return $ if null structurals
1790 then m
1791 else m { mStatements = mStatements m ++ [SuchThat structurals] }
1792
1793 channels =
1794 [ make opEq this that
1795 | (n, d) <- representations
1796 , n == name
1797 , let this = Reference name (Just (DeclHasRepr forg name domain))
1798 , let that = Reference name (Just (DeclHasRepr forg name d))
1799 ]
1800
1801 addChannels
1802 | forg == Given = return
1803 | usedBefore = return
1804 | null channels = return
1805 | otherwise = \ m -> return
1806 m { mStatements = mStatements m ++ [SuchThat channels] }
1807
1808 recordThis
1809 | usedBefore = return
1810 | otherwise = \ m ->
1811 let
1812 oldInfo = mInfo m
1813 newInfo = oldInfo
1814 { miRepresentations = representations ++ [(name, domain)]
1815 , miRepresentationsTree = (representationsTree ++ [(name, reprTree domain)])
1816 |> sortBy (comparing fst)
1817 |> groupBy ((==) `on` fst)
1818 |> mapMaybe (\ grp -> case grp of [] -> Nothing ; (x:_) -> Just (fst x, map snd grp) )
1819 }
1820 in return m { mInfo = newInfo }
1821
1822 fixReprForAllOthers
1823 | useChannelling = return -- no-op, if channelling=yes
1824 | otherwise = \ m ->
1825 let
1826 f (Reference nm _)
1827 | nm == name
1828 = Reference nm (Just (DeclHasRepr forg name domain))
1829 f x = x
1830 in
1831 return m { mStatements = transformBi f (mStatements m) }
1832
1833 fixReprForSameRegion
1834 | region == NoRegion = return -- no-op, if we aren't in a particular region
1835 | otherwise = \ m ->
1836 let
1837 f (Reference nm (Just (DeclNoRepr _ _ _ region')))
1838 | nm == name
1839 , region' == region
1840 = Reference nm (Just (DeclHasRepr forg name domain))
1841 f x = x
1842 in
1843 return m { mStatements = transformBi f (mStatements m) }
1844
1845
1846 logDebugVerbose $ vcat
1847 [ "Name :" <+> pretty name
1848 , "Previously :" <+> vcat [ pretty (show d) | (n,d) <- representations, n == name ]
1849 , "This guy :" <+> pretty (show domain)
1850 , "usedBefore? :" <+> pretty usedBefore
1851 ]
1852
1853 return model
1854 >>= addStructurals -- unless usedBefore: add structurals
1855 >>= addChannels -- for each in previously recorded representation
1856 >>= recordThis -- unless usedBefore: record (name, domain) as being used in the model
1857 >>= fixReprForAllOthers -- fix the representation of this guy in the whole model, if channelling=no
1858 >>= fixReprForSameRegion -- fix the representation of this guy in the whole model,
1859 -- for those references with the same "region"
1860 >>= resolveNames -- we need to re-resolve names to avoid repeatedly selecting representations
1861 -- for abstract stuff inside aliases.
1862
1863
1864 rule_ChooseReprForComprehension :: Config -> Rule
1865 rule_ChooseReprForComprehension config = Rule "choose-repr-for-comprehension" (const theRule) where
1866
1867 theRule (Comprehension body gensOrConds) = do
1868 (gocBefore, (nm, domain), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
1869 Generator (GenDomainNoRepr (Single nm) domain) -> return (nm, domain)
1870 _ -> na "rule_ChooseReprForComprehension"
1871
1872 let reprsWhichOrder
1873 | representationsGivens config == Sparse = reprsSparseOrder
1874 | representationLevels config == False = reprsStandardOrderNoLevels
1875 | otherwise = reprsStandardOrder
1876 domOpts <- reprOptions reprsWhichOrder domain
1877 when (null domOpts) $
1878 bug $ "No representation matches this beast:" <++> pretty domain
1879
1880 return
1881 [ RuleResult
1882 { ruleResultDescr = "Choosing representation for quantified variable" <+>
1883 pretty nm <> ":" <++> pretty thisDom
1884 , ruleResultType = ChooseRepr_Quantified
1885 , ruleResult = bugFailT "rule_ChooseReprForComprehension" $ do
1886 outDomains <- downD (nm, thisDom)
1887 structurals <- mkStructurals nm thisDom
1888 let updateRepr (Reference nm' _)
1889 | nm == nm'
1890 = Reference nm (Just (DeclHasRepr Quantified nm thisDom))
1891 updateRepr p = p
1892 let out' = Comprehension (transform updateRepr body)
1893 $ gocBefore
1894 ++ [ Generator (GenDomainHasRepr name dom)
1895 | (name, dom) <- outDomains ]
1896 ++ map Condition structurals
1897 ++ transformBi updateRepr gocAfter
1898 out <- resolveNamesX out'
1899 return out
1900 , ruleResultHook = Nothing
1901 }
1902 | thisDom <- domOpts
1903 ]
1904 theRule _ = na "rule_ChooseReprForComprehension"
1905
1906 mkStructurals name domain = do
1907 let ref = Reference name (Just (DeclHasRepr Quantified name domain))
1908 gen <- getStructurals downX1 domain
1909 gen ref
1910
1911
1912 rule_ChooseReprForLocals :: Config -> Rule
1913 rule_ChooseReprForLocals config = Rule "choose-repr-for-locals" (const theRule) where
1914
1915 theRule (WithLocals body (AuxiliaryVars locals)) = do
1916 (stmtBefore, (nm, domain), stmtAfter) <- matchFirst locals $ \ local -> case local of
1917 Declaration (FindOrGiven LocalFind nm domain) -> return (nm, domain)
1918 _ -> na "rule_ChooseReprForLocals"
1919
1920 let
1921 isReferencedWithoutRepr (Reference nm' (Just DeclNoRepr{})) | nm == nm' = True
1922 isReferencedWithoutRepr _ = False
1923
1924 unless (any isReferencedWithoutRepr (universeBi (body, stmtBefore, stmtAfter))) $
1925 na $ "This local variable seems to be handled before:" <+> pretty nm
1926
1927 let reprsWhichOrder
1928 | representationsAuxiliaries config == Sparse = reprsSparseOrder
1929 | representationLevels config == False = reprsStandardOrderNoLevels
1930 | otherwise = reprsStandardOrder
1931 domOpts <- reprOptions reprsWhichOrder domain
1932 when (null domOpts) $
1933 bug $ "No representation matches this beast:" <++> pretty domain
1934
1935 return
1936 [ RuleResult
1937 { ruleResultDescr = "Choosing representation for auxiliary variable" <+>
1938 pretty nm <> ":" <++> pretty thisDom
1939 , ruleResultType = ChooseRepr_Auxiliary
1940 , ruleResult = bugFailT "rule_ChooseReprForLocals" $ do
1941 outDomains <- downD (nm, thisDom)
1942 structurals <- mkStructurals nm thisDom
1943 let updateRepr (Reference nm' _)
1944 | nm == nm'
1945 = Reference nm (Just (DeclHasRepr LocalFind nm thisDom))
1946 updateRepr p = p
1947 let out' = WithLocals (transform updateRepr body) $ AuxiliaryVars
1948 ( stmtBefore
1949 ++ [ Declaration (FindOrGiven
1950 LocalFind
1951 name
1952 (forgetRepr dom))
1953 | (name, dom) <- outDomains ]
1954 ++ [ SuchThat structurals | not (null structurals) ]
1955 ++ transformBi updateRepr stmtAfter
1956 )
1957 out <- resolveNamesX out'
1958 return out
1959 , ruleResultHook = Nothing
1960 }
1961 | thisDom <- domOpts
1962 ]
1963 theRule _ = na "rule_ChooseReprForLocals"
1964
1965 mkStructurals name domain = do
1966 let ref = Reference name (Just (DeclHasRepr LocalFind name domain))
1967 gen <- getStructurals downX1 domain
1968 gen ref
1969
1970
1971 rule_GeneratorsFirst :: Rule
1972 rule_GeneratorsFirst = "generators-first" `namedRule` theRule where
1973 theRule (Comprehension body [])
1974 = return
1975 ( "Empty generators."
1976 , return $ AbstractLiteral $ AbsLitMatrix (mkDomainIntB 1 1) [body]
1977 )
1978 theRule (Comprehension body gensOrConds)
1979 | let (gens, rest) = mconcat
1980 [ case x of
1981 Generator{} -> ([x],[])
1982 _ -> ([],[x])
1983 | x <- gensOrConds
1984 ]
1985 , let gensOrConds' = gens ++ rest
1986 , gensOrConds /= gensOrConds'
1987 = return
1988 ( "Generators come first."
1989 , return $ Comprehension body gensOrConds'
1990 )
1991 theRule (Comprehension body gensOrConds)
1992 | let (lettings :: [Name], rest :: [GeneratorOrCondition]) = mconcat
1993 [ case x of
1994 ComprehensionLetting pat _ -> (universeBi pat,[] )
1995 _ -> ([] ,[x])
1996 | x <- gensOrConds
1997 ]
1998 , let f (Reference nm (Just (Alias x))) | nm `elem` lettings = f x
1999 f x = x
2000 , not (null lettings)
2001 = return
2002 ( "Inlining comprehension lettings."
2003 , return $ transformBi f $ Comprehension body rest
2004 )
2005 theRule _ = na "rule_GeneratorsFirst"
2006
2007
2008 rule_Eq :: Rule
2009 rule_Eq = "identical-domain-eq" `namedRule` theRule where
2010 theRule p = do
2011 (x,y) <- match opEq p
2012 domX <- domainOf x
2013 domY <- domainOf y
2014 unless (domX == domY) $ na "rule_Eq domains not identical"
2015 sameRepresentationTree x y
2016 xs <- downX x
2017 ys <- downX y
2018 unless (length xs == length ys) $ na "rule_Eq"
2019 when (xs == [x]) $ na "rule_Eq"
2020 when (ys == [y]) $ na "rule_Eq"
2021 return
2022 ( "Generic vertical rule for identical-domain equality"
2023 , return $ make opAnd $ fromList $ zipWith (\ i j -> [essence| &i = &j |] ) xs ys
2024 )
2025
2026
2027 rule_Neq :: Rule
2028 rule_Neq = "identical-domain-neq" `namedRule` theRule where
2029 theRule p = do
2030 (x,y) <- match opNeq p
2031 domX <- domainOf x
2032 domY <- domainOf y
2033 unless (domX == domY) $ na "rule_Neq domains not identical"
2034 sameRepresentationTree x y
2035 xs <- downX x
2036 ys <- downX y
2037 unless (length xs == length ys) $ na "rule_Neq"
2038 when (xs == [x]) $ na "rule_Neq"
2039 when (ys == [y]) $ na "rule_Neq"
2040 return
2041 ( "Generic vertical rule for identical-domain equality"
2042 , return $ make opOr $ fromList $ zipWith (\ i j -> [essence| &i != &j |] ) xs ys
2043 )
2044
2045
2046 rule_DotLtLeq :: Rule
2047 rule_DotLtLeq = "generic-DotLtLeq" `namedRule` theRule where
2048 theRule p = do
2049 (a,b,mk) <- case p of
2050 [essence| &a .< &b |] -> return ( a, b, \ i j -> [essence| &i <lex &j |] )
2051 [essence| &a .<= &b |] -> return ( a, b, \ i j -> [essence| &i <=lex &j |] )
2052 _ -> na "rule_DotLtLeq"
2053 ma <- symmetryOrdering a
2054 mb <- symmetryOrdering b
2055 return
2056 ( "Generic vertical rule for dotLt and dotLeq:" <+> pretty p
2057 , return $ mk ma mb
2058 )
2059
2060
2061 rule_Flatten_Lex :: Rule
2062 rule_Flatten_Lex = "flatten-lex" `namedRule` theRule where
2063 theRule [essence| &a <lex &b |] = do
2064 reject_flat a b
2065 fa <- flatten a
2066 fb <- flatten b
2067 tfa <- typeOf fa
2068 tfb <- typeOf fb
2069 case (tfa, tfb) of
2070 (TypeList TypeInt{}, TypeList TypeInt{}) -> return ()
2071 (TypeMatrix TypeInt{} TypeInt{}, TypeMatrix TypeInt{} TypeInt{}) -> return ()
2072 _ -> bug $ "flattener: " <+> vcat [stringToDoc $ show tfa, stringToDoc $ show tfb]
2073 return ( "Flatten Lex less"
2074 , return [essence| &fa <lex &fb |]
2075 )
2076 theRule [essence| &a <=lex &b |] = do
2077 reject_flat a b
2078 fa <- flatten a
2079 fb <- flatten b
2080 tfa <- typeOf fa
2081 tfb <- typeOf fb
2082 case (tfa, tfb) of
2083 (TypeList TypeInt{}, TypeList TypeInt{}) -> return ()
2084 (TypeMatrix TypeInt{} TypeInt{}, TypeMatrix TypeInt{} TypeInt{}) -> return ()
2085 _ -> bug $ "flattener: " <+> vcat [stringToDoc $ show tfa, stringToDoc $ show tfb]
2086 return ( "Flatten Lex Lt"
2087 , return [essence| &fa <=lex &fb |]
2088 )
2089 theRule _ = na "rule_Flatten_Lex"
2090 reject_flat a b = do
2091 ta <- typeOf a
2092 tb <- typeOf b
2093 case (ta, tb) of
2094 (TypeMatrix TypeBool TypeInt{}, _) ->
2095 na "rule_Flatten_Lex"
2096 (TypeMatrix TypeBool TypeBool, _) ->
2097 na "rule_Flatten_Lex"
2098 (TypeList TypeInt{}, _) ->
2099 na "rule_Flatten_Lex"
2100 (TypeMatrix TypeInt{} TypeInt{}, _) ->
2101 na "rule_Flatten_Lex"
2102 (TypeList TypeBool, _) ->
2103 na "rule_Flatten_Lex"
2104 (TypeMatrix TypeInt{} TypeBool, _) ->
2105 na "rule_Flatten_Lex"
2106 _ -> return ()
2107
2108 flatten a = do
2109 ta <- typeOf a
2110 case ta of
2111 TypeBool -> return [essence| [-toInt(&a)] |]
2112 TypeInt{} -> return [essence| [&a] |]
2113 TypeList TypeInt{} -> return a
2114 TypeMatrix TypeInt{} TypeInt{} -> return a
2115 TypeTuple ts -> do
2116 case a of
2117 AbstractLiteral x -> do
2118 case x of
2119 AbsLitTuple xs -> do
2120 fxs <- sequence (flatten <$> xs)
2121 let flatxs = fromList fxs
2122 return [essence| flatten(&flatxs) |]
2123 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this abslit fellow..."
2124 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2125 Constant c ->
2126 case c of
2127 ConstantAbstract ca ->
2128 case ca of
2129 AbsLitTuple xs -> do
2130 fxs <- sequence (flatten <$> (Constant <$> xs))
2131 let flatxs = fromList fxs
2132 return [essence| flatten(&flatxs) |]
2133 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2134 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2135 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2136 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2137 Op _ -> do
2138 (oName, o) <- quantifiedVar
2139 flatten $ Comprehension o [ComprehensionLetting oName a]
2140 _ -> do
2141 ps <- sequence $ (\(i,_) -> do
2142 (Single nm, tm) <- quantifiedVar
2143 return (i,nm,tm)) <$> (zip [1..] ts)
2144 let lts = (\(i,nm,_tm) -> ComprehensionLetting (Single nm) [essence| &a[&i] |]) <$> ps
2145 tup = AbstractLiteral $ AbsLitTuple $ (\(_,_,tm) -> tm) <$> ps
2146 flatten $ Comprehension tup lts
2147 _ ->
2148 case a of
2149 AbstractLiteral x -> do
2150 case x of
2151 AbsLitMatrix _ xs -> do
2152 fxs <- sequence (flatten <$> xs)
2153 let flatxs = fromList fxs
2154 return [essence| flatten(&flatxs) |]
2155 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this abslit fellow..."
2156 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2157 Constant c ->
2158 case c of
2159 ConstantAbstract ca ->
2160 case ca of
2161 AbsLitMatrix _ [] ->
2162 return [essence| ([] : `matrix indexed by [int()] of int`) |]
2163 AbsLitMatrix _ xs -> do
2164 fxs <- sequence (flatten <$> (Constant <$> xs))
2165 let flatxs = fromList fxs
2166 return [essence| flatten(&flatxs) |]
2167 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2168 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2169 TypedConstant tc _ -> flatten (Constant tc)
2170 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2171 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2172 Op _ -> do
2173 (oName, o) <- quantifiedVar
2174 flatten $ Comprehension o [ComprehensionLetting oName a]
2175 Reference nm ex ->
2176 bug $ "rule_FlattenLex: flatten isn't defined for this reference fellow..."
2177 <+> vcat [stringToDoc (show a)
2178 ,"reference:" <+> stringToDoc (show nm)
2179 ,"fellow:" <+> stringToDoc (show ex)]
2180 Comprehension body gocs -> do
2181 fbody <- flatten body
2182 let comp = Comprehension fbody gocs
2183 return [essence| flatten(&comp) |]
2184 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this expression fellow..."
2185
2186 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2187
2188
2189 rule_ReducerToComprehension :: Rule
2190 rule_ReducerToComprehension = "reducer-to-comprehension" `namedRule` theRule where
2191 theRule p = do
2192 (_, _, mk, coll) <- match opReducer p
2193 -- leave comprehensions alone
2194 let
2195 isComprehension Comprehension{} = True
2196 isComprehension _ = False
2197 case followAliases isComprehension coll of
2198 True -> na "rule_ReducerToComprehension"
2199 False -> return ()
2200 -- leave matrix literals alone
2201 case tryMatch matrixLiteral coll of
2202 Nothing -> return ()
2203 Just {} -> na "rule_ReducerToComprehension"
2204 tyColl <- typeOf coll
2205 howToIndex <- case tyColl of
2206 TypeSequence{} -> return $ Left ()
2207 TypeMatrix{} -> return $ Right ()
2208 TypeList{} -> return $ Right ()
2209 TypeSet{} -> return $ Right ()
2210 TypeMSet{} -> return $ Right ()
2211 _ -> na "rule_ReducerToComprehension"
2212 return
2213 ( "Creating a comprehension for the collection inside the reducer operator."
2214 , do
2215 (iPat, i) <- quantifiedVar
2216 case howToIndex of
2217 Left{} -> return $ mk [essence| [ &i[2] | &iPat <- &coll ] |]
2218 Right{} -> return $ mk [essence| [ &i | &iPat <- &coll ] |]
2219 )
2220
2221
2222 rule_TrueIsNoOp :: Rule
2223 rule_TrueIsNoOp = "true-is-noop" `namedRule` theRule where
2224 theRule (Op (MkOpTrue (OpTrue ref))) =
2225 case ref of
2226 Reference _ (Just DeclHasRepr{}) ->
2227 return ( "Remove the argument from true."
2228 , return $ Constant $ ConstantBool True
2229 )
2230 _ -> na "The argument of true doesn't have a representation."
2231 theRule _ = na "rule_TrueIsNoOp"
2232
2233
2234 rule_FlattenOf1D :: Rule
2235 rule_FlattenOf1D = "flatten-of-1D" `namedRule` theRule where
2236 theRule p = do
2237 x <- match opFlatten p
2238 tyx <- typeOf x
2239 out <- case tyx of
2240 TypeList TypeBool{} -> return x
2241 TypeList TypeInt{} -> return x
2242 TypeMatrix _ TypeBool{} -> return x
2243 TypeMatrix _ TypeInt{} -> return x
2244 TypeMatrix{} -> -- more than 1D
2245 case listOut x of
2246 Just [y] -> return (make opFlatten y)
2247 _ -> na "rule_FlattenOf1D"
2248 _ -> na "rule_FlattenOf1D"
2249 return ( "1D matrices do not need a flatten."
2250 , return out
2251 )
2252
2253
2254 rule_Decompose_AllDiff :: Rule
2255 rule_Decompose_AllDiff = "decompose-allDiff" `namedRule` theRule where
2256 theRule [essence| allDiff(&m) |] = do
2257 ty <- typeOf m
2258 case ty of
2259 TypeMatrix _ TypeBool -> na "allDiff can stay"
2260 TypeMatrix _ (TypeInt _) -> na "allDiff can stay"
2261 TypeMatrix _ _ -> return ()
2262 _ -> na "allDiff on something other than a matrix."
2263 index:_ <- indexDomainsOf m
2264 return
2265 ( "Decomposing allDiff. Type:" <+> pretty ty
2266 , do
2267 (iPat, i) <- quantifiedVar
2268 (jPat, j) <- quantifiedVar
2269 return
2270 [essence|
2271 and([ &m[&i] != &m[&j]
2272 | &iPat : &index
2273 , &jPat : &index
2274 , &i < &j
2275 ])
2276 |]
2277 )
2278 theRule _ = na "rule_Decompose_AllDiff"
2279
2280
2281 rule_Decompose_AllDiff_MapToSingleInt :: Rule
2282 rule_Decompose_AllDiff_MapToSingleInt = "decompose-allDiff-mapToSingleInt" `namedRule` theRule where
2283 theRule [essence| allDiff(&m) |] = do
2284 case m of
2285 Comprehension body gensOrConds -> do
2286 tyBody <- typeOf body
2287 case tyBody of
2288 TypeBool -> na "rule_Decompose_AllDiff_MapToSingleInt"
2289 TypeInt _ -> na "rule_Decompose_AllDiff_MapToSingleInt"
2290 TypeTuple{} -> do
2291 bodyBits <- downX1 body
2292 bodyBitSizes <- forM bodyBits $ \ b -> do
2293 bDomain <- domainOf b
2294 domainSizeOf bDomain
2295 case (bodyBits, bodyBitSizes) of
2296 ([a,b], [_a',b']) -> do
2297 let body'= [essence| &a * &b' + &b |]
2298 let m' = Comprehension body' gensOrConds
2299 return
2300 ( "Decomposing allDiff"
2301 , return [essence| allDiff(&m') |]
2302 )
2303 _ -> na "rule_Decompose_AllDiff_MapToSingleInt"
2304 _ -> na "allDiff on something other than a comprehension."
2305 _ -> na "allDiff on something other than a comprehension."
2306 theRule _ = na "rule_Decompose_AllDiff_MapToSingleInt"
2307
2308
2309 rule_DomainCardinality :: Rule
2310 rule_DomainCardinality = "domain-cardinality" `namedRule` theRule where
2311 theRule p = do
2312 maybeDomain <- match opTwoBars p
2313 d <- expandDomainReference <$> case maybeDomain of
2314 Domain d -> return d
2315 Reference _ (Just (Alias (Domain d))) -> return d
2316 _ -> na "rule_DomainCardinality"
2317 return
2318 ( "Cardinality of a domain"
2319 , case d of
2320 DomainInt _ [RangeBounded 1 u] -> return u
2321 _ -> do
2322 (iPat, _) <- quantifiedVar
2323 return [essence| sum([ 1 | &iPat : &d ]) |]
2324 )
2325
2326
2327 rule_DomainMinMax :: Rule
2328 rule_DomainMinMax = "domain-MinMax" `namedRule` theRule where
2329 theRule [essence| max(&maybeDomain) |] = do
2330 d <- getDomain maybeDomain
2331 return
2332 ( "max of a domain"
2333 , maxOfDomain d
2334 )
2335 theRule [essence| min(&maybeDomain) |] = do
2336 d <- getDomain maybeDomain
2337 return
2338 ( "min of a domain"
2339 , minOfDomain d
2340 )
2341 theRule _ = na "rule_DomainMinMax"
2342
2343 getDomain :: MonadFailDoc m => Expression -> m (Domain () Expression)
2344 getDomain (Domain d) = return d
2345 getDomain (Reference _ (Just (Alias (Domain d)))) = getDomain (Domain d)
2346 getDomain _ = na "rule_DomainMinMax.getDomain"
2347
2348
2349 rule_ComplexAbsPat :: Rule
2350 rule_ComplexAbsPat = "complex-pattern" `namedRule` theRule where
2351 theRule (Comprehension body gensOrConds) = do
2352 (gocBefore, (pat, domainOrExpr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
2353 Generator (GenDomainNoRepr pat@AbsPatTuple{} domain) -> return (pat, Left domain)
2354 Generator (GenInExpr pat@AbsPatTuple{} expr) -> return (pat, Right expr)
2355 _ -> na "rule_ComplexAbsPat"
2356 return
2357 ( "complex pattern on tuple patterns"
2358 , do
2359 (iPat, i) <- quantifiedVar
2360 let replacements = [ (p, make opMatrixIndexing i (map (fromInt . fromIntegral) is))
2361 | (p, is) <- genMappings pat
2362 ]
2363 let f x@(Reference nm _) = fromMaybe x (lookup nm replacements)
2364 f x = x
2365 return $ Comprehension (transform f body)
2366 $ gocBefore
2367 ++ [ either (Generator . GenDomainNoRepr iPat)
2368 (Generator . GenInExpr iPat)
2369 domainOrExpr ]
2370 ++ transformBi f gocAfter
2371 )
2372 theRule _ = na "rule_ComplexAbsPat"
2373
2374 -- i --> i -> []
2375 -- (i,j) --> i -> [1]
2376 -- j -> [2]
2377 -- (i,(j,k)) --> i -> [1]
2378 -- j -> [2,1]
2379 -- k -> [2,2]
2380 genMappings :: AbstractPattern -> [(Name, [Int])]
2381 genMappings (Single nm) = [(nm, [])]
2382 genMappings (AbsPatTuple pats)
2383 = concat
2384 [ [ (patCore, i:is) | (patCore, is) <- genMappings pat ]
2385 | (i, pat) <- zip [1..] pats
2386 ]
2387 genMappings (AbsPatMatrix pats)
2388 = concat
2389 [ [ (patCore, i:is) | (patCore, is) <- genMappings pat ]
2390 | (i, pat) <- zip [1..] pats
2391 ]
2392 genMappings pat = bug ("rule_ComplexLambda.genMappings:" <+> pretty (show pat))
2393
2394
2395 -- this rule doesn't use `namedRule` because it need access to ascendants through the zipper
2396 rule_InlineConditions :: Rule
2397 rule_InlineConditions = Rule "inline-conditions" theRule where
2398 theRule z (Comprehension body gensOrConds) = do
2399 let (toInline, toKeep) = mconcat
2400 [ case goc of
2401 Condition x | categoryOf x == CatDecision -> ([x],[])
2402 _ -> ([],[goc])
2403 | goc <- gensOrConds
2404 ]
2405 theGuard <- case toInline of
2406 [] -> na "No condition to inline."
2407 [x] -> return x
2408 xs -> return $ make opAnd $ fromList xs
2409 (nameQ, opSkip) <- queryQ z
2410 let bodySkipped = opSkip theGuard body
2411 return
2412 [ RuleResult
2413 { ruleResultDescr = "Inlining conditions, inside" <+> nameQ
2414 , ruleResultType = ExpressionRefinement
2415 , ruleResult = return $ Comprehension bodySkipped toKeep
2416 , ruleResultHook = Nothing
2417 } ]
2418 theRule _ _ = na "rule_InlineConditions"
2419
2420 -- keep going up, until finding a quantifier
2421 -- when found, return the skipping operator for the quantifier
2422 -- if none exists, do not apply the rule.
2423 -- (or maybe we should call bug right ahead, it can't be anything else.)
2424 queryQ z0 =
2425 case Zipper.up z0 of
2426 Nothing -> na "rule_InlineConditions (meh-1)"
2427 Just z -> do
2428 let h = hole z
2429 case ( match opAnd h, match opOr h, match opSum h, match opProduct h
2430 , match opMin h, match opMax h, match opOrdering h ) of
2431 (Just{}, _, _, _, _, _, _) -> return ("and", opAndSkip)
2432 (_, Just{}, _, _, _, _, _) -> return ("or" , opOrSkip )
2433 (_, _, Just{}, _, _, _, _) -> return ("sum", opSumSkip)
2434 (_, _, _, Just{}, _, _, _) -> return ("product", opProductSkip)
2435 (_, _, _, _, Just{}, _, _) -> na "rule_InlineConditions (min)"
2436 (_, _, _, _, _, Just{}, _) -> na "rule_InlineConditions (max)"
2437 (_, _, _, _, _, _, Just{}) -> return ("ordering", opSumSkip)
2438 _ -> na "rule_InlineConditions (meh-2)"
2439 -- case Zipper.up z of
2440 -- Nothing -> na "queryQ"
2441 -- Just u -> queryQ u
2442
2443 opAndSkip b x = [essence| &b -> &x |]
2444 opOrSkip b x = [essence| &b /\ &x |]
2445 opSumSkip b x = [essence| toInt(&b) * catchUndef(&x, 0) |]
2446 opProductSkip b x = [essence| [ 1
2447 , catchUndef(&x,1)
2448 ; int(0..1)
2449 ] [toInt(&b)] |]
2450
2451
2452 rule_InlineConditions_AllDiff :: Rule
2453 rule_InlineConditions_AllDiff = "inline-conditions-allDiff" `namedRule` theRule where
2454 theRule (Op (MkOpAllDiff (OpAllDiff (Comprehension body gensOrConds)))) = do
2455 let (toInline, toKeep) = mconcat
2456 [ case goc of
2457 Condition x | categoryOf x == CatDecision -> ([x],[])
2458 _ -> ([],[goc])
2459 | goc <- gensOrConds
2460 ]
2461 theGuard <- case toInline of
2462 [] -> na "No condition to inline."
2463 [x] -> return x
2464 xs -> return $ make opAnd $ fromList xs
2465
2466 tyBody <- typeOf body
2467 case tyBody of
2468 TypeInt{} -> return ()
2469 _ -> na "rule_InlineConditions_AllDiff, not an int"
2470 domBody <- domainOf body
2471 let
2472 collectLowerBounds (RangeSingle x) = return x
2473 collectLowerBounds (RangeBounded x _) = return x
2474 collectLowerBounds _ = userErr1 ("Unexpected infinite domain:" <+> pretty domBody)
2475
2476 collectLowerBoundsD (DomainInt _ rs) = mapM collectLowerBounds rs
2477 collectLowerBoundsD _ = userErr1 ("Expected an integer domain, but got:" <+> pretty domBody)
2478
2479 bounds <- collectLowerBoundsD domBody
2480 let lowerBound = make opMin (fromList bounds)
2481
2482 -- for each element, we do element-lowerBound+1
2483 -- this makes sure the smallest element is 1
2484 -- hence we can use 0 as the except value!
2485 let bodySkipped = [essence| toInt(&theGuard) * catchUndef(&body + (1 - &lowerBound), 0) |]
2486
2487 return
2488 ( "Inlining conditions, inside allDiff"
2489 , return $ make opAllDiffExcept (Comprehension bodySkipped toKeep) 0
2490 )
2491 theRule _ = na "rule_InlineConditions_AllDiff"
2492
2493
2494 rule_InlineConditions_MaxMin :: Rule
2495 rule_InlineConditions_MaxMin = "aux-for-MaxMin" `namedRule` theRule where
2496 theRule p = do
2497 when (categoryOf p < CatDecision) $ na "rule_InlineConditions_MaxMin"
2498 (nameQ, binOp, Comprehension body gensOrConds) <-
2499 case (match opMax p, match opMin p) of
2500 (Just res, _) -> return ("max", \ a b -> [essence| &a <= &b |], res )
2501 (_, Just res) -> return ("min", \ a b -> [essence| &a >= &b |], res )
2502 _ -> na "rule_InlineConditions_MaxMin"
2503 let
2504 (toInline, gocInExpr, _toKeep) = mconcat
2505 [ case goc of
2506 Condition x | categoryOf x == CatDecision -> ([x],[],[])
2507 Generator (GenInExpr {}) -> ([],[goc],[])
2508 _ -> ([],[],[goc])
2509 | goc <- gensOrConds
2510 ]
2511 when (null toInline && null gocInExpr) $ na "rule_InlineConditions_MaxMin"
2512 auxDomain <- domainOf body
2513 return
2514 ( "Creating auxiliary variable for a" <+> nameQ
2515 , do
2516 (auxName, aux) <- auxiliaryVar
2517 let auxDefinedLHS = make opSum (Comprehension 1 gensOrConds)
2518 let auxDefined = [essence| &auxDefinedLHS > 0 |]
2519 let auxUndefined = [essence| &auxDefinedLHS = 0 |]
2520 let aux' = WithLocals aux (DefinednessConstraints [auxDefined])
2521 return $ WithLocals aux'
2522 (AuxiliaryVars
2523 [ Declaration (FindOrGiven LocalFind auxName auxDomain)
2524 , SuchThat
2525 [ make opAnd $ Comprehension
2526 (binOp body aux)
2527 gensOrConds
2528
2529 -- either one of the members of this comprehension, or dontCare
2530 -- if it is indeed dontCare, care should be taken to make sure it isn't used as a normal value
2531 , make opAnd $ fromList
2532 [ make opImply auxDefined
2533 (make opOr $ Comprehension
2534 [essence| &body = &aux |]
2535 gensOrConds)
2536 , make opImply auxUndefined (make opDontCare aux)
2537 ]
2538 ]
2539 ])
2540 )
2541
2542
2543 rule_AttributeToConstraint :: Rule
2544 rule_AttributeToConstraint = "attribute-to-constraint" `namedRule` theRule where
2545 theRule (Op (MkOpAttributeAsConstraint (OpAttributeAsConstraint thing attr mval))) = do
2546 dom <- domainOf thing
2547 let conv = mkAttributeToConstraint dom attr mval thing
2548 return
2549 ( "Converting an attribute to a constraint"
2550 , bugFailT "rule_AttributeToConstraint" conv
2551 )
2552 theRule _ = na "rule_AttributeToConstraint"
2553
2554
2555 timedF :: MonadIO m => String -> (a -> m b) -> a -> m b
2556 timedF name comp = \ a -> timeItNamed name (comp a)
2557
2558
2559 evaluateModel ::
2560 MonadFailDoc m =>
2561 NameGen m =>
2562 EnumerateDomain m =>
2563 (?typeCheckerMode :: TypeCheckerMode) =>
2564 Model -> m Model
2565 evaluateModel m = do
2566 let
2567 full (Reference _ (Just (DeclHasRepr _ _ (singletonDomainInt -> Just val)))) =
2568 return val
2569 full p@Constant{} = return p
2570 full p@Domain{} = return p
2571 full p = do
2572 mconstant <- runExceptT (instantiateExpression [] p)
2573 case mconstant of
2574 Left{} -> return p
2575 Right constant ->
2576 if null [() | ConstantUndefined{} <- universe constant] -- if there are no undefined values in it
2577 then return (Constant constant)
2578 else return p
2579 let
2580 partial (Op op)
2581 | Just (x, y) <- case op of
2582 MkOpLeq (OpLeq x y) -> Just (x,y)
2583 MkOpGeq (OpGeq x y) -> Just (x,y)
2584 MkOpEq (OpEq x y) -> Just (x,y)
2585 _ -> Nothing
2586 , Reference nmX _ <- x
2587 , Reference nmY _ <- y
2588 , nmX == nmY
2589 , categoryOf x <= CatQuantified
2590 , categoryOf y <= CatQuantified
2591 = return (fromBool True)
2592 partial p@(Op x) = do
2593 mx' <- runExceptT (simplifyOp x)
2594 case mx' of
2595 Left{} -> return p
2596 Right x' -> do
2597 when (Op x == x') $ bug $ vcat
2598 [ "rule_PartialEvaluate, simplifier returns the input unchanged."
2599 , "input:" <+> vcat [ pretty (Op x)
2600 , pretty (show (Op x))
2601 ]
2602 ]
2603 return x'
2604 partial p = return p
2605
2606 (descendBiM full >=> transformBiM partial) m
2607
2608
2609 rule_FullEvaluate :: Rule
2610 rule_FullEvaluate = "full-evaluate" `namedRule` theRule where
2611 theRule Constant{} = na "rule_FullEvaluate"
2612 theRule Domain{} = na "rule_FullEvaluate"
2613 theRule (Reference _ (Just (Alias x))) -- selectively inline, unless x is huge
2614 | Just Comprehension{} <- match opToSet x
2615 = return ("Inline alias", return x)
2616 theRule p = do
2617 constant <- instantiateExpression [] p
2618 unless (null [() | ConstantUndefined{} <- universe constant]) $
2619 na "rule_PartialEvaluate, undefined"
2620 return ("Full evaluator", return $ Constant constant)
2621
2622
2623 rule_PartialEvaluate :: Rule
2624 rule_PartialEvaluate = "partial-evaluate" `namedRuleZ` theRule where
2625 -- if a variable only has a single value in its domain, replace it with the value
2626 theRule z (Reference _ (Just (DeclHasRepr _ _ (singletonDomainInt -> Just val)))) =
2627 case hole <$> Zipper.up z of
2628 Just (Op (MkOpTrue _)) -> na "rule_PartialEvaluate, inside a true(ref)"
2629 _ -> return ( "Partial evaluator"
2630 , return val
2631 )
2632 theRule _ (Op op)
2633 | Just (x, y) <- case op of
2634 MkOpLeq (OpLeq x y) -> Just (x,y)
2635 MkOpGeq (OpGeq x y) -> Just (x,y)
2636 MkOpEq (OpEq x y) -> Just (x,y)
2637 _ -> Nothing
2638 , Reference nmX _ <- x
2639 , Reference nmY _ <- y
2640 , nmX == nmY
2641 , categoryOf x <= CatQuantified
2642 , categoryOf y <= CatQuantified
2643 = return
2644 ( "Parameter = parameter (or quantified)"
2645 , return (fromBool True)
2646 )
2647 theRule _ (Op x) = do
2648 x' <- simplifyOp x
2649 when (Op x == x') $ bug $ vcat
2650 [ "rule_PartialEvaluate, simplifier returns the input unchanged."
2651 , "input:" <+> vcat [ pretty (Op x)
2652 , pretty (show (Op x))
2653 ]
2654 ]
2655 return
2656 ( "Partial evaluator"
2657 , return x'
2658 )
2659 theRule _ _ = na "rule_PartialEvaluate"
2660
2661
2662 -- | shifting quantifiers inwards, if they operate on a row of a 2d matrix,
2663 -- make them operate on the rows directly then index
2664 rule_QuantifierShift :: Rule
2665 rule_QuantifierShift = "quantifier-shift" `namedRule` theRule where
2666 theRule p = do
2667 (_, _, mkQuan, inner) <- match opReducer p
2668 (matrix, indexer) <- match opIndexing inner
2669 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2670 case ty of
2671 TypeMatrix{} -> return ()
2672 TypeList{} -> return ()
2673 _ -> na "rule_QuantifierShift"
2674 return
2675 ( "Shifting quantifier inwards"
2676 , return $ make opIndexing
2677 (make matrixLiteral
2678 ty
2679 index
2680 (map mkQuan elems))
2681 indexer
2682 )
2683
2684
2685 -- | shifting quantifiers inwards, if they operate on a flattened multi-dim matrix.
2686 rule_QuantifierShift2 :: Rule
2687 rule_QuantifierShift2 = "quantifier-shift2" `namedRule` theRule where
2688 theRule p = do
2689 (_, _, mkQuan, inner) <- match opReducer p
2690 matrix <- match opFlatten inner
2691 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2692 case ty of
2693 TypeMatrix{} -> return () -- the matrix literal should contain further matrix/list stuff.
2694 TypeList{} -> return ()
2695 _ -> na "rule_QuantifierShift2"
2696 return
2697 ( "Shifting quantifier inwards"
2698 , return $ mkQuan
2699 (make matrixLiteral
2700 ty
2701 index
2702 (map (mkQuan . flattenIfNeeded (matrixNumDims ty)) elems))
2703 )
2704
2705
2706 -- | shifting quantifiers inwards, if they operate on a concatenated multi-dim matrix.
2707 rule_QuantifierShift3 :: Rule
2708 rule_QuantifierShift3 = "quantifier-shift3" `namedRule` theRule where
2709 theRule p = do
2710 (_, True, mkQuan, inner) <- match opReducer p
2711 matrix <- match opConcatenate inner
2712 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2713 return
2714 ( "Shifting quantifier inwards"
2715 , return $ mkQuan $ make matrixLiteral
2716 ty
2717 index
2718 (map mkQuan elems)
2719 )
2720
2721
2722 rule_Comprehension_Simplify :: Rule
2723 rule_Comprehension_Simplify = "comprehension-simplify" `namedRule` theRule where
2724 theRule (Comprehension x gocs)
2725 | let isTrueCondition (Condition (Constant (ConstantBool True))) = True
2726 isTrueCondition _ = False
2727 , let gocs' = filter (not . isTrueCondition) gocs
2728 , length gocs' < length gocs
2729 = return
2730 ( "Removing true conditions"
2731 , return $ Comprehension x gocs'
2732 )
2733 theRule _ = na "rule_Comprehension_Simplify"
2734
2735
2736 rule_Xor_To_Sum :: Rule
2737 rule_Xor_To_Sum = "xor-to-sum" `namedRule` theRule where
2738 theRule [essence| xor(&arg) |] =
2739 case arg of
2740 Comprehension body goc -> do
2741 let argOut = Comprehension [essence| toInt(&body) |] goc
2742 return
2743 ( "xor to sum"
2744 , return [essence| 1 = sum(&argOut) % 2 |]
2745 )
2746 AbstractLiteral (AbsLitMatrix dom elems) -> do
2747 let argOut = AbstractLiteral $ AbsLitMatrix dom
2748 [ [essence| toInt(&el) |] | el <- elems ]
2749 return
2750 ( "xor to sum"
2751 , return [essence| 1 = sum(&argOut) % 2 |]
2752 )
2753 _ -> do
2754 (iPat, i) <- quantifiedVar
2755 return
2756 ( "xor to sum"
2757 , return [essence| 1 = sum([ toInt(&i) | &iPat <- &arg ]) % 2 |]
2758 )
2759 theRule _ = na "rule_Xor_To_Sum"
2760
2761
2762 rule_Comprehension_Cardinality :: Rule
2763 rule_Comprehension_Cardinality = "comprehension-cardinality" `namedRule` theRule where
2764 theRule p = do
2765 Comprehension _ gensOrConds <- match opTwoBars p
2766 let ofones = Comprehension (fromInt 1) gensOrConds
2767 return ( "Horizontal rule for comprehension cardinality"
2768 , return [essence| sum(&ofones) |]
2769 )
2770
2771 rule_Flatten_Cardinality :: Rule
2772 rule_Flatten_Cardinality = "flatten-cardinality" `namedRule` theRule where
2773 theRule p = do
2774 list <- match opTwoBars p >>= match opConcatenate
2775 return ( "Horizontal rule for comprehension cardinality"
2776 , do
2777 (iPat, i) <- quantifiedVar
2778 return [essence| sum([ |&i| | &iPat <- &list ]) |]
2779 )
2780