@@ -0,0 +1,780 @@
1+{-# OPTIONS_GHC -fno-warn-orphans #-}
2+module OpenAPI.Checker.Validate.Schema
3+ ( JsonType (..)
4+ , ForeachType (..)
5+ , foldType
6+ , forType_
7+ , TypedValue (..)
8+ , untypeValue
9+ , Bound (..)
10+ , schemaToFormula
11+ , foldLattice
12+ )
13+ where
14+
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
20+import Data.Coerce
21+import qualified Data.Foldable as F
22+import qualified Data.HashMap.Strict as HM
23+import qualified Data.HashMap.Strict.InsOrd as IOHM
24+import Data.HList
25+import Data.Int
26+import Data.Kind
27+import qualified Data.List.NonEmpty as NE
28+import qualified Data.Map as M
29+import Data.Maybe
30+import Data.OpenApi
31+import Data.Ord
32+import Data.Ratio
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)
37+import Data.Typeable
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
43+
44+-- | Type of a JSON value
45+data JsonType
46+ = Null
47+ | Boolean
48+ | Number
49+ | String
50+ | Array
51+ | Object
52+ deriving (Eq, Show)
53+
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
62+
63+deriving stock instance Eq (TypedValue t)
64+deriving stock instance Ord (TypedValue t)
65+deriving stock instance Show (TypedValue t)
66+
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
74+
75+data Bound a = Exclusive !a | Inclusive !a
76+ deriving (Eq, Show)
77+
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
84+
85+data Property = Property
86+ { propRequired :: Bool
87+ , propFormula :: ForeachType (JsonFormula OpenApi)
88+ , propRefSchema :: Traced OpenApi (Referenced Schema)
89+ }
90+ deriving stock (Eq, Ord, Show)
91+
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
104+ Items
105+ :: !(ForeachType (JsonFormula OpenApi))
106+ -> !(Traced OpenApi (Referenced Schema))
107+ -> Condition 'Array
108+ MaxItems :: !Integer -> Condition 'Array
109+ MinItems :: !Integer -> Condition 'Array
110+ UniqueItems :: Condition 'Array
111+ Properties
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
120+
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
142+
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
151+
152+deriving stock instance Eq (Condition t)
153+deriving stock instance Ord (Condition t)
154+deriving stock instance Show (Condition t)
155+
156+data SomeCondition where
157+ SomeCondition :: Typeable t => Condition t -> SomeCondition
158+
159+instance Eq SomeCondition where
160+ SomeCondition x == SomeCondition y = case cast x of
161+ Just x' -> x' == y
162+ Nothing -> False
163+
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)
168+
169+deriving stock instance Show SomeCondition
170+
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)
177+
178+disjAdd
179+ :: JsonFormula r t
180+ -> M.Map (Condition t) (Trace r (Condition t))
181+ -> JsonFormula r t
182+disjAdd (DNF yss) xs
183+ | any (`isMapSubsetOf` xs) yss = DNF yss
184+ | otherwise = DNF $ S.insert xs $ S.filter (not . isMapSubsetOf xs) yss
185+ where
186+ isMapSubsetOf a b = M.keysSet a `S.isSubsetOf` M.keysSet b
187+
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)
192+
193+pattern BottomFormula :: JsonFormula r t
194+pattern BottomFormula <- DNF (S.null -> True)
195+ where BottomFormula = DNF S.empty
196+
197+isSingleton :: S.Set a -> Maybe a
198+isSingleton s
199+ | S.size s == 1 = S.lookupMin s
200+ | otherwise = Nothing
201+
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 #-}
206+
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
210+
211+pattern TopFormula :: JsonFormula r t
212+pattern TopFormula <- DNF (isSingleton -> Just (M.null -> True))
213+ where TopFormula = DNF $ S.singleton M.empty
214+
215+instance BoundedJoinSemiLattice (JsonFormula r t) where
216+ bottom = BottomFormula
217+
218+instance BoundedMeetSemiLattice (JsonFormula r t) where
219+ top = TopFormula
220+
221+singletonFormula :: Trace r (Condition t) -> Condition t -> JsonFormula r t
222+singletonFormula t x = SingleConjunct [Traced t x]
223+
224+foldLattice
225+ :: BoundedLattice l
226+ => (Traced r (Condition t) -> l)
227+ -> JsonFormula r t
228+ -> 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
231+
232+satisfiesFormula :: TypedValue t -> JsonFormula r t -> Bool
233+satisfiesFormula val = foldLattice (satisfiesTyped val . getTraced)
234+
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
242+ }
243+
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
252+
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)
256+
257+foldType
258+ :: Monoid m
259+ => (forall x. Typeable x => (ForeachType f -> f x) -> m)
260+ -> m
261+foldType k =
262+ k forNull <>
263+ k forBoolean <>
264+ k forNumber <>
265+ k forString <>
266+ k forArray <>
267+ k forObject
268+
269+forType_
270+ :: Applicative m
271+ => (forall x. Typeable x => (ForeachType f -> f x) -> m ())
272+ -> m ()
273+forType_ k = do
274+ k forNull
275+ k forBoolean
276+ k forNumber
277+ k forString
278+ k forArray
279+ k forObject
280+ pure ()
281+
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
290+ }
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
298+ }
299+
300+instance (forall x. BoundedJoinSemiLattice (f x))
301+ => BoundedJoinSemiLattice (ForeachType f) where
302+ bottom = ForeachType
303+ { forNull = bottom
304+ , forBoolean = bottom
305+ , forNumber = bottom
306+ , forString = bottom
307+ , forArray = bottom
308+ , forObject = bottom
309+ }
310+
311+instance (forall x. BoundedMeetSemiLattice (f x))
312+ => BoundedMeetSemiLattice (ForeachType f) where
313+ top = ForeachType
314+ { forNull = top
315+ , forBoolean = top
316+ , forNumber = top
317+ , forString = top
318+ , forArray = top
319+ , forObject = top
320+ }
321+
322+instance Typeable t => Steppable Schema (Condition t) where
323+ data Step Schema (Condition t)
324+ = EnumField
325+ | MaximumFields -- maximum & exclusiveMaximum
326+ | MinimumFields -- minimum & exclusiveMinimum
327+ | MultipleOfField
328+ | FormatField
329+ | MaxLengthField
330+ | MinLengthField
331+ | PatternField
332+ | ItemsField
333+ | MaxItemsField
334+ | MinItemsField
335+ | UniqueItemsField
336+ | PropertiesFields -- properties, additionalProperties & required
337+ | MaxPropertiesField
338+ | MinPropertiesField
339+ | NullableField
340+ | IntegerType -- type=integer
341+ deriving (Eq, Ord, Show)
342+
343+instance Steppable Schema (Referenced Schema) where
344+ data Step Schema (Referenced Schema)
345+ = AllOfStep Int
346+ | OneOfStep Int
347+ | AnyOfStep Int
348+ | ItemsStep
349+ | AdditionalPropertiesStep
350+ | PropertiesStep Text
351+ deriving (Eq, Ord, Show)
352+
353+type ProcessM = ReaderT (Definitions Schema) (Writer (T.TracePrefixTree SubtreeCheckIssue OpenApi))
354+
355+warn :: Subtree t => Trace OpenApi t -> CheckIssue t -> ProcessM ()
356+warn t x = tell $ T.singleton $ AnItem t $ SubtreeCheckIssue x
357+
358+processRefSchema
359+ :: Traced OpenApi (Referenced Schema)
360+ -> ProcessM (ForeachType (JsonFormula OpenApi))
361+processRefSchema x = do
362+ defs <- ask
363+ processSchema $ dereferenceTraced defs x
364+
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.
368+processSchema
369+ :: Traced OpenApi Schema
370+ -> ProcessM (ForeachType (JsonFormula OpenApi))
371+processSchema (Traced t Schema{..}) = do
372+
373+ allClauses <- case _schemaAllOf of
374+ Nothing -> pure []
375+ Just [] -> [] <$ warn t (InvalidSchema "no items in allOf")
376+ Just xs -> sequence
377+ [ processRefSchema (Traced (t `Snoc` AllOfStep i) rs)
378+ | (i, rs) <- zip [0..] xs ]
379+
380+ anyClause <- case _schemaAnyOf of
381+ Nothing -> pure top
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 ]
386+
387+ oneClause <- case _schemaOneOf of
388+ Nothing -> pure top
389+ Just [] -> bottom <$ warn t (InvalidSchema "no items in oneOf")
390+ Just xs -> do
391+ checkOneOfDisjoint xs >>= \case
392+ True -> pure ()
393+ False -> warn t (NotSupported "Could not determine that oneOf branches are disjoint")
394+ joins <$> sequence
395+ [ processRefSchema (Traced (t `Snoc` OneOfStep i) rs)
396+ | (i, rs) <- zip [0..] xs ]
397+
398+ case _schemaNot of
399+ Nothing -> pure ()
400+ Just _ -> warn t (NotSupported "not clause is unsupported")
401+
402+ let
403+ typeClause = case _schemaType of
404+ Nothing -> top
405+ Just OpenApiNull -> bottom
406+ { forNull = top }
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
414+ { forString = top }
415+ Just OpenApiArray -> bottom
416+ { forArray = top }
417+ Just OpenApiObject -> bottom
418+ { forObject = top }
419+
420+ let
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
434+ Nothing -> pure top
435+ Just [] -> bottom <$ warn t (InvalidSchema "no items in enum")
436+ Just xs -> pure $ joins (valueEnum <$> xs)
437+
438+ let
439+ maximumClause = case _schemaMaximum of
440+ Nothing -> top
441+ Just n -> top
442+ { forNumber = singletonFormula (t `Snoc` MaximumFields) $ Maximum $
443+ case _schemaExclusiveMaximum of
444+ Just True -> Exclusive n
445+ _ -> Inclusive n }
446+
447+ minimumClause = case _schemaMinimum of
448+ Nothing -> top
449+ Just n -> top
450+ { forNumber = singletonFormula (t `Snoc` MinimumFields) $ Minimum $ Down $
451+ case _schemaExclusiveMinimum of
452+ Just True -> Exclusive $ Down n
453+ _ -> Inclusive $ Down n }
454+
455+ multipleOfClause = case _schemaMultipleOf of
456+ Nothing -> top
457+ Just n -> top
458+ { forNumber = singletonFormula (t `Snoc` MultipleOfField) $ MultipleOf n }
459+
460+ formatClause <- case _schemaFormat of
461+ Nothing -> pure top
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)
467+
468+ let
469+ maxLengthClause = case _schemaMaxLength of
470+ Nothing -> top
471+ Just n -> top
472+ { forString = singletonFormula (t `Snoc` MaxLengthField) $ MaxLength n }
473+
474+ minLengthClause = case _schemaMinLength of
475+ Nothing -> top
476+ Just n -> top
477+ { forString = singletonFormula (t `Snoc` MinLengthField) $ MinLength n }
478+
479+ patternClause = case _schemaPattern of
480+ Nothing -> top
481+ Just p -> top
482+ { forString = singletonFormula (t `Snoc` PatternField) $ Pattern p }
483+
484+ itemsClause <- case _schemaItems of
485+ Nothing -> pure top
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")
491+
492+ let
493+ maxItemsClause = case _schemaMaxItems of
494+ Nothing -> top
495+ Just n -> top
496+ { forArray = singletonFormula (t `Snoc` MaxItemsField) $ MaxItems n }
497+
498+ minItemsClause = case _schemaMinItems of
499+ Nothing -> top
500+ Just n -> top
501+ { forArray = singletonFormula (t `Snoc` MinItemsField) $ MinItems n }
502+
503+ uniqueItemsClause = case _schemaUniqueItems of
504+ Just True -> top
505+ { forArray = singletonFormula (t `Snoc` UniqueItemsField) UniqueItems }
506+ _ -> top
507+
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
516+ Just rs -> do
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)
524+ let
525+ allBottom f = getAll $ foldType $ \ty -> case ty f of
526+ BottomFormula -> All True
527+ _ -> All False
528+ allTop f = getAll $ foldType $ \ty -> case ty f of
529+ TopFormula -> All True
530+ _ -> All False
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
533+ propertiesClause
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
538+ | otherwise
539+ = top
540+ { forObject = singletonFormula (t `Snoc` PropertiesFields) $ Properties propMap addProps addPropSchema }
541+
542+ maxPropertiesClause = case _schemaMaxProperties of
543+ Nothing -> top
544+ Just n -> top
545+ { forObject = singletonFormula (t `Snoc` MaxPropertiesField) $ MaxProperties n }
546+
547+ minPropertiesClause = case _schemaMinProperties of
548+ Nothing -> top
549+ Just n -> top
550+ { forObject = singletonFormula (t `Snoc` MinPropertiesField) $ MinProperties n }
551+
552+ nullableClause
553+ | Just True <- _schemaNullable = bottom
554+ { forNull = singletonFormula (t `Snoc` NullableField) $ Exactly TNull }
555+ | otherwise = bottom
556+
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 -}
563+
564+checkOneOfDisjoint :: [Referenced Schema] -> ProcessM Bool
565+checkOneOfDisjoint = const $ pure True -- TODO
566+
567+schemaToFormula
568+ :: Definitions Schema
569+ -> Traced OpenApi Schema
570+ -> (ForeachType (JsonFormula OpenApi), T.TracePrefixTree SubtreeCheckIssue OpenApi)
571+schemaToFormula defs rs = runWriter . (`runReaderT` defs) $ processSchema rs
572+
573+checkFormulas
574+ :: HasAll (CheckEnv Schema) xs
575+ => HList 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
582+ [] -> do
583+ -- We have the following isomorphisms:
584+ -- (A ⊂ X ∪ Y) = (A ⊂ X) \/ (A ⊂ Y)
585+ -- (A ⊂ X ∩ Y) = (A ⊂ X) /\ (A ⊂ Y)
586+ -- (A ⊂ ⊤) = 1
587+ -- (X ∪ Y ⊂ B) = (X ⊂ B) /\ (Y ⊂ B)
588+ -- (∅ ⊂ B) = 1
589+ -- The remaining cases are, notably, not isomorphisms:
590+ -- 1) (A ⊂ ∅) <= 0
591+ -- 2) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
592+ -- 3) (⊤ ⊂ B) <= 0
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.
601+ --
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)).
605+ --
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.
610+ forType_ $ \ty ->
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]
618+
619+checkContradiction :: [Traced OpenApi (Condition t)] -> CompatFormula s ()
620+checkContradiction = undefined -- TODO
621+
622+checkImplication
623+ :: (HasAll (CheckEnv Schema) xs, Typeable t)
624+ => HList xs
625+ -> [Traced OpenApi (Condition t)]
626+ -> Traced OpenApi (Condition t)
627+ -> CompatFormula s ()
628+checkImplication env prods (Traced t cons) = case findExactly prods of
629+ Just e
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'
665+ Just rs -> do
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
682+ let
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)
694+ _ -> pure ()
695+ pure ()
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
701+ pure ()
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)
711+ where
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)
719+
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
736+ | NoMatchingItems
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
756+
757+instance Subtree Schema where
758+ data CheckIssue Schema
759+ = NotSupported Text
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
766+ let defs = getH env
767+ checkFormulas env (producer traces) $ schemaToFormula defs <$> (Traced <$> traces <*> schs)
768+
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
775+ let
776+ defs = getH env
777+ schs = dereference defs <$> refs
778+ schs' = retrace <$> traces <*> schs
779+ localTrace (getTrace <$> schs) $ do
780+ checkFormulas env (producer $ getTrace <$> schs') $ schemaToFormula defs <$> schs'