{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Data.Diverse.Cases
( Cases
, cases
, cases'
, CasesN
, casesN
, casesN'
) where
import Data.Diverse.Case
import Data.Diverse.Many
import Data.Diverse.Reiterate
import Data.Diverse.TypeLevel
import Data.Kind
import GHC.TypeLits
newtype Cases (fs :: [Type]) r (xs :: [Type]) = Cases (Many fs)
type instance CaseResult (Cases fs r) x = r
instance Reiterate (Cases fs r) xs where
reiterate :: Cases fs r xs -> Cases fs r (Tail xs)
reiterate (Cases Many fs
s) = forall (fs :: [*]) r (xs :: [*]). Many fs -> Cases fs r xs
Cases Many fs
s
instance UniqueMember (Head xs -> r) fs => Case (Cases fs r) xs where
case' :: Cases fs r xs -> Head xs -> CaseResult (Cases fs r) (Head xs)
case' (Cases Many fs
s) = forall x (xs :: [*]). UniqueMember x xs => Many xs -> x
grab @(Head xs -> r) Many fs
s
cases
:: forall r xs fs.
(AllConstrained ((~) r) (CaseResults (Cases fs r) fs), SameLength fs (Nub xs))
=> Many fs -> Cases fs r xs
cases :: forall r (xs :: [*]) (fs :: [*]).
(AllConstrained ((~) r) (CaseResults (Cases fs r) fs),
SameLength fs (Nub xs)) =>
Many fs -> Cases fs r xs
cases = forall (fs :: [*]) r (xs :: [*]). Many fs -> Cases fs r xs
Cases
cases'
:: forall r xs fs.
(AllConstrained ((~) r) (CaseResults (Cases fs r) fs))
=> Many fs -> Cases fs r xs
cases' :: forall r (xs :: [*]) (fs :: [*]).
AllConstrained ((~) r) (CaseResults (Cases fs r) fs) =>
Many fs -> Cases fs r xs
cases' = forall (fs :: [*]) r (xs :: [*]). Many fs -> Cases fs r xs
Cases
newtype CasesN (fs :: [Type]) r (n :: Nat) (xs :: [Type]) = CasesN (Many fs)
type instance CaseResult (CasesN fs r n) x = r
instance ReiterateN (CasesN fs r) n xs where
reiterateN :: CasesN fs r n xs -> CasesN fs r (n + 1) (Tail xs)
reiterateN (CasesN Many fs
s) = forall (fs :: [*]) r (n :: Nat) (xs :: [*]).
Many fs -> CasesN fs r n xs
CasesN Many fs
s
instance (MemberAt n (Head xs -> r) fs) => Case (CasesN fs r n) xs where
case' :: CasesN fs r n xs -> Head xs -> CaseResult (CasesN fs r n) (Head xs)
case' (CasesN Many fs
s) = forall (n :: Nat) x (xs :: [*]). MemberAt n x xs => Many xs -> x
grabN @n Many fs
s
casesN
:: forall r xs fs.
(AllConstrained ((~) r) (CaseResults (CasesN fs r 0) fs), SameLength fs xs)
=> Many fs -> CasesN fs r 0 xs
casesN :: forall r (xs :: [*]) (fs :: [*]).
(AllConstrained ((~) r) (CaseResults (CasesN fs r 0) fs),
SameLength fs xs) =>
Many fs -> CasesN fs r 0 xs
casesN = forall (fs :: [*]) r (n :: Nat) (xs :: [*]).
Many fs -> CasesN fs r n xs
CasesN
casesN'
:: forall r xs fs.
(AllConstrained ((~) r) (CaseResults (CasesN fs r 0) fs))
=> Many fs -> CasesN fs r 0 xs
casesN' :: forall r (xs :: [*]) (fs :: [*]).
AllConstrained ((~) r) (CaseResults (CasesN fs r 0) fs) =>
Many fs -> CasesN fs r 0 xs
casesN' = forall (fs :: [*]) r (n :: Nat) (xs :: [*]).
Many fs -> CasesN fs r n xs
CasesN