{-# LANGUAGE GADTs, TypeFamilies, PatternSynonyms, ScopedTypeVariables, RankNTypes, TypeOperators #-}
module Data.Category.Preorder where

import Prelude hiding ((.), id, Functor)

import Data.Category
import Data.Category.Limit
import Data.Category.CartesianClosed
import Data.Category.Functor
import Data.Category.Adjunction
import Data.Category.Enriched
import Data.Category.Enriched.Functor
import Data.Category.Enriched.Limit hiding (HasEnds(..))

data Preorder a x y where
  (:<=:) :: a -> a -> Preorder a x y

pattern Obj :: a -> Preorder a x y
pattern Obj a <- a :<=: _ where
  Obj a = a :<=: a
{-# COMPLETE Obj #-} -- Note: only complete for identity arrows `Obj Preorder a`

unObj :: Obj (Preorder a) x -> a
unObj (Obj a) = a

instance Eq a => Category (Preorder a) where
  src (s :<=: _) = Obj s
  tgt (_ :<=: t) = Obj t
  (b :<=: c) . (a :<=: b') = if b == b' then a :<=: c else error "Invalid composition"

instance (Eq a, Bounded a) => HasInitialObject (Preorder a) where
  type InitialObject (Preorder a) = ()
  initialObject = Obj minBound
  initialize (Obj a) = minBound :<=: a

instance (Eq a, Bounded a) => HasTerminalObject (Preorder a) where
  type TerminalObject (Preorder a) = ()
  terminalObject = Obj maxBound
  terminate (Obj a) = a :<=: maxBound

instance Ord a => HasBinaryProducts (Preorder a) where
  type BinaryProduct (Preorder a) x y = ()
  proj1 (Obj a) (Obj b) = min a b :<=: a
  proj2 (Obj a) (Obj b) = min a b :<=: b
  (a :<=: x) &&& (_a :<=: y) = a :<=: min x y

instance Ord a => HasBinaryCoproducts (Preorder a) where
  type BinaryCoproduct (Preorder a) x y = ()
  inj1 (Obj a) (Obj b) = a :<=: max a b
  inj2 (Obj a) (Obj b) = b :<=: max a b
  (x :<=: a) ||| (y :<=: _a) = max x y :<=: a

-- | `ordExp a b` is the largest x such that min x a <= b
ordExp :: (Ord a, Bounded a) => a -> a -> a
ordExp a b = if a <= b then maxBound else b

instance (Ord a, Bounded a) => CartesianClosed (Preorder a) where
  type Exponential (Preorder a) x y = ()
  apply (Obj a) (Obj b) = min (ordExp a b) a :<=: b
  tuple (Obj a) (Obj b) = b :<=: ordExp a (min a b)
  (z1 :<=: z2) ^^^ (y2 :<=: y1) = ordExp y1 z1 :<=: ordExp y2 z2


class Category k => EnumObjs k where
  enumObjs :: (forall a. Obj k a -> r) -> [r]

glb :: (Ord a, Bounded a) => [a] -> a
glb [] = maxBound
glb xs = minimum xs


type End' t = ()
end
  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)
  => t -> Obj (Preorder a) (End' t)
end t = Obj $ glb (enumObjs (\a -> unObj (getSelf (t %% (EOp a :<>: a)))))

endCounit
  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)
  => t -> Obj k b -> Preorder a (End' t) (t :%% (b, b))
endCounit t a = unObj (end t) :<=: unObj (getSelf (t %% (EOp a :<>: a)))

endFactorizer
  :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a)
  => t -> Obj (Preorder a) x -> (forall b. Obj k b -> Preorder a x (t :%% (b, b))) -> Preorder a x (End' t)
endFactorizer _ (Obj x) f = x :<=: glb (enumObjs (\b -> case f b of _ :<=: tbb -> tbb))


data Floor = Floor
instance Functor Floor where
  type Dom Floor = Preorder Double
  type Cod Floor = Preorder Integer
  type Floor :% a = ()
  Floor % (a :<=: b) = floor a :<=: floor b

data FromInteger = FromInteger
instance Functor FromInteger where
  type Dom FromInteger = Preorder Integer
  type Cod FromInteger = Preorder Double
  type FromInteger :% a = ()
  FromInteger % (a :<=: b) = fromInteger a :<=: fromInteger b

floorGaloisConnection :: Adjunction (Preorder Double) (Preorder Integer) FromInteger Floor
floorGaloisConnection = mkAdjunction FromInteger Floor
  (\(Obj a) (_fromIntegerA :<=: b) -> a :<=: floor b)
  (\(Obj b) (a :<=: _floorB) -> fromInteger a :<=: b)