@@ -1,5 +1,6 @@
11{-# OPTIONS_GHC -Wno-orphans #-}
2−module OpenAPI.Checker.Validate.Schema
2+
3+module Data.OpenApi.Compare.Validate.Schema
34 (
45 )
56where
@@ -10,63 +11,64 @@ import Data.Coerce
1011import Data.Foldable (for_, toList)
1112import Data.Functor
1213import Data.HList
14+import Data.List (genericIndex, genericLength, group)
1315import qualified Data.List.NonEmpty as NE
1416import qualified Data.Map as M
15−import Data.List (group, genericLength, genericIndex)
1617import Data.Maybe
1718import Data.OpenApi
19+import Data.OpenApi.Compare.Behavior
20+import Data.OpenApi.Compare.Paths
21+import qualified Data.OpenApi.Compare.PathsPrefixTree as P
22+import Data.OpenApi.Compare.Subtree
23+import Data.OpenApi.Compare.Validate.Schema.DNF
24+import Data.OpenApi.Compare.Validate.Schema.Issues
25+import Data.OpenApi.Compare.Validate.Schema.JsonFormula
26+import Data.OpenApi.Compare.Validate.Schema.Partition
27+import Data.OpenApi.Compare.Validate.Schema.Process
28+import Data.OpenApi.Compare.Validate.Schema.Traced
29+import Data.OpenApi.Compare.Validate.Schema.TypedJson
1830import Data.Ord
1931import Data.Ratio
2032import Data.Semigroup
2133import qualified Data.Set as S
2234import Data.Text (Text)
23−import OpenAPI.Checker.Behavior
24−import OpenAPI.Checker.Paths
25−import qualified OpenAPI.Checker.PathsPrefixTree as P
26−import OpenAPI.Checker.Subtree
27−import OpenAPI.Checker.Validate.Schema.DNF
28−import OpenAPI.Checker.Validate.Schema.Issues
29−import OpenAPI.Checker.Validate.Schema.JsonFormula
30−import OpenAPI.Checker.Validate.Schema.Traced
31−import OpenAPI.Checker.Validate.Schema.TypedJson
32−import OpenAPI.Checker.Validate.Schema.Partition
33−import OpenAPI.Checker.Validate.Schema.Process
3435
35−checkFormulas
36− :: (ReassembleHList xs (CheckEnv (Referenced Schema)))
37− => HList xs
38− -> Behavior 'SchemaLevel
39− -> ProdCons (Trace Schema)
40− -> ProdCons (Traced (Definitions Schema))
41− -> ProdCons (ForeachType JsonFormula, P.PathsPrefixTree Behave AnIssue 'SchemaLevel)
42− -> SemanticCompatFormula ()
36+checkFormulas ::
37+ (ReassembleHList xs (CheckEnv (Referenced Schema))) =>
38+ HList xs ->
39+ Behavior 'SchemaLevel ->
40+ ProdCons (Trace Schema) ->
41+ ProdCons (Traced (Definitions Schema)) ->
42+ ProdCons (ForeachType JsonFormula, P.PathsPrefixTree Behave AnIssue 'SchemaLevel) ->
43+ SemanticCompatFormula ()
4344checkFormulas env beh trs defs (ProdCons (fp, ep) (fc, ec)) =
4445 case P.toList ep ++ P.toList ec of
4546 issues@(_ : _) -> for_ issues $ embedFormula beh . anItem
4647 [] -> do
4748 -- We have the following isomorphisms:
48− -- (A ⊂ X ∪ Y) = (A ⊂ X) \/ (A ⊂ Y)
4949 -- (A ⊂ X ∩ Y) = (A ⊂ X) /\ (A ⊂ Y)
5050 -- (A ⊂ ⊤) = 1
5151 -- (X ∪ Y ⊂ B) = (X ⊂ B) /\ (Y ⊂ B)
5252 -- (∅ ⊂ B) = 1
5353 -- The remaining cases are, notably, not isomorphisms:
54− -- 1) (A ⊂ ∅) <= 0
55− -- 2) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
56− -- 3) (⊤ ⊂ B) <= 0
57− -- Therefore we have the isomorphisms with (∃ and ∀ being the N-ary
54+ -- 1) (A ⊂ X ∪ Y) <= (A ⊂ X) \/ (A ⊂ Y)
55+ -- 2) (A ⊂ ∅) <= 0
56+ -- 3) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
57+ -- 4) (⊤ ⊂ B) <= 0
58+ -- Therefore we have the implications with (∃ and ∀ being the N-ary
5859 -- versions of \/ and /\ respectively):
5960 -- (⋃_i ⋂_j A[i,j]) ⊂ (⋃_k ⋂_l B[k,l])
60− -- = ∃k ∀l ∀i, (⋂_j A[i,j]) ⊂ B[k,l]
61+ -- <= ∃k ∀l ∀i, (⋂_j A[i,j]) ⊂ B[k,l]
6162 -- = ∀i ∃k ∀l, (⋂_j A[i,j]) ⊂ B[k,l]
6263 -- with the caveat that the the set over which k ranges is nonempty.
63− -- This is because 1) is not an isomorphism.
64+ -- (because 2) is not an isomorphism), and that this is a sufficient
65+ -- but not necessary condition (because 1) is not an isomorphism).
6466 -- Our disjunction loses information, so it makes sense to nest it as
6567 -- deeply as possible, hence we choose the latter representation.
6668 --
6769 -- We delegate the verification of (⋂_j A[j]) ⊂ B to a separate heuristic
6870 -- function, with the understanding that ∃j, A[j] ⊂ B is a sufficient,
69− -- but not necessary condition (because of 2) and 3)).
71+ -- but not necessary condition (because of 3) and 4)).
7072 --
7173 -- If k ranges over an empty set, we have the isomorphism:
7274 -- (⋃_i ⋂_j A[i,j]) ⊂ ∅ = ∀i, (⋂_j A[i,j]) ⊂ ∅
@@ -143,21 +145,21 @@ checkFormulas env beh trs defs (ProdCons (fp, ep) (fc, ec)) =
143145 EnumDoesntSatisfy $ untypeValue e -- what does this look like when partitioned?
144146 issueFromDisjunct mPart ps = NoMatchingCondition mPart $ SomeCondition <$> S.toList ps
145147
146−checkContradiction
147− :: Behavior 'TypedSchemaLevel
148− -> Maybe Partition
149− -> S.Set (Condition t)
150− -> SemanticCompatFormula ()
148+checkContradiction ::
149+ Behavior 'TypedSchemaLevel ->
150+ Maybe Partition ->
151+ S.Set (Condition t) ->
152+ SemanticCompatFormula ()
151153checkContradiction beh mPart _ = issueAt beh $ maybe TypeBecomesEmpty PartitionBecomesEmpty mPart -- TODO #70
152154
153−checkImplication
154− :: (ReassembleHList xs (CheckEnv (Referenced Schema)))
155− => HList xs
156− -> Behavior 'TypedSchemaLevel
157− -> ProdCons (Trace Schema) -- the traces of the root schemas used in this comparison
158− -> S.Set (Condition t)
159− -> Condition t
160− -> SemanticCompatFormula ()
155+checkImplication ::
156+ (ReassembleHList xs (CheckEnv (Referenced Schema))) =>
157+ HList xs ->
158+ Behavior 'TypedSchemaLevel ->
159+ ProdCons (Trace Schema) -> -- the traces of the root schemas used in this comparison
160+ S.Set (Condition t) ->
161+ Condition t ->
162+ SemanticCompatFormula ()
161163checkImplication env beh trs prods cons = case findExactly prods of
162164 Just e
163165 | all (satisfiesTyped e) prods ->
@@ -165,124 +167,104 @@ checkImplication env beh trs prods cons = case findExactly prods of
165167 then pure ()
166168 else issueAt beh (EnumDoesntSatisfy $ untypeValue e)
167169 | otherwise -> pure () -- vacuously true
168−
169170 Nothing -> case cons of
170171 -- the above code didn't catch it, so there's no Exactly condition on the lhs
171172 Exactly e -> issueAt beh (NoMatchingEnum $ untypeValue e)
172−
173173 Maximum m -> foldCheck min m NoMatchingMaximum MatchingMaximumWeak $ \case
174174 Maximum m' -> Just m'
175175 _ -> Nothing
176−
177176 Minimum m -> foldCheck max m (NoMatchingMinimum . coerce) (MatchingMinimumWeak . coerce) $ \case
178177 Minimum m' -> Just m'
179178 _ -> Nothing
180−
181179 MultipleOf m -> foldCheck lcmScientific m NoMatchingMultipleOf MatchingMultipleOfWeak $ \case
182180 MultipleOf m' -> Just m'
183181 _ -> Nothing
184−
185182 NumberFormat f -> case flip any prods $ \case
186− NumberFormat f' -> f == f'
187− _ -> False
188− of
183+ NumberFormat f' -> f == f'
184+ _ -> False of
189185 True -> pure ()
190186 False -> issueAt beh (NoMatchingFormat f)
191−
192187 MaxLength m -> foldCheck min m NoMatchingMaxLength MatchingMaxLengthWeak $ \case
193188 MaxLength m' -> Just m'
194189 _ -> Nothing
195−
196190 MinLength m -> foldCheck max m NoMatchingMinLength MatchingMinLengthWeak $ \case
197191 MinLength m' -> Just m'
198192 _ -> Nothing
199−
200193 Pattern p -> case flip any prods $ \case
201− Pattern p' -> p == p'
202− _ -> False
203− of
194+ Pattern p' -> p == p'
195+ _ -> False of
204196 True -> pure ()
205197 False -> issueAt beh (NoMatchingPattern p) -- TODO: regex comparison #32
206−
207198 StringFormat f -> case flip any prods $ \case
208− StringFormat f' -> f == f'
209− _ -> False
210− of
199+ StringFormat f' -> f == f'
200+ _ -> False of
211201 True -> pure ()
212202 False -> issueAt beh (NoMatchingFormat f)
213−
214203 Items _ cons' -> case foldSome (<>) prods $ \case
215− Items _ rs -> Just (Just (rs NE.:| []), mempty)
216− TupleItems (map snd -> fs) -> Just (mempty, Just (fs NE.:| []))
217− _ -> Nothing
218− of
204+ Items _ rs -> Just (Just (rs NE.:| []), mempty)
205+ TupleItems (map snd -> fs) -> Just (mempty, Just (fs NE.:| []))
206+ _ -> Nothing of
219207 Just (mItems, Just pfs)
220208 | not $ allSame (length <$> pfs) -> pure () -- vacuously
221− | let plen = genericLength (NE.head pfs)
222− -> clarifyIssue (AnItem beh (anIssue TupleToArray)) $ for_ [0 .. plen - 1] $ \i -> do
223− let prod' = tracedConjunct $ case mItems of
224− Just prods' -> ((`genericIndex` i) <$> pfs) <> prods'
225− Nothing -> (`genericIndex` i) <$> pfs
226− checkCompatibility (beh >>> step (InItem i)) env $ ProdCons prod' cons'
209+ | let plen = genericLength (NE.head pfs) ->
210+ clarifyIssue (AnItem beh (anIssue TupleToArray)) $
211+ for_ [0 .. plen - 1] $ \i -> do
212+ let prod' = tracedConjunct $ case mItems of
213+ Just prods' -> ((`genericIndex` i) <$> pfs) <> prods'
214+ Nothing -> (`genericIndex` i) <$> pfs
215+ checkCompatibility (beh >>> step (InItem i)) env $ ProdCons prod' cons'
227216 Just (Just prods', Nothing) -> do
228217 let prod' = tracedConjunct prods'
229218 checkCompatibility (beh >>> step InItems) env $ ProdCons prod' cons'
230219 _ -> clarifyIssue (AnItem beh (anIssue NoMatchingItems)) $ do
231220 checkCompatibility (beh >>> step InItems) env $ ProdCons prodTopSchema cons'
232−
233221 TupleItems (map snd -> fs) -> case foldSome (<>) prods $ \case
234− TupleItems (map snd -> fs') -> Just (Just $ fs' NE.:| [], Just . Max $ genericLength fs', Just . Min $ genericLength fs', mempty)
235− MinItems m' -> Just (mempty, Just . Max $ m', mempty, mempty)
236− MaxItems m' -> Just (mempty, mempty, Just . Min $ m', mempty)
237− Items _ rs -> Just (mempty, mempty, mempty, Just (rs NE.:| []))
238− _ -> Nothing
239− of
240− -- if the length constraints in the producer are contradictory:
241− Just (_, Just (Max lowest), Just (Min highest), _) | lowest > highest -> pure ()
242− -- We have an explicit tuple items clause...
243− Just (Just pfs, Just (Max plen), _, _)
244− | plen /= genericLength fs -- ...of wrong length
245− -> issueAt beh (TupleItemsLengthChanged ProdCons {producer = plen, consumer = genericLength fs})
246− | otherwise
247− -> for_ [0 .. plen - 1] $ \i -> do
222+ TupleItems (map snd -> fs') -> Just (Just $ fs' NE.:| [], Just . Max $ genericLength fs', Just . Min $ genericLength fs', mempty)
223+ MinItems m' -> Just (mempty, Just . Max $ m', mempty, mempty)
224+ MaxItems m' -> Just (mempty, mempty, Just . Min $ m', mempty)
225+ Items _ rs -> Just (mempty, mempty, mempty, Just (rs NE.:| []))
226+ _ -> Nothing of
227+ -- if the length constraints in the producer are contradictory:
228+ Just (_, Just (Max lowest), Just (Min highest), _) | lowest > highest -> pure ()
229+ -- We have an explicit tuple items clause...
230+ Just (Just pfs, Just (Max plen), _, _)
231+ | plen /= genericLength fs -> -- ...of wrong length
232+ issueAt beh (TupleItemsLengthChanged ProdCons {producer = plen, consumer = genericLength fs})
233+ | otherwise ->
234+ for_ [0 .. plen - 1] $ \i -> do
248235 checkCompatibility (beh >>> step (InItem i)) env $ ProdCons (tracedConjunct $ (`genericIndex` i) <$> pfs) (fs `genericIndex` i)
249− -- We have a fixed length array in the producer...
250− Just (Nothing, Just (Max plen), Just (Min plen'), mProd)
251− | plen == plen'
252− -> clarifyIssue (AnItem beh (anIssue ArrayToTuple)) $ case mProd of
253− _ | plen /= genericLength fs -> -- ...of wrong length
254− issueAt beh (TupleItemsLengthChanged ProdCons {producer = plen, consumer = genericLength fs})
236+ -- We have a fixed length array in the producer...
237+ Just (Nothing, Just (Max plen), Just (Min plen'), mProd)
238+ | plen == plen' ->
239+ clarifyIssue (AnItem beh (anIssue ArrayToTuple)) $ case mProd of
240+ _
241+ | plen /= genericLength fs -> -- ...of wrong length
242+ issueAt beh (TupleItemsLengthChanged ProdCons {producer = plen, consumer = genericLength fs})
255243 Just rs -> for_ [0 .. plen - 1] $ \i -> do
256244 checkCompatibility (beh >>> step (InItem i)) env $ ProdCons (tracedConjunct rs) (fs `genericIndex` i)
257245 -- ...and no "items" schema
258246 Nothing -> clarifyIssue (AnItem beh (anIssue NoMatchingTupleItems)) $ do
259247 for_ [0 .. plen - 1] $ \i -> do
260248 checkCompatibility (beh >>> step (InItem i)) env $ ProdCons prodTopSchema (fs `genericIndex` i)
261− _ -> issueAt beh NoMatchingTupleItems
262−
249+ _ -> issueAt beh NoMatchingTupleItems
263250 MaxItems m -> foldCheck min m NoMatchingMaxItems MatchingMaxItemsWeak $ \case
264251 MaxItems m' -> Just m'
265252 TupleItems fs -> Just $ toInteger $ length fs
266253 _ -> Nothing
267−
268254 MinItems m -> foldCheck max m NoMatchingMinItems MatchingMinItemsWeak $ \case
269255 MinItems m' -> Just m'
270256 TupleItems fs -> Just $ toInteger $ length fs
271257 _ -> Nothing
272−
273258 UniqueItems -> case flip any prods $ \case
274− UniqueItems -> True
275− MaxItems 1 -> True
276− TupleItems fs | length fs == 1 -> True
277− _ -> False
278− of
259+ UniqueItems -> True
260+ MaxItems 1 -> True
261+ TupleItems fs | length fs == 1 -> True
262+ _ -> False of
279263 True -> pure ()
280264 False -> issueAt beh NoMatchingUniqueItems
281−
282265 Properties props _ madd -> case foldSome (<>) prods $ \case
283− Properties props' _ madd' -> Just $ (props', madd') NE.:| []
284− _ -> Nothing
285− of
266+ Properties props' _ madd' -> Just $ (props', madd') NE.:| []
267+ _ -> Nothing of
286268 Just pm ->
287269 anyOfAt beh NoMatchingProperties $ -- TODO: could first "concat" the lists
288270 NE.toList pm <&> \(props', madd') -> do
@@ -313,11 +295,9 @@ checkImplication env beh trs prods cons = case findExactly prods of
313295 (Just add', Just add) -> checkCompatibility (beh >>> step InAdditionalProperty) env (ProdCons add' add)
314296 pure ()
315297 Nothing -> issueAt beh NoMatchingProperties
316−
317298 MaxProperties m -> foldCheck min m NoMatchingMaxProperties MatchingMaxPropertiesWeak $ \case
318299 MaxProperties m' -> Just m'
319300 _ -> Nothing
320−
321301 MinProperties m -> foldCheck max m NoMatchingMinProperties MatchingMinPropertiesWeak $ \case
322302 MinProperties m' -> Just m'
323303 _ -> Nothing
@@ -325,14 +305,14 @@ checkImplication env beh trs prods cons = case findExactly prods of
325305 lcmScientific (toRational -> a) (toRational -> b) =
326306 fromRational $ lcm (numerator a) (numerator b) % gcd (denominator a) (denominator b)
327307
328− foldCheck
329− :: Eq a
330− => (a -> a -> a)
331− -> a
332− -> (a -> Issue 'TypedSchemaLevel)
333− -> (ProdCons a -> Issue 'TypedSchemaLevel)
334− -> (forall t. Condition t -> Maybe a)
335− -> SemanticCompatFormula ()
308+ foldCheck ::
309+ Eq a =>
310+ (a -> a -> a) ->
311+ a ->
312+ (a -> Issue 'TypedSchemaLevel) ->
313+ (ProdCons a -> Issue 'TypedSchemaLevel) ->
314+ (forall t. Condition t -> Maybe a) ->
315+ SemanticCompatFormula ()
336316 foldCheck f m missing weak extr = case foldSome f prods extr of
337317 Just m'
338318 | f m' m == m' -> pure ()