diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,19 @@ +Copyright Li-yao Xia (c) 2018 + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the “Software”), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies +of the Software, and to permit persons to whom the Software is furnished to do +so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,69 @@ +# Surgery for generic data types [![Hackage](https://img.shields.io/hackage/v/generic-data-surgery.svg)](https://hackage.haskell.org/package/generic-data-surgery) [![Build Status](https://travis-ci.org/Lysxia/generic-data-surgery.svg)](https://travis-ci.org/Lysxia/generic-data-surgery) + +Modify, add, or remove constructors and fields in generic types, to be used +with generic implementations. + +## Example + +Here is a simple record type equipped with a `checksum` function: + +```haskell +data Foo = Foo { x, y, z :: Int } + deriving (Eq, Generic, Show) + +checksum :: Foo -> Checksum +``` + +Let's encode it as a JSON object with an extra `"checksum"` key, +looking like this, where `X`, `Y`, `Z` are integers: + +``` +{ "x": X +, "y": Y +, "z": Z +, "checksum": X + Y + Z +} +``` + +We use `genericParseJSON`/`genericToJSON` to convert between JSON values +and a generic 4-field record, and `removeRField`/`insertRField` to +convert between that generic 4-field record and the 3-field `Foo`. + +### Remove field + +When decoding, we check the checksum and then throw it away. + +```haskell +instance FromJSON Foo where + parseJSON v = do + + r <- genericParseJSON defaultOptions v + -- r: a generic 4-field record {x,y,z,checksum} (checksum at index 3). + + let (cs, f) = (fmap fromOR . removeRField @"checksum" @3 . toOR') r + -- removeRField @"checksum" @3: split out the checksum field + -- from the three other fields. (cs, f) :: (Checksum, Foo) + + if checksum f == cs then + pure f + else + fail "Checksum failed" +``` + +### Insert field + +When encoding, we must compute the checksum to write it out. We put the +checksum in a pair `(checksum f, f)` with the original record, and +`insertRField` can then wrap it into a 4-field record passed into +`genericToJSON`. + +```haskell +instance ToJSON Foo where + toJSON f = + (genericToJSON defaultOptions . fromOR' . insertRField @"checksum" @3 . fmap toOR) + (checksum f, f) +``` + +See also the +[`examples/`](https://github.com/Lysxia/generic-data-surgery/tree/master/examples) +directory in the source repo. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/generic-data-surgery.cabal b/generic-data-surgery.cabal new file mode 100644 --- /dev/null +++ b/generic-data-surgery.cabal @@ -0,0 +1,60 @@ +name: generic-data-surgery +version: 0.1.0.0 +synopsis: Surgery for generic data types +description: + Transform data types before passing them to generic functions. +homepage: https://github.com/Lysxia/generic-data-surgery#readme +license: MIT +license-file: LICENSE +author: Li-yao Xia +maintainer: lysxia@gmail.com +copyright: 2018 Li-yao Xia +category: Other +build-type: Simple +extra-source-files: README.md +cabal-version: >=1.10 +tested-with: + GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.1, GHC == 8.6.2 + +library + hs-source-dirs: src + exposed-modules: + Generic.Data.Surgery + Generic.Data.Surgery.Internal + build-depends: + generic-data >= 0.2, + first-class-families >= 0.2, + base >= 4.9 && < 5 + ghc-options: -Wall + default-language: Haskell2010 + +test-suite surgery-test + hs-source-dirs: test + main-is: surgery.hs + build-depends: + tasty, + tasty-hunit, + generic-data, + generic-data-surgery, + base + ghc-options: -Wall + default-language: Haskell2010 + type: exitcode-stdio-1.0 + +test-suite lens-surgery-test + hs-source-dirs: test + main-is: lens-surgery.hs + build-depends: + tasty, + tasty-hunit, + generic-data-surgery, + generic-lens, + base + ghc-options: -Wall + default-language: Haskell2010 + type: exitcode-stdio-1.0 + buildable: False + +source-repository head + type: git + location: https://github.com/Lysxia/generic-data-surgery diff --git a/src/Generic/Data/Surgery.hs b/src/Generic/Data/Surgery.hs new file mode 100644 --- /dev/null +++ b/src/Generic/Data/Surgery.hs @@ -0,0 +1,122 @@ +-- | Surgery for generic data types: +-- remove and insert constructors and fields. +-- +-- Functions in this module are expected to be used with visible type +-- applications. Surgeries have a lot of type parameters, but usually only the +-- first one to three type arguments need to be passed via @TypeApplications@. +-- Functions are annotated with \"functional dependencies\", with a meaning +-- similar to the homonymous GHC extension for type classes (click on +-- \"Details\" under each function to see those). +-- +-- Remember that not all parameters to the left of a functional dependency +-- arrow need to be annotated explicitly to determine those on the right. Some +-- can also be inferred from the context. +-- +-- Note that constructors and fields are indexed from zero. + +module Generic.Data.Surgery + ( Data + + , toData + , fromData + , onData + + -- Microsurgery + + -- One common and simple situation is to wrap a couple of fields in some + -- newtype. You can leverage the @generic-lens@ library with the three + -- functions below. + -- + -- @ + -- over :: ASetter s t a b -> (a -> b) -> s -> t -- from lens or microlens + -- field :: HasField s t a b => Lens s t a b -- from generic-lens + -- @ + -- + -- For example, to wrap a field named @hidden@ in a newtype like + -- 'Generic.Data.Opaque' in some record type @R@: + -- + -- @ + -- 'onData' (over (field @"hidden") 'Generic.Data.Opaque') . 'toData' + -- :: R -> Data _ _ + -- @ + -- + -- The result is a type, that from the point of view of "GHC.Generics" + -- looks just like @R@ but with the field @hidden@ wrapped. + + -- * Getting into the operating room + , OR + + , toOR + , fromOR' + , toOR' + , fromOR + + , OROf + + -- * Surgeries + + -- ** Unnamed fields + , removeCField + , insertCField + , insertCField' + , modifyCField + + -- ** Named fields (records) + , removeRField + , insertRField + , insertRField' + , modifyRField + + -- ** Constructors + + -- | A constructor is extracted to a "tuple", which can be any + -- 'GHC.Generics.Generic' single-constructor type with the same number of + -- fields. + -- + -- Note that @()@ and 'Data.Functor.Identity.Identity' can be used as an + -- empty and a singleton tuple type respectively. + -- + -- When the tuple type can't be inferred and doesn't really matter, + -- an alternative to explicit type annotations is to use the @...ConstrT@ + -- variants of these surgeries, which are specialized to actual tuples + -- (@()@, 'Data.Functor.Identity.Identity', @(,)@, @(,,)@, up to 7 --- + -- because that's where 'GHC.Generics.Generic' instances currently stop). + + , removeConstr + , insertConstr + , modifyConstr + , removeConstrT + , insertConstrT + , modifyConstrT + + -- * Constraint synonyms + + -- | Hiding implementation details from the signatures above. + -- Useful to compose surgeries in a reusable way. + + -- ** Conversions + + , ToORRep + , ToOR + , FromORRep + , FromOR + + -- ** Surgeries + + , RmvCField + , InsCField + , ModCField + , RmvRField + , InsRField + , ModRField + , RmvConstr + , InsConstr + , ModConstr + , RmvConstrT + , InsConstrT + , ModConstrT + ) where + +import Generic.Data.Internal.Data + +import Generic.Data.Surgery.Internal diff --git a/src/Generic/Data/Surgery/Internal.hs b/src/Generic/Data/Surgery/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Generic/Data/Surgery/Internal.hs @@ -0,0 +1,1069 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | Operate on data types: insert\/modify\/delete fields and constructors. + +module Generic.Data.Surgery.Internal where + +import Control.Monad ((<=<)) +import Data.Bifunctor (bimap, first) +import Data.Coerce +import Data.Functor.Identity (Identity) +import Data.Kind (Constraint, Type) +import Data.Type.Equality (type (==)) +import GHC.Generics +import GHC.TypeLits + +import Fcf + ( Eval, If, _If, IsBool, Pure, Pure2, Bimap, Uncurry + , type (=<<), type (<=<), type (<$>) + ) + +import Generic.Data.Internal.Compat (Div) +import Generic.Data.Internal.Data (Data(Data,unData)) +import Generic.Data.Internal.Meta (MetaOf, MetaConsName, UnM1) +import Generic.Data.Internal.Utils (coerce', absurd1) + +-- | /A sterile Operating Room, where generic data comes to be altered./ +-- +-- Generic representation in a simplified shape @l@ at the type level +-- (reusing the constructors from "GHC.Generics" for convenience). +-- This representation makes it easy to modify fields and constructors. +-- +-- We may also refer to the representation @l@ as a "row" of constructors, +-- if it represents a sum type, otherwise it is a "row" of unnamed fields or +-- record fields for single-constructor types. +-- +-- @x@ corresponds to the last parameter of 'Rep', and is currently ignored by +-- this module (no support for 'Generic1'). +newtype OR (l :: k -> Type) (x :: k) = OR { unOR :: l x } + +-- | /Move fresh data to the Operating Room, where surgeries can be applied./ +-- +-- Convert a generic type to a generic representation. +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- a :: 'Type' -- Generic type +-- l :: k -> 'Type' -- Generic representation (simplified) +-- x :: k -- Ignored +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- a -> l +-- @ +toOR :: forall a l x. (Generic a, ToORRep a l) => a -> OR l x +toOR = OR . gLinearize . from + +-- | /Move altered data out of the Operating Room, to be consumed by/ +-- /some generic function./ +-- +-- Convert a generic representation to a \"synthetic\" type that behaves +-- like a generic type. +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- f :: k -> 'Type' -- 'Generic' representation (proper) +-- l :: k -> 'Type' -- Generic representation (simplified) +-- x :: k -- Ignored +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- f -> l +-- l -> f +-- @ +-- +-- ==== Implementation details +-- +-- The synthesized representation is made of balanced binary trees, +-- corresponding closely to what GHC would generate for an actual data type. +-- +-- That structure assumed by at least one piece of code out there (@aeson@). +fromOR' :: forall f l x. FromOR f l => OR l x -> Data f x +fromOR' = Data . gArborify . unOR + +-- | /Move altered data, produced by some generic function, to the operating/ +-- /room./ +-- +-- The inverse of 'fromOR''. +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- f :: k -> 'Type' -- 'Generic' representation (proper) +-- l :: k -> 'Type' -- Generic representation (simplified) +-- x :: k -- Ignored +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- f -> l +-- l -> f +-- @ +toOR' :: forall f l x. ToOR f l => Data f x -> OR l x +toOR' = OR . gLinearize . unData + +-- | /Move restored data out of the Operating Room and back to the real/ +-- /world./ +-- +-- The inverse of 'toOR'. +-- +-- It may be useful to annotate the output type of 'fromOR', +-- since the rest of the type depends on it and the only way to infer it +-- otherwise is from the context. The following annotations are possible: +-- +-- @ +-- 'fromOR' :: 'OROf' a -> a +-- 'fromOR' \@a -- with TypeApplications +-- @ +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- a :: 'Type' -- Generic type +-- l :: k -> 'Type' -- Generic representation (simplified) +-- x :: k -- Ignored +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- a -> l +-- @ +fromOR :: forall a l x. (Generic a, FromORRep a l) => OR l x -> a +fromOR = to . gArborify . unOR + +-- | The simplified generic representation type of type @a@, +-- that 'toOR' and 'fromOR' convert to and from. +type OROf a = OR (Linearize (Rep a)) () + +-- | This constraint means that @a@ is convertible /to/ its simplified +-- generic representation. Implies @'OROf' a ~ 'OR' l ()@. +type ToORRep a l = ToOR (Rep a) l + +-- | This constraint means that @a@ is convertible /from/ its simplified +-- generic representation. Implies @'OROf' a ~ 'OR' l ()@. +type FromORRep a l = FromOR (Rep a) l + +-- | Similar to 'ToORRep', but as a constraint on the standard +-- generic representation of @a@ directly, @f ~ 'Rep' a@. +type ToOR f l = (GLinearize f, Linearize f ~ l, f ~ Arborify l) + +-- | Similar to 'FromORRep', but as a constraint on the standard +-- generic representation of @a@ directly, @f ~ 'Rep' a@. +type FromOR f l = (GArborify f, Linearize f ~ l, f ~ Arborify l) + +-- + +-- | @'removeCField' \@n \@t@: remove the @n@-th field, of type @t@, in a +-- non-record single-constructor type. +-- +-- Inverse of 'insertCField'. +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- n :: 'Nat' -- Field position +-- t :: 'Type' -- Field type +-- lt :: k -> 'Type' -- Row with field +-- l :: k -> 'Type' -- Row without field +-- x :: k -- Ignored +-- @ +-- +-- ==== Signature +-- +-- @ +-- 'OR' lt x -- Data with field +-- -> +-- (t, 'OR' l x) -- Field value × Data without field +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- n lt -> t l +-- n t l -> lt +-- @ +removeCField + :: forall n t lt l x + . RmvCField n t lt l + => OR lt x -> (t, OR l x) +removeCField (OR a) = OR <$> gRemoveField @n a + +-- | @'removeRField' \@\"fdName\" \@n \@t@: remove the field @fdName@ +-- at position @n@ of type @t@ in a record type. +-- +-- Inverse of 'insertRField'. +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- fd :: 'Symbol' -- Field name +-- n :: 'Nat' -- Field position +-- t :: 'Type' -- Field type +-- lt :: k -> 'Type' -- Row with field +-- l :: k -> 'Type' -- Row without field +-- x :: k -- Ignored +-- @ +-- +-- ==== Signature +-- +-- @ +-- 'OR' lt x -- Data with field +-- -> +-- (t, 'OR' l x) -- Field value × Data without field +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- fd lt -> n t l +-- n lt -> fd t l +-- fd n t l -> lt +-- @ +removeRField + :: forall fd n t lt l x + . RmvRField fd n t lt l + => OR lt x -> (t, OR l x) +removeRField (OR a) = OR <$> gRemoveField @n a + +-- | @'insertCField' \@n \@t@: insert a field of type @t@ +-- at position @n@ in a non-record single-constructor type. +-- +-- Inverse of 'removeCField'. +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- n :: 'Nat' -- Field position +-- t :: 'Type' -- Field type +-- lt :: k -> 'Type' -- Row with field +-- l :: k -> 'Type' -- Row without field +-- x :: k -- Ignored +-- @ +-- +-- ==== Signature +-- +-- @ +-- (t, 'OR' l x) -- Field value × Data without field +-- -> +-- 'OR' lt x -- Data with field +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- n lt -> t l +-- n t l -> lt +-- @ +insertCField + :: forall n t lt l x + . InsCField n t lt l + => (t, OR l x) -> OR lt x +insertCField = uncurry (insertCField' @n) + +-- | Curried 'insertCField'. +insertCField' + :: forall n t lt l x + . InsCField n t lt l + => t -> OR l x -> OR lt x +insertCField' z (OR a) = OR (gInsertField @n z a) + +-- | @'insertRField' \@\"fdName\" \@n \@t@: insert a field +-- named @fdName@ of type @t@ at position @n@ in a record type. +-- +-- Inverse of 'removeRField'. +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- fd :: 'Symbol' -- Field name +-- n :: 'Nat' -- Field position +-- t :: 'Type' -- Field type +-- lt :: k -> 'Type' -- Row with field +-- l :: k -> 'Type' -- Row without field +-- x :: k -- Ignored +-- @ +-- +-- ==== Signature +-- +-- @ +-- (t, 'OR' l x) -- Field value × Data without field +-- -> +-- 'OR' lt x -- Data with field +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- fd lt -> n t l +-- n lt -> fd t l +-- fd n t l -> lt +-- @ +insertRField + :: forall fd n t lt l x + . InsRField fd n t lt l + => (t, OR l x) -> OR lt x +insertRField = uncurry (insertRField' @fd) + +-- | Curried 'insertRField'. +insertRField' + :: forall fd n t lt l x + . InsRField fd n t lt l + => t -> OR l x -> OR lt x +insertRField' z (OR a) = OR (gInsertField @n z a) + +-- | @'modifyCField' \@n \@t \@t'@: modify the field at position @n@ in a +-- non-record via a function @f :: t -> t'@ (changing the type of the field). +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- n :: 'Nat' -- Field position +-- t :: 'Type' -- Initial field type +-- t' :: 'Type' -- Final field type +-- lt :: k -> 'Type' -- Row with initial field +-- lt' :: k -> 'Type' -- Row with final field +-- l :: k -> 'Type' -- Row without field +-- x :: k -- Ignored +-- @ +-- +-- ==== Signature +-- +-- @ +-- (t -> t') -- Field modification +-- -> +-- 'OR' lt x -- Data with field t +-- -> +-- 'OR' lt' x -- Data with field t' +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- n lt -> t l +-- n lt' -> t' l +-- n t l -> lt +-- n t' l -> lt' +-- @ +modifyCField + :: forall n t t' lt lt' l x + . ModCField n t t' lt lt' l + => (t -> t') -> OR lt x -> OR lt' x +modifyCField f = insertCField @n @t' . first f . removeCField @n @t + +-- | @'modifyRField' \@\"fdName\" \@n \@t \@t'@: modify the field +-- @fdName@ at position @n@ in a record via a function @f :: t -> t'@ +-- (changing the type of the field). +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- fd :: 'Symbol' -- Field name +-- n :: 'Nat' -- Field position +-- t :: 'Type' -- Initial field type +-- t' :: 'Type' -- Final field type +-- lt :: k -> 'Type' -- Row with initial field +-- lt' :: k -> 'Type' -- Row with final field +-- l :: k -> 'Type' -- Row without field +-- x :: k -- Ignored +-- @ +-- +-- ==== Signature +-- +-- @ +-- (t -> t') -- Field modification +-- -> +-- 'OR' lt x -- Data with field t +-- -> +-- 'OR' lt' x -- Data with field t' +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- fd lt -> n t l +-- fd lt' -> n t' l +-- n lt -> fd t l +-- n lt' -> fd t' l +-- fd n t l -> lt +-- fd n t' l -> lt' +-- @ +modifyRField + :: forall fd n t t' lt lt' l x + . ModRField fd n t t' lt lt' l + => (t -> t') -> OR lt x -> OR lt' x +modifyRField f = insertRField @fd @n @t' . first f . removeRField @fd @n @t + +-- | @'removeConstr' \@\"C\" \@n \@t@: remove the @n@-th constructor, named @C@, +-- with contents isomorphic to the tuple @t@. +-- +-- Inverse of 'insertConstr'. +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- c :: 'Symbol' -- Constructor name +-- t :: 'Type' -- Tuple type to hold c's contents +-- n :: 'Nat' -- Constructor position +-- lc :: k -> 'Type' -- Row with constructor +-- l :: k -> 'Type' -- Row without constructor +-- l_t :: k -> 'Type' -- Field row of constructor c +-- x :: k -- Ignored +-- @ +-- +-- ==== Signature +-- +-- @ +-- 'OR' lc x -- Data with constructor +-- -> +-- Either t ('OR' l x) -- Constructor (as a tuple) | Data without constructor +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- c lc -> n l l_t +-- n lc -> c l l_t +-- c n l l_t -> lc +-- @ +-- +-- Note that there is no dependency to determine @t@. +removeConstr + :: forall c n t lc l l_t x + . RmvConstr c n t lc l l_t + => OR lc x -> Either t (OR l x) +removeConstr (OR a) = bimap + (to . coerce' . gArborify @(Arborify l_t)) OR (gRemoveConstr @n a) + +-- | A variant of 'removeConstr' that can infer the tuple type @t@ to hold +-- the contents of the removed constructor. +-- +-- See 'removeConstr'. +-- +-- === __Details__ +-- +-- ==== Extra functional dependency +-- +-- @ +-- l_t -> t +-- @ +removeConstrT + :: forall c n t lc l l_t x + . RmvConstrT c n t lc l l_t + => OR lc x -> Either t (OR l x) +removeConstrT = removeConstr @c @n @t + +-- | @'insertConstr' \@\"C\" \@n \@t@: insert a constructor @C@ at position @n@ +-- with contents isomorphic to the tuple @t@. +-- +-- Inverse of 'removeConstr'. +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- c :: 'Symbol' -- Constructor name +-- t :: 'Type' -- Tuple type to hold c's contents +-- n :: 'Nat' -- Constructor position +-- lc :: k -> 'Type' -- Row with constructor +-- l :: k -> 'Type' -- Row without constructor +-- l_t :: k -> 'Type' -- Field row of constructor c +-- x :: k -- Ignored +-- @ +-- +-- ==== Signature +-- +-- @ +-- Either t ('OR' l x) -- Constructor (as a tuple) | Data without constructor +-- -> +-- 'OR' lc x -- Data with constructor +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- c lc -> n l l_t +-- n lc -> c l l_t +-- c n l l_t -> lc +-- @ +-- +-- Note that there is no dependency to determine @t@. +insertConstr + :: forall c n t lc l l_t x + . InsConstr c n t lc l l_t + => Either t (OR l x) -> OR lc x +insertConstr z = + OR (gInsertConstr @n + (bimap (gLinearize @(Arborify l_t) . coerce' . from) unOR z)) + +-- | A variant of 'insertConstr' that can infer the tuple type @t@ to hold +-- the contents of the inserted constructor. +-- +-- See 'insertConstr'. +-- +-- === __Details__ +-- +-- ==== Extra functional dependency +-- +-- @ +-- l_t -> t +-- @ +insertConstrT + :: forall c n t lc l l_t x + . InsConstrT c n t lc l l_t + => Either t (OR l x) -> OR lc x +insertConstrT = insertConstr @c @n @t + +-- | @'modifyConstr' \@\"C\" \@n \@t \@t'@: modify the @n@-th constructor, +-- named @C@, with contents isomorphic to the tuple @t@, to another tuple @t'@. +-- +-- === __Details__ +-- +-- ==== Type parameters +-- +-- @ +-- c :: 'Symbol' -- Constructor name +-- t :: 'Type' -- Tuple type to hold c's initial contents +-- t' :: 'Type' -- Tuple type to hold c's final contents +-- n :: 'Nat' -- Constructor position +-- lc :: k -> 'Type' -- Row with initial constructor +-- lc' :: k -> 'Type' -- Row with final constructor +-- l :: k -> 'Type' -- Row without constructor +-- l_t :: k -> 'Type' -- Initial field row of constructor c +-- l_t' :: k -> 'Type' -- Final field row of constructor c +-- x :: k -- Ignored +-- @ +-- +-- ==== Signature +-- +-- @ +-- (t -> t') -- Constructor modification +-- -> +-- 'OR' lc x -- Data with initial constructor +-- -> +-- 'OR' lc' x -- Data with final constructor +-- @ +-- +-- ==== Functional dependencies +-- +-- @ +-- c lc -> n l l_t +-- c lc' -> n l l_t' +-- n lc -> c l l_t +-- n lc' -> c l l_t' +-- c n l l_t -> lc +-- c n l l_t' -> lc' +-- @ +-- +-- Note that there is no dependency to determine @t@ and @t'@. +modifyConstr + :: forall c n t t' lc lc' l l_t l_t' x + . ModConstr c n t t' lc lc' l l_t l_t' + => (t -> t') -> OR lc x -> OR lc' x +modifyConstr f = insertConstr @c @n @t' . first f . removeConstr @c @n @t + +-- | A variant of 'modifyConstr' that can infer the tuple types @t@ and @t'@ to +-- hold the contents of the inserted constructor. +-- +-- See 'modifyConstr'. +-- +-- === __Details__ +-- +-- ==== Extra functional dependencies +-- +-- @ +-- l_t -> t +-- l_t' -> t' +-- @ +modifyConstrT + :: forall c n t t' lc lc' l l_t l_t' x + . ModConstrT c n t t' lc lc' l l_t l_t' + => (t -> t') -> OR lc x -> OR lc' x +modifyConstrT = modifyConstr @c @n @t @t' + +-- + +-- | This constraint means that the (unnamed) field row @lt@ contains +-- a field of type @t@ at position @n@, and removing it yields row @l@. +type RmvCField n t lt l = + ( GRemoveField n lt + , CFieldSurgery n t lt l + ) + +-- | This constraint means that the record field row @lt@ contains a field of +-- type @t@ named @fd@ at position @n@, and removing it yields row @l@. +type RmvRField fd n t lt l = + ( GRemoveField n lt + , RFieldSurgery fd n t lt l + ) + +-- | This constraint means that inserting a field @t@ at position @n@ in the +-- (unnamed) field row @l@ yields row @lt@. +type InsCField n t lt l = + ( GInsertField n lt + , CFieldSurgery n t lt l + ) + +-- | This constraint means that inserting a field @t@ named @fd@ at position +-- @n@ in the record field row @l@ yields row @lt@. +type InsRField fd n t lt l = + ( GInsertField n lt + , RFieldSurgery fd n t lt l + ) + +-- | This constraint means that modifying a field @t@ to @t'@ at position @n@ +-- in the (unnamed) field row @lt@ yields row @lt'@. +-- @l@ is the row of fields common to @lt@ and @lt'@. +type ModCField n t t' lt lt' l = + ( RmvCField n t lt l + , InsCField n t' lt' l + ) + +-- | This constraint means that modifying a field @t@ named @fd@ at position @n@ +-- to @t'@ in the record field row @lt@ yields row @lt'@. +-- @l@ is the row of fields common to @lt@ and @lt'@. +type ModRField fd n t t' lt lt' l = + ( RmvRField fd n t lt l + , InsRField fd n t' lt' l + ) + +-- | This constraint means that the constructor row @lc@ contains a constructor +-- named @c@ at position @n@, and removing it from @lc@ yields row @l@. +-- Furthermore, constructor @c@ contains a field row @l_t@ compatible with the +-- tuple type @t@. +type RmvConstr c n t lc l l_t = + ( GRemoveConstr n lc + , GArborify (Arborify l_t) + , ConstrSurgery c n t lc l l_t + ) + +-- | A variant of 'RmvConstr' allowing @t@ to be inferred. +type RmvConstrT c n t lc l l_t = + ( RmvConstr c n t lc l l_t + , IsTuple (Arity l_t) t + ) + +-- | This constraint means that inserting a constructor @c@ at position @n@ +-- in the constructor row @l@ yields row @lc@. +-- Furthermore, constructor @c@ contains a field row @l_t@ compatible with the +-- tuple type @t@. +type InsConstr c n t lc l l_t = + ( GInsertConstr n lc + , GLinearize (Arborify l_t) + , ConstrSurgery c n t lc l l_t + ) + +-- | A variant of 'InsConstr' allowing @t@ to be inferred. +type InsConstrT c n t lc l l_t = + ( InsConstr c n t lc l l_t + , IsTuple (Arity l_t) t + ) + +-- | This constraint means that the constructor row @lc@ contains a constructor +-- named @c@ at position @n@ of type isomorphic to @t@, and modifying it to +-- @t'@ yields row @lc'@. +type ModConstr c n t t' lc lc' l l_t l_t' = + ( RmvConstr c n t lc l l_t + , InsConstr c n t' lc' l l_t' + ) + +-- | A variant of 'ModConstr' allowing @t@ and @t'@ to be inferred. +type ModConstrT c n t t' lc lc' l l_t l_t' = + ( ModConstr c n t t' lc lc' l l_t l_t' + , IsTuple (Arity l_t) t + , IsTuple (Arity l_t') t' + ) + +type FieldSurgery n t lt l = + ( t ~ Eval (FieldTypeAt n lt) + , l ~ Eval (RemoveField n lt) + ) + +type CFieldSurgery n t lt l = + ( lt ~ Eval (InsertField n 'Nothing t l) + , FieldSurgery n t lt l + ) + +type RFieldSurgery fd n t lt l = + ( n ~ Eval (FieldIndex fd lt) + , lt ~ Eval (InsertField n ('Just fd) t l) + , FieldSurgery n t lt l + ) + +type ConstrSurgery c n t lc l l_t = + ( Generic t + , MatchFields (UnM1 (Rep t)) (Arborify l_t) + , Coercible (Arborify l_t) (Rep t) + , n ~ Eval (ConstrIndex c lc) + , c ~ MetaConsName (MetaOf l_t) + , l_t ~ Linearize (Arborify l_t) + , l_t ~ Eval (ConstrAt n lc) + , lc ~ Eval (InsertConstr n l_t l) + , l ~ Eval (RemoveConstr n lc) + ) + +-- + +type family Linearize (f :: k -> *) :: k -> * +type instance Linearize (M1 D m f) = M1 D m (LinearizeSum f V1) +type instance Linearize (M1 C m f) = M1 C m (LinearizeProduct f U1) + +type family LinearizeSum (f :: k -> *) (tl :: k -> *) :: k -> * +type instance LinearizeSum V1 tl = tl +type instance LinearizeSum (f :+: g) tl = LinearizeSum f (LinearizeSum g tl) +type instance LinearizeSum (M1 c m f) tl = M1 c m (LinearizeProduct f U1) :+: tl + +type family LinearizeProduct (f :: k -> *) (tl :: k -> *) :: k -> * +type instance LinearizeProduct U1 tl = tl +type instance LinearizeProduct (f :*: g) tl = LinearizeProduct f (LinearizeProduct g tl) +type instance LinearizeProduct (M1 s m f) tl = M1 s m f :*: tl + +class GLinearize f where + gLinearize :: f x -> Linearize f x + +instance GLinearizeSum f V1 => GLinearize (M1 D m f) where + gLinearize (M1 a) = M1 (gLinearizeSum @_ @V1 (Left a)) + +instance GLinearizeProduct f U1 => GLinearize (M1 C m f) where + gLinearize (M1 a) = M1 (gLinearizeProduct a U1) + +class GLinearizeSum f tl where + gLinearizeSum :: Either (f x) (tl x) -> LinearizeSum f tl x + +instance GLinearizeSum V1 tl where + gLinearizeSum (Left v) = absurd1 v + gLinearizeSum (Right c) = c + +instance (GLinearizeSum g tl, GLinearizeSum f (LinearizeSum g tl)) + => GLinearizeSum (f :+: g) tl where + gLinearizeSum (Left (L1 a)) = gLinearizeSum @_ @(LinearizeSum g tl) (Left a) + gLinearizeSum (Left (R1 b)) = gLinearizeSum @f (Right (gLinearizeSum @g @tl (Left b))) + gLinearizeSum (Right c) = gLinearizeSum @f (Right (gLinearizeSum @g (Right c))) + +instance GLinearizeProduct f U1 => GLinearizeSum (M1 c m f) tl where + gLinearizeSum (Left (M1 a)) = L1 (M1 (gLinearizeProduct a U1)) + gLinearizeSum (Right c) = R1 c + +class GLinearizeProduct f tl where + gLinearizeProduct :: f x -> tl x -> LinearizeProduct f tl x + +instance GLinearizeProduct U1 tl where + gLinearizeProduct _ = id + +instance (GLinearizeProduct g tl, GLinearizeProduct f (LinearizeProduct g tl)) + => GLinearizeProduct (f :*: g) tl where + gLinearizeProduct (a :*: b) = gLinearizeProduct a . gLinearizeProduct b + +instance GLinearizeProduct (M1 s m f) tl where + gLinearizeProduct = (:*:) + +class GArborify f where + gArborify :: Linearize f x -> f x + +instance GArborifySum f V1 => GArborify (M1 D m f) where + gArborify (M1 a) = case gArborifySum @_ @V1 a of + Left a' -> M1 a' + Right v -> absurd1 v + +instance GArborifyProduct f U1 => GArborify (M1 C m f) where + gArborify (M1 a) = M1 (fst (gArborifyProduct @_ @U1 a)) + +class GArborifySum f tl where + gArborifySum :: LinearizeSum f tl x -> Either (f x) (tl x) + +instance GArborifySum V1 tl where + gArborifySum = Right + +instance (GArborifySum g tl, GArborifySum f (LinearizeSum g tl)) + => GArborifySum (f :+: g) tl where + gArborifySum = first R1 . gArborifySum <=< first L1 . gArborifySum + +instance GArborifyProduct f U1 => GArborifySum (M1 c m f) tl where + gArborifySum (L1 (M1 a)) = Left (M1 (fst (gArborifyProduct @_ @U1 a))) + gArborifySum (R1 c) = Right c + +class GArborifyProduct f tl where + gArborifyProduct :: LinearizeProduct f tl x -> (f x, tl x) + +instance GArborifyProduct U1 tl where + gArborifyProduct c = (U1, c) + +instance (GArborifyProduct g tl, GArborifyProduct f (LinearizeProduct g tl)) + => GArborifyProduct (f :*: g) tl where + gArborifyProduct abc = (a :*: b, c) where + (a, bc) = gArborifyProduct abc + (b, c) = gArborifyProduct bc + +instance GArborifyProduct (M1 s m f) tl where + gArborifyProduct (a :*: c) = (a, c) + +type family Arborify (f :: k -> *) :: k -> * +type instance Arborify (M1 D m f) = M1 D m (Eval (ArborifySum (CoArity f) f)) +type instance Arborify (M1 C m f) = M1 C m (Eval (ArborifyProduct (Arity f) f)) + +data ArborifySum (n :: Nat) (f :: k -> *) :: (k -> *) -> * +type instance Eval (ArborifySum n V1) = V1 +type instance Eval (ArborifySum n (f :+: g)) = + Eval (If (n == 1) + (ArborifyProduct (Arity f) f) + (Arborify' ArborifySum (:+:) n (Div n 2) f g)) + +data ArborifyProduct (n :: Nat) (f :: k -> *) :: (k -> *) -> * +type instance Eval (ArborifyProduct n (M1 C s f)) = M1 C s (Eval (ArborifyProduct n f)) +type instance Eval (ArborifyProduct n U1) = U1 +type instance Eval (ArborifyProduct n (f :*: g)) = + Eval (If (n == 1) + (Pure f) + (Arborify' ArborifyProduct (:*:) n (Div n 2) f g)) + +-- let nDiv2 = Div n 2 in ... +type Arborify' arb op n nDiv2 f g = + ( Uncurry (Pure2 op) + <=< Bimap (arb nDiv2) (arb (n-nDiv2)) + <=< SplitAt nDiv2 + ) (op f g) + +data SplitAt :: Nat -> (k -> *) -> (k -> *, k -> *) -> * +type instance Eval (SplitAt n (f :+: g)) = + Eval (If (n == 0) + (Pure '(V1, f :+: g)) + (Bimap (Pure2 (:+:) f) Pure =<< SplitAt (n-1) g)) +type instance Eval (SplitAt n (f :*: g)) = + Eval (If (n == 0) + (Pure '(U1, f :*: g)) + (Bimap (Pure2 (:*:) f) Pure =<< SplitAt (n-1) g)) + +data FieldTypeAt (n :: Nat) (f :: k -> *) :: * -> * +type instance Eval (FieldTypeAt n (M1 i c f)) = Eval (FieldTypeAt n f) +type instance Eval (FieldTypeAt n (f :+: V1)) = Eval (FieldTypeAt n f) +type instance Eval (FieldTypeAt n (f :*: g)) = + Eval (If (n == 0) (Pure (FieldTypeOf f)) (FieldTypeAt (n-1) g)) + +type family FieldTypeOf (f :: k -> *) :: * +type instance FieldTypeOf (M1 s m (K1 i a)) = a + +data RemoveField (n :: Nat) (f :: k -> *) :: (k -> *) -> * +type instance Eval (RemoveField n (M1 i m f)) = M1 i m (Eval (RemoveField n f)) +type instance Eval (RemoveField n (f :+: V1)) = Eval (RemoveField n f) :+: V1 +type instance Eval (RemoveField n (f :*: g)) = + Eval (If (n == 0) (Pure g) ((:*:) f <$> RemoveField (n-1) g)) + +type DefaultMetaSel field + = 'MetaSel field 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy + +data InsertField (n :: Nat) (fd :: Maybe Symbol) (t :: *) (f :: k -> *) :: (k -> *) -> * +type instance Eval (InsertField n fd t (M1 D m f)) = M1 D m (Eval (InsertField n fd t f)) +type instance Eval (InsertField n fd t (M1 C m f)) = M1 C m (Eval (InsertField n fd t f)) +type instance Eval (InsertField n fd t (f :+: V1)) = Eval (InsertField n fd t f) :+: V1 +type instance Eval (InsertField n fd t (f :*: g)) = + Eval (If (n == 0) + (Pure (M1 S (DefaultMetaSel fd) (K1 R t) :*: (f :*: g))) + ((:*:) f <$> InsertField (n-1) fd t g)) +type instance Eval (InsertField 0 fd t U1) = M1 S (DefaultMetaSel fd) (K1 R t) :*: U1 + +data Succ :: Nat -> Nat -> * +type instance Eval (Succ n) = 1 + n + +-- | Position of a record field +data FieldIndex (field :: Symbol) (f :: k -> *) :: Nat -> * +type instance Eval (FieldIndex field (M1 D m f)) = Eval (FieldIndex field f) +type instance Eval (FieldIndex field (M1 C m f)) = Eval (FieldIndex field f) +type instance Eval (FieldIndex field (f :+: V1)) = Eval (FieldIndex field f) +type instance Eval (FieldIndex field (M1 S ('MetaSel ('Just field') su ss ds) f :*: g)) + = Eval (If (field == field') (Pure 0) (Succ =<< FieldIndex field g)) + +-- | Number of fields of a single constructor +type family Arity (f :: k -> *) :: Nat +type instance Arity (M1 d m f) = Arity f +type instance Arity (f :+: V1) = Arity f +type instance Arity (f :*: g) = Arity f + Arity g +type instance Arity (K1 i c) = 1 +type instance Arity U1 = 0 + +-- | Number of constructors of a data type +type family CoArity (f :: k -> *) :: Nat +type instance CoArity (M1 D m f) = CoArity f +type instance CoArity (M1 C m f) = 1 +type instance CoArity V1 = 0 +type instance CoArity (f :+: g) = CoArity f + CoArity g + +class GRemoveField (n :: Nat) f where + gRemoveField :: f x -> (Eval (FieldTypeAt n f), Eval (RemoveField n f) x) + +instance GRemoveField n f => GRemoveField n (M1 i c f) where + gRemoveField (M1 a) = M1 <$> gRemoveField @n a + +instance GRemoveField n f => GRemoveField n (f :+: V1) where + gRemoveField (L1 a) = L1 <$> gRemoveField @n a + gRemoveField (R1 v) = absurd1 v + +instance (If (n == 0) (() :: Constraint) (GRemoveField (n-1) g), IsBool (n == 0)) + => GRemoveField n (M1 s m (K1 i t) :*: g) where + gRemoveField (a@(M1 (K1 t)) :*: b) = _If @(n == 0) + (t, b) + ((a :*:) <$> gRemoveField @(n-1) b) + +class GInsertField (n :: Nat) f where + gInsertField :: Eval (FieldTypeAt n f) -> Eval (RemoveField n f) x -> f x + +instance GInsertField n f => GInsertField n (M1 i c f) where + gInsertField t (M1 a) = M1 (gInsertField @n t a) + +instance GInsertField n f => GInsertField n (f :+: V1) where + gInsertField t (L1 a) = L1 (gInsertField @n t a) + gInsertField _ (R1 v) = absurd1 v + +instance (If (n == 0) (() :: Constraint) (GInsertField (n-1) g), IsBool (n == 0)) + => GInsertField n (M1 s m (K1 i t) :*: g) where + gInsertField t ab = _If @(n == 0) + (M1 (K1 t) :*: ab) + (let a :*: b = ab in a :*: gInsertField @(n-1) t b) + +data ConstrAt (n :: Nat) (f :: k -> *) :: (k -> *) -> * +type instance Eval (ConstrAt n (M1 i m f)) = Eval (ConstrAt n f) +type instance Eval (ConstrAt n (f :+: g)) = + Eval (If (n == 0) (Pure f) (ConstrAt (n-1) g)) + +data RemoveConstr (n :: Nat) (f :: k -> *) :: (k -> *) -> * +type instance Eval (RemoveConstr n (M1 i m f)) = M1 i m (Eval (RemoveConstr n f)) +type instance Eval (RemoveConstr n (f :+: g)) = + Eval (If (n == 0) (Pure g) ((:+:) f <$> RemoveConstr (n-1) g)) + +data InsertConstr (n :: Nat) (t :: k -> *) (f :: k -> *) :: (k -> *) -> * +type instance Eval (InsertConstr n t (M1 i m f)) = M1 i m (Eval (InsertConstr n t f)) +type instance Eval (InsertConstr n t (f :+: g)) = + Eval (If (n == 0) (Pure (t :+: (f :+: g))) ((:+:) f <$> InsertConstr (n-1) t g)) +type instance Eval (InsertConstr 0 t V1) = t :+: V1 + +data ConstrIndex (con :: Symbol) (f :: k -> *) :: Nat -> * +type instance Eval (ConstrIndex con (M1 D m f)) = Eval (ConstrIndex con f) +type instance Eval (ConstrIndex con (M1 C ('MetaCons con' fx s) f :+: g)) = + Eval (If (con == con') (Pure 0) (Succ =<< ConstrIndex con g)) + +class GRemoveConstr (n :: Nat) f where + gRemoveConstr :: f x -> Either (Eval (ConstrAt n f) x) (Eval (RemoveConstr n f) x) + +instance GRemoveConstr n f => GRemoveConstr n (M1 i c f) where + gRemoveConstr (M1 a) = M1 <$> gRemoveConstr @n a + +instance (If (n == 0) (() :: Constraint) (GRemoveConstr (n-1) g), IsBool (n == 0)) + => GRemoveConstr n (f :+: g) where + gRemoveConstr = _If @(n == 0) + (\case + L1 a -> Left a + R1 b -> Right b) + (\case + L1 a -> Right (L1 a) + R1 b -> R1 <$> gRemoveConstr @(n-1) b) + +class GInsertConstr (n :: Nat) f where + gInsertConstr :: Either (Eval (ConstrAt n f) x) (Eval (RemoveConstr n f) x) -> f x + +instance GInsertConstr n f => GInsertConstr n (M1 i c f) where + gInsertConstr = M1 . gInsertConstr @n . fmap unM1 + +instance (If (n == 0) (() :: Constraint) (GInsertConstr (n-1) g), IsBool (n == 0)) + => GInsertConstr n (f :+: g) where + gInsertConstr = _If @(n == 0) + (\case + Left a -> L1 a + Right b -> R1 b) + (\case + Left a -> R1 (gInsertConstr @(n-1) (Left a)) + Right (L1 a) -> L1 a + Right (R1 b) -> R1 (gInsertConstr @(n-1) (Right b))) + +-- | Generate equality constraints between fields of two matching generic +-- representations. +class MatchFields (f :: k -> *) (g :: k -> *) +instance (g' ~ M1 D d g, MatchFields f g) => MatchFields (M1 D c f) g' +-- Forcing the MetaCons field +instance (g' ~ M1 C ('MetaCons _cn _s _t) g, MatchFields f g) + => MatchFields (M1 C c f) g' +instance (g' ~ M1 S d g, MatchFields f g) => MatchFields (M1 S c f) g' +instance (g' ~ (g1 :+: g2), MatchFields f1 g1, MatchFields f2 g2) + => MatchFields (f1 :+: f2) g' +instance (g' ~ (g1 :*: g2), MatchFields f1 g1, MatchFields f2 g2) + => MatchFields (f1 :*: f2) g' +instance (g' ~ K1 j a) => MatchFields (K1 i a) g' +instance (g' ~ U1) => MatchFields U1 g' +instance (g' ~ V1) => MatchFields V1 g' + +class IsTuple (n :: Nat) (t :: k) +instance (t ~ ()) => IsTuple 0 t +instance (t ~ Identity a) => IsTuple 1 t +instance (t ~ (a, b)) => IsTuple 2 t +instance (t ~ (a, b, c)) => IsTuple 3 t +instance (t ~ (a, b, c, d)) => IsTuple 4 t +instance (t ~ (a, b, c, d, e)) => IsTuple 5 t +instance (t ~ (a, b, c, d, e, f)) => IsTuple 6 t +instance (t ~ (a, b, c, d, e, f, g)) => IsTuple 7 t + +-- | Unify the "spines" of two generic representations (the "spine" is +-- everything except the field types). +class UnifyRep (f :: k -> *) (g :: k -> *) +instance (g' ~ M1 D c g, UnifyRep f g) => UnifyRep (M1 D c f) g' +instance (g' ~ M1 C c g, UnifyRep f g) + => UnifyRep (M1 C c f) g' +instance (g' ~ M1 S c g, UnifyRep f g) => UnifyRep (M1 S c f) g' +instance (g' ~ (g1 :+: g2), UnifyRep f1 g1, UnifyRep f2 g2) + => UnifyRep (f1 :+: f2) g' +instance (g' ~ (g1 :*: g2), UnifyRep f1 g1, UnifyRep f2 g2) + => UnifyRep (f1 :*: f2) g' +instance (g' ~ K1 i b) => UnifyRep (K1 i a) g' +instance (g' ~ U1) => UnifyRep U1 g' +instance (g' ~ V1) => UnifyRep V1 g' + +-- | Can be used with @generic-lens@ for type-changing field updates. +-- +-- A specialization of the identity function to be used to fix types +-- of functions using 'Data' as input or output, unifying the "spines" of input +-- and output generic representations (the "spine" is everything except field +-- types, which may thus change). +onData + :: (UnifyRep (Rep a) (Rep b), UnifyRep (Rep a) (Rep b)) + => p a b -> p a b +onData = id diff --git a/test/lens-surgery.hs b/test/lens-surgery.hs new file mode 100644 --- /dev/null +++ b/test/lens-surgery.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE + DataKinds, + DeriveGeneric, + TypeApplications, + TypeOperators #-} + +{-# OPTIONS_GHC -Wno-unused-top-binds #-} + +import GHC.Generics (Generic) +import Test.Tasty +import Test.Tasty.HUnit + +import Data.Generics.Product (field) +import Data.Generics.Internal.VL.Lens + +import Generic.Data.Surgery (onData, toData) + +data T a = R { f :: a } deriving (Generic, Show) + +main :: IO () +main = defaultMain test + +show' :: Show (f ()) => f () -> String +show' = show + +test :: TestTree +test = testGroup "lens-surgery" + [ testCase "update" $ + "R {f = 42}" @?= (show' . onData (field @"f" .~ (42 :: Int)) . toData) (R ()) + ] diff --git a/test/surgery.hs b/test/surgery.hs new file mode 100644 --- /dev/null +++ b/test/surgery.hs @@ -0,0 +1,156 @@ +{-# LANGUAGE + CPP, + DataKinds, + DeriveGeneric, + FlexibleContexts, + TypeApplications, + TypeOperators #-} + +{-# OPTIONS_GHC -Wno-unused-top-binds #-} + +-- Many of these tests are more about ensuring things typecheck than really +-- comparing their runtime results. + +import Data.Bifunctor (second) +import Data.Functor.Identity +import GHC.Generics +import Test.Tasty +import Test.Tasty.HUnit + +import Generic.Data.Surgery + +import Generic.Data.Types (Data(Data)) + +data T = A | B Int | C Int Int Int Int Int deriving (Eq, Show, Generic) + +data P = P Int Int Int deriving (Eq, Show, Generic) +data R = R { u, v, w :: Int } deriving (Eq, Show, Generic) + +main :: IO () +main = defaultMain test + +show' :: Show (f ()) => f () -> String +show' = show + +unit :: f () -> f () +unit = id + +test :: TestTree +test = testGroup "surgery" + [ testRoundtrip + , testConsumer + , testProducer + ] + +rt :: (Eq a, Show a) => a -> (a -> a) -> Assertion +rt x f = x @?= f x + +testRoundtrip :: TestTree +testRoundtrip = testGroup "roundtrip" + [ testCase "to-from" $ rt (C 1 2 3 4 5) (fromOR . toOR) + , testCase "CField-rmv-ins" $ + rt (P 1 2 3) (fromOR . insertCField @1 . removeCField @1 . toOR) + , testCase "CField-ins-rmv" $ + rt ((), P 1 2 3) (fmap fromOR . removeCField @1 . insertCField @1 . fmap toOR) + , testCase "RField-rmv-ins" $ + rt (R 1 2 3) (fromOR . insertRField @"u" . removeRField @"u" . toOR) + , testCase "RField-ins-rmv" $ + rt ((), R 1 2 3) (fmap fromOR . removeRField @"t" . insertRField @"t" @1 . fmap toOR) +-- Type error on 8.0 +#if __GLASGOW_HASKELL__ >= 802 + , testCase "Constr-rmv-ins" $ + rt A (fromOR . insertConstrT @"A" . removeConstrT @"A" . toOR) +#endif + , testCase "Constr-ins-rmv" $ + rt (Right A) + (fmap fromOR . removeConstrT @"Z" . insertConstrT @"Z" @0 @() . fmap toOR) + ] + +testConsumer :: TestTree +testConsumer = testGroup "consumer" + [ testCase "removeCField" $ + "P 1 3" @?= + (show' . fromOR' . snd . removeCField @1 . toOR) (P 1 2 3) + + , testCase "removeRField" $ + "R {u = 1, w = 3}" @?= + (show' . fromOR' . snd . removeRField @"v" . toOR) (R 1 2 3) + + , testCase "insertCField" $ + "P 1 () 2 3" @?= + (show' . fromOR' . insertCField' @1 () . toOR) (P 1 2 3) + + , testCase "insertRField" $ + "R {u = 1, n = (), v = 2, w = 3}" @?= + (show' . fromOR' . insertRField' @"n" @1 () . toOR) (R 1 2 3) + +-- Loops on 8.0 +#if __GLASGOW_HASKELL__ >= 802 + -- N.B. Identity (for constructor B) is inferred. + , testCase "removeConstr" $ + "[Right A,Left (Identity 0),Right (C 1 2 3 4 5)]" @?= + (show . fmap (second (unit . fromOR') . removeConstrT @"B" . toOR)) + [A, B 0, C 1 2 3 4 5] + + , testCase "insertConstr" $ + "B 0" @?= (show . fromOR @T . insertConstrT @"B" . Left) (Identity 0) +#endif + ] + +testProducer :: TestTree +testProducer = testGroup "producer" + [ testCase "removeCField" $ + P 0 0 0 @?= + (fromOR . snd . removeCField @1 @[Int] . toOR') def + + , testCase "removeRField" $ + R 0 0 0 @?= + (fromOR . snd . removeRField @"v" @1 @[Int] . toOR') def + + , testCase "insertCField" $ + P 0 9 0 @?= + (fromOR . insertCField' @1 9 . toOR') def + + , testCase "insertCField" $ + R 0 9 0 @?= + (fromOR . insertRField' @"v" 9 . toOR') def + + , testCase "removeConstr" $ + Right A @?= + (fmap fromOR . removeConstrT @"D" @3 @() . toOR') def + + -- N.B. () (for constructor A) is inferred. + , testCase "insertConstr" $ + B 0 @?= + (fromOR . insertConstrT @"A" . Right . toOR') def + ] + +class Def a where + def :: a + +instance Def Int where + def = 0 + +instance Def [a] where + def = [] + +instance GDef f => Def (Data f x) where + def = Data gdef + +class GDef f where + gdef :: f x + +instance GDef f => GDef (M1 i c f) where + gdef = M1 gdef + +instance GDef f => GDef (f :+: g) where + gdef = L1 gdef + +instance (GDef f, GDef g) => GDef (f :*: g) where + gdef = gdef :*: gdef + +instance Def a => GDef (K1 i a) where + gdef = K1 def + +instance GDef U1 where + gdef = U1