@@ -0,0 +1,780 @@
1+{-# OPTIONS_GHC -fno-warn-orphans #-}
2+module OpenAPI.Checker.Validate.Schema
15+import Algebra.Lattice
16+import Control.Applicative
17+import Control.Monad.Reader
18+import Control.Monad.Writer
19+import qualified Data.Aeson as A
21+import qualified Data.Foldable as F
22+import qualified Data.HashMap.Strict as HM
23+import qualified Data.HashMap.Strict.InsOrd as IOHM
27+import qualified Data.List.NonEmpty as NE
28+import qualified Data.Map as M
33+import Data.Scientific
34+import qualified Data.Set as S
35+import Data.Text (Text)
36+import qualified Data.Text as T hiding (singleton)
38+import OpenAPI.Checker.Orphans ()
39+import OpenAPI.Checker.References
40+import OpenAPI.Checker.Subtree
41+import OpenAPI.Checker.Trace
42+import qualified OpenAPI.Checker.TracePrefixTree as T
44+-- | Type of a JSON value
54+-- | A 'A.Value' whose type we know
55+data TypedValue :: JsonType -> Type where
56+ TNull :: TypedValue 'Null
57+ TBool :: !Bool -> TypedValue 'Boolean
58+ TNumber :: !Scientific -> TypedValue 'Number
59+ TString :: !Text -> TypedValue 'String
60+ TArray :: !A.Array -> TypedValue 'Array
61+ TObject :: !A.Object -> TypedValue 'Object
63+deriving stock instance Eq (TypedValue t)
64+deriving stock instance Ord (TypedValue t)
65+deriving stock instance Show (TypedValue t)
67+untypeValue :: TypedValue t -> A.Value
68+untypeValue TNull = A.Null
69+untypeValue (TBool b) = A.Bool b
70+untypeValue (TNumber n) = A.Number n
71+untypeValue (TString s) = A.String s
72+untypeValue (TArray a) = A.Array a
73+untypeValue (TObject o) = A.Object o
75+data Bound a = Exclusive !a | Inclusive !a
78+-- | The order is lexicographical on @a * Bool@.
79+instance Ord a => Ord (Bound a) where
80+ Exclusive a `compare` Exclusive b = compare a b
81+ Exclusive a `compare` Inclusive b = if a <= b then LT else GT
82+ Inclusive a `compare` Exclusive b = if a < b then LT else GT
83+ Inclusive a `compare` Inclusive b = compare a b
85+data Property = Property
86+ { propRequired :: Bool
87+ , propFormula :: ForeachType (JsonFormula OpenApi)
88+ , propRefSchema :: Traced OpenApi (Referenced Schema)
90+ deriving stock (Eq, Ord, Show)
92+-- | A primitive structural condition for the "top level" of a JSON value (of a specific type)
93+data Condition :: JsonType -> Type where
94+ Exactly :: TypedValue t -> Condition t
95+ Maximum :: !(Bound Scientific) -> Condition 'Number
96+ Minimum :: !(Down (Bound (Down Scientific))) -> Condition 'Number
97+ -- ^ this has the right Ord
98+ MultipleOf :: !Scientific -> Condition 'Number
99+ NumberFormat :: !Format -> Condition 'Number
100+ MaxLength :: !Integer -> Condition 'String
101+ MinLength :: !Integer -> Condition 'String
102+ Pattern :: !Pattern -> Condition 'String
103+ StringFormat :: !Format -> Condition 'String
105+ :: !(ForeachType (JsonFormula OpenApi))
106+ -> !(Traced OpenApi (Referenced Schema))
108+ MaxItems :: !Integer -> Condition 'Array
109+ MinItems :: !Integer -> Condition 'Array
110+ UniqueItems :: Condition 'Array
112+ :: !(M.Map Text Property)
113+ -> !(ForeachType (JsonFormula OpenApi))
114+ -- ^ formula for additional properties
115+ -> !(Maybe (Traced OpenApi (Referenced Schema)))
116+ -- ^ schema for additional properties, Nothing means bottom
117+ -> Condition 'Object
118+ MaxProperties :: !Integer -> Condition 'Object
119+ MinProperties :: !Integer -> Condition 'Object
121+satisfiesTyped :: TypedValue t -> Condition t -> Bool
122+satisfiesTyped e (Exactly e') = e == e'
123+satisfiesTyped (TNumber n) (Maximum (Exclusive m)) = n < m
124+satisfiesTyped (TNumber n) (Maximum (Inclusive m)) = n <= m
125+satisfiesTyped (TNumber n) (Minimum (Down (Exclusive (Down m)))) = n > m
126+satisfiesTyped (TNumber n) (Minimum (Down (Inclusive (Down m)))) = n >= m
127+satisfiesTyped (TNumber n) (MultipleOf m) = denominator (toRational n / toRational m) == 1 -- TODO: could be better
128+satisfiesTyped (TNumber n) (NumberFormat f) = checkNumberFormat f n
129+satisfiesTyped (TString s) (MaxLength m) = fromIntegral (T.length s) <= m
130+satisfiesTyped (TString s) (MinLength m) = fromIntegral (T.length s) >= m
131+satisfiesTyped (TString s) (Pattern p) = undefined s p -- TODO: regex stuff
132+satisfiesTyped (TString s) (StringFormat f) = undefined s f-- TODO: string format
133+satisfiesTyped (TArray a) (Items f _) = all (`satisfies` f) a
134+satisfiesTyped (TArray a) (MaxItems m) = fromIntegral (F.length a) <= m
135+satisfiesTyped (TArray a) (MinItems m) = fromIntegral (F.length a) >= m
136+satisfiesTyped (TArray a) UniqueItems = S.size (S.fromList $ F.toList a) == F.length a -- TODO: could be better
137+satisfiesTyped (TObject o) (Properties props additional _)
138+ = all (`HM.member` o) (M.keys (M.filter propRequired props))
139+ && all (\(k, v) -> satisfies v $ maybe additional propFormula $ M.lookup k props) (HM.toList o)
140+satisfiesTyped (TObject o) (MaxProperties m) = fromIntegral (HM.size o) <= m
141+satisfiesTyped (TObject o) (MinProperties m) = fromIntegral (HM.size o) >= m
143+checkNumberFormat :: Format -> Scientific -> Bool
144+checkNumberFormat "int32" (toRational -> n) = denominator n == 1
145+ && n >= toRational (minBound :: Int32) && n <= toRational (maxBound :: Int32)
146+checkNumberFormat "int64" (toRational -> n) = denominator n == 1
147+ && n >= toRational (minBound :: Int64) && n <= toRational (maxBound :: Int64)
148+checkNumberFormat "float" _n = True
149+checkNumberFormat "double" _n = True
150+checkNumberFormat f _n = error $ "Invalid number format: " <> T.unpack f
152+deriving stock instance Eq (Condition t)
153+deriving stock instance Ord (Condition t)
154+deriving stock instance Show (Condition t)
156+data SomeCondition where
157+ SomeCondition :: Typeable t => Condition t -> SomeCondition
159+instance Eq SomeCondition where
160+ SomeCondition x == SomeCondition y = case cast x of
164+instance Ord SomeCondition where
165+ compare (SomeCondition x) (SomeCondition y) = case cast x of
166+ Just x' -> compare x' y
167+ Nothing -> compare (typeRep x) (typeRep y)
169+deriving stock instance Show SomeCondition
171+-- | A boolean formula (without "not") of 'Condition's. Represented as a
172+-- Disjunctive Normal Form: the formula is a disjunction of a set of conjuncts,
173+-- each of which is a conjunction of a set of 'Condition's.
174+newtype JsonFormula r t
175+ = DNF (S.Set (M.Map (Condition t) (Trace r (Condition t))))
176+ deriving stock (Eq, Ord, Show)
180+ -> M.Map (Condition t) (Trace r (Condition t))
183+ | any (`isMapSubsetOf` xs) yss = DNF yss
184+ | otherwise = DNF $ S.insert xs $ S.filter (not . isMapSubsetOf xs) yss
186+ isMapSubsetOf a b = M.keysSet a `S.isSubsetOf` M.keysSet b
188+instance Lattice (JsonFormula r t) where
189+ xss \/ DNF yss = S.foldl' disjAdd xss yss
190+ DNF xss /\ DNF yss = F.foldl' disjAdd bottom $
191+ liftA2 M.union (S.toList xss) (S.toList yss)
193+pattern BottomFormula :: JsonFormula r t
194+pattern BottomFormula <- DNF (S.null -> True)
195+ where BottomFormula = DNF S.empty
197+isSingleton :: S.Set a -> Maybe a
199+ | S.size s == 1 = S.lookupMin s
200+ | otherwise = Nothing
202+pattern Conjunct :: [Traced r (Condition t)] -> M.Map (Condition t) (Trace r (Condition t))
203+pattern Conjunct xs <- (map (uncurry $ flip Traced) . M.toList -> xs)
204+ where Conjunct xs = M.fromList [(x, t) | Traced t x <- xs]
205+{-# COMPLETE Conjunct #-}
207+pattern SingleConjunct :: [Traced r (Condition t)] -> JsonFormula r t
208+pattern SingleConjunct xs <- DNF (isSingleton -> Just (Conjunct xs))
209+ where SingleConjunct xs = DNF $ S.singleton $ Conjunct xs
211+pattern TopFormula :: JsonFormula r t
212+pattern TopFormula <- DNF (isSingleton -> Just (M.null -> True))
213+ where TopFormula = DNF $ S.singleton M.empty
215+instance BoundedJoinSemiLattice (JsonFormula r t) where
216+ bottom = BottomFormula
218+instance BoundedMeetSemiLattice (JsonFormula r t) where
221+singletonFormula :: Trace r (Condition t) -> Condition t -> JsonFormula r t
222+singletonFormula t x = SingleConjunct [Traced t x]
226+ => (Traced r (Condition t) -> l)
229+foldLattice f (DNF xss) = S.foldl' (\z w ->
230+ z \/ M.foldlWithKey' (\x y t -> x /\ f (Traced t y)) top w) bottom xss
232+satisfiesFormula :: TypedValue t -> JsonFormula r t -> Bool
233+satisfiesFormula val = foldLattice (satisfiesTyped val . getTraced)
235+data ForeachType (f :: JsonType -> Type) = ForeachType
236+ { forNull :: f 'Null
237+ , forBoolean :: f 'Boolean
238+ , forNumber :: f 'Number
239+ , forString :: f 'String
240+ , forArray :: f 'Array
241+ , forObject :: f 'Object
244+satisfies :: A.Value -> ForeachType (JsonFormula r) -> Bool
245+satisfies val p = case val of
246+ A.Null -> satisfiesFormula TNull $ forNull p
247+ A.Bool b -> satisfiesFormula (TBool b) $ forBoolean p
248+ A.Number n -> satisfiesFormula (TNumber n) $ forNumber p
249+ A.String s -> satisfiesFormula (TString s) $ forString p
250+ A.Array a -> satisfiesFormula (TArray a) $ forArray p
251+ A.Object o -> satisfiesFormula (TObject o) $ forObject p
253+deriving stock instance (forall x. Typeable x => Eq (f x)) => Eq (ForeachType f)
254+deriving stock instance (forall x. Typeable x => Ord (f x)) => Ord (ForeachType f)
255+deriving stock instance (forall x. Typeable x => Show (f x)) => Show (ForeachType f)
259+ => (forall x. Typeable x => (ForeachType f -> f x) -> m)
271+ => (forall x. Typeable x => (ForeachType f -> f x) -> m ())
282+instance (forall x. Lattice (f x)) => Lattice (ForeachType f) where
283+ f1 \/ f2 = ForeachType
284+ { forNull = forNull f1 \/ forNull f2
285+ , forBoolean = forBoolean f1 \/ forBoolean f2
286+ , forNumber = forNumber f1 \/ forNumber f2
287+ , forString = forString f1 \/ forString f2
288+ , forArray = forArray f1 \/ forArray f2
289+ , forObject = forObject f1 \/ forObject f2
291+ f1 /\ f2 = ForeachType
292+ { forNull = forNull f1 /\ forNull f2
293+ , forBoolean = forBoolean f1 /\ forBoolean f2
294+ , forNumber = forNumber f1 /\ forNumber f2
295+ , forString = forString f1 /\ forString f2
296+ , forArray = forArray f1 /\ forArray f2
297+ , forObject = forObject f1 /\ forObject f2
300+instance (forall x. BoundedJoinSemiLattice (f x))
301+ => BoundedJoinSemiLattice (ForeachType f) where
302+ bottom = ForeachType
304+ , forBoolean = bottom
305+ , forNumber = bottom
306+ , forString = bottom
308+ , forObject = bottom
311+instance (forall x. BoundedMeetSemiLattice (f x))
312+ => BoundedMeetSemiLattice (ForeachType f) where
322+instance Typeable t => Steppable Schema (Condition t) where
323+ data Step Schema (Condition t)
325+ | MaximumFields -- maximum & exclusiveMaximum
326+ | MinimumFields -- minimum & exclusiveMinimum
336+ | PropertiesFields -- properties, additionalProperties & required
337+ | MaxPropertiesField
338+ | MinPropertiesField
340+ | IntegerType -- type=integer
341+ deriving (Eq, Ord, Show)
343+instance Steppable Schema (Referenced Schema) where
344+ data Step Schema (Referenced Schema)
349+ | AdditionalPropertiesStep
350+ | PropertiesStep Text
351+ deriving (Eq, Ord, Show)
353+type ProcessM = ReaderT (Definitions Schema) (Writer (T.TracePrefixTree SubtreeCheckIssue OpenApi))
355+warn :: Subtree t => Trace OpenApi t -> CheckIssue t -> ProcessM ()
356+warn t x = tell $ T.singleton $ AnItem t $ SubtreeCheckIssue x
359+ :: Traced OpenApi (Referenced Schema)
360+ -> ProcessM (ForeachType (JsonFormula OpenApi))
361+processRefSchema x = do
363+ processSchema $ dereferenceTraced defs x
365+-- | Turn a schema into a tuple of 'JsonFormula's that describes the condition
366+-- for every possible type of a JSON value. The conditions are independent, and
367+-- are thus checked independently.
369+ :: Traced OpenApi Schema
370+ -> ProcessM (ForeachType (JsonFormula OpenApi))
371+processSchema (Traced t Schema{..}) = do
373+ allClauses <- case _schemaAllOf of
375+ Just [] -> [] <$ warn t (InvalidSchema "no items in allOf")
377+ [ processRefSchema (Traced (t `Snoc` AllOfStep i) rs)
378+ | (i, rs) <- zip [0..] xs ]
380+ anyClause <- case _schemaAnyOf of
382+ Just [] -> bottom <$ warn t (InvalidSchema "no items in anyOf")
383+ Just xs -> joins <$> sequence
384+ [ processRefSchema (Traced (t `Snoc` AnyOfStep i) rs)
385+ | (i, rs) <- zip [0..] xs ]
387+ oneClause <- case _schemaOneOf of
389+ Just [] -> bottom <$ warn t (InvalidSchema "no items in oneOf")
391+ checkOneOfDisjoint xs >>= \case
393+ False -> warn t (NotSupported "Could not determine that oneOf branches are disjoint")
395+ [ processRefSchema (Traced (t `Snoc` OneOfStep i) rs)
396+ | (i, rs) <- zip [0..] xs ]
400+ Just _ -> warn t (NotSupported "not clause is unsupported")
403+ typeClause = case _schemaType of
405+ Just OpenApiNull -> bottom
407+ Just OpenApiBoolean -> bottom
408+ { forBoolean = top }
409+ Just OpenApiNumber -> bottom
410+ { forBoolean = top }
411+ Just OpenApiInteger -> bottom
412+ { forNumber = singletonFormula (t `Snoc` IntegerType) $ MultipleOf 1 }
413+ Just OpenApiString -> bottom
415+ Just OpenApiArray -> bottom
417+ Just OpenApiObject -> bottom
421+ valueEnum A.Null = bottom
422+ { forNull = singletonFormula (t `Snoc` EnumField) $ Exactly TNull }
423+ valueEnum (A.Bool b) = bottom
424+ { forBoolean = singletonFormula (t `Snoc` EnumField) $ Exactly $ TBool b }
425+ valueEnum (A.Number n) = bottom
426+ { forNumber = singletonFormula (t `Snoc` EnumField) $ Exactly $ TNumber n }
427+ valueEnum (A.String s) = bottom
428+ { forString = singletonFormula (t `Snoc` EnumField) $ Exactly $ TString s }
429+ valueEnum (A.Array a) = bottom
430+ { forArray = singletonFormula (t `Snoc` EnumField) $ Exactly $ TArray a }
431+ valueEnum (A.Object o) = bottom
432+ { forObject = singletonFormula (t `Snoc` EnumField) $ Exactly $ TObject o }
433+ enumClause <- case _schemaEnum of
435+ Just [] -> bottom <$ warn t (InvalidSchema "no items in enum")
436+ Just xs -> pure $ joins (valueEnum <$> xs)
439+ maximumClause = case _schemaMaximum of
442+ { forNumber = singletonFormula (t `Snoc` MaximumFields) $ Maximum $
443+ case _schemaExclusiveMaximum of
444+ Just True -> Exclusive n
447+ minimumClause = case _schemaMinimum of
450+ { forNumber = singletonFormula (t `Snoc` MinimumFields) $ Minimum $ Down $
451+ case _schemaExclusiveMinimum of
452+ Just True -> Exclusive $ Down n
453+ _ -> Inclusive $ Down n }
455+ multipleOfClause = case _schemaMultipleOf of
458+ { forNumber = singletonFormula (t `Snoc` MultipleOfField) $ MultipleOf n }
460+ formatClause <- case _schemaFormat of
462+ Just f | f `elem` ["int32", "int64", "float", "double"] -> pure top
463+ { forNumber = singletonFormula (t `Snoc` FormatField) $ NumberFormat f }
464+ Just f | f `elem` ["byte", "binary", "date", "date-time", "password"] -> pure top
465+ { forString = singletonFormula (t `Snoc` FormatField) $ StringFormat f }
466+ Just f -> top <$ warn t (NotSupported $ "Unknown format: " <> f)
469+ maxLengthClause = case _schemaMaxLength of
472+ { forString = singletonFormula (t `Snoc` MaxLengthField) $ MaxLength n }
474+ minLengthClause = case _schemaMinLength of
477+ { forString = singletonFormula (t `Snoc` MinLengthField) $ MinLength n }
479+ patternClause = case _schemaPattern of
482+ { forString = singletonFormula (t `Snoc` PatternField) $ Pattern p }
484+ itemsClause <- case _schemaItems of
486+ Just (OpenApiItemsObject rs) -> do
487+ let trs = Traced (t `Snoc` ItemsStep) rs
488+ f <- processRefSchema trs
489+ pure top { forArray = singletonFormula (t `Snoc` ItemsField) $ Items f trs }
490+ Just (OpenApiItemsArray _) -> top <$ warn t (NotSupported "array in items is not supported")
493+ maxItemsClause = case _schemaMaxItems of
496+ { forArray = singletonFormula (t `Snoc` MaxItemsField) $ MaxItems n }
498+ minItemsClause = case _schemaMinItems of
501+ { forArray = singletonFormula (t `Snoc` MinItemsField) $ MinItems n }
503+ uniqueItemsClause = case _schemaUniqueItems of
505+ { forArray = singletonFormula (t `Snoc` UniqueItemsField) UniqueItems }
508+ (addProps, addPropSchema) <- case _schemaAdditionalProperties of
509+ Just (AdditionalPropertiesSchema rs) -> do
510+ let trs = Traced (t `Snoc` AdditionalPropertiesStep) rs
511+ (,Just trs) <$> processRefSchema trs
512+ Just (AdditionalPropertiesAllowed False) -> pure (bottom, Nothing)
513+ _ -> pure (top, Just $ Traced (t `Snoc` AdditionalPropertiesStep) $ Inline mempty)
514+ propList <- forM (S.toList . S.fromList $ IOHM.keys _schemaProperties <> _schemaRequired) $ \k -> do
515+ (f, sch) <- case IOHM.lookup k _schemaProperties of
517+ let trs = Traced (t `Snoc` PropertiesStep k) rs
518+ (,trs) <$> processRefSchema trs
519+ Nothing -> pure (addProps, fromMaybe (Traced (t `Snoc` AdditionalPropertiesStep) $ Inline mempty) addPropSchema)
520+ -- The mempty here is incorrect, but if addPropSchema was Nothing, then
521+ -- addProps is bottom, and k is in _schemaRequired. We handle this situation
522+ -- below and short-circuit the entire Properties condition to bottom
523+ pure (k, Property (k `elem` _schemaRequired) f sch)
525+ allBottom f = getAll $ foldType $ \ty -> case ty f of
526+ BottomFormula -> All True
528+ allTop f = getAll $ foldType $ \ty -> case ty f of
529+ TopFormula -> All True
531+ -- remove optional fields whose schemata match that of additional props
532+ propMap = M.filter (\p -> propRequired p || not (propFormula p /= addProps)) $ M.fromList propList
534+ | any (\p -> propRequired p && allBottom (propFormula p)) propMap
535+ = bottom -- if any required field has unsatisfiable schema
536+ | M.null propMap, allTop addProps
537+ = top -- if all fields are optional and have trivial schemata
540+ { forObject = singletonFormula (t `Snoc` PropertiesFields) $ Properties propMap addProps addPropSchema }
542+ maxPropertiesClause = case _schemaMaxProperties of
545+ { forObject = singletonFormula (t `Snoc` MaxPropertiesField) $ MaxProperties n }
547+ minPropertiesClause = case _schemaMinProperties of
550+ { forObject = singletonFormula (t `Snoc` MinPropertiesField) $ MinProperties n }
553+ | Just True <- _schemaNullable = bottom
554+ { forNull = singletonFormula (t `Snoc` NullableField) $ Exactly TNull }
555+ | otherwise = bottom
557+ pure $ nullableClause \/ meets (allClauses <>
558+ [ anyClause, oneClause, typeClause, enumClause, maximumClause, minimumClause
559+ , multipleOfClause, formatClause, maxLengthClause, minLengthClause
560+ , patternClause, itemsClause, maxItemsClause, minItemsClause
561+ , uniqueItemsClause, propertiesClause, maxPropertiesClause, minPropertiesClause])
562+{- TODO: ReadOnly/WriteOnly -}
564+checkOneOfDisjoint :: [Referenced Schema] -> ProcessM Bool
565+checkOneOfDisjoint = const $ pure True -- TODO
568+ :: Definitions Schema
569+ -> Traced OpenApi Schema
570+ -> (ForeachType (JsonFormula OpenApi), T.TracePrefixTree SubtreeCheckIssue OpenApi)
571+schemaToFormula defs rs = runWriter . (`runReaderT` defs) $ processSchema rs
574+ :: HasAll (CheckEnv Schema) xs
576+ -> Trace OpenApi Schema
577+ -> ProdCons (ForeachType (JsonFormula OpenApi), T.TracePrefixTree SubtreeCheckIssue OpenApi)
578+ -> CompatFormula Schema ()
579+checkFormulas env tr (ProdCons (fp, ep) (fc, ec)) =
580+ case T.toList ep ++ T.toList ec of
581+ issues@(_:_) -> F.for_ issues $ \(AnItem t (SubtreeCheckIssue e)) -> issueAtTrace t e
583+ -- We have the following isomorphisms:
584+ -- (A ⊂ X ∪ Y) = (A ⊂ X) \/ (A ⊂ Y)
585+ -- (A ⊂ X ∩ Y) = (A ⊂ X) /\ (A ⊂ Y)
587+ -- (X ∪ Y ⊂ B) = (X ⊂ B) /\ (Y ⊂ B)
589+ -- The remaining cases are, notably, not isomorphisms:
591+ -- 2) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
593+ -- Therefore we have the isomorphisms:
594+ -- (⋃_i ⋂_j A[i,j]) ⊂ (⋃_k ⋂_l B[k,l])
595+ -- = \/_k /\_l /\_i (⋂_j A[i,j]) ⊂ B[k,l]
596+ -- = /\_i \/_k /\_l (⋂_j A[i,j]) ⊂ B[k,l]
597+ -- with the caveat that the the set over which k ranges is nonempty.
598+ -- This is because 1) is not an isomorphism.
599+ -- Our disjunction loses information, so it makes sense to nest it as
600+ -- deeply as possible, hence we choose the latter representation.
602+ -- We delegate the verification of (⋂_j A[j]) ⊂ B to a separate heuristic
603+ -- function, with the understanding that \/_j A[j] ⊂ B is a sufficient,
604+ -- but not necessary condition (because of 2) and 3)).
606+ -- If k ranges over an empty set, we have the isomorphism:
607+ -- (⋃_i ⋂_j A[i,j]) ⊂ ∅ = /\_i (⋂_j A[i,j]) ⊂ ∅
608+ -- where we again delegate (⋂_j A[j]) ⊂ ∅ to a heuristic, though here the
609+ -- shortcut of \/_j A[j] ⊂ ∅ hardly helps.
611+ case (ty fp, ty fc) of
612+ (DNF pss, BottomFormula) -> F.for_ pss $ \(Conjunct ps) -> checkContradiction ps
613+ (DNF pss, SingleConjunct cs) -> F.for_ pss $ \(Conjunct ps) -> do
614+ F.for_ cs $ checkImplication env ps -- avoid disjuntion if there's only one conjunct
615+ (DNF pss, DNF css) -> F.for_ pss $ \(Conjunct ps) -> do
616+ anyOfM tr (SubtreeCheckIssue $ NoMatchingCondition $ SomeCondition . getTraced <$> ps)
617+ [F.for_ cs $ checkImplication env ps | Conjunct cs <- S.toList css]
619+checkContradiction :: [Traced OpenApi (Condition t)] -> CompatFormula s ()
620+checkContradiction = undefined -- TODO
623+ :: (HasAll (CheckEnv Schema) xs, Typeable t)
625+ -> [Traced OpenApi (Condition t)]
626+ -> Traced OpenApi (Condition t)
627+ -> CompatFormula s ()
628+checkImplication env prods (Traced t cons) = case findExactly prods of
630+ | all (satisfiesTyped e) (getTraced <$> prods) ->
631+ if satisfiesTyped e cons then pure ()
632+ else issueAtTrace t (EnumDoesntSatisfy e)
633+ | otherwise -> pure () -- vacuously true
634+ Nothing -> case cons of
635+ -- the above code didn't catch it, so there's no Exactly condition on the lhs
636+ Exactly e -> issueAtTrace t (NoMatchingEnum e)
637+ Maximum m -> case findRelevant min (\case Maximum m' -> Just m'; _ -> Nothing) prods of
638+ Just m' -> if m' <= m then pure ()
639+ else issueAtTrace t (MatchingMaximumWeak m m')
640+ Nothing -> issueAtTrace t (NoMatchingMaximum m)
641+ Minimum m -> case findRelevant max (\case Minimum m' -> Just m'; _ -> Nothing) prods of
642+ Just m' -> if m' >= m then pure ()
643+ else issueAtTrace t (MatchingMinimumWeak (coerce m) (coerce m'))
644+ Nothing -> issueAtTrace t (NoMatchingMinimum (coerce m))
645+ MultipleOf m -> case findRelevant lcmScientific (\case MultipleOf m' -> Just m'; _ -> Nothing) prods of
646+ Just m' -> if lcmScientific m m' == m' then pure ()
647+ else issueAtTrace t (MatchingMultipleOfWeak m m')
648+ Nothing -> issueAtTrace t (NoMatchingMultipleOf m)
649+ NumberFormat f -> if any (\case NumberFormat f' -> f == f'; _ -> False) $ getTraced <$> prods
650+ then pure () else issueAtTrace t (NoMatchingFormat f)
651+ MaxLength m -> case findRelevant min (\case MaxLength m' -> Just m'; _ -> Nothing) prods of
652+ Just m' -> if m' <= m then pure ()
653+ else issueAtTrace t (MatchingMaxLengthWeak m m')
654+ Nothing -> issueAtTrace t (NoMatchingMaxLength m)
655+ MinLength m -> case findRelevant max (\case MinLength m' -> Just m'; _ -> Nothing) prods of
656+ Just m' -> if m' >= m then pure ()
657+ else issueAtTrace t (MatchingMinLengthWeak m m')
658+ Nothing -> issueAtTrace t (NoMatchingMinLength m)
659+ Pattern p -> if any (\case Pattern p' -> p == p'; _ -> False) $ getTraced <$> prods
660+ then pure () else issueAtTrace t (NoMatchingPattern p)
661+ StringFormat f -> if any (\case StringFormat f' -> f == f'; _ -> False) $ getTraced <$> prods
662+ then pure () else issueAtTrace t (NoMatchingFormat f)
663+ Items _ (Traced t' cons') -> case findRelevant (<>) (\case Items _ rs -> Just (rs NE.:| []); _ -> Nothing) prods of
664+ Just (rs NE.:| []) -> localTrace' (ProdCons (getTrace rs) t') $ checkCompatibility env $ ProdCons (getTraced rs) cons'
666+ let sch = Inline mempty { _schemaAllOf = Just . NE.toList $ getTraced <$> rs }
667+ localTrace' (pure t' {- TODO: what? -}) $ checkCompatibility env $ ProdCons sch cons'
668+ Nothing -> issueAtTrace t NoMatchingItems
669+ MaxItems m -> case findRelevant min (\case MaxItems m' -> Just m'; _ -> Nothing) prods of
670+ Just m' -> if m' <= m then pure ()
671+ else issueAtTrace t (MatchingMaxItemsWeak m m')
672+ Nothing -> issueAtTrace t (NoMatchingMaxItems m)
673+ MinItems m -> case findRelevant max (\case MinItems m' -> Just m'; _ -> Nothing) prods of
674+ Just m' -> if m' >= m then pure ()
675+ else issueAtTrace t (MatchingMinItemsWeak m m')
676+ Nothing -> issueAtTrace t (NoMatchingMinItems m)
677+ UniqueItems -> if any ((== UniqueItems) . getTraced) prods then pure ()
678+ else issueAtTrace t NoMatchingUniqueItems
679+ Properties props _ madd -> case findRelevant (<>) (\case Properties props' _ madd' -> Just $ (props', madd') NE.:| []; _ -> Nothing) prods of
680+ Just ((props', madd') NE.:| []) -> do
681+ F.for_ (S.fromList $ M.keys props <> M.keys props') $ \k -> do
683+ go sch' sch = let schs = ProdCons sch' sch
684+ in localTrace' (getTrace <$> schs) $ checkCompatibility env $ getTraced <$> schs
685+ case (M.lookup k props', madd', M.lookup k props, madd) of
686+ (Nothing, Nothing, _, _) -> pure () -- vacuously
687+ (_, _, Nothing, Nothing) -> issueAtTrace t (UnexpectedProperty k)
688+ (Just p', _, Just p, _) -> go (propRefSchema p') (propRefSchema p)
689+ (Nothing, Just add', Just p, _) -> go add' (propRefSchema p)
690+ (Just p', _, Nothing, Just add) -> go (propRefSchema p') add
691+ (Nothing, Just _, Nothing, Just _) -> pure ()
692+ case (maybe False propRequired $ M.lookup k props', maybe False propRequired $ M.lookup k props) of
693+ (False, True) -> issueAtTrace t (PropertyNowRequired k)
696+ case (madd', madd) of
697+ (Nothing, _) -> pure () -- vacuously
698+ (_, Nothing) -> issueAtTrace t NoAdditionalProperties
699+ (Just add', Just add) -> let schs = ProdCons add' add
700+ in localTrace' (getTrace <$> schs) $ checkCompatibility env $ getTraced <$> schs
702+ Nothing -> issueAtTrace t NoMatchingProperties
703+ MaxProperties m -> case findRelevant min (\case MaxProperties m' -> Just m'; _ -> Nothing) prods of
704+ Just m' -> if m' <= m then pure ()
705+ else issueAtTrace t (MatchingMaxPropertiesWeak m m')
706+ Nothing -> issueAtTrace t (NoMatchingMaxProperties m)
707+ MinProperties m -> case findRelevant max (\case MinProperties m' -> Just m'; _ -> Nothing) prods of
708+ Just m' -> if m' >= m then pure ()
709+ else issueAtTrace t (MatchingMinPropertiesWeak m m')
710+ Nothing -> issueAtTrace t (NoMatchingMinProperties m)
712+ findExactly (Traced _ (Exactly x):_) = Just x
713+ findExactly (_:xs) = findExactly xs
714+ findExactly [] = Nothing
715+ findRelevant combine extract
716+ = fmap (foldr1 combine) . NE.nonEmpty . mapMaybe (extract . getTraced)
717+ lcmScientific (toRational -> a) (toRational -> b)
718+ = fromRational $ lcm (numerator a) (numerator b) % gcd (denominator a) (denominator b)
720+instance Typeable t => Subtree (Condition t) where
721+ data CheckIssue (Condition t)
722+ = EnumDoesntSatisfy (TypedValue t)
723+ | NoMatchingEnum (TypedValue t)
724+ | NoMatchingMaximum (Bound Scientific)
725+ | MatchingMaximumWeak (Bound Scientific) (Bound Scientific)
726+ | NoMatchingMinimum (Bound Scientific)
727+ | MatchingMinimumWeak (Bound Scientific) (Bound Scientific)
728+ | NoMatchingMultipleOf Scientific
729+ | MatchingMultipleOfWeak Scientific Scientific
730+ | NoMatchingFormat Format
731+ | NoMatchingMaxLength Integer
732+ | MatchingMaxLengthWeak Integer Integer
733+ | NoMatchingMinLength Integer
734+ | MatchingMinLengthWeak Integer Integer
735+ | NoMatchingPattern Pattern
737+ | NoMatchingMaxItems Integer
738+ | MatchingMaxItemsWeak Integer Integer
739+ | NoMatchingMinItems Integer
740+ | MatchingMinItemsWeak Integer Integer
741+ | NoMatchingUniqueItems
742+ | NoMatchingProperties
743+ | UnexpectedProperty Text
744+ | PropertyNowRequired Text
745+ | NoAdditionalProperties
746+ | NoMatchingMaxProperties Integer
747+ | MatchingMaxPropertiesWeak Integer Integer
748+ | NoMatchingMinProperties Integer
749+ | MatchingMinPropertiesWeak Integer Integer
750+ deriving stock (Eq, Ord, Show)
751+ type CheckEnv (Condition t) = CheckEnv Schema
752+ normalizeTrace = undefined
753+ checkCompatibility env conds = withTrace $ \traces -> do
754+ case Traced <$> traces <*> conds of
755+ ProdCons prod cons -> checkImplication env [prod] cons
757+instance Subtree Schema where
758+ data CheckIssue Schema
760+ | InvalidSchema Text
761+ | NoMatchingCondition [SomeCondition]
762+ deriving stock (Eq, Ord, Show)
763+ type CheckEnv Schema = '[Definitions Schema]
764+ normalizeTrace = undefined
765+ checkCompatibility env schs = withTrace $ \traces -> do
767+ checkFormulas env (producer traces) $ schemaToFormula defs <$> (Traced <$> traces <*> schs)
769+instance Subtree (Referenced Schema) where
770+ data CheckIssue (Referenced Schema)
771+ deriving stock (Eq, Ord, Show)
772+ type CheckEnv (Referenced Schema) = CheckEnv Schema
773+ normalizeTrace = undefined
774+ checkCompatibility env refs = withTrace $ \traces -> do
777+ schs = dereference defs <$> refs
778+ schs' = retrace <$> traces <*> schs
779+ localTrace (getTrace <$> schs) $ do
780+ checkFormulas env (producer $ getTrace <$> schs') $ schemaToFormula defs <$> schs'