{-# Language TypeApplications    #-}
{-# Language AllowAmbiguousTypes #-}
{-# Language ConstraintKinds     #-}
{-# Language DataKinds           #-}
{-# Language KindSignatures      #-}
{-# Language RankNTypes          #-}
{-# Language Safe                #-}

module Data.Order.Topology (
  -- * Left and right separated Alexandrov topologies
    Kan(..)
  , Open()
  , lower
  , upper
  , omap
  -- ** The left (/Inf/) topology
  , Inf
  , inf
  , (.?)
  , filterL
  -- ** The right (/Sup/) topology
  , Sup
  , sup
  , (?.)
  , filterR
) where

import safe Control.Applicative (liftA2)
import safe Data.Connection.Conn
import safe Data.Semigroup.Join
import safe Data.Lattice
import safe Data.Order
import safe Data.Universe.Class (Finite(..))
import safe Prelude hiding (Bounded, Eq(..), Ord(..))

-- | A pointed open set in a separated left or right < https://en.wikipedia.org/wiki/Alexandrov_topology Alexandrov topology >.
--
data Open (k :: Kan) a = Open (a -> Bool) a a

-- | The base point of a pointed lower set (i.e. an 'Inf').
--
lower :: Open k a -> a
lower (Open _ x _) = x

-- | The base point of a pointed upper set (i.e. a 'Sup').
-- 
upper :: Open k a -> a
upper (Open _ _ y) = y

-- | Map over a pointed open set in either topology.
--
omap :: Trip a b -> Open k a -> Open k b
omap (Conn f g h) (Open p x y) = Open (p . g) (h x) (f y)

-- Up-set ideals
up :: Preorder a => a -> a -> Bool
up a = (a <~)

-- Up-set anti-ideals
up' :: Preorder a => a -> a -> Bool
up' a = fmap not (a <~)

-- Down-set ideals
down :: Preorder a => a -> a -> Bool
down a = (<~ a)

-- Down-set anti-ideals
down' :: Preorder a => a -> a -> Bool
down' a = fmap not (<~ a)

---------------------------------------------------------------------
-- Inf
---------------------------------------------------------------------

type Inf = Open 'L


-- | Create an upper set: \( X_\geq(x) = \{ y \in X | y \geq x \} \)
--
-- Upper sets are the < https://en.wikipedia.org/wiki/Ideal_(order_theory) open sets > of the left Alexandrov topology.
--
-- This function is monotone:
--
-- > x <~ y <=> inf x <~ inf y
--
-- by the Yoneda lemma for preorders.
--
inf :: UpperBounded a => a -> Inf a
inf a = Open (const True) a top

infix 4 .?

-- | Check for membership in an /Inf/.
--
(.?) :: Preorder a => Inf a -> a -> Bool
(.?) (Open f l _) a = f a && down a l


infixr 5 `filterL`

-- | Filter an /Inf/ with an anti-filter.
--
-- The resulting set is open in the separated left Alexandrov topology.
--
-- Intersecting with an incomparable element cuts out everything
-- larger than its join with the base point:
--
-- >>> p = inf pi :: Inf Double
-- >>> p .? 1/0
-- True
-- >>> filterL (0/0) p .? 1/0
-- False
--
-- An example w/ the set inclusion lattice:
-- >>> x = Set.fromList [6,40] :: Set.Set Word8
-- >>> y = Set.fromList [1,6,9] :: Set.Set Word8
-- >>> z = filterL y $ inf x
-- fromList [6,40] ... fromList [1,6,9,40]
-- >>> z .? Set.fromList [1,6,40]
-- True
-- >>> z .? Set.fromList [6,9,40]
-- True
-- >>> z .? Set.fromList [1,6,9,40]
-- False
--
filterL :: Lattice a => a -> Inf a -> Inf a
filterL a p@(Open f l u) = if down' l a then Open (f /\ up' a) l (glb l a u) else p

---------------------------------------------------------------------
-- Sup
---------------------------------------------------------------------

type Sup = Open 'R

-- | Create a lower set \( X_\leq(x) = \{ y \in X | y \leq x \} \)
--
-- Lower sets are the <https://en.wikipedia.org/wiki/Filter_(mathematics) open sets > of the right Alexandrov topology.
--
-- This function is antitone:
--
-- > x <~ y <=> sup x >~ sup y
--
-- by the Yoneda lemma for preorders.
--
sup :: LowerBounded a => a -> Sup a
sup a = Open (const True) bottom a

infix 4 ?.

-- | Check for membership in a /Sup/.
--
(?.) :: Preorder a => a -> Sup a -> Bool
(?.) a (Open f _ u) = f a && up a u

infixl 5 `filterR`

-- | Filter a /Sup/ with an anti-ideal.
-- 
-- The resulting set is open in the separated right Alexandrov topology.
--
-- >>> p = sup pi :: Sup Double
-- >>> -1/0 ?. p
-- True
-- >>> -1/0 ?. filterR (0/0) p
-- False
--
filterR :: Lattice a => a -> Sup a -> Sup a
filterR a p@(Open f l u) = if up' u a then Open (f /\ down' a) (lub l a u) u else p

---------------------------------------------------------------------
-- Internal
---------------------------------------------------------------------


--deriving instance Eq a => Eq (Open k a)
instance Show a => Show (Open k a) where
  show (Open _ l r) = show l ++ " ... " ++ show r

-- |
-- Note that '~~' is strictly weaker than '==', as it ignores the 
-- location of the base point.
instance Finite a => Preorder (Open k a) where
  (Open f _ _) <~ (Open g _ _) = f <~ g

instance Lattice a => Semigroup (Join (Inf a)) where
  (<>) = liftA2 joinInf

instance UpperBounded a => Monoid (Join (Inf a)) where
  mempty = pure $ inf top

instance Lattice a => Semigroup (Meet (Inf a)) where
  (<>) = liftA2 meetInf

instance Bounded a => Monoid (Meet (Inf a)) where
  mempty = pure $ inf bottom


joinInf :: Lattice a => Inf a -> Inf a -> Inf a
joinInf (Open f1 l1 r1) (Open f2 l2 r2) = Open (f1 \/ f2) (l1 /\ l2) (r1 \/ r2)

meetInf :: Lattice a => Inf a -> Inf a -> Inf a
meetInf (Open f1 l1 r1) (Open f2 l2 r2) = Open (f1 /\ f2) (l1 \/ l2) (r1 /\ r2)

instance (Finite a, Lattice a) => Lattice (Inf a)
instance (Finite a, Bounded a) => Bounded (Inf a)


instance Lattice a => Semigroup (Join (Sup a)) where
  (<>) = liftA2 joinSup

instance LowerBounded a => Monoid (Join (Sup a)) where
  mempty = pure $ sup bottom

instance Lattice a => Semigroup (Meet (Sup a)) where
  (<>) = liftA2 meetSup

instance Bounded a => Monoid (Meet (Sup a)) where
  mempty = pure $ sup top

joinSup :: Lattice a => Sup a -> Sup a -> Sup a
joinSup (Open f1 l1 r1) (Open f2 l2 r2) = Open (f1 \/ f2) (l1 \/ l2) (r1 /\ r2)

meetSup :: Lattice a => Sup a -> Sup a -> Sup a
meetSup (Open f1 l1 r1) (Open f2 l2 r2) = Open (f1 /\ f2) (l1 /\ l2) (r1 \/ r2)

instance (Finite a, Lattice a) => Lattice (Sup a)
instance (Finite a, Bounded a) => Bounded (Sup a)

{- 

instance (Finite a, Bounded a) => Heyting (Sup a)
instance (Finite a, Bounded a) => Heyting (Sup a)

instance (Finite a, Bounded a) => Heyting (Inf a) where
  neg (Predicate f) = Predicate $ \a -> neg (f a)
  (Predicate f) <=> (Predicate g) = Predicate $ \a -> f a <=> g a

instance (Finite a, Bounded a) => Quantale (Meet (Inf a)) where
  (\\) = liftA2 impliesOpen
  (//) = flip (\\)

instance (Finite a, Bounded a) => Quantale (Meet (Sup a)) where
  (\\) = liftA2 impliesOpen
  (//) = flip (\\)

negOpen (Open f x) = Open $ \a -> neg (f a)
iffOpen (Open f x) (Open g x) = Open $ \a -> f a <=> g a

impliesOpen :: Bounded a => Open k a -> Open k a -> Open k a
impliesOpen (Open f x) (Open g y) = Open (\a -> f a <= g a) (if x > y then y else top)
-}