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 -- Substitute a decision letting everywhere it is named, including
852 -- through other decision lettings. The name is removed while its body
853 -- is expanded so a cyclic letting cannot diverge.
854 inline p@(Reference nm _) = do
855 mx <- gets (lookup nm)
856 case mx of
857 Nothing -> return p
858 Just x -> do
859 modify (filter ((/= nm) . fst))
860 x' <- transformM inline x
861 modify ((nm, x') :)
862 return x'
863 inline p = return p
864
865 statements = catMaybes
866 $ flip evalState []
867 $ forM (mStatements model)
868 $ \ st ->
869 case st of
870 Declaration (Letting nm x)
871 | categoryOf x == CatDecision
872 -> do
873 x' <- transformM inline x
874 modify ((nm, x') :)
875 return Nothing
876 -- The following doesn't work when the identifier is used in a domain
877 -- Declaration (Letting nm x@Reference{})
878 -- -> modify ((nm,x) :) >> return Nothing
879 _ -> Just <$> transformBiM inline st
880 in
881 model { mStatements = statements }
882
883 dropTagForSR ::
884 MonadFailDoc m =>
885 (?typeCheckerMode :: TypeCheckerMode) =>
886 Model -> m Model
887 dropTagForSR m = do
888 let
889 replacePredSucc [essence| pred(&x) |] = do
890 ty <- typeOf x
891 case ty of
892 TypeBool{} -> return [essence| false |]
893 -- since True becomes False
894 -- False becomes out-of-bounds, hence False
895 TypeInt{} -> do
896 let xTagInt = reTag TagInt x
897 return [essence| &xTagInt - 1 |]
898 _ -> bug "predSucc"
899 replacePredSucc [essence| succ(&x) |] = do
900 ty <- typeOf x
901 case ty of
902 TypeBool{} -> return [essence| !&x |]
903 -- since False becomes True
904 -- True becomes out-of-bounds, hence False
905 -- "succ" is exactly "negate" on bools
906 TypeInt{} -> do
907 let xTagInt = reTag TagInt x
908 return [essence| &xTagInt + 1 |]
909 _ -> bug "predSucc"
910 -- replacePredSucc [essence| &a .< &b |] = return [essence| &a < &b |]
911 -- replacePredSucc [essence| &a .<= &b |] = return [essence| &a <= &b |]
912 replacePredSucc x = return x
913
914 st <- transformBiM replacePredSucc (mStatements m)
915 return m { mStatements = transformBi (const TagInt) st }
916
917
918 updateDeclarations ::
919 MonadUserError m =>
920 MonadFailDoc m =>
921 NameGen m =>
922 EnumerateDomain m =>
923 (?typeCheckerMode :: TypeCheckerMode) =>
924 Model -> m Model
925 updateDeclarations model = do
926 let
927 representations = model |> mInfo |> miRepresentations
928
929 onEachStatement (inStatement, afters) =
930 case inStatement of
931 Declaration (FindOrGiven forg nm _) -> do
932 let
933 -- the refined domains for the high level declaration
934 domains = [ d | (n, d) <- representations, n == nm ]
935 nub <$> concatMapM (onEachDomain forg nm) domains
936 Declaration (GivenDomainDefnEnum name) -> return
937 [ Declaration (FindOrGiven Given (name `mappend` "_EnumSize") (DomainInt TagInt [])) ]
938 Declaration (Letting nm x) -> do
939 let
940 usedAfter :: Bool
941 usedAfter = nbUses nm afters > 0
942
943 nbComplexLiterals :: Int
944 nbComplexLiterals = sum
945 [ case y of
946 Constant (ConstantAbstract AbsLitMatrix{}) -> 0
947 Constant ConstantAbstract{} -> 1
948 AbstractLiteral AbsLitMatrix{} -> 0
949 AbstractLiteral{} -> 1
950 _ -> 0
951 | y <- universe x ]
952
953 isRefined :: Bool
954 isRefined = nbComplexLiterals == 0
955 return [inStatement | and [usedAfter, isRefined]]
956 Declaration LettingDomainDefnEnum{} -> return []
957 Declaration LettingDomainDefnUnnamed{} -> return []
958 SearchOrder orders -> do
959 orders' <- forM orders $ \case
960 BranchingOn nm -> do
961 let domains = [ d | (n, d) <- representations, n == nm ]
962 -- last one is the representation of what's in true(?)
963 -- put that first!
964 let reorder xs =
965 case reverse xs of
966 [] -> []
967 (y:ys) -> y : reverse ys
968 outNames <- concatMapM (onEachDomainSearch nm) (reorder domains)
969 return $ map BranchingOn $ nub outNames
970 Cut{} -> bug "updateDeclarations, Cut shouldn't be here"
971 return [ SearchOrder (concat orders') ]
972 _ -> return [inStatement]
973
974 onEachDomain forg nm domain =
975 runExceptT (downD (nm, domain)) >>= \case
976 Left err -> bug err
977 Right outs -> forM outs $ \ (n, d) -> do
978 d' <- transformBiM (trySimplify []) $ forgetRepr d
979 return $ Declaration (FindOrGiven forg n d')
980
981 onEachDomainSearch nm domain =
982 runExceptT (downD (nm, domain)) >>= \case
983 Left err -> bug err
984 Right outs -> return [ n
985 | (n, _) <- outs
986 ]
987
988 statements <- concatMapM onEachStatement (withAfter (mStatements model))
989 return model { mStatements = statements }
990
991
992 -- | checking whether any `Reference`s with `DeclHasRepr`s are left in the model
993 checkIfAllRefined :: MonadFailDoc m => Model -> m Model
994 checkIfAllRefined m | Just modelZipper <- mkModelZipper m = do -- we exclude the mInfo here
995 let returnMsg x = return
996 $ ""
997 : ("Not refined:" <+> vcat [ pretty (hole x)
998 , stringToDoc (show (hole x))
999 ])
1000 : [ nest 4 ("Context #" <> pretty i <> ":" <+> pretty c)
1001 | (i, c) <- zip allNats (drop 1 (ascendants x))
1002 ]
1003
1004 fails <- fmap (nubBy (\a b->show a == show b) . concat) $ forM (allContextsExceptReferences modelZipper) $ \ x ->
1005 case hole x of
1006 Reference _ (Just (DeclHasRepr _ _ dom))
1007 | not (isPrimitiveDomain dom) ->
1008 return $ ""
1009 : ("Not refined:" <+> vcat [ pretty (hole x)
1010 , stringToDoc (show (hole x))
1011 ])
1012 : ("Domain :" <+> pretty dom)
1013 : [ nest 4 ("Context #" <> pretty i <> ":" <+> pretty c)
1014 | (i, c) <- zip allNats (drop 1 (ascendants x))
1015 ]
1016 Constant (ConstantAbstract AbsLitMatrix{}) -> return []
1017 Constant ConstantAbstract{} -> returnMsg x
1018 AbstractLiteral AbsLitMatrix{} -> return []
1019 AbstractLiteral{} -> returnMsg x
1020 WithLocals{} -> returnMsg x
1021 Comprehension _ stmts -> do
1022 decisionConditions <-
1023 fmap catMaybes $ forM stmts $ \case
1024 Condition c ->
1025 if categoryOf c >= CatDecision
1026 then return (Just c)
1027 else return Nothing
1028 _ -> return Nothing
1029 comprehensionLettings <-
1030 fmap catMaybes $ forM stmts $ \ stmt -> case stmt of
1031 ComprehensionLetting{} -> return (Just stmt)
1032 _ -> return Nothing
1033 unsupportedGenerator <-
1034 fmap catMaybes $ forM stmts $ \ stmt -> case stmt of
1035 Generator GenInExpr{} -> return (Just stmt)
1036 _ -> return Nothing
1037 let msgs = [ "decision expressions as conditions"
1038 | not (null decisionConditions) ]
1039 ++ [ "local lettings"
1040 | not (null comprehensionLettings) ]
1041 ++ [ "unsupported generators"
1042 | not (null unsupportedGenerator) ]
1043 let msg = "Comprehension contains" <+> prettyListDoc id "," msgs <> "."
1044 case msgs of
1045 [] -> return []
1046 _ -> return $ [ msg ]
1047 ++ [ nest 4 (pretty (hole x)) ]
1048 ++ [ nest 4 ("Context #" <> pretty i <> ":" <+> pretty c)
1049 | (i, c) <- zip allNats (drop 1 (ascendants x))
1050 ]
1051 [essence| &_ .< &_ |] ->
1052 return ["", "Not refined:" <+> vcat [ pretty (hole x)
1053 , stringToDoc (show (hole x))
1054 ]]
1055 [essence| &_ .<= &_ |] ->
1056 return ["", "Not refined:" <+> vcat [ pretty (hole x)
1057 , stringToDoc (show (hole x))
1058 ]]
1059 _ -> return []
1060 unless (null fails) (bug (vcat fails))
1061 return m
1062 checkIfAllRefined m = return m
1063
1064
1065 -- | checking whether any undefined values creeped into the final model
1066 checkIfHasUndefined :: MonadFailDoc m => Model -> m Model
1067 checkIfHasUndefined m | Just modelZipper <- mkModelZipper m = do
1068 let returnMsg x = return
1069 $ ""
1070 : ("Undefined value in the final model:" <+> pretty (hole x))
1071 : [ nest 4 ("Context #" <> pretty i <> ":" <+> pretty c)
1072 | (i, c) <- zip allNats (drop 1 (ascendants x))
1073 ]
1074
1075 fails <- fmap concat $ forM (allContextsExceptReferences modelZipper) $ \ x ->
1076 case hole x of
1077 Constant ConstantUndefined{} -> returnMsg x
1078 _ -> return []
1079 unless (null fails) (bug (vcat fails))
1080 return m
1081 checkIfHasUndefined m = return m
1082
1083
1084 topLevelBubbles ::
1085 MonadFailDoc m =>
1086 MonadUserError m =>
1087 NameGen m =>
1088 (?typeCheckerMode :: TypeCheckerMode) =>
1089 Model -> m Model
1090 topLevelBubbles m = do
1091 let
1092 onStmt (SuchThat xs) = onExprs xs
1093 onStmt (Where xs) = concatMapM onWheres xs
1094 onStmt (Objective obj (WithLocals h locals)) =
1095 case locals of
1096 AuxiliaryVars locs -> ( locs ++ [Objective obj h] ) |> onStmts
1097 DefinednessConstraints locs -> ( [SuchThat locs] ++ [Objective obj h] ) |> onStmts
1098 onStmt (Declaration decl) =
1099 let
1100 f (WithLocals h locs) = tell [locs] >> return h
1101 f x = return x
1102
1103 (decl', locals) = runWriter (transformBiM f decl)
1104
1105 conv :: InBubble -> [Statement]
1106 conv (AuxiliaryVars locs) = locs
1107 conv (DefinednessConstraints locs) = [SuchThat locs]
1108
1109 newStmts :: [Statement]
1110 newStmts = concatMap conv locals
1111 in
1112 if null newStmts
1113 then return [Declaration decl]
1114 else onStmts (newStmts ++ [Declaration decl'])
1115 onStmt s = return [s]
1116
1117 -- a where that has a bubble at the top-most level will be replaced
1118 -- with a Comprehension. this is to avoid creating a where with decision variables inside.
1119 onWheres (WithLocals h (DefinednessConstraints locals)) =
1120 return $ map (Where . return) (locals ++ [h])
1121 onWheres (WithLocals h (AuxiliaryVars locals)) = do
1122 let (localfinds, gens) = mconcat
1123 [ case local of
1124 Declaration (FindOrGiven LocalFind nm dom) ->
1125 ([nm], [Generator (GenDomainNoRepr (Single nm) dom)])
1126 SuchThat xs ->
1127 ([], map Condition xs)
1128 _ -> bug ("topLevelBubbles.onWheres:" <+> pretty local)
1129 | local <- locals
1130 ]
1131 let forgetReprsOfLocalFinds (Reference nm _) | nm `elem` localfinds = Reference nm Nothing
1132 forgetReprsOfLocalFinds x = descend forgetReprsOfLocalFinds x
1133 let out = Comprehension h gens
1134 out' <- resolveNamesX (forgetReprsOfLocalFinds out)
1135 return [Where [out']]
1136 onWheres x = return [Where [x]]
1137
1138 onExpr (WithLocals h (AuxiliaryVars locals)) = ( locals ++ [SuchThat [h]]) |> onStmts
1139 onExpr (WithLocals h (DefinednessConstraints locals)) = ([SuchThat locals] ++ [SuchThat [h]]) |> onStmts
1140 onExpr x = return [SuchThat [x]]
1141
1142 onStmts = concatMapM onStmt
1143 onExprs = concatMapM onExpr
1144
1145 statements' <- onStmts (mStatements m)
1146 return m { mStatements = statements' }
1147
1148
1149 sliceThemMatrices ::
1150 Monad m =>
1151 (?typeCheckerMode :: TypeCheckerMode) =>
1152 Model -> m Model
1153 sliceThemMatrices model = do
1154 let
1155 -- nothing stays with a matrix type
1156 -- we are doing this top down
1157 -- when we reach a matrix-typed expression, we know it needs to be sliced
1158 -- we descend otherwise
1159 -- we also descend into components of the matrix-typed expression during slicing
1160 onExpr :: Monad m => Expression -> m Expression
1161 onExpr p = do
1162 let computeExistingSlices t =
1163 case match opSlicing t of
1164 Nothing -> return 0
1165 Just (t', _, _) -> (+1) <$> computeExistingSlices t'
1166 let isIndexedMatrix = do
1167 (m, is) <- match opMatrixIndexing p
1168 tyM <- typeOf m
1169 nSlices <- computeExistingSlices m
1170 return (m, nSlices, is, tyM)
1171 case isIndexedMatrix of
1172 Nothing -> descendM onExpr p
1173 Just (m, existingSlices, is, tyM) -> do
1174 let nestingLevel (TypeMatrix _ a) = 1 + nestingLevel a
1175 nestingLevel (TypeList a) = 1 + nestingLevel a
1176 nestingLevel _ = 0 :: Int
1177 -- "is" is the number of existing indices
1178 -- "nestingLevel" is the nesting level of the original matrix
1179 -- "existingSlices" is the number of existing slices
1180 let howMany = nestingLevel tyM - existingSlices - length is
1181 let unroll a 0 = a
1182 unroll a i = make opSlicing (unroll a (i-1)) Nothing Nothing
1183 m' <- descendM onExpr m
1184 is' <- mapM onExpr is
1185 let p' = make opMatrixIndexing m' is'
1186 return $ unroll p' howMany
1187
1188 statements <- descendBiM onExpr (mStatements model)
1189 return model { mStatements = statements }
1190
1191
1192 removeExtraSlices :: Monad m => Model -> m Model
1193 removeExtraSlices model = do
1194 let
1195 -- a slice at the end of a chain of slices & indexings
1196 -- does no good in Essence and should be removed
1197 onExpr :: Monad m => Expression -> m Expression
1198 onExpr (match opSlicing -> Just (m,Nothing,Nothing)) = onExpr m
1199 onExpr p@(match opIndexing -> Just _) = return p
1200 onExpr p = descendM onExpr p
1201
1202 statements <- descendBiM onExpr (mStatements model)
1203 return model { mStatements = statements }
1204
1205
1206 removeUnderscores :: Monad m => Model -> m Model
1207 removeUnderscores model = do
1208 let
1209 -- SR doesn't support identifiers that start with _
1210 -- we replace them with UNDERSCORE_
1211 onName :: Name -> Name
1212 onName (Name t) =
1213 case T.stripPrefix "_" t of
1214 Nothing -> Name t
1215 Just t' -> Name (mappend "UNDERSCORE__" t')
1216 onName n = n
1217
1218 return $ transformBi onName model
1219
1220
1221 lexSingletons :: (?typeCheckerMode :: TypeCheckerMode)
1222 => Monad m
1223 => Model -> m Model
1224 lexSingletons model = do
1225 let onExpr :: (?typeCheckerMode :: TypeCheckerMode)
1226 => Monad m => Expression -> m Expression
1227 onExpr [essence| &l <lex &r |] =
1228 case (matchSingleton l, matchSingleton r) of
1229 (Nothing, Nothing) -> return [essence| &l <lex &r |]
1230 (Just ls, Just rs) -> return [essence| &ls < &rs |]
1231 _ -> bug $ "lexSingleton: match inconsistent"
1232 onExpr [essence| &l <=lex &r |] =
1233 case (matchSingleton l, matchSingleton r) of
1234 (Nothing, Nothing) -> return [essence| &l <=lex &r |]
1235 (Just ls, Just rs) -> return [essence| &ls <= &rs |]
1236 _ -> bug $ "lexSingleton: match inconsistent"
1237 onExpr x = return x
1238 matchSingleton :: (?typeCheckerMode :: TypeCheckerMode)
1239 => Expression -> Maybe Expression
1240 matchSingleton (match matrixLiteral -> Just (TypeMatrix _ TypeInt{},_,[s])) =
1241 Just s
1242 matchSingleton _ = Nothing
1243 statements <- transformBiM onExpr (mStatements model)
1244 return model { mStatements = statements }
1245
1246
1247 logDebugIdModel :: MonadLog m => Doc -> Model -> m Model
1248 logDebugIdModel msg a = logDebug (msg <++> pretty (a {mInfo = def})) >> return a
1249
1250 prologue ::
1251 MonadFailDoc m =>
1252 MonadLog m =>
1253 NameGen m =>
1254 EnumerateDomain m =>
1255 (?typeCheckerMode :: TypeCheckerMode) =>
1256 Config ->
1257 Model ->
1258 m Model
1259 prologue config model = do
1260 void $ typeCheckModel_StandAlone model
1261 return model >>= logDebugIdModel "[input]"
1262 >>= enforceTagConsistency >>= logDebugIdModel "[enforceTagConsistency]"
1263 >>= removeUnderscores >>= logDebugIdModel "[removeUnderscores]"
1264 >>= return . addSearchOrder >>= logDebugIdModel "[addSearchOrder]"
1265 >>= attributeAsConstraints >>= logDebugIdModel "[attributeAsConstraints]"
1266 >>= inferAttributes >>= logDebugIdModel "[inferAttributes]"
1267 >>= inlineLettingDomainsForDecls >>= logDebugIdModel "[inlineLettingDomainsForDecls]"
1268 >>= lettingsForComplexInDoms >>= logDebugIdModel "[lettingsForComplexInDoms]"
1269 >>= distinctQuantifiedVars >>= logDebugIdModel "[distinctQuantifiedVars]"
1270 >>= return . initInfo >>= logDebugIdModel "[initInfo]"
1271 >>= addUnnamedSymmetryBreaking (unnamedSymmetryBreaking config)
1272 >>= logDebugIdModel "[addUnnamedSymmetryBreaking]"
1273 >>= removeUnnamedsFromModel >>= logDebugIdModel "[removeUnnamedsFromModel]"
1274 >>= removeEnumsFromModel >>= logDebugIdModel "[removeEnumsFromModel]"
1275 >>= finiteGivens >>= logDebugIdModel "[finiteGivens]"
1276 >>= renameQuantifiedVarsToAvoidShadowing
1277 >>= logDebugIdModel "[renameQuantifiedVarsToAvoidShadowing]"
1278 >>= resolveNames >>= logDebugIdModel "[resolveNames]"
1279 >>= checkCustomSymmetries
1280 >>= return . initInfo_Lettings >>= logDebugIdModel "[initInfo_Lettings]"
1281 >>= removeDomainLettings >>= logDebugIdModel "[removeDomainLettings]"
1282 >>= (let ?typeCheckerMode = RelaxedIntegerTags in typeCheckModel)
1283 >>= logDebugIdModel "[typeCheckModel]"
1284 >>= categoryChecking >>= logDebugIdModel "[categoryChecking]"
1285 >>= sanityChecks >>= logDebugIdModel "[sanityChecks]"
1286 >>= dealWithCuts >>= logDebugIdModel "[dealWithCuts]"
1287 >>= removeExtraSlices >>= logDebugIdModel "[removeExtraSlices]"
1288 -- >>= evaluateModel >>= logDebugIdModel "[evaluateModel]"
1289 >>= return . addTrueConstraints >>= logDebugIdModel "[addTrueConstraints]"
1290 >>= enforceTagConsistency >>= logDebugIdModel "[enforceTagConsistency]"
1291
1292
1293 epilogue ::
1294 MonadFailDoc m =>
1295 MonadLog m =>
1296 NameGen m =>
1297 EnumerateDomain m =>
1298 (?typeCheckerMode :: TypeCheckerMode) =>
1299 Model -> m Model
1300 epilogue model = return model
1301 >>= logDebugIdModel "[epilogue]"
1302 >>= lexSingletons >>= logDebugIdModel "[lexSingletons]"
1303 >>= resolveNames >>= logDebugIdModel "[resolveNames]"
1304 >>= updateDeclarations >>= logDebugIdModel "[updateDeclarations]"
1305 >>= return . inlineDecVarLettings >>= logDebugIdModel "[inlineDecVarLettings]"
1306 >>= topLevelBubbles >>= logDebugIdModel "[topLevelBubbles]"
1307 >>= checkIfAllRefined >>= logDebugIdModel "[checkIfAllRefined]"
1308 >>= checkIfHasUndefined >>= logDebugIdModel "[checkIfHasUndefined]"
1309 >>= sliceThemMatrices >>= logDebugIdModel "[sliceThemMatrices]"
1310 >>= dropTagForSR >>= logDebugIdModel "[dropTagForSR]"
1311 >>= return . emptyMatrixLiterals >>= logDebugIdModel "[emptyMatrixLiterals]"
1312 >>= return . expandDomainReferences
1313 >>= logDebugIdModel "[expandDomainReferences]"
1314 >>= return . reverseTrails >>= logDebugIdModel "[reverseTrails]"
1315 >>= return . oneSuchThat >>= logDebugIdModel "[oneSuchThat]"
1316 >>= return . languageEprime >>= logDebugIdModel "[languageEprime]"
1317
1318
1319 applicableRules :: forall m n .
1320 MonadUserError n =>
1321 MonadFailDoc n =>
1322 MonadLog n =>
1323 NameGen n =>
1324 EnumerateDomain n =>
1325 MonadUserError m =>
1326 MonadLog m =>
1327 NameGen m =>
1328 EnumerateDomain m =>
1329 MonadFailDoc m =>
1330 (?typeCheckerMode :: TypeCheckerMode) =>
1331 Config ->
1332 [Rule] ->
1333 ModelZipper ->
1334 n [(Doc, RuleResult m)]
1335 applicableRules Config{..} rulesAtLevel x = do
1336 let logAttempt = if logRuleAttempts then logInfo else const (return ())
1337 let logFail = if logRuleFails then logInfo else const (return ())
1338 let logSuccess = if logRuleSuccesses then logInfo else const (return ())
1339
1340 mys <- sequence [ do logAttempt ("attempting rule" <+> rName r <+> "on" <+> pretty (hole x))
1341 applied <- runExceptT $ runReaderT (rApply r x (hole x)) x
1342 return (rName r, applied)
1343 | r <- rulesAtLevel ]
1344 forM_ mys $ \ (rule, my) ->
1345 case my of
1346 Left failed -> unless ("N/A" `isPrefixOf` show failed) $ logFail $ vcat
1347 [ " rule failed:" <+> rule
1348 , " on:" <+> pretty (hole x)
1349 , " message:" <+> failed
1350 ]
1351 Right _ -> return ()
1352 return [ (name, res {ruleResult = ruleResult'})
1353 | (name, Right ress) <- mys
1354 , res <- ress
1355 , let ruleResult' = do
1356 rResult <- ruleResult res
1357 case (hole x, rResult) of
1358 (Reference nm1 _, Reference nm2 _)
1359 | not ("choose-repr" `isPrefixOf` show name)
1360 , nm1 == nm2 -> bug $ vcat
1361 [ "Rule applied inside a Reference."
1362 , "Rule :" <+> pretty name
1363 , "Rule input :" <+> pretty (hole x)
1364 , "Rule output :" <+> pretty rResult
1365 , "Rule input (show):" <+> pretty (show (hole x))
1366 , "Rule output (show):" <+> pretty (show rResult)
1367 ]
1368 _ -> return ()
1369 merr <- runExceptT (resolveNamesX rResult)
1370 case merr of
1371 Left err -> bug $ vcat
1372 [ "Name resolution failed after rule application."
1373 , "Rule :" <+> pretty name
1374 , "Rule input :" <+> pretty (hole x)
1375 , "Rule output :" <+> pretty rResult
1376 , "Rule input (show):" <+> pretty (show (hole x))
1377 , "Rule output (show):" <+> pretty (show rResult)
1378 , "The error :" <+> err
1379 ]
1380 Right r -> do
1381 logSuccess $ vcat
1382 [ "rule applied:" <+> name
1383 , " on:" <+> pretty (hole x)
1384 , " output:" <+> pretty r
1385 ]
1386 return r
1387 ]
1388
1389
1390 allRules :: (?typeCheckerMode :: TypeCheckerMode) => Config -> [[Rule]]
1391 allRules config =
1392 [ Transform.rules_Transform
1393 , [ rule_FullEvaluate
1394 ]
1395 , [ rule_PartialEvaluate
1396 ]
1397 ] ++ paramRules ++
1398 [ [ rule_ChooseRepr config
1399 , rule_ChooseReprForComprehension config
1400 , rule_ChooseReprForLocals config
1401 ]
1402 ] ++ bubbleUpRules ++
1403 [ [ rule_Eq
1404 , rule_Neq
1405 , rule_Comprehension_Cardinality
1406 , rule_Flatten_Cardinality
1407 ]
1408 , verticalRules
1409 , horizontalRules
1410 ] ++ otherRules
1411 ++ delayedRules
1412
1413
1414 -- | For information that can be readily pulled out from parameters.
1415 -- Some things are easier when everything involved is a param.
1416 -- These rules aren't necessary for correctness, but they can help remove some verbose expressions from the output.
1417 -- Make Savile Row happier so it makes us happier. :)
1418 paramRules :: [[Rule]]
1419 paramRules =
1420 [ [ Horizontal.Set.rule_Param_MinOfSet
1421 , Horizontal.Set.rule_Param_MaxOfSet
1422 , Horizontal.Set.rule_Param_Card
1423 ]
1424 , [ Horizontal.Function.rule_Param_DefinedRange
1425 , Horizontal.Relation.rule_Param_Card
1426 ]
1427 ]
1428
1429 verticalRules :: [Rule]
1430 verticalRules =
1431 [ Vertical.Permutation.PermutationAsFunction.rule_Image
1432 , Vertical.Permutation.PermutationAsFunction.rule_Image_permInverse
1433 , Vertical.Permutation.PermutationAsFunction.rule_double_permInverse
1434 , Vertical.Permutation.PermutationAsFunction.rule_Cardinality
1435 , Vertical.Permutation.PermutationAsFunction.rule_Defined
1436 , Vertical.Permutation.PermutationAsFunction.rule_Comprehension
1437
1438
1439 , Vertical.Tuple.rule_Tuple_Eq
1440 , Vertical.Tuple.rule_Tuple_Neq
1441 , Vertical.Tuple.rule_Tuple_Leq
1442 , Vertical.Tuple.rule_Tuple_Lt
1443 , Vertical.Tuple.rule_Tuple_TildeLeq
1444 , Vertical.Tuple.rule_Tuple_TildeLt
1445 , Vertical.Tuple.rule_Tuple_DotLeq
1446 , Vertical.Tuple.rule_Tuple_Index
1447
1448
1449
1450 , Vertical.Record.rule_Record_Eq
1451 , Vertical.Record.rule_Record_Neq
1452 , Vertical.Record.rule_Record_Leq
1453 , Vertical.Record.rule_Record_Lt
1454 , Vertical.Record.rule_Record_Index
1455
1456 , Vertical.Variant.rule_Variant_Eq
1457 , Vertical.Variant.rule_Variant_Neq
1458 , Vertical.Variant.rule_Variant_Leq
1459 , Vertical.Variant.rule_Variant_Lt
1460 , Vertical.Variant.rule_Variant_Index
1461 , Vertical.Variant.rule_Variant_Active
1462
1463 , Vertical.Matrix.rule_Comprehension_Literal
1464 , Vertical.Matrix.rule_Comprehension
1465 , Vertical.Matrix.rule_Comprehension_Flatten
1466 , Vertical.Matrix.rule_ModifierAroundIndexedMatrixLiteral
1467 , Vertical.Matrix.rule_Comprehension_LiteralIndexed
1468 , Vertical.Matrix.rule_Comprehension_Nested
1469 , Vertical.Matrix.rule_Comprehension_Hist
1470 , Vertical.Matrix.rule_Comprehension_ToSet_Matrix
1471 , Vertical.Matrix.rule_Comprehension_ToSet_List
1472 , Vertical.Matrix.rule_Comprehension_ToSet_List_DuplicateFree
1473 , Vertical.Matrix.rule_Matrix_Eq
1474 , Vertical.Matrix.rule_Matrix_Neq
1475 , Vertical.Matrix.rule_Matrix_TildeOrdering
1476 , Vertical.Matrix.rule_Matrix_Leq_Primitive
1477 , Vertical.Matrix.rule_Matrix_Leq_Decompose
1478 , Vertical.Matrix.rule_Matrix_Lt_Primitive
1479 , Vertical.Matrix.rule_Matrix_Lt_Decompose
1480 , Vertical.Matrix.rule_IndexingIdentical
1481 , Vertical.Matrix.rule_ExpandSlices
1482 , Vertical.Matrix.rule_Freq
1483
1484 , Vertical.Set.Explicit.rule_Min
1485 , Vertical.Set.Explicit.rule_Max
1486 , Vertical.Set.Explicit.rule_Card
1487 , Vertical.Set.Explicit.rule_Comprehension
1488 , Vertical.Set.Explicit.rule_PowerSet_Comprehension
1489 , Vertical.Set.Explicit.rule_In
1490 , Vertical.Set.ExplicitVarSizeWithDummy.rule_Comprehension
1491 , Vertical.Set.ExplicitVarSizeWithDummy.rule_PowerSet_Comprehension
1492 , Vertical.Set.ExplicitVarSizeWithFlags.rule_Comprehension
1493 , Vertical.Set.ExplicitVarSizeWithFlags.rule_PowerSet_Comprehension
1494 , Vertical.Set.ExplicitVarSizeWithMarker.rule_Card
1495 , Vertical.Set.ExplicitVarSizeWithMarker.rule_Comprehension
1496 , Vertical.Set.ExplicitVarSizeWithMarker.rule_PowerSet_Comprehension
1497 , Vertical.Set.Occurrence.rule_Comprehension
1498 , Vertical.Set.Occurrence.rule_PowerSet_Comprehension
1499 , Vertical.Set.Occurrence.rule_In
1500
1501 , Vertical.MSet.Occurrence.rule_Comprehension
1502 , Vertical.MSet.Occurrence.rule_Freq
1503
1504 , Vertical.MSet.ExplicitWithFlags.rule_Comprehension
1505 , Vertical.MSet.ExplicitWithFlags.rule_Freq
1506
1507 , Vertical.MSet.ExplicitWithRepetition.rule_Comprehension
1508
1509 , Vertical.Function.Function1D.rule_Comprehension
1510 , Vertical.Function.Function1D.rule_Comprehension_Defined
1511 , Vertical.Function.Function1D.rule_Image
1512
1513 , Vertical.Function.Function1DPartial.rule_Comprehension
1514 , Vertical.Function.Function1DPartial.rule_PowerSet_Comprehension
1515 , Vertical.Function.Function1DPartial.rule_Image_NotABool
1516 , Vertical.Function.Function1DPartial.rule_Image_Bool
1517 , Vertical.Function.Function1DPartial.rule_InDefined
1518 , Vertical.Function.Function1DPartial.rule_DefinedEqDefined
1519
1520 , Vertical.Function.FunctionND.rule_Comprehension
1521 , Vertical.Function.FunctionND.rule_Comprehension_Defined
1522 , Vertical.Function.FunctionND.rule_Image
1523
1524 , Vertical.Function.FunctionNDPartial.rule_Comprehension
1525 , Vertical.Function.FunctionNDPartial.rule_Image_NotABool
1526 , Vertical.Function.FunctionNDPartial.rule_Image_Bool
1527 , Vertical.Function.FunctionNDPartial.rule_InDefined
1528
1529 , Vertical.Function.FunctionNDPartialDummy.rule_Comprehension
1530 , Vertical.Function.FunctionNDPartialDummy.rule_Image
1531 , Vertical.Function.FunctionNDPartialDummy.rule_InDefined
1532
1533 , Vertical.Function.FunctionAsRelation.rule_Comprehension
1534 -- , Vertical.Function.FunctionAsRelation.rule_PowerSet_Comprehension
1535 , Vertical.Function.FunctionAsRelation.rule_Image_Eq
1536 , Vertical.Function.FunctionAsRelation.rule_InDefined
1537 , Vertical.Function.FunctionAsRelation.rule_InToSet
1538
1539 , Vertical.Sequence.ExplicitBounded.rule_Comprehension
1540 , Vertical.Sequence.ExplicitBounded.rule_Card
1541 , Vertical.Sequence.ExplicitBounded.rule_Image_Bool
1542 , Vertical.Sequence.ExplicitBounded.rule_Image_NotABool
1543 , Vertical.Sequence.ExplicitBounded.rule_Leq
1544 , Vertical.Sequence.ExplicitBounded.rule_Lt
1545
1546 , Vertical.Relation.RelationAsMatrix.rule_Comprehension
1547 , Vertical.Relation.RelationAsMatrix.rule_Image
1548
1549 , Vertical.Relation.RelationAsSet.rule_Comprehension
1550 , Vertical.Relation.RelationAsSet.rule_PowerSet_Comprehension
1551 , Vertical.Relation.RelationAsSet.rule_Card
1552 , Vertical.Relation.RelationAsSet.rule_In
1553
1554 , Vertical.Partition.PartitionAsSet.rule_Comprehension
1555 , Vertical.Partition.Occurrence.rule_Comprehension
1556
1557 ]
1558
1559 horizontalRules :: [Rule]
1560 horizontalRules =
1561 [ Horizontal.Permutation.rule_Cardinality_Literal
1562 , Horizontal.Permutation.rule_Equality
1563 , Horizontal.Permutation.rule_Disequality
1564 , Horizontal.Permutation.rule_Comprehension
1565 , Horizontal.Permutation.rule_Compose_Image
1566
1567
1568
1569
1570 , Horizontal.Permutation.rule_Defined_Literal
1571 , Horizontal.Permutation.rule_Image_Literal
1572 , Horizontal.Permutation.rule_In
1573 , Horizontal.Permutation.rule_Permutation_Inverse
1574
1575
1576
1577
1578
1579 , Horizontal.Set.rule_Comprehension_Literal
1580 , Horizontal.Set.rule_Eq
1581 , Horizontal.Set.rule_Neq
1582 , Horizontal.Set.rule_Subset
1583 , Horizontal.Set.rule_SubsetEq
1584 , Horizontal.Set.rule_Supset
1585 , Horizontal.Set.rule_SupsetEq
1586 , Horizontal.Set.rule_In
1587 , Horizontal.Set.rule_Card
1588 , Horizontal.Set.rule_CardViaFreq
1589 , Horizontal.Set.rule_Intersect
1590 , Horizontal.MSet.rule_Comprehension_ToSet
1591 , Horizontal.MSet.rule_Union
1592 , Horizontal.Set.rule_Union
1593 , Horizontal.Set.rule_Difference
1594 , Horizontal.Set.rule_PowerSet_Comprehension
1595 , Horizontal.Set.rule_PowerSet_Difference
1596 , Horizontal.Set.rule_MaxMin
1597
1598 , Horizontal.MSet.rule_Comprehension_Literal
1599 , Horizontal.MSet.rule_Freq_toMSet_Flatten
1600 , Horizontal.MSet.rule_Comprehension_ToSet_Literal
1601 , Horizontal.MSet.rule_Eq
1602 , Horizontal.MSet.rule_Neq
1603 , Horizontal.MSet.rule_Subset
1604 , Horizontal.MSet.rule_SubsetEq
1605 , Horizontal.MSet.rule_Supset
1606 , Horizontal.MSet.rule_SupsetEq
1607 , Horizontal.MSet.rule_Freq_Union
1608 , Horizontal.MSet.rule_Freq
1609 , Horizontal.MSet.rule_In
1610 , Horizontal.MSet.rule_Card
1611 , Horizontal.MSet.rule_MaxMin
1612
1613 , Horizontal.Function.rule_Comprehension_Literal
1614 , Horizontal.Function.rule_Image_Bool
1615 , Horizontal.Function.rule_Image_BoolMatrixIndexed
1616 , Horizontal.Function.rule_Image_BoolTupleIndexed
1617 , Horizontal.Function.rule_Image_Int
1618 , Horizontal.Function.rule_Image_IntMatrixIndexed
1619 , Horizontal.Function.rule_Image_IntTupleIndexed
1620 , Horizontal.Function.rule_Image_Matrix_LexLhs
1621 , Horizontal.Function.rule_Image_Matrix_LexRhs
1622
1623 , Horizontal.Function.rule_Comprehension_Image
1624 , Horizontal.Function.rule_Comprehension_ImageSet
1625 , Horizontal.Function.rule_Eq
1626 , Horizontal.Function.rule_Neq
1627 , Horizontal.Function.rule_Subset
1628 , Horizontal.Function.rule_SubsetEq
1629 , Horizontal.Function.rule_Supset
1630 , Horizontal.Function.rule_SupsetEq
1631 , Horizontal.Function.rule_Inverse
1632 , Horizontal.Function.rule_Card
1633 , Horizontal.Function.rule_Comprehension_PreImage
1634 , Horizontal.Function.rule_Comprehension_Defined
1635 , Horizontal.Function.rule_Comprehension_Range
1636 , Horizontal.Function.rule_In
1637 , Horizontal.Function.rule_Restrict_Image
1638 , Horizontal.Function.rule_Restrict_Comprehension
1639 , Horizontal.Function.rule_Comprehension_Defined_Size
1640 , Horizontal.Function.rule_Comprehension_Range_Size
1641 , Horizontal.Function.rule_Defined_Intersect
1642 , Horizontal.Function.rule_DefinedOrRange_Union
1643 , Horizontal.Function.rule_DefinedOrRange_Difference
1644
1645 , Horizontal.Sequence.rule_Comprehension_Literal
1646 , Horizontal.Sequence.rule_Image_Bool
1647 , Horizontal.Sequence.rule_Image_Int
1648 , Horizontal.Sequence.rule_Comprehension_Image
1649 , Horizontal.Sequence.rule_Image_Literal_Bool
1650 , Horizontal.Sequence.rule_Image_Literal_Int
1651 , Horizontal.Sequence.rule_Eq_Literal
1652 , Horizontal.Sequence.rule_Eq
1653 , Horizontal.Sequence.rule_Eq_Comprehension
1654 , Horizontal.Sequence.rule_Neq
1655 , Horizontal.Sequence.rule_Subset
1656 , Horizontal.Sequence.rule_SubsetEq
1657 , Horizontal.Sequence.rule_Supset
1658 , Horizontal.Sequence.rule_SupsetEq
1659 , Horizontal.Sequence.rule_Card
1660 , Horizontal.Sequence.rule_Comprehension_PreImage
1661 , Horizontal.Sequence.rule_Comprehension_Defined
1662 , Horizontal.Sequence.rule_Comprehension_Range
1663 , Horizontal.Sequence.rule_In
1664 , Horizontal.Sequence.rule_Restrict_Image
1665 , Horizontal.Sequence.rule_Restrict_Comprehension
1666 , Horizontal.Sequence.rule_Substring
1667 , Horizontal.Sequence.rule_Subsequence
1668
1669 , Horizontal.Relation.rule_Comprehension_Literal
1670 , Horizontal.Relation.rule_Comprehension_Projection
1671 , Horizontal.Relation.rule_PowerSet_Comprehension
1672 , Horizontal.Relation.rule_Image
1673 , Horizontal.Relation.rule_In
1674 , Horizontal.Relation.rule_Eq
1675 , Horizontal.Relation.rule_Neq
1676 , Horizontal.Relation.rule_Subset
1677 , Horizontal.Relation.rule_SubsetEq
1678 , Horizontal.Relation.rule_Supset
1679 , Horizontal.Relation.rule_SupsetEq
1680 , Horizontal.Relation.rule_Card
1681
1682 , Horizontal.Partition.rule_Comprehension_Literal
1683 , Horizontal.Partition.rule_Eq
1684 , Horizontal.Partition.rule_Neq
1685 , Horizontal.Partition.rule_Together
1686 , Horizontal.Partition.rule_Apart
1687 , Horizontal.Partition.rule_Party
1688 , Horizontal.Partition.rule_Participants
1689 , Horizontal.Partition.rule_Card
1690 , Horizontal.Partition.rule_In
1691
1692
1693 ]
1694
1695
1696 bubbleUpRules :: [[Rule]]
1697 bubbleUpRules =
1698 [
1699 [ BubbleUp.rule_MergeNested
1700 , BubbleUp.rule_ToAnd
1701 , BubbleUp.rule_ToMultiply_HeadOfIntComprehension
1702 , BubbleUp.rule_ConditionInsideGeneratorDomain
1703 , BubbleUp.rule_LiftVars
1704 ]
1705 ,
1706 [ BubbleUp.rule_NotBoolYet
1707 ]
1708 ]
1709
1710
1711 otherRules :: [[Rule]]
1712 otherRules =
1713 [
1714 [ rule_Xor_To_Sum ]
1715 ,
1716 [ TildeOrdering.rule_BoolInt
1717 , TildeOrdering.rule_MSet
1718 , TildeOrdering.rule_ViaMSet
1719 , TildeOrdering.rule_TildeLeq
1720 ]
1721 ,
1722 [ DontCare.rule_Bool
1723 , DontCare.rule_Int
1724 , DontCare.rule_Unnamed
1725 , DontCare.rule_Tuple
1726 , DontCare.rule_Record
1727 , DontCare.rule_Variant
1728 , DontCare.rule_Permutation
1729 , DontCare.rule_Matrix
1730 , DontCare.rule_Abstract
1731 ]
1732 ,
1733 [ rule_TrueIsNoOp
1734 , rule_FlattenOf1D
1735 , rule_Decompose_AllDiff
1736 , rule_Decompose_AllDiff_MapToSingleInt
1737
1738 , rule_GeneratorsFirst
1739 ]
1740 ,
1741 [ rule_DomainCardinality
1742 , rule_DomainMinMax
1743
1744 , rule_ComplexAbsPat
1745
1746 , rule_AttributeToConstraint
1747
1748 , rule_QuantifierShift
1749 , rule_QuantifierShift2
1750 , rule_QuantifierShift3
1751
1752 ]
1753
1754 , [ rule_Comprehension_Simplify
1755 ]
1756
1757 , [ rule_InlineConditions
1758 , rule_InlineConditions_AllDiff
1759 , rule_InlineConditions_MaxMin
1760 ]
1761 ]
1762
1763 -- | These rules depend on other rules firing first.
1764 delayedRules :: [[Rule]]
1765 delayedRules =
1766 [
1767 [ Vertical.Matrix.rule_Comprehension_Singleton
1768 , Vertical.Matrix.rule_Comprehension_SingletonDomain
1769 , Vertical.Matrix.rule_Concatenate_Singleton
1770 , Vertical.Matrix.rule_MatrixIndexing
1771
1772 ]
1773 , [ rule_ReducerToComprehension
1774 ]
1775 , [ rule_ApplySymmetries
1776 , rule_PermutationOrder
1777 , rule_PermutationOrderAfterRepresentation
1778 , rule_DotLtLeq
1779 , rule_Flatten_Lex
1780 ]
1781 ]
1782
1783
1784 rule_ChooseRepr :: (?typeCheckerMode :: TypeCheckerMode) => Config -> Rule
1785 rule_ChooseRepr config = Rule "choose-repr" (const theRule) where
1786
1787 theRule (Reference nm (Just (DeclNoRepr forg _ inpDom region))) | forg `elem` [Find, Given, CutFind] = do
1788 let reprsWhichOrder
1789 | (forg, representationsGivens config) == (Given, Sparse) = reprsSparseOrder
1790 | (forg, representationsFinds config) == (Find , Sparse) = reprsSparseOrder
1791 | not (representationLevels config) = reprsStandardOrderNoLevels
1792 | otherwise = reprsStandardOrder
1793 domOpts <- reprOptions reprsWhichOrder inpDom
1794 when (null domOpts) $
1795 bug $ "No representation matches this beast:" <++> pretty inpDom
1796 let options =
1797 [ RuleResult { ruleResultDescr = msg
1798 , ruleResultType = case forg of
1799 Find -> ChooseRepr_Find nm
1800 Given -> ChooseRepr_Given nm
1801 CutFind -> ChooseRepr_Cut nm
1802 _ -> bug "rule_ChooseRepr ruleResultType"
1803 , ruleResult = return out
1804 , ruleResultHook = Just hook
1805 , ruleResultSize = return $ expressionDepth $ Reference nm (Just (DeclHasRepr forg nm thisDom))
1806 }
1807 | thisDom <- domOpts
1808 , let msg = "Choosing representation for" <+> pretty nm <> ":" <++> pretty thisDom
1809 , let out = Reference nm (Just (DeclHasRepr forg nm thisDom))
1810 , let hook = mkHook (channelling config) forg nm thisDom region
1811 ]
1812 return options
1813 theRule _ = na "rule_ChooseRepr"
1814
1815 mkHook
1816 :: ( MonadLog m
1817 , MonadFail m
1818 , MonadFailDoc m
1819 , NameGen m
1820 , EnumerateDomain m
1821 )
1822 => Bool
1823 -> FindOrGiven
1824 -> Name
1825 -> Domain HasRepresentation Expression
1826 -> Region
1827 -> Model
1828 -> m Model
1829 mkHook useChannelling -- whether to use channelling or not
1830 forg -- find or given
1831 name -- name of the original declaration
1832 domain -- domain with representation selected
1833 region -- the region of the Reference we are working on
1834 model = do
1835 let
1836
1837 representations = model |> mInfo |> miRepresentations
1838 representationsTree = model |> mInfo |> miRepresentationsTree
1839 |> concatMap (\ (n, ds) -> map (n,) ds )
1840
1841 usedBefore = (name, reprTree domain) `elem` representationsTree
1842
1843 mkStructurals :: (MonadLog m, MonadFailDoc m, NameGen m, EnumerateDomain m)
1844 => m [Expression]
1845 mkStructurals = do
1846 let ref = Reference name (Just (DeclHasRepr forg name domain))
1847 logDebugVerbose $ "Generating structural constraints for:" <+> vcat [pretty ref, pretty domain]
1848 structurals <- getStructurals downX1 domain >>= \ gen -> gen ref
1849 logDebugVerbose $ "Before name resolution:" <+> vcat (map pretty structurals)
1850 resolved <- mapM resolveNamesX structurals -- re-resolving names
1851 logDebugVerbose $ "After name resolution:" <+> vcat (map pretty resolved)
1852 return resolved
1853
1854 addStructurals :: (MonadLog m, MonadFailDoc m, NameGen m, EnumerateDomain m)
1855 => Model -> m Model
1856 addStructurals
1857 | forg == Given = return
1858 | usedBefore = return
1859 | otherwise = \ m -> do
1860 structurals <- mkStructurals
1861 return $ if null structurals
1862 then m
1863 else m { mStatements = mStatements m ++ [SuchThat structurals] }
1864
1865 channels =
1866 [ make opEq this that
1867 | (n, d) <- representations
1868 , n == name
1869 , let this = Reference name (Just (DeclHasRepr forg name domain))
1870 , let that = Reference name (Just (DeclHasRepr forg name d))
1871 ]
1872
1873 addChannels
1874 | forg == Given = return
1875 | usedBefore = return
1876 | null channels = return
1877 | otherwise = \ m -> return
1878 m { mStatements = mStatements m ++ [SuchThat channels] }
1879
1880 recordThis
1881 | usedBefore = return
1882 | otherwise = \ m ->
1883 let
1884 oldInfo = mInfo m
1885 newInfo = oldInfo
1886 { miRepresentations = representations ++ [(name, domain)]
1887 , miRepresentationsTree = (representationsTree ++ [(name, reprTree domain)])
1888 |> sortBy (comparing fst)
1889 |> groupBy ((==) `on` fst)
1890 |> mapMaybe (\ grp -> case grp of [] -> Nothing ; (x:_) -> Just (fst x, map snd grp) )
1891 }
1892 in return m { mInfo = newInfo }
1893
1894 -- All symmetry comparisons of a variable must share one key,
1895 -- including separate independently-generated type actions. Other
1896 -- constraints may still channel that variable as usual.
1897 fixSymmetryRepresentations m =
1898 let pin (Reference nm (Just DeclNoRepr{})) | nm == name =
1899 Reference nm (Just (DeclHasRepr forg name domain))
1900 pin x = x
1901 onOp (Op (MkOpApplySymmetries (OpApplySymmetries delayed values syms))) =
1902 Op (MkOpApplySymmetries (OpApplySymmetries delayed (transformBi pin values) syms))
1903 onOp (Op (MkOpPermutationOrderAfterRepresentation (OpPermutationOrderAfterRepresentation ps values))) =
1904 make opPermutationOrderAfterRepresentation ps (transformBi pin values)
1905 onOp (Op (MkOpPermutationOrder (OpPermutationOrder ps values))) =
1906 make opPermutationOrder ps (transformBi pin values)
1907 onOp x = x
1908 in return m { mStatements = transformBi onOp (mStatements m) }
1909
1910 fixReprForAllOthers
1911 | useChannelling = fixSymmetryRepresentations
1912 | otherwise = \ m ->
1913 let
1914 f (Reference nm _)
1915 | nm == name
1916 = Reference nm (Just (DeclHasRepr forg name domain))
1917 f x = x
1918 in
1919 return m { mStatements = transformBi f (mStatements m) }
1920
1921 fixReprForSameRegion
1922 | region == NoRegion = return -- no-op, if we aren't in a particular region
1923 | otherwise = \ m ->
1924 let
1925 f (Reference nm (Just (DeclNoRepr _ _ _ region')))
1926 | nm == name
1927 , region' == region
1928 = Reference nm (Just (DeclHasRepr forg name domain))
1929 f x = x
1930 in
1931 return m { mStatements = transformBi f (mStatements m) }
1932
1933
1934 logDebugVerbose $ vcat
1935 [ "Name :" <+> pretty name
1936 , "Previously :" <+> vcat [ pretty (show d) | (n,d) <- representations, n == name ]
1937 , "This guy :" <+> pretty (show domain)
1938 , "usedBefore? :" <+> pretty usedBefore
1939 ]
1940
1941 return model
1942 >>= addStructurals -- unless usedBefore: add structurals
1943 >>= addChannels -- for each in previously recorded representation
1944 >>= recordThis -- unless usedBefore: record (name, domain) as being used in the model
1945 >>= fixReprForAllOthers -- fix the representation of this guy in the whole model, if channelling=no
1946 >>= fixReprForSameRegion -- fix the representation of this guy in the whole model,
1947 -- for those references with the same "region"
1948 >>= resolveNames -- we need to re-resolve names to avoid repeatedly selecting representations
1949 -- for abstract stuff inside aliases.
1950
1951
1952 rule_ChooseReprForComprehension :: Config -> Rule
1953 rule_ChooseReprForComprehension config = Rule "choose-repr-for-comprehension" (const theRule) where
1954
1955 theRule (Comprehension body gensOrConds) = do
1956 (gocBefore, (nm, domain), gocAfter) <- matchFirst gensOrConds $ \case
1957 Generator (GenDomainNoRepr (Single nm) domain) -> return (nm, domain)
1958 _ -> na "rule_ChooseReprForComprehension"
1959
1960 let reprsWhichOrder
1961 | representationsGivens config == Sparse = reprsSparseOrder
1962 | not (representationLevels config ) = reprsStandardOrderNoLevels
1963 | otherwise = reprsStandardOrder
1964 domOpts <- reprOptions reprsWhichOrder domain
1965 when (null domOpts) $
1966 bug $ "No representation matches this beast:" <++> pretty domain
1967
1968 return
1969 [ RuleResult
1970 { ruleResultDescr = "Choosing representation for quantified variable" <+>
1971 pretty nm <> ":" <++> pretty thisDom
1972 , ruleResultType = ChooseRepr_Quantified
1973 , ruleResult = bugFailT "rule_ChooseReprForComprehension" $ do
1974 outDomains <- downD (nm, thisDom)
1975 structurals <- mkStructurals nm thisDom
1976 let updateRepr (Reference nm' _)
1977 | nm == nm'
1978 = Reference nm (Just (DeclHasRepr Quantified nm thisDom))
1979 updateRepr p = p
1980 let out' = Comprehension (transform updateRepr body)
1981 $ gocBefore
1982 ++ [ Generator (GenDomainHasRepr name dom)
1983 | (name, dom) <- outDomains ]
1984 ++ map Condition structurals
1985 ++ transformBi updateRepr gocAfter
1986 out <- resolveNamesX out'
1987 return out
1988 , ruleResultHook = Nothing
1989 , ruleResultSize = return $ expressionDepth $ Reference nm (Just (DeclHasRepr Quantified nm thisDom))
1990 }
1991 | thisDom <- domOpts
1992 ]
1993 theRule _ = na "rule_ChooseReprForComprehension"
1994
1995 mkStructurals name domain = do
1996 let ref = Reference name (Just (DeclHasRepr Quantified name domain))
1997 gen <- getStructurals downX1 domain
1998 gen ref
1999
2000
2001 rule_ChooseReprForLocals :: Config -> Rule
2002 rule_ChooseReprForLocals config = Rule "choose-repr-for-locals" (const theRule) where
2003
2004 theRule (WithLocals body (AuxiliaryVars locals)) = do
2005 (stmtBefore, (nm, domain), stmtAfter) <- matchFirst locals $ \case
2006 Declaration (FindOrGiven LocalFind nm domain) -> return (nm, domain)
2007 _ -> na "rule_ChooseReprForLocals"
2008
2009 let
2010 isReferencedWithoutRepr (Reference nm' (Just DeclNoRepr{})) | nm == nm' = True
2011 isReferencedWithoutRepr _ = False
2012
2013 unless (any isReferencedWithoutRepr (universeBi (body, stmtBefore, stmtAfter))) $
2014 na $ "This local variable seems to be handled before:" <+> pretty nm
2015
2016 let reprsWhichOrder
2017 | representationsAuxiliaries config == Sparse = reprsSparseOrder
2018 | not (representationLevels config) = reprsStandardOrderNoLevels
2019 | otherwise = reprsStandardOrder
2020 domOpts <- reprOptions reprsWhichOrder domain
2021 when (null domOpts) $
2022 bug $ "No representation matches this beast:" <++> pretty domain
2023
2024 return
2025 [ RuleResult
2026 { ruleResultDescr = "Choosing representation for auxiliary variable" <+>
2027 pretty nm <> ":" <++> pretty thisDom
2028 , ruleResultType = ChooseRepr_Auxiliary
2029 , ruleResult = bugFailT "rule_ChooseReprForLocals" $ do
2030 outDomains <- downD (nm, thisDom)
2031 structurals <- mkStructurals nm thisDom
2032 let updateRepr (Reference nm' _)
2033 | nm == nm'
2034 = Reference nm (Just (DeclHasRepr LocalFind nm thisDom))
2035 updateRepr p = p
2036 let out' = WithLocals (transform updateRepr body) $ AuxiliaryVars
2037 ( stmtBefore
2038 ++ [ Declaration (FindOrGiven
2039 LocalFind
2040 name
2041 (forgetRepr dom))
2042 | (name, dom) <- outDomains ]
2043 ++ [ SuchThat structurals | not (null structurals) ]
2044 ++ transformBi updateRepr stmtAfter
2045 )
2046 out <- resolveNamesX out'
2047 return out
2048 , ruleResultHook = Nothing
2049 , ruleResultSize = return $ expressionDepth $ Reference nm (Just (DeclHasRepr LocalFind nm thisDom))
2050 }
2051 | thisDom <- domOpts
2052 ]
2053 theRule _ = na "rule_ChooseReprForLocals"
2054
2055 mkStructurals name domain = do
2056 let ref = Reference name (Just (DeclHasRepr LocalFind name domain))
2057 gen <- getStructurals downX1 domain
2058 gen ref
2059
2060
2061 rule_GeneratorsFirst :: Rule
2062 rule_GeneratorsFirst = "generators-first" `namedRule` theRule where
2063 theRule (Comprehension body [])
2064 = return
2065 ( "Empty generators."
2066 , return $ AbstractLiteral $ AbsLitMatrix (mkDomainIntB 1 1) [body]
2067 )
2068 theRule (Comprehension body gensOrConds)
2069 | let (gens, rest) = mconcat
2070 [ case x of
2071 Generator{} -> ([x],[])
2072 _ -> ([],[x])
2073 | x <- gensOrConds
2074 ]
2075 , let gensOrConds' = gens ++ rest
2076 , gensOrConds /= gensOrConds'
2077 = return
2078 ( "Generators come first."
2079 , return $ Comprehension body gensOrConds'
2080 )
2081 theRule (Comprehension body gensOrConds)
2082 | let (lettings :: [Name], rest :: [GeneratorOrCondition]) = mconcat
2083 [ case x of
2084 ComprehensionLetting pat _ -> (universeBi pat,[] )
2085 _ -> ([] ,[x])
2086 | x <- gensOrConds
2087 ]
2088 , let f (Reference nm (Just (Alias x))) | nm `elem` lettings = f x
2089 f x = x
2090 , not (null lettings)
2091 = return
2092 ( "Inlining comprehension lettings."
2093 , return $ transformBi f $ Comprehension body rest
2094 )
2095 theRule _ = na "rule_GeneratorsFirst"
2096
2097
2098 rule_Eq :: Rule
2099 rule_Eq = "identical-domain-eq" `namedRule` theRule where
2100 theRule p = do
2101 (x,y) <- match opEq p
2102 domX <- domainOf x
2103 domY <- domainOf y
2104 unless (domX == domY) $ na "rule_Eq domains not identical"
2105 sameRepresentationTree x y
2106 xs <- downX x
2107 ys <- downX y
2108 unless (length xs == length ys) $ na "rule_Eq"
2109 when (xs == [x]) $ na "rule_Eq"
2110 when (ys == [y]) $ na "rule_Eq"
2111 return
2112 ( "Generic vertical rule for identical-domain equality"
2113 , return $ make opAnd $ fromList $ zipWith (\ i j -> [essence| &i = &j |] ) xs ys
2114 )
2115
2116
2117 rule_Neq :: Rule
2118 rule_Neq = "identical-domain-neq" `namedRule` theRule where
2119 theRule p = do
2120 (x,y) <- match opNeq p
2121 domX <- domainOf x
2122 domY <- domainOf y
2123 unless (domX == domY) $ na "rule_Neq domains not identical"
2124 sameRepresentationTree x y
2125 xs <- downX x
2126 ys <- downX y
2127 unless (length xs == length ys) $ na "rule_Neq"
2128 when (xs == [x]) $ na "rule_Neq"
2129 when (ys == [y]) $ na "rule_Neq"
2130 return
2131 ( "Generic vertical rule for identical-domain equality"
2132 , return $ make opOr $ fromList $ zipWith (\ i j -> [essence| &i != &j |] ) xs ys
2133 )
2134
2135
2136 -- The public operators expand a parameter sequence; the internal operation keeps
2137 -- Eager intact until the source representation has been selected.
2138 rule_ApplySymmetries :: Rule
2139 rule_ApplySymmetries = "apply-symmetries" `namedRule` theRule where
2140 theRule (Op (MkOpApplySymmetries op@(OpApplySymmetries delayed values symmetries))) = do
2141 void $ typeOf op
2142 let opName = if delayed then "applySymmetriesAfterRepresentation" else "applySymmetries"
2143 when (categoryOf symmetries > CatParameter) $
2144 failDoc $ opName <> ": symmetries must be constant or given"
2145 let checkValue v = case followAliases id v of
2146 AbstractLiteral (AbsLitTuple xs) -> mapM_ checkValue xs
2147 Reference _ (Just DeclNoRepr{}) -> return ()
2148 Reference _ (Just DeclHasRepr{}) -> return ()
2149 _ -> failDoc $ opName <> ": values must be a tuple of variable references"
2150 checkValue values
2151 ts <- typeOf symmetries
2152 let entries = case ts of
2153 TypeSequence (TypeTuple xs) -> xs
2154 _ -> [] -- rejected by typeOf above
2155 return ("Apply the supplied symmetry tuples", do
2156 (pPat, entry) <- quantifiedVar
2157 let permTuple = make opIndexing entry (fromInt 2)
2158 let perms = [ make opIndexing permTuple (fromInt i)
2159 | i <- [1 .. genericLength entries] ]
2160 applied = if delayed
2161 then make opPermutationOrderAfterRepresentation perms values
2162 else make opPermutationOrder perms values
2163 return $ make opAnd $ Comprehension applied
2164 [Generator (GenInExpr pPat symmetries)])
2165 theRule _ = na "rule_ApplySymmetries"
2166
2167
2168 rule_PermutationOrder :: Rule
2169 rule_PermutationOrder = "permutation-order" `namedRule` theRule where
2170 theRule (match opPermutationOrder -> Just (perms, value0)) = do
2171 let value = followAliases id value0
2172 -- Wait for all representation choices before creating the image. This
2173 -- also checks nested tuple literals, which have no representation tree.
2174 let ready x = case followAliases id x of
2175 AbstractLiteral (AbsLitTuple xs) -> mapM_ ready xs
2176 r@Reference{} -> void $ domainOfR r
2177 _ -> na "permutationOrder: expected represented variables"
2178 ready value
2179 return ("Eager symmetry comparison in the source representation", do
2180 (lhs, rhs, locals) <- keys perms value
2181 let comparison = [essence| &lhs <=lex &rhs |]
2182 return $ if null locals then comparison
2183 else WithLocals comparison (AuxiliaryVars locals))
2184 theRule _ = na "rule_PermutationOrder"
2185
2186 keys perms x0 = case followAliases id x0 of
2187 AbstractLiteral (AbsLitTuple xs) -> do
2188 images <- mapM (keys perms) xs
2189 let lhs = make opFlatten $ fromList [a | (a,_,_) <- images]
2190 rhs = make opFlatten $ fromList [b | (_,b,_) <- images]
2191 return (lhs, rhs, concat [ds | (_,_,ds) <- images])
2192 x -> do
2193 ty <- typeOf x
2194 lhs <- symmetryOrderingVector x
2195 if isPrimitiveType ty
2196 -- Scalars and primitive matrices have a fixed coordinate order;
2197 -- relabelling their key needs no collection canonicalization.
2198 -- Avoid auxiliaries indexed by a quantified permutation here.
2199 then do
2200 dom <- domainOfR x
2201 rhs <- primitiveImageKey perms x dom
2202 return (lhs, rhs, [])
2203 else do
2204 dom <- domainOfR x
2205 (nm, _) <- auxiliaryVar
2206 let imageValue = Reference nm (Just (DeclHasRepr LocalFind nm dom))
2207 sameRepresentationTree x imageValue
2208 -- downD lowers the entire selected tree, not just its root.
2209 leaves <- downD (nm, dom)
2210 structurals <- getStructurals downX1 dom >>= (\f -> f imageValue)
2211 rhs <- symmetryOrderingVector imageValue
2212 let transformed = make opTransform perms x
2213 equality = [essence| &imageValue = &transformed |]
2214 return (lhs, rhs,
2215 [Declaration (FindOrGiven LocalFind name (forgetRepr d)) | (name,d) <- leaves]
2216 ++ [SuchThat (structurals ++ [equality])])
2217
2218 primitiveImageKey perms x (DomainMatrix index inner) = do
2219 let ix = forgetRepr index
2220 (iPat, i) <- quantifiedVarOverDomain ix
2221 let oldIndex = make opTransform (map (make opPermInverse) perms) i
2222 row <- primitiveImageKey perms [essence| &x[&oldIndex] |] inner
2223 return [essence| flatten([&row | &iPat : &ix]) |]
2224 primitiveImageKey perms x DomainBool = do
2225 let imageValue = make opTransform perms x
2226 return [essence| [-toInt(&imageValue)] |]
2227 primitiveImageKey perms x DomainInt{} =
2228 return $ fromList [make opTransform perms x]
2229 primitiveImageKey _ _ _ = na "permutationOrder: expected a primitive domain"
2230
2231
2232 symmetryOrderingVector ::
2233 (MonadFailDoc m, NameGen m, EnumerateDomain m, ?typeCheckerMode :: TypeCheckerMode)
2234 => Expression -> m Expression
2235 symmetryOrderingVector x =
2236 symmetryOrdering x >>= resolveNamesX >>= transformM tupleLitToMatrixLit >>= return . make opFlatten
2237 where
2238 tupleLitToMatrixLit (AbstractLiteral (AbsLitTuple xs)) = do
2239 xs' <- forM xs $ \v -> do
2240 ty <- typeOf v
2241 return $ oneDimensionaliser (matrixNumDims ty) v
2242 return (fromList xs')
2243 tupleLitToMatrixLit v = return v
2244
2245
2246 rule_PermutationOrderAfterRepresentation :: Rule
2247 rule_PermutationOrderAfterRepresentation = "generic-PermutationOrderAfterRepresentation" `namedRule` theRule where
2248 theRule p@(match opPermutationOrderAfterRepresentation -> Just (ps, x)) = do
2249 x_ord <- symmetryOrdering x
2250 let rhs = make opTransform ps x_ord
2251 return
2252 ( "Generic vertical rule for permutationOrderAfterRepresentation:" <+> pretty p
2253 , return [essence| &x_ord .<= &rhs |]
2254 )
2255 theRule _ = na "rule_PermutationOrderAfterRepresentation"
2256
2257
2258 rule_DotLtLeq :: Rule
2259 rule_DotLtLeq = "generic-DotLtLeq" `namedRule` theRule where
2260 theRule p = do
2261 (a,b,mk) <- case p of
2262 [essence| &a .< &b |] -> return ( a, b, \ i j -> [essence| &i <lex &j |] )
2263 [essence| &a .<= &b |] -> return ( a, b, \ i j -> [essence| &i <=lex &j |] )
2264 _ -> na "rule_DotLtLeq"
2265 ma <- symmetryOrderingVector a
2266 mb <- symmetryOrderingVector b
2267 return
2268 ( "Generic vertical rule for dotLt and dotLeq:" <+> pretty p
2269 , return $ mk ma mb
2270 )
2271
2272
2273 rule_Flatten_Lex :: Rule
2274 rule_Flatten_Lex = "flatten-lex" `namedRule` theRule where
2275 theRule [essence| &a <lex &b |] = do
2276 reject_flat a b
2277 fa <- flatten a
2278 fb <- flatten b
2279 tfa <- typeOf fa
2280 tfb <- typeOf fb
2281 case (tfa, tfb) of
2282 (TypeList TypeInt{}, TypeList TypeInt{}) -> return ()
2283 (TypeMatrix TypeInt{} TypeInt{}, TypeMatrix TypeInt{} TypeInt{}) -> return ()
2284 _ -> bug $ "flattener: " <+> vcat [stringToDoc $ show tfa, stringToDoc $ show tfb]
2285 return ( "Flatten Lex less"
2286 , return [essence| &fa <lex &fb |]
2287 )
2288 theRule [essence| &a <=lex &b |] = do
2289 reject_flat a b
2290 fa <- flatten a
2291 fb <- flatten b
2292 tfa <- typeOf fa
2293 tfb <- typeOf fb
2294 case (tfa, tfb) of
2295 (TypeList TypeInt{}, TypeList TypeInt{}) -> return ()
2296 (TypeMatrix TypeInt{} TypeInt{}, TypeMatrix TypeInt{} TypeInt{}) -> return ()
2297 _ -> bug $ "flattener: " <+> vcat [stringToDoc $ show tfa, stringToDoc $ show tfb]
2298 return ( "Flatten Lex Lt"
2299 , return [essence| &fa <=lex &fb |]
2300 )
2301 theRule _ = na "rule_Flatten_Lex"
2302 reject_flat a b = do
2303 ta <- typeOf a
2304 tb <- typeOf b
2305 case (ta, tb) of
2306 (TypeMatrix TypeBool TypeInt{}, _) ->
2307 na "rule_Flatten_Lex"
2308 (TypeMatrix TypeBool TypeBool, _) ->
2309 na "rule_Flatten_Lex"
2310 (TypeList TypeInt{}, _) ->
2311 na "rule_Flatten_Lex"
2312 (TypeMatrix TypeInt{} TypeInt{}, _) ->
2313 na "rule_Flatten_Lex"
2314 (TypeList TypeBool, _) ->
2315 na "rule_Flatten_Lex"
2316 (TypeMatrix TypeInt{} TypeBool, _) ->
2317 na "rule_Flatten_Lex"
2318 _ -> return ()
2319
2320 flatten a = do
2321 ta <- typeOf a
2322 case ta of
2323 TypeBool -> return [essence| [-toInt(&a)] |]
2324 TypeInt{} -> return [essence| [&a] |]
2325 TypeList TypeInt{} -> return a
2326 TypeMatrix TypeInt{} TypeInt{} -> return a
2327 TypeTuple ts -> do
2328 case a of
2329 AbstractLiteral x -> do
2330 case x of
2331 AbsLitTuple xs -> do
2332 fxs <- mapM flatten xs
2333 let flatxs = fromList fxs
2334 return [essence| flatten(&flatxs) |]
2335 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this abslit fellow..."
2336 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2337 Constant c ->
2338 case c of
2339 ConstantAbstract ca ->
2340 case ca of
2341 AbsLitTuple xs -> do
2342 fxs <- mapM flatten (Constant <$> xs)
2343 let flatxs = fromList fxs
2344 return [essence| flatten(&flatxs) |]
2345 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2346 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2347 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2348 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2349 Op _ -> do
2350 (oName, o) <- quantifiedVar
2351 flatten $ Comprehension o [ComprehensionLetting oName a]
2352 _ -> do
2353 ps <- mapM (\(i,_) -> do
2354 (Single nm, tm) <- quantifiedVar
2355 return (i,nm,tm)) (zip [1..] ts)
2356 let lts = (\(i,nm,_tm) -> ComprehensionLetting (Single nm) [essence| &a[&i] |]) <$> ps
2357 tup = AbstractLiteral $ AbsLitTuple $ (\(_,_,tm) -> tm) <$> ps
2358 flatten $ Comprehension tup lts
2359 _ ->
2360 case a of
2361 AbstractLiteral x -> do
2362 case x of
2363 AbsLitMatrix _ xs -> do
2364 fxs <- mapM flatten xs
2365 let flatxs = fromList fxs
2366 return [essence| flatten(&flatxs) |]
2367 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this abslit fellow..."
2368 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2369 Constant c ->
2370 case c of
2371 ConstantAbstract ca ->
2372 case ca of
2373 AbsLitMatrix _ [] ->
2374 return [essence| ([] : `matrix indexed by [int()] of int`) |]
2375 AbsLitMatrix _ xs -> do
2376 fxs <- mapM flatten (Constant <$> xs)
2377 let flatxs = fromList fxs
2378 return [essence| flatten(&flatxs) |]
2379 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2380 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2381 TypedConstant tc _ -> flatten (Constant tc)
2382 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this constant fellow..."
2383 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2384 Op _ -> do
2385 (oName, o) <- quantifiedVar
2386 flatten $ Comprehension o [ComprehensionLetting oName a]
2387 Reference nm ex ->
2388 bug $ "rule_FlattenLex: flatten isn't defined for this reference fellow..."
2389 <+> vcat [stringToDoc (show a)
2390 ,"reference:" <+> stringToDoc (show nm)
2391 ,"fellow:" <+> stringToDoc (show ex)]
2392 Comprehension body gocs -> do
2393 fbody <- flatten body
2394 let comp = Comprehension fbody gocs
2395 return [essence| flatten(&comp) |]
2396 _ -> bug $ "rule_FlattenLex: flatten isn't defined for this expression fellow..."
2397
2398 <+> vcat [pretty a, pretty ta, stringToDoc $ show a]
2399
2400
2401 rule_ReducerToComprehension :: Rule
2402 rule_ReducerToComprehension = "reducer-to-comprehension" `namedRule` theRule where
2403 theRule p = do
2404 (_, _, mk, coll) <- match opReducer p
2405 -- leave comprehensions alone
2406 let
2407 isComprehension Comprehension{} = True
2408 isComprehension _ = False
2409 case followAliases isComprehension coll of
2410 True -> na "rule_ReducerToComprehension"
2411 False -> return ()
2412 -- leave matrix literals alone
2413 case tryMatch matrixLiteral coll of
2414 Nothing -> return ()
2415 Just {} -> na "rule_ReducerToComprehension"
2416 tyColl <- typeOf coll
2417 howToIndex <- case tyColl of
2418 TypeSequence{} -> return $ Left ()
2419 TypeMatrix{} -> return $ Right ()
2420 TypeList{} -> return $ Right ()
2421 TypeSet{} -> return $ Right ()
2422 TypeMSet{} -> return $ Right ()
2423 _ -> na "rule_ReducerToComprehension"
2424 return
2425 ( "Creating a comprehension for the collection inside the reducer operator."
2426 , do
2427 (iPat, i) <- quantifiedVar
2428 case howToIndex of
2429 Left{} -> return $ mk [essence| [ &i[2] | &iPat <- &coll ] |]
2430 Right{} -> return $ mk [essence| [ &i | &iPat <- &coll ] |]
2431 )
2432
2433
2434 rule_TrueIsNoOp :: Rule
2435 rule_TrueIsNoOp = "true-is-noop" `namedRule` theRule where
2436 theRule (Op (MkOpTrue (OpTrue ref))) =
2437 case ref of
2438 Reference _ (Just DeclHasRepr{}) ->
2439 return ( "Remove the argument from true."
2440 , return $ Constant $ ConstantBool True
2441 )
2442 _ -> na "The argument of true doesn't have a representation."
2443 theRule _ = na "rule_TrueIsNoOp"
2444
2445
2446 rule_FlattenOf1D :: Rule
2447 rule_FlattenOf1D = "flatten-of-1D" `namedRule` theRule where
2448 theRule p = do
2449 x <- match opFlatten p
2450 tyx <- typeOf x
2451 out <- case tyx of
2452 TypeList TypeBool{} -> return x
2453 TypeList TypeInt{} -> return x
2454 TypeMatrix _ TypeBool{} -> return x
2455 TypeMatrix _ TypeInt{} -> return x
2456 TypeMatrix{} -> -- more than 1D
2457 case listOut x of
2458 Just [y] -> return (make opFlatten y)
2459 _ -> na "rule_FlattenOf1D"
2460 _ -> na "rule_FlattenOf1D"
2461 return ( "1D matrices do not need a flatten."
2462 , return out
2463 )
2464
2465
2466 rule_Decompose_AllDiff :: Rule
2467 rule_Decompose_AllDiff = "decompose-allDiff" `namedRule` theRule where
2468 theRule [essence| allDiff(&m) |] = do
2469 ty <- typeOf m
2470 case ty of
2471 TypeMatrix _ TypeBool -> na "allDiff can stay"
2472 TypeMatrix _ (TypeInt _) -> na "allDiff can stay"
2473 TypeMatrix _ _ -> return ()
2474 _ -> na "allDiff on something other than a matrix."
2475 index:_ <- indexDomainsOf m
2476 return
2477 ( "Decomposing allDiff. Type:" <+> pretty ty
2478 , do
2479 (iPat, i) <- quantifiedVar
2480 (jPat, j) <- quantifiedVar
2481 let indexInto matrix ix =
2482 case match opMatrixIndexingSlicing matrix of
2483 Just (base, indices) ->
2484 make opMatrixIndexingSlicing base (replaceFirstSlice ix indices)
2485 Nothing ->
2486 [essence| &matrix[&ix] |]
2487 replaceFirstSlice ix = \case
2488 Right _ : rest -> Left ix : rest
2489 indexer : rest -> indexer : replaceFirstSlice ix rest
2490 [] -> []
2491 mi = indexInto m i
2492 mj = indexInto m j
2493 return
2494 [essence|
2495 and([ &mi != &mj
2496 | &iPat : &index
2497 , &jPat : &index
2498 , &i < &j
2499 ])
2500 |]
2501 )
2502 theRule _ = na "rule_Decompose_AllDiff"
2503
2504
2505 rule_Decompose_AllDiff_MapToSingleInt :: Rule
2506 rule_Decompose_AllDiff_MapToSingleInt = "decompose-allDiff-mapToSingleInt" `namedRule` theRule where
2507 theRule [essence| allDiff(&m) |] = do
2508 case m of
2509 Comprehension body gensOrConds -> do
2510 tyBody <- typeOf body
2511 case tyBody of
2512 TypeBool -> na "rule_Decompose_AllDiff_MapToSingleInt"
2513 TypeInt _ -> na "rule_Decompose_AllDiff_MapToSingleInt"
2514 TypeTuple{} -> do
2515 bodyBits <- downX1 body
2516 bodyBitSizes <- forM bodyBits $ \ b -> do
2517 bDomain <- domainOf b
2518 domainSizeOf bDomain
2519 case (bodyBits, bodyBitSizes) of
2520 ([a,b], [_a',b']) -> do
2521 let body'= [essence| &a * &b' + &b |]
2522 let m' = Comprehension body' gensOrConds
2523 return
2524 ( "Decomposing allDiff"
2525 , return [essence| allDiff(&m') |]
2526 )
2527 _ -> na "rule_Decompose_AllDiff_MapToSingleInt"
2528 _ -> na "allDiff on something other than a comprehension."
2529 _ -> na "allDiff on something other than a comprehension."
2530 theRule _ = na "rule_Decompose_AllDiff_MapToSingleInt"
2531
2532
2533 rule_DomainCardinality :: Rule
2534 rule_DomainCardinality = "domain-cardinality" `namedRule` theRule where
2535 theRule p = do
2536 maybeDomain <- match opTwoBars p
2537 d <- expandDomainReference <$> case maybeDomain of
2538 Domain d -> return d
2539 Reference _ (Just (Alias (Domain d))) -> return d
2540 _ -> na "rule_DomainCardinality"
2541 return
2542 ( "Cardinality of a domain"
2543 , case d of
2544 DomainInt _ [RangeBounded 1 u] -> return u
2545 _ -> do
2546 (iPat, _) <- quantifiedVar
2547 return [essence| sum([ 1 | &iPat : &d ]) |]
2548 )
2549
2550
2551 rule_DomainMinMax :: Rule
2552 rule_DomainMinMax = "domain-MinMax" `namedRule` theRule where
2553 theRule [essence| max(&maybeDomain) |] = do
2554 d <- getDomain maybeDomain
2555 return
2556 ( "max of a domain"
2557 , maxOfDomain d
2558 )
2559 theRule [essence| min(&maybeDomain) |] = do
2560 d <- getDomain maybeDomain
2561 return
2562 ( "min of a domain"
2563 , minOfDomain d
2564 )
2565 theRule _ = na "rule_DomainMinMax"
2566
2567 getDomain :: MonadFailDoc m => Expression -> m (Domain () Expression)
2568 getDomain (Domain d) = return d
2569 getDomain (Reference _ (Just (Alias (Domain d)))) = getDomain (Domain d)
2570 getDomain _ = na "rule_DomainMinMax.getDomain"
2571
2572
2573 rule_ComplexAbsPat :: Rule
2574 rule_ComplexAbsPat = "complex-pattern" `namedRule` theRule where
2575 theRule (Comprehension body gensOrConds) = do
2576 (gocBefore, (pat, domainOrExpr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
2577 Generator (GenDomainNoRepr pat@AbsPatTuple{} domain) -> return (pat, Left domain)
2578 Generator (GenInExpr pat@AbsPatTuple{} expr) -> return (pat, Right expr)
2579 _ -> na "rule_ComplexAbsPat"
2580 return
2581 ( "complex pattern on tuple patterns"
2582 , do
2583 (iPat, i) <- quantifiedVar
2584 let replacements = [ (p, make opMatrixIndexing i (map (fromInt . fromIntegral) is))
2585 | (p, is) <- genMappings pat
2586 ]
2587 let f x@(Reference nm _) = fromMaybe x (lookup nm replacements)
2588 f x = x
2589 return $ Comprehension (transform f body)
2590 $ gocBefore
2591 ++ [ either (Generator . GenDomainNoRepr iPat)
2592 (Generator . GenInExpr iPat)
2593 domainOrExpr ]
2594 ++ transformBi f gocAfter
2595 )
2596 theRule _ = na "rule_ComplexAbsPat"
2597
2598 -- i --> i -> []
2599 -- (i,j) --> i -> [1]
2600 -- j -> [2]
2601 -- (i,(j,k)) --> i -> [1]
2602 -- j -> [2,1]
2603 -- k -> [2,2]
2604 genMappings :: AbstractPattern -> [(Name, [Int])]
2605 genMappings (Single nm) = [(nm, [])]
2606 genMappings (AbsPatTuple pats)
2607 = concat
2608 [ [ (patCore, i:is) | (patCore, is) <- genMappings pat ]
2609 | (i, pat) <- zip [1..] pats
2610 ]
2611 genMappings (AbsPatMatrix pats)
2612 = concat
2613 [ [ (patCore, i:is) | (patCore, is) <- genMappings pat ]
2614 | (i, pat) <- zip [1..] pats
2615 ]
2616 genMappings pat = bug ("rule_ComplexLambda.genMappings:" <+> pretty (show pat))
2617
2618
2619 -- this rule doesn't use `namedRule` because it need access to ascendants through the zipper
2620 rule_InlineConditions :: Rule
2621 rule_InlineConditions = "inline-conditions" `namedRuleZ` theRule where
2622 theRule z (Comprehension body gensOrConds) = do
2623 let (toInline, toKeep) = mconcat
2624 [ case goc of
2625 Condition x | categoryOf x == CatDecision -> ([x],[])
2626 _ -> ([],[goc])
2627 | goc <- gensOrConds
2628 ]
2629 theGuard <- case toInline of
2630 [] -> na "No condition to inline."
2631 [x] -> return x
2632 xs -> return $ make opAnd $ fromList xs
2633 (nameQ, opSkip) <- queryQ z
2634 let bodySkipped = opSkip theGuard body
2635 return
2636 ( "Inlining conditions, inside" <+> nameQ
2637 , return $ Comprehension bodySkipped toKeep
2638 )
2639 theRule _ _ = na "rule_InlineConditions"
2640
2641 -- keep going up, until finding a quantifier
2642 -- when found, return the skipping operator for the quantifier
2643 -- if none exists, do not apply the rule.
2644 -- (or maybe we should call bug right ahead, it can't be anything else.)
2645 queryQ z0 =
2646 case Zipper.up z0 of
2647 Nothing -> na "rule_InlineConditions (meh-1)"
2648 Just z -> do
2649 let h = hole z
2650 case ( match opAnd h, match opOr h, match opSum h, match opProduct h
2651 , match opMin h, match opMax h, match opOrdering h ) of
2652 (Just{}, _, _, _, _, _, _) -> return ("and", opAndSkip)
2653 (_, Just{}, _, _, _, _, _) -> return ("or" , opOrSkip )
2654 (_, _, Just{}, _, _, _, _) -> return ("sum", opSumSkip)
2655 (_, _, _, Just{}, _, _, _) -> return ("product", opProductSkip)
2656 (_, _, _, _, Just{}, _, _) -> na "rule_InlineConditions (min)"
2657 (_, _, _, _, _, Just{}, _) -> na "rule_InlineConditions (max)"
2658 (_, _, _, _, _, _, Just{}) -> return ("ordering", opSumSkip)
2659 _ -> na "rule_InlineConditions (meh-2)"
2660 -- case Zipper.up z of
2661 -- Nothing -> na "queryQ"
2662 -- Just u -> queryQ u
2663
2664 opAndSkip b x = [essence| &b -> &x |]
2665 opOrSkip b x = [essence| &b /\ &x |]
2666 opSumSkip b x = [essence| toInt(&b) * catchUndef(&x, 0) |]
2667 opProductSkip b x = [essence| [ 1
2668 , catchUndef(&x,1)
2669 ; int(0..1)
2670 ] [toInt(&b)] |]
2671
2672
2673 rule_InlineConditions_AllDiff :: Rule
2674 rule_InlineConditions_AllDiff = "inline-conditions-allDiff" `namedRule` theRule where
2675 theRule (Op (MkOpAllDiff (OpAllDiff (Comprehension body gensOrConds)))) = do
2676 let (toInline, toKeep) = mconcat
2677 [ case goc of
2678 Condition x | categoryOf x == CatDecision -> ([x],[])
2679 _ -> ([],[goc])
2680 | goc <- gensOrConds
2681 ]
2682 theGuard <- case toInline of
2683 [] -> na "No condition to inline."
2684 [x] -> return x
2685 xs -> return $ make opAnd $ fromList xs
2686
2687 tyBody <- typeOf body
2688 case tyBody of
2689 TypeInt{} -> return ()
2690 _ -> na "rule_InlineConditions_AllDiff, not an int"
2691 domBody <- domainOf body
2692 let
2693 collectLowerBounds (RangeSingle x) = return x
2694 collectLowerBounds (RangeBounded x _) = return x
2695 collectLowerBounds _ = userErr1 ("Unexpected infinite domain:" <+> pretty domBody)
2696
2697 collectLowerBoundsD (DomainInt _ rs) = mapM collectLowerBounds rs
2698 collectLowerBoundsD _ = userErr1 ("Expected an integer domain, but got:" <+> pretty domBody)
2699
2700 bounds <- collectLowerBoundsD domBody
2701 let lowerBound = make opMin (fromList bounds)
2702
2703 -- for each element, we do element-lowerBound+1
2704 -- this makes sure the smallest element is 1
2705 -- hence we can use 0 as the except value!
2706 let bodySkipped = [essence| toInt(&theGuard) * catchUndef(&body + (1 - &lowerBound), 0) |]
2707
2708 return
2709 ( "Inlining conditions, inside allDiff"
2710 , return $ make opAllDiffExcept (Comprehension bodySkipped toKeep) 0
2711 )
2712 theRule _ = na "rule_InlineConditions_AllDiff"
2713
2714
2715 rule_InlineConditions_MaxMin :: Rule
2716 rule_InlineConditions_MaxMin = "aux-for-MaxMin" `namedRule` theRule where
2717 theRule p = do
2718 when (categoryOf p < CatDecision) $ na "rule_InlineConditions_MaxMin"
2719 (nameQ, binOp, Comprehension body gensOrConds) <-
2720 case (match opMax p, match opMin p) of
2721 (Just res, _) -> return ("max", \ a b -> [essence| &a <= &b |], res )
2722 (_, Just res) -> return ("min", \ a b -> [essence| &a >= &b |], res )
2723 _ -> na "rule_InlineConditions_MaxMin"
2724 let
2725 (toInline, gocInExpr, _toKeep) = mconcat
2726 [ case goc of
2727 Condition x | categoryOf x == CatDecision -> ([x],[],[])
2728 Generator (GenInExpr {}) -> ([],[goc],[])
2729 _ -> ([],[],[goc])
2730 | goc <- gensOrConds
2731 ]
2732 when (null toInline && null gocInExpr) $ na "rule_InlineConditions_MaxMin"
2733 auxDomain <- domainOf body
2734 return
2735 ( "Creating auxiliary variable for a" <+> nameQ
2736 , do
2737 (auxName, aux) <- auxiliaryVar
2738 let auxDefinedLHS = make opSum (Comprehension 1 gensOrConds)
2739 let auxDefined = [essence| &auxDefinedLHS > 0 |]
2740 let auxUndefined = [essence| &auxDefinedLHS = 0 |]
2741 let aux' = WithLocals aux (DefinednessConstraints [auxDefined])
2742 return $ WithLocals aux'
2743 (AuxiliaryVars
2744 [ Declaration (FindOrGiven LocalFind auxName auxDomain)
2745 , SuchThat
2746 [ make opAnd $ Comprehension
2747 (binOp body aux)
2748 gensOrConds
2749
2750 -- either one of the members of this comprehension, or dontCare
2751 -- if it is indeed dontCare, care should be taken to make sure it isn't used as a normal value
2752 , make opAnd $ fromList
2753 [ make opImply auxDefined
2754 (make opOr $ Comprehension
2755 [essence| &body = &aux |]
2756 gensOrConds)
2757 , make opImply auxUndefined (make opDontCare aux)
2758 ]
2759 ]
2760 ])
2761 )
2762
2763
2764 rule_AttributeToConstraint :: Rule
2765 rule_AttributeToConstraint = "attribute-to-constraint" `namedRule` theRule where
2766 theRule (Op (MkOpAttributeAsConstraint (OpAttributeAsConstraint thing attr mval))) = do
2767 dom <- domainOf thing
2768 let conv = mkAttributeToConstraint dom attr mval thing
2769 return
2770 ( "Converting an attribute to a constraint"
2771 , bugFailT "rule_AttributeToConstraint" conv
2772 )
2773 theRule _ = na "rule_AttributeToConstraint"
2774
2775
2776 timedF :: MonadIO m => String -> (a -> m b) -> a -> m b
2777 timedF name comp a = timeItNamed name (comp a)
2778
2779
2780 evaluateModel ::
2781 MonadFailDoc m =>
2782 NameGen m =>
2783 EnumerateDomain m =>
2784 (?typeCheckerMode :: TypeCheckerMode) =>
2785 Model -> m Model
2786 evaluateModel m = do
2787 let
2788 full (Reference _ (Just (DeclHasRepr _ _ (singletonDomainInt -> Just val)))) =
2789 return val
2790 full p@Constant{} = return p
2791 full p@Domain{} = return p
2792 full p = do
2793 mconstant <- runExceptT (instantiateExpression [] p)
2794 case mconstant of
2795 Left{} -> return p
2796 Right constant ->
2797 if null [() | ConstantUndefined{} <- universe constant] -- if there are no undefined values in it
2798 then return (Constant constant)
2799 else return p
2800 let
2801 partial (Op op)
2802 | Just (x, y) <- case op of
2803 MkOpLeq (OpLeq x y) -> Just (x,y)
2804 MkOpGeq (OpGeq x y) -> Just (x,y)
2805 MkOpEq (OpEq x y) -> Just (x,y)
2806 _ -> Nothing
2807 , Reference nmX _ <- x
2808 , Reference nmY _ <- y
2809 , nmX == nmY
2810 , categoryOf x <= CatQuantified
2811 , categoryOf y <= CatQuantified
2812 = return (fromBool True)
2813 partial p@(Op x) = do
2814 mx' <- runExceptT (simplifyOp x)
2815 case mx' of
2816 Left{} -> return p
2817 Right x' -> do
2818 when (Op x == x') $ bug $ vcat
2819 [ "rule_PartialEvaluate, simplifier returns the input unchanged."
2820 , "input:" <+> vcat [ pretty (Op x)
2821 , pretty (show (Op x))
2822 ]
2823 ]
2824 return x'
2825 partial p = return p
2826
2827 (descendBiM full >=> transformBiM partial) m
2828
2829
2830 rule_FullEvaluate :: Rule
2831 rule_FullEvaluate = "full-evaluate" `namedRule` theRule where
2832 theRule Constant{} = na "rule_FullEvaluate"
2833 theRule Domain{} = na "rule_FullEvaluate"
2834 theRule (Reference _ (Just (Alias x))) -- selectively inline, unless x is huge
2835 | Just Comprehension{} <- match opToSet x
2836 = return ("Inline alias", return x)
2837 theRule p = do
2838 constant <- instantiateExpression [] p
2839 unless (null [() | ConstantUndefined{} <- universe constant]) $
2840 na "rule_PartialEvaluate, undefined"
2841 return ("Full evaluator", return $ Constant constant)
2842
2843
2844 rule_PartialEvaluate :: Rule
2845 rule_PartialEvaluate = "partial-evaluate" `namedRuleZ` theRule where
2846 -- if a variable only has a single value in its domain, replace it with the value
2847 theRule z (Reference _ (Just (DeclHasRepr _ _ (singletonDomainInt -> Just val)))) =
2848 case hole <$> Zipper.up z of
2849 Just (Op (MkOpTrue _)) -> na "rule_PartialEvaluate, inside a true(ref)"
2850 _ -> return ( "Partial evaluator"
2851 , return val
2852 )
2853 theRule _ (Op op)
2854 | Just (x, y) <- case op of
2855 MkOpLeq (OpLeq x y) -> Just (x,y)
2856 MkOpGeq (OpGeq x y) -> Just (x,y)
2857 MkOpEq (OpEq x y) -> Just (x,y)
2858 _ -> Nothing
2859 , Reference nmX _ <- x
2860 , Reference nmY _ <- y
2861 , nmX == nmY
2862 , categoryOf x <= CatQuantified
2863 , categoryOf y <= CatQuantified
2864 = return
2865 ( "Parameter = parameter (or quantified)"
2866 , return (fromBool True)
2867 )
2868 theRule _ (Op x) = do
2869 x' <- simplifyOp x
2870 when (Op x == x') $ bug $ vcat
2871 [ "rule_PartialEvaluate, simplifier returns the input unchanged."
2872 , "input:" <+> vcat [ pretty (Op x)
2873 , pretty (show (Op x))
2874 ]
2875 ]
2876 return
2877 ( "Partial evaluator"
2878 , return x'
2879 )
2880 theRule _ _ = na "rule_PartialEvaluate"
2881
2882
2883 -- | shifting quantifiers inwards, if they operate on a row of a 2d matrix,
2884 -- make them operate on the rows directly then index
2885 rule_QuantifierShift :: Rule
2886 rule_QuantifierShift = "quantifier-shift" `namedRule` theRule where
2887 theRule p = do
2888 (_, _, mkQuan, inner) <- match opReducer p
2889 (matrix, indexer) <- match opIndexing inner
2890 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2891 case ty of
2892 TypeMatrix{} -> return ()
2893 TypeList{} -> return ()
2894 _ -> na "rule_QuantifierShift"
2895 return
2896 ( "Shifting quantifier inwards"
2897 , return $ make opIndexing
2898 (make matrixLiteral
2899 ty
2900 index
2901 (map mkQuan elems))
2902 indexer
2903 )
2904
2905
2906 -- | shifting quantifiers inwards, if they operate on a flattened multi-dim matrix.
2907 rule_QuantifierShift2 :: Rule
2908 rule_QuantifierShift2 = "quantifier-shift2" `namedRule` theRule where
2909 theRule p = do
2910 (_, _, mkQuan, inner) <- match opReducer p
2911 matrix <- match opFlatten inner
2912 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2913 case ty of
2914 TypeMatrix{} -> return () -- the matrix literal should contain further matrix/list stuff.
2915 TypeList{} -> return ()
2916 _ -> na "rule_QuantifierShift2"
2917 return
2918 ( "Shifting quantifier inwards"
2919 , return $ mkQuan
2920 (make matrixLiteral
2921 ty
2922 index
2923 (map (mkQuan . flattenIfNeeded (matrixNumDims ty)) elems))
2924 )
2925
2926
2927 -- | shifting quantifiers inwards, if they operate on a concatenated multi-dim matrix.
2928 rule_QuantifierShift3 :: Rule
2929 rule_QuantifierShift3 = "quantifier-shift3" `namedRule` theRule where
2930 theRule p = do
2931 (_, True, mkQuan, inner) <- match opReducer p
2932 matrix <- match opConcatenate inner
2933 (TypeMatrix _ ty, index, elems) <- match matrixLiteral matrix
2934 return
2935 ( "Shifting quantifier inwards"
2936 , return $ mkQuan $ make matrixLiteral
2937 ty
2938 index
2939 (map mkQuan elems)
2940 )
2941
2942
2943 rule_Comprehension_Simplify :: Rule
2944 rule_Comprehension_Simplify = "comprehension-simplify" `namedRule` theRule where
2945 theRule (Comprehension x gocs)
2946 | let isTrueCondition (Condition (Constant (ConstantBool True))) = True
2947 isTrueCondition _ = False
2948 , let gocs' = filter (not . isTrueCondition) gocs
2949 , length gocs' < length gocs
2950 = return
2951 ( "Removing true conditions"
2952 , return $ Comprehension x gocs'
2953 )
2954 theRule _ = na "rule_Comprehension_Simplify"
2955
2956
2957 rule_Xor_To_Sum :: Rule
2958 rule_Xor_To_Sum = "xor-to-sum" `namedRule` theRule where
2959 theRule [essence| xor(&arg) |] =
2960 case arg of
2961 Comprehension body goc -> do
2962 let argOut = Comprehension [essence| toInt(&body) |] goc
2963 return
2964 ( "xor to sum"
2965 , return [essence| 1 = sum(&argOut) % 2 |]
2966 )
2967 AbstractLiteral (AbsLitMatrix dom elems) -> do
2968 let argOut = AbstractLiteral $ AbsLitMatrix dom
2969 [ [essence| toInt(&el) |] | el <- elems ]
2970 return
2971 ( "xor to sum"
2972 , return [essence| 1 = sum(&argOut) % 2 |]
2973 )
2974 _ -> do
2975 (iPat, i) <- quantifiedVar
2976 return
2977 ( "xor to sum"
2978 , return [essence| 1 = sum([ toInt(&i) | &iPat <- &arg ]) % 2 |]
2979 )
2980 theRule _ = na "rule_Xor_To_Sum"
2981
2982
2983 -- These representation-dependent assertions are symmetry hints, not reifiable
2984 -- predicates on abstract constants. Restrict them before any rewriting.
2985 checkCustomSymmetries :: MonadFailDoc m => Model -> m Model
2986 checkCustomSymmetries model = do
2987 forM_ (mStatements model) $ \st -> case st of
2988 SuchThat xs -> mapM_ checkAssertion xs
2989 _ -> rejectNested (universeBi st)
2990 return model
2991 where
2992 rejectNested xs = when (any isCustom xs) $
2993 failDoc "applySymmetries and applySymmetriesAfterRepresentation must be top-level such-that assertions"
2994 isCustom (Op MkOpApplySymmetries{}) = True
2995 isCustom _ = False
2996 checkAssertion (Op (MkOpApplySymmetries (OpApplySymmetries delayed values syms))) = do
2997 let opName = if delayed then "applySymmetriesAfterRepresentation" else "applySymmetries"
2998 rejectNested (universe values ++ universe syms)
2999 when (categoryOf syms > CatParameter) $
3000 failDoc $ opName <> ": symmetries must be constant or given"
3001 checkValues opName values
3002 checkAssertion x = rejectNested (universe x)
3003 checkValues opName x = case followAliases id x of
3004 AbstractLiteral (AbsLitTuple xs) -> mapM_ (checkValues opName) xs
3005 Reference _ (Just DeclNoRepr{}) -> return ()
3006 Reference _ (Just DeclHasRepr{}) -> return ()
3007 _ -> failDoc $ opName <> ": values must be a tuple of variable references"
3008
3009
3010 enforceTagConsistency :: MonadFail m => Model -> m Model
3011 enforceTagConsistency model = do
3012 let statements' = transformBi reDomExp $ transformBi reDomConst (mStatements model)
3013 return model { mStatements = statements' }
3014
3015
3016 addUnnamedSymmetryBreaking ::
3017 NameGen m =>
3018 Maybe UnnamedSymmetryBreaking ->
3019 Model ->
3020 m Model
3021 addUnnamedSymmetryBreaking mode model = do
3022
3023 let
3024 allUnnamedTypes :: [(Domain () Expression, Expression)]
3025 allUnnamedTypes =
3026 [ reTag (TagUnnamed nm') (DomainReference nm Nothing, x) --x is a TagInt at this point so we must reTag it
3027 | Declaration (LettingDomainDefnUnnamed nm@(Name nm') x) <- mStatements model
3028 ]
3029
3030 allDecVars =
3031 [ (Reference nm Nothing, domain)
3032 | Declaration (FindOrGiven Find nm domain) <- mStatements model
3033 ]
3034
3035 -- allDecVarsAux auxSuffix =
3036 -- [ (Reference (mconcat [nm, "_auxFor_", auxSuffix]) Nothing, domain)
3037 -- | Declaration (FindOrGiven Find nm domain) <- mStatements model
3038 -- ]
3039
3040 varsTuple = case allDecVars of
3041 [v] -> fst v
3042 _ -> AbstractLiteral $ AbsLitTuple $ map fst allDecVars
3043 -- mkAuxTuple auxSuffix = AbstractLiteral $ AbsLitTuple $ map fst (allDecVarsAux auxSuffix)
3044
3045 -- traceM $ show $ "Unnamed types in this model:" <++> prettyList id "," allUnnamedTypes
3046 -- traceM $ show $ "Unnamed decision variables in this model:" <++> prettyList id "," allDecVars
3047
3048 -- 3 axis of doom
3049 -- 1. Delayed/Eager. Delayed is permutationOrderAfterRepresentation(x, p) -- this is an efficient subset of x .<= p(x)
3050 -- Eager is x .<= p(x)
3051 -- 2. Scope. Consecutive
3052 -- AllPairs
3053 -- AllPermutations
3054 -- 3. Independently/Altogether
3055
3056 case mode of
3057 Nothing -> return model
3058 Just (UnnamedSymmetryBreaking delayedOrEager usbScope independentlyOrAltogether) -> do
3059 -- let newDecls =
3060 -- case delayedOrEager of
3061 -- USBDelayed -> []
3062 -- USBEager ->
3063 -- case independentlyOrAltogether of
3064 -- USBIndependently ->
3065 -- [ Declaration (FindOrGiven LocalFind nm' domain)
3066 -- | Declaration (FindOrGiven Find nm domain) <- mStatements model
3067 -- , (DomainReference uName _, _) <- allUnnamedTypes
3068 -- , let nm' = mconcat [nm, "_auxFor_", uName]
3069 -- ]
3070 -- USBAltogether ->
3071 -- [ Declaration (FindOrGiven LocalFind nm' domain)
3072 -- | Declaration (FindOrGiven Find nm domain) <- mStatements model
3073 -- , let nm' = mconcat [nm, "_auxFor_all"]
3074 -- ]
3075
3076 let
3077
3078 combinedPermApply perms =
3079 case delayedOrEager of
3080 USBDelayed -> make opPermutationOrderAfterRepresentation perms varsTuple
3081 USBEager -> make opPermutationOrder perms varsTuple
3082
3083 mkGenerator_Consecutive _ [] = bug "must have at least one unnamed type"
3084 mkGenerator_Consecutive perms [(u, uSize)] = do
3085 (iPat, i) <- quantifiedVar
3086 let perm = [essence| permutation((&i, succ(&i))) |]
3087 let applied = combinedPermApply (perm:perms)
3088 return [essence|
3089 and([ &applied
3090 | &iPat : &u
3091 , &i < &uSize
3092 ])
3093 |]
3094 mkGenerator_Consecutive perms ((u, uSize):us) = do
3095 (iPat, i) <- quantifiedVar
3096 let perm = [essence| permutation((&i, succ(&i))) |]
3097 applied <- mkGenerator_Consecutive (perm:perms) us
3098 return [essence|
3099 and([ &applied
3100 | &iPat : &u
3101 , &i < &uSize
3102 ])
3103 |]
3104
3105
3106 mkGenerator_AllPairs _ [] = bug "must have at least one unnamed type"
3107 mkGenerator_AllPairs perms [(u, _uSize)] = do
3108 (iPat, i) <- quantifiedVar
3109 (jPat, j) <- quantifiedVar
3110 let perm = [essence| permutation((&i, &j)) |]
3111 let applied = combinedPermApply (perm:perms)
3112 return [essence|
3113 and([ &applied
3114 | &iPat : &u
3115 , &jPat : &u
3116 , &i < &j
3117 ])
3118 |]
3119 mkGenerator_AllPairs perms ((u, _uSize):us) = do
3120 (iPat, i) <- quantifiedVar
3121 (jPat, j) <- quantifiedVar
3122 let perm = [essence| permutation((&i, &j)) |]
3123 applied <- mkGenerator_AllPairs (perm:perms) us
3124 return [essence|
3125 and([ &applied
3126 | &iPat : &u
3127 , &jPat : &u
3128 , &i < &j
3129 ])
3130 |]
3131
3132 mkGenerator_AllPermutations _ [] = bug "must have at least one unnamed type"
3133 mkGenerator_AllPermutations perms [(u, _uSize)] = do
3134 (iPat, i) <- quantifiedVar
3135 let perm = i
3136 let applied = combinedPermApply (perm:perms)
3137 return [essence|
3138 and([ &applied
3139 | &iPat : permutation of &u
3140 ])
3141 |]
3142 mkGenerator_AllPermutations perms ((u, _uSize):us) = do
3143 (iPat, i) <- quantifiedVar
3144 let perm = i
3145 applied <- mkGenerator_AllPermutations (perm:perms) us
3146 return [essence|
3147 and([ &applied
3148 | &iPat : permutation of &u
3149 ])
3150 |]
3151
3152 mkGenerator perms us =
3153 case usbScope of
3154 USBConsecutive -> mkGenerator_Consecutive perms us
3155 USBAllPairs -> mkGenerator_AllPairs perms us
3156 USBAllPermutations -> mkGenerator_AllPermutations perms us
3157 newCons <-
3158 case independentlyOrAltogether of
3159 USBIndependently -> do
3160 xs <- sequence
3161 [ mkGenerator [] [(u, uSize)]
3162 | (u@DomainReference{}, uSize) <- allUnnamedTypes
3163 ]
3164 return [SuchThat xs]
3165 USBAltogether -> do
3166 cons <- mkGenerator [] allUnnamedTypes
3167 return [SuchThat [cons]]
3168
3169 let stmts = newCons
3170 traceM $ show $ vcat $ "Adding the following unnamed symmetry breaking constraints:"
3171 : map (nest 4 . pretty) stmts
3172 return model { mStatements = mStatements model ++ stmts}
3173
3174
3175
3176 rule_Comprehension_Cardinality :: Rule
3177 rule_Comprehension_Cardinality = "comprehension-cardinality" `namedRule` theRule where
3178 theRule p = do
3179 Comprehension _ gensOrConds <- match opTwoBars p
3180 let ofones = Comprehension (fromInt 1) gensOrConds
3181 return ( "Horizontal rule for comprehension cardinality"
3182 , return [essence| sum(&ofones) |]
3183 )
3184
3185 rule_Flatten_Cardinality :: Rule
3186 rule_Flatten_Cardinality = "flatten-cardinality" `namedRule` theRule where
3187 theRule p = do
3188 list <- match opTwoBars p >>= match opConcatenate
3189 return ( "Horizontal rule for comprehension cardinality"
3190 , do
3191 (iPat, i) <- quantifiedVar
3192 return [essence| sum([ |&i| | &iPat <- &list ]) |]
3193 )