@@ -1,5 +1,6 @@
1{-# OPTIONS_GHC -Wno-orphans #-}
1{-# OPTIONS_GHC -Wno-orphans #-}
2−module OpenAPI.Checker.Validate.Schema
2+
3+module Data.OpenApi.Compare.Validate.Schema
@@ -10,63 +11,64 @@ import Data.Coerce
10import Data.Foldable (for_, toList)
11import Data.Foldable (for_, toList)
11import Data.Functor
12import Data.Functor
12import Data.HList
13import Data.HList
14+import Data.List (genericIndex, genericLength, group)
13import qualified Data.List.NonEmpty as NE
15import qualified Data.List.NonEmpty as NE
14import qualified Data.Map as M
16import qualified Data.Map as M
15−import Data.List (group, genericLength, genericIndex)
16import Data.Maybe
17import Data.Maybe
17import Data.OpenApi
18import Data.OpenApi
19+import Data.OpenApi.Compare.Behavior
20+import Data.OpenApi.Compare.Paths
21+import qualified Data.OpenApi.Compare.PathsPrefixTree as P
22+import Data.OpenApi.Compare.Subtree
23+import Data.OpenApi.Compare.Validate.Schema.DNF
24+import Data.OpenApi.Compare.Validate.Schema.Issues
25+import Data.OpenApi.Compare.Validate.Schema.JsonFormula
26+import Data.OpenApi.Compare.Validate.Schema.Partition
27+import Data.OpenApi.Compare.Validate.Schema.Process
28+import Data.OpenApi.Compare.Validate.Schema.Traced
29+import Data.OpenApi.Compare.Validate.Schema.TypedJson
18import Data.Ord
30import Data.Ord
19import Data.Ratio
31import Data.Ratio
20import Data.Semigroup
32import Data.Semigroup
21import qualified Data.Set as S
33import qualified Data.Set as S
22import Data.Text (Text)
34import Data.Text (Text)
23−import OpenAPI.Checker.Behavior
24−import OpenAPI.Checker.Paths
25−import qualified OpenAPI.Checker.PathsPrefixTree as P
26−import OpenAPI.Checker.Subtree
27−import OpenAPI.Checker.Validate.Schema.DNF
28−import OpenAPI.Checker.Validate.Schema.Issues
29−import OpenAPI.Checker.Validate.Schema.JsonFormula
30−import OpenAPI.Checker.Validate.Schema.Traced
31−import OpenAPI.Checker.Validate.Schema.TypedJson
32−import OpenAPI.Checker.Validate.Schema.Partition
33−import OpenAPI.Checker.Validate.Schema.Process
35−checkFormulas
36+checkFormulas ::
36− :: (ReassembleHList xs (CheckEnv (Referenced Schema)))
37+ (ReassembleHList xs (CheckEnv (Referenced Schema))) =>
37− => HList xs
38+ HList xs ->
38− -> Behavior 'SchemaLevel
39+ Behavior 'SchemaLevel ->
39− -> ProdCons (Trace Schema)
40+ ProdCons (Trace Schema) ->
40− -> ProdCons (Traced (Definitions Schema))
41+ ProdCons (Traced (Definitions Schema)) ->
41− -> ProdCons (ForeachType JsonFormula, P.PathsPrefixTree Behave AnIssue 'SchemaLevel)
42+ ProdCons (ForeachType JsonFormula, P.PathsPrefixTree Behave AnIssue 'SchemaLevel) ->
42− -> SemanticCompatFormula ()
43+ SemanticCompatFormula ()
43checkFormulas env beh trs defs (ProdCons (fp, ep) (fc, ec)) =
44checkFormulas env beh trs defs (ProdCons (fp, ep) (fc, ec)) =
44 case P.toList ep ++ P.toList ec of
45 case P.toList ep ++ P.toList ec of
45 issues@(_ : _) -> for_ issues $ embedFormula beh . anItem
46 issues@(_ : _) -> for_ issues $ embedFormula beh . anItem
47 -- We have the following isomorphisms:
48 -- We have the following isomorphisms:
48− -- (A ⊂ X ∪ Y) = (A ⊂ X) \/ (A ⊂ Y)
49 -- (A ⊂ X ∩ Y) = (A ⊂ X) /\ (A ⊂ Y)
49 -- (A ⊂ X ∩ Y) = (A ⊂ X) /\ (A ⊂ Y)
50 -- (A ⊂ ⊤) = 1
50 -- (A ⊂ ⊤) = 1
51 -- (X ∪ Y ⊂ B) = (X ⊂ B) /\ (Y ⊂ B)
51 -- (X ∪ Y ⊂ B) = (X ⊂ B) /\ (Y ⊂ B)
52 -- (∅ ⊂ B) = 1
52 -- (∅ ⊂ B) = 1
53 -- The remaining cases are, notably, not isomorphisms:
53 -- The remaining cases are, notably, not isomorphisms:
54− -- 1) (A ⊂ ∅) <= 0
54+ -- 1) (A ⊂ X ∪ Y) <= (A ⊂ X) \/ (A ⊂ Y)
55− -- 2) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
55+ -- 2) (A ⊂ ∅) <= 0
56− -- 3) (⊤ ⊂ B) <= 0
56+ -- 3) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
57− -- Therefore we have the isomorphisms with (∃ and ∀ being the N-ary
57+ -- 4) (⊤ ⊂ B) <= 0
58+ -- Therefore we have the implications with (∃ and ∀ being the N-ary
58 -- versions of \/ and /\ respectively):
59 -- versions of \/ and /\ respectively):
59 -- (⋃_i ⋂_j A[i,j]) ⊂ (⋃_k ⋂_l B[k,l])
60 -- (⋃_i ⋂_j A[i,j]) ⊂ (⋃_k ⋂_l B[k,l])
60− -- = ∃k ∀l ∀i, (⋂_j A[i,j]) ⊂ B[k,l]
61+ -- <= ∃k ∀l ∀i, (⋂_j A[i,j]) ⊂ B[k,l]
61 -- = ∀i ∃k ∀l, (⋂_j A[i,j]) ⊂ B[k,l]
62 -- = ∀i ∃k ∀l, (⋂_j A[i,j]) ⊂ B[k,l]
62 -- with the caveat that the the set over which k ranges is nonempty.
63 -- with the caveat that the the set over which k ranges is nonempty.
63− -- This is because 1) is not an isomorphism.
64+ -- (because 2) is not an isomorphism), and that this is a sufficient
65+ -- but not necessary condition (because 1) is not an isomorphism).
64 -- Our disjunction loses information, so it makes sense to nest it as
66 -- Our disjunction loses information, so it makes sense to nest it as
65 -- deeply as possible, hence we choose the latter representation.
67 -- deeply as possible, hence we choose the latter representation.
67 -- We delegate the verification of (⋂_j A[j]) ⊂ B to a separate heuristic
69 -- We delegate the verification of (⋂_j A[j]) ⊂ B to a separate heuristic
68 -- function, with the understanding that ∃j, A[j] ⊂ B is a sufficient,
70 -- function, with the understanding that ∃j, A[j] ⊂ B is a sufficient,
69− -- but not necessary condition (because of 2) and 3)).
71+ -- but not necessary condition (because of 3) and 4)).
71 -- If k ranges over an empty set, we have the isomorphism:
73 -- If k ranges over an empty set, we have the isomorphism:
72 -- (⋃_i ⋂_j A[i,j]) ⊂ ∅ = ∀i, (⋂_j A[i,j]) ⊂ ∅
74 -- (⋃_i ⋂_j A[i,j]) ⊂ ∅ = ∀i, (⋂_j A[i,j]) ⊂ ∅
@@ -143,21 +145,21 @@ checkFormulas env beh trs defs (ProdCons (fp, ep) (fc, ec)) =
143 EnumDoesntSatisfy $ untypeValue e -- what does this look like when partitioned?
145 EnumDoesntSatisfy $ untypeValue e -- what does this look like when partitioned?
144 issueFromDisjunct mPart ps = NoMatchingCondition mPart $ SomeCondition <$> S.toList ps
146 issueFromDisjunct mPart ps = NoMatchingCondition mPart $ SomeCondition <$> S.toList ps
146−checkContradiction
148+checkContradiction ::
147− :: Behavior 'TypedSchemaLevel
149+ Behavior 'TypedSchemaLevel ->
148− -> Maybe Partition
150+ Maybe Partition ->
149− -> S.Set (Condition t)
151+ S.Set (Condition t) ->
150− -> SemanticCompatFormula ()
152+ SemanticCompatFormula ()
151checkContradiction beh mPart _ = issueAt beh $ maybe TypeBecomesEmpty PartitionBecomesEmpty mPart -- TODO #70
153checkContradiction beh mPart _ = issueAt beh $ maybe TypeBecomesEmpty PartitionBecomesEmpty mPart -- TODO #70
153−checkImplication
155+checkImplication ::
154− :: (ReassembleHList xs (CheckEnv (Referenced Schema)))
156+ (ReassembleHList xs (CheckEnv (Referenced Schema))) =>
155− => HList xs
157+ HList xs ->
156− -> Behavior 'TypedSchemaLevel
158+ Behavior 'TypedSchemaLevel ->
157− -> ProdCons (Trace Schema) -- the traces of the root schemas used in this comparison
159+ ProdCons (Trace Schema) -> -- the traces of the root schemas used in this comparison
158− -> S.Set (Condition t)
160+ S.Set (Condition t) ->
159− -> Condition t
161+ Condition t ->
160− -> SemanticCompatFormula ()
162+ SemanticCompatFormula ()
161checkImplication env beh trs prods cons = case findExactly prods of
163checkImplication env beh trs prods cons = case findExactly prods of
163 | all (satisfiesTyped e) prods ->
165 | all (satisfiesTyped e) prods ->
@@ -165,124 +167,104 @@ checkImplication env beh trs prods cons = case findExactly prods of
165 then pure ()
167 then pure ()
166 else issueAt beh (EnumDoesntSatisfy $ untypeValue e)
168 else issueAt beh (EnumDoesntSatisfy $ untypeValue e)
167 | otherwise -> pure () -- vacuously true
169 | otherwise -> pure () -- vacuously true
169 Nothing -> case cons of
170 Nothing -> case cons of
170 -- the above code didn't catch it, so there's no Exactly condition on the lhs
171 -- the above code didn't catch it, so there's no Exactly condition on the lhs
171 Exactly e -> issueAt beh (NoMatchingEnum $ untypeValue e)
172 Exactly e -> issueAt beh (NoMatchingEnum $ untypeValue e)
173 Maximum m -> foldCheck min m NoMatchingMaximum MatchingMaximumWeak $ \case
173 Maximum m -> foldCheck min m NoMatchingMaximum MatchingMaximumWeak $ \case
174 Maximum m' -> Just m'
174 Maximum m' -> Just m'
175 _ -> Nothing
175 _ -> Nothing
177 Minimum m -> foldCheck max m (NoMatchingMinimum . coerce) (MatchingMinimumWeak . coerce) $ \case
176 Minimum m -> foldCheck max m (NoMatchingMinimum . coerce) (MatchingMinimumWeak . coerce) $ \case
178 Minimum m' -> Just m'
177 Minimum m' -> Just m'
179 _ -> Nothing
178 _ -> Nothing
181 MultipleOf m -> foldCheck lcmScientific m NoMatchingMultipleOf MatchingMultipleOfWeak $ \case
179 MultipleOf m -> foldCheck lcmScientific m NoMatchingMultipleOf MatchingMultipleOfWeak $ \case
182 MultipleOf m' -> Just m'
180 MultipleOf m' -> Just m'
183 _ -> Nothing
181 _ -> Nothing
185 NumberFormat f -> case flip any prods $ \case
182 NumberFormat f -> case flip any prods $ \case
186− NumberFormat f' -> f == f'
183+ NumberFormat f' -> f == f'
187− _ -> False
184+ _ -> False of
189 True -> pure ()
185 True -> pure ()
190 False -> issueAt beh (NoMatchingFormat f)
186 False -> issueAt beh (NoMatchingFormat f)
192 MaxLength m -> foldCheck min m NoMatchingMaxLength MatchingMaxLengthWeak $ \case
187 MaxLength m -> foldCheck min m NoMatchingMaxLength MatchingMaxLengthWeak $ \case
193 MaxLength m' -> Just m'
188 MaxLength m' -> Just m'
194 _ -> Nothing
189 _ -> Nothing
196 MinLength m -> foldCheck max m NoMatchingMinLength MatchingMinLengthWeak $ \case
190 MinLength m -> foldCheck max m NoMatchingMinLength MatchingMinLengthWeak $ \case
197 MinLength m' -> Just m'
191 MinLength m' -> Just m'
198 _ -> Nothing
192 _ -> Nothing
200 Pattern p -> case flip any prods $ \case
193 Pattern p -> case flip any prods $ \case
201− Pattern p' -> p == p'
194+ Pattern p' -> p == p'
202− _ -> False
195+ _ -> False of
204 True -> pure ()
196 True -> pure ()
205 False -> issueAt beh (NoMatchingPattern p) -- TODO: regex comparison #32
197 False -> issueAt beh (NoMatchingPattern p) -- TODO: regex comparison #32
207 StringFormat f -> case flip any prods $ \case
198 StringFormat f -> case flip any prods $ \case
208− StringFormat f' -> f == f'
199+ StringFormat f' -> f == f'
209− _ -> False
200+ _ -> False of
211 True -> pure ()
201 True -> pure ()
212 False -> issueAt beh (NoMatchingFormat f)
202 False -> issueAt beh (NoMatchingFormat f)
214 Items _ cons' -> case foldSome (<>) prods $ \case
203 Items _ cons' -> case foldSome (<>) prods $ \case
215− Items _ rs -> Just (Just (rs NE.:| []), mempty)
204+ Items _ rs -> Just (Just (rs NE.:| []), mempty)
216− TupleItems (map snd -> fs) -> Just (mempty, Just (fs NE.:| []))
205+ TupleItems (map snd -> fs) -> Just (mempty, Just (fs NE.:| []))
217− _ -> Nothing
206+ _ -> Nothing of
219 Just (mItems, Just pfs)
207 Just (mItems, Just pfs)
220 | not $ allSame (length <$> pfs) -> pure () -- vacuously
208 | not $ allSame (length <$> pfs) -> pure () -- vacuously
221− | let plen = genericLength (NE.head pfs)
209+ | let plen = genericLength (NE.head pfs) ->
222− -> clarifyIssue (AnItem beh (anIssue TupleToArray)) $ for_ [0 .. plen - 1] $ \i -> do
210+ clarifyIssue (AnItem beh (anIssue TupleToArray)) $
223− let prod' = tracedConjunct $ case mItems of
211+ for_ [0 .. plen - 1] $ \i -> do
224− Just prods' -> ((`genericIndex` i) <$> pfs) <> prods'
212+ let prod' = tracedConjunct $ case mItems of
225− Nothing -> (`genericIndex` i) <$> pfs
213+ Just prods' -> ((`genericIndex` i) <$> pfs) <> prods'
226− checkCompatibility (beh >>> step (InItem i)) env $ ProdCons prod' cons'
214+ Nothing -> (`genericIndex` i) <$> pfs
215+ checkCompatibility (beh >>> step (InItem i)) env $ ProdCons prod' cons'
227 Just (Just prods', Nothing) -> do
216 Just (Just prods', Nothing) -> do
228 let prod' = tracedConjunct prods'
217 let prod' = tracedConjunct prods'
229 checkCompatibility (beh >>> step InItems) env $ ProdCons prod' cons'
218 checkCompatibility (beh >>> step InItems) env $ ProdCons prod' cons'
230 _ -> clarifyIssue (AnItem beh (anIssue NoMatchingItems)) $ do
219 _ -> clarifyIssue (AnItem beh (anIssue NoMatchingItems)) $ do
231 checkCompatibility (beh >>> step InItems) env $ ProdCons prodTopSchema cons'
220 checkCompatibility (beh >>> step InItems) env $ ProdCons prodTopSchema cons'
233 TupleItems (map snd -> fs) -> case foldSome (<>) prods $ \case
221 TupleItems (map snd -> fs) -> case foldSome (<>) prods $ \case
234− TupleItems (map snd -> fs') -> Just (Just $ fs' NE.:| [], Just . Max $ genericLength fs', Just . Min $ genericLength fs', mempty)
222+ TupleItems (map snd -> fs') -> Just (Just $ fs' NE.:| [], Just . Max $ genericLength fs', Just . Min $ genericLength fs', mempty)
235− MinItems m' -> Just (mempty, Just . Max $ m', mempty, mempty)
223+ MinItems m' -> Just (mempty, Just . Max $ m', mempty, mempty)
236− MaxItems m' -> Just (mempty, mempty, Just . Min $ m', mempty)
224+ MaxItems m' -> Just (mempty, mempty, Just . Min $ m', mempty)
237− Items _ rs -> Just (mempty, mempty, mempty, Just (rs NE.:| []))
225+ Items _ rs -> Just (mempty, mempty, mempty, Just (rs NE.:| []))
238− _ -> Nothing
226+ _ -> Nothing of
239− of
227+ -- if the length constraints in the producer are contradictory:
240− -- if the length constraints in the producer are contradictory:
228+ Just (_, Just (Max lowest), Just (Min highest), _) | lowest > highest -> pure ()
241− Just (_, Just (Max lowest), Just (Min highest), _) | lowest > highest -> pure ()
229+ -- We have an explicit tuple items clause...
242− -- We have an explicit tuple items clause...
230+ Just (Just pfs, Just (Max plen), _, _)
243− Just (Just pfs, Just (Max plen), _, _)
231+ | plen /= genericLength fs -> -- ...of wrong length
244− | plen /= genericLength fs -- ...of wrong length
232+ issueAt beh (TupleItemsLengthChanged ProdCons {producer = plen, consumer = genericLength fs})
245− -> issueAt beh (TupleItemsLengthChanged ProdCons {producer = plen, consumer = genericLength fs})
233+ | otherwise ->
246− | otherwise
234+ for_ [0 .. plen - 1] $ \i -> do
247− -> for_ [0 .. plen - 1] $ \i -> do
248 checkCompatibility (beh >>> step (InItem i)) env $ ProdCons (tracedConjunct $ (`genericIndex` i) <$> pfs) (fs `genericIndex` i)
235 checkCompatibility (beh >>> step (InItem i)) env $ ProdCons (tracedConjunct $ (`genericIndex` i) <$> pfs) (fs `genericIndex` i)
249− -- We have a fixed length array in the producer...
236+ -- We have a fixed length array in the producer...
250− Just (Nothing, Just (Max plen), Just (Min plen'), mProd)
237+ Just (Nothing, Just (Max plen), Just (Min plen'), mProd)
251− | plen == plen'
238+ | plen == plen' ->
252− -> clarifyIssue (AnItem beh (anIssue ArrayToTuple)) $ case mProd of
239+ clarifyIssue (AnItem beh (anIssue ArrayToTuple)) $ case mProd of
253− _ | plen /= genericLength fs -> -- ...of wrong length
240+ _
254− issueAt beh (TupleItemsLengthChanged ProdCons {producer = plen, consumer = genericLength fs})
241+ | plen /= genericLength fs -> -- ...of wrong length
242+ issueAt beh (TupleItemsLengthChanged ProdCons {producer = plen, consumer = genericLength fs})
255 Just rs -> for_ [0 .. plen - 1] $ \i -> do
243 Just rs -> for_ [0 .. plen - 1] $ \i -> do
256 checkCompatibility (beh >>> step (InItem i)) env $ ProdCons (tracedConjunct rs) (fs `genericIndex` i)
244 checkCompatibility (beh >>> step (InItem i)) env $ ProdCons (tracedConjunct rs) (fs `genericIndex` i)
257 -- ...and no "items" schema
245 -- ...and no "items" schema
258 Nothing -> clarifyIssue (AnItem beh (anIssue NoMatchingTupleItems)) $ do
246 Nothing -> clarifyIssue (AnItem beh (anIssue NoMatchingTupleItems)) $ do
259 for_ [0 .. plen - 1] $ \i -> do
247 for_ [0 .. plen - 1] $ \i -> do
260 checkCompatibility (beh >>> step (InItem i)) env $ ProdCons prodTopSchema (fs `genericIndex` i)
248 checkCompatibility (beh >>> step (InItem i)) env $ ProdCons prodTopSchema (fs `genericIndex` i)
261− _ -> issueAt beh NoMatchingTupleItems
249+ _ -> issueAt beh NoMatchingTupleItems
263 MaxItems m -> foldCheck min m NoMatchingMaxItems MatchingMaxItemsWeak $ \case
250 MaxItems m -> foldCheck min m NoMatchingMaxItems MatchingMaxItemsWeak $ \case
264 MaxItems m' -> Just m'
251 MaxItems m' -> Just m'
265 TupleItems fs -> Just $ toInteger $ length fs
252 TupleItems fs -> Just $ toInteger $ length fs
266 _ -> Nothing
253 _ -> Nothing
268 MinItems m -> foldCheck max m NoMatchingMinItems MatchingMinItemsWeak $ \case
254 MinItems m -> foldCheck max m NoMatchingMinItems MatchingMinItemsWeak $ \case
269 MinItems m' -> Just m'
255 MinItems m' -> Just m'
270 TupleItems fs -> Just $ toInteger $ length fs
256 TupleItems fs -> Just $ toInteger $ length fs
271 _ -> Nothing
257 _ -> Nothing
273 UniqueItems -> case flip any prods $ \case
258 UniqueItems -> case flip any prods $ \case
274− UniqueItems -> True
259+ UniqueItems -> True
275− MaxItems 1 -> True
260+ MaxItems 1 -> True
276− TupleItems fs | length fs == 1 -> True
261+ TupleItems fs | length fs == 1 -> True
277− _ -> False
262+ _ -> False of
279 True -> pure ()
263 True -> pure ()
280 False -> issueAt beh NoMatchingUniqueItems
264 False -> issueAt beh NoMatchingUniqueItems
282 Properties props _ madd -> case foldSome (<>) prods $ \case
265 Properties props _ madd -> case foldSome (<>) prods $ \case
283− Properties props' _ madd' -> Just $ (props', madd') NE.:| []
266+ Properties props' _ madd' -> Just $ (props', madd') NE.:| []
284− _ -> Nothing
267+ _ -> Nothing of
286 Just pm ->
268 Just pm ->
287 anyOfAt beh NoMatchingProperties $ -- TODO: could first "concat" the lists
269 anyOfAt beh NoMatchingProperties $ -- TODO: could first "concat" the lists
288 NE.toList pm <&> \(props', madd') -> do
270 NE.toList pm <&> \(props', madd') -> do
@@ -313,11 +295,9 @@ checkImplication env beh trs prods cons = case findExactly prods of
313 (Just add', Just add) -> checkCompatibility (beh >>> step InAdditionalProperty) env (ProdCons add' add)
295 (Just add', Just add) -> checkCompatibility (beh >>> step InAdditionalProperty) env (ProdCons add' add)
315 Nothing -> issueAt beh NoMatchingProperties
297 Nothing -> issueAt beh NoMatchingProperties
317 MaxProperties m -> foldCheck min m NoMatchingMaxProperties MatchingMaxPropertiesWeak $ \case
298 MaxProperties m -> foldCheck min m NoMatchingMaxProperties MatchingMaxPropertiesWeak $ \case
318 MaxProperties m' -> Just m'
299 MaxProperties m' -> Just m'
319 _ -> Nothing
300 _ -> Nothing
321 MinProperties m -> foldCheck max m NoMatchingMinProperties MatchingMinPropertiesWeak $ \case
301 MinProperties m -> foldCheck max m NoMatchingMinProperties MatchingMinPropertiesWeak $ \case
322 MinProperties m' -> Just m'
302 MinProperties m' -> Just m'
323 _ -> Nothing
303 _ -> Nothing
@@ -325,14 +305,14 @@ checkImplication env beh trs prods cons = case findExactly prods of
325 lcmScientific (toRational -> a) (toRational -> b) =
305 lcmScientific (toRational -> a) (toRational -> b) =
326 fromRational $ lcm (numerator a) (numerator b) % gcd (denominator a) (denominator b)
306 fromRational $ lcm (numerator a) (numerator b) % gcd (denominator a) (denominator b)
328− foldCheck
308+ foldCheck ::
330− => (a -> a -> a)
310+ (a -> a -> a) ->
332− -> (a -> Issue 'TypedSchemaLevel)
312+ (a -> Issue 'TypedSchemaLevel) ->
333− -> (ProdCons a -> Issue 'TypedSchemaLevel)
313+ (ProdCons a -> Issue 'TypedSchemaLevel) ->
334− -> (forall t. Condition t -> Maybe a)
314+ (forall t. Condition t -> Maybe a) ->
335− -> SemanticCompatFormula ()
315+ SemanticCompatFormula ()
336 foldCheck f m missing weak extr = case foldSome f prods extr of
316 foldCheck f m missing weak extr = case foldSome f prods extr of
338 | f m' m == m' -> pure ()
318 | f m' m == m' -> pure ()