{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Composite.Fcf
  ( FromCompositeS,
    FromComposite,
    ToCompositeS,
    ToComposite,
    Union,
    Difference,
    Intersection,
    difference,
    union,
    intersection,
  )
where

import Composite.Record
import Data.Kind
import Data.Vinyl
import Data.Vinyl.Lens
import Data.Vinyl.TypeLevel as V
import Fcf
import qualified Fcf.Data.MapC
import GHC.TypeLits

-- | Turn a single `s :-> a` into an `'(s, a)`
--
-- @since 0.1.0.0
data FromCompositeS :: Type -> Exp (Symbol, Type)

type instance Eval (FromCompositeS (s :-> x)) = '(s, x)

-- | Turn a list of `(s -> a)` into a `MapC s a`
--
-- @since 0.1.0.0
data FromComposite :: [Type] -> Exp (Fcf.Data.MapC.MapC Symbol Type)

type instance Eval (FromComposite x) = Eval (Fcf.Data.MapC.FromList =<< Fcf.Map FromCompositeS x)

-- | Turn a single `(s, a)` into a `s :-> a`
--
-- @since 0.1.0.0
data ToCompositeS :: (Symbol, Type) -> Exp Type

type instance Eval (ToCompositeS '(s, x)) = s :-> x

-- | Turn a `MapC s a` into a list of `(s :-> a)`
--
-- @since 0.1.0.0
data ToComposite :: Fcf.Data.MapC.MapC Symbol Type -> Exp [Type]

type instance Eval (ToComposite x) = Eval (Fcf.Map ToCompositeS =<< Fcf.Data.MapC.ToList x)

-- | Difference
--
-- @since 0.1.0.0
data Difference :: [Type] -> [Type] -> Exp [Type]

type instance Eval (Difference xs ys) = Eval (ToComposite =<< Fcf.Data.MapC.Difference (Eval (FromComposite xs)) (Eval (FromComposite ys)))

-- | Difference
--
-- @since 0.1.0.0
data Union :: [Type] -> [Type] -> Exp [Type]

type instance Eval (Union xs ys) = Eval (ToComposite =<< Fcf.Data.MapC.Union (Eval (FromComposite xs)) (Eval (FromComposite ys)))

-- | Intersection
--
-- @since 0.1.0.0
data Intersection :: [Type] -> [Type] -> Exp [Type]

type instance Eval (Intersection xs ys) = Eval (ToComposite =<< Fcf.Data.MapC.Intersection (Eval (FromComposite xs)) (Eval (FromComposite ys)))

-- | Take the difference of two records by casting to the result of `Difference`.
--
-- @since 0.1.1.0
difference ::
  forall f xs ys zs.
  ( zs ~ Eval (Difference xs ys),
    zs ⊆ (xs V.++ ys)
  ) =>
  Rec f xs ->
  Rec f ys ->
  Rec f zs
difference :: Rec f xs -> Rec f ys -> Rec f zs
difference Rec f xs
x Rec f ys
y = Rec f (xs ++ ys) -> Rec f zs
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @zs (Rec f xs
x Rec f xs -> Rec f ys -> Rec f (xs ++ ys)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec f ys
y)

-- | Take the union of two records by casting to the result of `Union`.
--
-- @since 0.1.1.0
union ::
  forall f xs ys zs.
  ( zs ~ Eval (Union xs ys),
    zs ⊆ (xs V.++ ys)
  ) =>
  Rec f xs ->
  Rec f ys ->
  Rec f zs
union :: Rec f xs -> Rec f ys -> Rec f zs
union Rec f xs
x Rec f ys
y = Rec f (xs ++ ys) -> Rec f zs
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @zs (Rec f xs
x Rec f xs -> Rec f ys -> Rec f (xs ++ ys)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec f ys
y)

-- | Take the intersection of two records by casting to the result of `Intersection`.
--
-- @since 0.1.1.0
intersection ::
  forall f xs ys zs.
  ( zs ~ Eval (Intersection xs ys),
    zs ⊆ (xs V.++ ys)
  ) =>
  Rec f xs ->
  Rec f ys ->
  Rec f zs
intersection :: Rec f xs -> Rec f ys -> Rec f zs
intersection Rec f xs
x Rec f ys
y = Rec f (xs ++ ys) -> Rec f zs
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @zs (Rec f xs
x Rec f xs -> Rec f ys -> Rec f (xs ++ ys)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec f ys
y)