{-# LANGUAGE UndecidableInstances #-}
module Main where
import Algebra.Lattice (Lattice (..))
import Algebra.Lattice.Levitated (Levitated (..))
import Control.Applicative
import Control.Monad
import Data.Interval (
Interval,
pattern (:<->:),
pattern (:<-|:),
pattern (:<>:),
pattern (:<|:),
pattern (:|->:),
pattern (:|-|:),
pattern (:|>:),
pattern (:||:),
)
import Data.Interval qualified as Interval
import Data.Interval.Borel (Borel)
import Data.Interval.Borel qualified as Borel
import Data.Interval.Layers qualified as Layers
import Data.Semigroup
import GHC.TypeNats
import Test.Hspec
import Test.QuickCheck
import Text.Parsec (sepBy, try)
import Text.Parsec.Char (char, digit, spaces, string)
import Text.Parsec.Text (Parser)
import Text.ParserCombinators.Parsec (choice)
type family Ints (n :: Nat) x where
Ints 0 x = x
Ints n x = Int -> Ints (n - 1) x
main :: IO ()
main = hspec do
describe "smart constructors" do
it "orient finite intervals" do
property @(Ints 2 _) \x y -> when (x > y) do
(x :<>: y) `shouldBe` (y :<>: x)
(x :|>: y) `shouldBe` (y :<|: x)
(x :<|: y) `shouldBe` (y :|>: x)
(x :||: y) `shouldBe` (y :||: x)
(Levitate x :<->: Levitate y) `shouldBe` (Levitate y :<->: Levitate x)
(Levitate x :|->: Levitate y) `shouldBe` (Levitate y :<-|: Levitate x)
(Levitate x :<-|: Levitate y) `shouldBe` (Levitate y :|->: Levitate x)
(Levitate x :|-|: Levitate y) `shouldBe` (Levitate y :|-|: Levitate x)
it "orient infinite intervals" do
(Top :<->: Bottom) `shouldBe` (Bottom :<->: Top :: Interval Int)
(Top :|->: Bottom) `shouldBe` (Bottom :<-|: Top :: Interval Int)
(Top :<-|: Bottom) `shouldBe` (Bottom :|->: Top :: Interval Int)
(Top :|-|: Bottom) `shouldBe` (Bottom :|-|: Top :: Interval Int)
it "close point intervals" do
property @(Int -> _) \x -> do
(x :<>: x) `shouldBe` (x :||: x)
(x :|>: x) `shouldBe` (x :||: x)
(x :<|: x) `shouldBe` (x :||: x)
(x :||: x) `shouldBe` (x :||: x)
(Levitate x :<->: Levitate x) `shouldBe` (Levitate x :|-|: Levitate x)
(Levitate x :|->: Levitate x) `shouldBe` (Levitate x :|-|: Levitate x)
(Levitate x :<-|: Levitate x) `shouldBe` (Levitate x :|-|: Levitate x)
(Levitate x :|-|: Levitate x) `shouldBe` (Levitate x :|-|: Levitate x)
describe "Borel intervals" do
it "(<>) is commutative" do
property @(Ints 4 _) \a b x y -> do
let abxy = Borel.singleton (a :<>: b) <> Borel.singleton (x :<>: y)
xyab = Borel.singleton (x :<>: y) <> Borel.singleton (a :<>: b)
abxy `shouldBe` xyab
it "(<>) is associative" do
property @(Ints 6 _) \a b m n x y -> do
let ab = Borel.singleton (a :<>: b)
mn = Borel.singleton (m :<>: n)
xy = Borel.singleton (x :<>: y)
(ab <> mn) <> xy `shouldBe` ab <> (mn <> xy)
describe "Layers" do
it "(<>) is associative" do
property @(Ints 9 _) \a b c d e f x y z -> do
let abx = Layers.singleton (a :<>: b) (Sum x)
cdy = Layers.singleton (c :||: d) (Sum y)
efz = Layers.singleton (e :<>: f) (Sum z)
(abx <> cdy) <> efz `shouldBe` abx <> (cdy <> efz)
newtype Version = Version [Int]
deriving (Eq, Ord, Show)
version :: Parser Version
version = Version <$> sepBy (read <$> many digit) (char '.')
data Tk
= TkAnd
| TkOr
| TkBorel (Borel Version)
| TkOpen
| TkClose
tk :: Parser Tk
tk =
choice
[ try tkAnd
, try tkOr
, try do liftM2 ((TkBorel . Borel.singleton) .) tkCmp tkVersion
, try tkOpen
, try tkClose
]
where
tkAnd = TkAnd <$ (spaces *> string "&&" <* spaces)
tkOr = TkOr <$ (spaces *> string "||" <* spaces)
tkVersion = spaces *> version <* spaces
tkCmp =
choice
[ (Bottom :<-|:) . Levitate <$ try do string "<="
, (Bottom :<->:) . Levitate <$ try do string "<"
, (:|->: Top) . Levitate <$ try do string ">="
, (:<->: Top) . Levitate <$ try do string ">"
, Interval.point <$ try do string "=="
]
tkOpen = TkOpen <$ (spaces *> string "(" <* spaces)
tkClose = TkClose <$ (spaces *> string ")" <* spaces)
foldTk :: [Tk] -> Borel Version
foldTk = \case
[TkBorel b] -> b
TkOpen : TkBorel b0 : TkAnd : TkBorel b1 : TkClose : rest ->
foldTk do TkBorel (b0 /\ b1) : rest
TkOpen : TkBorel b0 : TkOr : TkBorel b1 : TkClose : rest ->
foldTk do TkBorel (b0 \/ b1) : rest
TkBorel b0 : TkAnd : TkOpen : rest ->
foldTk do TkBorel b0 : TkAnd : [TkBorel (foldTk (TkOpen : rest))]
TkBorel b0 : TkOr : TkOpen : rest ->
foldTk do TkBorel b0 : TkOr : [TkBorel (foldTk (TkOpen : rest))]
TkBorel b0 : TkAnd : TkBorel b1 : rest -> foldTk do TkBorel (b0 /\ b1) : rest
TkBorel b0 : TkOr : TkBorel b1 : rest -> foldTk do TkBorel (b0 \/ b1) : rest
TkOpen : TkBorel b : TkClose : rest -> foldTk do TkBorel b : rest
_ -> error "malformed bounds"
versionBounds :: Parser (Borel Version)
versionBounds = foldTk <$> many tk
-- >>> Text.Parsec.parse versionBounds "" ">= 2.0.0 && <3"
-- Right (Borel (fromList [(Version [2,0,0] :|>: Version [3])]))
-- >>> Text.Parsec.parse versionBounds "" ">= 4"
-- Right (Borel (fromList [(Levitate (Version [4]) :|->: Top)]))
-- >>> Text.Parsec.parse versionBounds "" "(>= 1.2 && <3) || (>= 4.0 && < 5)"
-- Right (Borel (fromList [(Version [1,2] :|>: Version [3]),(Version [4,0] :|>: Version [5])]))
-- >>> Text.Parsec.parse versionBounds "" "(>= 1.2 && <3) || (>= 2.0 && < 5)"
-- Right (Borel (fromList [(Version [1,2] :|>: Version [5])]))