From ae0742585a4ac6b5b0a10d8631a6f96b097c6067 Mon Sep 17 00:00:00 2001 From: Keagan McClelland Date: Tue, 21 Jun 2022 07:19:56 -0600 Subject: [PATCH] emver compression finished --- package.yaml | 2 + src/Lib/Types/Emver.hs | 1033 ++++++++++++++++++++++------------- test/Lib/Types/EmverProp.hs | 76 ++- 3 files changed, 733 insertions(+), 378 deletions(-) diff --git a/package.yaml b/package.yaml index 8055b86..3d492bc 100644 --- a/package.yaml +++ b/package.yaml @@ -87,12 +87,14 @@ library: - -fwarn-tabs - -O0 - -fdefer-typed-holes + - -fmax-pmcheck-models=40 else: ghc-options: - -Wall - -fwarn-tabs - -O2 - -fdefer-typed-holes + - -fmax-pmcheck-models=40 executables: start9-registry: diff --git a/src/Lib/Types/Emver.hs b/src/Lib/Types/Emver.hs index ed80f11..df607cb 100644 --- a/src/Lib/Types/Emver.hs +++ b/src/Lib/Types/Emver.hs @@ -59,7 +59,6 @@ import Startlude ( Foldable (length), Hashable, IsString (..), - Maybe (..), Monad ((>>=)), Monoid (mappend, mempty), NFData (..), @@ -72,7 +71,6 @@ import Startlude ( String, Word, Word64, - all, either, empty, flip, @@ -89,10 +87,10 @@ import Startlude ( toS, ($), ($>), + (&), (&&), (.), (<$>), - (<&&>), (<&>), (<<$>>), (||), @@ -105,7 +103,7 @@ import Data.List.NonEmpty qualified as NE import Data.Semigroup.Foldable (Foldable1 (foldMap1)) import Data.String.Interpolate.IsString (i) import Data.Text qualified as T -import Debug.Trace qualified +import Debug.Trace (trace) import GHC.Base (error) import GHC.Read qualified as GHC ( readsPrec, @@ -301,7 +299,11 @@ disj a b = reduce $ Disj a b beforeAfter :: Show a => a -> a -> a -beforeAfter before after = Debug.Trace.trace [i|BEFORE: #{before} ===> After #{after}|] after +beforeAfter before after = trace [i|BEFORE: #{before} ===> AFTER: #{after}|] after + + +leftRight :: Show a => (a, a) -> ((a, a) -> a) -> a +leftRight (l, r) f = let after = f (l, r) in trace [i|BEFORE: #{l}, #{r} ===> AFTER: #{after}|] after dbg :: Show a => a -> a @@ -320,356 +322,652 @@ reduce vr@(Anchor op v@(Version (0, 0, 0, 0))) = case op of (Left EQ) -> Anchor gt v (Left GT) -> Anchor eq v reduce vr@(Anchor _ _) = vr -reduce orig@(Conj x y) = case (reduce x, reduce y) of - -- conj units - (Any, vr) -> vr - (vr, Any) -> vr - -- conj annihilators - (None, _) -> None - (_, None) -> None - -- primitive conjunction reduction - (a@(Anchor (Right EQ) pt), y') -> if pt <|| y' then a else None - (x', b@(Anchor (Right EQ) pt)) -> if pt <|| x' then b else None - (a@(Anchor op pt), b@(Anchor op' pt')) -> case compare pt pt' of - -- conj commutes so we can make normalization order the points - GT -> conj b a - -- trivial cases where the points are identical - EQ -> case (isRight op, isRight op == isRight op', primOrd op == primOrd op') of - -- the theorems found here will elucidate what is going on - -- https://faculty.uml.edu/klevasseur/ads/s-laws-of-set-theory.html - -- conj idempodent law: these sets are identical - (_, True, True) -> a - -- conj complement law: these sets are opposites - (_, False, True) -> None - -- inequality incompatibility: these sets do not overlap - (True, True, False) -> None - -- conj absorption law (left): the left set is more specific - (True, False, False) -> a - -- conj absorption law (right): the right set is more specific - (False, False, False) -> b - -- all that is left is to intersect these sets. In every one of these cases the intersection can be expressed - -- as exactly the ordering that is not mentioned by the other two. - (False, True, False) -> reduce $ Anchor (Right $ complement (primOrd op) (primOrd op')) pt - -- pattern reduction, throughout you will see the following notation (primarily for visualization purposes) - -- o: this means 'eq' - -- >: this means 'lt' or 'lte' - -- <: this means 'gt' or 'gte' - -- x: this means 'neq' - -- you may find this notation a bit odd, after all the less than and greater than signs seem backwards, you can see - -- it more clearly by viewing them as area dividers. the wide part of the angle represents this concept of 'faces'. - -- By this analogy, > faces left, < faces right, x faces both left and right, and o faces neither left nor right - -- it turns out that we only care about the inner two components: the right facing component of the lesser point, - -- and the left facing component of the greater point. Why is left as an exercise to the reader. - LT -> case (fr op, fl op') of - -- Annihilator patterns: oo, ><, o<, >o - (False, False) -> None - -- Left specific patterns: ox, o>, >x, >> - (False, True) -> a - -- Right specific patterns: xo, b - -- Irreducible patterns: <>, , xx - (True, True) -> - if adjacent pt pt' - then -- here we have some weird edge cases if versions are immediately adjacent - case (op, op') of - -- <> - (Right GT, Right LT) -> None - (Left LT, Right LT) -> a - (Right GT, Left GT) -> b - (Left LT, Left GT) -> Conj a b - -- x> - (Left EQ, Right LT) -> Anchor lt pt - (Left EQ, Left GT) -> Conj a b - -- Anchor gt pt' - (Left LT, Left EQ) -> Conj a b - -- xx - (Left EQ, Left EQ) -> Conj a b - _ -> error [i|impossible reduction (anchor, anchor)|] - else Conj a b - -- insert anchor into irreducible conj pair - (a@(Anchor opa pta), y'@(Conj b@(Anchor opb ptb) c@(Anchor opc ptc))) - | opa == neq && opb == neq && opc == neq && pta < ptb && ptb < ptc -> Conj a y' - | otherwise -> - case (compare pta ptb, compare pta ptc) of - -- eq patterns reduce so prioritize conj'ing those - (EQ, LT) -> conj (conj a b) c - (GT, EQ) -> conj b (conj a c) - -- here we are to the right of an irreducible conj, so we try to reduce with the right side - (GT, GT) -> case conj c a of - -- cascade if successful - None -> None - Any -> b - cca@(Anchor _ _) -> conj b cca - -- otherwise we move xs out right - -- we know for sure at this point that the opc is x - _ -> case (fl opb, fr opa) of - (True, True) -> Conj b (Conj c a) -- xxx: x (xx) - (True, False) -> Conj a (Conj b c) -- xx>: > (xx) - (False, True) -> Conj b (Conj c a) -- Conj (Conj b a) c -- : (<>) x - -- here we are to the left of an irreducible conj, so we try to reduce the left side - (LT, LT) -> case conj a b of - -- cascade if successful - None -> None - Any -> c - cab@(Anchor _ _) -> conj cab c - -- otherwise we move xs out right - -- we know for sure that opb is x - _ -> case (fl opa, fr opc) of - (True, True) -> Conj a (Conj b c) -- xxx: x (xx) - (True, False) -> Conj c (Conj a b) -- xx>: > (xx) - (False, True) -> Conj a (Conj b c) -- Conj (Conj a c) b -- : (<>) x - -- here we are in the middle of an irreducible conj - (GT, LT) - -- xxx all irreducible - | opa == neq -> conj b (Conj a c) - -- if there is a remaining left face component it will reduce with the right side - | fl opa -> conj b (conj a c) - -- corollary - | fr opa -> conj (conj b a) c - -- only remaining case is eq, which subsumes both sides - | otherwise -> a - -- impossible because all anchors of equal versions reduce - (EQ, EQ) -> error [i|bug in equal anchor version reduction: #{orig} -> #{a}, #{b}, #{c}|] - -- ordinarily we reorder things so the lesser point is on the left - -- the only exception to this is the accumulation of x's on the right - -- so these cases should be impossible - _ -> error $ [i|bug in anchor order normalization: #{orig} -> #{a}, #{b}, #{c}|] - (x'@(Conj (Anchor opa pta) (Anchor opb ptb)), c@(Anchor opc ptc)) - -- in this case it is a fully reduced conj form with lower and upper bounds and a single x - | opc == neq && opa /= neq && opb /= neq && ptc > pta && ptc < ptb -> Conj x' c - -- isn't in normal form and we will attempt to do so by swapping args and reducing to hit the case above - | otherwise -> conj c x' - (x'@(Conj _ _), y'@(Anchor _ _)) -> conj y' x' - -- insert anchor into conj tree with a single bounded conj tree or x tree - (a@(Anchor opa pta), y'@(Conj b@(Anchor opb ptb) at@(Conj _ _))) -> - case (opa == neq, opb == neq) of - -- this means that the conj tree is all x's - (True, True) -> - case compare pta ptb of - LT -> Conj a y' - EQ -> y' - GT -> Conj b (Conj a at) - -- this means that b is a bound and so we put a with the rest of the x's - (True, False) -> - if fl opb && pta < ptb || fr opb && pta > ptb - then conj b (conj a at) - else y' - -- this means that the conj tree is all neqs and so when a is a bound we give it the bound position - (False, True) -> case compare pta ptb of - LT -> if fr opa then Conj a y' else a - EQ -> conj (conj a b) at - GT -> - if fl opa - then case conj a at of - a'@(Anchor _ _) -> conj a' b - (Conj a' at') -> Conj a' (Conj b at') - r -> error [i|impossible reduction: #{r}|] - else conj a at - -- a and b are the bounds and we leave the x tree alone - (False, False) -> conj (conj a b) at - -- insert anchor into conj tree that has two bounds and a x tree - (a@(Anchor opa pta), y'@(Conj bounds@(Conj (Anchor _ ptb) (Anchor _ ptc)) neqs)) - -- if the anchor is an x we put it into the x tree - | opa == neq -> if pta > ptb && pta < ptc then Conj bounds (conj a neqs) else y' - -- if not we smash it in with the bounds - | otherwise -> conj (conj a bounds) neqs - -- zip two irreducible conj pairs together - (x'@(Conj a@(Anchor opa pta) b@(Anchor opb ptb)), y'@(Conj c@(Anchor opc ptc) d@(Anchor opd ptd))) - -- we know for sure that a < b and c < d here - | opa /= neq && opb /= neq && opc == neq && opd == neq && ptc > pta && ptc < ptb && ptd < ptb -> Conj x' y' - | otherwise -> case (opa == neq, opb == neq, opc == neq, opd == neq) of - (False, False, False, False) -> conj (conj a c) (conj b d) - (False, _, False, _) -> conj (conj a c) (conj b d) - (_, False, _, False) -> conj (conj a c) (conj b d) - (True, True, False, False) -> conj y' x' - (False, True, True, False) -> conj (conj a d) (Conj b c) - (True, False, False, True) -> conj (conj b c) (Conj a d) - (False, False, True, True) -> case (ptc > pta && ptc < ptb, ptd > pta && ptd < ptb) of - (True, True) -> Conj x' y' - (True, False) -> Conj x' c - (False, True) -> Conj x' d - (False, False) -> x' - (True, True, True, False) -> Conj d (conj c x') - (True, True, False, True) -> Conj c (conj d x') - (True, False, True, True) -> Conj b (conj a y') - (False, True, True, True) -> Conj a (conj b y') - (True, True, True, True) -> conj a (conj b y') - -- insert irreducible conj pair into single bounded conj tree OR x tree - (x'@(Conj a@(Anchor opa pta) b@(Anchor opb ptb)), y'@(Conj c@(Anchor opc ptc) r)) - | opa /= neq && opb /= neq && opc == neq -> - if ptc > pta && ptc < ptb - then conj c (conj x' r) - else conj x' r - | otherwise -> conj a (conj b y') - (x'@(Conj (Anchor _ _) _), y'@(Conj (Anchor _ _) (Anchor _ _))) -> conj y' x' - -- insert irreducible conj pair into double bounded conj tree - (Conj a@(Anchor _ _) b@(Anchor _ _), y'@(Conj (Conj (Anchor _ _) (Anchor _ _)) _)) -> conj a (conj b y') - (x'@(Conj (Conj (Anchor _ _) (Anchor _ _)) _), y'@(Conj (Anchor _ _) (Anchor _ _))) -> conj y' x' - -- zip two conj trees - (Conj xBounds@(Conj (Anchor _ _) (Anchor _ _)) xNeqs, Conj yBounds@(Conj (Anchor _ _) (Anchor _ _)) yNeqs) -> - conj (conj xBounds yBounds) (conj xNeqs yNeqs) - (Conj xBounds@(Anchor _ _) xNeqs@(Conj _ _), Conj yBounds@(Conj (Anchor _ _) (Anchor _ _)) yNeqs) -> - conj (conj xBounds yBounds) (conj xNeqs yNeqs) - (Conj xBounds@(Conj (Anchor _ _) (Anchor _ _)) xNeqs, Conj yBounds@(Anchor _ _) yNeqs@(Conj _ _)) -> - conj (conj xBounds yBounds) (conj xNeqs yNeqs) - (Conj xBounds@(Anchor _ _) xNeqs@(Conj _ _), Conj yBounds@(Anchor _ _) yNeqs@(Conj _ _)) -> - conj (conj xBounds yBounds) (conj xNeqs yNeqs) - -- distribute right - (x', Disj p q) -> disj (conj x' p) (conj x' q) - -- distribute left - (Disj p q, y') -> disj (conj p y') (conj q y') - -- bugs - (Conj (Disj _ _) _, _) -> [i|bug in distributing conj over disj|] - (Conj _ (Disj _ _), _) -> [i|bug in distributing conj over disj|] - (_, Conj (Disj _ _) _) -> [i|bug in distributing conj over disj|] - (_, Conj _ (Disj _ _)) -> [i|bug in distributing conj over disj|] - (Conj Any _, _) -> [i|bug in conj any unit|] - (Conj _ Any, _) -> [i|bug in conj any unit|] - (_, Conj Any _) -> [i|bug in conj any unit|] - (_, Conj _ Any) -> [i|bug in conj any unit|] - (Conj None _, _) -> [i|bug in conj none annihilation|] - (Conj _ None, _) -> [i|bug in conj none annihilation|] - (_, Conj None _) -> [i|bug in conj none annihilation|] - (_, Conj _ None) -> [i|bug in conj none annihilation|] - (x', y') -> error [i|missing conj case: #{orig} -> #{x'}, #{y'}|] -reduce orig@(Disj x y) = case (reduce x, reduce y) of - -- disj annihilators - (Any, _) -> Any - (_, Any) -> Any - -- disj units - (None, vr) -> vr - (vr, None) -> vr - -- primitive disj reduction - (a@(Anchor (Left EQ) pt), y') -> if pt <|| y' then Any else a - (x', b@(Anchor (Left EQ) pt)) -> if pt <|| x' then Any else b - (a@(Anchor op pt), b@(Anchor op' pt')) -> case compare pt pt' of - GT -> disj b a - EQ -> case (isRight op, isRight op == isRight op', primOrd op == primOrd op') of - -- idempotence - (_, True, True) -> a - -- complement - (_, False, True) -> Any - -- union these sets - (True, True, False) -> reduce $ Anchor (Left $ complement (primOrd op) (primOrd op')) pt - -- disj absorption left: the left set is more general - (False, False, False) -> a - -- disj absorption right: the right set is more general - (True, False, False) -> b - -- inequality hypercompatibility: these sets are universal - (False, True, False) -> Any - LT -> case (fr op, fl op') of - -- Annihilator patterns: <>, , xx - (True, True) -> Any - -- Left general patterns: x<, xo, a - -- Right general patterns: >x, ox, o>, >> - (False, True) -> b - -- Irreducible patterns: >< >o o< oo - (False, False) -> Disj a b - (a@(Anchor opa pta), y'@(Disj b@(Anchor opb ptb) c@(Anchor opc ptc))) -> case (compare pta ptb, compare pta ptc) of - -- eq patterns reduce so prioritize disj'ing those - (EQ, LT) -> disj (disj a b) c - (GT, EQ) -> disj b (disj a c) - -- here we are to the right of an irreducible conj, so we try to reduce with the right side - (GT, GT) -> case disj c a of - -- cascade if successful - Any -> Any - None -> b - dca@(Anchor _ _) -> disj b dca - -- otherwise we move o's out right - -- we know for sure at this point that the opc is o - _ -> case (fl opb, fr opa) of - (True, True) -> Disj (Disj b a) c -- >o<: (><) o - (True, False) -> Disj b (Disj c a) -- >oo: > (oo) - (False, True) -> Disj a (Disj b c) -- oo<: < (oo) - (False, False) -> Disj b (Disj c a) -- ooo: o (oo) - -- here we are to the left of an irreducible conj, so we try to reduce the left side - (LT, LT) -> case disj a b of - -- -- cascade if successful - Any -> Any - None -> c - dab@(Anchor _ _) -> disj dab c - -- otherwise we move xs out right - -- we know for sure that opb is o - _ -> case (fl opa, fr opc) of - (True, True) -> Disj (Disj a c) b -- >o<: (><) o - (True, False) -> Disj a (Disj b c) -- >oo: > (oo) - (False, True) -> Disj c (Disj a b) -- oo<: < (oo) - (False, False) -> Disj a (Disj b c) -- ooo: o (oo) - -- here we are in the middle of an irreducible conj - (GT, LT) - -- >o< >oo oo< ooo all irreducible - | opa == eq -> disj b (Disj a c) - -- if there is a remaining left face component it will reduce with the left side - | fl opa -> disj (disj b a) c - -- corollary - | fr opa -> disj b (disj a c) - -- only remaining case is neq, which subsumes both sides - | otherwise -> a - -- impossible because all anchors of equal versions reduce - (EQ, EQ) -> error [i|bug in equal anchor version reduction: #{orig} -> #{a}, #{b}, #{c}|] - -- ordinarily we reorder things so the lesser point is on the left - -- the only exception to this is the accumulation of x's on the right - -- so these cases should be impossible - _ - | opb == eq && opc == eq -> Disj a y' - | otherwise -> error $ [i|bug in anchor order normalization: #{orig} -> #{a}, #{b}, #{c}|] - (x'@(Disj a@(Anchor _ pta) b@(Anchor _ ptb)), c@(Anchor _ ptc)) - | ptc > pta && ptc > ptb -> disj a (disj b c) - | otherwise -> disj c x' - (a@(Anchor opa pta), y'@(Conj b@(Anchor opb ptb) c@(Anchor opc ptc))) -> - case (compare pta ptb, compare pta ptc) of - (GT, GT) -> case (fr opc, fl opa) of - -- <> / x> || o / < - (False, False) -> Disj y' a - -- <> / x> || x / > +reduce orig@(Conj x y) = + (reduce x, reduce y) & \case + -- conj units + (Any, vr) -> vr + (vr, Any) -> vr + -- conj annihilators + (None, _) -> None + (_, None) -> None + -- primitive conjunction reduction + (a@(Anchor (Right EQ) pt), y') -> if pt <|| y' then a else None + (x', b@(Anchor (Right EQ) pt)) -> if pt <|| x' then b else None + (a@(Anchor op pt), b@(Anchor op' pt')) -> case compare pt pt' of + -- conj commutes so we can make normalization order the points + GT -> conj b a + -- trivial cases where the points are identical + EQ -> case (isRight op, isRight op == isRight op', primOrd op == primOrd op') of + -- the theorems found here will elucidate what is going on + -- https://faculty.uml.edu/klevasseur/ads/s-laws-of-set-theory.html + -- conj idempodent law: these sets are identical + (_, True, True) -> a + -- conj complement law: these sets are opposites + (_, False, True) -> None + -- inequality incompatibility: these sets do not overlap + (True, True, False) -> None + -- conj absorption law (left): the left set is more specific + (True, False, False) -> a + -- conj absorption law (right): the right set is more specific + (False, False, False) -> b + -- all that is left is to intersect these sets. In every one of these cases the intersection can be expressed + -- as exactly the ordering that is not mentioned by the other two. + (False, True, False) -> reduce $ Anchor (Right $ complement (primOrd op) (primOrd op')) pt + -- pattern reduction, throughout you will see the following notation (primarily for visualization purposes) + -- o: this means 'eq' + -- >: this means 'lt' or 'lte' + -- <: this means 'gt' or 'gte' + -- x: this means 'neq' + -- you may find this notation a bit odd, after all the less than and greater than signs seem backwards, you can see + -- it more clearly by viewing them as area dividers. the wide part of the angle represents this concept of 'faces'. + -- By this analogy, > faces left, < faces right, x faces both left and right, and o faces neither left nor right + -- it turns out that we only care about the inner two components: the right facing component of the lesser point, + -- and the left facing component of the greater point. Why is left as an exercise to the reader. + LT -> case (fr op, fl op') of + -- Annihilator patterns: oo, ><, o<, >o + (False, False) -> None + -- Left specific patterns: ox, o>, >x, >> (False, True) -> a - -- y' - -- + -- Right specific patterns: xo, b + -- Irreducible patterns: <>, , xx + (True, True) -> + if adjacent pt pt' + then -- here we have some weird edge cases if versions are immediately adjacent + case (op, op') of + -- <> + (Right GT, Right LT) -> None + (Left LT, Right LT) -> Anchor eq pt + (Right GT, Left GT) -> Anchor eq pt' + (Left LT, Left GT) -> Conj a b + -- x> + (Left EQ, Right LT) -> Anchor lt pt + (Left EQ, Left GT) -> Conj a b + -- Anchor gt pt' + (Left LT, Left EQ) -> Conj a b + -- xx + (Left EQ, Left EQ) -> Conj a b + _ -> error [i|impossible reduction (anchor, anchor)|] + else Conj a b + -- insert anchor into irreducible conj pair + (a@(Anchor opa pta), y'@(Conj b@(Anchor opb ptb) c@(Anchor opc ptc))) + | opa == neq && opb == neq && opc == neq && pta < ptb && ptb < ptc -> Conj a y' + | otherwise -> + case (compare pta ptb, compare pta ptc) of + -- eq patterns reduce so prioritize conj'ing those + (EQ, LT) -> conj (conj a b) c + (GT, EQ) -> conj b (conj a c) + -- here we are to the right of an irreducible conj, so we try to reduce with the right side + (GT, GT) -> case conj c a of + -- cascade if successful + None -> None + Any -> b + cca@(Anchor _ _) -> conj b cca + -- otherwise we move xs out right + -- we know for sure at this point that the opc is x + _ -> case (fl opb, fr opa) of + (True, True) -> Conj b (Conj c a) -- xxx: x (xx) + (True, False) -> Conj a (Conj b c) -- xx>: > (xx) + (False, True) -> Conj b (Conj c a) -- Conj (Conj b a) c -- : (<>) x + -- here we are to the left of an irreducible conj, so we try to reduce the left side + (LT, LT) -> case conj a b of + -- cascade if successful + None -> None + Any -> c + cab@(Anchor _ _) -> conj cab c + -- otherwise we move xs out right + -- we know for sure that opb is x + _ -> case (fl opa, fr opc) of + (True, True) -> Conj a (Conj b c) -- xxx: x (xx) + (True, False) -> Conj c (Conj a b) -- xx>: > (xx) + (False, True) -> Conj a (Conj b c) -- Conj (Conj a c) b -- : (<>) x + -- here we are in the middle of an irreducible conj + (GT, LT) + -- xxx all irreducible + | opa == neq -> conj b (Conj a c) + -- if there is a remaining left face component it will reduce with the right side + | fl opa -> conj b (conj a c) + -- corollary + | fr opa -> conj (conj b a) c + -- only remaining case is eq, which subsumes both sides + | otherwise -> a + -- impossible because all anchors of equal versions reduce + (EQ, EQ) -> error [i|bug in equal anchor version reduction: #{orig} -> #{a}, #{b}, #{c}|] + -- ordinarily we reorder things so the lesser point is on the left + -- the only exception to this is the accumulation of x's on the right + -- so these cases should be impossible + _ -> error $ [i|bug in anchor order normalization: #{orig} -> #{a}, #{b}, #{c}|] + (x'@(Conj (Anchor opa pta) (Anchor opb ptb)), c@(Anchor opc ptc)) + -- in this case it is a fully reduced conj form with lower and upper bounds and a single x + | opc == neq && opa /= neq && opb /= neq && ptc > pta && ptc < ptb -> Conj x' c + -- isn't in normal form and we will attempt to do so by swapping args and reducing to hit the case above + | otherwise -> conj c x' + (x'@(Conj _ _), y'@(Anchor _ _)) -> conj y' x' + -- insert anchor into conj tree with a single bounded conj tree or x tree + (a@(Anchor opa pta), y'@(Conj b@(Anchor opb ptb) at@(Conj _ _))) -> + case (opa == neq, opb == neq) of + -- this means that the conj tree is all x's + (True, True) -> + case compare pta ptb of + LT -> Conj a y' + EQ -> y' + GT -> conj b (conj a at) + -- this means that b is a bound and so we put a with the rest of the x's + (True, False) -> case compare pta ptb of + LT -> if fl opb then conj b (conj a at) else y' + EQ -> conj (conj a b) at + GT -> if fr opb then conj b (conj a at) else y' + -- this means that the conj tree is all neqs and so when a is a bound we give it the bound position + (False, True) -> case compare pta ptb of + LT -> if fr opa then Conj a y' else a + EQ -> conj (conj a b) at + GT -> + if fl opa + then case conj a at of + a'@(Anchor _ _) -> conj a' b + (Conj l@(Anchor opl _) r@(Anchor opr _)) + | opl /= neq -> Conj l (conj b r) + | opr /= neq -> Conj r (conj b l) + | otherwise -> error "bug" + (Conj a'@(Anchor _ _) at'@(Conj _ _)) -> Conj a' (conj b at') + r -> error [i|impossible reduction: #{r}|] + else conj a at + -- a and b are the bounds and we leave the x tree alone + (False, False) -> conj (conj a b) at + -- insert anchor into conj tree that has two bounds and a x tree + (a@(Anchor opa pta), y'@(Conj bounds@(Conj b@(Anchor _ ptb) c@(Anchor _ ptc)) neqs)) + -- if the anchor is an x we put it into the x tree + | opa == neq -> + if + | pta > ptb && pta < ptc -> Conj bounds (conj a neqs) + | pta == ptb -> conj (conj (conj a b) c) neqs + | pta == ptc -> conj (conj b (conj a c)) neqs + | otherwise -> y' + -- if not we smash it in with the bounds + | otherwise -> conj (conj a bounds) neqs + -- zip two irreducible conj pairs together + (x'@(Conj a@(Anchor opa pta) b@(Anchor opb ptb)), y'@(Conj c@(Anchor opc ptc) d@(Anchor opd ptd))) + -- we know for sure that a < b and c < d here + | opa /= neq && opb /= neq && opc == neq && opd == neq && ptc > pta && ptc < ptb && ptd < ptb -> Conj x' y' + | otherwise -> case (opa == neq, opb == neq, opc == neq, opd == neq) of + (False, False, False, False) -> conj (conj a c) (conj b d) + (False, _, False, _) -> conj (conj a c) (conj b d) + (_, False, _, False) -> conj (conj a c) (conj b d) + (True, True, False, False) -> conj y' x' + (False, True, True, False) -> conj (conj a d) (Conj b c) + (True, False, False, True) -> conj (conj b c) (Conj a d) + (False, False, True, True) + | ptc <|| x' && ptd <|| x' -> Conj x' y' + | ptc <|| x' -> conj x' c + | ptd <|| x' -> conj x' d + | otherwise -> x' + (True, True, True, False) -> conj d (conj c x') + (True, True, False, True) -> conj c (conj d x') + (True, False, True, True) -> conj b (conj a y') + (False, True, True, True) -> conj a (conj b y') + (True, True, True, True) -> conj a (conj b y') + -- insert irreducible conj pair into single bounded conj tree OR x tree + (x'@(Conj a@(Anchor opa pta) b@(Anchor opb ptb)), y'@(Conj c@(Anchor opc ptc) r)) + | opa /= neq && opb /= neq && opc == neq -> case (compare ptc pta, compare ptc ptb) of + (LT, LT) -> if fl opa then conj (conj c x') r else conj x' r + (EQ, LT) -> conj (conj (conj a c) b) r + (GT, LT) -> conj (conj (conj a c) b) r + (GT, EQ) -> conj (conj a (conj b c)) r + (GT, GT) -> if fr opb then conj (conj x' c) r else conj x' r + _ -> error "bug" + | otherwise -> conj a (conj b y') + (x'@(Conj (Anchor _ _) _), y'@(Conj (Anchor _ _) (Anchor _ _))) -> conj y' x' + -- insert irreducible conj pair into double bounded conj tree + (Conj a@(Anchor _ _) b@(Anchor _ _), y'@(Conj (Conj (Anchor _ _) (Anchor _ _)) _)) -> conj a (conj b y') + (x'@(Conj (Conj (Anchor _ _) (Anchor _ _)) _), y'@(Conj (Anchor _ _) (Anchor _ _))) -> conj y' x' + -- x tree, x tree + (Conj a@(Anchor (Left EQ) pta) ra, Conj b@(Anchor (Left EQ) ptb) rb) -> + let r = conj ra rb + in case compare pta ptb of + LT -> Conj a (Conj b r) + EQ -> Conj a r + GT -> Conj b (Conj a r) + -- x tree, single bounded conj tree + (x'@(Conj (Anchor (Left EQ) _) (Conj _ _)), Conj b@(Anchor _ _) rb@(Conj _ _)) -> conj b (conj x' rb) + -- single bounded conj tree, x tree + (Conj a@(Anchor _ _) ra@(Conj _ _), y'@(Conj (Anchor (Left EQ) _) (Conj _ _))) -> conj a (conj y' ra) + -- x tree, double bounded conj tree + (Conj a@(Anchor (Left EQ) _) ra@(Conj _ _), Conj yBounds@(Conj (Anchor _ _) (Anchor _ _)) yNeqs) -> conj ra (conj yBounds (conj a yNeqs)) + -- double bounded conj tree, x tree + (Conj xBounds@(Conj (Anchor _ _) (Anchor _ _)) xNeqs, Conj b@(Anchor (Left EQ) _) rb@(Conj _ _)) -> conj rb (conj xBounds (conj b xNeqs)) + -- double bounded conj tree, double bounded conj tree + (Conj xBounds@(Conj (Anchor _ _) (Anchor _ _)) xNeqs, Conj yBounds@(Conj (Anchor _ _) (Anchor _ _)) yNeqs) -> + conj (conj xBounds yBounds) (conj xNeqs yNeqs) + (Conj xBound@(Anchor _ _) xNeqs@(Conj _ _), Conj yBounds@(Conj (Anchor _ _) (Anchor _ _)) yNeqs) -> + conj (conj xBound yBounds) (conj xNeqs yNeqs) + (Conj xBounds@(Conj (Anchor _ _) (Anchor _ _)) xNeqs, Conj yBound@(Anchor _ _) yNeqs@(Conj _ _)) -> + conj (conj xBounds yBound) (conj xNeqs yNeqs) + (Conj xBounds@(Anchor _ _) xNeqs@(Conj _ _), Conj yBounds@(Anchor _ _) yNeqs@(Conj _ _)) -> + conj (conj xBounds yBounds) (conj xNeqs yNeqs) + -- distribute right + (x', Disj p q) -> disj (conj x' p) (conj x' q) + -- distribute left + (Disj p q, y') -> disj (conj p y') (conj q y') + -- bugs + (Conj (Disj _ _) _, _) -> [i|bug in distributing conj over disj|] + (Conj _ (Disj _ _), _) -> [i|bug in distributing conj over disj|] + (_, Conj (Disj _ _) _) -> [i|bug in distributing conj over disj|] + (_, Conj _ (Disj _ _)) -> [i|bug in distributing conj over disj|] + (Conj Any _, _) -> [i|bug in conj any unit|] + (Conj _ Any, _) -> [i|bug in conj any unit|] + (_, Conj Any _) -> [i|bug in conj any unit|] + (_, Conj _ Any) -> [i|bug in conj any unit|] + (Conj None _, _) -> [i|bug in conj none annihilation|] + (Conj _ None, _) -> [i|bug in conj none annihilation|] + (_, Conj None _) -> [i|bug in conj none annihilation|] + (_, Conj _ None) -> [i|bug in conj none annihilation|] + (x', y') -> error [i|missing conj case: #{orig} -> #{x'}, #{y'}|] +reduce orig@(Disj x y) = + (reduce x, reduce y) & \case + -- disj annihilators + (Any, _) -> Any + (_, Any) -> Any + -- disj units + (None, vr) -> vr + (vr, None) -> vr + -- primitive disj reduction + (a@(Anchor (Left EQ) pt), y') -> if pt <|| y' then Any else a + (x', b@(Anchor (Left EQ) pt)) -> if pt <|| x' then Any else b + (a@(Anchor op pt), b@(Anchor op' pt')) -> case compare pt pt' of + GT -> disj b a + EQ -> case (isRight op, isRight op == isRight op', primOrd op == primOrd op') of + -- idempotence + (_, True, True) -> a + -- complement + (_, False, True) -> Any + -- union these sets + (True, True, False) -> reduce $ Anchor (Left $ complement (primOrd op) (primOrd op')) pt + -- disj absorption left: the left set is more general + (False, False, False) -> a + -- disj absorption right: the right set is more general + (True, False, False) -> b + -- inequality hypercompatibility: these sets are universal + (False, True, False) -> Any + LT -> case (fr op, fl op') of + -- Annihilator patterns: <>, , xx (True, True) -> Any - (LT, LT) -> case (fr opa, fl opb) of - -- o / > || <> / Disj a y' - -- o / > || x> / xx - (False, True) -> y' - -- < / x || <> / a - -- < / x || x> / xx - (True, True) -> Any - (GT, LT) -> case (fl opa, fr opa) of - (True, True) -> Any - (True, False) -> c + -- Right general patterns: >x, ox, o>, >> (False, True) -> b - (False, False) -> y' + -- Irreducible patterns: >< >o o< oo + (False, False) -> Disj a b + -- anchor, irreducible disj pair + (a@(Anchor opa pta), y'@(Disj b@(Anchor opb ptb) c@(Anchor opc ptc))) -> case (compare pta ptb, compare pta ptc) of + -- eq patterns reduce so prioritize disj'ing those + (EQ, LT) -> disj (disj a b) c + (GT, EQ) -> disj b (disj a c) + -- here we are to the right of an irreducible conj, so we try to reduce with the right side + (GT, GT) -> case disj c a of + -- cascade if successful + Any -> Any + None -> b + dca@(Anchor _ _) -> disj b dca + -- otherwise just assemble to list + Disj _ _ -> Disj b (Disj c a) + _ -> error "bug" + -- here we are to the left of an irreducible conj, so we try to reduce the left side + (LT, LT) -> case disj a b of + Any -> Any + None -> c + -- cascade if successful + dab@(Anchor _ _) -> disj dab c + -- otherwise we move os out right + -- we know for sure that opb is o + _ -> Disj a y' + (GT, LT) + -- >o< >oo oo< ooo all irreducible + | opa == eq -> disj b (Disj a c) + -- if there is a remaining left face component it will reduce with the left side + | fl opa -> disj (disj b a) c + -- corollary + | fr opa -> disj b (disj a c) + -- only remaining case is neq, which subsumes both sides + | otherwise -> a + -- impossible because all anchors of equal versions reduce (EQ, EQ) -> error [i|bug in equal anchor version reduction: #{orig} -> #{a}, #{b}, #{c}|] - (EQ, _) -> conj (conj a b) c - (_, EQ) -> conj b (conj a c) - (LT, GT) -> error [i|bug in anchor order normalization: #{orig} -> #{a}, #{b}, #{c}|] - (x'@(Conj (Anchor _ _) (Anchor _ ptb)), c@(Anchor opc ptc)) - | ptc > ptb && not (fl opc) -> Disj x' c - | otherwise -> disj c x' - -- anchor into x tree - (Anchor _ _, Conj (Anchor (Left EQ) _) (Conj _ _)) -> error "Anchor, X Tree" - -- anchor into single bounded conj tree - (Anchor _ _, Conj (Anchor _ _) (Conj _ _)) -> error "Anchor, Single Bounded Conj Tree" - (Conj (Anchor _ _) (Conj _ _), Anchor _ _) -> error "Single Bounded Conj Tree, Anchor" - -- anchor into double bounded conj tree - (Anchor _ _, Conj (Conj _ _) _) -> error "Anchor, Double Bounded Conj Tree" - (x'@(Conj (Conj _ _) _), y'@(Anchor _ _)) -> conj y' x' - -- anchor into disj tree - (Anchor _ _, Disj (Conj _ _) _) -> error "Anchor, Disj tree with Conj at head" - (Disj (Conj _ _) _, Anchor _ _) -> error "Disj tree with Conj at head, Anchor" - (Anchor _ _, Disj (Anchor _ _) _) -> error "Anchor, Disj tree with Anchor at head" - (Disj (Anchor _ _) _, Anchor _ _) -> error "Disj tree with Anchor at head, Anchor" - (Conj (Anchor _ _) (Anchor _ _), Conj (Anchor _ _) (Anchor _ _)) -> error "Irreducible Conj Pair, Irreducible Conj Pair" - (Conj (Anchor _ _) (Anchor _ _), Disj (Anchor _ _) _) -> error "Irreducible Conj Pair, Disj tree with Anchor at head" - (Disj (Anchor _ _) _, Conj (Anchor _ _) (Anchor _ _)) -> error "Disj tree with Anchor at head, Irreducible Conj Pair" - (Disj (Anchor _ _) _, Disj (Anchor _ _) _) -> error "Disj tree with Anchor head, Disj tree with Anchor head" - (x', y') -> error [i|missing disj case: #{orig} -> #{x'}, #{y'}|] + -- ordinarily we reorder things so the lesser point is on the left + -- the only exception to this is the accumulation of x's on the right + -- so these cases should be impossible + _ + | opb == eq && opc == eq -> Disj a y' + | otherwise -> error $ [i|bug in anchor order normalization: #{orig} -> #{a}, #{b}, #{c}|] + -- irreducible disj pair, anchor + (x'@(Disj a@(Anchor _ pta) b@(Anchor _ ptb)), c@(Anchor _ ptc)) + | ptc > pta && ptc > ptb -> disj a (disj b c) + | otherwise -> disj c x' + -- anchor, irreducible conj pair + (a@(Anchor opa pta), y'@(Conj b@(Anchor opb ptb) c@(Anchor opc ptc))) -> + case (compare pta ptb, compare pta ptc) of + (GT, GT) -> case (fr opc, fl opa) of + -- <> / x> || o / < + (False, False) -> Disj y' a + -- <> / x> || x / > + (False, True) -> a + -- y' + -- + (True, True) -> Any + (LT, LT) -> case (fr opa, fl opb) of + -- o / > || <> / Disj a y' + -- o / > || x> / xx + (False, True) -> y' + -- < / x || <> / a + -- < / x || x> / xx + (True, True) -> Any + (GT, LT) -> case (fl opa, fr opa) of + (True, True) -> Any + (True, False) -> c + (False, True) -> b + (False, False) -> y' + (EQ, EQ) -> error [i|bug in equal anchor version reduction: #{orig} -> #{a}, #{b}, #{c}|] + (EQ, _) -> conj (disj a b) (disj a c) + (_, EQ) -> conj (disj a b) (disj a c) + (LT, GT) -> error [i|bug in anchor order normalization: #{orig} -> #{a}, #{b}, #{c}|] + -- irreducible conj pair, anchor + (x'@(Conj (Anchor _ _) (Anchor opb ptb)), c@(Anchor opc ptc)) + | ptc > ptb && not (fl opc) && not (fr opb) -> Disj x' c + | otherwise -> disj c x' + -- anchor, x tree + (a@(Anchor _ _), Conj b@(Anchor (Left EQ) ptb) r@(Conj _ _)) -> + if ptb <|| a + then disj a r + else conj b (disj a r) + -- x tree, anchor + (x'@(Conj (Anchor (Left EQ) _) (Conj _ _)), a@(Anchor _ _)) -> disj a x' + -- anchor, single bounded conj tree + (a@(Anchor _ pta), y'@(Conj b@(Anchor _ ptb) r@(Conj _ _))) -> case disj a b of + Any -> disj a r + dab@(Anchor _ _) -> conj dab (disj a r) + Disj _ _ -> if pta < ptb then Disj a y' else Disj y' a + _ -> error [i|bug in single bounded conj tree normalization|] + -- single bounded conj tree, anchor + (x'@(Conj (Anchor opa pta) (Conj _ _)), b@(Anchor opb ptb)) + | ptb > pta && fr opb && not (fl opb) && fl opa && not (fr opa) -> Disj x' b + | otherwise -> disj b x' + -- anchor, double bounded conj tree + (x'@(Anchor _ _), y'@(Conj bounds@(Conj (Anchor _ _) (Anchor _ _)) neqs)) -> case disj x' bounds of + dx'bounds@(Anchor _ _) -> conj dx'bounds (disj x' neqs) + dx'bounds@(Conj _ _) -> conj dx'bounds (disj x' neqs) + Disj (Anchor _ _) (Conj (Anchor _ _) (Anchor _ _)) -> Disj x' y' + Disj (Conj (Anchor _ _) (Anchor _ _)) (Anchor _ _) -> Disj y' x' + _ -> error "bug" + -- double bounded conj tree, anchor + (x'@(Conj (Conj (Anchor _ _) (Anchor opb ptb)) _), y'@(Anchor opc ptc)) + | ptc > ptb && not (fl opc) && not (fr opb) -> Disj x' y' + | otherwise -> disj y' x' + -- anchor, disj tree with conj head + (x'@(Anchor _ _), Disj ct@(Conj _ _) r) -> case disj x' ct of + Any -> Any + dx'ct@(Anchor _ _) -> disj dx'ct r + dx'ct@(Conj _ _) -> disj dx'ct r + Disj x''@(Anchor opa pta) ct'@(Conj (Anchor opb ptb) (Anchor _ _)) + | pta < ptb && not (fl opb) && not (fr opa) -> Disj x'' (disj ct' r) + | otherwise -> error "bug" + Disj x''@(Anchor opa pta) ct'@(Conj (Anchor opb ptb) (Conj _ _)) + | pta < ptb && not (fl opb) && not (fr opa) -> Disj x'' (disj ct' r) + | otherwise -> error "bug" + Disj x''@(Anchor opa pta) ct'@(Conj (Conj (Anchor opb ptb) (Anchor _ _)) _) + | pta < ptb && not (fl opb) && not (fr opa) -> Disj x'' (disj ct' r) + | otherwise -> error "bug" + Disj ct'@(Conj (Anchor _ _) (Anchor opb ptb)) x''@(Anchor opc ptc) + | ptc > ptb && not (fr opb) && not (fl opc) -> Disj ct' (disj x'' r) + | otherwise -> error "bug" + Disj ct'@(Conj (Anchor opa pta) (Conj _ _)) x''@(Anchor opb ptb) + | ptb > pta && not (fr opa) && not (fl opb) -> Disj ct' (disj x'' r) + | otherwise -> error "bug" + Disj ct'@(Conj (Conj (Anchor _ _) (Anchor opb ptb)) _) x''@(Anchor opc ptc) + | ptc > ptb && not (fr opb) && not (fl opc) -> Disj ct' (disj x'' r) + | otherwise -> error "bug" + _ -> error "bug" + -- disj tree with conj head, anchor + (x'@(Disj (Conj _ _) _), y'@(Anchor _ _)) -> disj y' x' + -- conj tree, disj tree with conj head + (x'@(Conj _ _), y'@(Disj b@(Conj _ _) r)) -> case disj x' b of + Any -> Any + dx'b@(Anchor _ _) -> disj dx'b r + dx'b@(Conj _ _) -> disj dx'b r + Disj p q + | p == x' && q == b -> Disj x' y' + | p == b && q == x' -> disj b (disj x' r) + | otherwise -> error "bug" + other -> error [i|#{other}, #{x'}, #{y'}|] + -- disj tree with conj head, conj tree + (x'@(Disj (Conj _ _) _), y'@(Conj _ _)) -> disj y' x' + -- anchor, disj tree with anchor head + (a@(Anchor _ _), y'@(Disj b@(Anchor _ _) r)) -> case disj a b of + Disj p q + | p == a && q == b -> Disj a y' + | p == b && q == a -> disj b (disj a r) + other -> disj other r + -- disj tree with anchor head, anchor + (x'@(Disj (Anchor _ _) _), y'@(Anchor _ _)) -> disj y' x' + -- irreducible conj pair, irreducible conj pair + (x'@(Conj a@(Anchor opa pta) b@(Anchor opb ptb)), y'@(Conj c@(Anchor opc ptc) d@(Anchor opd ptd))) -> + -- we know for certain that pta < ptb and ptc < ptd + case (fl opa, fr opb, fl opc, fr opd) of + -- <> <> + (False, False, False, False) -> case (compare pta ptc, compare pta ptd, compare ptb ptc, compare ptb ptd) of + -- a = c < b = d + (EQ, _, _, EQ) + | opa == geq && opc == gt && opd == leq && opb == lt -> Conj a d + | opc == geq && opa == gt && opb == leq && opd == lt -> Conj c b + | (opa == geq || opc == gt) && (opb == leq || opd == lt) -> x' + | (opc == geq || opa == gt) && (opd == leq || opb == lt) -> y' + | otherwise -> error "bug" + -- a = c < b < d + (EQ, _, _, LT) + | opa == geq && opc == gt -> Conj a d + | otherwise -> y' + -- a = c < d < b + (EQ, _, _, GT) + | opa == gt && opc == geq -> Conj c b + | otherwise -> x' + -- a < c < b = d + (LT, _, _, EQ) + | opd == leq && opb == lt -> Conj a d + | otherwise -> x' + -- c < a < b = d + (GT, _, _, EQ) + | opb == leq && opd == lt -> Conj c b + | otherwise -> y' + -- a < b = c < d + (_, _, EQ, _) + | opb == leq || opc == geq -> Conj a d + | otherwise -> Conj (Conj a d) (Anchor neq ptb) + -- c < a = d < b + (_, EQ, _, _) + | opd == leq || opa == geq -> Conj c b + | otherwise -> Conj (Conj c b) (Anchor neq pta) + -- a < b < c < d + (_, _, LT, _) -> Disj x' y' + -- c < d < a < b + (_, GT, _, _) -> Disj y' x' + -- a < c < b < d + (LT, _, GT, LT) -> Conj a d + -- c < a < d < b + (GT, LT, _, GT) -> Conj c b + -- a < c < d < b + (LT, _, _, GT) -> x' + -- c < a < b < d + (GT, _, _, LT) -> y' + -- <> Disj x' y' + | ptd <|| x' -> disj x' c + | ptb == ptd && opb == leq -> disj a c + | ptb == ptd && opb == lt -> Conj (disj a c) d + | ptb == ptc && opb == lt && opc == gt -> Conj a (Conj (Anchor neq ptb) d) + | pta == ptd && opa == gt -> y' + | a == c -> conj a (disj b d) + | pta == ptc -> conj (Anchor geq pta) (disj b d) + | ptd < pta -> y' + | ptc < pta && ptb < ptd -> y' + | pta < ptc -> Conj a d + | otherwise -> error [i|#{x'}, #{y'}|] + -- <> x> + (False, False, True, False) + | ptd < pta -> Disj y' x' + | ptc <|| x' -> disj d x' + | pta == ptc && opa == geq -> disj b d + | pta == ptc && opa == gt -> Conj c (disj b d) + | pta == ptd && opa == gt && opd == lt -> Conj b (Conj c (Anchor neq pta)) + | ptb == ptc && opb == lt -> y' + | b == d -> conj (disj a c) b + | ptb == ptd -> conj (disj a c) (Anchor leq ptd) + | ptb < ptc -> y' + | pta > ptc && ptb < ptd -> y' + | ptb > ptd -> Conj c b + | otherwise -> error [i|#{x'}, #{y'}|] + -- + (False, True, False, False) + | ptd < pta -> Disj y' x' + | otherwise -> disj y' x' + -- x> <> + (True, False, False, False) + | ptc > ptb -> Disj x' y' + | otherwise -> disj y' x' + -- disj c x' + | ptb <|| y' -> disj a y' + | ptb == ptd -> conj (disj a c) b + | otherwise -> error "bug" + -- + (False, True, True, False) + | ptd < pta -> Disj y' x' + | ptb <|| y' -> disj a y' + | ptc <|| x' -> disj d x' + | pta < ptd && ptc < pta && ptb > ptd -> Conj c b + | ptb == ptc -> b + | pta == ptd && opa == gt && opd == lt -> Conj c (Conj (Anchor neq pta) b) + | pta == ptd -> Conj c b + | pta == ptc && opa == gt -> Conj c (disj b d) + | ptb == ptd && opd == lt -> Conj (disj a c) b + | otherwise -> error [i|#{x'}, #{y'}|] + -- x> ptb -> Disj x' y' + | otherwise -> disj y' x' + -- x> x> + (True, False, True, False) + | pta <|| y' -> disj b y' + | ptc <|| x' -> disj d x' + | pta == ptc -> conj (disj b d) a + | otherwise -> error "bug" + -- xx ?? + (True, True, _, _) + | pta <|| y' && ptb <|| y' -> Any + | pta <|| y' -> b + | ptb <|| y' -> a + | otherwise -> x' + -- ?? xx + (_, _, True, True) + | ptc <|| x' && ptd <|| x' -> Any + | ptc <|| x' -> d + | ptd <|| x' -> c + | otherwise -> y' + -- irreducible conj pair, disj tree with anchor head + (x'@(Conj (Anchor opa pta) (Anchor opb ptb)), y'@(Disj c@(Anchor opc ptc) r)) -> case disj c x' of + Any -> Any + dcx'@(Anchor _ _) -> disj dcx' r + dcx'@(Conj _ _) -> disj dcx' r + Disj _ _ + | ptc > ptb && not (fl opc) && not (fr opb) -> Disj x' y' + | ptc < pta && not (fr opc) && not (fl opa) -> disj c (disj x' r) + | otherwise -> error "bug" + _ -> error "bug" + -- disj tree with anchor head, irreducible conj pair + (x'@(Disj (Anchor _ _) _), y'@(Conj (Anchor _ _) (Anchor _ _))) -> disj y' x' + -- disj tree, disj tree + (Disj a b, Disj c d) -> disj a (disj c (disj b d)) + (x', y'@(Disj a b)) -> case disj x' a of + Disj p q + | p == x' && q == a -> Disj x' y' + | p == a && q == x' -> disj a (disj x' b) + dx'a -> disj dx'a b + (x'@(Disj _ _), y') -> disj y' x' + -- x tree, x tree + (x'@(Conj a@(Anchor (Left EQ) pta) ra@(Conj _ _)), y'@(Conj b@(Anchor (Left EQ) ptb) rb@(Conj _ _))) -> case compare pta ptb of + LT -> if disj a rb == a then Conj a (disj ra y') else disj ra y' + EQ -> Conj a (disj ra rb) + GT -> if disj b ra == b then Conj b (disj x' rb) else disj x' rb + -- single bounded conj tree, x tree + (x'@(Conj (Anchor _ _) (Conj _ _)), y'@(Conj (Anchor (Left EQ) _) (Conj _ _))) -> disj y' x' + -- x tree, single bounded conj tree + (Conj a@(Anchor (Left EQ) pta) r@(Conj _ _), y'@(Conj (Anchor _ _) (Conj _ _))) -> + if pta <|| y' + then disj r y' + else conj a (disj r y') + -- -- x tree, irreducible conj pair + (Conj a@(Anchor (Left EQ) pta) r@(Conj _ _), y'@(Conj (Anchor _ _) (Anchor _ _))) -> + if pta <|| y' + then disj r y' + else conj a (disj r y') + -- irreducible conj pair, single bounded conj tree + (x'@(Conj (Anchor _ _) (Anchor _ _)), y'@(Conj c@(Anchor _ _) r)) -> case disj x' c of + Disj p q + | p == x' && q == c -> Disj x' y' + | p == c && q == x' -> Disj y' x' + | otherwise -> error "bug" + dx'c -> conj dx'c (disj x' r) + -- single bounded conj tree, irreducible conj pair + (x'@(Conj (Anchor opa pta) _), y'@(Conj (Anchor opb ptb) (Anchor _ _))) + | pta < ptb && not (fr opa) && not (fl opb) -> Disj x' y' + | otherwise -> disj y' x' + -- irreducible conj pair, double bounded conj tree + (x'@(Conj (Anchor _ _) (Anchor _ _)), y'@(Conj bounds@(Conj _ _) r)) -> case disj x' bounds of + Disj p q + | p == x' && q == bounds -> Disj x' y' + | p == bounds && q == x' -> Disj y' x' + dx'bounds -> conj dx'bounds (disj x' r) + -- double bounded conj tree, irreducible conj pair + (x'@(Conj (Conj _ (Anchor _ pta)) _), y'@(Conj (Anchor opb ptb) (Anchor _ _))) + | ptb > pta && not (fl opb) -> Disj x' y' + | otherwise -> disj y' x' + -- single bounded conj tree, single bounded conj tree + (x'@(Conj xBound@(Anchor _ _) xNeqs), y'@(Conj yBound@(Anchor _ _) yNeqs)) -> + case disj xBound yBound of + Disj p q + | p == xBound && q == yBound -> Disj x' y' + | p == yBound && q == xBound -> Disj y' x' + | otherwise -> error "bug" + dxy -> conj (conj dxy (disj xNeqs yNeqs)) (conj (disj xBound yNeqs) (disj yBound xNeqs)) + -- single bounded conj tree, double bounded conj tree + (x'@(Conj xBound@(Anchor _ _) xNeqs), y'@(Conj yBounds@(Conj (Anchor _ _) (Anchor _ _)) yNeqs)) -> + case disj xBound yBounds of + Disj p q + | p == xBound && q == yBounds -> Disj x' y' + | p == yBounds && q == xBound -> Disj y' x' + | otherwise -> error "bug" + dxy -> conj (conj dxy (disj xNeqs yNeqs)) (conj (disj xBound yNeqs) (disj yBounds xNeqs)) + -- double bounded conj tree, single bounded conj tree + (x'@(Conj xBounds@(Conj (Anchor _ _) (Anchor _ _)) xNeqs), y'@(Conj yBound@(Anchor _ _) yNeqs)) -> + case disj xBounds yBound of + Disj p q + | p == xBounds && q == yBound -> Disj x' y' + | p == yBound && q == xBounds -> Disj y' x' + | otherwise -> error "bug" + dxy -> conj (conj dxy (disj xNeqs yNeqs)) (conj (disj xBounds yNeqs) (disj yBound xNeqs)) + -- double bounded conj tree, double bounded conj tree + (x'@(Conj xBounds@(Conj (Anchor _ _) (Anchor _ _)) xNeqs), y'@(Conj yBounds@(Conj (Anchor _ _) (Anchor _ _)) yNeqs)) -> + case disj xBounds yBounds of + Disj p q + | p == xBounds && q == yBounds -> Disj x' y' + | p == yBounds && q == xBounds -> Disj y' x' + | otherwise -> error "bug" + dxy -> conj (conj dxy (disj xNeqs yNeqs)) (conj (disj xBounds yNeqs) (disj yBounds xNeqs)) + (x', y') -> error [i|missing disj case: #{orig} -> #{x'}, #{y'}|] exactly :: Version -> VersionRange @@ -805,24 +1103,21 @@ wildcard = hyphen :: Atto.Parser VersionRange hyphen = liftA2 (range True True) parseVersion (Atto.skipSpace *> Atto.char '-' *> Atto.skipSpace *> parseVersion) +-- data ConjNF = ConjNF +-- { conjNFLower :: Maybe (Version, Bool) +-- , conjNFUpper :: Maybe (Version, Bool) +-- , conjNFExclusions :: [Version] +-- } +-- deriving (Eq) -data ConjNF = ConjNF - { conjNFLower :: Maybe (Version, Bool) - , conjNFUpper :: Maybe (Version, Bool) - , conjNFExclusions :: [Version] - } - deriving (Eq) +-- isValidConjNF :: ConjNF -> Bool +-- isValidConjNF = \case +-- ConjNF (Just (v0, i0)) (Just (v1, i1)) ex -> v0 < v1 && all ((> v0) <&&> (< v1)) ex +-- ConjNF Nothing (Just (v1, i1)) ex -> all (< v1) ex +-- ConjNF (Just (v0, i0)) Nothing ex -> all (> v0) ex +-- ConjNF Nothing Nothing ex -> _ - -isValidConjNF :: ConjNF -> Bool -isValidConjNF = \case - ConjNF (Just (v0, i0)) (Just (v1, i1)) ex -> v0 < v1 && all ((> v0) <&&> (< v1)) ex - ConjNF Nothing (Just (v1, i1)) ex -> all (< v1) ex - ConjNF (Just (v0, i0)) Nothing ex -> all (> v0) ex - ConjNF Nothing Nothing ex -> _ - - -data DisjNF = DisjNF - { disjNFLower :: Maybe (Version, Bool) - , disjNFUpper :: Maybe (Version, Bool) - } +-- data DisjNF = DisjNF +-- { disjNFLower :: Maybe (Version, Bool) +-- , disjNFUpper :: Maybe (Version, Bool) +-- } diff --git a/test/Lib/Types/EmverProp.hs b/test/Lib/Types/EmverProp.hs index ca1f019..5c40cbf 100644 --- a/test/Lib/Types/EmverProp.hs +++ b/test/Lib/Types/EmverProp.hs @@ -4,6 +4,7 @@ module Lib.Types.EmverProp where import Startlude hiding ( Any, + check, filter, reduce, ) @@ -33,6 +34,22 @@ rangeGen = shrink rangeShrink $ choice [pure None, pure Any, anchorGen, disjGen, rangeShrink _ = [] +rangeGenNonTrivial :: MonadGen m => m VersionRange +rangeGenNonTrivial = + shrink rangeShrink $ + choice + [ anchorGen + , anchorGen + , anchorGen + , liftA2 Conj rangeGenNonTrivial rangeGenNonTrivial + , liftA2 Disj rangeGenNonTrivial rangeGenNonTrivial + ] + where + rangeShrink (Conj a b) = [a, b] + rangeShrink (Disj a b) = [a, b] + rangeShrink _ = [] + + anchorGen :: MonadGen m => m VersionRange anchorGen = do c <- element [LT, EQ, GT] @@ -202,9 +219,37 @@ prop_reduceDisjAnchor = property $ do obs <|| reduce (Disj a b) === obs <|| Disj a b +prop_reduceConjNone :: Property +prop_reduceConjNone = property $ do + a <- forAll anchorGen + reduce (Conj a None) === None + reduce (Conj None a) === None + + +prop_reduceConjAny :: Property +prop_reduceConjAny = property $ do + a <- forAll anchorGen + reduce (Conj a Any) === reduce a + reduce (Conj Any a) === reduce a + + +prop_reduceDisjNone :: Property +prop_reduceDisjNone = property $ do + a <- forAll anchorGen + reduce (Disj a None) === reduce a + reduce (Disj None a) === reduce a + + +prop_reduceDisjAny :: Property +prop_reduceDisjAny = property $ do + a <- forAll anchorGen + reduce (Disj a Any) === Any + reduce (Disj Any a) === Any + + prop_reduceTerminates :: Property -prop_reduceTerminates = withTests 1000 . property $ do - a <- forAll $ filter ((<= 100) . nodes) rangeGen +prop_reduceTerminates = withTests 1_000_000 . property $ do + a <- forAll $ filter ((<= 100) . nodes) rangeGenNonTrivial b <- lift $ timeout 100_000 (pure $! reduce a) case b of Nothing -> failure @@ -212,17 +257,18 @@ prop_reduceTerminates = withTests 1000 . property $ do prop_reduceIdentity :: Property -prop_reduceIdentity = withTests 1000 . property $ do - a <- forAll $ filter (((>= 3) <&&> (<= 100)) . nodes) rangeGen - obs <- forAll versionGen +prop_reduceIdentity = withTests 1_000_000 . withDiscards 2000 . property $ do + a <- forAll $ filter (((>= 5) <&&> (<= 100)) . nodes) rangeGenNonTrivial let b = reduce a + annotateShow b unless (b /= a) Test.discard - obs <|| a === obs <|| b + obs <- replicateM 20 $ forAll versionGen + for_ obs $ \ob -> ob <|| a === ob <|| b prop_reduceIdempotence :: Property -prop_reduceIdempotence = withTests 1000 . property $ do - a <- forAll $ filter (((>= 3) <&&> (<= 100)) . nodes) rangeGen +prop_reduceIdempotence = withTests 1_000_000 . property $ do + a <- forAll $ filter (((>= 3) <&&> (<= 100)) . nodes) rangeGenNonTrivial let b = reduce a annotateShow b let c = reduce b @@ -269,5 +315,17 @@ isConjNF = \case _ -> False +prop_reduceDisjTreeNormalForm :: Property +prop_reduceDisjTreeNormalForm = property $ do + a <- forAll rangeGenNonTrivial + let b = reduce a + annotateShow b + assert $ isDisjNF b + + +isDisjNF :: VersionRange -> Bool +isDisjNF = const True -- TODO + + tests :: IO Bool -tests = checkParallel $ $$discover +tests = checkSequential $ $$discover