{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE Trustworthy                #-}
{-# LANGUAGE UndecidableInstances       #-}
module Kleene.Equiv where

import Algebra.Lattice
       (BoundedJoinSemiLattice (..), BoundedMeetSemiLattice (..), Lattice (..),
       joinLeq)
import Algebra.PartialOrd (PartialOrd (..))
import Data.Semigroup     (Semigroup (..))

import Kleene.Classes
import Kleene.Internal.Pretty

-- $setup
-- >>> import Kleene.RE (RE)
-- >>> import Kleene.Classes
-- >>> import Algebra.PartialOrd (leq)
-- >>> import Data.Semigroup (Semigroup (..))

-- | Regular-expressions for which '==' is 'equivalent'.
--
-- >>> let re1 = star "a" <> "a" :: RE Char
-- >>> let re2 = "a" <> star "a" :: RE Char
--
-- >>> re1 == re2
-- False
--
-- >>> Equiv re1 == Equiv re2
-- True
--
-- 'Equiv' is also a 'PartialOrd' (but not 'Ord'!)
--
-- >>> Equiv "a" `leq` Equiv (star "a" :: RE Char)
-- True
--
-- Not all regular expessions are 'comparable':
--
-- >>> let reA = Equiv "a" :: Equiv RE Char
-- >>> let reB = Equiv "b" :: Equiv RE Char
-- >>> (leq reA reB, leq reB reA)
-- (False,False)
--
newtype Equiv r c = Equiv (r c)
  deriving (Int -> Equiv r c -> ShowS
[Equiv r c] -> ShowS
Equiv r c -> String
(Int -> Equiv r c -> ShowS)
-> (Equiv r c -> String)
-> ([Equiv r c] -> ShowS)
-> Show (Equiv r c)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (r :: * -> *) c. Show (r c) => Int -> Equiv r c -> ShowS
forall (r :: * -> *) c. Show (r c) => [Equiv r c] -> ShowS
forall (r :: * -> *) c. Show (r c) => Equiv r c -> String
$cshowsPrec :: forall (r :: * -> *) c. Show (r c) => Int -> Equiv r c -> ShowS
showsPrec :: Int -> Equiv r c -> ShowS
$cshow :: forall (r :: * -> *) c. Show (r c) => Equiv r c -> String
show :: Equiv r c -> String
$cshowList :: forall (r :: * -> *) c. Show (r c) => [Equiv r c] -> ShowS
showList :: [Equiv r c] -> ShowS
Show, NonEmpty (Equiv r c) -> Equiv r c
Equiv r c -> Equiv r c -> Equiv r c
(Equiv r c -> Equiv r c -> Equiv r c)
-> (NonEmpty (Equiv r c) -> Equiv r c)
-> (forall b. Integral b => b -> Equiv r c -> Equiv r c)
-> Semigroup (Equiv r c)
forall b. Integral b => b -> Equiv r c -> Equiv r c
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall (r :: * -> *) c.
Semigroup (r c) =>
NonEmpty (Equiv r c) -> Equiv r c
forall (r :: * -> *) c.
Semigroup (r c) =>
Equiv r c -> Equiv r c -> Equiv r c
forall (r :: * -> *) c b.
(Semigroup (r c), Integral b) =>
b -> Equiv r c -> Equiv r c
$c<> :: forall (r :: * -> *) c.
Semigroup (r c) =>
Equiv r c -> Equiv r c -> Equiv r c
<> :: Equiv r c -> Equiv r c -> Equiv r c
$csconcat :: forall (r :: * -> *) c.
Semigroup (r c) =>
NonEmpty (Equiv r c) -> Equiv r c
sconcat :: NonEmpty (Equiv r c) -> Equiv r c
$cstimes :: forall (r :: * -> *) c b.
(Semigroup (r c), Integral b) =>
b -> Equiv r c -> Equiv r c
stimes :: forall b. Integral b => b -> Equiv r c -> Equiv r c
Semigroup, Semigroup (Equiv r c)
Equiv r c
Semigroup (Equiv r c) =>
Equiv r c
-> (Equiv r c -> Equiv r c -> Equiv r c)
-> ([Equiv r c] -> Equiv r c)
-> Monoid (Equiv r c)
[Equiv r c] -> Equiv r c
Equiv r c -> Equiv r c -> Equiv r c
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall (r :: * -> *) c. Monoid (r c) => Semigroup (Equiv r c)
forall (r :: * -> *) c. Monoid (r c) => Equiv r c
forall (r :: * -> *) c. Monoid (r c) => [Equiv r c] -> Equiv r c
forall (r :: * -> *) c.
Monoid (r c) =>
Equiv r c -> Equiv r c -> Equiv r c
$cmempty :: forall (r :: * -> *) c. Monoid (r c) => Equiv r c
mempty :: Equiv r c
$cmappend :: forall (r :: * -> *) c.
Monoid (r c) =>
Equiv r c -> Equiv r c -> Equiv r c
mappend :: Equiv r c -> Equiv r c -> Equiv r c
$cmconcat :: forall (r :: * -> *) c. Monoid (r c) => [Equiv r c] -> Equiv r c
mconcat :: [Equiv r c] -> Equiv r c
Monoid, Lattice (Equiv r c)
Equiv r c
Lattice (Equiv r c) =>
Equiv r c -> BoundedJoinSemiLattice (Equiv r c)
forall a. Lattice a => a -> BoundedJoinSemiLattice a
forall (r :: * -> *) c.
BoundedJoinSemiLattice (r c) =>
Lattice (Equiv r c)
forall (r :: * -> *) c. BoundedJoinSemiLattice (r c) => Equiv r c
$cbottom :: forall (r :: * -> *) c. BoundedJoinSemiLattice (r c) => Equiv r c
bottom :: Equiv r c
BoundedJoinSemiLattice, Lattice (Equiv r c)
Equiv r c
Lattice (Equiv r c) =>
Equiv r c -> BoundedMeetSemiLattice (Equiv r c)
forall a. Lattice a => a -> BoundedMeetSemiLattice a
forall (r :: * -> *) c.
BoundedMeetSemiLattice (r c) =>
Lattice (Equiv r c)
forall (r :: * -> *) c. BoundedMeetSemiLattice (r c) => Equiv r c
$ctop :: forall (r :: * -> *) c. BoundedMeetSemiLattice (r c) => Equiv r c
top :: Equiv r c
BoundedMeetSemiLattice, Equiv r c -> Equiv r c -> Equiv r c
(Equiv r c -> Equiv r c -> Equiv r c)
-> (Equiv r c -> Equiv r c -> Equiv r c) -> Lattice (Equiv r c)
forall a. (a -> a -> a) -> (a -> a -> a) -> Lattice a
forall (r :: * -> *) c.
Lattice (r c) =>
Equiv r c -> Equiv r c -> Equiv r c
$c\/ :: forall (r :: * -> *) c.
Lattice (r c) =>
Equiv r c -> Equiv r c -> Equiv r c
\/ :: Equiv r c -> Equiv r c -> Equiv r c
$c/\ :: forall (r :: * -> *) c.
Lattice (r c) =>
Equiv r c -> Equiv r c -> Equiv r c
/\ :: Equiv r c -> Equiv r c -> Equiv r c
Lattice, Equiv r c -> String
Equiv r c -> ShowS
(Equiv r c -> String) -> (Equiv r c -> ShowS) -> Pretty (Equiv r c)
forall a. (a -> String) -> (a -> ShowS) -> Pretty a
forall (r :: * -> *) c. Pretty (r c) => Equiv r c -> String
forall (r :: * -> *) c. Pretty (r c) => Equiv r c -> ShowS
$cpretty :: forall (r :: * -> *) c. Pretty (r c) => Equiv r c -> String
pretty :: Equiv r c -> String
$cprettyS :: forall (r :: * -> *) c. Pretty (r c) => Equiv r c -> ShowS
prettyS :: Equiv r c -> ShowS
Pretty)

instance Equivalent c (r c) => Eq (Equiv r c) where
    == :: Equiv r c -> Equiv r c -> Bool
(==) = Equiv r c -> Equiv r c -> Bool
forall c k. Equivalent c k => k -> k -> Bool
equivalent

-- | \(a \preceq b := a \lor b = b \)
instance (Lattice (r c), Equivalent c (r c)) => PartialOrd (Equiv r c) where
    leq :: Equiv r c -> Equiv r c -> Bool
leq = Equiv r c -> Equiv r c -> Bool
forall a. (Eq a, Lattice a) => a -> a -> Bool
joinLeq

deriving instance Kleene       (r c) => Kleene       (Equiv r c)
deriving instance CharKleene c (r c) => CharKleene c (Equiv r c)
deriving instance Derivate   c (r c) => Derivate   c (Equiv r c)
deriving instance Match      c (r c) => Match      c (Equiv r c)
deriving instance Equivalent c (r c) => Equivalent c (Equiv r c)
deriving instance Complement c (r c) => Complement c (Equiv r c)