free-foil 0.5.0 → 0.6.0
raw patch · 30 files changed
+2485/−113 lines, 30 filesdep +should-not-typecheckdep ~containers
Dependencies added: should-not-typecheck
Dependency ranges changed: containers
Files
- ChangeLog.md +33/−0
- bench/binders/Config.hs +57/−0
- bench/binders/Generated.hs +22/−0
- bench/binders/Main.hs +269/−0
- bench/nfdata/Main.hs +87/−0
- bench/zipmatchk/Main.hs +42/−0
- free-foil.cabal +57/−2
- src/Control/Monad/Foil.hs +1/−1
- src/Control/Monad/Foil/Blocks.hs +3/−0
- src/Control/Monad/Foil/Internal.hs +102/−15
- src/Control/Monad/Foil/TH/MkInstancesFoil.hs +222/−7
- src/Control/Monad/Foil/Telescope.hs +8/−4
- src/Control/Monad/Free/Foil.hs +59/−5
- src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs +326/−7
- src/Data/ZipMatchK.hs +130/−0
- src/Data/ZipMatchK/Bifunctor.hs +29/−4
- src/Data/ZipMatchK/Functor.hs +31/−5
- src/Data/ZipMatchK/Generic.hs +163/−0
- src/Data/ZipMatchK/Mappings.hs +25/−0
- src/Data/ZipMatchK/TH.hs +194/−31
- test/Control/Monad/Foil/NameBinderListOfSpec.hs +151/−0
- test/Control/Monad/Foil/RolesSpec.hs +157/−0
- test/Control/Monad/Free/Foil/HoistSpec.hs +52/−0
- test/Control/Monad/Free/Foil/NFDataSpec.hs +36/−0
- test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs +22/−0
- test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/PatternsSyntax.hs +0/−16
- test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Syntax.hs +6/−7
- test/Data/ZipMatchK/SumProductSpec.hs +127/−0
- test/Data/ZipMatchK/THSpec.hs +46/−5
- test/laws/Control/Monad/Foil/Laws.hs +28/−4
ChangeLog.md view
@@ -1,5 +1,38 @@ # CHANGELOG for `free-foil` +# 0.6.0 — 2026-10-26++This release lets `mkFreeFoil` generate most instances of a signature, and adds folds that traverse terms without rebuilding them. Several breaking changes come with it, described first.++Breaking changes:++- Scope indices have the nominal role, so `coerce` can no longer change a scope (see [#113](https://github.com/fizruk/free-foil/pull/113), [#112](https://github.com/fizruk/free-foil/issues/112)). This applies to `Name`, `NameBinder`, `Scope`, `NameSet`, `NameBinders`, `NameMap`, the first index of `Substitution`, and the types of `Control.Monad.Foil.Blocks`.+ - To migrate, compare names of different scopes by `nameId`, and move a term to an extended scope with `sink`.+- `mkFreeFoil` generates the `Bifunctor`, `Bifoldable`, `Bitraversable`, `ZipMatchK`, `ZipMatchFoldK` and `NFData` instances of every signature, and `NFData` of every binding type (see [#116](https://github.com/fizruk/free-foil/pull/116), [#118](https://github.com/fizruk/free-foil/pull/118), [#119](https://github.com/fizruk/free-foil/pull/119)).+ - To migrate, delete these instances (or the splices deriving them), or leave them out with `mkFreeFoilWith`.+ - Instances for the payload types (identifiers, positions) must now be declared before the `mkFreeFoil` splice.+- `deriveCoSinkable` takes the scope-safe pattern type, like the other `derive*` functions (see [#122](https://github.com/fizruk/free-foil/pull/122)). The old function, which takes the raw identifier and pattern types, is renamed to `mkCoSinkableFoilPattern`.+- `nameBinderListOf` is a method of `CoSinkable` (see [#110](https://github.com/fizruk/free-foil/pull/110)). A module that imports `CoSinkable(..)` and defines its own `nameBinderListOf` must hide one of them.+- `deriveZipMatchK` needs a `ZipMatchFoldK` instance for every container type applied to a zipped parameter (see [#119](https://github.com/fizruk/free-foil/pull/119)). The library provides them for lists, `Maybe`, `Either`, pairs, `NonEmpty`, `Sum` and `Product`. Derive others with `deriveZipMatchK1`.++New:++- `ZipMatchFoldK` matches two values one level deep, like `ZipMatchK`, but folds the paired components into a monoid instead of rebuilding the value (see [#119](https://github.com/fizruk/free-foil/pull/119)). `deriveZipMatchK` derives it together with `ZipMatchK`.+- `zipMatchAllK` and `zipMatchAnyK` (with `1` and `2` variants) check a relation on all or on any of the paired components (see [#121](https://github.com/fizruk/free-foil/pull/121)).+- `foldAST` folds a term bottom-up, and `hoistAST` changes its signature by a natural transformation (see [#115](https://github.com/fizruk/free-foil/pull/115)).+- `deriveCoSinkable` derives `CoSinkable` for a scope-safe pattern type (see [#122](https://github.com/fizruk/free-foil/pull/122)).+- `mkFreeFoilWith` takes `FreeFoilOptions` to choose which instances to generate (see [#116](https://github.com/fizruk/free-foil/pull/116), [#118](https://github.com/fizruk/free-foil/pull/118)).+- `zipMatchKInstance` builds a `ZipMatchK` instance from constructor fields, for Template Haskell code (see [#116](https://github.com/fizruk/free-foil/pull/116)).+- `gnameBinderListOf` lists the binders of a pattern generically (see [#110](https://github.com/fizruk/free-foil/pull/110)).++Performance:++- `nameBinderListOf` no longer traverses the pattern for the library's instances and the generated ones (see [#110](https://github.com/fizruk/free-foil/pull/110), [#123](https://github.com/fizruk/free-foil/pull/123)).+- `withRefreshedPattern` is `INLINE`, so that it specialises at a known pattern type (see [#120](https://github.com/fizruk/free-foil/pull/120)).+- `rnf` of `AST` specialises at a known signature, and is about four times faster there (see [#114](https://github.com/fizruk/free-foil/pull/114)).+- The generated signature instances are marked `INLINE`, since GHC does not inline the derived methods of a large signature (see [#116](https://github.com/fizruk/free-foil/pull/116)).+- The `ZipMatchK` instances for `Sum` and `Product` are written out instead of generic, and no longer require `Bitraversable` (or `Traversable`) of the components (see [#109](https://github.com/fizruk/free-foil/pull/109)).+ # 0.5.0 — 2026-10-07 A release about *binders*. The law tests added after 0.4.0 ([#100](https://github.com/fizruk/free-foil/pull/100)) found bugs in how binders are sunk, ordered, paired and transported, and this release fixes them. The fixes change α-equivalence for patterns of several binders, so the release is major. It also generates single-binder pattern types as newtypes and removes the functions deprecated in 0.3.3 and 0.4.0.
+ bench/binders/Config.hs view
@@ -0,0 +1,57 @@+{-# LANGUAGE TemplateHaskell #-}++-- | A raw syntax for 'mkFreeFoil' whose patterns are variables and pairs, in+-- its own module because Template Haskell may not splice a value defined in+-- the same module. It follows @PatternsConfig@ of the test suite.+module Config where++import Control.Monad.Free.Foil.TH.MkFreeFoil++newtype BVarIdent = BVarIdent String++data BPattern+ = BPatternVar BVarIdent+ | BPatternPair BPattern BPattern++newtype BScopedTerm = BScopedTerm BTerm++data BTerm+ = BVar BVarIdent+ | BFun BPattern BScopedTerm++intToBVarIdent :: Int -> BVarIdent+intToBVarIdent i = BVarIdent ("x" <> show i)++bVar :: BVarIdent -> BTerm+bVar = BVar++bTermToScope :: BTerm -> BScopedTerm+bTermToScope = BScopedTerm++bScopeToTerm :: BScopedTerm -> BTerm+bScopeToTerm (BScopedTerm t) = t++bConfig :: FreeFoilConfig+bConfig = FreeFoilConfig+ { rawQuantifiedNames = []+ , freeFoilTermConfigs =+ [ FreeFoilTermConfig+ { rawIdentName = ''BVarIdent+ , rawTermName = ''BTerm+ , rawBindingName = ''BPattern+ , rawScopeName = ''BScopedTerm+ , rawVarConName = 'BVar+ , rawSubTermNames = []+ , rawSubScopeNames = []+ , intToRawIdentName = 'intToBVarIdent+ , rawVarIdentToTermName = 'bVar+ , rawTermToScopeName = 'bTermToScope+ , rawScopeToTermName = 'bScopeToTerm+ } ]+ , freeFoilNameModifier = ("FF" ++)+ , freeFoilScopeNameModifier = ("FFScoped" ++)+ , freeFoilConNameModifier = ("FF" ++)+ , freeFoilConvertFromName = ("from" ++)+ , freeFoilConvertToName = ("to" ++)+ , signatureNameModifier = (++ "Sig")+ }
+ bench/binders/Generated.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -Wno-missing-signatures #-}++-- | The syntax that 'mkFreeFoil' generates from "Config", whose pattern type+-- 'FFBPattern' has the 'Control.Monad.Foil.CoSinkable' instance it generates.+module Generated where++import Control.Monad.Free.Foil.TH.MkFreeFoil (mkFreeFoil)++import Config++mkFreeFoil bConfig+
+ bench/binders/Main.hs view
@@ -0,0 +1,269 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+-- The raw types below only serve Template Haskell.+{-# OPTIONS_GHC -Wno-unused-top-binds #-}++-- | What it costs to list the binders of a pattern with+-- 'Foil.nameBinderListOf', and the operations that go through it:+-- 'Foil.addSubstPattern', 'Foil.unsinkNameSet' (in 'supportOf') and the+-- default 'Foil.unifyPatterns' (in 'alphaEquiv').+--+-- The pattern types cover each way to get a 'Foil.CoSinkable' instance: the+-- library's own instances (with 'Telescope'), 'mkCoSinkableFoilPattern',+-- 'mkFreeFoil', instances written by hand and the generic default.+--+-- Each pattern type is measured twice. At a known type, a call can be+-- specialised. Through 'SomePattern', the 'Foil.CoSinkable' dictionary is+-- passed at run time, as it is in code that is polymorphic in the pattern+-- type, such as a generic typechecker.+module Main (main) where++import Data.Bifunctor.TH+import Test.Tasty.Bench++import qualified Control.Monad.Foil as Foil+import qualified Control.Monad.Foil.Example as Example+import Control.Monad.Foil.Telescope (Telescope (..))+import Control.Monad.Foil.TH (mkCoSinkableFoilPattern, mkFoilPattern)+import Control.Monad.Free.Foil+import Data.ZipMatchK.TH (deriveZipMatchK)+import Generics.Kind.TH (deriveGenericK)++import Generated (FFBPattern (..))++-- | A pattern of two binders, with every instance taken from its generic+-- default, as a client that derives 'GenericK' gets it.+data PairPattern (n :: Foil.S) (l :: Foil.S) where+ PairPattern :: Foil.NameBinder n i -> Foil.NameBinder i l -> PairPattern n l++deriveGenericK ''PairPattern+instance Foil.SinkableK PairPattern+instance Foil.HasNameBinders PairPattern+instance Foil.CoSinkable PairPattern+instance Foil.UnifiablePattern PairPattern++-- | 'PairPattern' with 'Foil.gnameBinderListOf' for 'Foil.nameBinderListOf'.+data GPairPattern (n :: Foil.S) (l :: Foil.S) where+ GPairPattern :: Foil.NameBinder n i -> Foil.NameBinder i l -> GPairPattern n l++deriveGenericK ''GPairPattern+instance Foil.SinkableK GPairPattern+instance Foil.HasNameBinders GPairPattern+instance Foil.CoSinkable GPairPattern where+ nameBinderListOf = Foil.gnameBinderListOf++-- | A pattern of variables and pairs with the instance that+-- 'mkCoSinkableFoilPattern' generates, as in a language generated from a BNFC grammar.+newtype RawIdent = RawIdent String+data RawPattern = RawPatternVar RawIdent | RawPatternPair RawPattern RawPattern++mkFoilPattern ''RawIdent ''RawPattern+mkCoSinkableFoilPattern ''RawIdent ''RawPattern++-- | A pattern of two binders with 'Foil.withPattern' written by hand and no+-- other method.+data HandPair (n :: Foil.S) (l :: Foil.S) where+ HandPair :: Foil.NameBinder n i -> Foil.NameBinder i l -> HandPair n l++instance Foil.CoSinkable HandPair where+ coSinkabilityProof rename (HandPair x y) cont =+ Foil.coSinkabilityProof rename x $ \rename' x' ->+ Foil.coSinkabilityProof rename' y $ \rename'' y' ->+ cont rename'' (HandPair x' y')++ withPattern withBinder _unit comp scope (HandPair x y) cont =+ withBinder scope x $ \fx x' ->+ let scope' = Foil.extendScope x' scope+ in withBinder scope' y $ \fy y' ->+ cont (comp fx fy) (HandPair x' y') (Foil.extendScope y' scope')++-- | A copy of the pattern of "Language.LambdaPi.Impl.Foil" and its instance:+-- wildcards, variables and pairs, with a recursive 'Foil.withPattern' and+-- 'Foil.nameBinderListOf' written by hand.+data LPPattern (n :: Foil.S) (l :: Foil.S) where+ LPWildcard :: LPPattern n n+ LPVar :: Foil.NameBinder n l -> LPPattern n l+ LPPair :: LPPattern n i -> LPPattern i l -> LPPattern n l++instance Foil.CoSinkable LPPattern where+ coSinkabilityProof rename pattern cont =+ case pattern of+ LPWildcard -> cont rename LPWildcard+ LPVar x ->+ Foil.coSinkabilityProof rename x $ \rename' x' ->+ cont rename' (LPVar x')+ LPPair l r ->+ Foil.coSinkabilityProof rename l $ \rename' l' ->+ Foil.coSinkabilityProof rename' r $ \rename'' r' ->+ cont rename'' (LPPair l' r')++ withPattern withNameBinder id' combine scope pattern cont =+ case pattern of+ LPWildcard -> cont id' LPWildcard scope+ LPVar x -> withNameBinder scope x $ \f x' ->+ cont f (LPVar x') (Foil.extendScope x' scope)+ LPPair l r -> Foil.withPattern withNameBinder id' combine scope l $ \fl l' scope' ->+ Foil.withPattern withNameBinder id' combine scope' r $ \fr r' scope'' ->+ cont (combine fl fr) (LPPair l' r') scope''++ nameBinderListOf pattern = go pattern Foil.NameBinderListEmpty+ where+ go :: LPPattern x y -> Foil.NameBinderList y z -> Foil.NameBinderList x z+ go LPWildcard rest = rest+ go (LPVar x) rest = Foil.NameBinderListCons x rest+ go (LPPair l r) rest = go l $! go r rest++-- | A telescope of @k@ steps @(x1 : \\y. y) (x2 : x1) ... (xk : x(k-1))@,+-- with the terms of "Control.Monad.Foil.Example" for payloads.+withTelescope+ :: forall r. Int+ -> (forall l. Telescope () Example.Expr Foil.VoidS l -> r)+ -> r+withTelescope k cont =+ Foil.withFresh Foil.emptyScope $ \y ->+ Foil.withFresh Foil.emptyScope $ \x ->+ go (k - 1) (Foil.extendScope x Foil.emptyScope) (Foil.nameOf x) $ \rest ->+ cont (TelescopeCons () (Example.LamE y (Example.VarE (Foil.nameOf y))) x rest)+ where+ go :: Foil.Distinct n+ => Int -> Foil.Scope n -> Foil.Name n+ -> (forall l. Telescope () Example.Expr n l -> r) -> r+ go 0 _ _ cont' = cont' TelescopeEmpty+ go j scope prev cont' = Foil.withFresh scope $ \b ->+ go (j - 1) (Foil.extendScope b scope) (Foil.nameOf b) $ \rest ->+ cont' (TelescopeCons () (Example.VarE (Foil.sink prev)) b rest)++data LamSig scope term+ = App term term+ | Lam scope+ deriving (Functor, Foldable, Traversable)++deriveBifunctor ''LamSig+deriveBifoldable ''LamSig+deriveBitraversable ''LamSig+deriveZipMatchK ''LamSig++-- | A pattern whose 'Foil.CoSinkable' dictionary travels with it.+data SomePattern where+ SomePattern :: Foil.CoSinkable pattern => pattern Foil.VoidS l -> SomePattern++-- | The length of a list of binders, which forces its spine.+size :: Foil.NameBinderList n l -> Int+size = go 0+ where+ go :: Int -> Foil.NameBinderList n l -> Int+ go !acc Foil.NameBinderListEmpty = acc+ go !acc (Foil.NameBinderListCons _ rest) = go (acc + 1) rest++-- | 'Foil.nameBinderListOf' through a dictionary. Not inlined, so that the+-- dictionary stays unknown at the call.+{-# NOINLINE listedSome #-}+listedSome :: SomePattern -> Int+listedSome (SomePattern pattern) = size (Foil.nameBinderListOf pattern)++-- | 'Foil.addSubstPattern' through a dictionary.+{-# NOINLINE substSome #-}+substSome :: [AST PairPattern LamSig Foil.VoidS] -> SomePattern -> Bool+substSome args (SomePattern pattern) =+ Foil.nullSubst (Foil.addSubstPattern Foil.identitySubst pattern args)++-- | A chain of λ-abstractions, each binding a pair of names, with a variable+-- bound by the outermost one at the bottom.+pairChain :: Int -> AST PairPattern LamSig Foil.VoidS+pairChain depth =+ withPair Foil.emptyScope $ \pattern x scope ->+ Node (Lam (ScopedAST pattern (go scope x (depth - 1))))+ where+ go :: Foil.Distinct n => Foil.Scope n -> Foil.Name n -> Int -> AST PairPattern LamSig n+ go _scope x 0 = Var x+ go scope x d = withPair scope $ \pattern _ scope' ->+ Node (Lam (ScopedAST pattern (go scope' (Foil.sink x) (d - 1))))++ withPair+ :: Foil.Distinct n+ => Foil.Scope n+ -> (forall l. Foil.DExt n l => PairPattern n l -> Foil.Name l -> Foil.Scope l -> r)+ -> r+ withPair scope cont =+ Foil.withFresh scope $ \b1 ->+ let scope1 = Foil.extendScope b1 scope+ in Foil.withFresh scope1 $ \b2 ->+ cont (PairPattern b1 b2) (Foil.sink (Foil.nameOf b1)) (Foil.extendScope b2 scope1)++main :: IO ()+main =+ Foil.withFresh Foil.emptyScope $ \b1 ->+ Foil.withFresh (Foil.extendScope b1 Foil.emptyScope) $ \b2 ->+ Foil.withFreshNameBinderList [(), (), (), ()] Foil.emptyScope Foil.emptyNameMap $ \_ list4 _ ->+ withTelescope 4 $ \tele4 ->+ let pair = PairPattern b1 b2+ var = FoilRawPatternVar b1+ thPair = FoilRawPatternPair (FoilRawPatternVar b1) (FoilRawPatternVar b2)+ ffPair = FFBPatternPair (FFBPatternVar b1) (FFBPatternVar b2)+ handPair = HandPair b1 b2+ lpPair = LPPair (LPVar b1) (LPVar b2)+ gpair = GPairPattern b1 b2+ args = [Node (App t t), t]+ t = pairChain 1+ chain = pairChain 1000+ in defaultMain+ [ bgroup "nameBinderListOf"+ [ bgroup "NameBinder"+ [ bench "known type" $ whnf (size . Foil.nameBinderListOf) b1+ , bench "a dictionary" $ whnf listedSome (SomePattern b1)+ ]+ , bgroup "TH pattern of 1"+ [ bench "known type" $ whnf (size . Foil.nameBinderListOf) var+ , bench "a dictionary" $ whnf listedSome (SomePattern var)+ ]+ , bgroup "NameBinderList of 4"+ [ bench "known type" $ whnf (size . Foil.nameBinderListOf) list4+ , bench "a dictionary" $ whnf listedSome (SomePattern list4)+ ]+ , bgroup "mkCoSinkableFoilPattern pair of 2"+ [ bench "known type" $ whnf (size . Foil.nameBinderListOf) thPair+ , bench "a dictionary" $ whnf listedSome (SomePattern thPair)+ ]+ , bgroup "mkFreeFoil pair of 2"+ [ bench "known type" $ whnf (size . Foil.nameBinderListOf) ffPair+ , bench "a dictionary" $ whnf listedSome (SomePattern ffPair)+ ]+ , bgroup "hand-written pair of 2"+ [ bench "known type" $ whnf (size . Foil.nameBinderListOf) handPair+ , bench "a dictionary" $ whnf listedSome (SomePattern handPair)+ ]+ , bgroup "lambda-pi pattern, pair of 2"+ [ bench "known type" $ whnf (size . Foil.nameBinderListOf) lpPair+ , bench "a dictionary" $ whnf listedSome (SomePattern lpPair)+ ]+ , bgroup "Telescope of 4"+ [ bench "known type" $ whnf (size . Foil.nameBinderListOf) tele4+ , bench "a dictionary" $ whnf listedSome (SomePattern tele4)+ ]+ , bgroup "generic pattern of 2"+ [ bench "known type" $ whnf (size . Foil.nameBinderListOf) pair+ , bench "a dictionary" $ whnf listedSome (SomePattern pair)+ ]+ , bgroup "generic pattern of 2 with gnameBinderListOf"+ [ bench "known type" $ whnf (size . Foil.nameBinderListOf) gpair+ , bench "a dictionary" $ whnf listedSome (SomePattern gpair)+ ]+ ]+ , bgroup "addSubstPattern, generic pattern of 2"+ [ bench "known type" $+ whnf (\p -> Foil.nullSubst (Foil.addSubstPattern Foil.identitySubst p args)) pair+ , bench "a dictionary" $ whnf (substSome args) (SomePattern pair)+ ]+ , bgroup "1000 nested generic patterns of 2"+ [ bench "alphaEquiv" $ whnf (alphaEquiv Foil.emptyScope chain) chain+ , bench "supportOf" $ whnf (Foil.nameSetSize . supportOf) chain+ ]+ ]
+ bench/nfdata/Main.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE GADTs #-}++-- | What it costs to force a term with 'rnf'.+--+-- Benchmarks force their results with 'rnf' (for example, through 'nf' of+-- tasty-bench), so the 'NFData' instance of 'AST' adds to every measurement+-- of a function that returns a term. The signature here takes the generic+-- 'NFData' instance, as user code usually does.+--+-- The workload is 100 random closed λ-terms of 4 to 32 nodes (about 1,850+-- nodes in total), comparable in size to the 100 normal forms of the+-- @random15@ corpus of [lambda-n-ways](https://github.com/sweirich/lambda-n-ways)+-- (Weirich's benchmark suite), and one random term of 20,000 nodes.+module Main (main) where++import Control.DeepSeq (NFData, force, rnf)+import Control.Exception (evaluate)+import Data.Bits (shiftR)+import Data.Word (Word64)+import GHC.Generics (Generic)+import Test.Tasty.Bench++import qualified Control.Monad.Foil as Foil+import Control.Monad.Free.Foil++data LamSig scope term+ = App term term+ | Lam scope+ deriving (Generic, NFData)++type Term = AST Foil.NameBinder LamSig++-- | A λ-term with de Bruijn indices, generated first and then converted.+data Raw = RVar Int | RApp Raw Raw | RLam Raw++-- | The linear congruential generator of Knuth's MMIX.+next :: Word64 -> Word64+next g = g * 6364136223846793005 + 1442695040888963407++-- | A number below @k@, from the high bits of the state.+pick :: Word64 -> Int -> Int+pick g k = fromIntegral ((g `shiftR` 33) `mod` fromIntegral k)++-- | @'gen' d s g@ is a random term of @s@ nodes under @d@ binders.+gen :: Int -> Int -> Word64 -> (Raw, Word64)+gen d s g0+ | s <= 1 && d > 0 = (RVar (pick g d), g)+ | d == 0 || s == 2 || pick g 100 < 50 =+ let (body, g') = gen (d + 1) (s - 1) g in (RLam body, g')+ | otherwise =+ let k = 1 + pick (next g) (s - 2)+ (fun, g1) = gen d k (next (next g))+ (arg, g2) = gen d (s - 1 - k) g1+ in (RApp fun arg, g2)+ where+ g = next g0++toTerm :: Foil.Distinct n => Foil.Scope n -> [Foil.Name n] -> Raw -> Term n+toTerm _ names (RVar i) = Var (names !! i)+toTerm scope names (RApp fun arg) = Node (App (toTerm scope names fun) (toTerm scope names arg))+toTerm scope names (RLam body) = Foil.withFresh scope $ \binder ->+ let scope' = Foil.extendScope binder scope+ in Node (Lam (ScopedAST binder (toTerm scope' (Foil.nameOf binder : map Foil.sink names) body)))++closed :: Raw -> Term Foil.VoidS+closed = toTerm Foil.emptyScope []++-- | 100 terms of 4 to 32 nodes.+corpus :: [Raw]+corpus = go (100 :: Int) 42+ where+ go 0 _ = []+ go k g =+ let (t, g') = gen 0 (4 + pick g 29) (next g)+ in t : go (k - 1) g'++main :: IO ()+main = do+ terms <- evaluate (force (map closed corpus))+ big <- evaluate (force (closed (fst (gen 0 20000 7))))+ defaultMain+ [ bench "rnf, 100 small terms" $ nf (foldr (\t r -> rnf t `seq` r) ()) terms+ , bench "rnf, one term of 20000 nodes" $ nf rnf big+ ]
bench/zipmatchk/Main.hs view
@@ -26,14 +26,21 @@ -- across the whole signature — as a real language's terms are — should cost the -- generic instance more the larger the signature is. The derived instance -- compiles to a single @case@, and should not care.+--+-- The last group measures the instances for 'Sum' and 'Product' of two+-- signatures (the data types à la carte of Swierstra), each with a derived+-- instance. module Main (main) where +import Data.Bifunctor.Product (Product (..))+import Data.Bifunctor.Sum (Sum (..)) import Data.Bifunctor.TH import Test.Tasty.Bench import qualified Control.Monad.Foil as Foil import Control.Monad.Free.Foil import Data.ZipMatchK+import Data.ZipMatchK.Bifunctor () import Data.ZipMatchK.TH (deriveZipMatchK) import Generics.Kind.TH (deriveGenericK) @@ -81,6 +88,35 @@ deriveBitraversable ''Sig44H deriveZipMatchK ''Sig44H +-- * Two signatures to combine++-- | Application alone.+data AppOnly scope term = AppOnly term term+ deriving (Functor, Foldable, Traversable)++-- | λ-abstraction alone.+newtype LamOnly scope term = LamOnly scope+ deriving (Functor, Foldable, Traversable)++-- | A tag with no children, to pair with every node of a signature.+data Tag scope term = Tag+ deriving (Functor, Foldable, Traversable)++deriveBifunctor ''AppOnly+deriveBifoldable ''AppOnly+deriveBitraversable ''AppOnly+deriveZipMatchK ''AppOnly++deriveBifunctor ''LamOnly+deriveBifoldable ''LamOnly+deriveBitraversable ''LamOnly+deriveZipMatchK ''LamOnly++deriveBifunctor ''Tag+deriveBifoldable ''Tag+deriveBitraversable ''Tag+deriveZipMatchK ''Tag+ -- * A large closed term -- | A closed term of the given depth: an application tree with a λ every other@@ -123,6 +159,10 @@ [ bench "generic" $ whnf (alphaEquiv Foil.emptyScope t44) t44 , bench "derived" $ whnf (alphaEquiv Foil.emptyScope u44) u44 ]+ , bgroup "two signatures"+ [ bench "Sum" $ whnf (alphaEquiv Foil.emptyScope s) s+ , bench "Product" $ whnf (alphaEquiv Foil.emptyScope p) p+ ] ] ] where@@ -132,3 +172,5 @@ u10 = mkTerm appSig10H lamSig10H depth t44 = mkTerm appSig44G lamSig44G depth u44 = mkTerm appSig44H lamSig44H depth+ s = mkTerm (\_ l r -> L2 (AppOnly l r)) (R2 . LamOnly) depth+ p = mkTerm (\d l r -> Pair (appSig2H d l r) Tag) (\scope -> Pair (lamSig2H scope) Tag) depth
free-foil.cabal view
@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.39.1.+-- This file has been generated from package.yaml by hpack version 0.37.0. -- -- see: https://github.com/sol/hpack name: free-foil-version: 0.5.0+version: 0.6.0 synopsis: Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads) description: Please see the README on GitHub at <https://github.com/fizruk/free-foil#readme> category: Parsing@@ -106,9 +106,11 @@ Control.Monad.Foil.BlocksSpec Control.Monad.Foil.ExampleLawsSpec Control.Monad.Foil.LawsSpec+ Control.Monad.Foil.NameBinderListOfSpec Control.Monad.Foil.NameMapSpec Control.Monad.Foil.NameRangeSpec Control.Monad.Foil.PatternTransportSpec+ Control.Monad.Foil.RolesSpec Control.Monad.Foil.SinkableSpec Control.Monad.Foil.TelescopeLawsSpec Control.Monad.Foil.UnifiablePatternSpec@@ -116,7 +118,9 @@ Control.Monad.Free.Foil.AlphaEquivSpec Control.Monad.Free.Foil.AnnotatedSpec Control.Monad.Free.Foil.ExampleSyntax+ Control.Monad.Free.Foil.HoistSpec Control.Monad.Free.Foil.LawsSpec+ Control.Monad.Free.Foil.NFDataSpec Control.Monad.Free.Foil.SupportSpec Control.Monad.Free.Foil.TH.MkFreeFoilSpec Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config@@ -125,6 +129,7 @@ Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsSyntax Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax Control.Monad.Free.Foil.TH.PatternTypesSpec+ Data.ZipMatchK.SumProductSpec Data.ZipMatchK.THSpec SpecHook Control.Monad.Foil.Laws@@ -149,6 +154,7 @@ , hspec-discover , kind-generics >=0.5.0 && <0.6 , kind-generics-th+ , should-not-typecheck >=2.1.0 && <2.2 , template-haskell >=2.21.0.0 && <2.24 , text >=1.2.3.1 && <2.2 default-language: Haskell2010@@ -160,6 +166,55 @@ Paths_free_foil hs-source-dirs: bench/alphaequiv+ ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -O2 -rtsopts+ build-depends:+ array >=0.5.3.0 && <0.6+ , base >=4.19 && <5+ , bifunctors >=5.5 && <5.7+ , binary ==0.8.*+ , bytestring >=0.11 && <0.13+ , containers >=0.6.8 && <0.9+ , deepseq >=1.4 && <1.6+ , free-foil+ , kind-generics >=0.5.0 && <0.6+ , tasty-bench+ , template-haskell >=2.21.0.0 && <2.24+ , text >=1.2.3.1 && <2.2+ default-language: Haskell2010++benchmark binders+ type: exitcode-stdio-1.0+ main-is: Main.hs+ other-modules:+ Config+ Generated+ Paths_free_foil+ hs-source-dirs:+ bench/binders+ ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -O2 -rtsopts+ build-depends:+ array >=0.5.3.0 && <0.6+ , base >=4.19 && <5+ , bifunctors >=5.5 && <5.7+ , binary ==0.8.*+ , bytestring >=0.11 && <0.13+ , containers >=0.6.8 && <0.9+ , deepseq >=1.4 && <1.6+ , free-foil+ , kind-generics >=0.5.0 && <0.6+ , kind-generics-th+ , tasty-bench+ , template-haskell >=2.21.0.0 && <2.24+ , text >=1.2.3.1 && <2.2+ default-language: Haskell2010++benchmark nfdata+ type: exitcode-stdio-1.0+ main-is: Main.hs+ other-modules:+ Paths_free_foil+ hs-source-dirs:+ bench/nfdata ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -O2 -rtsopts build-depends: array >=0.5.3.0 && <0.6
src/Control/Monad/Foil.hs view
@@ -116,7 +116,7 @@ withFreshNameBinderListIn, NameBinderList(..), nameBindersList,- nameBinderListOf,+ gnameBinderListOf, fromNameBindersList, snocNameBinderList, concatNameBinderLists,
src/Control/Monad/Foil/Blocks.hs view
@@ -2,6 +2,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wno-redundant-constraints #-}@@ -77,6 +78,7 @@ -- -- @since 0.4.0 data ExtWithin (n :: S) (l :: S) = UnsafeExtWithin [NameRange]+type role ExtWithin nominal nominal -- | The reservations an 'ExtWithin' is evidence about: sorted, disjoint, -- adjacent ranges coalesced, empty ones dropped.@@ -345,6 +347,7 @@ -- -- @since 0.4.0 data ScopeUnion (n :: S) (m :: S) (k :: S) = UnsafeScopeUnion+type role ScopeUnion nominal nominal nominal -- | Test that a scope is precisely the union of two others, and produce the -- witness if so. \(O(n+m)\).
src/Control/Monad/Foil/Internal.hs view
@@ -16,6 +16,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}@@ -85,12 +86,17 @@ -- @since 0.0.1 newtype Scope (n :: S) = UnsafeScope RawScope deriving newtype NFData+-- Scope indices are nominal here and in the other types below, so that+-- 'Data.Coerce.coerce' cannot change them unless the @Unsafe@ constructors+-- are in scope.+type role Scope nominal -- | A name in a safe scope, indexed by a type-level scope index @n@. -- -- @since 0.0.1 newtype Name (n :: S) = UnsafeName RawName deriving newtype (NFData, Eq, Ord, Show)+type role Name nominal -- | Convert 'Name' into an identifier. -- This may be useful for printing and debugging.@@ -105,6 +111,7 @@ newtype NameBinder (n :: S) (l :: S) = UnsafeNameBinder (Name l) deriving newtype (NFData, Eq, Ord, Show)+type role NameBinder nominal nominal -- | An empty scope (without any names). --@@ -209,7 +216,7 @@ -- @since 0.1.0 compNamesOf :: NamesOf n i o o' -> NamesOf i l o' o'' -> NamesOf n l o o'' compNamesOf (NamesOf xs) (NamesOf ys) =- NamesOf (coerce xs ++ ys)+ NamesOf (unsafeCoerce xs ++ ys) -- ** Refreshing binders @@ -367,7 +374,7 @@ -- variable. -- -- @since 0.0.1-{-# INLINABLE withRefreshedPattern #-}+{-# INLINE withRefreshedPattern #-} withRefreshedPattern :: (Distinct o, CoSinkable pattern, Sinkable e, InjectName e) => Scope o -- ^ Ambient scope.@@ -593,6 +600,7 @@ -- @since 0.4.0 newtype NameSet (n :: S) = UnsafeNameSet RawScope deriving newtype (NFData, Eq, Semigroup, Monoid)+type role NameSet nominal -- | An empty set of names. --@@ -660,6 +668,7 @@ -- | The names a pattern binds. -- -- @since 0.4.0+{-# INLINABLE nameSetOfPattern #-} nameSetOfPattern :: CoSinkable binder => binder n l -> NameSet l nameSetOfPattern binder = UnsafeNameSet bound where@@ -686,6 +695,7 @@ -- an occurrence of the outer name. -- -- @since 0.4.0+{-# INLINABLE unsinkNameSet #-} unsinkNameSet :: CoSinkable binder => binder n l -> NameSet l -> NameSet n unsinkNameSet binder (UnsafeNameSet names) = UnsafeNameSet (names IntSet.\\ bound) where@@ -940,6 +950,7 @@ -- -- @since 0.1.0 newtype NameBinders (n :: S) (l :: S) = UnsafeNameBinders IntSet+type role NameBinders nominal nominal -- | /Unsafely/ merge sets of binders (via set union). --@@ -1088,6 +1099,8 @@ withPattern withBinder unit comp scope (nameBindersList binders) $ \f binders' scope' -> cont f (fromNameBindersList binders') scope' + nameBinderListOf = nameBindersList+ instance CoSinkable NameBinderList where coSinkabilityProof rename NameBinderListEmpty cont = cont rename NameBinderListEmpty coSinkabilityProof rename (NameBinderListCons binder binders) cont =@@ -1095,14 +1108,36 @@ coSinkabilityProof rename' binders $ \rename'' binders' -> cont rename'' (NameBinderListCons binder' binders') - withPattern withBinder unit comp scope binders cont = case binders of- NameBinderListEmpty -> cont unit NameBinderListEmpty scope- NameBinderListCons x xs ->- withBinder scope x $ \f x' ->- let scope' = extendScope x' scope- in withPattern withBinder unit comp scope' xs $ \f' xs' scope'' ->- cont (comp f f') (NameBinderListCons x' xs') scope''+ withPattern+ :: forall o f n l r. Distinct o+ => (forall x y z r'. Distinct z => Scope z -> NameBinder x y -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')+ -> (forall x z z'. DExt z z' => f x x z z')+ -> (forall x y y' z z' z''. (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')+ -> Scope o+ -> NameBinderList n l+ -> (forall o'. DExt o o' => f n l o o' -> NameBinderList o o' -> Scope o' -> r)+ -> r+ withPattern withBinder unit comp = go+ where+ -- The loop takes the three functions from its context, so that a call+ -- with known functions specialises it when 'withPattern' inlines.+ go+ :: forall p i. Distinct p+ => Scope p+ -> NameBinderList i l+ -> (forall p'. DExt p p' => f i l p p' -> NameBinderList p p' -> Scope p' -> r)+ -> r+ go scope binders cont = case binders of+ NameBinderListEmpty -> cont unit NameBinderListEmpty scope+ NameBinderListCons x xs ->+ withBinder scope x $ \f x' ->+ let scope' = extendScope x' scope+ in go scope' xs $ \f' xs' scope'' ->+ cont (comp f f') (NameBinderListCons x' xs') scope''+ {-# INLINE withPattern #-} + nameBinderListOf = id+ -- ** Pattern combinators -- | An empty pattern type specifies zero possibilities for patterns.@@ -1121,6 +1156,7 @@ instance CoSinkable V2 where coSinkabilityProof _ v2 _ = absurd2 v2 withPattern _ _ _ _ v2 _ = absurd2 v2+ nameBinderListOf = absurd2 instance UnifiablePattern V2 where unifyPatterns = absurd2 @@ -1133,6 +1169,7 @@ instance CoSinkable U2 where coSinkabilityProof rename U2 cont = cont rename U2 withPattern _withBinder unit _combine scope U2 cont = cont unit U2 scope+ nameBinderListOf U2 = NameBinderListEmpty instance UnifiablePattern U2 where unifyPatterns U2 U2 = SameNameBinders emptyNameBinders @@ -1269,6 +1306,7 @@ -- an instance that checks the shape of two patterns first. -- -- @since 0.5.0+{-# INLINABLE unsafeUnifyPatternBinders #-} unsafeUnifyPatternBinders :: (CoSinkable pattern, Distinct n) => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r@@ -1670,7 +1708,30 @@ -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> Scope o' -> r) -> r withPattern = gunsafeWithPatternViaHasNameBinders+ -- Inlining the generic traversal lets a caller with known functions, such+ -- as the default 'nameBinderListOf', specialise it.+ {-# INLINE withPattern #-} + -- | Collect name binders of a generalized pattern into a name binder list,+ -- in the order 'withPattern' visits them.+ --+ -- The default collects them with 'withPattern'+ -- ('nameBinderListOfViaWithPattern'). It is cheap when the instance's+ -- 'withPattern' inlines into it, as the generic default does and as a+ -- non-recursive one marked @INLINE@ does. Otherwise it costs a traversal+ -- that allocates several closures per binder, and an instance should list+ -- its binders directly, as the instances that @mkCoSinkableFoilPattern@ and+ -- @mkFreeFoil@ generate do. An instance with the generic 'withPattern' can+ -- take 'gnameBinderListOf'.+ --+ -- This is a method of 'CoSinkable' since 0.6.0. Up to 0.5.0, it was a+ -- function outside the class, of the same type.+ --+ -- @since 0.2.0+ nameBinderListOf :: pattern n l -> NameBinderList n l+ nameBinderListOf = nameBinderListOfViaWithPattern+ {-# INLINE nameBinderListOf #-}+ -- ** Transporting a pattern's payloads -- | The renaming that carries a pattern's payloads into the ambient scope of@@ -1796,17 +1857,20 @@ compWithNameBinderList (WithNameBinderList f) (WithNameBinderList g) = WithNameBinderList (f . g) --- | Collect name binders of a generalized pattern into a name binder list,--- which can be more easily traversed.+-- | Collect the binders of a pattern with 'withPattern'. This is the default+-- of 'nameBinderListOf'. ----- @since 0.2.0-nameBinderListOf :: (CoSinkable binder) => binder n l -> NameBinderList n l-nameBinderListOf pat = withPattern+-- @since 0.6.0+{-# INLINE nameBinderListOfViaWithPattern #-}+nameBinderListOfViaWithPattern :: (CoSinkable binder) => binder n l -> NameBinderList n l+nameBinderListOfViaWithPattern pat = withPattern (\_scope' binder k -> unsafeAssertFresh binder $ \binder' -> k (WithNameBinderList (NameBinderListCons binder)) binder') idWithNameBinderList- compWithNameBinderList+ -- Unlike 'compWithNameBinderList', this builds the rest of the list first,+ -- so that no binder leaves a thunk behind.+ (\(WithNameBinderList f) (WithNameBinderList g) -> WithNameBinderList (\rest -> f $! g rest)) emptyScope pat (\(WithNameBinderList f) _ _ -> f NameBinderListEmpty)@@ -1815,6 +1879,8 @@ coSinkabilityProof _rename (UnsafeNameBinder name) cont = cont unsafeCoerce (UnsafeNameBinder name) + nameBinderListOf binder = NameBinderListCons binder NameBinderListEmpty+ withPattern withBinder _ _ scope binder cont = withBinder scope binder $ \f binder' -> cont f binder' (extendScope binder' scope)@@ -1827,6 +1893,7 @@ -- @since 0.0.1 newtype Substitution (e :: S -> Type) (i :: S) (o :: S) = UnsafeSubstitution (IntMap (e o))+type role Substitution representational nominal nominal -- | Apply substitution to a given name. --@@ -1874,6 +1941,7 @@ -- order the pattern binds them. -- -- @since 0.2.0+{-# INLINABLE addSubstPattern #-} addSubstPattern :: CoSinkable binder => Substitution e i o@@ -1923,6 +1991,7 @@ -- -- @since 0.0.1 newtype NameMap (n :: S) a = NameMap { getNameMap :: IntMap a } deriving (Functor, Foldable, Traversable)+type role NameMap nominal representational -- | An empty map belongs in the empty scope. --@@ -1959,6 +2028,7 @@ -- as there are binders in the input pattern (generalized binder). -- -- @since 0.2.0+{-# INLINABLE addNameBinders #-} addNameBinders :: CoSinkable binder => binder n l -> [a] -> NameMap n a -> NameMap l a addNameBinders pat = addNameBinderList (nameBinderListOf pat) @@ -2541,6 +2611,7 @@ -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> Scope o' -> r) -- ^ Continuation, accepting the result for the entire pattern, a (possibly refreshed) pattern, and the scope extended by that pattern. -> r+{-# INLINE gunsafeWithPatternViaHasNameBinders #-} gunsafeWithPatternViaHasNameBinders withBinder id_ comp_ scope pat cont = withPattern withBinder id_ comp_ scope (unsafeNameBinderListFromRaw raw) $ \result binders scope' -> cont result (gunsafeSetNameBinderList (unsafeCoerce pat) binders) scope' -- FIXME: safer version@@ -2548,6 +2619,22 @@ -- The binders in the order of the pattern. 'NameBinders' is a set, so -- going through it would put them back in ascending order of names. raw = ggetNameBindersRaw (fromK @_ @pattern @(n :&&: l :&&: LoT0) pat)++-- | 'nameBinderListOf' through the generic representation, without a+-- traversal by 'withPattern'. It lists the binders in the order of the+-- generic 'withPattern' ('gunsafeWithPatternViaHasNameBinders'), so an+-- instance that takes the generic default of 'withPattern' can use it:+--+-- > instance CoSinkable MyPattern where+-- > nameBinderListOf = gnameBinderListOf+--+-- @since 0.6.0+gnameBinderListOf+ :: forall pattern n l. (GenericK pattern, GHasNameBinders (RepK pattern))+ => pattern n l -> NameBinderList n l+gnameBinderListOf pat =+ unsafeNameBinderListFromRaw (ggetNameBindersRaw (fromK @_ @pattern @(n :&&: l :&&: LoT0) pat))+{-# INLINE gnameBinderListOf #-} -- | The binders of a pattern, in the order of the pattern, from their raw names. --
src/Control/Monad/Foil/TH/MkInstancesFoil.hs view
@@ -3,7 +3,11 @@ {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE TemplateHaskellQuotes #-} {-# OPTIONS_GHC -fno-warn-type-defaults #-}-module Control.Monad.Foil.TH.MkInstancesFoil where+module Control.Monad.Foil.TH.MkInstancesFoil (+ mkInstancesFoil,+ mkCoSinkableFoilPattern,+ deriveCoSinkable,+) where import Language.Haskell.TH @@ -23,7 +27,7 @@ TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT - coSinkablePatternD <- deriveCoSinkable nameT patternT+ coSinkablePatternD <- mkCoSinkableFoilPattern nameT patternT return $ [ InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilScopeT (map (VarT . tvarName) scopeTVars)))@@ -79,20 +83,26 @@ where xi = mkName ("x" ++ show i) --- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances.+-- | Generate the 'Foil.CoSinkable' instance of the pattern type that+-- 'Control.Monad.Foil.TH.MkFoilData.mkFoilPattern' generates from a raw+-- pattern type, given the raw types of identifiers and patterns.+-- 'deriveCoSinkable' takes the scope-safe pattern type itself. ----- @since 0.1.0-deriveCoSinkable+-- Up to 0.5.0, this was 'deriveCoSinkable'.+--+-- @since 0.6.0+mkCoSinkableFoilPattern :: Name -- ^ Type name for raw variable identifiers. -> Name -- ^ Type name for raw patterns. -> Q [Dec]-deriveCoSinkable nameT patternT = do+mkCoSinkableFoilPattern nameT patternT = do TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT return [ InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (PeelConT foilPatternT (map (VarT . tvarName) patternTVars))) [ FunD 'Foil.coSinkabilityProof (map clausePattern patternCons)- , FunD 'Foil.withPattern (map clauseWithPattern patternCons) ]+ , FunD 'Foil.withPattern (map clauseWithPattern patternCons)+ , FunD 'Foil.nameBinderListOf (map clauseNameBinderListOf patternCons) ] ] where@@ -132,6 +142,27 @@ where xi = mkName ("x" ++ show i) + -- The binders of the binding fields, in order, without going through+ -- 'Foil.withPattern'.+ clauseNameBinderListOf :: Con -> Clause+ clauseNameBinderListOf (NormalC conName params) =+ Clause [ConP foilConName [] conParamPatterns] (NormalB body) []+ where+ foilConName = mkName ("Foil" ++ nameBase conName)+ conParamPatterns = zipWith mkConParamPattern params [1 :: Int ..]+ mkConParamPattern (_bang, PeelConT tyName _)+ | tyName == nameT || tyName == patternT = VarP . xi+ mkConParamPattern _ = const WildP+ xi i = mkName ("x" ++ show i)+ binding =+ [ AppE (VarE 'Foil.nameBinderListOf) (VarE (xi i))+ | ((_bang, PeelConT tyName _), i) <- zip params [1 :: Int ..]+ , tyName == nameT || tyName == patternT ]+ body = case binding of+ [] -> ConE 'Foil.NameBinderListEmpty+ _ -> foldr1 (\l r -> foldl AppE (VarE 'Foil.concatNameBinderLists) [l, r]) binding+ clauseNameBinderListOf _ = error "Only normal constructors are supported here"+ clauseWithPattern :: Con -> Clause clauseWithPattern RecC{} = error "Record constructors (RecC) are not supported yet!" clauseWithPattern InfixC{} = error "Infix constructors (InfixC) are not supported yet!"@@ -169,3 +200,187 @@ go (i + 1) scope' rename' (AppE p (VarE xi)) conPatterns where xi = mkName ("x" ++ show i)++-- | Generate the 'Foil.CoSinkable' instance of a scope-safe pattern type.+-- 'mkCoSinkableFoilPattern' takes the raw pattern type instead.+--+-- > data Pat (n :: S) (l :: S) where+-- > PatVar :: NameBinder n l -> Pat n l+-- > PatPair :: NameBinder n i -> NameBinder i l -> Pat n l+-- >+-- > deriveCoSinkable ''Pat+--+-- A field is a 'Foil.NameBinder', a nested pattern, or a payload that+-- mentions no scope. A payload indexed by a scope needs a hand-written+-- instance (see 'Foil.transportPayload').+--+-- @since 0.6.0+deriveCoSinkable :: Name -> Q [Dec]+deriveCoSinkable patternT = do+ (tvars, cons) <- reify patternT >>= \case+ TyConI (DataD _ _ tvs _ cs _) -> return (tvs, cs)+ TyConI (NewtypeD _ _ tvs _ c _) -> return (tvs, [c])+ _ -> fail ("deriveCoSinkable: " ++ show patternT ++ " is not a data type")+ let params = map tvarName tvars+ if length params < 2+ then fail ("deriveCoSinkable: " ++ show patternT ++ " has fewer than two type parameters")+ else do+ fields <- concat <$> mapM (patternConFields patternT) cons+ coSinkClauses <- mapM patternCoSinkabilityProofClause fields+ withPatClauses <- mapM patternWithPatternClause fields+ listClauses <- mapM patternNameBinderListOfClause fields+ -- A pattern that nests itself has a recursive 'Foil.withPattern', which+ -- cannot inline.+ let recursive = or [ h == ConT patternT | (_, sorts) <- fields, PatternNested h <- sorts ]+ inline = [ PragmaD (InlineP 'Foil.withPattern Inline FunLike AllPhases) | not recursive ]+ return+ [ InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (foldl AppT (ConT patternT) (map VarT (take (length params - 2) params))))+ ([ FunD 'Foil.coSinkabilityProof coSinkClauses+ , FunD 'Foil.withPattern withPatClauses+ , FunD 'Foil.nameBinderListOf listClauses+ ] ++ inline)+ ]++-- | How a field of a pattern constructor takes part in its instance.+data PatternField+ = PatternBinder -- ^ A 'Foil.NameBinder'.+ | PatternNested Type -- ^ A nested pattern, with its own 'Foil.CoSinkable'; its type's head.+ | PatternPayload -- ^ A field that mentions no scope.++-- | The constructors of a pattern type, each with the sorts of its fields.+-- The scopes of a constructor are the last two arguments of its return type+-- and its existential variables, such as the intermediate scope of a pair.+patternConFields :: Name -> Con -> Q [(Name, [PatternField])]+patternConFields patternT = go []+ where+ go bound = \case+ NormalC conName _ -> fail ("deriveCoSinkable: constructor " ++ show conName+ ++ " of " ++ show patternT ++ " is not in GADT syntax, so its scopes are unknown")+ RecC conName _ -> go bound (NormalC conName [])+ InfixC _ conName _ -> go bound (NormalC conName [])+ ForallC tvs _ con -> go (bound ++ map tvarName tvs) con+ RecGadtC conNames types retType -> go bound (GadtC conNames (map removeName types) retType)+ GadtC conNames types retType -> do+ let (_, args) = unApplyType retType+ scopes = [ v | VarT v <- drop (length args - 2) args ] ++ bound+ sorts <- mapM (fieldSort scopes . snd) types+ return [ (conName, sorts) | conName <- conNames ]++ fieldSort scopes type_ =+ let (headT, args) = unApplyType type_+ mentions = any (`elem` scopes) (namesOfType type_)+ lastTwoScopes = case reverse args of+ VarT b : VarT a : _ -> a `elem` scopes && b `elem` scopes+ _ -> False+ in case headT of+ ConT n | n == ''Foil.NameBinder -> return PatternBinder+ _ | lastTwoScopes -> return (PatternNested headT)+ | not mentions -> return PatternPayload+ | otherwise -> fail ("deriveCoSinkable: a field of type " ++ pprint type_+ ++ " in " ++ show patternT ++ " mentions a scope; write the instance by hand"+ ++ " (transportPayload is the sanctioned way to rebuild such a field)")++-- | A type split into its head and arguments, without parentheses and kind+-- signatures.+unApplyType :: Type -> (Type, [Type])+unApplyType = go []+ where+ go acc (AppT f x) = go (x : acc) f+ go acc (ParensT t) = go acc t+ go acc (SigT t _) = go acc t+ go acc t = (t, acc)++-- | The type variables a type mentions.+namesOfType :: Type -> [Name]+namesOfType = \case+ VarT v -> [v]+ AppT f x -> namesOfType f ++ namesOfType x+ SigT t _ -> namesOfType t+ ParensT t -> namesOfType t+ AppKindT t _ -> namesOfType t+ _ -> []++isBindingField :: PatternField -> Bool+isBindingField = \case+ PatternPayload -> False+ _ -> True++-- | One 'Foil.coSinkabilityProof' clause: the binding fields are renamed in+-- turn, each with the renaming the previous one extended.+patternCoSinkabilityProofClause :: (Name, [PatternField]) -> Q Clause+patternCoSinkabilityProofClause (conName, sorts) = do+ rename <- newName (if any isBindingField sorts then "rename" else "_rename")+ cont <- newName "cont"+ xs <- mapM (\i -> newName ("x" ++ show i)) [1 .. length sorts]+ let go renameCur [] fields = return (VarE cont `AppE` VarE renameCur `AppE` foldl AppE (ConE conName) (fields []))+ go renameCur ((PatternPayload, x) : rest) fields = go renameCur rest (fields . (VarE x :))+ go renameCur ((_, x) : rest) fields = do+ renameNext <- newName "rename'"+ x' <- newName (nameBase x ++ "'")+ body <- go renameNext rest (fields . (VarE x' :))+ return (VarE 'Foil.coSinkabilityProof `AppE` VarE renameCur `AppE` VarE x+ `AppE` LamE [VarP renameNext, VarP x'] body)+ body <- go rename (zip sorts xs) id+ return (Clause [VarP rename, ConP conName [] (map VarP xs), VarP cont] (NormalB body) [])++-- | One 'Foil.withPattern' clause, in the form of+-- 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil': a binder field goes+-- through @withBinder@ and extends the scope for the fields to its right, a+-- nested pattern through its own 'Foil.withPattern', and the results compose+-- left to right.+patternWithPatternClause :: (Name, [PatternField]) -> Q Clause+patternWithPatternClause (conName, sorts) = do+ let nBinding = length (filter isBindingField sorts)+ hasNested = any (\case PatternNested _ -> True; _ -> False) sorts+ usedIf b n = if b then n else '_' : n+ withBinder <- newName (usedIf (nBinding > 0) "withBinder")+ unit_ <- newName (usedIf (nBinding == 0 || hasNested) "unit_")+ comp_ <- newName (usedIf (nBinding >= 2 || hasNested) "comp_")+ scope <- newName "scope"+ cont <- newName "cont"+ xs <- mapM (\i -> newName ("x" ++ show i)) [1 .. length sorts]+ let go scopeCur acc [] fields =+ return (VarE cont `AppE` maybe (VarE unit_) id acc+ `AppE` foldl AppE (ConE conName) (fields [])+ `AppE` VarE scopeCur)+ go scopeCur acc ((PatternPayload, x) : rest) fields = go scopeCur acc rest (fields . (VarE x :))+ go scopeCur acc ((sort_, x) : rest) fields = do+ x' <- newName (nameBase x ++ "'")+ f <- newName "f"+ scopeNext <- newName "scope'"+ let acc' = case acc of+ Nothing -> VarE f+ Just a -> VarE comp_ `AppE` a `AppE` VarE f+ body <- go scopeNext (Just acc') rest (fields . (VarE x' :))+ return $ case sort_ of+ PatternBinder ->+ VarE withBinder `AppE` VarE scopeCur `AppE` VarE x+ `AppE` LamE [VarP f, VarP x']+ (LetE [ValD (VarP scopeNext)+ (NormalB (VarE 'Foil.extendScope `AppE` VarE x' `AppE` VarE scopeCur)) []]+ body)+ _ ->+ VarE 'Foil.withPattern `AppE` VarE withBinder `AppE` VarE unit_+ `AppE` VarE comp_ `AppE` VarE scopeCur `AppE` VarE x+ `AppE` LamE [VarP f, VarP x', VarP scopeNext] body+ body <- go scope Nothing (zip sorts xs) id+ return (Clause+ [VarP withBinder, VarP unit_, VarP comp_, VarP scope, ConP conName [] (map VarP xs), VarP cont]+ (NormalB body) [])++-- | One 'Foil.nameBinderListOf' clause: the binding fields, left to right.+patternNameBinderListOfClause :: (Name, [PatternField]) -> Q Clause+patternNameBinderListOfClause (conName, sorts) = do+ xs <- mapM (\i -> newName ("x" ++ show i)) [1 .. length sorts]+ let pats = [ if isBindingField s then VarP x else WildP | (s, x) <- zip sorts xs ]+ -- A binder is consed on directly. Only a nested pattern's list is+ -- concatenated, since 'Foil.concatNameBinderLists' is recursive and+ -- copies its first argument.+ list = \case+ [] -> ConE 'Foil.NameBinderListEmpty+ [(PatternNested _, x)] -> VarE 'Foil.nameBinderListOf `AppE` VarE x+ (PatternNested _, x) : rest ->+ VarE 'Foil.concatNameBinderLists `AppE` (VarE 'Foil.nameBinderListOf `AppE` VarE x) `AppE` list rest+ (_, x) : rest -> ConE 'Foil.NameBinderListCons `AppE` VarE x `AppE` list rest+ body = list [ (s, x) | (s, x) <- zip sorts xs, isBindingField s ]+ return (Clause [ConP conName [] pats] (NormalB body) [])
src/Control/Monad/Foil/Telescope.hs view
@@ -62,6 +62,9 @@ -- with each payload moved by the transport and the scope reached /before/ its -- own binder. Moving a payload may refresh its own binders, which is why the -- instance needs @'RelMonad' 'Name' e@.+--+-- 'nameBinderListOf' is 'telescopeBinders', which reads the binders off the+-- telescope rather than rebuilding it with 'withPattern'. instance (Sinkable e, RelMonad Name e) => CoSinkable (Telescope label e) where coSinkabilityProof rename TelescopeEmpty cont = cont rename TelescopeEmpty coSinkabilityProof rename (TelescopeCons label payload binder rest) cont =@@ -103,6 +106,8 @@ (TelescopeCons label (transportPayload scope transport payload) binder' rest') scope'' + nameBinderListOf = telescopeBinders+ -- | Two telescopes unify when their binders line up and their payloads agree. -- -- Labels are ignored, which is what α-equivalence should do with a label: a@@ -221,15 +226,14 @@ -- | The chain of binders a telescope forms. ----- This is 'nameBinderListOf' at a telescope, written out. The general one--- goes through 'withPattern' and so rebuilds the telescope only to throw it--- away, which is worth avoiding on the checking path.+-- This is 'nameBinderListOf' at a telescope, as a function of its own, which+-- needs no 'RelMonad' instance for the payloads. -- -- @since 0.4.0 telescopeBinders :: Telescope label e n l -> NameBinderList n l telescopeBinders TelescopeEmpty = NameBinderListEmpty telescopeBinders (TelescopeCons _ _ binder rest) =- NameBinderListCons binder (telescopeBinders rest)+ NameBinderListCons binder $! telescopeBinders rest -- | Close a set of parameters under the parameters their payloads need. --
src/Control/Monad/Free/Foil.hs view
@@ -32,7 +32,6 @@ import Data.ZipMatchK import qualified Generics.Kind as Kind import Generics.Kind (GenericK(..), Field, Exists, Var0, Var1, (:$:), Atom((:@:), Kon), (:+:), (:*:))-import Data.Coerce (coerce) import Data.IntMap.Strict (IntMap) import qualified Data.IntMap.Strict as IntMap import Data.Map (Map)@@ -46,7 +45,9 @@ data ScopedAST binder sig n where ScopedAST :: binder n l -> AST binder sig l -> ScopedAST binder sig n +-- INLINABLE, so that it specialises together with the instance for AST. instance (forall x y. NFData (binder x y), forall l. NFData (AST binder sig l)) => NFData (ScopedAST binder sig n) where+ {-# INLINABLE rnf #-} rnf (ScopedAST binder body) = rnf binder `seq` rnf body -- | A term, generated by a signature 'Bifunctor' @sig@,@@ -60,9 +61,20 @@ Node :: sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n deriving instance Generic (AST binder sig n)-deriving instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))- => NFData (AST binder sig n) +-- | 'rnf' forces the names, the binders, and the nodes through the 'NFData'+-- instance of the signature. GHC specialises it where the binder and the+-- signature are known. On the λ-terms of the @nfdata@ benchmark, the+-- specialised 'rnf' is about four times faster than the general one.+instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))+ => NFData (AST binder sig n) where+ -- Without a specialisation, each node is forced through dictionaries built+ -- from the quantified constraints. The specialised rnf calls itself on the+ -- subterms and inlines the signature's rnf.+ {-# INLINABLE rnf #-}+ rnf (Var name) = rnf name+ rnf (Node node) = rnf node+ instance GenericK (ScopedAST binder sig) where type RepK (ScopedAST binder sig) = Exists Foil.S@@ -167,6 +179,7 @@ -- | Substitution for a single generalized pattern. -- -- @since 0.2.0+{-# INLINABLE substitutePattern #-} substitutePattern :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Scope o -- ^ Resulting scope.@@ -180,6 +193,47 @@ where env' = Foil.addSubstPattern env binders args +-- * Transformations between signatures++-- | Fold a term bottom-up into a scope-indexed carrier @r@. A variable goes+-- through the first function, a scoped subterm through the second, given its+-- binder and the fold of its body, and a node through the third, once its+-- subterms are folded. The scope indices stay as they are, so the carrier+-- can be another kind of term, as in 'hoistAST', or anything indexed by the+-- scope, such as @'Const' Int@ for a node count.+--+-- To change the binder type as well, map it in the second function:+--+-- > foldAST Var (\binder body -> ScopedAST (toBinder binder) body) Node+--+-- @since 0.6.0+{-# INLINABLE foldAST #-}+foldAST+ :: forall binder sig r s n. Bifunctor sig+ => (forall m. Foil.Name m -> r m) -- ^ A variable.+ -> (forall m l. binder m l -> r l -> s m) -- ^ A scoped subterm, from its binder and the fold of its body.+ -> (forall m. sig (s m) (r m) -> r m) -- ^ A node, its subterms folded.+ -> AST binder sig n+ -> r n+foldAST var scoped node = go+ where+ go :: forall m. AST binder sig m -> r m+ go (Var x) = var x+ go (Node t) = node (bimap (\(ScopedAST binder body) -> scoped binder (go body)) go t)++-- | Change the signature of a term by a natural transformation of+-- signatures, keeping the binders, as @hoistFree@ of the free package does+-- for a free monad. Each node is rebuilt, so this costs a traversal.+--+-- @since 0.6.0+{-# INLINABLE hoistAST #-}+hoistAST+ :: Bifunctor sig+ => (forall a b. sig a b -> sig' a b)+ -> AST binder sig n+ -> AST binder sig' n+hoistAST f = foldAST Var ScopedAST (Node . f)+ -- * \(\alpha\)-equivalence -- | Refresh (force) all binders in a term, minimizing the used indices.@@ -249,7 +303,7 @@ -> AST binder sig n -> AST binder sig n -> Bool-alphaEquiv _scope (Var x) (Var y) = x == coerce y+alphaEquiv _scope (Var x) (Var y) = x == y alphaEquiv scope (Node l) (Node r) = case zipMatchWith2 (unit . alphaEquivScoped scope) (unit . alphaEquiv scope) l r of Nothing -> False@@ -483,7 +537,7 @@ => AST binder sig n -> AST binder sig l -> Bool-unsafeEqAST (Var x) (Var y) = x == coerce y+unsafeEqAST (Var x) (Var y) = Foil.nameId x == Foil.nameId y unsafeEqAST (Node t1) (Node t2) = case zipMatchWith2 (unit . unsafeEqScopedAST) (unit . unsafeEqAST) t1 t2 of Nothing -> False
src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs view
@@ -8,20 +8,28 @@ module Control.Monad.Free.Foil.TH.MkFreeFoil ( FreeFoilConfig(..), FreeFoilTermConfig(..),+ FreeFoilOptions(..),+ defaultFreeFoilOptions, mkFreeFoil,+ mkFreeFoilWith, mkFreeFoilConversions, ) where import Language.Haskell.TH import Language.Haskell.TH.Syntax (addModFinalizer) -import Control.Monad (forM, forM_, when)+import Control.DeepSeq (NFData (..))+import Control.Monad (forM, forM_, unless, when) import qualified Control.Monad.Foil as Foil import Control.Monad.Foil.TH.Util import qualified Control.Monad.Free.Foil as Foil+import Data.Bifoldable (Bifoldable (..)) import Data.Bifunctor+import Data.Bitraversable (Bitraversable (..))+import Data.ZipMatchK (ZipMatchFoldK, ZipMatchK)+import Data.ZipMatchK.TH (zipMatchFoldKInstance, zipMatchKInstance) import Data.Char (toUpper)-import Data.List (find, unzip4, (\\), nub)+import Data.List (find, intercalate, unzip4, (\\), nub) import Data.Maybe (fromMaybe, isJust, catMaybes, listToMaybe, mapMaybe, maybeToList) import Data.Map (Map)@@ -566,6 +574,35 @@ [VarP withBinder, VarP unit_, VarP comp_, VarP scope, ConP conName [] (map VarP xs), VarP cont] (NormalB body) []) +-- | One 'Foil.nameBinderListOf' clause for a generated binding constructor:+--+-- > nameBinderListOf (Con x1 x2 _) =+-- > concatNameBinderLists (nameBinderListOf x1) (nameBinderListOf x2)+--+-- The binder and nested-pattern fields are listed left to right, in the order+-- in which the 'Foil.withPattern' clause of 'mkWithPatternClause' visits them,+-- and payload fields are skipped. A constructor that binds nothing lists no+-- binders.+mkNameBinderListOfClause :: FreeFoilConfig -> (Name, [Type]) -> Q Clause+mkNameBinderListOfClause config (rawConName, rawFieldTypes) = do+ let conName = toConName config rawConName+ sorts = map (bindingFieldSortOf config) rawFieldTypes+ xs <- mapM (\i -> newName ("x" <> show i)) [1 .. length sorts]+ let fieldPattern sort x+ | isBindingFieldSort sort = VarP x+ | otherwise = WildP+ -- A binder is consed on directly. Only a nested binding type's list is+ -- concatenated, since 'Foil.concatNameBinderLists' is recursive and+ -- copies its first argument.+ list = \case+ [] -> ConE 'Foil.NameBinderListEmpty+ [(FieldPattern, x)] -> VarE 'Foil.nameBinderListOf `AppE` VarE x+ (FieldPattern, x) : rest ->+ VarE 'Foil.concatNameBinderLists `AppE` (VarE 'Foil.nameBinderListOf `AppE` VarE x) `AppE` list rest+ (_, x) : rest -> ConE 'Foil.NameBinderListCons `AppE` VarE x `AppE` list rest+ body = list [ (sort, x) | (sort, x) <- zip sorts xs, isBindingFieldSort sort ]+ return (Clause [ConP conName [] (zipWith fieldPattern sorts xs)] (NormalB body) [])+ termConToPat :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [([Name], Pat, Pat, [Exp])] termConToPat rawTypeName config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go where@@ -909,6 +946,39 @@ ForallC _params _ctx con -> go con RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) +-- | Options of 'mkFreeFoilWith'.+--+-- @since 0.6.0+data FreeFoilOptions = FreeFoilOptions+ { signatureInstances :: [Name]+ -- ^ The classes whose instances every generated signature gets.+ -- 'Bifunctor', 'Bifoldable', 'Bitraversable' and 'NFData' come with+ -- @INLINE@ pragmas on the methods, and 'ZipMatchK' and 'ZipMatchFoldK' are+ -- written out as "Data.ZipMatchK.TH" derives them. All six are generated+ -- by default, since GHC does not inline the derived methods of a+ -- signature with about ten constructors or more, and every generic+ -- traversal of the syntax goes through them. Leave out the instances you write or derive+ -- yourself. With @[]@, none is generated. Any other class name is+ -- rejected by the splice, and so is 'Bitraversable' without its+ -- superclasses. The instances of the payload types, such as identifiers+ -- and positions, must be declared before the splice, since a later+ -- declaration group is not visible to it.+ , patternInstances :: [Name]+ -- ^ The classes whose instances every generated binding type gets:+ -- 'NFData' by default, written out. A binding type is a GADT whenever a+ -- constructor binds two names, which rules out the 'GHC.Generics.Generic'+ -- default. The same rules as for 'signatureInstances' apply.+ }++-- | The default options. Every instance is generated.+--+-- @since 0.6.0+defaultFreeFoilOptions :: FreeFoilOptions+defaultFreeFoilOptions = FreeFoilOptions+ { signatureInstances = [''Bifunctor, ''Bifoldable, ''Bitraversable, ''ZipMatchK, ''ZipMatchFoldK, ''NFData]+ , patternInstances = [''NFData]+ }+ -- | Generate scope-safe types and pattern synonyms for a given raw set of types: -- -- 1. Scope-safe quantified types (e.g. type schemas, defining equations of functions, unification constraints, data/type declarations)@@ -923,11 +993,20 @@ -- pattern has the runtime representation of the field it wraps. Otherwise the -- pattern type is @data@. --+-- Signatures are generated together with instances of 'Bitraversable',+-- 'ZipMatchK' and 'ZipMatchFoldK'. Use 'mkFreeFoilWith' to control which instances are generated.+-- -- @since 0.2.0 mkFreeFoil :: FreeFoilConfig -> Q [Dec]-mkFreeFoil config@FreeFoilConfig{..} = concat <$> sequence+mkFreeFoil = mkFreeFoilWith defaultFreeFoilOptions++-- | 'mkFreeFoil' with options.+--+-- @since 0.6.0+mkFreeFoilWith :: FreeFoilOptions -> FreeFoilConfig -> Q [Dec]+mkFreeFoilWith FreeFoilOptions{..} config@FreeFoilConfig{..} = checkSignatureInstances >> concat <$> sequence [ mapM mkQuantifiedType rawQuantifiedNames- , mapM mkBindingType freeFoilTermConfigs+ , concat <$> mapM mkBindingType freeFoilTermConfigs , concat <$> mapM mkPatternCoSinkable freeFoilTermConfigs , concat <$> mapM mkSignatureTypes freeFoilTermConfigs , concat <$> mapM mkPatternSynonyms freeFoilTermConfigs@@ -963,7 +1042,16 @@ ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A scope-safe version of '" ++ show rawName ++ "'.") return (DataD [] name newParams Nothing newCons []) - mkBindingType FreeFoilTermConfig{..} = do+ -- The binding type and, unless opted out, its instances.+ mkBindingType termConfig = do+ dec <- mkBindingType' termConfig+ instances <- case dec of+ DataD _ name params _ cons _ -> mkPatternInstances patternInstances name params cons+ NewtypeD _ name params _ con _ -> mkPatternInstances patternInstances name params [con]+ _ -> return []+ return (dec : instances)++ mkBindingType' FreeFoilTermConfig{..} = do (tvars, cons) <- reifyDataOrNewtype rawBindingName let bindingName = toFreeFoilName config rawBindingName rawRetType = PeelConT rawBindingName (map (VarT . tvarName) tvars)@@ -984,7 +1072,9 @@ -- GenericK default routes every binder operation through a generic -- representation traversal, which costs a measurable constant per binder -- at runtime (see issue #82); the concrete instance removes it, and a- -- client no longer declares (or hand-writes) the instance itself.+ -- client no longer declares (or hand-writes) the instance itself. The+ -- instance lists its binders directly in 'Foil.nameBinderListOf', since+ -- the default would go through the recursive 'Foil.withPattern'. mkPatternCoSinkable FreeFoilTermConfig{..} = do (tvars, cons) <- reifyDataOrNewtype rawBindingName let bindingName = toFreeFoilName config rawBindingName@@ -1002,10 +1092,12 @@ _ -> return () coSinkClauses <- mapM (mkCoSinkabilityProofClause config) flatCons withPatClauses <- mapM (mkWithPatternClause config) flatCons+ listClauses <- mapM (mkNameBinderListOfClause config) flatCons return [ InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) bindingT) [ FunD 'Foil.coSinkabilityProof coSinkClauses , FunD 'Foil.withPattern withPatClauses+ , FunD 'Foil.nameBinderListOf listClauses ] ] @@ -1014,7 +1106,29 @@ subsigs <- concat <$> mapM (mkSignatureType termConfig) (rawSubTermNames <> rawSubScopeNames) return (sig ++ subsigs) - mkSignatureType termConfig@FreeFoilTermConfig{..} rawName = do+ -- The signature with its synonyms and, unless opted out, its instances.+ mkSignatureType termConfig rawName = do+ decs <- mkSignatureType' termConfig rawName+ instances <- concat <$> sequence+ [ mkSignatureInstances signatureInstances name (map tvarName (take (length params - 2) params)) scope term cons+ | DataD _ name params _ cons _ <- decs ]+ return (decs ++ instances)++ checkSignatureInstances = do+ let unknown = filter (`notElem` supportedSignatureInstances) signatureInstances+ unless (null unknown) $ fail $ unlines+ [ "mkFreeFoilWith: cannot generate instances of " <> intercalate ", " (map show unknown)+ , " the signature instances it generates are " <> intercalate ", " (map show supportedSignatureInstances)+ ]+ let unknownPat = filter (`notElem` supportedPatternInstances) patternInstances+ unless (null unknownPat) $ fail $ unlines+ [ "mkFreeFoilWith: cannot generate instances of " <> intercalate ", " (map show unknownPat)+ , " the pattern instances it generates are " <> intercalate ", " (map show supportedPatternInstances)+ ]+ when (''Bitraversable `elem` signatureInstances && any (`notElem` signatureInstances) [''Bifunctor, ''Bifoldable]) $+ fail "mkFreeFoilWith: Bitraversable needs Bifunctor and Bifoldable among the signature instances"++ mkSignatureType' termConfig@FreeFoilTermConfig{..} rawName = do (tvars, cons) <- reifyDataOrNewtype rawName let sigName = toSignatureName config rawName tvars' = map (VarT . tvarName) tvars@@ -1057,6 +1171,211 @@ TyConI (DataD _ctx _name tvars _kind cons _deriv) -> return (tvars, cons) TyConI (NewtypeD _ctx _name tvars _kind con _deriv) -> return (tvars, [con]) _ -> error ("not a data or newtype: " ++ show name)++-- * Instances of a generated signature++-- | The shape of a field of a signature constructor, as far as its bifunctor+-- instances care. It is the scoped position, the term position, a type that+-- mentions neither, or a type constructor applied to one or two trailing+-- arguments that do, such as a list of terms or a sub-signature applied to+-- the scope and the term.+data SigField+ = SigPayload+ | SigScope+ | SigTerm+ | SigInside [SigField]++sigFieldShape :: Name -> Name -> Name -> Type -> Q SigField+sigFieldShape conName scope term fieldType = go fieldType+ where+ mentions t = sigMentions scope t || sigMentions term t+ go t = case sigStrip t of+ VarT v+ | v == scope -> return SigScope+ | v == term -> return SigTerm+ t' -> do+ let (_, args) = sigUnApply t'+ trailing = dropWhile (not . mentions) args+ case trailing of+ [] -> return SigPayload+ _ | length trailing <= 2 -> SigInside <$> mapM go trailing+ | otherwise -> fail $ unlines+ [ "mkFreeFoil: cannot generate the bifunctor instances of a signature:"+ , " constructor " <> show conName <> " has a field of type " <> pprint fieldType+ , " whose scope or term positions sit under a type constructor of arity above two;"+ , " leave the bifunctor classes out of signatureInstances (see mkFreeFoilWith)"+ , " and derive those instances yourself"+ ]++isSigPayload :: SigField -> Bool+isSigPayload SigPayload = True+isSigPayload _ = False++-- | The function to apply at a field under @bimap f g@, @bifoldMap f g@ and+-- @bitraverse f g@ respectively.+sigMapper, sigFolder, sigTraverser :: Exp -> Exp -> SigField -> Exp+sigMapper f g = \case+ SigPayload -> VarE 'id+ SigScope -> f+ SigTerm -> g+ SigInside [a] -> AppE (VarE 'fmap) (sigMapper f g a)+ SigInside [a, b] -> AppE (AppE (VarE 'bimap) (sigMapper f g a)) (sigMapper f g b)+ SigInside _ -> error "mkFreeFoil: a field of arity above two"+sigFolder f g = \case+ SigPayload -> AppE (VarE 'const) (VarE 'mempty)+ SigScope -> f+ SigTerm -> g+ SigInside [a] -> AppE (VarE 'foldMap) (sigFolder f g a)+ SigInside [a, b] -> AppE (AppE (VarE 'bifoldMap) (sigFolder f g a)) (sigFolder f g b)+ SigInside _ -> error "mkFreeFoil: a field of arity above two"+sigTraverser f g = \case+ SigPayload -> VarE 'pure+ SigScope -> f+ SigTerm -> g+ SigInside [a] -> AppE (VarE 'traverse) (sigTraverser f g a)+ SigInside [a, b] -> AppE (AppE (VarE 'bitraverse) (sigTraverser f g a)) (sigTraverser f g b)+ SigInside _ -> error "mkFreeFoil: a field of arity above two"++-- | The constructors of a generated signature with their fields.+sigConFields :: Con -> [(Name, [Type])]+sigConFields = \case+ GadtC names fields _ -> [ (n, map snd fields) | n <- names ]+ ForallC _ _ con -> sigConFields con+ NormalC n fields -> [(n, map snd fields)]+ RecC n fields -> [(n, [ t | (_, _, t) <- fields ])]+ _ -> []++-- | The classes 'mkSignatureInstances' knows.+supportedSignatureInstances :: [Name]+supportedSignatureInstances = [''Bifunctor, ''Bifoldable, ''Bitraversable, ''ZipMatchK, ''ZipMatchFoldK, ''NFData]++-- | The classes 'mkPatternInstances' knows.+supportedPatternInstances :: [Name]+supportedPatternInstances = [''NFData]++-- | An 'NFData' instance written out: one clause per constructor, forcing+-- every field in turn. The signatures get @INLINE@ on 'rnf', since theirs can+-- be large and is never self-recursive (the recursive positions are the type+-- variables); a binding type's is small and may be recursive, so it gets none.+nfDataInstance :: Bool -> Type -> [Type] -> [(Name, [Type])] -> Q Dec+nfDataInstance inline headT context fields = do+ clauses <- forM fields $ \(conName, types) -> do+ xs <- mapM (const (newName "x")) types+ let body = case xs of+ [] -> ConE '()+ _ -> foldr1 (\a b -> InfixE (Just a) (VarE 'seq) (Just b)) [ AppE (VarE 'rnf) (VarE x) | x <- xs ]+ return (Clause [ConP conName [] (map VarP xs)] (NormalB body) [])+ return (InstanceD Nothing context (AppT (ConT ''NFData) headT)+ ([ PragmaD (InlineP 'rnf Inline FunLike AllPhases) | inline ] ++ [FunD 'rnf clauses]))++-- | The fixed type parameters a field mentions, for an instance context.+usedParams :: [Name] -> [(Name, [Type])] -> [Name]+usedParams params fields = [ v | v <- params, any (any (sigMentions v) . snd) fields ]++-- | The requested instances of a generated binding type, out of 'NFData'.+mkPatternInstances :: [Name] -> Name -> [TyVarBndr BndrVis] -> [Con] -> Q [Dec]+mkPatternInstances wanted name params cons+ | ''NFData `elem` wanted, not (null fields) = do+ dec <- nfDataInstance False headT [ AppT (ConT ''NFData) (VarT v) | v <- usedParams fixed fields ] fields+ return [dec]+ | otherwise = return []+ where+ fields = concatMap sigConFields cons+ names = map tvarName params+ fixed = take (length names - 2) names+ headT = foldl AppT (ConT name) (map VarT names)++-- | The requested instances of a generated signature, out of 'Bifunctor',+-- 'Bifoldable' and 'Bitraversable', their methods marked @INLINE@,+-- 'ZipMatchK' and 'ZipMatchFoldK'. A signature without constructors gets none.+mkSignatureInstances :: [Name] -> Name -> [Name] -> Name -> Name -> [Con] -> Q [Dec]+mkSignatureInstances wanted sigName params scope term cons+ | null fields = return []+ | otherwise = do+ bifunctorDecs <-+ if any want [''Bifunctor, ''Bifoldable, ''Bitraversable]+ then mkBifunctorInstances+ else return []+ zipDecs <-+ if want ''ZipMatchK+ then zipMatchKInstance sigName (params ++ [scope, term]) 2 fields+ else return []+ zipFoldDecs <-+ if want ''ZipMatchFoldK+ then zipMatchFoldKInstance sigName (params ++ [scope, term]) 2 fields+ else return []+ nfDecs <-+ if want ''NFData+ then (: []) <$> nfDataInstance True (AppT (AppT headT (VarT scope)) (VarT term))+ -- Only the positions and parameters some field mentions: a+ -- signature without scoped positions gets no constraint on+ -- @scope@, which -Wredundant-constraints would otherwise flag.+ [ AppT (ConT ''NFData) (VarT v) | v <- usedParams (params ++ [scope, term]) fields ] fields+ else return []+ return (bifunctorDecs ++ zipDecs ++ zipFoldDecs ++ nfDecs)+ where+ fields = concatMap sigConFields cons+ want = (`elem` wanted)+ headT = foldl AppT (ConT sigName) (map VarT params)+ inline name = PragmaD (InlineP name Inline FunLike AllPhases)+ instanceOf cls decs = InstanceD Nothing [] (AppT (ConT cls) headT) decs++ mkBifunctorInstances = do+ shapes <- forM fields $ \(conName, types) ->+ (,) conName <$> mapM (sigFieldShape conName scope term) types+ -- Underscored, since a constructor may use neither function.+ f <- newName "_f"+ g <- newName "_g"+ let methodClause (conName, sh) mkBody = do+ xs <- mapM (const (newName "_x")) sh+ return (Clause [VarP f, VarP g, ConP conName [] (map VarP xs)] (NormalB (mkBody conName (zip sh xs))) [])+ at s x = AppE s (VarE x)+ bimapBody conName shxs = foldl AppE (ConE conName)+ [ if isSigPayload sh then VarE x else sigMapper (VarE f) (VarE g) sh `at` x | (sh, x) <- shxs ]+ bifoldBody _ shxs =+ case [ sigFolder (VarE f) (VarE g) sh `at` x | (sh, x) <- shxs, not (isSigPayload sh) ] of+ [] -> VarE 'mempty+ es -> foldr1 (\a b -> InfixE (Just a) (VarE '(<>)) (Just b)) es+ bitravBody conName shxs =+ case [ sigTraverser (VarE f) (VarE g) sh `at` x | (sh, x) <- shxs ] of+ [] -> AppE (VarE 'pure) (ConE conName)+ (e : es) -> foldl (\acc e' -> InfixE (Just acc) (VarE '(<*>)) (Just e'))+ (InfixE (Just (ConE conName)) (VarE '(<$>)) (Just e)) es+ bimapClauses <- mapM (`methodClause` bimapBody) shapes+ bifoldClauses <- mapM (`methodClause` bifoldBody) shapes+ bitravClauses <- mapM (`methodClause` bitravBody) shapes+ return $ concat+ [ [ instanceOf ''Bifunctor [inline 'bimap, FunD 'bimap bimapClauses] | want ''Bifunctor ]+ , [ instanceOf ''Bifoldable [inline 'bifoldMap, FunD 'bifoldMap bifoldClauses] | want ''Bifoldable ]+ , [ instanceOf ''Bitraversable [inline 'bitraverse, FunD 'bitraverse bitravClauses] | want ''Bitraversable ]+ ]++sigMentions :: Name -> Type -> Bool+sigMentions v = go+ where+ go = \case+ VarT u -> u == v+ AppT a b -> go a || go b+ AppKindT t _ -> go t+ SigT t _ -> go t+ ParensT t -> go t+ InfixT l _ r -> go l || go r+ UInfixT l _ r -> go l || go r+ ForallT _ _ t -> go t+ _ -> False++sigStrip :: Type -> Type+sigStrip (ParensT t) = sigStrip t+sigStrip (SigT t _) = sigStrip t+sigStrip t = t++sigUnApply :: Type -> (Type, [Type])+sigUnApply = go []+ where+ go args (AppT f x) = go (x : args) f+ go args (ParensT t) = go args t+ go args (SigT t _) = go args t+ go args t = (t, args) -- | Generate conversions to and from scope-safe representation: --
src/Data/ZipMatchK.hs view
@@ -13,6 +13,9 @@ module Data.ZipMatchK.Mappings, ZipMatchK(..), zipMatchK,+ ZipMatchFoldK(..),+ zipMatchAllK,+ zipMatchAnyK, -- * Specializations -- ** Unification of plain 'Data.Kind.Type's zipMatchViaEq,@@ -20,11 +23,19 @@ -- ** Unification of 'Data.Functor.Functor's zipMatchWith1, zipMatch1,+ zipMatchFold1,+ zipMatchAll1,+ zipMatchAny1, -- ** Unification of 'Data.Bifunctor.Bifunctor's zipMatchWith2, zipMatch2,+ zipMatchFold2,+ zipMatchAll2,+ zipMatchAny2, ) where +import Data.Coerce (coerce)+import Data.Monoid (All (..), Any (..)) import Generics.Kind import Data.Bitraversable @@ -92,3 +103,122 @@ -- @since 0.3.0 zipMatch2 :: (Bitraversable f, ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b')) zipMatch2 = zipMatchWith2 pairA pairA++-- | 'zipMatchFoldK' specialised to functors.+--+-- >>> zipMatchFold1 (\x y -> [x + y]) (Just 1) (Just (2 :: Int))+-- Just [3]+-- >>> zipMatchFold1 (\x y -> [x + y]) [1, 2] [10, 20 :: Int]+-- Just [11,22]+-- >>> zipMatchFold1 (\x y -> [x + y]) [1, 2] [10 :: Int]+-- Nothing+--+-- @since 0.6.0+zipMatchFold1+ :: (ZipMatchFoldK f, Monoid m)+ => (a -> a' -> m)+ -> f a -> f a' -> Maybe m+zipMatchFold1 f = zipMatchFoldK (f :%: F0)++-- | 'zipMatchFoldK' specialised to bifunctors. With 'Data.Monoid.All' it+-- checks that two nodes have the same constructor and that their components+-- satisfy a relation, without building anything for the components:+--+-- >>> import Data.Monoid (All (..))+-- >>> let same = zipMatchFold2 (\x y -> All (x == y)) (\x y -> All (x == y))+-- >>> getAll <$> same (Left 1) (Left (1 :: Int) :: Either Int Int)+-- Just True+-- >>> getAll <$> same (Left 1) (Left (2 :: Int) :: Either Int Int)+-- Just False+-- >>> getAll <$> same (Left 1) (Right (1 :: Int) :: Either Int Int)+-- Nothing+--+-- @since 0.6.0+zipMatchFold2+ :: (ZipMatchFoldK f, Monoid m)+ => (a -> a' -> m)+ -> (b -> b' -> m)+ -> f a b -> f a' b' -> Maybe m+zipMatchFold2 f g = zipMatchFoldK (f :%: g :%: F0)++-- | Check a relation on all paired components: 'Nothing' when the shapes+-- differ, as for 'zipMatchFoldK', and otherwise whether every component+-- satisfies its relation. The components are checked left to right, and the+-- check stops at the first that fails.+--+-- > zipMatchAllK = fmap getAll . zipMatchFoldK (coerce relations)+--+-- @since 0.6.0+zipMatchAllK :: forall f as bs. ZipMatchFoldK f => Folds Bool as bs -> f :@@: as -> f :@@: bs -> Maybe Bool+zipMatchAllK relations x y = getAll <$> zipMatchFoldK @_ @f @as @bs (coerce relations) x y+{-# INLINE zipMatchAllK #-}++-- | 'zipMatchAllK' specialised to functors.+--+-- >>> zipMatchAll1 (==) (Just 1) (Just (1 :: Int))+-- Just True+-- >>> zipMatchAll1 (==) [1, 2] [1, 3 :: Int]+-- Just False+-- >>> zipMatchAll1 (==) [1, 2] [1 :: Int]+-- Nothing+--+-- @since 0.6.0+zipMatchAll1 :: ZipMatchFoldK f => (a -> a' -> Bool) -> f a -> f a' -> Maybe Bool+zipMatchAll1 f = zipMatchAllK (f :%: F0)+{-# INLINE zipMatchAll1 #-}++-- | 'zipMatchAllK' specialised to bifunctors.+--+-- >>> zipMatchAll2 (==) (==) (Left 1) (Left (1 :: Int) :: Either Int Int)+-- Just True+-- >>> zipMatchAll2 (==) (==) (Left 1) (Right (1 :: Int) :: Either Int Int)+-- Nothing+--+-- @since 0.6.0+zipMatchAll2+ :: ZipMatchFoldK f+ => (a -> a' -> Bool)+ -> (b -> b' -> Bool)+ -> f a b -> f a' b' -> Maybe Bool+zipMatchAll2 f g = zipMatchAllK (f :%: g :%: F0)+{-# INLINE zipMatchAll2 #-}++-- | Check a relation on some paired component: 'Nothing' when the shapes+-- differ, as for 'zipMatchFoldK', and otherwise whether some component+-- satisfies its relation. The components are checked left to right, and the+-- check stops at the first that succeeds.+--+-- > zipMatchAnyK = fmap getAny . zipMatchFoldK (coerce relations)+--+-- @since 0.6.0+zipMatchAnyK :: forall f as bs. ZipMatchFoldK f => Folds Bool as bs -> f :@@: as -> f :@@: bs -> Maybe Bool+zipMatchAnyK relations x y = getAny <$> zipMatchFoldK @_ @f @as @bs (coerce relations) x y+{-# INLINE zipMatchAnyK #-}++-- | 'zipMatchAnyK' specialised to functors.+--+-- >>> zipMatchAny1 (==) [1, 2] [3, 2 :: Int]+-- Just True+-- >>> zipMatchAny1 (==) [1, 2] [3, 4 :: Int]+-- Just False+-- >>> zipMatchAny1 (==) [] [1 :: Int]+-- Nothing+--+-- @since 0.6.0+zipMatchAny1 :: ZipMatchFoldK f => (a -> a' -> Bool) -> f a -> f a' -> Maybe Bool+zipMatchAny1 f = zipMatchAnyK (f :%: F0)+{-# INLINE zipMatchAny1 #-}++-- | 'zipMatchAnyK' specialised to bifunctors.+--+-- >>> zipMatchAny2 (==) (==) (Right 1) (Right (2 :: Int) :: Either Int Int)+-- Just False+--+-- @since 0.6.0+zipMatchAny2+ :: ZipMatchFoldK f+ => (a -> a' -> Bool)+ -> (b -> b' -> Bool)+ -> f a b -> f a' b' -> Maybe Bool+zipMatchAny2 f g = zipMatchAnyK (f :%: g :%: F0)+{-# INLINE zipMatchAny2 #-}
src/Data/ZipMatchK/Bifunctor.hs view
@@ -8,13 +8,17 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-}--- | This module provides 'GenericK' and 'ZipMatchK' instances for 'Sum' and 'Product',+{-# LANGUAGE GADTs #-}+-- | This module provides 'GenericK', 'ZipMatchK' and 'ZipMatchFoldK' instances for 'Sum' and 'Product', -- to enable the use of 'ZipMatchK' with the data types à la carte approach.+--+-- The 'ZipMatchK' and 'ZipMatchFoldK' instances are written out, in the form that+-- "Data.ZipMatchK.TH" derives, rather than taken from the generic default,+-- which converts every node to its "Generics.Kind" representation and back. module Data.ZipMatchK.Bifunctor where import Data.Kind (Type) import Generics.Kind-import Data.Bitraversable import Data.Bifunctor.Sum import Data.Bifunctor.Product @@ -30,6 +34,27 @@ :*: Field ((Kon g :@: Var0) :@: Var1) -- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.-instance (Bitraversable f, Bitraversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type -> Type))+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type -> Type)) where+ zipMatchWithK mappings@(_ :^: _ :^: M0) l r = case (l, r) of+ (L2 x, L2 y) -> L2 <$> zipMatchWithK @_ @f mappings x y+ (R2 x, R2 y) -> R2 <$> zipMatchWithK @_ @g mappings x y+ _ -> Nothing+ -- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.-instance (Bitraversable f, Bitraversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type -> Type))+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type -> Type)) where+ zipMatchWithK mappings@(_ :^: _ :^: M0) (Pair x1 x2) (Pair y1 y2) =+ Pair <$> zipMatchWithK @_ @f mappings x1 y1 <*> zipMatchWithK @_ @g mappings x2 y2++-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.+instance (ZipMatchFoldK f, ZipMatchFoldK g) => ZipMatchFoldK (Sum f (g :: Type -> Type -> Type)) where+ {-# INLINE zipMatchFoldK #-}+ zipMatchFoldK folds@(_ :%: _ :%: F0) l r = case (l, r) of+ (L2 x, L2 y) -> zipMatchFoldK @_ @f folds x y+ (R2 x, R2 y) -> zipMatchFoldK @_ @g folds x y+ _ -> Nothing++-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.+instance (ZipMatchFoldK f, ZipMatchFoldK g) => ZipMatchFoldK (Product f (g :: Type -> Type -> Type)) where+ {-# INLINE zipMatchFoldK #-}+ zipMatchFoldK folds@(_ :%: _ :%: F0) (Pair x1 x2) (Pair y1 y2) =+ (<>) <$> zipMatchFoldK @_ @f folds x1 y1 <*> zipMatchFoldK @_ @g folds x2 y2
src/Data/ZipMatchK/Functor.hs view
@@ -8,8 +8,13 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-}--- | This module provides 'GenericK' and 'ZipMatchK' instances for 'Sum' and 'Product',+{-# LANGUAGE GADTs #-}+-- | This module provides 'GenericK', 'ZipMatchK' and 'ZipMatchFoldK' instances for 'Sum' and 'Product', -- to enable the use of 'ZipMatchK' with the data types à la carte approach.+--+-- The 'ZipMatchK' and 'ZipMatchFoldK' instances are written out, in the form that+-- "Data.ZipMatchK.TH" derives, rather than taken from the generic default,+-- which converts every node to its "Generics.Kind" representation and back. module Data.ZipMatchK.Functor where import Data.Kind (Type)@@ -28,7 +33,28 @@ Field (Kon f :@: Var0) :*: Field (Kon g :@: Var0) --- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.-instance (Traversable f, Traversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type))--- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.-instance (Traversable f, Traversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type))+-- | Note: instance is limited to 'Type'-kinded functors @f@ and @g@.+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type)) where+ zipMatchWithK mappings@(_ :^: M0) l r = case (l, r) of+ (InL x, InL y) -> InL <$> zipMatchWithK @_ @f mappings x y+ (InR x, InR y) -> InR <$> zipMatchWithK @_ @g mappings x y+ _ -> Nothing++-- | Note: instance is limited to 'Type'-kinded functors @f@ and @g@.+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type)) where+ zipMatchWithK mappings@(_ :^: M0) (Pair x1 x2) (Pair y1 y2) =+ Pair <$> zipMatchWithK @_ @f mappings x1 y1 <*> zipMatchWithK @_ @g mappings x2 y2++-- | Note: instance is limited to 'Type'-kinded functors @f@ and @g@.+instance (ZipMatchFoldK f, ZipMatchFoldK g) => ZipMatchFoldK (Sum f (g :: Type -> Type)) where+ {-# INLINE zipMatchFoldK #-}+ zipMatchFoldK folds@(_ :%: F0) l r = case (l, r) of+ (InL x, InL y) -> zipMatchFoldK @_ @f folds x y+ (InR x, InR y) -> zipMatchFoldK @_ @g folds x y+ _ -> Nothing++-- | Note: instance is limited to 'Type'-kinded functors @f@ and @g@.+instance (ZipMatchFoldK f, ZipMatchFoldK g) => ZipMatchFoldK (Product f (g :: Type -> Type)) where+ {-# INLINE zipMatchFoldK #-}+ zipMatchFoldK folds@(_ :%: F0) (Pair x1 x2) (Pair y1 y2) =+ (<>) <$> zipMatchFoldK @_ @f folds x1 y1 <*> zipMatchFoldK @_ @g folds x2 y2
src/Data/ZipMatchK/Generic.hs view
@@ -20,6 +20,7 @@ import Data.Kind (Constraint, Type) import Data.List.NonEmpty+import Data.Monoid (Ap (..)) import Generics.Kind import Generics.Kind.Examples () import GHC.TypeError@@ -56,6 +57,43 @@ => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs) zipMatchWithK = genericZipMatchWithK @f @as @bs @cs +-- | Kind-polymorphic syntactic matching of two values that folds the paired+-- components into a monoid instead of rebuilding the value.+--+-- 'zipMatchFoldK' answers 'Nothing' exactly when 'zipMatchWithK' with+-- functions that always succeed would: when the constructors differ, or a+-- component compared by its own 'ZipMatchK' differs. Otherwise it combines+-- the folding functions applied to the paired components, left to right with+-- '<>'. Nothing else is built, neither the matched value nor a pair per+-- component, so a check of all components (with 'Data.Monoid.All', say)+-- allocates nothing for the components and stops at the first one that+-- fails.+--+-- The default implementation is generic, via 'Generics.Kind.RepK', with the+-- costs described at 'ZipMatchK'. 'Data.ZipMatchK.TH.deriveZipMatchK' derives+-- a written-out instance together with the one of 'ZipMatchK'.+--+-- @since 0.6.0+class ZipMatchFoldK (f :: k) where+ -- | Perform one level of equality testing and fold the paired components.+ --+ -- @since 0.6.0+ zipMatchFoldK :: forall as bs m. Monoid m => Folds m as bs -> f :@@: as -> f :@@: bs -> Maybe m+ default zipMatchFoldK :: forall as bs m.+ (GenericK f, GZipMatchFold (RepK f), Monoid m)+ => Folds m as bs -> f :@@: as -> f :@@: bs -> Maybe m+ zipMatchFoldK = genericZipMatchFoldK @f @as @bs @m++-- | Generic implementation of 'zipMatchFoldK'.+--+-- @since 0.6.0+genericZipMatchFoldK :: forall f as bs m.+ (GenericK f, GZipMatchFold (RepK f), Monoid m)+ => Folds m as bs -> f :@@: as -> f :@@: bs -> Maybe m+genericZipMatchFoldK folds x y = gzipMatchFold folds+ (fromK @_ @f @as x)+ (fromK @_ @f @bs y)+ -- | Generic implementation of 'Data.ZipMatch.zipMatchK'. -- -- @since 0.2.0@@ -89,6 +127,14 @@ instance ZipMatchK a => ZipMatchK (Either a) instance ZipMatchK NonEmpty +instance ZipMatchFoldK (,)+instance ZipMatchK a => ZipMatchFoldK ((,) a)+instance ZipMatchFoldK []+instance ZipMatchFoldK Maybe+instance ZipMatchFoldK Either+instance ZipMatchK a => ZipMatchFoldK (Either a)+instance ZipMatchFoldK NonEmpty+ -- | What 'gzipMatchWith' requires when the components are paired up. -- -- @since 0.2.0@@ -235,3 +281,120 @@ :$$: 'ShowType (Eval a)) => ZipMatchFields (Eval a) where type ReqsZipMatchFieldsWith (Eval a) as bs cs = TypeError ('Text "Atom Eval is not supported by ZipMatchFields") zipMatchFieldsWith = undefined++-- | Folding matches on the "Generics.Kind" representation of a type, which is+-- what the default 'ZipMatchFoldK' instance goes through.+--+-- @since 0.6.0+class GZipMatchFold (f :: LoT k -> Type) where+ -- | Match two representations and fold their components with the given+ -- functions.+ --+ -- @since 0.6.0+ gzipMatchFold :: Monoid m => Folds m as bs -> f as -> f bs -> Maybe m++instance GZipMatchFold V1 where+ gzipMatchFold _ _ _ = error "impossible: Generics.Kind.V1 value!"++instance GZipMatchFold U1 where+ gzipMatchFold _ U1 U1 = Just mempty++instance GZipMatchFold f => GZipMatchFold (M1 i c f) where+ gzipMatchFold g (M1 x) (M1 y) = gzipMatchFold g x y++instance (GZipMatchFold f, GZipMatchFold g) => GZipMatchFold (f :+: g) where+ gzipMatchFold g (L1 x) (L1 y) = gzipMatchFold g x y+ gzipMatchFold g (R1 x) (R1 y) = gzipMatchFold g x y+ gzipMatchFold _ _ _ = Nothing++instance (GZipMatchFold f, GZipMatchFold g) => GZipMatchFold (f :*: g) where+ gzipMatchFold g (x :*: y) (x' :*: y') =+ liftA2 (<>) (gzipMatchFold g x x') (gzipMatchFold g y y')++instance ZipMatchFieldsFold t => GZipMatchFold (Field t) where+ gzipMatchFold = zipMatchFieldsFold++instance GZipMatchFold f => GZipMatchFold (c :=>: f) where+ gzipMatchFold g (SuchThat x) (SuchThat y) = gzipMatchFold g x y++instance TypeError ('Text "Existentials are not supported")+ => GZipMatchFold (Exists k f) where+ gzipMatchFold = undefined++-- | Folding matches of a single field of a constructor, by the shape of its+-- type. A field of a type that has no zipped parameter is compared by its+-- 'ZipMatchK' and contributes 'mempty'. A field of a type applied to zipped+-- parameters is folded by that type's 'ZipMatchFoldK'.+--+-- @since 0.6.0+class ZipMatchFieldsFold (t :: Atom d Type) where+ -- | Match two fields and fold their contents.+ --+ -- @since 0.6.0+ zipMatchFieldsFold :: Monoid m => Folds m as bs -> Field t as -> Field t bs -> Maybe m++instance ApplyMappings v => ZipMatchFieldsFold (Var v) where+ zipMatchFieldsFold g (Field x) (Field y) = Just (applyFolds @_ @v g x y)++instance ZipMatchK k => ZipMatchFieldsFold (Kon k) where+ zipMatchFieldsFold _ (Field l) (Field r) = mempty <$ zipMatchWithK @_ @k M0 l r++-- The components of a nested field can fail to match (two lists of different+-- lengths, say), so they are folded in @'Ap' 'Maybe' m@.+instance {-# OVERLAPPING #-} (ZipMatchFieldsFold t, ZipMatchFoldK k) => ZipMatchFieldsFold (Kon k :@: t) where+ zipMatchFieldsFold :: forall as bs m. Monoid m =>+ Folds m as bs -> Field (Kon k :@: t) as -> Field (Kon k :@: t) bs -> Maybe m+ zipMatchFieldsFold g (Field l) (Field r) =+ getAp =<< zipMatchFoldK @_ @k @(Interpret t as :&&: LoT0) @(Interpret t bs :&&: LoT0)+ ((\ll rr -> Ap (zipMatchFieldsFold g (Field ll :: Field t as) (Field rr :: Field t bs))) :%: F0) l r++instance {-# OVERLAPPING #-} (ZipMatchFieldsFold t1, ZipMatchFieldsFold t2, ZipMatchFoldK k) => ZipMatchFieldsFold ((Kon (k :: Type -> Type -> Type) :@: t1) :@: t2) where+ zipMatchFieldsFold :: forall as bs m. Monoid m =>+ Folds m as bs -> Field ((Kon k :@: t1) :@: t2) as -> Field ((Kon k :@: t1) :@: t2) bs -> Maybe m+ zipMatchFieldsFold g (Field l) (Field r) =+ getAp =<< zipMatchFoldK @_ @k @(Interpret t1 as :&&: Interpret t2 as :&&: LoT0) @(Interpret t1 bs :&&: Interpret t2 bs :&&: LoT0)+ ((\ll rr -> Ap (zipMatchFieldsFold g (Field ll :: Field t1 as) (Field rr :: Field t1 bs)))+ :%: ((\ll rr -> Ap (zipMatchFieldsFold g (Field ll :: Field t2 as) (Field rr :: Field t2 bs)))+ :%: F0)) l r++instance {-# OVERLAPPABLE #-} TypeError+ ('Text "The type constructor is kind-polymorphic:"+ :$$: 'Text " " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk -> Type)+ :$$: 'Text "Possible fix:"+ :$$: 'Text " add an explicit kind signature"+ :$$: 'Text " " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type))+ => ZipMatchFieldsFold (Kon (k :: kk -> Type) :@: t) where+ zipMatchFieldsFold = undefined++instance {-# OVERLAPPABLE #-} TypeError+ ('Text "The type constructor is kind-polymorphic:"+ :$$: 'Text " " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk1 -> kk2 -> Type)+ :$$: 'Text "Possible fix:"+ :$$: 'Text " add an explicit kind signature"+ :$$: 'Text " " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type -> Type))+ => ZipMatchFieldsFold ((Kon (k :: kk1 -> kk2 -> Type) :@: t1) :@: t2) where+ zipMatchFieldsFold = undefined++instance {-# OVERLAPPABLE #-} TypeError+ ('Text "Atom :@: is not supported by ZipMatchFieldsFold is a general form:"+ :$$: 'Text " when attempting to use a generic instance for"+ :$$: 'ShowType (f :@: t)+ :$$: 'ShowType f :<>: 'Text " : " :<>: 'ShowType (Atom d (k1 -> Type)))+ => ZipMatchFieldsFold ((f :: Atom d (k1 -> Type)) :@: t) where+ zipMatchFieldsFold = undefined++instance TypeError+ ('Text "Atom ForAll is not supported by ZipMatchFieldsFold"+ :$$: 'Text " when attempting to use a generic instance for"+ :$$: 'ShowType (ForAll a)) => ZipMatchFieldsFold (ForAll a) where+ zipMatchFieldsFold = undefined+instance TypeError+ ('Text "Atom :=>>: is not supported by ZipMatchFieldsFold"+ :$$: 'Text " when attempting to use a generic instance for"+ :$$: 'ShowType (c :=>>: a)) => ZipMatchFieldsFold (c :=>>: a) where+ zipMatchFieldsFold = undefined+instance TypeError+ ('Text "Atom Eval is not supported by ZipMatchFieldsFold"+ :$$: 'Text " when attempting to use a generic instance for"+ :$$: 'ShowType (Eval a)) => ZipMatchFieldsFold (Eval a) where+ zipMatchFieldsFold = undefined
src/Data/ZipMatchK/Mappings.hs view
@@ -35,6 +35,20 @@ -> Mappings as bs cs -- ^ Zipping for other type parameters. -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs) +infixr 5 :%:+type Folds :: Type -> LoT k -> LoT k -> Type+-- | A collection of folding functions for 'Data.ZipMatchK.zipMatchFoldK',+-- one per type parameter, each combining two components into a monoid.+--+-- @since 0.6.0+data Folds m (as :: LoT k) (bs :: LoT k) where+ -- | An empty collection (when there are no (more) type parameters).+ F0 :: Folds m LoT0 LoT0+ -- | A non-empty collection (when there is at least one type parameter).+ (:%:) :: (a -> b -> m) -- ^ Folding for the first type parameter.+ -> Folds m as bs -- ^ Folding for other type parameters.+ -> Folds m (a :&&: as) (b :&&: bs)+ -- | Type parameter lists that can be paired up componentwise. -- -- @since 0.2.0@@ -63,11 +77,22 @@ -> Interpret (Var v) bs -- ^ Second collection of values (one per type parameter). -> Maybe (Interpret (Var v) cs) + -- | Apply a collection of folding functions to collections of values.+ --+ -- @since 0.6.0+ applyFolds :: forall m (as :: LoT d) (bs :: LoT d).+ Folds m as bs -- ^ A collection of folding functions.+ -> Interpret (Var v) as -- ^ First collection of values (one per type parameter).+ -> Interpret (Var v) bs -- ^ Second collection of values (one per type parameter).+ -> m+ instance ApplyMappings (VZ :: TyVar (Type -> tys) Type) where applyMappings (f :^: _) x y = f x y+ applyFolds (f :%: _) x y = f x y instance ApplyMappings v => ApplyMappings (VS v :: TyVar (ty -> tys) Type) where applyMappings (_ :^: fs) x y = applyMappings @_ @v fs x y+ applyFolds (_ :%: fs) x y = applyFolds @_ @v fs x y -- | Pair two values in a context. --
src/Data/ZipMatchK/TH.hs view
@@ -1,7 +1,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE ViewPatterns #-}--- | Template Haskell derivation of 'ZipMatchK' instances.+-- | Template Haskell derivation of 'ZipMatchK' and 'ZipMatchFoldK' instances. -- -- The generic instance (the one obtained by writing @instance ZipMatchK TermSig@ -- with no body) converts a node into its "Generics.Kind" representation on@@ -35,6 +35,8 @@ deriveZipMatchK1, deriveZipMatchK2, deriveZipMatchKWith,+ zipMatchKInstance,+ zipMatchFoldKInstance, ) where import Data.List (foldl')@@ -42,10 +44,12 @@ import Language.Haskell.TH import Control.Monad.Foil.TH.Util (removeName, tvarName)-import Data.ZipMatchK.Generic (ZipMatchK (..))-import Data.ZipMatchK.Mappings (Mappings (..))+import Data.Monoid (Ap (..))+import Data.ZipMatchK.Generic (ZipMatchFoldK (..), ZipMatchK (..))+import Data.ZipMatchK.Mappings (Folds (..), Mappings (..)) --- | Derive a 'ZipMatchK' instance, zipping /all/ type parameters.+-- | Derive the 'ZipMatchK' and 'ZipMatchFoldK' instances, zipping /all/ type+-- parameters. -- -- For a signature bifunctor --@@ -59,6 +63,12 @@ -- > (AppSig l1 l2, AppSig r1 r2) -> AppSig <$> g l1 r1 <*> g l2 r2 -- > (LamSig l1, LamSig r1) -> LamSig <$> f l1 r1 -- > _ -> Nothing+-- >+-- > instance ZipMatchFoldK TermSig where+-- > zipMatchFoldK (f :%: g :%: F0) x y = case (x, y) of+-- > (AppSig l1 l2, AppSig r1 r2) -> Just (g l1 r1 <> g l2 r2)+-- > (LamSig l1, LamSig r1) -> Just (f l1 r1)+-- > _ -> Nothing -- -- Use 'deriveZipMatchK2' when the type has extra parameters that should stay -- fixed (an annotation, say), as a signature generated by@@ -68,15 +78,16 @@ deriveZipMatchK :: Name -> Q [Dec] deriveZipMatchK = deriveZipMatchKWith Nothing --- | Derive a 'ZipMatchK' instance for a functor, zipping the last type parameter--- and fixing the rest.+-- | Derive the 'ZipMatchK' and 'ZipMatchFoldK' instances for a functor, zipping+-- the last type parameter and fixing the rest. -- -- @since 0.3.2 deriveZipMatchK1 :: Name -> Q [Dec] deriveZipMatchK1 = deriveZipMatchKWith (Just 1) --- | Derive a 'ZipMatchK' instance for a signature bifunctor, zipping the last two--- type parameters (the scoped terms and the terms) and fixing the rest.+-- | Derive the 'ZipMatchK' and 'ZipMatchFoldK' instances for a signature+-- bifunctor, zipping the last two type parameters (the scoped terms and the+-- terms) and fixing the rest. -- -- For a signature with an extra parameter (a source position, for instance) --@@ -95,8 +106,8 @@ deriveZipMatchK2 :: Name -> Q [Dec] deriveZipMatchK2 = deriveZipMatchKWith (Just 2) --- | Derive a 'ZipMatchK' instance, zipping the last @n@ type parameters and--- fixing the rest. 'Nothing' zips all of them.+-- | Derive the 'ZipMatchK' and 'ZipMatchFoldK' instances, zipping the last @n@+-- type parameters and fixing the rest. 'Nothing' zips all of them. -- -- Every fixed parameter that occurs in a field gets a 'ZipMatchK' constraint in -- the instance context.@@ -113,32 +124,184 @@ then fail (show typeName ++ " has " ++ show (length params) ++ " type parameter(s), cannot zip the last " ++ show n) else do- let (fixed, zipped) = splitAt (length params - n) params- zippedSet = Set.fromList zipped+ let zippedSet = Set.fromList (drop (length params - n) params)+ fieldsOf <- concat <$> mapM (constructorFields params zippedSet) cons+ (++) <$> zipMatchKInstance typeName params n fieldsOf+ <*> zipMatchFoldKInstance typeName params n fieldsOf - -- One zipping function per zipped parameter, in order.- mappingVars <- mapM (const (newName "_f")) zipped- let mappings = zip zipped (map VarE mappingVars)- mappingsPat = foldr (\v p -> InfixP (VarP v) '(:^:) p) (ConP 'M0 [] []) mappingVars+-- | The 'ZipMatchK' instance of a data type, given its name, its type+-- parameters in order, how many of the last ones are zipped, and the fields+-- of each constructor in terms of those parameters. This is what+-- 'deriveZipMatchKWith' generates after reifying the type. It is for code+-- that declares the type in the same splice, such as+-- 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil', which cannot reify it.+--+-- @since 0.6.0+zipMatchKInstance :: Name -> [Name] -> Int -> [(Name, [Type])] -> Q [Dec]+zipMatchKInstance typeName params n fieldsOf = do+ let (fixed, zipped) = splitAt (length params - n) params+ zippedSet = Set.fromList zipped - fieldsOf <- concat <$> mapM (constructorFields params zippedSet) cons- clauses <- mapM (conClause zippedSet mappings) fieldsOf- let fallthrough- | length fieldsOf > 1 = [Match WildP (NormalB (ConE 'Nothing)) []]- | otherwise = []+ -- One zipping function per zipped parameter, in order.+ mappingVars <- mapM (const (newName "_f")) zipped+ let mappings = zip zipped (map VarE mappingVars)+ mappingsPat = foldr (\v p -> InfixP (VarP v) '(:^:) p) (ConP 'M0 [] []) mappingVars - x <- newName "x"- y <- newName "y"- let body = CaseE (TupE [Just (VarE x), Just (VarE y)]) (clauses ++ fallthrough)- impl = FunD 'zipMatchWithK- [Clause [mappingsPat, VarP x, VarP y] (NormalB body) []]+ clauses <- mapM (conClause zippedSet mappings) fieldsOf+ let fallthrough+ | length fieldsOf > 1 = [Match WildP (NormalB (ConE 'Nothing)) []]+ | otherwise = [] - headType = foldl' AppT (ConT typeName) (map VarT fixed)- usedVars = foldMap (foldMap freeVarsOfType . snd) fieldsOf- context = [ AppT (ConT ''ZipMatchK) (VarT v)- | v <- fixed, v `Set.member` usedVars ]+ x <- newName "x"+ y <- newName "y"+ let body = CaseE (TupE [Just (VarE x), Just (VarE y)]) (clauses ++ fallthrough)+ impl = FunD 'zipMatchWithK+ [Clause [mappingsPat, VarP x, VarP y] (NormalB body) []] - return [InstanceD Nothing context (AppT (ConT ''ZipMatchK) headType) [impl]]+ headType = foldl' AppT (ConT typeName) (map VarT fixed)+ usedVars = foldMap (foldMap freeVarsOfType . snd) fieldsOf+ context = [ AppT (ConT ''ZipMatchK) (VarT v)+ | v <- fixed, v `Set.member` usedVars ]++ return [InstanceD Nothing context (AppT (ConT ''ZipMatchK) headType) [impl]]++-- | The 'ZipMatchFoldK' instance of a data type, from the same arguments as+-- 'zipMatchKInstance'. A field of a zipped parameter contributes the result of+-- its folding function, a field of a type applied to zipped parameters is+-- folded by that type's 'ZipMatchFoldK', and any other field is compared by+-- its 'ZipMatchK' and contributes nothing. The contributions are combined with+-- '<>', nested to the right, so that a lazy monoid such as 'Data.Monoid.All'+-- stops at the first field that fails. The method is @INLINE@, so that at a+-- call site with a known monoid and known folding functions the match+-- compiles to a @case@ on the two values with the functions applied in place.+--+-- @since 0.6.0+zipMatchFoldKInstance :: Name -> [Name] -> Int -> [(Name, [Type])] -> Q [Dec]+zipMatchFoldKInstance typeName params n fieldsOf = do+ let (fixed, zipped) = splitAt (length params - n) params+ zippedSet = Set.fromList zipped++ -- One folding function per zipped parameter, in order.+ foldVars <- mapM (const (newName "_f")) zipped+ let folds = zip zipped (map VarE foldVars)+ foldsPat = foldr (\v p -> InfixP (VarP v) '(:%:) p) (ConP 'F0 [] []) foldVars++ clauses <- mapM (foldConClause zippedSet folds) fieldsOf+ let fallthrough+ | length fieldsOf > 1 = [Match WildP (NormalB (ConE 'Nothing)) []]+ | otherwise = []++ x <- newName "x"+ y <- newName "y"+ let body = CaseE (TupE [Just (VarE x), Just (VarE y)]) (clauses ++ fallthrough)+ impl = FunD 'zipMatchFoldK+ [Clause [foldsPat, VarP x, VarP y] (NormalB body) []]++ headType = foldl' AppT (ConT typeName) (map VarT fixed)+ types = concatMap snd fieldsOf+ needsZipMatchK = foldMap (zipMatchKVars zippedSet) types+ needsZipMatchFoldK = foldMap (zipMatchFoldKVars zippedSet) types+ context = [ AppT (ConT ''ZipMatchK) (VarT v) | v <- fixed, v `Set.member` needsZipMatchK ]+ ++ [ AppT (ConT ''ZipMatchFoldK) (VarT v) | v <- fixed, v `Set.member` needsZipMatchFoldK ]++ return [InstanceD Nothing context (AppT (ConT ''ZipMatchFoldK) headType)+ [PragmaD (InlineP 'zipMatchFoldK Inline FunLike AllPhases), impl]]++-- | How a field takes part in a folding match.+data FieldFolder+ = Total Exp -- ^ @l -> r -> m@: a zipped parameter.+ | Partial Exp -- ^ @l -> r -> Maybe m@: a type applied to zipped parameters.+ | Check Exp -- ^ @l -> r -> Maybe c@: a type without zipped parameters.++-- | Compile a field type into a 'FieldFolder', as 'fieldZipper' does for+-- 'zipMatchWithK'. The components of a nested type can fail to match, so when+-- one of them does, all of them are folded in @'Ap' 'Maybe' m@.+fieldFolder :: Set.Set Name -> [(Name, Exp)] -> Type -> Q FieldFolder+fieldFolder zipped folds type_ = case stripType type_ of+ VarT v | Just f <- lookup v folds -> return (Total f)+ t | not (mentionsZipped zipped t) -> return (Check (AppE (VarE 'zipMatchWithK) (ConE 'M0)))+ | otherwise -> do+ let (_headType, args) = unApply t+ zippedArgs = dropWhile (not . mentionsZipped zipped) args+ argFolders <- mapM (fieldFolder zipped folds) zippedArgs+ let list = foldr (\e m -> InfixE (Just e) (ConE '(:%:)) (Just m)) (ConE 'F0)+ total = [ e | Total e <- argFolders ]+ if length total == length argFolders+ then return (Partial (AppE (VarE 'zipMatchFoldK) (list total)))+ else do+ wrapped <- mapM inAp argFolders+ l <- newName "l"+ r <- newName "r"+ let call = AppE (AppE (AppE (VarE 'zipMatchFoldK) (list wrapped)) (VarE l)) (VarE r)+ return (Partial (LamE [VarP l, VarP r]+ (InfixE (Just (VarE 'getAp)) (VarE '(=<<)) (Just call))))+ where+ -- A folding function into @'Ap' 'Maybe' m@.+ inAp folder = do+ a <- newName "a"+ b <- newName "b"+ let applied e = AppE (AppE e (VarE a)) (VarE b)+ ap e = LamE [VarP a, VarP b] (AppE (ConE 'Ap) e)+ return $ case folder of+ Total e -> ap (AppE (ConE 'Just) (applied e))+ Partial e -> ap (applied e)+ Check e -> ap (InfixE (Just (VarE 'mempty)) (VarE '(<$)) (Just (applied e)))++-- | One @case@ alternative of 'zipMatchFoldK', matching a constructor with+-- itself: the fields that can fail are matched first, then the contributions+-- are combined.+foldConClause :: Set.Set Name -> [(Name, Exp)] -> (Name, [Type]) -> Q Match+foldConClause zipped folds (conName, types) = do+ lvars <- mapM (const (newName "l")) types+ rvars <- mapM (const (newName "r")) types+ folders <- mapM (fieldFolder zipped folds) types+ steps <- sequence+ [ case folder of+ Total f -> return (Nothing, Just (AppE (AppE f (VarE l)) (VarE r)))+ Partial f -> do+ m <- newName "m"+ return (Just (AppE (AppE f (VarE l)) (VarE r), VarP m), Just (VarE m))+ Check f ->+ return (Just (AppE (AppE f (VarE l)) (VarE r), WildP), Nothing)+ | (folder, (l, r)) <- zip folders (zip lvars rvars) ]+ let contributions = [ e | (_, Just e) <- steps ]+ combined = case contributions of+ [] -> VarE 'mempty+ _ -> foldr1 (\a b -> InfixE (Just a) (VarE '(<>)) (Just b)) contributions+ matchJust (scrutinee, pat) rest =+ CaseE scrutinee+ [ Match (ConP 'Nothing [] []) (NormalB (ConE 'Nothing)) []+ , Match (ConP 'Just [] [pat]) (NormalB rest) [] ]+ body = foldr matchJust (AppE (ConE 'Just) combined) [ c | (Just c, _) <- steps ]+ return (Match+ (TupP [ ConP conName [] (map VarP lvars)+ , ConP conName [] (map VarP rvars) ])+ (NormalB body) [])++-- | The fixed type parameters whose 'ZipMatchK' instance folding a field of+-- this type needs: those of a type without zipped parameters, and the fixed+-- arguments of a type applied to zipped ones.+zipMatchKVars :: Set.Set Name -> Type -> Set.Set Name+zipMatchKVars zipped type_ = case stripType type_ of+ VarT v | v `Set.member` zipped -> Set.empty+ t | not (mentionsZipped zipped t) -> freeVarsOfType t+ | otherwise ->+ let (_headType, args) = unApply t+ (fixedArgs, zippedArgs) = break (mentionsZipped zipped) args+ in foldMap freeVarsOfType fixedArgs <> foldMap (zipMatchKVars zipped) zippedArgs++-- | The fixed type parameters whose 'ZipMatchFoldK' instance folding a field of+-- this type needs: a parameter applied to zipped ones.+zipMatchFoldKVars :: Set.Set Name -> Type -> Set.Set Name+zipMatchFoldKVars zipped type_ = case stripType type_ of+ t | not (mentionsZipped zipped t) -> Set.empty+ | otherwise ->+ let (headType, args) = unApply t+ zippedArgs = dropWhile (not . mentionsZipped zipped) args+ here = case stripType headType of+ VarT v | null (takeWhile (not . mentionsZipped zipped) args) -> Set.singleton v+ _ -> Set.empty+ in here <> foldMap (zipMatchFoldKVars zipped) zippedArgs -- | The type parameters and constructors of a @data@ or @newtype@ declaration. reifyDataType :: Name -> Q ([TyVarBndr BndrVis], [Con])
+ test/Control/Monad/Foil/NameBinderListOfSpec.hs view
@@ -0,0 +1,151 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+-- The raw types below only serve Template Haskell.+{-# OPTIONS_GHC -Wno-unused-top-binds #-}+-- | The laws of 'Foil.CoSinkable', with the agreement of+-- 'Foil.nameBinderListOf' and 'Foil.withPattern', for the ways to get an+-- instance that no other suite covers: 'mkCoSinkableFoilPattern',+-- 'deriveCoSinkable' and the generic defaults of this package. The+-- pattern types consist of wildcards, variables and pairs, so that the+-- binders of a pattern come from fields at different depths. One more pattern+-- type binds two names in one constructor, next to a payload.+module Control.Monad.Foil.NameBinderListOfSpec (spec) where++import Test.Hspec+import Test.QuickCheck++import qualified Control.Monad.Foil as Foil+-- 'mkCoSinkableFoilPattern' binds a variable named @rename@.+import Control.Monad.Foil.Laws hiding (rename)+import Control.Monad.Foil.TH (deriveCoSinkable, mkCoSinkableFoilPattern, mkFoilPattern)+import Generics.Kind.TH (deriveGenericK)++-- | A raw pattern, from which 'mkFoilPattern' and 'mkCoSinkableFoilPattern' generate+-- 'FoilRawPattern' and its instance, which lists its binders directly.+newtype RawIdent = RawIdent String+data RawPattern+ = RawPatternWild+ | RawPatternVar RawIdent+ | RawPatternPair RawPattern RawPattern++mkFoilPattern ''RawIdent ''RawPattern+mkCoSinkableFoilPattern ''RawIdent ''RawPattern++-- | A scope-safe pattern whose instance 'deriveCoSinkable' generates.+data DerivedPattern (n :: Foil.S) (l :: Foil.S) where+ DerivedPatternWild :: DerivedPattern n n+ DerivedPatternVar :: Foil.NameBinder n l -> DerivedPattern n l+ DerivedPatternPair :: DerivedPattern n i -> DerivedPattern i l -> DerivedPattern n l++deriveCoSinkable ''DerivedPattern++-- | A scope-safe pattern that binds two names in one constructor, next to a+-- payload, as a pattern for a pair or a recursor might.+data TwoPattern (n :: Foil.S) (l :: Foil.S) where+ TwoPatternVar :: Foil.NameBinder n l -> TwoPattern n l+ TwoPatternPair :: Int -> Foil.NameBinder n i -> Foil.NameBinder i l -> TwoPattern n l++deriveCoSinkable ''TwoPattern++-- | A pattern whose instances are the generic defaults.+data GenericPattern (n :: Foil.S) (l :: Foil.S) where+ GenericPatternWild :: GenericPattern n n+ GenericPatternVar :: Foil.NameBinder n l -> GenericPattern n l+ GenericPatternPair :: GenericPattern n i -> GenericPattern i l -> GenericPattern n l++deriveGenericK ''GenericPattern+instance Foil.SinkableK GenericPattern+instance Foil.HasNameBinders GenericPattern+instance Foil.CoSinkable GenericPattern++spec :: Spec+spec = do+ describe "a pattern from mkCoSinkableFoilPattern" $+ coSinkableSpec rawPatternNames genRawPattern extensionByCoercion+ describe "a pattern from deriveCoSinkable" $+ coSinkableSpec derivedPatternNames genDerivedPattern extensionByCoercion+ describe "a pattern with two binders and a payload, from deriveCoSinkable" $+ coSinkableSpec twoPatternNames genTwoPattern extensionByCoercion+ describe "a pattern with the generic defaults" $ do+ coSinkableSpec genericPatternNames genGenericPattern extensionByCoercion+ it "gnameBinderListOf lists the binders in the order of withPattern" $+ forAllShow (genPatternCase genGenericPattern Inclusions) (showPatternCase genericPatternNames) $+ \(PatternCase _ p) ->+ nameBinderListNames (Foil.gnameBinderListOf p) === patternRawNames p++-- | The shape of a pattern: where the wildcards, variables and pairs are. This+-- follows the generators of "Control.Monad.Free.Foil.TH.PatternTypesSpec".+data Shape = Wildcard | Variable | Pair Shape Shape++-- | A shape of nesting depth at most @d@.+genShape :: Int -> Gen Shape+genShape d = frequency $+ [ (1, pure Wildcard), (3, pure Variable) ] +++ [ (2, Pair <$> genShape (d - 1) <*> genShape (d - 1)) | d > 0 ]++-- | A pattern of a random shape, built with the given constructors.+genShaped+ :: forall p. Foil.CoSinkable p+ => (forall n. p n n)+ -> (forall n l. Foil.NameBinder n l -> p n l)+ -> (forall n i l. p n i -> p i l -> p n l)+ -> GenPattern p+genShaped wild var pair ctx = withCtx ctx $ \scope -> do+ shape <- genShape 2+ go shape scope+ where+ go :: Foil.Distinct m => Shape -> Foil.Scope m -> Gen (PatIn p m)+ go shape scope = case shape of+ Wildcard -> pure (PatIn wild)+ Variable -> withHintedBinder scope (pure . PatIn . var)+ Pair left right -> do+ PatIn l <- go left scope+ PatIn r <- go right (Foil.extendScopePattern l scope)+ pure (PatIn (pair l r))++rawPatternNames :: PatternNames FoilRawPattern+rawPatternNames = \case+ FoilRawPatternWild -> []+ FoilRawPatternVar b -> [Foil.nameId (Foil.nameOf b)]+ FoilRawPatternPair l r -> rawPatternNames l ++ rawPatternNames r++genRawPattern :: GenPattern FoilRawPattern+genRawPattern = genShaped FoilRawPatternWild FoilRawPatternVar FoilRawPatternPair++genericPatternNames :: PatternNames GenericPattern+genericPatternNames = \case+ GenericPatternWild -> []+ GenericPatternVar b -> [Foil.nameId (Foil.nameOf b)]+ GenericPatternPair l r -> genericPatternNames l ++ genericPatternNames r++genGenericPattern :: GenPattern GenericPattern+genGenericPattern = genShaped GenericPatternWild GenericPatternVar GenericPatternPair++derivedPatternNames :: PatternNames DerivedPattern+derivedPatternNames = \case+ DerivedPatternWild -> []+ DerivedPatternVar b -> [Foil.nameId (Foil.nameOf b)]+ DerivedPatternPair l r -> derivedPatternNames l ++ derivedPatternNames r++genDerivedPattern :: GenPattern DerivedPattern+genDerivedPattern = genShaped DerivedPatternWild DerivedPatternVar DerivedPatternPair++twoPatternNames :: PatternNames TwoPattern+twoPatternNames = \case+ TwoPatternVar b -> [Foil.nameId (Foil.nameOf b)]+ TwoPatternPair _ x y -> [Foil.nameId (Foil.nameOf x), Foil.nameId (Foil.nameOf y)]++genTwoPattern :: GenPattern TwoPattern+genTwoPattern ctx = withCtx ctx $ \scope -> oneof+ [ withHintedBinder scope (pure . PatIn . TwoPatternVar)+ , withHintedBinder scope $ \x ->+ withHintedBinder (Foil.extendScope x scope) $ \y -> do+ k <- arbitrary+ pure (PatIn (TwoPatternPair k x y))+ ]
+ test/Control/Monad/Foil/RolesSpec.hs view
@@ -0,0 +1,157 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE MonoLocalBinds #-}+{-# OPTIONS_GHC -fdefer-type-errors -Wno-deferred-type-errors #-}++-- | The scope indices of the foil's types are nominal, so 'coerce' cannot+-- change them, while 'sink' and coercions that keep the scope still work.+--+-- The rejected coercions are checked with 'shouldNotTypecheck' from the+-- @should-not-typecheck@ package, which needs this module to be compiled+-- with @-fdefer-type-errors@. The module imports only the public modules,+-- where the @Unsafe@ constructors are not in scope: with them, 'coerce'+-- would still unwrap the newtypes and succeed.+module Control.Monad.Foil.RolesSpec (spec) where++import Data.Coerce (coerce)+import Data.Foldable (toList)+import Data.Monoid (Sum (..))+import Test.Hspec+import Test.ShouldNotTypecheck (shouldNotTypecheck)++import Control.Monad.Foil+import Control.Monad.Foil.Blocks++-- * Coercions that change a scope index (none of these typecheck)++-- | A name moves to an unrelated scope.+anyName :: Name n -> Name l+anyName = coerce++-- | A name of the inner scope escapes its binder.+escapeName :: NameBinder n l -> Name l -> Name n+escapeName _ = coerce++binderOuter :: NameBinder n l -> NameBinder n' l+binderOuter = coerce++binderInner :: NameBinder n l -> NameBinder n l'+binderInner = coerce++anyScope :: Scope n -> Scope l+anyScope = coerce++anyNameSet :: NameSet n -> NameSet l+anyNameSet = coerce++substDomain :: Substitution e i o -> Substitution e i' o+substDomain = coerce++nameBindersOuter :: NameBinders n l -> NameBinders n' l+nameBindersOuter = coerce++nameBindersInner :: NameBinders n l -> NameBinders n l'+nameBindersInner = coerce++anyNameMap :: NameMap n a -> NameMap l a+anyNameMap = coerce++extWithinOuter :: ExtWithin n l -> ExtWithin n' l+extWithinOuter = coerce++extWithinInner :: ExtWithin n l -> ExtWithin n l'+extWithinInner = coerce++blockOuter :: Block c l -> Block c' l+blockOuter = coerce++blockInner :: Block c l -> Block c l'+blockInner = coerce++scopeUnionLeft :: ScopeUnion n m k -> ScopeUnion n' m k+scopeUnionLeft = coerce++scopeUnionRight :: ScopeUnion n m k -> ScopeUnion n m' k+scopeUnionRight = coerce++scopeUnionWhole :: ScopeUnion n m k -> ScopeUnion n m k'+scopeUnionWhole = coerce++-- | The value does not typecheck. Weak head normal form is enough to raise+-- the deferred type error of a 'coerce', and not every type here has an+-- 'Control.DeepSeq.NFData' instance, so the value is forced with 'seq'.+rejected :: a -> Expectation+rejected x = shouldNotTypecheck (x `seq` ())++-- * Coercions that keep the scope (these typecheck)++-- | A user newtype over names, as a generated single-binder pattern is.+newtype Var n = Var (Name n)++toVar :: Name n -> Var n+toVar = coerce++valuesAsSum :: NameMap n Int -> NameMap n (Sum Int)+valuesAsSum = coerce++-- | 'sink', with the target scope pinned by a binder the caller holds.+sunkVia :: (Sinkable e, DExt n l) => NameBinder n l -> e n -> e l+sunkVia _ = sink++sunk1Via :: (Functor f, Sinkable e, DExt n l) => NameBinder n l -> f (e n) -> f (e l)+sunk1Via _ = sink1++spec :: Spec+spec = do+ describe "coerce cannot change a scope index" $ do+ it "of a Name" $+ withFresh emptyScope $ \x -> rejected (nameId (anyName (nameOf x)))+ it "of a Name bound by a NameBinder (escaping the binder)" $+ withFresh emptyScope $ \x -> rejected (nameId (escapeName x (nameOf x)))+ it "of a NameBinder (the outer scope)" $+ withFresh emptyScope $ \x -> rejected (nameId (nameOf (binderOuter x)))+ it "of a NameBinder (the inner scope)" $+ withFresh emptyScope $ \x -> rejected (nameId (nameOf (binderInner x)))+ it "of a Scope" $+ rejected (anyScope emptyScope)+ it "of a NameSet" $+ withFresh emptyScope $ \x -> rejected (anyNameSet (nameSetSingleton (nameOf x)))+ it "of a Substitution (the domain)" $+ rejected (substDomain (voidSubst :: Substitution Name VoidS VoidS))+ it "of NameBinders (the outer scope)" $+ rejected (nameBindersOuter (emptyNameBinders :: NameBinders VoidS VoidS))+ it "of NameBinders (the inner scope)" $+ rejected (nameBindersInner (emptyNameBinders :: NameBinders VoidS VoidS))+ it "of a NameMap" $+ rejected (anyNameMap (emptyNameMap :: NameMap VoidS Char))+ it "of ExtWithin (the outer scope)" $+ rejected (extWithinOuter (extWithinRefl (NameRange 0 9) :: ExtWithin VoidS VoidS))+ it "of ExtWithin (the inner scope)" $+ rejected (extWithinInner (extWithinRefl (NameRange 0 9) :: ExtWithin VoidS VoidS))+ it "of a Block (the outer scope)" $+ rejected (blockOuter (beginBlock (NameRange 0 9) :: Block VoidS VoidS))+ it "of a Block (the inner scope)" $+ rejected (blockInner (beginBlock (NameRange 0 9) :: Block VoidS VoidS))+ it "of a ScopeUnion (each of the three scopes)" $+ case checkScopeUnion emptyScope emptyScope emptyScope of+ Nothing -> expectationFailure "the empty scope is the union of two empty scopes"+ Just u -> do+ rejected (scopeUnionLeft u)+ rejected (scopeUnionRight u)+ rejected (scopeUnionWhole u)++ describe "scope changes that remain possible" $ do+ it "sink moves a name to an extended scope" $+ withFresh emptyScope $ \x ->+ withFresh (extendScope x emptyScope) $ \y ->+ nameId (sunkVia y (nameOf x)) `shouldBe` nameId (nameOf x)+ it "sink1 moves a list of names to an extended scope" $+ withFresh emptyScope $ \x ->+ withFresh (extendScope x emptyScope) $ \y ->+ map nameId (sunk1Via y [nameOf x]) `shouldBe` [nameId (nameOf x)]+ it "coerce wraps a name in a user newtype, keeping its scope" $+ withFresh emptyScope $ \x ->+ case toVar (nameOf x) of+ Var x' -> nameId x' `shouldBe` nameId (nameOf x)+ it "coerce changes the values of a NameMap, keeping its scope" $+ withFresh emptyScope $ \x ->+ map getSum (toList (valuesAsSum (addNameBinder x 1 emptyNameMap))) `shouldBe` [1]
+ test/Control/Monad/Free/Foil/HoistSpec.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+-- | 'foldAST' and 'hoistAST' on the untyped λ-calculus of+-- "Control.Monad.Free.Foil.Example". The identity transformations are+-- identities, a round trip through a sum of signatures is one, and a fold+-- into a node count counts.+module Control.Monad.Free.Foil.HoistSpec (spec) where++import Data.Bifunctor.Sum (Sum (..))+import Test.Hspec++import Control.Monad.Foil (NameBinder, S (..))+import Control.Monad.Free.Foil+import Control.Monad.Free.Foil.Example++-- | The terms under test: Church numerals and their applications.+terms :: [(String, Expr VoidS)]+terms =+ [ ("church " ++ show n, churchN n) | n <- [0 .. 6 :: Int] ] +++ [ ("church 2 applied to church 3", AppE (churchN 2) (churchN 3))+ , ("church 3 normalised", nf' (AppE (churchN 2) (churchN 3)))+ ]++-- | A node count, indexed by the scope so that it can be the carrier of+-- 'foldAST'.+newtype Count (n :: S) = Count { getCount :: Int }++-- | The number of variables and nodes of a term, through 'foldAST'.+sizeOf :: Expr n -> Int+sizeOf = getCount . foldAST (const (Count 1)) (\_ body -> Count (getCount body)) node+ where+ node :: ExprF (Count m) (Count m) -> Count m+ node = \case+ AppF f x -> Count (1 + getCount f + getCount x)+ LamF b -> Count (1 + getCount b)++spec :: Spec+spec = do+ describe "hoistAST" $ do+ it "is the identity on the identity transformation" $+ mapM_ (\(name, t) -> (name, show (hoistAST id t)) `shouldBe` (name, show t)) terms+ it "round-trips through a sum of signatures" $+ let there = hoistAST L2 :: Expr n -> AST NameBinder (Sum ExprF ExprF) n+ back = hoistAST (\case L2 x -> x; R2 x -> x)+ in mapM_ (\(name, t) -> (name, show (back (there t))) `shouldBe` (name, show t)) terms+ describe "foldAST" $ do+ it "rebuilds a term with the constructors" $+ mapM_ (\(name, t) -> (name, show (foldAST Var ScopedAST Node t)) `shouldBe` (name, show t)) terms+ it "counts the nodes of a Church numeral" $+ mapM_ (\n -> (n, sizeOf (churchN n)) `shouldBe` (n, 2 * n + 3)) [0 .. 6 :: Int]
+ test/Control/Monad/Free/Foil/NFDataSpec.hs view
@@ -0,0 +1,36 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+-- | 'rnf' of a term forces every field of every node, also the fields that+-- hold no subterms, which a traversal of the signature as a 'Bifoldable'+-- would skip.+module Control.Monad.Free.Foil.NFDataSpec (spec) where++import Control.DeepSeq (NFData, rnf)+import Control.Exception (evaluate)+import GHC.Generics (Generic)+import Test.Hspec++import qualified Control.Monad.Foil as Foil+import Control.Monad.Free.Foil++-- | λ-terms with integer literals.+data LitSig scope term+ = AppSig term term+ | LamSig scope+ | LitSig Int+ deriving (Generic, NFData)++type Term = AST Foil.NameBinder LitSig++-- | @λx. x lit@.+applyToLit :: Int -> Term Foil.VoidS+applyToLit n = Foil.withFresh Foil.emptyScope $ \binder ->+ Node (LamSig (ScopedAST binder (Node (AppSig (Var (Foil.nameOf binder)) (Node (LitSig n))))))++spec :: Spec+spec = describe "rnf of AST" $ do+ it "forces a term" $+ evaluate (rnf (applyToLit 1)) `shouldReturn` ()+ it "forces a field of the signature under a binder" $+ evaluate (rnf (applyToLit (error "the literal"))) `shouldThrow` errorCall "the literal"
test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs view
@@ -12,6 +12,12 @@ import qualified Control.Monad.Foil as Foil import qualified Data.Map as Map+import Control.DeepSeq (rnf)+import Data.Bifoldable (bifoldMap)+import Data.Bifunctor (bimap)+import Data.Bitraversable (bitraverse)+import Data.Monoid (Sum (..))+import Data.ZipMatchK (Mappings (..), ZipMatchK (..)) import Test.Hspec import Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config@@ -34,6 +40,19 @@ spec :: Spec spec = do+ describe "the generated instances of the signature" $ do+ it "map the term and the scoped positions apart" $+ bimap (+ 1) (* 2) (LetSig (10 :: Int) (3 :: Int)) `shouldBe` LetSig 20 4+ it "fold over both positions" $+ getSum (bifoldMap (const (Sum 1)) (const (Sum 10)) (LetSig () ())) `shouldBe` (11 :: Int)+ it "traverse both positions" $+ bitraverse Just Just (AppSig 'a' 'b' :: TermSig () Char) `shouldBe` Just (AppSig 'a' 'b')+ it "force a term and its patterns" $+ rnf (toTerm Foil.emptyScope Map.empty (Let (PatternVar x) identity (ScopedTerm (Var x)))) `shouldBe` ()+ it "match equal constructors and reject different ones" $ do+ zipMatchWithK (zipAdd :^: zipAdd :^: M0) (AppSig 1 2 :: TermSig Int Int) (AppSig 10 20) `shouldBe` Just (AppSig 11 22)+ zipMatchWithK (zipAdd :^: zipAdd :^: M0) (AppSig 1 2 :: TermSig Int Int) (FunSig 3) `shouldBe` Nothing+ describe "a pattern adjacent to its scope (Fun)" $ it "round-trips, and the body still refers to the binder" $ case roundtrip (Fun (PatternVar x) (ScopedTerm (Var x))) of@@ -71,3 +90,6 @@ where isFun Fun{} = True isFun _ = False++zipAdd :: Int -> Int -> Maybe Int+zipAdd a b = Just (a + b)
test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/PatternsSyntax.hs view
@@ -21,8 +21,6 @@ import Control.Monad.Free.Foil.Binary () import Control.Monad.Free.Foil.Binary.TH (deriveBinaryPattern) import Control.Monad.Free.Foil.TH.MkFreeFoil-import Data.Bifunctor.TH-import Data.ZipMatchK import Generics.Kind.TH (deriveGenericK) import Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsConfig@@ -46,19 +44,5 @@ instance Foil.HasNameBinders FFNPattern instance Foil.UnifiablePattern FFNPattern deriveBinaryPattern ''FFNPattern--deriveBifunctor ''MTermSig-deriveBifoldable ''MTermSig-deriveBitraversable ''MTermSig-deriveGenericK ''MTermSig-instance ZipMatchK MTermSig--deriveBifunctor ''ATermSig-deriveBifoldable ''ATermSig-deriveBitraversable ''ATermSig--deriveBifunctor ''NTermSig-deriveBifoldable ''NTermSig-deriveBitraversable ''NTermSig mkFreeFoilConversions conversionsConfig
test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Syntax.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-}@@ -29,7 +31,6 @@ import Control.Monad.Free.Foil.Binary () import Control.Monad.Free.Foil.Binary.TH (deriveBinaryPattern) import Control.Monad.Free.Foil.TH.MkFreeFoil-import Data.Bifunctor.TH import Data.ZipMatchK import Generics.Kind.TH (deriveGenericK) @@ -44,12 +45,10 @@ instance Foil.UnifiablePattern FFPattern deriveBinaryPattern ''FFPattern -deriveBifunctor ''TermSig-deriveBifoldable ''TermSig-deriveBitraversable ''TermSig--deriveGenericK ''TermSig instance ZipMatchK VarIdent where zipMatchWithK = zipMatchViaEq-instance ZipMatchK TermSig mkFreeFoilConversions config++-- For the tests of the generated instances.+deriving instance (Eq scope, Eq term) => Eq (TermSig scope term)+deriving instance (Show scope, Show term) => Show (TermSig scope term)
+ test/Data/ZipMatchK/SumProductSpec.hs view
@@ -0,0 +1,127 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++-- | The written-out 'ZipMatchK' and 'ZipMatchFoldK' instances for 'Sum' and+-- 'Product' must agree with the generic ones, which 'genericZipMatchWithK' and+-- 'genericZipMatchFoldK' still compute from the 'Generics.Kind.GenericK'+-- instances. As in "Data.ZipMatchK.THSpec", the test+-- compares the two on every pair of a set of sample values.+module Data.ZipMatchK.SumProductSpec (spec) where++import qualified Data.Bifunctor.Product as Bi+import qualified Data.Bifunctor.Sum as Bi+import qualified Data.Functor.Product as F+import qualified Data.Functor.Sum as F+import Generics.Kind (LoT (..))+import Test.Hspec++import Data.ZipMatchK+import Data.ZipMatchK.Bifunctor ()+import Data.ZipMatchK.Functor ()+import Data.ZipMatchK.Generic (genericZipMatchFoldK, genericZipMatchWithK)+import Data.ZipMatchK.TH++-- | A signature bifunctor.+data LamSig scope term = App term term | Lam scope+ deriving (Functor, Foldable, Traversable, Eq, Show)++deriveZipMatchK ''LamSig++-- | A functor.+newtype Boxed term = Boxed [term]+ deriving (Functor, Foldable, Traversable, Eq, Show)++deriveZipMatchK1 ''Boxed++-- | Zip two values by equality, so that the result has the same type as the+-- inputs and can be compared with '=='.+zipEq :: Eq a => a -> a -> Maybe a+zipEq x y+ | x == y = Just x+ | otherwise = Nothing++lamSamples :: [LamSig String String]+lamSamples = [App "x" "y", App "x" "x", Lam "s", Lam "t"]++boxedSamples :: [Boxed String]+boxedSamples = [Boxed [], Boxed ["x"], Boxed ["x", "y"]]++spec :: Spec+spec = do+ describe "Data.Bifunctor.Sum" $+ it "agrees with the generic instance on every pair of samples" $+ sequence_+ [ zipMatchWithK @_ @(Bi.Sum LamSig LamSig) mappings2 x y+ `shouldBe` genericZipMatchWithK @(Bi.Sum LamSig LamSig) mappings2 x y+ | let samples = map Bi.L2 lamSamples ++ map Bi.R2 lamSamples+ , x <- samples, y <- samples ]++ describe "Data.Bifunctor.Product" $+ it "agrees with the generic instance on every pair of samples" $+ sequence_+ [ zipMatchWithK @_ @(Bi.Product LamSig LamSig) mappings2 x y+ `shouldBe` genericZipMatchWithK @(Bi.Product LamSig LamSig) mappings2 x y+ | let samples = [Bi.Pair a b | a <- lamSamples, b <- lamSamples]+ , x <- samples, y <- samples ]++ describe "Data.Functor.Sum" $+ it "agrees with the generic instance on every pair of samples" $+ sequence_+ [ zipMatchWithK @_ @(F.Sum Boxed Boxed) (zipEq :^: M0) x y+ `shouldBe` genericZipMatchWithK @(F.Sum Boxed Boxed) (zipEq :^: M0) x y+ | let samples = map F.InL boxedSamples ++ map F.InR boxedSamples+ , x <- samples, y <- samples ]++ describe "Data.Functor.Product" $+ it "agrees with the generic instance on every pair of samples" $+ sequence_+ [ zipMatchWithK @_ @(F.Product Boxed Boxed) (zipEq :^: M0) x y+ `shouldBe` genericZipMatchWithK @(F.Product Boxed Boxed) (zipEq :^: M0) x y+ | let samples = [F.Pair a b | a <- boxedSamples, b <- boxedSamples]+ , x <- samples, y <- samples ]++ describe "Data.Bifunctor.Sum, ZipMatchFoldK" $+ it "agrees with the generic instance on every pair of samples" $+ sequence_+ [ zipMatchFoldK @_ @(Bi.Sum LamSig LamSig) folds2 x y+ `shouldBe` genericZipMatchFoldK @(Bi.Sum LamSig LamSig) folds2 x y+ | let samples = map Bi.L2 lamSamples ++ map Bi.R2 lamSamples+ , x <- samples, y <- samples ]++ describe "Data.Bifunctor.Product, ZipMatchFoldK" $+ it "agrees with the generic instance on every pair of samples" $+ sequence_+ [ zipMatchFoldK @_ @(Bi.Product LamSig LamSig) folds2 x y+ `shouldBe` genericZipMatchFoldK @(Bi.Product LamSig LamSig) folds2 x y+ | let samples = [Bi.Pair a b | a <- lamSamples, b <- lamSamples]+ , x <- samples, y <- samples ]++ describe "Data.Functor.Sum, ZipMatchFoldK" $+ it "agrees with the generic instance on every pair of samples" $+ sequence_+ [ zipMatchFoldK @_ @(F.Sum Boxed Boxed) (collect "t" :%: F0) x y+ `shouldBe` genericZipMatchFoldK @(F.Sum Boxed Boxed) (collect "t" :%: F0) x y+ | let samples = map F.InL boxedSamples ++ map F.InR boxedSamples+ , x <- samples, y <- samples ]++ describe "Data.Functor.Product, ZipMatchFoldK" $+ it "agrees with the generic instance on every pair of samples" $+ sequence_+ [ zipMatchFoldK @_ @(F.Product Boxed Boxed) (collect "t" :%: F0) x y+ `shouldBe` genericZipMatchFoldK @(F.Product Boxed Boxed) (collect "t" :%: F0) x y+ | let samples = [F.Pair a b | a <- boxedSamples, b <- boxedSamples]+ , x <- samples, y <- samples ]+ where+ mappings2 :: Mappings (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)+ mappings2 = zipEq :^: zipEq :^: M0++ folds2 :: Folds [String] (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)+ folds2 = collect "s" :%: collect "t" :%: F0++ -- The two components, tagged with the position they come from.+ collect :: String -> String -> String -> [String]+ collect tag x y = [tag ++ ":" ++ x ++ "/" ++ y]
test/Data/ZipMatchK/THSpec.hs view
@@ -11,12 +11,15 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} --- | The derived 'ZipMatchK' instance must agree with the generic one.+-- | The derived 'ZipMatchK' and 'ZipMatchFoldK' instances must agree with the+-- generic ones. -- -- Both are available for the same type: 'deriveZipMatchK' provides the--- instance, and 'genericZipMatchWithK' computes the generic answer without--- needing one. So the test compares the two, on every pair of a set of sample--- values, over the field shapes a signature actually uses.+-- instances, and 'genericZipMatchWithK' and 'genericZipMatchFoldK' compute the+-- generic answers without needing them. So the test compares the two, on every+-- pair of a set of sample values, over the field shapes a signature actually+-- uses. The folds collect the components they meet, so the comparison also+-- checks the order in which they are combined. module Data.ZipMatchK.THSpec (spec) where import Data.List.NonEmpty (NonEmpty (..))@@ -26,7 +29,8 @@ import Test.Hspec import Data.ZipMatchK-import Data.ZipMatchK.Generic (genericZipMatchWithK)+import Data.Maybe (isJust)+import Data.ZipMatchK.Generic (genericZipMatchFoldK, genericZipMatchWithK) import Data.ZipMatchK.TH -- | An annotation, standing for the extra parameter a generated signature has.@@ -127,6 +131,43 @@ [ zipMatchWithK @_ @Boxed (zipEq :^: M0) x y `shouldBe` genericZipMatchWithK @Boxed (zipEq :^: M0) x y | x <- boxedSamples, y <- boxedSamples ]++ describe "deriveZipMatchK2, ZipMatchFoldK" $ do+ it "agrees with the generic instance on every pair of samples" $+ sequence_+ [ zipMatchFoldK @_ @(RichSig Ann) folds x y+ `shouldBe` genericZipMatchFoldK @(RichSig Ann) folds x y+ | x <- richSamples, y <- richSamples ]+ it "fails exactly where zipMatchWithK fails" $+ sequence_+ [ isJust (zipMatchFoldK @_ @(RichSig Ann) folds x y)+ `shouldBe` isJust (zipMatchWithK @_ @(RichSig Ann) keep x y)+ | x <- richSamples, y <- richSamples ]++ describe "deriveZipMatchK, ZipMatchFoldK" $+ it "agrees with the generic instance on every pair of samples" $+ sequence_+ [ zipMatchFoldK @_ @LamSig folds x y+ `shouldBe` genericZipMatchFoldK @LamSig folds x y+ | x <- lamSamples, y <- lamSamples ]++ describe "deriveZipMatchK1, ZipMatchFoldK" $+ it "agrees with the generic instance on every pair of samples" $+ sequence_+ [ zipMatchFoldK @_ @Boxed (collect "t" :%: F0) x y+ `shouldBe` genericZipMatchFoldK @Boxed (collect "t" :%: F0) x y+ | x <- boxedSamples, y <- boxedSamples ] where mappings :: Mappings (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0) mappings = zipEq :^: zipEq :^: M0++ -- Functions that always succeed, so that only the shapes can fail.+ keep :: Mappings (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)+ keep = (\x _ -> Just x) :^: (\x _ -> Just x) :^: M0++ folds :: Folds [String] (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)+ folds = collect "s" :%: collect "t" :%: F0++ -- The two components, tagged with the position they come from.+ collect :: String -> String -> String -> [String]+ collect tag x y = [tag ++ ":" ++ x ++ "/" ++ y]
test/laws/Control/Monad/Foil/Laws.hs view
@@ -75,6 +75,7 @@ -- * Laws of 'CoSinkable' PatternCase (..), genPatternCase,+ showPatternCase, CoSinkableLaws (..), coSinkableLaws, CoSinkLaw (..),@@ -242,10 +243,21 @@ NameBinderListCons b rest -> nameId (nameOf b) : nameBinderListNames rest -- | The raw names a pattern binds, in the order in which 'withPattern'--- visits them (through 'nameBinderListOf').+-- visits them. patternRawNames :: CoSinkable p => p n l -> [Int]-patternRawNames = nameBinderListNames . nameBinderListOf+patternRawNames pat = withPattern+ (\scope binder k -> withFresh scope $ \binder' ->+ k (RawNames (nameId (nameOf binder) :)) binder')+ (RawNames id)+ (\(RawNames f) (RawNames g) -> RawNames (f . g))+ emptyScope+ pat+ (\(RawNames f) _ _ -> f []) +-- | A difference list of raw names, indexed like the results of+-- 'withPattern'.+newtype RawNames (n :: S) (l :: S) (o :: S) (o' :: S) = RawNames ([Int] -> [Int])+ -- | Show the names a pattern binds, in the library's order. showPattern :: CoSinkable p => p n l -> String showPattern = showPatternWith patternRawNames@@ -526,7 +538,7 @@ -- order of 'withPattern'. data CoSinkLaw = CoSinkIdentity | CoSinkComposition | CoSinkExtension | CoSinkBinders- | WithPatternOrder+ | WithPatternOrder | NameBinderListOfOrder deriving (Eq, Show, Enum, Bounded) -- | 'withPattern' visits the binders of a pattern in the order of its@@ -537,8 +549,16 @@ counterexample "the order of the pattern is on the left, the order of withPattern on the right" $ binders p === patternRawNames p +-- | 'nameBinderListOf' lists the binders of a pattern in the order in which+-- 'withPattern' visits them, as its default does.+nameBinderListOfLaw :: CoSinkable p => p n l -> Property+nameBinderListOfLaw p =+ counterexample "nameBinderListOf on the left, the order of withPattern on the right" $+ nameBinderListNames (nameBinderListOf p) === patternRawNames p+ -- | All laws of 'coSinkabilityProof' for a pattern type, along each class--- of renamings, and the law of the traversal order of 'withPattern'.+-- of renamings, the law of the traversal order of 'withPattern', and the+-- agreement of 'nameBinderListOf' with it. coSinkableSpec :: CoSinkable p => PatternNames p -> GenPattern p -> (RenamingClass -> CoSinkLaw -> Verdict) -> Spec@@ -546,6 +566,9 @@ law (verdict Inclusions WithPatternOrder) "withPattern visits binders in the order of the pattern" $ forAllShow (genPatternCase genPat Inclusions) (showPatternCase binders) $ \(PatternCase _ p) -> withPatternOrderLaw binders p+ law (verdict Inclusions NameBinderListOfOrder) "nameBinderListOf lists the binders in the order of withPattern" $+ forAllShow (genPatternCase genPat Inclusions) (showPatternCase binders) $+ \(PatternCase _ p) -> nameBinderListOfLaw p forM_ allRenamingClasses $ \cls -> describe ("along " <> show cls) $ forM_ [CoSinkIdentity, CoSinkComposition, CoSinkExtension, CoSinkBinders] $ \name -> law (verdict cls name) (show name) $@@ -557,6 +580,7 @@ lawOf CoSinkExtension = coSinkExtension laws lawOf CoSinkBinders = coSinkBinders laws lawOf WithPatternOrder = \(PatternCase _ p) -> withPatternOrderLaw binders p+ lawOf NameBinderListOfOrder = \(PatternCase _ p) -> nameBinderListOfLaw p -- * Laws of 'UnifiablePattern'