diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for large-anon + +## 0.1.0.0 -- 2022-04-06 + +* First public release diff --git a/large-anon.cabal b/large-anon.cabal new file mode 100644 --- /dev/null +++ b/large-anon.cabal @@ -0,0 +1,186 @@ +cabal-version: 2.4 +name: large-anon +version: 0.1.0.0 +synopsis: Scalable anonymous records +description: The @large-anon@ package provides support for anonymous + records in Haskell, with a focus on compile-time (and + run-time) scalability. +bug-reports: https://github.com/well-typed/large-records/issues +license: BSD-3-Clause +author: Edsko de Vries +maintainer: edsko@well-typed.com +category: Records +extra-source-files: CHANGELOG.md +tested-with: GHC ==8.8.4 || ==8.10.7 || ==9.0.2 + +library + exposed-modules: + Data.Record.Anon + Data.Record.Anon.Simple + Data.Record.Anon.Advanced + Data.Record.Anon.Plugin + Data.Record.Anon.Plugin.Internal.Runtime + + other-modules: + -- Module organization: + -- + -- o The modules in @Core.*@ can only import from other modules in + -- @Core.*@ and modules in @Util.*@. + -- o The modules in the rest of @Internal.*@ can import from @Core.*@ and + -- @Util.*@, as well "Data.Record.Anon.Plugin.Internal.Runtime". + -- + -- See detailed discussion in the runtime module. + -- + + Data.Record.Anon.Internal.Util.SmallHashMap + Data.Record.Anon.Internal.Util.StrictArray + + Data.Record.Anon.Internal.Core.Canonical + Data.Record.Anon.Internal.Core.Diff + Data.Record.Anon.Internal.Core.FieldName + + Data.Record.Anon.Internal.Reflection + Data.Record.Anon.Internal.Advanced + Data.Record.Anon.Internal.Simple + + Data.Record.Anon.Internal.Plugin + + Data.Record.Anon.Internal.Plugin.TC.Constraints.AllFields + Data.Record.Anon.Internal.Plugin.TC.Constraints.KnownFields + Data.Record.Anon.Internal.Plugin.TC.Constraints.KnownHash + Data.Record.Anon.Internal.Plugin.TC.Constraints.RowHasField + Data.Record.Anon.Internal.Plugin.TC.Constraints.SubRow + Data.Record.Anon.Internal.Plugin.TC.EquivClasses + Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI + Data.Record.Anon.Internal.Plugin.TC.NameResolution + Data.Record.Anon.Internal.Plugin.TC.Parsing + Data.Record.Anon.Internal.Plugin.TC.Rewriter + Data.Record.Anon.Internal.Plugin.TC.Row.KnownField + Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow + Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow + Data.Record.Anon.Internal.Plugin.TC.Solver + Data.Record.Anon.Internal.Plugin.TC.TyConSubst + + Data.Record.Anon.Internal.Plugin.Source + Data.Record.Anon.Internal.Plugin.Source.GhcShim + Data.Record.Anon.Internal.Plugin.Source.Names + Data.Record.Anon.Internal.Plugin.Source.NamingT + Data.Record.Anon.Internal.Plugin.Source.Options + + build-depends: + base >= 4.13 && < 4.18 + , aeson >= 1.4.4 && < 2.1 + , containers >= 0.6.2 && < 0.7 + , ghc-tcplugin-api >= 0.7.1 && < 0.8 + , hashable >= 1.3 && < 1.4 + , mtl >= 2.2.1 && < 2.3 + , optics-core >= 0.3 && < 0.5 + , primitive >= 0.7.1 && < 0.8 + , record-hasfield >= 1.0 && < 1.1 + , sop-core >= 0.5 && < 0.6 + , syb >= 0.7 && < 0.8 + , tagged >= 0.8.6 && < 0.9 + , typelet >= 0.1 && < 0.2 + + -- large-generics 0.2 starts using 'SmallArray' instead of 'Vector' + , large-generics >= 0.2 && < 0.3 + + -- Whatever version is bundled with ghc + , ghc + hs-source-dirs: + src + default-language: + Haskell2010 + ghc-options: + -Wall + -Wredundant-constraints + -Wno-unticked-promoted-constructors + + if impl(ghc >= 8.10) + ghc-options: + -Wunused-packages + + if flag(debug) + build-depends: + recover-rtti >= 0.4.1 + cpp-options: + -DDEBUG + +test-suite test-large-anon + default-language: + Haskell2010 + type: + exitcode-stdio-1.0 + hs-source-dirs: + test + main-is: + TestLargeAnon.hs + other-modules: + Test.Infra.Generics + Test.Infra.MarkStrictness + Test.Infra.Discovery + Test.Infra.DynRecord + Test.Infra.DynRecord.Advanced + Test.Infra.DynRecord.Simple + Test.Prop.Record.Combinators.Constrained + Test.Prop.Record.Combinators.Simple + Test.Prop.Record.Model + Test.Prop.Record.Model.Generator + Test.Prop.Record.Model.Orphans + Test.Sanity.AllFields + Test.Sanity.Applicative + Test.Sanity.BlogPost + Test.Sanity.CheckIsSubRow + Test.Sanity.Discovery + Test.Sanity.DuplicateFields + Test.Sanity.Generics + Test.Sanity.HasField + Test.Sanity.Intersection + Test.Sanity.Merging + Test.Sanity.Named.Record1 + Test.Sanity.Named.Record2 + Test.Sanity.PolyKinds + Test.Sanity.RecordLens + Test.Sanity.Simple + Test.Sanity.SrcPlugin.WithoutTypelet + Test.Sanity.SrcPlugin.WithTypelet + Test.Sanity.TypeLevelMetadata + build-depends: + base + , aeson + , aeson-pretty + , bytestring + , large-anon + , large-generics + , mtl + , optics-core + , parsec + , QuickCheck + , record-dot-preprocessor + , sop-core + , tasty + , tasty-hunit + , tasty-quickcheck + , text + , typelet + , validation-selective + + -- required when using record-dot-preprocessor + , record-hasfield + ghc-options: + -Wall + -Wredundant-constraints + -Wno-unticked-promoted-constructors + -fno-show-valid-hole-fits + + if impl(ghc >= 8.10) + ghc-options: -Wunused-packages + + if impl(ghc >= 9.0.1) + -- Work out ghc problem. See more detailed discussion in large-records. + ghc-options: -Wno-unused-imports + +Flag debug + Description: Enable internal debugging features + Default: False + Manual: True diff --git a/src/Data/Record/Anon.hs b/src/Data/Record/Anon.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon.hs @@ -0,0 +1,78 @@ +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE PatternSynonyms #-} + +-- | Supporting definitions used by both the simple and the advanced interface +-- +-- To use the anonymous records library, you will want to use either the simple +-- interface in "Data.Record.Anon.Simple" or the advanced interface in +-- "Data.Record.Anon.Advanced". /This/ module provides definitions that are used +-- by both. Moreover, unlike @.Simple@ and @.Advanced@, this module is designed +-- to be imported unqualified. A typical import section will therefore look +-- something like +-- +-- > import Data.Record.Anon +-- > import Data.Record.Anon.Simple (Record) +-- > import qualified Data.Record.Anon.Simple as Anon +-- +-- In addition, since the classes and type families defined here as handled by +-- the plugin, you will also want to enable that: +-- +-- > {-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} +module Data.Record.Anon ( + -- * Rows + pattern (:=) + , Row + , Merge + + -- * Constraints + , AllFields + , KnownFields + , SubRow + , RowHasField + + -- * Fields + , Field + , KnownHash(..) + + -- * Type-level metadata + -- + -- | This is primarily for interop with @generics-sop@. + , FieldTypes + , SimpleFieldTypes + + -- * Type utilities + , Some(..) + , Reflected(..) + + -- * Re-exports + , module Data.Functor.Product + , module Data.Proxy + , module Data.SOP.BasicFunctors + , module Data.SOP.Classes + , module Data.SOP.Constraint + , module Data.SOP.Dict + , module GHC.Records.Compat + , module GHC.TypeLits + ) where + +-- We use explicit import lists for all modules we re-export, so that +-- Haddock knows what to include in the documentation (and moreover we don't +-- end up exporting something unexpected). + +import Data.Functor.Product (Product(..)) +import Data.Proxy (Proxy(..)) +import Data.SOP.BasicFunctors (I(..), K(..), (:.:)(..), unI) +import Data.SOP.Classes (type (-.->)(..)) +import Data.SOP.Constraint (Compose) +import Data.SOP.Dict (Dict(..)) +import GHC.Records.Compat (HasField(..)) +import GHC.TypeLits (KnownSymbol) + +import Data.Record.Anon.Plugin.Internal.Runtime +import Data.Record.Anon.Internal.Advanced (Field, Some(..)) +import Data.Record.Anon.Internal.Reflection (Reflected(Reflected)) + + + + + diff --git a/src/Data/Record/Anon/Advanced.hs b/src/Data/Record/Anon/Advanced.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Advanced.hs @@ -0,0 +1,568 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +-- | Advanced interface (with a functor argument) +-- +-- See "Data.Record.Anon.Simple" for the simple interface. +-- You will probably also want to import "Data.Record.Anon". +-- +-- Intended for qualified import. +-- +-- > import Data.Record.Anon +-- > import Data.Record.Anon.Advanced (Record) +-- > import qualified Data.Record.Anon.Advanced as Anon +module Data.Record.Anon.Advanced ( + Record + -- * Construction + , empty + , insert + , insertA + , applyPending + -- * Field access + , get + , set + -- * Changing rows + , project + , inject + , lens + , merge + -- * Combinators + -- ** " Functor " + , map + , cmap + -- ** " Applicable " + , pure + , cpure + , ap + -- ** " Foldable " + , collapse + , toList + -- ** " Traversable " + , mapM + , cmapM + , sequenceA + , sequenceA' + -- ** Zipping + , zip + , zipWith + , zipWithM + , czipWith + , czipWithM + -- * Constraint reification and reflection + , reifyAllFields + , reflectAllFields + , reifyKnownFields + , reflectKnownFields + , A.InRow(..) + , reifySubRow + , reflectSubRow + -- * Existential records + , A.SomeRecord(..) + , someRecord + -- * Experimental integration with @typelet@ + -- + -- | + -- The @typelet@ plugin provides support for type sharing. These functions + -- can be used to construct records that result in ghc core that is truly + -- linear in size. + , letRecordT + , letInsertAs + ) where + +import Prelude hiding (sequenceA, map, mapM, pure, zip, zipWith) + +import TypeLet + +import Data.Record.Anon + +import Data.Record.Anon.Internal.Advanced (Record) +import qualified Data.Record.Anon.Internal.Advanced as A + +-- $setup +-- >>> :set -XDataKinds +-- >>> :set -XOverloadedLabels +-- >>> :set -XTypeOperators +-- >>> :set -fplugin=TypeLet -fplugin=Data.Record.Anon.Plugin +-- >>> :set -dppr-cols=200 +-- >>> import Prelude hiding (pure) +-- >>> import qualified Prelude +-- >>> import Data.Record.Anon +-- >>> import TypeLet + +{------------------------------------------------------------------------------- + Construction + + Here and elsewhere, we don't just re-export the function, but instead provide + an alias for it. This means that all user-facing documentation and, + importantly, all docspec tests, are in public modules. + + Unfortunately, docspec (being ghci-based) cannot take advantage of the source + plugin, so we cannot give testable examples using ANON_F. +-------------------------------------------------------------------------------} + +-- | Empty record +empty :: Record f '[] +empty = A.empty + +-- | Insert new field +-- +-- >>> :{ +-- example :: Record Maybe [ "a" := Bool, "b" := Int ] +-- example = +-- insert #a (Just True) +-- $ insert #b Nothing +-- $ empty +-- :} +-- +-- Instead of using 'insert' and 'empty', you can also write this as +-- +-- > example = ANON_F { +-- > a = Just True +-- > , b = Nothing +-- > } +insert :: Field n -> f a -> Record f r -> Record f (n := a : r) +insert = A.insert + +-- | Applicative insert +-- +-- This is a simple wrapper around 'insert', but can be quite useful when +-- constructing records. Consider code like +-- +-- >>> :{ +-- example :: Applicative m => m a -> m b -> m (a, b) +-- example ma mb = (,) <$> ma <*> mb +-- :} +-- +-- We cannot really extend this to the world of named records, but we /can/ +-- do something comparable using anonymous records: +-- +-- >>> :{ +-- example :: +-- Applicative m +-- => m (f a) -> m (f b) -> m (Record f [ "a" := a, "b" := b ]) +-- example ma mb = +-- insertA #a ma +-- $ insertA #b mb +-- $ Prelude.pure empty +-- :} +-- +-- As for regular 'insert', this example too can instead be written using +-- @ANON_F@ and 'sequenceA' (or 'sequenceA''). +-- +-- > example ma mb = sequenceA $ ANON_F { +-- > a = Comp ma +-- > , b = Comp mb +-- > } +insertA :: + Applicative m + => Field n -> m (f a) -> m (Record f r) -> m (Record f (n ':= a : r)) +insertA = A.insertA + +-- | Apply all pending changes to the record +-- +-- Updates to a record are stored in a hashtable. As this hashtable grows, +-- record field access and update will become more expensive. Applying the +-- updates, resulting in a flat vector, is an @O(n)@ operation. This will happen +-- automatically whenever another @O(n)@ operation is applied (for example, +-- mapping a function over the record). However, occassionally it is useful to +-- explicitly apply these changes, for example after constructing a record or +-- updating a lot of fields. +applyPending :: Record f r -> Record f r +applyPending = A.applyPending + +{------------------------------------------------------------------------------- + Field access +-------------------------------------------------------------------------------} + +-- | Get field from the record +-- +-- This is just a wrapper around 'getField'. +-- +-- >>> :{ +-- example :: Record Maybe [ "a" := Bool, "b" := Int ] -> Maybe Bool +-- example r = get #a r +-- :} +-- +-- If using @record-dot-preprocessor@, you can also write this example as +-- +-- > example r = r.a +-- +-- If the field does not exist, you will get a type error about an unsolvable +-- 'RowHasField' constraint: +-- +-- >>> :{ +-- absentField :: Record Maybe [ "a" := Bool, "b" := Int ] -> Maybe Char +-- absentField r = get #c r +-- :} +-- ... +-- ...No instance for (RowHasField "c"... +-- ... +-- +-- Type mismatches will result in regular type errors: +-- +-- >>> :{ +-- wrongType :: Record Maybe [ "a" := Bool, "b" := Int ] -> Maybe Char +-- wrongType r = get #a r +-- :} +-- ... +-- ...Couldn't match...Char...Bool... +-- ... +-- +-- When part of the record is not known, it might not be possible to resolve a +-- 'HasField' constraint until later. For example, in +-- +-- >>> :{ +-- unknownField :: Record Maybe [ x := Bool, "b" := Int ] -> Maybe Int +-- unknownField r = get #b r +-- :} +-- ... +-- ...No instance for (RowHasField "b"... +-- ... +-- +-- (Note that @x@ here is a variable, not a string.) It is important that the +-- constraint remains unsolved in this example, because if @x == "b"@, the first +-- field would shadow the second, and the result type should be @Maybe Bool@ +-- instead of @Maybe Int@. +get :: RowHasField n r a => Field n -> Record f r -> f a +get = A.get + +-- | Update field in the record +-- +-- This is just a wrapper around 'setField'. +-- +-- >>> :{ +-- example :: +-- Record Maybe [ "a" := Bool, "b" := Int ] +-- -> Record Maybe [ "a" := Bool, "b" := Int ] +-- example r = set #a (Just False) r +-- :} +-- +-- If using @record-dot-preprocessor@, can also write this example as +-- +-- > example r = r{a = Just False} +set :: RowHasField n r a => Field n -> f a -> Record f r -> Record f r +set = A.set + +{------------------------------------------------------------------------------- + Changing rows +-------------------------------------------------------------------------------} + +-- | Project from one record to another +-- +-- Both the source record and the target record must be fully known. +-- +-- The target record can omit fields from the source record, as well as +-- rearrange them: +-- +-- >>> :{ +-- example :: +-- Record f [ "a" := Char, "b" := Int, "c" := Bool ] +-- -> Record f [ "c" := Bool, "a" := Char ] +-- example = project +-- :} +-- +-- Of course, it is not possible to /add/ fields: +-- +-- >>> :{ +-- example :: +-- Record f [ "c" := Bool, "a" := Char ] +-- -> Record f [ "a" := Char, "b" := Int, "c" := Bool ] +-- example = project +-- :} +-- ... +-- ...No instance for (SubRow... +-- ... +-- +-- Type inference will work through projections: field types are unified based +-- on their name: +-- +-- >>> :{ +-- example :: +-- Record f [ "a" := Char, "b" := Int, "c" := Bool ] +-- -> Record f [ "c" := _, "a" := Char ] +-- example = project +-- :} +-- ... +-- ...Found type wildcard...Bool... +-- ... +-- +-- As we saw in 'merge', 'project' can also flatten 'Merge'd rows. +project :: SubRow r r' => Record f r -> Record f r' +project = A.project + +-- | Inject smaller record into larger record +-- +-- This is just the 'lens' setter. +inject :: SubRow r r' => Record f r' -> Record f r -> Record f r +inject = A.inject + +-- | Lens from one record to another +-- +-- See 'project' for examples ('project' is just the lens getter, without the +-- setter). +lens :: + SubRow r r' + => Record f r -> (Record f r', Record f r' -> Record f r) +lens = A.lens + +-- | Merge two records +-- +-- The 'Merge' type family does not reduce: +-- +-- >>> :{ +-- example :: Record Maybe (Merge '[ "a" := Bool ] '[]) +-- example = merge (insert #a (Just True) empty) empty +-- :} +-- +-- If you want to flatten the row after merging, you can use 'project': +-- +-- >>> :{ +-- example :: Record Maybe '[ "a" := Bool ] +-- example = project $ merge (insert #a (Just True) empty) empty +-- :} +-- +-- 'HasField' constraints can be resolved for merged records, subject to the +-- same condition discussed in 'get': all fields in the record must be known up +-- to the requested field (in case of shadowing). So the record /may/ be fully +-- known: +-- +-- >>> :{ +-- example :: Record f (Merge '[ "a" := Bool ] '[ "b" := Char ]) -> f Char +-- example r = get #b r +-- :} +-- +-- but it doesn't have to be: +-- +-- >>> :{ +-- example :: Record I (Merge '[ "a" := Bool ] r) -> I Bool +-- example = get #a +-- :} +-- +-- However, just like in the case of unknown fields (see example in 'get'), +-- if earlier parts in the record are unknown we get type error: +-- +-- >>> :{ +-- example :: Record I (Merge r '[ "b" := Char ]) -> I Char +-- example r = get #b r +-- :} +-- ... +-- ...No instance for (RowHasField "b"... +-- ... +merge :: Record f r -> Record f r' -> Record f (Merge r r') +merge = A.merge + +{------------------------------------------------------------------------------- + Combinators +-------------------------------------------------------------------------------} + +-- | Analogue to 'Prelude.fmap' +map :: (forall x. f x -> g x) -> Record f r -> Record g r +map f = A.map f + +-- | Analogue to 'Prelude.mapM' +mapM :: Applicative m => (forall x. f x -> m (g x)) -> Record f r -> m (Record g r) +mapM f = A.mapM f + +-- | Constrained form of 'map' +cmap :: + AllFields r c + => Proxy c -> (forall x. c x => f x -> g x) -> Record f r -> Record g r +cmap p f = A.cmap p f + +-- | Constrained form of 'cmap' +cmapM :: + (Applicative m, AllFields r c) + => Proxy c + -> (forall x. c x => f x -> m (g x)) + -> Record f r -> m (Record g r) +cmapM p f = A.cmapM p f + +-- | Analogue of 'Prelude.pure' +pure :: KnownFields r => (forall x. f x) -> Record f r +pure f = A.pure f + +-- | Constrained form of 'pure' +cpure :: AllFields r c => Proxy c -> (forall x. c x => f x) -> Record f r +cpure p f = A.cpure p f + +-- | Analogue of '<*>' +ap :: Record (f -.-> g) r -> Record f r -> Record g r +ap = A.ap + +-- | Analogue of 'Data.Foldable.toList' +collapse :: Record (K a) r -> [a] +collapse = A.collapse + +-- | Like 'collapse', but also include field names +toList :: KnownFields r => Record (K a) r -> [(String, a)] +toList = A.toList + +-- | Analogue of 'Prelude.sequenceA' +sequenceA :: Applicative m => Record (m :.: f) r -> m (Record f r) +sequenceA = A.sequenceA + +-- | Simplified form of 'sequenceA' +sequenceA' :: Applicative m => Record m r -> m (Record I r) +sequenceA' = A.sequenceA' + +-- | Analogue of 'Prelude.zip' +zip :: Record f r -> Record g r -> Record (Product f g) r +zip = A.zip + +-- | Analogue of 'Prelude.zipWith' +zipWith :: + (forall x. f x -> g x -> h x) + -> Record f r -> Record g r -> Record h r +zipWith f = A.zipWith f + +-- | Analogue of 'Control.Monad.zipWithM' +zipWithM :: + Applicative m + => (forall x. f x -> g x -> m (h x)) + -> Record f r -> Record g r -> m (Record h r) +zipWithM f = A.zipWithM f + +-- | Constrained form of 'zipWith' +czipWith :: + AllFields r c + => Proxy c + -> (forall x. c x => f x -> g x -> h x) + -> Record f r -> Record g r -> Record h r +czipWith p f = A.czipWith p f + +-- | Constrained form of 'zipWithM' +czipWithM :: + (Applicative m, AllFields r c) + => Proxy c + -> (forall x. c x => f x -> g x -> m (h x)) + -> Record f r -> Record g r -> m (Record h r) +czipWithM p f = A.czipWithM p f + +{------------------------------------------------------------------------------- + Constraint reification and reflection +-------------------------------------------------------------------------------} + +-- | Record of dictionaries +-- +-- This reifies an 'AllFields' constraint as a record. +-- +-- Inverse to 'reflectKnownFields'. +reifyAllFields :: AllFields r c => proxy c -> Record (Dict c) r +reifyAllFields = A.reifyAllFields + +-- | Establish 'AllFields' from a record of dictionaries +-- +-- Inverse to 'reifyKnownFields'. +reflectAllFields :: Record (Dict c) r -> Reflected (AllFields r c) +reflectAllFields = A.reflectAllFields + +-- | Record of field names +-- +-- This reifies a 'KnownFields' constraint as a record. +-- +-- Inverse to 'reflectAllFields'. +reifyKnownFields :: KnownFields r => proxy r -> Record (K String) r +reifyKnownFields = A.reifyKnownFields + +-- | Establish 'KnownFields' from a record of field names +-- +-- Inverse to 'reifyAllFields'. +reflectKnownFields :: Record (K String) r -> Reflected (KnownFields r) +reflectKnownFields = A.reflectKnownFields + +-- | Record over @r'@ with evidence that every field is in @r@. +-- +-- This reifies a 'SubRow' constraint. +-- +-- Inverse to 'reflectSubRow'. +reifySubRow :: (KnownFields r', SubRow r r') => Record (A.InRow r) r' +reifySubRow = A.reifySubRow + +-- | Establish 'SubRow' from a record of evidence. +-- +-- Inverse to 'reifySubRow'. +reflectSubRow :: Record (A.InRow r) r' -> Reflected (SubRow r r') +reflectSubRow = A.reflectSubRow + +{------------------------------------------------------------------------------- + Existential records +-------------------------------------------------------------------------------} + +-- | Construct record with existentially quantified row variable +-- +-- Existentially quantified records arise for example when parsing JSON values +-- as records. Pattern matching on the result of 'someRecord' brings into scope +-- an existentially quantified row variable @r@, along with a record over @r@; +-- every field in record contains the value specified, as well as evidence that +-- that that field is indeed an element of @r@. +-- +-- For such a record to be useful, you will probably want to prove additional +-- constraints @AllFields r c@; you can do this using 'reflectAllFields', +-- provided that you carefully pick your @f@ such that you can define a function +-- +-- > fieldSatisfiesC :: forall c. f x -> Dict c x +-- +-- for every @c@ you want to prove. +-- +-- It is also possible to do a runtime check to see if the existential row @r@ +-- can be projected to some concrete known row @r'@. To do this, construct a +-- record of evidence with type +-- +-- > Record (InRow r) r' +-- +-- and then call 'reflectSubRow'. To construct this record of evidence you will +-- need to do a runtime type check to verify that the types of the fields in +-- concrete row match the types of the corresponding fields in the inferred row +-- (the inferred row may contain fields that are not present in the concrete +-- row, of course). An obvious candidate for doing this is +-- 'Data.Typeable.Typeable', but for specific applications (with specific +-- subsets of types of interest) other choices may be possible also. +-- +-- The @large-anon@ test suite contains examples of doing both of these things; +-- see @Test.Infra.DynRecord.Simple@ (or @Test.Infra.DynRecord.Advanced@ for +-- rows over kind other than @Type@) for examples of proving additional +-- constraints, and @Test.Infra.Discovery@ for an example of how you could do a +-- projection check. +someRecord :: [(String, Some f)] -> A.SomeRecord f +someRecord = A.someRecord + +{------------------------------------------------------------------------------- + Experimental integration with @typelet@ +-------------------------------------------------------------------------------} + +-- | Introduce type variable for a row +-- +-- This can be used in conjunction with 'letInsertAs': +-- +-- >>> :{ +-- example :: Record I '[ "a" := Int, "b" := Char, "c" := Bool ] +-- example = letRecordT $ \p -> castEqual $ +-- letInsertAs p #c (I True) empty $ \xs02 -> +-- letInsertAs p #b (I 'X' ) xs02 $ \xs01 -> +-- letInsertAs p #a (I 1 ) xs01 $ \xs00 -> +-- castEqual xs00 +-- :} +letRecordT :: forall r f. + (forall r'. Let r' r => Proxy r' -> Record f r) + -> Record f r +letRecordT f = A.letRecordT f + +-- | Insert field into a record and introduce type variable for the result +letInsertAs :: forall r r' f n a. + Proxy r -- ^ Type of the record we are constructing + -> Field n -- ^ New field to be inserted + -> f a -- ^ Value of the new field + -> Record f r' -- ^ Record constructed so far + -> (forall r''. Let r'' (n := a : r') => Record f r'' -> Record f r) + -- ^ Assign type variable to new partial record, and continue + -> Record f r +letInsertAs p n x r f = A.letInsertAs p n x r f + + + diff --git a/src/Data/Record/Anon/Internal/Advanced.hs b/src/Data/Record/Anon/Internal/Advanced.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Advanced.hs @@ -0,0 +1,655 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} + +-- | Full record representation +-- +-- Intended for qualified import. +-- +-- > import Data.Record.Anon.Internal.Advanced (Record) +-- > import qualified Data.Record.Anon.Internal.Advanced as A +module Data.Record.Anon.Internal.Advanced ( + -- * Definition + Record -- opaque + -- * Main API + , Field(..) + , empty + , insert + , insertA + , get + , set + , merge + , lens + , project + , inject + , applyPending + -- * Combinators + -- ** " Foldable " + , map + , cmap + -- ** " Applicable " + , pure + , cpure + , ap + -- ** " Foldable " + , collapse + , toList + -- ** " Traversable " + , mapM + , cmapM + , sequenceA + , sequenceA' + -- ** Zipping + , zip + , zipWith + , zipWithM + , czipWith + , czipWithM + -- * Reification and reflection + , reifyKnownFields + , reflectKnownFields + , reifyAllFields + , reflectAllFields + , InRow(..) + , reifySubRow + , reflectSubRow + -- * Existential records + , Some(..) + , SomeRecord(..) + , someRecord + -- * Support for @typelet@ + , letRecordT + , letInsertAs + ) where + +import Prelude hiding (map, mapM, zip, zipWith, sequenceA, pure) +import qualified Prelude + +import Data.Aeson (ToJSON(..), FromJSON(..)) +import Data.Bifunctor +import Data.Coerce (coerce) +import Data.Functor.Product +import Data.Kind +import Data.Primitive.SmallArray +import Data.Proxy +import Data.Record.Generic hiding (FieldName) +import Data.SOP.Classes (fn_2) +import Data.SOP.Constraint +import Data.Tagged +import GHC.Exts (Any) +import GHC.OverloadedLabels +import GHC.Records.Compat +import GHC.TypeLits +import TypeLet.UserAPI + +import qualified Optics.Core as Optics + +import qualified Data.Record.Generic.Eq as Generic +import qualified Data.Record.Generic.JSON as Generic +import qualified Data.Record.Generic.Show as Generic + +import Data.Record.Anon.Internal.Core.Canonical (Canonical) +import Data.Record.Anon.Internal.Core.Diff (Diff) +import Data.Record.Anon.Internal.Core.FieldName +import Data.Record.Anon.Internal.Reflection (Reflected(..)) +import Data.Record.Anon.Internal.Util.StrictArray (StrictArray) + +import Data.Record.Anon.Plugin.Internal.Runtime + +import qualified Data.Record.Anon.Internal.Core.Canonical as Canon +import qualified Data.Record.Anon.Internal.Core.Diff as Diff +import qualified Data.Record.Anon.Internal.Reflection as Unsafe +import qualified Data.Record.Anon.Internal.Util.StrictArray as Strict + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Anonymous record +data Record (f :: k -> Type) (r :: Row k) = + NoPending {-# UNPACK #-} !(Canonical f) + | HasPending {-# UNPACK #-} !(Canonical f) !(Diff f) + +{------------------------------------------------------------------------------- + Conversion +-------------------------------------------------------------------------------} + +-- | Construct canonical form of the record (i.e., apply the internal 'Diff') +-- +-- This is @O(n)@, and should be done only for operations on records that are +-- @O(n)@ /anyway/, so that the cost can be absorbed. +toCanonical :: Record f r -> Canonical f +toCanonical (NoPending c) = c +toCanonical (HasPending c d) = Diff.apply d c + +-- | Construct 'Record' from 'Canonical' representation (empty 'Diff') +-- +-- This function is unsafe because we cannot verify whether the record matches +-- it's row specification @r@. +unsafeFromCanonical :: Canonical f -> Record f r +unsafeFromCanonical = NoPending + +{------------------------------------------------------------------------------- + HasField +-------------------------------------------------------------------------------} + +-- | Proxy for a field name, with 'IsLabel' instance +-- +-- The 'IsLabel' instance makes it possible to write +-- +-- > #foo +-- +-- to mean +-- +-- > Field (Proxy @"foo") +data Field n where + Field :: (KnownSymbol n, KnownHash n) => Proxy n -> Field n + +instance (n ~ n', KnownSymbol n, KnownHash n) => IsLabel n' (Field n) where + fromLabel = Field (Proxy @n) + +instance forall k (n :: Symbol) (f :: k -> Type) (r :: Row k) (a :: k). + (KnownSymbol n, KnownHash n, RowHasField n r a) + => HasField n (Record f r) (f a) where + + -- INLINE pragma important: it makes the 'NoPendingCases' cases very close + -- to the performance of using a 'SmallArray' directly. + {-# INLINE hasField #-} + hasField r = ( + \x -> unsafeSetField ix name x r + , unsafeGetField ix name r + ) + where + name :: FieldName + name = mkFieldName (Proxy @n) + + ix :: Int + ix = proxy rowHasField (Proxy @'(n, r, a)) + +-- | Compile-time construction of a 'FieldName' +mkFieldName :: (KnownSymbol n, KnownHash n) => Proxy n -> FieldName +mkFieldName p = FieldName (hashVal p) (symbolVal p) + +instance (RowHasField n r a, KnownSymbol n, KnownHash n) + => Optics.LabelOptic n Optics.A_Lens (Record f r) (Record f r) (f a) (f a) where + labelOptic = aux (fromLabel @n) + where + aux :: Field n -> Optics.Lens' (Record f r) (f a) + aux n = Optics.lens (get n) (flip (set n)) + +-- | Low level field accessor +-- +-- It is the responsibility of the plugin to ensure that the field index and +-- the field type match. +unsafeGetField :: forall k (f :: k -> Type) (r :: Row k) (a :: k). + Int -> FieldName -> Record f r -> f a +unsafeGetField i n = co . \case + NoPending c -> Canon.getAtIndex c i + HasPending c d -> Diff.get (i, n) d c + where + co :: f Any -> f a + co = noInlineUnsafeCo + +-- | Low level field update +-- +-- See comments in 'getField'. +unsafeSetField :: forall k (f :: k -> Type) (r :: Row k) (a :: k). + Int -> FieldName -> f a -> Record f r -> Record f r +unsafeSetField i n x = \case + NoPending c -> HasPending c (go Diff.empty) + HasPending c d -> HasPending c (go d) + where + go :: Diff f -> Diff f + go = Diff.set (i, n) (co x) + + co :: f a -> f Any + co = noInlineUnsafeCo + +get :: forall n f r a. + RowHasField n r a + => Field n -> Record f r -> f a +get (Field _) = getField @n @(Record f r) + +set :: forall n f r a. + RowHasField n r a + => Field n -> f a -> Record f r -> Record f r +set (Field _) = flip (setField @n @(Record f r)) + +{------------------------------------------------------------------------------- + Main API +-------------------------------------------------------------------------------} + +empty :: Record f '[] +empty = NoPending mempty + +insert :: forall k (f :: k -> Type) (r :: Row k) (a :: k) (n :: Symbol). + Field n -> f a -> Record f r -> Record f (n := a : r) +insert (Field n) x = \case + NoPending c -> HasPending c (go Diff.empty) + HasPending c d -> HasPending c (go d) + where + go :: Diff f -> Diff f + go = Diff.insert (mkFieldName n) (co x) + + co :: f a -> f Any + co = noInlineUnsafeCo + +insertA :: + Applicative m + => Field n -> m (f a) -> m (Record f r) -> m (Record f (n := a : r)) +insertA f x r = insert f <$> x <*> r + +merge :: Record f r -> Record f r' -> Record f (Merge r r') +merge (toCanonical -> r) (toCanonical -> r') = + unsafeFromCanonical $ r <> r' + +lens :: forall f r r'. + SubRow r r' + => Record f r -> (Record f r', Record f r' -> Record f r) +lens = \(toCanonical -> r) -> + bimap getter setter $ + Canon.lens (proxy projectIndices (Proxy @'(r, r'))) r + where + getter :: Canonical f -> Record f r' + getter = unsafeFromCanonical + + setter :: (Canonical f -> Canonical f) -> Record f r' -> Record f r + setter f (toCanonical -> r) = unsafeFromCanonical (f r) + +-- | Project out subrecord +-- +-- This is just the 'lens' getter. +project :: SubRow r r' => Record f r -> Record f r' +project = fst . lens + +-- | Inject subrecord +-- +-- This is just the 'lens' setter. +inject :: SubRow r r' => Record f r' -> Record f r -> Record f r +inject small = ($ small) . snd . lens + +applyPending :: Record f r -> Record f r +applyPending (toCanonical -> r) = unsafeFromCanonical r + +{------------------------------------------------------------------------------- + Unconstrained combinators +-------------------------------------------------------------------------------} + +map :: (forall x. f x -> g x) -> Record f r -> Record g r +map f (toCanonical -> r) = unsafeFromCanonical $ + Canon.map f r + +mapM :: + Applicative m + => (forall x. f x -> m (g x)) + -> Record f r -> m (Record g r) +mapM f (toCanonical -> r) = fmap unsafeFromCanonical $ + Canon.mapM f r + +zip :: Record f r -> Record g r -> Record (Product f g) r +zip = zipWith Pair + +zipWith :: + (forall x. f x -> g x -> h x) + -> Record f r -> Record g r -> Record h r +zipWith f (toCanonical -> r) (toCanonical -> r') = unsafeFromCanonical $ + Canon.zipWith f r r' + +zipWithM :: + Applicative m + => (forall x. f x -> g x -> m (h x)) + -> Record f r -> Record g r -> m (Record h r) +zipWithM f (toCanonical -> r) (toCanonical -> r') = fmap unsafeFromCanonical $ + Canon.zipWithM f r r' + +collapse :: Record (K a) r -> [a] +collapse (toCanonical -> r) = + Canon.collapse r + +sequenceA :: Applicative m => Record (m :.: f) r -> m (Record f r) +sequenceA (toCanonical -> r) = fmap unsafeFromCanonical $ + Canon.sequenceA r + +sequenceA' :: Applicative m => Record m r -> m (Record I r) +sequenceA' = sequenceA . co + where + co :: Record m r -> Record (m :.: I) r + co = noInlineUnsafeCo + +pure :: forall f r. KnownFields r => (forall x. f x) -> Record f r +pure f = unsafeFromCanonical $ + Canon.fromList $ Prelude.map (const f) (proxy fieldNames (Proxy @r)) + +ap :: Record (f -.-> g) r -> Record f r -> Record g r +ap (toCanonical -> r) (toCanonical -> r') = unsafeFromCanonical $ + Canon.ap r r' + +{------------------------------------------------------------------------------- + Reification and reflection + + The @KnownFields@ constraint on @reifyProject@ is a little dissatisfying, as + it feels like an orthogonal concern. Ultimately the reason is that in + + > Record f (r :: Row k) + + we have @f :: k -> Type@, as opposed to @f :: Symbol -> k -> Type@. That is + a generalization we could at some point consider, but until we do, the + + > RowHasField n r a + + constraint introduced in the body 'InRow' involves an /existential/ @n@; + a /separate/ record with 'KnownSymbol' evidence would therefore not give us + any information about /this/ @n@. +-------------------------------------------------------------------------------} + +reifyKnownFields :: forall k (r :: Row k) proxy. + KnownFields r + => proxy r -> Record (K String) r +reifyKnownFields _ = + unsafeFromCanonical $ + Canon.fromList $ co $ proxy fieldNames (Proxy @r) + where + co :: [String] -> [K String Any] + co = coerce + +reflectKnownFields :: forall k (r :: Row k). + Record (K String) r + -> Reflected (KnownFields r) +reflectKnownFields names = + Unsafe.reflectKnownFields $ Tagged $ collapse names + +reifyAllFields :: forall k (r :: Row k) (c :: k -> Constraint) proxy. + AllFields r c + => proxy c -> Record (Dict c) r +reifyAllFields _ = unsafeFromCanonical $ + Canon.fromVector . Strict.fromLazy $ + fmap aux $ proxy fieldDicts (Proxy @r) + where + aux :: DictAny c -> Dict c Any + aux DictAny = Dict + +reflectAllFields :: forall k (c :: k -> Constraint) (r :: Row k). + Record (Dict c) r + -> Reflected (AllFields r c) +reflectAllFields dicts = + Unsafe.reflectAllFields $ Tagged $ + fmap aux $ Strict.toLazy $ Canon.toVector $ toCanonical dicts + where + aux :: Dict c Any -> DictAny c + aux Dict = DictAny + +-- | @InRow r a@ is evidence that there exists some @n@ s.t. @(n := a)@ in @r@. +data InRow (r :: Row k) (a :: k) where + InRow :: forall k (n :: Symbol) (r :: Row k) (a :: k). + ( KnownSymbol n + , RowHasField n r a + ) + => Proxy n -> InRow r a + +reifySubRow :: forall k (r :: Row k) (r' :: Row k). + (SubRow r r', KnownFields r') + => Record (InRow r) r' +reifySubRow = + zipWith aux ixs (reifyKnownFields (Proxy @r')) + where + ixs :: Record (K Int) r' + ixs = unsafeFromCanonical $ + Canon.fromVector $ co $ proxy projectIndices (Proxy @'(r, r')) + + co :: StrictArray Int -> StrictArray (K Int Any) + co = coerce + + aux :: forall x. K Int x -> K String x -> InRow r x + aux (K i) (K name) = + case someSymbolVal name of + SomeSymbol p -> unsafeInRow i p + +reflectSubRow :: forall k (r :: Row k) (r' :: Row k). + Record (InRow r) r' + -> Reflected (SubRow r r') +reflectSubRow (toCanonical -> ixs) = + Unsafe.reflectSubRow $ Tagged $ + (\inRow@(InRow p) -> aux inRow p) <$> Canon.toVector ixs + where + aux :: forall x n. RowHasField n r x => InRow r x -> Proxy n -> Int + aux _ _ = proxy rowHasField (Proxy @'(n, r, x)) + +unsafeInRow :: forall n r a. KnownSymbol n => Int -> Proxy n -> InRow r a +unsafeInRow i p = + case reflected of + Reflected -> InRow p + where + reflected :: Reflected (RowHasField n r a) + reflected = Unsafe.reflectRowHasField $ Tagged i + +{------------------------------------------------------------------------------- + Existential records +-------------------------------------------------------------------------------} + +-- | Existential type ("there exists an @x@ such that @f x@") +data Some (f :: k -> Type) where + Some :: forall k (f :: k -> Type) (x :: k). f x -> Some f + +-- | Discovered row variable +-- +-- See 'Data.Record.Anon.Advanced.someRecord' for detailed discussion. +data SomeRecord (f :: k -> Type) where + SomeRecord :: forall k (r :: Row k) (f :: k -> Type). + KnownFields r + => Record (Product (InRow r) f) r + -> SomeRecord f + +someRecord :: forall k (f :: k -> Type). [(String, Some f)] -> SomeRecord f +someRecord fields = + mkSomeRecord $ + unsafeFromCanonical . Canon.fromList $ + Prelude.zipWith aux [0..] (Prelude.map (first someSymbolVal) fields) + where + aux :: Int -> (SomeSymbol, Some f) -> Product (InRow r) f Any + aux i (SomeSymbol n, Some fx) = Pair (unsafeInRow i n) (co fx) + + co :: f x -> f Any + co = noInlineUnsafeCo + + mkSomeRecord :: forall r. Record (Product (InRow r) f) r -> SomeRecord f + mkSomeRecord r = + case reflected of + Reflected -> SomeRecord r + where + reflected :: Reflected (KnownFields r) + reflected = reflectKnownFields $ map getName r + + getName :: Product (InRow r) f x -> K String x + getName (Pair (InRow p) _) = K $ symbolVal p + +{------------------------------------------------------------------------------- + Conversion to/from generic 'Rep' +-------------------------------------------------------------------------------} + +recordToRep :: Record f r -> Rep I (Record f r) +recordToRep (toCanonical -> r) = + Rep $ co . Strict.toLazy . Canon.toVector $ r + where + -- Second @Any@ is really (f (Any)) + co :: SmallArray (f Any) -> SmallArray (I Any) + co = noInlineUnsafeCo + +repToRecord :: Rep I (Record f r) -> Record f r +repToRecord (Rep r) = + unsafeFromCanonical $ Canon.fromVector . Strict.fromLazy . co $ r + where + -- First @Any@ is really (f Any)@ + co :: SmallArray (I Any) -> SmallArray (f Any) + co = noInlineUnsafeCo + +{------------------------------------------------------------------------------- + Generics instance +-------------------------------------------------------------------------------} + +class (AllFields r (Compose c f), KnownFields r) => RecordConstraints f r c +instance (AllFields r (Compose c f), KnownFields r) => RecordConstraints f r c + +recordConstraints :: forall f r c. + RecordConstraints f r c + => Proxy c -> Rep (Dict c) (Record f r) +recordConstraints _ = Rep $ + co . aux <$> proxy fieldDicts (Proxy @r) + where + aux :: DictAny (Compose c f) -> Dict (Compose c f) Any + aux DictAny = Dict + + -- The second 'Any' is really (f Any) + co :: Dict (Compose c f) Any -> Dict c Any + co = noInlineUnsafeCo + +recordMetadata :: forall k (f :: k -> Type) (r :: Row k). + KnownFields r + => Metadata (Record f r) +recordMetadata = Metadata { + recordName = "Record" + , recordConstructor = "Record" + , recordSize = length fields + , recordFieldMetadata = Rep $ smallArrayFromList fields + } + where + fields :: [FieldMetadata Any] + fields = fieldMetadata (Proxy @r) + +instance KnownFields r => Generic (Record f r) where + type Constraints (Record f r) = RecordConstraints f r + type MetadataOf (Record f r) = FieldTypes f r + + from = recordToRep + to = repToRecord + dict = recordConstraints + metadata = const recordMetadata + +{------------------------------------------------------------------------------- + Instances for standard type classes + + These instances all depend on the generics integration. +-------------------------------------------------------------------------------} + +instance RecordConstraints f r Show => Show (Record f r) where + showsPrec = Generic.gshowsPrec + +instance RecordConstraints f r Eq => Eq (Record f r) where + (==) = Generic.geq + +instance ( RecordConstraints f r Eq + , RecordConstraints f r Ord + ) => Ord (Record f r) where + compare = Generic.gcompare + +instance RecordConstraints f r ToJSON => ToJSON (Record f r) where + toJSON = Generic.gtoJSON + +instance RecordConstraints f r FromJSON => FromJSON (Record f r) where + parseJSON = Generic.gparseJSON + +{------------------------------------------------------------------------------- + UTIL. Not sure if we still need this +-------------------------------------------------------------------------------} + +{- + +data Constrained (c :: k -> Constraint) (f :: k -> Type) (x :: k) where + Constrained :: c x => f x -> Constrained c f x + +constrain :: forall k (c :: k -> Constraint) (f :: k -> Type) (r :: Row k). + AllFields r c + => Proxy c -> Record f r -> Record (Constrained c f) r +constrain p (Record.toCanonical -> r) = Record.unsafeFromCanonical $ + Canon.fromLazyVector $ + V.zipWith aux (Canon.toLazyVector r) (fieldDicts (Proxy @r) p) + where + aux :: f Any -> DictAny c -> Constrained c f Any + aux x DictAny = Constrained x + +-} + +{------------------------------------------------------------------------------- + Constrained combinators +-------------------------------------------------------------------------------} + +cpure :: forall r f c. + AllFields r c + => Proxy c + -> (forall x. c x => f x) + -> Record f r +cpure p f = map (\Dict -> f) $ reifyAllFields p + +cmap :: forall r c f g. + AllFields r c + => Proxy c + -> (forall x. c x => f x -> g x) + -> Record f r -> Record g r +cmap p f = zipWith (\Dict -> f) (reifyAllFields p) + +cmapM :: + (Applicative m, AllFields r c) + => Proxy c + -> (forall x. c x => f x -> m (g x)) + -> Record f r -> m (Record g r) +cmapM p f = sequenceA . cmap p (Comp . f) + +toList :: forall r a. KnownFields r => Record (K a) r -> [(String, a)] +toList = Prelude.zipWith aux (fieldMetadata (Proxy @r)) . collapse + where + aux :: FieldMetadata b -> a -> (String, a) + aux (FieldMetadata p _) a = (symbolVal p, a) + +czipWithM :: forall m r c f g h. + (Applicative m, AllFields r c) + => Proxy c + -> (forall x. c x => f x -> g x -> m (h x)) + -> Record f r -> Record g r -> m (Record h r) +czipWithM p f r r' = + sequenceA $ map (fn_2 . f') (reifyAllFields p) `ap` r `ap` r' + where + f' :: Dict c x -> f x -> g x -> (m :.: h) x + f' Dict fx gx = Comp $ f fx gx + +czipWith :: + AllFields r c + => Proxy c + -> (forall x. c x => f x -> g x -> h x) + -> Record f r -> Record g r -> Record h r +czipWith p f a b = unI $ czipWithM p (\x y -> I (f x y)) a b + +{------------------------------------------------------------------------------- + Support for @typelet@ +-------------------------------------------------------------------------------} + +-- | Introduce type variable for a row +letRecordT :: forall r f. + (forall r'. Let r' r => Proxy r' -> Record f r) + -> Record f r +letRecordT f = letT' (Proxy @r) f + +-- | Insert field into a record and introduce type variable for the result +letInsertAs :: forall r r' f n a. + Proxy r -- ^ Type of the record we are constructing + -> Field n -- ^ New field to be inserted + -> f a -- ^ Value of the new field + -> Record f r' -- ^ Record constructed so far + -> (forall r''. Let r'' (n := a : r') => Record f r'' -> Record f r) + -- ^ Assign type variable to new partial record, and continue + -> Record f r +letInsertAs _ n x r = letAs' (insert n x r) + + diff --git a/src/Data/Record/Anon/Internal/Core/Canonical.hs b/src/Data/Record/Anon/Internal/Core/Canonical.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Core/Canonical.hs @@ -0,0 +1,227 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE RoleAnnotations #-} + +-- | Canonical gecord (i.e., no diff) +-- +-- Intended for qualified import. +-- +-- > import Data.Record.Anonymous.Internal.Canonical (Canonical) +-- > import qualified Data.Record.Anonymous.Internal.Canonical as Canon +module Data.Record.Anon.Internal.Core.Canonical ( + Canonical(..) + -- * Indexed access + , getAtIndex + , setAtIndex + -- * Conversion + , toList + , fromList + , toVector + , fromVector + -- * Basic API + , insert + , lens + -- * Simple (non-constrained) combinators + , map + , mapM + , zipWith + , zipWithM + , collapse + , sequenceA + , ap + -- * Debugging support +#if DEBUG + , toString +#endif + ) where + +import Prelude hiding (map, mapM, zip, zipWith, sequenceA, pure) + +import Data.Coerce (coerce) +import Data.Kind +import Data.SOP.BasicFunctors +import Data.SOP.Classes (type (-.->)(apFn)) +import GHC.Exts (Any) + +#if DEBUG +import Debug.RecoverRTTI (AnythingToString(..)) +#endif + +import qualified Data.Foldable as Foldable + +import Data.Record.Anon.Internal.Util.StrictArray (StrictArray) + +import qualified Data.Record.Anon.Internal.Util.StrictArray as Strict + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Canonical record representation +-- +-- Canonicity here refers to the fact that we have no @Diff@ to apply (see +-- "Data.Record.Anonymous.Internal.Diff"). In this case, the record is +-- represented as a strict vector in row order (@large-anon@ is strict by +-- default; lazy records can be achieved using boxing). This order is important: +-- it makes it possible to define functions such as @mapM@ (for which ordering +-- must be well-defined). +-- +-- Type level shadowing is reflected at the term level: if a record has +-- duplicate fields in its type, it will have multiple entries for that field +-- in the vector. +-- +-- TODO: Currently we have no way of recovering the value of shadowed fields, +-- adding an API for that is future work. The work by Daan Leijen on scoped +-- labels might offer some inspiration there. +-- +-- NOTE: When we cite the algorithmic complexity of operations on 'Canonical', +-- we assume that 'HashMap' inserts and lookups are @O(1)@, which they are in +-- practice (especially given the relatively small size of typical records), +-- even if theoretically they are @O(log n)@. See also the documentation of +-- "Data.HashMap.Strict". +newtype Canonical (f :: k -> Type) = Canonical (StrictArray (f Any)) + deriving newtype (Semigroup, Monoid) + +type role Canonical representational + +deriving instance Show a => Show (Canonical (K a)) + +{------------------------------------------------------------------------------- + Indexed access +-------------------------------------------------------------------------------} + +-- | Get field at the specified index +-- +-- @O(1)@. +getAtIndex :: Canonical f -> Int -> f Any +getAtIndex (Canonical c) ix = c Strict.! ix + +-- | Set fields at the specified indices +-- +-- @O(n)@ in the size of the record (independent of the number of field updates) +-- @O(1)@ if the list of updates is empty. +setAtIndex :: [(Int, f Any)] -> Canonical f -> Canonical f +setAtIndex [] c = c +setAtIndex fs (Canonical v) = Canonical (v Strict.// fs) + +{------------------------------------------------------------------------------- + Conversion +-------------------------------------------------------------------------------} + +-- | To strict vector +toVector :: Canonical f -> StrictArray (f Any) +toVector (Canonical v) = v + +-- | From strict vector +fromVector :: StrictArray (f Any) -> Canonical f +fromVector = Canonical + +-- | All fields in row order +-- +-- @O(n)@ +toList :: Canonical f -> [f Any] +toList = Foldable.toList . toVector + +-- | From list of fields in row order +-- +-- @O(n)@. +fromList :: [f Any] -> Canonical f +fromList = fromVector . Strict.fromList + +{------------------------------------------------------------------------------- + Basic API +-------------------------------------------------------------------------------} + +-- | Insert fields into the record +-- +-- It is the responsibility of the caller to make sure that the linear +-- concatenation of the new fields to the existing record matches the row order +-- of the new record. +-- +-- @O(n)@ in the number of inserts and the size of the record. +-- @O(1)@ if the list of inserts is empty. +insert :: forall f. [f Any] -> Canonical f -> Canonical f +insert [] = id +insert new = prepend + where + prepend :: Canonical f -> Canonical f + prepend (Canonical v) = Canonical (Strict.fromList new <> v) + +-- | Project out some fields in the selected order +-- +-- It is the responsibility of the caller that the list of indices is in row +-- order of the new record. +-- +-- @O(n)@ (in both directions) +lens :: StrictArray Int -> Canonical f -> (Canonical f, Canonical f -> Canonical f) +lens is (Canonical v) = ( + Canonical $ + Strict.backpermute v is + , \(Canonical v') -> Canonical $ + Strict.update v (Strict.zipWith (,) is v') + ) + +{------------------------------------------------------------------------------- + Simple (non-constrained) combinators +-------------------------------------------------------------------------------} + +map :: (forall x. f x -> g x) -> Canonical f -> Canonical g +map f (Canonical v) = Canonical $ fmap f v + +mapM :: + Applicative m + => (forall x. f x -> m (g x)) + -> Canonical f -> m (Canonical g) +mapM f (Canonical v) = Canonical <$> Strict.mapM f v + +-- | Zip two records +-- +-- Precondition: the two records must have the same shape. +zipWith :: + (forall x. f x -> g x -> h x) + -> Canonical f -> Canonical g -> Canonical h +zipWith f (Canonical v) (Canonical v') = Canonical $ Strict.zipWith f v v' + +-- | Applicative zip of two records +-- +-- Precondition: the two records must have the same shape. +zipWithM :: + Applicative m + => (forall x. f x -> g x -> m (h x)) + -> Canonical f -> Canonical g -> m (Canonical h) +zipWithM f (Canonical v) (Canonical v') = Canonical <$> Strict.zipWithM f v v' + +collapse :: Canonical (K a) -> [a] +collapse (Canonical v) = co $ Foldable.toList v + where + co :: [K a Any] -> [a] + co = coerce + +sequenceA :: Applicative m => Canonical (m :.: f) -> m (Canonical f) +sequenceA (Canonical v) = Canonical <$> Strict.mapM unComp v + +ap :: Canonical (f -.-> g) -> Canonical f -> Canonical g +ap = zipWith apFn + +{------------------------------------------------------------------------------- + Debugging support +-------------------------------------------------------------------------------} + +#if DEBUG +toString :: forall k (f :: k -> Type). Canonical f -> String +toString = show . aux + where + aux :: Canonical f -> Canonical (K (AnythingToString (f Any))) + aux = coerce +#endif diff --git a/src/Data/Record/Anon/Internal/Core/Diff.hs b/src/Data/Record/Anon/Internal/Core/Diff.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Core/Diff.hs @@ -0,0 +1,222 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} + +-- | Record diff +-- +-- Intended for qualified import. +-- +-- > import Data.Record.Anonymous.Internal.Diff (Diff) +-- > import qualified Data.Record.Anonymous.Internal.Diff as Diff +module Data.Record.Anon.Internal.Core.Diff ( + Diff(..) + -- * Incremental construction + , empty + , get + , set + , insert + -- * Batch operations + , apply + -- * Debugging support +#if DEBUG + , toString +#endif + ) where + +import Data.IntMap (IntMap) +import Data.Kind +import Data.List.NonEmpty (NonEmpty(..), (<|)) +import Data.SOP.BasicFunctors +import GHC.Exts (Any) +import qualified Data.IntMap.Strict as IntMap + +#if DEBUG +import Debug.RecoverRTTI (AnythingToString(..)) +import Data.Record.Generic.Rep.Internal (noInlineUnsafeCo) +#endif + +import qualified Data.List.NonEmpty as NE + +import Data.Record.Anon.Internal.Core.Canonical (Canonical(..)) +import Data.Record.Anon.Internal.Core.FieldName (FieldName) +import Data.Record.Anon.Internal.Util.SmallHashMap (SmallHashMap) + +import qualified Data.Record.Anon.Internal.Core.Canonical as Canon +import qualified Data.Record.Anon.Internal.Util.SmallHashMap as HashMap + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Record changes to a ('Canonical') record. +-- +-- Unlike 'Canon.set' and 'Canon.insert', 'Diff.set' and 'Diff.insert' deal with +-- a single field at a time, at @O(1)@ cost. This is the raison d'ĂȘtre of +-- 'Diff': amortize the cost of repeated updates/inserts. Specifically, a series +-- of inserts or updates will build a 'Diff' which will take @O(n)@ to apply, +-- but that 'apply' should be /executed/ only when we do an operation which is +-- @O(n)@ anyway, thereby absorbing the cost. +-- +-- This is also the reason that 'Diff' is name based, not index based: inserting +-- a new field would increase all indices of existing fields by 1, an inherently +-- @O(n)@ operation. +-- +-- NOTE: As for 'Canonical', when citing algorithmic complexity of operations on +-- 'Diff', we assume that 'HashMap' inserts and lookups are @O(1)@. See +-- 'Canonical' for more detailed justification. +-- +-- NOTE: Since @large-anon@ currently only supports records with strict fields, +-- we use strict 'HashMap' here. +data Diff (f :: k -> Type) = Diff { + -- | New values of existing fields + -- + -- Indices refer to the original record. + diffUpd :: !(IntMap (f Any)) + + -- | List of new fields, most recently inserted first + -- + -- May contain duplicates: fields inserted later shadow earlier fields. + , diffIns :: [FieldName] + + -- | Values for the newly inserted fields + -- + -- If the field is shadowed, the list will have multiple entries. Entries + -- in the lists are from new to old, so the head of the list is the + -- "currently visible" entry. + , diffNew :: !(SmallHashMap FieldName (NonEmpty (f Any))) + } + +type role Diff representational + +deriving instance Show a => Show (Diff (K a)) + +{------------------------------------------------------------------------------- + Incremental construction + + TODO: We should property check these postconditions. +-------------------------------------------------------------------------------} + +-- | Empty difference +-- +-- Postcondition: +-- +-- > apply empty c == c +empty :: Diff f +empty = Diff { + diffUpd = IntMap.empty + , diffIns = [] + , diffNew = HashMap.empty + } + +-- | Get field +-- +-- Precondition: field must be present in the diff or in the record. +-- Postcondition: +-- +-- > Diff.get f d c == Canon.get f (Diff.apply d c) +-- +-- @O(1)@. +get :: (Int, FieldName) -> Diff f -> Canonical f -> f Any +get (i, f) Diff{..} c = + case HashMap.lookup f diffNew of + Just xs -> NE.head xs -- inserted in the diff + Nothing -> case IntMap.lookup i diffUpd of + Just x -> x -- updated in the diff + Nothing -> Canon.getAtIndex c i -- unchanged in the diff + +-- | Update existing field +-- +-- Precondition: field must be present in the diff or in the record. +-- Postcondition: +-- +-- > Diff.apply (Diff.set f x c d) c == Canon.set [(f, x)] (apply d c) +-- +-- It is useful to spell out what happens when inserts and updated are mixed: +-- +-- * When a field is inserted and then updated, we just update the corresponding +-- entry in 'diffNew'. +-- * When an /existing/ field is first updated and then a new field with the +-- same name is added, an entry is added to 'diffNew' but 'diffUpd' will also +-- contain an entry for this field. This doesn't matter: when the diff is +-- applied, the new field will shadow the old, and when we 'get' the value +-- of a field, we similarly /first/ check 'diffNew'. +-- * When the /same/ field is inserted more than once, updates to that field +-- will effectively affect all of them (since we store only a single value), +-- but only the first value will matter as it will shadow all the others. +-- +-- @O(1)@. +set :: forall f. (Int, FieldName) -> f Any -> Diff f -> Diff f +set (i, f) x d@Diff{..} = + case HashMap.alterExisting f updateInserted diffNew of + Just ((), diffNew') -> d { diffNew = diffNew' } + Nothing -> d { diffUpd = IntMap.insert i x diffUpd } + where + updateInserted :: NonEmpty (f Any) -> ((), Maybe (NonEmpty (f Any))) + updateInserted (_ :| prev) = ((), Just (x :| prev)) + +-- | Insert new field +-- +-- Precondition: none (if the field already exists, it will be shadowed). +-- Postcondition: +-- +-- > Diff.apply (Diff.insert f x d) c = Canon.insert [(f, x)] (apply d c) +-- +-- @(1)@. +insert :: forall f. FieldName -> f Any -> Diff f -> Diff f +insert f x d@Diff{..} = d { + diffIns = f : diffIns + , diffNew = HashMap.alter (Just . insertField) f diffNew + } + where + insertField :: Maybe (NonEmpty (f Any)) -> NonEmpty (f Any) + insertField Nothing = x :| [] + insertField (Just prev) = x <| prev + +{------------------------------------------------------------------------------- + Batch operations +-------------------------------------------------------------------------------} + +-- | All new fields (including shadowed fields), from new to old +-- +-- @O(n)@. +allNewFields :: Diff f -> [f Any] +allNewFields = \Diff{..} -> go diffNew diffIns + where + go :: SmallHashMap FieldName (NonEmpty (f Any)) -> [FieldName] -> [f Any] + go _ [] = [] + go vs (x:xs) = case HashMap.alterExisting x NE.uncons vs of + Nothing -> error "allNewFields: invariant violation" + Just (v, vs') -> v : go vs' xs + +-- | Apply diff +-- +-- @O(n)@ in the size of the 'Canonical' and the 'Diff' in general. +-- @O(1)@ if the `Diff` is empty. +apply :: forall f. Diff f -> Canonical f -> Canonical f +apply d = + Canon.insert (allNewFields d) + . Canon.setAtIndex (IntMap.toList (diffUpd d)) + +{------------------------------------------------------------------------------- + Debugging support +-------------------------------------------------------------------------------} + +#if DEBUG +toString :: forall k (f :: k -> Type). Diff f -> String +toString = show . mapDiff (K . AnythingToString . co) + where + mapDiff :: (forall x. f x -> g x) -> Diff f -> Diff g + mapDiff f Diff{..} = Diff{ + diffUpd = fmap f diffUpd + , diffIns = diffIns + , diffNew = fmap (fmap f) diffNew + } + + co :: f x -> f Any + co = noInlineUnsafeCo +#endif diff --git a/src/Data/Record/Anon/Internal/Core/FieldName.hs b/src/Data/Record/Anon/Internal/Core/FieldName.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Core/FieldName.hs @@ -0,0 +1,68 @@ +-- | Field name +-- +-- Intended for qualified import. +-- +-- > import Data.Record.Anon.Internal.Core.FieldName (FieldName(..)) +-- > import qualified Data.Record.Anon.Internal.Core.FieldName as FieldName +module Data.Record.Anon.Internal.Core.FieldName ( + -- * Definition + FieldName(..) + -- * Conversion + , fromString + , fromFastString + ) where + +import Data.Hashable +import Data.String + +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Record field name +-- +-- A fieldname carries its own hash, which is computed by the plugin at +-- compile time. +data FieldName = FieldName { + fieldNameHash :: Int + , fieldNameLabel :: String + } + -- For the 'Eq' and 'Ord' instances it's important the 'Int' comes first + deriving (Eq, Ord) + +{------------------------------------------------------------------------------- + Conversion +-------------------------------------------------------------------------------} + +-- | From 'FastString' +-- +-- This happens at compile time in the plugin. +fromFastString :: FastString -> FieldName +fromFastString = fromString . unpackFS + +{------------------------------------------------------------------------------- + Instances +-------------------------------------------------------------------------------} + +-- | Convenience constructor for 'FieldName' +-- +-- This function is primarily for use in the 'Show' instance and for debugging. +-- Other applications should use 'fieldNameVal' instead, so that the hash +-- is computed at compile time instead. +instance IsString FieldName where + fromString str = FieldName (hash str) str + +instance Hashable FieldName where + hash = fieldNameHash + hashWithSalt s = hashWithSalt s . fieldNameHash + +instance Show FieldName where + showsPrec p n = showParen (p >= 11) $ + showString "fromString " . showsPrec 11 (fieldNameLabel n) + +instance Outputable FieldName where + ppr = ppr . fieldNameLabel + + diff --git a/src/Data/Record/Anon/Internal/Plugin.hs b/src/Data/Record/Anon/Internal/Plugin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin.hs @@ -0,0 +1,36 @@ +module Data.Record.Anon.Internal.Plugin (plugin) where + +import GHC.TcPlugin.API + +import qualified GHC.Plugins + +import Data.Record.Anon.Internal.Plugin.TC.NameResolution +import Data.Record.Anon.Internal.Plugin.TC.Rewriter +import Data.Record.Anon.Internal.Plugin.TC.Solver +import Data.Record.Anon.Internal.Plugin.Source + +-- | The large-anon plugins +-- +-- This consists of two plugins: +-- +-- 1. The type checker plugin forms the heart of this package. It solves +-- the various constraints we have on rows, and computes type-level metadata. +-- 2. The source plugin offers syntactic sugar for record construction. +plugin :: GHC.Plugins.Plugin +plugin = GHC.Plugins.defaultPlugin { + GHC.Plugins.tcPlugin = \_args -> Just $ + mkTcPlugin tcPlugin + , GHC.Plugins.parsedResultAction = \args _modSummary -> + sourcePlugin args + , GHC.Plugins.pluginRecompile = + GHC.Plugins.purePlugin + } + +tcPlugin :: TcPlugin +tcPlugin = TcPlugin { + tcPluginInit = nameResolution + , tcPluginSolve = solve + , tcPluginRewrite = rewrite + , tcPluginStop = const $ return () + } + diff --git a/src/Data/Record/Anon/Internal/Plugin/Source.hs b/src/Data/Record/Anon/Internal/Plugin/Source.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/Source.hs @@ -0,0 +1,174 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TupleSections #-} + +module Data.Record.Anon.Internal.Plugin.Source (sourcePlugin) where + +import Control.Monad +import Control.Monad.Trans +import Data.Generics (everywhereM, mkM) + +import Data.Record.Anon.Internal.Plugin.Source.GhcShim +import Data.Record.Anon.Internal.Plugin.Source.Names +import Data.Record.Anon.Internal.Plugin.Source.NamingT +import Data.Record.Anon.Internal.Plugin.Source.Options + +{------------------------------------------------------------------------------- + Top-level +-------------------------------------------------------------------------------} + +sourcePlugin :: [String] -> HsParsedModule -> Hsc HsParsedModule +sourcePlugin opts + parsed@HsParsedModule{ + hpm_module = L l modl@HsModule{ + hsmodDecls = decls + , hsmodImports = imports + } + } = do + (decls', modls) <- runNamingHsc $ + everywhereM + (mkM $ transformExpr $ parseOpts opts) + decls + return $ parsed { + hpm_module = L l $ modl { + hsmodDecls = decls' + , hsmodImports = imports ++ map (importDecl True) modls + } + } + +transformExpr :: Options -> LHsExpr GhcPs -> NamingT Hsc (LHsExpr GhcPs) +transformExpr options@Options{debug} e@(L l expr) + | RecordCon _ext (L _ nm) (HsRecFields flds dotdot) <- expr + , Unqual nm' <- nm + , Nothing <- dotdot + , Just mode <- parseMode (occNameString nm') + , Just flds' <- mapM getField flds + = do e' <- anonRec options mode l flds' + when debug $ lift $ issueWarning l (debugMsg e') + return e' + + | otherwise + = return e + where + getField :: + LHsRecField GhcPs (LHsExpr GhcPs) + -> Maybe (FastString, LHsExpr GhcPs) + getField (L _ (HsRecField (L _ fieldOcc) arg pun)) + | FieldOcc _ (L _ nm) <- fieldOcc + , Unqual nm' <- nm + , not pun + = Just (occNameFS nm', arg) + + | otherwise + = Nothing + +debugMsg :: LHsExpr GhcPs -> SDoc +debugMsg expr = pprSetDepth AllTheWay $ vcat [ + text "large-records: splicing in the following expression:" + , ppr expr + ] + +{------------------------------------------------------------------------------- + Main translation +-------------------------------------------------------------------------------} + +anonRec :: + Options + -> Mode + -> SrcSpan + -> [(FastString, LHsExpr GhcPs)] + -> NamingT Hsc (LHsExpr GhcPs) +anonRec Options{typelet, noapply} mode l = \fields -> + applyDiff =<< go fields + where + LargeAnonNames{..} = largeAnonNames mode + + go :: [(FastString, LHsExpr GhcPs)] -> NamingT Hsc (LHsExpr GhcPs) + go fields + | null fields = do + useName largeAnon_empty + return $ mkVar l largeAnon_empty + | not typelet = do + recordWithoutTypelet mode l fields + | otherwise = do + p <- freshVar l "p" + fields' <- mapM (\(n, e) -> (n,e,) <$> freshVar l "xs") fields + recordWithTypelet mode l p fields' + + applyDiff :: LHsExpr GhcPs -> NamingT Hsc (LHsExpr GhcPs) + applyDiff e + | noapply = return e + | otherwise = do + useName largeAnon_applyPending + return $ mkVar l largeAnon_applyPending `mkHsApp` e + +recordWithoutTypelet :: + Mode + -> SrcSpan + -> [(FastString, LHsExpr GhcPs)] + -> NamingT Hsc (LHsExpr GhcPs) +recordWithoutTypelet mode l = \fields -> do + useName largeAnon_empty + useName largeAnon_insert + return $ go fields + where + LargeAnonNames{..} = largeAnonNames mode + + go :: [(FastString, LHsExpr GhcPs)] -> LHsExpr GhcPs + go [] = mkVar l largeAnon_empty + go ((n,e):fs) = mkVar l largeAnon_insert `mkHsApps` [mkLabel l n, e, go fs] + +-- | Experimental support for typelet +-- +-- See documentation of 'letRecordT' and 'letInsertAs'. +recordWithTypelet :: + Mode + -> SrcSpan + -> RdrName -- ^ Fresh var for the proxy + -> [(FastString, LHsExpr GhcPs, RdrName)] -- ^ Fresh var for each insert + -> NamingT Hsc (LHsExpr GhcPs) +recordWithTypelet mode l p = \fields -> do + useName largeAnon_empty + useName largeAnon_insert + useName largeAnon_letRecordT + useName largeAnon_letInsertAs + useName typelet_castEqual + + return $ + mkHsApp (mkVar l largeAnon_letRecordT) $ + simpleLam p $ mkHsApp (mkVar l typelet_castEqual) $ + go (mkVar l largeAnon_empty) $ reverse fields + where + LargeAnonNames{..} = largeAnonNames mode + + go :: + LHsExpr GhcPs + -> [(FastString, LHsExpr GhcPs, RdrName)] + -> LHsExpr GhcPs + go prev [] = mkHsApp (mkVar l typelet_castEqual) prev + go prev ((n,e,x):fs) = mkHsApps (mkVar l largeAnon_letInsertAs) [ + mkVar l p + , mkLabel l n + , e + , prev + , simpleLam x $ go (mkVar l x) fs + ] + where + +{------------------------------------------------------------------------------- + Auxiliary +-------------------------------------------------------------------------------} + +mkVar :: SrcSpan -> RdrName -> LHsExpr GhcPs +mkVar l name = L l $ HsVar defExt (L l name) + +mkLabel :: SrcSpan -> FastString -> LHsExpr GhcPs +mkLabel l n = L l $ HsOverLabel defExt Nothing n + +-- | Construct simple lambda +-- +-- Constructs lambda of the form +-- +-- > \x -> e +simpleLam :: RdrName -> LHsExpr GhcPs -> LHsExpr GhcPs +simpleLam x body = mkHsLam [nlVarPat x] body diff --git a/src/Data/Record/Anon/Internal/Plugin/Source/GhcShim.hs b/src/Data/Record/Anon/Internal/Plugin/Source/GhcShim.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/Source/GhcShim.hs @@ -0,0 +1,145 @@ +{-# LANGUAGE CPP #-} + +-- | Thin shim around the GHC API +-- +-- For the typechecker part we have the excellent @ghc-tcplugin-api@ library; +-- unfortunately, we have no such library for source plugins. We could reuse a +-- small part of @ghc-tcplugin-api@ here, but there isn't too much point: source +-- plugins need quite a different subset of the GHC API than typechecker plugins +-- do. +module Data.Record.Anon.Internal.Plugin.Source.GhcShim ( + -- * Extensions + HasDefaultExt(..) + + -- * Miscellaneous + , importDecl + , issueWarning +#if __GLASGOW_HASKELL__ < 900 + , mkHsApps +#endif + + -- * Re-exports +#if __GLASGOW_HASKELL__ < 900 + , module BasicTypes + , module FastString + , module GHC + , module HscMain + , module HscTypes + , module Name + , module NameCache + , module OccName + , module Outputable + , module RdrName + , module UniqSupply +#else + , module GHC + , module GHC.Data.FastString + , module GHC.Driver.Main + , module GHC.Driver.Types + , module GHC.Types.Name + , module GHC.Types.Name.Cache + , module GHC.Types.Name.Occurrence + , module GHC.Types.Name.Reader + , module GHC.Types.Unique.Supply + , module GHC.Utils.Outputable +#endif + ) where + +#if __GLASGOW_HASKELL__ < 900 + +import Data.List (foldl') + +import Bag (listToBag) +import BasicTypes (Origin(Generated), PromotionFlag(NotPromoted)) +import ErrUtils (mkWarnMsg) +import FastString (FastString) +import GHC +import GhcPlugins +import HscMain (getHscEnv) +import HscTypes +import Name (mkInternalName) +import NameCache (NameCache(nsUniqs)) +import OccName +import Outputable +import RdrName (RdrName(Exact), rdrNameOcc, mkRdrQual, mkRdrUnqual) +import UniqSupply (takeUniqFromSupply) + +#else + +import GHC +import GHC.Data.Bag (listToBag) +import GHC.Data.FastString (FastString) +import GHC.Driver.Main (getHscEnv) +import GHC.Driver.Types +import GHC.Plugins +import GHC.Types.Name (mkInternalName) +import GHC.Types.Name.Cache (NameCache(nsUniqs)) +import GHC.Types.Name.Occurrence +import GHC.Types.Name.Reader (RdrName(Exact), rdrNameOcc, mkRdrQual, mkRdrUnqual) +import GHC.Types.Unique.Supply (takeUniqFromSupply) +import GHC.Utils.Error (mkWarnMsg) +import GHC.Utils.Outputable + +#endif + +{------------------------------------------------------------------------------- + Miscellaneous +-------------------------------------------------------------------------------} + +-- | Optionally @qualified@ import declaration +importDecl :: Bool -> ModuleName -> LImportDecl GhcPs +importDecl qualified name = noLoc $ ImportDecl { + ideclExt = defExt + , ideclSourceSrc = NoSourceText + , ideclName = noLoc name + , ideclPkgQual = Nothing + , ideclSafe = False + , ideclImplicit = False + , ideclAs = Nothing + , ideclHiding = Nothing +#if __GLASGOW_HASKELL__ < 810 + , ideclQualified = qualified +#else + , ideclQualified = if qualified then QualifiedPre else NotQualified +#endif +#if __GLASGOW_HASKELL__ < 900 + , ideclSource = False +#else + , ideclSource = NotBoot +#endif + } + +issueWarning :: SrcSpan -> SDoc -> Hsc () +issueWarning l errMsg = do + dynFlags <- getDynFlags + liftIO $ printOrThrowWarnings dynFlags . listToBag . (:[]) $ + mkWarnMsg dynFlags l neverQualify errMsg + +#if __GLASGOW_HASKELL__ < 900 +mkHsApps :: + LHsExpr (GhcPass id) + -> [LHsExpr (GhcPass id)] + -> LHsExpr (GhcPass id) +mkHsApps = foldl' mkHsApp +#endif + +{------------------------------------------------------------------------------- + Extensions +-------------------------------------------------------------------------------} + +class HasDefaultExt a where + defExt :: a + +#if __GLASGOW_HASKELL__ < 810 +instance HasDefaultExt NoExt where + defExt = noExt +#else +instance HasDefaultExt NoExtField where + defExt = noExtField +#endif + +#if __GLASGOW_HASKELL__ >= 900 +instance HasDefaultExt LayoutInfo where + defExt = NoLayoutInfo +#endif + diff --git a/src/Data/Record/Anon/Internal/Plugin/Source/Names.hs b/src/Data/Record/Anon/Internal/Plugin/Source/Names.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/Source/Names.hs @@ -0,0 +1,52 @@ +-- | Names used in code generation +-- +-- Intended for unqualified. +module Data.Record.Anon.Internal.Plugin.Source.Names ( + -- * large-anon + LargeAnonNames(..) + , largeAnonNames + -- * typelet + , typelet_castEqual + ) where + +import Data.Record.Anon.Internal.Plugin.Source.GhcShim +import Data.Record.Anon.Internal.Plugin.Source.Options (Mode(..)) + +{------------------------------------------------------------------------------- + large-anon +-------------------------------------------------------------------------------} + +-- | Named required for code generation +-- +-- All names are expected to be qualified with the full module name +data LargeAnonNames = LargeAnonNames { + largeAnon_empty :: RdrName + , largeAnon_insert :: RdrName + , largeAnon_applyPending :: RdrName + , largeAnon_letRecordT :: RdrName + , largeAnon_letInsertAs :: RdrName + } + +largeAnonNames :: Mode -> LargeAnonNames +largeAnonNames mode = LargeAnonNames { + largeAnon_empty = mkRdrQual modl $ mkVarOcc "empty" + , largeAnon_insert = mkRdrQual modl $ mkVarOcc "insert" + , largeAnon_applyPending = mkRdrQual modl $ mkVarOcc "applyPending" + , largeAnon_letRecordT = mkRdrQual modl $ mkVarOcc "letRecordT" + , largeAnon_letInsertAs = mkRdrQual modl $ mkVarOcc "letInsertAs" + } + where + modl :: ModuleName + modl = case mode of + Simple -> mkModuleName "Data.Record.Anon.Simple" + Advanced -> mkModuleName "Data.Record.Anon.Advanced" + +{------------------------------------------------------------------------------- + Typelet +-------------------------------------------------------------------------------} + +typelet :: ModuleName +typelet = mkModuleName "TypeLet" + +typelet_castEqual :: RdrName +typelet_castEqual = mkRdrQual typelet $ mkVarOcc "castEqual" diff --git a/src/Data/Record/Anon/Internal/Plugin/Source/NamingT.hs b/src/Data/Record/Anon/Internal/Plugin/Source/NamingT.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/Source/NamingT.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +-- | Naming things is hard +module Data.Record.Anon.Internal.Plugin.Source.NamingT ( + -- * Monad definition + NamingT -- opaque + , runNamingT + , runNamingHsc + -- * Key features of NamingT + , useName + , fresh + -- * Convenience derived features + , freshVar + ) where + +import Control.Monad.Reader +import Control.Monad.State +import Data.Bifunctor +import Data.IORef +import Data.Set (Set) + +import qualified Data.Set as Set + +import Data.Record.Anon.Internal.Plugin.Source.GhcShim + +{------------------------------------------------------------------------------- + Monad definition +-------------------------------------------------------------------------------} + +data Env = Env { + envNameCache :: IORef NameCache + } + +-- | Naming things is hard +-- +-- The 'NamingT' monad transformer that provides two things: +-- +-- 1. Keep track of the imports we need for the names that we use. +-- 2. Generation of fresh names. +newtype NamingT m a = WrapNamingT { + unwrapNamingT :: StateT (Set ModuleName) (ReaderT Env m) a + } + deriving (Functor, Applicative, Monad) + +instance MonadTrans NamingT where + lift = WrapNamingT . lift . lift + +runNamingT :: Functor m => IORef NameCache -> NamingT m a -> m (a, [ModuleName]) +runNamingT ncVar = + fmap (second Set.toList) + . flip runReaderT env + . flip runStateT Set.empty + . unwrapNamingT + where + env :: Env + env = Env { envNameCache = ncVar } + +runNamingHsc :: NamingT Hsc a -> Hsc (a, [ModuleName]) +runNamingHsc ma = do + env <- getHscEnv + runNamingT (hsc_NC env) ma + +{------------------------------------------------------------------------------- + Key features of NamingT +-------------------------------------------------------------------------------} + +useName :: Monad m => RdrName -> NamingT m () +useName (Qual modl _) = WrapNamingT $ modify (Set.insert modl) +useName _otherwise = error "useName: expected qualified name" + +fresh :: MonadIO m => SrcSpan -> RdrName -> NamingT m RdrName +fresh l name = WrapNamingT $ do + ncVar <- asks envNameCache + liftIO $ atomicModifyIORef ncVar aux + where + aux :: NameCache -> (NameCache, RdrName) + aux nc = ( + nc { nsUniqs = us } + , Exact $ mkInternalName newUniq (newOccName (rdrNameOcc name)) l + ) + where + (newUniq, us) = takeUniqFromSupply (nsUniqs nc) + + -- Even when we generate fresh names, ghc can still complain about name + -- shadowing, because this check only considers the 'OccName', not the + -- unique. We therefore prefix the name with an underscore to avoid the + -- warning. + newOccName :: OccName -> OccName + newOccName n = mkOccName (occNameSpace n) . ("_" ++) $ occNameString n + +{------------------------------------------------------------------------------- + Derived convenience functions +-------------------------------------------------------------------------------} + +freshVar :: MonadIO m => SrcSpan -> String -> NamingT m RdrName +freshVar l = fresh l . mkRdrUnqual . mkVarOcc diff --git a/src/Data/Record/Anon/Internal/Plugin/Source/Options.hs b/src/Data/Record/Anon/Internal/Plugin/Source/Options.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/Source/Options.hs @@ -0,0 +1,45 @@ +module Data.Record.Anon.Internal.Plugin.Source.Options ( + -- * Options + Options(..) + , parseOpts + -- * Mode + , Mode(..) + , parseMode + ) where + +{------------------------------------------------------------------------------- + Options +-------------------------------------------------------------------------------} + +data Options = Options { + debug :: Bool -- ^ Dump generated code + , typelet :: Bool -- ^ Integrate with @typelet@ for truly O(1) coresize + , noapply :: Bool -- ^ Omit the call to 'applyDiff' + } + +defaultOptions :: Options +defaultOptions = Options { + debug = False + , typelet = False + , noapply = False + } + +parseOpts :: [String] -> Options +parseOpts = ($ defaultOptions) . foldr (.) id . map aux + where + aux :: String -> Options -> Options + aux "debug" opts = opts { debug = True } + aux "typelet" opts = opts { typelet = True } + aux "noapply" opts = opts { noapply = True } + aux opt _ = error $ "invalid option: " ++ show opt + +{------------------------------------------------------------------------------- + Mode +-------------------------------------------------------------------------------} + +data Mode = Simple | Advanced + +parseMode :: String -> Maybe Mode +parseMode "ANON" = Just Simple +parseMode "ANON_F" = Just Advanced +parseMode _ = Nothing diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/AllFields.hs b/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/AllFields.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/AllFields.hs @@ -0,0 +1,166 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} + +module Data.Record.Anon.Internal.Plugin.TC.Constraints.AllFields ( + CAllFields(..) + , parseAllFields + , solveAllFields + ) where + +import Data.Bifunctor +import Data.Foldable (toList) +import Data.Void + +import Data.Record.Anon.Internal.Plugin.TC.Row.KnownField (KnownField(..)) +import Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow (KnownRow) +import Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow (Fields) +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI +import Data.Record.Anon.Internal.Plugin.TC.NameResolution +import Data.Record.Anon.Internal.Plugin.TC.Parsing +import Data.Record.Anon.Internal.Plugin.TC.TyConSubst + +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow as KnownRow +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow as ParsedRow + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Parsed form of @AllFields c r@ +data CAllFields = CAllFields { + -- | Fields of the record (parsed form of @r@) + allFieldsParsedFields :: Fields + + -- | Type of the fields (@r@) + , allFieldsTypeFields :: Type + + -- | Constraint required for each field (@c@) + , allFieldsTypeConstraint :: Type + + -- | Constraint argument kind (the @k@ in @c :: k -> Constraint@) + , allFieldsTypeKind :: Type + } + +{------------------------------------------------------------------------------- + Outputable +-------------------------------------------------------------------------------} + +instance Outputable CAllFields where + ppr (CAllFields parsedFields typeConstraint typeKind typeFields) = parens $ + text "CAllFields" <+> braces (vcat [ + text "allFieldsParsedFields" <+> text "=" <+> ppr parsedFields + , text "allFieldsTypeFields " <+> text "=" <+> ppr typeFields + , text "allFieldsTypeConstraint" <+> text "=" <+> ppr typeConstraint + , text "allFieldsTypeKind" <+> text "=" <+> ppr typeKind + ]) + +{------------------------------------------------------------------------------- + Parser +-------------------------------------------------------------------------------} + +parseAllFields :: + TyConSubst + -> ResolvedNames + -> Ct + -> ParseResult Void (GenLocated CtLoc CAllFields) +parseAllFields tcs rn@ResolvedNames{..} = + parseConstraint' clsAllFields $ \case + [k, r, c] -> do + fields <- ParsedRow.parseFields tcs rn r + return CAllFields { + allFieldsParsedFields = fields + , allFieldsTypeFields = r + , allFieldsTypeConstraint = c + , allFieldsTypeKind = k + } + _invalidNumArgs -> + Nothing + +{------------------------------------------------------------------------------- + Evidence +-------------------------------------------------------------------------------} + +-- | Construct evidence +-- +-- For each field we need an evidence variable corresponding to the evidence +-- that that fields satisfies the constraint. +evidenceAllFields :: + ResolvedNames + -> CAllFields + -> KnownRow (Type, EvVar) + -> TcPluginM 'Solve EvTerm +evidenceAllFields ResolvedNames{..} CAllFields{..} fields = do + fields' <- mapM dictForField (KnownRow.toList fields) + return $ + evDataConApp + (classDataCon clsAllFields) + typeArgsEvidence + [ mkCoreApps (Var idEvidenceAllFields) $ concat [ + map Type typeArgsEvidence + , [mkListExpr (mkTyConApp tyConDictAny typeArgsDict) fields'] + ] + ] + where + -- Type arguments to @Dict@ and to @AllFields@ + typeArgsDict, typeArgsEvidence :: [Type] + typeArgsDict = [ + allFieldsTypeKind + , allFieldsTypeConstraint + ] + typeArgsEvidence = [ + allFieldsTypeKind + , allFieldsTypeFields + , allFieldsTypeConstraint + ] + + dictForField :: KnownField (Type, EvVar) -> TcPluginM 'Solve EvExpr + dictForField KnownField{ knownFieldInfo = (fieldType, dict) } = do + return $ mkCoreConApps dataConDictAny $ concat [ + map Type typeArgsDict + , [ -- We have a dictionary of type @c a@ from the evidence we get + -- from ghc; we cast it to @c Any@ to serve as arg to @DictAny@. + mkCoreApps (Var idUnsafeCoerce) [ + Type $ mkAppTy allFieldsTypeConstraint fieldType + , Type $ mkAppTy allFieldsTypeConstraint anyAtKind + , Var dict + ] + ] + ] + + -- Any at kind @k@ + anyAtKind :: Type + anyAtKind = mkTyConApp anyTyCon [allFieldsTypeKind] + +{------------------------------------------------------------------------------- + Solver +-------------------------------------------------------------------------------} + +solveAllFields :: + ResolvedNames + -> Ct + -> GenLocated CtLoc CAllFields + -> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct]) +solveAllFields rn orig (L loc cr@CAllFields{..}) = do + case ParsedRow.allKnown allFieldsParsedFields of + Nothing -> + return (Nothing, []) + Just fields -> do + fields' :: KnownRow (Type, CtEvidence) + <- KnownRow.traverse fields $ \_nm typ -> fmap (typ,) $ + newWanted loc $ + mkAppTy allFieldsTypeConstraint typ + ev <- evidenceAllFields rn cr $ second getEvVar <$> fields' + return ( + Just (ev, orig) + , map (mkNonCanonical . snd) (toList fields') + ) + where + getEvVar :: CtEvidence -> EvVar + getEvVar ct = case ctev_dest ct of + EvVarDest var -> var + HoleDest _ -> error "impossible (we don't ask for primitive equality)" + + diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/KnownFields.hs b/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/KnownFields.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/KnownFields.hs @@ -0,0 +1,121 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} + +module Data.Record.Anon.Internal.Plugin.TC.Constraints.KnownFields ( + CKnownFields(..) + , parseKnownFields + , solveKnownFields + ) where + +import Data.Void + +import Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow (KnownRow) +import Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow (Fields) +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI +import Data.Record.Anon.Internal.Plugin.TC.NameResolution +import Data.Record.Anon.Internal.Plugin.TC.Parsing +import Data.Record.Anon.Internal.Plugin.TC.TyConSubst + +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.KnownField as KnownField +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow as KnownRow +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow as ParsedRow + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Parsed form of a @KnownFields (r :: [(Symbol, Kind)]) @ constraint +data CKnownFields = CKnownFields { + -- | Fields of the record + knownFieldsParsedFields :: Fields + + -- | Type of the record fields (@r@) + , knownFieldsTypeRecord :: Type + + -- | Kind of the type information (@k@) + , knownFieldsTypeKind :: Type + } + +{------------------------------------------------------------------------------- + Outputable +-------------------------------------------------------------------------------} + +instance Outputable CKnownFields where + ppr (CKnownFields parsedFields typeRecord typeKind) = parens $ + text "CKnownFields" <+> braces (vcat [ + text "knownFieldsParsedFields" <+> text "=" <+> ppr parsedFields + , text "knownFieldsTypeRecord" <+> text "=" <+> ppr typeRecord + , text "knownFieldsTypeKind" <+> text "=" <+> ppr typeKind + ]) + +{------------------------------------------------------------------------------- + Parser +-------------------------------------------------------------------------------} + +parseKnownFields :: + TyConSubst + -> ResolvedNames + -> Ct + -> ParseResult Void (GenLocated CtLoc CKnownFields) +parseKnownFields tcs rn@ResolvedNames{..} = + parseConstraint' clsKnownFields $ \case + [k, r] -> do + fields <- ParsedRow.parseFields tcs rn r + return CKnownFields { + knownFieldsParsedFields = fields + , knownFieldsTypeRecord = r + , knownFieldsTypeKind = k + } + _invalidNumArgs -> + Nothing + +{------------------------------------------------------------------------------- + Evidence +-------------------------------------------------------------------------------} + +-- | Construct evidence +-- +-- For each field we need an evidence variable corresponding to the evidence +-- that that field name satisfies KnownSymbol. +evidenceKnownFields :: + ResolvedNames + -> CKnownFields + -> KnownRow a + -> TcPluginM 'Solve EvTerm +evidenceKnownFields ResolvedNames{..} CKnownFields{..} r = do + fields <- mapM KnownField.toExpr (KnownRow.toList r) + return $ + evDataConApp + (classDataCon clsKnownFields) + typeArgsEvidence + [ mkCoreApps (Var idEvidenceKnownFields) $ concat [ + map Type typeArgsEvidence + , [ mkListExpr stringTy fields ] + ] + ] + where + typeArgsEvidence :: [Type] + typeArgsEvidence = [ + knownFieldsTypeKind + , knownFieldsTypeRecord + ] + +{------------------------------------------------------------------------------- + Solver +-------------------------------------------------------------------------------} + +solveKnownFields :: + ResolvedNames + -> Ct + -> GenLocated CtLoc CKnownFields + -> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct]) +solveKnownFields rn orig (L _ cm@CKnownFields{..}) = do + -- See 'solveRecordConstraints' for a discussion of 'allFieldsKnown' + case ParsedRow.allKnown knownFieldsParsedFields of + Nothing -> + return (Nothing, []) + Just fields -> do + ev <- evidenceKnownFields rn cm fields + return (Just (ev, orig), []) diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/KnownHash.hs b/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/KnownHash.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/KnownHash.hs @@ -0,0 +1,101 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RecordWildCards #-} + +module Data.Record.Anon.Internal.Plugin.TC.Constraints.KnownHash ( + CKnownHash(..) + , parseKnownHash + , solveKnownHash + ) where + +import Data.Hashable (hash) +import Data.Void + +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI +import Data.Record.Anon.Internal.Plugin.TC.NameResolution +import Data.Record.Anon.Internal.Plugin.TC.Parsing +import Data.Record.Anon.Internal.Plugin.TC.TyConSubst + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Parsed form of an @KnownFieldLabel f@ constraint +data CKnownHash = CKnownHash { + -- | The underlying @FastString@ when the label is a literal. + knownHashLabel :: FastString + + -- | The raw type argument to the @KnownFieldLabel@ constraint. + , knownHashType :: Type + } + +{------------------------------------------------------------------------------- + Outputable +-------------------------------------------------------------------------------} + +instance Outputable CKnownHash where + ppr (CKnownHash hashLabel hashType) = parens $ + text "CKnownHash" <+> braces (vcat [ + text "knownHashLabel" <+> text "=" <+> ppr hashLabel + , text "knownHashType" <+> text "=" <+> ppr hashType + ]) + +{------------------------------------------------------------------------------- + Parser +-------------------------------------------------------------------------------} + +parseKnownHash :: + TyConSubst + -> ResolvedNames + -> Ct + -> ParseResult Void (GenLocated CtLoc CKnownHash) +parseKnownHash _ ResolvedNames{..} = + parseConstraint isRelevant $ \(ty, label) -> do + return $ CKnownHash { + knownHashLabel = label + , knownHashType = ty + } + where + isRelevant :: Class -> [Type] -> Maybe (Type, FastString) + isRelevant cls args + | [ty] <- args + , cls == clsKnownHash + , Just label <- isStrLitTy ty + = Just (ty, label) + + | otherwise + = Nothing + +evidenceKnownFieldLabel :: + ResolvedNames + -> CKnownHash + -> TcPluginM 'Solve EvTerm +evidenceKnownFieldLabel ResolvedNames{..} CKnownHash{..} = + return $ + evDataConApp + (classDataCon clsKnownHash) + typeArgsEvidence + [ mkCoreApps (Var idEvidenceKnownHash) $ concat [ + map Type typeArgsEvidence + , [ mkUncheckedIntExpr . fromIntegral $ + hash (unpackFS knownHashLabel) + ] + ] + ] + where + typeArgsEvidence :: [Type] + typeArgsEvidence = [ + knownHashType + ] + +{------------------------------------------------------------------------------- + Solver +-------------------------------------------------------------------------------} + +solveKnownHash :: + ResolvedNames + -> Ct + -> GenLocated CtLoc CKnownHash + -> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct]) +solveKnownHash rn orig (L _ lbl) = do + ev <- evidenceKnownFieldLabel rn lbl + return (Just (ev, orig), []) diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/RowHasField.hs b/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/RowHasField.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/RowHasField.hs @@ -0,0 +1,143 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} + +module Data.Record.Anon.Internal.Plugin.TC.Constraints.RowHasField ( + CRowHasField(..) + , parseRowHasField + , solveRowHasField + ) where + +import Data.Void +import GHC.Stack + +import Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow (Fields, FieldLabel(..)) +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI +import Data.Record.Anon.Internal.Plugin.TC.NameResolution +import Data.Record.Anon.Internal.Plugin.TC.Parsing +import Data.Record.Anon.Internal.Plugin.TC.TyConSubst + +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow as ParsedRow + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Parsed form of a @RowHasField n r@ with @r :: Row k@ constraint +data CRowHasField = CRowHasField { + -- | Label we're looking for (@n@) + hasFieldLabel :: FieldLabel + + -- | Fields of the record (parsed form of @r@) + -- + -- These may be fully or partially known, or completely unknown. + , hasFieldRecord :: Fields + + -- | Row kind (@k@) + , hasFieldTypeKind :: Type + + -- | Record field (@n@) + , hasFieldTypeLabel :: Type + + -- | Row (@r@) + , hasFieldTypeRow :: Type + + -- | Type of the record field we're looking for (@a@) + -- + -- Although @a@ will be of the form @f a'@ for some @a'@, we do not + -- enforce that here (but instead generate a new wanted equality + -- constraint to enforce this). + , hasFieldTypeField :: Type + } + +{------------------------------------------------------------------------------- + Outputable +-------------------------------------------------------------------------------} + +instance Outputable CRowHasField where + ppr (CRowHasField label record typeKind typeLabel typeRow typeField) = parens $ + text "CRowHasField" <+> braces (vcat [ + text "hasFieldLabel" <+> text "=" <+> ppr label + , text "hasFieldRecord" <+> text "=" <+> ppr record + , text "hasFieldTypeKind" <+> text "=" <+> ppr typeKind + , text "hasFieldTypeLabel" <+> text "=" <+> ppr typeLabel + , text "hasFieldTypeRow" <+> text "=" <+> ppr typeRow + , text "hasFieldTypeField" <+> text "=" <+> ppr typeField + ]) + +{------------------------------------------------------------------------------- + Parser +-------------------------------------------------------------------------------} + +parseRowHasField :: + HasCallStack + => TyConSubst + -> ResolvedNames + -> Ct + -> ParseResult Void (GenLocated CtLoc CRowHasField) +parseRowHasField tcs rn@ResolvedNames{..} = + parseConstraint' clsRowHasField $ \[k, n, r, a] -> do + label <- ParsedRow.parseFieldLabel n + fields <- ParsedRow.parseFields tcs rn r + + return $ CRowHasField { + hasFieldLabel = label + , hasFieldRecord = fields + , hasFieldTypeKind = k + , hasFieldTypeLabel = n + , hasFieldTypeRow = r + , hasFieldTypeField = a + } + +{------------------------------------------------------------------------------- + Evidence +-------------------------------------------------------------------------------} + +evidenceHasField :: + ResolvedNames + -> CRowHasField + -> Int -- ^ Field index + -> TcPluginM 'Solve EvTerm +evidenceHasField ResolvedNames{..} CRowHasField{..} i = do + return $ + evDataConApp + (classDataCon clsRowHasField) + typeArgsEvidence + [ mkCoreApps (Var idEvidenceRowHasField) $ concat [ + map Type typeArgsEvidence + , [mkUncheckedIntExpr $ fromIntegral i] + ] + ] + where + typeArgsEvidence :: [Type] + typeArgsEvidence = [ + hasFieldTypeKind + , hasFieldTypeLabel + , hasFieldTypeRow + , hasFieldTypeField + ] + +{------------------------------------------------------------------------------- + Solver +-------------------------------------------------------------------------------} + +solveRowHasField :: + ResolvedNames + -> Ct + -> GenLocated CtLoc CRowHasField + -> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct]) +solveRowHasField _ _ (L _ CRowHasField{hasFieldLabel = FieldVar _}) = + return (Nothing, []) +solveRowHasField rn orig (L loc hf@CRowHasField{hasFieldLabel = FieldKnown name, ..}) = + case ParsedRow.lookup name hasFieldRecord of + Nothing -> + -- TODO: If the record is fully known, we should issue a custom type + -- error here rather than leaving the constraint unsolved + return (Nothing, []) + Just (i, typ) -> do + eq <- newWanted loc $ + mkPrimEqPredRole Nominal + hasFieldTypeField + typ + ev <- evidenceHasField rn hf i + return (Just (ev, orig), [mkNonCanonical eq]) diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/SubRow.hs b/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/SubRow.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/Constraints/SubRow.hs @@ -0,0 +1,133 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RecordWildCards #-} + +module Data.Record.Anon.Internal.Plugin.TC.Constraints.SubRow ( + CSubRow(..) + , parseSubRow + , solveSubRow + ) where + +import Control.Monad (forM) +import Data.Void + +import Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow (Fields) +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI +import Data.Record.Anon.Internal.Plugin.TC.NameResolution +import Data.Record.Anon.Internal.Plugin.TC.Parsing +import Data.Record.Anon.Internal.Plugin.TC.TyConSubst + +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow as KnownRow +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow as ParsedRow + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Parsed form of @SubRow@ +-- +-- > SubRow (r :: [(Symbol, k)]) (r' :: [(Symbol, k)]) +data CSubRow = CSubRow { + -- | Fields on the LHS + subrowParsedLHS :: Fields + + -- | Fields on the RHS + , subrowParsedRHS :: Fields + + -- | Left-hand side (@r@) + , subrowTypeLHS :: Type + + -- | Right-hand side (@r'@) + , subrowTypeRHS :: Type + + -- | Functor argument kind (@k@) + , subrowTypeKind :: Type + } + +{------------------------------------------------------------------------------- + Outputable +-------------------------------------------------------------------------------} + +instance Outputable CSubRow where + ppr (CSubRow parsedLHS parsedRHS typeLHS typeRHS typeKind) = parens $ + text "CSubRow" <+> braces (vcat [ + text "subrowParsedLHS" <+> text "=" <+> ppr parsedLHS + , text "subrowParsedRHS" <+> text "=" <+> ppr parsedRHS + , text "subrowTypeLHS" <+> text "=" <+> ppr typeLHS + , text "subrowTypeRHS" <+> text "=" <+> ppr typeRHS + , text "subrowTypeKind" <+> text "=" <+> ppr typeKind + ]) + +{------------------------------------------------------------------------------- + Parser +-------------------------------------------------------------------------------} + +parseSubRow :: + TyConSubst + -> ResolvedNames + -> Ct + -> ParseResult Void (GenLocated CtLoc CSubRow) +parseSubRow tcs rn@ResolvedNames{..} = + parseConstraint' clsSubRow $ \[typeKind, typeLHS, typeRHS] -> do + fieldsLHS <- ParsedRow.parseFields tcs rn typeLHS + fieldsRHS <- ParsedRow.parseFields tcs rn typeRHS + return $ CSubRow { + subrowParsedLHS = fieldsLHS + , subrowParsedRHS = fieldsRHS + , subrowTypeLHS = typeLHS + , subrowTypeRHS = typeRHS + , subrowTypeKind = typeKind + } + +{------------------------------------------------------------------------------- + Evidence +-------------------------------------------------------------------------------} + +evidenceSubRow :: + ResolvedNames + -> CSubRow + -> [Int] + -> TcPluginM 'Solve EvTerm +evidenceSubRow ResolvedNames{..} CSubRow{..} fields = do + return $ + evDataConApp + (classDataCon clsSubRow) + typeArgsEvidence + [ mkCoreApps (Var idEvidenceSubRow) $ concat [ + map Type typeArgsEvidence + , [ mkListExpr intTy $ + map (mkUncheckedIntExpr . fromIntegral) fields ] + ] + ] + where + typeArgsEvidence :: [Type] + typeArgsEvidence = [ + subrowTypeKind + , subrowTypeLHS + , subrowTypeRHS + ] + +{------------------------------------------------------------------------------- + Solver +-------------------------------------------------------------------------------} + +solveSubRow :: + ResolvedNames + -> Ct + -> GenLocated CtLoc CSubRow + -> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct]) +solveSubRow rn orig (L loc proj@CSubRow{..}) = + case ( ParsedRow.allKnown subrowParsedLHS + , ParsedRow.allKnown subrowParsedRHS + ) of + (Just lhs, Just rhs) -> + case KnownRow.isSubRow lhs rhs of + Right inBoth -> do + eqs <- forM inBoth $ \(_i, (l, r)) -> + newWanted loc $ mkPrimEqPredRole Nominal l r + ev <- evidenceSubRow rn proj (map fst inBoth) + return (Just (ev, orig), map mkNonCanonical eqs) + Left _err -> + -- TODO: Return a custom error message + return (Nothing, []) + _otherwise -> + return (Nothing, []) diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/EquivClasses.hs b/src/Data/Record/Anon/Internal/Plugin/TC/EquivClasses.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/EquivClasses.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +module Data.Record.Anon.Internal.Plugin.TC.EquivClasses ( + constructEquivClasses + , canonicalize + ) where + +import Data.Bifunctor +import Data.Foldable (toList) +import Data.Graph (Graph, Vertex) +import Data.Map (Map) +import Data.Set (Set) + +import qualified Data.Graph as Graph +import qualified Data.Map as Map +import qualified Data.Set as Set + +-- | Given a set of equivalent pairs, map every value to canonical value +-- +-- Example with two classes: +-- +-- >>> constructEquivClasses [(1, 2), (4, 5), (2, 3)] +-- fromList [(1,1),(2,1),(3,1),(4,4),(5,4)] +-- +-- Adding one element that connects both classes: +-- +-- >>> constructEquivClasses [(1, 2), (4, 5), (2, 3), (3, 4)] +-- fromList [(1,1),(2,1),(3,1),(4,1),(5,1)] +constructEquivClasses :: forall a. Ord a => [(a, a)] -> Map a a +constructEquivClasses equivs = + Map.unions $ map (pickCanonical . map fromVertex . toList) $ + Graph.components graph + where + allValues :: Set a + allValues = Set.fromList $ concatMap (\(x, y) -> [x, y]) equivs + + toVertex :: a -> Vertex + fromVertex :: Vertex -> a + + toVertex a = Map.findWithDefault (error "toVertex: impossible") a $ + Map.fromList $ zip (Set.toList allValues) [1..] + fromVertex v = Map.findWithDefault (error "fromVertex: impossible") v $ + Map.fromList $ zip [1..] (Set.toList allValues) + + graph :: Graph + graph = Graph.buildG (1, Set.size allValues) $ + map (bimap toVertex toVertex) equivs + + -- Given a previously established equivalence class, construct a mapping + -- that maps each value to an (arbitrary) canonical value. + pickCanonical :: [a] -> Map a a + pickCanonical cls = Map.fromList $ zip cls (repeat (minimum cls)) + +canonicalize :: Ord a => Map a a -> a -> a +canonicalize canon x = Map.findWithDefault x x canon diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/GhcTcPluginAPI.hs b/src/Data/Record/Anon/Internal/Plugin/TC/GhcTcPluginAPI.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/GhcTcPluginAPI.hs @@ -0,0 +1,95 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} + +{-# OPTIONS_GHC -Wno-orphans #-} + +-- | Thin layer around ghc-tcplugin-api +module Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI ( + -- * Standard exports + module GHC.TcPlugin.API + , module GHC.Builtin.Names + , module GHC.Builtin.Types + , module GHC.Builtin.Types.Prim + , module GHC.Core.Make + , module GHC.Utils.Outputable + + -- * Additional exports + , splitAppTys + , unpackFS + + -- * New functonality + , isCanonicalVarEq + ) where + +#if __GLASGOW_HASKELL__ < 900 +import Data.List.NonEmpty (NonEmpty, toList) +#endif + +import GHC.TcPlugin.API +import GHC.Builtin.Names +import GHC.Builtin.Types +import GHC.Builtin.Types.Prim +import GHC.Core.Make +import GHC.Utils.Outputable + +#if __GLASGOW_HASKELL__ >= 808 && __GLASGOW_HASKELL__ < 810 +import FastString (unpackFS) +import TcRnTypes (Ct(..)) +import Type (splitAppTys) +#endif + +#if __GLASGOW_HASKELL__ >= 810 && __GLASGOW_HASKELL__ < 900 +import Constraint (Ct(..)) +import FastString (unpackFS) +import Type (splitAppTys) +#endif + +#if __GLASGOW_HASKELL__ >= 900 && __GLASGOW_HASKELL__ < 902 +import GHC.Core.Type (splitAppTys) +import GHC.Data.FastString (unpackFS) +import GHC.Tc.Types.Constraint (Ct(..)) +#endif + +#if __GLASGOW_HASKELL__ >= 902 +import GHC.Core.Type (splitAppTys) +import GHC.Data.FastString (unpackFS) +import GHC.Tc.Types.Constraint (Ct(..), CanEqLHS(..)) +#endif + +isCanonicalVarEq :: Ct -> Maybe (TcTyVar, Type) +#if __GLASGOW_HASKELL__ >= 808 && __GLASGOW_HASKELL__ < 902 +isCanonicalVarEq = \case + CTyEqCan{..} -> Just (cc_tyvar, cc_rhs) + CFunEqCan{..} -> Just (cc_fsk, mkTyConApp cc_fun cc_tyargs) + _otherwise -> Nothing +#endif +#if __GLASGOW_HASKELL__ >= 902 +isCanonicalVarEq = \case + CEqCan{..} + | TyVarLHS var <- cc_lhs + -> Just (var, cc_rhs) + | TyFamLHS tyCon args <- cc_lhs + , Just var <- getTyVar_maybe cc_rhs + -> Just (var, mkTyConApp tyCon args) + _otherwise + -> Nothing +#endif + +-- TODO: Ideally we would actually show the location information obviously +instance Outputable CtLoc where + ppr _ = text "" + +#if __GLASGOW_HASKELL__ < 900 +instance Outputable a => Outputable (NonEmpty a) where + ppr = ppr . toList +#endif + +#if __GLASGOW_HASKELL__ >= 902 +instance (Outputable l, Outputable e) => Outputable (GenLocated l e) where + ppr (L l e) = parens $ text "L" <+> ppr l <+> ppr e +#endif diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/NameResolution.hs b/src/Data/Record/Anon/Internal/Plugin/TC/NameResolution.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/NameResolution.hs @@ -0,0 +1,82 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RecordWildCards #-} + +module Data.Record.Anon.Internal.Plugin.TC.NameResolution ( + ResolvedNames(..) + , nameResolution + ) where + +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI + +-- | Names we need to parse constraints or generate core +-- +-- Listed alphabetically. +data ResolvedNames = ResolvedNames { + clsAllFields :: Class + , clsKnownFields :: Class + , clsKnownHash :: Class + , clsRowHasField :: Class + , clsSubRow :: Class + , dataConDictAny :: DataCon + , idEvidenceAllFields :: Id + , idEvidenceKnownFields :: Id + , idEvidenceKnownHash :: Id + , idEvidenceRowHasField :: Id + , idEvidenceSubRow :: Id + , idUnsafeCoerce :: Id + , tyConDictAny :: TyCon + , tyConMerge :: TyCon + , tyConFieldTypes :: TyCon + , tyConPair :: TyCon + , tyConSimpleFieldTypes :: TyCon + } + +nameResolution :: TcPluginM 'Init ResolvedNames +nameResolution = do + modl <- getModule "large-anon" "Data.Record.Anon.Plugin.Internal.Runtime" + + let getClass :: MonadTcPlugin m => String -> m Class + getTyCon :: MonadTcPlugin m => String -> m TyCon + getDataCon :: MonadTcPlugin m => String -> m DataCon + getVar :: MonadTcPlugin m => String -> m Id + getPromDataCon :: MonadTcPlugin m => String -> m TyCon + + getClass cls = lookupOrig modl (mkTcOcc cls) >>= tcLookupClass + getTyCon con = lookupOrig modl (mkTcOcc con) >>= tcLookupTyCon + getDataCon con = lookupOrig modl (mkDataOcc con) >>= tcLookupDataCon + getVar var = lookupOrig modl (mkVarOcc var) >>= tcLookupId + getPromDataCon con = promoteDataCon <$> getDataCon con + + clsAllFields <- getClass "AllFields" + clsKnownFields <- getClass "KnownFields" + clsKnownHash <- getClass "KnownHash" + clsRowHasField <- getClass "RowHasField" + clsSubRow <- getClass "SubRow" + + dataConDictAny <- getDataCon "DictAny" + + idEvidenceAllFields <- getVar "evidenceAllFields" + idEvidenceKnownFields <- getVar "evidenceKnownFields" + idEvidenceKnownHash <- getVar "evidenceKnownHash" + idEvidenceRowHasField <- getVar "evidenceRowHasField" + idEvidenceSubRow <- getVar "evidenceSubRow" + idUnsafeCoerce <- getVar "noInlineUnsafeCo" + + tyConDictAny <- getTyCon "DictAny" + tyConFieldTypes <- getTyCon "FieldTypes" + tyConMerge <- getTyCon "Merge" + tyConPair <- getPromDataCon ":=" + tyConSimpleFieldTypes <- getTyCon "SimpleFieldTypes" + + return $ ResolvedNames {..} + +{------------------------------------------------------------------------------- + Auxiliary +-------------------------------------------------------------------------------} + +getModule :: MonadTcPlugin m => String -> String -> m Module +getModule pkg modl = do + r <- findImportedModule (mkModuleName modl) (Just (fsLit pkg)) + case r of + Found _ m -> return m + _otherwise -> panic $ "Could not find " ++ modl ++ " in package " ++ pkg diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/Parsing.hs b/src/Data/Record/Anon/Internal/Plugin/TC/Parsing.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/Parsing.hs @@ -0,0 +1,156 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} + +-- | Generic parsing infrastructure +-- +-- TODO: Perhaps we could move this (or some form of this) to ghc-tcplugin-api? +-- (The @typelet@ package could then use it, too.) +module Data.Record.Anon.Internal.Plugin.TC.Parsing ( + -- * Basic infrastructure + ParseResult(..) + , parseAll + , parseAll' + , withOrig + -- * Parsers for specific (but not @large-anon@ specific) constructs + , parseConstraint + , parseConstraint' + , parseCons + , parseNil + , parseInjTyConApp + ) where + +import Data.Bifunctor +import Data.Foldable (toList) +import Data.Void +import GHC.Stack + +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI +import Data.Record.Anon.Internal.Plugin.TC.TyConSubst + +{------------------------------------------------------------------------------- + Basic infrastructure +-------------------------------------------------------------------------------} + +data ParseResult e a = + -- | Parse successful + ParseOk a + + -- | Different constraint than we're looking for (does not imply an error) + | ParseNoMatch + + -- | Constraint of the shape we're looking for, but something is wrong + | ParseError e + deriving (Functor) + +instance Bifunctor ParseResult where + bimap _ g (ParseOk a) = ParseOk (g a) + bimap _ _ ParseNoMatch = ParseNoMatch + bimap f _ (ParseError e) = ParseError (f e) + +-- | Apply parser to each value in turn, bailing at the first error +parseAll :: forall e a b. (a -> ParseResult e b) -> [a] -> Either e [b] +parseAll f = go [] + where + go :: [b] -> [a] -> Either e [b] + go acc [] = Right (reverse acc) + go acc (a:as) = case f a of + ParseOk b -> go (b:acc) as + ParseNoMatch -> go acc as + ParseError e -> Left e + +-- | Variation on 'parseAll' which rules out the error case +parseAll' :: (a -> ParseResult Void b) -> [a] -> [b] +parseAll' f = aux . parseAll f + where + aux :: Either Void [b] -> [b] + aux (Left v) = absurd v + aux (Right bs) = bs + +-- | Bundle the parse result with the original value +withOrig :: (a -> ParseResult e b) -> (a -> ParseResult e (a, b)) +withOrig f x = fmap (x, ) $ f x + +{------------------------------------------------------------------------------- + Parsers for specific (but not @large-anon@ specific) constructs +-------------------------------------------------------------------------------} + +-- | Generic constraint parser +-- +-- TODO: If we add some parsing infra to ghc-tcplugin-api, maybe a (form of) +-- this function could live there too. +parseConstraint :: + HasCallStack + => (Class -> [Type] -> Maybe a) -- ^ Do we want to try and match against this? + -> (a -> Maybe b) -- ^ Parser for the class arguments + -> Ct -- ^ Constraint to parse + -> ParseResult e (GenLocated CtLoc b) +parseConstraint p f ct = fmap (L $ ctLoc ct) $ + -- TODO: classify up to equalities..? + case classifyPredType (ctPred ct) of + ClassPred cls args | Just a <- p cls args -> + case f a of + Just parsed -> + ParseOk parsed + Nothing -> + panic $ concat [ + "Unexpected " + , showSDocUnsafe (ppr cls) + , " constraint with arguments:\n" + , unlines (map (showSDocUnsafe . ppr) args) + , "\nat\n" + , prettyCallStack callStack + ] + _otherwise -> + ParseNoMatch + +-- | Specialization of 'parseConstraint', just checking the class name +parseConstraint' :: + HasCallStack + => Class -- ^ Predicate we want to match against + -> ([Type] -> Maybe a) -- ^ Parser for the class arguments + -> Ct -- ^ Constraint to parse + -> ParseResult e (GenLocated CtLoc a) +parseConstraint' cls = parseConstraint p + where + p :: Class -> [Type] -> Maybe [Type] + p cls' args = if cls == cls' then Just args else Nothing + +-- | Parse @x ': xs == (':) x xs == ((':) x) xs@ +parseCons :: TyConSubst -> Type -> Maybe (Type, Type) +parseCons tcs t = do + args <- parseInjTyConApp tcs promotedConsDataCon t + case args of + [_k, x, xs] -> Just (x, xs) + _otherwise -> Nothing + +-- | Parse @'[]@ +parseNil :: TyConSubst -> Type -> Maybe () +parseNil tcs t = do + args <- parseInjTyConApp tcs promotedNilDataCon t + case args of + [_k] -> Just () + _otherwise -> Nothing + +-- | Parse application of an injective type constructor +parseInjTyConApp :: TyConSubst -> TyCon -> Type -> Maybe [Type] +parseInjTyConApp tcs tyCon t = do + splits <- splitTyConApp_upTo tcs t + + -- At this point we might have multiple matches + -- + -- > t ~ TyCon1 args1 + -- > t ~ TyCon1 args1' + -- > t ~ TyCon2 args2 + -- > .. + -- + -- We are only interested in the equalities with @tyCon@ at the head, but + -- this may still leave us with multiple equalities + -- + -- > t ~ tyCon args1 + -- > t ~ tyCon args1' + -- + -- When this is the case, however, by injectivity of 'tyCon' we know that + -- @args1 ~ args1'@, so we can just return /any/ of the matches; we will + -- return the first. + lookup tyCon (toList splits) diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/Rewriter.hs b/src/Data/Record/Anon/Internal/Plugin/TC/Rewriter.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/Rewriter.hs @@ -0,0 +1,103 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE NamedFieldPuns #-} + +module Data.Record.Anon.Internal.Plugin.TC.Rewriter (rewrite) where + +import Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow (KnownRow) +import Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow (Fields) +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI +import Data.Record.Anon.Internal.Plugin.TC.NameResolution +import Data.Record.Anon.Internal.Plugin.TC.TyConSubst + +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.KnownField as KnownField +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow as KnownRow +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow as ParsedRow + +rewrite :: ResolvedNames -> UniqFM TyCon TcPluginRewriter +rewrite rn@ResolvedNames{..} = listToUFM [ + (tyConFieldTypes , rewriteRecordMetadataOf tyConFieldTypes rn) + , (tyConSimpleFieldTypes , rewriteRecordMetadataOf tyConSimpleFieldTypes rn) + ] + +data Args = Args { + -- | Functor argument, if any + argsFunctor :: Maybe Type + + -- | Parsed fields + , argsParsedFields :: Maybe Fields + + -- | Known record, if all fields are known + , argsParsedKnown :: Maybe (KnownRow Type) + } + +mkArgs :: TyConSubst -> ResolvedNames -> Maybe Type -> Type -> Args +mkArgs tcs rn argsFunctor r = Args{..} + where + argsParsedFields = ParsedRow.parseFields tcs rn r + argsParsedKnown = ParsedRow.allKnown =<< argsParsedFields + +parseArgs :: [Ct] -> ResolvedNames -> [Type] -> Args +parseArgs given rn = \case + [_k, f, r] -> mkArgs tcs rn (Just f) r + [ r] -> mkArgs tcs rn Nothing r + args -> panic $ concat [ + "Data.Record.Anon.Plugin.Rewriter.parseArgs: " + , "unexpected arguments: " + , showSDocUnsafe (ppr args) + ] + where + tcs :: TyConSubst + tcs = mkTyConSubst given + +rewriteRecordMetadataOf :: TyCon -> ResolvedNames -> TcPluginRewriter +rewriteRecordMetadataOf fun rn given args@(parseArgs given rn -> Args{..}) = +-- trace _debugInput $ +-- trace _debugParsed $ + case argsParsedKnown of + Nothing -> + return TcPluginNoRewrite + Just knownFields -> + return TcPluginRewriteTo { + tcRewriterWanteds = [] + , tcPluginReduction = + mkTyFamAppReduction + "large-anon" + Nominal + fun + args + (computeMetadataOf argsFunctor knownFields) + } + where + _debugInput :: String + _debugInput = unlines [ + "*** input" + , concat [ + "given:" + , showSDocUnsafe (ppr given) + ] + , concat [ + "args: " + , showSDocUnsafe (ppr args) + ] + ] + + _debugParsed :: String + _debugParsed = unlines [ + "*** parsed" + , concat [ + "parsedFields: " + , showSDocUnsafe (ppr argsParsedFields) + ] + , concat [ + "mKnownFields: " + , showSDocUnsafe (ppr argsParsedKnown) + ] + ] + +computeMetadataOf :: Maybe Type -> KnownRow Type -> TcType +computeMetadataOf mf r = + mkPromotedListTy + (mkTupleTy Boxed [mkTyConTy typeSymbolKindCon, liftedTypeKind]) + (map (KnownField.toType mf) $ KnownRow.toList r) diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/Row/KnownField.hs b/src/Data/Record/Anon/Internal/Plugin/TC/Row/KnownField.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/Row/KnownField.hs @@ -0,0 +1,88 @@ +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE DataKinds #-} + +-- | Information about a field in a record +-- +-- Intended for qualified import +-- +-- > import Data.Record.Anon.Internal.Plugin.TC.Row.KnownField (KnownField(..)) +-- > import qualified Data.Record.Anonymous.Row.Record.KnownField as KnownField +module Data.Record.Anon.Internal.Plugin.TC.Row.KnownField ( + -- * Definition + KnownField(..) + -- * Interop with @large-generics@ + , fromString + -- * Code generation + , toExpr + , toType + ) where + +import Data.Record.Anon.Internal.Core.FieldName (FieldName(..)) +import qualified Data.Record.Anon.Internal.Core.FieldName as FieldName + +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Context-free information about a field in a record +-- +-- In other words, we do /not/ know the /index/ of the field here, as that +-- depends the context (the particular record it is part of). +data KnownField a = KnownField { + knownFieldName :: FieldName + , knownFieldInfo :: a + } + deriving (Functor, Foldable) + +{------------------------------------------------------------------------------- + Interop with @large-generics@ +-------------------------------------------------------------------------------} + +-- | Construct 'KnownField' from just a string +-- +-- NOTE: This involves a hash computation. This is unavoidable as long as +-- @large-generics@ does not precompute those. +fromString :: String -> KnownField () +fromString name = KnownField { + knownFieldName = FieldName.fromString name + , knownFieldInfo = () + } + +{------------------------------------------------------------------------------- + Code generation +-------------------------------------------------------------------------------} + +-- | Name of the field as a term-level expression +toExpr :: KnownField a -> TcPluginM 'Solve CoreExpr +toExpr KnownField{knownFieldName = FieldName{..}} = + mkStringExpr fieldNameLabel + +-- | Type-level pair @'(n, a)@ or @'(n, f a)@ +toType :: Maybe Type -> KnownField Type -> Type +toType mf KnownField{knownFieldName = FieldName{..}, knownFieldInfo} = + -- mkPromotedPairTy is only introduced in ghc 9.2 + mkTyConApp + (promotedTupleDataCon Boxed 2) + [ mkTyConTy typeSymbolKindCon -- kind of first arg + , liftedTypeKind -- kind of second arg + , mkStrLitTy (fsLit fieldNameLabel) + , case mf of + Just f -> f `mkAppTy` knownFieldInfo + Nothing -> knownFieldInfo + ] + +{------------------------------------------------------------------------------- + Outputable +-------------------------------------------------------------------------------} + +instance Outputable a => Outputable (KnownField a) where + ppr (KnownField name info) = parens $ + text "KnownField" + <+> ppr name + <+> ppr info + diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/Row/KnownRow.hs b/src/Data/Record/Anon/Internal/Plugin/TC/Row/KnownRow.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/Row/KnownRow.hs @@ -0,0 +1,211 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | Information about a record +-- +-- Intended for qualified import. +-- +-- > import Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow (KnownRow(..)) +-- > import qualified Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow as KnownRow +module Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow ( + -- * Definition + KnownRow(..) + -- * Construction + , fromList + , toList + , visibleMap + -- * Combinators + , traverse + , indexed + -- * Check for subrows + , NotSubRow(..) + , isSubRow + ) where + +import Prelude hiding (traverse) +import qualified Prelude + +import Control.Monad.State (State, evalState, state) +import Data.Either (partitionEithers) + +import Data.Record.Anon.Internal.Core.FieldName (FieldName) +import Data.Record.Anon.Internal.Util.SmallHashMap (SmallHashMap) + +import Data.Record.Anon.Internal.Plugin.TC.Row.KnownField (KnownField(..)) +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI + +import qualified Data.Record.Anon.Internal.Util.SmallHashMap as HashMap + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Record with statically known shape +data KnownRow a = KnownRow { + -- | Information about each field in the record, in user-specified order. + -- + -- Order matters, because records with the same fields in a different + -- order are not considered equal by the library (merely isomorphic). + -- + -- May contain duplicates (if fields are shadowed). + knownRecordVector :: [KnownField a] + + -- | "Most recent" position of each field in the record + -- + -- Shadowed fields are not included in this map. + -- + -- Invariant: + -- + -- > HashMap.lookup n knownRecordNames == Just i + -- > ==> knownFieldName (knownRecordVector V.! i) == n + , knownRecordVisible :: SmallHashMap FieldName Int + + -- | Are all fields in this record visible? + -- + -- 'False' if some fields are shadowed. + , knownRecordAllVisible :: Bool + } + deriving (Functor, Foldable) + +{------------------------------------------------------------------------------- + Conversion +-------------------------------------------------------------------------------} + +toList :: KnownRow a -> [KnownField a] +toList = knownRecordVector + +visibleMap :: KnownRow a -> SmallHashMap FieldName (KnownField a) +visibleMap KnownRow{..} = (knownRecordVector !!) <$> knownRecordVisible + +{------------------------------------------------------------------------------- + Construction +-------------------------------------------------------------------------------} + +fromList :: forall a. + [KnownField a] + -- ^ Fields of the record in the order they appear in the row types + -- + -- In other words, fields earlier in the list shadow later fields. + -> KnownRow a +fromList = go [] 0 HashMap.empty True + where + go :: [KnownField a] -- Acc fields, reverse order (includes shadowed) + -> Int -- Next index + -> SmallHashMap FieldName Int -- Acc indices of visible fields + -> Bool -- Are all already processed fields visible? + -> [KnownField a] -- To process + -> KnownRow a + go accFields !nextIndex !accVisible !accAllVisible = \case + [] -> KnownRow { + knownRecordVector = reverse accFields + , knownRecordVisible = accVisible + , knownRecordAllVisible = accAllVisible + } + f:fs + | name `HashMap.member` accVisible -> + -- Field shadowed + go (f : accFields) + (succ nextIndex) + accVisible + False + fs + | otherwise -> + go (f : accFields) + (succ nextIndex) + (HashMap.insert name nextIndex accVisible) + accAllVisible + fs + where + name = knownFieldName f + +{------------------------------------------------------------------------------- + Combinators +-------------------------------------------------------------------------------} + +traverse :: forall m a b. + Applicative m + => KnownRow a + -> (FieldName -> a -> m b) + -> m (KnownRow b) +traverse KnownRow{..} f = + mkRow <$> Prelude.traverse f' knownRecordVector + where + mkRow :: [KnownField b] -> KnownRow b + mkRow updated = KnownRow { + knownRecordVector = updated + , knownRecordVisible = knownRecordVisible + , knownRecordAllVisible = knownRecordAllVisible + } + + f' :: KnownField a -> m (KnownField b) + f' (KnownField nm info) = KnownField nm <$> f nm info + +indexed :: KnownRow a -> KnownRow (Int, a) +indexed r = + flip evalState 0 $ + traverse r (const aux) + where + aux :: a -> State Int (Int, a) + aux a = state $ \i -> ((i, a), succ i) + +{------------------------------------------------------------------------------- + Check for projections +-------------------------------------------------------------------------------} + +-- | Reason why we cannot failed to prove 'SubRow' +data NotSubRow = + -- | We do not support precords with shadowed fields + -- + -- Since these fields can only come from the source record, and shadowed + -- fields in the source record are invisible, shadowed fields in the target + -- could only be duplicates of the same field in the source. This is not + -- particularly useful, so we don't support it. Moreover, since we actually + -- create /lenses/ from these subrows, it is important that every field in + -- the source record corresponds to at most /one/ field in the target. + TargetContainsShadowedFields + + -- | Some fields in the target are missing in the source + | SourceMissesFields [FieldName] + deriving (Show, Eq) + +-- | Check if one row is a subrow of another +-- +-- If it is, returns the paired information from both records in the order of +-- the /target/ record along with the index into the /source/ record. +-- +-- See 'NotSubRow' for some discussion of shadowing. +isSubRow :: forall a b. + KnownRow a + -> KnownRow b + -> Either NotSubRow [(Int, (a, b))] +isSubRow recordA recordB = + if not (knownRecordAllVisible recordB) then + Left TargetContainsShadowedFields + else + uncurry checkMissing + . partitionEithers + $ map findInA (toList recordB) + where + findInA :: KnownField b -> Either FieldName (Int, (a, b)) + findInA b = + case HashMap.lookup (knownFieldName b) (visibleMap (indexed recordA)) of + Nothing -> Left $ knownFieldName b + Just a -> Right $ distrib (knownFieldInfo a, knownFieldInfo b) + + checkMissing :: [FieldName] -> x -> Either NotSubRow x + checkMissing [] x = Right x + checkMissing missing _ = Left $ SourceMissesFields missing + + distrib :: ((i, a), b) -> (i, (a, b)) + distrib ((i, a), b) = (i, (a, b)) + +{------------------------------------------------------------------------------- + Outputable +-------------------------------------------------------------------------------} + +instance Outputable a => Outputable (KnownRow a) where + ppr = ppr . toList diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/Row/ParsedRow.hs b/src/Data/Record/Anon/Internal/Plugin/TC/Row/ParsedRow.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/Row/ParsedRow.hs @@ -0,0 +1,193 @@ +{-# LANGUAGE RecordWildCards #-} + +-- | Parsed form of a row type in the source +-- +-- Intended for qualified import. +-- +-- import Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow (Fields) +-- import qualified Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow as ParsedRow +module Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow ( + -- * Definition + Fields -- opaque + , FieldLabel(..) + -- * Query + , lookup + , allKnown + -- * Parsing + , parseFields + , parseFieldLabel + ) where + +import Prelude hiding (lookup) + +import Control.Monad (mzero) +import Data.Foldable (asum) + +import Data.Record.Anon.Internal.Core.FieldName (FieldName) + +import qualified Data.Record.Anon.Internal.Core.FieldName as FieldName + +import Data.Record.Anon.Internal.Plugin.TC.Row.KnownField (KnownField(..)) +import Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow (KnownRow(..)) +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI +import Data.Record.Anon.Internal.Plugin.TC.NameResolution (ResolvedNames(..)) +import Data.Record.Anon.Internal.Plugin.TC.Parsing +import Data.Record.Anon.Internal.Plugin.TC.TyConSubst (TyConSubst) + +import qualified Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow as KnownRow + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +data Fields = + FieldsCons Field Fields + | FieldsNil + | FieldsVar TyVar + | FieldsMerge Fields Fields + +data Field = Field FieldLabel Type + +data FieldLabel = + FieldKnown FieldName + | FieldVar TyVar + deriving (Eq) + +{------------------------------------------------------------------------------- + Query +-------------------------------------------------------------------------------} + +-- | Find field type by name +-- +-- Since records are left-biased, we report the /first/ match, independent of +-- what is in the record tail. If however we encounter an unknown (variable) +-- field, we stop the search: even if a later field matches the one we're +-- looking for, the unknown field might too and, crucially, might not have the +-- same type. +-- +-- Put another way: unlike in 'checkAllFieldsKnown', we do not insist that /all/ +-- fields are known here, but only the fields up to (including) the one we're +-- looking for. +-- +-- Returns the index and the type of the field, if found. +lookup :: FieldName -> Fields -> Maybe (Int, Type) +lookup nm = go 0 . (:[]) + where + go :: Int -> [Fields] -> Maybe (Int, Type) + go _ [] = Nothing + go i (fs:fss) = + case fs of + FieldsNil -> + go i fss + FieldsVar _ -> + -- The moment we encounter a variable (unknown part of the record), + -- we must say that the field is unknown (see discussion above) + Nothing + FieldsCons (Field (FieldKnown nm') typ) fs' -> + if nm == nm' then + Just (i, typ) + else + go (succ i) (fs':fss) + FieldsCons (Field (FieldVar _) _) _ -> + -- We must also stop when we see a field with an unknown name + Nothing + FieldsMerge l r -> + go i (l:r:fss) + + +-- | Return map from field name to type, /if/ all fields are statically known +allKnown :: Fields -> Maybe (KnownRow Type) +allKnown + = go [] . (:[]) + where + go :: [KnownField Type] + -> [Fields] + -> Maybe (KnownRow Type) + go acc [] = Just $ KnownRow.fromList (reverse acc) + go acc (fs:fss) = + case fs of + FieldsNil -> + go acc fss + FieldsCons (Field (FieldKnown nm) typ) fs' -> + go (knownField nm typ : acc) (fs':fss) + FieldsCons (Field (FieldVar _) _) _ -> + Nothing + FieldsVar _ -> + Nothing + FieldsMerge l r -> + go acc (l:r:fss) + + knownField :: FieldName -> Type -> KnownField Type + knownField nm typ = KnownField { + knownFieldName = nm + , knownFieldInfo = typ + } + +{------------------------------------------------------------------------------- + Parsing +-------------------------------------------------------------------------------} + +parseFields :: TyConSubst -> ResolvedNames -> Type -> Maybe Fields +parseFields tcs rn@ResolvedNames{..} = go + where + go :: Type -> Maybe Fields + go fields = asum [ + do (f, fs) <- parseCons tcs fields + f' <- parseField tcs rn f + (FieldsCons f') <$> go fs + , do parseNil tcs fields + return FieldsNil + , do FieldsVar <$> getTyVar_maybe fields + , do args <- parseInjTyConApp tcs tyConMerge fields + (left, right) <- case args of + [l, r] -> return (l, r) + _otherwise -> mzero + FieldsMerge <$> go left <*> go right + ] + +parseField :: TyConSubst -> ResolvedNames -> Type -> Maybe Field +parseField tcs rn field = do + (label, typ) <- parsePair tcs rn field + label' <- parseFieldLabel label + return $ Field label' typ + +parseFieldLabel :: Type -> Maybe FieldLabel +parseFieldLabel label = asum [ + fieldKnown <$> isStrLitTy label + , FieldVar <$> getTyVar_maybe label + ] + where + fieldKnown :: FastString -> FieldLabel + fieldKnown = FieldKnown . FieldName.fromFastString + +-- | Parse @(x := y)@ +parsePair :: TyConSubst -> ResolvedNames -> Type -> Maybe (Type, Type) +parsePair tcs ResolvedNames{..} t = do + args <- parseInjTyConApp tcs tyConPair t + case args of + [_kx, _ky, x, y] -> Just (x, y) + _otherwise -> Nothing + +{------------------------------------------------------------------------------- + Outputable +-------------------------------------------------------------------------------} + +instance Outputable Fields where + ppr (FieldsCons f fs) = parens $ + text "FieldsCons" + <+> ppr f + <+> ppr fs + ppr FieldsNil = text "FieldsNil" + ppr (FieldsVar var) = parens $ text "FieldsVar" <+> ppr var + ppr (FieldsMerge l r) = parens $ text "Merge" <+> ppr l <+> ppr r + +instance Outputable Field where + ppr (Field label typ) = parens $ + text "Field" + <+> ppr label + <+> ppr typ + +instance Outputable FieldLabel where + ppr (FieldKnown nm) = parens $ text "FieldKnown" <+> ppr nm + ppr (FieldVar var) = parens $ text "FieldVar" <+> ppr var + diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/Solver.hs b/src/Data/Record/Anon/Internal/Plugin/TC/Solver.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/Solver.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RecordWildCards #-} + +module Data.Record.Anon.Internal.Plugin.TC.Solver ( + solve + ) where + +import Data.Bifunctor +import Data.Maybe (catMaybes) +import Data.Traversable (forM) + +import Data.Record.Anon.Internal.Plugin.TC.Constraints.AllFields +import Data.Record.Anon.Internal.Plugin.TC.Constraints.KnownFields +import Data.Record.Anon.Internal.Plugin.TC.Constraints.KnownHash +import Data.Record.Anon.Internal.Plugin.TC.Constraints.RowHasField +import Data.Record.Anon.Internal.Plugin.TC.Constraints.SubRow +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI +import Data.Record.Anon.Internal.Plugin.TC.NameResolution +import Data.Record.Anon.Internal.Plugin.TC.Parsing +import Data.Record.Anon.Internal.Plugin.TC.TyConSubst + +{------------------------------------------------------------------------------- + Top-level solver +-------------------------------------------------------------------------------} + +solve :: ResolvedNames -> TcPluginSolver +solve rn given wanted = +-- trace _debugInput $ +-- trace _debugParsed $ + do (solved, new) <- fmap (bimap catMaybes concat . unzip) $ concatM [ + forM parsedAllFields $ uncurry (solveAllFields rn) + , forM parsedKnownFields $ uncurry (solveKnownFields rn) + , forM parsedKnownHash $ uncurry (solveKnownHash rn) + , forM parsedRowHasField $ uncurry (solveRowHasField rn) + , forM parsedSubRow $ uncurry (solveSubRow rn) + ] + return $ TcPluginOk solved new + where + tcs :: TyConSubst + tcs = mkTyConSubst given + + parsedAllFields :: [(Ct, GenLocated CtLoc CAllFields)] + parsedKnownFields :: [(Ct, GenLocated CtLoc CKnownFields)] + parsedKnownHash :: [(Ct, GenLocated CtLoc CKnownHash)] + parsedRowHasField :: [(Ct, GenLocated CtLoc CRowHasField)] + parsedSubRow :: [(Ct, GenLocated CtLoc CSubRow)] + + parsedAllFields = parseAll' (withOrig (parseAllFields tcs rn)) wanted + parsedKnownFields = parseAll' (withOrig (parseKnownFields tcs rn)) wanted + parsedKnownHash = parseAll' (withOrig (parseKnownHash tcs rn)) wanted + parsedRowHasField = parseAll' (withOrig (parseRowHasField tcs rn)) wanted + parsedSubRow = parseAll' (withOrig (parseSubRow tcs rn)) wanted + + _debugInput :: String + _debugInput = unlines [ + "*** input" + , concat [ + "given:" + , showSDocUnsafe (ppr given) + ] + , concat [ + "wanted: " + , showSDocUnsafe (ppr wanted) + ] + ] + + _debugParsed :: String + _debugParsed = unlines [ + "*** parsed" + , concat ["parsedAllFields: ", showSDocUnsafe $ ppr parsedAllFields] + , concat ["parsedKnownFields: ", showSDocUnsafe $ ppr parsedKnownFields] + , concat ["parsedKnownHash: ", showSDocUnsafe $ ppr parsedKnownFields] + , concat ["parsedRowHasField: ", showSDocUnsafe $ ppr parsedRowHasField] + , concat ["parsedSubRow: ", showSDocUnsafe $ ppr parsedSubRow] + , concat ["tcs (TyConSubst): ", showSDocUnsafe $ ppr tcs] + ] + +{------------------------------------------------------------------------------- + Auxiliary +-------------------------------------------------------------------------------} + +concatM :: Applicative m => [m [a]] -> m [a] +concatM = fmap concat . sequenceA diff --git a/src/Data/Record/Anon/Internal/Plugin/TC/TyConSubst.hs b/src/Data/Record/Anon/Internal/Plugin/TC/TyConSubst.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Plugin/TC/TyConSubst.hs @@ -0,0 +1,330 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} + +module Data.Record.Anon.Internal.Plugin.TC.TyConSubst ( + TyConSubst -- opaque + , mkTyConSubst + , splitTyConApp_upTo + ) where + +import Data.Bifunctor +import Data.Either (partitionEithers) +import Data.Foldable (toList, asum) +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Map (Map) + +import qualified Data.Map as Map + +import Data.Record.Anon.Internal.Plugin.TC.EquivClasses +import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI hiding ((<>)) + +{------------------------------------------------------------------------------- + The main type + + TODO: maybe this could be sped up with + ? +-------------------------------------------------------------------------------} + +-- | Substitution for recognizing 'TyCon' applications modulo equalities +-- +-- During constraint solving the set of " given " constraints includes so-called +-- "canonical equalities": equalities of the form +-- +-- > var ~ typ (CTyEqCan) +-- > var ~ TyCon arg1 .. argN (CFunEqCan, the TyCon will be a type family) +-- +-- The problem we want to solve is recognizing if some type τ is of the form +-- +-- > TyCon arg1 arg2 .. argN (0 <= N) +-- +-- modulo those canonical equalities. We limit the scope of what we try to do: +-- +-- o We are only interested in recognizing types of the form above +-- (as opposed to general parsing-modulo-equalities). +-- o We will only use the canonical equalities as-is: we will not attempt to +-- derive any additional equalities from them (i.e. if, say, we know that +-- @x ~ T1@ and @x ~ T2@, we will not attempt to use the fact that this means +-- that @T1 ~ T2@, nor any derived conclusions thereof). We /will/ however +-- try to apply the canononical equalities as often as is necessary (e.g., +-- first applying @x ~ T y@, then applying @y ~ T2@). +-- +-- We solve this problem by constructing a 'TyConSubst': a possibly +-- non-deterministic substitution mapping type variables to types of the form +-- above (that is, a type constructor applied to some arguments). +-- +-- We detail the construction of this substitution below (see documentation of +-- 'Classified' and 'process'), but once we have this substitution, the +-- recognition problem becomes easy: +-- +-- 1. Without loss of generality, let τ be of the form @t arg1 arg2 .. argN@ +-- 2. If @t@ is a 'TyCon', we're done. +-- 3. Otherwise, if @t@ is a variable @x@, lookup @x@ in the substitution; if +-- there is one (or more) mappings for @x@, then we have successfully +-- recognized τ to be of the form above. There is no need to apply the +-- substitution repeatedly. +-- +-- The substitution is non-deterministic because there might be multiple +-- matches. For example, if we have +-- +-- > type family Foo where +-- > Foo = Int +-- +-- then we might well have equalities @x ~ Int, x ~ Foo@ in scope, and so a type +-- @x@ would match two different 'TyCon's. What we do know, however, is that if +-- τ matches both @t arg1 .. argN@ and @t' arg1' .. argM'@ (possibly @N /= M@), +-- then +-- +-- > t arg1 .. argN ~ t' arg1' .. argM' +-- +-- If @t == t'@, we can conclude that the arguments are equal only if @t@ is +-- injective. +data TyConSubst = TyConSubst { + -- | Mapping from (canonical) variables to 'TyCon' applications + tyConSubstMap :: Map TcTyVar (NonEmpty (TyCon, [Type])) + + -- | Map each variable to the canonical representative + -- + -- See 'Classified' for a detailed discussion of canonical variables. + , tyConSubstCanon :: Map TcTyVar TcTyVar + } + +{------------------------------------------------------------------------------- + Basic functionality for working with 'TyConSubst' +-------------------------------------------------------------------------------} + +-- | Empty substitution +-- +-- The canonical variables map is established once when the initial substitution +-- is generated and not updated thereafter. +tyConSubstEmpty :: Map TcTyVar TcTyVar -> TyConSubst +tyConSubstEmpty canon = TyConSubst { + tyConSubstMap = Map.empty + , tyConSubstCanon = canon + } + +-- | Lookup a variable in the substitution +tyConSubstLookup :: TcTyVar -> TyConSubst -> Maybe (NonEmpty (TyCon, [Type])) +tyConSubstLookup var TyConSubst{..} = Map.lookup var' tyConSubstMap + where + var' :: TcTyVar + var' = canonicalize tyConSubstCanon var + +-- | Extend substitution with new bindings +tyConSubstExtend :: + [(TcTyVar, (TyCon, [Type]))] + -> TyConSubst -> TyConSubst +tyConSubstExtend new subst@TyConSubst{..} = subst { + tyConSubstMap = Map.unionWith (<>) + (Map.fromList $ map (uncurry aux) new) + tyConSubstMap + } + where + aux :: TcTyVar -> (TyCon, [Type]) -> (TcTyVar, NonEmpty (TyCon, [Type])) + aux var s = (canonicalize tyConSubstCanon var, s :| []) + +{------------------------------------------------------------------------------- + Classification +-------------------------------------------------------------------------------} + +-- | Classified canonical equality constraints +-- +-- The first step in the construction of the 'TyConSubst' is to classify the +-- available canonical equalities as one of three categories, defined below. +data Classified = Classified { + -- | " Obviously " productive mappings + -- + -- An equality @var := TyCon args@ is productive, because as soon as we + -- apply it, we are done: we have successfully recognized a type as being + -- an application of a concrete type constructor (note that we only ever + -- apply the substitution to the head @t@ of a type @t args@, never to the + -- arguments). + classifiedProductive :: [(TcTyVar, (TyCon, [Type]))] + + -- | Extend equivalence class of variables + -- + -- An equality @var1 := var2@ we will regard as extending the equivalence + -- classes of variables (see 'constructEquivClasses'). + , classifiedExtendEquivClass :: [(TcTyVar, TcTyVar)] + + -- | Substitutions we need to reconsider later + -- + -- An equality @var1 := var2 args@ (with @args@ a non-empty list of + -- arguments) is most problematic. Applying it /may/ allow us to make + -- progress, but it may not (consider for example @var := var arg@). We + -- will reconsider such equalities at the end (see 'process'). + , classifiedReconsider :: [(TcTyVar, (TcTyVar, NonEmpty Type))] + } + +instance Semigroup Classified where + c1 <> c2 = Classified { + classifiedProductive = combine classifiedProductive + , classifiedExtendEquivClass = combine classifiedExtendEquivClass + , classifiedReconsider = combine classifiedReconsider + } + where + combine :: (Classified -> [a]) -> [a] + combine f = f c1 ++ f c2 + +instance Monoid Classified where + mempty = Classified [] [] [] + +productive :: TcTyVar -> (TyCon, [Type]) -> Classified +productive var (tyCon, args) = mempty { + classifiedProductive = [(var, (tyCon, args))] + } + +extendEquivClass :: TcTyVar -> TcTyVar -> Classified +extendEquivClass var var' = mempty { + classifiedExtendEquivClass = [(var, var')] + } + +reconsider :: TcTyVar -> (TcTyVar, NonEmpty Type) -> Classified +reconsider var (var', args) = mempty { + classifiedReconsider = [(var, (var', args))] + } + +-- | Classify a set of given constraints +-- +-- See 'Classified' for details. +classify :: [Ct] -> Classified +classify = go mempty + where + go :: Classified -> [Ct] -> Classified + go acc [] = acc + go acc (c:cs) = + case isCanonicalVarEq c of + Just (var, splitAppTys -> (fn, args)) + | Just tyCon <- tyConAppTyCon_maybe fn -> + go (productive var (tyCon, args) <> acc) cs + | Just var' <- getTyVar_maybe fn, null args -> + go (extendEquivClass var var' <> acc) cs + | Just var' <- getTyVar_maybe fn, x:xs <- args -> + go (reconsider var (var', x :| xs) <> acc) cs + _otherwise -> + go acc cs + +{------------------------------------------------------------------------------- + Processing +-------------------------------------------------------------------------------} + +-- | Construct 'TyCon' substitution from classified equality constraints +-- +-- The difficult part in constructing this substitution are the equalities of +-- the form @var1 ~ var2 args@, which we ear-marked as "to reconsider" during +-- classification. +-- +-- We will do this iteratively: +-- +-- o We first construct a set of variable equivalence classes based on +-- 'classifiedExtendEquivClass' (using 'constructEquivClasses'), and use that +-- along with the "obviously productive" equalities ('classifiedProductive') +-- as the initial value of the accumulator (a 'TyConSubst'). +-- o We then repeatedly consider the remaining equalities. Whenever there is +-- a substitution available in the accumulator for @var2@ which turns it into +-- a type of the form @TyCon args'@, we add @var1 := TyCon args' args@ to the +-- accumulator. +-- o We keep doing this until we can make no more progress. +-- +-- The functions for working with 'TyConSubst' take the variable equivalence +-- classes into acocunt, so we do not need to do that here. +-- +-- Two observations: +-- +-- o This process must terminate: there are a finite number of constraints +-- to consider, and whenever we apply a substitution from the accumulator, +-- we get an "obviously productive" substitution: we do not create new work +-- in the loop. +-- o We may end up ignoring some substitutions: if there is a substitution +-- @var1 := var2 args@ and we don't have any (productive) substitutions for +-- @var2@, we will just ignore it. +-- +-- A note on recursive bindings: a direct or indirect recursive binding +-- +-- > x := x args1 x := y args1 +-- > y := x args2 +-- +-- where @args1, args2@ are non-empty lists of arguments, /cannot/ be relevant: +-- if they were, that would imply that there is some type constructor (regular +-- datatype or type family) which can be applied to an arbitrary number of +-- arguments. Such datatypes or type families cannot be defined in Haskell. +-- We therefore take no special care in handling recursive bindings, other than +-- to note (as we did above) that the process must terminate. +process :: Classified -> TyConSubst +process Classified{..} = + go initSubst classifiedReconsider + where + initSubst :: TyConSubst + initSubst = + tyConSubstExtend classifiedProductive + $ tyConSubstEmpty (constructEquivClasses classifiedExtendEquivClass) + + go :: TyConSubst + -> [(TcTyVar, (TcTyVar, NonEmpty Type))] + -> TyConSubst + go acc rs = + let (prod, rest) = tryApply makeProductive rs in + if null prod + then acc -- No other equations can be made productive + else go (tyConSubstExtend prod acc) rest + where + makeProductive :: + (TcTyVar, (TcTyVar, NonEmpty Type)) + -> Maybe (NonEmpty (TcTyVar, (TyCon, [Type]))) + makeProductive (var, (var', args)) = + fmap (fmap (uncurry aux)) (tyConSubstLookup var' acc) + where + aux :: TyCon -> [Type] -> (TcTyVar, (TyCon, [Type])) + aux tyCon args' = (var, (tyCon, (args' ++ toList args))) + +-- | Construct 'TyConSubst' +-- +-- This is the main function that builds the 'TyConSubst' from the set of +-- " given " constraints. The actual work is done by 'classify' and 'process'. +mkTyConSubst :: [Ct] -> TyConSubst +mkTyConSubst = process . classify + +{------------------------------------------------------------------------------- + Using +-------------------------------------------------------------------------------} + +-- | Like 'splitTyConApp_maybe', but taking canonical equalities into account +-- +-- See 'TyConSubst' for a detailed discussion. +splitTyConApp_upTo :: TyConSubst -> Type -> Maybe (NonEmpty (TyCon, [Type])) +splitTyConApp_upTo subst typ = asum [ + -- Direct match + do tyCon <- tyConAppTyCon_maybe fn + return ((tyCon, args) :| []) + + -- Indirect match + , do var <- getTyVar_maybe fn + fmap (fmap (second (++ args))) $ tyConSubstLookup var subst + ] + where + (fn, args) = splitAppTys typ + +{------------------------------------------------------------------------------- + Outputable +-------------------------------------------------------------------------------} + +instance Outputable TyConSubst where + ppr TyConSubst{..} = parens $ + text "TyConSubst" + <+> ppr tyConSubstMap + <+> ppr tyConSubstCanon + +{------------------------------------------------------------------------------- + Internal auxiliary +-------------------------------------------------------------------------------} + +-- | Attempt to apply a non-deterministic function to a list of values +-- +-- Returns the successful results as well as the inputs on which the function +-- failed. +tryApply :: forall a b. (a -> Maybe (NonEmpty b)) -> [a] -> ([b], [a]) +tryApply f = first (concat . map toList) . partitionEithers . map f' + where + f' :: a -> Either (NonEmpty b) a + f' a = maybe (Right a) Left $ f a diff --git a/src/Data/Record/Anon/Internal/Reflection.hs b/src/Data/Record/Anon/Internal/Reflection.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Reflection.hs @@ -0,0 +1,48 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} + +-- | Low-level reflection utility for internal use. +-- +-- Intended for qualified import: +-- +-- > import Data.Record.Anon.Internal.Reflection (Reflected(..)) +-- > import qualified Data.Record.Anon.Internal.Reflection as Unsafe +module Data.Record.Anon.Internal.Reflection ( + Reflected(..) + , reflectKnownFields + , reflectAllFields + , reflectSubRow + , reflectRowHasField + ) where + +import Data.Record.Anon.Plugin.Internal.Runtime + +{------------------------------------------------------------------------------- + Dictionary +-------------------------------------------------------------------------------} + +-- | Evidence of some constraint @c@ +-- +-- This is like 'Data.Record.Anon.Dict', but without the functor argument. +data Reflected c where + Reflected :: c => Reflected c + +{------------------------------------------------------------------------------- + Reflection +-------------------------------------------------------------------------------} + +newtype WK r = MkWK (KnownFields r => Reflected (KnownFields r)) +newtype WA r c = MkWA (AllFields r c => Reflected (AllFields r c)) +newtype WS r r' = MkWS (SubRow r r' => Reflected (SubRow r r')) +newtype WR n r a = MkWR (RowHasField n r a => Reflected (RowHasField n r a)) + +reflectKnownFields :: DictKnownFields k r -> Reflected (KnownFields r) +reflectAllFields :: DictAllFields k r c -> Reflected (AllFields r c) +reflectSubRow :: DictSubRow k r r' -> Reflected (SubRow r r') +reflectRowHasField :: DictRowHasField k n r a -> Reflected (RowHasField n r a) + +reflectKnownFields f = noInlineUnsafeCo (MkWK Reflected) f +reflectAllFields f = noInlineUnsafeCo (MkWA Reflected) f +reflectSubRow f = noInlineUnsafeCo (MkWS Reflected) f +reflectRowHasField f = noInlineUnsafeCo (MkWR Reflected) f diff --git a/src/Data/Record/Anon/Internal/Simple.hs b/src/Data/Record/Anon/Internal/Simple.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Simple.hs @@ -0,0 +1,284 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | Simple interface to the anonymous records library +-- +-- This module defines a type @Record r@ such that, for example, +-- +-- > Record '[ '("a", Bool), '("b", Char) ] +-- +-- is the type of records with two fields @a@ and @b@, of types @Bool@ and +-- @Char@ respectively. The difference between the simple interface and the +-- advanced interface is that the advanced interface defines a type +-- +-- > Record f '[ '("a", Bool), '("b", Char) ] +-- +-- In this case, fields @a@ and @b@ have type @f Bool@ and @f Char@ instead. +-- See "Data.Record.Anonymous.Advanced" for details. +-- +-- NOTE: We do not offer a set of combinators in the simple interface, as these +-- are not likely to be very useful. In the rare cases that they are needed, +-- users should use 'toAdvanced'/'fromAdvanced' to temporary use the advanced +-- API for these operations. +-- +-- This module is intended for qualified import. +-- +-- > import Data.Record.Anonymous.Simple (Record) +-- > import qualified Data.Record.Anonymous.Simple as Anon +module Data.Record.Anon.Internal.Simple ( + Record -- opaque + -- * Basic API + , Field -- opaque + , empty + , insert + , insertA + , get + , set + , merge + , lens + , project + , inject + , applyPending + -- * Constraints + , RecordConstraints + -- * Interop with the advanced interface + , toAdvanced + , fromAdvanced + , sequenceA + -- * Support for @typelet@ + , letRecordT + , letInsertAs + ) where + +import Prelude hiding (sequenceA) + +import Data.Aeson (ToJSON(..), FromJSON(..)) +import Data.Bifunctor +import Data.Record.Generic +import Data.Record.Generic.Eq +import Data.Record.Generic.JSON +import Data.Record.Generic.Show +import Data.Tagged +import GHC.Exts +import GHC.OverloadedLabels +import GHC.Records.Compat +import GHC.TypeLits +import TypeLet +import Data.Primitive.SmallArray + +import qualified Optics.Core as Optics + +import Data.Record.Anon.Plugin.Internal.Runtime + +import Data.Record.Anon.Internal.Advanced (Field(..)) + +import qualified Data.Record.Anon.Internal.Advanced as A + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Anonymous record +-- +-- A @Record r@ has a field @n@ of type @x@ for every @(n := x)@ in @r@. +-- +-- To construct a 'Record', use 'Data.Record.Anon.Simple.insert' and +-- 'Data.Record.Anon.Simple.empty', or use the @ANON@ syntax. See +-- 'Data.Record.Anon.Simple.insert' for examples. +-- +-- To access fields of the record, either use the 'GHC.Records.Compat.HasField' +-- instances (possibly using the @record-dot-preprocessor@), or using +-- 'Data.Record.Anon.Simple.get' and 'Data.Record.Anon.Simple.set'. +-- +-- Remember to enable the plugin when working with anonymous records: +-- +-- > {-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} +-- +-- NOTE: For some applications it is useful to have an additional functor +-- parameter @f@, so that every field has type @f x@ instead. +-- See "Data.Record.Anon.Advanced". +newtype Record r = SimpleRecord { toAdvanced :: A.Record I r } + +{------------------------------------------------------------------------------- + Interop with advanced API +-------------------------------------------------------------------------------} + +fromAdvanced :: A.Record I r -> Record r +fromAdvanced = SimpleRecord + +sequenceA :: Applicative m => A.Record m r -> m (Record r) +sequenceA = fmap fromAdvanced . A.sequenceA' + +{------------------------------------------------------------------------------- + Basic API +-------------------------------------------------------------------------------} + +empty :: Record '[] +empty = fromAdvanced $ A.empty + +insert :: Field n -> a -> Record r -> Record (n := a : r) +insert n x = fromAdvanced . A.insert n (I x) . toAdvanced + +insertA :: + Applicative m + => Field n -> m a -> m (Record r) -> m (Record (n := a : r)) +insertA f x r = insert f <$> x <*> r + +merge :: Record r -> Record r' -> Record (Merge r r') +merge r r' = fromAdvanced $ A.merge (toAdvanced r) (toAdvanced r') + +lens :: SubRow r r' => Record r -> (Record r', Record r' -> Record r) +lens = + bimap fromAdvanced (\f -> fromAdvanced . f . toAdvanced) + . A.lens + . toAdvanced + +project :: SubRow r r' => Record r -> Record r' +project = fst . lens + +inject :: SubRow r r' => Record r' -> Record r -> Record r +inject small = ($ small) . snd . lens + +applyPending :: Record r -> Record r +applyPending = fromAdvanced . A.applyPending . toAdvanced + +{------------------------------------------------------------------------------- + HasField +-------------------------------------------------------------------------------} + +instance HasField n (A.Record I r) (I a) + => HasField (n :: Symbol) ( Record r) a where + hasField = aux . hasField @n . toAdvanced + where + aux :: (I a -> A.Record I r, I a) -> (a -> Record r, a) + aux (setX, x) = (fromAdvanced . setX . I, unI x) + +instance Optics.LabelOptic n Optics.A_Lens (A.Record I r) (A.Record I r) (I a) (I a) + => Optics.LabelOptic n Optics.A_Lens ( Record r) ( Record r) a a where + labelOptic = toAdvanced Optics.% fromLabel @n Optics.% fromI + where + toAdvanced :: Optics.Iso' (Record r) (A.Record I r) + toAdvanced = Optics.coerced + + fromI :: Optics.Iso' (I a) a + fromI = Optics.coerced + +-- | Get field from the record +-- +-- This is just a wrapper around 'getField'. +get :: forall n r a. RowHasField n r a => Field n -> Record r -> a +get (Field _) = getField @n @(Record r) + +-- | Update field in the record +-- +-- This is just a wrapper around 'setField'. +set :: forall n r a. RowHasField n r a => Field n -> a -> Record r -> Record r +set (Field _) = flip (setField @n @(Record r)) + +{------------------------------------------------------------------------------- + Constraints +-------------------------------------------------------------------------------} + +class (AllFields r c, KnownFields r) => RecordConstraints r c +instance (AllFields r c, KnownFields r) => RecordConstraints r c + +{------------------------------------------------------------------------------- + Generics + + We define 'dict' and 'metadata' directly rather than going through the + instance for 'A.Record'; we /could/ do that, but it's hassle and doesn't + really buy us anything. +-------------------------------------------------------------------------------} + +recordConstraints :: forall r c. + RecordConstraints r c + => Proxy c -> Rep (Dict c) (Record r) +recordConstraints _ = Rep $ + aux <$> proxy fieldDicts (Proxy @r) + where + aux :: DictAny c -> Dict c Any + aux DictAny = Dict + +instance KnownFields r => Generic (Record r) where + type Constraints (Record r) = RecordConstraints r + type MetadataOf (Record r) = SimpleFieldTypes r + + from = fromAdvancedRep . from . toAdvanced + to = fromAdvanced . to . toAdvancedRep + dict = recordConstraints + metadata = const recordMetadata + +fromAdvancedRep :: Rep I (A.Record I r) -> Rep I (Record r) +fromAdvancedRep = noInlineUnsafeCo + +toAdvancedRep :: Rep I (Record r) -> Rep I (A.Record I r) +toAdvancedRep = noInlineUnsafeCo + +recordMetadata :: forall r. KnownFields r => Metadata (Record r) +recordMetadata = Metadata { + recordName = "Record" + , recordConstructor = "Record" + , recordSize = length fields + , recordFieldMetadata = Rep $ smallArrayFromList fields + } + where + fields :: [FieldMetadata Any] + fields = fieldMetadata (Proxy @r) + +{------------------------------------------------------------------------------- + Instances + + As for the generic instances, we make no attempt to go through the advanced + API here, as it's painful for little benefit. +-------------------------------------------------------------------------------} + +instance RecordConstraints r Show => Show (Record r) where + showsPrec = gshowsPrec + +instance RecordConstraints r Eq => Eq (Record r) where + (==) = geq + +instance ( RecordConstraints r Eq + , RecordConstraints r Ord + ) => Ord (Record r) where + compare = gcompare + +instance RecordConstraints r ToJSON => ToJSON (Record r) where + toJSON = gtoJSON + +instance RecordConstraints r FromJSON => FromJSON (Record r) where + parseJSON = gparseJSON + +{------------------------------------------------------------------------------- + Support for @typelet@ +-------------------------------------------------------------------------------} + +-- | Introduce type variable for a row +letRecordT :: forall r. + (forall r'. Let r' r => Proxy r' -> Record r) + -> Record r +letRecordT f = letT' (Proxy @r) f + +-- | Insert field into a record and introduce type variable for the result +letInsertAs :: forall r r' n a. + Proxy r -- ^ Type of the record we are constructing + -> Field n -- ^ New field to be inserted + -> a -- ^ Value of the new field + -> Record r' -- ^ Record constructed so far + -> (forall r''. Let r'' (n := a : r') => Record r'' -> Record r) + -- ^ Assign type variable to new partial record, and continue + -> Record r +letInsertAs _ n x r = letAs' (insert n x r) + diff --git a/src/Data/Record/Anon/Internal/Util/SmallHashMap.hs b/src/Data/Record/Anon/Internal/Util/SmallHashMap.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Util/SmallHashMap.hs @@ -0,0 +1,130 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} + +-- | Strict hash table designed for small hash tables +-- +-- Currently this is is just a wrapper around a 'Map'. We do not use 'HashMap', +-- since for small hash tables the overhead from having to copy all the small +-- arrays defeats the purpose of having a 'Diff' in the first place. +-- +-- Having this as a separate abstraction also allows us to easily change the +-- representation of the 'HashMap' without affecting the rest of the code. +-- +-- Intended for qualified import. +-- +-- > import Data.Record.Anon.Internal.Util.SmallHashMap (SmallHashMap) +-- > import qualified Data.Record.Anon.Internal.Util.SmallHashMap as HashMap +module Data.Record.Anon.Internal.Util.SmallHashMap ( + SmallHashMap + -- * Standard operations + , null + , empty + , lookup + , member + , insert + , toList + , alter + -- * Non-standard operations + , alterExisting + ) where + +import Prelude hiding (lookup, null) + +import Control.Monad.State +import Data.Bifunctor +import Data.Coerce (coerce) +import Data.Hashable (Hashable(hash)) +import Data.Map.Strict (Map) +import Data.Tuple (swap) + +import qualified Data.Map.Strict as Map + +{------------------------------------------------------------------------------- + Wrapper to compare keys based on their hash first +-------------------------------------------------------------------------------} + +newtype Hashed k = Hashed k + deriving (Show) + +instance (Hashable k, Eq k) => Eq (Hashed k) where + Hashed a == Hashed b = and [ + hash a == hash b + , a == b + ] + +instance (Hashable k, Ord k) => Ord (Hashed k) where + compare (Hashed a) (Hashed b) = mconcat [ + compare (hash a) (hash b) + , compare a b + ] + +{------------------------------------------------------------------------------- + Definition of the HashMap proper +-------------------------------------------------------------------------------} + +newtype SmallHashMap k a = Wrap { unwrap :: Map (Hashed k) a } + deriving (Show) + +-- | Cannot derive 'Functor' because the 'Functor' instance for 'Map' is wrong +-- (not strict) +instance Functor (SmallHashMap k) where + fmap f = Wrap . Map.map f . unwrap + +{------------------------------------------------------------------------------- + Standard operations +-------------------------------------------------------------------------------} + +null :: forall k a. SmallHashMap k a -> Bool +null = coerce $ Map.null @(Hashed k) @a + +empty :: forall k a. SmallHashMap k a +empty = coerce $ Map.empty @(Hashed k) @a + +lookup :: forall k a. (Hashable k, Ord k) => k -> SmallHashMap k a -> Maybe a +lookup = coerce $ Map.lookup @(Hashed k) @a + +member :: forall k a. (Hashable k, Ord k) => k -> SmallHashMap k a -> Bool +member = coerce $ Map.member @(Hashed k) @a + +insert :: forall k a. + (Hashable k, Ord k) + => k -> a -> SmallHashMap k a -> SmallHashMap k a +insert = coerce $ Map.insert @(Hashed k) @a + +toList :: forall k a. SmallHashMap k a -> [(k, a)] +toList = coerce $ Map.toList @(Hashed k) @a + +alter :: forall k a. + (Hashable k, Ord k) + => (Maybe a -> Maybe a) -> k -> SmallHashMap k a -> SmallHashMap k a +alter = coerce $ Map.alter @(Hashed k) @a + +{------------------------------------------------------------------------------- + Non-standard operations +-------------------------------------------------------------------------------} + +-- | Alter an existing key +-- +-- Returns 'Nothing' if the key does not exist. +-- +-- @O(1)@. +alterExisting :: forall k a b. + (Hashable k, Ord k) + => k -> (a -> (b, Maybe a)) -> SmallHashMap k a -> Maybe (b, SmallHashMap k a) +alterExisting k f m + | null m = Nothing + | otherwise = + fmap (second Wrap . swap) + . distrib + . flip runState Nothing + . Map.alterF f' (Hashed k) + . unwrap + $ m + where + f' :: Maybe a -> State (Maybe b) (Maybe a) + f' Nothing = state $ \_ -> (Nothing, Nothing) + f' (Just a) = state $ \_ -> swap $ first Just (f a) + + distrib :: (x, Maybe y) -> Maybe (x, y) + distrib (x, my) = (x,) <$> my diff --git a/src/Data/Record/Anon/Internal/Util/StrictArray.hs b/src/Data/Record/Anon/Internal/Util/StrictArray.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Internal/Util/StrictArray.hs @@ -0,0 +1,191 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Data.Record.Anon.Internal.Util.StrictArray ( + StrictArray -- opaque + -- * Reads + , (!) + -- * Conversion + , fromList + , fromListN + , fromLazy + , toLazy + -- * Non-monadic combinators + , (//) + , update + , backpermute + , zipWith + -- * Monadic combinators + , mapM + , zipWithM + ) where + +import Prelude hiding (mapM, zipWith) + +import Control.Monad (forM_) +import Data.Primitive.SmallArray + +import qualified Control.Monad as Monad +import qualified Data.Foldable as Foldable + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Strict vector +-- +-- Implemented as a wrapper around a 'SmallArray'. +-- +-- NOTE: None of the operations on 'Vector' do any bounds checking. +-- +-- NOTE: 'Vector' is implemented as a newtype around 'SmallArray', which in turn +-- is defined as +-- +-- > data SmallArray a = SmallArray (SmallArray# a) +-- +-- Furthermore, 'Canonical' is a newtype around 'Vector', which is then used in +-- 'Record' as +-- +-- > data Record (f :: k -> Type) (r :: Row k) = Record { +-- > recordCanon :: {-# UNPACK #-} !(Canonical f) +-- > , .. +-- > } +-- +-- This means that 'Record' will have /direct/ access (no pointers) to the +-- 'SmallArray#'. +newtype StrictArray a = WrapLazy { unwrapLazy :: SmallArray a } + deriving newtype (Show, Eq, Foldable, Semigroup, Monoid) + +{------------------------------------------------------------------------------- + Reads +-------------------------------------------------------------------------------} + +(!) :: StrictArray a -> Int -> a +(!) = indexSmallArray . unwrapLazy + +{------------------------------------------------------------------------------- + Conversion +-------------------------------------------------------------------------------} + +fromList :: [a] -> StrictArray a +fromList as = fromListN (length as) as + +fromListN :: Int -> [a] -> StrictArray a +fromListN n as = WrapLazy $ runSmallArray $ do + r <- newSmallArray n undefined + forM_ (zip [0..] as) $ \(i, !a) -> + writeSmallArray r i a + return r + +fromLazy :: forall a. SmallArray a -> StrictArray a +fromLazy v = go 0 + where + go :: Int -> StrictArray a + go i + | i < sizeofSmallArray v + = let !_a = indexSmallArray v i in go (succ i) + + | otherwise + = WrapLazy v + +toLazy :: StrictArray a -> SmallArray a +toLazy = unwrapLazy + +{------------------------------------------------------------------------------- + Non-monadic combinators +-------------------------------------------------------------------------------} + +instance Functor StrictArray where + fmap f (WrapLazy as) = WrapLazy $ runSmallArray $ do + r <- newSmallArray newSize undefined + forArrayM_ as $ \i a -> writeSmallArray r i $! f a + return r + where + newSize :: Int + newSize = sizeofSmallArray as + +(//) :: StrictArray a -> [(Int, a)] -> StrictArray a +(//) (WrapLazy as) as' = WrapLazy $ runSmallArray $ do + r <- thawSmallArray as 0 newSize + forM_ as' $ \(i, !a) -> writeSmallArray r i a + return r + where + newSize :: Int + newSize = sizeofSmallArray as + +update :: StrictArray a -> StrictArray (Int, a) -> StrictArray a +update (WrapLazy as) (WrapLazy as') = WrapLazy $ runSmallArray $ do + r <- thawSmallArray as 0 newSize + forArrayM_ as' $ \_i (j, !a) -> writeSmallArray r j a + return r + where + newSize :: Int + newSize = sizeofSmallArray as + +backpermute :: StrictArray a -> StrictArray Int -> StrictArray a +backpermute (WrapLazy as) (WrapLazy is) = WrapLazy $ runSmallArray $ do + r <- newSmallArray newSize undefined + forArrayM_ is $ \i j -> writeSmallArray r i $! indexSmallArray as j + return r + where + newSize :: Int + newSize = length is + +zipWith :: (a -> b -> c) -> StrictArray a -> StrictArray b -> StrictArray c +zipWith f (WrapLazy as) (WrapLazy bs) = WrapLazy $ runSmallArray $ do + r <- newSmallArray newSize undefined + forM_ [0 .. newSize - 1] $ \i -> do + let !c = f (indexSmallArray as i) (indexSmallArray bs i) + writeSmallArray r i c + return r + where + newSize :: Int + newSize = min (sizeofSmallArray as) (sizeofSmallArray bs) + +{------------------------------------------------------------------------------- + Applicative combinators + + NOTE: The monadic combinators here do two traversals, first collecting all + elements of the vector in memory, and then constructing the new vector. The + alternative is to use 'traverseSmallArrayP', but it is only sound with + certain monads. Since this restriction would leak out to users of the library + (through the monadic combinators on 'Record'), we prefer to avoid it. +-------------------------------------------------------------------------------} + +mapM :: forall m a b. + Applicative m + => (a -> m b) -> StrictArray a -> m (StrictArray b) +mapM f (WrapLazy as) = + fromListN newSize <$> + traverse f (Foldable.toList as) + where + newSize :: Int + newSize = sizeofSmallArray as + +zipWithM :: + Applicative m + => (a -> b -> m c) -> StrictArray a -> StrictArray b -> m (StrictArray c) +zipWithM f (WrapLazy as) (WrapLazy bs) = do + fromListN newSize <$> + Monad.zipWithM f (Foldable.toList as) (Foldable.toList bs) + where + newSize :: Int + newSize = min (sizeofSmallArray as) (sizeofSmallArray bs) + +{------------------------------------------------------------------------------- + Internal auxiliary +-------------------------------------------------------------------------------} + +forArrayM_ :: forall m a. Monad m => SmallArray a -> (Int -> a -> m ()) -> m () +forArrayM_ arr f = go 0 + where + go :: Int -> m () + go i + | i < sizeofSmallArray arr + = f i (indexSmallArray arr i) >> go (succ i) + + | otherwise + = return () + diff --git a/src/Data/Record/Anon/Plugin.hs b/src/Data/Record/Anon/Plugin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Plugin.hs @@ -0,0 +1,15 @@ +{-# OPTIONS_HADDOCK hide #-} + +-- | Type checker and source plugin for working with anonymous records +-- +-- To use this, add +-- +-- > {-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} +-- +-- to your module. You should not need to import this module; see +-- "Data.Record.Anon.Simple" or "Data.Record.Anon.Advanced" instead. +module Data.Record.Anon.Plugin (plugin) where + +import Data.Record.Anon.Internal.Plugin (plugin) + + diff --git a/src/Data/Record/Anon/Plugin/Internal/Runtime.hs b/src/Data/Record/Anon/Plugin/Internal/Runtime.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Plugin/Internal/Runtime.hs @@ -0,0 +1,276 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} + +{-# OPTIONS_HADDOCK hide #-} + +-- | Runtime for code generated by the plugin +-- +-- Users should not need to import from this module directly. +module Data.Record.Anon.Plugin.Internal.Runtime ( + -- * Row + Pair(..) + , Row + -- * RowHasField + , RowHasField(..) + , DictRowHasField + , evidenceRowHasField + -- * Term-level metadata + , KnownFields(..) + , DictKnownFields + , evidenceKnownFields + , fieldMetadata + -- * Type-level metadata + , FieldTypes + , SimpleFieldTypes + -- * AllFields + , AllFields(..) + , DictAny(..) + , DictAllFields + , evidenceAllFields + -- * KnownHash + , KnownHash(..) + , evidenceKnownHash + -- * Merging + , Merge + -- * Subrecords + , SubRow(..) + , DictSubRow + , evidenceSubRow + -- * Utility + , noInlineUnsafeCo + ) where + +import Data.Kind +import Data.Primitive.SmallArray +import Data.Record.Generic hiding (FieldName) +import Data.SOP.Constraint (Compose) +import Data.Tagged +import GHC.Exts (Any) +import GHC.TypeLits +import Unsafe.Coerce (unsafeCoerce) + +import Data.Record.Anon.Internal.Util.StrictArray (StrictArray) + +import qualified Data.Record.Anon.Internal.Util.StrictArray as Strict + +{------------------------------------------------------------------------------- + IMPLEMENTATION NOTE + + Support for name resolution in typechecker plugins is a bit rudimentary. The + only available API is + + > lookupOrig :: Module -> OccName -> TcPluginM Name + + This function can /only/ be used to look things up in the given module that + are /defined by/ that module; it won't find anything that is merely /exported/ + by the module. This makes name lookup brittle: an internal re-organization + that changes where things are defined might break the plugin, even if the + export lists of those modules have not changed. This is merely annoying for + internal reshuffling, but worse for external reshuffling as such changes would + be considered entirely backwards compatible and not require any major version + changes. + + We address this in two ways: + + 1. Anything defined internally in this package that needs to be referred by the + plugin is defined in here in this @.Runtime@ module. This does have the + unfortunate consequence that this module contains definitions that are not + necessarily related to each other, apart from "required by the plugin". + 2. We avoid dependencies on external packages altogether. For example, instead + of the plugin providing evidence for 'HasField' directly, it instead + provides evidence for a 'HasField'-like class defined here in the + @.Runtime@ module. We then give a "forwarding" instance for the " real " + 'HasField' in terms of that class; the plugin does not need to be aware of + that forwarding instance, of course, and it won't be done in this module. + + Avoiding any external dependencies here has an additional advantage: even if + we accept that the plugin must specifiy the exact module where something is + defined in an external package, there is a secondary problem: users who then + use the plugin must declare those packages as explicit dependencies, or else + name resolution will fail at compile time (of the user's package) with a + mysterious error message. It may be possible to work around this problem by + using something else instead of @findImportedModule@, but avoiding external + dependencies just bypasses the problem altogether. + + NOTE: In order to avoid headaches with cyclic module dependencies, we use the + convention that the runtime can only import from @Data.Record.Anon.Internal.Core.*@, + which in turn cannot import from the runtime (and can only import from other + modules in the Core.*@). One important consequence of this split is that + nothing in @Core.*@ is aware of the concept of rows, which is introduced here. +-------------------------------------------------------------------------------} + +{------------------------------------------------------------------------------- + Row +-------------------------------------------------------------------------------} + +-- | Pair of values +-- +-- This is used exclusively promoted to the type level, in 'Row'. +data Pair a b = a := b + +-- | Row: type-level list of field names and corresponding field types +type Row k = [Pair Symbol k] + +{------------------------------------------------------------------------------- + HasField +-------------------------------------------------------------------------------} + +-- | Specialized form of 'HasField' +-- +-- @RowHasField n r a@ holds if there is an @(n := a)@ in @r@. +class RowHasField (n :: Symbol) (r :: Row k) (a :: k) | n r -> a where + rowHasField :: DictRowHasField k n r a + rowHasField = undefined + +type DictRowHasField k (n :: Symbol) (r :: Row k) (a :: k) = + Tagged '(n, r, a) Int + +evidenceRowHasField :: forall k n r a. Int -> DictRowHasField k n r a +evidenceRowHasField = Tagged + +{------------------------------------------------------------------------------- + Term-level metadata + + NOTE: Here and elsewhere, we provide an (undefined) default implementation, + to avoid the method showing up in the Haddocks. In practice this makes no + difference: the body of the class is not exported, and instances are instead + computed by the plugin. +-------------------------------------------------------------------------------} + +-- | Require that all field names in @r@ are known +class KnownFields (r :: Row k) where + fieldNames :: DictKnownFields k r + fieldNames = undefined + +type DictKnownFields k (r :: Row k) = Tagged r [String] + +evidenceKnownFields :: forall k r. [String] -> DictKnownFields k r +evidenceKnownFields = Tagged + +{------------------------------------------------------------------------------- + Type-level metadata +-------------------------------------------------------------------------------} + +-- | Type-level metadata +-- +-- > FieldTypes Maybe [ "a" := Int, "b" := Bool ] +-- > == [ '("a", Maybe Int), '("b", Maybe Bool) ] +type family FieldTypes (f :: k -> Type) (r :: Row k) :: [(Symbol, Type)] + +-- | Like 'FieldTypes', but for the simple API (no functor argument) +-- +-- > SimpleFieldTypes [ "a" := Int, "b" := Bool ] +-- > == [ '("a", Int), '("b", Bool) ] +type family SimpleFieldTypes (r :: Row Type) :: [(Symbol, Type)] + +{------------------------------------------------------------------------------- + AllFields +-------------------------------------------------------------------------------} + +-- | Require that @c x@ holds for every @(n := x)@ in @r@. +class AllFields (r :: Row k) (c :: k -> Constraint) where + -- | Vector of dictionaries, in row order + fieldDicts :: DictAllFields k r c + fieldDicts = undefined + +type DictAllFields k (r :: Row k) (c :: k -> Constraint) = + Tagged r (SmallArray (DictAny c)) + +data DictAny c where + DictAny :: c Any => DictAny c + +evidenceAllFields :: forall k r c. [DictAny c] -> DictAllFields k r c +evidenceAllFields = Tagged . smallArrayFromList + +instance {-# OVERLAPPING #-} + (KnownFields r, Show a) + => AllFields r (Compose Show (K a)) where + fieldDicts = Tagged $ + smallArrayFromList $ map (const DictAny) $ proxy fieldNames (Proxy @r) + +instance {-# OVERLAPPING #-} + (KnownFields r, Eq a) + => AllFields r (Compose Eq (K a)) where + fieldDicts = Tagged $ + smallArrayFromList $ map (const DictAny) $ proxy fieldNames (Proxy @r) + +instance {-# OVERLAPPING #-} + (KnownFields r, Ord a) + => AllFields r (Compose Ord (K a)) where + fieldDicts = Tagged $ + smallArrayFromList $ map (const DictAny) $ proxy fieldNames (Proxy @r) + +fieldMetadata :: forall k (r :: Row k) proxy. + KnownFields r + => proxy r -> [FieldMetadata Any] +fieldMetadata _ = map aux $ proxy fieldNames (Proxy @r) + where + -- @large-anon@ only supports records with strict fields. + aux :: String -> FieldMetadata Any + aux name = case someSymbolVal name of + SomeSymbol p -> FieldMetadata p FieldStrict + +{------------------------------------------------------------------------------- + Merging records +-------------------------------------------------------------------------------} + +-- | Merge two rows +-- +-- See 'Data.Record.Anon.Advanced.merge' for detailed discussion. +type family Merge :: Row k -> Row k -> Row k + +{------------------------------------------------------------------------------- + KnownHash + + This class is exported /with/ its body from the library (no reason not to). + so we avoid using 'DictKnownHash' in the class definition. +-------------------------------------------------------------------------------} + +-- | Symbol (type-level string) with compile-time computed hash +-- +-- Instances are computed on the fly by the plugin. +class KnownHash (s :: Symbol) where + hashVal :: forall proxy. proxy s -> Int + +type DictKnownHash (s :: Symbol) = + forall proxy. proxy s -> Int + +evidenceKnownHash :: forall (s :: Symbol). + Int -> DictKnownHash s +evidenceKnownHash x _ = x + +{------------------------------------------------------------------------------- + Subrecord +-------------------------------------------------------------------------------} + +-- | Subrecords +-- +-- If @SubRow r r'@ holds, we can project (or create a lens) @r@ to @r'@. +-- See 'Data.Record.Anon.Advanced.project' for detailed discussion. +class SubRow (r :: Row k) (r' :: Row k) where + projectIndices :: DictSubRow k r r' + projectIndices = undefined + +-- | In order of the fields in the /target/ record, the index in the /source/ +type DictSubRow k (r :: Row k) (r' :: Row k) = + Tagged '(r, r') (StrictArray Int) + +evidenceSubRow :: forall k r r'. [Int] -> DictSubRow k r r' +evidenceSubRow = Tagged . Strict.fromList + +{------------------------------------------------------------------------------- + Utility +-------------------------------------------------------------------------------} + +noInlineUnsafeCo :: a -> b +{-# NOINLINE noInlineUnsafeCo #-} +noInlineUnsafeCo = unsafeCoerce diff --git a/src/Data/Record/Anon/Simple.hs b/src/Data/Record/Anon/Simple.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Anon/Simple.hs @@ -0,0 +1,278 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE RankNTypes #-} + +-- | Simple interface (without a functor argument) +-- +-- See "Data.Record.Anon.Advanced" for the advanced interface. +-- You will probably also want to import "Data.Record.Anon". +-- +-- Intended for qualified import. +-- +-- > import Data.Record.Anon +-- > import Data.Record.Anon.Simple (Record) +-- > import qualified Data.Record.Anon.Simple as Anon +module Data.Record.Anon.Simple ( + Record + -- * Construction + , empty + , insert + , insertA + , applyPending + -- * Field access + , get + , set + -- * Changing rows + , project + , inject + , lens + , merge + -- * Interop with the advanced API + , toAdvanced + , fromAdvanced + , sequenceA + -- * Experimental integration with @typelet@ + -- + -- | + -- The @typelet@ plugin provides support for type sharing. These functions + -- can be used to construct records that result in ghc core that is truly + -- linear in size. + , letRecordT + , letInsertAs + ) where + +import Prelude hiding (sequenceA) + +import TypeLet + +import Data.Record.Anon + +import Data.Record.Anon.Internal.Simple (Record) +import qualified Data.Record.Anon.Internal.Simple as S +import qualified Data.Record.Anon.Internal.Advanced as A + +-- $setup +-- >>> :set -XDataKinds +-- >>> :set -XOverloadedLabels +-- >>> :set -XTypeOperators +-- >>> :set -fplugin=TypeLet -fplugin=Data.Record.Anon.Plugin +-- >>> :set -dppr-cols=200 +-- >>> import TypeLet +-- >>> import Data.Record.Anon + +{------------------------------------------------------------------------------- + Construction + + See discussion in Data.Record.Anon.Advanced for why we don't simply re-export. +-------------------------------------------------------------------------------} + +-- | Empty record +empty :: Record '[] +empty = S.empty + +-- | Insert new field +-- +-- >>> :{ +-- example :: Record [ "a" := Bool, "b" := Int ] +-- example = +-- insert #a True +-- $ insert #b 1 +-- $ empty +-- :} +-- +-- Instead of using 'insert' and 'empty', you can also write this as +-- +-- > example = ANON { +-- > a = True +-- > , b = 1 +-- > } +insert :: Field n -> a -> Record r -> Record (n := a : r) +insert = S.insert + +-- | Applicative insert +-- +-- This is a simple wrapper around 'insert', but can be quite useful when +-- constructing records. Consider code like +-- +-- >>> :{ +-- example :: Applicative m => m a -> m b -> m (a, b) +-- example ma mb = (,) <$> ma <*> mb +-- :} +-- +-- We cannot really extend this to the world of named records, but we /can/ +-- do something comparable using anonymous records: +-- +-- >>> :{ +-- example :: Applicative m => m a -> m b -> m (Record [ "a" := a, "b" := b ]) +-- example ma mb = +-- insertA #a ma +-- $ insertA #b mb +-- $ pure empty +-- :} +-- +-- However, it may be more convenient to use the advanced API for this. +-- See 'Data.Record.Anon.Advanced.insertA'. +insertA :: + Applicative m + => Field n -> m a -> m (Record r) -> m (Record (n := a : r)) +insertA = S.insertA + +-- | Apply all pending changes to the record +-- +-- Updates to a record are stored in a hashtable. As this hashtable grows, +-- record field access and update will become more expensive. Applying the +-- updates, resulting in a flat vector, is an @O(n)@ operation. This will happen +-- automatically whenever another @O(n)@ operation is applied (for example, +-- mapping a function over the record). However, occassionally it is useful to +-- explicitly apply these changes, for example after constructing a record or +-- updating a lot of fields. +applyPending :: Record r -> Record r +applyPending = S.applyPending + +{------------------------------------------------------------------------------- + Field access +-------------------------------------------------------------------------------} + +-- | Get field from the record +-- +-- This is just a wrapper around 'getField'. +-- +-- >>> :{ +-- example :: Record [ "a" := Bool, "b" := Int ] -> Bool +-- example r = get #a r +-- :} +-- +-- If using @record-dot-preprocessor@, you can also write this example as +-- +-- > example r = r.a +-- +-- See 'Data.Record.Anon.Advanced.get' for additional discussion. +get :: RowHasField n r a => Field n -> Record r -> a +get = S.get + +-- | Update field in the record +-- +-- This is just a wrapper around 'setField'. +-- +-- >>> :{ +-- example :: +-- Record [ "a" := Bool, "b" := Int ] +-- -> Record [ "a" := Bool, "b" := Int ] +-- example r = set #a False r +-- :} +-- +-- If using @record-dot-preprocessor@, can also write this example as +-- +-- > example r = r{a = False} +set :: RowHasField n r a => Field n -> a -> Record r -> Record r +set = S.set + +{------------------------------------------------------------------------------- + Changing rows +-------------------------------------------------------------------------------} + +-- | Project from one record to another +-- +-- Both the source record and the target record must be fully known. +-- +-- The target record can omit fields from the source record, as well as +-- rearrange them: +-- +-- >>> :{ +-- example :: +-- Record [ "a" := Char, "b" := Int, "c" := Bool ] +-- -> Record [ "c" := Bool, "a" := Char ] +-- example = project +-- :} +-- +-- As we saw in 'merge', 'project' can also flatten 'Merge'd rows. +-- See 'Data.Record.Anon.Advanced.project' for additional discussion. +project :: SubRow r r' => Record r -> Record r' +project = S.project + +-- | Inject smaller record into larger record +-- +-- This is just the 'lens' setter. +inject :: SubRow r r' => Record r' -> Record r -> Record r +inject = S.inject + +-- | Lens from one record to another +-- +-- See 'project' for examples ('project' is just the lens getter, without the +-- setter). +lens :: SubRow r r' => Record r -> (Record r', Record r' -> Record r) +lens = S.lens + +-- | Merge two records +-- +-- The 'Merge' type family does not reduce: +-- +-- >>> :{ +-- example :: Record (Merge '[ "a" := Bool ] '[]) +-- example = merge (insert #a True empty) empty +-- :} +-- +-- If you want to flatten the row after merging, you can use 'project': +-- +-- >>> :{ +-- example :: Record '[ "a" := Bool ] +-- example = project $ merge (insert #a True empty) empty +-- :} +-- +-- See 'Data.Record.Anon.Advanced.merge' for additional discussion. +merge :: Record r -> Record r' -> Record (Merge r r') +merge = S.merge + +{------------------------------------------------------------------------------- + Interop with the advanced API +-------------------------------------------------------------------------------} + +-- | Move from the simple to the advanced interface +-- +-- This is an @O(1)@ operation. +toAdvanced :: Record r -> A.Record I r +toAdvanced = S.toAdvanced + +-- | Move from the advanced to the simple interface +-- +-- This is an @O(1)@ operation. +fromAdvanced :: A.Record I r -> Record r +fromAdvanced = S.fromAdvanced + +-- | Sequence all actions +sequenceA :: Applicative m => A.Record m r -> m (Record r) +sequenceA = S.sequenceA + +{------------------------------------------------------------------------------- + Experimental integration with @typelet@ +-------------------------------------------------------------------------------} + +-- | Introduce type variable for a row +-- +-- This can be used in conjunction with 'letInsertAs': +-- +-- >>> :{ +-- example :: Record '[ "a" := Int, "b" := Char, "c" := Bool ] +-- example = letRecordT $ \p -> castEqual $ +-- letInsertAs p #c True empty $ \xs02 -> +-- letInsertAs p #b 'X' xs02 $ \xs01 -> +-- letInsertAs p #a 1 xs01 $ \xs00 -> +-- castEqual xs00 +-- :} +letRecordT :: forall r. + (forall r'. Let r' r => Proxy r' -> Record r) + -> Record r +letRecordT f = S.letRecordT f + +-- | Insert field into a record and introduce type variable for the result +letInsertAs :: forall r r' n a. + Proxy r -- ^ Type of the record we are constructing + -> Field n -- ^ New field to be inserted + -> a -- ^ Value of the new field + -> Record r' -- ^ Record constructed so far + -> (forall r''. Let r'' (n := a : r') => Record r'' -> Record r) + -- ^ Assign type variable to new partial record, and continue + -> Record r +letInsertAs p n x r f = S.letInsertAs p n x r f + diff --git a/test/Test/Infra/Discovery.hs b/test/Test/Infra/Discovery.hs new file mode 100644 --- /dev/null +++ b/test/Test/Infra/Discovery.hs @@ -0,0 +1,213 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +module Test.Infra.Discovery ( + -- * Intersect rows + InBothRows(..) + , inLeftRow + , inRightRow + , intersectRows + -- * Check for projection + , NotSubRow + , checkIsSubRow + , maybeProject + -- * Compute intersection + , Intersection(..) + , intersect + -- * Auxiliary + , catMaybeF + , pairFst + , pairSnd + ) where + +import Data.Kind +import Data.Maybe (catMaybes) +import Data.Typeable +import GHC.TypeLits + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record, InRow(InRow)) +import qualified Data.Record.Anon.Advanced as Anon +import Control.Monad.State + +{------------------------------------------------------------------------------- + Intersect rows + + NOTE: A constraint @SubRow r r@ is not completely trivial: it means that + there are no shadowed fields. +-------------------------------------------------------------------------------} + +data InBothRows (r1 :: Row k) (r2 :: Row k) (a :: k) where + InBothRows :: forall k (n :: Symbol) (r1 :: Row k) (r2 :: Row k) (a :: k). + ( KnownSymbol n + , RowHasField n r1 a + , RowHasField n r2 a + ) + => Proxy n -> InBothRows r1 r2 a + +inLeftRow :: InBothRows r1 r2 a -> InRow r1 a +inLeftRow (InBothRows n) = InRow n + +inRightRow :: InBothRows r1 r2 a -> InRow r2 a +inRightRow (InBothRows n) = InRow n + +intersectRows :: forall k (r1 :: Row k) (r2 :: Row k) proxy proxy'. + ( KnownFields r1 + , KnownFields r2 + , SubRow r1 r1 + , SubRow r2 r2 + , AllFields r1 Typeable + , AllFields r2 Typeable + ) + => proxy r1 -> proxy' r2 -> Record (Maybe :.: InBothRows r1 r2) r2 +intersectRows _ _ = + go Anon.reifySubRow Anon.reifySubRow + where + go :: Record (InRow r1) r1 + -> Record (InRow r2) r2 + -> Record (Maybe :.: InBothRows r1 r2) r2 + go r1 r2 = Anon.cmap (Proxy @Typeable) (findField r1) r2 + + findField :: forall x2. + Typeable x2 + => Record (InRow r1) r1 -> InRow r2 x2 -> (Maybe :.: InBothRows r1 r2) x2 + findField r1 f = Comp $ + findMatch . catMaybes $ + Anon.collapse $ Anon.cmap (Proxy @Typeable) (K . checkIsMatch f) r1 + + checkIsMatch :: forall x1 x2. + (Typeable x1, Typeable x2) + => InRow r2 x2 -> InRow r1 x1 -> Maybe (InBothRows r1 r2 x2) + checkIsMatch (InRow x2) (InRow x1) = do + Refl <- sameSymbol x1 x2 + Refl <- eqT :: Maybe (x1 :~: x2) + return $ InBothRows x1 + + findMatch :: [a] -> Maybe a + findMatch [] = Nothing + findMatch [a] = Just a + findMatch _ = error "intersectRows: error: multiple matches" + +{------------------------------------------------------------------------------- + Check for projection +-------------------------------------------------------------------------------} + +-- | Fields that are missing or have the wrong type +-- +-- TODO: Ideally we should distinguish between type errors and missing fields. +type NotSubRow = [String] + +checkIsSubRow :: forall k (r1 :: Row k) (r2 :: Row k) proxy proxy'. + ( KnownFields r1 + , KnownFields r2 + , SubRow r1 r1 + , SubRow r2 r2 + , AllFields r1 Typeable + , AllFields r2 Typeable + ) + => proxy r1 -> proxy' r2 -> Either NotSubRow (Reflected (SubRow r1 r2)) +checkIsSubRow p1 p2 = + uncurry postprocess . flip runState [] . Anon.sequenceA $ + Anon.zipWith + checkInLeft + (intersectRows p1 p2) + (Anon.reifyKnownFields (Proxy @r2)) + where + checkInLeft :: + (Maybe :.: InBothRows r1 r2) x + -> K String x + -> (State [String] :.: Maybe :.: InRow r1) x + checkInLeft (Comp Nothing) (K name) = Comp $ state $ \missing -> + (Comp Nothing, name : missing) + checkInLeft (Comp (Just inBoth)) _ = Comp $ state $ \missing -> + (Comp (Just (inLeftRow inBoth)), missing) + + postprocess :: + Record (Maybe :.: InRow r1) r2 + -> [String] + -> Either NotSubRow (Reflected (SubRow r1 r2)) + postprocess matched missing = + maybe (Left missing) (Right . Anon.reflectSubRow) $ + Anon.sequenceA matched + +maybeProject :: forall k (f :: k -> Type) (r1 :: Row k) (r2 :: Row k) proxy. + ( KnownFields r1 + , KnownFields r2 + , SubRow r1 r1 + , SubRow r2 r2 + , AllFields r1 Typeable + , AllFields r2 Typeable + ) + => Record f r1 -> proxy r2 -> Either NotSubRow (Record f r2) +maybeProject r1 p = aux <$> checkIsSubRow r1 p + where + aux :: Reflected (SubRow r1 r2) -> Record f r2 + aux Reflected = Anon.project r1 + +{------------------------------------------------------------------------------- + Compute intersection +-------------------------------------------------------------------------------} + +data Intersection (r1 :: Row k) (r2 :: Row k) where + Intersection :: forall k (r1 :: Row k) (r2 :: Row k) (ri :: Row k). + ( KnownFields ri + , SubRow r1 ri + , SubRow r2 ri + ) + => Proxy ri -> Intersection r1 r2 + +intersect :: forall k (r1 :: Row k) (r2 :: Row k) proxy proxy'. + ( KnownFields r1 + , KnownFields r2 + , SubRow r1 r1 + , SubRow r2 r2 + , AllFields r1 Typeable + , AllFields r2 Typeable + ) + => proxy r1 -> proxy' r2 -> Intersection r1 r2 +intersect p1 p2 = + (\(Anon.SomeRecord r) -> aux $ Anon.map pairSnd r) $ + catMaybeF (intersectRows p1 p2) + where + aux :: forall ri. + KnownFields ri + => Record (InBothRows r1 r2) ri -> Intersection r1 r2 + aux r = + case (project1, project2) of + (Reflected, Reflected) -> Intersection (Proxy @ri) + where + project1 :: Reflected (SubRow r1 ri) + project1 = Anon.reflectSubRow $ Anon.map inLeftRow r + + project2 :: Reflected (SubRow r2 ri) + project2 = Anon.reflectSubRow $ Anon.map inRightRow r + +{------------------------------------------------------------------------------- + Auxiliary +-------------------------------------------------------------------------------} + +catMaybeF :: KnownFields r => Record (Maybe :.: f) r -> Anon.SomeRecord f +catMaybeF = + Anon.someRecord + . catMaybes + . map distrib + . Anon.toList + . Anon.map (K . Some) + where + distrib :: (String, Some (Maybe :.: f)) -> Maybe (String, Some f) + distrib (_, Some (Comp Nothing)) = Nothing + distrib (n, Some (Comp (Just fx))) = Just (n, Some fx) + +pairFst :: Product f g x -> f x +pairFst (Pair fx _) = fx + +pairSnd :: Product f g x -> g x +pairSnd (Pair _ gx) = gx + + diff --git a/test/Test/Infra/DynRecord.hs b/test/Test/Infra/DynRecord.hs new file mode 100644 --- /dev/null +++ b/test/Test/Infra/DynRecord.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE GADTs #-} + +-- | Simple dynamic record type, for testing purposes only +module Test.Infra.DynRecord ( + -- * Definition + DynRecord(..) + , Value(..) + -- * Unparsing + , ToValue(..) + , toValues + ) where + +import Data.Kind + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) +import qualified Data.Record.Anon.Advanced as Anon + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +data DynRecord = DynRecord [(String, Value)] + deriving (Show, Eq) + +data Value = + VI Int + | VB Bool + | VC Char + deriving (Show, Eq) + +{------------------------------------------------------------------------------- + Unparsing +-------------------------------------------------------------------------------} + +class ToValue (f :: k -> Type) (a :: k) where + toValue :: f a -> Value + +instance ToValue I Int where toValue = VI . unI +instance ToValue I Bool where toValue = VB . unI +instance ToValue I Char where toValue = VC . unI + +toValues :: forall k (f :: k -> Type) (r :: Row k). + AllFields r (ToValue f) + => Record f r + -> Record (K Value) r +toValues = Anon.cmap (Proxy @(ToValue f)) aux + where + aux :: ToValue f x => f x -> K Value x + aux = K . toValue diff --git a/test/Test/Infra/DynRecord/Advanced.hs b/test/Test/Infra/DynRecord/Advanced.hs new file mode 100644 --- /dev/null +++ b/test/Test/Infra/DynRecord/Advanced.hs @@ -0,0 +1,150 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} + +-- | 'DynRecord' interop with the advanced record API. +-- +-- Intended for qualified import +-- +-- > import qualified Test.Infra.DynRecord.Advanced as Dyn +module Test.Infra.DynRecord.Advanced ( + -- * Type inference + ValidField(..) + , IsValue(..) + , SomeRecord(..) + , inferType + -- * Lens + , toLens + , toRecord + ) where + +import Data.Bifunctor +import Data.Kind +import Data.Record.Generic +import Data.SOP.Constraint +import Data.Typeable + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) +import qualified Data.Record.Anon.Advanced as Anon + +import Test.Infra.Discovery +import Test.Infra.DynRecord + +{------------------------------------------------------------------------------- + Type inference +-------------------------------------------------------------------------------} + +data ValidField (f :: k -> Type) (x :: k) where + ValidField :: + ( Typeable x + , Show (f x) + , Eq (f x) + , ToValue f x + ) + => f x -> ValidField f x + +class IsValue f where + isValue :: Value -> Some (ValidField f) + +data SomeRecord (f :: k -> Type) where + SomeRecord :: forall k (f :: k -> Type) (r :: Row k). + ( KnownFields r + , SubRow r r + , AllFields r Typeable + , AllFields r (Compose Show f) + , AllFields r (Compose Eq f) + , AllFields r (ToValue f) + ) + => Record f r -> SomeRecord f + +inferType :: forall k (f :: k -> Type). IsValue f => DynRecord -> SomeRecord f +inferType (DynRecord r) = + case Anon.someRecord (map (second isValue) r) of + Anon.SomeRecord record -> + case Anon.reflectSubRow (Anon.map pairFst record) of + Reflected -> withSomeRecord (Anon.map pairSnd record) + where + withSomeRecord :: + ( KnownFields r + , SubRow r r + ) + => Record (ValidField f) r -> SomeRecord f + withSomeRecord record = + case ( Anon.reflectAllFields (Anon.map dictTypeable record) + , Anon.reflectAllFields (Anon.map dictShow record) + , Anon.reflectAllFields (Anon.map dictEq record) + , Anon.reflectAllFields (Anon.map dictToValue record) + ) of + (Reflected, Reflected, Reflected, Reflected) -> + SomeRecord (Anon.map fieldValue record) + + fieldValue :: ValidField f x -> f x + fieldValue (ValidField value) = value + + dictTypeable :: ValidField f x -> Dict Typeable x + dictShow :: ValidField f x -> Dict (Compose Show f) x + dictEq :: ValidField f x -> Dict (Compose Eq f) x + dictToValue :: ValidField f x -> Dict (ToValue f) x + + dictTypeable (ValidField _) = Dict + dictShow (ValidField _) = Dict + dictEq (ValidField _) = Dict + dictToValue (ValidField _) = Dict + +{------------------------------------------------------------------------------- + Projection to known row +-------------------------------------------------------------------------------} + +-- | Lens to record over some known row @r@ +toLens :: forall k (f :: k -> Type) (r :: Row k) proxy. + ( IsValue f + , KnownFields r + , SubRow r r + , AllFields r Typeable + ) + => proxy r + -> DynRecord + -> Either NotSubRow (Record f r, Record f r -> DynRecord) +toLens p = \r -> + -- In order to be able to check if we can project to the known row @r@, + -- we must first to type inference on the @DynRecord@. /If/ this succeeds, + -- we know the types line up, and there can be no further type errors + -- (there is no need for a separate parsing step). + case inferType r of + SomeRecord r' -> + fmap (withSomeRecord r') $ checkIsSubRow r' p + where + -- @r'@ is the row inferred for the 'DynRecord' + withSomeRecord :: forall (r' :: Row k). + ( KnownFields r' + , AllFields r' (ToValue f) + ) + => Record f r' + -> Reflected (SubRow r' r) + -> (Record f r, Record f r -> DynRecord) + withSomeRecord r Reflected = ( + getter + , DynRecord . Anon.toList . toValues . setter + ) + where + getter :: Record f r + setter :: Record f r -> Record f r' + (getter, setter) = Anon.lens r + +toRecord :: forall k (r :: Row k) (f :: k -> *) proxy. + ( IsValue f + , KnownFields r + , SubRow r r + , AllFields r Typeable + ) + => proxy r + -> DynRecord + -> Either NotSubRow (Record f r) +toRecord p = fmap fst . toLens p diff --git a/test/Test/Infra/DynRecord/Simple.hs b/test/Test/Infra/DynRecord/Simple.hs new file mode 100644 --- /dev/null +++ b/test/Test/Infra/DynRecord/Simple.hs @@ -0,0 +1,152 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} + +-- | 'DynRecord' interop with the simple record API. +-- +-- Intended for qualified import. +-- +-- > import qualified Test.Infra.DynRecord.Simple as Dyn +module Test.Infra.DynRecord.Simple ( + -- * Type inference + ValidField(..) + , SomeRecord(..) + , inferType + -- * Lens + , toLens + , toRecord + ) where + +import Data.Bifunctor +import Data.Kind +import Data.Typeable + +import Data.Record.Anon +import Data.Record.Anon.Simple (Record) + +import qualified Data.Record.Anon.Advanced as A +import qualified Data.Record.Anon.Simple as S + +import Test.Infra.Discovery +import Test.Infra.DynRecord + +{------------------------------------------------------------------------------- + Type inference + + NOTE: This canont be defined in terms of A.Dyn.inferType, because if we did, + we would get in scope @AllFields r (Compose Show I)@, from which we cannot + deduce @AllFields r Show@: @Show (I x)@ does not imply @Show x@. We could + potentially solve this using a Beam-style HKD definition, but it's not that + relevant for this test case. +-------------------------------------------------------------------------------} + +data ValidField x where + ValidField :: + ( Typeable x + , Show x + , Eq x + , ToValue I x + ) + => x -> ValidField x + +data SomeRecord where + SomeRecord :: forall (r :: Row Type). + ( KnownFields r + , SubRow r r + , AllFields r Typeable + , AllFields r Show + , AllFields r Eq + , AllFields r (ToValue I) + ) + => Record r -> SomeRecord + +inferType :: DynRecord -> SomeRecord +inferType (DynRecord r) = + case A.someRecord $ map (second mkField) r of + A.SomeRecord record -> + case A.reflectSubRow (A.map pairFst record) of + Reflected -> withSomeRecord (A.map pairSnd record) + where + withSomeRecord :: + ( KnownFields r + , SubRow r r + ) + => A.Record ValidField r -> SomeRecord + withSomeRecord record = + case ( A.reflectAllFields (A.map dictTypeable record) + , A.reflectAllFields (A.map dictShow record) + , A.reflectAllFields (A.map dictEq record) + , A.reflectAllFields (A.map dictToValue record) + ) of + (Reflected, Reflected, Reflected, Reflected) -> + SomeRecord (S.fromAdvanced $ A.map fieldValue record) + + fieldValue :: ValidField x -> I x + fieldValue (ValidField value) = I value + + dictTypeable :: ValidField x -> Dict Typeable x + dictShow :: ValidField x -> Dict Show x + dictEq :: ValidField x -> Dict Eq x + dictToValue :: ValidField x -> Dict (ToValue I) x + + dictTypeable (ValidField _) = Dict + dictShow (ValidField _) = Dict + dictEq (ValidField _) = Dict + dictToValue (ValidField _) = Dict + + mkField :: Value -> Some ValidField + mkField (VI x) = Some $ ValidField x + mkField (VB x) = Some $ ValidField x + mkField (VC x) = Some $ ValidField x + +{------------------------------------------------------------------------------- + Projection to known row +-------------------------------------------------------------------------------} + +-- | Lens to record over some known row @r@ +toLens :: forall (r :: Row Type) proxy. + ( KnownFields r + , SubRow r r + , AllFields r Typeable + ) + => proxy r + -> DynRecord + -> Either NotSubRow (Record r, Record r -> DynRecord) +toLens p = \r -> + -- In order to be able to check if we can project to the known row @r@, + -- we must first to type inference on the @DynRecord@. /If/ this succeeds, + -- we know the types line up, and there can be no further type errors + -- (there is no need for a separate parsing step). + case inferType r of + SomeRecord r' -> + fmap (withSomeRecord r') $ checkIsSubRow r' p + where + -- @r'@ is the row inferred for the 'DynRecord' + withSomeRecord :: forall (r' :: Row Type). + ( KnownFields r' + , AllFields r' (ToValue I) + ) + => Record r' + -> Reflected (SubRow r' r) + -> (Record r, Record r -> DynRecord) + withSomeRecord r Reflected = ( + getter + , DynRecord . A.toList . toValues . S.toAdvanced . setter + ) + where + getter :: Record r + setter :: Record r -> Record r' + (getter, setter) = S.lens r + +toRecord :: forall (r :: Row Type) proxy. + ( KnownFields r + , SubRow r r + , AllFields r Typeable + ) + => proxy r + -> DynRecord + -> Either NotSubRow (Record r) +toRecord p = fmap fst . toLens p diff --git a/test/Test/Infra/Generics.hs b/test/Test/Infra/Generics.hs new file mode 100644 --- /dev/null +++ b/test/Test/Infra/Generics.hs @@ -0,0 +1,72 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + +-- | Additional generic functions used in tests +module Test.Infra.Generics ( + describeRecord + , debugFieldTypes + ) where + +import Data.Kind +import Data.List (intercalate) +import Data.Record.Generic +import Data.SOP +import Data.Typeable +import GHC.TypeLits + +import qualified Data.Record.Generic.Rep as Rep + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) + +-- | Show type of every field in the record +describeRecord :: forall (a :: Type). + (Generic a, Constraints a Typeable) + => Proxy a + -> String +describeRecord p = + combine + . Rep.collapse + . Rep.cmap (Proxy @Typeable) aux + $ names + where + names :: Rep (K String) a + names = recordFieldNames $ metadata p + + -- @x@ here will be of the form @f x'@, for some @x'@, and we have a + -- constraint @Typeable (f x')@ in scope. We therefore do not need to + -- manually apply @f@ here. + aux :: forall x. Typeable x => K String x -> K String x + aux (K name) = K $ name ++ " :: " ++ show (typeRep (Proxy @x)) + + combine :: [String] -> String + combine fs = concat [ + "Record {" + , intercalate ", " fs + , "}" + ] + +-- | Like 'describeRecord', but exclusively using type-level information. +-- +-- WARNING: The @All@ constraint will lead to quadratic code. This is for +-- debugging only. +debugFieldTypes :: forall f r. + All IsField (FieldTypes f r) + => Proxy (Record f r) -> String +debugFieldTypes _ = + (\str -> "[" ++ str ++ "]") . intercalate "," . hcollapse $ + aux (shape :: Shape (FieldTypes f r)) + where + aux :: forall fs. All IsField fs => Shape fs -> NP (K String) fs + aux ShapeNil = Nil + aux (ShapeCons s) = name :* aux s + + name :: forall n a. KnownSymbol n => K String '(n, a) + name = K (symbolVal (Proxy @n)) + + + diff --git a/test/Test/Infra/MarkStrictness.hs b/test/Test/Infra/MarkStrictness.hs new file mode 100644 --- /dev/null +++ b/test/Test/Infra/MarkStrictness.hs @@ -0,0 +1,66 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +-- | Proof of concept: mark strictness at the type-level +-- +-- This is an illustration of how to take advantage of the polykinded nature of +-- the advanced 'Record' interface. +module Test.Infra.MarkStrictness ( + -- * Definition + MarkStrictness(..) + , Boxed(..) + ) where + +import Data.Kind +import Data.SOP.BasicFunctors + +import Data.Record.Anon + +import Test.Infra.DynRecord +import Test.Infra.DynRecord.Advanced + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +data MarkStrictness a = Strict a | Lazy a + +data Boxed :: MarkStrictness Type -> Type where + BoxStrict :: !a -> Boxed (Strict a) + BoxLazy :: a -> Boxed (Lazy a) + +{------------------------------------------------------------------------------- + Standard instances +-------------------------------------------------------------------------------} + +instance Show a => Show (Boxed (Strict a)) where + show (BoxStrict x) = show x +instance Show a => Show (Boxed (Lazy a)) where + show (BoxLazy x) = show x + +instance Eq a => Eq (Boxed (Strict a)) where + BoxStrict x == BoxStrict y = x == y +instance Eq a => Eq (Boxed (Lazy a)) where + BoxLazy x == BoxLazy y = x == y + +{------------------------------------------------------------------------------- + Interop with 'DynRecord' +-------------------------------------------------------------------------------} + +instance ToValue I a => ToValue Boxed (Lazy a) where + toValue (BoxLazy x) = toValue (I x) +instance ToValue I a => ToValue Boxed (Strict a) where + toValue (BoxStrict x) = toValue (I x) + +-- | Type inference for a value +-- +-- Just for the example, we infer all 'Int' fields are strict and all other +-- fields as lazy. +instance IsValue Boxed where + isValue (VI x) = Some $ ValidField $ BoxStrict x + isValue (VB x) = Some $ ValidField $ BoxLazy x + isValue (VC x) = Some $ ValidField $ BoxLazy x diff --git a/test/Test/Prop/Record/Combinators/Constrained.hs b/test/Test/Prop/Record/Combinators/Constrained.hs new file mode 100644 --- /dev/null +++ b/test/Test/Prop/Record/Combinators/Constrained.hs @@ -0,0 +1,97 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} + +module Test.Prop.Record.Combinators.Constrained (tests) where + +import Control.Monad.ST +import Data.Proxy +import Data.Record.Generic.LowerBound +import Data.SOP.BasicFunctors +import Data.STRef + +import qualified Data.Record.Anon.Advanced as Anon + +import Test.Tasty +import Test.Tasty.QuickCheck + +import Test.Prop.Record.Model.Orphans () +import Test.Prop.Record.Model.Generator + +import qualified Test.Prop.Record.Model as Modl + +tests :: TestTree +tests = testGroup "Test.Prop.Record.Combinators.Constrained" [ + testProperty "cpure" test_cpure + , testProperty "cmap" test_cmap + , testProperty "cmapM" test_cmapM + , testProperty "czipWith" test_czipWith + , testProperty "czipWithM" test_czipWithM + ] + +{------------------------------------------------------------------------------- + Tests proper +-------------------------------------------------------------------------------} + +test_cpure :: SomeFields -> Property +test_cpure sf = + someModlRecord sf (\mf -> Modl.cpure p mf (I lowerBound)) + === someAnonRecord p sf ( Anon.cpure p (I lowerBound)) + where + p = Proxy @LowerBound + +test_cmap :: SomeRecord I -> Property +test_cmap r = + onModlRecord p (Modl.cmap p f) r + === onAnonRecord p (Anon.cmap p f) r + where + p = Proxy @Show + + f :: Show a => I a -> K String a + f (I x) = K (show x) + +test_cmapM :: SomeRecord I -> Property +test_cmapM r = + (run $ \ref -> onModlRecordM p (Modl.cmapM p (f ref)) r) + === (run $ \ref -> onAnonRecordM p (Anon.cmapM p (f ref)) r) + where + p = Proxy @Show + + run :: (forall s. STRef s Int -> ST s a) -> (a, Int) + run st = runST $ do + ref <- newSTRef 0 + a <- st ref + (a,) <$> readSTRef ref + + f :: Show a => STRef s Int -> I a -> ST s (K String a) + f ref (I x) = do + modifySTRef ref succ + return (K $ show x) + +test_czipWith :: SomeRecordPair I I -> Property +test_czipWith r = + onModlRecordPair p (Modl.czipWith p f) r + === onAnonRecordPair p (Anon.czipWith p f) r + where + p = Proxy @Show + + f :: Show x => I x -> I x -> K String x + f (I x) (I y) = K (show x ++ show y) + +test_czipWithM :: SomeRecordPair I I -> Property +test_czipWithM r = + run (\ref -> onModlRecordPairM p (Modl.czipWithM p (f ref)) r) + === run (\ref -> onAnonRecordPairM p (Anon.czipWithM p (f ref)) r) + where + p = Proxy @Show + + run :: (forall s. STRef s Bool -> ST s a) -> a + run st = runST $ newSTRef False >>= st + + -- Function that uses some state from processing the /previous/ element + -- (As an example of an order dependency) + f :: Show x => STRef s Bool -> I x -> I x -> ST s (I x) + f ref (I x) (I y) = do + b <- readSTRef ref + writeSTRef ref $ even (length (show x)) + return . I $ if b then x else y diff --git a/test/Test/Prop/Record/Combinators/Simple.hs b/test/Test/Prop/Record/Combinators/Simple.hs new file mode 100644 --- /dev/null +++ b/test/Test/Prop/Record/Combinators/Simple.hs @@ -0,0 +1,143 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} + +module Test.Prop.Record.Combinators.Simple (tests) where + +import Control.Monad.State +import Data.Bifunctor +import Data.SOP + +import qualified Data.Record.Anon.Advanced as Anon + +import Test.Tasty +import Test.Tasty.QuickCheck + +import Test.Prop.Record.Model.Orphans () +import Test.Prop.Record.Model.Generator + +import qualified Test.Prop.Record.Model as Modl + +tests :: TestTree +tests = testGroup "Test.Prop.Record.Combinators.Simple" [ + testProperty "map" test_map + , testProperty "mapM" test_mapM + , testProperty "zip" test_zip + , testProperty "zipWith" test_zipWith + , testProperty "zipWithM" test_zipWithM + , testProperty "collapse" test_collapse + , testProperty "sequenceA" test_sequenceA + , testProperty "pure" test_pure + , testProperty "ap" test_ap + ] + +{------------------------------------------------------------------------------- + Auxiliary +-------------------------------------------------------------------------------} + +pTop :: Proxy Top +pTop = Proxy + +{------------------------------------------------------------------------------- + Tests proper +-------------------------------------------------------------------------------} + +test_map :: + SomeRecord (K Int) + -> Fun Int Int + -> Property +test_map r (applyFun -> f) = + onModlRecord pTop (Modl.map f') r + === onAnonRecord pTop (Anon.map f') r + where + f' :: K Int x -> K Int x + f' = mapKK f + +test_mapM :: + SomeRecord (K Int) + -> Fun (Int, Word) (Int, Word) + -> Property +test_mapM r (applyFun -> f) = + (run $ onModlRecordM pTop (Modl.mapM f') r) + === (run $ onAnonRecordM pTop (Anon.mapM f') r) + where + run :: State Word a -> a + run = flip evalState 0 + + f' :: K Int x -> State Word (K Int x) + f' (K x) = state $ \s -> first K $ f (x, s) + +test_zip :: + SomeRecordPair (K Int) (K Int) + -> Property +test_zip r = + onModlRecordPair pTop Modl.zip r + === onAnonRecordPair pTop Anon.zip r + +test_zipWith :: + SomeRecordPair (K Int) (K Int) + -> Fun (Int, Int) Int + -> Property +test_zipWith r (applyFun -> f) = + onModlRecordPair pTop (Modl.zipWith f') r + === onAnonRecordPair pTop (Anon.zipWith f') r + where + f' :: K Int x -> K Int x -> K Int x + f' (K x) (K y) = K $ f (x, y) + +test_zipWithM :: + SomeRecordPair (K Int) (K Int) + -> Fun (Int, Int, Word) (Int, Word) + -> Property +test_zipWithM r (applyFun -> f) = + (run $ onModlRecordPairM pTop (Modl.zipWithM f') r) + === (run $ onAnonRecordPairM pTop (Anon.zipWithM f') r) + where + run :: State Word a -> a + run = flip evalState 0 + + f' :: K Int x -> K Int x -> State Word (K Int x) + f' (K x) (K y) = state $ \s -> first K $ f (x, y, s) + +test_collapse :: + SomeRecord (K Int) + -> Property +test_collapse (SR mf r) = + Modl.collapse r + === Anon.collapse (Modl.toRecord mf r) + +test_sequenceA :: + SomeRecord (K Int) + -> Fun (Int, Word) (Int, Word) + -> Property +test_sequenceA r (applyFun -> f) = + (run $ onModlRecordM pTop Modl.sequenceA r') + === (run $ onAnonRecordM pTop Anon.sequenceA r') + where + run :: State Word a -> a + run = flip evalState 0 + + r' :: SomeRecord (State Word :.: K Int) + r' = onModlRecord pTop (Modl.map f') r + + f' :: K Int x -> (State Word :.: K Int) x + f' (K x) = Comp $ state $ \s -> first K $ f (x, s) + +test_pure :: SomeFields -> Property +test_pure sf = + someModlRecord sf (\mf -> Modl.pure mf (K True)) + === someAnonRecord pTop sf ( Anon.pure (K True)) + +test_ap :: + SomeRecordPair (K Int) (K Int) + -> Property +test_ap (SR2 mf rx ry) = + onModlRecordPair pTop Modl.ap r' + === onAnonRecordPair pTop Anon.ap r' + where + r' :: SomeRecordPair (K Int -.-> K Int) (K Int) + r' = SR2 mf (Modl.map f rx) ry + + f :: K Int x -> (K Int -.-> K Int) x + f (K x) = fn $ \(K y) -> K (x + y) diff --git a/test/Test/Prop/Record/Model.hs b/test/Test/Prop/Record/Model.hs new file mode 100644 --- /dev/null +++ b/test/Test/Prop/Record/Model.hs @@ -0,0 +1,269 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +-- | Model for records +-- +-- 'NP' from @sop-core@ forms the basis for our model, along with a choice of +-- shape (zero, one, or two fields). +-- +-- Intended for qualified import. +-- +-- > import Test.Prop.Model (ModelRecord(..), ModelFields(..)) +-- > import qualified Test.Prop.Model as Model +module Test.Prop.Record.Model ( + -- * Model proper + ModelFields(..) + , Types + , ModelRecord(..) + -- * Constraints + , ModelSatisfies + , satisfyAll + -- * Conversion to/from 'Record' + , toRecord + , fromRecord + , toRecordOfDicts + -- * Combinators + -- ** "Functor" + , map + , mapM + , cmap + , cmapM + -- ** Zipping + , zip + , zipWith + , zipWithM + , czipWith + , czipWithM + -- ** "Foldable" + , collapse + -- ** "Traversable" + , sequenceA + -- ** "Applicative" + , pure + , cpure + , ap + ) where + +import Prelude hiding (map, mapM, zip, zipWith, sequenceA, pure) + +import Data.Functor.Product +import Data.Kind +import Data.SOP (NP(..), SListI, All) + +import qualified Data.SOP as SOP + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) +import qualified Data.Record.Anon.Advanced as Anon + +{------------------------------------------------------------------------------- + Model proper +-------------------------------------------------------------------------------} + +-- | Shapes of the different kinds of records we want to test +-- +-- We want to test +-- +-- * Records of different size (0, 1, or 2 fields) +-- * Fields ordered alphabetically or not +-- (for tests where order of processing matters) +-- +-- TODO: Once we have support for /dropping/ fields, we should also add some +-- cases with duplicate fields here. We currently cannot, since we cannot define +-- 'fromRecord' for such records. +data ModelFields :: Row Type -> Type where + MF0 :: ModelFields '[ ] + MF1 :: ModelFields '[ "b" := Bool ] + MF2 :: ModelFields '[ "a" := Word, "b" := Bool ] + MF2' :: ModelFields '[ "b" := Word, "a" := Bool ] + +deriving instance Show (ModelFields xs) +deriving instance Eq (ModelFields xs) + +type family Types (fields :: Row k) :: [k] where + Types '[] = '[] + Types (_ := t : ts) = t ': Types ts + +data ModelRecord f r = MR (NP f (Types r)) + +deriving instance Show (NP f (Types r)) => Show (ModelRecord f r) +deriving instance Eq (NP f (Types r)) => Eq (ModelRecord f r) + +{------------------------------------------------------------------------------- + Constraints +-------------------------------------------------------------------------------} + +class (c Word, c Bool) => ModelSatisfies c +instance (c Word, c Bool) => ModelSatisfies c + +satisfyAll :: + ModelSatisfies c + => Proxy c + -> ModelFields r + -> (All c (Types r) => a) + -> a +satisfyAll _ MF0 k = k +satisfyAll _ MF1 k = k +satisfyAll _ MF2 k = k +satisfyAll _ MF2' k = k + +{------------------------------------------------------------------------------- + Conversion from/to model +-------------------------------------------------------------------------------} + +toRecord :: ModelFields xs -> ModelRecord f xs -> Record f xs +toRecord MF0 (MR Nil) = + Anon.empty +toRecord MF1 (MR (b :* Nil)) = + Anon.insert #b b + $ Anon.empty +toRecord MF2 (MR (a :* b :* Nil)) = + Anon.insert #a a + $ Anon.insert #b b + $ Anon.empty +toRecord MF2' (MR (b :* a :* Nil)) = + Anon.insert #b b + $ Anon.insert #a a + $ Anon.empty + +fromRecord :: ModelFields xs -> Record f xs -> ModelRecord f xs +fromRecord MF0 _r = + MR Nil +fromRecord MF1 r = + MR (Anon.get #b r :* Nil) +fromRecord MF2 r = + MR (Anon.get #a r :* Anon.get #b r :* Nil) +fromRecord MF2' r = + MR (Anon.get #b r :* Anon.get #a r :* Nil) + +toRecordOfDicts :: + ModelSatisfies c + => Proxy c + -> ModelFields r + -> (AllFields r c => a) + -> a +toRecordOfDicts _ MF0 k = k +toRecordOfDicts _ MF1 k = k +toRecordOfDicts _ MF2 k = k +toRecordOfDicts _ MF2' k = k + +{------------------------------------------------------------------------------- + Simple combinators +-------------------------------------------------------------------------------} + +map :: + SListI (Types r) + => (forall x. f x -> g x) -> ModelRecord f r -> ModelRecord g r +map f (MR np) = MR (SOP.hmap f np) + +mapM :: + SListI (Types r) + => Applicative m + => (forall x. f x -> m (g x)) + -> ModelRecord f r -> m (ModelRecord g r) +mapM f (MR np) = MR <$> SOP.htraverse' f np + +zip :: + SListI (Types r) + => ModelRecord f r -> ModelRecord g r -> ModelRecord (Product f g) r +zip = zipWith Pair + +zipWith :: + SListI (Types r) + => (forall x. f x -> g x -> h x) + -> ModelRecord f r -> ModelRecord g r -> ModelRecord h r +zipWith f (MR np) (MR np') = MR (SOP.hzipWith f np np') + +zipWithM :: forall m f g h r. + SListI (Types r) + => Applicative m + => (forall x. f x -> g x -> m (h x)) + -> ModelRecord f r -> ModelRecord g r -> m (ModelRecord h r) +zipWithM f (MR np) (MR np') = + fmap MR $ SOP.hsequence' $ SOP.hzipWith f' np np' + where + f' :: forall x. f x -> g x -> (m :.: h) x + f' x y = Comp $ f x y + +collapse :: SListI (Types r) => ModelRecord (K a) r -> [a] +collapse (MR np) = SOP.hcollapse np + +sequenceA :: + SListI (Types r) + => Applicative m + => ModelRecord (m :.: f) r -> m (ModelRecord f r) +sequenceA (MR np) = MR <$> SOP.hsequence' np + +pure :: ModelFields r -> (forall x. f x) -> ModelRecord f r +pure MF0 f = MR (SOP.hpure f) +pure MF1 f = MR (SOP.hpure f) +pure MF2 f = MR (SOP.hpure f) +pure MF2' f = MR (SOP.hpure f) + +ap :: + SListI (Types r) + => ModelRecord (f -.-> g) r -> ModelRecord f r -> ModelRecord g r +ap (MR np) (MR np') = MR $ SOP.hliftA2 apFn np np' + +{------------------------------------------------------------------------------- + Constrained combinators +-------------------------------------------------------------------------------} + +cpure :: + ModelSatisfies c + => Proxy c + -> ModelFields r + -> (forall x. c x => f x) + -> ModelRecord f r +cpure p MF0 f = MR (SOP.hcpure p f) +cpure p MF1 f = MR (SOP.hcpure p f) +cpure p MF2 f = MR (SOP.hcpure p f) +cpure p MF2' f = MR (SOP.hcpure p f) + +cmap :: + All c (Types r) + => Proxy c + -> (forall x. c x => f x -> g x) + -> ModelRecord f r -> ModelRecord g r +cmap p f (MR np) = MR (SOP.hcmap p f np) + +cmapM :: + (Applicative m, All c (Types r)) + => Proxy c + -> (forall x. c x => f x -> m (g x)) + -> ModelRecord f r -> m (ModelRecord g r) +cmapM p f (MR np) = fmap MR $ SOP.hctraverse' p f np + +czipWith :: + All c (Types r) + => Proxy c + -> (forall x. c x => f x -> g x -> h x) + -> ModelRecord f r -> ModelRecord g r -> ModelRecord h r +czipWith p f (MR np) (MR np') = MR (SOP.hczipWith p f np np') + +czipWithM :: forall m c f g h r. + (Applicative m, All c (Types r)) + => Proxy c + -> (forall x. c x => f x -> g x -> m (h x)) + -> ModelRecord f r -> ModelRecord g r -> m (ModelRecord h r) +czipWithM p f (MR np) (MR np') = + fmap MR $ SOP.hsequence' $ SOP.hczipWith p f' np np' + where + f' :: forall x. c x => f x -> g x -> (m :.: h) x + f' x y = Comp $ f x y diff --git a/test/Test/Prop/Record/Model/Generator.hs b/test/Test/Prop/Record/Model/Generator.hs new file mode 100644 --- /dev/null +++ b/test/Test/Prop/Record/Model/Generator.hs @@ -0,0 +1,359 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} +{-# OPTIONS -Wno-orphans #-} + +module Test.Prop.Record.Model.Generator ( + -- * Existential wrapper around 'ModelRecord' that hides the record shape + SomeFields(..) + , SomeRecord(..) + , SomeRecordPair(..) + -- * Construction + , someModlRecord + , someAnonRecord + -- * Mapping + , onModlRecord + , onModlRecordM + , onModlRecordPair + , onModlRecordPairM + , onAnonRecord + , onAnonRecordM + , onAnonRecordPair + , onAnonRecordPairM + ) where + +import Data.Proxy +import Data.SOP (NP(..), SListI, All) +import Data.SOP.BasicFunctors + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) + +import Test.QuickCheck + +import Test.Prop.Record.Model ( + ModelRecord(..) + , ModelFields(..) + , ModelSatisfies + , Types + ) + +import qualified Test.Prop.Record.Model as Model + +{------------------------------------------------------------------------------- + Existential wrapper around 'ModelRecord' that hides the record shape +-------------------------------------------------------------------------------} + +data SomeFields where + SF :: SListI (Types r) => ModelFields r -> SomeFields + +data SomeRecord f where + SR :: SListI (Types r) + => ModelFields r -> ModelRecord f r -> SomeRecord f + +data SomeRecordPair f g where + SR2 :: SListI (Types r) + => ModelFields r + -> ModelRecord f r -> ModelRecord g r -> SomeRecordPair f g + +{------------------------------------------------------------------------------- + Construction +-------------------------------------------------------------------------------} + +someModlRecord :: + SomeFields + -> (forall r. SListI (Types r) => ModelFields r -> ModelRecord f r) + -> SomeRecord f +someModlRecord (SF mf) f = SR mf (f mf) + +someAnonRecord :: forall c f. + ModelSatisfies c + => Proxy c + -> SomeFields + -> (forall r. (KnownFields r, AllFields r c) => Record f r) + -> SomeRecord f +someAnonRecord _ (SF mf) f = SR mf (Model.fromRecord mf $ f' mf) + where + f' :: ModelFields r -> Record f r + f' MF0 = f + f' MF1 = f + f' MF2 = f + f' MF2' = f + +{------------------------------------------------------------------------------- + Mapping +-------------------------------------------------------------------------------} + +onModlRecord :: + ModelSatisfies c + => Proxy c + -> (forall r. All c (Types r) => ModelRecord f r -> ModelRecord g r) + -> SomeRecord f -> SomeRecord g +onModlRecord p f = unI . onModlRecordM p (I . f) + +onModlRecordPair :: + ModelSatisfies c + => Proxy c + -> ( forall r. + All c (Types r) + => ModelRecord f r -> ModelRecord g r -> ModelRecord h r + ) + -> SomeRecordPair f g -> SomeRecord h +onModlRecordPair p f = unI . onModlRecordPairM p (I .: f) + +onModlRecordM :: + (Functor m, ModelSatisfies c) + => Proxy c + -> (forall r. All c (Types r) => ModelRecord f r -> m (ModelRecord g r)) + -> SomeRecord f -> m (SomeRecord g) +onModlRecordM p f (SR mf r) = Model.satisfyAll p mf $ SR mf <$> f r + +onModlRecordPairM :: + (Functor m, ModelSatisfies c) + => Proxy c + -> ( forall r. + All c (Types r) + => ModelRecord f r -> ModelRecord g r -> m (ModelRecord h r) + ) + -> SomeRecordPair f g -> m (SomeRecord h) +onModlRecordPairM p f (SR2 mf r r') = Model.satisfyAll p mf $ SR mf <$> f r r' + +onAnonRecord :: + ModelSatisfies c + => Proxy c + -> (forall r. AllFields r c => Record f r -> Record g r) + -> SomeRecord f -> SomeRecord g +onAnonRecord p f = unI . onAnonRecordM p (I . f) + +onAnonRecordPair :: + ModelSatisfies c + => Proxy c + -> (forall r. AllFields r c => Record f r -> Record g r -> Record h r) + -> SomeRecordPair f g -> SomeRecord h +onAnonRecordPair p f = unI . onAnonRecordPairM p (I .: f) + +onAnonRecordM :: forall m c f g. + (Functor m, ModelSatisfies c) + => Proxy c + -> (forall r. AllFields r c => Record f r -> m (Record g r)) + -> SomeRecord f -> m (SomeRecord g) +onAnonRecordM p f = \(SR mf r) -> SR mf <$> f' mf r + where + f' :: forall r. ModelFields r -> ModelRecord f r -> m (ModelRecord g r) + f' mf r = + Model.toRecordOfDicts p mf $ + Model.fromRecord mf <$> + f (Model.toRecord mf r) + +onAnonRecordPairM :: forall m c f g h. + (Functor m, ModelSatisfies c) + => Proxy c + -> (forall r. AllFields r c => Record f r -> Record g r -> m (Record h r)) + -> SomeRecordPair f g -> m (SomeRecord h) +onAnonRecordPairM p f = \(SR2 mf r r') -> SR mf <$> f' mf r r' + where + f' :: forall r. + ModelFields r + -> ModelRecord f r -> ModelRecord g r -> m (ModelRecord h r) + f' mf r r' = + Model.toRecordOfDicts p mf $ + Model.fromRecord mf <$> + f (Model.toRecord mf r) (Model.toRecord mf r') + +{------------------------------------------------------------------------------- + Generators for ModelRecord for concrete rows +-------------------------------------------------------------------------------} + +instance Arbitrary (ModelRecord f '[]) where + arbitrary = pure $ MR Nil + +instance ( Arbitrary (f Bool) + ) => Arbitrary (ModelRecord f '[ "b" := Bool ]) where + arbitrary = + (\x -> MR (x :* Nil)) + <$> arbitrary + + shrink (MR (x :* Nil)) = concat [ + (\x' -> MR (x' :* Nil)) <$> shrink x + ] + +instance ( Arbitrary (f Word) + , Arbitrary (f Bool) + ) => Arbitrary (ModelRecord f [ "a" := Word, "b" := Bool ]) where + arbitrary = + (\x y -> MR (x :* y :* Nil)) + <$> arbitrary + <*> arbitrary + + shrink (MR (x :* y :* Nil)) = concat [ + (\x' -> MR (x' :* y :* Nil)) <$> shrink x + , (\y' -> MR (x :* y' :* Nil)) <$> shrink y + ] + +instance ( Arbitrary (f Word) + , Arbitrary (f Bool) + ) => Arbitrary (ModelRecord f [ "b" := Word, "a" := Bool ]) where + arbitrary = + (\x y -> MR (x :* y :* Nil)) + <$> arbitrary + <*> arbitrary + + shrink (MR (x :* y :* Nil)) = concat [ + (\x' -> MR (x' :* y :* Nil)) <$> shrink x + , (\y' -> MR (x :* y' :* Nil)) <$> shrink y + ] + +{------------------------------------------------------------------------------- + Generators for existential wrappers +-------------------------------------------------------------------------------} + +instance Arbitrary SomeFields where + arbitrary = elements [ + SF MF0 + , SF MF1 + , SF MF2 + , SF MF2' + ] + + shrink (SF MF0) = [] + shrink (SF MF1) = [SF MF0] + shrink (SF MF2) = [SF MF1] + shrink (SF MF2') = [SF MF1] + +instance ( Arbitrary (f Word), Arbitrary (f Bool) + ) => Arbitrary (SomeRecord f) where + arbitrary = oneof [ + SR MF0 <$> arbitrary + , SR MF1 <$> arbitrary + , SR MF2 <$> arbitrary + , SR MF2' <$> arbitrary + ] + + shrink (SR MF0 r) = concat [ + SR MF0 <$> shrink r + ] + shrink (SR MF1 r) = concat [ + SR MF1 <$> shrink r + , pure $ SR MF0 (dropHead r) + ] + shrink (SR MF2 r) = concat [ + SR MF2 <$> shrink r + , pure $ SR MF1 (dropHead r) + ] + shrink (SR MF2' r) = concat [ + SR MF2' <$> shrink r + -- can't remove a field here (at least, not easily) + ] + +instance ( Arbitrary (f Word), Arbitrary (f Bool) + , Arbitrary (g Word), Arbitrary (g Bool) + ) => Arbitrary (SomeRecordPair f g) where + arbitrary = oneof [ + SR2 MF0 <$> arbitrary <*> arbitrary + , SR2 MF1 <$> arbitrary <*> arbitrary + , SR2 MF2 <$> arbitrary <*> arbitrary + , SR2 MF2' <$> arbitrary <*> arbitrary + ] + + shrink (SR2 MF0 r r') = concat [ + SR2 MF0 <$> shrink r <*> pure r' + , SR2 MF0 <$> pure r <*> shrink r' + ] + shrink (SR2 MF1 r r') = concat [ + SR2 MF1 <$> shrink r <*> pure r' + , SR2 MF1 <$> pure r <*> shrink r' + , pure $ SR2 MF0 (dropHead r) (dropHead r') + ] + shrink (SR2 MF2 r r') = concat [ + SR2 MF2 <$> shrink r <*> pure r' + , SR2 MF2 <$> pure r <*> shrink r' + , pure $ SR2 MF1 (dropHead r) (dropHead r') + ] + shrink (SR2 MF2' r r') = concat [ + SR2 MF2' <$> shrink r <*> pure r' + , SR2 MF2' <$> pure r <*> shrink r' + -- can't remove a field here (at least, not easily) + ] + +{------------------------------------------------------------------------------- + Show/Eq instances +-------------------------------------------------------------------------------} + +deriving instance Show SomeFields + +instance ( Show (f Word), Show (f Bool) + ) => Show (SomeRecord f) where + show (SR MF0 r) = show r + show (SR MF1 r) = show r + show (SR MF2 r) = show r + show (SR MF2' r) = show r + +instance ( Show (f Word), Show (f Bool) + , Show (g Word), Show (g Bool) + ) => Show (SomeRecordPair f g) where + show (SR2 MF0 r r') = show (r, r') + show (SR2 MF1 r r') = show (r, r') + show (SR2 MF2 r r') = show (r, r') + show (SR2 MF2' r r') = show (r, r') + +instance ( Eq (f Word), Eq (f Bool) + ) => Eq (SomeRecord f) where + x == y = + case (x, y) of + (SR MF0 r , SR MF0 r') -> r == r' + (SR MF1 r , SR MF1 r') -> r == r' + (SR MF2 r , SR MF2 r') -> r == r' + (SR MF2' r , SR MF2' r') -> r == r' + (_ , _ ) -> False + where + -- Make sure we don't omit a case above + _coverAllCases :: () + _coverAllCases = + case x of + SR MF0 _ -> () + SR MF1 _ -> () + SR MF2 _ -> () + SR MF2' _ -> () + +instance ( Eq (f Word), Eq (f Bool) + , Eq (g Word), Eq (g Bool) + ) => Eq (SomeRecordPair f g) where + x == y = + case (x, y) of + (SR2 MF0 r1 r2 , SR2 MF0 r1' r2' ) -> r1 == r1' && r2 == r2' + (SR2 MF1 r1 r2 , SR2 MF1 r1' r2' ) -> r1 == r1' && r2 == r2' + (SR2 MF2 r1 r2 , SR2 MF2 r1' r2' ) -> r1 == r1' && r2 == r2' + (SR2 MF2' r1 r2 , SR2 MF2' r1' r2' ) -> r1 == r1' && r2 == r2' + (_ , _ ) -> False + where + -- Make sure we don't omit a case above + _coverAllCases :: () + _coverAllCases = + case x of + SR2 MF0 _ _ -> () + SR2 MF1 _ _ -> () + SR2 MF2 _ _ -> () + SR2 MF2' _ _ -> () + +{------------------------------------------------------------------------------- + Auxiliary +-------------------------------------------------------------------------------} + +dropHead :: ModelRecord f (n := x ': xs) -> ModelRecord f xs +dropHead (MR (_ :* xs)) = MR xs + +(.:) :: (c -> d) -> (a -> b -> c) -> a -> b -> d +(f .: g) x y = f (g x y) + diff --git a/test/Test/Prop/Record/Model/Orphans.hs b/test/Test/Prop/Record/Model/Orphans.hs new file mode 100644 --- /dev/null +++ b/test/Test/Prop/Record/Model/Orphans.hs @@ -0,0 +1,15 @@ +{-# OPTIONS -Wno-orphans #-} + +module Test.Prop.Record.Model.Orphans () where + +import Data.SOP.BasicFunctors + +import Test.QuickCheck + +instance Arbitrary a => Arbitrary (K a b) where + arbitrary = K <$> arbitrary + shrink (K a) = K <$> shrink a + +instance Arbitrary a => Arbitrary (I a) where + arbitrary = I <$> arbitrary + shrink (I a) = I <$> shrink a diff --git a/test/Test/Sanity/AllFields.hs b/test/Test/Sanity/AllFields.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/AllFields.hs @@ -0,0 +1,79 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +module Test.Sanity.AllFields (tests) where + +import Data.Proxy +import Data.SOP.BasicFunctors +import Data.SOP.Dict + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) +import qualified Data.Record.Anon.Advanced as Anon + +import Test.Tasty +import Test.Tasty.HUnit + +tests :: TestTree +tests = testGroup "Test.Sanity.AllFields" [ + testCase "manual" test_manual + , testCase "derived" test_derived + ] + +{------------------------------------------------------------------------------- + Example value +-------------------------------------------------------------------------------} + +recordA :: Record I [ "a" := Int, "b" := Bool, "c" := Char ] +recordA = + Anon.insert #a (I 1) + $ Anon.insert #b (I True) + $ Anon.insert #c (I 'a') + $ Anon.empty + +-- | Manually created record of dictionaries +-- +-- Normally this record would be constructed by the plugin (for 'RecordDicts' +-- instance). +recordD :: Record (Dict (Compose Show I)) [ "a" := Int, "b" := Bool, "c" := Char ] +recordD = + Anon.insert #a Dict + $ Anon.insert #b Dict + $ Anon.insert #c Dict + $ Anon.empty + +{------------------------------------------------------------------------------- + Auxiliary +-------------------------------------------------------------------------------} + +showFields :: Record (Dict (Compose Show f)) r -> Record f r -> [String] +showFields ds xs = Anon.collapse $ Anon.zipWith aux ds xs + where + aux :: (Dict (Compose Show f)) x -> f x -> K String x + aux Dict x = K (show x) + +{------------------------------------------------------------------------------- + Tests proper +-------------------------------------------------------------------------------} + +-- | Test with manually constructed record-of-dictionaries +-- +-- Just a sanity check on the sanity check that the test makes sense. +test_manual :: Assertion +test_manual = do + assertEqual "" expected $ showFields recordD recordA + where + expected :: [String] + expected = ["I 1", "I True", "I 'a'"] + +test_derived :: Assertion +test_derived = do + assertEqual "" expected $ + showFields (Anon.reifyAllFields (Proxy @(Compose Show I))) recordA + where + expected :: [String] + expected = ["I 1", "I True", "I 'a'"] diff --git a/test/Test/Sanity/Applicative.hs b/test/Test/Sanity/Applicative.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/Applicative.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE OverloadedLabels #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +module Test.Sanity.Applicative (tests) where + +import Validation + +import Data.Record.Anon +import Data.Record.Anon.Simple (Record) +import qualified Data.Record.Anon.Simple as Anon + +import Test.Tasty +import Test.Tasty.HUnit + +tests :: TestTree +tests = testGroup "Test.Sanity.Applicative" [ + testCase "insertA" test_insertA + ] + +test_insertA :: Assertion +test_insertA = + case example of + Failure _ -> error "unexpected failure" + Success r -> assertEqual "" r validated + +{------------------------------------------------------------------------------- + Example values +-------------------------------------------------------------------------------} + +example :: Validation [String] (Record [ "a" := Int, "b" := Bool, "c" := Char ]) +example = + Anon.insertA #a validateInt + $ Anon.insertA #b validateBool + $ Anon.insertA #c validateChar + $ pure Anon.empty + where + validateInt :: Validation [String] Int + validateBool :: Validation [String] Bool + validateChar :: Validation [String] Char + + validateInt = Success 1 + validateBool = Success True + validateChar = Success 'a' + +validated :: Record [ "a" := Int, "b" := Bool, "c" := Char ] +validated = + Anon.insert #a 1 + $ Anon.insert #b True + $ Anon.insert #c 'a' + $ Anon.empty diff --git a/test/Test/Sanity/BlogPost.hs b/test/Test/Sanity/BlogPost.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/BlogPost.hs @@ -0,0 +1,379 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fplugin=RecordDotPreprocessor -fplugin=Data.Record.Anon.Plugin #-} + +module Test.Sanity.BlogPost ( + tests + -- * Examples for the blog post + , checkIsSubRow + , exampleRender + , exampleRender' + , magenta + , magenta' + , ordImpliesEq + , purple + , recordToJSON + , recordToJSON' + , reduceBlue + , reduceGreen + , reduceRed + , showRecord + , smallerSatisfies + ) where + +import Data.Aeson (ToJSON(..), Value) +import Data.Bifunctor +import Data.Function (on) +import Data.Kind +import Data.Maybe +import Data.SOP (fn_3) +import Data.String +import Data.Type.Equality +import GHC.TypeLits +import Optics.Core (over) +import Text.Parsec (Parsec, ParseError) +import Text.Read (readMaybe) + +import qualified Data.Aeson as Aeson +import qualified Data.Aeson.Encode.Pretty as Aeson.Pretty +import qualified Data.ByteString.Lazy as Lazy (ByteString) +import qualified Data.ByteString.Lazy.Char8 as Lazy.BS.C8 +import qualified Data.Text as Text +import qualified Text.Parsec as Parsec + +import Data.Record.Anon +import Data.Record.Anon.Simple (Record) +import Data.Record.Anon.Advanced (InRow(..)) + +import qualified Data.Record.Anon.Advanced as A +import qualified Data.Record.Anon.Simple as S + +import Test.Tasty +import Test.Tasty.HUnit + +tests :: TestTree +tests = testGroup "Test.Sanity.BlogPost" [ + testCase "showColor" test_showColor + , testCase "toJSON" test_toJSON + , testCase "parseConfig" test_parseConfig + , testCase "recordToJSON" test_recordToJSON + ] + +test_showColor :: Assertion +test_showColor = + assertEqual "" expected $ + show magenta + where + expected :: String + expected = "Record {red = 1.0, green = 0.0, blue = 1.0}" + +test_toJSON :: Assertion +test_toJSON = + assertEqual "" expected $ + Aeson.Pretty.encodePretty' aesonPrettyConfig $ + toJSON magenta + where + expected :: Lazy.ByteString + expected = Lazy.BS.C8.intercalate "\n" [ + "{" + , " \"red\": 1," + , " \"green\": 0," + , " \"blue\": 1" + , "}" + ] + +test_parseConfig :: Assertion +test_parseConfig = do + assertEqual "in order" expected . first show $ + runParser parseConfig ["2.1", "14", "Example"] + assertEqual "out of order" expected . first show $ + runParser parseConfig' ["Example", "2.1", "14"] + assertEqual "out of order, WRONG" expected' . first show $ + runParser parseConfigWRONG ["Example", "2.1", "14"] + where + expected :: Either String (Record Config) + expected = Right ANON { + margin = 2.1 + , fontSize = 14 + , header = "Example" + } + + expected' :: Either String (Record Config) + expected' = Left "(line 1, column 1):\nunexpected Example" + +test_recordToJSON :: Assertion +test_recordToJSON = do + assertEqual "" expected $ + Aeson.Pretty.encodePretty' aesonPrettyConfig $ + recordToJSON + defaultFieldToJSON{header = FieldToJSON headerToJSON} + defaultConfig + where + expected :: Lazy.ByteString + expected = Lazy.BS.C8.intercalate "\n" [ + "{" + , " \"margin\": 1," + , " \"fontSize\": 18," + , " \"header\": null" + , "}" + ] + + headerToJSON :: String -> Value + headerToJSON "" = Aeson.Null + headerToJSON xs = toJSON xs + +aesonPrettyConfig :: Aeson.Pretty.Config +aesonPrettyConfig = Aeson.Pretty.defConfig { + Aeson.Pretty.confCompare = compare `on` (fieldIndex . Text.unpack) + } + where + -- This is pretty hacky, but it just makes the examples a bit nicer and + -- avoids compatibility problems between Aeson versions. + fieldIndex :: String -> Int + -- Color + fieldIndex "red" = 0 + fieldIndex "green" = 1 + fieldIndex "blue" = 2 + -- Config + fieldIndex "margin" = 0 + fieldIndex "fontSize" = 1 + fieldIndex "header" = 2 + -- Other + fieldIndex name = error $ "fieldIndex: unknown field " ++ show name + +{------------------------------------------------------------------------------- + Introduction example + + Introduces ANON syntax, and field get/set +-------------------------------------------------------------------------------} + +magenta :: Record [ "red" := Double, "green" := Double, "blue" := Double ] +magenta = ANON { red = 1, green = 0, blue = 1 } + +reduceRed :: RowHasField "red" r Double => Record r -> Record r +reduceRed c = c{red = c.red * 0.9} + +{------------------------------------------------------------------------------- + The simple API + + - Alternative syntax for writing records + - Alternative ways to access fields + o set/get + o lens + - Show and other standard instances + Show the signature of `showRecord`, forward reference to discussion + about `KnownFields` and `AllFields`. + - Generics (example: ToJSON) + - Subrows +-------------------------------------------------------------------------------} + +purple :: Record [ "red" := Double, "green" := Double, "blue" := Double ] +purple = + S.insert #red 0.5 + $ S.insert #green 0 + $ S.insert #blue 0.5 + $ S.empty + +reduceGreen :: RowHasField "green" r Double => Record r -> Record r +reduceGreen c = S.set #green (S.get #green c * 0.9) c + +reduceBlue :: RowHasField "blue" r Double => Record r -> Record r +reduceBlue = over #blue (* 0.9) + +showRecord :: (KnownFields r, AllFields r Show) => Record r -> String +showRecord = show + +type Config = [ + "margin" := Double + , "fontSize" := Int + , "header" := String + ] + +defaultConfig :: Record Config +defaultConfig = ANON { + margin = 1 + , fontSize = 18 + , header = "" + } + +render :: Record Config -> () +render = undefined + +exampleRender :: () +exampleRender = render $ defaultConfig{margin = 2} + +render' :: SubRow Config overrides => Record overrides -> () +render' overrides = render (S.inject overrides defaultConfig) + +exampleRender' :: () +exampleRender' = render' $ ANON { margin = 2 } + +{------------------------------------------------------------------------------- + Advanced API + + - Functor argument + - Usefulness of ordering +-------------------------------------------------------------------------------} + +magenta' :: A.Record I [ "red" := Double, "green" := Double, "blue" := Double ] +magenta' = S.toAdvanced magenta + +parseConfig :: Parser (Record Config) +parseConfig = S.sequenceA $ ANON_F { + margin = parseDouble + , fontSize = parseInt + , header = parseString + } + +parseConfig' :: Parser (Record Config) +parseConfig' = fmap S.project . S.sequenceA $ ANON_F { + header = parseString + , margin = parseDouble + , fontSize = parseInt + } + +parseConfigWRONG :: Parser (Record Config) +parseConfigWRONG = S.sequenceA . A.project $ ANON_F { + header = parseString + , margin = parseDouble + , fontSize = parseInt + } + +{------------------------------------------------------------------------------- + Slightly more elaborate example: generate JSON with per-field overrides +-------------------------------------------------------------------------------} + +newtype FieldToJSON a = FieldToJSON (a -> Value) + +recordToJSON :: KnownFields r => A.Record FieldToJSON r -> Record r -> Value +recordToJSON fs xs = Aeson.object . map (first fromString) $ + A.toList $ A.zipWith aux fs (S.toAdvanced xs) + where + aux :: FieldToJSON x -> I x -> K Value x + aux (FieldToJSON f) (I x) = K (f x) + +defaultFieldToJSON :: AllFields r ToJSON => A.Record FieldToJSON r +defaultFieldToJSON = A.cpure (Proxy @ToJSON) (FieldToJSON toJSON) + +newtype NamedFieldToJSON a = NamedFieldToJSON (String -> a -> Value) + +recordToJSON' :: forall r. + KnownFields r + => A.Record NamedFieldToJSON r -> Record r -> Value +recordToJSON' fs xs = Aeson.object . map (first fromString) $ + A.toList $ + A.pure (fn_3 aux) + `A.ap` fs + `A.ap` A.reifyKnownFields (Proxy @r) + `A.ap` S.toAdvanced xs + where + aux :: NamedFieldToJSON x -> K String x -> I x -> K Value x + aux (NamedFieldToJSON f) (K name) (I x) = K (f name x) + +{------------------------------------------------------------------------------- + Examples of proving constraints + + No induction, so we must do something different. +-------------------------------------------------------------------------------} + +ordImpliesEq :: AllFields r Ord => Reflected (AllFields r Eq) +ordImpliesEq = + A.reflectAllFields $ + A.map aux (A.reifyAllFields (Proxy @Ord)) + where + aux :: forall x. Dict Ord x -> Dict Eq x + aux Dict = Dict + +smallerSatisfies :: forall r r' c. + (SubRow r r', AllFields r c) + => Proxy c -> Proxy r -> Reflected (AllFields r' c) +smallerSatisfies pc _ = + A.reflectAllFields $ + A.project (A.reifyAllFields pc :: A.Record (Dict c) r) + +{------------------------------------------------------------------------------- + Advanced example: check for projection + + We avoid Typeable, just to show that we can. The version in + "Test.Infra.Discovery" gives better error messages and is kind-polymorphic. +-------------------------------------------------------------------------------} + +data SupportedType a where + SupportedInt :: SupportedType Int + SupportedBool :: SupportedType Bool + +class IsSupportedType a where + supportedType :: Proxy a -> SupportedType a + +instance IsSupportedType Int where supportedType _ = SupportedInt +instance IsSupportedType Bool where supportedType _ = SupportedBool + +sameType :: SupportedType a -> SupportedType b -> Maybe (a :~: b) +sameType SupportedInt SupportedInt = Just Refl +sameType SupportedBool SupportedBool = Just Refl +sameType _ _ = Nothing + +checkIsSubRow :: forall (r :: Row Type) (r' :: Row Type) proxy proxy'. + ( KnownFields r + , KnownFields r' + , SubRow r r + , SubRow r' r' + , AllFields r IsSupportedType + , AllFields r' IsSupportedType + ) + => proxy r -> proxy' r' -> Maybe (Reflected (SubRow r r')) +checkIsSubRow _ _ = + A.reflectSubRow <$> go A.reifySubRow A.reifySubRow + where + go :: A.Record (InRow r ) r + -> A.Record (InRow r') r' + -> Maybe (A.Record (InRow r) r') + go r r' = A.cmapM (Proxy @IsSupportedType) (findField r) r' + + findField :: forall x'. + IsSupportedType x' + => A.Record (InRow r) r -> InRow r' x' -> Maybe (InRow r x') + findField r x' = + listToMaybe . catMaybes . A.collapse $ + A.cmap (Proxy @IsSupportedType) (checkIsMatch x') r + + checkIsMatch :: forall x x'. + (IsSupportedType x, IsSupportedType x') + => InRow r' x' -> InRow r x -> K (Maybe (InRow r x')) x + checkIsMatch (InRow x') (InRow x) = K $ do + Refl <- sameSymbol x x' + Refl <- sameType (supportedType (Proxy @x)) (supportedType (Proxy @x')) + return $ InRow x + +{------------------------------------------------------------------------------- + Auxiliary: simple Parsec instantation just for demonstration purposes +-------------------------------------------------------------------------------} + +type Parser a = Parsec [String] () a + +runParser :: Parser a -> [String] -> Either ParseError a +runParser p = Parsec.runParser p () "" + +parser :: Read a => Parser a +parser = Parsec.tokenPrim id (\pos _ _ -> pos) readMaybe + +parseDouble :: Parser Double +parseDouble = parser + +parseInt :: Parser Int +parseInt = parser + +parseString :: Parser String +parseString = Parsec.tokenPrim id (\pos _ _ -> pos) Just diff --git a/test/Test/Sanity/CheckIsSubRow.hs b/test/Test/Sanity/CheckIsSubRow.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/CheckIsSubRow.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +module Test.Sanity.CheckIsSubRow (tests) where + +import Data.Typeable + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) + +import Test.Tasty +import Test.Tasty.HUnit + +import Test.Infra.Discovery + +tests :: TestTree +tests = testGroup "Test.Sanity.CheckIsSubRow" [ + testCase "maybeProject" test_maybeProject + ] + +test_maybeProject :: Assertion +test_maybeProject = do + case maybeProject example1 (Proxy @Row2) of + Left _ -> assertFailure "Should be able to project to Row2" + Right r1 -> assertEqual "Should be equal" r1 example2 + + case maybeProject example1 (Proxy @Row3) of + Left missing -> assertEqual "missing" ["c"] missing + Right _ -> assertFailure "Should not be able to project to Row3" + +{------------------------------------------------------------------------------- + Example values +-------------------------------------------------------------------------------} + +type Row1 = [ "a" := Int, "b" := Bool, "c" := Char ] +type Row2 = [ "c" := Char, "a" := Int ] +type Row3 = [ "c" := Bool, "a" := Int ] + +example1 :: Record I Row1 +example1 = ANON_F { + a = I 1 + , b = I True + , c = I 'a' + } + +example2 :: Record I Row2 +example2 = ANON_F { + c = I 'a' + , a = I 1 + } diff --git a/test/Test/Sanity/Discovery.hs b/test/Test/Sanity/Discovery.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/Discovery.hs @@ -0,0 +1,186 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +module Test.Sanity.Discovery (tests) where + +import Data.Either (fromRight) +import Data.Record.Generic + +import Data.Record.Anon + +import qualified Data.Record.Anon.Simple as S +import qualified Data.Record.Anon.Advanced as A + +import Test.Tasty +import Test.Tasty.HUnit + +import Test.Infra.Discovery +import Test.Infra.DynRecord +import Test.Infra.MarkStrictness + +import qualified Test.Infra.DynRecord.Simple as Dyn.S +import qualified Test.Infra.DynRecord.Advanced as Dyn.A + +{------------------------------------------------------------------------------- + Tests proper +-------------------------------------------------------------------------------} + +tests :: TestTree +tests = testGroup "Test.Sanity.Discovery" [ + testGroup "Simple" [ + testCase "inferType" test_simple_inferType + , testCase "toLens" test_simple_toLens + ] + , testGroup "Advanced" [ + testCase "inferType" test_advanced_inferType + , testCase "toLens" test_advanced_toLens + ] + ] + +{------------------------------------------------------------------------------- + Tests for the simple API (kind Type) +-------------------------------------------------------------------------------} + +type ExpectedSimple = [ "a" := Int, "c" := Char ] + +test_simple_inferType :: Assertion +test_simple_inferType = + case Dyn.S.inferType example1 of + Dyn.S.SomeRecord r -> do + assertEqual "show" expected $ + show r + + -- The comparison test implies that we are parsing one record, then + -- using the result to parse another /in the same shape/ + assertEqual "compare" (Right r) $ + Dyn.S.toRecord r example2 + where + expected :: String + expected = "Record {a = 1, b = True, c = 'a'}" + +test_simple_toLens :: Assertion +test_simple_toLens = do + assertEqual "get" expectedGet $ + show get + assertEqual "set" example1' $ + set (S.set #c 'b' get) + assertEqual "missingField" expectedMissingField . fmap (const ()) $ + Dyn.S.toLens (Proxy @ExpectedSimple) exampleMissingField + assertEqual "wrongType" expectedWrongType . fmap (const ()) $ + Dyn.S.toLens (Proxy @ExpectedSimple) exampleWrongType + where + get :: S.Record ExpectedSimple + set :: S.Record ExpectedSimple -> DynRecord + (get, set) = + fromRight (error "unexpected error") $ + Dyn.S.toLens (Proxy @ExpectedSimple) example1 + + expectedGet :: String + expectedGet = "Record {a = 1, c = 'a'}" + + expectedMissingField :: Either NotSubRow () + expectedMissingField = Left ["c"] + + -- TODO: For now we don't get more information in case of a type error + expectedWrongType :: Either NotSubRow () + expectedWrongType = Left ["c"] + +{------------------------------------------------------------------------------- + Tests for the advanced API (kind other than Type) + + These follow the same structure as the tests for the simple API. We don't + explicitly test the error cases again here ('NotSubRow'), since the + projection and parsing machinery is the same for the simple and the advanced + case. +-------------------------------------------------------------------------------} + +type ExpectedAdvanced = [ "a" := Strict Int, "c" := Lazy Char ] + +test_advanced_inferType :: Assertion +test_advanced_inferType = + case Dyn.A.inferType example1 :: Dyn.A.SomeRecord Boxed of + Dyn.A.SomeRecord r -> do + assertEqual "show" expected $ + show r + + -- The comparison test implies that we are parsing one record, then + -- using the result to parse another /in the same shape/ + assertEqual "compare" (Right r) $ + Dyn.A.toRecord r example2 + where + expected :: String + expected = "Record {a = 1, b = True, c = 'a'}" + +test_advanced_toLens :: Assertion +test_advanced_toLens = do + assertEqual "get" expectedGet $ + show get + assertEqual "set" example1' $ + set (A.set #c (BoxLazy 'b') get) + where + get :: A.Record Boxed ExpectedAdvanced + set :: A.Record Boxed ExpectedAdvanced -> DynRecord + (get, set) = + fromRight (error "unexpected error") $ + Dyn.A.toLens (Proxy @ExpectedAdvanced) example1 + + expectedGet :: String + expectedGet = "Record {a = 1, c = 'a'}" + +{------------------------------------------------------------------------------- + Example 'DynRecord' values + + These are used both for the simple and the advanced tests (which of course + interpret them differently). + + TODO: We should have a test with some shadowing. + TODO: We should not have all fields alphabetical. +-------------------------------------------------------------------------------} + +-- | Main running example +example1 :: DynRecord +example1 = DynRecord [ + ("a", VI 1) + , ("b", VB True) + , ("c", VC 'a') + ] + +-- | Like 'example1', but one field updated +example1' :: DynRecord +example1' = DynRecord [ + ("a", VI 1) + , ("b", VB True) + , ("c", VC 'b') + ] + +-- | Equal to 'example1', but with some additional fields +-- +-- We should be able to parse this according to the type inferred for +-- 'example1'. +example2 :: DynRecord +example2 = DynRecord [ + ("a", VI 1) + , ("b", VB True) + , ("c", VC 'a') + , ("d", VI 2) + ] + +-- | Example that does not conform to 'Expected': field missing +exampleMissingField :: DynRecord +exampleMissingField = DynRecord [ + ("a", VI 1) + ] + +-- | Example that does not conform to 'Expected': wrong field type +exampleWrongType :: DynRecord +exampleWrongType = DynRecord [ + ("a", VI 1) + , ("b", VB True) + , ("c", VB False) + ] + diff --git a/test/Test/Sanity/DuplicateFields.hs b/test/Test/Sanity/DuplicateFields.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/DuplicateFields.hs @@ -0,0 +1,276 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +module Test.Sanity.DuplicateFields (tests) where + +import Data.Proxy +import Data.Record.Generic.LowerBound +import Data.SOP.BasicFunctors + +import Test.Tasty +import Test.Tasty.HUnit + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) +import qualified Data.Record.Anon.Advanced as Anon + +import Test.Infra.Generics + +tests :: TestTree +tests = testGroup "Test.Sanity.DuplicateFields" [ + testGroup "Generics" [ + testCase "fieldTypes" test_fieldTypes + , testCase "describe" test_describe + , testCase "show" test_show + , testCase "read" test_read + ] + , testGroup "HasField" [ + testCase "get" test_get + , testCase "set" test_set + ] + , testGroup "Lenses" [ + testCase "project" test_project + , testCase "update" test_update + ] + , testGroup "Merging" [ + testCase "mergeSameType" test_mergeSameType + , testCase "mergeDifferentType" test_mergeDifferentType + ] + ] + +{------------------------------------------------------------------------------- + Examples +-------------------------------------------------------------------------------} + +type InterspersedSameType = + Record I [ "a" := Char + , "b" := Word + , "c" := () + , "b" := Word + , "d" := [Double] + ] + +type InterspersedDiffType = + Record I [ "a" := Char + , "b" := Word + , "c" := () + , "b" := Bool + , "d" := [Double] + ] + +interspersedSameType :: InterspersedSameType +interspersedSameType = + Anon.insert #a (I 'a') + $ Anon.insert #b (I 1) + $ Anon.insert #c (I ()) + $ Anon.insert #b (I 2) + $ Anon.insert #d (I [3.14]) + $ Anon.empty + +interspersedDiffType :: InterspersedDiffType +interspersedDiffType = + Anon.insert #a (I 'a') + $ Anon.insert #b (I 1) + $ Anon.insert #c (I ()) + $ Anon.insert #b (I True) + $ Anon.insert #d (I [3.14]) + $ Anon.empty + +{------------------------------------------------------------------------------- + Generics +-------------------------------------------------------------------------------} + +test_fieldTypes :: Assertion +test_fieldTypes = do + assertEqual "same" expected $ + debugFieldTypes (Proxy @InterspersedSameType) + assertEqual "diff" expected $ + debugFieldTypes (Proxy @InterspersedDiffType) + where + expected :: String + expected = "[a,b,c,b,d]" + +test_describe :: Assertion +test_describe = do + assertEqual "same" expectedSame $ + describeRecord (Proxy @InterspersedSameType) + assertEqual "diff" expectedDiff $ + describeRecord (Proxy @InterspersedDiffType) + where + expectedSame, expectedDiff :: String + expectedSame = concat [ + "Record {a :: I Char" + , ", b :: I Word" + , ", c :: I ()" + , ", b :: I Word" + , ", d :: I [Double]" + , "}" + ] + expectedDiff = concat [ + "Record {a :: I Char" + , ", b :: I Word" + , ", c :: I ()" + , ", b :: I Bool" + , ", d :: I [Double]" + , "}" + ] + +test_show :: Assertion +test_show = do + assertEqual "same" expectedSame $ + show interspersedSameType + assertEqual "diff" expectedDiff $ + show interspersedDiffType + where + expectedSame, expectedDiff :: String + expectedSame = concat [ + "Record {a = I 'a'" + , ", b = I 1" + , ", c = I ()" + , ", b = I 2" + , ", d = I [3.14]" + , "}" + ] + expectedDiff = concat [ + "Record {a = I 'a'" + , ", b = I 1" + , ", c = I ()" + , ", b = I True" + , ", d = I [3.14]" + , "}" + ] + +test_read :: Assertion +test_read = do + assertEqual "" expectedSame $ + Anon.cpure (Proxy @LowerBound) (I lowerBound) + assertEqual "" expectedDiff $ + Anon.cpure (Proxy @LowerBound) (I lowerBound) + where + expectedSame :: InterspersedSameType + expectedSame = + Anon.insert #a (I '\NUL') + $ Anon.insert #b (I 0) + $ Anon.insert #c (I ()) + $ Anon.insert #b (I 0) + $ Anon.insert #d (I []) + $ Anon.empty + + expectedDiff :: InterspersedDiffType + expectedDiff = + Anon.insert #a (I '\NUL') + $ Anon.insert #b (I 0) + $ Anon.insert #c (I ()) + $ Anon.insert #b (I False) + $ Anon.insert #d (I []) + $ Anon.empty + +{------------------------------------------------------------------------------- + HasField +-------------------------------------------------------------------------------} + +test_get :: Assertion +test_get = do + assertEqual "same" (I 1) $ + Anon.get #b interspersedSameType + assertEqual "diff" (I 1) $ + Anon.get #b interspersedDiffType + +test_set :: Assertion +test_set = do + assertEqual "same" expectedSameType $ + Anon.set #b (I 3) interspersedSameType + assertEqual "diff" expectedDiffType $ + Anon.set #b (I 3) interspersedDiffType + where + expectedSameType :: InterspersedSameType + expectedSameType = + Anon.insert #a (I 'a') + $ Anon.insert #b (I 3) + $ Anon.insert #c (I ()) + $ Anon.insert #b (I 2) + $ Anon.insert #d (I [3.14]) + $ Anon.empty + + expectedDiffType :: InterspersedDiffType + expectedDiffType = + Anon.insert #a (I 'a') + $ Anon.insert #b (I 3) + $ Anon.insert #c (I ()) + $ Anon.insert #b (I True) + $ Anon.insert #d (I [3.14]) + $ Anon.empty + +{------------------------------------------------------------------------------- + Lenses +-------------------------------------------------------------------------------} + +test_project :: Assertion +test_project = do + assertEqual "same" expected $ + Anon.project interspersedSameType + assertEqual "diff" expected $ + Anon.project interspersedDiffType + where + expected :: Record I [ "a" := Char + , "b" := Word + , "c" := () + , "d" := [Double] + ] + expected = + Anon.insert #a (I 'a') + $ Anon.insert #b (I 1) + $ Anon.insert #c (I ()) + $ Anon.insert #d (I [3.14]) + $ Anon.empty + +test_update :: Assertion +test_update = do + assertEqual "same" (upd interspersedSameType) $ + setSame new + assertEqual "diff" (upd interspersedDiffType) $ + setDiff new + where + (_, setSame) = Anon.lens interspersedSameType + (_, setDiff) = Anon.lens interspersedDiffType + + upd :: RowHasField "d" r [Double] => Record I r -> Record I r + upd r = Anon.set #d (I [1.618]) r + + new :: Record I '[ "d" := [Double] ] + new = Anon.insert #d (I [1.618]) $ Anon.empty + +{------------------------------------------------------------------------------- + Merging +-------------------------------------------------------------------------------} + +test_mergeSameType :: Assertion +test_mergeSameType = do + assertEqual "" expected actual + where + actual :: Record I '[ "a" := Bool ] + actual = Anon.project $ + Anon.merge + (Anon.insert #a (I True) Anon.empty) + (Anon.insert #a (I False) Anon.empty) + + expected :: Record I '[ "a" := Bool ] + expected = Anon.insert #a (I True) Anon.empty + +test_mergeDifferentType :: Assertion +test_mergeDifferentType = do + assertEqual "" expected actual + where + actual :: Record I '[ "a" := Bool ] + actual = Anon.project $ + Anon.merge (Anon.insert #a (I True) Anon.empty) + (Anon.insert #a (I 'a') Anon.empty) + + expected :: Record I '[ "a" := Bool ] + expected = Anon.insert #a (I True) Anon.empty diff --git a/test/Test/Sanity/Generics.hs b/test/Test/Sanity/Generics.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/Generics.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} +{-# OPTIONS_GHC -Wno-orphans #-} -- for the ToJSON/FromJSON instances + +module Test.Sanity.Generics (tests) where + +import Data.Aeson +import Data.Record.Generic + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) +import qualified Data.Record.Anon.Advanced as Anon + +import Test.Tasty +import Test.Tasty.HUnit + +import Test.Infra.Generics + +import qualified Test.Sanity.Named.Record1 as R1 +import qualified Test.Sanity.Named.Record2 as R2 + +-- add test with non-I functor + +tests :: TestTree +tests = testGroup "Test.Sanity.Generics" [ + testCase "Show" test_Show + , testCase "Eq" test_Eq + , testCase "Ord" test_Ord + , testCase "describeRecord" test_describeRecord + , testCase "JSON" test_JSON + ] + +{------------------------------------------------------------------------------- + Example values +-------------------------------------------------------------------------------} + +type TypeRecord1 = Record I [ "x" := Bool, "y" := Char, "z" := () ] + +record1 :: Record I [ "x" := Bool, "y" := Char, "z" := () ] +record1 = + Anon.insert #x (I True) + $ Anon.insert #y (I 'a') + $ Anon.insert #z (I ()) + $ Anon.empty + +-- | Example where the fields do not appear in alphabetical order +-- +-- Ordering matters in the 'Generic' instance. +record2 :: Record I [ "y" := Char, "x" := Bool ] +record2 = + Anon.insert #y (I 'a') + $ Anon.insert #x (I True) + $ Anon.empty + +-- | Example that doesn't use I as the functor +record3 :: Record (K ()) [ "y" := Char, "x" := Bool ] +record3 = + Anon.insert #y (K ()) + $ Anon.insert #x (K ()) + $ Anon.empty + +{------------------------------------------------------------------------------- + Tests proper +-------------------------------------------------------------------------------} + +test_Show :: Assertion +test_Show = do + assertEqual "R1" (show (R1.Record (I True) (I 'a') (I ()))) $ show record1 + assertEqual "R2" (show (R2.Record (I 'a') (I True))) $ show record2 + assertEqual "R3" (show (R2.Record (K ()) (K ()))) $ show record3 + +test_Eq :: Assertion +test_Eq = do + assertEqual "equal" True $ + record1 == record1 + assertEqual "not equal" False $ + record1 == (Anon.set #x (I False) record1) + +test_Ord :: Assertion +test_Ord = do + assertEqual "R1" (compare (R1.Record (I True) (I 'a') (I ())) (R1.Record (I False) (I 'a') (I ()))) $ + compare record1 (Anon.set #x (I False) record1) + assertEqual "R2" (compare (R2.Record (I 'a') (I True)) (R2.Record (I 'a') (I False))) $ + compare record2 (Anon.set #x (I False) record2) + +-- Test 'describeRecord' +-- +-- The primary motivation for 'test_describeRecord' is actually not to test the +-- function itself, but to verify that constraint resolution is working ok. +-- Specifically, that the implicit kind argument to 'Typeable' is handled by ghc +-- and does not need to be taken into account by the @large-anon@ plugin. +test_describeRecord :: Assertion +test_describeRecord = do + assertEqual "" expected $ describeRecord (Proxy @TypeRecord1) + where + expected :: String + expected = "Record {x :: I Bool, y :: I Char, z :: I ()}" + +test_JSON :: Assertion +test_JSON = do + assertEqual "R1" (Just record1) $ decode (encode record1) + assertEqual "R2" (Just record2) $ decode (encode record2) + +{------------------------------------------------------------------------------- + Auxiliary +-------------------------------------------------------------------------------} + +instance FromJSON a => FromJSON (I a) where + parseJSON = fmap I . parseJSON + +instance ToJSON a => ToJSON (I a) where + toJSON = toJSON . unI diff --git a/test/Test/Sanity/HasField.hs b/test/Test/Sanity/HasField.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/HasField.hs @@ -0,0 +1,63 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +module Test.Sanity.HasField (tests) where + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) +import qualified Data.Record.Anon.Advanced as Anon + +import Test.Tasty +import Test.Tasty.HUnit + +tests :: TestTree +tests = testGroup "Test.Sanity.HasField" [ + testCase "HasField" test_HasField + ] + +{------------------------------------------------------------------------------- + Example values +-------------------------------------------------------------------------------} + +record1 :: Record I [ "x" := Bool, "y" := Char, "z" := () ] +record1 = + Anon.insert #x (I True) + $ Anon.insert #y (I 'a') + $ Anon.insert #z (I ()) + $ Anon.empty + +record1' :: Record I [ "x" := Bool, "y" := Char, "z" := () ] +record1' = + Anon.insert #x (I False) + $ Anon.insert #y (I 'a') + $ Anon.insert #z (I ()) + $ Anon.empty + +{------------------------------------------------------------------------------- + Tests proper +-------------------------------------------------------------------------------} + +test_HasField :: Assertion +test_HasField = do + -- get + + assertEqual "get field 1" (I True) $ Anon.get #x record1 + assertEqual "get field 2" (I 'a') $ Anon.get #y record1 + assertEqual "get field 3" (I ()) $ Anon.get #z record1 + + -- set then get + + assertEqual "set field 1, then get field 1" (I False) $ + Anon.get #x (Anon.set #x (I False) record1) + assertEqual "set field 1, then get field 2" (I 'a') $ + Anon.get #y (Anon.set #x (I False) record1) + + -- set + + assertEqual "set field 1" record1' $ Anon.set #x (I False) record1 + + diff --git a/test/Test/Sanity/Intersection.hs b/test/Test/Sanity/Intersection.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/Intersection.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +module Test.Sanity.Intersection (tests) where + +import Data.SOP.BasicFunctors + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) +import qualified Data.Record.Anon.Advanced as Anon + +import Test.Tasty +import Test.Tasty.HUnit + +import Test.Infra.Discovery + +tests :: TestTree +tests = testGroup "Test.Sanity.Intersection" [ + testCase "intersection" test_intersection + ] + +test_intersection :: Assertion +test_intersection = + case intersect example1 example2 of + Intersection p -> go p + where + go :: forall ri. + (SubRow Row1 ri, SubRow Row2 ri) + => Proxy ri -> Assertion + go _ = do + assertEqual "1" example1' $ + Anon.inject projected2 example1 + assertEqual "2" example2' $ + Anon.inject projected1 example2 + where + projected1, projected2 :: Record I ri + projected1 = Anon.project example1 + projected2 = Anon.project example2 + +{------------------------------------------------------------------------------- + Example values + + Row1 only have field "a" in common: field "b" is absent in Row2, + and field "c" has a different type +-------------------------------------------------------------------------------} + +type Row1 = [ "a" := Int, "b" := Bool, "c" := Char ] +type Row2 = [ "c" := Double, "a" := Int ] + +example1, example1' :: Record I Row1 +example1 = ANON_F { + a = I 1 + , b = I True + , c = I 'a' + } +example1' = ANON_F { + a = I 2 + , b = I True + , c = I 'a' + } + +example2, example2' :: Record I Row2 +example2 = ANON_F { + c = I 3.14 + , a = I 2 + } +example2' = ANON_F { + c = I 3.14 + , a = I 1 + } diff --git a/test/Test/Sanity/Merging.hs b/test/Test/Sanity/Merging.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/Merging.hs @@ -0,0 +1,101 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -Wno-redundant-constraints #-} +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +module Test.Sanity.Merging (tests) where + +import Data.SOP.BasicFunctors + +import Test.Tasty +import Test.Tasty.HUnit + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) +import qualified Data.Record.Anon.Advanced as Anon + +tests :: TestTree +tests = testGroup "Test.Sanity.Merging" [ + testCase "concrete" test_concrete + , testCase "polymorphic" test_polymorphic + , testCase "eqConstraint" test_eqConstraint + ] + +{------------------------------------------------------------------------------- + Example values +-------------------------------------------------------------------------------} + +ab, ab' :: + Record I (Merge [ "a" := Bool , "b" := Int ] + [ "c" := Double , "d" := Char ]) +ab = Anon.merge a b +ab' = Anon.merge a' b + +a, a' :: Record I [ "a" := Bool, "b" := Int ] +a = + Anon.insert #a (I True) + $ Anon.insert #b (I (1 :: Int)) + $ Anon.empty +a' = + Anon.insert #a (I False) + $ Anon.insert #b (I (1 :: Int)) + $ Anon.empty + +b :: Record I [ "c" := Double, "d" := Char ] +b = Anon.insert #c (I 3.14) + $ Anon.insert #d (I 'a') + $ Anon.empty + +{------------------------------------------------------------------------------- + Tests proper +-------------------------------------------------------------------------------} + +test_concrete :: Assertion +test_concrete = do + assertEqual "get" (I True) $ Anon.get #a ab + assertEqual "set" ab' $ Anon.set #a (I False) ab + +test_polymorphic :: Assertion +test_polymorphic = do + assertEqual "get" (I 1) $ getPoly ab + assertEqual "set" ab' $ setPoly ab + where + getPoly :: Record I (Merge [ "a" := Bool, "b" := Int ] r) -> I Int + getPoly = Anon.get #b + + setPoly :: + Record I (Merge [ "a" := Bool, "b" := Int ] r) + -> Record I (Merge [ "a" := Bool, "b" := Int ] r) + setPoly = Anon.set #a (I False) + +-- | Test that type equalities are handled correctly +test_eqConstraint :: Assertion +test_eqConstraint = do + assertEqual "a" (I True) $ f1 ab + assertEqual "b" (I 1) $ f2 ab + assertEqual "c" (I 3.14) $ f3 ab + where + -- Single simple equality + f1 :: row ~ Merge [ "a" := Bool , "b" := Int ] + [ "c" := Double , "d" := Char ] + => Record I row -> I Bool + f1 = Anon.get #a + + -- Multiple (transitive) equalities + f2 :: ( tf1 ~ tf2 + , tf2 ~ Merge + , row ~ tf1 [ "a" := Bool , "b" := Int ] + [ "c" := Double , "d" := Char ] + ) + => Record I row -> I Int + f2 = Anon.get #b + + -- Equality with partial application + f3 :: ( merge ~ Merge [ "a" := Bool , "b" := Int ] + , row ~ merge [ "c" := Double , "d" := Char ] + ) + => Record I row -> I Double + f3 = Anon.get #c diff --git a/test/Test/Sanity/Named/Record1.hs b/test/Test/Sanity/Named/Record1.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/Named/Record1.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} + +module Test.Sanity.Named.Record1 ( + Record(..) + ) where + +-- | Non-anonymous record (for comparison with equivalent anonymous record) +data Record f = Record { x :: f Bool, y :: f Char, z :: f () } + +deriving instance (Show (f Bool), Show (f Char), Show (f ())) => Show (Record f) +deriving instance (Eq (f Bool), Eq (f Char), Eq (f ())) => Eq (Record f) +deriving instance (Ord (f Bool), Ord (f Char), Ord (f ())) => Ord (Record f) diff --git a/test/Test/Sanity/Named/Record2.hs b/test/Test/Sanity/Named/Record2.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/Named/Record2.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} + +module Test.Sanity.Named.Record2 ( + Record(..) + ) where + +-- | Non-anonymous record (for comparison with equivalent anonymous record) +data Record f = Record { y :: f Char, x :: f Bool } + +deriving instance (Show (f Char), Show (f Bool)) => Show (Record f) +deriving instance (Eq (f Char), Eq (f Bool)) => Eq (Record f) +deriving instance (Ord (f Char), Ord (f Bool)) => Ord (Record f) + diff --git a/test/Test/Sanity/PolyKinds.hs b/test/Test/Sanity/PolyKinds.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/PolyKinds.hs @@ -0,0 +1,86 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +module Test.Sanity.PolyKinds (tests) where + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) +import qualified Data.Record.Anon.Advanced as Anon + +import Test.Tasty +import Test.Tasty.HUnit + +import Test.Infra.MarkStrictness + +{------------------------------------------------------------------------------- + Tests proper +-------------------------------------------------------------------------------} + +tests :: TestTree +tests = testGroup "Test.Sanity.PolyKinds" [ + testCase "hasField" test_hasField + , testCase "show" test_show + , testCase "project" test_project + , testCase "merge" test_merge + ] + +-- | Test generics ('AllFields' and 'KnownFields') +test_show :: Assertion +test_show = + assertEqual "" expected $ + show exampleRecord1' + where + expected :: String + expected = "Record {a = True, b = 1234}" + +-- | 'HasField' (and 'KnownHash', but that's no different for polykinds) +test_hasField :: Assertion +test_hasField = do + assertEqual "get" (BoxStrict 1234) $ + Anon.get #b $ exampleRecord1 + assertEqual "set" exampleRecord1' $ + Anon.set #a (BoxLazy True) $ exampleRecord1 + +-- | 'Project' +-- +-- NOTE: The projection must ignore the undefined value. +test_project :: Assertion +test_project = + assertEqual "" exampleRecord2 $ + Anon.project exampleRecord1 + +-- | Merging +test_merge :: Assertion +test_merge = + assertEqual "" exampleRecord1' $ + Anon.project $ Anon.merge exampleRecord2 exampleRecord3 + +{------------------------------------------------------------------------------- + Examples +-------------------------------------------------------------------------------} + +exampleRecord1, exampleRecord1' :: + Record Boxed [ "a" := Lazy Bool + , "b" := Strict Int + ] +exampleRecord1 = + Anon.insert #a (BoxLazy undefined) + $ Anon.insert #b (BoxStrict 1234) + $ Anon.empty +exampleRecord1' = + Anon.insert #a (BoxLazy True) + $ Anon.insert #b (BoxStrict 1234) + $ Anon.empty + +exampleRecord2 :: Record Boxed '[ "b" := Strict Int ] +exampleRecord2 = + Anon.insert #b (BoxStrict 1234) + $ Anon.empty + +exampleRecord3 :: Record Boxed '[ "a" := Lazy Bool ] +exampleRecord3 = + Anon.insert #a (BoxLazy True) + $ Anon.empty diff --git a/test/Test/Sanity/RecordLens.hs b/test/Test/Sanity/RecordLens.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/RecordLens.hs @@ -0,0 +1,86 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +module Test.Sanity.RecordLens (tests) where + +import Test.Tasty +import Test.Tasty.HUnit + +import Data.Record.Anon +import Data.Record.Anon.Advanced (Record) +import qualified Data.Record.Anon.Advanced as Anon + +tests :: TestTree +tests = testGroup "Test.Sanity.RecordLens" [ + testGroup "Isomorphic projections" [ + testCase "id" test_id + , testCase "reorder" test_reorder + , testCase "merge" test_merge + ] + , testGroup "General lenses" [ + testCase "lens" test_lens + ] + ] + +{------------------------------------------------------------------------------- + Example values +-------------------------------------------------------------------------------} + +recordA :: Record I [ "a" := Bool, "b" := Char, "c" := Int ] +recordA = + Anon.insert #a (I True) + $ Anon.insert #b (I 'a') + $ Anon.insert #c (I 1) + $ Anon.empty + +recordA' :: Record I [ "b" := Char, "a" := Bool, "c" := Int ] +recordA' = + Anon.insert #b (I 'a') + $ Anon.insert #a (I True) + $ Anon.insert #c (I 1) + $ Anon.empty + +recordWithMerge :: Record I (Merge '[ "a" := Bool ] [ "b" := Char, "c" := Int ]) +recordWithMerge = + Anon.merge + ( Anon.insert #a (I True) + $ Anon.empty + ) + ( Anon.insert #b (I 'a') + $ Anon.insert #c (I 1) + $ Anon.empty + ) + +recordB :: Record I [ "c" := Int, "b" := Char ] +recordB = + Anon.insert #c (I 1) + $ Anon.insert #b (I 'a') + $ Anon.empty + +{------------------------------------------------------------------------------- + Tests for isomorphic projections +-------------------------------------------------------------------------------} + +test_id :: Assertion +test_id = assertEqual "" recordA $ Anon.project recordA + +test_reorder :: Assertion +test_reorder = assertEqual "" recordA' $ Anon.project recordA + +test_merge :: Assertion +test_merge = assertEqual "" recordA $ Anon.project recordWithMerge + +{------------------------------------------------------------------------------- + Test for more general lenses +-------------------------------------------------------------------------------} + +test_lens :: Assertion +test_lens = do + let (getter, setter) = Anon.lens recordA + assertEqual "get" recordB $ + getter + assertEqual "set" (Anon.set #c (I 2) recordA) $ + setter (Anon.set #c (I 2) recordB) diff --git a/test/Test/Sanity/Simple.hs b/test/Test/Sanity/Simple.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/Simple.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +-- | Tests for the @Simple@ interface +-- +-- The @Simple@ is a thin wrapper around the @Advanced@ interface, so a few +-- select sanity tests suffice. +module Test.Sanity.Simple (tests) where + +import Test.Tasty +import Test.Tasty.HUnit + +import Data.Record.Anon +import Data.Record.Anon.Simple (Record) +import qualified Data.Record.Anon.Simple as Anon + +tests :: TestTree +tests = testGroup "Test.Sanity.Simple" [ + testCase "hasField" test_hasField + , testCase "merge" test_merge + ] + +{------------------------------------------------------------------------------- + Example values +-------------------------------------------------------------------------------} + +recordA :: Record [ "a" := Bool, "b" := Char ] +recordA = + Anon.insert #a True + $ Anon.insert #b 'a' + $ Anon.empty + +recordA' :: Record [ "a" := Bool, "b" := Char ] +recordA' = + Anon.insert #a False + $ Anon.insert #b 'a' + $ Anon.empty + +{------------------------------------------------------------------------------- + Tests proper +-------------------------------------------------------------------------------} + +test_hasField :: Assertion +test_hasField = do + assertEqual "get" True $ Anon.get #a recordA + assertEqual "set" recordA' $ Anon.set #a False recordA + +test_merge :: Assertion +test_merge = do + assertEqual "left" recordA $ Anon.project $ Anon.merge Anon.empty recordA + assertEqual "right" recordA $ Anon.project $ Anon.merge recordA Anon.empty diff --git a/test/Test/Sanity/SrcPlugin/WithTypelet.hs b/test/Test/Sanity/SrcPlugin/WithTypelet.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/SrcPlugin/WithTypelet.hs @@ -0,0 +1,95 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=TypeLet -fplugin=Data.Record.Anon.Plugin #-} +{-# OPTIONS_GHC -fplugin-opt=Data.Record.Anon.Plugin:typelet #-} +-- {-# OPTIONS_GHC -fplugin-opt=Data.Record.Anon.Plugin:debug #-} + +-- | Tests for @typelet@ +-- +-- These tests are identical to the ones in @WithoutTypelet@, except that we +-- enable the @typelet@ plugin option here. +module Test.Sanity.SrcPlugin.WithTypelet (tests) where + +import Data.SOP.BasicFunctors + +import Data.Record.Anon + +import qualified Data.Record.Anon.Advanced as A +import qualified Data.Record.Anon.Simple as S + +import Test.Tasty +import Test.Tasty.HUnit + +{------------------------------------------------------------------------------- + Tests proper +-------------------------------------------------------------------------------} + +tests :: TestTree +tests = testGroup "Test.Sanity.SrcPlugin.WithTypelet" [ + testCase "simple" test_simple + , testCase "advanced" test_advanced + ] + +test_simple :: Assertion +test_simple = do + assertEqual "inorder" expected $ example_simple + assertEqual "reordered" expected $ example_simple_reordered + where + expected :: S.Record '[ "a" := Int, "b" := Char, "c" := Bool ] + expected = + S.insert #a 1 + $ S.insert #b 'a' + $ S.insert #c True + $ S.empty + +test_advanced :: Assertion +test_advanced = do + assertEqual "I" expectedI $ example_advanced_I + assertEqual "Maybe" expectedMaybe $ example_advanced_Maybe + where + expectedI :: A.Record I [ "a" := Int, "b" := Char, "c" := Bool] + expectedI = + A.insert #a (I 1) + $ A.insert #b (I 'a') + $ A.insert #c (I True) + $ A.empty + + expectedMaybe :: Maybe (A.Record I '[ "b" := Char, "a" := Bool ]) + expectedMaybe = Just $ + A.insert #b (I 'a') + $ A.insert #a (I True) + $ A.empty + +{------------------------------------------------------------------------------- + Examples +-------------------------------------------------------------------------------} + +example_simple :: S.Record '[ "a" := Int, "b" := Char, "c" := Bool ] +example_simple = ANON { + a = 1 + , b = 'a' + , c = True + } + +-- | Check that the use of typelet does not hinder type inference +example_simple_reordered :: S.Record '[ "a" := Int, "b" := Char, "c" := Bool ] +example_simple_reordered = S.project $ ANON { + a = 1 + , c = True + , b = 'a' + } + +example_advanced_I :: A.Record I '[ "a" := Int, "b" := Char, "c" := Bool ] +example_advanced_I = ANON_F { + a = I 1 + , b = I 'a' + , c = I True + } + +example_advanced_Maybe :: Maybe (A.Record I '[ "b" := Char, "a" := Bool ]) +example_advanced_Maybe = A.sequenceA' $ ANON_F { + b = Just 'a' + , a = Just True + } diff --git a/test/Test/Sanity/SrcPlugin/WithoutTypelet.hs b/test/Test/Sanity/SrcPlugin/WithoutTypelet.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/SrcPlugin/WithoutTypelet.hs @@ -0,0 +1,95 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} +-- {-# OPTIONS_GHC -fplugin-opt=Data.Record.Anon.Plugin:debug #-} +-- {-# OPTIONS_GHC -fplugin-opt=Data.Record.Anon.Plugin:noapply #-} + +module Test.Sanity.SrcPlugin.WithoutTypelet (tests) where + +import Data.SOP.BasicFunctors + +import Data.Record.Anon + +import qualified Data.Record.Anon.Advanced as A +import qualified Data.Record.Anon.Simple as S + +import Test.Tasty +import Test.Tasty.HUnit + +{------------------------------------------------------------------------------- + Tests proper +-------------------------------------------------------------------------------} + +tests :: TestTree +tests = testGroup "Test.Sanity.SrcPlugin.WithoutTypelet" [ + testCase "simple" test_simple + , testCase "advanced" test_advanced + ] + +test_simple :: Assertion +test_simple = do + assertEqual "inorder" expected $ example_simple + assertEqual "reordered" expected $ example_simple_reordered + where + expected :: S.Record '[ "a" := Int, "b" := Char, "c" := Bool ] + expected = + S.insert #a 1 + $ S.insert #b 'a' + $ S.insert #c True + $ S.empty + +test_advanced :: Assertion +test_advanced = do + assertEqual "I" expectedI $ example_advanced_I + assertEqual "Maybe" expectedMaybe $ example_advanced_Maybe + where + expectedI :: A.Record I [ "a" := Int, "b" := Char, "c" := Bool] + expectedI = + A.insert #a (I 1) + $ A.insert #b (I 'a') + $ A.insert #c (I True) + $ A.empty + + expectedMaybe :: Maybe (A.Record I '[ "b" := Char, "a" := Bool ]) + expectedMaybe = Just $ + A.insert #b (I 'a') + $ A.insert #a (I True) + $ A.empty + +{------------------------------------------------------------------------------- + Examples +-------------------------------------------------------------------------------} + +example_simple :: S.Record '[ "a" := Int, "b" := Char, "c" := Bool ] +example_simple = ANON { + a = 1 + , b = 'a' + , c = True + } + +-- | Example showing that we can easily reorder fields +-- +-- Importantly, the @a = 1@ assignment does /not/ lead to warnings about +-- defaulting @1@: the projection causes a unificaiton to happen between its +-- type and @Int@ (provided we have a type annotation, of course). +example_simple_reordered :: S.Record '[ "a" := Int, "b" := Char, "c" := Bool ] +example_simple_reordered = S.project $ ANON { + a = 1 + , c = True + , b = 'a' + } + +example_advanced_I :: A.Record I '[ "a" := Int, "b" := Char, "c" := Bool ] +example_advanced_I = ANON_F { + a = I 1 + , b = I 'a' + , c = I True + } + +example_advanced_Maybe :: Maybe (A.Record I '[ "b" := Char, "a" := Bool ]) +example_advanced_Maybe = A.sequenceA' $ ANON_F { + b = Just 'a' + , a = Just True + } diff --git a/test/Test/Sanity/TypeLevelMetadata.hs b/test/Test/Sanity/TypeLevelMetadata.hs new file mode 100644 --- /dev/null +++ b/test/Test/Sanity/TypeLevelMetadata.hs @@ -0,0 +1,122 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fplugin=Data.Record.Anon.Plugin #-} + +-- | Test type-level metadata +-- +-- It is important that we have a separate test for this, because we don't +-- actually rely on this information anywhere; it is only for SOP interop. +module Test.Sanity.TypeLevelMetadata (tests) where + +import Data.Record.Generic +import Data.Record.Generic.SOP +import Data.Kind +import Data.Typeable +import GHC.TypeLits + +import Test.Tasty +import Test.Tasty.HUnit + +import Data.Record.Anon + +import qualified Data.Record.Anon.Simple as S +import qualified Data.Record.Anon.Advanced as A + +tests :: TestTree +tests = testGroup "Test.Sanity.TypeLevelMetadata" [ + testCase "metadata" test_metadata + , testCase "toFromSOP" test_toFromSOP + ] + +{------------------------------------------------------------------------------- + Example values +-------------------------------------------------------------------------------} + +recordA :: A.Record I [ "a" := Bool, "b" := Char ] +recordA = + A.insert #a (I True) + $ A.insert #b (I 'a') + $ A.empty + +recordS :: S.Record [ "a" := Bool, "b" := Char ] +recordS = + S.insert #a True + $ S.insert #b 'a' + $ S.empty + +{------------------------------------------------------------------------------- + Auxiliary infrastructure + + Obviously the 'GetMetadata' instances are inductive and will result in + quadratic core code blowup; they are here only for testing. +-------------------------------------------------------------------------------} + +type family Fst (p :: (k1, k2)) :: k1 where Fst '(x, y) = x +type family Snd (p :: (k1, k2)) :: k2 where Snd '(x, y) = y + +class GetMetadata (xs :: [(Symbol, Type)]) where + getMetadata :: Proxy xs -> [(String, String)] + +instance GetMetadata '[] where + getMetadata _ = [] + +instance ( KnownSymbol (Fst x) + , Typeable (Snd x) + , GetMetadata xs + ) => GetMetadata (x ': xs) where + getMetadata _ = + (symbolVal (Proxy @(Fst x)), show (typeRep (Proxy @(Snd x)))) + : getMetadata (Proxy @xs) + +-- | Reflect field metadata from the type-level information +getMetadataA :: forall f r. + GetMetadata (FieldTypes f r) + => A.Record f r -- ^ Serves as a proxy only + -> [(String, String)] +getMetadataA _ = getMetadata (Proxy @(FieldTypes f r)) + +-- | Like 'getMetadataA', but for the simple API +getMetadataS :: forall r. + GetMetadata (SimpleFieldTypes r) + => S.Record r -- ^ Serves as a proxy only + -> [(String, String)] +getMetadataS _ = getMetadata (Proxy @(SimpleFieldTypes r)) + +{------------------------------------------------------------------------------- + Tests proper + + TODO: We should have a test somewhere for normalization; this too depends + on having accurate type-level information (it's what it was introduced for + in the first place). +-------------------------------------------------------------------------------} + +test_metadata :: Assertion +test_metadata = do + assertEqual "advanced" expectedA $ + getMetadataA recordA + assertEqual "simple" expectedS $ + getMetadataS recordS + where + expectedA, expectedS :: [(String, String)] + expectedA = [ + ("a", "I Bool") + , ("b", "I Char") + ] + expectedS = [ + ("a", "Bool") + , ("b", "Char") + ] + +test_toFromSOP :: Assertion +test_toFromSOP = + assertEqual "" (Just recordA) $ + (to . fromSOP <$> toSOP (from recordA)) diff --git a/test/TestLargeAnon.hs b/test/TestLargeAnon.hs new file mode 100644 --- /dev/null +++ b/test/TestLargeAnon.hs @@ -0,0 +1,48 @@ +module Main (main) where + +import Test.Tasty + +import qualified Test.Prop.Record.Combinators.Constrained +import qualified Test.Prop.Record.Combinators.Simple +import qualified Test.Sanity.AllFields +import qualified Test.Sanity.Applicative +import qualified Test.Sanity.BlogPost +import qualified Test.Sanity.CheckIsSubRow +import qualified Test.Sanity.Discovery +import qualified Test.Sanity.DuplicateFields +import qualified Test.Sanity.Generics +import qualified Test.Sanity.HasField +import qualified Test.Sanity.Intersection +import qualified Test.Sanity.Merging +import qualified Test.Sanity.PolyKinds +import qualified Test.Sanity.RecordLens +import qualified Test.Sanity.Simple +import qualified Test.Sanity.SrcPlugin.WithoutTypelet +import qualified Test.Sanity.SrcPlugin.WithTypelet +import qualified Test.Sanity.TypeLevelMetadata + +main :: IO () +main = defaultMain $ testGroup "large-anon" [ + testGroup "Sanity" [ + Test.Sanity.HasField.tests + , Test.Sanity.Generics.tests + , Test.Sanity.Merging.tests + , Test.Sanity.RecordLens.tests + , Test.Sanity.DuplicateFields.tests + , Test.Sanity.TypeLevelMetadata.tests + , Test.Sanity.AllFields.tests + , Test.Sanity.Applicative.tests + , Test.Sanity.Simple.tests + , Test.Sanity.PolyKinds.tests + , Test.Sanity.CheckIsSubRow.tests + , Test.Sanity.Discovery.tests + , Test.Sanity.SrcPlugin.WithoutTypelet.tests + , Test.Sanity.SrcPlugin.WithTypelet.tests + , Test.Sanity.Intersection.tests + , Test.Sanity.BlogPost.tests + ] + , testGroup "Prop" [ + Test.Prop.Record.Combinators.Simple.tests + , Test.Prop.Record.Combinators.Constrained.tests + ] + ]