{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE InstanceSigs #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Data.Functor.Polynomial.Finitary.Tag(
    FinPolyTag(..),
) where

import Data.Kind (Type)
import Data.Void (Void)
import Data.Type.Equality ((:~:)(..))

import Data.GADT.Compare (GEq(..), GCompare(..), GOrdering(..))
import Data.GADT.HasFinitary (HasFinitary(..))

import Data.Polynomial (P(..))

-- | Tag GADT for @'Ev' p@.
--
--   @FinPolyTag p n@ witnesses that @n@ is the position type of one summand of @'Ev' p@.
--
--   This gives @'Ev' p@ an instance of 'Polynomial' from the @polynomial-functor@ package,
--   with @'Tag' ('Ev' p) = 'FinPolyTag' p@.
data FinPolyTag (p :: P) (n :: Type) where
    FinPolyEnd  ::                    FinPolyTag 'U       Void
    FinPolyStop ::                    FinPolyTag ('S p)   Void
    FinPolyGo   :: FinPolyTag p n ->  FinPolyTag ('S p)   n
    FinPolyCons :: FinPolyTag p n ->  FinPolyTag ('T p)   (Either () n)

instance HasFinitary (FinPolyTag p) where
    withFinitary :: forall n r. FinPolyTag p n -> (Finitary n => r) -> r
withFinitary FinPolyTag p n
FinPolyEnd      Finitary n => r
body = r
Finitary n => r
body
    withFinitary FinPolyTag p n
FinPolyStop     Finitary n => r
body = r
Finitary n => r
body
    withFinitary (FinPolyGo   FinPolyTag p n
t) Finitary n => r
body = FinPolyTag p n -> (Finitary n => r) -> r
forall n r. FinPolyTag p n -> (Finitary n => r) -> r
forall (tag :: * -> *) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary FinPolyTag p n
t r
Finitary n => r
body
    withFinitary (FinPolyCons FinPolyTag p n
t) Finitary n => r
body = FinPolyTag p n -> (Finitary n => r) -> r
forall n r. FinPolyTag p n -> (Finitary n => r) -> r
forall (tag :: * -> *) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary FinPolyTag p n
t r
Finitary n => r
Finitary n => r
body

instance GEq (FinPolyTag p) where
    geq :: forall a b. FinPolyTag p a -> FinPolyTag p b -> Maybe (a :~: b)
geq FinPolyTag p a
FinPolyEnd       FinPolyTag p b
FinPolyEnd       = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    geq FinPolyTag p a
FinPolyStop      FinPolyTag p b
FinPolyStop      = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    geq (FinPolyGo   FinPolyTag p a
t) (FinPolyGo   FinPolyTag p b
t') = FinPolyTag p a -> FinPolyTag p b -> Maybe (a :~: b)
forall a b. FinPolyTag p a -> FinPolyTag p b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq FinPolyTag p a
t FinPolyTag p b
FinPolyTag p b
t'
    geq (FinPolyCons FinPolyTag p n
t) (FinPolyCons FinPolyTag p n
t') = do
        Refl <- FinPolyTag p n -> FinPolyTag p n -> Maybe (n :~: n)
forall a b. FinPolyTag p a -> FinPolyTag p b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq FinPolyTag p n
t FinPolyTag p n
FinPolyTag p n
t'
        pure Refl
    geq FinPolyTag p a
_ FinPolyTag p b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance GCompare (FinPolyTag p) where
    gcompare :: forall a b. FinPolyTag p a -> FinPolyTag p b -> GOrdering a b
gcompare FinPolyTag p a
FinPolyEnd      FinPolyTag p b
FinPolyEnd       = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
    gcompare FinPolyTag p a
FinPolyStop     FinPolyTag p b
FinPolyStop      = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
    gcompare (FinPolyGo   FinPolyTag p a
t) (FinPolyGo   FinPolyTag p b
t') = FinPolyTag p a -> FinPolyTag p b -> GOrdering a b
forall a b. FinPolyTag p a -> FinPolyTag p b -> GOrdering a b
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare FinPolyTag p a
t FinPolyTag p b
FinPolyTag p b
t'
    gcompare (FinPolyCons FinPolyTag p n
t) (FinPolyCons FinPolyTag p n
t') = case FinPolyTag p n -> FinPolyTag p n -> GOrdering n n
forall a b. FinPolyTag p a -> FinPolyTag p b -> GOrdering a b
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare FinPolyTag p n
t FinPolyTag p n
FinPolyTag p n
t' of
        GOrdering n n
GLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
        GOrdering n n
GEQ -> GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
        GOrdering n n
GGT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
    -- Remaining cases: constructors with different arities/indices can't share p,
    -- so these are exhaustive within a fixed p.
    gcompare FinPolyTag p a
FinPolyStop     (FinPolyGo   FinPolyTag p b
_)  = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    gcompare (FinPolyGo   FinPolyTag p a
_) FinPolyTag p b
FinPolyStop      = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT