red-black-record 2.1.0.3 → 2.1.1.0
raw patch · 11 files changed
+3743/−3343 lines, 11 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ Data.RBR: Comp :: f (g p) -> (:.:)
+ Data.RBR: VariantInjection :: (f v -> Variant f t) -> VariantInjection
+ Data.RBR: [runVariantInjection] :: VariantInjection -> f v -> Variant f t
+ Data.RBR: class (kc k, vc v) => KeyValueConstraints (kc :: Symbol -> Constraint) (vc :: q -> Constraint) (k :: Symbol) (v :: q)
+ Data.RBR: class Maplike (t :: Map Symbol Type)
+ Data.RBR: class (vc v) => ValueConstraint (vc :: q -> Constraint) (k :: Symbol) (v :: q)
+ Data.RBR: collapse'_Record :: (Maplike t, Monoid a) => Record (K a) t -> a
+ Data.RBR: collapse_Variant :: Maplike t => Variant (K a) t -> a
+ Data.RBR: cpure'_Record :: forall c t f. KeysValuesAll (KeyValueConstraints KnownSymbol c) t => Proxy c -> (forall v. c v => String -> f v) -> Record f t
+ Data.RBR: eliminate_Variant :: Maplike t => Record (Case f r) t -> Variant f t -> r
+ Data.RBR: infixr 7 :.:
+ Data.RBR: injections_Variant :: Maplike t => Record (VariantInjection f t) t
+ Data.RBR: liftA2_Record :: Maplike t => (forall a. f a -> g a -> h a) -> Record f t -> Record g t -> Record h t
+ Data.RBR: liftA2_Variant :: Maplike t => (forall a. f a -> g a -> h a) -> Record f t -> Variant g t -> Variant h t
+ Data.RBR: liftA_Record :: Maplike t => (forall a. f a -> g a) -> Record f t -> Record g t
+ Data.RBR: liftA_Variant :: Maplike t => (forall a. f a -> g a) -> Variant f t -> Variant g t
+ Data.RBR: newtype VariantInjection (f :: q -> Type) (t :: Map Symbol q) (v :: q)
+ Data.RBR: newtype (:.:) (f :: l -> Type) (g :: k -> l) (p :: k) :: forall l k. () => l -> Type -> k -> l -> k -> Type
+ Data.RBR: prettyShow_Record :: forall t f. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) => (forall x. Show x => f x -> String) -> Record f t -> String
+ Data.RBR: prettyShow_RecordI :: forall t. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) => Record I t -> String
+ Data.RBR: prettyShow_Variant :: forall t flat f. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) => (forall x. Show x => f x -> String) -> Variant f t -> String
+ Data.RBR: prettyShow_VariantI :: forall t flat. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) => Variant I t -> String
+ Data.RBR: pure_Record :: Maplike t => (forall v. f v) -> Record f t
+ Data.RBR: sequence'_Record :: (Maplike t, Applicative f) => Record (f :.: g) t -> f (Record g t)
+ Data.RBR: sequence_Record :: (Maplike t, Applicative f) => Record f t -> f (Record I t)
+ Data.RBR: type IsRecordType (r :: Type) (t :: Map Symbol Type) = (Generic r, ToRecord r, RecordCode r ~ t, FromRecord r)
+ Data.RBR: type IsVariantType (v :: Type) (t :: Map Symbol Type) = (Generic v, ToVariant v, VariantCode v ~ t, FromVariant v)
+ Data.RBR.Internal: VariantInjection :: (f v -> Variant f t) -> VariantInjection
+ Data.RBR.Internal: [runVariantInjection] :: VariantInjection -> f v -> Variant f t
+ Data.RBR.Internal: class (kc k, vc v) => KeyValueConstraints (kc :: Symbol -> Constraint) (vc :: q -> Constraint) (k :: Symbol) (v :: q)
+ Data.RBR.Internal: class Maplike (t :: Map Symbol Type)
+ Data.RBR.Internal: class (vc v) => ValueConstraint (vc :: q -> Constraint) (k :: Symbol) (v :: q)
+ Data.RBR.Internal: collapse'_Record :: (Maplike t, Monoid a) => Record (K a) t -> a
+ Data.RBR.Internal: collapse_Variant :: Maplike t => Variant (K a) t -> a
+ Data.RBR.Internal: cpure'_Record :: forall c t f. KeysValuesAll (KeyValueConstraints KnownSymbol c) t => Proxy c -> (forall v. c v => String -> f v) -> Record f t
+ Data.RBR.Internal: eliminate_Variant :: Maplike t => Record (Case f r) t -> Variant f t -> r
+ Data.RBR.Internal: injections_Variant :: Maplike t => Record (VariantInjection f t) t
+ Data.RBR.Internal: instance (Data.RBR.Internal.Maplike left, Data.RBR.Internal.Maplike right) => Data.RBR.Internal.Maplike ('Data.RBR.Internal.N color left k v right)
+ Data.RBR.Internal: instance Data.RBR.Internal.Maplike 'Data.RBR.Internal.E
+ Data.RBR.Internal: instance forall q (kc :: GHC.Types.Symbol -> GHC.Types.Constraint) (k :: GHC.Types.Symbol) (vc :: q -> GHC.Types.Constraint) (v :: q). (kc k, vc v) => Data.RBR.Internal.KeyValueConstraints kc vc k v
+ Data.RBR.Internal: instance forall q (vc :: q -> GHC.Types.Constraint) (v :: q) (k :: GHC.Types.Symbol). vc v => Data.RBR.Internal.ValueConstraint vc k v
+ Data.RBR.Internal: liftA2_Record :: Maplike t => (forall a. f a -> g a -> h a) -> Record f t -> Record g t -> Record h t
+ Data.RBR.Internal: liftA2_Variant :: Maplike t => (forall a. f a -> g a -> h a) -> Record f t -> Variant g t -> Variant h t
+ Data.RBR.Internal: liftA_Record :: Maplike t => (forall a. f a -> g a) -> Record f t -> Record g t
+ Data.RBR.Internal: liftA_Variant :: Maplike t => (forall a. f a -> g a) -> Variant f t -> Variant g t
+ Data.RBR.Internal: newtype VariantInjection (f :: q -> Type) (t :: Map Symbol q) (v :: q)
+ Data.RBR.Internal: prettyShow_Record :: forall t f. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) => (forall x. Show x => f x -> String) -> Record f t -> String
+ Data.RBR.Internal: prettyShow_RecordI :: forall t. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) => Record I t -> String
+ Data.RBR.Internal: prettyShow_Variant :: forall t flat f. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) => (forall x. Show x => f x -> String) -> Variant f t -> String
+ Data.RBR.Internal: prettyShow_VariantI :: forall t flat. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) => Variant I t -> String
+ Data.RBR.Internal: pure_Record :: Maplike t => (forall v. f v) -> Record f t
+ Data.RBR.Internal: sequence'_Record :: (Maplike t, Applicative f) => Record (f :.: g) t -> f (Record g t)
+ Data.RBR.Internal: sequence_Record :: (Maplike t, Applicative f) => Record f t -> f (Record I t)
+ Data.RBR.Internal: type IsRecordType (r :: Type) (t :: Map Symbol Type) = (Generic r, ToRecord r, RecordCode r ~ t, FromRecord r)
+ Data.RBR.Internal: type IsVariantType (v :: Type) (t :: Map Symbol Type) = (Generic v, ToVariant v, VariantCode v ~ t, FromVariant v)
+ Data.RBR.Subset: 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)
+ Data.RBR.Subset: eliminateSubset :: forall subset whole f r. (Maplike subset, Maplike whole, Subset subset whole) => Record (Case f r) whole -> Variant f subset -> r
+ Data.RBR.Subset: fieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) => Record f whole -> (Record f subset -> Record f whole, Record f subset)
+ Data.RBR.Subset: fromRecordSuperset :: forall r t whole. (IsRecordType r t, Maplike t, Subset t whole) => Record I whole -> r
+ Data.RBR.Subset: getFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) => Record f whole -> Record f subset
+ Data.RBR.Subset: injectSubset :: forall subset whole f. (Maplike subset, Maplike whole, Subset subset whole) => Variant f subset -> Variant f whole
+ Data.RBR.Subset: matchSubset :: forall subset whole f. (Maplike subset, Maplike whole, Subset subset whole) => Variant f whole -> Maybe (Variant f subset)
+ Data.RBR.Subset: modifyFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) => (Record f subset -> Record f subset) -> Record f whole -> Record f whole
+ Data.RBR.Subset: projectSubset :: forall subset whole f. (Maplike subset, Subset subset whole) => Record f whole -> Record f subset
+ Data.RBR.Subset: setFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) => Record f subset -> Record f whole -> Record f whole
+ Data.RBR.Subset: type Subset (subset :: Map Symbol q) (whole :: Map Symbol q) = KeysValuesAll (PresentIn whole) subset
Files
- CHANGELOG.md +62/−51
- LICENSE +30/−30
- README.md +3/−4
- lib-demoted/Data/RBR/Demoted.hs +215/−215
- lib/Data/RBR.hs +172/−158
- lib/Data/RBR/Examples.hs +346/−349
- lib/Data/RBR/Internal.hs +2065/−1897
- lib/Data/RBR/Subset.hs +208/−0
- red-black-record.cabal +78/−77
- tests/doctests.hs +8/−7
- tests/tests.hs +556/−555
CHANGELOG.md view
@@ -1,51 +1,62 @@-# Revision history for red-black-record - -## 2.1.0.0 - -- Made the type-level map poly-kinded in the values, as there wasn't a real - reason to force them to the Type kind. -- Removed deprecated EmptyMap (use Empty instead). - -## 2.0.4.0 - -- Compatibility with sop-core 0.5.0.0. -- Contravariant intance for Case newtype. - -## 2.0.3.0 - -- Issue #7: FromVariant & ToVariant instances for sum types with branches with - no arguments. - -## 2.0.2.2 - -- Improved compilation times for type-level deletion. - -## 2.0.0.0 - -- BREAKING CHANGES - - The constructors for the type-level map are now hidden. - - The name of the type-level map has changed from RBT to Map, to - de-emphasize implementation details. - -- Added the "Deletable" typeclass with de "delete" and "winnow" methods. - -- Solved bugs with coloring/balancing, added new tests. - -- Data.RBR.Internal is still exported, but it doesn't appear in the Haddocks. - It appears that Haddock doesn't play well with reexported-modules sections in - Cabal. - -## 1.1.0.0 - -- Field and Branch type families to help speed up type-level computations. - - Apparently, having identical invocations of a "costly to compute" type family - in a signature slowed things down. - -## 1.0.0.2 - -- Improved compilation times for getters by refactoring `KeyHelper`. - -## 1.0.0.0 - -- First version. Released on an unsuspecting world. +# Revision history for red-black-record++## 2.1.1.0+- Added NP-like functions for working on Records, like sequence_Record.+ They are memebers of the Maplike typeclass.+- Deprecated the -Subset functions from Data.RBR and created a new module+ Data.RBR.Subset with new versions. To avoid collisions, Data.RBR.Subset+ should be imported qualified.+- Deprecated a number of other functions that had Productlike / Sumlike+ constraints, added new functions with Maplike constraints.+- Added IsRecordType, IsVariantType.+- Added KeyValueConstraints, ValueConstraint.++## 2.1.0.0++- Made the type-level map poly-kinded in the values, as there wasn't a real+ reason to force them to the Type kind. +- Removed deprecated EmptyMap (use Empty instead).++## 2.0.4.0++- Compatibility with sop-core 0.5.0.0.+- Contravariant intance for Case newtype.++## 2.0.3.0++- Issue #7: FromVariant & ToVariant instances for sum types with branches with+ no arguments.++## 2.0.2.2++- Improved compilation times for type-level deletion.++## 2.0.0.0++- BREAKING CHANGES+ - The constructors for the type-level map are now hidden.+ - The name of the type-level map has changed from RBT to Map, to+ de-emphasize implementation details. ++- Added the "Deletable" typeclass with de "delete" and "winnow" methods.++- Solved bugs with coloring/balancing, added new tests.++- Data.RBR.Internal is still exported, but it doesn't appear in the Haddocks.+ It appears that Haddock doesn't play well with reexported-modules sections in+ Cabal.++## 1.1.0.0++- Field and Branch type families to help speed up type-level computations. ++ Apparently, having identical invocations of a "costly to compute" type family+ in a signature slowed things down.++## 1.0.0.2++- Improved compilation times for getters by refactoring `KeyHelper`.++## 1.0.0.0++- First version. Released on an unsuspecting world.
LICENSE view
@@ -1,30 +1,30 @@-Copyright (c) 2018, Daniel Diaz - -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - - * Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - - * Redistributions in binary form must reproduce the above - copyright notice, this list of conditions and the following - disclaimer in the documentation and/or other materials provided - with the distribution. - - * Neither the name of Daniel Diaz nor the names of other - contributors may be used to endorse or promote products derived - from this software without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT -OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, -SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT -LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +Copyright (c) 2018, Daniel Diaz++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Daniel Diaz nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
README.md view
@@ -21,10 +21,9 @@ and variants are isomorphic to [n-ary unlabeled sums](http://hackage.haskell.org/package/sop-core-0.4.0.0/docs/Data-SOP.html#t:NS). The [sop-core](http://hackage.haskell.org/package/sop-core) library provides-such unlabeled types, along with a rich API for manipulating them. Instead of-reinventing the wheel, red-black-record defines conversion functions to-facilitate working in the "unlabeled" world and then coming back to records and-variants.+such unlabeled types, along with a rich API for manipulating them.+red-black-record defines conversion functions to facilitate working in the+"unlabeled" world, if needed, and then coming back to records and variants. There is another world towards which bridges must be built: the everyday Haskell world of conventional records and sums. In fact, one of the motivations
lib-demoted/Data/RBR/Demoted.hs view
@@ -1,215 +1,215 @@-{-# 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.Demoted where - -import Data.RBR.Internal - -import Data.Proxy -import Data.Kind -import Data.Typeable -import GHC.TypeLits - -emptyMap :: Map String TypeRep -emptyMap = E - -class DemotableColor (c :: Color) where - demoteColor :: Proxy c -> Color - -instance DemotableColor R where - demoteColor _ = R - -instance DemotableColor B where - demoteColor _ = B - -class DemotableMap (t :: Map Symbol Type) where - demoteMap :: Proxy t -> Map String TypeRep - -instance DemotableMap E where - demoteMap _ = E - -instance (DemotableColor c, - KnownSymbol s, - Typeable ty, - DemotableMap l, - DemotableMap r) - => DemotableMap (N c l s ty r) where - demoteMap _ = N (demoteColor (Proxy @c)) - (demoteMap (Proxy @l)) - (symbolVal (Proxy @s)) - (typeRep (Proxy @ty)) - (demoteMap (Proxy @r)) - -t_insert :: Ord a => a -> v -> Map a v -> Map a v -t_insert x val s = - N B a v z b - where - N _ a v z b = ins s - ins E = N R E x val E - ins s@(N B a y val' b) - | x<y = t_balance (ins a) y val' b - | x>y = t_balance a y val' (ins b) - | otherwise = s - ins s@(N R a y val' b) - | x<y = N R (ins a) y val' b - | x>y = N R a y val' (ins b) - | otherwise = s - -t_balance :: Map a v -> a -> v -> Map a v -> Map a v -t_balance (N R a x xv b) y yv (N R c z zv d) = N R (N B a x xv b) y yv (N B c z zv d) -t_balance (N R (N R a x xv b) y yv c) z zv d = N R (N B a x xv b) y yv (N B c z zv d) -t_balance (N R a x xv (N R b y yv c)) z zv d = N R (N B a x xv b) y yv (N B c z zv d) -t_balance a x xv (N R b y yv (N R c z zv d)) = N R (N B a x xv b) y yv (N B c z zv d) -t_balance a x xv (N R (N R b y yv c) z zv d) = N R (N B a x xv b) y yv (N B c z zv d) -t_balance a x xv b = N B a x xv b - - -t_delete :: Ord a => a -> Map a v -> Map a v -t_delete x t = - case del t of {N _ a y yv b -> N B a y yv b; _ -> E} - where - del E = E - del (N _ a y yv b) - | x<y = delformLeft a y yv b - | x>y = delformRight a y yv b - | otherwise = t_app a b - delformLeft a@(N B _ _ _ _) y yv b = t_balleft (del a) y yv b - delformLeft a y yv b = N R (del a) y yv b - - delformRight a y yv b@(N B _ _ _ _) = t_balright a y yv (del b) - delformRight a y yv b = N R a y yv (del b) - -t_balleft :: Map a v -> a -> v -> Map a v -> Map a v -t_balleft (N R a x xv b) y yv c = N R (N B a x xv b) y yv c -t_balleft bl x xv (N B a y yv b) = t_balance bl x xv (N R a y yv b) -t_balleft bl x xv (N R (N B a y yv b) z zv c) = N R (N B bl x xv a) y yv (t_balance b z zv (t_sub1 c)) - -t_balright :: Map a v -> a -> v -> Map a v -> Map a v -t_balright a x xv (N R b y yv c) = N R a x xv (N B b y yv c) -t_balright (N B a x xv b) y yv bl = t_balance (N R a x xv b) y yv bl -t_balright (N R a x xv (N B b y yv c)) z zv bl = N R (t_balance (t_sub1 a) x xv b) y yv (N B c z zv bl) - -t_sub1 :: Map a v -> Map a v -t_sub1 (N B a x xv b) = N R a x xv b -t_sub1 _ = error "invariance violation" - -t_app :: Map a v -> Map a v -> Map a v -t_app E x = x -t_app x E = x -t_app (N R a x xv b) (N R c y yv d) = - case t_app b c of - N R b' z zv c' -> N R (N R a x xv b') z zv (N R c' y yv d) - bc -> N R a x xv (N R bc y yv d) -t_app (N B a x xv b) (N B c y yv d) = - case t_app b c of - N R b' z zv c' -> N R (N B a x xv b') z zv (N B c' y yv d) - bc -> t_balleft a x xv (N B bc y yv d) -t_app a (N R b x xv c) = N R (t_app a b) x xv c -t_app (N R a x xv b) c = N R a x xv (t_app b c) - --- The original term-level code, taken from: --- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html --- --- {- Version 1, 'untyped' -} --- data Color = R | B deriving Show --- data RB a = E | T Color (RB a) a (RB a) deriving Show --- --- {- Insertion and membership test as by Okasaki -} --- insert :: Ord a => a -> RB a -> RB a --- insert x s = --- T B a z b --- where --- T _ a z b = ins s --- ins E = T R E x E --- ins s@(T B a y b) --- | x<y = balance (ins a) y b --- | x>y = balance a y (ins b) --- | otherwise = s --- ins s@(T R a y b) --- | x<y = T R (ins a) y b --- | x>y = T R a y (ins b) --- | otherwise = s --- --- --- {- balance: first equation is new, --- to make it work with a weaker invariant -} --- balance :: RB a -> a -> RB a -> RB a --- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d) --- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d) --- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d) --- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d) --- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d) --- balance a x b = T B a x b --- --- member :: Ord a => a -> RB a -> Bool --- member x E = False --- member x (T _ a y b) --- | x<y = member x a --- | x>y = member x b --- | otherwise = True --- --- {- deletion a la SMK -} --- delete :: Ord a => a -> RB a -> RB a --- delete x t = --- case del t of {T _ a y b -> T B a y b; _ -> E} --- where --- del E = E --- del (T _ a y b) --- | x<y = delformLeft a y b --- | x>y = delformRight a y b --- | otherwise = app a b --- delformLeft a@(T B _ _ _) y b = balleft (del a) y b --- delformLeft a y b = T R (del a) y b --- --- delformRight a y b@(T B _ _ _) = balright a y (del b) --- delformRight a y b = T R a y (del b) --- --- balleft :: RB a -> a -> RB a -> RB a --- balleft (T R a x b) y c = T R (T B a x b) y c --- balleft bl x (T B a y b) = balance bl x (T R a y b) --- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c)) --- --- balright :: RB a -> a -> RB a -> RB a --- balright a x (T R b y c) = T R a x (T B b y c) --- balright (T B a x b) y bl = balance (T R a x b) y bl --- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) --- --- sub1 :: RB a -> RB a --- sub1 (T B a x b) = T R a x b --- sub1 _ = error "invariance violation" --- --- app :: RB a -> RB a -> RB a --- app E x = x --- app x E = x --- app (T R a x b) (T R c y d) = --- case app b c of --- T R b' z c' -> T R(T R a x b') z (T R c' y d) --- bc -> T R a x (T R bc y d) --- app (T B a x b) (T B c y d) = --- case app b c of --- T R b' z c' -> T R(T B a x b') z (T B c' y d) --- bc -> balleft a x (T B bc y d) --- app a (T R b x c) = T R (app a b) x c --- app (T R a x b) c = T R a x (app b c) - +{-# 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.Demoted where++import Data.RBR.Internal++import Data.Proxy+import Data.Kind+import Data.Typeable+import GHC.TypeLits++emptyMap :: Map String TypeRep+emptyMap = E++class DemotableColor (c :: Color) where+ demoteColor :: Proxy c -> Color++instance DemotableColor R where+ demoteColor _ = R++instance DemotableColor B where+ demoteColor _ = B++class DemotableMap (t :: Map Symbol Type) where+ demoteMap :: Proxy t -> Map String TypeRep++instance DemotableMap E where+ demoteMap _ = E++instance (DemotableColor c,+ KnownSymbol s,+ Typeable ty,+ DemotableMap l,+ DemotableMap r) + => DemotableMap (N c l s ty r) where+ demoteMap _ = N (demoteColor (Proxy @c)) + (demoteMap (Proxy @l)) + (symbolVal (Proxy @s)) + (typeRep (Proxy @ty)) + (demoteMap (Proxy @r))++t_insert :: Ord a => a -> v -> Map a v -> Map a v+t_insert x val s =+ N B a v z b+ where+ N _ a v z b = ins s+ ins E = N R E x val E+ ins s@(N B a y val' b)+ | x<y = t_balance (ins a) y val' b+ | x>y = t_balance a y val' (ins b)+ | otherwise = s+ ins s@(N R a y val' b)+ | x<y = N R (ins a) y val' b+ | x>y = N R a y val' (ins b)+ | otherwise = s++t_balance :: Map a v -> a -> v -> Map a v -> Map a v+t_balance (N R a x xv b) y yv (N R c z zv d) = N R (N B a x xv b) y yv (N B c z zv d)+t_balance (N R (N R a x xv b) y yv c) z zv d = N R (N B a x xv b) y yv (N B c z zv d)+t_balance (N R a x xv (N R b y yv c)) z zv d = N R (N B a x xv b) y yv (N B c z zv d)+t_balance a x xv (N R b y yv (N R c z zv d)) = N R (N B a x xv b) y yv (N B c z zv d)+t_balance a x xv (N R (N R b y yv c) z zv d) = N R (N B a x xv b) y yv (N B c z zv d)+t_balance a x xv b = N B a x xv b+++t_delete :: Ord a => a -> Map a v -> Map a v+t_delete x t =+ case del t of {N _ a y yv b -> N B a y yv b; _ -> E}+ where+ del E = E+ del (N _ a y yv b)+ | x<y = delformLeft a y yv b+ | x>y = delformRight a y yv b+ | otherwise = t_app a b+ delformLeft a@(N B _ _ _ _) y yv b = t_balleft (del a) y yv b+ delformLeft a y yv b = N R (del a) y yv b++ delformRight a y yv b@(N B _ _ _ _) = t_balright a y yv (del b)+ delformRight a y yv b = N R a y yv (del b)++t_balleft :: Map a v -> a -> v -> Map a v -> Map a v+t_balleft (N R a x xv b) y yv c = N R (N B a x xv b) y yv c+t_balleft bl x xv (N B a y yv b) = t_balance bl x xv (N R a y yv b)+t_balleft bl x xv (N R (N B a y yv b) z zv c) = N R (N B bl x xv a) y yv (t_balance b z zv (t_sub1 c))++t_balright :: Map a v -> a -> v -> Map a v -> Map a v+t_balright a x xv (N R b y yv c) = N R a x xv (N B b y yv c)+t_balright (N B a x xv b) y yv bl = t_balance (N R a x xv b) y yv bl+t_balright (N R a x xv (N B b y yv c)) z zv bl = N R (t_balance (t_sub1 a) x xv b) y yv (N B c z zv bl)++t_sub1 :: Map a v -> Map a v+t_sub1 (N B a x xv b) = N R a x xv b+t_sub1 _ = error "invariance violation"++t_app :: Map a v -> Map a v -> Map a v+t_app E x = x+t_app x E = x+t_app (N R a x xv b) (N R c y yv d) =+ case t_app b c of+ N R b' z zv c' -> N R (N R a x xv b') z zv (N R c' y yv d)+ bc -> N R a x xv (N R bc y yv d)+t_app (N B a x xv b) (N B c y yv d) = + case t_app b c of+ N R b' z zv c' -> N R (N B a x xv b') z zv (N B c' y yv d)+ bc -> t_balleft a x xv (N B bc y yv d)+t_app a (N R b x xv c) = N R (t_app a b) x xv c+t_app (N R a x xv b) c = N R a x xv (t_app b c)++-- The original term-level code, taken from:+-- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html+--+-- {- Version 1, 'untyped' -}+-- data Color = R | B deriving Show+-- data RB a = E | T Color (RB a) a (RB a) deriving Show+-- +-- {- Insertion and membership test as by Okasaki -}+-- insert :: Ord a => a -> RB a -> RB a+-- insert x s =+-- T B a z b+-- where+-- T _ a z b = ins s+-- ins E = T R E x E+-- ins s@(T B a y b)+-- | x<y = balance (ins a) y b+-- | x>y = balance a y (ins b)+-- | otherwise = s+-- ins s@(T R a y b)+-- | x<y = T R (ins a) y b+-- | x>y = T R a y (ins b)+-- | otherwise = s+-- +-- +-- {- balance: first equation is new,+-- to make it work with a weaker invariant -}+-- balance :: RB a -> a -> RB a -> RB a+-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d)+-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)+-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)+-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)+-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)+-- balance a x b = T B a x b+--+-- member :: Ord a => a -> RB a -> Bool+-- member x E = False+-- member x (T _ a y b)+-- | x<y = member x a+-- | x>y = member x b+-- | otherwise = True+-- +-- {- deletion a la SMK -}+-- delete :: Ord a => a -> RB a -> RB a+-- delete x t =+-- case del t of {T _ a y b -> T B a y b; _ -> E}+-- where+-- del E = E+-- del (T _ a y b)+-- | x<y = delformLeft a y b+-- | x>y = delformRight a y b+-- | otherwise = app a b+-- delformLeft a@(T B _ _ _) y b = balleft (del a) y b+-- delformLeft a y b = T R (del a) y b+--+-- delformRight a y b@(T B _ _ _) = balright a y (del b)+-- delformRight a y b = T R a y (del b)+-- +-- balleft :: RB a -> a -> RB a -> RB a+-- balleft (T R a x b) y c = T R (T B a x b) y c+-- balleft bl x (T B a y b) = balance bl x (T R a y b)+-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c))+-- +-- balright :: RB a -> a -> RB a -> RB a+-- balright a x (T R b y c) = T R a x (T B b y c)+-- balright (T B a x b) y bl = balance (T R a x b) y bl+-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)+-- +-- sub1 :: RB a -> RB a+-- sub1 (T B a x b) = T R a x b+-- sub1 _ = error "invariance violation"+-- +-- app :: RB a -> RB a -> RB a+-- app E x = x+-- app x E = x+-- app (T R a x b) (T R c y d) =+-- case app b c of+-- T R b' z c' -> T R(T R a x b') z (T R c' y d)+-- bc -> T R a x (T R bc y d)+-- app (T B a x b) (T B c y d) = +-- case app b c of+-- T R b' z c' -> T R(T B a x b') z (T B c' y d)+-- bc -> balleft a x (T B bc y d)+-- app a (T R b x c) = T R (app a b) x c+-- app (T R a x b) c = T R a x (app b c)+
lib/Data/RBR.hs view
@@ -1,158 +1,172 @@-{-| - This module provides extensible 'Record' and 'Variant' types, which are - indexed by a type-level 'Map'. - - Many functions in this module require the use of @TypeApplications@ to - avoid ambiguity. The order of the applications is the order of the type - variables in the function signature's @forall@. The first type variable is - usually the field/branch name and it's always required. The other type - variables can often be inferred. - - Meaning of commonly used type and kind variables: - - - @t@: A type-level 'Map', usually of kind @Map Symbol q@. - - @k@: A key of kind 'Symbol' in a type-level 'Map'. - - @v@: A type value of kind @q@ in a type-level 'Map'. - - @q@: The kind of the type value @v@. - - @f@: A type constructor of kind @q -> Type@ that wraps the type @v@. - - @flat@: A type-level list of kind @[q]@ whose elements correspond to values in a type-level 'Map'. - --} -module Data.RBR ( - -- * Type-level map - -- $typelevel - Map, - Empty, - KeysValuesAll(), - KnownKey(), - demoteKeys, - KnownKeyTypeableValue(), - demoteEntries, - -- * Records and Variants - Record, - unit, - cpure_Record, - collapse_Record, - prettyShowRecord, - prettyShowRecordI, - Variant, - impossible, - prettyShowVariant, - prettyShowVariantI, - -- ** Inserting and widening - Insertable (Insert), - InsertAll, - FromList, - insert, - addField, - insertI, - addFieldI, - widen, - -- ** Deleting and winnowing - Deletable (Delete), - delete, - winnow, - winnowI, - -- ** Projecting and injecting - Key (Value), - Field, - field, - Branch, - branch, - project, - projectI, - getField, - getFieldI, - setField, - setFieldI, - modifyField, - modifyFieldI, - inject, - injectI, - match, - matchI, - -- ** Eliminating variants - eliminate, - Case (..), - addCase, - addCaseI, - -- ** Subsets of fields and branches - PresentIn, - ProductlikeSubset, - fieldSubset, - projectSubset, - getFieldSubset, - setFieldSubset, - modifyFieldSubset, - SumlikeSubset, - branchSubset, - injectSubset, - matchSubset, - eliminateSubset, - -- * Interfacing with normal records - -- $nominal - ToRecord (..), - FromRecord (..), - VariantCode, - ToVariant (..), - FromVariant(..), - -- * Interfacing with Data.SOP - Productlike (..), - prefixNP, - breakNP, - toNP, - fromNP, - Sumlike (..), - prefixNS, - breakNS, - toNS, - fromNS, - -- * Data.SOP re-exports - I(..), - K(..), - NP(..), - NS(..), - ) where - -import Data.RBR.Internal -import Data.SOP (I(..),K(..),NP(..),NS(..)) - -{- $setup - ->>> :set -XDataKinds -XTypeApplications -XPartialTypeSignatures -XFlexibleContexts -XTypeFamilies -XDeriveGeneric ->>> :set -Wno-partial-type-signatures ->>> import Data.RBR ->>> import Data.SOP ->>> import GHC.Generics - --} - -{- $typelevel - - A type-level map that keeps track of which keys are present, and to which - types they correspond. - - Implemented as a red-black tree, and used as a kind by means of @DataKinds@. --} - -{- $nominal - - Typeclasses for converting to and from normal Haskell records and sum types. - - They have default implementations based in "GHC.Generics": - ->>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) ->>> instance ToRecord Person ->>> instance FromRecord Person - ->>> data Summy = Lefty Int | Righty Bool deriving (Generic,Show) ->>> instance ToVariant Summy ->>> instance FromVariant Summy - - Only single-constructor records with named fields can have 'ToRecord' and - 'FromRecord' instances. - - Only sum types with exactly one anonymous argument on each branch can have - 'ToVariant' and 'FromVariant' instances. - --} +{-| + This module provides extensible 'Record' and 'Variant' types, which are+ indexed by a type-level 'Map'.++ Many functions in this module require the use of @TypeApplications@ to+ avoid ambiguity. The order of the applications is the order of the type+ variables in the function signature's @forall@. The first type variable is+ usually the field/branch name and it's always required. The other type+ variables can often be inferred.++ Meaning of commonly used type and kind variables:++ - @t@: A type-level 'Map', usually of kind @Map Symbol q@.+ - @k@: A key of kind 'Symbol' in a type-level 'Map'. + - @v@: A type value of kind @q@ in a type-level 'Map'.+ - @q@: The kind of the type value @v@.+ - @f@: A type constructor of kind @q -> Type@ that wraps the type @v@. + - @flat@: A type-level list of kind @[q]@ whose elements correspond to values in a type-level 'Map'.+ +-}+module Data.RBR (+ -- * Type-level map+ -- $typelevel+ Map,+ Empty,+ KeysValuesAll(),+ KnownKey(),+ demoteKeys,+ KnownKeyTypeableValue(),+ demoteEntries,+ KeyValueConstraints(),+ ValueConstraint(),+ PresentIn(),+ -- * Records and Variants+ Record,+ unit,+ Variant,+ impossible,+ -- ** Inserting and widening+ Insertable (Insert),+ InsertAll,+ FromList,+ insert,+ addField,+ insertI,+ addFieldI,+ widen,+ -- ** Deleting and winnowing+ Deletable (Delete),+ delete,+ winnow,+ winnowI,+ -- ** Projecting and injecting+ Key (Value),+ Field,+ field,+ Branch,+ branch,+ project,+ projectI,+ getField,+ getFieldI,+ setField,+ setFieldI,+ modifyField,+ modifyFieldI,+ inject,+ injectI,+ match,+ matchI,+ -- ** Transformations+ Maplike(..),+ cpure_Record,+ cpure'_Record,+ VariantInjection(..),+ prettyShow_Record,+ prettyShow_RecordI,+ prettyShow_Variant,+ prettyShow_VariantI,+ -- ** Eliminating variants+ eliminate_Variant,+ Case (..),+ addCase,+ addCaseI,+ -- * Interfacing with normal records+ -- $nominal+ ToRecord (..),+ FromRecord (..),+ IsRecordType,+ VariantCode,+ ToVariant (..),+ FromVariant(..),+ IsVariantType,+ -- * Interfacing with Data.SOP+ Productlike (..),+ prefixNP,+ breakNP,+ toNP,+ fromNP,+ Sumlike (..),+ prefixNS,+ breakNS,+ toNS,+ fromNS,+ -- * Data.SOP re-exports+ I(..),+ K(..),+ NP(..),+ NS(..),+ (:.:)(..),+ -- * Deprecated+ collapse_Record,+ eliminate,+ prettyShowRecord,+ prettyShowRecordI,+ prettyShowVariant,+ prettyShowVariantI,+ ProductlikeSubset,+ fieldSubset,+ projectSubset,+ getFieldSubset,+ setFieldSubset,+ modifyFieldSubset,+ SumlikeSubset,+ branchSubset,+ injectSubset,+ matchSubset,+ eliminateSubset+ ) where++import Data.RBR.Internal+import Data.SOP (I(..),K(..),NP(..),NS(..),(:.:)(..),Top)++{- $setup+ +>>> :set -XDataKinds -XTypeApplications -XPartialTypeSignatures -XFlexibleContexts -XTypeFamilies -XDeriveGeneric +>>> :set -Wno-partial-type-signatures +>>> import Data.RBR+>>> import Data.SOP+>>> import GHC.Generics++-}++{- $typelevel+ + A type-level map that keeps track of which keys are present, and to which+ types they correspond.++ Implemented as a red-black tree, and used as a kind by means of @DataKinds@. +-} ++{- $nominal+ + Typeclasses for converting to and from normal Haskell records and sum types.++ They have default implementations based in "GHC.Generics":++>>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show)+>>> instance ToRecord Person +>>> instance FromRecord Person ++>>> data Summy = Lefty Int | Righty Bool deriving (Generic,Show)+>>> instance ToVariant Summy +>>> instance FromVariant Summy ++ Only single-constructor records with named fields can have 'ToRecord' and+ 'FromRecord' instances.++ Only sum types with exactly one anonymous argument on each branch can have+ 'ToVariant' and 'FromVariant' instances.++-}
lib/Data/RBR/Examples.hs view
@@ -1,349 +1,346 @@-module Data.RBR.Examples ( - -- * Setup code - -- $setup - - -- * Constructing a record and viewing its fields. - -- $record1 - - -- * Getting a subset of fields out of a record - -- $record2 - - -- * Creating a Record out of a conventional Haskell record - -- $record3 - - -- * Injecting into a Variant and eliminating it - -- $variant1 - - -- * Working with a bigger error type inside a function - -- $variant1bError - - -- * Creating a Variant out of a sum type and matching on it - -- $variant2 - - -- * Changing the way a specific record field is parsed from JSON - -- $json1 - - -- * Parsing a record from JSON using aliased fields - -- $json2 - - -- * Parsing a subset of a record's fields from JSON and inserting them in an existing record value - -- $json3 - - -- * Ensuring all branches of a sum type are parsed from JSON - -- $json4sum - - -- * External examples - -- $externalexamples - ) where - -import Data.RBR -import Data.SOP - -{- $setup - ->>> :set -XDataKinds -XTypeApplications ->>> :set -XFlexibleContexts -XTypeFamilies -XAllowAmbiguousTypes -XScopedTypeVariables ->>> :set -XDeriveGeneric ->>> :set -XPartialTypeSignatures ->>> :set -Wno-partial-type-signatures ->>> import Data.RBR ->>> import Data.SOP ->>> import Data.SOP.NP (cpure_NP,sequence_NP,liftA2_NP,collapse_NP) ->>> import Data.String ->>> import Data.Proxy ->>> import Data.Foldable ->>> import Data.Profunctor (Star(..)) ->>> import GHC.Generics ->>> import qualified Data.Text ->>> import Data.Aeson ->>> import Data.Aeson.Types (explicitParseField,Parser,parseMaybe) - --} - -{- $record1 - -We use 'addFieldI' instead of 'addField' because we are dealing with pure -records. - ->>> :{ - let r = addFieldI @"name" "Foo" - . addFieldI @"age" 5 - $ unit - in print (getFieldI @"name" r) -:} -"Foo" - --} - -{- $record2 - -Notice that the subset is specified as a type-level tree using 'FromList', a -type family that takes a list of type-level tuples. - -Because here the types of each field can be inferred, we can use a wildcard -(enabled by the @PartialTypeSignatures@ extension). - ->>> :{ - let r = addFieldI @"name" "Foo" - . addFieldI @"age" 5 - . addFieldI @"whatever" 'x' - $ unit - s = getFieldSubset @(FromList [ '("age",_), '("whatever",_) ]) r - in putStrLn (prettyShowRecordI s) -:} -{age = 5, whatever = 'x'} - --} - -{- $record3 - ->>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) ->>> instance ToRecord Person ->>> :{ - let r = addFieldI @"whatever" 'x' (toRecord (Person "Foo" 50)) - in putStrLn (prettyShowRecordI r) -:} -{age = 50, name = "Foo", whatever = 'x'} - --} - -{- $variant1 - - Here the full type of the 'Variant' is inferred from the type of its - 'Record' of eliminators. - ->>> :{ - let b = injectI @"left" 'c' - e = addCaseI @"left" putChar - . addCaseI @"right" @Bool print - $ unit - in eliminate e b -:} -c - --} - -{- $variant1bError - - A function can use internally an error 'Variant' bigger than the one it - eventually returns. The internal branches of the 'Variant' can be removed with - 'winnow'. - - This library makes it more involved than it should be, because inserting an - entry and then deleting it can result in structurally dissimilar type-level - maps. So we need extra type annotations in 'winnow', and also a call to - 'injectSubset' to perform the conversion. - ->>> type Smaller = FromList '[ '("foo",Char), '("bar",Int) ] ->>> :{ - let func :: Int -> Variant I Smaller - func i = - let v = if (i == 0) then injectI @"baz" "internal" - else injectI @"foo" 'c' - r = case winnowI @"baz" @String @(Insert "baz" String Smaller) v of - Right e -> error "this is the baz internal error" - Left smaller -> smaller - in injectSubset r - in putStrLn $ prettyShowVariantI (func 1) -:} -foo ('c') - --} - - -{- $variant2 - ->>> data Summy = Lefty Int | Righty Bool deriving (Generic,Show) ->>> instance ToVariant Summy ->>> :{ - let v = toVariant (Lefty 5) - in matchI @"Lefty" v -:} -Just 5 - --} - -{- $json1 - - We start in the @sop-core@ world, creating a product of parsing functions - (one for each field) using 'cpure_NP'. - - Then we convert that product to a 'Record', apply to it a transformation - that uses field selectors, and convert it back to a product. - - Then we demote the field names and combine them with the product of - 'Data.Aeson.Value' parsers using 'liftA2_NP', getting a product of - 'Data.Aeson.Object' parsers. - - Then we use 'sequence_NP' to convert the product of parsers into a parser - of 'Record'. - ->>> :{ - let parseSpecial - :: forall r c flat. (Generic r, - FromRecord r, - RecordCode r ~ c, - KeysValuesAll KnownKey c, - Productlike '[] c flat, - All FromJSON flat) - => (Record (Star Parser Data.Aeson.Value) c -> Record (Star Parser Data.Aeson.Value) c) - -> Data.Aeson.Value - -> Parser r - parseSpecial transform = - let mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) - fieldParsers = transform $ fromNP @c (cpure_NP (Proxy @FromJSON) (Star parseJSON)) - Star parser = fromNP <$> sequence_NP (liftA2_NP mapKSS (toNP @c demoteKeys) (toNP fieldParsers)) - in withObject "someobj" $ \o -> fromRecord <$> parser o - :} - ->>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) ->>> instance ToRecord Person ->>> instance FromRecord Person ->>> :{ - instance FromJSON Person where - parseJSON = parseSpecial (setField @"name" (Star (\_ -> pure "foo"))) - :} - ->>> Data.Aeson.eitherDecode @Person (fromString "{ \"name\" : null, \"age\" : 50 }") -Right (Person {name = "foo", age = 50}) - --} - - -{- $json2 - - The aliases are passed as a 'Record' with values wrapped in the 'K' - functor. This means that there aren't really any values of the type that - corresponds to each field, only the `String` annotations. - ->>> :{ - let parseWithAliases - :: forall r c flat. (Generic r, - FromRecord r, - RecordCode r ~ c, - KeysValuesAll KnownKey c, - Productlike '[] c flat, - All FromJSON flat) - => Record (K String) c - -> Data.Aeson.Value - -> Parser r - parseWithAliases aliases = - let mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) - fieldParsers = cpure_NP (Proxy @FromJSON) (Star parseJSON) - Star parser = fromNP <$> sequence_NP (liftA2_NP mapKSS (toNP @c aliases) fieldParsers) - in withObject "someobj" $ \o -> fromRecord <$> parser o - :} - - We have to use 'getFieldSubset' because the aliases are listed in a - different order than the record fields, and that might result in different - type-level trees. If the orders were the same, we wouldn't need it. - ->>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) ->>> instance ToRecord Person ->>> instance FromRecord Person ->>> :{ - instance FromJSON Person where - parseJSON = let aliases = addField @"age" (K "bar") - . addField @"name" (K "foo") - $ unit - in parseWithAliases (getFieldSubset @(RecordCode Person) aliases) - :} - ->>> Data.Aeson.eitherDecode @Person (fromString "{ \"foo\" : \"John\", \"bar\" : 50 }") -Right (Person {name = "John", age = 50}) - --} - - - -{- $json3 - ->>> :{ - let parseFieldSubset - :: forall subset subflat c flat r. (Generic r, - FromRecord r, - RecordCode r ~ c, - ProductlikeSubset subset c subflat, - KeysValuesAll KnownKey subset, - All FromJSON subflat) - => r - -> Data.Aeson.Value - -> Parser r - parseFieldSubset r = - let mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) - objNP = liftA2_NP mapKSS (toNP @subset demoteKeys) (cpure_NP (Proxy @FromJSON) (Star parseJSON)) - intoOriginal subr = fromRecord (setFieldSubset @subset subr (toRecord r)) - Star subparser = intoOriginal . fromNP @subset <$> sequence_NP objNP - in withObject "someobj" subparser - :} - ->>> data Person = Person { name :: String, age :: Int, whatever :: Bool } deriving (Generic, Show) ->>> instance ToRecord Person ->>> instance FromRecord Person ->>> :{ - let original = Person "John" 50 True - Just v = Data.Aeson.decode @Data.Aeson.Value (fromString "{ \"name\" : \"Mark\", \"age\" : 70 }") - subsetParser = parseFieldSubset @(FromList [ '("name",_), '("age",_) ]) original - Just s = parseMaybe subsetParser v - in s - :} -Person {name = "Mark", age = 70, whatever = True} - --} - - -{- $json4sum - - To ensure that we don't forget any branch when parsing a sum type from JSON, - we can create a n-ary product of parsers, one for each branch. - - Then we create a n-ary product of injections. Each component of the - product creates a n-ary sum out of the value of the corresponding branch. - - We combine the n-ary product of parsers with the n-ary product of - injections, and collapse all the resulting parsers with - 'Control.Applicative.asum'. - - Then we convert the n-ary sum value that "wins" into a 'Variant' and - finally back into the original type. - ->>> :{ - let parseAll - :: forall r c flat. (Generic r, - FromVariant r, - VariantCode r ~ c, - KeysValuesAll KnownKey c, - Productlike '[] c flat, - Sumlike '[] c flat, - All FromJSON flat) - => Data.Aeson.Value - -> Parser r - parseAll = - let mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) - branchParsers = liftA2_NP mapKSS (toNP @c demoteKeys) (cpure_NP (Proxy @FromJSON) (Star parseJSON)) - injected = liftA2_NP (\f star -> K (unK . apFn f . I <$> star)) (injections @flat) branchParsers - Star parser = asum $ collapse_NP injected - in withObject "someobj" (\o -> fromVariant @r . fromNS <$> parser o) - :} - ->>> data ThisOrThat = This String | That Int deriving (Generic, Show) ->>> instance FromVariant ThisOrThat ->>> :{ - let Just v = Data.Aeson.decode @Data.Aeson.Value (fromString "{ \"That\" : 70 }") - Just s = parseMaybe (parseAll @ThisOrThat) v - in s - :} -That 70 - --} - -{- $externalexamples - - * [Is there a canonical way of comparing/changing one/two records in haskell? (SO)](https://stackoverflow.com/a/57574731/1364288) - * [Given a record of functions, and a record of data of the types acted on by the functions, how to generically apply the function record? (SO)](https://stackoverflow.com/a/58890226/1364288) - * [Help with Generics. (Reddit)](https://www.reddit.com/r/haskell/comments/cteemj/help_with_generics/expyjfk) - * [Adventures assembling records of capabilities. (Discourse)](https://discourse.haskell.org/t/adventures-assembling-records-of-capabilities/623) - * [Resources on sop-core and generics-sop. (GitHub)](https://github.com/well-typed/generics-sop/issues/47) - --} - +module Data.RBR.Examples (+ -- * Setup code+ -- $setup++ -- * Constructing a record and viewing its fields.+ -- $record1+ + -- * Getting a subset of fields out of a record+ -- $record2+ + -- * Creating a Record out of a conventional Haskell record+ -- $record3+ + -- * Injecting into a Variant and eliminating it+ -- $variant1+ + -- * Working with a bigger error type inside a function+ -- $variant1bError+ + -- * Creating a Variant out of a sum type and matching on it+ -- $variant2+ + -- * Changing the way a specific record field is parsed from JSON+ -- $json1+ + -- * Parsing a record from JSON using aliased fields+ -- $json2+ + -- * Parsing a subset of a record's fields from JSON and inserting them in an existing record value+ -- $json3+ + -- * Ensuring all branches of a sum type are parsed from JSON+ -- $json4sum++ -- * External examples+ -- $externalexamples+ ) where++import Data.RBR+import Data.SOP++{- $setup+ +>>> :set -XDataKinds -XTypeApplications +>>> :set -XFlexibleContexts -XTypeFamilies -XAllowAmbiguousTypes -XScopedTypeVariables+>>> :set -XDeriveGeneric +>>> :set -XPartialTypeSignatures +>>> :set -XTypeOperators+>>> :set -Wno-partial-type-signatures +>>> import Data.RBR+>>> import qualified Data.RBR.Subset as S+>>> import Data.SOP+>>> import Data.SOP.NP (cpure_NP,sequence_NP,liftA2_NP,collapse_NP)+>>> import Data.String+>>> import Data.Proxy+>>> import Data.Foldable+>>> import Data.Profunctor (Star(..))+>>> import GHC.Generics (Generic)+>>> import GHC.TypeLits+>>> import qualified Data.Text+>>> import Data.Aeson+>>> import Data.Aeson.Types (explicitParseField,Parser,parseMaybe)++-}++{- $record1+ +We use 'addFieldI' instead of 'addField' because we are dealing with pure+records.++>>> :{ + let r = addFieldI @"name" "Foo"+ . addFieldI @"age" 5+ $ unit+ in print (getFieldI @"name" r)+:}+"Foo"+ +-} ++{- $record2+ +Notice that the subset is specified as a type-level tree using 'FromList', a+type family that takes a list of type-level tuples.++Because here the types of each field can be inferred, we can use a wildcard+(enabled by the @PartialTypeSignatures@ extension).++>>> :{ + let r = addFieldI @"name" "Foo"+ . addFieldI @"age" 5+ . addFieldI @"whatever" 'x'+ $ unit+ s = S.getFieldSubset @(FromList [ '("age",_), '("whatever",_) ]) r+ in putStrLn (prettyShow_RecordI s)+:}+{age = 5, whatever = 'x'} ++-} ++{- $record3+ +>>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show)+>>> instance ToRecord Person +>>> :{ + let r = addFieldI @"whatever" 'x' (toRecord (Person "Foo" 50))+ in putStrLn (prettyShow_RecordI r)+:}+{age = 50, name = "Foo", whatever = 'x'} ++-} ++{- $variant1+ + Here the full type of the 'Variant' is inferred from the type of its+ 'Record' of eliminators.++>>> :{+ let b = injectI @"left" 'c'+ e = addCaseI @"left" putChar+ . addCaseI @"right" @Bool print+ $ unit+ in eliminate_Variant e b+:}+c++-} ++{- $variant1bError+ + A function can use internally an error 'Variant' bigger than the one it+ eventually returns. The internal branches of the 'Variant' can be removed with+ 'winnow'. ++ This library makes it more involved than it should be, because inserting an+ entry and then deleting it can result in structurally dissimilar type-level+ maps. So we need extra type annotations in 'winnow', and also a call to+ 'injectSubset' to perform the conversion.+ +>>> type Smaller = FromList '[ '("foo",Char), '("bar",Int) ]+>>> :{+ let func :: Int -> Variant I Smaller + func i = + let v = if (i == 0) then injectI @"baz" "internal"+ else injectI @"foo" 'c'+ r = case winnowI @"baz" @String @(Insert "baz" String Smaller) v of+ Right e -> error "this is the baz internal error"+ Left smaller -> smaller+ in S.injectSubset r+ in putStrLn $ prettyShow_VariantI (func 1)+:}+foo ('c')++-} +++{- $variant2+ +>>> data Summy = Lefty Int | Righty Bool deriving (Generic,Show)+>>> instance ToVariant Summy +>>> :{+ let v = toVariant (Lefty 5)+ in matchI @"Lefty" v+:}+Just 5++-} ++{- $json1+ + We start in the @sop-core@ world, creating a product of parsing functions+ (one for each field) using 'cpure_NP'. ++ Then we convert that product to a 'Record', apply to it a transformation+ that uses field selectors, and convert it back to a product.++ Then we demote the field names and combine them with the product of+ 'Data.Aeson.Value' parsers using 'liftA2_NP', getting a product of+ 'Data.Aeson.Object' parsers.++ Then we use 'sequence_NP' to convert the product of parsers into a parser+ of 'Record'.++>>> :{+ let parseSpecial+ :: forall r c flat. (IsRecordType r c, + Maplike c,+ KeysValuesAll (KeyValueConstraints KnownSymbol FromJSON) c) + => (Record ((,) String :.: Star Parser Data.Aeson.Value) c -> Record ((,) String :.: Star Parser Data.Aeson.Value) c)+ -> Data.Aeson.Value + -> Parser r+ parseSpecial transform = + let fieldParsers = transform $ + cpure'_Record (Proxy @FromJSON) $ \fieldName -> Comp (fieldName,Star parseJSON)+ applyName (Comp (fieldName,Star f)) = Star (\o -> explicitParseField f o (Data.Text.pack fieldName))+ Star objectParser = sequence_Record $ liftA_Record applyName fieldParsers+ in withObject "someobj" $ \o -> fromRecord <$> objectParser o+ :}++>>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show)+>>> instance ToRecord Person +>>> instance FromRecord Person +>>> :{ + instance FromJSON Person where + parseJSON = parseSpecial (setField @"name" (Comp ("anothername",Star (\_ -> pure "foo"))))+ :}++>>> Data.Aeson.eitherDecode @Person (fromString "{ \"anothername\" : null, \"age\" : 50 }")+Right (Person {name = "foo", age = 50})++-}+++{- $json2+ + The aliases are passed as a 'Record' with values wrapped in the 'K'+ functor. This means that there aren't really any values of the type that+ corresponds to each field, only the `String` annotations.++>>> :{+ let parseWithAliases+ :: forall r c flat. (IsRecordType r c, + Maplike c,+ KeysValuesAll (ValueConstraint FromJSON) c) + => Record (K String) c+ -> Data.Aeson.Value + -> Parser r+ parseWithAliases aliases = + let fieldParsers = cpure_Record (Proxy @(ValueConstraint FromJSON)) (Star parseJSON)+ mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name))+ Star objectParser = sequence_Record $ liftA2_Record mapKSS aliases fieldParsers+ in withObject "someobj" $ \o -> fromRecord <$> objectParser o+ :}++ We have to use 'getFieldSubset' because the aliases are listed in a+ different order than the record fields, and that might result in different+ type-level trees. If the orders were the same, we wouldn't need it. ++>>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show)+>>> instance ToRecord Person +>>> instance FromRecord Person +>>> :{ + instance FromJSON Person where + parseJSON = let aliases = addField @"age" (K "bar")+ . addField @"name" (K "foo")+ $ unit+ in parseWithAliases (S.getFieldSubset @(RecordCode Person) aliases)+ :}++>>> Data.Aeson.eitherDecode @Person (fromString "{ \"foo\" : \"John\", \"bar\" : 50 }")+Right (Person {name = "John", age = 50})++-}++++{- $json3+ +>>> :{+ let parseFieldSubset+ :: forall subset c r. (IsRecordType r c, + S.Subset subset c,+ Maplike subset,+ KeysValuesAll (KeyValueConstraints KnownSymbol FromJSON) subset) + => r + -> Data.Aeson.Value+ -> Parser r + parseFieldSubset r = + let subparser = + sequence_Record $+ cpure'_Record (Proxy @FromJSON) $ \fieldName ->+ Star (\o -> explicitParseField parseJSON o (Data.Text.pack fieldName))+ intoOriginal subrecord = fromRecord (S.setFieldSubset @subset subrecord (toRecord r))+ Star parser = intoOriginal <$> subparser+ in withObject "someobj" parser+ :}++>>> data Person = Person { name :: String, age :: Int, whatever :: Bool } deriving (Generic, Show)+>>> instance ToRecord Person +>>> instance FromRecord Person +>>> :{ + let original = Person "John" 50 True+ Just v = Data.Aeson.decode @Data.Aeson.Value (fromString "{ \"name\" : \"Mark\", \"age\" : 70 }")+ subsetParser = parseFieldSubset @(FromList [ '("name",_), '("age",_) ]) original+ Just s = parseMaybe subsetParser v+ in s+ :}+Person {name = "Mark", age = 70, whatever = True}++-}+++{- $json4sum+ + To ensure that we don't forget any branch when parsing a sum type from JSON, + we can create a n-ary product of parsers, one for each branch.++ Then we create a n-ary product of injections. Each component of the+ product creates a n-ary sum out of the value of the corresponding branch.++ We combine the n-ary product of parsers with the n-ary product of+ injections, and collapse all the resulting parsers with+ 'Control.Applicative.asum'.++ Then we convert the n-ary sum value that "wins" into a 'Variant' and+ finally back into the original type.++>>> :{+ let parseAll+ :: forall r c flat. (IsVariantType r c, + Maplike c,+ KeysValuesAll (KeyValueConstraints KnownSymbol FromJSON) c) + => Data.Aeson.Value + -> Parser r+ parseAll = + let fieldParsers = cpure'_Record (Proxy @FromJSON) $ \fieldName -> + Star (\o -> explicitParseField parseJSON o (Data.Text.pack fieldName))+ injected = liftA2_Record (\f star -> K [ runVariantInjection f . I <$> star ]) injections_Variant fieldParsers + Star parser = asum $ collapse'_Record injected+ in withObject "someobj" (\o -> fromVariant <$> parser o)+ :}++>>> data ThisOrThat = This String | That Int deriving (Generic, Show)+>>> instance FromVariant ThisOrThat+>>> instance ToVariant ThisOrThat+>>> :{ + let Just v = Data.Aeson.decode @Data.Aeson.Value (fromString "{ \"That\" : 70 }")+ Just s = parseMaybe (parseAll @ThisOrThat) v+ in s+ :}+That 70++-}++{- $externalexamples+ + * [Is there a canonical way of comparing/changing one/two records in haskell? (SO)](https://stackoverflow.com/a/57574731/1364288)+ * [Given a record of functions, and a record of data of the types acted on by the functions, how to generically apply the function record? (SO)](https://stackoverflow.com/a/58890226/1364288) + * [Help with Generics. (Reddit)](https://www.reddit.com/r/haskell/comments/cteemj/help_with_generics/expyjfk)+ * [Adventures assembling records of capabilities. (Discourse)](https://discourse.haskell.org/t/adventures-assembling-records-of-capabilities/623)+ * [Creating a result piecewise from stateful computation. (SO)](https://stackoverflow.com/a/60067270/1364288)+ * [Extracting sections of function pipelines. (GitHub)](https://gist.github.com/danidiaz/2157e68f5d4967e468a9d062d4476adf#file-pipelines3-hs)+ * [Resources on sop-core and generics-sop. (GitHub)](https://github.com/well-typed/generics-sop/issues/47)++-}+
lib/Data/RBR/Internal.hs view
@@ -1,1897 +1,2065 @@--- | See <https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html here> for --- the original term-level code by Stefan Kahrs. It is also copied at the end --- of this file. Some parts of the type-level code include the correspondign --- term-level parts in their comments. -{-# 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.Functor.Contravariant (Contravariant(contramap)) -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) - - -{- $setup - ->>> :set -XDataKinds -XTypeApplications -XPartialTypeSignatures -XFlexibleContexts -XTypeFamilies -XDeriveGeneric ->>> :set -Wno-partial-type-signatures ->>> import Data.RBR ->>> import Data.SOP ->>> import GHC.Generics - --} - - --- | The color of a node. -data Color = R - | B - deriving (Show,Eq) - --- | A Red-Black tree. It will be used as a kind, to index the 'Record' and 'Variant' types. -data Map symbol q = E - | N Color (Map symbol q) symbol q (Map symbol q) - deriving (Show,Eq) - --- | A map without entries. See also 'unit' and 'impossible'. -type Empty = E - --- --- --- This code has been copied and adapted from the corresponding Data.SOP code (the All constraint). --- - --- Why is this KeysValuesAllF type family needed at all? Why is not KeysValuesAll sufficient by itself? --- In fact, if I delete KeysValuesAllF and use eclusively KeysValuesAll, functions like demoteKeys seem to still work fine. --- --- UndecidableSuperClasses and RankNTypes seem to be required by KeysValuesAllF. -type family - KeysValuesAllF (c :: symbol -> q -> Constraint) (t :: Map symbol q) :: Constraint where - KeysValuesAllF _ E = () - KeysValuesAllF c (N color left k v right) = (c k v, KeysValuesAll c left, KeysValuesAll c right) - -{- | Require a constraint for every key-value pair in a tree. This is a generalization of 'Data.SOP.All' from "Data.SOP". --} -class KeysValuesAllF c t => KeysValuesAll (c :: symbol -> q -> Constraint) (t :: Map symbol q) where - - -- 'cpara_Map' constructs a 'Record' by means of a constraint for producing - -- the nodes of the tree. The constraint is passed as a 'Data.Proxy.Proxy'. - 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) - -{- | - Create a 'Record', knowing that both keys and values satisfy a 2-place constraint. The constraint is passed as a 'Data.Proxy.Proxy'. - - The naming scheme follows that of 'Data.SOP.NP.cpure_NP'. - -} -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 - -{- | Create a 'Record' containing the names of each field. - - The names are represented by a constant functor 'K' carrying an annotation - of type 'String'. This means that there aren't actually any values of the - type that corresponds to each field, only the 'String' annotations. - ->>> putStrLn $ prettyShowRecord show $ demoteKeys @(Insert "foo" Char (Insert "bar" Bool Empty)) -{bar = K "bar", foo = K "foo"} - --} -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 - -{- | - Two-place constraint saying that a 'Symbol' key can be demoted to 'String'. Nothing is required from the corresponding value. - - Defined using the "class synonym" <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ trick>. --} -class KnownSymbol k => KnownKey (k :: Symbol) (v :: q) -instance KnownSymbol k => KnownKey k v - -{- | - Create a record containing the names of each field along with a term-level - representation of each type. - ->>> putStrLn $ prettyShowRecord show $ demoteEntries @(Insert "foo" Char (Insert "bar" Bool Empty)) -{bar = K ("bar",Bool), foo = K ("foo",Char)} - - See also 'collapse_Record' for getting the entries as a list. --} -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 - -{- | - Two-place constraint saying that a 'Symbol' key can be demoted to 'String', and that the corresponding value 'Type' has a term-level representation. - - Defined using the "class synonym" <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ trick>. --} -class (KnownSymbol k, Typeable v) => KnownKeyTypeableValue (k :: Symbol) (v :: q) -instance (KnownSymbol k, Typeable v) => KnownKeyTypeableValue k v - --- class KeyValueTop (k :: Symbol) (v :: z) --- instance KeyValueTop k v - --- --- - -{- | An extensible product-like type with named fields. - - The values in the 'Record' come wrapped in a type constructor @f@, which - por pure records will be the identity functor 'I'. - - See also 'insert', 'delete' and 'project'. --} -data Record (f :: q -> Type) (t :: Map Symbol q) 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 a 'Record' composed of 'K' annotations. - ->>> collapse_Record unit -[] - ->>> collapse_Record (insert @"bar" (K False) unit) -[False] - - The naming scheme follows that of 'Data.SOP.NP.collapse_NP'. - --} -collapse_Record :: forall t result a. (Productlike '[] t result) => Record (K a) t -> [a] -collapse_Record = collapse_NP . toNP - -{- | Show a 'Record' in a friendlier way than the default 'Show' instance. The - function argument will usually be 'show', but it can be used to unwrap the - value of each field before showing it. --} -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)) ++ "}" - - -{- | Like 'prettyShowRecord' but specialized to pure records. --} -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 - -{-| A Record without components is a boring, uninformative type whose single value can be conjured out of thin air. --} -unit :: Record f Empty -unit = Empty - -{- | An extensible sum-like type with named branches. - - The values in the 'Variant' come wrapped in a type constructor @f@, which - por pure variants will be the identity functor 'I'. - - See also 'widen', 'winnow' and 'inject'. --} -data Variant (f :: q -> Type) (t :: Map Symbol q) 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) ++ ")" - -{-| A Variant without branches doesn't have any values. From an impossible thing, anything can come out. --} -impossible :: Variant f Empty -> b -impossible v = case v of - -{- | Show a 'Variant' in a friendlier way than the default 'Show' instance. The - function argument will usually be 'show', but it can be used to unwrap the - value of the branch before showing it. --} -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) - -{- | Like 'prettyShowVariant' but specialized to pure variants. --} -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 - --- --- --- Insertion - -{- | Insert a list of type level key / value pairs into a type-level map. --} -type family InsertAll (es :: [(Symbol,q)]) (t :: Map Symbol q) :: Map Symbol q where - InsertAll '[] t = t - InsertAll ( '(name,fieldType) ': es ) t = Insert name fieldType (InsertAll es t) - -{- | Build a type-level map out of a list of type level key / value pairs. --} -type FromList (es :: [(Symbol,q)]) = InsertAll es Empty - - -{- | - Adds a new field to a 'Record'. - ->>> project @"foo" (insert @"foo" (I 'a') unit) -I 'a' - ->>> project @"foo" (insert @"foo" @Char Nothing unit) -Nothing - - -} -insert :: forall k v t f. Insertable k v t => f v -> Record f t -> Record f (Insert k v t) -insert = _insert @_ @k @v @t @f - -{- | - Lets you use a 'Variant' in a bigger context - than the one in which is was defined. - -} -widen :: forall k v t f. Insertable k v t => Variant f t -> Variant f (Insert k v t) -widen = _widen @_ @k @v @t @f - -{- | Alias for 'insert'. --} -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 - -{- | Like 'insert' but specialized to pure 'Record's. - ->>> projectI @"foo" (insertI @"foo" 'a' unit) -'a' - --} -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 - -{- | Like 'addField' but specialized to pure 'Record's. --} -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 that determines if the pair of a 'Symbol' key and a type can - be inserted into a type-level map. - - The associated type family 'Insert' produces the resulting map. - - At the term level, this manifests in 'insert', which adds a new field to a - record, and in 'widen', which lets you use a 'Variant' in a bigger context - than the one in which is was defined. 'insert' tends to be more useful in - practice. - - If the map already has the key but with a /different/ type, the - insertion fails to compile. - -} -class Insertable (k :: Symbol) (v :: q) (t :: Map Symbol q) where - type Insert k v t :: Map Symbol q - _insert :: f v -> Record f t -> Record f (Insert k v t) - _widen :: Variant f t -> Variant f (Insert k v t) - --- insert x s = --- T B a z b --- where --- T _ a z b = ins s -instance (InsertableHelper1 k v t, Insert1 k v t ~ inserted, CanMakeBlack inserted) => 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 k) where - type MakeBlack t :: Map Symbol k - 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 :: q) - (t :: Map Symbol q) where - type Insert1 k v t :: Map Symbol q - 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 - -- FIXME possible duplicate work with CmpSymbol: both in constraint and in associated type family. - -- Is that bad? How to avoid it? - 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 :: q) - (color :: Color) - (left :: Map Symbol q) - (k' :: Symbol) - (v' :: q) - (right :: Map Symbol q) where - type Insert2 ordering k v color left k' v' right :: Map Symbol q - 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) - --- ins s@(T B a y b) --- | x<y = balance (ins a) y b -instance (InsertableHelper1 k v left, Insert1 k v left ~ inserted, - Balanceable inserted 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 - --- ins s@(T B a y b) --- | x<y = balance (ins a) y b -instance (InsertableHelper1 k v left, Insert1 k v left ~ inserted, - Balanceable inserted 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 - - --- This instance implies that we can't change the type associated to an --- existing key. If we did that, we wouldn't be able to widen Variants that --- happen to match that key! -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 - --- ins s@(T B a y b) --- | ... --- | x>y = balance a y (ins b) -instance (InsertableHelper1 k v right, Insert1 k v right ~ inserted, - Balanceable left k' v' inserted - ) - => 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) - --- ins s@(T R a y b) --- | ... --- | x>y = T R a y (ins b) -instance (InsertableHelper1 k v right, Insert1 k v right ~ inserted, - Balanceable left k' v' inserted - ) - => 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 q) (k :: Symbol) (v :: q) (right :: Map Symbol q) where - type Balance left k v right :: Map Symbol q - 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 - -- FIXME possible duplicate work with ShouldBalance: both in constraint and in associated type family. - -- Is that bad? How to avoid it? - 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 q) - (k :: Symbol) - (v :: q) - (right :: Map Symbol q) where - type Balance' action left k v right :: Map Symbol q - 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) - --- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d) -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) - --- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d) -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) - --- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d) -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) - --- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d) -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) - - --- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d) -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) - --- balance a x b = T B a x b -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 - - --- --- --- Accessing fields - --- --- These two type families exist to avoid duplicating expensive type-level --- computations, in particular the Value' computations. --- --- Record accessors are compiled WAY slower without them! --- -{- | Auxiliary type family to avoid repetition and help improve compilation times. - -} -type family Field (f :: q -> Type) (t :: Map Symbol q) (v :: q) where - Field f t v = Record f t -> (f v -> Record f t, f v) - -{- | Auxiliary type family to avoid repetition and help improve compilation times. - -} -type family Branch (f :: q -> Type) (t :: Map Symbol q) (v :: q) where - Branch f t v = (Variant f t -> Maybe (f v), f v -> Variant f t) - --- -{- | - Class that determines if a given 'Symbol' key is present in a type-level - map. - - The 'Value' type family gives the 'Type' corresponding to the key. --} -class Key (k :: Symbol) (t :: Map Symbol q) where - type Value k t :: q - _field :: Field f t (Value k t) - _branch :: Branch f t (Value k t) - -{- | - Takes a field name (given through @TypeApplications@) and a - 'Record', and returns a pair of a setter for the field and the original - value of the field. --} -field :: forall k t f. Key k t => Field f t (Value k t) -field = _field @_ @k @t - -{- | - Takes a branch name (given through @TypeApplications@) and - returns a pair of a match function and a constructor. --} -branch :: forall k t f. Key k t => Branch f t (Value k t) -branch = _branch @_ @k @t - --- member :: Ord a => a -> RB a -> Bool -class KeyHelper (ordering :: Ordering) (k :: Symbol) (left :: Map Symbol q) (v :: q) (right :: Map Symbol q) where - type Value' ordering k left v right :: q - 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 - --- | x<y = member x a -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)) - --- | x>y = member x b -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)) - --- | otherwise = True -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) - -{- | Get the value of a field for a 'Record'. - - --} -project :: forall k t f . Key k t => Record f t -> f (Value k t) -project = snd . field @k @t - -{- | Alias for 'project'. --} -getField :: forall k t f . Key k t => Record f t -> f (Value k t) -getField = project @k @t @f - -{- | Set the value of a field for a 'Record'. --} -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 - -{- | Modify the value of a field for a 'Record'. --} -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)) - -{- | Put a value into the branch of a 'Variant'. - ->>> match @"foo" (inject @"foo" (I 'a') :: Variant I (Insert "foo" Char Empty)) -Just (I 'a') - --} -inject :: forall k t f. Key k t => f (Value k t) -> Variant f t -inject = snd (branch @k @t) - -{- | Check if a 'Variant' value is the given branch. --} -match :: forall k t f. Key k t => Variant f t -> Maybe (f (Value k t)) -match = fst (branch @k @t) - -{- | Like 'project' but specialized to pure 'Record's. - ->>> projectI @"foo" (insertI @"foo" 'a' (insertI @"bar" False unit)) -'a' - --} -projectI :: forall k t . Key k t => Record I t -> Value k t -projectI = unI . snd . field @k @t - -{- | Like 'getField' but specialized to pure 'Record's. --} -getFieldI :: forall k t . Key k t => Record I t -> Value k t -getFieldI = projectI @k @t - -{- | Like 'setField' but specialized to pure 'Record's. --} -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) - -{- | Like 'modifyField' but specialized to pure 'Record's. --} -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) - -{- | Like 'inject' but specialized to pure 'Variant's. - ->>> matchI @"foo" (injectI @"foo" 'a' :: Variant I (Insert "foo" Char Empty)) -Just 'a' - --} -injectI :: forall k t. Key k t => Value k t -> Variant I t -injectI = snd (branch @k @t) . I - -{- | Like 'match' but specialized to pure 'Variants's. --} -matchI :: forall k t . Key k t => Variant I t -> Maybe (Value k t) -matchI v = unI <$> fst (branch @k @t) v - -{- | Process a 'Variant' using a eliminator 'Record' that carries - handlers for each possible branch of the 'Variant'. - ->>> eliminate (addCaseI @"foo" @Int succ (addCaseI @"bar" pred unit)) (injectI @"bar" 33) -32 - --} -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)) - -{- | Represents a handler for a branch of a 'Variant'. --} -newtype Case f a b = Case (f b -> a) - -instance Functor f => Contravariant (Case f a) where - contramap g (Case c) = Case (c . fmap g) - -{- | A form of 'addField' for creating eliminators for 'Variant's. --} -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) - -{- | A pure version of 'addCase'. --} -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)) - --- --- --- Subsetting - -newtype SetField f a b = SetField { getSetField :: f b -> a -> a } - --- this odd trick again... -class (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol q) (k :: Symbol) (v :: q) -instance (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol q) (k :: Symbol) (v :: q) - -{- | Constraint for maps that represent subsets of fields of 'Record'-like types. --} -type ProductlikeSubset (subset :: Map Symbol q) (whole :: Map Symbol q) (flat :: [q]) = - (KeysValuesAll (PresentIn whole) subset, - Productlike '[] subset flat, - SListI flat) - -{- | Like 'field', but targets multiple fields at the same time - --} -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) - -{- | 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. - ->>> prettyShowRecordI $ projectSubset @(Insert "foo" _ (Insert "bar" _ Empty)) (insertI @"foo" 'a' (insertI @"bar" True (insertI @"baz" (Just ()) unit))) -"{bar = True, foo = 'a'}" - - Can also be used to convert between 'Record's with structurally dissimilar - type-level maps that nevertheless hold the same entries. --} -projectSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) - => Record f whole - -> Record f subset -projectSubset = snd . fieldSubset - -{- | Alias for 'projectSubset'. --} -getFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) - => Record f whole - -> Record f subset -getFieldSubset = projectSubset - -{- | Like 'setField', but sets multiple fields at the same time. - --} -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 - -{- | Like 'modifyField', but modifies multiple fields at the same time. - --} -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)) - - -{- | Constraint for maps that represent subsets of branches of 'Variant'-like types. --} -type SumlikeSubset (subset :: Map Symbol q) (whole :: Map Symbol q) (subflat :: [q]) (wholeflat :: [q]) = - (KeysValuesAll (PresentIn whole) subset, - Productlike '[] whole wholeflat, - Sumlike '[] whole wholeflat, - SListI wholeflat, - Productlike '[] subset subflat, - Sumlike '[] subset subflat, - SListI subflat) - -{- | Like 'branch', but targets multiple branches at the same time. --} -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)))) - -- 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 = 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) - -{- | 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 subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat) - => Variant f subset -> Variant f whole -injectSubset = snd (branchSubset @subset @whole @subflat @wholeflat) - -{- | Like 'match', but matches more than one branch. --} -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) - -{- | - Like 'eliminate', but allows the eliminator 'Record' to have more fields - than there are branches in the 'Variant'. --} -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 - --- - --- Interaction with Data.SOP - -{- | Class from converting 'Record's to and from the n-ary product type 'NP' from "Data.SOP". - - 'prefixNP' flattens a 'Record' and adds it to the initial part of the product. - - 'breakNP' reconstructs a 'Record' from the initial part of the product and returns the unconsumed part. - - The functions 'toNP' and 'fromNP' are usually easier to use. --} -class Productlike (start :: [k]) - (t :: Map Symbol k) - (result :: [k]) | 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) - -{- | - Flattens a 'Record' and adds it to the initial part of the product. --} -prefixNP:: forall start t result f. Productlike start t result => Record f t -> NP f start -> NP f result -prefixNP = _prefixNP @_ @start @t @result - -{- | - Reconstructs a 'Record' from the initial part of the product and returns the unconsumed part. --} -breakNP :: forall start t result f. Productlike start t result => NP f result -> (Record f t, NP f start) -breakNP = _breakNP @_ @start @t @result - -{- | Convert a 'Record' into a n-ary product. The order of the elements in the - product is not the order of insertion in the record. - ->>> toNP (insertI @"foo" 'a' (insertI @"bar" True unit)) -I True :* I 'a' :* Nil - --} -toNP :: forall t result f. Productlike '[] t result => Record f t -> NP f result -toNP r = prefixNP r Nil - -{- | Convert a n-ary product into a compatible 'Record'. Usually follows an invocation of 'toNP'. - ->>> prettyShowRecordI . fromNP @(Insert "foo" _ (Insert "bar" _ Empty)) . toNP $ insertI @"foo" 'a' (insertI @"bar" True unit) -"{bar = True, foo = 'a'}" - --} -fromNP :: forall t result f. Productlike '[] t result => NP f result -> Record f t -fromNP np = let (r,Nil) = breakNP np in r - -{- | Class from converting 'Variant's to and from the n-ary sum type 'NS' from "Data.SOP". - - 'prefixNS' flattens a 'Variant' and adds it to the initial part of the sum. - - 'breakNS' reconstructs a 'Variant' from the initial part of the sum and returns the unconsumed part. - - The functions 'toNS' and 'fromNS' are usually easier to use. --} -class Sumlike (start :: [k]) - (t :: Map Symbol k) - (result :: [k]) | 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) - -{- | - - Flattens a 'Variant' and adds it to the initial part of the sum. --} -prefixNS :: forall start t result f. Sumlike start t result => Either (NS f start) (Variant f t) -> NS f result -prefixNS = _prefixNS @_ @start @t @result - -{- | - Reconstructs a 'Variant' from the initial part of the sum and returns the unconsumed part. --} -breakNS :: forall start t result f. Sumlike start t result => NS f result -> Either (NS f start) (Variant f t) -breakNS = _breakNS @_ @start @t @result - -{- | Convert a 'Variant' into a n-ary sum. - ->>> toNS (injectI @"foo" 'a' :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) -S (Z (I 'a')) - --} -toNS :: forall t result f. Sumlike '[] t result => Variant f t -> NS f result -toNS = prefixNS . Right - -{- | Convert a n-ary sum into a compatible 'Variant'. - ->>> prettyShowVariantI $ fromNS @(Insert "foo" _ (Insert "bar" _ Empty)) . toNS $ (injectI @"foo" 'a' :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) -"foo ('a')" - --} -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 - --- --- --- Interfacing with normal records - -class ToRecord (r :: Type) where - type RecordCode r :: Map Symbol Type - -- https://stackoverflow.com/questions/22087549/defaultsignatures-and-associated-type-families/22088808 - 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 - VariantCode' acc (C1 (G.MetaCons k _ _) G.U1) = Insert k () 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 (Key k t, Value k t ~ ()) - => FromVariantHelper t (C1 (G.MetaCons k x y) G.U1) - where - fromVariant' v = case matchI @k @t v of - Just x -> Just (M1 G.U1) - 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 (Key k t, Value k t ~ ()) => - ToVariantHelper t (C1 (G.MetaCons k x y) G.U1) where - toVariant' (M1 G.U1) = injectI @k () - -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 - --- --- --- deletion --- --- --- - -type family DiscriminateBalL (l :: Map k v) (r :: Map k v) :: Bool where - DiscriminateBalL (N R _ _ _ _) _ = False - DiscriminateBalL _ _ = True - -class BalanceableL (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where - type BalL l k v r :: Map Symbol q - 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 q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where - type BalL' b l k v r :: Map Symbol q - 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 - --- balleft :: RB a -> a -> RB a -> RB a --- balleft (T R a x b) y c = T R (T B a x b) y c -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 - --- balleft bl x (T B a y b) = balance bl x (T R a y b) --- the @(N B in the call to balance tree is misleading, as it is ingored... -instance (N R t2 z zv t3 ~ g, BalanceableHelper (ShouldBalance t1 g) t1 y yv g) => - 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')) - --- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c)) -instance (N R l k kv r ~ g, BalanceableHelper (ShouldBalance t3 g) t3 z zv g) => - 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))) - - --- balright :: RB a -> a -> RB a -> RB a --- balright a x (T R b y c) = T R a x (T B b y c) --- balright (T B a x b) y bl = balance (T R a x b) y bl --- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) -type family DiscriminateBalR (l :: Map k v) (r :: Map k v) :: Bool where - DiscriminateBalR _ (N R _ _ _ _) = False - DiscriminateBalR _ _ = True - -class BalanceableR (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where - type BalR l k v r :: Map Symbol q - 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 q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where - type BalR' b l k v r :: Map Symbol q - 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 - --- balright :: RB a -> a -> RB a -> RB a --- balright a x (T R b y c) = T R a x (T B b y c) -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) - --- balright (T B a x b) y bl = balance (T R a x b) y bl -instance (N R t2 z zv t3 ~ g, ShouldBalance g t1 ~ shouldbalance, BalanceableHelper shouldbalance g 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) - --- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) -instance (N R t2 u uv t3 ~ g, ShouldBalance g l ~ shouldbalance, BalanceableHelper shouldbalance g 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) - --- app :: RB a -> RB a -> RB a --- app E x = x --- app x E = x --- app (T R a x b) (T R c y d) = --- case app b c of --- T R b' z c' -> T R(T R a x b') z (T R c' y d) --- bc -> T R a x (T R bc y d) --- app (T B a x b) (T B c y d) = --- case app b c of --- T R b' z c' -> T R(T B a x b') z (T B c' y d) --- bc -> balleft a x (T B bc y d) --- app a (T R b x c) = T R (app a b) x c --- app (T R a x b) c = T R a x (app b c) - - -class Fuseable (l :: Map Symbol q) (r :: Map Symbol q) where - type Fuse l r :: Map Symbol q - 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 - --- app E x = x -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 - --- app x E = x -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 - --- app a (T R b x c) = T R (app a b) x c -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 - - --- app (T R a x b) c = T R a x (app b c) -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))) - - --- app (T R a x b) (T R c y d) = -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 q) (l :: Map Symbol q) (r :: Map Symbol q) where - type Fuse1 fused l r :: Map Symbol q - 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) - --- app (T R a x b) (T R c y d) = --- case app b c of --- T R b' z c' -> T R (T R a x b') z (T R c' y d) --- FIXME: The Fuseable constraint is repeated from avobe :( -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) - - --- app (T R a x b) (T R c y d) = --- case app b c of --- ... --- bc -> T R a x (T R bc y d) --- FIXME: The Fuseable constraint is repeated from above :( -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) - --- app (T R a x b) (T R c y d) = --- case app b c of --- ... --- bc -> T R a x (T R bc y d) -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) - --- app (T B a x b) (T B c y d) = -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) - --- could FuseableHelper1 and FuseableHelper2 be, well... fused? -class FuseableHelper2 (fused :: Map Symbol q) (l :: Map Symbol q) (r :: Map Symbol q) where - type Fuse2 fused l r :: Map Symbol q - 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) - --- app (T B a x b) (T B c y d) = --- case app b c of --- T R b' z c' -> T R (T B a x b') z (T B c' y d) -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) - --- app (T B a x b) (T B c y d) = --- case app b c of --- ... --- bc -> balleft a x (T B bc y d) -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)) - --- app (T B a x b) (T B c y d) = --- case app b c of --- ... --- bc -> balleft a x (T B bc y d) -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)) - - --- del E = E --- del (T _ a y b) --- | x<y = delformLeft a y b --- | x>y = delformRight a y b --- | otherwise = app a b -class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where - type Del k v t :: Map Symbol q - del :: Record f t -> Record f (Del k v t) - win :: Variant f t -> Either (Variant f (Del k v t)) (f v) - --- delformLeft a@(T B _ _ _) y b = balleft (del a) y b --- delformLeft a y b = T R (del a) y b --- In the term-level code, the k to delete is already on the environment. -class DelableL (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where - type DelL k v l kx vx r :: Map Symbol q - 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) - --- delformLeft a@(T B _ _ _) y b = balleft (del a) y b -instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableL deleted 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) - --- delformLeft a y b = T R (del a) y b -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) - --- delformLeft a y b = T R (del a) y b -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) - --- delformRight a y b@(T B _ _ _) = balright a y (del b) --- delformRight a y b = T R a y (del b) -class DelableR (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where - type DelR k v l kx vx r :: Map Symbol q - 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) - --- delformRight a y b@(T B _ _ _) = balright a y (del b) -instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableR left kx vx deleted) - => 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)) - --- delformRight a y b = T R a y (del b) -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) - --- delformRight a y b = T R a y (del b) -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) - --- del E = E -instance Delable k v E where - type Del k v E = E - del _ = unit - win = impossible - --- the color is discarded --- del (T _ a y b) --- | x<y = delformLeft a y b --- | x>y = delformRight a y b --- | otherwise = app a b -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 :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where - type Del' ordering k v l kx vx r :: Map Symbol q - 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) - --- | x<y = delformLeft a y b -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 - --- | otherwise = app a b -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) - --- | x>y = delformRight a y b -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 that determines if the pair of a 'Symbol' key and a type can - be deleted from a type-level map. - - The associated type family 'Delete' produces the resulting map. - - At the term level, this manifests in 'delete', which removes a field from - a record, and in 'winnow', which checks if a 'Variant' is of a given - branch and returns the value in the branch if there's a match, or a - reduced 'Variant' if there isn't. 'winnow' tends to be more useful in - practice. - - If the map already has the key but with a /different/ type, the deletion - fails to compile. - -} -class Deletable (k :: Symbol) (v :: q) (t :: Map Symbol q) where - type Delete k v t :: Map Symbol q - _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, Del k v t ~ deleted, CanMakeBlack deleted) => 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) - -{- | - Removes a field from a 'Record'. - -} -delete :: forall k v t f . Deletable k v t => Record f t -> Record f (Delete k v t) -delete = _delete @_ @k @v @t - -{- | - Checks if a 'Variant' is of a given branch and returns the value in the - branch if there's a match, or a reduced 'Variant' if there isn't. - -} -winnow :: forall k v t f . Deletable k v t => Variant f t -> Either (Variant f (Delete k v t)) (f v) -winnow = _winnow @_ @k @v @t - -{- | Like 'winnow' but specialized to pure 'Variant's. - ->>> winnow @"bar" @Bool (injectI @"bar" False :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) -Right (I False) - ->>> prettyShowVariantI `first` winnow @"foo" @Char (injectI @"bar" False :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) -Left "bar (False)" - --} -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 - --- The original term-level code, taken from: --- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html --- --- {- Version 1, 'untyped' -} --- data Color = R | B deriving Show --- data RB a = E | T Color (RB a) a (RB a) deriving Show --- --- {- Insertion and membership test as by Okasaki -} --- insert :: Ord a => a -> RB a -> RB a --- insert x s = --- T B a z b --- where --- T _ a z b = ins s --- ins E = T R E x E --- ins s@(T B a y b) --- | x<y = balance (ins a) y b --- | x>y = balance a y (ins b) --- | otherwise = s --- ins s@(T R a y b) --- | x<y = T R (ins a) y b --- | x>y = T R a y (ins b) --- | otherwise = s --- --- --- {- balance: first equation is new, --- to make it work with a weaker invariant -} --- balance :: RB a -> a -> RB a -> RB a --- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d) --- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d) --- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d) --- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d) --- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d) --- balance a x b = T B a x b --- --- member :: Ord a => a -> RB a -> Bool --- member x E = False --- member x (T _ a y b) --- | x<y = member x a --- | x>y = member x b --- | otherwise = True --- --- {- deletion a la SMK -} --- delete :: Ord a => a -> RB a -> RB a --- delete x t = --- case del t of {T _ a y b -> T B a y b; _ -> E} --- where --- del E = E --- del (T _ a y b) --- | x<y = delformLeft a y b --- | x>y = delformRight a y b --- | otherwise = app a b --- delformLeft a@(T B _ _ _) y b = balleft (del a) y b --- delformLeft a y b = T R (del a) y b --- --- delformRight a y b@(T B _ _ _) = balright a y (del b) --- delformRight a y b = T R a y (del b) --- --- balleft :: RB a -> a -> RB a -> RB a --- balleft (T R a x b) y c = T R (T B a x b) y c --- balleft bl x (T B a y b) = balance bl x (T R a y b) --- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c)) --- --- balright :: RB a -> a -> RB a -> RB a --- balright a x (T R b y c) = T R a x (T B b y c) --- balright (T B a x b) y bl = balance (T R a x b) y bl --- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) --- --- sub1 :: RB a -> RB a --- sub1 (T B a x b) = T R a x b --- sub1 _ = error "invariance violation" --- --- app :: RB a -> RB a -> RB a --- app E x = x --- app x E = x --- app (T R a x b) (T R c y d) = --- case app b c of --- T R b' z c' -> T R (T R a x b') z (T R c' y d) --- bc -> T R a x (T R bc y d) --- app (T B a x b) (T B c y d) = --- case app b c of --- T R b' z c' -> T R(T B a x b') z (T B c' y d) --- bc -> balleft a x (T B bc y d) --- app a (T R b x c) = T R (app a b) x c --- app (T R a x b) c = T R a x (app b c) - +-- | See <https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html here> for+-- the original term-level code by Stefan Kahrs. It is also copied at the end+-- of this file. Some parts of the type-level code include the correspondign+-- term-level parts in their comments.+{-# 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.Functor.Contravariant (Contravariant(contramap))+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,(:.:)(..),Top)+import Data.SOP.NP (collapse_NP,liftA_NP,liftA2_NP,cliftA_NP,cliftA2_NP,pure_NP,sequence_NP,sequence'_NP)+import Data.SOP.NS (collapse_NS,ap_NS,injections,Injection)+++{- $setup+ +>>> :set -XDataKinds -XTypeApplications -XPartialTypeSignatures -XFlexibleContexts -XTypeFamilies -XDeriveGeneric +>>> :set -Wno-partial-type-signatures +>>> import Data.RBR+>>> import Data.SOP+>>> import GHC.Generics++-}+++-- | The color of a node.+data Color = R+ | B+ deriving (Show,Eq)++-- | A Red-Black tree. It will be used as a kind, to index the 'Record' and 'Variant' types.+data Map symbol q = E + | N Color (Map symbol q) symbol q (Map symbol q)+ deriving (Show,Eq)++-- | A map without entries. See also 'unit' and 'impossible'.+type Empty = E++--+--+-- This code has been copied and adapted from the corresponding Data.SOP code (the All constraint).+--++-- Why is this KeysValuesAllF type family needed at all? Why is not KeysValuesAll sufficient by itself?+-- In fact, if I delete KeysValuesAllF and use eclusively KeysValuesAll, functions like demoteKeys seem to still work fine.+--+-- UndecidableSuperClasses and RankNTypes seem to be required by KeysValuesAllF.+type family+ KeysValuesAllF (c :: symbol -> q -> Constraint) (t :: Map symbol q) :: Constraint where+ KeysValuesAllF _ E = ()+ KeysValuesAllF c (N color left k v right) = (c k v, KeysValuesAll c left, KeysValuesAll c right)++{- | Require a constraint for every key-value pair in a tree. This is a generalization of 'Data.SOP.All' from "Data.SOP".+-}+class KeysValuesAllF c t => KeysValuesAll (c :: symbol -> q -> Constraint) (t :: Map symbol q) where++ -- 'cpara_Map' constructs a 'Record' by means of a constraint for producing+ -- the nodes of the tree. The constraint is passed as a 'Data.Proxy.Proxy'.+ 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++{- | This typeclass provides generalizations of 'Applicative'-like functions+ - which work over 'Record's and 'Variant's.+-}+class Maplike (t :: Map Symbol Type) where+ {- | + See 'cpure_Record' and 'cpure'_Record' for more useful versions of+ this function.++ The naming scheme follows that of 'Data.SOP.NP.pure_NP'.+ -}+ pure_Record :: (forall v. f v) -> Record f t+ {- | + Pulls out an 'Applicative' that wraps each field, resulting in an 'Applicative' containing a pure 'Record'.++ The naming scheme follows that of 'Data.SOP.NP.sequence_NP'.+ -}+ sequence_Record :: Applicative f => Record f t -> f (Record I t)+ {- | + Like 'sequence_Record', but only pulls out the outer 'Applicative'+ from an 'Applicative' composition that wraps each field. See '(:.:)'.++ This can be useful for staged computations, where each stage is+ represented by an 'Applicative' layer.++ The naming scheme follows that of 'Data.SOP.NP.sequence'_NP'.+ -}+ sequence'_Record :: Applicative f => Record (f :.: g) t -> f (Record g t)+ {- | Apply a transformation to the type constructor which wraps the fields of a 'Record'.+ + The naming scheme follows that of 'Data.SOP.NP.liftA_NP'.+ -}+ liftA_Record :: (forall a. f a -> g a) -> Record f t -> Record g t+ {- | + The naming scheme follows that of 'Data.SOP.NP.liftA2_NP'.+ -}+ liftA2_Record :: (forall a. f a -> g a -> h a) -> Record f t -> Record g t -> Record h t+ {- | Apply a transformation to the active branch of a 'Variant'.+ + The naming scheme follows that of 'Data.SOP.NS.liftA_NS'.+ -}+ liftA_Variant :: (forall a. f a -> g a) -> Variant f t -> Variant g t+ {- | Given a 'Record' of transformation, apply the one which matches the active branch of 'Variant'.+ + The naming scheme follows that of 'Data.SOP.NS.liftA_NS'.+ -}+ liftA2_Variant :: (forall a. f a -> g a -> h a) -> Record f t -> Variant g t -> Variant h t+ {- | + Construct a 'Record' made of functions which take a value of the+ field's type and inject it in the 'Variant' branch which corresponds+ to the field.+ -}+ injections_Variant :: Record (VariantInjection f t) t+ {- | Collapse a 'Record' composed of 'K' monoidal annotations.+ + >>> collapse'_Record (unit :: Record (K [Bool]) Empty)+ []++ >>> collapse'_Record (insert @"bar" (K [False]) unit)+ [False]++ The naming scheme follows that of 'Data.SOP.NP.collapse_NP'.++ -}+ collapse'_Record :: Monoid a => Record (K a) t -> a+ collapse_Variant :: Variant (K a) t -> a++instance Maplike E where+ pure_Record _ = Empty+ sequence_Record Empty = pure Empty+ sequence'_Record Empty = pure Empty+ liftA_Record _ Empty = Empty+ liftA2_Record _ Empty Empty = Empty+ liftA_Variant _ neverHappens = impossible neverHappens+ liftA2_Variant _ Empty neverHappens = impossible neverHappens+ injections_Variant = Empty+ collapse'_Record Empty = mempty+ collapse_Variant = impossible++instance (Maplike left, Maplike right) => Maplike (N color left k v right) where+ pure_Record f = Node (pure_Record f) f (pure_Record f)+ sequence_Record (Node left v right) = (\l x r -> Node l (I x) r) <$> sequence_Record left <*> v <*> sequence_Record right+ sequence'_Record (Node left (Comp v) right) = (\l x r -> Node l x r) <$> sequence'_Record left <*> v <*> sequence'_Record right+ liftA_Record trans (Node left1 v1 right1) = Node (liftA_Record trans left1) (trans v1) (liftA_Record trans right1)+ liftA2_Record trans (Node left1 v1 right1) (Node left2 v2 right2) = Node (liftA2_Record trans left1 left2) (trans v1 v2) (liftA2_Record trans right1 right2)+ liftA_Variant trans vv = case vv of+ Here fv -> Here (trans fv)+ LookLeft leftV -> LookLeft (liftA_Variant trans leftV)+ LookRight rightV -> LookRight (liftA_Variant trans rightV)+ liftA2_Variant trans (Node left rv right) vv = case vv of+ Here fv -> Here (trans rv fv)+ LookLeft leftV -> LookLeft (liftA2_Variant trans left leftV)+ LookRight rightV -> LookRight (liftA2_Variant trans right rightV)+ injections_Variant = + let injections_Left = liftA_Record (\(VariantInjection j) -> VariantInjection $ LookLeft . j) (injections_Variant @left)+ injections_Right = liftA_Record (\(VariantInjection j) -> VariantInjection $ LookRight . j) (injections_Variant @right)+ in Node injections_Left (VariantInjection $ Here) injections_Right+ collapse'_Record (Node left (K v) right) = collapse'_Record left <> (v <> collapse'_Record right) + collapse_Variant vv = case vv of+ Here (K a) -> a+ LookLeft leftV -> collapse_Variant leftV+ LookRight rightV -> collapse_Variant rightV++{- |+ A function which takes the value of a field and injects it into the corresponding branch of a 'Variant'.++ See also 'Data.SOP.NS.Injection'.+ -}+newtype VariantInjection (f :: q -> Type) (t :: Map Symbol q) (v :: q) = VariantInjection { runVariantInjection :: f v -> Variant f 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)++{- |+ Create a 'Record', knowing that both keys and values satisfy a 2-place constraint. The constraint is passed as a 'Data.Proxy.Proxy'.++ The naming scheme follows that of 'Data.SOP.NP.cpure_NP'.+ -}+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 ++{- |+ Create a 'Record', knowing that the keys can be demoted to strings and that+ the values satisfy some constraint. The constraint is passed as a+ 'Data.Proxy.Proxy'.++ The fuction that constructs each field receives the name of the field as an+ argument.++ The naming scheme follows that of 'Data.SOP.NP.cpure_NP'.+ -}+cpure'_Record :: forall c t f. KeysValuesAll (KeyValueConstraints KnownSymbol c) t => (Proxy c) -> (forall v. c v => String -> f v) -> Record f t+cpure'_Record _ fpure = cpara_Map (Proxy @(KeyValueConstraints KnownSymbol c)) unit go+ where+ go :: forall left k' v' right color. (KeyValueConstraints KnownSymbol c k' v', KeysValuesAll (KeyValueConstraints KnownSymbol c) left, KeysValuesAll (KeyValueConstraints KnownSymbol c) right) + => Record f left+ -> Record f right+ -> Record f (N color left k' v' right)+ go left right = Node left (fpure @v' (symbolVal (Proxy @k'))) right +++{- | Create a 'Record' containing the names of each field. + + The names are represented by a constant functor 'K' carrying an annotation+ of type 'String'. This means that there aren't actually any values of the+ type that corresponds to each field, only the 'String' annotations.++>>> putStrLn $ prettyShow_Record show $ demoteKeys @(Insert "foo" Char (Insert "bar" Bool Empty))+{bar = K "bar", foo = K "foo"}++ For computations involving field names, sometimes 'cpure\'_Record' is a better option.++-} +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 ++{- |+ Two-place constraint saying that a 'Symbol' key can be demoted to 'String'. Nothing is required from the corresponding value.++ Defined using the "class synonym" <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ trick>.+-}+class KnownSymbol k => KnownKey (k :: Symbol) (v :: q)+instance KnownSymbol k => KnownKey k v +++{- | + Create a record containing the names of each field along with a term-level+ representation of each type.++>>> putStrLn $ prettyShow_Record show $ demoteEntries @(Insert "foo" Char (Insert "bar" Bool Empty))+{bar = K ("bar",Bool), foo = K ("foo",Char)}++ See also 'collapse_Record' for getting the entries as a list.+-}+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 ++{- |+ Two-place constraint saying that a 'Symbol' key can be demoted to 'String', and that the corresponding value 'Type' has a term-level representation. ++ Defined using the "class synonym" <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ trick>.+-}+class (KnownSymbol k, Typeable v) => KnownKeyTypeableValue (k :: Symbol) (v :: q)+instance (KnownSymbol k, Typeable v) => KnownKeyTypeableValue k v ++{- |+ Lifts two one-place constraints (one for keys, one for values) to a two-place constraint. Useful with function like 'cpure_Record'.++ Defined using the "class synonym" <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ trick>.+-}+class (kc k, vc v) => KeyValueConstraints (kc :: Symbol -> Constraint) (vc :: q -> Constraint) (k :: Symbol) (v :: q)+instance (kc k, vc v) => KeyValueConstraints kc vc k v++{- |+ Lifts a one-place constraint for values to a two-place constraint. Useful with function like 'cpure_Record'.++ Defined using the "class synonym" <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ trick>.+-}+class (vc v) => ValueConstraint (vc :: q -> Constraint) (k :: Symbol) (v :: q)+instance (vc v) => ValueConstraint vc k v++--+--++{- | An extensible product-like type with named fields.+ + The values in the 'Record' come wrapped in a type constructor @f@, which+ por pure records will be the identity functor 'I'.++ See also 'insert', 'delete' and 'project'.+-}+data Record (f :: q -> Type) (t :: Map Symbol q) 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) ++ ")"+++{-# DEPRECATED collapse_Record "Use collapse'_Record" #-}+collapse_Record :: forall t result a. (Productlike '[] t result) => Record (K a) t -> [a]+collapse_Record = collapse_NP . toNP+++{- | Show a 'Record' in a friendlier way than the default 'Show' instance. The+ function argument will usually be 'show', but it can be used to unwrap the+ value of each field before showing it.+-}+prettyShow_Record :: forall t f. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) + => (forall x. Show x => f x -> String) + -> Record f t + -> String+prettyShow_Record showf r = + let showfs = cpure'_Record (Proxy @Show) $ \fieldName -> Comp (fieldName, Case showf)+ entries = liftA2_Record (\(Comp (fieldName,Case f)) fv -> K [ fieldName ++ " = " ++ f fv ]) showfs r+ in "{" ++ mconcat (intersperse ", " (collapse'_Record entries)) ++ "}"+++{- | Like 'prettyShow_Record' but specialized to pure records.+-}+prettyShow_RecordI :: forall t. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) => Record I t -> String+prettyShow_RecordI r = prettyShow_Record (show . unI) r +++{-# DEPRECATED prettyShowRecord "Use prettyShow_Record" #-}+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)) ++ "}"+++{-# DEPRECATED prettyShowRecordI "Use prettyShow_RecordI" #-}+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 ++{-| A Record without components is a boring, uninformative type whose single value can be conjured out of thin air.+-}+unit :: Record f Empty+unit = Empty++{- | An extensible sum-like type with named branches.+ + The values in the 'Variant' come wrapped in a type constructor @f@, which+ por pure variants will be the identity functor 'I'.++ See also 'widen', 'winnow' and 'inject'.+-}+data Variant (f :: q -> Type) (t :: Map Symbol q) 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) ++ ")"++{-| A Variant without branches doesn't have any values. From an impossible thing, anything can come out. +-}+impossible :: Variant f Empty -> b+impossible v = case v of+++{- | Show a 'Variant' in a friendlier way than the default 'Show' instance. The+ function argument will usually be 'show', but it can be used to unwrap the+ value of the branch before showing it.+-}+prettyShow_Variant :: forall t flat f. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t)+ => (forall x. Show x => f x -> String) + -> Variant f t + -> String+prettyShow_Variant showf v = + let showfs = cpure'_Record (Proxy @Show) $ \fieldName -> Comp (fieldName, Case showf)+ entries = liftA2_Variant (\(Comp (fieldName,Case f)) fv -> K (fieldName ++ " (" ++ f fv ++ ")")) showfs v+ in collapse_Variant entries++{- | Like 'prettyShow_Variant' but specialized to pure variants.+-}+prettyShow_VariantI :: forall t flat. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t)+ => Variant I t -> String+prettyShow_VariantI v = prettyShow_Variant (show . unI) v +++{-# DEPRECATED prettyShowVariant "Use prettyShow_Variant" #-}+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)++{-# DEPRECATED prettyShowVariantI "Use prettyShow_VariantI" #-}+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 ++--+--+-- Insertion++{- | Insert a list of type level key / value pairs into a type-level map. +-}+type family InsertAll (es :: [(Symbol,q)]) (t :: Map Symbol q) :: Map Symbol q where+ InsertAll '[] t = t+ InsertAll ( '(name,fieldType) ': es ) t = Insert name fieldType (InsertAll es t)++{- | Build a type-level map out of a list of type level key / value pairs. +-}+type FromList (es :: [(Symbol,q)]) = InsertAll es Empty+++{- |+ Adds a new field to a 'Record'.++>>> project @"foo" (insert @"foo" (I 'a') unit)+I 'a'++>>> project @"foo" (insert @"foo" @Char Nothing unit)+Nothing++ -}+insert :: forall k v t f. Insertable k v t => f v -> Record f t -> Record f (Insert k v t)+insert = _insert @_ @k @v @t @f++{- |+ Lets you use a 'Variant' in a bigger context+ than the one in which is was defined. + -}+widen :: forall k v t f. Insertable k v t => Variant f t -> Variant f (Insert k v t)+widen = _widen @_ @k @v @t @f++{- | Alias for 'insert'. +-}+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++{- | Like 'insert' but specialized to pure 'Record's.+ +>>> projectI @"foo" (insertI @"foo" 'a' unit)+'a'++-}+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++{- | Like 'addField' but specialized to pure 'Record's.+-}+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 that determines if the pair of a 'Symbol' key and a type can+ be inserted into a type-level map.+ + The associated type family 'Insert' produces the resulting map.++ At the term level, this manifests in 'insert', which adds a new field to a+ record, and in 'widen', which lets you use a 'Variant' in a bigger context+ than the one in which is was defined. 'insert' tends to be more useful in+ practice.++ If the map already has the key but with a /different/ type, the+ insertion fails to compile.+ -}+class Insertable (k :: Symbol) (v :: q) (t :: Map Symbol q) where+ type Insert k v t :: Map Symbol q+ _insert :: f v -> Record f t -> Record f (Insert k v t)+ _widen :: Variant f t -> Variant f (Insert k v t)++-- insert x s =+-- T B a z b+-- where+-- T _ a z b = ins s+instance (InsertableHelper1 k v t, Insert1 k v t ~ inserted, CanMakeBlack inserted) => 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 k) where+ type MakeBlack t :: Map Symbol k+ 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 :: q) + (t :: Map Symbol q) where+ type Insert1 k v t :: Map Symbol q + 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+ -- FIXME possible duplicate work with CmpSymbol: both in constraint and in associated type family. + -- Is that bad? How to avoid it?+ 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 :: q) + (color :: Color) + (left :: Map Symbol q) + (k' :: Symbol) + (v' :: q) + (right :: Map Symbol q) where+ type Insert2 ordering k v color left k' v' right :: Map Symbol q + 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)++-- ins s@(T B a y b)+-- | x<y = balance (ins a) y b+instance (InsertableHelper1 k v left, Insert1 k v left ~ inserted,+ Balanceable inserted 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++-- ins s@(T B a y b)+-- | x<y = balance (ins a) y b+instance (InsertableHelper1 k v left, Insert1 k v left ~ inserted,+ Balanceable inserted 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+++-- This instance implies that we can't change the type associated to an+-- existing key. If we did that, we wouldn't be able to widen Variants that+-- happen to match that key!+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++-- ins s@(T B a y b)+-- | ...+-- | x>y = balance a y (ins b)+instance (InsertableHelper1 k v right, Insert1 k v right ~ inserted,+ Balanceable left k' v' inserted+ )+ => 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)++-- ins s@(T R a y b)+-- | ...+-- | x>y = T R a y (ins b)+instance (InsertableHelper1 k v right, Insert1 k v right ~ inserted,+ Balanceable left k' v' inserted+ )+ => 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 q) (k :: Symbol) (v :: q) (right :: Map Symbol q) where+ type Balance left k v right :: Map Symbol q+ 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+ -- FIXME possible duplicate work with ShouldBalance: both in constraint and in associated type family. + -- Is that bad? How to avoid it?+ 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 q) + (k :: Symbol) + (v :: q) + (right :: Map Symbol q) where+ type Balance' action left k v right :: Map Symbol q+ 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)++-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d)+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)++-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)+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)++-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)+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)++-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)+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)+++-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)+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)++-- balance a x b = T B a x b+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+++--+--+-- Accessing fields++--+-- These two type families exist to avoid duplicating expensive type-level+-- computations, in particular the Value' computations.+--+-- Record accessors are compiled WAY slower without them!+--+{- | Auxiliary type family to avoid repetition and help improve compilation times.+ -}+type family Field (f :: q -> Type) (t :: Map Symbol q) (v :: q) where+ Field f t v = Record f t -> (f v -> Record f t, f v)++{- | Auxiliary type family to avoid repetition and help improve compilation times.+ -}+type family Branch (f :: q -> Type) (t :: Map Symbol q) (v :: q) where+ Branch f t v = (Variant f t -> Maybe (f v), f v -> Variant f t)++--+{- | + Class that determines if a given 'Symbol' key is present in a type-level+ map.++ The 'Value' type family gives the 'Type' corresponding to the key.+-} +class Key (k :: Symbol) (t :: Map Symbol q) where+ type Value k t :: q+ _field :: Field f t (Value k t)+ _branch :: Branch f t (Value k t)++{- |+ Takes a field name (given through @TypeApplications@) and a+ 'Record', and returns a pair of a setter for the field and the original+ value of the field.+-}+field :: forall k t f. Key k t => Field f t (Value k t)+field = _field @_ @k @t++{- |+ Takes a branch name (given through @TypeApplications@) and+ returns a pair of a match function and a constructor.+-}+branch :: forall k t f. Key k t => Branch f t (Value k t)+branch = _branch @_ @k @t++-- member :: Ord a => a -> RB a -> Bool+class KeyHelper (ordering :: Ordering) (k :: Symbol) (left :: Map Symbol q) (v :: q) (right :: Map Symbol q) where + type Value' ordering k left v right :: q+ 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++-- | x<y = member x a+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))++-- | x>y = member x b+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))++-- | otherwise = True+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)++{- | Get the value of a field for a 'Record'. +++-}+project :: forall k t f . Key k t => Record f t -> f (Value k t)+project = snd . field @k @t++{- | Alias for 'project'.+-}+getField :: forall k t f . Key k t => Record f t -> f (Value k t)+getField = project @k @t @f++{- | Set the value of a field for a 'Record'. +-}+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++{- | Modify the value of a field for a 'Record'. +-}+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))++{- | Put a value into the branch of a 'Variant'.++>>> match @"foo" (inject @"foo" (I 'a') :: Variant I (Insert "foo" Char Empty))+Just (I 'a')++-}+inject :: forall k t f. Key k t => f (Value k t) -> Variant f t+inject = snd (branch @k @t)++{- | Check if a 'Variant' value is the given branch.+-}+match :: forall k t f. Key k t => Variant f t -> Maybe (f (Value k t))+match = fst (branch @k @t)++{- | Like 'project' but specialized to pure 'Record's.++>>> projectI @"foo" (insertI @"foo" 'a' (insertI @"bar" False unit))+'a'++-}+projectI :: forall k t . Key k t => Record I t -> Value k t+projectI = unI . snd . field @k @t++{- | Like 'getField' but specialized to pure 'Record's.+-}+getFieldI :: forall k t . Key k t => Record I t -> Value k t+getFieldI = projectI @k @t++{- | Like 'setField' but specialized to pure 'Record's.+-}+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)++{- | Like 'modifyField' but specialized to pure 'Record's.+-}+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)++{- | Like 'inject' but specialized to pure 'Variant's.+ +>>> matchI @"foo" (injectI @"foo" 'a' :: Variant I (Insert "foo" Char Empty))+Just 'a'++-}+injectI :: forall k t. Key k t => Value k t -> Variant I t+injectI = snd (branch @k @t) . I++{- | Like 'match' but specialized to pure 'Variants's.+-}+matchI :: forall k t . Key k t => Variant I t -> Maybe (Value k t)+matchI v = unI <$> fst (branch @k @t) v++{-# DEPRECATED eliminate "Use eliminate_Variant instead." #-}+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)) ++{- | Process a 'Variant' using a eliminator 'Record' that carries+ handlers for each possible branch of the 'Variant'.++>>> eliminate_Variant (addCaseI @"foo" @Int succ (addCaseI @"bar" pred unit)) (injectI @"bar" 33)+32++-}+eliminate_Variant :: Maplike t => Record (Case f r) t -> Variant f t -> r+eliminate_Variant cases variant = + let adapt (Case f) x = K (f x) + in collapse_Variant $ liftA2_Variant adapt cases variant++{- | Represents a handler for a branch of a 'Variant'. +-}+newtype Case f a b = Case (f b -> a)++instance Functor f => Contravariant (Case f a) where+ contramap g (Case c) = Case (c . fmap g)++{- | A form of 'addField' for creating eliminators for 'Variant's.+-}+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)++{- | A pure version of 'addCase'.+-}+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))++--+--+-- Subsetting++newtype SetField f a b = SetField { getSetField :: f b -> a -> a }+ +{- | For a given 'Map', produces a two-place constraint confirming the presence+ - of a entry.+ -+ Defined using the "class synonym" <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ trick>.+-}+class (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol q) (k :: Symbol) (v :: q) +instance (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol q) (k :: Symbol) (v :: q)++{-# DEPRECATED ProductlikeSubset "This constraint is obsolete" #-}+type ProductlikeSubset (subset :: Map Symbol q) (whole :: Map Symbol q) (flat :: [q]) = + (KeysValuesAll (PresentIn whole) subset,+ Productlike '[] subset flat,+ SListI flat)++{-# DEPRECATED fieldSubset "Use Data.RBR.Subset.fieldSubset" #-}+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)++{-# DEPRECATED projectSubset "Use Data.RBR.Subset.projectSubset" #-}+projectSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) + => Record f whole + -> Record f subset+projectSubset = snd . fieldSubset++{-# DEPRECATED getFieldSubset "Use Data.RBR.Subset.getFieldSubset" #-}+getFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) + => Record f whole + -> Record f subset+getFieldSubset = projectSubset++{-# DEPRECATED setFieldSubset "Use Data.RBR.Subset.setFieldSubset" #-}+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 ++{-# DEPRECATED modifyFieldSubset "Use Data.RBR.Subset.modifyFieldSubset" #-}+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))+++{-# DEPRECATED SumlikeSubset "This constraint is obsolete" #-}+type SumlikeSubset (subset :: Map Symbol q) (whole :: Map Symbol q) (subflat :: [q]) (wholeflat :: [q]) = + (KeysValuesAll (PresentIn whole) subset,+ Productlike '[] whole wholeflat,+ Sumlike '[] whole wholeflat,+ SListI wholeflat,+ Productlike '[] subset subflat,+ Sumlike '[] subset subflat,+ SListI subflat)++{-# DEPRECATED branchSubset "Use Data.RBR.Subset.branchSubset" #-}+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))))+ -- 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 = 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)+++{-# DEPRECATED injectSubset "Use Data.RBR.Subset.injectSubset" #-}+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)++{-# DEPRECATED matchSubset "Use Data.RBR.Subset.matchSubset" #-}+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)++{-# DEPRECATED eliminateSubset "Use Data.RBR.Subset.eliminateSubset" #-}+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 ++--+-- Interaction with Data.SOP++{- | Class from converting 'Record's to and from the n-ary product type 'NP' from "Data.SOP".+ + 'prefixNP' flattens a 'Record' and adds it to the initial part of the product.++ 'breakNP' reconstructs a 'Record' from the initial part of the product and returns the unconsumed part.++ The functions 'toNP' and 'fromNP' are usually easier to use. +-}+class Productlike (start :: [k])+ (t :: Map Symbol k) + (result :: [k]) | 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)++{- | + Flattens a 'Record' and adds it to the initial part of the product.+-}+prefixNP:: forall start t result f. Productlike start t result => Record f t -> NP f start -> NP f result+prefixNP = _prefixNP @_ @start @t @result++{- | + Reconstructs a 'Record' from the initial part of the product and returns the unconsumed part.+-}+breakNP :: forall start t result f. Productlike start t result => NP f result -> (Record f t, NP f start)+breakNP = _breakNP @_ @start @t @result++{- | Convert a 'Record' into a n-ary product. The order of the elements in the+ product is not the order of insertion in the record.++>>> toNP (insertI @"foo" 'a' (insertI @"bar" True unit))+I True :* I 'a' :* Nil ++-}+toNP :: forall t result f. Productlike '[] t result => Record f t -> NP f result+toNP r = prefixNP r Nil++{- | Convert a n-ary product into a compatible 'Record'. Usually follows an invocation of 'toNP'. ++>>> prettyShow_RecordI . fromNP @(Insert "foo" _ (Insert "bar" _ Empty)) . toNP $ insertI @"foo" 'a' (insertI @"bar" True unit)+"{bar = True, foo = 'a'}"++-}+fromNP :: forall t result f. Productlike '[] t result => NP f result -> Record f t+fromNP np = let (r,Nil) = breakNP np in r++{- | Class from converting 'Variant's to and from the n-ary sum type 'NS' from "Data.SOP".+ + 'prefixNS' flattens a 'Variant' and adds it to the initial part of the sum.++ 'breakNS' reconstructs a 'Variant' from the initial part of the sum and returns the unconsumed part.++ The functions 'toNS' and 'fromNS' are usually easier to use. +-}+class Sumlike (start :: [k]) + (t :: Map Symbol k) + (result :: [k]) | 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)++{- | + + Flattens a 'Variant' and adds it to the initial part of the sum.+-}+prefixNS :: forall start t result f. Sumlike start t result => Either (NS f start) (Variant f t) -> NS f result +prefixNS = _prefixNS @_ @start @t @result++{- | + Reconstructs a 'Variant' from the initial part of the sum and returns the unconsumed part.+-}+breakNS :: forall start t result f. Sumlike start t result => NS f result -> Either (NS f start) (Variant f t)+breakNS = _breakNS @_ @start @t @result++{- | Convert a 'Variant' into a n-ary sum. + +>>> toNS (injectI @"foo" 'a' :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty)))+S (Z (I 'a')) ++-}+toNS :: forall t result f. Sumlike '[] t result => Variant f t -> NS f result+toNS = prefixNS . Right++{- | Convert a n-ary sum into a compatible 'Variant'. + +>>> prettyShow_VariantI $ fromNS @(Insert "foo" _ (Insert "bar" _ Empty)) . toNS $ (injectI @"foo" 'a' :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty)))+"foo ('a')"++-}+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++--+--+-- Interfacing with normal records++class ToRecord (r :: Type) where+ type RecordCode r :: Map Symbol Type+ -- https://stackoverflow.com/questions/22087549/defaultsignatures-and-associated-type-families/22088808+ 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)++{- |+ The naming scheme follows that of 'Generics.SOP.IsProductType'.+ -}+type IsRecordType (r :: Type) (t :: Map Symbol Type) = (G.Generic r, ToRecord r, RecordCode r ~ t, FromRecord r)++-- {- |+-- A version of 'fromRecord' which accepts 'Record' values with more fields than the target nominal record, and possibly in an incompatible order.+-- -}+-- fromRecordSuperset :: forall r subset whole flat. (FromRecord r, RecordCode r ~ subset, ProductlikeSubset subset whole flat) => Record I whole -> r+-- fromRecordSuperset = fromRecord @r . projectSubset @subset @whole @flat++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+ VariantCode' acc (C1 (G.MetaCons k _ _) G.U1) = Insert k () 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."++{- |+ The naming scheme follows that of 'Generics.SOP.IsProductType'.+ -}+type IsVariantType (v :: Type) (t :: Map Symbol Type) = (G.Generic v, ToVariant v, VariantCode v ~ t, FromVariant v)++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 (Key k t, Value k t ~ ()) + => FromVariantHelper t (C1 (G.MetaCons k x y) G.U1)+ where+ fromVariant' v = case matchI @k @t v of+ Just x -> Just (M1 G.U1)+ 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 (Key k t, Value k t ~ ()) =>+ ToVariantHelper t (C1 (G.MetaCons k x y) G.U1) where+ toVariant' (M1 G.U1) = injectI @k ()++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++--+--+-- deletion+--+--+--++type family DiscriminateBalL (l :: Map k v) (r :: Map k v) :: Bool where+ DiscriminateBalL (N R _ _ _ _) _ = False+ DiscriminateBalL _ _ = True++class BalanceableL (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where+ type BalL l k v r :: Map Symbol q+ 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 q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where+ type BalL' b l k v r :: Map Symbol q+ 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++-- balleft :: RB a -> a -> RB a -> RB a+-- balleft (T R a x b) y c = T R (T B a x b) y c+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++-- balleft bl x (T B a y b) = balance bl x (T R a y b)+-- the @(N B in the call to balance tree is misleading, as it is ingored...+instance (N R t2 z zv t3 ~ g, BalanceableHelper (ShouldBalance t1 g) t1 y yv g) => + 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'))++-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c))+instance (N R l k kv r ~ g, BalanceableHelper (ShouldBalance t3 g) t3 z zv g) => + 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)))+++-- balright :: RB a -> a -> RB a -> RB a+-- balright a x (T R b y c) = T R a x (T B b y c)+-- balright (T B a x b) y bl = balance (T R a x b) y bl+-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)+type family DiscriminateBalR (l :: Map k v) (r :: Map k v) :: Bool where+ DiscriminateBalR _ (N R _ _ _ _) = False+ DiscriminateBalR _ _ = True++class BalanceableR (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where+ type BalR l k v r :: Map Symbol q+ 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 q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where+ type BalR' b l k v r :: Map Symbol q+ 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++-- balright :: RB a -> a -> RB a -> RB a+-- balright a x (T R b y c) = T R a x (T B b y c)+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)++-- balright (T B a x b) y bl = balance (T R a x b) y bl+instance (N R t2 z zv t3 ~ g, ShouldBalance g t1 ~ shouldbalance, BalanceableHelper shouldbalance g 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)++-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)+instance (N R t2 u uv t3 ~ g, ShouldBalance g l ~ shouldbalance, BalanceableHelper shouldbalance g 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)++-- app :: RB a -> RB a -> RB a+-- app E x = x+-- app x E = x+-- app (T R a x b) (T R c y d) =+-- case app b c of+-- T R b' z c' -> T R(T R a x b') z (T R c' y d)+-- bc -> T R a x (T R bc y d)+-- app (T B a x b) (T B c y d) = +-- case app b c of+-- T R b' z c' -> T R(T B a x b') z (T B c' y d)+-- bc -> balleft a x (T B bc y d)+-- app a (T R b x c) = T R (app a b) x c+-- app (T R a x b) c = T R a x (app b c)+++class Fuseable (l :: Map Symbol q) (r :: Map Symbol q) where+ type Fuse l r :: Map Symbol q+ 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++-- app E x = x+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++-- app x E = x+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++-- app a (T R b x c) = T R (app a b) x c+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+++-- app (T R a x b) c = T R a x (app b c)+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)))+++-- app (T R a x b) (T R c y d) =+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 q) (l :: Map Symbol q) (r :: Map Symbol q) where+ type Fuse1 fused l r :: Map Symbol q+ 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)++-- app (T R a x b) (T R c y d) =+-- case app b c of+-- T R b' z c' -> T R (T R a x b') z (T R c' y d)+-- FIXME: The Fuseable constraint is repeated from avobe :(+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)+++-- app (T R a x b) (T R c y d) =+-- case app b c of+-- ...+-- bc -> T R a x (T R bc y d)+-- FIXME: The Fuseable constraint is repeated from above :(+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)++-- app (T R a x b) (T R c y d) =+-- case app b c of+-- ...+-- bc -> T R a x (T R bc y d)+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)++-- app (T B a x b) (T B c y d) = +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)++-- could FuseableHelper1 and FuseableHelper2 be, well... fused?+class FuseableHelper2 (fused :: Map Symbol q) (l :: Map Symbol q) (r :: Map Symbol q) where+ type Fuse2 fused l r :: Map Symbol q+ 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)++-- app (T B a x b) (T B c y d) = +-- case app b c of+-- T R b' z c' -> T R (T B a x b') z (T B c' y d)+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)++-- app (T B a x b) (T B c y d) = +-- case app b c of+-- ...+-- bc -> balleft a x (T B bc y d)+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))++-- app (T B a x b) (T B c y d) = +-- case app b c of+-- ...+-- bc -> balleft a x (T B bc y d)+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))+++-- del E = E+-- del (T _ a y b)+-- | x<y = delformLeft a y b+-- | x>y = delformRight a y b+-- | otherwise = app a b+class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where+ type Del k v t :: Map Symbol q+ del :: Record f t -> Record f (Del k v t)+ win :: Variant f t -> Either (Variant f (Del k v t)) (f v) ++-- delformLeft a@(T B _ _ _) y b = balleft (del a) y b+-- delformLeft a y b = T R (del a) y b+-- In the term-level code, the k to delete is already on the environment.+class DelableL (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where+ type DelL k v l kx vx r :: Map Symbol q+ 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) ++-- delformLeft a@(T B _ _ _) y b = balleft (del a) y b+instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableL deleted 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)++-- delformLeft a y b = T R (del a) y b+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)++-- delformLeft a y b = T R (del a) y b+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)++-- delformRight a y b@(T B _ _ _) = balright a y (del b)+-- delformRight a y b = T R a y (del b)+class DelableR (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where+ type DelR k v l kx vx r :: Map Symbol q+ 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) ++-- delformRight a y b@(T B _ _ _) = balright a y (del b)+instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableR left kx vx deleted) + => 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))++-- delformRight a y b = T R a y (del b)+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)++-- delformRight a y b = T R a y (del b)+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)++-- del E = E+instance Delable k v E where+ type Del k v E = E+ del _ = unit+ win = impossible++-- the color is discarded+-- del (T _ a y b)+-- | x<y = delformLeft a y b+-- | x>y = delformRight a y b+-- | otherwise = app a b+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 :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where+ type Del' ordering k v l kx vx r :: Map Symbol q+ 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) ++-- | x<y = delformLeft a y b+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 ++-- | otherwise = app a b+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)++-- | x>y = delformRight a y b+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 that determines if the pair of a 'Symbol' key and a type can+ be deleted from a type-level map.+ + The associated type family 'Delete' produces the resulting map.++ At the term level, this manifests in 'delete', which removes a field from+ a record, and in 'winnow', which checks if a 'Variant' is of a given+ branch and returns the value in the branch if there's a match, or a+ reduced 'Variant' if there isn't. 'winnow' tends to be more useful in+ practice.++ If the map already has the key but with a /different/ type, the deletion+ fails to compile.+ -}+class Deletable (k :: Symbol) (v :: q) (t :: Map Symbol q) where+ type Delete k v t :: Map Symbol q+ _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, Del k v t ~ deleted, CanMakeBlack deleted) => 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)++{- | + Removes a field from a 'Record'.+ -}+delete :: forall k v t f . Deletable k v t => Record f t -> Record f (Delete k v t)+delete = _delete @_ @k @v @t++{- | + Checks if a 'Variant' is of a given branch and returns the value in the+ branch if there's a match, or a reduced 'Variant' if there isn't. + -}+winnow :: forall k v t f . Deletable k v t => Variant f t -> Either (Variant f (Delete k v t)) (f v)+winnow = _winnow @_ @k @v @t ++{- | Like 'winnow' but specialized to pure 'Variant's.+ +>>> winnow @"bar" @Bool (injectI @"bar" False :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty)))+Right (I False)++>>> prettyShow_VariantI `first` winnow @"foo" @Char (injectI @"bar" False :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty)))+Left "bar (False)" ++-}+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++-- The original term-level code, taken from:+-- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html+--+-- {- Version 1, 'untyped' -}+-- data Color = R | B deriving Show+-- data RB a = E | T Color (RB a) a (RB a) deriving Show+-- +-- {- Insertion and membership test as by Okasaki -}+-- insert :: Ord a => a -> RB a -> RB a+-- insert x s =+-- T B a z b+-- where+-- T _ a z b = ins s+-- ins E = T R E x E+-- ins s@(T B a y b)+-- | x<y = balance (ins a) y b+-- | x>y = balance a y (ins b)+-- | otherwise = s+-- ins s@(T R a y b)+-- | x<y = T R (ins a) y b+-- | x>y = T R a y (ins b)+-- | otherwise = s+-- +-- +-- {- balance: first equation is new,+-- to make it work with a weaker invariant -}+-- balance :: RB a -> a -> RB a -> RB a+-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d)+-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)+-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)+-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)+-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)+-- balance a x b = T B a x b+--+-- member :: Ord a => a -> RB a -> Bool+-- member x E = False+-- member x (T _ a y b)+-- | x<y = member x a+-- | x>y = member x b+-- | otherwise = True+-- +-- {- deletion a la SMK -}+-- delete :: Ord a => a -> RB a -> RB a+-- delete x t =+-- case del t of {T _ a y b -> T B a y b; _ -> E}+-- where+-- del E = E+-- del (T _ a y b)+-- | x<y = delformLeft a y b+-- | x>y = delformRight a y b+-- | otherwise = app a b+-- delformLeft a@(T B _ _ _) y b = balleft (del a) y b+-- delformLeft a y b = T R (del a) y b+--+-- delformRight a y b@(T B _ _ _) = balright a y (del b)+-- delformRight a y b = T R a y (del b)+-- +-- balleft :: RB a -> a -> RB a -> RB a+-- balleft (T R a x b) y c = T R (T B a x b) y c+-- balleft bl x (T B a y b) = balance bl x (T R a y b)+-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c))+-- +-- balright :: RB a -> a -> RB a -> RB a+-- balright a x (T R b y c) = T R a x (T B b y c)+-- balright (T B a x b) y bl = balance (T R a x b) y bl+-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)+-- +-- sub1 :: RB a -> RB a+-- sub1 (T B a x b) = T R a x b+-- sub1 _ = error "invariance violation"+-- +-- app :: RB a -> RB a -> RB a+-- app E x = x+-- app x E = x+-- app (T R a x b) (T R c y d) =+-- case app b c of+-- T R b' z c' -> T R (T R a x b') z (T R c' y d)+-- bc -> T R a x (T R bc y d)+-- app (T B a x b) (T B c y d) = +-- case app b c of+-- T R b' z c' -> T R(T B a x b') z (T B c' y d)+-- bc -> balleft a x (T B bc y d)+-- app a (T R b x c) = T R (app a b) x c+-- app (T R a x b) c = T R a x (app b c)+
+ lib/Data/RBR/Subset.hs view
@@ -0,0 +1,208 @@+{-| + 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'.+ + __Edit:__ 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 (+ Subset,+ fieldSubset,+ projectSubset,+ getFieldSubset,+ setFieldSubset,+ modifyFieldSubset,+ branchSubset,+ injectSubset,+ matchSubset, + eliminateSubset,+ fromRecordSuperset+ ) 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 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 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)+++++{- | 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 @(Insert "foo" _ (Insert "bar" _ Empty)) (insertI @"foo" 'a' (insertI @"bar" True (insertI @"baz" (Just ()) unit)))+"{bar = True, foo = 'a'}"++ Can 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 = snd . fieldSubset++{- | Alias for 'projectSubset'.+-}+getFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) + => Record f whole + -> Record f subset+getFieldSubset = 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 subset whole = fst (fieldSubset whole) 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 f r = uncurry ($) (fmap f (fieldSubset @subset @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 = + let inj2case = \adapt (VariantInjection vif) -> Case $ \fv -> adapt (vif fv) -- (\fv -> adapt (fromNS @t (unK (apFn fn 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 = fieldSubset @subset @whole+ in+ (,)+ (let injs :: Record (Case f (Maybe (Variant f subset))) subset + injs = liftA_Record (inj2case Just) (injections_Variant @subset)+ -- fixme: possibly inefficient?+ 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)++{- | 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 = snd (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 = fst (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 cases = + let reducedCases = getFieldSubset @subset @whole cases+ in eliminate_Variant 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 = fromRecord . projectSubset+
red-black-record.cabal view
@@ -1,77 +1,78 @@-cabal-version: 2.0 -name: red-black-record -version: 2.1.0.3 -synopsis: Extensible records and variants indexed by a type-level Red-Black tree. - -description: A library that provides extensible records and variants, - both indexed by a type-level red-black tree that maps - Symbol keys to value types of any kind. - . - The keys correspond to fields - names in records, and to branch names in variants. - . - At the term level, value types come wrapped in a type - constructor of kind @q -> Type@, where @q@ is the kind of - value types. - . - The records and variants can be converted to and from - regular Haskell datatypes; also to and from the unlabelled - n-ary products and sums of the @sop-core@ package. - -license: BSD3 -license-file: LICENSE -author: Daniel Diaz -maintainer: diaz_carrete@yahoo.com -category: Data -extra-source-files: CHANGELOG.md, - README.md -build-type: Simple - -source-repository head - type: git - location: https://github.com/danidiaz/red-black-record.git - -library - exposed-modules: Data.RBR - Data.RBR.Internal - Data.RBR.Examples - build-depends: base >= 4.10.0.0 && < 5, - sop-core >= 0.4.0.0 && < 0.6 - hs-source-dirs: lib - default-language: Haskell2010 - -library demoted - exposed-modules: Data.RBR.Demoted - build-depends: base >= 4.10.0.0 && < 5, - sop-core >= 0.4.0.0 && < 0.6, - red-black-record - hs-source-dirs: lib-demoted - default-language: Haskell2010 - -test-suite doctests - type: exitcode-stdio-1.0 - hs-source-dirs: tests - ghc-options: -threaded - main-is: doctests.hs - build-depends: base >= 4.10.0.0 && < 5, - sop-core >= 0.4.0.0 && < 0.6, - red-black-record, - aeson >= 1.4.0.0 && < 1.5, - bytestring >= 0.10, - text >= 1.1, - profunctors >= 5, - doctest >= 0.16.2 - default-language: Haskell2010 - -test-suite tests - type: exitcode-stdio-1.0 - hs-source-dirs: tests - main-is: tests.hs - build-depends: - base >= 4.10.0.0 && < 5, - sop-core >= 0.4.0.0 && < 0.6, - tasty >= 0.10.1.1, - tasty-hunit >= 0.9.2, - red-black-record, - demoted - default-language: Haskell2010 +cabal-version: 2.0+name: red-black-record+version: 2.1.1.0+synopsis: Extensible records and variants indexed by a type-level Red-Black tree.++description: A library that provides extensible records and variants,+ both indexed by a type-level red-black tree that maps+ Symbol keys to value types of any kind. + .+ The keys correspond to fields+ names in records, and to branch names in variants.+ . + At the term level, value types come wrapped in a type+ constructor of kind @q -> Type@, where @q@ is the kind of+ value types.+ .+ The records and variants can be converted to and from+ regular Haskell datatypes; also to and from the unlabelled+ n-ary products and sums of the @sop-core@ package.++license: BSD3+license-file: LICENSE+author: Daniel Diaz+maintainer: diaz_carrete@yahoo.com+category: Data+extra-source-files: CHANGELOG.md,+ README.md+build-type: Simple++source-repository head+ type: git+ location: https://github.com/danidiaz/red-black-record.git++library+ exposed-modules: Data.RBR+ Data.RBR.Subset+ Data.RBR.Internal+ Data.RBR.Examples+ build-depends: base >= 4.10.0.0 && < 5,+ sop-core >= 0.4.0.0 && < 0.6+ hs-source-dirs: lib+ default-language: Haskell2010++library demoted+ exposed-modules: Data.RBR.Demoted+ build-depends: base >= 4.10.0.0 && < 5,+ sop-core >= 0.4.0.0 && < 0.6,+ red-black-record+ hs-source-dirs: lib-demoted+ default-language: Haskell2010++test-suite doctests+ type: exitcode-stdio-1.0+ hs-source-dirs: tests+ ghc-options: -threaded+ main-is: doctests.hs+ build-depends: base >= 4.10.0.0 && < 5,+ sop-core >= 0.4.0.0 && < 0.6,+ red-black-record,+ aeson >= 1.4.0.0 && < 1.5,+ bytestring >= 0.10,+ text >= 1.1,+ profunctors >= 5,+ doctest >= 0.16.2+ default-language: Haskell2010++test-suite tests+ type: exitcode-stdio-1.0+ hs-source-dirs: tests+ main-is: tests.hs+ build-depends:+ base >= 4.10.0.0 && < 5,+ sop-core >= 0.4.0.0 && < 0.6,+ tasty >= 0.10.1.1,+ tasty-hunit >= 0.9.2,+ red-black-record,+ demoted+ default-language: Haskell2010
tests/doctests.hs view
@@ -1,7 +1,8 @@-import Test.DocTest - -main = doctest ["-ilib", - "lib/Data/RBR.hs", - "lib/Data/RBR/Internal.hs", - "lib/Data/RBR/Examples.hs" - ] +import Test.DocTest++main = doctest ["-ilib", + "lib/Data/RBR.hs",+ "lib/Data/RBR/Subset.hs",+ "lib/Data/RBR/Examples.hs",+ "lib/Data/RBR/Internal.hs"+ ]
tests/tests.hs view
@@ -1,555 +1,556 @@-{-# LANGUAGE DataKinds, - TypeOperators, - TypeFamilies, - TypeApplications, - DeriveGeneric, - StandaloneDeriving, - UndecidableInstances, - KindSignatures, - PartialTypeSignatures, - FlexibleContexts, - ScopedTypeVariables -#-} -{-# OPTIONS_GHC -Wno-partial-type-signatures #-} -module Main where - -import Data.RBR -import Data.RBR.Demoted (emptyMap,DemotableMap(demoteMap),t_insert,t_delete) -import Data.SOP -import Data.SOP.NP (cpure_NP,collapse_NP) -import Data.Typeable -import Data.Proxy -import GHC.TypeLits -import Data.Kind -import GHC.Generics (Generic) - -import Test.Tasty -import Test.Tasty.HUnit (testCase,Assertion,assertEqual,assertBool) - - -main :: IO () -main = defaultMain tests - -tests :: TestTree -tests = testGroup "Tests" [ testCase "recordGetSet01" testRecordGetSet01, - testCase "variantInjectMatch01" testVariantInjectMatch01, - testCase "projectSubset01" testProjectSubset01, - testGroup "nominalConversion" [ - testCase "toRecord01" testToRecord01, - testCase "fromRecord01" testFromRecord01, - testCase "toVariant01" testToVariant01, - testCase "toVariant02Units" testToVariant02Units, - testCase "fromVariant01" testFromVariant01, - testCase "fromVariant02Units" testFromVariant02Units - ], - testGroup "deletion" [ - testGroup "records" [ - testCase "recordDeletionSingleElem" testRecordDeletionSingleElem, - testCase "recordDeletionLeftElem" testRecordDeletionLeftElem, - testCase "recordDeletionRightElem" testRecordDeletionRightElem - ], - testGroup "variants" [ - testCase "variantDeletionSingleElem" testVariantDeletionSingleElem, - testCase "variantDeletionLeftElem" testVariantDeletionLeftElem, - testCase "variantDeletionRightElem" testVariantDeletionRightElem, - testCase "variantDeletion3Elem" testVariantDeletion3Elem, - testCase "variantDeletionMany" testVariantDeletionMany, - testCase "variantDeletionManyB" testVariantDeletionManyB - ] - ], - testGroup "typeLevelTermLvel" [ - testCase "tandem01" testInTandem01, - testCase "tandem02" testInTandem02, - testCase "tandem03" testInTandem03, - testCase "tandem04" testInTandem04 - ], - testGroup "polyKindedMap" [ - testCase "polyKinded01" polyKinded01, - testCase "polyKinded02" polyKinded02 - ] - ] - - -testRecordGetSet01 :: Assertion -testRecordGetSet01 = do - let r = insertI @"bfoo" 'c' - . insertI @"bbar" True - . insertI @"bbaz" (1::Int) - . insertI @"afoo" 'd' - . insertI @"abar" False - . insertI @"abaz" (2::Int) - . insertI @"zfoo" 'x' - . insertI @"zbar" False - . insertI @"zbaz" (4::Int) - . insertI @"dfoo" 'z' - . insertI @"dbar" True - . insertI @"dbaz" (5::Int) - . insertI @"fbaz" (6::Int) - $ unit - s = setFieldI @"fbaz" 9 (setFieldI @"zfoo" 'k' r) - assertEqual "bfoo" (getFieldI @"bfoo" s) 'c' - assertEqual "bbar" (getFieldI @"bbar" s) True - assertEqual "bbaz" (getFieldI @"bbaz" s) (1::Int) - assertEqual "afoo" (getFieldI @"afoo" s) 'd' - assertEqual "abar" (getFieldI @"abar" s) False - assertEqual "abaz" (getFieldI @"abaz" s) (2::Int) - assertEqual "zfoo" (getFieldI @"zfoo" s) 'k' - assertEqual "zbar" (getFieldI @"zbar" s) False - assertEqual "zbaz" (getFieldI @"zbaz" s) (4::Int) - assertEqual "dfoo" (getFieldI @"dfoo" s) 'z' - assertEqual "dbar" (getFieldI @"dbar" s) True - assertEqual "dbaz" (getFieldI @"dbaz" s) (5::Int) - assertEqual "fbaz" (getFieldI @"fbaz" s) (9::Int) - return () - -type Tree01 = FromList [ '("bfoo",Char), - '("bbar",Bool), - '("bbaz",Int), - '("afoo",Char), - '("abar",Bool), - '("abaz",Int), - '("zfoo",Char), - '("zbar",Bool), - '("zbaz",Int), - '("dfoo",Char), - '("dbar",Bool), - '("dbaz",Int), - '("fbaz",Int), - '("kgoz",Int) ] - -testVariantInjectMatch01 :: Assertion -testVariantInjectMatch01 = do - let r0 = injectI @"bfoo" @Tree01 'c' - r1 = injectI @"bbar" @Tree01 True - r2 = injectI @"bbaz" @Tree01 (1::Int) - r3 = injectI @"afoo" @Tree01 'd' - r4 = injectI @"abar" @Tree01 False - r5 = injectI @"abaz" @Tree01 (2::Int) - r6 = injectI @"zfoo" @Tree01 'x' - r7 = injectI @"zbar" @Tree01 False - r8 = injectI @"zbaz" @Tree01 (4::Int) - r9 = injectI @"dfoo" @Tree01 'z' - r10 = injectI @"dbar" @Tree01 True - r11 = injectI @"dbaz" @Tree01 (5::Int) - r12 = injectI @"fbaz" @Tree01 (6::Int) - r13 = injectI @"kgoz" @Tree01 (9::Int) - assertEqual "bfoo" (matchI @"bfoo" r0 ) $ Just 'c' - assertEqual "bbar" (matchI @"bbar" r1 ) $ Just True - assertEqual "bbaz" (matchI @"bbaz" r2 ) $ Just (1::Int) - assertEqual "afoo" (matchI @"afoo" r3 ) $ Just 'd' - assertEqual "abar" (matchI @"abar" r4 ) $ Just False - assertEqual "abaz" (matchI @"abaz" r5 ) $ Just (2::Int) - assertEqual "zfoo" (matchI @"zfoo" r6 ) $ Just 'x' - assertEqual "zbar" (matchI @"zbar" r7 ) $ Just False - assertEqual "zbaz" (matchI @"zbaz" r8 ) $ Just (4::Int) - assertEqual "dfoo" (matchI @"dfoo" r9 ) $ Just 'z' - assertEqual "dbar" (matchI @"dbar" r10) $ Just True - assertEqual "dbaz" (matchI @"dbaz" r11) $ Just (5::Int) - assertEqual "fbaz" (matchI @"fbaz" r12) $ Just (6::Int) - assertEqual "kgoz" (matchI @"kgoz" r13) $ Just (9::Int) - return () - - -testProjectSubset01 :: Assertion -testProjectSubset01 = do - let r = insertI @"foo" 'c' - . insertI @"bar" True - . insertI @"baz" (1::Int) - $ unit - s = projectSubset @(FromList '[ '("bar",_), - '("baz",_) ]) r - bar = getFieldI @"bar" s - baz = getFieldI @"baz" s - assertEqual "bar" bar True - assertEqual "baz" baz 1 - -data Person = Person { name :: String, age :: Int, whatever :: Char } deriving (Generic,Eq,Show) - -instance ToRecord Person -instance FromRecord Person - -testToRecord01 :: Assertion -testToRecord01 = do - let r = toRecord (Person "Foo" 50 'z') - assertEqual "name" "Foo" (getFieldI @"name" r) - assertEqual "age" 50 (getFieldI @"age" r) - assertEqual "whatever" 'z' (getFieldI @"whatever" r) - -testFromRecord01 :: Assertion -testFromRecord01 = do - let r = insertI @"name" "Foo" - . insertI @"age" 50 - . insertI @"whatever" 'z' - $ unit - assertEqual "person" (Person "Foo" 50 'z') (fromRecord r) - -data Variant01 = Variant01A Int - | Variant01B Char - | Variant01C Bool - | Variant01D Bool - deriving (Generic,Eq,Show) - -instance ToVariant Variant01 -instance FromVariant Variant01 - -testToVariant01 :: Assertion -testToVariant01 = do - let val1 = Variant01A 0 - val2 = Variant01B 'c' - val3 = Variant01C True - cases = addCaseI @"Variant01A" (const 'F') - . addCaseI @"Variant01B" id - . addCaseI @"Variant01C" (const 'F') - . addCaseI @"Variant01D" (const 'F') - $ unit - variant = toVariant (Variant01B 'T') - -- Eliminate would also work because the order of the eliminators is the - -- same as the order of the cases. - assertEqual "T" 'T' (eliminateSubset cases variant) - -data Variant02Unit = - Variant02A - | Variant02B Char - | Variant02C deriving (Generic,Eq,Show) - -instance ToVariant Variant02Unit -instance FromVariant Variant02Unit - -testToVariant02Units :: Assertion -testToVariant02Units = do - let cases = addCaseI @"Variant02A" (const 'a') - . addCaseI @"Variant02B" id - . addCaseI @"Variant02C" (const 'c') - $ unit - variantA = toVariant Variant02A - variantB = toVariant (Variant02B 'b') - variantC = toVariant Variant02C - -- Eliminate would also work because the order of the eliminators is the - -- same as the order of the cases. - assertEqual "a" 'a' (eliminateSubset cases variantA) - assertEqual "b" 'b' (eliminateSubset cases variantB) - assertEqual "c" 'c' (eliminateSubset cases variantC) - -testFromVariant01 :: IO () -testFromVariant01 = do - let val1 = fromVariant (injectI @"Variant01A" 1) - val2 = fromVariant (injectI @"Variant01B" 'z') - val3 = fromVariant (injectI @"Variant01C" True) - val4 = fromVariant (injectI @"Variant01D" False) - assertEqual "Variant01A" val1 (Variant01A 1) - assertEqual "Variant01B" val2 (Variant01B 'z') - assertEqual "Variant01C" val3 (Variant01C True) - assertEqual "Variant01D" val4 (Variant01D False) - -testFromVariant02Units :: IO () -testFromVariant02Units = do - let val1 = fromVariant (injectI @"Variant02A" ()) - val2 = fromVariant (injectI @"Variant02B" 'b') - val3 = fromVariant (injectI @"Variant02C" ()) - assertEqual "Variant02A" val1 Variant02A - assertEqual "Variant02B" val2 (Variant02B 'b') - assertEqual "Variant02C" val3 Variant02C - -testRecordDeletionSingleElem :: IO () -testRecordDeletionSingleElem = do - let r = insertI @"bar" False - . insertI @"foo" 'c' - . delete @"foo" @Bool - . insertI @"foo" True - $ unit - assertEqual "foo" (getFieldI @"foo" r) 'c' - assertEqual "bar" (getFieldI @"bar" r) False - -testVariantDeletionSingleElem :: IO () -testVariantDeletionSingleElem = do - let v = injectI @"foo" @(FromList '[ '("foo",Bool) ]) False - Right r = winnowI @"foo" @Bool v - assertEqual "foo" False r - -testRecordDeletionRightElem :: IO () -testRecordDeletionRightElem = do - let r = delete @"foo" @Char - . insertI @"foo" 'f' - . insertI @"bar" 'b' - $ unit - assertEqual "bar" (getFieldI @"bar" r) 'b' - -testVariantDeletionRightElem :: IO () -testVariantDeletionRightElem = do - let v = injectI @"foo" @(FromList '[ '("foo",Bool), '("bar",Char) ]) False - Left v' = winnowI @"bar" @Char v - Right r = winnowI @"foo" @Bool v' - assertEqual "foo" False r - -testRecordDeletionLeftElem :: IO () -testRecordDeletionLeftElem = do - let r = delete @"bar" @Char - . insertI @"foo" 'f' - . insertI @"bar" 'b' - $ unit - assertEqual "foo" (getFieldI @"foo" r) 'f' - -testVariantDeletionLeftElem :: IO () -testVariantDeletionLeftElem = do - let v = injectI @"bar" @(FromList '[ '("foo",Bool), '("bar",Char) ]) 'b' - Left v' = winnowI @"foo" @Bool v - Right r = winnowI @"bar" @Char v' - assertEqual "bar" 'b' r - -type TreeX3 = FromList [ '("bfoo",Char), - '("bbar",Bool), - '("bbaz",Int) ] - -testVariantDeletion3Elem :: IO () -testVariantDeletion3Elem = do - let v = injectI @"bbaz" @TreeX3 1 - Right r = winnowI @"bbaz" @Int v - assertEqual "bbaz" 1 r - - -type Tree02 = FromList [ - '("bfoo",Char), - '("bbar",Bool), - '("bbaz",Int), - '("afoo",Char), - '("abar",Bool), - '("abaz",Int), - '("zfoo",Char), - '("zbar",Bool), - '("zbaz",Int), - '("dfoo",Char), - '("dbar",Bool), - '("dbaz",Int), - '("fbaz",Int), - '("kgoz",Int) - ] - -testVariantDeletionMany :: IO () -testVariantDeletionMany = do - let a00 = injectI @"bfoo" @Tree02 'z' - Left a02 = winnowI @"bbar" @Bool a00 - Left a03 = winnowI @"bbaz" @Int a02 - Left a04 = winnowI @"afoo" @Char a03 - Left a05 = winnowI @"abar" @Bool a04 - Left a06 = winnowI @"abaz" @Int a05 - Left a07 = winnowI @"zfoo" @Char a06 - Left a08 = winnowI @"zbar" @Bool a07 - Left a09 = winnowI @"zbaz" @Int a08 - Left a10 = winnowI @"dfoo" @Char a09 - Left a11 = winnowI @"dbar" @Bool a10 - Left a12 = winnowI @"dbaz" @Int a11 - Left a13 = winnowI @"fbaz" @Int a12 - Left a14 = winnowI @"kgoz" @Int a13 - Right a = winnowI @"bfoo" @Char a14 - assertEqual "bfoo" a 'z' - return () - -type Tree02b = FromList [ - '("bfoo",Char), - '("bbar",Bool), - '("bbaz",Int), - '("afoo",Char), - '("abar",Bool), - '("abaz",Int), - '("zfoo",Char), - '("zbar",Bool), - '("zbaz",Int), - '("dfoo",Char), - '("dbar",Bool), - '("dbaz",Int), - '("fbaz",Int), - '("kgoz",Int) - ] - -testVariantDeletionManyB :: IO () -testVariantDeletionManyB = do - let a00 = injectI @"bfoo" @Tree02b 'z' - a00' = widen @"ggg" @Char a00 - Left a02 = winnowI @"bbar" @Bool a00 - Left a03 = winnowI @"bbaz" @Int a02 - Left a04 = winnowI @"afoo" @Char a03 - Left a05 = winnowI @"abar" @Bool a04 - Left a06 = winnowI @"abaz" @Int a05 - a06b = widen @"bbb" @Int a06 - Left a07 = winnowI @"zfoo" @Char a06b - Left a08 = winnowI @"zbar" @Bool a07 - Left a09 = winnowI @"zbaz" @Int a08 - Left a10 = winnowI @"dfoo" @Char a09 - Left a10b = winnowI @"zzz" @Float a10 -- non-existent entry - Right m = winnowI @"bfoo" @Char a10b - Left a11 = winnowI @"dbar" @Bool a10b - Left a12 = winnowI @"dbaz" @Int a11 - Left a13 = winnowI @"fbaz" @Int a12 - Left a14 = winnowI @"kgoz" @Int a13 - Left a15 = winnowI @"ggg" @Char a14 - Right a = winnowI @"bfoo" @Char a15 - assertEqual "bfoo" m 'z' - assertEqual "bfoo" a 'z' - return () - -type Actions01 = [Act In "f1" Bool, - Act In "f2" Char, - Act In "f3" Float, - Act In "f4" (Int -> Int), - Act In "f5" Bool, - Act In "f6" Char, - Act In "f7" String, - Act In "f8" (Char -> Char), - Act In "f9" Bool, - Act In "f10" Char, - Act In "f11" Float - ] - -testInTandem01 :: IO () -testInTandem01 = assertEqual "" (demoteMap (Proxy @(Perform Actions01))) (perform (demoteActions (Proxy @Actions01))) - -type Actions02 = [Act In "f11" Bool, - Act In "f10" Int, - Act In "f9" Char, - Act In "f8" (Char -> Char), - Act In "f7" Int, - Act In "f6" Char, - Act In "f5" Float, - Act In "f4" Int, - Act In "f3" (Char -> Int), - Act In "f2" Bool, - Act In "f1" Char - ] - -testInTandem02 :: IO () -testInTandem02 = assertEqual "" (demoteMap (Proxy @(Perform Actions02))) (perform (demoteActions (Proxy @Actions02))) - -type Actions03 = [Act In "ff1" Bool, - Act In "af2" Char, - Act In "wf3" Int, - Act In "uf4" Bool, - Act In "uf5" Char, - Act In "af6" Int, - Act In "pf7" Bool, - Act De "qf5" Char, - Act De "bf2" Char, - Act In "hf8" (Int -> Int), - Act De "mf4" Bool, - Act In "af9" Bool, - Act In "yf10" Char, - Act In "mf11" String, - Act De "zf3" Int - ] - -testInTandem03 :: IO () -testInTandem03 = assertEqual "" (demoteMap (Proxy @(Perform Actions03))) (perform (demoteActions (Proxy @Actions03))) - - -type Actions04 = [Act In "ef1" Bool, - Act In "ef2" Char, - Act De "ef3" Int, -- we can delete entries that don't exist - Act In "af3" Int, - Act De "af3" Int, - Act In "kf4" Bool, - Act De "kf4" Bool, - Act In "pf5" Char, - Act De "pf5" Char, - Act In "zf6" Int, - Act De "zf6" Int, - Act In "ff7" Bool, - Act De "ff7" Bool, - Act In "rf5" Char, - Act De "rf5" Char, - Act De "ef2" Char, - Act In "lf8" (Int -> Int), - Act In "lll" Bool, - Act De "lll" Bool, - Act De "lf8" (Int -> Int), - Act In "ef1" Bool, -- we can re-add the exact same entry - Act De "ef1" Bool - ] - -testInTandem04 :: IO () -testInTandem04 = assertEqual "" (demoteMap (Proxy @(Perform Actions04))) (perform (demoteActions (Proxy @Actions04))) - - --- sequences of actions for tests --- --- -data InsertOrDelete = In - | De - deriving (Show, Eq) - -class DemotableInsertOrDelete (iod :: InsertOrDelete) where - demoteIoD :: Proxy iod -> InsertOrDelete - -instance DemotableInsertOrDelete 'In where - demoteIoD _ = In - -instance DemotableInsertOrDelete 'De where - demoteIoD _ = De - -data Action s t = Act InsertOrDelete s t deriving (Show, Eq) - -class DemotableAction (a :: Action Symbol Type) where - demoteAction :: Proxy a -> Action String TypeRep - -instance (DemotableInsertOrDelete iod, KnownSymbol s, Typeable t) => DemotableAction (Act iod s t) where - demoteAction _ = Act (demoteIoD (Proxy @iod)) - (symbolVal (Proxy @s)) - (typeRep (Proxy @t)) - -demoteActions :: forall as. All DemotableAction as => Proxy (as :: [Action Symbol Type]) -> [Action String TypeRep] -demoteActions _ = collapse_NP $ cpure_NP @_ @as (Proxy @DemotableAction) conjure - where - conjure :: forall a. DemotableAction a => K (Action String TypeRep) a - conjure = K (demoteAction (Proxy @a)) - -type family Perform (as :: [Action Symbol Type]) :: Map Symbol Type where - Perform (Act In s v ': as) = Insert s v (Perform as) - Perform (Act De s v ': as) = Delete s v (Perform as) - Perform '[] = Empty - -perform :: [Action String TypeRep] -> Map String TypeRep -perform = foldr (\(Act iod s v) t -> case iod of In -> t_insert s v t - De -> t_delete s t) - emptyMap - --- --- --- - -type PolyKinded01 = FromList '[ '("aaa","v1"), - '("bbb","v2"), - '("ccc","v3"), - '("ddd","v4"), - '("eee","v5") ] - -polyKindedRecord01 :: Record Proxy PolyKinded01 -polyKindedRecord01 = - insert @"aaa" (Proxy @"v1") - . insert @"bbb" (Proxy @"v2") - . insert @"ccc" (Proxy @"v3") - . insert @"ddd" (Proxy @"v4") - . insert @"eee" (Proxy @"v5") - $ unit - -polyKinded01 :: Assertion -polyKinded01 = do - let r = insert @"aaa" (Proxy @"v1") - . insert @"bbb" (Proxy @"v2") - . insert @"ccc" (Proxy @"v3") - . insert @"ddd" (Proxy @"v4") - . insert @"eee" (Proxy @"v5") - . insert @"abb" (Proxy @"v2") - . insert @"acc" (Proxy @"v3") - . insert @"add" (Proxy @"v4") - . insert @"aee" (Proxy @"v5") - $ unit - proxy :: Proxy "v2" - proxy = getField @"abb" r - return () - -polyKinded02 :: Assertion -polyKinded02 = do - let r = demoteEntries @PolyKinded01 - K (_,trep) = getField @"eee" r - assertEqual "" trep (typeRep (Proxy @"v5")) - return () - - +{-# LANGUAGE DataKinds,+ TypeOperators,+ TypeFamilies,+ TypeApplications,+ DeriveGeneric,+ StandaloneDeriving,+ UndecidableInstances,+ KindSignatures,+ PartialTypeSignatures,+ FlexibleContexts,+ ScopedTypeVariables+#-}+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}+module Main where++import Data.RBR+import qualified Data.RBR.Subset as S+import Data.RBR.Demoted (emptyMap,DemotableMap(demoteMap),t_insert,t_delete) +import Data.SOP+import Data.SOP.NP (cpure_NP,collapse_NP)+import Data.Typeable+import Data.Proxy+import GHC.TypeLits+import Data.Kind+import GHC.Generics (Generic)++import Test.Tasty+import Test.Tasty.HUnit (testCase,Assertion,assertEqual,assertBool)+++main :: IO ()+main = defaultMain tests++tests :: TestTree+tests = testGroup "Tests" [ testCase "recordGetSet01" testRecordGetSet01,+ testCase "variantInjectMatch01" testVariantInjectMatch01,+ testCase "projectSubset01" testProjectSubset01,+ testGroup "nominalConversion" [+ testCase "toRecord01" testToRecord01,+ testCase "fromRecord01" testFromRecord01,+ testCase "toVariant01" testToVariant01,+ testCase "toVariant02Units" testToVariant02Units,+ testCase "fromVariant01" testFromVariant01,+ testCase "fromVariant02Units" testFromVariant02Units+ ],+ testGroup "deletion" [+ testGroup "records" [+ testCase "recordDeletionSingleElem" testRecordDeletionSingleElem,+ testCase "recordDeletionLeftElem" testRecordDeletionLeftElem,+ testCase "recordDeletionRightElem" testRecordDeletionRightElem+ ],+ testGroup "variants" [+ testCase "variantDeletionSingleElem" testVariantDeletionSingleElem,+ testCase "variantDeletionLeftElem" testVariantDeletionLeftElem,+ testCase "variantDeletionRightElem" testVariantDeletionRightElem,+ testCase "variantDeletion3Elem" testVariantDeletion3Elem,+ testCase "variantDeletionMany" testVariantDeletionMany, + testCase "variantDeletionManyB" testVariantDeletionManyB + ]+ ],+ testGroup "typeLevelTermLvel" [+ testCase "tandem01" testInTandem01,+ testCase "tandem02" testInTandem02,+ testCase "tandem03" testInTandem03,+ testCase "tandem04" testInTandem04+ ],+ testGroup "polyKindedMap" [+ testCase "polyKinded01" polyKinded01,+ testCase "polyKinded02" polyKinded02+ ]+ ]+++testRecordGetSet01 :: Assertion+testRecordGetSet01 = do+ let r = insertI @"bfoo" 'c'+ . insertI @"bbar" True+ . insertI @"bbaz" (1::Int)+ . insertI @"afoo" 'd'+ . insertI @"abar" False+ . insertI @"abaz" (2::Int)+ . insertI @"zfoo" 'x'+ . insertI @"zbar" False+ . insertI @"zbaz" (4::Int)+ . insertI @"dfoo" 'z'+ . insertI @"dbar" True+ . insertI @"dbaz" (5::Int)+ . insertI @"fbaz" (6::Int)+ $ unit+ s = setFieldI @"fbaz" 9 (setFieldI @"zfoo" 'k' r)+ assertEqual "bfoo" (getFieldI @"bfoo" s) 'c'+ assertEqual "bbar" (getFieldI @"bbar" s) True+ assertEqual "bbaz" (getFieldI @"bbaz" s) (1::Int)+ assertEqual "afoo" (getFieldI @"afoo" s) 'd'+ assertEqual "abar" (getFieldI @"abar" s) False+ assertEqual "abaz" (getFieldI @"abaz" s) (2::Int)+ assertEqual "zfoo" (getFieldI @"zfoo" s) 'k'+ assertEqual "zbar" (getFieldI @"zbar" s) False+ assertEqual "zbaz" (getFieldI @"zbaz" s) (4::Int)+ assertEqual "dfoo" (getFieldI @"dfoo" s) 'z'+ assertEqual "dbar" (getFieldI @"dbar" s) True+ assertEqual "dbaz" (getFieldI @"dbaz" s) (5::Int)+ assertEqual "fbaz" (getFieldI @"fbaz" s) (9::Int)+ return ()++type Tree01 = FromList [ '("bfoo",Char),+ '("bbar",Bool),+ '("bbaz",Int),+ '("afoo",Char),+ '("abar",Bool),+ '("abaz",Int),+ '("zfoo",Char),+ '("zbar",Bool),+ '("zbaz",Int),+ '("dfoo",Char),+ '("dbar",Bool),+ '("dbaz",Int),+ '("fbaz",Int),+ '("kgoz",Int) ]++testVariantInjectMatch01 :: Assertion+testVariantInjectMatch01 = do+ let r0 = injectI @"bfoo" @Tree01 'c'+ r1 = injectI @"bbar" @Tree01 True+ r2 = injectI @"bbaz" @Tree01 (1::Int)+ r3 = injectI @"afoo" @Tree01 'd'+ r4 = injectI @"abar" @Tree01 False+ r5 = injectI @"abaz" @Tree01 (2::Int)+ r6 = injectI @"zfoo" @Tree01 'x'+ r7 = injectI @"zbar" @Tree01 False+ r8 = injectI @"zbaz" @Tree01 (4::Int)+ r9 = injectI @"dfoo" @Tree01 'z'+ r10 = injectI @"dbar" @Tree01 True+ r11 = injectI @"dbaz" @Tree01 (5::Int)+ r12 = injectI @"fbaz" @Tree01 (6::Int)+ r13 = injectI @"kgoz" @Tree01 (9::Int)+ assertEqual "bfoo" (matchI @"bfoo" r0 ) $ Just 'c'+ assertEqual "bbar" (matchI @"bbar" r1 ) $ Just True+ assertEqual "bbaz" (matchI @"bbaz" r2 ) $ Just (1::Int)+ assertEqual "afoo" (matchI @"afoo" r3 ) $ Just 'd'+ assertEqual "abar" (matchI @"abar" r4 ) $ Just False+ assertEqual "abaz" (matchI @"abaz" r5 ) $ Just (2::Int)+ assertEqual "zfoo" (matchI @"zfoo" r6 ) $ Just 'x'+ assertEqual "zbar" (matchI @"zbar" r7 ) $ Just False+ assertEqual "zbaz" (matchI @"zbaz" r8 ) $ Just (4::Int)+ assertEqual "dfoo" (matchI @"dfoo" r9 ) $ Just 'z'+ assertEqual "dbar" (matchI @"dbar" r10) $ Just True+ assertEqual "dbaz" (matchI @"dbaz" r11) $ Just (5::Int)+ assertEqual "fbaz" (matchI @"fbaz" r12) $ Just (6::Int)+ assertEqual "kgoz" (matchI @"kgoz" r13) $ Just (9::Int)+ return ()+++testProjectSubset01 :: Assertion+testProjectSubset01 = do+ let r = insertI @"foo" 'c'+ . insertI @"bar" True+ . insertI @"baz" (1::Int)+ $ unit+ s = S.projectSubset @(FromList '[ '("bar",_),+ '("baz",_) ]) r+ bar = getFieldI @"bar" s+ baz = getFieldI @"baz" s+ assertEqual "bar" bar True+ assertEqual "baz" baz 1++data Person = Person { name :: String, age :: Int, whatever :: Char } deriving (Generic,Eq,Show)++instance ToRecord Person+instance FromRecord Person++testToRecord01 :: Assertion+testToRecord01 = do+ let r = toRecord (Person "Foo" 50 'z')+ assertEqual "name" "Foo" (getFieldI @"name" r)+ assertEqual "age" 50 (getFieldI @"age" r)+ assertEqual "whatever" 'z' (getFieldI @"whatever" r)++testFromRecord01 :: Assertion+testFromRecord01 = do+ let r = insertI @"name" "Foo"+ . insertI @"age" 50+ . insertI @"whatever" 'z'+ $ unit+ assertEqual "person" (Person "Foo" 50 'z') (fromRecord r)++data Variant01 = Variant01A Int+ | Variant01B Char+ | Variant01C Bool+ | Variant01D Bool+ deriving (Generic,Eq,Show)++instance ToVariant Variant01+instance FromVariant Variant01++testToVariant01 :: Assertion+testToVariant01 = do+ let val1 = Variant01A 0+ val2 = Variant01B 'c'+ val3 = Variant01C True+ cases = addCaseI @"Variant01A" (const 'F')+ . addCaseI @"Variant01B" id+ . addCaseI @"Variant01C" (const 'F')+ . addCaseI @"Variant01D" (const 'F')+ $ unit+ variant = toVariant (Variant01B 'T')+ -- Eliminate would also work because the order of the eliminators is the+ -- same as the order of the cases.+ assertEqual "T" 'T' (S.eliminateSubset cases variant)++data Variant02Unit = + Variant02A + | Variant02B Char + | Variant02C deriving (Generic,Eq,Show)++instance ToVariant Variant02Unit+instance FromVariant Variant02Unit++testToVariant02Units :: Assertion+testToVariant02Units = do+ let cases = addCaseI @"Variant02A" (const 'a')+ . addCaseI @"Variant02B" id+ . addCaseI @"Variant02C" (const 'c')+ $ unit+ variantA = toVariant Variant02A+ variantB = toVariant (Variant02B 'b')+ variantC = toVariant Variant02C+ -- Eliminate would also work because the order of the eliminators is the+ -- same as the order of the cases.+ assertEqual "a" 'a' (S.eliminateSubset cases variantA)+ assertEqual "b" 'b' (S.eliminateSubset cases variantB)+ assertEqual "c" 'c' (S.eliminateSubset cases variantC)++testFromVariant01 :: IO ()+testFromVariant01 = do+ let val1 = fromVariant (injectI @"Variant01A" 1)+ val2 = fromVariant (injectI @"Variant01B" 'z')+ val3 = fromVariant (injectI @"Variant01C" True)+ val4 = fromVariant (injectI @"Variant01D" False)+ assertEqual "Variant01A" val1 (Variant01A 1)+ assertEqual "Variant01B" val2 (Variant01B 'z')+ assertEqual "Variant01C" val3 (Variant01C True)+ assertEqual "Variant01D" val4 (Variant01D False)+ +testFromVariant02Units :: IO ()+testFromVariant02Units = do+ let val1 = fromVariant (injectI @"Variant02A" ())+ val2 = fromVariant (injectI @"Variant02B" 'b')+ val3 = fromVariant (injectI @"Variant02C" ())+ assertEqual "Variant02A" val1 Variant02A+ assertEqual "Variant02B" val2 (Variant02B 'b')+ assertEqual "Variant02C" val3 Variant02C++testRecordDeletionSingleElem :: IO ()+testRecordDeletionSingleElem = do+ let r = insertI @"bar" False+ . insertI @"foo" 'c'+ . delete @"foo" @Bool + . insertI @"foo" True+ $ unit+ assertEqual "foo" (getFieldI @"foo" r) 'c'+ assertEqual "bar" (getFieldI @"bar" r) False++testVariantDeletionSingleElem :: IO ()+testVariantDeletionSingleElem = do+ let v = injectI @"foo" @(FromList '[ '("foo",Bool) ]) False+ Right r = winnowI @"foo" @Bool v+ assertEqual "foo" False r++testRecordDeletionRightElem :: IO ()+testRecordDeletionRightElem = do+ let r = delete @"foo" @Char+ . insertI @"foo" 'f'+ . insertI @"bar" 'b'+ $ unit+ assertEqual "bar" (getFieldI @"bar" r) 'b'++testVariantDeletionRightElem :: IO ()+testVariantDeletionRightElem = do+ let v = injectI @"foo" @(FromList '[ '("foo",Bool), '("bar",Char) ]) False+ Left v' = winnowI @"bar" @Char v+ Right r = winnowI @"foo" @Bool v'+ assertEqual "foo" False r++testRecordDeletionLeftElem :: IO ()+testRecordDeletionLeftElem = do+ let r = delete @"bar" @Char+ . insertI @"foo" 'f'+ . insertI @"bar" 'b'+ $ unit+ assertEqual "foo" (getFieldI @"foo" r) 'f'++testVariantDeletionLeftElem :: IO ()+testVariantDeletionLeftElem = do+ let v = injectI @"bar" @(FromList '[ '("foo",Bool), '("bar",Char) ]) 'b'+ Left v' = winnowI @"foo" @Bool v+ Right r = winnowI @"bar" @Char v'+ assertEqual "bar" 'b' r++type TreeX3 = FromList [ '("bfoo",Char),+ '("bbar",Bool),+ '("bbaz",Int) ]++testVariantDeletion3Elem :: IO ()+testVariantDeletion3Elem = do+ let v = injectI @"bbaz" @TreeX3 1+ Right r = winnowI @"bbaz" @Int v+ assertEqual "bbaz" 1 r+++type Tree02 = FromList [ + '("bfoo",Char),+ '("bbar",Bool),+ '("bbaz",Int),+ '("afoo",Char),+ '("abar",Bool),+ '("abaz",Int),+ '("zfoo",Char),+ '("zbar",Bool),+ '("zbaz",Int),+ '("dfoo",Char),+ '("dbar",Bool),+ '("dbaz",Int),+ '("fbaz",Int),+ '("kgoz",Int) + ]++testVariantDeletionMany :: IO ()+testVariantDeletionMany = do+ let a00 = injectI @"bfoo" @Tree02 'z'+ Left a02 = winnowI @"bbar" @Bool a00+ Left a03 = winnowI @"bbaz" @Int a02+ Left a04 = winnowI @"afoo" @Char a03+ Left a05 = winnowI @"abar" @Bool a04+ Left a06 = winnowI @"abaz" @Int a05+ Left a07 = winnowI @"zfoo" @Char a06+ Left a08 = winnowI @"zbar" @Bool a07+ Left a09 = winnowI @"zbaz" @Int a08+ Left a10 = winnowI @"dfoo" @Char a09+ Left a11 = winnowI @"dbar" @Bool a10+ Left a12 = winnowI @"dbaz" @Int a11+ Left a13 = winnowI @"fbaz" @Int a12+ Left a14 = winnowI @"kgoz" @Int a13+ Right a = winnowI @"bfoo" @Char a14+ assertEqual "bfoo" a 'z'+ return ()++type Tree02b = FromList [ + '("bfoo",Char),+ '("bbar",Bool),+ '("bbaz",Int),+ '("afoo",Char),+ '("abar",Bool),+ '("abaz",Int),+ '("zfoo",Char),+ '("zbar",Bool),+ '("zbaz",Int),+ '("dfoo",Char),+ '("dbar",Bool),+ '("dbaz",Int),+ '("fbaz",Int),+ '("kgoz",Int) + ]++testVariantDeletionManyB :: IO ()+testVariantDeletionManyB = do+ let a00 = injectI @"bfoo" @Tree02b 'z'+ a00' = widen @"ggg" @Char a00+ Left a02 = winnowI @"bbar" @Bool a00+ Left a03 = winnowI @"bbaz" @Int a02+ Left a04 = winnowI @"afoo" @Char a03+ Left a05 = winnowI @"abar" @Bool a04+ Left a06 = winnowI @"abaz" @Int a05+ a06b = widen @"bbb" @Int a06+ Left a07 = winnowI @"zfoo" @Char a06b+ Left a08 = winnowI @"zbar" @Bool a07+ Left a09 = winnowI @"zbaz" @Int a08+ Left a10 = winnowI @"dfoo" @Char a09+ Left a10b = winnowI @"zzz" @Float a10 -- non-existent entry+ Right m = winnowI @"bfoo" @Char a10b+ Left a11 = winnowI @"dbar" @Bool a10b+ Left a12 = winnowI @"dbaz" @Int a11+ Left a13 = winnowI @"fbaz" @Int a12+ Left a14 = winnowI @"kgoz" @Int a13+ Left a15 = winnowI @"ggg" @Char a14+ Right a = winnowI @"bfoo" @Char a15+ assertEqual "bfoo" m 'z'+ assertEqual "bfoo" a 'z'+ return ()++type Actions01 = [Act In "f1" Bool,+ Act In "f2" Char,+ Act In "f3" Float,+ Act In "f4" (Int -> Int),+ Act In "f5" Bool,+ Act In "f6" Char,+ Act In "f7" String,+ Act In "f8" (Char -> Char),+ Act In "f9" Bool,+ Act In "f10" Char,+ Act In "f11" Float+ ]++testInTandem01 :: IO ()+testInTandem01 = assertEqual "" (demoteMap (Proxy @(Perform Actions01))) (perform (demoteActions (Proxy @Actions01)))+ +type Actions02 = [Act In "f11" Bool,+ Act In "f10" Int,+ Act In "f9" Char,+ Act In "f8" (Char -> Char),+ Act In "f7" Int,+ Act In "f6" Char,+ Act In "f5" Float,+ Act In "f4" Int,+ Act In "f3" (Char -> Int),+ Act In "f2" Bool,+ Act In "f1" Char+ ]++testInTandem02 :: IO ()+testInTandem02 = assertEqual "" (demoteMap (Proxy @(Perform Actions02))) (perform (demoteActions (Proxy @Actions02)))+ +type Actions03 = [Act In "ff1" Bool,+ Act In "af2" Char,+ Act In "wf3" Int,+ Act In "uf4" Bool,+ Act In "uf5" Char,+ Act In "af6" Int,+ Act In "pf7" Bool,+ Act De "qf5" Char,+ Act De "bf2" Char,+ Act In "hf8" (Int -> Int),+ Act De "mf4" Bool,+ Act In "af9" Bool,+ Act In "yf10" Char,+ Act In "mf11" String,+ Act De "zf3" Int+ ]++testInTandem03 :: IO ()+testInTandem03 = assertEqual "" (demoteMap (Proxy @(Perform Actions03))) (perform (demoteActions (Proxy @Actions03)))+++type Actions04 = [Act In "ef1" Bool,+ Act In "ef2" Char,+ Act De "ef3" Int, -- we can delete entries that don't exist+ Act In "af3" Int,+ Act De "af3" Int, + Act In "kf4" Bool,+ Act De "kf4" Bool,+ Act In "pf5" Char,+ Act De "pf5" Char,+ Act In "zf6" Int,+ Act De "zf6" Int,+ Act In "ff7" Bool,+ Act De "ff7" Bool,+ Act In "rf5" Char,+ Act De "rf5" Char,+ Act De "ef2" Char,+ Act In "lf8" (Int -> Int),+ Act In "lll" Bool,+ Act De "lll" Bool,+ Act De "lf8" (Int -> Int),+ Act In "ef1" Bool, -- we can re-add the exact same entry+ Act De "ef1" Bool+ ]++testInTandem04 :: IO ()+testInTandem04 = assertEqual "" (demoteMap (Proxy @(Perform Actions04))) (perform (demoteActions (Proxy @Actions04)))+++-- sequences of actions for tests+--+--+data InsertOrDelete = In+ | De + deriving (Show, Eq)++class DemotableInsertOrDelete (iod :: InsertOrDelete) where+ demoteIoD :: Proxy iod -> InsertOrDelete++instance DemotableInsertOrDelete 'In where+ demoteIoD _ = In++instance DemotableInsertOrDelete 'De where+ demoteIoD _ = De++data Action s t = Act InsertOrDelete s t deriving (Show, Eq)++class DemotableAction (a :: Action Symbol Type) where + demoteAction :: Proxy a -> Action String TypeRep++instance (DemotableInsertOrDelete iod, KnownSymbol s, Typeable t) => DemotableAction (Act iod s t) where+ demoteAction _ = Act (demoteIoD (Proxy @iod)) + (symbolVal (Proxy @s)) + (typeRep (Proxy @t))++demoteActions :: forall as. All DemotableAction as => Proxy (as :: [Action Symbol Type]) -> [Action String TypeRep] +demoteActions _ = collapse_NP $ cpure_NP @_ @as (Proxy @DemotableAction) conjure+ where + conjure :: forall a. DemotableAction a => K (Action String TypeRep) a+ conjure = K (demoteAction (Proxy @a))++type family Perform (as :: [Action Symbol Type]) :: Map Symbol Type where+ Perform (Act In s v ': as) = Insert s v (Perform as)+ Perform (Act De s v ': as) = Delete s v (Perform as)+ Perform '[] = Empty++perform :: [Action String TypeRep] -> Map String TypeRep+perform = foldr (\(Act iod s v) t -> case iod of In -> t_insert s v t+ De -> t_delete s t) + emptyMap++--+--+--++type PolyKinded01 = FromList '[ '("aaa","v1"),+ '("bbb","v2"), + '("ccc","v3"), + '("ddd","v4"), + '("eee","v5") ]++polyKindedRecord01 :: Record Proxy PolyKinded01+polyKindedRecord01 = + insert @"aaa" (Proxy @"v1")+ . insert @"bbb" (Proxy @"v2")+ . insert @"ccc" (Proxy @"v3")+ . insert @"ddd" (Proxy @"v4")+ . insert @"eee" (Proxy @"v5")+ $ unit++polyKinded01 :: Assertion+polyKinded01 = do+ let r = insert @"aaa" (Proxy @"v1")+ . insert @"bbb" (Proxy @"v2")+ . insert @"ccc" (Proxy @"v3")+ . insert @"ddd" (Proxy @"v4")+ . insert @"eee" (Proxy @"v5")+ . insert @"abb" (Proxy @"v2")+ . insert @"acc" (Proxy @"v3")+ . insert @"add" (Proxy @"v4")+ . insert @"aee" (Proxy @"v5")+ $ unit+ proxy :: Proxy "v2"+ proxy = getField @"abb" r+ return ()++polyKinded02 :: Assertion+polyKinded02 = do+ let r = demoteEntries @PolyKinded01+ K (_,trep) = getField @"eee" r+ assertEqual "" trep (typeRep (Proxy @"v5"))+ return ()++