{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
------------------------------------------------------------------------
-- |
-- Module      :  Data.Extensible.Inclusion
-- Copyright   :  (c) Fumiaki Kinoshita 2018
-- License     :  BSD3
--
-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--
------------------------------------------------------------------------
module Data.Extensible.Inclusion (
  -- * Inclusion
  type (⊆)
  , Include
  , inclusion
  , shrink
  , spread
  -- * Key-value
  , IncludeAssoc
  , Associated
  , Associated'
  , inclusionAssoc
  , shrinkAssoc
  , spreadAssoc
  ) where

import Data.Constraint
import Data.Extensible.Class
import Data.Extensible.Product
import Data.Extensible.Sum
import Data.Extensible.Internal.Rig
import Data.Proxy

-- | Unicode alias for 'Include'
type xs ⊆ ys = Include ys xs

-- | @ys@ contains @xs@
type Include ys = Forall (Member ys)

-- | Reify the inclusion of type level sets.
inclusion :: forall xs ys. Include ys xs => xs :& Membership ys
inclusion :: forall {k} (xs :: [k]) (ys :: [k]).
Include ys xs =>
xs :& Membership ys
inclusion = Proxy (Member ys)
-> (forall (x :: k). Member ys x => Membership ys x)
-> xs :& Membership ys
forall {k} (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> Type) (h :: k -> Type).
Forall c xs =>
proxy c -> (forall (x :: k). c x => h x) -> xs :& h
hrepeatFor (Proxy (Member ys)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Member ys)) Membership ys x
forall (x :: k). Member ys x => Membership ys x
forall {k} (xs :: [k]) (x :: k). Member xs x => Membership xs x
membership
{-# INLINABLE inclusion #-}

-- | /O(n)/ Select some elements.
shrink :: (xs ⊆ ys) => ys :& h -> xs :& h
shrink :: forall {k} (xs :: [k]) (ys :: [k]) (h :: k -> Type).
(xs ⊆ ys) =>
(ys :& h) -> xs :& h
shrink ys :& h
h = (forall (x :: k). Membership ys x -> h x)
-> (xs :& Membership ys) -> xs :& h
forall {k} (g :: k -> Type) (h :: k -> Type) (xs :: [k]).
(forall (x :: k). g x -> h x) -> (xs :& g) -> xs :& h
hmap ((ys :& h) -> Membership ys x -> h x
forall {k} (xs :: [k]) (h :: k -> Type) (x :: k).
(xs :& h) -> Membership xs x -> h x
hindex ys :& h
h) xs :& Membership ys
forall {k} (xs :: [k]) (ys :: [k]).
Include ys xs =>
xs :& Membership ys
inclusion
{-# INLINE shrink #-}

-- | /O(1)/ Embed to a larger union.
spread :: (xs ⊆ ys) => xs :/ h -> ys :/ h
spread :: forall {k} (xs :: [k]) (ys :: [k]) (h :: k -> Type).
(xs ⊆ ys) =>
(xs :/ h) -> ys :/ h
spread (EmbedAt Membership xs x
i h x
h) = Optic'
  (->)
  (Const (h x -> ys :/ h))
  (xs :& Membership ys)
  (Membership ys x)
-> (Membership ys x -> h x -> ys :/ h)
-> (xs :& Membership ys)
-> h x
-> ys :/ h
forall r s a. Optic' (->) (Const r) s a -> (a -> r) -> s -> r
views (Membership xs x
-> Optic'
     (->)
     (Const (h x -> ys :/ h))
     (xs :& Membership ys)
     (Membership ys x)
forall (xs :: [k]) (h :: k -> Type) (x :: k).
ExtensibleConstr (:&) xs h x =>
Membership xs x
-> Optic' (->) (Const (h x -> ys :/ h)) (xs :& h) (h x)
forall k (f :: Type -> Type) (p :: Type -> Type -> Type)
       (t :: [k] -> (k -> Type) -> Type) (xs :: [k]) (h :: k -> Type)
       (x :: k).
(Extensible f p t, ExtensibleConstr t xs h x) =>
Membership xs x -> Optic' p f (t xs h) (h x)
pieceAt Membership xs x
i) Membership ys x -> h x -> ys :/ h
forall {k} (xs :: [k]) (x :: k) (h :: k -> Type).
Membership xs x -> h x -> xs :/ h
EmbedAt xs :& Membership ys
forall {k} (xs :: [k]) (ys :: [k]).
Include ys xs =>
xs :& Membership ys
inclusion h x
h
{-# INLINE spread #-}

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

type family Associated' (xs :: [Assoc k v]) (t :: Assoc k v) :: Constraint where
  Associated' xs (k ':> v) = Lookup xs k v

-- | @'Associated' xs (k ':> v)@ is equivalent to @'Associate' k v xs@
class Associated' xs t => Associated xs t where
  getAssociation :: Membership xs t

instance (Associated' xs t, t ~ (k ':> v)) => Associated xs t where
  getAssociation :: Membership xs t
getAssociation = Membership xs t
Membership xs (k ':> v)
forall {k} {v} (xs :: [Assoc k v]) (k1 :: k) (v1 :: v).
Lookup xs k1 v1 =>
Membership xs (k1 ':> v1)
association

-- | Similar to 'Include', but this focuses on keys.
type IncludeAssoc ys = Forall (Associated ys)

-- | Reify the inclusion of type level sets.
inclusionAssoc :: forall xs ys. IncludeAssoc ys xs => xs :& Membership ys
inclusionAssoc :: forall {k} {v} (xs :: [Assoc k v]) (ys :: [Assoc k v]).
IncludeAssoc ys xs =>
xs :& Membership ys
inclusionAssoc = Proxy (Associated ys)
-> (forall (x :: Assoc k v). Associated ys x => Membership ys x)
-> xs :& Membership ys
forall {k} (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> Type) (h :: k -> Type).
Forall c xs =>
proxy c -> (forall (x :: k). c x => h x) -> xs :& h
hrepeatFor (Proxy (Associated ys)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Associated ys)) Membership ys x
forall {k} {v} (xs :: [Assoc k v]) (t :: Assoc k v).
Associated xs t =>
Membership xs t
forall (x :: Assoc k v). Associated ys x => Membership ys x
getAssociation
{-# INLINABLE inclusionAssoc #-}

-- | /O(n)/ Select some elements.
shrinkAssoc :: (IncludeAssoc ys xs) => ys :& h -> xs :& h
shrinkAssoc :: forall {k} {v} (ys :: [Assoc k v]) (xs :: [Assoc k v])
       (h :: Assoc k v -> Type).
IncludeAssoc ys xs =>
(ys :& h) -> xs :& h
shrinkAssoc ys :& h
h = (forall (x :: Assoc k v). Membership ys x -> h x)
-> (xs :& Membership ys) -> xs :& h
forall {k} (g :: k -> Type) (h :: k -> Type) (xs :: [k]).
(forall (x :: k). g x -> h x) -> (xs :& g) -> xs :& h
hmap ((ys :& h) -> Membership ys x -> h x
forall {k} (xs :: [k]) (h :: k -> Type) (x :: k).
(xs :& h) -> Membership xs x -> h x
hindex ys :& h
h) xs :& Membership ys
forall {k} {v} (xs :: [Assoc k v]) (ys :: [Assoc k v]).
IncludeAssoc ys xs =>
xs :& Membership ys
inclusionAssoc
{-# INLINE shrinkAssoc #-}

-- | /O(1)/ Embed to a larger union.
spreadAssoc :: (IncludeAssoc ys xs) => xs :/ h -> ys :/ h
spreadAssoc :: forall {k} {v} (ys :: [Assoc k v]) (xs :: [Assoc k v])
       (h :: Assoc k v -> Type).
IncludeAssoc ys xs =>
(xs :/ h) -> ys :/ h
spreadAssoc (EmbedAt Membership xs x
i h x
h) = Optic'
  (->)
  (Const (h x -> ys :/ h))
  (xs :& Membership ys)
  (Membership ys x)
-> (Membership ys x -> h x -> ys :/ h)
-> (xs :& Membership ys)
-> h x
-> ys :/ h
forall r s a. Optic' (->) (Const r) s a -> (a -> r) -> s -> r
views (Membership xs x
-> Optic'
     (->)
     (Const (h x -> ys :/ h))
     (xs :& Membership ys)
     (Membership ys x)
forall (xs :: [Assoc k v]) (h :: Assoc k v -> Type)
       (x :: Assoc k v).
ExtensibleConstr (:&) xs h x =>
Membership xs x
-> Optic' (->) (Const (h x -> ys :/ h)) (xs :& h) (h x)
forall k (f :: Type -> Type) (p :: Type -> Type -> Type)
       (t :: [k] -> (k -> Type) -> Type) (xs :: [k]) (h :: k -> Type)
       (x :: k).
(Extensible f p t, ExtensibleConstr t xs h x) =>
Membership xs x -> Optic' p f (t xs h) (h x)
pieceAt Membership xs x
i) Membership ys x -> h x -> ys :/ h
forall {k} (xs :: [k]) (x :: k) (h :: k -> Type).
Membership xs x -> h x -> xs :/ h
EmbedAt xs :& Membership ys
forall {k} {v} (xs :: [Assoc k v]) (ys :: [Assoc k v]).
IncludeAssoc ys xs =>
xs :& Membership ys
inclusionAssoc h x
h
{-# INLINE spreadAssoc #-}