module Data.Extensible.Inclusion (
(⊆)()
, Include
, inclusion
, shrink
, spread
, IncludeAssoc
, Associated
, inclusionAssoc
, shrinkAssoc
, spreadAssoc
, coinclusion
, wrench
, retrench
, Nullable(..)
, nullable
, mapNullable
) where
import Data.Extensible.Class
import Data.Extensible.Product
import Data.Extensible.Sum
import Data.Extensible.Internal
import Data.Extensible.Internal.Rig
import Data.Monoid
type xs ⊆ ys = Include ys xs
type Include ys = Forall (Member ys)
inclusion :: forall xs ys. Include ys xs => Membership ys :* xs
inclusion = htabulateFor (Proxy :: Proxy (Member ys)) (const membership)
shrink :: (xs ⊆ ys) => h :* ys -> h :* xs
shrink h = hmap (hindex h) inclusion
spread :: (xs ⊆ ys) => h :| xs -> h :| ys
spread (EmbedAt i h) = views (pieceAt i) EmbedAt inclusion h
coinclusion :: (Include ys xs, Generate ys) => Nullable (Membership xs) :* ys
coinclusion = flip appEndo (htabulate (const Null))
$ hfoldMap getConst'
$ hmapWithIndex (\src dst -> Const' $ Endo $ pieceAt dst `over` const (Eine src))
$ inclusion
wrench :: (Generate ys, xs ⊆ ys) => h :* xs -> Nullable h :* ys
wrench xs = mapNullable (flip hlookup xs) `hmap` coinclusion
retrench :: (Generate ys, xs ⊆ ys) => h :| ys -> Nullable ((:|) h) xs
retrench (EmbedAt i h) = views (pieceAt i) (mapNullable (`EmbedAt`h)) coinclusion
class Associated xs t where
getAssociation :: Membership xs t
instance Associate k v xs => Associated xs (k ':> v) where
getAssociation = association
type IncludeAssoc ys = Forall (Associated ys)
inclusionAssoc :: forall xs ys. IncludeAssoc ys xs => Membership ys :* xs
inclusionAssoc = htabulateFor (Proxy :: Proxy (Associated ys)) (const getAssociation)
shrinkAssoc :: (IncludeAssoc ys xs) => h :* ys -> h :* xs
shrinkAssoc h = hmap (hindex h) inclusionAssoc
spreadAssoc :: (IncludeAssoc ys xs) => h :| xs -> h :| ys
spreadAssoc (EmbedAt i h) = views (pieceAt i) EmbedAt inclusionAssoc h