{-# 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 = ($)

-- | 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 { 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 v r = getConst2 $ biMetamorph @_ @_ @r @v @(AppliesTo x) @Either @SwitchData @(Const2 x) @(Const2 x)
  Proxy doNil doUncons doCons $ SwitchData r v
  where
    doNil (SwitchData _ v) = impossible v
    doUncons :: forall ℓ f τ ϕ ρ. (KnownSymbol ℓ, AppliesTo x f τ, HasType ℓ f ϕ, HasType ℓ τ ρ)
             => Label ℓ -> SwitchData ϕ ρ -> Either (SwitchData (ϕ .- ℓ) (ρ .- ℓ)) (Const2 x f τ)
    doUncons l (SwitchData r v) = bimap (SwitchData $ lazyRemove l r) (Const2 . applyTo (r .! l)) $ trial v l
    -- doCons :: forall ℓ f τ ϕ ρ. (KnownSymbol ℓ, AppliesTo x f τ)
    --        => Label ℓ -> Either (Const2 x f τ) (Const2 x ϕ ρ) -> Const2 x (Extend ℓ f ϕ) (Extend ℓ τ ρ)
    doCons _ (Left  (Const2 x)) = Const2 x
    doCons _ (Right (Const2 x)) = Const2 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 = flip switch