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.MSet.rule_Comprehension_ToSet
1577 , Horizontal.MSet.rule_Union
1578 , Horizontal.Set.rule_Union
1579 , Horizontal.Set.rule_Difference
1580 , Horizontal.Set.rule_PowerSet_Comprehension
1581 , Horizontal.Set.rule_PowerSet_Difference
1582 , Horizontal.Set.rule_MaxMin
1583
1584 , Horizontal.MSet.rule_Comprehension_Literal
1585 , Horizontal.MSet.rule_Freq_toMSet_Flatten
1586 , Horizontal.MSet.rule_Comprehension_ToSet_Literal
1587 , Horizontal.MSet.rule_Eq
1588 , Horizontal.MSet.rule_Neq
1589 , Horizontal.MSet.rule_Subset
1590 , Horizontal.MSet.rule_SubsetEq
1591 , Horizontal.MSet.rule_Supset
1592 , Horizontal.MSet.rule_SupsetEq
1593 , Horizontal.MSet.rule_Freq_Union
1594 , Horizontal.MSet.rule_Freq
1595 , Horizontal.MSet.rule_In
1596 , Horizontal.MSet.rule_Card
1597 , Horizontal.MSet.rule_MaxMin
1598
1599 , Horizontal.Function.rule_Comprehension_Literal
1600 , Horizontal.Function.rule_Image_Bool
1601 , Horizontal.Function.rule_Image_BoolMatrixIndexed
1602 , Horizontal.Function.rule_Image_BoolTupleIndexed
1603 , Horizontal.Function.rule_Image_Int
1604 , Horizontal.Function.rule_Image_IntMatrixIndexed
1605 , Horizontal.Function.rule_Image_IntTupleIndexed
1606 , Horizontal.Function.rule_Image_Matrix_LexLhs
1607 , Horizontal.Function.rule_Image_Matrix_LexRhs
1608
1609 , Horizontal.Function.rule_Comprehension_Image
1610 , Horizontal.Function.rule_Comprehension_ImageSet
1611 , Horizontal.Function.rule_Eq
1612 , Horizontal.Function.rule_Neq
1613 , Horizontal.Function.rule_Subset
1614 , Horizontal.Function.rule_SubsetEq
1615 , Horizontal.Function.rule_Supset
1616 , Horizontal.Function.rule_SupsetEq
1617 , Horizontal.Function.rule_Inverse
1618 , Horizontal.Function.rule_Card
1619 , Horizontal.Function.rule_Comprehension_PreImage
1620 , Horizontal.Function.rule_Comprehension_Defined
1621 , Horizontal.Function.rule_Comprehension_Range
1622 , Horizontal.Function.rule_In
1623 , Horizontal.Function.rule_Restrict_Image
1624 , Horizontal.Function.rule_Restrict_Comprehension
1625 , Horizontal.Function.rule_Comprehension_Defined_Size
1626 , Horizontal.Function.rule_Comprehension_Range_Size
1627 , Horizontal.Function.rule_Defined_Intersect
1628 , Horizontal.Function.rule_DefinedOrRange_Union
1629 , Horizontal.Function.rule_DefinedOrRange_Difference
1630
1631 , Horizontal.Sequence.rule_Comprehension_Literal
1632 , Horizontal.Sequence.rule_Image_Bool
1633 , Horizontal.Sequence.rule_Image_Int
1634 , Horizontal.Sequence.rule_Comprehension_Image
1635 , Horizontal.Sequence.rule_Image_Literal_Bool
1636 , Horizontal.Sequence.rule_Image_Literal_Int
1637 , Horizontal.Sequence.rule_Eq_Literal
1638 , Horizontal.Sequence.rule_Eq
1639 , Horizontal.Sequence.rule_Eq_Comprehension
1640 , Horizontal.Sequence.rule_Neq
1641 , Horizontal.Sequence.rule_Subset
1642 , Horizontal.Sequence.rule_SubsetEq
1643 , Horizontal.Sequence.rule_Supset
1644 , Horizontal.Sequence.rule_SupsetEq
1645 , Horizontal.Sequence.rule_Card
1646 , Horizontal.Sequence.rule_Comprehension_PreImage
1647 , Horizontal.Sequence.rule_Comprehension_Defined
1648 , Horizontal.Sequence.rule_Comprehension_Range
1649 , Horizontal.Sequence.rule_In
1650 , Horizontal.Sequence.rule_Restrict_Image
1651 , Horizontal.Sequence.rule_Restrict_Comprehension
1652 , Horizontal.Sequence.rule_Substring
1653 , Horizontal.Sequence.rule_Subsequence
1654
1655 , Horizontal.Relation.rule_Comprehension_Literal
1656 , Horizontal.Relation.rule_Comprehension_Projection
1657 , Horizontal.Relation.rule_PowerSet_Comprehension
1658 , Horizontal.Relation.rule_Image
1659 , Horizontal.Relation.rule_In
1660 , Horizontal.Relation.rule_Eq
1661 , Horizontal.Relation.rule_Neq
1662 , Horizontal.Relation.rule_Subset
1663 , Horizontal.Relation.rule_SubsetEq
1664 , Horizontal.Relation.rule_Supset
1665 , Horizontal.Relation.rule_SupsetEq
1666 , Horizontal.Relation.rule_Card
1667
1668 , Horizontal.Partition.rule_Comprehension_Literal
1669 , Horizontal.Partition.rule_Eq
1670 , Horizontal.Partition.rule_Neq
1671 , Horizontal.Partition.rule_Together
1672 , Horizontal.Partition.rule_Apart
1673 , Horizontal.Partition.rule_Party
1674 , Horizontal.Partition.rule_Participants
1675 , Horizontal.Partition.rule_Card
1676 , Horizontal.Partition.rule_In
1677
1678
1679 ]
1680
1681
1682 bubbleUpRules :: [[Rule]]
1683 bubbleUpRules =
1684 [
1685 [ BubbleUp.rule_MergeNested
1686 , BubbleUp.rule_ToAnd
1687 , BubbleUp.rule_ToMultiply_HeadOfIntComprehension
1688 , BubbleUp.rule_ConditionInsideGeneratorDomain
1689 , BubbleUp.rule_LiftVars
1690 ]
1691 ,
1692 [ BubbleUp.rule_NotBoolYet
1693 ]
1694 ]
1695
1696
1697 otherRules :: [[Rule]]
1698 otherRules =
1699 [
1700 [ rule_Xor_To_Sum ]
1701 ,
1702 [ TildeOrdering.rule_BoolInt
1703 , TildeOrdering.rule_MSet
1704 , TildeOrdering.rule_ViaMSet
1705 , TildeOrdering.rule_TildeLeq
1706 ]
1707 ,
1708 [ DontCare.rule_Bool
1709 , DontCare.rule_Int
1710 , DontCare.rule_Unnamed
1711 , DontCare.rule_Tuple
1712 , DontCare.rule_Record
1713 , DontCare.rule_Variant
1714 , DontCare.rule_Permutation
1715 , DontCare.rule_Matrix
1716 , DontCare.rule_Abstract
1717 ]
1718 ,
1719 [ rule_TrueIsNoOp
1720 , rule_FlattenOf1D
1721 , rule_Decompose_AllDiff
1722 , rule_Decompose_AllDiff_MapToSingleInt
1723
1724 , rule_GeneratorsFirst
1725 ]
1726 ,
1727 [ rule_DomainCardinality
1728 , rule_DomainMinMax
1729
1730 , rule_ComplexAbsPat
1731
1732 , rule_AttributeToConstraint
1733
1734 , rule_QuantifierShift
1735 , rule_QuantifierShift2
1736 , rule_QuantifierShift3
1737
1738 ]
1739
1740 , [ rule_Comprehension_Simplify
1741 ]
1742
1743 , [ rule_InlineConditions
1744 , rule_InlineConditions_AllDiff
1745 , rule_InlineConditions_MaxMin
1746 ]
1747 ]
1748
1749 -- | These rules depend on other rules firing first.
1750 delayedRules :: [[Rule]]
1751 delayedRules =
1752 [
1753 [ Vertical.Matrix.rule_Comprehension_Singleton
1754 , Vertical.Matrix.rule_Comprehension_SingletonDomain
1755 , Vertical.Matrix.rule_Concatenate_Singleton
1756 , Vertical.Matrix.rule_MatrixIndexing
1757
1758 ]
1759 , [ rule_ReducerToComprehension
1760 ]
1761 , [ rule_QuickPermutationOrder
1762 , rule_DotLtLeq
1763 , rule_Flatten_Lex
1764 ]
1765 ]
1766
1767
1768 rule_ChooseRepr :: (?typeCheckerMode :: TypeCheckerMode) => Config -> Rule
1769 rule_ChooseRepr config = Rule "choose-repr" (const theRule) where
1770
1771 theRule (Reference nm (Just (DeclNoRepr forg _ inpDom region))) | forg `elem` [Find, Given, CutFind] = do
1772 let reprsWhichOrder
1773 | (forg, representationsGivens config) == (Given, Sparse) = reprsSparseOrder
1774 | (forg, representationsFinds config) == (Find , Sparse) = reprsSparseOrder
1775 | not (representationLevels config) = reprsStandardOrderNoLevels
1776 | otherwise = reprsStandardOrder
1777 domOpts <- reprOptions reprsWhichOrder inpDom
1778 when (null domOpts) $
1779 bug $ "No representation matches this beast:" <++> pretty inpDom
1780 let options =
1781 [ RuleResult { ruleResultDescr = msg
1782 , ruleResultType = case forg of
1783 Find -> ChooseRepr_Find nm
1784 Given -> ChooseRepr_Given nm
1785 CutFind -> ChooseRepr_Cut nm
1786 _ -> bug "rule_ChooseRepr ruleResultType"
1787 , ruleResult = return out
1788 , ruleResultHook = Just hook
1789 , ruleResultSize = return $ expressionDepth $ Reference nm (Just (DeclHasRepr forg nm thisDom))
1790 }
1791 | thisDom <- domOpts
1792 , let msg = "Choosing representation for" <+> pretty nm <> ":" <++> pretty thisDom
1793 , let out = Reference nm (Just (DeclHasRepr forg nm thisDom))
1794 , let hook = mkHook (channelling config) forg nm thisDom region
1795 ]
1796 return options
1797 theRule _ = na "rule_ChooseRepr"
1798
1799 mkHook
1800 :: ( MonadLog m
1801 , MonadFail m
1802 , MonadFailDoc m
1803 , NameGen m
1804 , EnumerateDomain m
1805 )
1806 => Bool
1807 -> FindOrGiven
1808 -> Name
1809 -> Domain HasRepresentation Expression
1810 -> Region
1811 -> Model
1812 -> m Model
1813 mkHook useChannelling -- whether to use channelling or not
1814 forg -- find or given
1815 name -- name of the original declaration
1816 domain -- domain with representation selected
1817 region -- the region of the Reference we are working on
1818 model = do
1819 let
1820
1821 representations = model |> mInfo |> miRepresentations
1822 representationsTree = model |> mInfo |> miRepresentationsTree
1823 |> concatMap (\ (n, ds) -> map (n,) ds )
1824
1825 usedBefore = (name, reprTree domain) `elem` representationsTree
1826
1827 mkStructurals :: (MonadLog m, MonadFailDoc m, NameGen m, EnumerateDomain m)
1828 => m [Expression]
1829 mkStructurals = do
1830 let ref = Reference name (Just (DeclHasRepr forg name domain))
1831 logDebugVerbose $ "Generating structural constraints for:" <+> vcat [pretty ref, pretty domain]
1832 structurals <- getStructurals downX1 domain >>= \ gen -> gen ref
1833 logDebugVerbose $ "Before name resolution:" <+> vcat (map pretty structurals)
1834 resolved <- mapM resolveNamesX structurals -- re-resolving names
1835 logDebugVerbose $ "After name resolution:" <+> vcat (map pretty resolved)
1836 return resolved
1837
1838 addStructurals :: (MonadLog m, MonadFailDoc m, NameGen m, EnumerateDomain m)
1839 => Model -> m Model
1840 addStructurals
1841 | forg == Given = return
1842 | usedBefore = return
1843 | otherwise = \ m -> do
1844 structurals <- mkStructurals
1845 return $ if null structurals
1846 then m
1847 else m { mStatements = mStatements m ++ [SuchThat structurals] }
1848
1849 channels =
1850 [ make opEq this that
1851 | (n, d) <- representations
1852 , n == name
1853 , let this = Reference name (Just (DeclHasRepr forg name domain))
1854 , let that = Reference name (Just (DeclHasRepr forg name d))
1855 ]
1856
1857 addChannels
1858 | forg == Given = return
1859 | usedBefore = return
1860 | null channels = return
1861 | otherwise = \ m -> return
1862 m { mStatements = mStatements m ++ [SuchThat channels] }
1863
1864 recordThis
1865 | usedBefore = return
1866 | otherwise = \ m ->
1867 let
1868 oldInfo = mInfo m
1869 newInfo = oldInfo
1870 { miRepresentations = representations ++ [(name, domain)]
1871 , miRepresentationsTree = (representationsTree ++ [(name, reprTree domain)])
1872 |> sortBy (comparing fst)
1873 |> groupBy ((==) `on` fst)
1874 |> mapMaybe (\ grp -> case grp of [] -> Nothing ; (x:_) -> Just (fst x, map snd grp) )
1875 }
1876 in return m { mInfo = newInfo }
1877
1878 fixReprForAllOthers
1879 | useChannelling = return -- no-op, if channelling=yes
1880 | otherwise = \ m ->
1881 let
1882 f (Reference nm _)
1883 | nm == name
1884 = Reference nm (Just (DeclHasRepr forg name domain))
1885 f x = x
1886 in
1887 return m { mStatements = transformBi f (mStatements m) }
1888
1889 fixReprForSameRegion
1890 | region == NoRegion = return -- no-op, if we aren't in a particular region
1891 | otherwise = \ m ->
1892 let
1893 f (Reference nm (Just (DeclNoRepr _ _ _ region')))
1894 | nm == name
1895 , region' == region
1896 = Reference nm (Just (DeclHasRepr forg name domain))
1897 f x = x
1898 in
1899 return m { mStatements = transformBi f (mStatements m) }
1900
1901
1902 logDebugVerbose $ vcat
1903 [ "Name :" <+> pretty name
1904 , "Previously :" <+> vcat [ pretty (show d) | (n,d) <- representations, n == name ]
1905 , "This guy :" <+> pretty (show domain)
1906 , "usedBefore? :" <+> pretty usedBefore
1907 ]
1908
1909 return model
1910 >>= addStructurals -- unless usedBefore: add structurals
1911 >>= addChannels -- for each in previously recorded representation
1912 >>= recordThis -- unless usedBefore: record (name, domain) as being used in the model
1913 >>= fixReprForAllOthers -- fix the representation of this guy in the whole model, if channelling=no
1914 >>= fixReprForSameRegion -- fix the representation of this guy in the whole model,
1915 -- for those references with the same "region"
1916 >>= resolveNames -- we need to re-resolve names to avoid repeatedly selecting representations
1917 -- for abstract stuff inside aliases.
1918
1919
1920 rule_ChooseReprForComprehension :: Config -> Rule
1921 rule_ChooseReprForComprehension config = Rule "choose-repr-for-comprehension" (const theRule) where
1922
1923 theRule (Comprehension body gensOrConds) = do
1924 (gocBefore, (nm, domain), gocAfter) <- matchFirst gensOrConds $ \case
1925 Generator (GenDomainNoRepr (Single nm) domain) -> return (nm, domain)
1926 _ -> na "rule_ChooseReprForComprehension"
1927
1928 let reprsWhichOrder
1929 | representationsGivens config == Sparse = reprsSparseOrder
1930 | not (representationLevels config ) = reprsStandardOrderNoLevels
1931 | otherwise = reprsStandardOrder
1932 domOpts <- reprOptions reprsWhichOrder domain
1933 when (null domOpts) $
1934 bug $ "No representation matches this beast:" <++> pretty domain
1935
1936 return
1937 [ RuleResult
1938 { ruleResultDescr = "Choosing representation for quantified variable" <+>
1939 pretty nm <> ":" <++> pretty thisDom
1940 , ruleResultType = ChooseRepr_Quantified
1941 , ruleResult = bugFailT "rule_ChooseReprForComprehension" $ do
1942 outDomains <- downD (nm, thisDom)
1943 structurals <- mkStructurals nm thisDom
1944 let updateRepr (Reference nm' _)
1945 | nm == nm'
1946 = Reference nm (Just (DeclHasRepr Quantified nm thisDom))
1947 updateRepr p = p
1948 let out' = Comprehension (transform updateRepr body)
1949 $ gocBefore
1950 ++ [ Generator (GenDomainHasRepr name dom)
1951 | (name, dom) <- outDomains ]
1952 ++ map Condition structurals
1953 ++ transformBi updateRepr gocAfter
1954 out <- resolveNamesX out'
1955 return out
1956 , ruleResultHook = Nothing
1957 , ruleResultSize = return $ expressionDepth $ Reference nm (Just (DeclHasRepr Quantified nm thisDom))
1958 }
1959 | thisDom <- domOpts
1960 ]
1961 theRule _ = na "rule_ChooseReprForComprehension"
1962
1963 mkStructurals name domain = do
1964 let ref = Reference name (Just (DeclHasRepr Quantified name domain))
1965 gen <- getStructurals downX1 domain
1966 gen ref
1967
1968
1969 rule_ChooseReprForLocals :: Config -> Rule
1970 rule_ChooseReprForLocals config = Rule "choose-repr-for-locals" (const theRule) where
1971
1972 theRule (WithLocals body (AuxiliaryVars locals)) = do
1973 (stmtBefore, (nm, domain), stmtAfter) <- matchFirst locals $ \case
1974 Declaration (FindOrGiven LocalFind nm domain) -> return (nm, domain)
1975 _ -> na "rule_ChooseReprForLocals"
1976
1977 let
1978 isReferencedWithoutRepr (Reference nm' (Just DeclNoRepr{})) | nm == nm' = True
1979 isReferencedWithoutRepr _ = False
1980
1981 unless (any isReferencedWithoutRepr (universeBi (body, stmtBefore, stmtAfter))) $
1982 na $ "This local variable seems to be handled before:" <+> pretty nm
1983
1984 let reprsWhichOrder
1985 | representationsAuxiliaries config == Sparse = reprsSparseOrder
1986 | not (representationLevels config) = reprsStandardOrderNoLevels
1987 | otherwise = reprsStandardOrder
1988 domOpts <- reprOptions reprsWhichOrder domain
1989 when (null domOpts) $
1990 bug $ "No representation matches this beast:" <++> pretty domain
1991
1992 return
1993 [ RuleResult
1994 { ruleResultDescr = "Choosing representation for auxiliary variable" <+>
1995 pretty nm <> ":" <++> pretty thisDom
1996 , ruleResultType = ChooseRepr_Auxiliary
1997 , ruleResult = bugFailT "rule_ChooseReprForLocals" $ do
1998 outDomains <- downD (nm, thisDom)
1999 structurals <- mkStructurals nm thisDom
2000 let updateRepr (Reference nm' _)
2001 | nm == nm'
2002 = Reference nm (Just (DeclHasRepr LocalFind nm thisDom))
2003 updateRepr p = p
2004 let out' = WithLocals (transform updateRepr body) $ AuxiliaryVars
2005 ( stmtBefore
2006 ++ [ Declaration (FindOrGiven
2007 LocalFind
2008 name
2009 (forgetRepr dom))
2010 | (name, dom) <- outDomains ]
2011 ++ [ SuchThat structurals | not (null structurals) ]
2012 ++ transformBi updateRepr stmtAfter
2013 )
2014 out <- resolveNamesX out'
2015 return out
2016 , ruleResultHook = Nothing
2017 , ruleResultSize = return $ expressionDepth $ Reference nm (Just (DeclHasRepr LocalFind nm thisDom))
2018 }
2019 | thisDom <- domOpts
2020 ]
2021 theRule _ = na "rule_ChooseReprForLocals"
2022
2023 mkStructurals name domain = do
2024 let ref = Reference name (Just (DeclHasRepr LocalFind name domain))
2025 gen <- getStructurals downX1 domain
2026 gen ref
2027
2028
2029 rule_GeneratorsFirst :: Rule
2030 rule_GeneratorsFirst = "generators-first" `namedRule` theRule where
2031 theRule (Comprehension body [])
2032 = return
2033 ( "Empty generators."
2034 , return $ AbstractLiteral $ AbsLitMatrix (mkDomainIntB 1 1) [body]
2035 )
2036 theRule (Comprehension body gensOrConds)
2037 | let (gens, rest) = mconcat
2038 [ case x of
2039 Generator{} -> ([x],[])
2040 _ -> ([],[x])
2041 | x <- gensOrConds
2042 ]
2043 , let gensOrConds' = gens ++ rest
2044 , gensOrConds /= gensOrConds'
2045 = return
2046 ( "Generators come first."
2047 , return $ Comprehension body gensOrConds'
2048 )
2049 theRule (Comprehension body gensOrConds)
2050 | let (lettings :: [Name], rest :: [GeneratorOrCondition]) = mconcat
2051 [ case x of
2052 ComprehensionLetting pat _ -> (universeBi pat,[] )
2053 _ -> ([] ,[x])
2054 | x <- gensOrConds
2055 ]
2056 , let f (Reference nm (Just (Alias x))) | nm `elem` lettings = f x
2057 f x = x
2058 , not (null lettings)
2059 = return
2060 ( "Inlining comprehension lettings."
2061 , return $ transformBi f $ Comprehension body rest
2062 )
2063 theRule _ = na "rule_GeneratorsFirst"
2064
2065
2066 rule_Eq :: Rule
2067 rule_Eq = "identical-domain-eq" `namedRule` theRule where
2068 theRule p = do
2069 (x,y) <- match opEq p
2070 domX <- domainOf x
2071 domY <- domainOf y
2072 unless (domX == domY) $ na "rule_Eq domains not identical"
2073 sameRepresentationTree x y
2074 xs <- downX x
2075 ys <- downX y
2076 unless (length xs == length ys) $ na "rule_Eq"
2077 when (xs == [x]) $ na "rule_Eq"
2078 when (ys == [y]) $ na "rule_Eq"
2079 return
2080 ( "Generic vertical rule for identical-domain equality"
2081 , return $ make opAnd $ fromList $ zipWith (\ i j -> [essence| &i = &j |] ) xs ys
2082 )
2083
2084
2085 rule_Neq :: Rule
2086 rule_Neq = "identical-domain-neq" `namedRule` theRule where
2087 theRule p = do
2088 (x,y) <- match opNeq p
2089 domX <- domainOf x
2090 domY <- domainOf y
2091 unless (domX == domY) $ na "rule_Neq domains not identical"
2092 sameRepresentationTree x y
2093 xs <- downX x
2094 ys <- downX y
2095 unless (length xs == length ys) $ na "rule_Neq"
2096 when (xs == [x]) $ na "rule_Neq"
2097 when (ys == [y]) $ na "rule_Neq"
2098 return
2099 ( "Generic vertical rule for identical-domain equality"
2100 , return $ make opOr $ fromList $ zipWith (\ i j -> [essence| &i != &j |] ) xs ys
2101 )
2102
2103
2104 rule_QuickPermutationOrder :: Rule
2105 rule_QuickPermutationOrder = "generic-QuickPermutationOrder" `namedRule` theRule where
2106 theRule p@(match opQuickPermutationOrder -> Just (ps, x)) = do
2107 x_ord <- symmetryOrdering x
2108 let rhs = make opTransform ps x_ord
2109 return
2110 ( "Generic vertical rule for quickPermutationOrder:" <+> pretty p
2111 , return [essence| &x_ord .<= &rhs |]
2112 )
2113 theRule _ = na "rule_QuickPermutationOrder"
2114
2115
2116 rule_DotLtLeq :: Rule
2117 rule_DotLtLeq = "generic-DotLtLeq" `namedRule` theRule where
2118 theRule p = do
2119 (a,b,mk) <- case p of
2120 [essence| &a .< &b |] -> return ( a, b, \ i j -> [essence| &i <lex &j |] )
2121 [essence| &a .<= &b |] -> return ( a, b, \ i j -> [essence| &i <=lex &j |] )
2122 _ -> na "rule_DotLtLeq"
2123 -- at this point, tuples vs matrix literal shouldn't matter
2124 -- replace tuple literals with matrix literals
2125 let
2126 tupleLitToMatrixLit (AbstractLiteral (AbsLitTuple xs)) = do
2127 xs' <- forM xs $ \ x -> do
2128 ty <- typeOf x
2129 let x' = oneDimensionaliser (matrixNumDims ty) x
2130 return x'
2131 return (fromList xs')
2132 tupleLitToMatrixLit x = return x
2133 ma <- symmetryOrdering a >>= resolveNamesX >>= transformM tupleLitToMatrixLit >>= return . make opFlatten
2134 mb <- symmetryOrdering b >>= resolveNamesX >>= transformM tupleLitToMatrixLit >>= return . make opFlatten
2135 return
2136 ( "Generic vertical rule for dotLt and dotLeq:" <+> pretty p
2137 , return $ mk ma mb
2138 )
2139
2140
2141 rule_Flatten_Lex :: Rule
2142 rule_Flatten_Lex = "flatten-lex" `namedRule` theRule where
2143 theRule [essence| &a <lex &b |] = do
2144 reject_flat a b
2145 fa <- flatten a
2146 fb <- flatten b
2147 tfa <- typeOf fa
2148 tfb <- typeOf fb
2149 case (tfa, tfb) of
2150 (TypeList TypeInt{}, TypeList TypeInt{}) -> return ()
2151 (TypeMatrix TypeInt{} TypeInt{}, TypeMatrix TypeInt{} TypeInt{}) -> return ()
2152 _ -> bug $ "flattener: " <+> vcat [stringToDoc $ show tfa, stringToDoc $ show tfb]
2153 return ( "Flatten Lex less"
2154 , return [essence| &fa <lex &fb |]
2155 )
2156 theRule [essence| &a <=lex &b |] = do
2157 reject_flat a b
2158 fa <- flatten a
2159 fb <- flatten b
2160 tfa <- typeOf fa
2161 tfb <- typeOf fb
2162 case (tfa, tfb) of
2163 (TypeList TypeInt{}, TypeList TypeInt{}) -> return ()
2164 (TypeMatrix TypeInt{} TypeInt{}, TypeMatrix TypeInt{} TypeInt{}) -> return ()
2165 _ -> bug $ "flattener: " <+> vcat [stringToDoc $ show tfa, stringToDoc $ show tfb]
2166 return ( "Flatten Lex Lt"
2167 , return [essence| &fa <=lex &fb |]
2168 )
2169 theRule _ = na "rule_Flatten_Lex"
2170 reject_flat a b = do
2171 ta <- typeOf a
2172 tb <- typeOf b
2173 case (ta, tb) of
2174 (TypeMatrix TypeBool TypeInt{}, _) ->
2175 na "rule_Flatten_Lex"
2176 (TypeMatrix TypeBool TypeBool, _) ->
2177 na "rule_Flatten_Lex"
2178 (TypeList TypeInt{}, _) ->
2179 na "rule_Flatten_Lex"
2180 (TypeMatrix TypeInt{} TypeInt{}, _) ->
2181 na "rule_Flatten_Lex"
2182 (TypeList TypeBool, _) ->
2183 na "rule_Flatten_Lex"
2184 (TypeMatrix TypeInt{} TypeBool, _) ->
2185 na "rule_Flatten_Lex"
2186 _ -> return ()
2187
2188 flatten a = do
2189 ta <- typeOf a
2190 case ta of
2191 TypeBool -> return [essence| [-toInt(&a)] |]
2192 TypeInt{} -> return [essence| [&a] |]
2193 TypeList TypeInt{} -> return a
2194 TypeMatrix TypeInt{} TypeInt{} -> return a
2195 TypeTuple ts -> do
2196 case a of
2197 AbstractLiteral x -> do
2198 case x of
2199 AbsLitTuple xs -> do
2200 fxs <- mapM flatten xs
2201 let flatxs = fromList fxs
2202 return [essence| flatten(&flatxs) |]
2203 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this abslit fellow..."
2204 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2205 Constant c ->
2206 case c of
2207 ConstantAbstract ca ->
2208 case ca of
2209 AbsLitTuple xs -> do
2210 fxs <- mapM flatten (Constant <$> xs)
2211 let flatxs = fromList fxs
2212 return [essence| flatten(&flatxs) |]
2213 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2214 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2215 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2216 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2217 Op _ -> do
2218 (oName, o) <- quantifiedVar
2219 flatten $ Comprehension o [ComprehensionLetting oName a]
2220 _ -> do
2221 ps <- mapM (\(i,_) -> do
2222 (Single nm, tm) <- quantifiedVar
2223 return (i,nm,tm)) (zip [1..] ts)
2224 let lts = (\(i,nm,_tm) -> ComprehensionLetting (Single nm) [essence| &a[&i] |]) <$> ps
2225 tup = AbstractLiteral $ AbsLitTuple $ (\(_,_,tm) -> tm) <$> ps
2226 flatten $ Comprehension tup lts
2227 _ ->
2228 case a of
2229 AbstractLiteral x -> do
2230 case x of
2231 AbsLitMatrix _ xs -> do
2232 fxs <- mapM flatten xs
2233 let flatxs = fromList fxs
2234 return [essence| flatten(&flatxs) |]
2235 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this abslit fellow..."
2236 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2237 Constant c ->
2238 case c of
2239 ConstantAbstract ca ->
2240 case ca of
2241 AbsLitMatrix _ [] ->
2242 return [essence| ([] : `matrix indexed by [int()] of int`) |]
2243 AbsLitMatrix _ xs -> do
2244 fxs <- mapM flatten (Constant <$> xs)
2245 let flatxs = fromList fxs
2246 return [essence| flatten(&flatxs) |]
2247 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2248 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2249 TypedConstant tc _ -> flatten (Constant tc)
2250 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2251 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2252 Op _ -> do
2253 (oName, o) <- quantifiedVar
2254 flatten $ Comprehension o [ComprehensionLetting oName a]
2255 Reference nm ex ->
2256 bug $ "rule_FlattenLex: flatten isn't defined for this reference fellow..."
2257 <+> vcat [stringToDoc (show a)
2258 ,"reference:" <+> stringToDoc (show nm)
2259 ,"fellow:" <+> stringToDoc (show ex)]
2260 Comprehension body gocs -> do
2261 fbody <- flatten body
2262 let comp = Comprehension fbody gocs
2263 return [essence| flatten(&comp) |]
2264 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this expression fellow..."
2265
2266 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2267
2268
2269 rule_ReducerToComprehension :: Rule
2270 rule_ReducerToComprehension = "reducer-to-comprehension" `namedRule` theRule where
2271 theRule p = do
2272 (_, _, mk, coll) <- match opReducer p
2273 -- leave comprehensions alone
2274 let
2275 isComprehension Comprehension{} = True
2276 isComprehension _ = False
2277 case followAliases isComprehension coll of
2278 True -> na "rule_ReducerToComprehension"
2279 False -> return ()
2280 -- leave matrix literals alone
2281 case tryMatch matrixLiteral coll of
2282 Nothing -> return ()
2283 Just {} -> na "rule_ReducerToComprehension"
2284 tyColl <- typeOf coll
2285 howToIndex <- case tyColl of
2286 TypeSequence{} -> return $ Left ()
2287 TypeMatrix{} -> return $ Right ()
2288 TypeList{} -> return $ Right ()
2289 TypeSet{} -> return $ Right ()
2290 TypeMSet{} -> return $ Right ()
2291 _ -> na "rule_ReducerToComprehension"
2292 return
2293 ( "Creating a comprehension for the collection inside the reducer operator."
2294 , do
2295 (iPat, i) <- quantifiedVar
2296 case howToIndex of
2297 Left{} -> return $ mk [essence| [ &i[2] | &iPat <- &coll ] |]
2298 Right{} -> return $ mk [essence| [ &i | &iPat <- &coll ] |]
2299 )
2300
2301
2302 rule_TrueIsNoOp :: Rule
2303 rule_TrueIsNoOp = "true-is-noop" `namedRule` theRule where
2304 theRule (Op (MkOpTrue (OpTrue ref))) =
2305 case ref of
2306 Reference _ (Just DeclHasRepr{}) ->
2307 return ( "Remove the argument from true."
2308 , return $ Constant $ ConstantBool True
2309 )
2310 _ -> na "The argument of true doesn't have a representation."
2311 theRule _ = na "rule_TrueIsNoOp"
2312
2313
2314 rule_FlattenOf1D :: Rule
2315 rule_FlattenOf1D = "flatten-of-1D" `namedRule` theRule where
2316 theRule p = do
2317 x <- match opFlatten p
2318 tyx <- typeOf x
2319 out <- case tyx of
2320 TypeList TypeBool{} -> return x
2321 TypeList TypeInt{} -> return x
2322 TypeMatrix _ TypeBool{} -> return x
2323 TypeMatrix _ TypeInt{} -> return x
2324 TypeMatrix{} -> -- more than 1D
2325 case listOut x of
2326 Just [y] -> return (make opFlatten y)
2327 _ -> na "rule_FlattenOf1D"
2328 _ -> na "rule_FlattenOf1D"
2329 return ( "1D matrices do not need a flatten."
2330 , return out
2331 )
2332
2333
2334 rule_Decompose_AllDiff :: Rule
2335 rule_Decompose_AllDiff = "decompose-allDiff" `namedRule` theRule where
2336 theRule [essence| allDiff(&m) |] = do
2337 ty <- typeOf m
2338 case ty of
2339 TypeMatrix _ TypeBool -> na "allDiff can stay"
2340 TypeMatrix _ (TypeInt _) -> na "allDiff can stay"
2341 TypeMatrix _ _ -> return ()
2342 _ -> na "allDiff on something other than a matrix."
2343 index:_ <- indexDomainsOf m
2344 return
2345 ( "Decomposing allDiff. Type:" <+> pretty ty
2346 , do
2347 (iPat, i) <- quantifiedVar
2348 (jPat, j) <- quantifiedVar
2349 let indexInto matrix ix =
2350 case match opMatrixIndexingSlicing matrix of
2351 Just (base, indices) ->
2352 make opMatrixIndexingSlicing base (replaceFirstSlice ix indices)
2353 Nothing ->
2354 [essence| &matrix[&ix] |]
2355 replaceFirstSlice ix = \case
2356 Right _ : rest -> Left ix : rest
2357 indexer : rest -> indexer : replaceFirstSlice ix rest
2358 [] -> []
2359 mi = indexInto m i
2360 mj = indexInto m j
2361 return
2362 [essence|
2363 and([ &mi != &mj
2364 | &iPat : &index
2365 , &jPat : &index
2366 , &i < &j
2367 ])
2368 |]
2369 )
2370 theRule _ = na "rule_Decompose_AllDiff"
2371
2372
2373 rule_Decompose_AllDiff_MapToSingleInt :: Rule
2374 rule_Decompose_AllDiff_MapToSingleInt = "decompose-allDiff-mapToSingleInt" `namedRule` theRule where
2375 theRule [essence| allDiff(&m) |] = do
2376 case m of
2377 Comprehension body gensOrConds -> do
2378 tyBody <- typeOf body
2379 case tyBody of
2380 TypeBool -> na "rule_Decompose_AllDiff_MapToSingleInt"
2381 TypeInt _ -> na "rule_Decompose_AllDiff_MapToSingleInt"
2382 TypeTuple{} -> do
2383 bodyBits <- downX1 body
2384 bodyBitSizes <- forM bodyBits $ \ b -> do
2385 bDomain <- domainOf b
2386 domainSizeOf bDomain
2387 case (bodyBits, bodyBitSizes) of
2388 ([a,b], [_a',b']) -> do
2389 let body'= [essence| &a * &b' + &b |]
2390 let m' = Comprehension body' gensOrConds
2391 return
2392 ( "Decomposing allDiff"
2393 , return [essence| allDiff(&m') |]
2394 )
2395 _ -> na "rule_Decompose_AllDiff_MapToSingleInt"
2396 _ -> na "allDiff on something other than a comprehension."
2397 _ -> na "allDiff on something other than a comprehension."
2398 theRule _ = na "rule_Decompose_AllDiff_MapToSingleInt"
2399
2400
2401 rule_DomainCardinality :: Rule
2402 rule_DomainCardinality = "domain-cardinality" `namedRule` theRule where
2403 theRule p = do
2404 maybeDomain <- match opTwoBars p
2405 d <- expandDomainReference <$> case maybeDomain of
2406 Domain d -> return d
2407 Reference _ (Just (Alias (Domain d))) -> return d
2408 _ -> na "rule_DomainCardinality"
2409 return
2410 ( "Cardinality of a domain"
2411 , case d of
2412 DomainInt _ [RangeBounded 1 u] -> return u
2413 _ -> do
2414 (iPat, _) <- quantifiedVar
2415 return [essence| sum([ 1 | &iPat : &d ]) |]
2416 )
2417
2418
2419 rule_DomainMinMax :: Rule
2420 rule_DomainMinMax = "domain-MinMax" `namedRule` theRule where
2421 theRule [essence| max(&maybeDomain) |] = do
2422 d <- getDomain maybeDomain
2423 return
2424 ( "max of a domain"
2425 , maxOfDomain d
2426 )
2427 theRule [essence| min(&maybeDomain) |] = do
2428 d <- getDomain maybeDomain
2429 return
2430 ( "min of a domain"
2431 , minOfDomain d
2432 )
2433 theRule _ = na "rule_DomainMinMax"
2434
2435 getDomain :: MonadFailDoc m => Expression -> m (Domain () Expression)
2436 getDomain (Domain d) = return d
2437 getDomain (Reference _ (Just (Alias (Domain d)))) = getDomain (Domain d)
2438 getDomain _ = na "rule_DomainMinMax.getDomain"
2439
2440
2441 rule_ComplexAbsPat :: Rule
2442 rule_ComplexAbsPat = "complex-pattern" `namedRule` theRule where
2443 theRule (Comprehension body gensOrConds) = do
2444 (gocBefore, (pat, domainOrExpr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
2445 Generator (GenDomainNoRepr pat@AbsPatTuple{} domain) -> return (pat, Left domain)
2446 Generator (GenInExpr pat@AbsPatTuple{} expr) -> return (pat, Right expr)
2447 _ -> na "rule_ComplexAbsPat"
2448 return
2449 ( "complex pattern on tuple patterns"
2450 , do
2451 (iPat, i) <- quantifiedVar
2452 let replacements = [ (p, make opMatrixIndexing i (map (fromInt . fromIntegral) is))
2453 | (p, is) <- genMappings pat
2454 ]
2455 let f x@(Reference nm _) = fromMaybe x (lookup nm replacements)
2456 f x = x
2457 return $ Comprehension (transform f body)
2458 $ gocBefore
2459 ++ [ either (Generator . GenDomainNoRepr iPat)
2460 (Generator . GenInExpr iPat)
2461 domainOrExpr ]
2462 ++ transformBi f gocAfter
2463 )
2464 theRule _ = na "rule_ComplexAbsPat"
2465
2466 -- i --> i -> []
2467 -- (i,j) --> i -> [1]
2468 -- j -> [2]
2469 -- (i,(j,k)) --> i -> [1]
2470 -- j -> [2,1]
2471 -- k -> [2,2]
2472 genMappings :: AbstractPattern -> [(Name, [Int])]
2473 genMappings (Single nm) = [(nm, [])]
2474 genMappings (AbsPatTuple pats)
2475 = concat
2476 [ [ (patCore, i:is) | (patCore, is) <- genMappings pat ]
2477 | (i, pat) <- zip [1..] pats
2478 ]
2479 genMappings (AbsPatMatrix pats)
2480 = concat
2481 [ [ (patCore, i:is) | (patCore, is) <- genMappings pat ]
2482 | (i, pat) <- zip [1..] pats
2483 ]
2484 genMappings pat = bug ("rule_ComplexLambda.genMappings:" <+> pretty (show pat))
2485
2486
2487 -- this rule doesn't use `namedRule` because it need access to ascendants through the zipper
2488 rule_InlineConditions :: Rule
2489 rule_InlineConditions = "inline-conditions" `namedRuleZ` theRule where
2490 theRule z (Comprehension body gensOrConds) = do
2491 let (toInline, toKeep) = mconcat
2492 [ case goc of
2493 Condition x | categoryOf x == CatDecision -> ([x],[])
2494 _ -> ([],[goc])
2495 | goc <- gensOrConds
2496 ]
2497 theGuard <- case toInline of
2498 [] -> na "No condition to inline."
2499 [x] -> return x
2500 xs -> return $ make opAnd $ fromList xs
2501 (nameQ, opSkip) <- queryQ z
2502 let bodySkipped = opSkip theGuard body
2503 return
2504 ( "Inlining conditions, inside" <+> nameQ
2505 , return $ Comprehension bodySkipped toKeep
2506 )
2507 theRule _ _ = na "rule_InlineConditions"
2508
2509 -- keep going up, until finding a quantifier
2510 -- when found, return the skipping operator for the quantifier
2511 -- if none exists, do not apply the rule.
2512 -- (or maybe we should call bug right ahead, it can't be anything else.)
2513 queryQ z0 =
2514 case Zipper.up z0 of
2515 Nothing -> na "rule_InlineConditions (meh-1)"
2516 Just z -> do
2517 let h = hole z
2518 case ( match opAnd h, match opOr h, match opSum h, match opProduct h
2519 , match opMin h, match opMax h, match opOrdering h ) of
2520 (Just{}, _, _, _, _, _, _) -> return ("and", opAndSkip)
2521 (_, Just{}, _, _, _, _, _) -> return ("or" , opOrSkip )
2522 (_, _, Just{}, _, _, _, _) -> return ("sum", opSumSkip)
2523 (_, _, _, Just{}, _, _, _) -> return ("product", opProductSkip)
2524 (_, _, _, _, Just{}, _, _) -> na "rule_InlineConditions (min)"
2525 (_, _, _, _, _, Just{}, _) -> na "rule_InlineConditions (max)"
2526 (_, _, _, _, _, _, Just{}) -> return ("ordering", opSumSkip)
2527 _ -> na "rule_InlineConditions (meh-2)"
2528 -- case Zipper.up z of
2529 -- Nothing -> na "queryQ"
2530 -- Just u -> queryQ u
2531
2532 opAndSkip b x = [essence| &b -> &x |]
2533 opOrSkip b x = [essence| &b /\ &x |]
2534 opSumSkip b x = [essence| toInt(&b) * catchUndef(&x, 0) |]
2535 opProductSkip b x = [essence| [ 1
2536 , catchUndef(&x,1)
2537 ; int(0..1)
2538 ] [toInt(&b)] |]
2539
2540
2541 rule_InlineConditions_AllDiff :: Rule
2542 rule_InlineConditions_AllDiff = "inline-conditions-allDiff" `namedRule` theRule where
2543 theRule (Op (MkOpAllDiff (OpAllDiff (Comprehension body gensOrConds)))) = do
2544 let (toInline, toKeep) = mconcat
2545 [ case goc of
2546 Condition x | categoryOf x == CatDecision -> ([x],[])
2547 _ -> ([],[goc])
2548 | goc <- gensOrConds
2549 ]
2550 theGuard <- case toInline of
2551 [] -> na "No condition to inline."
2552 [x] -> return x
2553 xs -> return $ make opAnd $ fromList xs
2554
2555 tyBody <- typeOf body
2556 case tyBody of
2557 TypeInt{} -> return ()
2558 _ -> na "rule_InlineConditions_AllDiff, not an int"
2559 domBody <- domainOf body
2560 let
2561 collectLowerBounds (RangeSingle x) = return x
2562 collectLowerBounds (RangeBounded x _) = return x
2563 collectLowerBounds _ = userErr1 ("Unexpected infinite domain:" <+> pretty domBody)
2564
2565 collectLowerBoundsD (DomainInt _ rs) = mapM collectLowerBounds rs
2566 collectLowerBoundsD _ = userErr1 ("Expected an integer domain, but got:" <+> pretty domBody)
2567
2568 bounds <- collectLowerBoundsD domBody
2569 let lowerBound = make opMin (fromList bounds)
2570
2571 -- for each element, we do element-lowerBound+1
2572 -- this makes sure the smallest element is 1
2573 -- hence we can use 0 as the except value!
2574 let bodySkipped = [essence| toInt(&theGuard) * catchUndef(&body + (1 - &lowerBound), 0) |]
2575
2576 return
2577 ( "Inlining conditions, inside allDiff"
2578 , return $ make opAllDiffExcept (Comprehension bodySkipped toKeep) 0
2579 )
2580 theRule _ = na "rule_InlineConditions_AllDiff"
2581
2582
2583 rule_InlineConditions_MaxMin :: Rule
2584 rule_InlineConditions_MaxMin = "aux-for-MaxMin" `namedRule` theRule where
2585 theRule p = do
2586 when (categoryOf p < CatDecision) $ na "rule_InlineConditions_MaxMin"
2587 (nameQ, binOp, Comprehension body gensOrConds) <-
2588 case (match opMax p, match opMin p) of
2589 (Just res, _) -> return ("max", \ a b -> [essence| &a <= &b |], res )
2590 (_, Just res) -> return ("min", \ a b -> [essence| &a >= &b |], res )
2591 _ -> na "rule_InlineConditions_MaxMin"
2592 let
2593 (toInline, gocInExpr, _toKeep) = mconcat
2594 [ case goc of
2595 Condition x | categoryOf x == CatDecision -> ([x],[],[])
2596 Generator (GenInExpr {}) -> ([],[goc],[])
2597 _ -> ([],[],[goc])
2598 | goc <- gensOrConds
2599 ]
2600 when (null toInline && null gocInExpr) $ na "rule_InlineConditions_MaxMin"
2601 auxDomain <- domainOf body
2602 return
2603 ( "Creating auxiliary variable for a" <+> nameQ
2604 , do
2605 (auxName, aux) <- auxiliaryVar
2606 let auxDefinedLHS = make opSum (Comprehension 1 gensOrConds)
2607 let auxDefined = [essence| &auxDefinedLHS > 0 |]
2608 let auxUndefined = [essence| &auxDefinedLHS = 0 |]
2609 let aux' = WithLocals aux (DefinednessConstraints [auxDefined])
2610 return $ WithLocals aux'
2611 (AuxiliaryVars
2612 [ Declaration (FindOrGiven LocalFind auxName auxDomain)
2613 , SuchThat
2614 [ make opAnd $ Comprehension
2615 (binOp body aux)
2616 gensOrConds
2617
2618 -- either one of the members of this comprehension, or dontCare
2619 -- if it is indeed dontCare, care should be taken to make sure it isn't used as a normal value
2620 , make opAnd $ fromList
2621 [ make opImply auxDefined
2622 (make opOr $ Comprehension
2623 [essence| &body = &aux |]
2624 gensOrConds)
2625 , make opImply auxUndefined (make opDontCare aux)
2626 ]
2627 ]
2628 ])
2629 )
2630
2631
2632 rule_AttributeToConstraint :: Rule
2633 rule_AttributeToConstraint = "attribute-to-constraint" `namedRule` theRule where
2634 theRule (Op (MkOpAttributeAsConstraint (OpAttributeAsConstraint thing attr mval))) = do
2635 dom <- domainOf thing
2636 let conv = mkAttributeToConstraint dom attr mval thing
2637 return
2638 ( "Converting an attribute to a constraint"
2639 , bugFailT "rule_AttributeToConstraint" conv
2640 )
2641 theRule _ = na "rule_AttributeToConstraint"
2642
2643
2644 timedF :: MonadIO m => String -> (a -> m b) -> a -> m b
2645 timedF name comp a = timeItNamed name (comp a)
2646
2647
2648 evaluateModel ::
2649 MonadFailDoc m =>
2650 NameGen m =>
2651 EnumerateDomain m =>
2652 (?typeCheckerMode :: TypeCheckerMode) =>
2653 Model -> m Model
2654 evaluateModel m = do
2655 let
2656 full (Reference _ (Just (DeclHasRepr _ _ (singletonDomainInt -> Just val)))) =
2657 return val
2658 full p@Constant{} = return p
2659 full p@Domain{} = return p
2660 full p = do
2661 mconstant <- runExceptT (instantiateExpression [] p)
2662 case mconstant of
2663 Left{} -> return p
2664 Right constant ->
2665 if null [() | ConstantUndefined{} <- universe constant] -- if there are no undefined values in it
2666 then return (Constant constant)
2667 else return p
2668 let
2669 partial (Op op)
2670 | Just (x, y) <- case op of
2671 MkOpLeq (OpLeq x y) -> Just (x,y)
2672 MkOpGeq (OpGeq x y) -> Just (x,y)
2673 MkOpEq (OpEq x y) -> Just (x,y)
2674 _ -> Nothing
2675 , Reference nmX _ <- x
2676 , Reference nmY _ <- y
2677 , nmX == nmY
2678 , categoryOf x <= CatQuantified
2679 , categoryOf y <= CatQuantified
2680 = return (fromBool True)
2681 partial p@(Op x) = do
2682 mx' <- runExceptT (simplifyOp x)
2683 case mx' of
2684 Left{} -> return p
2685 Right x' -> do
2686 when (Op x == x') $ bug $ vcat
2687 [ "rule_PartialEvaluate, simplifier returns the input unchanged."
2688 , "input:" <+> vcat [ pretty (Op x)
2689 , pretty (show (Op x))
2690 ]
2691 ]
2692 return x'
2693 partial p = return p
2694
2695 (descendBiM full >=> transformBiM partial) m
2696
2697
2698 rule_FullEvaluate :: Rule
2699 rule_FullEvaluate = "full-evaluate" `namedRule` theRule where
2700 theRule Constant{} = na "rule_FullEvaluate"
2701 theRule Domain{} = na "rule_FullEvaluate"
2702 theRule (Reference _ (Just (Alias x))) -- selectively inline, unless x is huge
2703 | Just Comprehension{} <- match opToSet x
2704 = return ("Inline alias", return x)
2705 theRule p = do
2706 constant <- instantiateExpression [] p
2707 unless (null [() | ConstantUndefined{} <- universe constant]) $
2708 na "rule_PartialEvaluate, undefined"
2709 return ("Full evaluator", return $ Constant constant)
2710
2711
2712 rule_PartialEvaluate :: Rule
2713 rule_PartialEvaluate = "partial-evaluate" `namedRuleZ` theRule where
2714 -- if a variable only has a single value in its domain, replace it with the value
2715 theRule z (Reference _ (Just (DeclHasRepr _ _ (singletonDomainInt -> Just val)))) =
2716 case hole <$> Zipper.up z of
2717 Just (Op (MkOpTrue _)) -> na "rule_PartialEvaluate, inside a true(ref)"
2718 _ -> return ( "Partial evaluator"
2719 , return val
2720 )
2721 theRule _ (Op op)
2722 | Just (x, y) <- case op of
2723 MkOpLeq (OpLeq x y) -> Just (x,y)
2724 MkOpGeq (OpGeq x y) -> Just (x,y)
2725 MkOpEq (OpEq x y) -> Just (x,y)
2726 _ -> Nothing
2727 , Reference nmX _ <- x
2728 , Reference nmY _ <- y
2729 , nmX == nmY
2730 , categoryOf x <= CatQuantified
2731 , categoryOf y <= CatQuantified
2732 = return
2733 ( "Parameter = parameter (or quantified)"
2734 , return (fromBool True)
2735 )
2736 theRule _ (Op x) = do
2737 x' <- simplifyOp x
2738 when (Op x == x') $ bug $ vcat
2739 [ "rule_PartialEvaluate, simplifier returns the input unchanged."
2740 , "input:" <+> vcat [ pretty (Op x)
2741 , pretty (show (Op x))
2742 ]
2743 ]
2744 return
2745 ( "Partial evaluator"
2746 , return x'
2747 )
2748 theRule _ _ = na "rule_PartialEvaluate"
2749
2750
2751 -- | shifting quantifiers inwards, if they operate on a row of a 2d matrix,
2752 -- make them operate on the rows directly then index
2753 rule_QuantifierShift :: Rule
2754 rule_QuantifierShift = "quantifier-shift" `namedRule` theRule where
2755 theRule p = do
2756 (_, _, mkQuan, inner) <- match opReducer p
2757 (matrix, indexer) <- match opIndexing inner
2758 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2759 case ty of
2760 TypeMatrix{} -> return ()
2761 TypeList{} -> return ()
2762 _ -> na "rule_QuantifierShift"
2763 return
2764 ( "Shifting quantifier inwards"
2765 , return $ make opIndexing
2766 (make matrixLiteral
2767 ty
2768 index
2769 (map mkQuan elems))
2770 indexer
2771 )
2772
2773
2774 -- | shifting quantifiers inwards, if they operate on a flattened multi-dim matrix.
2775 rule_QuantifierShift2 :: Rule
2776 rule_QuantifierShift2 = "quantifier-shift2" `namedRule` theRule where
2777 theRule p = do
2778 (_, _, mkQuan, inner) <- match opReducer p
2779 matrix <- match opFlatten inner
2780 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2781 case ty of
2782 TypeMatrix{} -> return () -- the matrix literal should contain further matrix/list stuff.
2783 TypeList{} -> return ()
2784 _ -> na "rule_QuantifierShift2"
2785 return
2786 ( "Shifting quantifier inwards"
2787 , return $ mkQuan
2788 (make matrixLiteral
2789 ty
2790 index
2791 (map (mkQuan . flattenIfNeeded (matrixNumDims ty)) elems))
2792 )
2793
2794
2795 -- | shifting quantifiers inwards, if they operate on a concatenated multi-dim matrix.
2796 rule_QuantifierShift3 :: Rule
2797 rule_QuantifierShift3 = "quantifier-shift3" `namedRule` theRule where
2798 theRule p = do
2799 (_, True, mkQuan, inner) <- match opReducer p
2800 matrix <- match opConcatenate inner
2801 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2802 return
2803 ( "Shifting quantifier inwards"
2804 , return $ mkQuan $ make matrixLiteral
2805 ty
2806 index
2807 (map mkQuan elems)
2808 )
2809
2810
2811 rule_Comprehension_Simplify :: Rule
2812 rule_Comprehension_Simplify = "comprehension-simplify" `namedRule` theRule where
2813 theRule (Comprehension x gocs)
2814 | let isTrueCondition (Condition (Constant (ConstantBool True))) = True
2815 isTrueCondition _ = False
2816 , let gocs' = filter (not . isTrueCondition) gocs
2817 , length gocs' < length gocs
2818 = return
2819 ( "Removing true conditions"
2820 , return $ Comprehension x gocs'
2821 )
2822 theRule _ = na "rule_Comprehension_Simplify"
2823
2824
2825 rule_Xor_To_Sum :: Rule
2826 rule_Xor_To_Sum = "xor-to-sum" `namedRule` theRule where
2827 theRule [essence| xor(&arg) |] =
2828 case arg of
2829 Comprehension body goc -> do
2830 let argOut = Comprehension [essence| toInt(&body) |] goc
2831 return
2832 ( "xor to sum"
2833 , return [essence| 1 = sum(&argOut) % 2 |]
2834 )
2835 AbstractLiteral (AbsLitMatrix dom elems) -> do
2836 let argOut = AbstractLiteral $ AbsLitMatrix dom
2837 [ [essence| toInt(&el) |] | el <- elems ]
2838 return
2839 ( "xor to sum"
2840 , return [essence| 1 = sum(&argOut) % 2 |]
2841 )
2842 _ -> do
2843 (iPat, i) <- quantifiedVar
2844 return
2845 ( "xor to sum"
2846 , return [essence| 1 = sum([ toInt(&i) | &iPat <- &arg ]) % 2 |]
2847 )
2848 theRule _ = na "rule_Xor_To_Sum"
2849
2850
2851 enforceTagConsistency :: MonadFail m => Model -> m Model
2852 enforceTagConsistency model = do
2853 let statements' = transformBi reDomExp $ transformBi reDomConst (mStatements model)
2854 return model { mStatements = statements' }
2855
2856
2857 addUnnamedSymmetryBreaking ::
2858 NameGen m =>
2859 Maybe UnnamedSymmetryBreaking ->
2860 Model ->
2861 m Model
2862 addUnnamedSymmetryBreaking mode model = do
2863
2864 let
2865 allUnnamedTypes :: [(Domain () Expression, Expression)]
2866 allUnnamedTypes =
2867 [ reTag (TagUnnamed nm') (DomainReference nm Nothing, x) --x is a TagInt at this point so we must reTag it
2868 | Declaration (LettingDomainDefnUnnamed nm@(Name nm') x) <- mStatements model
2869 ]
2870
2871 allDecVars =
2872 [ (Reference nm Nothing, domain)
2873 | Declaration (FindOrGiven Find nm domain) <- mStatements model
2874 ]
2875
2876 -- allDecVarsAux auxSuffix =
2877 -- [ (Reference (mconcat [nm, "_auxFor_", auxSuffix]) Nothing, domain)
2878 -- | Declaration (FindOrGiven Find nm domain) <- mStatements model
2879 -- ]
2880
2881 varsTuple = case allDecVars of
2882 [v] -> fst v
2883 _ -> AbstractLiteral $ AbsLitTuple $ map fst allDecVars
2884 -- mkAuxTuple auxSuffix = AbstractLiteral $ AbsLitTuple $ map fst (allDecVarsAux auxSuffix)
2885
2886 -- traceM $ show $ "Unnamed types in this model:" <++> prettyList id "," allUnnamedTypes
2887 -- traceM $ show $ "Unnamed decision variables in this model:" <++> prettyList id "," allDecVars
2888
2889 -- 3 axis of doom
2890 -- 1. Quick/Complete. Quick is quickPermutationOrder(x, p) -- this is an efficient subset of x .<= p(x)
2891 -- Complete is x .<= p(x)
2892 -- 2. Scope. Consecutive
2893 -- AllPairs
2894 -- AllPermutations
2895 -- 3. Independently/Altogether
2896
2897 case mode of
2898 Nothing -> return model
2899 Just (UnnamedSymmetryBreaking quickOrComplete usbScope independentlyOrAltogether) -> do
2900 -- let newDecls =
2901 -- case quickOrComplete of
2902 -- USBQuick -> []
2903 -- USBComplete ->
2904 -- case independentlyOrAltogether of
2905 -- USBIndependently ->
2906 -- [ Declaration (FindOrGiven LocalFind nm' domain)
2907 -- | Declaration (FindOrGiven Find nm domain) <- mStatements model
2908 -- , (DomainReference uName _, _) <- allUnnamedTypes
2909 -- , let nm' = mconcat [nm, "_auxFor_", uName]
2910 -- ]
2911 -- USBAltogether ->
2912 -- [ Declaration (FindOrGiven LocalFind nm' domain)
2913 -- | Declaration (FindOrGiven Find nm domain) <- mStatements model
2914 -- , let nm' = mconcat [nm, "_auxFor_all"]
2915 -- ]
2916
2917 let
2918
2919 combinedPermApply perms =
2920 case quickOrComplete of
2921 USBQuick -> make opQuickPermutationOrder perms varsTuple
2922 USBComplete ->
2923 let applied = make opTransform perms varsTuple
2924 in [essence| &varsTuple .<= &applied |]
2925
2926 mkGenerator_Consecutive _ [] = bug "must have at least one unnamed type"
2927 mkGenerator_Consecutive perms [(u, uSize)] = do
2928 (iPat, i) <- quantifiedVar
2929 let perm = [essence| permutation((&i, succ(&i))) |]
2930 let applied = combinedPermApply (perm:perms)
2931 return [essence|
2932 and([ &applied
2933 | &iPat : &u
2934 , &i < &uSize
2935 ])
2936 |]
2937 mkGenerator_Consecutive perms ((u, uSize):us) = do
2938 (iPat, i) <- quantifiedVar
2939 let perm = [essence| permutation((&i, succ(&i))) |]
2940 applied <- mkGenerator_Consecutive (perm:perms) us
2941 return [essence|
2942 and([ &applied
2943 | &iPat : &u
2944 , &i < &uSize
2945 ])
2946 |]
2947
2948
2949 mkGenerator_AllPairs _ [] = bug "must have at least one unnamed type"
2950 mkGenerator_AllPairs perms [(u, _uSize)] = do
2951 (iPat, i) <- quantifiedVar
2952 (jPat, j) <- quantifiedVar
2953 let perm = [essence| permutation((&i, &j)) |]
2954 let applied = combinedPermApply (perm:perms)
2955 return [essence|
2956 and([ &applied
2957 | &iPat : &u
2958 , &jPat : &u
2959 , &i < &j
2960 ])
2961 |]
2962 mkGenerator_AllPairs perms ((u, _uSize):us) = do
2963 (iPat, i) <- quantifiedVar
2964 (jPat, j) <- quantifiedVar
2965 let perm = [essence| permutation((&i, &j)) |]
2966 applied <- mkGenerator_AllPairs (perm:perms) us
2967 return [essence|
2968 and([ &applied
2969 | &iPat : &u
2970 , &jPat : &u
2971 , &i < &j
2972 ])
2973 |]
2974
2975 mkGenerator_AllPermutations _ [] = bug "must have at least one unnamed type"
2976 mkGenerator_AllPermutations perms [(u, _uSize)] = do
2977 (iPat, i) <- quantifiedVar
2978 let perm = i
2979 let applied = combinedPermApply (perm:perms)
2980 return [essence|
2981 and([ &applied
2982 | &iPat : permutation of &u
2983 ])
2984 |]
2985 mkGenerator_AllPermutations perms ((u, _uSize):us) = do
2986 (iPat, i) <- quantifiedVar
2987 let perm = i
2988 applied <- mkGenerator_AllPermutations (perm:perms) us
2989 return [essence|
2990 and([ &applied
2991 | &iPat : permutation of &u
2992 ])
2993 |]
2994
2995 mkGenerator perms us =
2996 case usbScope of
2997 USBConsecutive -> mkGenerator_Consecutive perms us
2998 USBAllPairs -> mkGenerator_AllPairs perms us
2999 USBAllPermutations -> mkGenerator_AllPermutations perms us
3000 newCons <-
3001 case independentlyOrAltogether of
3002 USBIndependently -> do
3003 xs <- sequence
3004 [ mkGenerator [] [(u, uSize)]
3005 | (u@DomainReference{}, uSize) <- allUnnamedTypes
3006 ]
3007 return [SuchThat xs]
3008 USBAltogether -> do
3009 cons <- mkGenerator [] allUnnamedTypes
3010 return [SuchThat [cons]]
3011
3012 let stmts = newCons
3013 traceM $ show $ vcat $ "Adding the following unnamed symmetry breaking constraints:"
3014 : map (nest 4 . pretty) stmts
3015 return model { mStatements = mStatements model ++ stmts}
3016
3017
3018
3019 rule_Comprehension_Cardinality :: Rule
3020 rule_Comprehension_Cardinality = "comprehension-cardinality" `namedRule` theRule where
3021 theRule p = do
3022 Comprehension _ gensOrConds <- match opTwoBars p
3023 let ofones = Comprehension (fromInt 1) gensOrConds
3024 return ( "Horizontal rule for comprehension cardinality"
3025 , return [essence| sum(&ofones) |]
3026 )
3027
3028 rule_Flatten_Cardinality :: Rule
3029 rule_Flatten_Cardinality = "flatten-cardinality" `namedRule` theRule where
3030 theRule p = do
3031 list <- match opTwoBars p >>= match opConcatenate
3032 return ( "Horizontal rule for comprehension cardinality"
3033 , do
3034 (iPat, i) <- quantifiedVar
3035 return [essence| sum([ |&i| | &iPat <- &list ]) |]
3036 )