never executed always true always false
1 -- {-# OPTIONS_GHC -fmax-pmcheck-iterations=50000000 #-} -- stupid cmdargs
2
3 module Conjure.Process.ValidateConstantForDomain ( validateConstantForDomain ) where
4
5 import Conjure.Prelude
6 import Conjure.Language.Constant
7 import Conjure.Language.Definition
8 import Conjure.Language.Domain
9 import Conjure.Language.Type
10 import Conjure.Language.Pretty
11 import Conjure.Language.Instantiate ( instantiateExpression )
12 import Conjure.Process.AttributeAsConstraints ( mkAttributeToConstraint )
13 import Conjure.Process.Enumerate ( EnumerateDomain, enumerateDomain )
14
15 -- containers
16 import Data.Set as S ( size, size, fromList, toList, toAscList, difference )
17
18
19 -- | Assuming both the value and the domain are normalised
20 -- TODO: this is incomplete, which means parameter values won't be checked for every property
21
22 validateConstantForDomain ::
23 forall m r .
24 MonadFailDoc m =>
25 NameGen m =>
26 EnumerateDomain m =>
27 (?typeCheckerMode :: TypeCheckerMode) =>
28 Pretty r =>
29 Eq r =>
30 Name -> Constant -> Domain r Constant -> m ()
31
32 validateConstantForDomain _ (viewConstantBool -> Just _) DomainBool{} = return ()
33
34 validateConstantForDomain _ _ (DomainInt _ []) = return () -- no restrictions
35
36 -- enums, always ok
37 validateConstantForDomain _ (ConstantEnum (Name ty1) _ _) (DomainInt (TagEnum ty2) _) | ty1 == ty2 = return ()
38
39 validateConstantForDomain name c@(viewConstantIntWithTag -> Just (cTag, i)) d@(DomainInt dTag rs) | cTag == dTag =
40 let
41 intInRange RangeOpen = True
42 intInRange (RangeSingle (ConstantInt _ a)) = i == a
43 intInRange (RangeLowerBounded (ConstantInt _ a)) = i >= a
44 intInRange (RangeUpperBounded (ConstantInt _ a)) = i <= a
45 intInRange (RangeBounded (ConstantInt _ a) (ConstantInt _ b)) = i >= a && i <= b
46 intInRange _ = False
47 in unless (any intInRange rs) (constantNotInDomain name c d)
48
49 validateConstantForDomain _ (viewConstantIntWithTag -> Just (_, i)) (DomainUnnamed _ (ConstantInt _ a)) | i >= 1 && i <= a = return ()
50
51 validateConstantForDomain _ _ (DomainEnum _ Nothing _) = return () -- no restrictions
52 validateConstantForDomain name c d@(DomainEnum _ _ Nothing) =
53 failDoc $ vcat [ "validateConstantForDomain: enum not handled"
54 , pretty name
55 , pretty c
56 , pretty d
57 ]
58 validateConstantForDomain name
59 c@(viewConstantIntWithTag -> Just (cTag, _))
60 d@(DomainEnum _ (Just ranges) (Just mp)) = nested c d $ do
61 let
62 -- lu :: MonadFailDoc m => Name -> m Constant
63 lu (ConstantEnum _ _ nm) =
64 case lookup nm mp of
65 Nothing -> failDoc $ "No value for:" <+> pretty nm
66 Just v -> return (ConstantInt cTag v)
67 lu (ConstantInt t v) = return (ConstantInt t v)
68 lu x = failDoc $ "validateConstantForDomain.lu" <+> pretty x
69
70 -- lu2 :: MonadFailDoc m => Range Name -> m (Range Constant)
71 lu2 = mapM lu
72
73 rs <- mapM lu2 ranges
74 validateConstantForDomain name c (DomainInt cTag rs :: Domain r Constant)
75
76 validateConstantForDomain name
77 c@(viewConstantTuple -> Just cs)
78 d@(DomainTuple ds) = nested c d $ zipWithM_ (validateConstantForDomain name) cs ds
79
80 validateConstantForDomain name
81 c@(viewConstantRecord -> Just cs)
82 d@(DomainRecord (sortOn fst -> ds))
83 | map fst cs == map fst ds
84 = nested c d $ zipWithM_ (validateConstantForDomain name) (map snd cs) (map snd ds)
85 | otherwise
86 = constantNotInDomain name c d
87
88 validateConstantForDomain name
89 c@(viewConstantVariant -> Just (_, n, c'))
90 d@(DomainVariant ds)
91 | Just d' <- lookup n ds
92 = nested c d $ validateConstantForDomain name c' d'
93 | otherwise
94 = constantNotInDomain name c d
95
96 validateConstantForDomain name
97 c@(viewConstantMatrix -> Just (cIndex, vals))
98 d@(DomainMatrix dIndex dInner) = do
99 nested c d $
100 mapM_ (\ val -> validateConstantForDomain name val dInner ) vals
101 let
102 isEmptyIntDomain (DomainInt _ []) = True
103 isEmptyIntDomain _ = False
104 unless (cIndex == dIndex || isEmptyIntDomain cIndex) $ failDoc $ vcat
105 [ "The indices do not match between the value and the domain."
106 , "Value :" <+> pretty c
107 , "Domain:" <+> pretty d
108 ]
109
110 validateConstantForDomain name
111 c@(viewConstantSet -> Just vals)
112 d@(DomainSet _ (SetAttr sizeAttr) dInner) = do
113 let cardinalityOK = case sizeAttr of
114 SizeAttr_None -> True
115 SizeAttr_Size (ConstantInt _ s) -> s == genericLength vals
116 SizeAttr_MinSize (ConstantInt _ s) -> s <= genericLength vals
117 SizeAttr_MaxSize (ConstantInt _ s) -> genericLength vals <= s
118 SizeAttr_MinMaxSize (ConstantInt _ smin) (ConstantInt _ smax) ->
119 smin <= genericLength vals && genericLength vals <= smax
120 _ -> False
121 unless cardinalityOK $ failDoc $ vcat
122 [ "The value is not a member of the domain."
123 , "Value :" <+> pretty c
124 , "Domain:" <+> pretty d
125 , "Reason: Domain attributes are not satisfied."
126 , "Specifically:" <+> pretty sizeAttr
127 ]
128 nested c d $ mapM_ (\ val -> validateConstantForDomain name val dInner ) vals
129
130 validateConstantForDomain name
131 c@(viewConstantMSet -> Just vals)
132 d@(DomainMSet _ (MSetAttr sizeAttr occurAttr) dInner) = do
133 let cardinalityOK = case sizeAttr of
134 SizeAttr_None -> True
135 SizeAttr_Size (ConstantInt _ s) -> s == genericLength vals
136 SizeAttr_MinSize (ConstantInt _ s) -> s <= genericLength vals
137 SizeAttr_MaxSize (ConstantInt _ s) -> genericLength vals <= s
138 SizeAttr_MinMaxSize (ConstantInt _ smin) (ConstantInt _ smax) ->
139 smin <= genericLength vals && genericLength vals <= smax
140 _ -> False
141 unless cardinalityOK $ failDoc $ vcat
142 [ "The value is not a member of the domain."
143 , "Value :" <+> pretty c
144 , "Domain:" <+> pretty d
145 , "Reason: Domain attributes are not satisfied."
146 , "Specifically:" <+> pretty sizeAttr
147 ]
148 let occurOK = case occurAttr of
149 OccurAttr_None -> True
150 OccurAttr_MinOccur (ConstantInt _ s) -> and [ s <= occ | (_, occ) <- histogram vals ]
151 OccurAttr_MaxOccur (ConstantInt _ s) -> and [ occ <= s | (_, occ) <- histogram vals ]
152 OccurAttr_MinMaxOccur (ConstantInt _ smin) (ConstantInt _ smax) ->
153 and [ smin <= occ && occ <= smax | (_, occ) <- histogram vals ]
154 _ -> False
155 unless occurOK $ failDoc $ vcat
156 [ "The value is not a member of the domain."
157 , "Value :" <+> pretty c
158 , "Domain:" <+> pretty d
159 , "Reason: Domain attributes are not satisfied."
160 , "Specifically:" <+> pretty occurAttr
161 ]
162 nested c d $ mapM_ (\ val -> validateConstantForDomain name val dInner ) vals
163
164 validateConstantForDomain name
165 c@(viewConstantFunction -> Just vals)
166 d@(DomainFunction _ _ dFrom dTo) = nested c d $ do
167 mapM_ (\ val -> validateConstantForDomain name (fst val) dFrom) vals
168 mapM_ (\ val -> validateConstantForDomain name (snd val) dTo ) vals
169
170 validateConstantForDomain name
171 c@(viewConstantSequence -> Just vals)
172 d@(DomainSequence _ attr dInner) = do
173 case attr of
174 SequenceAttr sizeAttr@(SizeAttr_Size (ConstantInt _ s)) _ | s /= genericLength vals ->
175 failDoc $ vcat
176 [ "The value is not a member of the domain."
177 , "Value :" <+> pretty c
178 , "Domain:" <+> pretty d
179 , "Reason: Domain attributes are not satisfied."
180 , "Specifically:" <+> pretty sizeAttr
181 ]
182 SequenceAttr _ jectivity | jectivity `elem` [JectivityAttr_Surjective, JectivityAttr_Bijective] -> do
183 constants <- enumerateDomain (forgetRepr dInner)
184 let missing = S.toAscList (S.fromList constants `S.difference` S.fromList vals)
185 unless (null missing) $ failDoc $ vcat
186 [ "The value is not a member of the domain."
187 , "Value :" <+> pretty c
188 , "Domain:" <+> pretty d
189 , "Reason: Domain attributes are not satisfied."
190 , "Specifically:" <+> pretty JectivityAttr_Surjective
191 ]
192 _ -> return ()
193 nested c d $
194 mapM_ (\ val -> validateConstantForDomain name val dInner ) vals
195
196 validateConstantForDomain name
197 c@(viewConstantRelation -> Just valss)
198 d@(DomainRelation _ (RelationAttr sizeAttr (BinaryRelationAttrs binRelAttrs)) dInners) = do
199 let numValss = genericLength valss
200 let cardinalityOK = case sizeAttr of
201 SizeAttr_None -> True
202 SizeAttr_Size (ConstantInt _ s) -> s == numValss
203 SizeAttr_MinSize (ConstantInt _ s) -> s <= numValss
204 SizeAttr_MaxSize (ConstantInt _ s) -> numValss <= s
205 SizeAttr_MinMaxSize (ConstantInt _ smin) (ConstantInt _ smax) ->
206 smin <= numValss && numValss <= smax
207 _ -> False
208 unless cardinalityOK $ failDoc $ vcat
209 [ "The value is not a member of the domain."
210 , "Value :" <+> pretty c
211 , "Domain:" <+> pretty d
212 , "Reason: Domain attributes are not satisfied."
213 , "Specifically:" <+> pretty sizeAttr
214 ]
215 when (S.size binRelAttrs > 0 && length dInners /= 2) $ failDoc $ vcat
216 [ "The value is not a member of the domain."
217 , "Value :" <+> pretty c
218 , "Domain:" <+> pretty d
219 , "Reason: Binary relation attributes cannot be used for this domain."
220 , "Specifically:" <+> prettyList id "," (S.toList binRelAttrs)
221 ]
222 forM_ (S.toList binRelAttrs) $ \ a -> do
223 constraint <- mkAttributeToConstraint (fmap Constant d) (binRelToAttrName a) Nothing (Constant c)
224 evaluated <- instantiateExpression [] constraint
225 case evaluated of
226 ConstantBool True -> return ()
227 ConstantBool False -> failDoc $ vcat
228 [ "The value is not a member of the domain."
229 , "Value :" <+> pretty c
230 , "Domain:" <+> pretty d
231 , "Reason: Domain attributes are not satisfied."
232 , "Specifically:" <+> pretty a
233 ]
234 evaluatedC -> failDoc $ vcat
235 [ "The value is not a member of the domain."
236 , "Value :" <+> pretty c
237 , "Domain:" <+> pretty d
238 , "Reason: Domain attributes are not satisfied."
239 , "Specifically:" <+> pretty a
240 , "Evaluted to:" <+> pretty evaluatedC
241 ]
242 nested c d $ forM_ valss $ \ vals ->
243 zipWithM_ (validateConstantForDomain name) vals dInners
244
245 validateConstantForDomain name
246 c@(viewConstantPartition -> Just valss)
247 d@(DomainPartition _ _ dInner) = nested c d $
248 mapM_ (\ val -> validateConstantForDomain name val dInner ) (concat valss)
249
250 validateConstantForDomain name c@(TypedConstant c' _) d = nested c d $ validateConstantForDomain name c' d
251
252 validateConstantForDomain name c d = constantNotInDomain name c d
253
254
255 nested ::
256 MonadFailDoc m =>
257 Pretty c =>
258 Pretty d =>
259 c -> d -> ExceptT m () -> m ()
260 nested c d inner = do
261 mres <- runExceptT inner
262 case mres of
263 Right () -> return ()
264 Left err ->
265 failDoc $ vcat
266 [ "The value is not a member of the domain."
267 , "Value :" <+> pretty c
268 , "Domain:" <+> pretty d
269 , "Reason:"
270 , nest 4 err
271 ]
272
273
274 constantNotInDomain :: (MonadFailDoc m, Pretty r) => Name -> Constant -> Domain r Constant -> m ()
275 constantNotInDomain n c d = failDoc $ vcat
276 [ "The value is not a member of the domain."
277 , "Name :" <+> pretty n
278 , "Value :" <+> pretty c
279 , "Domain:" <+> pretty d
280 ]
281
282