@@ -16,16 +16,20 @@ module OpenAPI.Checker.Validate.Schema
1616where
1717
1818import Algebra.Lattice
19+import Algebra.Lattice.Lifted
1920import Control.Applicative
2021import Control.Arrow
2122import Control.Comonad.Env hiding (env)
2223import Control.Monad.Reader hiding (ask)
2324import qualified Control.Monad.Reader as R
2425import Control.Monad.State
26+import qualified Control.Monad.Trans.Reader as R (liftCatch)
27+import qualified Control.Monad.Trans.Writer as W (liftCatch)
2528import Control.Monad.Writer
2629import qualified Data.Aeson as A
2730import qualified Data.ByteString.Lazy as BSL
2831import Data.Coerce
32+import Data.Foldable
2933import qualified Data.Foldable as F
3034import Data.Functor
3135import Data.Functor.Identity
@@ -34,6 +38,8 @@ import qualified Data.HashMap.Strict as HM
3438import qualified Data.HashMap.Strict.InsOrd as IOHM
3539import Data.Int
3640import Data.Kind
41+import Data.List (sortBy)
42+import qualified Data.List as L
3743import qualified Data.List.NonEmpty as NE
3844import qualified Data.Map as M
3945import Data.Maybe
@@ -167,7 +173,7 @@ showCondition = \case
167173 showForEachJsonFormula i =
168174 bulletList $
169175 foldType
170− (\t f -> case f i of
176+ (\t f -> case getJsonFormula $ f i of
171177 BottomFormula -> mempty
172178 (DNF conds') ->
173179 let conds = S.toList <$> S.toList conds'
@@ -243,28 +249,25 @@ instance Ord SomeCondition where
243249
244250deriving stock instance Show SomeCondition
245251
246−-- | A boolean formula (without "not") of 'Condition's. Represented as a
247−-- Disjunctive Normal Form: the formula is a disjunction of a set of conjuncts,
248−-- each of which is a conjunction of a set of 'Condition's.
249−newtype JsonFormula t
250− = DNF (S.Set (S.Set (Condition t)))
252+-- | A boolean formula (without "not") represented as a Disjunctive Normal Form:
253+-- the formula is a disjunction of a set of conjuncts, each of which is a
254+-- conjunction of a set of some elementary formulas.
255+newtype DNF a
256+ = DNF (S.Set (S.Set a))
251257 deriving stock (Eq, Ord, Show)
252258
253−disjAdd
254− :: JsonFormula t
255− -> S.Set (Condition t)
256− -> JsonFormula t
259+disjAdd :: Ord a => DNF a -> S.Set a -> DNF a
257260disjAdd (DNF yss) xs
258261 | any (`S.isSubsetOf` xs) yss = DNF yss
259262 | otherwise = DNF $ S.insert xs $ S.filter (not . S.isSubsetOf xs) yss
260263
261−instance Lattice (JsonFormula t) where
264+instance Ord a => Lattice (DNF a) where
262265 xss \/ DNF yss = S.foldl' disjAdd xss yss
263266 DNF xss /\ DNF yss =
264267 F.foldl' disjAdd bottom $
265268 liftA2 S.union (S.toList xss) (S.toList yss)
266269
267−pattern BottomFormula :: JsonFormula t
270+pattern BottomFormula :: DNF a
268271pattern BottomFormula <-
269272 DNF (S.null -> True)
270273 where
@@ -275,7 +278,7 @@ isSingleton s
275278 | S.size s == 1 = S.lookupMin s
276279 | otherwise = Nothing
277280
278−pattern Conjunct :: [Condition t] -> S.Set (Condition t)
281+pattern Conjunct :: Ord a => [a] -> S.Set a
279282pattern Conjunct xs <-
280283 (S.toList -> xs)
281284 where
@@ -283,28 +286,28 @@ pattern Conjunct xs <-
283286
284287{-# COMPLETE Conjunct #-}
285288
286−pattern SingleConjunct :: [Condition t] -> JsonFormula t
289+pattern SingleConjunct :: Ord a => [a] -> DNF a
287290pattern SingleConjunct xs <-
288291 DNF (isSingleton -> Just (Conjunct xs))
289292 where
290293 SingleConjunct xs = DNF $ S.singleton $ Conjunct xs
291294
292−pattern TopFormula :: JsonFormula t
295+pattern TopFormula :: DNF a
293296pattern TopFormula <-
294297 DNF (isSingleton -> Just (S.null -> True))
295298 where
296299 TopFormula = DNF $ S.singleton S.empty
297300
298−instance BoundedJoinSemiLattice (JsonFormula t) where
301+instance Ord a => BoundedJoinSemiLattice (DNF a) where
299302 bottom = BottomFormula
300303
301−instance BoundedMeetSemiLattice (JsonFormula t) where
304+instance Ord a => BoundedMeetSemiLattice (DNF a) where
302305 top = TopFormula
303306
304307foldLattice
305308 :: BoundedLattice l
306− => (Condition t -> l)
307− -> JsonFormula t
309+ => (a -> l)
310+ -> DNF a
308311 -> l
309312foldLattice f (DNF xss) =
310313 S.foldl'
@@ -313,8 +316,12 @@ foldLattice f (DNF xss) =
313316 bottom
314317 xss
315318
319+newtype JsonFormula t = JsonFormula {getJsonFormula :: DNF (Condition t)}
320+ deriving stock (Eq, Ord, Show)
321+ deriving newtype (Lattice, BoundedJoinSemiLattice, BoundedMeetSemiLattice)
322+
316323satisfiesFormula :: TypedValue t -> JsonFormula t -> Bool
317−satisfiesFormula val = foldLattice (satisfiesTyped val)
324+satisfiesFormula val = foldLattice (satisfiesTyped val) . getJsonFormula
318325
319326data ForeachType (f :: JsonType -> Type) = ForeachType
320327 { forNull :: f 'Null
@@ -424,6 +431,14 @@ instance Steppable Schema (Referenced Schema) where
424431 | NotStep
425432 deriving stock (Eq, Ord, Show)
426433
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)
441+
427442instance Steppable Schema (Definitions (Referenced Schema)) where
428443 data Step Schema (Definitions (Referenced Schema)) = PropertiesStep
429444 deriving stock (Eq, Ord, Show)
@@ -535,7 +550,7 @@ processSchema
535550 -> m (ForeachType JsonFormula)
536551processSchema sch@(extract -> Schema {..}) = do
537552 let singletonFormula :: Condition t -> JsonFormula t
538− singletonFormula f = SingleConjunct [f]
553+ singletonFormula f = JsonFormula $ SingleConjunct [f]
539554
540555 allClauses <- case tracedAllOf sch of
541556 Nothing -> pure []
@@ -730,11 +745,11 @@ processSchema sch@(extract -> Schema {..}) = do
730745 pure (addProps, fromMaybe fakeSchema addPropSchema)
731746 pure (k, Property (k `elem` _schemaRequired) f psch)
732747 let allBottom f = getAll $
733− foldType $ \_ ty -> case ty f of
748+ foldType $ \_ ty -> case getJsonFormula $ ty f of
734749 BottomFormula -> All True
735750 _ -> All False
736751 allTop f = getAll $
737− foldType $ \_ ty -> case ty f of
752+ foldType $ \_ ty -> case getJsonFormula $ ty f of
738753 TopFormula -> All True
739754 _ -> All False
740755 -- remove optional fields whose schemata match that of additional props
@@ -810,9 +825,10 @@ checkFormulas
810825 :: (ReassembleHList xs (CheckEnv (Referenced Schema)))
811826 => HList xs
812827 -> Behavior 'SchemaLevel
828+ -> ProdCons (Traced (Definitions Schema))
813829 -> ProdCons (ForeachType JsonFormula, P.PathsPrefixTree Behave AnIssue 'SchemaLevel)
814830 -> SemanticCompatFormula ()
815−checkFormulas env beh (ProdCons (fp, ep) (fc, ec)) =
831+checkFormulas env beh defs (ProdCons (fp, ep) (fc, ec)) =
816832 case P.toList ep ++ P.toList ec of
817833 issues@(_ : _) -> F.for_ issues $ embedFormula beh . anItem
818834 [] -> do
@@ -826,23 +842,47 @@ checkFormulas env beh (ProdCons (fp, ep) (fc, ec)) =
826842 -- 1) (A ⊂ ∅) <= 0
827843 -- 2) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
828844 -- 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):
830847 -- (⋃_i ⋂_j A[i,j]) ⊂ (⋃_k ⋂_l B[k,l])
831− -- = \/_k /\_l /\_i (⋂_j A[i,j]) ⊂ B[k,l]
832− -- = /\_i \/_k /\_l (⋂_j A[i,j]) ⊂ B[k,l]
848+ -- = ∃k ∀l ∀i, (⋂_j A[i,j]) ⊂ B[k,l]
849+ -- = ∀i ∃k ∀l, (⋂_j A[i,j]) ⊂ B[k,l]
833850 -- with the caveat that the the set over which k ranges is nonempty.
834851 -- This is because 1) is not an isomorphism.
835852 -- Our disjunction loses information, so it makes sense to nest it as
836853 -- deeply as possible, hence we choose the latter representation.
837854 --
838855 -- 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,
840857 -- but not necessary condition (because of 2) and 3)).
841858 --
842859 -- 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]) ⊂ ∅
844861 -- 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.
863+ --
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:
867+ -- ⊤ = ⊔_α P[α]
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
880+ -- 1-element sets.
881+ --
882+ -- Since the set:
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.
846886 let typesRestricted = not (anyBottomTypes fp) && anyBottomTypes fc
847887 -- Specifically handle the case when a schema's type has been
848888 -- restricted from "all" to specific types: if all types were allowed
@@ -851,7 +891,7 @@ checkFormulas env beh (ProdCons (fp, ep) (fc, ec)) =
851891 when typesRestricted $ issueAt beh $ TypesRestricted $ nonBottomTypes fc
852892 forType_ $ \tyName ty -> do
853893 let beh' = beh >>> step (OfType tyName)
854− case (ty fp, ty fc) of
894+ case (getJsonFormula $ ty fp, getJsonFormula $ ty fc) of
855895 (DNF pss, BottomFormula) -> unless typesRestricted $ do
856896 -- don't repeat the TypesRestricted issue
857897 F.for_ pss $ \(Conjunct ps) -> checkContradiction beh' ps
@@ -862,26 +902,293 @@ checkFormulas env beh (ProdCons (fp, ep) (fc, ec)) =
862902 -- In this case we want to show which restrictions were added. (instead
863903 -- of showing an empty list restrictions that couldn't be satisfied.)
864904 F.for_ css $ \(Conjunct cs) -> F.for_ cs $ checkImplication env beh' []
865− (DNF pss, DNF css) -> F.for_ pss $ \(Conjunct ps) -> do
866− anyOfAt
867− beh'
868− (issueFromConjunct ps)
869− [F.for_ cs $ checkImplication env beh' ps | Conjunct cs <- S.toList css]
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
912+ -- unlucky:
913+ (DNF pss, DNF css) -> F.for_ pss $ \(Conjunct ps) -> do
914+ anyOfAt
915+ beh'
916+ (issueFromConjunct Nothing ps)
917+ [F.for_ cs $ checkImplication env beh' ps | Conjunct cs <- S.toList css]
870918 pure ()
871919 where
872920 anyBottomTypes f = getAny $
873− foldType $ \_ ty -> case ty f of
921+ foldType $ \_ ty -> case getJsonFormula $ ty f of
874922 BottomFormula -> Any True
875923 _ -> mempty
876− nonBottomTypes f = foldType $ \tyName ty -> case ty f of
924+ nonBottomTypes f = foldType $ \tyName ty -> case getJsonFormula $ ty f of
877925 BottomFormula -> mempty
878926 _ -> [tyName]
879− issueFromConjunct :: Typeable t => [Condition t] -> Issue 'TypedSchemaLevel
880− issueFromConjunct ps
927+ issueFromConjunct :: Typeable t => Partition -> [Condition t] -> Issue 'TypedSchemaLevel
928+ issueFromConjunct _ ps
881929 | Just e <- findExactly ps
882930 , all (satisfiesTyped e) ps =
883− EnumDoesntSatisfy $ untypeValue e
884− issueFromConjunct ps = NoMatchingCondition $ SomeCondition <$> ps
931+ EnumDoesntSatisfy $ untypeValue e -- what does this look like when partitioned?
932+ issueFromConjunct mPart ps = NoMatchingCondition mPart $ SomeCondition <$> ps
933+
934+data PartitionData
935+ = DByEnumValue (DNF (S.Set A.Value))
936+ | DByProperties (DNF (S.Set Text, S.Set Text)) -- optional, required
937+ deriving stock (Eq, Ord, Show)
938+
939+data PartitionChoice
940+ = CByEnumValue (S.Set A.Value)
941+ | CByProperties (S.Set Text) (S.Set Text) -- included, excluded
942+ deriving stock (Eq, Ord, Show)
943+
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
948+
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
953+
954+data PartitionLocation
955+ = PHere
956+ | PInProperty Text PartitionLocation
957+ deriving stock (Eq, Ord, Show)
958+
959+newtype Partitions = Partitions (M.Map PartitionLocation (S.Set PartitionData))
960+ deriving stock (Eq, Ord, Show)
961+
962+instance Lattice Partitions where
963+ Partitions xss /\ Partitions yss = Partitions $ M.unionWith conj xss yss
964+ where
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
967+ where
968+ disj xs ys = S.fromList . catMaybes $ liftA2 disjPart (S.toList xs) (S.toList ys)
969+
970+instance BoundedMeetSemiLattice Partitions where
971+ top = Partitions M.empty
972+
973+-- The lattice has no bottom, but we use 'Lifted' to adjoin a free bottom element
974+
975+type PartitionM = ReaderT (Traced (Definitions Schema)) (State (MemoState ()))
976+
977+ignoreKnot :: KnotTier (Lifted Partitions) () PartitionM
978+ignoreKnot =
979+ KnotTier
980+ { onKnotFound = pure ()
981+ , onKnotUsed = \_ -> pure bottom
982+ , tieKnot = \_ -> pure
983+ }
984+
985+singletonPart :: PartitionData -> Lifted Partitions
986+singletonPart = Lift . Partitions . M.singleton PHere . S.singleton
987+
988+partitionSchema :: Traced Schema -> PartitionM (Lifted Partitions)
989+partitionSchema sch = do
990+ allClauses <- case tracedAllOf sch of
991+ Nothing -> pure []
992+ Just xs -> mapM partitionRefSchema xs
993+
994+ anyClause <- case tracedAnyOf sch of
995+ Nothing -> pure top
996+ Just xs -> joins <$> mapM partitionRefSchema xs
997+
998+ oneClause <- case tracedOneOf sch of
999+ Nothing -> pure top
1000+ Just xs -> joins <$> mapM partitionRefSchema xs
1001+
1002+ byEnumClause <- case _schemaEnum $ extract sch of
1003+ Nothing -> pure top
1004+ Just xs ->
1005+ pure . singletonPart $
1006+ DByEnumValue $ SingleConjunct [S.fromList xs]
1007+
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)]
1016+ _ -> pure top
1017+
1018+ -- We can partition on something nested in a property only if the property is
1019+ -- required
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
1024+
1025+ pure $ meets $ allClauses <> [anyClause, oneClause, byEnumClause, byPropertiesClause] <> inPropertiesClauses
1026+
1027+partitionRefSchema :: Traced (Referenced Schema) -> PartitionM (Lifted Partitions)
1028+partitionRefSchema x = do
1029+ defs <- R.ask
1030+ memoWithKnot ignoreKnot (partitionSchema $ dereference defs x) (ask x)
1031+
1032+newtype LiftA f a = LiftA {getLiftA :: f a}
1033+ deriving newtype (Functor, Applicative)
1034+
1035+instance (Lattice a, Applicative f) => Lattice (LiftA f a) where
1036+ (/\) = liftA2 (/\)
1037+ (\/) = liftA2 (\/)
1038+
1039+instance (BoundedJoinSemiLattice a, Applicative f) => BoundedJoinSemiLattice (LiftA f a) where
1040+ bottom = pure bottom
1041+
1042+instance (BoundedMeetSemiLattice a, Applicative f) => BoundedMeetSemiLattice (LiftA f a) where
1043+ top = pure top
1044+
1045+partitionCondition :: Condition t -> PartitionM (Lifted Partitions)
1046+partitionCondition = \case
1047+ Exactly x ->
1048+ pure . singletonPart $
1049+ DByEnumValue $ SingleConjunct [S.singleton $ untypeValue x]
1050+ Properties props _ madd -> do
1051+ let byProps = case madd of
1052+ Just _ -> top
1053+ Nothing ->
1054+ singletonPart $
1055+ DByProperties $
1056+ SingleConjunct
1057+ [ ( M.keysSet $ M.filter (not . propRequired) props
1058+ , M.keysSet $ M.filter propRequired props
1059+ )
1060+ ]
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
1065+ _ -> pure top
1066+
1067+partitionJsonFormulas
1068+ :: ProdCons (Traced (Definitions Schema))
1069+ -> ProdCons (JsonFormula t)
1070+ -> Lifted Partitions
1071+partitionJsonFormulas defs pc = producer pcPart \/ consumer pcPart
1072+ where
1073+ pcPart = partitionFormula <$> defs <*> pc
1074+ partitionFormula def (JsonFormula xss) = runIdentity . runMemo () . (`runReaderT` def) $ do
1075+ getLiftA . foldLattice (LiftA . partitionCondition) $ xss
1076+
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]
1081+ where
1082+ locLength :: PartitionLocation -> Int
1083+ locLength = walk 0
1084+ where
1085+ walk !n PHere = n
1086+ walk !n (PInProperty _ l) = walk (n + 1) l
1087+ go [] = Nothing
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 =
1095+ -- TODO: improve
1096+ Just (loc, S.map (CByEnumValue . S.singleton) $ S.unions enums)
1097+ | otherwise = go ps
1098+
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)
1104+
1105+mBottom :: IntersectionM a
1106+mBottom = lift . lift $ Nothing
1107+
1108+catchBottom :: IntersectionM a -> IntersectionM a -> IntersectionM a
1109+catchBottom act handler = R.liftCatch (W.liftCatch (\a h -> a <|> h ())) act (\_ -> handler)
1110+
1111+mChange :: IntersectionM ()
1112+mChange = tell $ Any True
1113+
1114+intersectSchema
1115+ :: PartitionLocation
1116+ -> PartitionChoice
1117+ -> Traced Schema
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
1131+ [] -> mBottom
1132+ schs -> pure schs
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
1137+ [] -> mBottom
1138+ schs -> pure schs
1139+ let sch' = (extract sch) {_schemaAllOf = allOf', _schemaAnyOf = anyOf', _schemaOneOf = oneOf'}
1140+ -- Now the local changes:
1141+ case loc of
1142+ PInProperty k loc' -> case IOHM.lookup k $ tracedProperties sch of
1143+ Nothing -> error $ "Partitioning via absent property: " <> T.unpack k
1144+ Just prop -> do
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
1150+ Nothing -> do
1151+ mChange
1152+ pure $ S.toList vals
1153+ Just xs -> do
1154+ when (any (`S.notMember` vals) xs) mChange
1155+ case filter (`S.member` vals) xs of
1156+ [] -> mBottom
1157+ xs' -> pure xs'
1158+ pure $ sch' {_schemaEnum = Just enum'}
1159+ CByProperties {} -> error "CByProperties not implemented"
1160+
1161+intersectRefSchema
1162+ :: PartitionLocation
1163+ -> PartitionChoice
1164+ -> Traced (Referenced Schema)
1165+ -> IntersectionM (Referenced Schema)
1166+intersectRefSchema loc part rs = do
1167+ defs <- R.ask
1168+ Inline <$> intersectSchema loc part (dereference defs rs)
1169+
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]
1180+ Nothing -> bottom
1181+intersectCondition _defs _loc _part cond = SingleConjunct [cond]
1182+
1183+intersectFormula :: Traced (Definitions Schema) -> PartitionLocation -> PartitionChoice -> JsonFormula t -> JsonFormula t
1184+intersectFormula defs loc part = JsonFormula . foldLattice (intersectCondition defs loc part) . getJsonFormula
1185+
1186+type Partition = Maybe (PartitionLocation, PartitionChoice)
1187+
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]
8851192
8861193checkContradiction
8871194 :: Behavior 'TypedSchemaLevel
@@ -889,6 +1196,13 @@ checkContradiction
8891196 -> SemanticCompatFormula ()
8901197checkContradiction beh _ = issueAt beh NoContradiction -- TODO #70
8911198
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}
1205+
8921206checkImplication
8931207 :: (ReassembleHList xs (CheckEnv (Referenced Schema)))
8941208 => HList xs
@@ -949,10 +1263,7 @@ checkImplication env beh prods cons = case findExactly prods of
9491263 then pure ()
9501264 else issueAt beh (NoMatchingFormat f)
9511265 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'
953− Just rs -> do
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'
9561267 Nothing -> issueAt beh NoMatchingItems
9571268 MaxItems m -> case findRelevant min (\case MaxItems m' -> Just m'; _ -> Nothing) prods of
9581269 Just m' ->
@@ -1079,7 +1390,7 @@ instance Issuable 'TypedSchemaLevel where
10791390 | -- | consumer declares a minimum number of properties in the object ($1), producer declares a weaker (lower) limit ($2)
10801391 MatchingMinPropertiesWeak (ProdCons Integer)
10811392 | -- | 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]
10831394 | -- | 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)
10841395 -- AKA consumer does not have the type
10851396 NoContradiction
@@ -1128,15 +1439,23 @@ instance Issuable 'TypedSchemaLevel where
11281439 describeIssue Forward (NoMatchingMinProperties n) = para $ "Minimum number of properties added: " <> show' n <> "."
11291440 describeIssue Backward (NoMatchingMinProperties n) = para $ "Minimum number of properties removed: " <> show' n <> "."
11301441 describeIssue _ (MatchingMinPropertiesWeak (ProdCons p c)) = para $ "Minimum number of properties has changed from " <> show' p <> " to " <> show' c <> "."
1131− describeIssue _ (NoMatchingCondition conds) =
1132− para "Expected the following conditions to hold, but they didn't (please file a bug if you see this):"
1442+ describeIssue _ (NoMatchingCondition mPart conds) =
1443+ para
1444+ (case mPart of
1445+ Nothing -> "Could not verify that the following conditions hold (please file a bug if you see this)"
1446+ Just locPart ->
1447+ showPartition locPart
1448+ <> " – could not verify that the following conditions hold (please file a bug if you see this):")
11331449 <> bulletList ((\(SomeCondition c) -> showCondition c) <$> conds)
1134− describeIssue Forward NoContradiction = para "The type has been removed."
1135− describeIssue Backward NoContradiction = para "The type has been added."
1450+ describeIssue Forward NoContradiction = para "The value has been removed."
1451+ describeIssue Backward NoContradiction = para "The value has been added."
11361452
11371453showJSONValue :: A.Value -> Blocks
11381454showJSONValue v = codeBlockWith ("", ["json"], mempty) (T.decodeUtf8 . BSL.toStrict . A.encode $ v)
11391455
1456+showJSONValueInline :: A.Value -> Inlines
1457+showJSONValueInline v = code (T.decodeUtf8 . BSL.toStrict . A.encode $ v)
1458+
11401459showBound :: Show a => Bound a -> Inlines
11411460showBound (Inclusive x) = show' x <> " inclusive"
11421461showBound (Exclusive x) = show' x <> " exclusive"
@@ -1206,6 +1525,40 @@ describeJSONType = \case
12061525 Array -> "Array"
12071526 Object -> "Object"
12081527
1528+instance Behavable 'TypedSchemaLevel 'TypedSchemaLevel where
1529+ data Behave 'TypedSchemaLevel 'TypedSchemaLevel
1530+ = InPartition (PartitionLocation, PartitionChoice)
1531+ deriving stock (Eq, Ord, Show)
1532+
1533+ describeBehaviour (InPartition partition) = showPartition partition
1534+
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 "
1549+ <> listCodes incl
1550+ <> " and does not contain the properties "
1551+ <> listCodes excl
1552+ where
1553+ listCodes :: [Text] -> Inlines
1554+ listCodes = fold . L.intersperse ", " . fmap code
1555+ renderPartitionLocation :: PartitionLocation -> Inlines
1556+ renderPartitionLocation p = code $ "$" <> renderPartitionLocation' p
1557+ where
1558+ renderPartitionLocation' :: PartitionLocation -> Text
1559+ renderPartitionLocation' PHere = mempty
1560+ renderPartitionLocation' (PInProperty prop rest) = "." <> prop <> renderPartitionLocation' rest
1561+
12091562instance Behavable 'TypedSchemaLevel 'SchemaLevel where
12101563 data Behave 'TypedSchemaLevel 'SchemaLevel
12111564 = InItems
@@ -1271,4 +1624,4 @@ instance Subtree Schema where
12711624 structuralItems _ = structuralIssue
12721625 checkSemanticCompatibility env beh schs = do
12731626 let defs = getH env
1274− checkFormulas env beh $ schemaToFormula <$> defs <*> schs
1627+ checkFormulas env beh defs $ schemaToFormula <$> defs <*> schs