module Data.Extensible.Inclusion (
Position
, runPosition
, (∈)()
, Member(..)
, Expecting
, Missing
, Ambiguous
, ord
, (⊆)()
, Include
, inclusion
, shrink
, subset
, spread
, coinclusion
, wrench
, retrench
, Nullable(..)
, nullable
, mapNullable
) where
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 => Position ys :* xs
inclusion = generateFor (Proxy :: Proxy (Member ys)) (const membership)
shrink :: (xs ⊆ ys) => h :* ys -> h :* xs
shrink h = hmap (\pos -> hlookup pos h) inclusion
subset :: (xs ⊆ ys, Functor f) => (h :* xs -> f (h :* xs)) -> h :* ys -> f (h :* ys)
subset f ys = fmap (write ys) $ f (shrink ys) where
write y xs = flip appEndo y
$ hfoldMap getConst'
$ hzipWith (\dst src -> Const' $ Endo $ sectorAt dst `over` const src) inclusion xs
spread :: (xs ⊆ ys) => h :| xs -> h :| ys
spread (UnionAt pos h) = UnionAt (hlookup pos inclusion) h
coinclusion :: (Include ys xs, Generate ys) => Nullable (Position xs) :* ys
coinclusion = flip appEndo (generate (const Null))
$ hfoldMap getConst'
$ htabulate (\src dst -> Const' $ Endo $ sectorAt 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 (UnionAt pos h) = flip UnionAt h `mapNullable` hlookup pos coinclusion