{-# LANGUAGE UndecidableInstances #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  HGeometry.Ord.Dynamic
-- Copyright   :  (C) Frank Staals
-- License     :  see the LICENSE file
-- Maintainer  :  Frank Staals
--------------------------------------------------------------------------------
module HGeometry.Ord.Dynamic where

import Data.Kind
import Data.Proxy
import Data.Reflection
import Unsafe.Coerce

--------------------------------------------------------------------------------

-- Implementation from
-- https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection

-- | Values of type '@a@' in our dynamically constructed 'Ord' instance
newtype O (s :: Type) (a :: Type) = O { forall s a. O s a -> a
runO :: a } deriving (Int -> O s a -> ShowS
[O s a] -> ShowS
O s a -> String
(Int -> O s a -> ShowS)
-> (O s a -> String) -> ([O s a] -> ShowS) -> Show (O s a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s a. Show a => Int -> O s a -> ShowS
forall s a. Show a => [O s a] -> ShowS
forall s a. Show a => O s a -> String
$cshowsPrec :: forall s a. Show a => Int -> O s a -> ShowS
showsPrec :: Int -> O s a -> ShowS
$cshow :: forall s a. Show a => O s a -> String
show :: O s a -> String
$cshowList :: forall s a. Show a => [O s a] -> ShowS
showList :: [O s a] -> ShowS
Show)

-- | An Ord Dictionary
newtype OrdDict a = OrdDict { forall a. OrdDict a -> a -> a -> Ordering
compare_ :: a -> a -> Ordering }

instance Reifies s (OrdDict a) => Eq (O s a) where
  (O a
l) == :: O s a -> O s a -> Bool
== (O a
r) = let cmp :: a -> a -> Ordering
cmp = OrdDict a -> a -> a -> Ordering
forall a. OrdDict a -> a -> a -> Ordering
compare_ (OrdDict a -> a -> a -> Ordering)
-> OrdDict a -> a -> a -> Ordering
forall a b. (a -> b) -> a -> b
$ Proxy s -> OrdDict a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> OrdDict a
reflect (Proxy s
forall {k} (t :: k). Proxy t
Proxy :: Proxy s)
                           in case a
l a -> a -> Ordering
`cmp` a
r of
                                Ordering
EQ -> Bool
True
                                Ordering
_  -> Bool
False

instance (Eq (O s a), Reifies s (OrdDict a)) => Ord (O s a) where
  (O a
l) compare :: O s a -> O s a -> Ordering
`compare` (O a
r) = let cmp :: a -> a -> Ordering
cmp = OrdDict a -> a -> a -> Ordering
forall a. OrdDict a -> a -> a -> Ordering
compare_ (OrdDict a -> a -> a -> Ordering)
-> OrdDict a -> a -> a -> Ordering
forall a b. (a -> b) -> a -> b
$ Proxy s -> OrdDict a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> OrdDict a
reflect (Proxy s
forall {k} (t :: k). Proxy t
Proxy :: Proxy s)
                                  in a
l a -> a -> Ordering
`cmp` a
r

-- | Run a computation with a given ordering
withOrd       :: (a -> a -> Ordering) -> (forall s. Reifies s (OrdDict a) => O s b) -> b
withOrd :: forall a b.
(a -> a -> Ordering)
-> (forall s. Reifies s (OrdDict a) => O s b) -> b
withOrd a -> a -> Ordering
cmp forall s. Reifies s (OrdDict a) => O s b
v = OrdDict a -> (forall s. Reifies s (OrdDict a) => Proxy s -> b) -> b
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify ((a -> a -> Ordering) -> OrdDict a
forall a. (a -> a -> Ordering) -> OrdDict a
OrdDict a -> a -> Ordering
cmp) (O s b -> b
forall s a. O s a -> a
runO (O s b -> b) -> (Proxy s -> O s b) -> Proxy s -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. O s b -> Proxy s -> O s b
forall {k} {k} (f :: k -> k -> *) (s :: k) (a :: k).
f s a -> Proxy s -> f s a
asProxyOf O s b
forall s. Reifies s (OrdDict a) => O s b
v)
  where
    asProxyOf      :: f s a -> Proxy s -> f s a
    asProxyOf :: forall {k} {k} (f :: k -> k -> *) (s :: k) (a :: k).
f s a -> Proxy s -> f s a
asProxyOf f s a
v' Proxy s
_ = f s a
v'

--------------------------------------------------------------------------------
-- * Introducing and removing the dynamic order type
-- Note that all of these may be unsafe if used incorrectly

-- | Lifts a container f whose values (of type a) depend on '@s@' into a
-- more general computation in that produces a '@f a@' (depending on s).
--
-- running time: \(O(1)\)
extractOrd1 :: f (O s a) -> O s (f a)
extractOrd1 :: forall (f :: * -> *) s a. f (O s a) -> O s (f a)
extractOrd1 = f (O s a) -> O s (f a)
forall a b. a -> b
unsafeCoerce


-- | Introduce dynamic order in a container '@f@'.
--
-- running time: \(O(1)\)
introOrd1 :: f a -> f (O s a)
introOrd1 :: forall (f :: * -> *) a s. f a -> f (O s a)
introOrd1 = f a -> f (O s a)
forall a b. a -> b
unsafeCoerce

-- | Lifts a function that works on a container '@f@' of
-- orderable-things into one that works on dynamically ordered ones.
liftOrd1   :: (f (O s a) -> g (O s a))
           -> f a -> O s (g a)
liftOrd1 :: forall (f :: * -> *) s a (g :: * -> *).
(f (O s a) -> g (O s a)) -> f a -> O s (g a)
liftOrd1 f (O s a) -> g (O s a)
f = g (O s a) -> O s (g a)
forall (f :: * -> *) s a. f (O s a) -> O s (f a)
extractOrd1 (g (O s a) -> O s (g a)) -> (f a -> g (O s a)) -> f a -> O s (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (O s a) -> g (O s a)
f (f (O s a) -> g (O s a)) -> (f a -> f (O s a)) -> f a -> g (O s a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> f (O s a)
forall (f :: * -> *) a s. f a -> f (O s a)
introOrd1


-- | Lifts a container f whose keys (of type k) depend on '@s@' into a
-- more general computation in that produces a @`f k v`@ (depending on s).
--
-- running time: \(O(1)\)
extractOrd2 :: f (O s k) v -> O s (f k v)
extractOrd2 :: forall {k} (f :: * -> k -> *) s k (v :: k).
f (O s k) v -> O s (f k v)
extractOrd2 = f (O s k) v -> O s (f k v)
forall a b. a -> b
unsafeCoerce

-- | Introduce dynamic order in a container '@f@' that has keys of type
-- k.
--
-- running time: \(O(1)\)
introOrd2 :: f k v -> f (O s k) v
introOrd2 :: forall {k} (f :: * -> k -> *) k (v :: k) s. f k v -> f (O s k) v
introOrd2 = f k v -> f (O s k) v
forall a b. a -> b
unsafeCoerce