{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
-----------------------------------------------------------------------------
-- |
-- Module: Data.Row.Switch
--
-- This module provides the ability to discharge a polymorphic variant using
-- a record that has matching fields.
--
-----------------------------------------------------------------------------


module Data.Row.Switch
  ( AppliesTo(..)
  , switch
  , caseon
  )
where

import Data.Proxy

import Data.Bifunctor (Bifunctor(..))
import Data.Row.Internal
import Data.Row.Records
import Data.Row.Variants

-- | A simple class that we use to provide a constraint for function application.
class AppliesTo r f x | r x -> f, f r -> x where
  applyTo :: f -> x -> r
instance AppliesTo r (x -> r) x where
  applyTo :: (x -> r) -> x -> r
applyTo = (x -> r) -> x -> r
forall a b. (a -> b) -> a -> b
($)

-- | A pair of a record and a variant.
data SwitchData r v = SwitchData (Rec r) (Var v)

-- | Like 'Const' but for two ignored type arguments.
newtype Const2 x y z = Const2 { Const2 x y z -> x
getConst2 :: x }

-- | A 'Var' and a 'Rec' can combine if their rows line up properly.
-- Given a Variant along with a Record of functions from each possible value
-- of the variant to a single output type, apply the correct
-- function to the value in the variant.
switch :: forall v r x. BiForall r v (AppliesTo x) => Var v -> Rec r -> x
switch :: Var v -> Rec r -> x
switch Var v
v Rec r
r = Const2 x r v -> x
forall x k (y :: k) k (z :: k). Const2 x y z -> x
getConst2 (Const2 x r v -> x) -> Const2 x r v -> x
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy (Const2 x), Proxy Either)
-> (SwitchData Empty Empty -> Const2 x Empty Empty)
-> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: Row *) (ρ2 :: Row *).
    (KnownSymbol ℓ, AppliesTo x τ1 τ2, HasType ℓ τ1 ρ1,
     HasType ℓ τ2 ρ2) =>
    Label ℓ
    -> SwitchData ρ1 ρ2
    -> Either (SwitchData (ρ1 .- ℓ) (ρ2 .- ℓ)) (Const2 x τ1 τ2))
-> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: Row *) (ρ2 :: Row *).
    (KnownSymbol ℓ, AppliesTo x τ1 τ2, FrontExtends ℓ τ1 ρ1,
     FrontExtends ℓ τ2 ρ2, AllUniqueLabels (Extend ℓ τ1 ρ1),
     AllUniqueLabels (Extend ℓ τ2 ρ2)) =>
    Label ℓ
    -> Either (Const2 x ρ1 ρ2) (Const2 x τ1 τ2)
    -> Const2 x (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
-> SwitchData r v
-> Const2 x r v
forall k1 k2 (r1 :: Row k1) (r2 :: Row k2)
       (c :: k1 -> k2 -> Constraint) (p :: * -> * -> *)
       (f :: Row k1 -> Row k2 -> *) (g :: Row k1 -> Row k2 -> *)
       (h :: k1 -> k2 -> *).
(BiForall r1 r2 c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty Empty -> g Empty Empty)
-> (forall (ℓ :: Symbol) (τ1 :: k1) (τ2 :: k2) (ρ1 :: Row k1)
           (ρ2 :: Row k2).
    (KnownSymbol ℓ, c τ1 τ2, HasType ℓ τ1 ρ1, HasType ℓ τ2 ρ2) =>
    Label ℓ -> f ρ1 ρ2 -> p (f (ρ1 .- ℓ) (ρ2 .- ℓ)) (h τ1 τ2))
-> (forall (ℓ :: Symbol) (τ1 :: k1) (τ2 :: k2) (ρ1 :: Row k1)
           (ρ2 :: Row k2).
    (KnownSymbol ℓ, c τ1 τ2, FrontExtends ℓ τ1 ρ1,
     FrontExtends ℓ τ2 ρ2, AllUniqueLabels (Extend ℓ τ1 ρ1),
     AllUniqueLabels (Extend ℓ τ2 ρ2)) =>
    Label ℓ
    -> p (g ρ1 ρ2) (h τ1 τ2) -> g (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
-> f r1 r2
-> g r1 r2
biMetamorph @_ @_ @r @v @(AppliesTo x) @Either @SwitchData @(Const2 x) @(Const2 x)
  Proxy (Proxy (Const2 x), Proxy Either)
forall k (t :: k). Proxy t
Proxy SwitchData Empty Empty -> Const2 x Empty Empty
forall (r :: Row *) a. SwitchData r Empty -> a
doNil forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: Row *) (ρ2 :: Row *).
(KnownSymbol ℓ, AppliesTo x τ1 τ2, HasType ℓ τ1 ρ1,
 HasType ℓ τ2 ρ2) =>
Label ℓ
-> SwitchData ρ1 ρ2
-> Either (SwitchData (ρ1 .- ℓ) (ρ2 .- ℓ)) (Const2 x τ1 τ2)
doUncons forall k k k k k k p x (y :: k) (z :: k) (y :: k) (z :: k) (y :: k)
       (z :: k).
p -> Either (Const2 x y z) (Const2 x y z) -> Const2 x y z
forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: Row *) (ρ2 :: Row *).
(KnownSymbol ℓ, AppliesTo x τ1 τ2, FrontExtends ℓ τ1 ρ1,
 FrontExtends ℓ τ2 ρ2, AllUniqueLabels (Extend ℓ τ1 ρ1),
 AllUniqueLabels (Extend ℓ τ2 ρ2)) =>
Label ℓ
-> Either (Const2 x ρ1 ρ2) (Const2 x τ1 τ2)
-> Const2 x (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
doCons (SwitchData r v -> Const2 x r v) -> SwitchData r v -> Const2 x r v
forall a b. (a -> b) -> a -> b
$ Rec r -> Var v -> SwitchData r v
forall (r :: Row *) (v :: Row *). Rec r -> Var v -> SwitchData r v
SwitchData Rec r
r Var v
v
  where
    doNil :: SwitchData r Empty -> a
doNil (SwitchData Rec r
_ Var Empty
v) = Var Empty -> a
forall a. Var Empty -> a
impossible Var Empty
v
    doUncons :: forall ℓ f τ ϕ ρ. (KnownSymbol ℓ, AppliesTo x f τ, HasType ℓ f ϕ, HasType ℓ τ ρ)
             => Label ℓ -> SwitchData ϕ ρ -> Either (SwitchData (ϕ .- ℓ) (ρ .- ℓ)) (Const2 x f τ)
    doUncons :: Label ℓ
-> SwitchData ϕ ρ
-> Either (SwitchData (ϕ .- ℓ) (ρ .- ℓ)) (Const2 x f τ)
doUncons Label ℓ
l (SwitchData Rec ϕ
r Var ρ
v) = (Var (ρ .- ℓ) -> SwitchData (ϕ .- ℓ) (ρ .- ℓ))
-> (τ -> Const2 x f τ)
-> Either (Var (ρ .- ℓ)) τ
-> Either (SwitchData (ϕ .- ℓ) (ρ .- ℓ)) (Const2 x f τ)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Rec (ϕ .- ℓ) -> Var (ρ .- ℓ) -> SwitchData (ϕ .- ℓ) (ρ .- ℓ)
forall (r :: Row *) (v :: Row *). Rec r -> Var v -> SwitchData r v
SwitchData (Rec (ϕ .- ℓ) -> Var (ρ .- ℓ) -> SwitchData (ϕ .- ℓ) (ρ .- ℓ))
-> Rec (ϕ .- ℓ) -> Var (ρ .- ℓ) -> SwitchData (ϕ .- ℓ) (ρ .- ℓ)
forall a b. (a -> b) -> a -> b
$ Label ℓ -> Rec ϕ -> Rec (ϕ .- ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Rec r -> Rec (r .- l)
lazyRemove Label ℓ
l Rec ϕ
r) (x -> Const2 x f τ
forall k k x (y :: k) (z :: k). x -> Const2 x y z
Const2 (x -> Const2 x f τ) -> (τ -> x) -> τ -> Const2 x f τ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> τ -> x
forall r f x. AppliesTo r f x => f -> x -> r
applyTo (Rec ϕ
r Rec ϕ -> Label ℓ -> ϕ .! ℓ
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Rec r -> Label l -> r .! l
.! Label ℓ
l)) (Either (Var (ρ .- ℓ)) τ
 -> Either (SwitchData (ϕ .- ℓ) (ρ .- ℓ)) (Const2 x f τ))
-> Either (Var (ρ .- ℓ)) τ
-> Either (SwitchData (ϕ .- ℓ) (ρ .- ℓ)) (Const2 x f τ)
forall a b. (a -> b) -> a -> b
$ Var ρ -> Label ℓ -> Either (Var (ρ .- ℓ)) (ρ .! ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Var ρ
v Label ℓ
l
    -- doCons :: forall ℓ f τ ϕ ρ. (KnownSymbol ℓ, AppliesTo x f τ)
    --        => Label ℓ -> Either (Const2 x f τ) (Const2 x ϕ ρ) -> Const2 x (Extend ℓ f ϕ) (Extend ℓ τ ρ)
    doCons :: p -> Either (Const2 x y z) (Const2 x y z) -> Const2 x y z
doCons p
_ (Left  (Const2 x
x)) = x -> Const2 x y z
forall k k x (y :: k) (z :: k). x -> Const2 x y z
Const2 x
x
    doCons p
_ (Right (Const2 x
x)) = x -> Const2 x y z
forall k k x (y :: k) (z :: k). x -> Const2 x y z
Const2 x
x

-- | The same as 'switch' but with the argument order reversed
caseon :: forall v r x. BiForall r v (AppliesTo x) => Rec r -> Var v -> x
caseon :: Rec r -> Var v -> x
caseon = (Var v -> Rec r -> x) -> Rec r -> Var v -> x
forall a b c. (a -> b -> c) -> b -> a -> c
flip Var v -> Rec r -> x
forall (v :: Row *) (r :: Row *) x.
BiForall r v (AppliesTo x) =>
Var v -> Rec r -> x
switch