{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE InstanceSigs #-}
module Data.Functor.Polynomial.Finitary(
    Ev(..), Ev₀(..),
    toSum, fromSum, toProduct, fromProduct,
    toComp, fromComp
) where

import Data.Kind (Type)

import Data.Void (absurd)
import GHC.Generics hiding (S,C,D)

import Data.Singletons

import Data.Polynomial
import Data.Functor.Polynomial.Class (Polynomial(..))
import Data.Functor.Polynomial.Finitary.Tag ( FinPolyTag(..) )
import qualified Data.Functor.Polynomial as FP

data Ev₀ (p :: P₀) (x :: Type) where
    MakeEv₀ :: Ev p x -> Ev₀ (NZ p) x

deriving instance Eq x => Eq (Ev₀ p x)
deriving instance Ord x => Ord (Ev₀ p x)
deriving instance Show x => Show (Ev₀ p x)
deriving instance Functor (Ev₀ p)

data Ev (p :: P) (x :: Type) where
    End :: Ev 'U x
    Stop :: Ev ('S p) x
    Go :: Ev p x -> Ev ('S p) x
    (:::) :: x -> Ev p x -> Ev ('T p) x

infixr 7 :::

deriving instance Eq x => Eq (Ev p x)
deriving instance Ord x => Ord (Ev p x)
deriving instance Show x => Show (Ev p x)
deriving instance Functor (Ev p)
deriving instance Foldable (Ev p)
deriving instance Traversable (Ev p)

toSum :: Sing p -> Sing q -> Ev (p + q) x -> (Ev p :+: Ev q) x
toSum :: forall (p :: P) (q :: P) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum Sing p
sp Sing q
sq Ev (p + q) x
hx = case Sing p
sp of
    Sing p
SingP p
SingU -> case Ev (p + q) x
hx of
        Ev (p + q) x
Stop -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
Ev 'U x
forall x. Ev 'U x
End
        Go Ev p x
gx -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev q x
Ev p x
gx
    SingS SingP p
sp' -> case Ev (p + q) x
hx of
        Ev (p + q) x
Stop -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
Ev ('S p) x
forall (p :: P) x. Ev ('S p) x
Stop
        Go Ev p x
hx' -> case Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum Sing p
SingP p
sp' Sing q
sq Ev p x
Ev (p + q) x
hx' of
            L1 Ev p x
fx -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (Ev p x -> Ev ('S p) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go Ev p x
fx)
            R1 Ev q x
gx -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev q x
gx
    SingT SingP p
sp' -> case Sing q
sq of
        Sing q
SingP q
SingU -> case Ev (p + q) x
hx of
            Ev (p + q) x
Stop -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev q x
Ev 'U x
forall x. Ev 'U x
End
            Go Ev p x
fx -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
Ev p x
fx
        SingS SingP p
sq' -> case Ev (p + q) x
hx of
            Ev (p + q) x
Stop -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev q x
Ev ('S p) x
forall (p :: P) x. Ev ('S p) x
Stop
            Go Ev p x
hx' -> case Sing p -> Sing p -> Ev (p + p) x -> (:+:) (Ev p) (Ev p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum Sing p
sp Sing p
SingP p
sq' Ev p x
Ev (p + p) x
hx' of
                L1 Ev p x
fx -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
fx
                R1 Ev p x
gx -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (Ev p x -> Ev ('S p) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go Ev p x
gx)
        SingT SingP p
sq' -> case Ev (p + q) x
hx of
            x
x ::: Ev p x
hx' -> case Sing p -> Sing p -> Ev (p + p) x -> (:+:) (Ev p) (Ev p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum Sing p
SingP p
sp' Sing p
SingP p
sq' Ev p x
Ev (p + p) x
hx' of
                L1 Ev p x
fx -> Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (x
x x -> Ev p x -> Ev ('T p) x
forall x (p :: P). x -> Ev p x -> Ev ('T p) x
::: Ev p x
fx)
                R1 Ev p x
gx -> Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (x
x x -> Ev p x -> Ev ('T p) x
forall x (p :: P). x -> Ev p x -> Ev ('T p) x
::: Ev p x
gx)

fromSum :: Sing p -> Sing q -> (Ev p :+: Ev q) x -> Ev (p + q) x
fromSum :: forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
sp Sing q
sq (:+:) (Ev p) (Ev q) x
fgx = case Sing p
sp of
    Sing p
SingP p
SingU -> case (:+:) (Ev p) (Ev q) x
fgx of
        L1 Ev p x
End -> Ev (p + q) x
Ev ('S q) x
forall (p :: P) x. Ev ('S p) x
Stop
        R1 Ev q x
gx -> Ev q x -> Ev ('S q) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go Ev q x
gx
    SingS SingP p
sp' -> case (:+:) (Ev p) (Ev q) x
fgx of
        L1 Ev p x
Stop -> Ev (p + q) x
Ev ('S (PlusPoly p q)) x
forall (p :: P) x. Ev ('S p) x
Stop
        L1 (Go Ev p x
fx) -> Ev (PlusPoly p q) x -> Ev ('S (PlusPoly p q)) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go (Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SingP p
sp' Sing q
sq (Ev p x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
fx))
        R1 Ev q x
gx -> Ev (PlusPoly p q) x -> Ev ('S (PlusPoly p q)) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go (Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SingP p
sp' Sing q
sq (Ev q x -> (:+:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev q x
gx))
    SingT SingP p
sp' -> case Sing q
sq of
        Sing q
SingP q
SingU -> case (:+:) (Ev p) (Ev q) x
fgx of
            L1 Ev p x
fx -> Ev p x -> Ev ('S p) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go Ev p x
fx
            R1 Ev q x
End -> Ev (p + q) x
Ev ('S ('T p)) x
forall (p :: P) x. Ev ('S p) x
Stop
        SingS SingP p
sq' -> case (:+:) (Ev p) (Ev q) x
fgx of
            L1 Ev p x
fx -> Ev (PlusPoly ('T p) p) x -> Ev ('S (PlusPoly ('T p) p)) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go (Sing p -> Sing p -> (:+:) (Ev p) (Ev p) x -> Ev (p + p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
sp Sing p
SingP p
sq' (Ev p x -> (:+:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
fx))
            R1 Ev q x
Stop -> Ev (p + q) x
Ev ('S (PlusPoly ('T p) p)) x
forall (p :: P) x. Ev ('S p) x
Stop
            R1 (Go Ev p x
gx) -> Ev (PlusPoly ('T p) p) x -> Ev ('S (PlusPoly ('T p) p)) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go (Sing ('T p)
-> Sing p -> (:+:) (Ev ('T p)) (Ev p) x -> Ev ('T p + p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
Sing ('T p)
sp Sing p
SingP p
sq' (Ev p x -> (:+:) (Ev ('T p)) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev p x
gx))
        SingT SingP p
sq' -> case (:+:) (Ev p) (Ev q) x
fgx of
            L1 (x
x ::: Ev p x
fx) -> x
x x -> Ev (PlusPoly p p) x -> Ev ('T (PlusPoly p p)) x
forall x (p :: P). x -> Ev p x -> Ev ('T p) x
::: Sing p -> Sing p -> (:+:) (Ev p) (Ev p) x -> Ev (p + p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SingP p
sp' Sing p
SingP p
sq' (Ev p x -> (:+:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
fx)
            R1 (x
x ::: Ev p x
gx) -> x
x x -> Ev (PlusPoly p p) x -> Ev ('T (PlusPoly p p)) x
forall x (p :: P). x -> Ev p x -> Ev ('T p) x
::: Sing p -> Sing p -> (:+:) (Ev p) (Ev p) x -> Ev (p + p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SingP p
sp' Sing p
SingP p
sq' (Ev p x -> (:+:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev p x
gx)

fromProduct :: Sing p -> Sing q -> (Ev p :*: Ev q) x -> Ev (p * q) x
fromProduct :: forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
fromProduct Sing p
sp Sing q
sq (Ev p x
fx :*: Ev q x
gx) = case Sing p
sp of
    Sing p
SingP p
SingU -> Ev q x
Ev (p * q) x
gx
    SingS SingP p
sp' -> case Sing q
sq of
        Sing q
SingP q
SingU -> Ev p x
Ev (p * q) x
fx
        SingS SingP p
sq' -> case (Ev p x
fx, Ev q x
gx) of
            (Ev p x
Stop,  Ev q x
Stop)  -> Ev (p * q) x
Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall (p :: P) x. Ev ('S p) x
Stop
            (Go Ev p x
fx', Ev q x
Stop)  -> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go (Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
 -> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x)
-> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall a b. (a -> b) -> a -> b
$ Sing (PlusPoly p p)
-> Sing (TimesPoly p p)
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
-> Ev (PlusPoly p p + TimesPoly p p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum (Sing p
SingP p
sp' Sing p -> Sing p -> Sing (p + p)
forall k (x :: k) (y :: k).
SPlus k =>
Sing x -> Sing y -> Sing (x + y)
forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x + y)
%+ Sing p
SingP p
sq') (Sing p
SingP p
sp' Sing p -> Sing p -> Sing (p * p)
forall k (x :: k) (y :: k).
STimes k =>
Sing x -> Sing y -> Sing (x * y)
forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x * y)
%* Sing p
SingP p
sq') (Ev (PlusPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (Ev (PlusPoly p p) x
 -> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x)
-> Ev (PlusPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall a b. (a -> b) -> a -> b
$ Sing p -> Sing p -> (:+:) (Ev p) (Ev p) x -> Ev (p + p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SingP p
sp' Sing p
SingP p
sq' (Ev p x -> (:+:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Ev p x
fx'))
            (Ev p x
Stop,  Go Ev p x
gx') -> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go (Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
 -> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x)
-> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall a b. (a -> b) -> a -> b
$ Sing (PlusPoly p p)
-> Sing (TimesPoly p p)
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
-> Ev (PlusPoly p p + TimesPoly p p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum (Sing p
SingP p
sp' Sing p -> Sing p -> Sing (p + p)
forall k (x :: k) (y :: k).
SPlus k =>
Sing x -> Sing y -> Sing (x + y)
forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x + y)
%+ Sing p
SingP p
sq') (Sing p
SingP p
sp' Sing p -> Sing p -> Sing (p * p)
forall k (x :: k) (y :: k).
STimes k =>
Sing x -> Sing y -> Sing (x * y)
forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x * y)
%* Sing p
SingP p
sq') (Ev (PlusPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (Ev (PlusPoly p p) x
 -> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x)
-> Ev (PlusPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall a b. (a -> b) -> a -> b
$ Sing p -> Sing p -> (:+:) (Ev p) (Ev p) x -> Ev (p + p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum Sing p
SingP p
sp' Sing p
SingP p
sq' (Ev p x -> (:+:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Ev p x
gx'))
            (Go Ev p x
fx', Go Ev p x
gx') -> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go (Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
 -> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x)
-> Ev (PlusPoly (PlusPoly p p) (TimesPoly p p)) x
-> Ev ('S (PlusPoly (PlusPoly p p) (TimesPoly p p))) x
forall a b. (a -> b) -> a -> b
$ Sing (PlusPoly p p)
-> Sing (TimesPoly p p)
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
-> Ev (PlusPoly p p + TimesPoly p p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:+:) (Ev p) (Ev q) x -> Ev (p + q) x
fromSum (Sing p
SingP p
sp' Sing p -> Sing p -> Sing (p + p)
forall k (x :: k) (y :: k).
SPlus k =>
Sing x -> Sing y -> Sing (x + y)
forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x + y)
%+ Sing p
SingP p
sq') (Sing p
SingP p
sp' Sing p -> Sing p -> Sing (p * p)
forall k (x :: k) (y :: k).
STimes k =>
Sing x -> Sing y -> Sing (x * y)
forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x * y)
%* Sing p
SingP p
sq') (Ev (TimesPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (Ev (TimesPoly p p) x
 -> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x)
-> Ev (TimesPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall a b. (a -> b) -> a -> b
$ Sing p -> Sing p -> (:*:) (Ev p) (Ev p) x -> Ev (p * p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
fromProduct Sing p
SingP p
sp' Sing p
SingP p
sq' (Ev p x
fx' Ev p x -> Ev p x -> (:*:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev p x
gx'))
        SingT SingP p
sq' -> case Ev q x
gx of
            x
x ::: Ev p x
gx' -> x
x x -> Ev (TimesPoly ('S p) p) x -> Ev ('T (TimesPoly ('S p) p)) x
forall x (p :: P). x -> Ev p x -> Ev ('T p) x
::: Sing p -> Sing p -> (:*:) (Ev p) (Ev p) x -> Ev (p * p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
fromProduct Sing p
sp Sing p
SingP p
sq' (Ev p x
fx Ev p x -> Ev p x -> (:*:) (Ev p) (Ev p) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev p x
gx')
    SingT SingP p
sp' -> case Ev p x
fx of
        x
x ::: Ev p x
fx' -> x
x x -> Ev (TimesPoly p q) x -> Ev ('T (TimesPoly p q)) x
forall x (p :: P). x -> Ev p x -> Ev ('T p) x
::: Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
fromProduct Sing p
SingP p
sp' Sing q
sq (Ev p x
fx' Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
gx)

toProduct :: Sing p -> Sing q -> Ev (p * q) x -> (Ev p :*: Ev q) x
toProduct :: forall (p :: P) (q :: P) x.
Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
toProduct Sing p
sp Sing q
sq Ev (p * q) x
hx = case Sing p
sp of
    Sing p
SingP p
SingU -> Ev p x
Ev 'U x
forall x. Ev 'U x
End Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
Ev (p * q) x
hx
    SingS SingP p
sp' -> case Sing q
sq of
        Sing q
SingP q
SingU -> Ev p x
Ev (p * q) x
hx Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
Ev 'U x
forall x. Ev 'U x
End
        SingS SingP p
sq' -> case Ev (p * q) x
hx of
            Ev (p * q) x
Stop -> Ev p x
Ev ('S p) x
forall (p :: P) x. Ev ('S p) x
Stop Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
Ev ('S p) x
forall (p :: P) x. Ev ('S p) x
Stop
            Go Ev p x
hx' -> case Sing (PlusPoly p p)
-> Sing (TimesPoly p p)
-> Ev (PlusPoly p p + TimesPoly p p) x
-> (:+:) (Ev (PlusPoly p p)) (Ev (TimesPoly p p)) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum (Sing p
SingP p
sp' Sing p -> Sing p -> Sing (p + p)
forall k (x :: k) (y :: k).
SPlus k =>
Sing x -> Sing y -> Sing (x + y)
forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x + y)
%+ Sing p
SingP p
sq') (Sing p
SingP p
sp' Sing p -> Sing p -> Sing (p * p)
forall k (x :: k) (y :: k).
STimes k =>
Sing x -> Sing y -> Sing (x * y)
forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x * y)
%* Sing p
SingP p
sq') Ev p x
Ev (PlusPoly p p + TimesPoly p p) x
hx' of
                L1 Ev (PlusPoly p p) x
hx'' -> case Sing p -> Sing p -> Ev (p + p) x -> (:+:) (Ev p) (Ev p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> Ev (p + q) x -> (:+:) (Ev p) (Ev q) x
toSum Sing p
SingP p
sp' Sing p
SingP p
sq' Ev (PlusPoly p p) x
Ev (p + p) x
hx'' of
                    L1 Ev p x
fx' -> Ev p x -> Ev ('S p) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go Ev p x
fx' Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
Ev ('S p) x
forall (p :: P) x. Ev ('S p) x
Stop
                    R1 Ev p x
gx' -> Ev p x
Ev ('S p) x
forall (p :: P) x. Ev ('S p) x
Stop Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev p x -> Ev ('S p) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go Ev p x
gx'
                R1 Ev (TimesPoly p p) x
hx'' ->
                    let Ev p x
fx' :*: Ev p x
gx' = Sing p -> Sing p -> Ev (p * p) x -> (:*:) (Ev p) (Ev p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
toProduct Sing p
SingP p
sp' Sing p
SingP p
sq' Ev (TimesPoly p p) x
Ev (p * p) x
hx''
                    in Ev p x -> Ev ('S p) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go Ev p x
fx' Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev p x -> Ev ('S p) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go Ev p x
gx'
        SingT SingP p
sq' -> case Ev (p * q) x
hx of
            x
x ::: Ev p x
hx' ->
                let Ev p x
fx :*: Ev p x
gx' = Sing p -> Sing p -> Ev (p * p) x -> (:*:) (Ev p) (Ev p) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
toProduct Sing p
sp Sing p
SingP p
sq' Ev p x
Ev (p * p) x
hx'
                in Ev p x
fx Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: (x
x x -> Ev p x -> Ev ('T p) x
forall x (p :: P). x -> Ev p x -> Ev ('T p) x
::: Ev p x
gx')
    SingT SingP p
sp' -> case Ev (p * q) x
hx of
        x
x ::: Ev p x
hx' ->
            let Ev p x
fx' :*: Ev q x
gx = Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
toProduct Sing p
SingP p
sp' Sing q
sq Ev p x
Ev (p * q) x
hx'
            in (x
x x -> Ev p x -> Ev ('T p) x
forall x (p :: P). x -> Ev p x -> Ev ('T p) x
::: Ev p x
fx') Ev p x -> Ev q x -> (:*:) (Ev p) (Ev q) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ev q x
gx

fromComp :: SingP p -> SingP q -> Ev p (Ev q x) -> Ev (p << q) x
fromComp :: forall (p :: P) (q :: P) x.
SingP p -> SingP q -> Ev p (Ev q x) -> Ev (p << q) x
fromComp SingP p
sp SingP q
sq Ev p (Ev q x)
fgx = case SingP p
sp of
    SingP p
SingU -> Ev (p << q) x
Ev 'U x
forall x. Ev 'U x
End
    SingS SingP p
sp' -> case Ev p (Ev q x)
fgx of
        Ev p (Ev q x)
Stop -> Ev (p << q) x
Ev ('S (ComposePoly p q)) x
forall (p :: P) x. Ev ('S p) x
Stop
        Go Ev p (Ev q x)
fgx' -> Ev (ComposePoly p q) x -> Ev ('S (ComposePoly p q)) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go (SingP p -> SingP q -> Ev p (Ev q x) -> Ev (p << q) x
forall (p :: P) (q :: P) x.
SingP p -> SingP q -> Ev p (Ev q x) -> Ev (p << q) x
fromComp SingP p
sp' SingP q
sq Ev p (Ev q x)
Ev p (Ev q x)
fgx')
    SingT SingP p
sp' -> case Ev p (Ev q x)
fgx of
        Ev q x
gx ::: Ev p (Ev q x)
fgx' -> Sing q
-> Sing (ComposePoly p q)
-> (:*:) (Ev q) (Ev (ComposePoly p q)) x
-> Ev (q * ComposePoly p q) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> (:*:) (Ev p) (Ev q) x -> Ev (p * q) x
fromProduct Sing q
SingP q
sq (Sing p
SingP p
sp' Sing p -> Sing q -> Sing (p << q)
forall k (x :: k) (y :: k).
SCompose k =>
Sing x -> Sing y -> Sing (x << y)
forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x << y)
%<< Sing q
SingP q
sq) (Ev q x
gx Ev q x
-> Ev (ComposePoly p q) x -> (:*:) (Ev q) (Ev (ComposePoly p q)) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: SingP p -> SingP q -> Ev p (Ev q x) -> Ev (p << q) x
forall (p :: P) (q :: P) x.
SingP p -> SingP q -> Ev p (Ev q x) -> Ev (p << q) x
fromComp SingP p
sp' SingP q
sq Ev p (Ev q x)
Ev p (Ev q x)
fgx')

toComp :: SingP p -> SingP q -> Ev (p << q) x -> Ev p (Ev q x)
toComp :: forall (p :: P) (q :: P) x.
SingP p -> SingP q -> Ev (p << q) x -> Ev p (Ev q x)
toComp SingP p
sp SingP q
sq Ev (p << q) x
hx = case SingP p
sp of
    SingP p
SingU -> Ev p (Ev q x)
Ev 'U (Ev q x)
forall x. Ev 'U x
End
    SingS SingP p
sp' -> case Ev (p << q) x
hx of
        Ev (p << q) x
Stop -> Ev p (Ev q x)
Ev ('S p) (Ev q x)
forall (p :: P) x. Ev ('S p) x
Stop
        Go Ev p x
hx' -> Ev p (Ev q x) -> Ev ('S p) (Ev q x)
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go (SingP p -> SingP q -> Ev (p << q) x -> Ev p (Ev q x)
forall (p :: P) (q :: P) x.
SingP p -> SingP q -> Ev (p << q) x -> Ev p (Ev q x)
toComp SingP p
sp' SingP q
sq Ev p x
Ev (p << q) x
hx')
    SingT SingP p
sp' -> 
        let Ev q x
gx :*: Ev (ComposePoly p q) x
hx' = Sing q
-> Sing (ComposePoly p q)
-> Ev (q * ComposePoly p q) x
-> (:*:) (Ev q) (Ev (ComposePoly p q)) x
forall (p :: P) (q :: P) x.
Sing p -> Sing q -> Ev (p * q) x -> (:*:) (Ev p) (Ev q) x
toProduct Sing q
SingP q
sq (Sing p
SingP p
sp' Sing p -> Sing q -> Sing (p << q)
forall k (x :: k) (y :: k).
SCompose k =>
Sing x -> Sing y -> Sing (x << y)
forall (x :: P) (y :: P). Sing x -> Sing y -> Sing (x << y)
%<< Sing q
SingP q
sq) Ev (p << q) x
Ev (q * ComposePoly p q) x
hx
        in Ev q x
gx Ev q x -> Ev p (Ev q x) -> Ev ('T p) (Ev q x)
forall x (p :: P). x -> Ev p x -> Ev ('T p) x
::: SingP p -> SingP q -> Ev (p << q) x -> Ev p (Ev q x)
forall (p :: P) (q :: P) x.
SingP p -> SingP q -> Ev (p << q) x -> Ev p (Ev q x)
toComp SingP p
sp' SingP q
sq Ev (ComposePoly p q) x
Ev (p << q) x
hx'


---

instance Polynomial (Ev p) where
    type Tag (Ev p) = FinPolyTag p

    toPoly :: Ev p x -> FP.Poly (FinPolyTag p) x
    toPoly :: forall x. Ev p x -> Poly (FinPolyTag p) x
toPoly Ev p x
End        = FinPolyTag p Void -> (Void -> x) -> Poly (FinPolyTag p) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
FP.P FinPolyTag p Void
FinPolyTag 'U Void
FinPolyEnd  Void -> x
forall a. Void -> a
absurd
    toPoly Ev p x
Stop       = FinPolyTag p Void -> (Void -> x) -> Poly (FinPolyTag p) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
FP.P FinPolyTag p Void
FinPolyTag ('S p) Void
forall (p1 :: P). FinPolyTag ('S p1) Void
FinPolyStop Void -> x
forall a. Void -> a
absurd
    toPoly (Go Ev p x
ev)    = case Ev p x -> Poly (Tag (Ev p)) x
forall x. Ev p x -> Poly (Tag (Ev p)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly Ev p x
ev of
                            FP.P Tag (Ev p) n
t n -> x
rep -> FinPolyTag p n -> (n -> x) -> Poly (FinPolyTag p) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
FP.P (FinPolyTag p n -> FinPolyTag ('S p) n
forall (p1 :: P) n. FinPolyTag p1 n -> FinPolyTag ('S p1) n
FinPolyGo FinPolyTag p n
Tag (Ev p) n
t) n -> x
rep
    toPoly (x
x ::: Ev p x
ev) = case Ev p x -> Poly (Tag (Ev p)) x
forall x. Ev p x -> Poly (Tag (Ev p)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly Ev p x
ev of
                            FP.P Tag (Ev p) n
t n -> x
rep -> FinPolyTag p (Either () n)
-> (Either () n -> x) -> Poly (FinPolyTag p) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
FP.P (FinPolyTag p n -> FinPolyTag ('T p) (Either () n)
forall (p1 :: P) n1.
FinPolyTag p1 n1 -> FinPolyTag ('T p1) (Either () n1)
FinPolyCons FinPolyTag p n
Tag (Ev p) n
t)
                                             (\case Left ()  -> x
x
                                                    Right n
i  -> n -> x
rep n
i)

    fromPoly :: FP.Poly (FinPolyTag p) x -> Ev p x
    fromPoly :: forall x. Poly (FinPolyTag p) x -> Ev p x
fromPoly (FP.P FinPolyTag p n
tag n -> x
rep) = case FinPolyTag p n
tag of
        FinPolyTag p n
FinPolyEnd    -> Ev p x
Ev 'U x
forall x. Ev 'U x
End
        FinPolyTag p n
FinPolyStop   -> Ev p x
Ev ('S p1) x
forall (p :: P) x. Ev ('S p) x
Stop
        FinPolyGo   FinPolyTag p1 n
t -> Ev p1 x -> Ev ('S p1) x
forall (p :: P) x. Ev p x -> Ev ('S p) x
Go (Poly (Tag (Ev p1)) x -> Ev p1 x
forall x. Poly (Tag (Ev p1)) x -> Ev p1 x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (FinPolyTag p1 n -> (n -> x) -> Poly (FinPolyTag p1) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
FP.P FinPolyTag p1 n
t n -> x
rep))
        FinPolyCons FinPolyTag p1 n1
t -> n -> x
rep (() -> Either () n1
forall a b. a -> Either a b
Left ()) x -> Ev p1 x -> Ev ('T p1) x
forall x (p :: P). x -> Ev p x -> Ev ('T p) x
::: Poly (Tag (Ev p1)) x -> Ev p1 x
forall x. Poly (Tag (Ev p1)) x -> Ev p1 x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (FinPolyTag p1 n1 -> (n1 -> x) -> Poly (FinPolyTag p1) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
FP.P FinPolyTag p1 n1
t (n -> x
rep (n -> x) -> (n1 -> n) -> n1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n1 -> n
n1 -> Either () n1
forall a b. b -> Either a b
Right))