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