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