-- | Utilities for traversing heterogeneous trees. A heterogeneous tree is a
-- collection of datatypes that "contain" eachother in some form of tree
-- structure.
module Data.OpenApi.Compare.Paths
  ( NiceQuiver,
    AdditionalQuiverConstraints,
    Paths (..),
    DiffPaths (..),
    catDiffPaths,
    AnItem (..),
    step,

    -- * Reexports
    (>>>),
    (<<<),
  )
where

import Control.Category
import Data.Kind
import Data.Type.Equality
import Type.Reflection
import Prelude hiding ((.))

type NiceQuiver (q :: k -> j -> Type) (a :: k) (b :: j) =
  (Typeable q, Typeable a, Typeable b, Ord (q a b), Show (q a b), AdditionalQuiverConstraints q a b)

type family AdditionalQuiverConstraints (q :: k -> j -> Type) (a :: k) (b :: j) :: Constraint

-- | All the possible ways to navigate between nodes in a heterogeneous tree
-- form a quiver. The hom-sets of the free category constructed from this quiver
-- are the sets of various multi-step paths between nodes. This is similar to a
-- list, but indexed. The list is in reverse because in practice we append
-- items at the end one at a time.
data Paths (q :: k -> k -> Type) (a :: k) (b :: k) where
  Root :: Paths q a a
  Snoc :: NiceQuiver q b c => Paths q a b -> !(q b c) -> Paths q a c

infixl 5 `Snoc`

deriving stock instance Show (Paths q a b)

step :: NiceQuiver q a b => q a b -> Paths q a b
step :: q a b -> Paths q a b
step q a b
s = Paths q a a
forall k (q :: k -> k -> *) (a :: k). Paths q a a
Root Paths q a a -> q a b -> Paths q a b
forall k (q :: k -> k -> *) (b :: k) (c :: k) (a :: k).
NiceQuiver q b c =>
Paths q a b -> q b c -> Paths q a c
`Snoc` q a b
s

instance Category (Paths q) where
  id :: Paths q a a
id = Paths q a a
forall k (q :: k -> k -> *) (a :: k). Paths q a a
Root
  Paths q b c
Root . :: Paths q b c -> Paths q a b -> Paths q a c
. Paths q a b
xs = Paths q a b
Paths q a c
xs
  (Snoc Paths q b b
ys q b c
y) . Paths q a b
xs = Paths q a b -> q b c -> Paths q a c
forall k (q :: k -> k -> *) (b :: k) (c :: k) (a :: k).
NiceQuiver q b c =>
Paths q a b -> q b c -> Paths q a c
Snoc (Paths q b b
ys Paths q b b -> Paths q a b -> Paths q a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Paths q a b
xs) q b c
y

typeRepRHS :: Typeable b => Paths q a b -> TypeRep b
typeRepRHS :: Paths q a b -> TypeRep b
typeRepRHS Paths q a b
_ = TypeRep b
forall k (a :: k). Typeable a => TypeRep a
typeRep

typeRepLHS :: Typeable b => Paths q a b -> TypeRep a
typeRepLHS :: Paths q a b -> TypeRep a
typeRepLHS Paths q a b
Root = TypeRep a
forall k (a :: k). Typeable a => TypeRep a
typeRep
typeRepLHS (Snoc Paths q a b
xs q b b
_) = Paths q a b -> TypeRep a
forall k (b :: k) (q :: k -> k -> *) (a :: k).
Typeable b =>
Paths q a b -> TypeRep a
typeRepLHS Paths q a b
xs

instance TestEquality (Paths q a) where
  testEquality :: Paths q a a -> Paths q a b -> Maybe (a :~: b)
testEquality Paths q a a
Root Paths q a b
Root = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality Paths q a a
Root (Snoc Paths q a b
ys q b b
_) = TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Paths q a b -> TypeRep a
forall k (b :: k) (q :: k -> k -> *) (a :: k).
Typeable b =>
Paths q a b -> TypeRep a
typeRepLHS Paths q a b
ys) TypeRep b
forall k (a :: k). Typeable a => TypeRep a
typeRep
  testEquality (Snoc Paths q a b
xs q b a
_) Paths q a b
Root = TypeRep a -> TypeRep a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TypeRep a
forall k (a :: k). Typeable a => TypeRep a
typeRep (Paths q a b -> TypeRep a
forall k (b :: k) (q :: k -> k -> *) (a :: k).
Typeable b =>
Paths q a b -> TypeRep a
typeRepLHS Paths q a b
xs)
  testEquality (Snoc Paths q a b
_ q b a
_) (Snoc Paths q a b
_ q b b
_) = TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TypeRep a
forall k (a :: k). Typeable a => TypeRep a
typeRep TypeRep b
forall k (a :: k). Typeable a => TypeRep a
typeRep

instance Eq (Paths q a b) where
  Paths q a b
Root == :: Paths q a b -> Paths q a b -> Bool
== Paths q a b
Root = Bool
True
  Snoc Paths q a b
xs q b b
x == Snoc Paths q a b
ys q b b
y
    | Just b :~: b
Refl <- TypeRep b -> TypeRep b -> Maybe (b :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Paths q a b -> TypeRep b
forall k (b :: k) (q :: k -> k -> *) (a :: k).
Typeable b =>
Paths q a b -> TypeRep b
typeRepRHS Paths q a b
xs) (Paths q a b -> TypeRep b
forall k (b :: k) (q :: k -> k -> *) (a :: k).
Typeable b =>
Paths q a b -> TypeRep b
typeRepRHS Paths q a b
ys) =
      Paths q a b
xs Paths q a b -> Paths q a b -> Bool
forall a. Eq a => a -> a -> Bool
== Paths q a b
Paths q a b
ys Bool -> Bool -> Bool
&& q b b
x q b b -> q b b -> Bool
forall a. Eq a => a -> a -> Bool
== q b b
q b b
y
  Paths q a b
_ == Paths q a b
_ = Bool
False

instance Ord (Paths q a b) where
  compare :: Paths q a b -> Paths q a b -> Ordering
compare Paths q a b
Root Paths q a b
Root = Ordering
EQ
  compare Paths q a b
Root (Snoc Paths q a b
_ q b b
_) = Ordering
LT
  compare (Snoc Paths q a b
_ q b b
_) Paths q a b
Root = Ordering
GT
  compare (Snoc Paths q a b
xs q b b
x) (Snoc Paths q a b
ys q b b
y) =
    case TypeRep b -> TypeRep b -> Maybe (b :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Paths q a b -> TypeRep b
forall k (b :: k) (q :: k -> k -> *) (a :: k).
Typeable b =>
Paths q a b -> TypeRep b
typeRepRHS Paths q a b
xs) (Paths q a b -> TypeRep b
forall k (b :: k) (q :: k -> k -> *) (a :: k).
Typeable b =>
Paths q a b -> TypeRep b
typeRepRHS Paths q a b
ys) of
      Just b :~: b
Refl -> Paths q a b -> Paths q a b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Paths q a b
xs Paths q a b
Paths q a b
ys Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> q b b -> q b b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare q b b
x q b b
q b b
y
      Maybe (b :~: b)
Nothing -> SomeTypeRep -> SomeTypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Paths q a b -> SomeTypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep Paths q a b
xs) (Paths q a b -> SomeTypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep Paths q a b
ys)

-- | Like a differece list, but indexed.
newtype DiffPaths (q :: k -> k -> Type) (a :: k) (b :: k)
  = DiffPaths (forall c. Paths q c a -> Paths q c b)

catDiffPaths :: DiffPaths q a b -> DiffPaths q b c -> DiffPaths q a c
catDiffPaths :: DiffPaths q a b -> DiffPaths q b c -> DiffPaths q a c
catDiffPaths (DiffPaths forall (c :: k). Paths q c a -> Paths q c b
f) (DiffPaths forall (c :: k). Paths q c b -> Paths q c c
g) = (forall (c :: k). Paths q c a -> Paths q c c) -> DiffPaths q a c
forall k (q :: k -> k -> *) (a :: k) (b :: k).
(forall (c :: k). Paths q c a -> Paths q c b) -> DiffPaths q a b
DiffPaths (Paths q c b -> Paths q c c
forall (c :: k). Paths q c b -> Paths q c c
g (Paths q c b -> Paths q c c)
-> (Paths q c a -> Paths q c b) -> Paths q c a -> Paths q c c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Paths q c a -> Paths q c b
forall (c :: k). Paths q c a -> Paths q c b
f)

-- _DiffPaths :: Iso (DiffPaths q a b) (DiffPaths q c d) (Paths q a b) (Paths q c d)
-- _DiffPaths = dimap (\(DiffPaths f) -> f Root) $
--   fmap $ \xs -> DiffPaths (>>> xs)

-- | An item related to some path relative to the root @r@.
data AnItem (q :: k -> k -> Type) (f :: k -> Type) (r :: k) where
  AnItem :: Ord (f a) => Paths q r a -> !(f a) -> AnItem q f r

-- the Ord is yuck but we need it and it should be fine in monomorphic cases

instance Eq (AnItem q f r) where
  AnItem Paths q r a
xs f a
fx == :: AnItem q f r -> AnItem q f r -> Bool
== AnItem Paths q r a
ys f a
fy
    | Just a :~: a
Refl <- Paths q r a -> Paths q r a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Paths q r a
xs Paths q r a
ys =
      Paths q r a
xs Paths q r a -> Paths q r a -> Bool
forall a. Eq a => a -> a -> Bool
== Paths q r a
Paths q r a
ys Bool -> Bool -> Bool
&& f a
fx f a -> f a -> Bool
forall a. Eq a => a -> a -> Bool
== f a
f a
fy
  AnItem q f r
_ == AnItem q f r
_ = Bool
False

instance Typeable r => Ord (AnItem q f r) where
  compare :: AnItem q f r -> AnItem q f r -> Ordering
compare (AnItem Paths q r a
xs f a
fx) (AnItem Paths q r a
ys f a
fy) =
    case Paths q r a -> Paths q r a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Paths q r a
xs Paths q r a
ys of
      Just a :~: a
Refl -> Paths q r a -> Paths q r a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Paths q r a
xs Paths q r a
Paths q r a
ys Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> f a -> f a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare f a
fx f a
f a
fy
      Maybe (a :~: a)
Nothing -> case Paths q r a
xs of
        Paths q r a
Root -> case Paths q r a
ys of
          Paths q r a
Root -> SomeTypeRep -> SomeTypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Paths q r a -> SomeTypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep Paths q r a
xs) (Paths q r a -> SomeTypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep Paths q r a
ys)
          Snoc Paths q r b
_ q b a
_ -> SomeTypeRep -> SomeTypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Paths q r a -> SomeTypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep Paths q r a
xs) (Paths q r a -> SomeTypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep Paths q r a
ys)
        Snoc Paths q r b
_ q b a
_ -> case Paths q r a
ys of
          Paths q r a
Root -> SomeTypeRep -> SomeTypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Paths q r a -> SomeTypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep Paths q r a
xs) (Paths q r a -> SomeTypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep Paths q r a
ys)
          Snoc Paths q r b
_ q b a
_ -> SomeTypeRep -> SomeTypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Paths q r a -> SomeTypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep Paths q r a
xs) (Paths q r a -> SomeTypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep Paths q r a
ys)