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 let indexInto matrix ix =
2347 case match opMatrixIndexingSlicing matrix of
2348 Just (base, indices) ->
2349 make opMatrixIndexingSlicing base (replaceFirstSlice ix indices)
2350 Nothing ->
2351 [essence| &matrix[&ix] |]
2352 replaceFirstSlice ix = \case
2353 Right _ : rest -> Left ix : rest
2354 indexer : rest -> indexer : replaceFirstSlice ix rest
2355 [] -> []
2356 mi = indexInto m i
2357 mj = indexInto m j
2358 return
2359 [essence|
2360 and([ &mi != &mj
2361 | &iPat : &index
2362 , &jPat : &index
2363 , &i < &j
2364 ])
2365 |]
2366 )
2367 theRule _ = na "rule_Decompose_AllDiff"
2368
2369
2370 rule_Decompose_AllDiff_MapToSingleInt :: Rule
2371 rule_Decompose_AllDiff_MapToSingleInt = "decompose-allDiff-mapToSingleInt" `namedRule` theRule where
2372 theRule [essence| allDiff(&m) |] = do
2373 case m of
2374 Comprehension body gensOrConds -> do
2375 tyBody <- typeOf body
2376 case tyBody of
2377 TypeBool -> na "rule_Decompose_AllDiff_MapToSingleInt"
2378 TypeInt _ -> na "rule_Decompose_AllDiff_MapToSingleInt"
2379 TypeTuple{} -> do
2380 bodyBits <- downX1 body
2381 bodyBitSizes <- forM bodyBits $ \ b -> do
2382 bDomain <- domainOf b
2383 domainSizeOf bDomain
2384 case (bodyBits, bodyBitSizes) of
2385 ([a,b], [_a',b']) -> do
2386 let body'= [essence| &a * &b' + &b |]
2387 let m' = Comprehension body' gensOrConds
2388 return
2389 ( "Decomposing allDiff"
2390 , return [essence| allDiff(&m') |]
2391 )
2392 _ -> na "rule_Decompose_AllDiff_MapToSingleInt"
2393 _ -> na "allDiff on something other than a comprehension."
2394 _ -> na "allDiff on something other than a comprehension."
2395 theRule _ = na "rule_Decompose_AllDiff_MapToSingleInt"
2396
2397
2398 rule_DomainCardinality :: Rule
2399 rule_DomainCardinality = "domain-cardinality" `namedRule` theRule where
2400 theRule p = do
2401 maybeDomain <- match opTwoBars p
2402 d <- expandDomainReference <$> case maybeDomain of
2403 Domain d -> return d
2404 Reference _ (Just (Alias (Domain d))) -> return d
2405 _ -> na "rule_DomainCardinality"
2406 return
2407 ( "Cardinality of a domain"
2408 , case d of
2409 DomainInt _ [RangeBounded 1 u] -> return u
2410 _ -> do
2411 (iPat, _) <- quantifiedVar
2412 return [essence| sum([ 1 | &iPat : &d ]) |]
2413 )
2414
2415
2416 rule_DomainMinMax :: Rule
2417 rule_DomainMinMax = "domain-MinMax" `namedRule` theRule where
2418 theRule [essence| max(&maybeDomain) |] = do
2419 d <- getDomain maybeDomain
2420 return
2421 ( "max of a domain"
2422 , maxOfDomain d
2423 )
2424 theRule [essence| min(&maybeDomain) |] = do
2425 d <- getDomain maybeDomain
2426 return
2427 ( "min of a domain"
2428 , minOfDomain d
2429 )
2430 theRule _ = na "rule_DomainMinMax"
2431
2432 getDomain :: MonadFailDoc m => Expression -> m (Domain () Expression)
2433 getDomain (Domain d) = return d
2434 getDomain (Reference _ (Just (Alias (Domain d)))) = getDomain (Domain d)
2435 getDomain _ = na "rule_DomainMinMax.getDomain"
2436
2437
2438 rule_ComplexAbsPat :: Rule
2439 rule_ComplexAbsPat = "complex-pattern" `namedRule` theRule where
2440 theRule (Comprehension body gensOrConds) = do
2441 (gocBefore, (pat, domainOrExpr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
2442 Generator (GenDomainNoRepr pat@AbsPatTuple{} domain) -> return (pat, Left domain)
2443 Generator (GenInExpr pat@AbsPatTuple{} expr) -> return (pat, Right expr)
2444 _ -> na "rule_ComplexAbsPat"
2445 return
2446 ( "complex pattern on tuple patterns"
2447 , do
2448 (iPat, i) <- quantifiedVar
2449 let replacements = [ (p, make opMatrixIndexing i (map (fromInt . fromIntegral) is))
2450 | (p, is) <- genMappings pat
2451 ]
2452 let f x@(Reference nm _) = fromMaybe x (lookup nm replacements)
2453 f x = x
2454 return $ Comprehension (transform f body)
2455 $ gocBefore
2456 ++ [ either (Generator . GenDomainNoRepr iPat)
2457 (Generator . GenInExpr iPat)
2458 domainOrExpr ]
2459 ++ transformBi f gocAfter
2460 )
2461 theRule _ = na "rule_ComplexAbsPat"
2462
2463 -- i --> i -> []
2464 -- (i,j) --> i -> [1]
2465 -- j -> [2]
2466 -- (i,(j,k)) --> i -> [1]
2467 -- j -> [2,1]
2468 -- k -> [2,2]
2469 genMappings :: AbstractPattern -> [(Name, [Int])]
2470 genMappings (Single nm) = [(nm, [])]
2471 genMappings (AbsPatTuple pats)
2472 = concat
2473 [ [ (patCore, i:is) | (patCore, is) <- genMappings pat ]
2474 | (i, pat) <- zip [1..] pats
2475 ]
2476 genMappings (AbsPatMatrix pats)
2477 = concat
2478 [ [ (patCore, i:is) | (patCore, is) <- genMappings pat ]
2479 | (i, pat) <- zip [1..] pats
2480 ]
2481 genMappings pat = bug ("rule_ComplexLambda.genMappings:" <+> pretty (show pat))
2482
2483
2484 -- this rule doesn't use `namedRule` because it need access to ascendants through the zipper
2485 rule_InlineConditions :: Rule
2486 rule_InlineConditions = "inline-conditions" `namedRuleZ` theRule where
2487 theRule z (Comprehension body gensOrConds) = do
2488 let (toInline, toKeep) = mconcat
2489 [ case goc of
2490 Condition x | categoryOf x == CatDecision -> ([x],[])
2491 _ -> ([],[goc])
2492 | goc <- gensOrConds
2493 ]
2494 theGuard <- case toInline of
2495 [] -> na "No condition to inline."
2496 [x] -> return x
2497 xs -> return $ make opAnd $ fromList xs
2498 (nameQ, opSkip) <- queryQ z
2499 let bodySkipped = opSkip theGuard body
2500 return
2501 ( "Inlining conditions, inside" <+> nameQ
2502 , return $ Comprehension bodySkipped toKeep
2503 )
2504 theRule _ _ = na "rule_InlineConditions"
2505
2506 -- keep going up, until finding a quantifier
2507 -- when found, return the skipping operator for the quantifier
2508 -- if none exists, do not apply the rule.
2509 -- (or maybe we should call bug right ahead, it can't be anything else.)
2510 queryQ z0 =
2511 case Zipper.up z0 of
2512 Nothing -> na "rule_InlineConditions (meh-1)"
2513 Just z -> do
2514 let h = hole z
2515 case ( match opAnd h, match opOr h, match opSum h, match opProduct h
2516 , match opMin h, match opMax h, match opOrdering h ) of
2517 (Just{}, _, _, _, _, _, _) -> return ("and", opAndSkip)
2518 (_, Just{}, _, _, _, _, _) -> return ("or" , opOrSkip )
2519 (_, _, Just{}, _, _, _, _) -> return ("sum", opSumSkip)
2520 (_, _, _, Just{}, _, _, _) -> return ("product", opProductSkip)
2521 (_, _, _, _, Just{}, _, _) -> na "rule_InlineConditions (min)"
2522 (_, _, _, _, _, Just{}, _) -> na "rule_InlineConditions (max)"
2523 (_, _, _, _, _, _, Just{}) -> return ("ordering", opSumSkip)
2524 _ -> na "rule_InlineConditions (meh-2)"
2525 -- case Zipper.up z of
2526 -- Nothing -> na "queryQ"
2527 -- Just u -> queryQ u
2528
2529 opAndSkip b x = [essence| &b -> &x |]
2530 opOrSkip b x = [essence| &b /\ &x |]
2531 opSumSkip b x = [essence| toInt(&b) * catchUndef(&x, 0) |]
2532 opProductSkip b x = [essence| [ 1
2533 , catchUndef(&x,1)
2534 ; int(0..1)
2535 ] [toInt(&b)] |]
2536
2537
2538 rule_InlineConditions_AllDiff :: Rule
2539 rule_InlineConditions_AllDiff = "inline-conditions-allDiff" `namedRule` theRule where
2540 theRule (Op (MkOpAllDiff (OpAllDiff (Comprehension body gensOrConds)))) = do
2541 let (toInline, toKeep) = mconcat
2542 [ case goc of
2543 Condition x | categoryOf x == CatDecision -> ([x],[])
2544 _ -> ([],[goc])
2545 | goc <- gensOrConds
2546 ]
2547 theGuard <- case toInline of
2548 [] -> na "No condition to inline."
2549 [x] -> return x
2550 xs -> return $ make opAnd $ fromList xs
2551
2552 tyBody <- typeOf body
2553 case tyBody of
2554 TypeInt{} -> return ()
2555 _ -> na "rule_InlineConditions_AllDiff, not an int"
2556 domBody <- domainOf body
2557 let
2558 collectLowerBounds (RangeSingle x) = return x
2559 collectLowerBounds (RangeBounded x _) = return x
2560 collectLowerBounds _ = userErr1 ("Unexpected infinite domain:" <+> pretty domBody)
2561
2562 collectLowerBoundsD (DomainInt _ rs) = mapM collectLowerBounds rs
2563 collectLowerBoundsD _ = userErr1 ("Expected an integer domain, but got:" <+> pretty domBody)
2564
2565 bounds <- collectLowerBoundsD domBody
2566 let lowerBound = make opMin (fromList bounds)
2567
2568 -- for each element, we do element-lowerBound+1
2569 -- this makes sure the smallest element is 1
2570 -- hence we can use 0 as the except value!
2571 let bodySkipped = [essence| toInt(&theGuard) * catchUndef(&body + (1 - &lowerBound), 0) |]
2572
2573 return
2574 ( "Inlining conditions, inside allDiff"
2575 , return $ make opAllDiffExcept (Comprehension bodySkipped toKeep) 0
2576 )
2577 theRule _ = na "rule_InlineConditions_AllDiff"
2578
2579
2580 rule_InlineConditions_MaxMin :: Rule
2581 rule_InlineConditions_MaxMin = "aux-for-MaxMin" `namedRule` theRule where
2582 theRule p = do
2583 when (categoryOf p < CatDecision) $ na "rule_InlineConditions_MaxMin"
2584 (nameQ, binOp, Comprehension body gensOrConds) <-
2585 case (match opMax p, match opMin p) of
2586 (Just res, _) -> return ("max", \ a b -> [essence| &a <= &b |], res )
2587 (_, Just res) -> return ("min", \ a b -> [essence| &a >= &b |], res )
2588 _ -> na "rule_InlineConditions_MaxMin"
2589 let
2590 (toInline, gocInExpr, _toKeep) = mconcat
2591 [ case goc of
2592 Condition x | categoryOf x == CatDecision -> ([x],[],[])
2593 Generator (GenInExpr {}) -> ([],[goc],[])
2594 _ -> ([],[],[goc])
2595 | goc <- gensOrConds
2596 ]
2597 when (null toInline && null gocInExpr) $ na "rule_InlineConditions_MaxMin"
2598 auxDomain <- domainOf body
2599 return
2600 ( "Creating auxiliary variable for a" <+> nameQ
2601 , do
2602 (auxName, aux) <- auxiliaryVar
2603 let auxDefinedLHS = make opSum (Comprehension 1 gensOrConds)
2604 let auxDefined = [essence| &auxDefinedLHS > 0 |]
2605 let auxUndefined = [essence| &auxDefinedLHS = 0 |]
2606 let aux' = WithLocals aux (DefinednessConstraints [auxDefined])
2607 return $ WithLocals aux'
2608 (AuxiliaryVars
2609 [ Declaration (FindOrGiven LocalFind auxName auxDomain)
2610 , SuchThat
2611 [ make opAnd $ Comprehension
2612 (binOp body aux)
2613 gensOrConds
2614
2615 -- either one of the members of this comprehension, or dontCare
2616 -- if it is indeed dontCare, care should be taken to make sure it isn't used as a normal value
2617 , make opAnd $ fromList
2618 [ make opImply auxDefined
2619 (make opOr $ Comprehension
2620 [essence| &body = &aux |]
2621 gensOrConds)
2622 , make opImply auxUndefined (make opDontCare aux)
2623 ]
2624 ]
2625 ])
2626 )
2627
2628
2629 rule_AttributeToConstraint :: Rule
2630 rule_AttributeToConstraint = "attribute-to-constraint" `namedRule` theRule where
2631 theRule (Op (MkOpAttributeAsConstraint (OpAttributeAsConstraint thing attr mval))) = do
2632 dom <- domainOf thing
2633 let conv = mkAttributeToConstraint dom attr mval thing
2634 return
2635 ( "Converting an attribute to a constraint"
2636 , bugFailT "rule_AttributeToConstraint" conv
2637 )
2638 theRule _ = na "rule_AttributeToConstraint"
2639
2640
2641 timedF :: MonadIO m => String -> (a -> m b) -> a -> m b
2642 timedF name comp a = timeItNamed name (comp a)
2643
2644
2645 evaluateModel ::
2646 MonadFailDoc m =>
2647 NameGen m =>
2648 EnumerateDomain m =>
2649 (?typeCheckerMode :: TypeCheckerMode) =>
2650 Model -> m Model
2651 evaluateModel m = do
2652 let
2653 full (Reference _ (Just (DeclHasRepr _ _ (singletonDomainInt -> Just val)))) =
2654 return val
2655 full p@Constant{} = return p
2656 full p@Domain{} = return p
2657 full p = do
2658 mconstant <- runExceptT (instantiateExpression [] p)
2659 case mconstant of
2660 Left{} -> return p
2661 Right constant ->
2662 if null [() | ConstantUndefined{} <- universe constant] -- if there are no undefined values in it
2663 then return (Constant constant)
2664 else return p
2665 let
2666 partial (Op op)
2667 | Just (x, y) <- case op of
2668 MkOpLeq (OpLeq x y) -> Just (x,y)
2669 MkOpGeq (OpGeq x y) -> Just (x,y)
2670 MkOpEq (OpEq x y) -> Just (x,y)
2671 _ -> Nothing
2672 , Reference nmX _ <- x
2673 , Reference nmY _ <- y
2674 , nmX == nmY
2675 , categoryOf x <= CatQuantified
2676 , categoryOf y <= CatQuantified
2677 = return (fromBool True)
2678 partial p@(Op x) = do
2679 mx' <- runExceptT (simplifyOp x)
2680 case mx' of
2681 Left{} -> return p
2682 Right x' -> do
2683 when (Op x == x') $ bug $ vcat
2684 [ "rule_PartialEvaluate, simplifier returns the input unchanged."
2685 , "input:" <+> vcat [ pretty (Op x)
2686 , pretty (show (Op x))
2687 ]
2688 ]
2689 return x'
2690 partial p = return p
2691
2692 (descendBiM full >=> transformBiM partial) m
2693
2694
2695 rule_FullEvaluate :: Rule
2696 rule_FullEvaluate = "full-evaluate" `namedRule` theRule where
2697 theRule Constant{} = na "rule_FullEvaluate"
2698 theRule Domain{} = na "rule_FullEvaluate"
2699 theRule (Reference _ (Just (Alias x))) -- selectively inline, unless x is huge
2700 | Just Comprehension{} <- match opToSet x
2701 = return ("Inline alias", return x)
2702 theRule p = do
2703 constant <- instantiateExpression [] p
2704 unless (null [() | ConstantUndefined{} <- universe constant]) $
2705 na "rule_PartialEvaluate, undefined"
2706 return ("Full evaluator", return $ Constant constant)
2707
2708
2709 rule_PartialEvaluate :: Rule
2710 rule_PartialEvaluate = "partial-evaluate" `namedRuleZ` theRule where
2711 -- if a variable only has a single value in its domain, replace it with the value
2712 theRule z (Reference _ (Just (DeclHasRepr _ _ (singletonDomainInt -> Just val)))) =
2713 case hole <$> Zipper.up z of
2714 Just (Op (MkOpTrue _)) -> na "rule_PartialEvaluate, inside a true(ref)"
2715 _ -> return ( "Partial evaluator"
2716 , return val
2717 )
2718 theRule _ (Op op)
2719 | Just (x, y) <- case op of
2720 MkOpLeq (OpLeq x y) -> Just (x,y)
2721 MkOpGeq (OpGeq x y) -> Just (x,y)
2722 MkOpEq (OpEq x y) -> Just (x,y)
2723 _ -> Nothing
2724 , Reference nmX _ <- x
2725 , Reference nmY _ <- y
2726 , nmX == nmY
2727 , categoryOf x <= CatQuantified
2728 , categoryOf y <= CatQuantified
2729 = return
2730 ( "Parameter = parameter (or quantified)"
2731 , return (fromBool True)
2732 )
2733 theRule _ (Op x) = do
2734 x' <- simplifyOp x
2735 when (Op x == x') $ bug $ vcat
2736 [ "rule_PartialEvaluate, simplifier returns the input unchanged."
2737 , "input:" <+> vcat [ pretty (Op x)
2738 , pretty (show (Op x))
2739 ]
2740 ]
2741 return
2742 ( "Partial evaluator"
2743 , return x'
2744 )
2745 theRule _ _ = na "rule_PartialEvaluate"
2746
2747
2748 -- | shifting quantifiers inwards, if they operate on a row of a 2d matrix,
2749 -- make them operate on the rows directly then index
2750 rule_QuantifierShift :: Rule
2751 rule_QuantifierShift = "quantifier-shift" `namedRule` theRule where
2752 theRule p = do
2753 (_, _, mkQuan, inner) <- match opReducer p
2754 (matrix, indexer) <- match opIndexing inner
2755 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2756 case ty of
2757 TypeMatrix{} -> return ()
2758 TypeList{} -> return ()
2759 _ -> na "rule_QuantifierShift"
2760 return
2761 ( "Shifting quantifier inwards"
2762 , return $ make opIndexing
2763 (make matrixLiteral
2764 ty
2765 index
2766 (map mkQuan elems))
2767 indexer
2768 )
2769
2770
2771 -- | shifting quantifiers inwards, if they operate on a flattened multi-dim matrix.
2772 rule_QuantifierShift2 :: Rule
2773 rule_QuantifierShift2 = "quantifier-shift2" `namedRule` theRule where
2774 theRule p = do
2775 (_, _, mkQuan, inner) <- match opReducer p
2776 matrix <- match opFlatten inner
2777 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2778 case ty of
2779 TypeMatrix{} -> return () -- the matrix literal should contain further matrix/list stuff.
2780 TypeList{} -> return ()
2781 _ -> na "rule_QuantifierShift2"
2782 return
2783 ( "Shifting quantifier inwards"
2784 , return $ mkQuan
2785 (make matrixLiteral
2786 ty
2787 index
2788 (map (mkQuan . flattenIfNeeded (matrixNumDims ty)) elems))
2789 )
2790
2791
2792 -- | shifting quantifiers inwards, if they operate on a concatenated multi-dim matrix.
2793 rule_QuantifierShift3 :: Rule
2794 rule_QuantifierShift3 = "quantifier-shift3" `namedRule` theRule where
2795 theRule p = do
2796 (_, True, mkQuan, inner) <- match opReducer p
2797 matrix <- match opConcatenate inner
2798 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2799 return
2800 ( "Shifting quantifier inwards"
2801 , return $ mkQuan $ make matrixLiteral
2802 ty
2803 index
2804 (map mkQuan elems)
2805 )
2806
2807
2808 rule_Comprehension_Simplify :: Rule
2809 rule_Comprehension_Simplify = "comprehension-simplify" `namedRule` theRule where
2810 theRule (Comprehension x gocs)
2811 | let isTrueCondition (Condition (Constant (ConstantBool True))) = True
2812 isTrueCondition _ = False
2813 , let gocs' = filter (not . isTrueCondition) gocs
2814 , length gocs' < length gocs
2815 = return
2816 ( "Removing true conditions"
2817 , return $ Comprehension x gocs'
2818 )
2819 theRule _ = na "rule_Comprehension_Simplify"
2820
2821
2822 rule_Xor_To_Sum :: Rule
2823 rule_Xor_To_Sum = "xor-to-sum" `namedRule` theRule where
2824 theRule [essence| xor(&arg) |] =
2825 case arg of
2826 Comprehension body goc -> do
2827 let argOut = Comprehension [essence| toInt(&body) |] goc
2828 return
2829 ( "xor to sum"
2830 , return [essence| 1 = sum(&argOut) % 2 |]
2831 )
2832 AbstractLiteral (AbsLitMatrix dom elems) -> do
2833 let argOut = AbstractLiteral $ AbsLitMatrix dom
2834 [ [essence| toInt(&el) |] | el <- elems ]
2835 return
2836 ( "xor to sum"
2837 , return [essence| 1 = sum(&argOut) % 2 |]
2838 )
2839 _ -> do
2840 (iPat, i) <- quantifiedVar
2841 return
2842 ( "xor to sum"
2843 , return [essence| 1 = sum([ toInt(&i) | &iPat <- &arg ]) % 2 |]
2844 )
2845 theRule _ = na "rule_Xor_To_Sum"
2846
2847
2848 enforceTagConsistency :: MonadFail m => Model -> m Model
2849 enforceTagConsistency model = do
2850 let statements' = transformBi reDomExp $ transformBi reDomConst (mStatements model)
2851 return model { mStatements = statements' }
2852
2853
2854 addUnnamedSymmetryBreaking ::
2855 NameGen m =>
2856 Maybe UnnamedSymmetryBreaking ->
2857 Model ->
2858 m Model
2859 addUnnamedSymmetryBreaking mode model = do
2860
2861 let
2862 allUnnamedTypes :: [(Domain () Expression, Expression)]
2863 allUnnamedTypes =
2864 [ reTag (TagUnnamed nm') (DomainReference nm Nothing, x) --x is a TagInt at this point so we must reTag it
2865 | Declaration (LettingDomainDefnUnnamed nm@(Name nm') x) <- mStatements model
2866 ]
2867
2868 allDecVars =
2869 [ (Reference nm Nothing, domain)
2870 | Declaration (FindOrGiven Find nm domain) <- mStatements model
2871 ]
2872
2873 -- allDecVarsAux auxSuffix =
2874 -- [ (Reference (mconcat [nm, "_auxFor_", auxSuffix]) Nothing, domain)
2875 -- | Declaration (FindOrGiven Find nm domain) <- mStatements model
2876 -- ]
2877
2878 varsTuple = case allDecVars of
2879 [v] -> fst v
2880 _ -> AbstractLiteral $ AbsLitTuple $ map fst allDecVars
2881 -- mkAuxTuple auxSuffix = AbstractLiteral $ AbsLitTuple $ map fst (allDecVarsAux auxSuffix)
2882
2883 -- traceM $ show $ "Unnamed types in this model:" <++> prettyList id "," allUnnamedTypes
2884 -- traceM $ show $ "Unnamed decision variables in this model:" <++> prettyList id "," allDecVars
2885
2886 -- 3 axis of doom
2887 -- 1. Quick/Complete. Quick is quickPermutationOrder(x, p) -- this is an efficient subset of x .<= p(x)
2888 -- Complete is x .<= p(x)
2889 -- 2. Scope. Consecutive
2890 -- AllPairs
2891 -- AllPermutations
2892 -- 3. Independently/Altogether
2893
2894 case mode of
2895 Nothing -> return model
2896 Just (UnnamedSymmetryBreaking quickOrComplete usbScope independentlyOrAltogether) -> do
2897 -- let newDecls =
2898 -- case quickOrComplete of
2899 -- USBQuick -> []
2900 -- USBComplete ->
2901 -- case independentlyOrAltogether of
2902 -- USBIndependently ->
2903 -- [ Declaration (FindOrGiven LocalFind nm' domain)
2904 -- | Declaration (FindOrGiven Find nm domain) <- mStatements model
2905 -- , (DomainReference uName _, _) <- allUnnamedTypes
2906 -- , let nm' = mconcat [nm, "_auxFor_", uName]
2907 -- ]
2908 -- USBAltogether ->
2909 -- [ Declaration (FindOrGiven LocalFind nm' domain)
2910 -- | Declaration (FindOrGiven Find nm domain) <- mStatements model
2911 -- , let nm' = mconcat [nm, "_auxFor_all"]
2912 -- ]
2913
2914 let
2915
2916 combinedPermApply perms =
2917 case quickOrComplete of
2918 USBQuick -> make opQuickPermutationOrder perms varsTuple
2919 USBComplete ->
2920 let applied = make opTransform perms varsTuple
2921 in [essence| &varsTuple .<= &applied |]
2922
2923 mkGenerator_Consecutive _ [] = bug "must have at least one unnamed type"
2924 mkGenerator_Consecutive perms [(u, uSize)] = do
2925 (iPat, i) <- quantifiedVar
2926 let perm = [essence| permutation((&i, succ(&i))) |]
2927 let applied = combinedPermApply (perm:perms)
2928 return [essence|
2929 and([ &applied
2930 | &iPat : &u
2931 , &i < &uSize
2932 ])
2933 |]
2934 mkGenerator_Consecutive perms ((u, uSize):us) = do
2935 (iPat, i) <- quantifiedVar
2936 let perm = [essence| permutation((&i, succ(&i))) |]
2937 applied <- mkGenerator_Consecutive (perm:perms) us
2938 return [essence|
2939 and([ &applied
2940 | &iPat : &u
2941 , &i < &uSize
2942 ])
2943 |]
2944
2945
2946 mkGenerator_AllPairs _ [] = bug "must have at least one unnamed type"
2947 mkGenerator_AllPairs perms [(u, _uSize)] = do
2948 (iPat, i) <- quantifiedVar
2949 (jPat, j) <- quantifiedVar
2950 let perm = [essence| permutation((&i, &j)) |]
2951 let applied = combinedPermApply (perm:perms)
2952 return [essence|
2953 and([ &applied
2954 | &iPat : &u
2955 , &jPat : &u
2956 , &i < &j
2957 ])
2958 |]
2959 mkGenerator_AllPairs perms ((u, _uSize):us) = do
2960 (iPat, i) <- quantifiedVar
2961 (jPat, j) <- quantifiedVar
2962 let perm = [essence| permutation((&i, &j)) |]
2963 applied <- mkGenerator_AllPairs (perm:perms) us
2964 return [essence|
2965 and([ &applied
2966 | &iPat : &u
2967 , &jPat : &u
2968 , &i < &j
2969 ])
2970 |]
2971
2972 mkGenerator_AllPermutations _ [] = bug "must have at least one unnamed type"
2973 mkGenerator_AllPermutations perms [(u, _uSize)] = do
2974 (iPat, i) <- quantifiedVar
2975 let perm = i
2976 let applied = combinedPermApply (perm:perms)
2977 return [essence|
2978 and([ &applied
2979 | &iPat : permutation of &u
2980 ])
2981 |]
2982 mkGenerator_AllPermutations perms ((u, _uSize):us) = do
2983 (iPat, i) <- quantifiedVar
2984 let perm = i
2985 applied <- mkGenerator_AllPermutations (perm:perms) us
2986 return [essence|
2987 and([ &applied
2988 | &iPat : permutation of &u
2989 ])
2990 |]
2991
2992 mkGenerator perms us =
2993 case usbScope of
2994 USBConsecutive -> mkGenerator_Consecutive perms us
2995 USBAllPairs -> mkGenerator_AllPairs perms us
2996 USBAllPermutations -> mkGenerator_AllPermutations perms us
2997 newCons <-
2998 case independentlyOrAltogether of
2999 USBIndependently -> do
3000 xs <- sequence
3001 [ mkGenerator [] [(u, uSize)]
3002 | (u@DomainReference{}, uSize) <- allUnnamedTypes
3003 ]
3004 return [SuchThat xs]
3005 USBAltogether -> do
3006 cons <- mkGenerator [] allUnnamedTypes
3007 return [SuchThat [cons]]
3008
3009 let stmts = newCons
3010 traceM $ show $ vcat $ "Adding the following unnamed symmetry breaking constraints:"
3011 : map (nest 4 . pretty) stmts
3012 return model { mStatements = mStatements model ++ stmts}
3013
3014
3015
3016 rule_Comprehension_Cardinality :: Rule
3017 rule_Comprehension_Cardinality = "comprehension-cardinality" `namedRule` theRule where
3018 theRule p = do
3019 Comprehension _ gensOrConds <- match opTwoBars p
3020 let ofones = Comprehension (fromInt 1) gensOrConds
3021 return ( "Horizontal rule for comprehension cardinality"
3022 , return [essence| sum(&ofones) |]
3023 )
3024
3025 rule_Flatten_Cardinality :: Rule
3026 rule_Flatten_Cardinality = "flatten-cardinality" `namedRule` theRule where
3027 theRule p = do
3028 list <- match opTwoBars p >>= match opConcatenate
3029 return ( "Horizontal rule for comprehension cardinality"
3030 , do
3031 (iPat, i) <- quantifiedVar
3032 return [essence| sum([ |&i| | &iPat <- &list ]) |]
3033 )