never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Process.Sanity ( sanityChecks, isInfinite ) where
4
5 import Conjure.Prelude
6 import Conjure.UserError
7 import Conjure.Language
8 import Conjure.Language.CategoryOf
9
10
11 sanityChecks :: (MonadFailDoc m, MonadUserError m) => Model -> m Model
12 sanityChecks model = do
13 let
14 recordErr :: MonadWriter [Doc] m => [Doc] -> m ()
15 recordErr = tell . return . vcat
16
17 check :: (MonadFailDoc m, MonadWriter [Doc] m) => Model -> m Model
18 check m = do
19 upToOneObjective m
20 upToOneHeuristic m
21 upToOneBranchingOn m
22 forM_ (mStatements m) $ \ st -> case st of
23 Declaration (FindOrGiven Given _ _) -> return () -- skip
24 Declaration FindOrGiven{} -> mapM_ (checkDomain True (Just st)) (universeBi (forgetRefs st))
25 _ -> mapM_ (checkDomain False (Just st)) (universeBi (forgetRefs st))
26 forM_ (mStatements m) $ \ st -> case st of
27 SuchThat{} ->
28 forM_ (universeBi st) $ \ x -> do
29 case x of
30 Comprehension{} ->
31 forM_ (universeBi x) $ \case
32 GenDomainNoRepr _ dom -> checkDomain True (Just st) dom
33 _ -> return ()
34 _ -> return ()
35 let mab = case x of
36 [essence| &a = &b |] -> Just (a,b)
37 [essence| &a != &b |] -> Just (a,b)
38 _ -> Nothing
39 case mab of
40 Just (a,b) -> do
41 let
42 disallowed (Comprehension _ gocs) =
43 or [ not $ null [ () | Generator (GenInExpr {}) <- gocs ]
44 , not $ null [ () | Condition c <- gocs, categoryOf c == CatDecision ]
45 ]
46 disallowed _ = False
47 when (disallowed a || disallowed b) $
48 recordErr [ "Type error in" <+> vcat
49 [ pretty x
50 , "Cannot use a comprehension in an equality expression."
51 ] ]
52 _ -> return ()
53 _ -> return ()
54 mapM_ checkFactorial (universeBi $ mStatements m)
55 statements2 <- transformBiM updateSizeAttr =<< transformBiM checkLit (mStatements m)
56 return m { mStatements = statements2 }
57
58 -- check for mset attributes
59 -- check for binary relation attrobutes
60 checkDomain :: MonadWriter [Doc] m => Bool -> Maybe Statement -> Domain () Expression -> m ()
61 checkDomain checkForInfinity mstmt domain = case domain of
62 DomainInt _ rs | checkForInfinity && isInfinite rs -> recordErr
63 [ "Infinite integer domain."
64 , "Context:" <++> maybe (pretty domain) pretty mstmt
65 ]
66 DomainMatrix index _
67 | domainCanIndexMatrix index -> return ()
68 | otherwise -> recordErr
69 [ "A matrix cannot be indexed with this domain:" <++> pretty index
70 , "Context:" <++> maybe (pretty domain) pretty mstmt
71 ]
72 DomainSequence _ (SequenceAttr size _) _ ->
73 case size of
74 SizeAttr_Size{} -> return ()
75 SizeAttr_MaxSize{} -> return ()
76 SizeAttr_MinMaxSize{} -> return ()
77 _ -> recordErr
78 [ "sequence requires (at least) one of the following attributes: size, maxSize"
79 , "Context:" <++> maybe (pretty domain) pretty mstmt
80 ]
81 DomainMSet _ (MSetAttr size occur) _ ->
82 case (size, occur) of
83 (SizeAttr_Size{}, _) -> return ()
84 (SizeAttr_MaxSize{}, _) -> return ()
85 (SizeAttr_MinMaxSize{}, _) -> return ()
86 (_, OccurAttr_MaxOccur{}) -> return ()
87 (_, OccurAttr_MinMaxOccur{}) -> return ()
88 _ -> recordErr
89 [ "mset requires (at least) one of the following attributes: size, maxSize, maxOccur"
90 , "Context:" <++> maybe (pretty domain) pretty mstmt
91 ]
92 DomainRelation _ (RelationAttr _ binRelAttr) [a,b]
93 | binRelAttr /= def && a /= b
94 -> recordErr
95 [ "Binary relation attributes can only be used for binary relation between identical domains."
96 , "Either remove these attributes:" <+> pretty binRelAttr
97 , "Or make sure that the relation is between identical domains."
98 , "Context:" <++> maybe (pretty domain) pretty mstmt
99 ]
100 DomainRelation _ (RelationAttr _ binRelAttr) innerDoms
101 | binRelAttr /= def && length innerDoms /= 2
102 -> recordErr
103 [ "Binary relation attributes can only be used on binary relations."
104 , "Either remove these attributes:" <+> pretty binRelAttr
105 , "Or make sure that the relation is binary."
106 , "Context:" <++> maybe (pretty domain) pretty mstmt
107 ]
108 _ -> return ()
109
110
111 updateSizeAttr :: Monad m => SizeAttr Expression -> m (SizeAttr Expression)
112 updateSizeAttr (SizeAttr_MinMaxSize a b) | a == b = return (SizeAttr_Size a)
113 updateSizeAttr s = return s
114
115
116 -- check for function literals
117 -- they cannot map the same element to multiple range elemnets
118 -- check for partition literals
119 -- the parts have to be disjoint
120 -- TODO: Generate where clauses for when they contain parameters.
121 checkLit :: MonadFailDoc m => Expression -> m Expression
122 checkLit lit = case lit of
123 AbstractLiteral (AbsLitSet xs) -> do
124 let ys = fromList xs
125 return $ WithLocals lit (DefinednessConstraints [ [essence| allDiff(&ys) |] ])
126 AbstractLiteral (AbsLitFunction mappings) -> do
127 let defineds = fromList $ map fst mappings
128 return $ WithLocals lit (DefinednessConstraints [ [essence| allDiff(&defineds) |] ])
129 AbstractLiteral (AbsLitPartition parts) -> do
130 let disjoint = concat
131 [ checks
132 | (part1, after) <- withAfter parts
133 , part2 <- after
134 , let checks = [ [essence| &el1 != &el2 |]
135 | el1 <- part1
136 , el2 <- part2
137 ]
138 ]
139 return $
140 if null disjoint
141 then lit
142 else WithLocals lit (DefinednessConstraints disjoint)
143 _ -> return lit
144
145 checkFactorial :: MonadWriter [Doc] m => Expression -> m ()
146 checkFactorial p@[essence| factorial(&x) |]
147 | categoryOf x >= CatDecision
148 = recordErr
149 [ "The factorial function does not work on decision expressions."
150 , "Context:" <++> pretty p
151 ]
152 checkFactorial _ = return ()
153
154 upToOne :: MonadWriter [Doc] m => (Statement -> Bool) -> Doc -> Model -> m ()
155 upToOne f message m = do
156 let found = [ st | st <- mStatements m, f st ]
157 unless (length found <= 1) $ recordErr
158 [ "Expected at most one \'" <> message <> "\' statement, but got" <+> pretty (length found) <> "."
159 , vcat $ map (nest 4 . ("-" <+>) . pretty) found
160 ]
161
162 upToOneObjective :: MonadWriter [Doc] m => Model -> m ()
163 upToOneObjective = upToOne (\ st -> case st of Objective{} -> True; _ -> False) "objective"
164
165 upToOneHeuristic :: MonadWriter [Doc] m => Model -> m ()
166 upToOneHeuristic = upToOne (\ st -> case st of SearchHeuristic{} -> True; _ -> False) "heuristic"
167
168 upToOneBranchingOn :: MonadWriter [Doc] m => Model -> m ()
169 upToOneBranchingOn = upToOne (\ st -> case st of SearchOrder{} -> True; _ -> False) "branching on"
170
171
172 (model', errs) <- runWriterT (check model)
173 if null errs
174 then return model'
175 else userErr errs
176
177 -- | return True if a bunch of ranges represent an infinite domain.
178 -- return False if finite. also, return false if unsure.
179 isInfinite :: [Range a] -> Bool
180 isInfinite [] = True
181 isInfinite [RangeOpen{}] = True
182 isInfinite [RangeLowerBounded{}] = True
183 isInfinite [RangeUpperBounded{}] = True
184 isInfinite _ = False
185
186 forgetRefs :: Statement -> Statement
187 forgetRefs = transformBi f
188 where
189 f (Reference nm _) = Reference nm Nothing
190 f x = x