{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Diverse.Which.Internal (
Which(..)
, impossible
, impossible'
, pick
, pick0
, pickOnly
, pickL
, pickTag
, pickN
, obvious
, trial
, trial'
, trial0
, trial0'
, trialL
, trialL'
, trialTag
, trialTag'
, trialN
, trialN'
, pattern W
, Diversify
, diversify
, diversify'
, diversify0
, DiversifyL
, diversifyL
, DiversifyN
, diversifyN
, Reinterpret
, reinterpret
, Reinterpret'
, reinterpret'
, ReinterpretL
, reinterpretL
, ReinterpretL'
, reinterpretL'
, ReinterpretN'
, reinterpretN'
, Switch
, switch
, which
, Switcher(..)
, SwitchN
, switchN
, whichN
, SwitcherN(..)
) where
import Control.Applicative
import Control.DeepSeq
import Control.Monad
import Data.Diverse.AFunctor
import Data.Diverse.ATraversable
import Data.Diverse.Case
import Data.Diverse.CaseFunc
import Data.Diverse.Reduce
import Data.Diverse.Reiterate
import Data.Diverse.TypeLevel
import Data.Kind
import Data.Semigroup (Semigroup(..))
import Data.Tagged
import Data.Void
import GHC.Exts (Any)
import qualified GHC.Generics as G
import GHC.TypeLits
import Text.ParserCombinators.ReadPrec
import Text.Read
import qualified Text.Read.Lex as L
import Unsafe.Coerce
data Which (xs :: [Type]) = Which {-# UNPACK #-} !Int Any
type role Which representational
instance G.Generic (Which '[]) where
type Rep (Which '[]) = G.V1
from :: forall x. Which '[] -> Rep (Which '[]) x
from Which '[]
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"No generic representation for Which '[]"
to :: forall x. Rep (Which '[]) x -> Which '[]
to Rep (Which '[]) x
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"No values for Which '[]"
instance G.Generic (Which '[x]) where
type Rep (Which '[x]) = G.Rec0 x
from :: forall x. Which '[x] -> Rep (Which '[x]) x
from Which '[x]
v = forall k i c (p :: k). c -> K1 i c p
G.K1 (forall a. Which '[a] -> a
obvious Which '[x]
v)
to :: forall x. Rep (Which '[x]) x -> Which '[x]
to ( G.K1 x
a) = forall x. x -> Which '[x]
pickOnly x
a
instance G.Generic (Which (x ': x' ': xs)) where
type Rep (Which (x ': x' ': xs)) = (G.Rec0 x) G.:+: (G.Rec0 (Which (x' ': xs)))
from :: forall x. Which (x : x' : xs) -> Rep (Which (x : x' : xs)) x
from Which (x : x' : xs)
v = case forall x (xs :: [*]). Which (x : xs) -> Either (Which xs) x
trial0 Which (x : x' : xs)
v of
Right x
x -> forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
G.L1 ( forall k i c (p :: k). c -> K1 i c p
G.K1 x
x)
Left Which (x' : xs)
v' -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
G.R1 ( forall k i c (p :: k). c -> K1 i c p
G.K1 Which (x' : xs)
v')
to :: forall x. Rep (Which (x : x' : xs)) x -> Which (x : x' : xs)
to Rep (Which (x : x' : xs)) x
x = case Rep (Which (x : x' : xs)) x
x of
G.L1 ( G.K1 x
a) -> forall x (xs :: [*]). x -> Which (x : xs)
pick0 x
a
G.R1 ( G.K1 Which (x' : xs)
v) -> forall x (xs :: [*]). Which xs -> Which (x : xs)
diversify0 Which (x' : xs)
v
instance Semigroup (Which '[]) where
Which '[]
a <> :: Which '[] -> Which '[] -> Which '[]
<> Which '[]
_ = Which '[]
a
impossible :: Which '[] -> a
impossible :: forall a. Which '[] -> a
impossible Which '[]
a = case Which '[]
a of {}
impossible' :: Which '[Void] -> a
impossible' :: forall a. Which '[Void] -> a
impossible' Which '[Void]
a = case Which '[Void]
a of {}
pick :: forall x xs. UniqueMember x xs => x -> Which xs
pick :: forall x (xs :: [*]). UniqueMember x xs => x -> Which xs
pick = forall x (xs :: [*]) (n :: Nat).
(NatToInt n, n ~ IndexOf x xs) =>
x -> Which xs
pick_
pick_ :: forall x xs n. (NatToInt n, n ~ IndexOf x xs) => x -> Which xs
pick_ :: forall x (xs :: [*]) (n :: Nat).
(NatToInt n, n ~ IndexOf x xs) =>
x -> Which xs
pick_ = forall (xs :: [*]). Int -> Any -> Which xs
Which (forall (n :: Nat). NatToInt n => Int
natToInt @n) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b
unsafeCoerce
pickL :: forall l x xs. (UniqueLabelMember l xs, x ~ KindAtLabel l xs)
=> x -> Which xs
pickL :: forall {k1} (l :: k1) x (xs :: [*]).
(UniqueLabelMember l xs, x ~ KindAtLabel l xs) =>
x -> Which xs
pickL = forall x (xs :: [*]) (n :: Nat).
(NatToInt n, n ~ IndexOf x xs) =>
x -> Which xs
pick_ @x
pickTag :: forall l x xs . (UniqueMember (Tagged l x) xs)
=> x -> Which xs
pickTag :: forall {k} (l :: k) x (xs :: [*]).
UniqueMember (Tagged l x) xs =>
x -> Which xs
pickTag x
a = forall x (xs :: [*]). UniqueMember x xs => x -> Which xs
pick @(Tagged l x) (forall {k} (s :: k) b. b -> Tagged s b
Tagged @l x
a)
pickOnly :: x -> Which '[x]
pickOnly :: forall x. x -> Which '[x]
pickOnly = forall x (xs :: [*]). x -> Which (x : xs)
pick0
pick0 :: x -> Which (x ': xs)
pick0 :: forall x (xs :: [*]). x -> Which (x : xs)
pick0 = forall (xs :: [*]). Int -> Any -> Which xs
Which Int
0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b
unsafeCoerce
pickN :: forall n x xs. MemberAt n x xs => x -> Which xs
pickN :: forall (n :: Nat) x (xs :: [*]). MemberAt n x xs => x -> Which xs
pickN = forall (xs :: [*]). Int -> Any -> Which xs
Which (forall (n :: Nat). NatToInt n => Int
natToInt @n) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b
unsafeCoerce
obvious :: Which '[a] -> a
obvious :: forall a. Which '[a] -> a
obvious (Which Int
_ Any
v) = forall a b. a -> b
unsafeCoerce Any
v
trial_
:: forall n x xs.
(NatToInt n, n ~ IndexOf x xs)
=> Which xs -> Either (Which (Remove x xs)) x
trial_ :: forall (n :: Nat) x (xs :: [*]).
(NatToInt n, n ~ IndexOf x xs) =>
Which xs -> Either (Which (Remove x xs)) x
trial_ (Which Int
n Any
v) = let i :: Int
i = forall (n :: Nat). NatToInt n => Int
natToInt @n
in if Int
n forall a. Eq a => a -> a -> Bool
== Int
i
then forall a b. b -> Either a b
Right (forall a b. a -> b
unsafeCoerce Any
v)
else if Int
n forall a. Ord a => a -> a -> Bool
> Int
i
then forall a b. a -> Either a b
Left (forall (xs :: [*]). Int -> Any -> Which xs
Which (Int
n forall a. Num a => a -> a -> a
- Int
1) Any
v)
else forall a b. a -> Either a b
Left (forall (xs :: [*]). Int -> Any -> Which xs
Which Int
n Any
v)
trialN
:: forall n x xs.
(MemberAt n x xs)
=> Which xs -> Either (Which (RemoveIndex n xs)) x
trialN :: forall (n :: Nat) x (xs :: [*]).
MemberAt n x xs =>
Which xs -> Either (Which (RemoveIndex n xs)) x
trialN (Which Int
n Any
v) = let i :: Int
i = forall (n :: Nat). NatToInt n => Int
natToInt @n
in if Int
n forall a. Eq a => a -> a -> Bool
== Int
i
then forall a b. b -> Either a b
Right (forall a b. a -> b
unsafeCoerce Any
v)
else if Int
n forall a. Ord a => a -> a -> Bool
> Int
i
then forall a b. a -> Either a b
Left (forall (xs :: [*]). Int -> Any -> Which xs
Which (Int
n forall a. Num a => a -> a -> a
- Int
1) Any
v)
else forall a b. a -> Either a b
Left (forall (xs :: [*]). Int -> Any -> Which xs
Which Int
n Any
v)
trial
:: forall x xs.
(UniqueMember x xs)
=> Which xs -> Either (Which (Remove x xs)) x
trial :: forall x (xs :: [*]).
UniqueMember x xs =>
Which xs -> Either (Which (Remove x xs)) x
trial = forall (n :: Nat) x (xs :: [*]).
(NatToInt n, n ~ IndexOf x xs) =>
Which xs -> Either (Which (Remove x xs)) x
trial_
trialL
:: forall l x xs.
(UniqueLabelMember l xs, x ~ KindAtLabel l xs)
=> Which xs -> Either (Which (Remove x xs)) x
trialL :: forall {k1} (l :: k1) x (xs :: [*]).
(UniqueLabelMember l xs, x ~ KindAtLabel l xs) =>
Which xs -> Either (Which (Remove x xs)) x
trialL = forall (n :: Nat) x (xs :: [*]).
(NatToInt n, n ~ IndexOf x xs) =>
Which xs -> Either (Which (Remove x xs)) x
trial_ @_ @x
trial_'
:: forall n x xs.
(NatToInt n, n ~ IndexOf x xs)
=> Which xs -> Maybe x
trial_' :: forall (n :: Nat) x (xs :: [*]).
(NatToInt n, n ~ IndexOf x xs) =>
Which xs -> Maybe x
trial_' (Which Int
n Any
v) = let i :: Int
i = forall (n :: Nat). NatToInt n => Int
natToInt @n
in if Int
n forall a. Eq a => a -> a -> Bool
== Int
i
then forall a. a -> Maybe a
Just (forall a b. a -> b
unsafeCoerce Any
v)
else forall a. Maybe a
Nothing
trialTag
:: forall l x xs.
(UniqueMember (Tagged l x) xs)
=> Which xs -> Either (Which (Remove (Tagged l x) xs)) x
trialTag :: forall {k} (l :: k) x (xs :: [*]).
UniqueMember (Tagged l x) xs =>
Which xs -> Either (Which (Remove (Tagged l x) xs)) x
trialTag Which xs
xs = forall {k} (s :: k) b. Tagged s b -> b
unTagged forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall x (xs :: [*]).
UniqueMember x xs =>
Which xs -> Either (Which (Remove x xs)) x
trial @(Tagged l x) Which xs
xs
trialN'
:: forall n x xs.
(MemberAt n x xs)
=> Which xs -> Maybe x
trialN' :: forall (n :: Nat) x (xs :: [*]).
MemberAt n x xs =>
Which xs -> Maybe x
trialN' (Which Int
n Any
v) = let i :: Int
i = forall (n :: Nat). NatToInt n => Int
natToInt @n
in if Int
n forall a. Eq a => a -> a -> Bool
== Int
i
then forall a. a -> Maybe a
Just (forall a b. a -> b
unsafeCoerce Any
v)
else forall a. Maybe a
Nothing
trial'
:: forall x xs.
(UniqueMember x xs)
=> Which xs -> Maybe x
trial' :: forall x (xs :: [*]). UniqueMember x xs => Which xs -> Maybe x
trial' = forall (n :: Nat) x (xs :: [*]).
(NatToInt n, n ~ IndexOf x xs) =>
Which xs -> Maybe x
trial_'
trialL'
:: forall l x xs.
(UniqueLabelMember l xs, x ~ KindAtLabel l xs)
=> Which xs -> Maybe x
trialL' :: forall {k1} (l :: k1) x (xs :: [*]).
(UniqueLabelMember l xs, x ~ KindAtLabel l xs) =>
Which xs -> Maybe x
trialL' = forall (n :: Nat) x (xs :: [*]).
(NatToInt n, n ~ IndexOf x xs) =>
Which xs -> Maybe x
trial_' @_ @x
trialTag'
:: forall l x xs.
(UniqueMember (Tagged l x) xs)
=> Which xs -> Maybe x
trialTag' :: forall {k} (l :: k) x (xs :: [*]).
UniqueMember (Tagged l x) xs =>
Which xs -> Maybe x
trialTag' Which xs
xs = forall {k} (s :: k) b. Tagged s b -> b
unTagged forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall x (xs :: [*]). UniqueMember x xs => Which xs -> Maybe x
trial' @(Tagged l x) Which xs
xs
trial0 :: forall x xs. Which (x ': xs) -> Either (Which xs) x
trial0 :: forall x (xs :: [*]). Which (x : xs) -> Either (Which xs) x
trial0 (Which Int
n Any
v) = if Int
n forall a. Eq a => a -> a -> Bool
== Int
0
then forall a b. b -> Either a b
Right (forall a b. a -> b
unsafeCoerce Any
v)
else forall a b. a -> Either a b
Left (forall (xs :: [*]). Int -> Any -> Which xs
Which (Int
n forall a. Num a => a -> a -> a
- Int
1) Any
v)
trial0' :: forall x xs. Which (x ': xs) -> Maybe x
trial0' :: forall x (xs :: [*]). Which (x : xs) -> Maybe x
trial0' (Which Int
n Any
v) = if Int
n forall a. Eq a => a -> a -> Bool
== Int
0
then forall a. a -> Maybe a
Just (forall a b. a -> b
unsafeCoerce Any
v)
else forall a. Maybe a
Nothing
pattern W :: forall x xs. (UniqueMember x xs) => x -> Which xs
pattern $bW :: forall x (xs :: [*]). UniqueMember x xs => x -> Which xs
$mW :: forall {r} {x} {xs :: [*]}.
UniqueMember x xs =>
Which xs -> (x -> r) -> ((# #) -> r) -> r
W x <- (trial' -> Just x)
where W x
x = forall x (xs :: [*]). UniqueMember x xs => x -> Which xs
pick x
x
type Diversify (branch :: [Type]) (tree :: [Type]) = Switch (CaseDiversify branch tree) (Which tree) branch
diversify :: forall branch tree. Diversify branch tree => Which branch -> Which tree
diversify :: forall (branch :: [*]) (tree :: [*]).
Diversify branch tree =>
Which branch -> Which tree
diversify = forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
c r xs -> Which xs -> r
which (forall {k} (branch :: [*]) (tree :: [*]) (r :: k) (branch' :: [*]).
CaseDiversify branch tree r branch'
CaseDiversify @branch @tree @_ @branch)
data CaseDiversify (branch :: [Type]) (tree :: [Type]) r (branch' :: [Type]) = CaseDiversify
type instance CaseResult (CaseDiversify branch tree r) x = r
instance Reiterate (CaseDiversify r branch tree) branch' where
reiterate :: CaseDiversify r branch tree branch'
-> CaseDiversify r branch tree (Tail branch')
reiterate CaseDiversify r branch tree branch'
CaseDiversify = forall {k} (branch :: [*]) (tree :: [*]) (r :: k) (branch' :: [*]).
CaseDiversify branch tree r branch'
CaseDiversify
instance (UniqueMember x tree, Unique x branch) =>
Case (CaseDiversify branch tree (Which tree)) (x ': branch') where
case' :: CaseDiversify branch tree (Which tree) (x : branch')
-> Head (x : branch')
-> CaseResult
(CaseDiversify branch tree (Which tree)) (Head (x : branch'))
case' CaseDiversify branch tree (Which tree) (x : branch')
CaseDiversify = forall x (xs :: [*]). UniqueMember x xs => x -> Which xs
pick
diversify0 :: forall x xs. Which xs -> Which (x ': xs)
diversify0 :: forall x (xs :: [*]). Which xs -> Which (x : xs)
diversify0 (Which Int
n Any
v) = forall (xs :: [*]). Int -> Any -> Which xs
Which (Int
n forall a. Num a => a -> a -> a
+ Int
1) Any
v
diversify' :: forall branch tree. (Diversify branch tree, SameLength branch tree) => Which branch -> Which tree
diversify' :: forall (branch :: [*]) (tree :: [*]).
(Diversify branch tree, SameLength branch tree) =>
Which branch -> Which tree
diversify' = forall (branch :: [*]) (tree :: [*]).
Diversify branch tree =>
Which branch -> Which tree
diversify
type DiversifyL (ls :: [k]) (branch :: [Type]) (tree :: [Type]) =
( Diversify branch tree
, branch ~ KindsAtLabels ls tree
, UniqueLabels ls tree
, IsDistinct ls
)
diversifyL :: forall ls branch tree. (DiversifyL ls branch tree) => Which branch -> Which tree
diversifyL :: forall {k} (ls :: [k]) (branch :: [*]) (tree :: [*]).
DiversifyL ls branch tree =>
Which branch -> Which tree
diversifyL = forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
c r xs -> Which xs -> r
which (forall {k} (branch :: [*]) (tree :: [*]) (r :: k) (branch' :: [*]).
CaseDiversify branch tree r branch'
CaseDiversify @branch @tree @_ @branch)
type DiversifyN (ns :: [Nat]) (branch :: [Type]) (tree :: [Type]) =
( SwitchN Which (CaseDiversifyN ns) (Which tree) 0 branch
, KindsAtIndices ns tree ~ branch
)
diversifyN :: forall ns branch tree. (DiversifyN ns branch tree) => Which branch -> Which tree
diversifyN :: forall (ns :: [Nat]) (branch :: [*]) (tree :: [*]).
DiversifyN ns branch tree =>
Which branch -> Which tree
diversifyN = forall {k} (w :: k -> *) (c :: * -> Nat -> k -> *) r (n :: Nat)
(xs :: k).
SwitchN w c r n xs =>
c r n xs -> w xs -> r
whichN (forall {k} (ns :: [Nat]) (r :: k) (n :: Nat) (branch' :: [*]).
CaseDiversifyN ns r n branch'
CaseDiversifyN @ns @_ @0 @branch)
data CaseDiversifyN (ns :: [Nat]) r (n :: Nat) (branch' :: [Type]) = CaseDiversifyN
type instance CaseResult (CaseDiversifyN ns r n) x = r
instance ReiterateN (CaseDiversifyN ns r) n branch' where
reiterateN :: CaseDiversifyN ns r n branch'
-> CaseDiversifyN ns r (n + 1) (Tail branch')
reiterateN CaseDiversifyN ns r n branch'
CaseDiversifyN = forall {k} (ns :: [Nat]) (r :: k) (n :: Nat) (branch' :: [*]).
CaseDiversifyN ns r n branch'
CaseDiversifyN
instance MemberAt (KindAtIndex n ns) x tree =>
Case (CaseDiversifyN ns (Which tree) n) (x ': branch') where
case' :: CaseDiversifyN ns (Which tree) n (x : branch')
-> Head (x : branch')
-> CaseResult
(CaseDiversifyN ns (Which tree) n) (Head (x : branch'))
case' CaseDiversifyN ns (Which tree) n (x : branch')
CaseDiversifyN Head (x : branch')
v = forall (n :: Nat) x (xs :: [*]). MemberAt n x xs => x -> Which xs
pickN @(KindAtIndex n ns) Head (x : branch')
v
type Reinterpret (branch :: [Type]) (tree :: [Type]) = Switch (CaseReinterpret branch tree) (Either (Which (Complement tree branch)) (Which branch)) tree
reinterpret :: forall branch tree. (Reinterpret branch tree) =>
Which tree -> Either (Which (Complement tree branch)) (Which branch)
reinterpret :: forall (branch :: [*]) (tree :: [*]).
Reinterpret branch tree =>
Which tree
-> Either (Which (Complement tree branch)) (Which branch)
reinterpret = forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
c r xs -> Which xs -> r
which (forall {k} (branch :: [*]) (tree :: [*]) (r :: k) (tree' :: [*]).
CaseReinterpret branch tree r tree'
CaseReinterpret @branch @tree @_ @tree)
data CaseReinterpret (branch :: [Type]) (tree :: [Type]) r (tree' :: [Type]) = CaseReinterpret
type instance CaseResult (CaseReinterpret branch tree r) x = r
instance Reiterate (CaseReinterpret branch tree r) tree' where
reiterate :: CaseReinterpret branch tree r tree'
-> CaseReinterpret branch tree r (Tail tree')
reiterate CaseReinterpret branch tree r tree'
CaseReinterpret = forall {k} (branch :: [*]) (tree :: [*]) (r :: k) (tree' :: [*]).
CaseReinterpret branch tree r tree'
CaseReinterpret
instance ( MaybeUniqueMember x branch
, comp ~ Complement tree branch
, MaybeUniqueMember x comp
, Unique x tree
) =>
Case (CaseReinterpret branch tree (Either (Which comp) (Which branch))) (x ': tree') where
case' :: CaseReinterpret
branch tree (Either (Which comp) (Which branch)) (x : tree')
-> Head (x : tree')
-> CaseResult
(CaseReinterpret branch tree (Either (Which comp) (Which branch)))
(Head (x : tree'))
case' CaseReinterpret
branch tree (Either (Which comp) (Which branch)) (x : tree')
CaseReinterpret Head (x : tree')
a =
case forall (n :: Nat). NatToInt n => Int
natToInt @(PositionOf x branch) of
Int
0 -> let j :: Int
j = forall (n :: Nat). NatToInt n => Int
natToInt @(PositionOf x comp)
in forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall (xs :: [*]). Int -> Any -> Which xs
Which (Int
j forall a. Num a => a -> a -> a
- Int
1) (forall a b. a -> b
unsafeCoerce Head (x : tree')
a)
Int
i -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (xs :: [*]). Int -> Any -> Which xs
Which (Int
i forall a. Num a => a -> a -> a
- Int
1) (forall a b. a -> b
unsafeCoerce Head (x : tree')
a)
type Reinterpret' (branch :: [Type]) (tree :: [Type]) = Switch (CaseReinterpret' branch tree) (Maybe (Which branch)) tree
reinterpret' :: forall branch tree. (Reinterpret' branch tree) => Which tree -> Maybe (Which branch)
reinterpret' :: forall (branch :: [*]) (tree :: [*]).
Reinterpret' branch tree =>
Which tree -> Maybe (Which branch)
reinterpret' = forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
c r xs -> Which xs -> r
which (forall {k} (branch :: [*]) (tree :: [*]) (r :: k) (tree' :: [*]).
CaseReinterpret' branch tree r tree'
CaseReinterpret' @branch @tree @_ @tree)
data CaseReinterpret' (branch :: [Type]) (tree :: [Type]) r (tree' :: [Type]) = CaseReinterpret'
type instance CaseResult (CaseReinterpret' branch tree r) x = r
instance Reiterate (CaseReinterpret' branch tree r) tree' where
reiterate :: CaseReinterpret' branch tree r tree'
-> CaseReinterpret' branch tree r (Tail tree')
reiterate CaseReinterpret' branch tree r tree'
CaseReinterpret' = forall {k} (branch :: [*]) (tree :: [*]) (r :: k) (tree' :: [*]).
CaseReinterpret' branch tree r tree'
CaseReinterpret'
instance ( MaybeUniqueMember x branch
, comp ~ Complement tree branch
, Unique x tree
) =>
Case (CaseReinterpret' branch tree (Maybe (Which branch))) (x ': tree') where
case' :: CaseReinterpret' branch tree (Maybe (Which branch)) (x : tree')
-> Head (x : tree')
-> CaseResult
(CaseReinterpret' branch tree (Maybe (Which branch)))
(Head (x : tree'))
case' CaseReinterpret' branch tree (Maybe (Which branch)) (x : tree')
CaseReinterpret' Head (x : tree')
a =
case forall (n :: Nat). NatToInt n => Int
natToInt @(PositionOf x branch) of
Int
0 -> forall a. Maybe a
Nothing
Int
i -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (xs :: [*]). Int -> Any -> Which xs
Which (Int
i forall a. Num a => a -> a -> a
- Int
1) (forall a b. a -> b
unsafeCoerce Head (x : tree')
a)
type ReinterpretL (ls :: [k]) (branch :: [Type]) (tree :: [Type]) =
( Reinterpret branch tree
, branch ~ KindsAtLabels ls tree
, UniqueLabels ls tree
, IsDistinct ls
)
reinterpretL :: forall ls branch tree. (ReinterpretL ls branch tree)
=> Which tree -> Either (Which (Complement tree branch)) (Which branch)
reinterpretL :: forall {k} (ls :: [k]) (branch :: [*]) (tree :: [*]).
ReinterpretL ls branch tree =>
Which tree
-> Either (Which (Complement tree branch)) (Which branch)
reinterpretL = forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
c r xs -> Which xs -> r
which (forall {k} (branch :: [*]) (tree :: [*]) (r :: k) (tree' :: [*]).
CaseReinterpret branch tree r tree'
CaseReinterpret @branch @tree @_ @tree)
type ReinterpretL' (ls :: [k]) (branch :: [Type]) (tree :: [Type]) =
( Reinterpret' branch tree
, branch ~ KindsAtLabels ls tree
, UniqueLabels ls tree
, IsDistinct ls
)
reinterpretL' :: forall ls branch tree. (ReinterpretL' ls branch tree)
=> Which tree -> Maybe (Which branch)
reinterpretL' :: forall {k} (ls :: [k]) (branch :: [*]) (tree :: [*]).
ReinterpretL' ls branch tree =>
Which tree -> Maybe (Which branch)
reinterpretL' = forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
c r xs -> Which xs -> r
which (forall {k} (branch :: [*]) (tree :: [*]) (r :: k) (tree' :: [*]).
CaseReinterpret' branch tree r tree'
CaseReinterpret' @branch @tree @_ @tree)
type ReinterpretN' (ns :: [Nat]) (branch :: [Type]) (tree :: [Type]) =
( SwitchN Which (CaseReinterpretN' ns) (Maybe (Which branch)) 0 tree
, KindsAtIndices ns tree ~ branch)
reinterpretN' :: forall ns branch tree. (ReinterpretN' ns branch tree)
=> Which tree -> Maybe (Which branch)
reinterpretN' :: forall (ns :: [Nat]) (branch :: [*]) (tree :: [*]).
ReinterpretN' ns branch tree =>
Which tree -> Maybe (Which branch)
reinterpretN' = forall {k} (w :: k -> *) (c :: * -> Nat -> k -> *) r (n :: Nat)
(xs :: k).
SwitchN w c r n xs =>
c r n xs -> w xs -> r
whichN (forall {k} (indices :: [Nat]) (r :: k) (n :: Nat) (tree' :: [*]).
CaseReinterpretN' indices r n tree'
CaseReinterpretN' @ns @_ @0 @tree)
data CaseReinterpretN' (indices :: [Nat]) r (n :: Nat) (tree' :: [Type]) = CaseReinterpretN'
type instance CaseResult (CaseReinterpretN' indices r n) x = r
instance ReiterateN (CaseReinterpretN' indices r) n tree' where
reiterateN :: CaseReinterpretN' indices r n tree'
-> CaseReinterpretN' indices r (n + 1) (Tail tree')
reiterateN CaseReinterpretN' indices r n tree'
CaseReinterpretN' = forall {k} (indices :: [Nat]) (r :: k) (n :: Nat) (tree' :: [*]).
CaseReinterpretN' indices r n tree'
CaseReinterpretN'
instance (MaybeMemberAt n' x branch, n' ~ PositionOf n indices) =>
Case (CaseReinterpretN' indices (Maybe (Which branch)) n) (x ': tree) where
case' :: CaseReinterpretN' indices (Maybe (Which branch)) n (x : tree)
-> Head (x : tree)
-> CaseResult
(CaseReinterpretN' indices (Maybe (Which branch)) n)
(Head (x : tree))
case' CaseReinterpretN' indices (Maybe (Which branch)) n (x : tree)
CaseReinterpretN' Head (x : tree)
a =
case forall (n :: Nat). NatToInt n => Int
natToInt @n' of
Int
0 -> forall a. Maybe a
Nothing
Int
i -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (xs :: [*]). Int -> Any -> Which xs
Which (Int
i forall a. Num a => a -> a -> a
- Int
1) (forall a b. a -> b
unsafeCoerce Head (x : tree)
a)
newtype Switcher c r (xs :: [Type]) = Switcher (c r xs)
type instance Reduced (Switcher c r xs) = r
instance ( Case (c r) (x ': x' ': xs)
, Reduce (Which (x' ': xs)) (Switcher c r (x' ': xs))
, Reiterate (c r) (x : x' : xs)
, r ~ CaseResult (c r) x
) =>
Reduce (Which (x ': x' ': xs)) (Switcher c r (x ': x' ': xs)) where
reduce :: Switcher c r (x : x' : xs)
-> Which (x : x' : xs) -> Reduced (Switcher c r (x : x' : xs))
reduce (Switcher c r (x : x' : xs)
c) Which (x : x' : xs)
v =
case forall x (xs :: [*]). Which (x : xs) -> Either (Which xs) x
trial0 Which (x : x' : xs)
v of
Right x
a -> forall (c :: [*] -> *) (xs :: [*]).
Case c xs =>
c xs -> Head xs -> CaseResult c (Head xs)
case' c r (x : x' : xs)
c x
a
Left Which (x' : xs)
v' -> forall v handler.
Reduce v handler =>
handler -> v -> Reduced handler
reduce (forall {k} (c :: k -> [*] -> *) (r :: k) (xs :: [*]).
c r xs -> Switcher c r xs
Switcher (forall (c :: [*] -> *) (xs :: [*]).
Reiterate c xs =>
c xs -> c (Tail xs)
reiterate c r (x : x' : xs)
c)) Which (x' : xs)
v'
{-# INLINABLE reduce #-}
instance (Case (c r) '[x], r ~ CaseResult (c r) x) => Reduce (Which '[x]) (Switcher c r '[x]) where
reduce :: Switcher c r '[x] -> Which '[x] -> Reduced (Switcher c r '[x])
reduce (Switcher c r '[x]
c) Which '[x]
v = case forall a. Which '[a] -> a
obvious Which '[x]
v of
x
a -> forall (c :: [*] -> *) (xs :: [*]).
Case c xs =>
c xs -> Head xs -> CaseResult c (Head xs)
case' c r '[x]
c x
a
instance Reduce (Which '[]) (Switcher c r '[]) where
reduce :: Switcher c r '[] -> Which '[] -> Reduced (Switcher c r '[])
reduce Switcher c r '[]
_ = forall a. Which '[] -> a
impossible
instance Reduce (Void) (Switcher c r '[]) where
reduce :: Switcher c r '[] -> Void -> Reduced (Switcher c r '[])
reduce Switcher c r '[]
_ = forall a. Void -> a
absurd
instance Reduce (Which '[Void]) (Switcher c r '[]) where
reduce :: Switcher c r '[] -> Which '[Void] -> Reduced (Switcher c r '[])
reduce Switcher c r '[]
_ = forall a. Which '[Void] -> a
impossible'
type Switch c r xs = Reduce (Which xs) (Switcher c r xs)
switch :: Switch c r xs => Which xs -> c r xs -> r
switch :: forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
Which xs -> c r xs -> r
switch Which xs
w c r xs
c = forall v handler.
Reduce v handler =>
handler -> v -> Reduced handler
reduce (forall {k} (c :: k -> [*] -> *) (r :: k) (xs :: [*]).
c r xs -> Switcher c r xs
Switcher c r xs
c) Which xs
w
which :: Switch c r xs => c r xs -> Which xs -> r
which :: forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
c r xs -> Which xs -> r
which = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
Which xs -> c r xs -> r
switch
newtype SwitcherN c r (n :: Nat) (xs :: [Type]) = SwitcherN (c r n xs)
type instance Reduced (SwitcherN c r n xs) = r
instance ( Case (c r n) (x ': x' ': xs)
, Reduce (Which (x' ': xs)) (SwitcherN c r (n + 1) (x' ': xs))
, ReiterateN (c r) n (x : x' : xs)
, r ~ CaseResult (c r n) x
) =>
Reduce (Which (x ': x' ': xs)) (SwitcherN c r n (x ': x' ': xs)) where
reduce :: SwitcherN c r n (x : x' : xs)
-> Which (x : x' : xs) -> Reduced (SwitcherN c r n (x : x' : xs))
reduce (SwitcherN c r n (x : x' : xs)
c) Which (x : x' : xs)
v =
case forall x (xs :: [*]). Which (x : xs) -> Either (Which xs) x
trial0 Which (x : x' : xs)
v of
Right x
a -> forall (c :: [*] -> *) (xs :: [*]).
Case c xs =>
c xs -> Head xs -> CaseResult c (Head xs)
case' c r n (x : x' : xs)
c x
a
Left Which (x' : xs)
v' -> forall v handler.
Reduce v handler =>
handler -> v -> Reduced handler
reduce (forall {k} (c :: k -> Nat -> [*] -> *) (r :: k) (n :: Nat)
(xs :: [*]).
c r n xs -> SwitcherN c r n xs
SwitcherN (forall (c :: Nat -> [*] -> *) (n :: Nat) (xs :: [*]).
ReiterateN c n xs =>
c n xs -> c (n + 1) (Tail xs)
reiterateN c r n (x : x' : xs)
c)) Which (x' : xs)
v'
{-# INLINABLE reduce #-}
instance (Case (c r n) '[x], r ~ CaseResult (c r n) x) => Reduce (Which '[x]) (SwitcherN c r n '[x]) where
reduce :: SwitcherN c r n '[x]
-> Which '[x] -> Reduced (SwitcherN c r n '[x])
reduce (SwitcherN c r n '[x]
c) Which '[x]
v = case forall a. Which '[a] -> a
obvious Which '[x]
v of
x
a -> forall (c :: [*] -> *) (xs :: [*]).
Case c xs =>
c xs -> Head xs -> CaseResult c (Head xs)
case' c r n '[x]
c x
a
whichN :: SwitchN w c r n xs => c r n xs -> w xs -> r
whichN :: forall {k} (w :: k -> *) (c :: * -> Nat -> k -> *) r (n :: Nat)
(xs :: k).
SwitchN w c r n xs =>
c r n xs -> w xs -> r
whichN = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall {k} (w :: k -> *) (c :: * -> Nat -> k -> *) r (n :: Nat)
(xs :: k).
SwitchN w c r n xs =>
w xs -> c r n xs -> r
switchN
class SwitchN w c r (n :: Nat) xs where
switchN :: w xs -> c r n xs -> r
instance Reduce (Which xs) (SwitcherN c r n xs) => SwitchN Which c r n xs where
switchN :: Which xs -> c r n xs -> r
switchN Which xs
w c r n xs
c = forall v handler.
Reduce v handler =>
handler -> v -> Reduced handler
reduce (forall {k} (c :: k -> Nat -> [*] -> *) (r :: k) (n :: Nat)
(xs :: [*]).
c r n xs -> SwitcherN c r n xs
SwitcherN c r n xs
c) Which xs
w
instance (Switch CaseEqWhich Bool (x ': xs)) =>
Eq (Which (x ': xs)) where
l :: Which (x : xs)
l@(Which Int
i Any
_) == :: Which (x : xs) -> Which (x : xs) -> Bool
== (Which Int
j Any
u) =
if Int
i forall a. Eq a => a -> a -> Bool
/= Int
j
then Bool
False
else forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
Which xs -> c r xs -> r
switch Which (x : xs)
l (forall {k} (r :: k) (xs :: [*]). Any -> CaseEqWhich r xs
CaseEqWhich Any
u)
instance Eq (Which '[]) where
Which '[]
_ == :: Which '[] -> Which '[] -> Bool
== Which '[]
_ = Bool
True
newtype CaseEqWhich r (xs :: [Type]) = CaseEqWhich Any
type instance CaseResult (CaseEqWhich r) x = r
instance Reiterate (CaseEqWhich r) (x ': xs) where
reiterate :: CaseEqWhich r (x : xs) -> CaseEqWhich r (Tail (x : xs))
reiterate (CaseEqWhich Any
r) = forall {k} (r :: k) (xs :: [*]). Any -> CaseEqWhich r xs
CaseEqWhich Any
r
instance Eq x => Case (CaseEqWhich Bool) (x ': xs) where
case' :: CaseEqWhich Bool (x : xs)
-> Head (x : xs) -> CaseResult (CaseEqWhich Bool) (Head (x : xs))
case' (CaseEqWhich Any
r) Head (x : xs)
l = Head (x : xs)
l forall a. Eq a => a -> a -> Bool
== forall a b. a -> b
unsafeCoerce Any
r
instance ( Switch CaseEqWhich Bool (x ': xs)
, Switch CaseOrdWhich Ordering (x ': xs)
) =>
Ord (Which (x ': xs)) where
compare :: Which (x : xs) -> Which (x : xs) -> Ordering
compare l :: Which (x : xs)
l@(Which Int
i Any
_) (Which Int
j Any
u) =
if Int
i forall a. Eq a => a -> a -> Bool
/= Int
j
then forall a. Ord a => a -> a -> Ordering
compare Int
i Int
j
else forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
Which xs -> c r xs -> r
switch Which (x : xs)
l (forall {k} (r :: k) (xs :: [*]). Any -> CaseOrdWhich r xs
CaseOrdWhich Any
u)
instance Ord (Which '[]) where
compare :: Which '[] -> Which '[] -> Ordering
compare Which '[]
_ Which '[]
_ = Ordering
EQ
newtype CaseOrdWhich r (xs :: [Type]) = CaseOrdWhich Any
type instance CaseResult (CaseOrdWhich r) x = r
instance Reiterate (CaseOrdWhich r) (x ': xs) where
reiterate :: CaseOrdWhich r (x : xs) -> CaseOrdWhich r (Tail (x : xs))
reiterate (CaseOrdWhich Any
r) = forall {k} (r :: k) (xs :: [*]). Any -> CaseOrdWhich r xs
CaseOrdWhich Any
r
instance Ord x => Case (CaseOrdWhich Ordering) (x ': xs) where
case' :: CaseOrdWhich Ordering (x : xs)
-> Head (x : xs)
-> CaseResult (CaseOrdWhich Ordering) (Head (x : xs))
case' (CaseOrdWhich Any
r) Head (x : xs)
l = forall a. Ord a => a -> a -> Ordering
compare Head (x : xs)
l (forall a b. a -> b
unsafeCoerce Any
r)
instance (Switch CaseShowWhich ShowS (x ': xs)) =>
Show (Which (x ': xs)) where
showsPrec :: Int -> Which (x : xs) -> ShowS
showsPrec Int
d Which (x : xs)
v = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
app_prec) (forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
c r xs -> Which xs -> r
which (forall {k} (r :: k) (xs :: [*]). Int -> CaseShowWhich r xs
CaseShowWhich Int
0) Which (x : xs)
v)
where
app_prec :: Int
app_prec = Int
10
instance Show (Which '[]) where
showsPrec :: Int -> Which '[] -> ShowS
showsPrec Int
_ = forall a. Which '[] -> a
impossible
newtype CaseShowWhich r (xs :: [Type]) = CaseShowWhich Int
type instance CaseResult (CaseShowWhich r) x = r
instance Reiterate (CaseShowWhich r) (x ': xs) where
reiterate :: CaseShowWhich r (x : xs) -> CaseShowWhich r (Tail (x : xs))
reiterate (CaseShowWhich Int
i) = forall {k} (r :: k) (xs :: [*]). Int -> CaseShowWhich r xs
CaseShowWhich (Int
i forall a. Num a => a -> a -> a
+ Int
1)
instance Show x => Case (CaseShowWhich ShowS) (x ': xs) where
case' :: CaseShowWhich ShowS (x : xs)
-> Head (x : xs)
-> CaseResult (CaseShowWhich ShowS) (Head (x : xs))
case' (CaseShowWhich Int
i) Head (x : xs)
v = [Char] -> ShowS
showString [Char]
"pickN @" forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString (forall a. Show a => a -> [Char]
show Int
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec (Int
app_prec forall a. Num a => a -> a -> a
+ Int
1) Head (x : xs)
v
where app_prec :: Int
app_prec = Int
10
class WhichRead v where
whichReadPrec :: Int -> Int -> ReadPrec v
coerceReadWhich :: forall x xs. Which xs -> Which (x ': xs)
coerceReadWhich :: forall x (xs :: [*]). Which xs -> Which (x : xs)
coerceReadWhich (Which Int
i Any
x) = forall (xs :: [*]). Int -> Any -> Which xs
Which Int
i Any
x
readWhich :: forall x xs. Read x => Int -> Int -> ReadPrec (Which (x ': xs))
readWhich :: forall x (xs :: [*]).
Read x =>
Int -> Int -> ReadPrec (Which (x : xs))
readWhich Int
i Int
j = forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Int
i forall a. Eq a => a -> a -> Bool
== Int
j) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. ReadPrec a -> ReadPrec a
parens (forall a. Int -> ReadPrec a -> ReadPrec a
prec Int
app_prec forall a b. (a -> b) -> a -> b
$ (forall (xs :: [*]). Int -> Any -> Which xs
Which Int
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b
unsafeCoerce) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Read a => ReadPrec a
readPrec @x)
where
app_prec :: Int
app_prec = Int
10
instance Read x => WhichRead (Which '[x]) where
whichReadPrec :: Int -> Int -> ReadPrec (Which '[x])
whichReadPrec = forall x (xs :: [*]).
Read x =>
Int -> Int -> ReadPrec (Which (x : xs))
readWhich
instance (Read x, WhichRead (Which (x' ': xs))) => WhichRead (Which (x ': x' ': xs)) where
whichReadPrec :: Int -> Int -> ReadPrec (Which (x : x' : xs))
whichReadPrec Int
i Int
j = forall x (xs :: [*]).
Read x =>
Int -> Int -> ReadPrec (Which (x : xs))
readWhich Int
i Int
j
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall x (xs :: [*]). Which xs -> Which (x : xs)
coerceReadWhich forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall v. WhichRead v => Int -> Int -> ReadPrec v
whichReadPrec Int
i (Int
j forall a. Num a => a -> a -> a
+ Int
1) :: ReadPrec (Which (x' ': xs))))
{-# INLINABLE whichReadPrec #-}
instance WhichRead (Which (x ': xs)) =>
Read (Which (x ': xs)) where
readPrec :: ReadPrec (Which (x : xs))
readPrec =
forall a. ReadPrec a -> ReadPrec a
parens forall a b. (a -> b) -> a -> b
$ forall a. Int -> ReadPrec a -> ReadPrec a
prec Int
app_prec forall a b. (a -> b) -> a -> b
$ do
forall a. ReadP a -> ReadPrec a
lift forall a b. (a -> b) -> a -> b
$ Lexeme -> ReadP ()
L.expect ([Char] -> Lexeme
Ident [Char]
"pickN")
forall a. ReadP a -> ReadPrec a
lift forall a b. (a -> b) -> a -> b
$ Lexeme -> ReadP ()
L.expect ([Char] -> Lexeme
Punc [Char]
"@")
Int
i <- forall a. ReadP a -> ReadPrec a
lift forall a. (Eq a, Num a) => ReadP a
L.readDecP
Which Int
n Any
v <- forall v. WhichRead v => Int -> Int -> ReadPrec v
whichReadPrec Int
i Int
0 :: ReadPrec (Which (x ': xs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (xs :: [*]). Int -> Any -> Which xs
Which Int
n Any
v
where
app_prec :: Int
app_prec = Int
10
instance NFData (Which '[]) where
rnf :: Which '[] -> ()
rnf = forall a. Which '[] -> a
impossible
instance (Reduce (Which (x ': xs)) (Switcher (CaseFunc NFData) () (x ': xs))) =>
NFData (Which (x ': xs)) where
rnf :: Which (x : xs) -> ()
rnf Which (x : xs)
x = forall (c :: * -> [*] -> *) r (xs :: [*]).
Switch c r xs =>
Which xs -> c r xs -> r
switch Which (x : xs)
x (forall (k :: * -> Constraint) r (xs :: [*]).
(forall x. k x => x -> r) -> CaseFunc k r xs
CaseFunc @NFData forall a. NFData a => a -> ()
rnf)
instance AFunctor Which c '[] where
afmap :: c '[] -> Which '[] -> Which (CaseResults c '[])
afmap c '[]
_ = forall a. Which '[] -> a
impossible
instance ( Reiterate c (a ': as)
, AFunctor Which c as
, Case c (a ': as)
) =>
AFunctor Which c (a ': as) where
afmap :: c (a : as) -> Which (a : as) -> Which (CaseResults c (a : as))
afmap c (a : as)
c Which (a : as)
v = case forall x (xs :: [*]). Which (x : xs) -> Either (Which xs) x
trial0 Which (a : as)
v of
Right a
a' -> forall (xs :: [*]). Int -> Any -> Which xs
Which Int
0 (forall a b. a -> b
unsafeCoerce (forall (c :: [*] -> *) (xs :: [*]).
Case c xs =>
c xs -> Head xs -> CaseResult c (Head xs)
case' c (a : as)
c a
a'))
Left Which as
v' -> forall x (xs :: [*]). Which xs -> Which (x : xs)
diversify0 (forall (f :: [*] -> *) (c :: [*] -> *) (xs :: [*]).
AFunctor f c xs =>
c xs -> f xs -> f (CaseResults c xs)
afmap (forall (c :: [*] -> *) (xs :: [*]).
Reiterate c xs =>
c xs -> c (Tail xs)
reiterate c (a : as)
c) Which as
v')
{-# INLINABLE afmap #-}
instance ATraversable Which c m '[] where
atraverse :: forall (xs' :: [*]).
(Applicative m, IsTraversalCase c,
xs' ~ TraverseResults c m '[]) =>
c m '[] -> Which '[] -> m (Which xs')
atraverse c m '[]
_ = forall a. Which '[] -> a
impossible
instance ( Reiterate (c m) (a ': as)
, ATraversable Which c m as
, Case (c m) (a ': as)
) =>
ATraversable Which c m (a ': as) where
atraverse :: forall (xs' :: [*]).
(Applicative m, IsTraversalCase c,
xs' ~ TraverseResults c m (a : as)) =>
c m (a : as) -> Which (a : as) -> m (Which xs')
atraverse c m (a : as)
c Which (a : as)
v = case forall x (xs :: [*]). Which (x : xs) -> Either (Which xs) x
trial0 Which (a : as)
v of
Right a
a' -> forall (xs :: [*]). Int -> Any -> Which xs
Which Int
0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. a -> b
unsafeCoerce (forall (c :: [*] -> *) (xs :: [*]).
Case c xs =>
c xs -> Head xs -> CaseResult c (Head xs)
case' c m (a : as)
c a
a')
Left Which as
v' -> forall a b. a -> b
unsafeCoerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x (xs :: [*]). Which xs -> Which (x : xs)
diversify0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: [*] -> *) (c :: (* -> *) -> [*] -> *) (m :: * -> *)
(xs :: [*]) (xs' :: [*]).
(ATraversable f c m xs, Applicative m, IsTraversalCase c,
xs' ~ TraverseResults c m xs) =>
c m xs -> f xs -> m (f xs')
atraverse (forall (c :: [*] -> *) (xs :: [*]).
Reiterate c xs =>
c xs -> c (Tail xs)
reiterate c m (a : as)
c) Which as
v'
{-# INLINABLE atraverse #-}