{-# LANGUAGE ExistentialQuantification, GADTs #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE CPP #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Safe #-}
#endif
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE PolyKinds #-}
#endif
module Data.Dependent.Sum where
import Control.Applicative
#if MIN_VERSION_base(4,7,0)
import Data.Typeable (Typeable)
#else
import Data.Dependent.Sum.Typeable ()
#endif
import Data.GADT.Show
import Data.GADT.Compare
import Data.Maybe (fromMaybe)
data DSum tag f = forall a. !(tag a) :=> f a
#if MIN_VERSION_base(4,7,0)
deriving Typeable
#endif
infixr 1 :=>, ==>
(==>) :: Applicative f => tag a -> a -> DSum tag f
k :: tag a
k ==> :: tag a -> a -> DSum tag f
==> v :: a
v = tag a
k tag a -> f a -> DSum tag f
forall k (tag :: k -> *) (f :: k -> *) (a :: k).
tag a -> f a -> DSum tag f
:=> a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
v
class GShow tag => ShowTag tag f where
showTaggedPrec :: tag a -> Int -> f a -> ShowS
instance Show (f a) => ShowTag ((:=) a) f where
showTaggedPrec :: (a := a) -> Int -> f a -> ShowS
showTaggedPrec Refl = Int -> f a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
instance Show (f a) => ShowTag (GOrdering a) f where
showTaggedPrec :: GOrdering a a -> Int -> f a -> ShowS
showTaggedPrec GEQ = Int -> f a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
showTaggedPrec _ = \p :: Int
p _ -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 10)
( String -> ShowS
showString "error "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
forall a. Show a => a -> ShowS
shows "type information lost into the mists of oblivion"
)
instance ShowTag tag f => Show (DSum tag f) where
showsPrec :: Int -> DSum tag f -> ShowS
showsPrec p :: Int
p (tag :: tag a
tag :=> value :: f a
value) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 10)
( Int -> tag a -> ShowS
forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec 0 tag a
tag
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " :=> "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. tag a -> Int -> f a -> ShowS
forall k (tag :: k -> *) (f :: k -> *) (a :: k).
ShowTag tag f =>
tag a -> Int -> f a -> ShowS
showTaggedPrec tag a
tag 1 f a
value
)
class GRead tag => ReadTag tag f where
readTaggedPrec :: tag a -> Int -> ReadS (f a)
instance Read (f a) => ReadTag ((:=) a) f where
readTaggedPrec :: (a := a) -> Int -> ReadS (f a)
readTaggedPrec Refl = Int -> ReadS (f a)
forall a. Read a => Int -> ReadS a
readsPrec
instance ReadTag tag f => Read (DSum tag f) where
readsPrec :: Int -> ReadS (DSum tag f)
readsPrec p :: Int
p = Bool -> ReadS (DSum tag f) -> ReadS (DSum tag f)
forall a. Bool -> ReadS a -> ReadS a
readParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1) (ReadS (DSum tag f) -> ReadS (DSum tag f))
-> ReadS (DSum tag f) -> ReadS (DSum tag f)
forall a b. (a -> b) -> a -> b
$ \s :: String
s ->
[[(DSum tag f, String)]] -> [(DSum tag f, String)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ GReadResult tag -> forall b. (forall (a :: k). tag a -> b) -> b
forall k (t :: k -> *).
GReadResult t -> forall b. (forall (a :: k). t a -> b) -> b
getGReadResult GReadResult tag
withTag ((forall (a :: k). tag a -> [(DSum tag f, String)])
-> [(DSum tag f, String)])
-> (forall (a :: k). tag a -> [(DSum tag f, String)])
-> [(DSum tag f, String)]
forall a b. (a -> b) -> a -> b
$ \tag :: tag a
tag ->
[ (tag a
tag tag a -> f a -> DSum tag f
forall k (tag :: k -> *) (f :: k -> *) (a :: k).
tag a -> f a -> DSum tag f
:=> f a
val, String
rest'')
| (val :: f a
val, rest'' :: String
rest'') <- tag a -> Int -> ReadS (f a)
forall k (tag :: k -> *) (f :: k -> *) (a :: k).
ReadTag tag f =>
tag a -> Int -> ReadS (f a)
readTaggedPrec tag a
tag 1 String
rest'
]
| (withTag :: GReadResult tag
withTag, rest :: String
rest) <- Int -> GReadS tag
forall k (t :: k -> *). GRead t => Int -> GReadS t
greadsPrec Int
p String
s
, let (con :: String
con, rest' :: String
rest') = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt 5 String
rest
, String
con String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== " :=> "
]
class GEq tag => EqTag tag f where
eqTagged :: tag a -> tag a -> f a -> f a -> Bool
instance Eq (f a) => EqTag ((:=) a) f where
eqTagged :: (a := a) -> (a := a) -> f a -> f a -> Bool
eqTagged Refl Refl = f a -> f a -> Bool
forall a. Eq a => a -> a -> Bool
(==)
instance EqTag tag f => Eq (DSum tag f) where
(t1 :: tag a
t1 :=> x1 :: f a
x1) == :: DSum tag f -> DSum tag f -> Bool
== (t2 :: tag a
t2 :=> x2 :: f a
x2) = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ do
a :~: a
Refl <- tag a -> tag a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a := b)
geq tag a
t1 tag a
t2
Bool -> Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (tag a -> tag a -> f a -> f a -> Bool
forall k (tag :: k -> *) (f :: k -> *) (a :: k).
EqTag tag f =>
tag a -> tag a -> f a -> f a -> Bool
eqTagged tag a
t1 tag a
tag a
t2 f a
x1 f a
f a
x2)
class (EqTag tag f, GCompare tag) => OrdTag tag f where
compareTagged :: tag a -> tag a -> f a -> f a -> Ordering
instance Ord (f a) => OrdTag ((:=) a) f where
compareTagged :: (a := a) -> (a := a) -> f a -> f a -> Ordering
compareTagged Refl Refl = f a -> f a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
instance OrdTag tag f => Ord (DSum tag f) where
compare :: DSum tag f -> DSum tag f -> Ordering
compare (t1 :: tag a
t1 :=> x1 :: f a
x1) (t2 :: tag a
t2 :=> x2 :: f a
x2) = case tag a -> tag a -> GOrdering a a
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare tag a
t1 tag a
t2 of
GLT -> Ordering
LT
GGT -> Ordering
GT
GEQ -> tag a -> tag a -> f a -> f a -> Ordering
forall k (tag :: k -> *) (f :: k -> *) (a :: k).
OrdTag tag f =>
tag a -> tag a -> f a -> f a -> Ordering
compareTagged tag a
t1 tag a
tag a
t2 f a
x1 f a
f a
x2