{-# LANGUAGE DataKinds,
TypeOperators,
ConstraintKinds,
PolyKinds,
TypeFamilies,
GADTs,
MultiParamTypeClasses,
FunctionalDependencies,
FlexibleInstances,
FlexibleContexts,
UndecidableInstances,
UndecidableSuperClasses,
TypeApplications,
ScopedTypeVariables,
AllowAmbiguousTypes,
ExplicitForAll,
RankNTypes,
DefaultSignatures,
PartialTypeSignatures,
LambdaCase,
EmptyCase
#-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Data.RBR.Subset (
Subset,
fieldSubset,
projectSubset,
getFieldSubset,
setFieldSubset,
modifyFieldSubset,
branchSubset,
injectSubset,
matchSubset,
fromRecordSuperset,
eliminateSubset
) where
import Data.Proxy
import Data.Kind
import Data.Monoid (Endo(..))
import GHC.TypeLits
import Data.SOP (K(..),I(..))
import Data.RBR.Internal hiding
(
ProductlikeSubset,
fieldSubset,
projectSubset,
getFieldSubset,
setFieldSubset,
modifyFieldSubset,
SumlikeSubset,
branchSubset,
injectSubset,
matchSubset,
eliminateSubset
)
type Subset (subset :: Map Symbol q) (whole :: Map Symbol q) = KeysValuesAll (PresentIn whole) subset
fieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole)
=> Record f whole -> (Record f subset -> Record f whole, Record f subset)
fieldSubset r =
(,)
(let goset :: forall left k v right color. (PresentIn whole k v, KeysValuesAll (PresentIn whole) left,
KeysValuesAll (PresentIn whole) right)
=> Record (SetField f (Record f whole)) left
-> Record (SetField f (Record f whole)) right
-> Record (SetField f (Record f whole)) (N color left k v right)
goset left right = Node left (SetField (\v w -> fst (field @k @whole w) v)) right
setters :: Record (SetField f (Record f whole)) _ = cpara_Map (Proxy @(PresentIn whole)) unit goset
appz (SetField func) fv = K (Endo (func fv))
in \toset -> appEndo (collapse'_Record (liftA2_Record appz setters toset)) r)
(let goget :: forall left k v right color. (PresentIn whole k v, KeysValuesAll (PresentIn whole) left,
KeysValuesAll (PresentIn whole) right)
=> Record f left
-> Record f right
-> Record f (N color left k v right)
goget left right = Node left (project @k @whole r) right
in cpara_Map (Proxy @(PresentIn whole)) unit goget)
projectSubset :: forall subset whole f. (Maplike subset, Subset subset whole)
=> Record f whole
-> Record f subset
projectSubset = snd . fieldSubset
getFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole)
=> Record f whole
-> Record f subset
getFieldSubset = projectSubset
setFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole)
=> Record f subset
-> Record f whole
-> Record f whole
setFieldSubset subset whole = fst (fieldSubset whole) subset
modifyFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole)
=> (Record f subset -> Record f subset)
-> Record f whole
-> Record f whole
modifyFieldSubset f r = uncurry ($) (fmap f (fieldSubset @subset @whole r))
branchSubset :: forall subset whole f. (Maplike subset, Maplike whole, Subset subset whole)
=> (Variant f whole -> Maybe (Variant f subset), Variant f subset -> Variant f whole)
branchSubset =
let inj2case = \adapt (Case vif) -> Case $ \fv -> adapt (vif fv)
subs :: forall f. Record f whole -> (Record f subset -> Record f whole, Record f subset)
subs = fieldSubset @subset @whole
in
(,)
(let injs :: Record (Case f (Maybe (Variant f subset))) subset
injs = liftA_Record (inj2case Just) (injections'_Variant @subset)
wholeinjs :: Record (Case f (Maybe (Variant f subset))) whole
wholeinjs = pure_Record (Case (\_ -> Nothing))
mixedinjs = fst (subs wholeinjs) injs
in eliminate_Variant mixedinjs)
(let wholeinjs :: Record (Case f (Variant f whole)) whole
wholeinjs = liftA_Record (inj2case id) (injections'_Variant @whole)
injs = snd (subs wholeinjs)
in eliminate_Variant injs)
injectSubset :: forall subset whole f. (Maplike subset, Maplike whole, Subset subset whole)
=> Variant f subset -> Variant f whole
injectSubset = snd (branchSubset @subset @whole)
matchSubset :: forall subset whole f. (Maplike subset, Maplike whole, Subset subset whole)
=> Variant f whole -> Maybe (Variant f subset)
matchSubset = fst (branchSubset @subset @whole)
eliminateSubset :: forall subset whole f r. (Maplike subset, Maplike whole, Subset subset whole)
=> Record (Case f r) whole -> Variant f subset -> r
eliminateSubset cases =
let reducedCases = getFieldSubset @subset @whole cases
in eliminate_Variant reducedCases
fromRecordSuperset :: forall r t whole. (IsRecordType r t, Maplike t, Subset t whole) => Record I whole -> r
fromRecordSuperset = fromRecord . projectSubset