{-# 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.Internal where
import Data.Proxy
import Data.Kind
import Data.Typeable
import Data.Coerce
import Data.Bifunctor (first)
import Data.Monoid (Endo(..))
import Data.List (intersperse)
import Data.Foldable (asum)
import GHC.TypeLits
import GHC.Generics (D1,C1,S1(..),M1(..),K1(..),Rec0(..))
import qualified GHC.Generics as G
import Data.SOP (I(..),K(..),unI,unK,NP(..),NS(..),All,SListI,type (-.->)(Fn,apFn),mapKIK)
import Data.SOP.NP (collapse_NP,liftA_NP,liftA2_NP,cliftA_NP,cliftA2_NP,pure_NP)
import Data.SOP.NS (collapse_NS,ap_NS,injections,Injection)
data Color = R
| B
deriving (Show,Eq)
data Map k v = E
| N Color (Map k v) k v (Map k v)
deriving (Show,Eq)
type EmptyMap = E
type family
KeysValuesAllF (c :: k -> v -> Constraint) (t :: Map k v) :: Constraint where
KeysValuesAllF _ E = ()
KeysValuesAllF c (N color left k v right) = (c k v, KeysValuesAll c left, KeysValuesAll c right)
class KeysValuesAllF c t => KeysValuesAll (c :: k -> v -> Constraint) (t :: Map k v) where
cpara_Map ::
proxy c
-> r E
-> (forall left k v right color . (c k v, KeysValuesAll c left, KeysValuesAll c right)
=> r left -> r right -> r (N color left k v right))
-> r t
instance KeysValuesAll c E where
cpara_Map _p nil _step = nil
instance (c k v, KeysValuesAll c left, KeysValuesAll c right) => KeysValuesAll c (N color left k v right) where
cpara_Map p nil cons =
cons (cpara_Map p nil cons) (cpara_Map p nil cons)
cpure_Record :: forall c t f. KeysValuesAll c t => (Proxy c) -> (forall k v. c k v => f v) -> Record f t
cpure_Record _ fpure = cpara_Map (Proxy @c) unit go
where
go :: forall left k' v' right color. (c k' v', KeysValuesAll c left, KeysValuesAll c right)
=> Record f left
-> Record f right
-> Record f (N color left k' v' right)
go left right = Node left (fpure @k' @v') right
demoteKeys :: forall t. KeysValuesAll KnownKey t => Record (K String) t
demoteKeys = cpara_Map (Proxy @KnownKey) unit go
where
go :: forall left k v right color. (KnownKey k v, KeysValuesAll KnownKey left, KeysValuesAll KnownKey right)
=> Record (K String) left
-> Record (K String) right
-> Record (K String) (N color left k v right)
go left right = Node left (K (symbolVal (Proxy @k))) right
class KnownSymbol k => KnownKey (k :: Symbol) (v :: z)
instance KnownSymbol k => KnownKey k v
demoteEntries :: forall t. KeysValuesAll KnownKeyTypeableValue t => Record (K (String,TypeRep)) t
demoteEntries = cpara_Map (Proxy @KnownKeyTypeableValue) unit go
where
go :: forall left k v right color. (KnownKeyTypeableValue k v, KeysValuesAll KnownKeyTypeableValue left, KeysValuesAll KnownKeyTypeableValue right)
=> Record (K (String,TypeRep)) left
-> Record (K (String,TypeRep)) right
-> Record (K (String,TypeRep)) (N color left k v right)
go left right = Node left (K (symbolVal (Proxy @k),typeRep (Proxy @v))) right
class (KnownSymbol k, Typeable v) => KnownKeyTypeableValue (k :: Symbol) (v :: Type)
instance (KnownSymbol k, Typeable v) => KnownKeyTypeableValue k v
data Record (f :: Type -> Type) (t :: Map Symbol Type) where
Empty :: Record f E
Node :: Record f left -> f v -> Record f right -> Record f (N color left k v right)
instance (Productlike '[] t result, Show (NP f result)) => Show (Record f t) where
show x = "fromNP (" ++ show (toNP x) ++ ")"
collapse_Record :: forall t result a. (Productlike '[] t result) => Record (K a) t -> [a]
collapse_Record = collapse_NP . toNP
prettyShowRecord :: forall t flat f. (KeysValuesAll KnownKey t,Productlike '[] t flat, All Show flat, SListI flat)
=> (forall x. Show x => f x -> String)
-> Record f t
-> String
prettyShowRecord showf r =
let keysflat = toNP @t (demoteKeys @t)
valuesflat = toNP @t r
entries = cliftA2_NP (Proxy @Show) (\(K key) fv -> K (key ++ " = " ++ showf fv))
keysflat
valuesflat
in "{" ++ mconcat (intersperse ", " (collapse_NP entries)) ++ "}"
prettyShowRecordI :: forall t flat. (KeysValuesAll KnownKey t,Productlike '[] t flat, All Show flat, SListI flat) => Record I t -> String
prettyShowRecordI r = prettyShowRecord (show . unI) r
unit :: Record f E
unit = Empty
data Variant (f :: Type -> Type) (t :: Map Symbol Type) where
Here :: f v -> Variant f (N color left k v right)
LookRight :: Variant f t -> Variant f (N color' left' k' v' t)
LookLeft :: Variant f t -> Variant f (N color' t k' v' right')
instance (Sumlike '[] t result, Show (NS f result)) => Show (Variant f t) where
show x = "fromNS (" ++ show (toNS x) ++ ")"
impossible :: Variant f E -> b
impossible v = case v of
prettyShowVariant :: forall t flat f. (KeysValuesAll KnownKey t,Productlike '[] t flat, Sumlike '[] t flat, All Show flat, SListI flat)
=> (forall x. Show x => f x -> String)
-> Variant f t
-> String
prettyShowVariant showf v =
let keysflat = toNP @t (demoteKeys @t)
eliminators = cliftA_NP (Proxy @Show) (\(K k) -> Fn (\fv -> (K (k ++ " (" ++ showf fv ++ ")")))) keysflat
valuesflat = toNS @t v
in collapse_NS (ap_NS eliminators valuesflat)
prettyShowVariantI :: forall t flat. (KeysValuesAll KnownKey t,Productlike '[] t flat, Sumlike '[] t flat, All Show flat, SListI flat)
=> Variant I t -> String
prettyShowVariantI v = prettyShowVariant (show . unI) v
type family InsertAll (es :: [(Symbol,Type)]) (t :: Map Symbol Type) :: Map Symbol Type where
InsertAll '[] t = t
InsertAll ( '(name,fieldType) ': es ) t = Insert name fieldType (InsertAll es t)
type FromList (es :: [(Symbol,Type)]) = InsertAll es E
addField :: forall k v t f . Insertable k v t => f v -> Record f t -> Record f (Insert k v t)
addField = insert @k @v @t @f
insertI :: forall k v t . Insertable k v t => v -> Record I t -> Record I (Insert k v t)
insertI = insert @k @v @t . I
addFieldI :: forall k v t . Insertable k v t => v -> Record I t -> Record I (Insert k v t)
addFieldI = insertI @k @v @t
class Insertable (k :: Symbol) (v :: Type) (t :: Map Symbol Type) where
type Insert k v t :: Map Symbol Type
insert :: f v -> Record f t -> Record f (Insert k v t)
widen :: Variant f t -> Variant f (Insert k v t)
instance (InsertableHelper1 k v t, CanMakeBlack (Insert1 k v t)) => Insertable k v t where
type Insert k v t = MakeBlack (Insert1 k v t)
insert fv r = makeBlackR (insert1 @k @v fv r)
widen v = makeBlackV (widen1 @k @v v)
class CanMakeBlack (t :: Map Symbol Type) where
type MakeBlack t :: Map Symbol Type
makeBlackR :: Record f t -> Record f (MakeBlack t)
makeBlackV :: Variant f t -> Variant f (MakeBlack t)
instance CanMakeBlack (N color left k v right) where
type MakeBlack (N color left k v right) = N B left k v right
makeBlackR (Node left fv right) = Node left fv right
makeBlackV v = case v of
LookLeft l -> LookLeft l
Here v -> Here v
LookRight r -> LookRight r
instance CanMakeBlack E where
type MakeBlack E = E
makeBlackR Empty = Empty
makeBlackV = impossible
class InsertableHelper1 (k :: Symbol)
(v :: Type)
(t :: Map Symbol Type) where
type Insert1 k v t :: Map Symbol Type
insert1 :: f v -> Record f t -> Record f (Insert1 k v t)
widen1 :: Variant f t -> Variant f (Insert1 k v t)
instance InsertableHelper1 k v E where
type Insert1 k v E = N R E k v E
insert1 fv Empty = Node Empty fv Empty
widen1 = impossible
instance (CmpSymbol k k' ~ ordering,
InsertableHelper2 ordering k v color left k' v' right
)
=> InsertableHelper1 k v (N color left k' v' right) where
type Insert1 k v (N color left k' v' right) = Insert2 (CmpSymbol k k') k v color left k' v' right
insert1 = insert2 @ordering @k @v @color @left @k' @v' @right
widen1 = widen2 @ordering @k @v @color @left @k' @v' @right
class InsertableHelper2 (ordering :: Ordering)
(k :: Symbol)
(v :: Type)
(color :: Color)
(left :: Map Symbol Type)
(k' :: Symbol)
(v' :: Type)
(right :: Map Symbol Type) where
type Insert2 ordering k v color left k' v' right :: Map Symbol Type
insert2 :: f v -> Record f (N color left k' v' right) -> Record f (Insert2 ordering k v color left k' v' right)
widen2 :: Variant f (N color left k' v' right) -> Variant f (Insert2 ordering k v color left k' v' right)
instance (InsertableHelper1 k v left,
Balanceable (Insert1 k v left) k' v' right
)
=> InsertableHelper2 LT k v B left k' v' right where
type Insert2 LT k v B left k' v' right = Balance (Insert1 k v left) k' v' right
insert2 fv (Node left fv' right) = balanceR @_ @k' @v' @right (Node (insert1 @k @v fv left) fv' right)
widen2 v = balanceV @(Insert1 k v left) @k' @v' @right $ case v of
Here x -> Here x
LookLeft x -> LookLeft (widen1 @k @v x)
LookRight x -> LookRight x
instance (InsertableHelper1 k v left,
Balanceable (Insert1 k v left) k' v' right
)
=> InsertableHelper2 LT k v R left k' v' right where
type Insert2 LT k v R left k' v' right = N R (Insert1 k v left) k' v' right
insert2 fv (Node left fv' right) = Node (insert1 @k @v fv left) fv' right
widen2 v = case v of
Here x -> Here x
LookLeft x -> LookLeft (widen1 @k @v x)
LookRight x -> LookRight x
instance InsertableHelper2 EQ k v color left k v right where
type Insert2 EQ k v color left k v right = N color left k v right
insert2 fv (Node left _ right) = Node left fv right
widen2 = id
instance (InsertableHelper1 k v right,
Balanceable left k' v' (Insert1 k v right)
)
=> InsertableHelper2 GT k v B left k' v' right where
type Insert2 GT k v B left k' v' right = Balance left k' v' (Insert1 k v right)
insert2 fv (Node left fv' right) = balanceR @left @k' @v' @_ (Node left fv' (insert1 @k @v fv right))
widen2 v = balanceV @left @k' @v' @(Insert1 k v right) $ case v of
Here x -> Here x
LookLeft x -> LookLeft x
LookRight x -> LookRight (widen1 @k @v x)
instance (InsertableHelper1 k v right,
Balanceable left k' v' (Insert1 k v right)
)
=> InsertableHelper2 GT k v R left k' v' right where
type Insert2 GT k v R left k' v' right = N R left k' v' (Insert1 k v right)
insert2 fv (Node left fv' right) = Node left fv' (insert1 @k @v fv right)
widen2 v = case v of
Here x -> Here x
LookLeft x -> LookLeft x
LookRight x -> LookRight (widen1 @k @v x)
data BalanceAction = BalanceSpecial
| BalanceLL
| BalanceLR
| BalanceRL
| BalanceRR
| DoNotBalance
deriving Show
type family ShouldBalance (left :: Map k' v') (right :: Map k' v') :: BalanceAction where
ShouldBalance (N R _ _ _ _) (N R _ _ _ _) = BalanceSpecial
ShouldBalance (N R (N R _ _ _ _) _ _ _) _ = BalanceLL
ShouldBalance (N R _ _ _ (N R _ _ _ _)) _ = BalanceLR
ShouldBalance _ (N R (N R _ _ _ _) _ _ _) = BalanceRL
ShouldBalance _ (N R _ _ _ (N R _ _ _ _)) = BalanceRR
ShouldBalance _ _ = DoNotBalance
class Balanceable (left :: Map Symbol Type) (k :: Symbol) (v :: Type) (right :: Map Symbol Type) where
type Balance left k v right :: Map Symbol Type
balanceR :: Record f (N color left k v right) -> Record f (Balance left k v right)
balanceV :: Variant f (N color left k v right) -> Variant f (Balance left k v right)
instance (ShouldBalance left right ~ action,
BalanceableHelper action left k v right
)
=> Balanceable left k v right where
type Balance left k v right = Balance' (ShouldBalance left right) left k v right
balanceR = balanceR' @action @left @k @v @right
balanceV = balanceV' @action @left @k @v @right
class BalanceableHelper (action :: BalanceAction)
(left :: Map Symbol Type)
(k :: Symbol)
(v :: Type)
(right :: Map Symbol Type) where
type Balance' action left k v right :: Map Symbol Type
balanceR' :: Record f (N color left k v right) -> Record f (Balance' action left k v right)
balanceV' :: Variant f (N color left k v right) -> Variant f (Balance' action left k v right)
instance BalanceableHelper BalanceSpecial (N R left1 k1 v1 right1) kx vx (N R left2 k2 v2 right2) where
type Balance' BalanceSpecial (N R left1 k1 v1 right1) kx vx (N R left2 k2 v2 right2) =
N R (N B left1 k1 v1 right1) kx vx (N B left2 k2 v2 right2)
balanceR' (Node (Node left1 v1 right1) vx (Node left2 v2 right2)) =
(Node (Node left1 v1 right1) vx (Node left2 v2 right2))
balanceV' v = case v of
LookLeft (LookLeft x) -> LookLeft (LookLeft x)
LookLeft (Here x) -> LookLeft (Here x)
LookLeft (LookRight x) -> LookLeft (LookRight x)
Here x -> Here x
LookRight (LookLeft x) -> LookRight (LookLeft x)
LookRight (Here x) -> LookRight (Here x)
LookRight (LookRight x) -> LookRight (LookRight x)
instance BalanceableHelper BalanceLL (N R (N R a k1 v1 b) k2 v2 c) k3 v3 d where
type Balance' BalanceLL (N R (N R a k1 v1 b) k2 v2 c) k3 v3 d =
N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d)
balanceR' (Node (Node (Node a fv1 b) fv2 c) fv3 d) =
Node (Node a fv1 b) fv2 (Node c fv3 d)
balanceV' v = case v of
LookLeft (LookLeft x) -> LookLeft (case x of LookLeft y -> LookLeft y
Here y -> Here y
LookRight y -> LookRight y)
LookLeft (Here x) -> Here x
LookLeft (LookRight x) -> LookRight (LookLeft x)
Here x -> LookRight (Here x)
LookRight x -> LookRight (LookRight x)
instance BalanceableHelper BalanceLR (N R a k1 v1 (N R b k2 v2 c)) k3 v3 d where
type Balance' BalanceLR (N R a k1 v1 (N R b k2 v2 c)) k3 v3 d =
N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d)
balanceR' (Node (Node a fv1 (Node b fv2 c)) fv3 d) =
Node (Node a fv1 b) fv2 (Node c fv3 d)
balanceV' v = case v of
LookLeft (LookLeft x) -> LookLeft (LookLeft x)
LookLeft (Here x) -> LookLeft (Here x)
LookLeft (LookRight x) -> case x of LookLeft y -> LookLeft (LookRight y)
Here y -> Here y
LookRight y -> LookRight (LookLeft y)
Here x -> LookRight (Here x)
LookRight x -> LookRight (LookRight x)
instance BalanceableHelper BalanceRL a k1 v1 (N R (N R b k2 v2 c) k3 v3 d) where
type Balance' BalanceRL a k1 v1 (N R (N R b k2 v2 c) k3 v3 d) =
N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d)
balanceR' (Node a fv1 (Node (Node b fv2 c) fv3 d)) =
Node (Node a fv1 b) fv2 (Node c fv3 d)
balanceV' v = case v of
LookLeft x -> LookLeft (LookLeft x)
Here x -> LookLeft (Here x)
LookRight (LookLeft x) -> case x of LookLeft y -> LookLeft (LookRight y)
Here y -> Here y
LookRight y -> LookRight (LookLeft y)
LookRight (Here x) -> LookRight (Here x)
LookRight (LookRight x) -> LookRight (LookRight x)
instance BalanceableHelper BalanceRR a k1 v1 (N R b k2 v2 (N R c k3 v3 d)) where
type Balance' BalanceRR a k1 v1 (N R b k2 v2 (N R c k3 v3 d)) =
N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d)
balanceR' (Node a fv1 (Node b fv2 (Node c fv3 d))) =
Node (Node a fv1 b) fv2 (Node c fv3 d)
balanceV' v = case v of
LookLeft x -> LookLeft (LookLeft x)
Here x -> LookLeft (Here x)
LookRight (LookLeft x) -> LookLeft (LookRight x)
LookRight (Here x) -> Here x
LookRight (LookRight x) -> LookRight (case x of LookLeft y -> LookLeft y
Here y -> Here y
LookRight y -> LookRight y)
instance BalanceableHelper DoNotBalance a k v b where
type Balance' DoNotBalance a k v b = N B a k v b
balanceR' (Node left v right) = (Node left v right)
balanceV' v = case v of
LookLeft l -> LookLeft l
Here v -> Here v
LookRight r -> LookRight r
type family Field (f :: Type -> Type) (t :: Map Symbol Type) (v :: Type) where
Field f t v = Record f t -> (f v -> Record f t, f v)
type family Branch (f :: Type -> Type) (t :: Map Symbol Type) (v :: Type) where
Branch f t v = (Variant f t -> Maybe (f v), f v -> Variant f t)
class Key (k :: Symbol) (t :: Map Symbol Type) where
type Value k t :: Type
field :: Field f t (Value k t)
branch :: Branch f t (Value k t)
class KeyHelper (ordering :: Ordering) (k :: Symbol) (left :: Map Symbol Type) (v :: Type) (right :: Map Symbol Type) where
type Value' ordering k left v right :: Type
field' :: Field f (N colorx left kx v right) (Value' ordering k left v right)
branch' :: Branch f (N colorx left kx v right) (Value' ordering k left v right)
instance (CmpSymbol k' k ~ ordering, KeyHelper ordering k left v' right) => Key k (N color left k' v' right) where
type Value k (N color left k' v' right) = Value' (CmpSymbol k' k) k left v' right
field = field' @ordering @k @left @v' @right
branch = branch' @ordering @k @left @v' @right
instance (CmpSymbol k2 k ~ ordering, KeyHelper ordering k left2 v2 right2)
=> KeyHelper LT k left v (N color2 left2 k2 v2 right2) where
type Value' LT k left v (N color2 left2 k2 v2 right2) = Value' (CmpSymbol k2 k) k left2 v2 right2
field' (Node left fv right) =
let (setter,x) = field' @ordering @k @left2 @v2 @right2 right
in (\z -> Node left fv (setter z),x)
branch' =
let (match,inj) = branch' @ordering @k @left2 @v2 @right2
in (\case LookRight x -> match x
_ -> Nothing,
\fv -> LookRight (inj fv))
instance (CmpSymbol k2 k ~ ordering, KeyHelper ordering k left2 v2 right2)
=> KeyHelper GT k (N color2 left2 k2 v2 right2) v' right where
type Value' GT k (N color2 left2 k2 v2 right2) v' right = Value' (CmpSymbol k2 k) k left2 v2 right2
field' (Node left fv right) =
let (setter,x) = field' @ordering @k @left2 @v2 @right2 left
in (\z -> Node (setter z) fv right,x)
branch' =
let (match,inj) = branch' @ordering @k @left2 @v2 @right2
in (\case LookLeft x -> match x
_ -> Nothing,
\fv -> LookLeft (inj fv))
instance KeyHelper EQ k left v right where
type Value' EQ k left v right = v
field' (Node left fv right) = (\x -> Node left x right, fv)
branch' = (\case Here x -> Just x
_ -> Nothing,
Here)
project :: forall k t f . Key k t => Record f t -> f (Value k t)
project = snd . field @k @t
getField :: forall k t f . Key k t => Record f t -> f (Value k t)
getField = project @k @t @f
setField :: forall k t f . Key k t => f (Value k t) -> Record f t -> Record f t
setField fv r = fst (field @k @t @f r) fv
modifyField :: forall k t f . Key k t => (f (Value k t) -> f (Value k t)) -> Record f t -> Record f t
modifyField f r = uncurry ($) (fmap f (field @k @t @f r))
inject :: forall k t f. Key k t => f (Value k t) -> Variant f t
inject = snd (branch @k @t)
match :: forall k t f. Key k t => Variant f t -> Maybe (f (Value k t))
match = fst (branch @k @t)
projectI :: forall k t . Key k t => Record I t -> Value k t
projectI = unI . snd . field @k @t
getFieldI :: forall k t . Key k t => Record I t -> Value k t
getFieldI = projectI @k @t
setFieldI :: forall k t . Key k t => Value k t -> Record I t -> Record I t
setFieldI v r = fst (field @k @t r) (I v)
modifyFieldI :: forall k t . Key k t => (Value k t -> Value k t) -> Record I t -> Record I t
modifyFieldI f = modifyField @k @t (I . f . unI)
injectI :: forall k t. Key k t => Value k t -> Variant I t
injectI = snd (branch @k @t) . I
matchI :: forall k t . Key k t => Variant I t -> Maybe (Value k t)
matchI v = unI <$> fst (branch @k @t) v
eliminate :: (Productlike '[] t result, Sumlike '[] t result, SListI result) => Record (Case f r) t -> Variant f t -> r
eliminate cases variant =
let adapt (Case e) = Fn (\fv -> K (e fv))
in collapse_NS (ap_NS (liftA_NP adapt (toNP cases)) (toNS variant))
newtype Case f a b = Case (f b -> a)
addCase :: forall k v t f a. Insertable k v t => (f v -> a) -> Record (Case f a) t -> Record (Case f a) (Insert k v t)
addCase f = addField @k @v @t (Case f)
addCaseI :: forall k v t a. Insertable k v t => (v -> a) -> Record (Case I a) t -> Record (Case I a) (Insert k v t)
addCaseI f = addField @k @v @t (Case (f . unI))
newtype SetField f a b = SetField { getSetField :: f b -> a -> a }
class (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol Type) (k :: Symbol) (v :: Type)
instance (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol Type) (k :: Symbol) (v :: Type)
type ProductlikeSubset (subset :: Map Symbol Type) (whole :: Map Symbol Type) (flat :: [Type]) =
(KeysValuesAll (PresentIn whole) subset,
Productlike '[] subset flat,
SListI flat)
fieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat)
=> 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 = toNP @subset @_ @(SetField f (Record f whole)) (cpara_Map (Proxy @(PresentIn whole)) unit goset)
appz (SetField func) fv = K (Endo (func fv))
in \toset -> appEndo (mconcat (collapse_NP (liftA2_NP appz setters (toNP 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 flat f. (ProductlikeSubset subset whole flat)
=> Record f whole
-> Record f subset
projectSubset = snd . fieldSubset
getFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat)
=> Record f whole
-> Record f subset
getFieldSubset = projectSubset
setFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat)
=> Record f subset
-> Record f whole
-> Record f whole
setFieldSubset subset whole = fst (fieldSubset whole) subset
modifyFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat)
=> (Record f subset -> Record f subset)
-> Record f whole
-> Record f whole
modifyFieldSubset f r = uncurry ($) (fmap f (fieldSubset @subset @whole r))
type SumlikeSubset (subset :: Map Symbol Type) (whole :: Map Symbol Type) (subflat :: [Type]) (wholeflat :: [Type]) =
(KeysValuesAll (PresentIn whole) subset,
Productlike '[] whole wholeflat,
Sumlike '[] whole wholeflat,
SListI wholeflat,
Productlike '[] subset subflat,
Sumlike '[] subset subflat,
SListI subflat)
branchSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat)
=> (Variant f whole -> Maybe (Variant f subset), Variant f subset -> Variant f whole)
branchSubset =
let inj2case :: forall t flat f v. Sumlike '[] t flat => (_ -> _) -> Injection _ flat v -> Case _ _ v
inj2case = \adapt -> \fn -> Case (\fv -> adapt (fromNS @t (unK (apFn fn 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 = fromNP @subset (liftA_NP (inj2case Just) (injections @subflat))
wholeinjs :: Record (Case f (Maybe (Variant f subset))) whole
wholeinjs = fromNP @whole (pure_NP (Case (\_ -> Nothing)))
mixedinjs = fst (subs wholeinjs) injs
in eliminate mixedinjs)
(let wholeinjs :: Record (Case f (Variant f whole)) whole
wholeinjs = fromNP @whole (liftA_NP (inj2case id) (injections @wholeflat))
injs = snd (subs wholeinjs)
in eliminate injs)
injectSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat)
=> Variant f subset -> Variant f whole
injectSubset = snd (branchSubset @subset @whole @subflat @wholeflat)
matchSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat)
=> Variant f whole -> Maybe (Variant f subset)
matchSubset = fst (branchSubset @subset @whole @subflat @wholeflat)
eliminateSubset :: forall subset whole subflat wholeflat f r. (SumlikeSubset subset whole subflat wholeflat)
=> Record (Case f r) whole -> Variant f subset -> r
eliminateSubset cases =
let reducedCases = getFieldSubset @subset @whole cases
in eliminate reducedCases
class Productlike (start :: [Type])
(t :: Map Symbol Type)
(result :: [Type]) | start t -> result, result t -> start where
prefixNP:: Record f t -> NP f start -> NP f result
breakNP :: NP f result -> (Record f t, NP f start)
instance Productlike start E start where
prefixNP _ start = start
breakNP start = (Empty, start)
instance (Productlike start right middle,
Productlike (v ': middle) left result)
=> Productlike start (N color left k v right) result where
prefixNP (Node left fv right) start =
prefixNP @_ @left @result left (fv :* prefixNP @start @right @middle right start)
breakNP result =
let (left, fv :* middle) = breakNP @_ @left @result result
(right, start) = breakNP @start @right middle
in (Node left fv right, start)
toNP :: forall t result f. Productlike '[] t result => Record f t -> NP f result
toNP r = prefixNP r Nil
fromNP :: forall t result f. Productlike '[] t result => NP f result -> Record f t
fromNP np = let (r,Nil) = breakNP np in r
class Sumlike (start :: [Type])
(t :: Map Symbol Type)
(result :: [Type]) | start t -> result, result t -> start where
prefixNS :: Either (NS f start) (Variant f t) -> NS f result
breakNS :: NS f result -> Either (NS f start) (Variant f t)
instance Sumlike start
(N color E k v E)
(v ': start) where
prefixNS = \case
Left l -> S l
Right x -> case x of Here fv -> Z @_ @v @start fv
breakNS = \case
Z x -> Right (Here x)
S x -> Left x
instance (Sumlike start (N colorR leftR kR vR rightR) middle,
Sumlike (v ': middle) (N colorL leftL kL vL rightL) result)
=> Sumlike start
(N color (N colorL leftL kL vL rightL) k v (N colorR leftR kR vR rightR))
result where
prefixNS = \case
Left x ->
prefixNS @_ @(N colorL leftL kL vL rightL) (Left (S (prefixNS @_ @(N colorR leftR kR vR rightR) (Left x))))
Right x ->
case x of LookLeft x -> prefixNS @(v ': middle) @(N colorL leftL kL vL rightL) @result (Right x)
Here x -> prefixNS @_ @(N colorL leftL kL vL rightL) (Left (Z x))
LookRight x -> prefixNS @_ @(N colorL leftL kL vL rightL) (Left (S (prefixNS (Right x))))
breakNS ns = case breakNS @(v ': middle) @(N colorL leftL kL vL rightL) ns of
Left x -> case x of
Z x -> Right (Here x)
S x -> case breakNS @start @(N colorR leftR kR vR rightR) x of
Left ns -> Left ns
Right v -> Right (LookRight v)
Right v -> Right (LookLeft v)
instance Sumlike (v ': start) (N colorL leftL kL vL rightL) result
=> Sumlike start (N color (N colorL leftL kL vL rightL) k v E) result where
prefixNS = \case
Left x ->
prefixNS @_ @(N colorL leftL kL vL rightL) (Left (S x))
Right x ->
case x of LookLeft x -> prefixNS @(v ': start) @(N colorL leftL kL vL rightL) @result (Right x)
Here x -> prefixNS @_ @(N colorL leftL kL vL rightL) (Left (Z x))
breakNS ns = case breakNS @(v ': start) @(N colorL leftL kL vL rightL) ns of
Left x -> case x of
Z x -> Right (Here x)
S x -> Left x
Right v -> Right (LookLeft v)
instance Sumlike start (N colorR leftR kR vR rightR) middle
=> Sumlike start (N color E k v (N colorR leftR kR vR rightR)) (v ': middle) where
prefixNS = \case
Left x -> S (prefixNS @_ @(N colorR leftR kR vR rightR) (Left x))
Right x ->
case x of Here x -> Z x
LookRight x -> S (prefixNS @_ @(N colorR leftR kR vR rightR) (Right x))
breakNS = \case
Z x -> Right (Here x)
S x -> case breakNS @_ @(N colorR leftR kR vR rightR) x of
Left ns -> Left ns
Right v -> Right (LookRight v)
toNS :: forall t result f. Sumlike '[] t result => Variant f t -> NS f result
toNS = prefixNS . Right
fromNS :: forall t result f. Sumlike '[] t result => NS f result -> Variant f t
fromNS ns = case breakNS ns of
Left _ -> error "this never happens"
Right x -> x
class ToRecord (r :: Type) where
type RecordCode r :: Map Symbol Type
type RecordCode r = RecordCode' E (G.Rep r)
toRecord :: r -> Record I (RecordCode r)
default toRecord :: (G.Generic r,ToRecordHelper E (G.Rep r),RecordCode r ~ RecordCode' E (G.Rep r)) => r -> Record I (RecordCode r)
toRecord r = toRecord' unit (G.from r)
class ToRecordHelper (start :: Map Symbol Type) (g :: Type -> Type) where
type RecordCode' start g :: Map Symbol Type
toRecord' :: Record I start -> g x -> Record I (RecordCode' start g)
instance ToRecordHelper E fields => ToRecordHelper E (D1 meta (C1 metacons fields)) where
type RecordCode' E (D1 meta (C1 metacons fields)) = RecordCode' E fields
toRecord' r (M1 (M1 g)) = toRecord' @E @fields r g
instance (Insertable k v start) =>
ToRecordHelper start
(S1 ('G.MetaSel ('Just k)
unpackedness
strictness
laziness)
(Rec0 v))
where
type RecordCode' start
(S1 ('G.MetaSel ('Just k)
unpackedness
strictness
laziness)
(Rec0 v)) = Insert k v start
toRecord' start (M1 (K1 v)) = insertI @k v start
instance ( ToRecordHelper start t2,
RecordCode' start t2 ~ middle,
ToRecordHelper middle t1
) =>
ToRecordHelper start (t1 G.:*: t2)
where
type RecordCode' start (t1 G.:*: t2) = RecordCode' (RecordCode' start t2) t1
toRecord' start (t1 G.:*: t2) = toRecord' @middle (toRecord' @start start t2) t1
class ToRecord r => FromRecord (r :: Type) where
fromRecord :: Record I (RecordCode r) -> r
default fromRecord :: (G.Generic r, FromRecordHelper (RecordCode r) (G.Rep r)) => Record I (RecordCode r) -> r
fromRecord r = G.to (fromRecord' @(RecordCode r) @(G.Rep r) r)
class FromRecordHelper (t :: Map Symbol Type) (g :: Type -> Type) where
fromRecord' :: Record I t -> g x
instance FromRecordHelper t fields => FromRecordHelper t (D1 meta (C1 metacons fields)) where
fromRecord' r = M1 (M1 (fromRecord' @t @fields r))
instance (Key k t, Value k t ~ v) =>
FromRecordHelper t
(S1 ('G.MetaSel ('Just k)
unpackedness
strictness
laziness)
(Rec0 v))
where
fromRecord' r = let v = projectI @k r in M1 (K1 v)
instance ( FromRecordHelper t t1,
FromRecordHelper t t2
) =>
FromRecordHelper t (t1 G.:*: t2)
where
fromRecord' r =
let v1 = fromRecord' @_ @t1 r
v2 = fromRecord' @_ @t2 r
in v1 G.:*: v2
type family VariantCode (s :: Type) :: Map Symbol Type where
VariantCode s = VariantCode' E (G.Rep s)
type family VariantCode' (acc :: Map Symbol Type) (g :: Type -> Type) :: Map Symbol Type where
VariantCode' acc (D1 meta fields) = VariantCode' acc fields
VariantCode' acc (t1 G.:+: t2) = VariantCode' (VariantCode' acc t2) t1
VariantCode' acc (C1 (G.MetaCons k _ _) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v))) = Insert k v acc
class FromVariant (s :: Type) where
fromVariant :: Variant I (VariantCode s) -> s
default fromVariant :: (G.Generic s, FromVariantHelper (VariantCode s) (G.Rep s)) => Variant I (VariantCode s) -> s
fromVariant v = case fromVariant' @(VariantCode s) v of
Just x -> G.to x
Nothing -> error "fromVariant match fail. Should not happen."
class FromVariantHelper (t :: Map Symbol Type) (g :: Type -> Type) where
fromVariant' :: Variant I t -> Maybe (g x)
instance FromVariantHelper t fields => FromVariantHelper t (D1 meta fields) where
fromVariant' v = M1 <$> fromVariant' @t v
instance (Key k t, Value k t ~ v)
=> FromVariantHelper t (C1 (G.MetaCons k x y) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v)))
where
fromVariant' v = case matchI @k @t v of
Just x -> Just (M1 (M1 (K1 x)) )
Nothing -> Nothing
instance ( FromVariantHelper t t1,
FromVariantHelper t t2
) =>
FromVariantHelper t (t1 G.:+: t2)
where
fromVariant' v = case fromVariant' @t @t1 v of
Just x1 -> Just (G.L1 x1)
Nothing -> case fromVariant' @t @t2 v of
Just x2 -> Just (G.R1 x2)
Nothing -> Nothing
class ToVariant (s :: Type) where
toVariant :: s -> Variant I (VariantCode s)
default toVariant :: (G.Generic s, ToVariantHelper (VariantCode s) (G.Rep s)) => s -> Variant I (VariantCode s)
toVariant s = toVariant' @(VariantCode s) @(G.Rep s) (G.from s)
class ToVariantHelper (t :: Map Symbol Type) (g :: Type -> Type) where
toVariant' :: g x -> Variant I t
instance ToVariantHelper t fields => ToVariantHelper t (D1 meta fields) where
toVariant' (M1 fields) = toVariant' @t fields
instance (Key k t, Value k t ~ v) =>
ToVariantHelper t (C1 (G.MetaCons k x y) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v)))
where
toVariant' (M1 (M1 (K1 v))) = injectI @k v
instance ( ToVariantHelper t t1,
ToVariantHelper t t2
) =>
ToVariantHelper t (t1 G.:+: t2)
where
toVariant' = \case
G.L1 l -> toVariant' @t l
G.R1 r -> toVariant' @t r
type family DiscriminateBalL (l :: Map k v) (r :: Map k v) :: Bool where
DiscriminateBalL (N R _ _ _ _) _ = False
DiscriminateBalL _ _ = True
class BalanceableL (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
type BalL l k v r :: Map Symbol Type
balLR :: Record f (N color l k v r) -> Record f (BalL l k v r)
balLV :: Variant f (N color l k v r) -> Variant f (BalL l k v r)
class BalanceableHelperL (b :: Bool) (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
type BalL' b l k v r :: Map Symbol Type
balLR' :: Record f (N color l k v r) -> Record f (BalL' b l k v r)
balLV' :: Variant f (N color l k v r) -> Variant f (BalL' b l k v r)
instance (DiscriminateBalL l r ~ b, BalanceableHelperL b l k v r) => BalanceableL l k v r where
type BalL l k v r = BalL' (DiscriminateBalL l r) l k v r
balLR = balLR' @b @l @k @v @r
balLV = balLV' @b @l @k @v @r
instance BalanceableHelperL False (N R left1 k1 v1 right1) k2 v2 right2 where
type BalL' False (N R left1 k1 v1 right1) k2 v2 right2 =
(N R (N B left1 k1 v1 right1) k2 v2 right2)
balLR' (Node (Node left' v' right') v right) = Node (Node left' v' right') v right
balLV' v = case v of LookLeft x -> LookLeft (case x of LookLeft y -> LookLeft y
Here y -> Here y
LookRight y -> LookRight y)
Here x -> Here x
LookRight x -> LookRight x
instance (BalanceableHelper (ShouldBalance t1 (N R t2 z zv t3)) t1 y yv (N R t2 z zv t3)) =>
BalanceableHelperL True t1 y yv (N B t2 z zv t3) where
type BalL' True t1 y yv (N B t2 z zv t3)
= Balance t1 y yv (N R t2 z zv t3)
balLR' (Node left1 v1 (Node left2 v2 right2)) =
balanceR @t1 @y @yv @(N R t2 z zv t3) (Node left1 v1 (Node left2 v2 right2))
balLV' v = balanceV @t1 @y @yv @(N R t2 z zv t3) (case v of
LookLeft l -> LookLeft l
Here x -> Here x
LookRight r -> LookRight (case r of
LookLeft l' -> LookLeft l'
Here x' -> Here x'
LookRight r' -> LookRight r'))
instance (BalanceableHelper (ShouldBalance t3 (N R l k kv r)) t3 z zv (N R l k kv r)) =>
BalanceableHelperL True t1 y yv (N R (N B t2 u uv t3) z zv (N B l k kv r)) where
type BalL' True t1 y yv (N R (N B t2 u uv t3) z zv (N B l k kv r)) =
N R (N B t1 y yv t2) u uv (Balance t3 z zv (N R l k kv r))
balLR' (Node left1 v1 (Node (Node left2 v2 right2) vx (Node left3 v3 right3))) =
Node (Node left1 v1 left2) v2 (balanceR @t3 @z @zv @(N R l k kv r) (Node right2 vx (Node left3 v3 right3)))
balLV' v = case v of LookLeft left1 -> LookLeft (LookLeft left1)
Here v1 -> LookLeft (Here v1)
LookRight (LookLeft (LookLeft left2)) -> LookLeft (LookRight left2)
LookRight (LookLeft (Here v2)) -> Here v2
LookRight (LookLeft (LookRight right2)) -> LookRight (balanceV @t3 @z @zv @(N R l k kv r) (LookLeft right2))
LookRight (Here vx) -> LookRight (balanceV @t3 @z @zv @(N R l k kv r) (Here vx))
LookRight (LookRight rr) -> LookRight (balanceV @t3 @z @zv @(N R l k kv r) (LookRight (case rr of
LookLeft left3 -> LookLeft left3
Here v3 -> Here v3
LookRight right3 -> LookRight right3)))
type family DiscriminateBalR (l :: Map k v) (r :: Map k v) :: Bool where
DiscriminateBalR _ (N R _ _ _ _) = False
DiscriminateBalR _ _ = True
class BalanceableR (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
type BalR l k v r :: Map Symbol Type
balRR :: Record f (N color l k v r) -> Record f (BalR l k v r)
balRV :: Variant f (N color l k v r) -> Variant f (BalR l k v r)
class BalanceableHelperR (b :: Bool) (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
type BalR' b l k v r :: Map Symbol Type
balRR' :: Record f (N color l k v r) -> Record f (BalR' b l k v r)
balRV' :: Variant f (N color l k v r) -> Variant f (BalR' b l k v r)
instance (DiscriminateBalR l r ~ b, BalanceableHelperR b l k v r) => BalanceableR l k v r where
type BalR l k v r = BalR' (DiscriminateBalR l r) l k v r
balRR = balRR' @b @l @k @v @r
balRV = balRV' @b @l @k @v @r
instance BalanceableHelperR False right2 k2 v2 (N R left1 k1 v1 right1) where
type BalR' False right2 k2 v2 (N R left1 k1 v1 right1) =
(N R right2 k2 v2 (N B left1 k1 v1 right1))
balRR' (Node right v (Node left' v' right')) = Node right v (Node left' v' right')
balRV' v = case v of LookLeft x -> LookLeft x
Here x -> Here x
LookRight x -> LookRight (case x of LookLeft y -> LookLeft y
Here y -> Here y
LookRight y -> LookRight y)
instance (BalanceableHelper (ShouldBalance (N R t2 z zv t3) t1) (N R t2 z zv t3) y yv t1) =>
BalanceableHelperR True (N B t2 z zv t3) y yv t1 where
type BalR' True (N B t2 z zv t3) y yv t1
= Balance (N R t2 z zv t3) y yv t1
balRR' (Node (Node left1 v1 right1) v2 right2) = balanceR @(N R t2 z zv t3) @y @yv @t1
(Node (Node left1 v1 right1) v2 right2)
balRV' v = balanceV @(N R t2 z zv t3) @y @yv @t1 (case v of
LookLeft l -> LookLeft (case l of
LookLeft l' -> LookLeft l'
Here x' -> Here x'
LookRight r' -> LookRight r')
Here x -> Here x
LookRight r -> LookRight r)
instance (BalanceableHelper (ShouldBalance (N R t2 u uv t3) l) (N R t2 u uv t3) z zv l) =>
BalanceableHelperR True (N R (N B t2 u uv t3) z zv (N B l k kv r)) y yv t1 where
type BalR' True (N R (N B t2 u uv t3) z zv (N B l k kv r)) y yv t1 =
N R (Balance (N R t2 u uv t3) z zv l) k kv (N B r y yv t1)
balRR' (Node (Node (Node left2 v2 right2) vx (Node left3 v3 right3)) v1 left1) =
Node (balanceR @(N R t2 u uv t3) @z @zv @l (Node (Node left2 v2 right2) vx left3)) v3 (Node right3 v1 left1)
balRV' v = case v of
LookLeft (LookLeft rr) -> LookLeft (balanceV @(N R t2 u uv t3) @z @zv @l (LookLeft (case rr of
LookLeft t2 -> LookLeft t2
Here uv -> Here uv
LookRight t3 -> LookRight t3)))
LookLeft (Here zv) -> LookLeft (balanceV @(N R t2 u uv t3) @z @zv @l (Here zv))
LookLeft (LookRight (LookLeft l)) -> LookLeft (balanceV @(N R t2 u uv t3) @z @zv @l (LookRight l))
LookLeft (LookRight (Here kv)) -> Here kv
LookLeft (LookRight (LookRight r)) -> LookRight (LookLeft r)
Here yv -> LookRight (Here yv)
LookRight t1 -> LookRight (LookRight t1)
class Fuseable (l :: Map Symbol Type) (r :: Map Symbol Type) where
type Fuse l r :: Map Symbol Type
fuseRecord :: Record f l -> Record f r -> Record f (Fuse l r)
fuseVariant :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r)
instance Fuseable E E where
type Fuse E E = E
fuseRecord _ _ = unit
fuseVariant v = case v of
instance Fuseable E (N color left k v right) where
type Fuse E (N color left k v right) = N color left k v right
fuseRecord _ r = r
fuseVariant e = case e of
Right v -> v
instance Fuseable (N color left k v right) E where
type Fuse (N color left k v right) E = N color left k v right
fuseRecord r _ = r
fuseVariant e = case e of
Left v -> v
instance Fuseable (N B left1 k1 v1 right1) left2 => Fuseable (N B left1 k1 v1 right1) (N R left2 k2 v2 right2) where
type Fuse (N B left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R (Fuse (N B left1 k1 v1 right1) left2) k2 v2 right2
fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node (fuseRecord @(N B left1 k1 v1 right1) (Node left1 v1 right1) left2) v2 right2
fuseVariant e = case e of
Left l -> case l of
LookLeft left1 -> LookLeft (fuseVariant @(N B left1 k1 v1 right1) @left2 (Left (LookLeft left1)))
Here v1 -> LookLeft (fuseVariant @(N B left1 k1 v1 right1) @left2 (Left (Here v1)))
LookRight right1 -> LookLeft (fuseVariant @(N B left1 k1 v1 right1) @left2 (Left (LookRight right1)))
Right r -> case r of
LookLeft left2 -> LookLeft (fuseVariant @(N B left1 k1 v1 right1) @left2 (Right left2))
Here v2 -> Here v2
LookRight right2 -> LookRight right2
instance Fuseable right1 (N B left2 k2 v2 right2) => Fuseable (N R left1 k1 v1 right1) (N B left2 k2 v2 right2) where
type Fuse (N R left1 k1 v1 right1) (N B left2 k2 v2 right2) = N R left1 k1 v1 (Fuse right1 (N B left2 k2 v2 right2))
fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node left1 v1 (fuseRecord @_ @(N B left2 k2 v2 right2) right1 (Node left2 v2 right2))
fuseVariant e = case e of
Left l -> case l of
LookLeft left1 -> LookLeft left1
Here v1 -> Here v1
LookRight right1 -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Left right1))
Right r -> case r of
LookLeft left2 -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Right (LookLeft left2)))
Here v2 -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Right (Here v2)))
LookRight right2 -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Right (LookRight right2)))
instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper1 fused (N R left1 k1 v1 right1) (N R left2 k2 v2 right2)) => Fuseable (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where
type Fuse (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = Fuse1 (Fuse right1 left2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2)
fuseRecord = fuseRecord1 @(Fuse right1 left2)
fuseVariant = fuseVariant1 @(Fuse right1 left2)
class FuseableHelper1 (fused :: Map Symbol Type) (l :: Map Symbol Type) (r :: Map Symbol Type) where
type Fuse1 fused l r :: Map Symbol Type
fuseRecord1 :: Record f l -> Record f r -> Record f (Fuse l r)
fuseVariant1 :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r)
instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z zv s2) => FuseableHelper1 (N R s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where
type Fuse1 (N R s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R (N R left1 k1 v1 s1) z zv (N R s2 k2 v2 right2)
fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) =
case fuseRecord right1 left2 of
Node s1 zv s2 -> Node (Node left1 v1 s1) zv (Node s2 v2 right2)
fuseVariant1 e =
case e of
Left l -> case l of
LookLeft left1 -> LookLeft (LookLeft left1)
Here v1 -> LookLeft (Here v1)
LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
LookLeft s1 -> LookLeft (LookRight s1)
Here zv -> Here zv
LookRight s2 -> LookRight (LookLeft s2)
Right r -> case r of
LookLeft left2 -> case fuseVariant @right1 @left2 (Right left2) of
LookLeft s1 -> LookLeft (LookRight s1)
Here zv -> Here zv
LookRight s2 -> LookRight (LookLeft s2)
Here v2 -> LookRight (Here v2)
LookRight right2 -> LookRight (LookRight right2)
instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z zv s2) => FuseableHelper1 (N B s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where
type Fuse1 (N B s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R left1 k1 v1 (N R (N B s1 z zv s2) k2 v2 right2)
fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) =
case fuseRecord right1 left2 of
Node s1 zv s2 -> Node left1 v1 (Node (Node s1 zv s2) v2 right2)
fuseVariant1 e =
case e of
Left l -> case l of
LookLeft left1 -> LookLeft left1
Here v1 -> Here v1
LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
LookLeft s1 -> LookRight (LookLeft (LookLeft s1))
Here zv -> LookRight (LookLeft (Here zv))
LookRight s2 -> LookRight (LookLeft (LookRight s2))
Right r -> case r of
LookLeft left2 -> case fuseVariant @right1 @left2 (Right left2) of
LookLeft s1 -> LookRight (LookLeft (LookLeft s1))
Here zv -> LookRight (LookLeft (Here zv))
LookRight s2 -> LookRight (LookLeft (LookRight s2))
Here v2 -> LookRight (Here v2)
LookRight right2 -> LookRight (LookRight right2)
instance FuseableHelper1 E (N R left1 k1 v1 E) (N R E k2 v2 right2) where
type Fuse1 E (N R left1 k1 v1 E) (N R E k2 v2 right2) = N R left1 k1 v1 (N R E k2 v2 right2)
fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) = Node left1 v1 (Node Empty v2 right2)
fuseVariant1 e =
case e of
Left l -> case l of
LookLeft left1 -> LookLeft left1
Here v1 -> Here v1
Right r -> case r of
Here v2 -> LookRight (Here v2)
LookRight right2 -> LookRight (LookRight right2)
instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper2 fused (N B left1 k1 v1 right1) (N B left2 k2 v2 right2)) => Fuseable (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where
type Fuse (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = Fuse2 (Fuse right1 left2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2)
fuseRecord = fuseRecord2 @(Fuse right1 left2)
fuseVariant = fuseVariant2 @(Fuse right1 left2)
class FuseableHelper2 (fused :: Map Symbol Type) (l :: Map Symbol Type) (r :: Map Symbol Type) where
type Fuse2 fused l r :: Map Symbol Type
fuseRecord2 :: Record f l -> Record f r -> Record f (Fuse l r)
fuseVariant2 :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r)
instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z zv s2) => FuseableHelper2 (N R s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where
type Fuse2 (N R s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = N R (N B left1 k1 v1 s1) z zv (N B s2 k2 v2 right2)
fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) =
case fuseRecord right1 left2 of
Node s1 zv s2 -> Node (Node left1 v1 s1) zv (Node s2 v2 right2)
fuseVariant2 e =
case e of
Left l -> case l of
LookLeft left1 -> LookLeft (LookLeft left1)
Here v1 -> LookLeft (Here v1)
LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
LookLeft s1 -> LookLeft (LookRight s1)
Here zv -> Here zv
LookRight s2 -> LookRight (LookLeft s2)
Right r -> case r of
LookLeft left2 -> case fuseVariant @right1 @left2 (Right left2) of
LookLeft s1 -> LookLeft (LookRight s1)
Here zv -> Here zv
LookRight s2 -> LookRight (LookLeft s2)
Here v2 -> LookRight (Here v2)
LookRight right2 -> LookRight (LookRight right2)
instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z zv s2, BalanceableL left1 k1 v1 (N B (N B s1 z zv s2) k2 v2 right2)) => FuseableHelper2 (N B s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where
type Fuse2 (N B s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = BalL left1 k1 v1 (N B (N B s1 z zv s2) k2 v2 right2)
fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) =
case fuseRecord @right1 @left2 right1 left2 of
Node s1 zv s2 -> balLR @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (Node left1 v1 (Node (Node s1 zv s2) v2 right2))
fuseVariant2 e = balLV @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (case e of
Left l -> case l of
LookLeft left1 -> LookLeft left1
Here v1 -> Here v1
LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
LookLeft s1 -> LookRight (LookLeft (LookLeft s1))
Here zv -> LookRight (LookLeft (Here zv))
LookRight s2 -> LookRight (LookLeft (LookRight s2))
Right r -> case r of
LookLeft left2 -> case fuseVariant @right1 @left2 (Right left2) of
LookLeft s1 -> LookRight (LookLeft (LookLeft s1))
Here zv -> LookRight (LookLeft (Here zv))
LookRight s2 -> LookRight (LookLeft (LookRight s2))
Here v2 -> LookRight (Here v2)
LookRight right2 -> LookRight (LookRight right2))
instance (BalanceableL left1 k1 v1 (N B E k2 v2 right2)) => FuseableHelper2 E (N B left1 k1 v1 E) (N B E k2 v2 right2) where
type Fuse2 E (N B left1 k1 v1 E) (N B E k2 v2 right2) = BalL left1 k1 v1 (N B E k2 v2 right2)
fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) =
balLR @left1 @k1 @v1 @(N B E k2 v2 right2) (Node left1 v1 (Node Empty v2 right2))
fuseVariant2 e = balLV @left1 @k1 @v1 @(N B E k2 v2 right2) (case e of
Left l -> case l of
LookLeft left1 -> LookLeft left1
Here v1 -> Here v1
Right r -> case r of
Here v2 -> LookRight (Here v2)
LookRight right2 -> LookRight (LookRight right2))
class Delable (k :: Symbol) (v :: Type) (t :: Map Symbol Type) where
type Del k v t :: Map Symbol Type
del :: Record f t -> Record f (Del k v t)
win :: Variant f t -> Either (Variant f (Del k v t)) (f v)
class DelableL (k :: Symbol) (v :: Type) (l :: Map Symbol Type) (kx :: Symbol) (vx :: Type) (r :: Map Symbol Type) where
type DelL k v l kx vx r :: Map Symbol Type
delL :: Record f (N color l kx vx r) -> Record f (DelL k v l kx vx r)
winL :: Variant f (N color l kx vx r) -> Either (Variant f (DelL k v l kx vx r)) (f v)
instance (Delable k v (N B leftz kz vz rightz), BalanceableL (Del k v (N B leftz kz vz rightz)) kx vx right)
=> DelableL k v (N B leftz kz vz rightz) kx vx right where
type DelL k v (N B leftz kz vz rightz) kx vx right = BalL (Del k v (N B leftz kz vz rightz)) kx vx right
delL (Node left vx right) = balLR @(Del k v (N B leftz kz vz rightz)) @kx @vx @right (Node (del @k @v left) vx right)
winL v = first (balLV @(Del k v (N B leftz kz vz rightz)) @kx @vx @right) (case v of
LookLeft l -> first LookLeft (win @k @v l)
Here vx -> Left $ Here vx
LookRight r -> Left $ LookRight r)
instance (Delable k v (N R leftz kz vz rightz)) => DelableL k v (N R leftz kz vz rightz) kx vx right where
type DelL k v (N R leftz kz vz rightz) kx vx right = N R (Del k v (N R leftz kz vz rightz)) kx vx right
delL (Node left vx right) = Node (del @k @v left) vx right
winL v = case v of
LookLeft l -> first LookLeft (win @k @v l)
Here vx -> Left (Here vx)
LookRight r -> Left (LookRight r)
instance DelableL k v E kx vx right where
type DelL k v E kx vx right = N R E kx vx right
delL (Node left vx right) = Node Empty vx right
winL v = case v of
Here vx -> Left (Here vx)
LookRight r -> Left (LookRight r)
class DelableR (k :: Symbol) (v :: Type) (l :: Map Symbol Type) (kx :: Symbol) (vx :: Type) (r :: Map Symbol Type) where
type DelR k v l kx vx r :: Map Symbol Type
delR :: Record f (N color l kx vx r) -> Record f (DelR k v l kx vx r)
winR :: Variant f (N color l kx vx r) -> Either (Variant f (DelR k v l kx vx r)) (f v)
instance (Delable k v (N B leftz kz vz rightz), BalanceableR left kx vx (Del k v (N B leftz kz vz rightz))) => DelableR k v left kx vx (N B leftz kz vz rightz) where
type DelR k v left kx vx (N B leftz kz vz rightz) = BalR left kx vx (Del k v (N B leftz kz vz rightz))
delR (Node left vx right) = balRR @left @kx @vx @(Del k v (N B leftz kz vz rightz)) (Node left vx (del @k @v right))
winR v = first (balRV @left @kx @vx @(Del k v (N B leftz kz vz rightz))) (case v of
LookLeft l -> Left $ LookLeft l
Here vx -> Left $ Here vx
LookRight r -> first LookRight (win @k @v r))
instance (Delable k v (N R leftz kz vz rightz)) => DelableR k v left kx vx (N R leftz kz vz rightz) where
type DelR k v left kx vx (N R leftz kz vz rightz) = N R left kx vx (Del k v (N R leftz kz vz rightz))
delR (Node left vx right) = Node left vx (del @k @v right)
winR v = case v of
LookLeft l -> Left (LookLeft l)
Here vx -> Left (Here vx)
LookRight r -> first LookRight (win @k @v r)
instance DelableR k v left kx vx E where
type DelR k v left kx vx E = N R left kx vx E
delR (Node left vx right) = Node left vx Empty
winR v = case v of
LookLeft l -> Left (LookLeft l)
Here vx -> Left (Here vx)
instance Delable k v E where
type Del k v E = E
del _ = unit
win = impossible
instance (CmpSymbol kx k ~ ordering, DelableHelper ordering k v left kx vx right) => Delable k v (N color left kx vx right) where
type Del k v (N color left kx vx right) = Del' (CmpSymbol kx k) k v left kx vx right
del = del' @(CmpSymbol kx k) @k @v @left @kx @vx @right
win = win' @(CmpSymbol kx k) @k @v @left @kx @vx @right
class DelableHelper (ordering :: Ordering) (k :: Symbol) (v :: Type) (l :: Map Symbol Type) (kx :: Symbol) (vx :: Type) (r :: Map Symbol Type) where
type Del' ordering k v l kx vx r :: Map Symbol Type
del' :: Record f (N color l kx vx r) -> Record f (Del' ordering k v l kx vx r)
win' :: Variant f (N color l kx vx r) -> Either (Variant f (Del' ordering k v l kx vx r)) (f v)
instance DelableL k v left kx vx right => DelableHelper GT k v left kx vx right where
type Del' GT k v left kx vx right = DelL k v left kx vx right
del' = delL @k @v @left @kx @vx @right
win' = winL @k @v @left @kx @vx @right
instance Fuseable left right => DelableHelper EQ k v left k v right where
type Del' EQ k v left k v right = Fuse left right
del' (Node left _ right) = fuseRecord @left @right left right
win' v = case v of
LookLeft l -> Left $ fuseVariant @left @right (Left l)
Here v -> Right v
LookRight r -> Left $ fuseVariant @left @right (Right r)
instance DelableR k v left kx vx right => DelableHelper LT k v left kx vx right where
type Del' LT k v left kx vx right = DelR k v left kx vx right
del' = delR @k @v @left @kx @vx @right
win' = winR @k @v @left @kx @vx @right
class Deletable (k :: Symbol) (v :: Type) (t :: Map Symbol Type) where
type Delete k v t :: Map Symbol Type
delete :: Record f t -> Record f (Delete k v t)
winnow :: Variant f t -> Either (Variant f (Delete k v t)) (f v)
instance (Delable k v t, CanMakeBlack (Del k v t)) => Deletable k v t where
type Delete k v t = MakeBlack (Del k v t)
delete r = makeBlackR (del @k @v r)
winnow v = first makeBlackV (win @k @v v)
winnowI :: forall k v t . Deletable k v t => Variant I t -> Either (Variant I (Delete k v t)) v
winnowI = fmap unI . winnow @k @v @t