{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE DataKinds #-}
module Data.Summer
(
Sum
, pattern Inj
, tag
, inject
, inspect
, consider
, considerFirst
, variant
, UnorderedMatch(unorderedMatch)
, Match(match, override, unmatch)
, Unmatch
, TagIn
, HasTagIn
, Delete
, HaveSameTagsIn
, Matcher
, Weaken(weaken)
, noOpWeaken
, inmap
, smap
, ApplyFunction(apply)
, type ForAll
) where
import Control.Exception (catch, SomeException)
import Unsafe.Coerce (unsafeCoerce)
import GHC.Exts (Any, Constraint)
import GHC.TypeLits (Nat, KnownNat, natVal, type (+))
import Data.Proxy (Proxy(Proxy))
import Data.Kind (Type)
import Control.Monad (unless)
import Generics.SOP (Generic(..))
import qualified Generics.SOP as SOP
import Data.Profunctor (Profunctor(dimap), Choice(..))
import Data.Typeable (typeRep, Typeable)
import Data.ForAll (type ForAll)
data Sum (xs :: [*]) = UnsafeInj {-# UNPACK #-} !Word Any
deriving (Typeable)
eject :: Sum '[x] -> x
eject :: Sum '[x] -> x
eject (UnsafeInj Word
_ Any
x) = Any -> x
forall a b. a -> b
unsafeCoerce Any
x
{-# INLINE CONLIKE eject #-}
variant :: forall a b xs p f. (a `HasTagIn` xs, Applicative f, Choice p) => p a (f b) -> p (Sum xs) (f (Sum (Replace a b xs)))
variant :: p a (f b) -> p (Sum xs) (f (Sum (Replace a b xs)))
variant p a (f b)
p = (Sum xs -> Either a (Sum (Replace a b xs)))
-> (Either (f b) (Sum (Replace a b xs))
-> f (Sum (Replace a b xs)))
-> p (Either a (Sum (Replace a b xs)))
(Either (f b) (Sum (Replace a b xs)))
-> p (Sum xs) (f (Sum (Replace a b xs)))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Sum xs -> Either a (Sum (Replace a b xs))
try Either (f b) (Sum (Replace a b xs)) -> f (Sum (Replace a b xs))
replace (p a (f b)
-> p (Either a (Sum (Replace a b xs)))
(Either (f b) (Sum (Replace a b xs)))
forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' p a (f b)
p) where
try :: Sum xs -> Either a (Sum (Replace a b xs))
try :: Sum xs -> Either a (Sum (Replace a b xs))
try (UnsafeInj Word
t Any
x) = if Word
t Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn a xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @a @xs then a -> Either a (Sum (Replace a b xs))
forall a b. a -> Either a b
Left (Any -> a
forall a b. a -> b
unsafeCoerce Any
x) else Sum (Replace a b xs) -> Either a (Sum (Replace a b xs))
forall a b. b -> Either a b
Right (Word -> Any -> Sum (Replace a b xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
t Any
x)
replace :: Either (f b) (Sum (Replace a b xs)) -> f (Sum (Replace a b xs))
replace :: Either (f b) (Sum (Replace a b xs)) -> f (Sum (Replace a b xs))
replace = \case
Left f b
fb -> (b -> Sum (Replace a b xs)) -> f b -> f (Sum (Replace a b xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Word -> Any -> Sum (Replace a b xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn a xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @a @xs) (Any -> Sum (Replace a b xs))
-> (b -> Any) -> b -> Sum (Replace a b xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Any
forall a b. a -> b
unsafeCoerce) f b
fb
Right Sum (Replace a b xs)
s -> Sum (Replace a b xs) -> f (Sum (Replace a b xs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sum (Replace a b xs)
s
{-# INLINE CONLIKE variant #-}
type family Replace x y xs where
Replace x y (x ': xs) = y ': xs
Replace x y (z ': xs) = z ': Replace x y xs
Replace x y '[] = '[]
instance Generic (Sum '[]) where
type Code (Sum '[]) = '[]
from :: Sum '[] -> Rep (Sum '[])
from Sum '[]
a = [Char] -> SOP I '[]
forall a. HasCallStack => [Char] -> a
error [Char]
"Generics.SOP.from: Impossible to create an empty sum"
to :: Rep (Sum '[]) -> Sum '[]
to Rep (Sum '[])
a = [Char] -> Sum '[]
forall a. HasCallStack => [Char] -> a
error [Char]
"Generics.SOP.to: Impossible to create an empty sum"
instance Generic (Sum xs) => Generic (Sum (x ': xs)) where
type Code (Sum (x ': xs)) = '[x] ': Code (Sum xs)
from :: Sum (x : xs) -> Rep (Sum (x : xs))
from (UnsafeInj Word
0 Any
x) = NS (NP I) ('[x] : Code (Sum xs)) -> SOP I ('[x] : Code (Sum xs))
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP.SOP (NP I '[x] -> NS (NP I) ('[x] : Code (Sum xs))
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
SOP.Z (x -> I x
forall a. a -> I a
SOP.I (Any -> x
forall a b. a -> b
unsafeCoerce Any
x) I x -> NP I '[] -> NP I '[x]
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
SOP.:* NP I '[]
forall k (a :: k -> *). NP a '[]
SOP.Nil))
from Sum (x : xs)
xs = NS (NP I) ('[x] : Code (Sum xs)) -> SOP I ('[x] : Code (Sum xs))
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP.SOP (NS (NP I) (Code (Sum xs)) -> NS (NP I) ('[x] : Code (Sum xs))
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
SOP.S NS (NP I) (Code (Sum xs))
ns) where
SOP.SOP NS (NP I) (Code (Sum xs))
ns = Sum xs -> SOP I (Code (Sum xs))
forall a. Generic a => a -> Rep a
from (Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
xs)
to :: Rep (Sum (x : xs)) -> Sum (x : xs)
to (SOP.SOP NS (NP I) (Code (Sum (x : xs)))
ns) = case NS (NP I) (Code (Sum (x : xs)))
ns of
SOP.Z (SOP.I x
x SOP.:* NP I xs
SOP.Nil) -> Word -> Any -> Sum (x : xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
0 (x -> Any
forall a b. a -> b
unsafeCoerce x
x)
SOP.S NS (NP I) xs
s -> Sum xs -> Sum (x : xs)
recall (SOP I (Code (Sum xs)) -> Sum xs
forall a. Generic a => Rep a -> a
to (NS (NP I) xs -> SOP I xs
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP.SOP NS (NP I) xs
s))
where
recall :: Sum xs -> Sum (x ': xs)
recall :: Sum xs -> Sum (x : xs)
recall (UnsafeInj Word
i Any
a) = Word -> Any -> Sum (x : xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
i Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) Any
a
type role Sum representational
pattern Inj :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs
pattern $bInj :: x -> Sum xs
$mInj :: forall r x (xs :: [*]).
HasTagIn x xs =>
Sum xs -> (x -> r) -> (Void# -> r) -> r
Inj x <- (inspect -> Just x)
where
Inj x
x = x -> Sum xs
forall x (xs :: [*]). HasTagIn x xs => x -> Sum xs
inject x
x
type family TagIn (x :: k) (xs :: [k]) where
TagIn x (x ': xs) = 0
TagIn x (y ': xs) = 1 + TagIn x xs
class KnownNat (x `TagIn` xs) => x `HasTagIn` xs
instance KnownNat (x `TagIn` xs) => x `HasTagIn` xs
tag :: forall x xs. x `HasTagIn` xs => Word
tag :: Word
tag = Integer -> Word
forall a. Num a => Integer -> a
fromInteger (Integer -> Word) -> Integer -> Word
forall a b. (a -> b) -> a -> b
$ Proxy (TagIn x xs) -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (TagIn x xs)
forall k (t :: k). Proxy t
Proxy @(TagIn x xs))
{-# INLINE CONLIKE tag #-}
inject :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs
inject :: x -> Sum xs
inject x
x = Word -> Any -> Sum xs
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs) (x -> Any
forall a b. a -> b
unsafeCoerce x
x)
{-# INLINE CONLIKE inject #-}
inspect :: forall x xs. (x `HasTagIn` xs) => Sum xs -> Maybe x
inspect :: Sum xs -> Maybe x
inspect (UnsafeInj Word
tag' Any
x) = if HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
tag' then x -> Maybe x
forall a. a -> Maybe a
Just (Any -> x
forall a b. a -> b
unsafeCoerce Any
x) else Maybe x
forall a. Maybe a
Nothing
{-# INLINE CONLIKE inspect #-}
type family Delete (x :: k) (xs :: [k]) :: [k] where
Delete x (x ': xs) = xs
Delete x (y ': xs) = y ': Delete x xs
Delete x '[] = '[]
consider :: forall x xs. (x `HasTagIn` xs) => Sum xs -> Either (Sum (Delete x xs)) x
consider :: Sum xs -> Either (Sum (Delete x xs)) x
consider (UnsafeInj Word
tag' Any
x) =
if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs
then x -> Either (Sum (Delete x xs)) x
forall a b. b -> Either a b
Right (Any -> x
forall a b. a -> b
unsafeCoerce Any
x)
else Sum (Delete x xs) -> Either (Sum (Delete x xs)) x
forall a b. a -> Either a b
Left (Word -> Any -> Sum (Delete x xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (if Word
tag' Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
>= HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word
tag' Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1 else Word
tag') Any
x)
{-# INLINE CONLIKE consider #-}
considerFirst :: forall x xs. Sum (x ': xs) -> Either (Sum xs) x
considerFirst :: Sum (x : xs) -> Either (Sum xs) x
considerFirst = Sum (x : xs) -> Either (Sum xs) x
forall x (xs :: [*]).
HasTagIn x xs =>
Sum xs -> Either (Sum (Delete x xs)) x
consider
{-# INLINE CONLIKE considerFirst #-}
inmap :: forall x y xs. (x `HasTagIn` xs, y `HasTagIn` xs) => (x -> y) -> Sum xs -> Sum xs
inmap :: (x -> y) -> Sum xs -> Sum xs
inmap x -> y
f uv :: Sum xs
uv@(UnsafeInj Word
tag' Any
x) = if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word -> Any -> Sum xs
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn y xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @y @xs) (y -> Any
forall a b. a -> b
unsafeCoerce (x -> y
f (Any -> x
forall a b. a -> b
unsafeCoerce Any
x))) else Sum xs
uv
{-# INLINE CONLIKE inmap #-}
smap :: forall x y xs ys. (Weaken (Delete x xs) ys, x `HasTagIn` xs, y `HasTagIn` ys) => (x -> y) -> Sum xs -> Sum ys
smap :: (x -> y) -> Sum xs -> Sum ys
smap x -> y
f uv :: Sum xs
uv@(UnsafeInj Word
tag' Any
x) = if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn y ys => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @y @ys) (y -> Any
forall a b. a -> b
unsafeCoerce (x -> y
f (Any -> x
forall a b. a -> b
unsafeCoerce Any
x))) else Sum (Delete x xs) -> Sum ys
forall (xs :: [*]) (ys :: [*]). Weaken xs ys => Sum xs -> Sum ys
weaken (Sum xs -> Sum (Delete x xs)
forall x (xs :: [*]). HasTagIn x xs => Sum xs -> Sum (Delete x xs)
unsafeForget @x Sum xs
uv)
{-# INLINE CONLIKE smap #-}
class HaveSameTagsIn xs ys
instance {-# OVERLAPPABLE #-} HaveSameTagsIn '[] ys
instance {-# OVERLAPPABLE #-} HaveSameTagsIn xs ys => HaveSameTagsIn (x ': xs) (x ': ys)
noOpWeaken :: forall xs ys. (xs `HaveSameTagsIn` ys) => Sum xs -> Sum ys
noOpWeaken :: Sum xs -> Sum ys
noOpWeaken = Sum xs -> Sum ys
forall a b. a -> b
unsafeCoerce
{-# INLINE CONLIKE noOpWeaken #-}
unsafeForget :: forall x xs. x `HasTagIn` xs => Sum xs -> Sum (Delete x xs)
unsafeForget :: Sum xs -> Sum (Delete x xs)
unsafeForget (UnsafeInj Word
tag' Any
x) = if Word
tag' Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word -> Any -> Sum (Delete x xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
tag' Any
x
else if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then [Char] -> Sum (Delete x xs)
forall a. HasCallStack => [Char] -> a
error [Char]
"unsafeForget: you can't forget the truth"
else Word -> Any -> Sum (Delete x xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
tag' Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Any
x
{-# INLINE CONLIKE unsafeForget #-}
unsafeForgetFirst :: Sum (x ': xs) -> Sum xs
unsafeForgetFirst :: Sum (x : xs) -> Sum xs
unsafeForgetFirst (UnsafeInj Word
tag' Any
x) = Word -> Any -> Sum xs
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
tag' Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Any
x
{-# INLINE CONLIKE unsafeForgetFirst #-}
instance (Eq (Sum xs), Eq x) => Eq (Sum (x ': xs)) where
uv :: Sum (x : xs)
uv@(UnsafeInj Word
tag' Any
x) == :: Sum (x : xs) -> Sum (x : xs) -> Bool
== uv' :: Sum (x : xs)
uv'@(UnsafeInj Word
tag'' Any
x')
| Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
tag'' =
if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0
then Any -> x
forall a b. a -> b
unsafeCoerce @_ @x Any
x x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== Any -> x
forall a b. a -> b
unsafeCoerce @_ @x Any
x'
else Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv Sum xs -> Sum xs -> Bool
forall a. Eq a => a -> a -> Bool
== Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv'
| Bool
otherwise = Bool
False
{-# INLINE CONLIKE (==) #-}
instance Eq (Sum '[]) where
== :: Sum '[] -> Sum '[] -> Bool
(==) = [Char] -> Sum '[] -> Sum '[] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"(==) base case: impossible by construction"
{-# INLINE CONLIKE (==) #-}
instance Show (Sum '[]) where
showsPrec :: Int -> Sum '[] -> ShowS
showsPrec Int
n Sum '[]
uv = [Char] -> ShowS
forall a. HasCallStack => [Char] -> a
error [Char]
"show base case: impossible by construction"
instance (Show x, Typeable x, Show (Sum xs)) => Show (Sum (x ': xs)) where
showsPrec :: Int -> Sum (x : xs) -> ShowS
showsPrec Int
d uv :: Sum (x : xs)
uv@(UnsafeInj Word
tag' Any
x)
| Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
[Char] -> ShowS
showString [Char]
"Inj @"
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ShowS -> ShowS
showParen Bool
True (Int -> TypeRep -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Proxy x -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy x
forall k (t :: k). Proxy t
Proxy @x)))
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString [Char]
" "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ShowS -> ShowS
showParen Bool
True (Int -> x -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec @x (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Any -> x
forall a b. a -> b
unsafeCoerce Any
x))
| Bool
otherwise = Int -> Sum xs -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec @(Sum xs) Int
d (Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv)
class Weaken xs ys where
weaken :: Sum xs -> Sum ys
instance (Weaken xs ys, x `HasTagIn` ys) => Weaken (x ': xs) ys where
weaken :: Sum (x : xs) -> Sum ys
weaken uv :: Sum (x : xs)
uv@(UnsafeInj Word
tag' Any
x) =
if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0
then Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn x ys => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @ys) Any
x
else let UnsafeInj Word
tag'' Any
_ = Sum xs -> Sum ys
forall (xs :: [*]) (ys :: [*]). Weaken xs ys => Sum xs -> Sum ys
weaken @xs @ys (Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv) in Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
tag'' Any
x
{-# INLINE CONLIKE weaken #-}
instance Weaken '[] ys where
weaken :: Sum '[] -> Sum ys
weaken = [Char] -> Sum '[] -> Sum ys
forall a. HasCallStack => [Char] -> a
error [Char]
"weaken base case: impossible by construction"
{-# INLINE CONLIKE weaken #-}
class UnorderedMatch xs matcher where
unorderedMatch :: Sum xs -> matcher
instance UnorderedMatch '[] r where
unorderedMatch :: Sum '[] -> r
unorderedMatch = [Char] -> Sum '[] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"unordered match base case: impossible by construction"
instance
( Result matcher ~ r
, Match (Unmatcher matcher r)
, Matcher (Unmatcher matcher r) r ~ matcher
, y `HasTagIn` xs
, UnorderedMatch (Delete y xs) matcher
) => UnorderedMatch xs ((y -> r) -> matcher) where
unorderedMatch :: Sum xs -> (y -> r) -> matcher
unorderedMatch :: Sum xs -> (y -> r) -> matcher
unorderedMatch uv :: Sum xs
uv@(UnsafeInj Word
tag' Any
x) y -> r
f =
if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn y xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @y @xs
then r
-> Matcher (Unmatcher matcher r) r
-> Matcher (Unmatcher matcher r) r
forall (xs :: [*]) r. Match xs => r -> Matcher xs r -> Matcher xs r
override @(Unmatcher matcher r) @r (y -> r
f (Any -> y
forall a b. a -> b
unsafeCoerce Any
x)) (Matcher (Unmatcher matcher r) r
-> Matcher (Unmatcher matcher r) r)
-> Matcher (Unmatcher matcher r) r
-> Matcher (Unmatcher matcher r) r
forall a b. (a -> b) -> a -> b
$ Sum (Delete y xs) -> matcher
forall (xs :: [*]) matcher.
UnorderedMatch xs matcher =>
Sum xs -> matcher
unorderedMatch @(Delete y xs) @matcher (Sum xs -> Sum (Delete y xs)
forall x (xs :: [*]). HasTagIn x xs => Sum xs -> Sum (Delete x xs)
unsafeForget @y Sum xs
uv)
else Sum (Delete y xs) -> matcher
forall (xs :: [*]) matcher.
UnorderedMatch xs matcher =>
Sum xs -> matcher
unorderedMatch @(Delete y xs) @matcher (Sum xs -> Sum (Delete y xs)
forall x (xs :: [*]). HasTagIn x xs => Sum xs -> Sum (Delete x xs)
unsafeForget @y Sum xs
uv)
type family Result matcher :: Type where
Result ((x -> r) -> matcher) = r
Result r = r
type family Unmatcher matcher r :: [Type] where
Unmatcher r r = '[]
Unmatcher ((x -> r) -> matcher) r = x ': Unmatcher matcher r
type family Matcher xs r :: Type where
Matcher '[] r = r
Matcher (x ': xs) r = (x -> r) -> Matcher xs r
class Match xs where
match :: forall r. Sum xs -> Matcher xs r
unmatch :: (forall r. Matcher xs r) -> Sum xs
override :: forall r. r -> Matcher xs r -> Matcher xs r
instance Match '[] where
match :: Sum '[] -> Matcher '[] r
match = [Char] -> Sum '[] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"match base case: impossible by construction"
{-# INLINE CONLIKE match #-}
unmatch :: (forall r. Matcher '[] r) -> Sum '[]
unmatch forall r. Matcher '[] r
r = Sum '[]
forall r. Matcher '[] r
r
{-# INLINE CONLIKE unmatch #-}
override :: r -> Matcher '[] r -> Matcher '[] r
override = r -> Matcher '[] r -> Matcher '[] r
forall a b. a -> b -> a
const
{-# INLINE CONLIKE override #-}
instance (Unmatch xs (x ': xs), Match xs) => Match (x ': xs) where
match :: forall r. Sum (x ': xs) -> (x -> r) -> Matcher xs r
match :: Sum (x : xs) -> (x -> r) -> Matcher xs r
match uv :: Sum (x : xs)
uv@(UnsafeInj Word
tag' Any
x) x -> r
f =
if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0
then r -> Matcher xs r -> Matcher xs r
forall (xs :: [*]) r. Match xs => r -> Matcher xs r -> Matcher xs r
override @xs @r (x -> r
f (Any -> x
forall a b. a -> b
unsafeCoerce Any
x)) (Matcher xs r -> Matcher xs r) -> Matcher xs r -> Matcher xs r
forall a b. (a -> b) -> a -> b
$ Sum xs -> Matcher xs r
forall (xs :: [*]) r. Match xs => Sum xs -> Matcher xs r
match @xs @r (Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv)
else Sum xs -> Matcher xs r
forall (xs :: [*]) r. Match xs => Sum xs -> Matcher xs r
match @xs @r (Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv)
{-# INLINE CONLIKE match #-}
unmatch :: (forall r. (x -> r) -> Matcher xs r) -> Sum (x ': xs)
unmatch :: (forall r. (x -> r) -> Matcher xs r) -> Sum (x : xs)
unmatch forall r. (x -> r) -> Matcher xs r
g = forall (ys :: [*]). Unmatch xs ys => Matcher xs (Sum ys) -> Sum ys
forall (xs :: [*]) (ys :: [*]).
Unmatch xs ys =>
Matcher xs (Sum ys) -> Sum ys
unmatchGo @xs (Matcher xs (Sum (x : xs)) -> Sum (x : xs))
-> Matcher xs (Sum (x : xs)) -> Sum (x : xs)
forall a b. (a -> b) -> a -> b
$ (x -> Sum (x : xs)) -> Matcher xs (Sum (x : xs))
forall r. (x -> r) -> Matcher xs r
g @(Sum (x ': xs)) (Word -> Any -> Sum (x : xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
0 (Any -> Sum (x : xs)) -> (x -> Any) -> x -> Sum (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. x -> b
forall a b. a -> b
unsafeCoerce @x)
{-# INLINE CONLIKE unmatch #-}
override :: r -> Matcher (x : xs) r -> Matcher (x : xs) r
override r
r Matcher (x : xs) r
m = (Matcher xs r -> Matcher xs r)
-> ((x -> r) -> Matcher xs r) -> (x -> r) -> Matcher xs r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (r -> Matcher xs r -> Matcher xs r
forall (xs :: [*]) r. Match xs => r -> Matcher xs r -> Matcher xs r
override @xs r
r) Matcher (x : xs) r
(x -> r) -> Matcher xs r
m
{-# INLINE CONLIKE override #-}
class Unmatch xs ys where
unmatchGo :: Matcher xs (Sum ys) -> Sum ys
instance Unmatch '[] ys where
unmatchGo :: Matcher '[] (Sum ys) -> Sum ys
unmatchGo = Matcher '[] (Sum ys) -> Sum ys
forall a. a -> a
id
{-# INLINE CONLIKE unmatchGo #-}
instance (Unmatch xs ys, x `HasTagIn` ys) => Unmatch (x ': xs) ys where
unmatchGo :: Matcher (x : xs) (Sum ys) -> Sum ys
unmatchGo Matcher (x : xs) (Sum ys)
f = Matcher xs (Sum ys) -> Sum ys
forall (xs :: [*]) (ys :: [*]).
Unmatch xs ys =>
Matcher xs (Sum ys) -> Sum ys
unmatchGo @xs (Matcher (x : xs) (Sum ys)
(x -> Sum ys) -> Matcher xs (Sum ys)
f (Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn x ys => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @ys) (Any -> Sum ys) -> (x -> Any) -> x -> Sum ys
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. x -> b
forall a b. a -> b
unsafeCoerce @x))
{-# INLINE CONLIKE unmatchGo #-}
class ForAll c xs => ApplyFunction c xs where
apply :: (forall a. c a => a -> y) -> Sum xs -> y
instance ApplyFunction c '[] where
apply :: (forall a. c a => a -> y) -> Sum '[] -> y
apply forall a. c a => a -> y
_f Sum '[]
x = [Char] -> y
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: empty sum"
{-# INLINE CONLIKE apply #-}
instance (c x, ApplyFunction c xs) => ApplyFunction c (x ': xs) where
apply :: (forall a. c a => a -> y) -> Sum (x : xs) -> y
apply forall a. c a => a -> y
f Sum (x : xs)
x = case Sum (x : xs) -> Either (Sum xs) x
forall x (xs :: [*]). Sum (x : xs) -> Either (Sum xs) x
considerFirst Sum (x : xs)
x of
Right x
x' -> x -> y
forall a. c a => a -> y
f x
x'
Left Sum xs
xs -> (forall a. c a => a -> y) -> Sum xs -> y
forall (c :: * -> Constraint) (xs :: [*]) y.
ApplyFunction c xs =>
(forall a. c a => a -> y) -> Sum xs -> y
apply @c forall a. c a => a -> y
f Sum xs
xs
{-# INLINE CONLIKE apply #-}