@@ -16,16 +16,20 @@ module OpenAPI.Checker.Validate.Schema
18import Algebra.Lattice
18import Algebra.Lattice
19+import Algebra.Lattice.Lifted
19import Control.Applicative
20import Control.Applicative
20import Control.Arrow
21import Control.Arrow
21import Control.Comonad.Env hiding (env)
22import Control.Comonad.Env hiding (env)
22import Control.Monad.Reader hiding (ask)
23import Control.Monad.Reader hiding (ask)
23import qualified Control.Monad.Reader as R
24import qualified Control.Monad.Reader as R
24import Control.Monad.State
25import Control.Monad.State
26+import qualified Control.Monad.Trans.Reader as R (liftCatch)
27+import qualified Control.Monad.Trans.Writer as W (liftCatch)
25import Control.Monad.Writer
28import Control.Monad.Writer
26import qualified Data.Aeson as A
29import qualified Data.Aeson as A
27import qualified Data.ByteString.Lazy as BSL
30import qualified Data.ByteString.Lazy as BSL
28import Data.Coerce
31import Data.Coerce
29import qualified Data.Foldable as F
33import qualified Data.Foldable as F
30import Data.Functor
34import Data.Functor
31import Data.Functor.Identity
35import Data.Functor.Identity
@@ -34,6 +38,8 @@ import qualified Data.HashMap.Strict as HM
34import qualified Data.HashMap.Strict.InsOrd as IOHM
38import qualified Data.HashMap.Strict.InsOrd as IOHM
35import Data.Int
39import Data.Int
36import Data.Kind
40import Data.Kind
41+import Data.List (sortBy)
42+import qualified Data.List as L
37import qualified Data.List.NonEmpty as NE
43import qualified Data.List.NonEmpty as NE
38import qualified Data.Map as M
44import qualified Data.Map as M
39import Data.Maybe
45import Data.Maybe
@@ -167,7 +173,7 @@ showCondition = \case
167 showForEachJsonFormula i =
173 showForEachJsonFormula i =
168 bulletList $
174 bulletList $
170− (\t f -> case f i of
176+ (\t f -> case getJsonFormula $ f i of
171 BottomFormula -> mempty
177 BottomFormula -> mempty
172 (DNF conds') ->
178 (DNF conds') ->
173 let conds = S.toList <$> S.toList conds'
179 let conds = S.toList <$> S.toList conds'
@@ -243,28 +249,25 @@ instance Ord SomeCondition where
244deriving stock instance Show SomeCondition
250deriving stock instance Show SomeCondition
246−-- | A boolean formula (without "not") of 'Condition's. Represented as a
252+-- | A boolean formula (without "not") represented as a Disjunctive Normal Form:
247−-- Disjunctive Normal Form: the formula is a disjunction of a set of conjuncts,
253+-- the formula is a disjunction of a set of conjuncts, each of which is a
248−-- each of which is a conjunction of a set of 'Condition's.
254+-- conjunction of a set of some elementary formulas.
249−newtype JsonFormula t
255+newtype DNF a
250− = DNF (S.Set (S.Set (Condition t)))
256+ = DNF (S.Set (S.Set a))
251 deriving stock (Eq, Ord, Show)
257 deriving stock (Eq, Ord, Show)
253−disjAdd
259+disjAdd :: Ord a => DNF a -> S.Set a -> DNF a
255− -> S.Set (Condition t)
257disjAdd (DNF yss) xs
260disjAdd (DNF yss) xs
258 | any (`S.isSubsetOf` xs) yss = DNF yss
261 | any (`S.isSubsetOf` xs) yss = DNF yss
259 | otherwise = DNF $ S.insert xs $ S.filter (not . S.isSubsetOf xs) yss
262 | otherwise = DNF $ S.insert xs $ S.filter (not . S.isSubsetOf xs) yss
261−instance Lattice (JsonFormula t) where
264+instance Ord a => Lattice (DNF a) where
262 xss \/ DNF yss = S.foldl' disjAdd xss yss
265 xss \/ DNF yss = S.foldl' disjAdd xss yss
263 DNF xss /\ DNF yss =
266 DNF xss /\ DNF yss =
264 F.foldl' disjAdd bottom $
267 F.foldl' disjAdd bottom $
265 liftA2 S.union (S.toList xss) (S.toList yss)
268 liftA2 S.union (S.toList xss) (S.toList yss)
267−pattern BottomFormula :: JsonFormula t
270+pattern BottomFormula :: DNF a
268pattern BottomFormula <-
271pattern BottomFormula <-
269 DNF (S.null -> True)
272 DNF (S.null -> True)
@@ -275,7 +278,7 @@ isSingleton s
275 | S.size s == 1 = S.lookupMin s
278 | S.size s == 1 = S.lookupMin s
276 | otherwise = Nothing
279 | otherwise = Nothing
278−pattern Conjunct :: [Condition t] -> S.Set (Condition t)
281+pattern Conjunct :: Ord a => [a] -> S.Set a
279pattern Conjunct xs <-
282pattern Conjunct xs <-
280 (S.toList -> xs)
283 (S.toList -> xs)
@@ -283,28 +286,28 @@ pattern Conjunct xs <-
284{-# COMPLETE Conjunct #-}
287{-# COMPLETE Conjunct #-}
286−pattern SingleConjunct :: [Condition t] -> JsonFormula t
289+pattern SingleConjunct :: Ord a => [a] -> DNF a
287pattern SingleConjunct xs <-
290pattern SingleConjunct xs <-
288 DNF (isSingleton -> Just (Conjunct xs))
291 DNF (isSingleton -> Just (Conjunct xs))
290 SingleConjunct xs = DNF $ S.singleton $ Conjunct xs
293 SingleConjunct xs = DNF $ S.singleton $ Conjunct xs
292−pattern TopFormula :: JsonFormula t
295+pattern TopFormula :: DNF a
293pattern TopFormula <-
296pattern TopFormula <-
294 DNF (isSingleton -> Just (S.null -> True))
297 DNF (isSingleton -> Just (S.null -> True))
296 TopFormula = DNF $ S.singleton S.empty
299 TopFormula = DNF $ S.singleton S.empty
298−instance BoundedJoinSemiLattice (JsonFormula t) where
301+instance Ord a => BoundedJoinSemiLattice (DNF a) where
299 bottom = BottomFormula
302 bottom = BottomFormula
301−instance BoundedMeetSemiLattice (JsonFormula t) where
304+instance Ord a => BoundedMeetSemiLattice (DNF a) where
302 top = TopFormula
305 top = TopFormula
304foldLattice
307foldLattice
305 :: BoundedLattice l
308 :: BoundedLattice l
306− => (Condition t -> l)
309+ => (a -> l)
307− -> JsonFormula t
310+ -> DNF a
309foldLattice f (DNF xss) =
312foldLattice f (DNF xss) =
@@ -313,8 +316,12 @@ foldLattice f (DNF xss) =
319+newtype JsonFormula t = JsonFormula {getJsonFormula :: DNF (Condition t)}
320+ deriving stock (Eq, Ord, Show)
321+ deriving newtype (Lattice, BoundedJoinSemiLattice, BoundedMeetSemiLattice)
316satisfiesFormula :: TypedValue t -> JsonFormula t -> Bool
323satisfiesFormula :: TypedValue t -> JsonFormula t -> Bool
317−satisfiesFormula val = foldLattice (satisfiesTyped val)
324+satisfiesFormula val = foldLattice (satisfiesTyped val) . getJsonFormula
319data ForeachType (f :: JsonType -> Type) = ForeachType
326data ForeachType (f :: JsonType -> Type) = ForeachType
320 { forNull :: f 'Null
327 { forNull :: f 'Null
@@ -424,6 +431,14 @@ instance Steppable Schema (Referenced Schema) where
424 | NotStep
431 | NotStep
425 deriving stock (Eq, Ord, Show)
432 deriving stock (Eq, Ord, Show)
434+instance Steppable (Referenced Schema) (Referenced Schema) where
435+ data Step (Referenced Schema) (Referenced Schema)
436+ = -- | Invariant (for better memoization only): the "tail" of the trace is
437+ -- the "least" of the traces of the conjuncted schemata
438+ ConjunctedWith (NE.NonEmpty (Trace (Referenced Schema)))
439+ | Partitioned PartitionLocation PartitionChoice
440+ deriving stock (Eq, Ord, Show)
427instance Steppable Schema (Definitions (Referenced Schema)) where
442instance Steppable Schema (Definitions (Referenced Schema)) where
428 data Step Schema (Definitions (Referenced Schema)) = PropertiesStep
443 data Step Schema (Definitions (Referenced Schema)) = PropertiesStep
429 deriving stock (Eq, Ord, Show)
444 deriving stock (Eq, Ord, Show)
@@ -535,7 +550,7 @@ processSchema
535 -> m (ForeachType JsonFormula)
550 -> m (ForeachType JsonFormula)
536processSchema sch@(extract -> Schema {..}) = do
551processSchema sch@(extract -> Schema {..}) = do
537 let singletonFormula :: Condition t -> JsonFormula t
552 let singletonFormula :: Condition t -> JsonFormula t
538− singletonFormula f = SingleConjunct [f]
553+ singletonFormula f = JsonFormula $ SingleConjunct [f]
540 allClauses <- case tracedAllOf sch of
555 allClauses <- case tracedAllOf sch of
541 Nothing -> pure []
556 Nothing -> pure []
@@ -730,11 +745,11 @@ processSchema sch@(extract -> Schema {..}) = do
730 pure (addProps, fromMaybe fakeSchema addPropSchema)
745 pure (addProps, fromMaybe fakeSchema addPropSchema)
731 pure (k, Property (k `elem` _schemaRequired) f psch)
746 pure (k, Property (k `elem` _schemaRequired) f psch)
732 let allBottom f = getAll $
747 let allBottom f = getAll $
733− foldType $ \_ ty -> case ty f of
748+ foldType $ \_ ty -> case getJsonFormula $ ty f of
734 BottomFormula -> All True
749 BottomFormula -> All True
735 _ -> All False
750 _ -> All False
736 allTop f = getAll $
751 allTop f = getAll $
737− foldType $ \_ ty -> case ty f of
752+ foldType $ \_ ty -> case getJsonFormula $ ty f of
738 TopFormula -> All True
753 TopFormula -> All True
739 _ -> All False
754 _ -> All False
740 -- remove optional fields whose schemata match that of additional props
755 -- remove optional fields whose schemata match that of additional props
@@ -810,9 +825,10 @@ checkFormulas
810 :: (ReassembleHList xs (CheckEnv (Referenced Schema)))
825 :: (ReassembleHList xs (CheckEnv (Referenced Schema)))
811 => HList xs
826 => HList xs
812 -> Behavior 'SchemaLevel
827 -> Behavior 'SchemaLevel
828+ -> ProdCons (Traced (Definitions Schema))
813 -> ProdCons (ForeachType JsonFormula, P.PathsPrefixTree Behave AnIssue 'SchemaLevel)
829 -> ProdCons (ForeachType JsonFormula, P.PathsPrefixTree Behave AnIssue 'SchemaLevel)
814 -> SemanticCompatFormula ()
830 -> SemanticCompatFormula ()
815−checkFormulas env beh (ProdCons (fp, ep) (fc, ec)) =
831+checkFormulas env beh defs (ProdCons (fp, ep) (fc, ec)) =
816 case P.toList ep ++ P.toList ec of
832 case P.toList ep ++ P.toList ec of
817 issues@(_ : _) -> F.for_ issues $ embedFormula beh . anItem
833 issues@(_ : _) -> F.for_ issues $ embedFormula beh . anItem
@@ -826,23 +842,47 @@ checkFormulas env beh (ProdCons (fp, ep) (fc, ec)) =
826 -- 1) (A ⊂ ∅) <= 0
842 -- 1) (A ⊂ ∅) <= 0
827 -- 2) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
843 -- 2) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
828 -- 3) (⊤ ⊂ B) <= 0
844 -- 3) (⊤ ⊂ B) <= 0
829− -- Therefore we have the isomorphisms:
845+ -- Therefore we have the isomorphisms with (∃ and ∀ being the N-ary
846+ -- versions of \/ and /\ respectively):
830 -- (⋃_i ⋂_j A[i,j]) ⊂ (⋃_k ⋂_l B[k,l])
847 -- (⋃_i ⋂_j A[i,j]) ⊂ (⋃_k ⋂_l B[k,l])
831− -- = \/_k /\_l /\_i (⋂_j A[i,j]) ⊂ B[k,l]
848+ -- = ∃k ∀l ∀i, (⋂_j A[i,j]) ⊂ B[k,l]
832− -- = /\_i \/_k /\_l (⋂_j A[i,j]) ⊂ B[k,l]
849+ -- = ∀i ∃k ∀l, (⋂_j A[i,j]) ⊂ B[k,l]
833 -- with the caveat that the the set over which k ranges is nonempty.
850 -- with the caveat that the the set over which k ranges is nonempty.
834 -- This is because 1) is not an isomorphism.
851 -- This is because 1) is not an isomorphism.
835 -- Our disjunction loses information, so it makes sense to nest it as
852 -- Our disjunction loses information, so it makes sense to nest it as
836 -- deeply as possible, hence we choose the latter representation.
853 -- deeply as possible, hence we choose the latter representation.
838 -- We delegate the verification of (⋂_j A[j]) ⊂ B to a separate heuristic
855 -- We delegate the verification of (⋂_j A[j]) ⊂ B to a separate heuristic
839− -- function, with the understanding that \/_j A[j] ⊂ B is a sufficient,
856+ -- function, with the understanding that ∃j, A[j] ⊂ B is a sufficient,
840 -- but not necessary condition (because of 2) and 3)).
857 -- but not necessary condition (because of 2) and 3)).
842 -- If k ranges over an empty set, we have the isomorphism:
859 -- If k ranges over an empty set, we have the isomorphism:
843− -- (⋃_i ⋂_j A[i,j]) ⊂ ∅ = /\_i (⋂_j A[i,j]) ⊂ ∅
860+ -- (⋃_i ⋂_j A[i,j]) ⊂ ∅ = ∀i, (⋂_j A[i,j]) ⊂ ∅
844 -- where we again delegate (⋂_j A[j]) ⊂ ∅ to a heuristic, though here the
861 -- where we again delegate (⋂_j A[j]) ⊂ ∅ to a heuristic, though here the
845− -- shortcut of \/_j A[j] ⊂ ∅ hardly helps.
862+ -- shortcut of ∃j, A[j] ⊂ ∅ hardly helps.
864+ -- Disjunctions tend to erase informative error messages, so we may want
865+ -- to avoid them. This can be formally done as follows: if we can
866+ -- partition the universal set into a disjoint union of some parts:
868+ -- such that the conjuncts in our disjunctive normal form are subordinate
869+ -- to the partition:
870+ -- ∀i ∃α, (⋂_j A[i,j]) ⊂ P[α]
871+ -- ∀k ∃α, (⋂_l B[k,l]) ⊂ P[α]
872+ -- then we can partition the sets over which i and k range into partitions
873+ -- I[α] and K[α], and then in each "bucket" verify the inclusion in the
874+ -- aforementioned way:
875+ -- ∀α, (⋃_i∈I[α] ⋂_j A[i,j]) ⊂ (⋃_k∈K[α] ⋂_l B[k,l])
876+ -- = ∀α ∀i∈I[α] ∃k∈K[α] ∀l, (⋂_j A[i,j]) ⊂ B[k,l]
877+ -- We already somewhat do this by partitioning JSON into types, but we can
878+ -- additionally partition e.g. "enum" fields or existence of particular
879+ -- properties. This works especially well if we manage to ensure K[α] are
883+ -- (⋃_i∈I[α] ⋂_j A[i,j]) = (⋃_i ⋂_j A[i,j]) ∩ P[α]
884+ -- does not actually appear in the source schema, we need to construct it
885+ -- ourselves and come up with a name for it.
846 let typesRestricted = not (anyBottomTypes fp) && anyBottomTypes fc
886 let typesRestricted = not (anyBottomTypes fp) && anyBottomTypes fc
847 -- Specifically handle the case when a schema's type has been
887 -- Specifically handle the case when a schema's type has been
848 -- restricted from "all" to specific types: if all types were allowed
888 -- restricted from "all" to specific types: if all types were allowed
@@ -851,7 +891,7 @@ checkFormulas env beh (ProdCons (fp, ep) (fc, ec)) =
851 when typesRestricted $ issueAt beh $ TypesRestricted $ nonBottomTypes fc
891 when typesRestricted $ issueAt beh $ TypesRestricted $ nonBottomTypes fc
852 forType_ $ \tyName ty -> do
892 forType_ $ \tyName ty -> do
853 let beh' = beh >>> step (OfType tyName)
893 let beh' = beh >>> step (OfType tyName)
854− case (ty fp, ty fc) of
894+ case (getJsonFormula $ ty fp, getJsonFormula $ ty fc) of
855 (DNF pss, BottomFormula) -> unless typesRestricted $ do
895 (DNF pss, BottomFormula) -> unless typesRestricted $ do
856 -- don't repeat the TypesRestricted issue
896 -- don't repeat the TypesRestricted issue
857 F.for_ pss $ \(Conjunct ps) -> checkContradiction beh' ps
897 F.for_ pss $ \(Conjunct ps) -> checkContradiction beh' ps
@@ -862,26 +902,293 @@ checkFormulas env beh (ProdCons (fp, ep) (fc, ec)) =
862 -- In this case we want to show which restrictions were added. (instead
902 -- In this case we want to show which restrictions were added. (instead
863 -- of showing an empty list restrictions that couldn't be satisfied.)
903 -- of showing an empty list restrictions that couldn't be satisfied.)
864 F.for_ css $ \(Conjunct cs) -> F.for_ cs $ checkImplication env beh' []
904 F.for_ css $ \(Conjunct cs) -> F.for_ cs $ checkImplication env beh' []
865− (DNF pss, DNF css) -> F.for_ pss $ \(Conjunct ps) -> do
905+ (pss', css') -> F.for_ (tryPartition defs $ ProdCons (JsonFormula pss') (JsonFormula css')) $ \case
906+ (mPart, ProdCons pf cf) -> do
907+ let beh'' = foldr ((<<<) . step . InPartition) beh' mPart
908+ case (getJsonFormula pf, getJsonFormula cf) of
909+ (DNF pss, BottomFormula) -> F.for_ pss $ \(Conjunct ps) -> checkContradiction beh'' ps
910+ (DNF pss, SingleConjunct cs) -> F.for_ pss $ \(Conjunct ps) -> do
911+ F.for_ cs $ checkImplication env beh'' ps
913+ (DNF pss, DNF css) -> F.for_ pss $ \(Conjunct ps) -> do
868− (issueFromConjunct ps)
916+ (issueFromConjunct Nothing ps)
869− [F.for_ cs $ checkImplication env beh' ps | Conjunct cs <- S.toList css]
917+ [F.for_ cs $ checkImplication env beh' ps | Conjunct cs <- S.toList css]
872 anyBottomTypes f = getAny $
920 anyBottomTypes f = getAny $
873− foldType $ \_ ty -> case ty f of
921+ foldType $ \_ ty -> case getJsonFormula $ ty f of
874 BottomFormula -> Any True
922 BottomFormula -> Any True
875 _ -> mempty
923 _ -> mempty
876− nonBottomTypes f = foldType $ \tyName ty -> case ty f of
924+ nonBottomTypes f = foldType $ \tyName ty -> case getJsonFormula $ ty f of
877 BottomFormula -> mempty
925 BottomFormula -> mempty
878 _ -> [tyName]
926 _ -> [tyName]
879− issueFromConjunct :: Typeable t => [Condition t] -> Issue 'TypedSchemaLevel
927+ issueFromConjunct :: Typeable t => Partition -> [Condition t] -> Issue 'TypedSchemaLevel
880− issueFromConjunct ps
928+ issueFromConjunct _ ps
881 | Just e <- findExactly ps
929 | Just e <- findExactly ps
882 , all (satisfiesTyped e) ps =
930 , all (satisfiesTyped e) ps =
883− EnumDoesntSatisfy $ untypeValue e
931+ EnumDoesntSatisfy $ untypeValue e -- what does this look like when partitioned?
884− issueFromConjunct ps = NoMatchingCondition $ SomeCondition <$> ps
932+ issueFromConjunct mPart ps = NoMatchingCondition mPart $ SomeCondition <$> ps
935+ = DByEnumValue (DNF (S.Set A.Value))
936+ | DByProperties (DNF (S.Set Text, S.Set Text)) -- optional, required
937+ deriving stock (Eq, Ord, Show)
940+ = CByEnumValue (S.Set A.Value)
941+ | CByProperties (S.Set Text) (S.Set Text) -- included, excluded
942+ deriving stock (Eq, Ord, Show)
944+conjPart :: PartitionData -> PartitionData -> Maybe PartitionData
945+conjPart (DByEnumValue xss) (DByEnumValue yss) = Just . DByEnumValue $ xss /\ yss
946+conjPart (DByProperties xss) (DByProperties yss) = Just . DByProperties $ xss /\ yss
947+conjPart _ _ = Nothing
949+disjPart :: PartitionData -> PartitionData -> Maybe PartitionData
950+disjPart (DByEnumValue xss) (DByEnumValue yss) = Just . DByEnumValue $ xss \/ yss
951+disjPart (DByProperties xss) (DByProperties yss) = Just . DByProperties $ xss \/ yss
952+disjPart _ _ = Nothing
954+data PartitionLocation
956+ | PInProperty Text PartitionLocation
957+ deriving stock (Eq, Ord, Show)
959+newtype Partitions = Partitions (M.Map PartitionLocation (S.Set PartitionData))
960+ deriving stock (Eq, Ord, Show)
962+instance Lattice Partitions where
963+ Partitions xss /\ Partitions yss = Partitions $ M.unionWith conj xss yss
965+ conj xs ys = S.fromList . catMaybes $ liftA2 conjPart (S.toList xs) (S.toList ys)
966+ Partitions xss \/ Partitions yss = Partitions $ M.intersectionWith disj xss yss
968+ disj xs ys = S.fromList . catMaybes $ liftA2 disjPart (S.toList xs) (S.toList ys)
970+instance BoundedMeetSemiLattice Partitions where
971+ top = Partitions M.empty
973+-- The lattice has no bottom, but we use 'Lifted' to adjoin a free bottom element
975+type PartitionM = ReaderT (Traced (Definitions Schema)) (State (MemoState ()))
977+ignoreKnot :: KnotTier (Lifted Partitions) () PartitionM
980+ { onKnotFound = pure ()
981+ , onKnotUsed = \_ -> pure bottom
982+ , tieKnot = \_ -> pure
985+singletonPart :: PartitionData -> Lifted Partitions
986+singletonPart = Lift . Partitions . M.singleton PHere . S.singleton
988+partitionSchema :: Traced Schema -> PartitionM (Lifted Partitions)
989+partitionSchema sch = do
990+ allClauses <- case tracedAllOf sch of
992+ Just xs -> mapM partitionRefSchema xs
994+ anyClause <- case tracedAnyOf sch of
996+ Just xs -> joins <$> mapM partitionRefSchema xs
998+ oneClause <- case tracedOneOf sch of
1000+ Just xs -> joins <$> mapM partitionRefSchema xs
1002+ byEnumClause <- case _schemaEnum $ extract sch of
1003+ Nothing -> pure top
1005+ pure . singletonPart $
1006+ DByEnumValue $ SingleConjunct [S.fromList xs]
1008+ -- We can only partition by presence of a property if additional properties
1009+ -- are disallowed, and the property is not optional
1010+ let reqd = S.fromList $ _schemaRequired $ extract sch
1011+ byPropertiesClause <- case _schemaAdditionalProperties $ extract sch of
1012+ Just (AdditionalPropertiesAllowed False) -> do
1013+ let props = S.fromList . IOHM.keys . _schemaProperties $ extract sch
1014+ pure . singletonPart $
1015+ DByProperties $ SingleConjunct [(props S.\\ reqd, props `S.intersection` reqd)]
1018+ -- We can partition on something nested in a property only if the property is
1020+ let reqdProps = IOHM.filterWithKey (\k _ -> k `S.member` reqd) $ tracedProperties sch
1021+ inPropertiesClauses <- forM (IOHM.toList reqdProps) $ \(k, rs) -> do
1022+ f <- partitionRefSchema rs
1023+ pure $ fmap (\(Partitions m) -> Partitions $ M.mapKeysMonotonic (PInProperty k) m) f
1025+ pure $ meets $ allClauses <> [anyClause, oneClause, byEnumClause, byPropertiesClause] <> inPropertiesClauses
1027+partitionRefSchema :: Traced (Referenced Schema) -> PartitionM (Lifted Partitions)
1028+partitionRefSchema x = do
1030+ memoWithKnot ignoreKnot (partitionSchema $ dereference defs x) (ask x)
1032+newtype LiftA f a = LiftA {getLiftA :: f a}
1033+ deriving newtype (Functor, Applicative)
1035+instance (Lattice a, Applicative f) => Lattice (LiftA f a) where
1039+instance (BoundedJoinSemiLattice a, Applicative f) => BoundedJoinSemiLattice (LiftA f a) where
1040+ bottom = pure bottom
1042+instance (BoundedMeetSemiLattice a, Applicative f) => BoundedMeetSemiLattice (LiftA f a) where
1045+partitionCondition :: Condition t -> PartitionM (Lifted Partitions)
1046+partitionCondition = \case
1048+ pure . singletonPart $
1049+ DByEnumValue $ SingleConjunct [S.singleton $ untypeValue x]
1050+ Properties props _ madd -> do
1051+ let byProps = case madd of
1057+ [ ( M.keysSet $ M.filter (not . propRequired) props
1058+ , M.keysSet $ M.filter propRequired props
1061+ inProps <- forM (M.toList $ M.filter propRequired props) $ \(k, prop) -> do
1062+ f <- partitionRefSchema $ propRefSchema prop
1063+ pure $ fmap (\(Partitions m) -> Partitions $ M.mapKeysMonotonic (PInProperty k) m) f
1064+ pure $ byProps /\ meets inProps
1067+partitionJsonFormulas
1068+ :: ProdCons (Traced (Definitions Schema))
1069+ -> ProdCons (JsonFormula t)
1070+ -> Lifted Partitions
1071+partitionJsonFormulas defs pc = producer pcPart \/ consumer pcPart
1073+ pcPart = partitionFormula <$> defs <*> pc
1074+ partitionFormula def (JsonFormula xss) = runIdentity . runMemo () . (`runReaderT` def) $ do
1075+ getLiftA . foldLattice (LiftA . partitionCondition) $ xss
1077+selectPartition :: Lifted Partitions -> Maybe (PartitionLocation, S.Set PartitionChoice)
1078+selectPartition Bottom = Nothing
1079+selectPartition (Lift (Partitions m)) =
1080+ go [(loc, part) | (loc, parts) <- sortBy (comparing $ locLength . fst) $ M.toList m, part <- S.toList parts]
1082+ locLength :: PartitionLocation -> Int
1086+ walk !n (PInProperty _ l) = walk (n + 1) l
1088+ -- Skip partitioning by property for now
1089+ go ((_, DByProperties _) : ps) = go ps
1090+ -- Don't partition by enum value at the root (this reports removed enum values as contradictions in their respective partitions)
1091+ go ((PHere, DByEnumValue _) : ps) = go ps
1092+ go ((loc, DByEnumValue (DNF xss)) : ps)
1093+ -- Check that no disjunction branches are unresticted
1094+ | Just enums <- traverse (fmap (foldr1 S.intersection) . NE.nonEmpty . S.toList) . S.toList $ xss =
1096+ Just (loc, S.map (CByEnumValue . S.singleton) $ S.unions enums)
1097+ | otherwise = go ps
1099+-- This essentially has 3 cases:
1100+-- Nothing -- we have produced a bottom schema
1101+-- Just (False, _) -- there's been no change to the schema
1102+-- Just (True, x) -- x is a new schema
1103+type IntersectionM = ReaderT (Traced (Definitions Schema)) (WriterT Any Maybe)
1105+mBottom :: IntersectionM a
1106+mBottom = lift . lift $ Nothing
1108+catchBottom :: IntersectionM a -> IntersectionM a -> IntersectionM a
1109+catchBottom act handler = R.liftCatch (W.liftCatch (\a h -> a <|> h ())) act (\_ -> handler)
1111+mChange :: IntersectionM ()
1112+mChange = tell $ Any True
1115+ :: PartitionLocation
1118+ -> IntersectionM Schema
1119+intersectSchema loc part sch = do
1120+ allOf' <- forM (tracedAllOf sch) $ \rss ->
1121+ -- Assuming i ranges over a nonempty set (checked in processSchema)
1122+ -- (⋂_i A[i]) ∩ X = ⋂_i (A[i] ∩ X)
1123+ -- If any intersections are empty, the result is empty. If any intersections are a change, the result is a change.
1124+ traverse (intersectRefSchema loc part) rss
1125+ anyOf' <- forM (tracedAnyOf sch) $ \rss -> do
1126+ -- (⋃_i A[i]) ∩ X = ⋃_i (A[i] ∩ X)
1127+ -- Collect only the nonempty A[i] ∩ X, unless there are none, in which case the result is empty.
1128+ -- If any schema is empty, we remove it from the list which constitutes a change.
1129+ mSchemas <- forM rss $ \rs -> catchBottom (Just <$> intersectRefSchema loc part rs) (mChange >> pure Nothing)
1130+ case catMaybes mSchemas of
1133+ oneOf' <- forM (tracedOneOf sch) $ \rss -> do
1134+ -- Same as anyOf'. By intersecting we're only making them more disjoint if anything.
1135+ mSchemas <- forM rss $ \rs -> catchBottom (Just <$> intersectRefSchema loc part rs) (mChange >> pure Nothing)
1136+ case catMaybes mSchemas of
1139+ let sch' = (extract sch) {_schemaAllOf = allOf', _schemaAnyOf = anyOf', _schemaOneOf = oneOf'}
1140+ -- Now the local changes:
1142+ PInProperty k loc' -> case IOHM.lookup k $ tracedProperties sch of
1143+ Nothing -> error $ "Partitioning via absent property: " <> T.unpack k
1145+ prop' <- intersectRefSchema loc' part prop
1146+ pure $ sch' {_schemaProperties = IOHM.adjust (const prop') k $ _schemaProperties sch'}
1147+ PHere -> case part of
1148+ CByEnumValue vals -> do
1149+ enum' <- case _schemaEnum sch' of
1152+ pure $ S.toList vals
1154+ when (any (`S.notMember` vals) xs) mChange
1155+ case filter (`S.member` vals) xs of
1158+ pure $ sch' {_schemaEnum = Just enum'}
1159+ CByProperties {} -> error "CByProperties not implemented"
1162+ :: PartitionLocation
1164+ -> Traced (Referenced Schema)
1165+ -> IntersectionM (Referenced Schema)
1166+intersectRefSchema loc part rs = do
1168+ Inline <$> intersectSchema loc part (dereference defs rs)
1170+intersectCondition :: Traced (Definitions Schema) -> PartitionLocation -> PartitionChoice -> Condition t -> DNF (Condition t)
1171+intersectCondition _defs PHere (CByEnumValue values) cond@(Exactly x) =
1172+ if untypeValue x `S.member` values then SingleConjunct [cond] else bottom
1173+intersectCondition defs (PInProperty k loc) part cond@(Properties props add madd) = case M.lookup k props of
1174+ Nothing -> SingleConjunct [cond] -- shouldn't happen
1175+ Just prop -> case runWriterT . (`runReaderT` defs) $ intersectRefSchema loc part $ propRefSchema prop of
1176+ Just (rs', Any True) ->
1177+ let trs' = traced (ask (propRefSchema prop) >>> step (Partitioned loc part)) rs'
1178+ in SingleConjunct [Properties (M.insert k prop {propRefSchema = trs'} props) add madd]
1179+ Just (_, Any False) -> SingleConjunct [cond]
1181+intersectCondition _defs _loc _part cond = SingleConjunct [cond]
1183+intersectFormula :: Traced (Definitions Schema) -> PartitionLocation -> PartitionChoice -> JsonFormula t -> JsonFormula t
1184+intersectFormula defs loc part = JsonFormula . foldLattice (intersectCondition defs loc part) . getJsonFormula
1186+type Partition = Maybe (PartitionLocation, PartitionChoice)
1188+tryPartition :: ProdCons (Traced (Definitions Schema)) -> ProdCons (JsonFormula t) -> [(Partition, ProdCons (JsonFormula t))]
1189+tryPartition defs pc = case selectPartition $ partitionJsonFormulas defs pc of
1190+ Nothing -> [(Nothing, pc)]
1191+ Just (loc, parts) -> [(Just (loc, part), intersectFormula <$> defs <*> pure loc <*> pure part <*> pc) | part <- S.toList parts]
886checkContradiction
1193checkContradiction
887 :: Behavior 'TypedSchemaLevel
1194 :: Behavior 'TypedSchemaLevel
@@ -889,6 +1196,13 @@ checkContradiction
889 -> SemanticCompatFormula ()
1196 -> SemanticCompatFormula ()
890checkContradiction beh _ = issueAt beh NoContradiction -- TODO #70
1197checkContradiction beh _ = issueAt beh NoContradiction -- TODO #70
1199+tracedConjunct :: NE.NonEmpty (Traced (Referenced Schema)) -> Traced (Referenced Schema)
1200+tracedConjunct refSchemas = case NE.sortWith ask refSchemas of
1201+ (rs NE.:| []) -> rs
1202+ (rs1 NE.:| rs2 : rss) ->
1203+ traced (ask rs1 >>> step (ConjunctedWith $ ask <$> rs2 NE.:| rss)) $
1204+ Inline mempty {_schemaAllOf = Just $ extract <$> rs1 : rs2 : rss}
892checkImplication
1206checkImplication
893 :: (ReassembleHList xs (CheckEnv (Referenced Schema)))
1207 :: (ReassembleHList xs (CheckEnv (Referenced Schema)))
894 => HList xs
1208 => HList xs
@@ -949,10 +1263,7 @@ checkImplication env beh prods cons = case findExactly prods of
949 then pure ()
1263 then pure ()
950 else issueAt beh (NoMatchingFormat f)
1264 else issueAt beh (NoMatchingFormat f)
951 Items _ cons' -> case findRelevant (<>) (\case Items _ rs -> Just (rs NE.:| []); _ -> Nothing) prods of
1265 Items _ cons' -> case findRelevant (<>) (\case Items _ rs -> Just (rs NE.:| []); _ -> Nothing) prods of
952− Just (rs NE.:| []) -> checkCompatibility (beh >>> step InItems) env $ ProdCons rs cons'
954− let sch = Inline mempty {_schemaAllOf = Just . NE.toList $ extract <$> rs}
955− checkCompatibility (beh >>> step InItems) env $ ProdCons (traced (ask $ NE.head rs) sch) cons' -- TODO: bad trace
1266+ Just (tracedConjunct -> rs) -> checkCompatibility (beh >>> step InItems) env $ ProdCons rs cons'
956 Nothing -> issueAt beh NoMatchingItems
1267 Nothing -> issueAt beh NoMatchingItems
957 MaxItems m -> case findRelevant min (\case MaxItems m' -> Just m'; _ -> Nothing) prods of
1268 MaxItems m -> case findRelevant min (\case MaxItems m' -> Just m'; _ -> Nothing) prods of
958 Just m' ->
1269 Just m' ->
@@ -1079,7 +1390,7 @@ instance Issuable 'TypedSchemaLevel where
1079 | -- | consumer declares a minimum number of properties in the object ($1), producer declares a weaker (lower) limit ($2)
1390 | -- | consumer declares a minimum number of properties in the object ($1), producer declares a weaker (lower) limit ($2)
1080 MatchingMinPropertiesWeak (ProdCons Integer)
1391 MatchingMinPropertiesWeak (ProdCons Integer)
1081 | -- | producer declares that the value must satisfy a disjunction of some conditions, but consumer's requirements couldn't be matched against any single one of them (TODO: split heuristic #71)
1392 | -- | producer declares that the value must satisfy a disjunction of some conditions, but consumer's requirements couldn't be matched against any single one of them (TODO: split heuristic #71)
1082− NoMatchingCondition [SomeCondition]
1393+ NoMatchingCondition Partition [SomeCondition]
1083 | -- | producer indicates that values of this type are now allowed, but the consumer does not do so (currently we only check immediate contradictions, c.f. #70)
1394 | -- | producer indicates that values of this type are now allowed, but the consumer does not do so (currently we only check immediate contradictions, c.f. #70)
1084 -- AKA consumer does not have the type
1395 -- AKA consumer does not have the type
1085 NoContradiction
1396 NoContradiction
@@ -1128,15 +1439,23 @@ instance Issuable 'TypedSchemaLevel where
1128 describeIssue Forward (NoMatchingMinProperties n) = para $ "Minimum number of properties added: " <> show' n <> "."
1439 describeIssue Forward (NoMatchingMinProperties n) = para $ "Minimum number of properties added: " <> show' n <> "."
1129 describeIssue Backward (NoMatchingMinProperties n) = para $ "Minimum number of properties removed: " <> show' n <> "."
1440 describeIssue Backward (NoMatchingMinProperties n) = para $ "Minimum number of properties removed: " <> show' n <> "."
1130 describeIssue _ (MatchingMinPropertiesWeak (ProdCons p c)) = para $ "Minimum number of properties has changed from " <> show' p <> " to " <> show' c <> "."
1441 describeIssue _ (MatchingMinPropertiesWeak (ProdCons p c)) = para $ "Minimum number of properties has changed from " <> show' p <> " to " <> show' c <> "."
1131− describeIssue _ (NoMatchingCondition conds) =
1442+ describeIssue _ (NoMatchingCondition mPart conds) =
1132− para "Expected the following conditions to hold, but they didn't (please file a bug if you see this):"
1443+ para
1445+ Nothing -> "Could not verify that the following conditions hold (please file a bug if you see this)"
1447+ showPartition locPart
1448+ <> " – could not verify that the following conditions hold (please file a bug if you see this):")
1133 <> bulletList ((\(SomeCondition c) -> showCondition c) <$> conds)
1449 <> bulletList ((\(SomeCondition c) -> showCondition c) <$> conds)
1134− describeIssue Forward NoContradiction = para "The type has been removed."
1450+ describeIssue Forward NoContradiction = para "The value has been removed."
1135− describeIssue Backward NoContradiction = para "The type has been added."
1451+ describeIssue Backward NoContradiction = para "The value has been added."
1137showJSONValue :: A.Value -> Blocks
1453showJSONValue :: A.Value -> Blocks
1138showJSONValue v = codeBlockWith ("", ["json"], mempty) (T.decodeUtf8 . BSL.toStrict . A.encode $ v)
1454showJSONValue v = codeBlockWith ("", ["json"], mempty) (T.decodeUtf8 . BSL.toStrict . A.encode $ v)
1456+showJSONValueInline :: A.Value -> Inlines
1457+showJSONValueInline v = code (T.decodeUtf8 . BSL.toStrict . A.encode $ v)
1140showBound :: Show a => Bound a -> Inlines
1459showBound :: Show a => Bound a -> Inlines
1141showBound (Inclusive x) = show' x <> " inclusive"
1460showBound (Inclusive x) = show' x <> " inclusive"
1142showBound (Exclusive x) = show' x <> " exclusive"
1461showBound (Exclusive x) = show' x <> " exclusive"
@@ -1206,6 +1525,40 @@ describeJSONType = \case
1206 Array -> "Array"
1525 Array -> "Array"
1207 Object -> "Object"
1526 Object -> "Object"
1528+instance Behavable 'TypedSchemaLevel 'TypedSchemaLevel where
1529+ data Behave 'TypedSchemaLevel 'TypedSchemaLevel
1530+ = InPartition (PartitionLocation, PartitionChoice)
1531+ deriving stock (Eq, Ord, Show)
1533+ describeBehaviour (InPartition partition) = showPartition partition
1535+showPartition :: (PartitionLocation, PartitionChoice) -> Inlines
1536+showPartition = \case
1537+ (partition, CByEnumValue (S.toList -> [v])) ->
1538+ "In cases where " <> renderPartitionLocation partition <> " is " <> showJSONValueInline v
1539+ (partition, CByEnumValue (S.toList -> vs)) ->
1540+ "In cases where " <> renderPartitionLocation partition <> " has values: "
1541+ <> (fold . L.intersperse ", " . fmap showJSONValueInline $ vs)
1542+ (partition, CByProperties (S.toList -> incl) (S.toList -> [])) ->
1543+ "In cases where " <> renderPartitionLocation partition <> " contains the properties: " <> listCodes incl
1544+ (partition, CByProperties (S.toList -> []) (S.toList -> excl)) ->
1545+ "In cases where " <> renderPartitionLocation partition <> " does not contain the properties: " <> listCodes excl
1546+ (partition, CByProperties (S.toList -> incl) (S.toList -> excl)) ->
1547+ "In cases where " <> renderPartitionLocation partition
1548+ <> " contains the properties "
1550+ <> " and does not contain the properties "
1553+ listCodes :: [Text] -> Inlines
1554+ listCodes = fold . L.intersperse ", " . fmap code
1555+ renderPartitionLocation :: PartitionLocation -> Inlines
1556+ renderPartitionLocation p = code $ "$" <> renderPartitionLocation' p
1558+ renderPartitionLocation' :: PartitionLocation -> Text
1559+ renderPartitionLocation' PHere = mempty
1560+ renderPartitionLocation' (PInProperty prop rest) = "." <> prop <> renderPartitionLocation' rest
1209instance Behavable 'TypedSchemaLevel 'SchemaLevel where
1562instance Behavable 'TypedSchemaLevel 'SchemaLevel where
1210 data Behave 'TypedSchemaLevel 'SchemaLevel
1563 data Behave 'TypedSchemaLevel 'SchemaLevel
1211 = InItems
1564 = InItems
@@ -1271,4 +1624,4 @@ instance Subtree Schema where
1271 structuralItems _ = structuralIssue
1624 structuralItems _ = structuralIssue
1272 checkSemanticCompatibility env beh schs = do
1625 checkSemanticCompatibility env beh schs = do
1273 let defs = getH env
1626 let defs = getH env
1274− checkFormulas env beh $ schemaToFormula <$> defs <*> schs
1627+ checkFormulas env beh defs $ schemaToFormula <$> defs <*> schs