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