{-# 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' type
      Which(..) -- exporting constructor unsafely!

      -- * Single type
      -- ** Construction
    , impossible
    , impossible'
    -- , totally
    , pick
    , pick0
    , pickOnly
    , pickL
    , pickTag
    , pickN
      -- ** Destruction
    , obvious
    , trial
    , trial'
    , trial0
    , trial0'
    , trialL
    , trialL'
    , trialTag
    , trialTag'
    , trialN
    , trialN'
    , pattern W

      -- * Multiple types
      -- ** Injection
    , Diversify
    , diversify
    , diversify'
    , diversify0
    , DiversifyL
    , diversifyL
    , DiversifyN
    , diversifyN
      -- ** Inverse Injection
    , Reinterpret
    -- , Reinterpreted
    , reinterpret
    , Reinterpret'
    , reinterpret'
    , ReinterpretL
    -- , ReinterpretedL
    , reinterpretL
    , ReinterpretL'
    , reinterpretL'
    , ReinterpretN'
    , reinterpretN'

      -- * Catamorphism
    , 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

-- | A 'Which' is an anonymous sum type (also known as a polymorphic variant, or co-record)
-- which can only contain one of the types in the typelist.
-- This is essentially a typed version of 'Data.Dynamic'.
--
-- The following functions are available can be used to manipulate unique types in the typelist
--
-- * constructor: 'pick'
-- * destructor: 'trial'
-- * injection: 'diversify' and 'reinterpret'
-- * catamorphism: 'which' or 'switch'
--
-- These functions are type specified. This means labels are not required because the types themselves can be used to access the 'Which'.
-- It is a compile error to use those functions for duplicate fields.
--
-- For duplicate types in the list of possible types, Nat-indexed version of the functions are available:
--
-- * constructor: 'pickN'
-- * destructor: 'trialN'
-- * inejction: 'diversifyN' and 'reinterpretN'
-- * catamorphism: 'whichN' or 'switchN'
--
-- Encoding: The variant contains a value whose type is at the given position in the type list.
-- This is the same encoding as <https://github.com/haskus/haskus-utils/blob/master/src/lib/Haskus/Utils/Variant.hs Haskus.Util.Variant> and <https://hackage.haskell.org/package/HList-0.4.1.0/docs/src/Data-HList-Variant.html Data.Hlist.Variant>.
--
-- The constructor is only exported in the "Data.Diverse.Which.Internal" module
data Which (xs :: [Type]) = Which {-# UNPACK #-} !Int Any

-- Just like Haskus and HList versions, inferred type is phantom which is wrong
-- representational means:
-- @
-- Coercible '[Int] '[IntLike] => Coercible (Which '[Int]) (Which '[IntLike])
-- @
type role Which representational

----------------------------------------------

-- | A terminating 'G.Generic' instance for no types encoded as a 'Which '[]'.
-- The 'G.C1' and 'G.S1' metadata are not encoded.
instance G.Generic (Which '[]) where
    type Rep (Which '[]) = G.V1
    from :: forall x. Which '[] -> Rep (Which '[]) x
from Which '[]
_ = {- G.V1 -} 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 '[]"

-- | A terminating 'G.Generic' instance for one type encoded with 'pick''.
-- The 'G.C1' and 'G.S1' metadata are not encoded.
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 = {- G.Rec0 -} 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.Rec0 -} G.K1 x
a) = forall x. x -> Which '[x]
pickOnly x
a

-- | A 'G.Generic' instance encoded as either the 'x' value ('G.:+:') or the 'diversify0'ed remaining 'Which xs'.
-- The 'G.C1' and 'G.S1' metadata are not encoded.
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 ({- G.Rec0 -} 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 ({- G.Rec0 -} 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 {- G.Rec0 -} Rep (Which (x : x' : xs)) x
x = case Rep (Which (x : x' : xs)) x
x of
        G.L1 ({- G.Rec0 -} G.K1 x
a) -> forall x (xs :: [*]). x -> Which (x : xs)
pick0 x
a
        G.R1 ({- G.Rec0 -} 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

-- | Analogous to 'Data.Void.absurd'. Renamed 'impossible' to avoid conflicts.
--
-- Since 'Which \'[]' values logically don't exist, this witnesses the
-- logical reasoning tool of \"ex falso quodlibet\",
-- ie "from falsehood, anything follows".
--
-- A 'Which \'[]' is a 'Which' with no alternatives, which may occur as a 'Left'-over from 'trial'ing a @Which '[x]@ with one type.
-- It is an uninhabited type, just like 'Data.Void.Void'
impossible :: Which '[] -> a
impossible :: forall a. Which '[] -> a
impossible Which '[]
a = case Which '[]
a of {}
-- Copied from http://hackage.haskell.org/package/base/docs/src/Data.Void.html

-- | A @Which '[Void]@ is equivalent to @Which '[]@
-- A @Which '[Void]@ might occur if you lift a 'Void' into a @Which@ with 'pick'.
-- This allows you to convert it back to 'Void' or @Which '[]@
impossible' :: Which '[Void] -> a
impossible' :: forall a. Which '[Void] -> a
impossible' Which '[Void]
a = case Which '[Void]
a of {}

-- -- | This function is useful to type restrict something that returns a polymorphic type
-- -- to return (Which '[]). Eg. use this that to prove at compile time that a
-- -- finished continuation monad has no more unhandled holes.
-- totally :: f (Which '[]) -> f (Which '[])
-- totally = id

-- | Lift a value into a 'Which' of possibly other types @xs@.
-- @xs@ can be inferred or specified with TypeApplications.
-- NB. forall is used to specify @xs@ first, so TypeApplications can be used to specify @xs@ first
--
-- @
-- 'pick' \'A' \@_ \@'[Int, Bool, Char, Maybe String] :: Which '[Int, Bool, Char, Maybe String]
-- @
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

-- | A variation of 'pick' where @x@ is specified via a label
--
-- @
-- let y = 'pickL' \@Foo (Tagged (5 :: Int)) :: Which '[Bool, Tagged Foo Int, Tagged Bar Char]
--     x = 'trialL' \@Foo y
-- x `shouldBe` (Right (Tagged 5))
-- @
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

-- | Variation of 'pick' specialized to 'Tagged' that automatically tags the value.
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)

-- | A variation of 'pick' into a 'Which' of a single type.
--
-- @
-- 'pickOnly' \'A' :: Which '[Char]
-- @
pickOnly :: x -> Which '[x]
pickOnly :: forall x. x -> Which '[x]
pickOnly = forall x (xs :: [*]). x -> Which (x : xs)
pick0

-- | A variation of 'pick' into a 'Which' where @x@ is the first type.
--
-- @
-- 'pick0' \'A' :: Which '[Char, Int, Bool]
-- @
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

-- | Lift a value into a 'Which' of possibly other (possibley indistinct) types, where the value is the @n@-th type.
--
-- @
-- 'pickN' \@4 (5 :: Int) :: Which '[Bool, Int, Char, Bool, Int, Char]
-- @
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

-- | It is 'obvious' what value is inside a 'Which' of one type.
--
-- @
-- let x = 'pick'' \'A' :: Which '[Char]
-- 'obvious' x \`shouldBe` \'A'
-- @
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' the n-th type of a 'Which', and get 'Either' the 'Right' value or the 'Left'-over possibilities.
--
-- @
-- let x = 'pick' \'A' \@_ \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String]
-- 'trialN' \@1 x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Int, Char, Maybe String]
-- @
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' a type in a 'Which' and 'Either' get the 'Right' value or the 'Left'-over possibilities.
--
-- @
-- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String]
-- 'trial' \@Char x \`shouldBe` Right \'A'
-- 'trial' \@Int x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Bool, Char, Maybe String]
-- @
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_

-- | A variation of 'trial' where x is specified via a label
--
-- @
-- let y = 'pickL' \@Foo (Tagged (5 :: Int)) :: Which '[Bool, Tagged Foo Int, Tagged Bar Char]
--     x = 'trialL' \@Foo Proxy y
-- x `shouldBe` (Right (Tagged 5))
-- @
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

-- | Variation of 'trialL' specialized to 'Tagged' which untags the field.
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

-- | Variation of 'trialN' which returns a Maybe
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

-- | Variation of 'trial' which returns a Maybe
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_'

-- | Variation of 'trialL' which returns a Maybe
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

-- | Variation of 'trialL'' specialized to 'Tagged' which untags the field.
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

-- | A variation of a 'Which' 'trial' which 'trial's the first type in the type list.
--
-- @
-- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String]
-- 'trial0' x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Bool, Char, Maybe String]
-- @
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)

-- | Variation of 'trial0' which returns a Maybe
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 synonym that makes pattern matching on Which possible.
--   For example, this will return @Just 5@:
--
-- @
-- let y = pick (5 :: Int) :: Which '[Bool, String, Int]
-- in  case y of
--       W (i :: Int) -> Just i
--       _ -> Nothing
-- @
--
-- Keep in mind, GHC is not smart enough and will always throw a warning about
-- incomplete pattern matches without a catch-all clause.
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
-----------------------------------------------------------------

-- | A friendlier constraint synonym for 'diversify'.
type Diversify (branch :: [Type]) (tree :: [Type]) = Switch (CaseDiversify branch tree) (Which tree) branch

-- | Convert a 'Which' to another 'Which' that may include other possibilities.
-- That is, @branch@ is equal or is a subset of @tree@.
--
-- This can also be used to rearrange the order of the types in the 'Which'.
--
-- It is a compile error if @tree@ has duplicate types with @branch@.
--
-- NB. Use TypeApplications with @_ to specify @tree@.
--
-- @
-- let a = 'pick'' (5 :: Int) :: 'Which' '[Int]
--     b = 'diversify' \@_ \@[Int, Bool] a :: 'Which' '[Int, Bool]
--     c = 'diversify' \@_ \@[Bool, Int] b :: 'Which' '[Bool, Int]
-- @
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

-- | The @Unique x branch@ is important to get a compile error if the from @branch@ doesn't have a unique x
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

-- | A simple version of 'diversify' which add another type to the front of the typelist.
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

-- | A restricted version of 'diversify' which only rearranges the types
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

------------------------------------------------------------------

-- | A friendlier constraint synonym for 'diversifyL'.
type DiversifyL (ls :: [k]) (branch :: [Type]) (tree :: [Type]) =
    ( Diversify branch tree
    , branch ~ KindsAtLabels ls tree
    , UniqueLabels ls tree
    , IsDistinct ls
    )

-- | A variation of 'diversify' where @branch@is additionally specified by a labels list.
--
-- @
-- let y = 'pickOnly' (5 :: Tagged Bar Int)
--     y' = 'diversifyL' \@'[Bar] y :: 'Which' '[Tagged Bar Int, Tagged Foo Bool]
--     y'' = 'diversifyL' \@'[Bar, Foo] y' :: 'Which' '[Tagged Foo Bool, Tagged Bar Int]
-- 'switch' y'' ('Data.Diverse.CaseFunc.CaseFunc' \@'Data.Typeable.Typeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` \"Tagged * Bar Int"
-- @
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)

------------------------------------------------------------------

-- | A friendlier constraint synonym for 'diversifyN'.
type DiversifyN (ns :: [Nat]) (branch :: [Type]) (tree :: [Type]) =
    ( SwitchN Which (CaseDiversifyN ns) (Which tree) 0 branch
    , KindsAtIndices ns tree ~ branch
    )

-- | A variation of 'diversify' which uses a Nat list @indices@ to specify how to reorder the fields, where
--
-- @
-- indices[branch_idx] = tree_idx
-- @
--
-- This variation allows @tree@ to contain duplicate types with @branch@ since
-- the mapping is specified by @indicies@.
--
-- @
-- let y = 'pickOnly' (5 :: Int)
--     y' = 'diversifyN' \@'[0] \@_ \@[Int, Bool] y
--     y'' = 'diversifyN' \@[1,0] \@_ \@[Bool, Int] y'
-- 'switch' y'' ('Data.Diverse.CaseFunc.CaseFunc' \@'Data.Typeable.Typeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` \"Int"
-- @
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

------------------------------------------------------------------

-- | A friendlier constraint synonym for 'reinterpret'.
type Reinterpret (branch :: [Type]) (tree :: [Type]) = Switch (CaseReinterpret branch tree) (Either (Which (Complement tree branch)) (Which branch)) tree

-- -- | A variation of 'Reinterpret' that exposes @branchlessTree ~ Complement tree branch@
-- type Reinterpreted branch tree branchlessTree = (Reinterpret branch tree, branchlessTree ~ Complement tree branch)

-- | Convert a 'Which' into possibly another 'Which' with a totally different typelist.
-- Returns either a 'Which' with the 'Right' value, or a 'Which' with the 'Left'over @compliment@ types.
--
-- It is a compile error if @branch@ or @compliment@ has duplicate types with @tree@.
--
-- NB. forall used to specify @branch@ first, so TypeApplications can be used to specify @branch@ first.
--
-- @
--     let a = 'pick' \@[Int, Char, Bool] (5 :: Int) :: 'Which' '[Int, Char, Bool]
--     let  b = 'reinterpret' @[String, Char] y
--     b \`shouldBe` Left ('pick' (5 :: Int)) :: 'Which' '[Int, Bool]
--     let c = 'reinterpret' @[String, Int] a
--     c \`shouldBe` Right ('pick' (5 :: Int)) :: 'Which' '[String, Int]
-- @
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 -- Compile error to ensure reinterpret only works with unique fields
         ) =>
         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)
                 -- safe use of partial! j will never be zero due to check above
                 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)

------------------------------------------------------------------

-- | A friendlier constraint synonym for 'reinterpret''.
type Reinterpret' (branch :: [Type]) (tree :: [Type]) = Switch (CaseReinterpret' branch tree) (Maybe (Which branch)) tree

-- | Variation of 'reinterpret' which returns a Maybe.
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 -- Compile error to ensure reinterpret only works with unique fields
         ) =>
         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)

------------------------------------------------------------------

-- | A friendlier constraint synonym for 'reinterpretL'.
type ReinterpretL (ls :: [k]) (branch :: [Type]) (tree :: [Type]) =
    ( Reinterpret branch tree
    , branch ~ KindsAtLabels ls tree
    , UniqueLabels ls tree
    , IsDistinct ls
    )

-- -- | A variation of 'ReinterpretL' that exposes @branchlessTree ~ Complement tree branch@
-- type ReinterpretedL ls branch tree branchlessTree = (ReinterpretL ls branch tree, branchlessTree ~ Complement tree branch)

-- | A variation of 'reinterpret' where the @branch@ is additionally specified with a labels list.
--
-- @
-- let y = 'pick' \@[Tagged Bar Int, Tagged Foo Bool, Tagged Hi Char, Tagged Bye Bool] (5 :: Tagged Bar Int)
--     y' = 'reinterpretL' \@[Foo, Bar] y
--     x = 'pick' \@[Tagged Foo Bool, Tagged Bar Int] (5 :: Tagged Bar Int)
-- y' \`shouldBe` Right x
-- @
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)

-- | A friendlier constraint synonym for 'reinterpretL'.
type ReinterpretL' (ls :: [k]) (branch :: [Type]) (tree :: [Type]) =
    ( Reinterpret' branch tree
    , branch ~ KindsAtLabels ls tree
    , UniqueLabels ls tree
    , IsDistinct ls
    )

-- | Variation of 'reinterpretL' which returns a Maybe.
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)

------------------------------------------------------------------

-- | A friendlier constraint synonym for 'reinterpretN'.
type ReinterpretN' (ns :: [Nat]) (branch :: [Type]) (tree :: [Type]) =
    ( SwitchN Which (CaseReinterpretN' ns) (Maybe (Which branch)) 0 tree
    , KindsAtIndices ns tree ~ branch)

-- | A limited variation of 'reinterpret'' which uses a Nat list @n@ to specify how to reorder the fields, where
--
-- @
-- indices[branch_idx] = tree_idx
-- @
--
-- This variation allows @tree@ to contain duplicate types with @branch@
-- since the mapping is specified by @indicies@.
--
-- However, unlike 'reinterpert', in this variation,
-- @branch@ must be a subset of @tree@ instead of any arbitrary Which.
-- Also it returns a Maybe instead of Either.
--
-- This is so that the same @indices@ can be used in 'narrowN'.
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)

------------------------------------------------------------------

-- | 'Switcher' is an instance of 'Reduce' for which __'reiterate'__s through the possibilities in a 'Which',
-- delegating handling to 'Case', ensuring termination when 'Which' only contains one type.
newtype Switcher c r (xs :: [Type]) = Switcher (c r xs)

type instance Reduced (Switcher c r xs) = r

-- | 'trial0' each type in a 'Which', and either handle the 'case'' with value discovered, or __'reiterate'__
-- trying the next type in the type list.
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 -- This means all @r@ for all typelist must be the same @r@
         ) =>
         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'
    -- GHC 8.2.1 can optimize to single case statement. See https://ghc.haskell.org/trac/ghc/ticket/12877
    {-# INLINABLE reduce #-}
     -- This makes compiling tests a little faster than with no pragma

-- | Terminating case of the loop, ensuring that a instance of @Case '[]@
-- with an empty typelist is not required.
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

-- | Allow 'Which \'[]' to be 'reinterpret''ed or 'diversify'ed into anything else
-- This is safe because @Which '[]@ is uninhabited, and this is already something that
-- can be done with 'impossible'
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

-- | Allow 'Void' to be 'reinterpret''ed or 'diversify'ed into anything else
-- This is safe because @Void@ is uninhabited, and this is already something that
-- can be done with '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

-- | Allow 'Which \'[Void]' to be 'reinterpret''ed or 'diversify'ed into anything else
-- This is safe because @Which '[Void]@ is uninhabited, and this is already something that
-- can be done with 'impossible'
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'

------------------------------------------------------------------

-- | A friendlier constraint synonym for 'reinterpretN'.
type Switch c r xs = Reduce (Which xs) (Switcher c r xs)

-- | A switch/case statement for 'Which'. This is equivalent to @flip 'which'@
--
-- Use 'Case' instances like 'Data.Diverse.Cases.Cases' to apply a 'Which' of functions to a variant of values.
--
-- @
-- let y = 'Data.Diverse.Which.pick' (5 :: Int) :: 'Data.Diverse.Which.Which' '[Int, Bool]
-- 'Data.Diverse.Which.switch' y (
--     'Data.Diverse.Cases.cases' (show \@Bool
--         'Data.Diverse.Many../' show \@Int
--         'Data.Diverse.Many../' 'Data.Diverse.Many.nil')) \`shouldBe` "5"
-- @
--
-- Or 'Data.Diverse.CaseFunc.CaseFunc' \@'Data.Typeable.Typeable' to apply a polymorphic function that work on all 'Typeable's.
--
-- @
-- let y = 'Data.Diverse.Which.pick' (5 :: Int) :: 'Data.Diverse.Which.Which' '[Int, Bool]
-- 'Data.Diverse.Which.switch' y ('Data.Diverse.CaseFunc.CaseFunc' \@'Data.Typeable.Typeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` "Int"
-- @
--
-- Or you may use your own custom instance of 'Case'.
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

-- | Catamorphism for 'Which'. This is @flip 'switch'@.
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

------------------------------------------------------------------

-- | 'SwitcherN' is a variation of 'Switcher' which __'reiterateN'__s through the possibilities in a 'Which',
-- delegating work to 'CaseN', ensuring termination when 'Which' only contains one type.
newtype SwitcherN c r (n :: Nat) (xs :: [Type]) = SwitcherN (c r n xs)

type instance Reduced (SwitcherN c r n xs) = r

-- | 'trial0' each type in a 'Which', and either handle the 'case'' with value discovered, or __'reiterateN'__
-- trying the next type in the type list.
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 -- This means all @r@ for all typelist must be the same @r@
         ) =>
         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'
    -- Ghc 8.2.1 can optimize to single case statement. See https://ghc.haskell.org/trac/ghc/ticket/12877
    {-# INLINABLE reduce #-}
 -- This makes compiling tests a little faster than with no pragma

-- | Terminating case of the loop, ensuring that a instance of @Case '[]@
-- with an empty typelist is not required.
-- You can't reduce 'zilch'
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

-- | Catamorphism for 'Which'. This is equivalent to @flip 'switchN'@.
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

-- | A switch/case statement for 'Which'. This is equivalent to @flip 'whichN'@
--
-- Use 'Case' instances like 'Data.Diverse.Cases.CasesN' to apply a 'Which' of functions to a variant of values
-- in index order.
--
-- @
-- let y = 'pickN' \@0 (5 :: Int) :: 'Which' '[Int, Bool, Bool, Int]
-- 'switchN' y (
--     'Data.Diverse.Cases.casesN' (show \@Int
--         'Data.Diverse.Many../' show \@Bool
--         'Data.Diverse.Many../' show \@Bool
--         'Data.Diverse.Many../' show \@Int
--         'Data.Diverse.Many../' 'Data.Diverse.Many.nil')) \`shouldBe` "5"
-- @
--
-- Or you may use your own custom instance of 'Case'.
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

-----------------------------------------------------------------

-- | Two 'Which'es are only equal iff they both contain the equivalnet value at the same type index.
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)

-- | @('zilch' == 'zilch') == True@
instance Eq (Which '[]) where
    Which '[]
_ == :: Which '[] -> Which '[] -> Bool
== Which '[]
_ = Bool
True

-- | Do not export constructor
-- Stores the right Any to be compared when the correct type is discovered
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

-----------------------------------------------------------------

-- | A 'Which' with a type at smaller type index is considered smaller.
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)

-- | @('compare' 'zilch' 'zilch') == EQ@
instance Ord (Which '[]) where
    compare :: Which '[] -> Which '[] -> Ordering
compare Which '[]
_ Which '[]
_ = Ordering
EQ

-- | Do not export constructor
-- Stores the right Any to be compared when the correct type is discovered
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)

------------------------------------------------------------------

-- | @show ('pick'' \'A') == "pick \'A'"@
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

-- | coerce Which to another type without incrementing Int.
-- THis is because 'WhichRead' instance already increments the int
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

-- | Succeed reading if the Int index match
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 #-} -- This makes compiling tests a little faster than with no pragma

-- | This 'Read' instance tries to read using the each type in the typelist, using the first successful type read.
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)

------------------------------------------------------------------

-- class AFunctor f c xs where
--     afmap :: c xs -> f xs -> f (CaseResults c xs)

-- | Terminating AFunctor instance for empty type list
instance AFunctor Which c '[] where
    afmap :: c '[] -> Which '[] -> Which (CaseResults c '[])
afmap c '[]
_ = forall a. Which '[] -> a
impossible

-- | Recursive AFunctor instance for non empty type list
-- delegate afmap'ing the remainder to an instance of Collector' with one less type in the type list
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 #-}
    -- This makes compiling tests a little faster than with no pragma

------------------------------------------------------------------

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 #-}