{-| 
    This module contains versions of functions from "Data.RBR", generalized to
    work with a subset of the fields of a 'Record' or the branches of a
    'Variant'.

    Besides working with subsets of fields and branches, this module is useful
    for another thing. The equality of type-level trees is unfortunately too
    strict: inserting the same elements but in /different order/ can result in
    structurally different trees, which in its turn causes annoying errors when
    trying to combine 'Record's, even as they have exactly the same fields.

    To solve these kinds of problems, functions like 'projectSubset' can be
    used to transform 'Record's indexed by one map into records indexed by
    another.

    For example, consider this code:

>>> :{
    prettyShow_RecordI $
      liftA2_Record
        (\_ x -> x)
        ( id
            $ S.projectSubset @(FromList ['("bar", _), '("foo", _)]) -- rearrange
            $ insertI @"foo"
              'a'
            $ insertI @"bar"
              True
            $ unit
        )
        ( id
            $ insertI @"bar"
              True
            $ insertI @"foo"
              'a'
            $ unit
        )
:}
"{bar = True, foo = 'a'}"

    If we remove the 'projectSubset' line that rearranges the structure of the
    first record's index map, the code ceases to compile.
    
    __Note:__ There are functions of the same name in the "Data.RBR" module,
    but they are deprecated. The functions from this module should be used
    instead, preferably qualified. The changes have to do mainly with the
    required constraints.
-}
{-# 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 (
        -- * The subset constraint
        Subset,
        -- * Record subset functions
        fieldSubset,
        projectSubset,
        getFieldSubset,
        setFieldSubset,
        modifyFieldSubset,
        -- * Variant subset functions
        branchSubset,
        injectSubset,
        matchSubset, 
        -- * Miscellany functions
        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
   )

{- $setup
 
>>> :set -XDataKinds -XTypeApplications -XPartialTypeSignatures -XFlexibleContexts -XTypeFamilies -XDeriveGeneric 
>>> :set -Wno-partial-type-signatures  
>>> import Data.RBR
>>> import qualified Data.RBR.Subset as S
>>> import Data.SOP
>>> import GHC.Generics

-}

{- | A type-level map is a subset of another if all of its entries are present in the other map.

-}
type Subset (subset :: Map Symbol q) (whole :: Map Symbol q) = KeysValuesAll (PresentIn whole) subset


{- | Like 'field', but targets multiple fields at the same time 

-}
fieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) 
            => Record f whole -> (Record f subset -> Record f whole, Record f subset)
fieldSubset :: forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
Record f whole
-> (Record f subset -> Record f whole, Record f subset)
fieldSubset Record f whole
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 :: forall (left :: Map Symbol (*)) (k :: Symbol) v
       (right :: Map Symbol (*)) (color :: 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 Record (SetField f (Record f whole)) left
left Record (SetField f (Record f whole)) right
right = Record (SetField f (Record f whole)) left
-> SetField f (Record f whole) v
-> Record (SetField f (Record f whole)) right
-> Record (SetField f (Record f whole)) ('N color left k v right)
forall {q} (f :: q -> *) (left :: Map Symbol q) (v :: q)
       (right :: Map Symbol q) (color :: Color) (k :: Symbol).
Record f left
-> f v -> Record f right -> Record f ('N color left k v right)
Node Record (SetField f (Record f whole)) left
left ((f v -> Record f whole -> Record f whole)
-> SetField f (Record f whole) v
forall q (f :: q -> *) a (b :: q).
(f b -> a -> a) -> SetField f a b
SetField (\f v
v Record f whole
w -> (f v -> Record f whole, f v) -> f v -> Record f whole
forall a b. (a, b) -> a
fst (forall {q} (k :: Symbol) (t :: Map Symbol q) (f :: q -> *).
Key k t =>
Field f t (Value k t)
forall (k :: Symbol) (t :: Map Symbol (*)) (f :: * -> *).
Key k t =>
Field f t (Value k t)
field @k @whole Record f whole
w) f v
v)) Record (SetField f (Record f whole)) right
right
         Record (SetField f (Record f whole)) subset
setters :: Record (SetField f (Record f whole)) _ = Proxy (PresentIn whole)
-> Record (SetField f (Record f whole)) 'E
-> (forall (left :: Map Symbol (*)) (k :: Symbol) v
           (right :: Map Symbol (*)) (color :: 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))
-> Record (SetField f (Record f whole)) subset
forall symbol q (c :: symbol -> q -> Constraint)
       (t :: Map symbol q) (proxy :: (symbol -> q -> Constraint) -> *)
       (r :: Map symbol q -> *).
KeysValuesAll c t =>
proxy c
-> r 'E
-> (forall (left :: Map symbol q) (k :: symbol) (v :: q)
           (right :: Map symbol q) (color :: Color).
    (c k v, KeysValuesAll c left, KeysValuesAll c right) =>
    r left -> r right -> r ('N color left k v right))
-> r t
forall (proxy :: (Symbol -> * -> Constraint) -> *)
       (r :: Map Symbol (*) -> *).
proxy (PresentIn whole)
-> r 'E
-> (forall (left :: Map Symbol (*)) (k :: Symbol) v
           (right :: Map Symbol (*)) (color :: Color).
    (PresentIn whole k v, KeysValuesAll (PresentIn whole) left,
     KeysValuesAll (PresentIn whole) right) =>
    r left -> r right -> r ('N color left k v right))
-> r subset
cpara_Map (forall {k} (t :: k). Proxy t
forall (t :: Symbol -> * -> Constraint). Proxy t
Proxy @(PresentIn whole)) Record (SetField f (Record f whole)) 'E
forall {q} (f :: q -> *). Record f Empty
unit 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)
forall (left :: Map Symbol (*)) (k :: Symbol) v
       (right :: Map Symbol (*)) (color :: 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
         appz :: SetField f a b -> f b -> K (Endo a) b
appz (SetField f b -> a -> a
func) f b
fv = Endo a -> K (Endo a) b
forall k a (b :: k). a -> K a b
K ((a -> a) -> Endo a
forall a. (a -> a) -> Endo a
Endo (f b -> a -> a
func f b
fv))
      in \Record f subset
toset -> Endo (Record f whole) -> Record f whole -> Record f whole
forall a. Endo a -> a -> a
appEndo (Record (K (Endo (Record f whole))) subset -> Endo (Record f whole)
forall a. Monoid a => Record (K a) subset -> a
forall (t :: Map Symbol (*)) a.
(Maplike t, Monoid a) =>
Record (K a) t -> a
collapse'_Record ((forall a.
 SetField f (Record f whole) a
 -> f a -> K (Endo (Record f whole)) a)
-> Record (SetField f (Record f whole)) subset
-> Record f subset
-> Record (K (Endo (Record f whole))) subset
forall (t :: Map Symbol (*)) (f :: * -> *) (g :: * -> *)
       (h :: * -> *).
Maplike t =>
(forall a. f a -> g a -> h a)
-> Record f t -> Record g t -> Record h t
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(forall a. f a -> g a -> h a)
-> Record f subset -> Record g subset -> Record h subset
liftA2_Record SetField f (Record f whole) a -> f a -> K (Endo (Record f whole)) a
forall a.
SetField f (Record f whole) a -> f a -> K (Endo (Record f whole)) a
forall {q} {k} {f :: q -> *} {a} {b :: q} {b :: k}.
SetField f a b -> f b -> K (Endo a) b
appz Record (SetField f (Record f whole)) subset
setters Record f subset
toset)) Record f whole
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 :: forall (left :: Map Symbol (*)) (k :: Symbol) v
       (right :: Map Symbol (*)) (color :: 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 Record f left
left Record f right
right = Record f left
-> f v -> Record f right -> Record f ('N color left k v right)
forall {q} (f :: q -> *) (left :: Map Symbol q) (v :: q)
       (right :: Map Symbol q) (color :: Color) (k :: Symbol).
Record f left
-> f v -> Record f right -> Record f ('N color left k v right)
Node Record f left
left (forall {q} (k :: Symbol) (t :: Map Symbol q) (f :: q -> *).
Key k t =>
Record f t -> f (Value k t)
forall (k :: Symbol) (t :: Map Symbol (*)) (f :: * -> *).
Key k t =>
Record f t -> f (Value k t)
project @k @whole Record f whole
r) Record f right
right
      in Proxy (PresentIn whole)
-> Record f 'E
-> (forall (left :: Map Symbol (*)) (k :: Symbol) v
           (right :: Map Symbol (*)) (color :: 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))
-> Record f subset
forall symbol q (c :: symbol -> q -> Constraint)
       (t :: Map symbol q) (proxy :: (symbol -> q -> Constraint) -> *)
       (r :: Map symbol q -> *).
KeysValuesAll c t =>
proxy c
-> r 'E
-> (forall (left :: Map symbol q) (k :: symbol) (v :: q)
           (right :: Map symbol q) (color :: Color).
    (c k v, KeysValuesAll c left, KeysValuesAll c right) =>
    r left -> r right -> r ('N color left k v right))
-> r t
forall (proxy :: (Symbol -> * -> Constraint) -> *)
       (r :: Map Symbol (*) -> *).
proxy (PresentIn whole)
-> r 'E
-> (forall (left :: Map Symbol (*)) (k :: Symbol) v
           (right :: Map Symbol (*)) (color :: Color).
    (PresentIn whole k v, KeysValuesAll (PresentIn whole) left,
     KeysValuesAll (PresentIn whole) right) =>
    r left -> r right -> r ('N color left k v right))
-> r subset
cpara_Map (forall {k} (t :: k). Proxy t
forall (t :: Symbol -> * -> Constraint). Proxy t
Proxy @(PresentIn whole)) Record f 'E
forall {q} (f :: q -> *). Record f Empty
unit Record f left
-> Record f right -> Record f ('N color left k v right)
forall (left :: Map Symbol (*)) (k :: Symbol) v
       (right :: Map Symbol (*)) (color :: 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)




{- | Like 'project', but extracts multiple fields at the same time.

     The types in the subset tree can often be inferred and left as wildcards in type signature.
 
>>> :{ 
  prettyShow_RecordI
    $ S.projectSubset @(FromList ['("foo", _), '("bar", _)])
    $ insertI @"foo"
      'a'
    $ insertI @"bar"
      True
    $ insertI @"baz"
      (Just ())
    $ unit
:}
"{bar = True, foo = 'a'}"

     This function also be used to convert between 'Record's with structurally dissimilar
     type-level maps that nevertheless hold the same entries. 
-}
projectSubset :: forall subset whole f. (Maplike subset, Subset subset whole) 
              => Record f whole 
              -> Record f subset
projectSubset :: forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
Record f whole -> Record f subset
projectSubset =  (Record f subset -> Record f whole, Record f subset)
-> Record f subset
forall a b. (a, b) -> b
snd ((Record f subset -> Record f whole, Record f subset)
 -> Record f subset)
-> (Record f whole
    -> (Record f subset -> Record f whole, Record f subset))
-> Record f whole
-> Record f subset
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Record f whole
-> (Record f subset -> Record f whole, Record f subset)
forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
Record f whole
-> (Record f subset -> Record f whole, Record f subset)
fieldSubset

{- | Alias for 'projectSubset'.
-}
getFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole)  
               => Record f whole 
               -> Record f subset
getFieldSubset :: forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
Record f whole -> Record f subset
getFieldSubset = Record f whole -> Record f subset
forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
Record f whole -> Record f subset
projectSubset

{- | Like 'setField', but sets multiple fields at the same time.
 
-}
setFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) 
               => Record f subset
               -> Record f whole 
               -> Record f whole
setFieldSubset :: forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
Record f subset -> Record f whole -> Record f whole
setFieldSubset Record f subset
subset Record f whole
whole = (Record f subset -> Record f whole, Record f subset)
-> Record f subset -> Record f whole
forall a b. (a, b) -> a
fst (Record f whole
-> (Record f subset -> Record f whole, Record f subset)
forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
Record f whole
-> (Record f subset -> Record f whole, Record f subset)
fieldSubset Record f whole
whole) Record f subset
subset 

{- | Like 'modifyField', but modifies multiple fields at the same time.
 
-}
modifyFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) 
                  => (Record f subset -> Record f subset)
                  -> Record f whole 
                  -> Record f whole
modifyFieldSubset :: forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
(Record f subset -> Record f subset)
-> Record f whole -> Record f whole
modifyFieldSubset Record f subset -> Record f subset
f Record f whole
r = ((Record f subset -> Record f whole)
 -> Record f subset -> Record f whole)
-> (Record f subset -> Record f whole, Record f subset)
-> Record f whole
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Record f subset -> Record f whole)
-> Record f subset -> Record f whole
forall a b. (a -> b) -> a -> b
($) ((Record f subset -> Record f subset)
-> (Record f subset -> Record f whole, Record f subset)
-> (Record f subset -> Record f whole, Record f subset)
forall a b.
(a -> b)
-> (Record f subset -> Record f whole, a)
-> (Record f subset -> Record f whole, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Record f subset -> Record f subset
f (forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
Record f whole
-> (Record f subset -> Record f whole, Record f subset)
fieldSubset @subset @whole Record f whole
r))


{- | Like 'branch', but targets multiple branches at the same time.
-}
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 :: forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Maplike whole, Subset subset whole) =>
(Variant f whole -> Maybe (Variant f subset),
 Variant f subset -> Variant f whole)
branchSubset = 
    let inj2case :: (t -> a) -> Case f t b -> Case f a b
inj2case = \t -> a
adapt (Case f b -> t
vif) -> (f b -> a) -> Case f a b
forall q (f :: q -> *) a (b :: q). (f b -> a) -> Case f a b
Case ((f b -> a) -> Case f a b) -> (f b -> a) -> Case f a b
forall a b. (a -> b) -> a -> b
$ \f b
fv -> t -> a
adapt (f b -> t
vif f b
fv) 
        -- The intuition is that getting the setter and the getter together might be faster at compile-time.
        -- The intuition might be wrong.
        subs :: forall f. Record f whole -> (Record f subset -> Record f whole, Record f subset)
        subs :: forall (f :: * -> *).
Record f whole
-> (Record f subset -> Record f whole, Record f subset)
subs = forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
Record f whole
-> (Record f subset -> Record f whole, Record f subset)
fieldSubset @subset @whole
     in
     (,)
     (let injs :: Record (Case f (Maybe (Variant f subset))) subset 
          injs :: Record (Case f (Maybe (Variant f subset))) subset
injs = (forall a.
 Case f (Variant f subset) a -> Case f (Maybe (Variant f subset)) a)
-> Record (Case f (Variant f subset)) subset
-> Record (Case f (Maybe (Variant f subset))) subset
forall (t :: Map Symbol (*)) (f :: * -> *) (g :: * -> *).
Maplike t =>
(forall a. f a -> g a) -> Record f t -> Record g t
forall (f :: * -> *) (g :: * -> *).
(forall a. f a -> g a) -> Record f subset -> Record g subset
liftA_Record ((Variant f subset -> Maybe (Variant f subset))
-> Case f (Variant f subset) a
-> Case f (Maybe (Variant f subset)) a
forall {q} {t} {a} {f :: q -> *} {b :: q}.
(t -> a) -> Case f t b -> Case f a b
inj2case Variant f subset -> Maybe (Variant f subset)
forall a. a -> Maybe a
Just) (forall (t :: Map Symbol (*)) (f :: * -> *).
Maplike t =>
Record (Case f (Variant f t)) t
injections'_Variant @subset)
          -- fixme: possibly inefficient?
          wholeinjs :: Record (Case f (Maybe (Variant f subset))) whole 
          wholeinjs :: Record (Case f (Maybe (Variant f subset))) whole
wholeinjs = (forall v. Case f (Maybe (Variant f subset)) v)
-> Record (Case f (Maybe (Variant f subset))) whole
forall (t :: Map Symbol (*)) (f :: * -> *).
Maplike t =>
(forall v. f v) -> Record f t
forall (f :: * -> *). (forall v. f v) -> Record f whole
pure_Record ((f v -> Maybe (Variant f subset))
-> Case f (Maybe (Variant f subset)) v
forall q (f :: q -> *) a (b :: q). (f b -> a) -> Case f a b
Case (\f v
_ -> Maybe (Variant f subset)
forall a. Maybe a
Nothing))
          mixedinjs :: Record (Case f (Maybe (Variant f subset))) whole
mixedinjs = (Record (Case f (Maybe (Variant f subset))) subset
 -> Record (Case f (Maybe (Variant f subset))) whole,
 Record (Case f (Maybe (Variant f subset))) subset)
-> Record (Case f (Maybe (Variant f subset))) subset
-> Record (Case f (Maybe (Variant f subset))) whole
forall a b. (a, b) -> a
fst (Record (Case f (Maybe (Variant f subset))) whole
-> (Record (Case f (Maybe (Variant f subset))) subset
    -> Record (Case f (Maybe (Variant f subset))) whole,
    Record (Case f (Maybe (Variant f subset))) subset)
forall (f :: * -> *).
Record f whole
-> (Record f subset -> Record f whole, Record f subset)
subs Record (Case f (Maybe (Variant f subset))) whole
wholeinjs) Record (Case f (Maybe (Variant f subset))) subset
injs
       in Record (Case f (Maybe (Variant f subset))) whole
-> Variant f whole -> Maybe (Variant f subset)
forall (t :: Map Symbol (*)) (f :: * -> *) r.
Maplike t =>
Record (Case f r) t -> Variant f t -> r
eliminate_Variant Record (Case f (Maybe (Variant f subset))) whole
mixedinjs)
     (let wholeinjs :: Record (Case f (Variant f whole)) whole
          wholeinjs :: Record (Case f (Variant f whole)) whole
wholeinjs = (forall a.
 Case f (Variant f whole) a -> Case f (Variant f whole) a)
-> Record (Case f (Variant f whole)) whole
-> Record (Case f (Variant f whole)) whole
forall (t :: Map Symbol (*)) (f :: * -> *) (g :: * -> *).
Maplike t =>
(forall a. f a -> g a) -> Record f t -> Record g t
forall (f :: * -> *) (g :: * -> *).
(forall a. f a -> g a) -> Record f whole -> Record g whole
liftA_Record ((Variant f whole -> Variant f whole)
-> Case f (Variant f whole) a -> Case f (Variant f whole) a
forall {q} {t} {a} {f :: q -> *} {b :: q}.
(t -> a) -> Case f t b -> Case f a b
inj2case Variant f whole -> Variant f whole
forall a. a -> a
id) (forall (t :: Map Symbol (*)) (f :: * -> *).
Maplike t =>
Record (Case f (Variant f t)) t
injections'_Variant @whole)
          injs :: Record (Case f (Variant f whole)) subset
injs = (Record (Case f (Variant f whole)) subset
 -> Record (Case f (Variant f whole)) whole,
 Record (Case f (Variant f whole)) subset)
-> Record (Case f (Variant f whole)) subset
forall a b. (a, b) -> b
snd (Record (Case f (Variant f whole)) whole
-> (Record (Case f (Variant f whole)) subset
    -> Record (Case f (Variant f whole)) whole,
    Record (Case f (Variant f whole)) subset)
forall (f :: * -> *).
Record f whole
-> (Record f subset -> Record f whole, Record f subset)
subs Record (Case f (Variant f whole)) whole
wholeinjs)
       in Record (Case f (Variant f whole)) subset
-> Variant f subset -> Variant f whole
forall (t :: Map Symbol (*)) (f :: * -> *) r.
Maplike t =>
Record (Case f r) t -> Variant f t -> r
eliminate_Variant Record (Case f (Variant f whole)) subset
injs)

{- | Like 'inject', but injects one of several possible branches.
 
     Can also be used to convert between 'Variant's with structurally
     dissimilar type-level maps that nevertheless hold the same entries. 
-}
injectSubset :: forall subset whole f. (Maplike subset, Maplike whole, Subset subset whole)
             => Variant f subset -> Variant f whole
injectSubset :: forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Maplike whole, Subset subset whole) =>
Variant f subset -> Variant f whole
injectSubset = (Variant f whole -> Maybe (Variant f subset),
 Variant f subset -> Variant f whole)
-> Variant f subset -> Variant f whole
forall a b. (a, b) -> b
snd (forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Maplike whole, Subset subset whole) =>
(Variant f whole -> Maybe (Variant f subset),
 Variant f subset -> Variant f whole)
branchSubset @subset @whole)

{- | Like 'match', but matches more than one branch.
-}
matchSubset :: forall subset whole f. (Maplike subset, Maplike whole, Subset subset whole)
            => Variant f whole -> Maybe (Variant f subset)
matchSubset :: forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Maplike whole, Subset subset whole) =>
Variant f whole -> Maybe (Variant f subset)
matchSubset = (Variant f whole -> Maybe (Variant f subset),
 Variant f subset -> Variant f whole)
-> Variant f whole -> Maybe (Variant f subset)
forall a b. (a, b) -> a
fst (forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Maplike whole, Subset subset whole) =>
(Variant f whole -> Maybe (Variant f subset),
 Variant f subset -> Variant f whole)
branchSubset @subset @whole)

{- | 
     Like 'eliminate', but allows the eliminator 'Record' to have more fields
     than there are branches in the 'Variant'.
-}
eliminateSubset :: forall subset whole f r. (Maplike subset, Maplike whole, Subset subset whole)
                => Record (Case f r) whole -> Variant f subset -> r
eliminateSubset :: forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *) r.
(Maplike subset, Maplike whole, Subset subset whole) =>
Record (Case f r) whole -> Variant f subset -> r
eliminateSubset Record (Case f r) whole
cases = 
    let reducedCases :: Record (Case f r) subset
reducedCases = forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
Record f whole -> Record f subset
getFieldSubset @subset @whole Record (Case f r) whole
cases
     in Record (Case f r) subset -> Variant f subset -> r
forall (t :: Map Symbol (*)) (f :: * -> *) r.
Maplike t =>
Record (Case f r) t -> Variant f t -> r
eliminate_Variant Record (Case f r) subset
reducedCases 

{- | 
     A common composition of 'fromRecord' and 'projectSubset'.
-}
fromRecordSuperset :: forall r t whole. (IsRecordType r t, Maplike t, Subset t whole) => Record I whole -> r 
fromRecordSuperset :: forall r (t :: Map Symbol (*)) (whole :: Map Symbol (*)).
(IsRecordType r t, Maplike t, Subset t whole) =>
Record I whole -> r
fromRecordSuperset = Record I t -> r
Record I (RecordCode r) -> r
forall r. FromRecord r => Record I (RecordCode r) -> r
fromRecord (Record I t -> r)
-> (Record I whole -> Record I t) -> Record I whole -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Record I whole -> Record I t
forall (subset :: Map Symbol (*)) (whole :: Map Symbol (*))
       (f :: * -> *).
(Maplike subset, Subset subset whole) =>
Record f whole -> Record f subset
projectSubset