diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,11 @@ # Revision history for generics-mrsop +## 2.1.0 -- Jul 2019 + +- Added datatype `Holes` for representing families annotated with holes. +- Brought in some monadic attribute grammar combinators +- Big documentation update on a number of places + ## 2.0.0 -- Mar 2019 - `Eq1` and `Show1` are now called `EqHO` and `ShowHO`. This avoids clashing with the @@ -20,4 +26,4 @@ ## 1.0.0.0 -- May 2018 -* First version. Released on an unsuspecting world. +- First version. Released on an unsuspecting world. diff --git a/generics-mrsop.cabal b/generics-mrsop.cabal --- a/generics-mrsop.cabal +++ b/generics-mrsop.cabal @@ -1,5 +1,5 @@ name: generics-mrsop -version: 2.0.0 +version: 2.1.0 synopsis: Generic Programming with Mutually Recursive Sums of Products. @@ -36,6 +36,7 @@ Generics.MRSOP.Base, Generics.MRSOP.Opaque, Generics.MRSOP.Util, + Generics.MRSOP.Holes Generics.MRSOP.TH, Generics.MRSOP.Zipper, Generics.MRSOP.Zipper.Deep, @@ -80,4 +81,4 @@ source-repository this type: git location: https://github.com/VictorCMiraldo/generics-mrsop - tag: v2.0.0 + tag: v2.1.0 diff --git a/src/Generics/MRSOP/AG.hs b/src/Generics/MRSOP/AG.hs --- a/src/Generics/MRSOP/AG.hs +++ b/src/Generics/MRSOP/AG.hs @@ -11,68 +11,65 @@ import Generics.MRSOP.Base --- | Annotated version of Fix. This is basically the 'Cofree' datatype, --- but for n-ary functors +-- * Annotated Fixpoints + +-- $annfixpoints +-- +-- Annotated fixpoints are a very useful construction. Suppose the generic +-- algorithm at hand frequently requires the height of the tree being processed. +-- Instead of recomputing the height of the trees everytime we need them, +-- we can annotate the whole tree with its height at each given point. +-- +-- Given an algebra that computes height at one point, assuming +-- the recursive positions have been substituted with their own heights, +-- +-- > heightAlgebra :: Rep ki (Const Int) xs -> Const Int iy +-- > heightAlgebra = Const . (1+) . elimRep (const 0) getConst (maximum . (0:)) +-- +-- We can annotate each node with their height with the 'synthesize' function. +-- +-- > synthesize heightAlgebra :: Fix ki codes ix -> AnnFix ki codes (Const Int) ix +-- +-- Note how using just 'cata' would simply count the number of nodes, forgetting +-- the intermediate values. +-- +-- > cata heightAlgebra :: Fix ki codes ix -> Const Int ix +-- + +-- | Annotated version of Fix. This is basically the 'Cofree' datatype, +-- but for n-ary functors. data AnnFix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (phi :: Nat -> *) (n :: Nat) = - AnnFix (phi n) - (Rep ki (AnnFix ki codes phi) (Lkup n codes)) + AnnFix (phi n) (Rep ki (AnnFix ki codes phi) (Lkup n codes)) +-- |Retrieves the top annotation at the current value. getAnn :: AnnFix ki codes ann ix -> ann ix getAnn (AnnFix a _) = a +-- |Catamorphism with access to the annotations annCata :: IsNat ix - => (forall iy. IsNat iy => chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) + => (forall iy. IsNat iy => chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) -- ^ -> AnnFix ki codes chi ix -> phi ix annCata f (AnnFix a x) = f a (mapRep (annCata f) x) --- | Forget the annotations +-- | Forgetful natural transformation back into 'Fix' forgetAnn :: AnnFix ki codes a ix -> Fix ki codes ix forgetAnn (AnnFix _ rep) = Fix (mapRep forgetAnn rep) +-- | Maps over the annotations within an annotated fixpoint mapAnn :: (IsNat ix) - => (forall iy. chi iy -> phi iy) + => (forall iy. chi iy -> phi iy) -- ^ -> AnnFix ki codes chi ix -> AnnFix ki codes phi ix mapAnn f = synthesizeAnn (\x _ -> f x) --- | Synthesized attributes -synthesizeAnn :: forall ki codes chi phi ix - . (IsNat ix) - => - (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) - -> AnnFix ki codes chi ix - -> AnnFix ki codes phi ix -synthesizeAnn f = annCata alg - where - alg :: forall iy - . chi iy - -> Rep ki (AnnFix ki codes phi) (Lkup iy codes) - -> AnnFix ki codes phi iy - alg ann rep = AnnFix (f ann (mapRep getAnn rep)) rep - --- |Example of using 'synthesize' to annotate a tree with its size --- at every node. --- --- > sizeAlgebra :: Rep ki (Const (Sum Int)) xs -> Const (Sum Int) iy --- > sizeAlgebra = (Const 1 <>) . monoidAlgebra --- --- Annotate each node with the number of subtrees --- --- > sizeGeneric' :: (IsNat ix) --- > => Fix ki codes ix -> AnnFix ki codes (Const (Sum Int)) ix --- > sizeGeneric' = synthesize sizeAlgebra --- --- Note how using just 'cata' will simply count the number of nodes --- --- > sizeGeneric :: (IsNat ix) --- > => Fix ki codes ix -> Const (Sum Int) ix --- > sizeGeneric = cata sizeAlgebra --- +-- |Annotates a tree at every node with the result +-- of the catamorphism with the supplied algebra called at +-- each node. synthesize :: forall ki phi codes ix . (IsNat ix) - => (forall iy . (IsNat iy) => Rep ki phi (Lkup iy codes) -> phi iy) + => (forall iy . (IsNat iy) => Rep ki phi (Lkup iy codes) -> phi iy) -- ^ -> Fix ki codes ix -> AnnFix ki codes phi ix synthesize f = cata alg @@ -83,3 +80,32 @@ -> AnnFix ki codes phi iy alg xs = AnnFix (f (mapRep getAnn xs)) xs + +-- |Monadic variant of 'synthesize' +synthesizeM :: forall ki phi codes ix m + . (Monad m , IsNat ix) + => (forall iy . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy)) -- ^ + -> Fix ki codes ix + -> m (AnnFix ki codes phi ix) +synthesizeM f = cataM alg + where + alg :: forall iy + . (IsNat iy) + => Rep ki (AnnFix ki codes phi) (Lkup iy codes) + -> m (AnnFix ki codes phi iy) + alg xs = flip AnnFix xs <$> f (mapRep getAnn xs) + +-- | Synthesized attributes with an algebra that has access to the annotations. +synthesizeAnn :: forall ki codes chi phi ix + . (IsNat ix) + => (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) -- ^ + -> AnnFix ki codes chi ix + -> AnnFix ki codes phi ix +synthesizeAnn f = annCata alg + where + alg :: forall iy + . chi iy + -> Rep ki (AnnFix ki codes phi) (Lkup iy codes) + -> AnnFix ki codes phi iy + alg ann rep = AnnFix (f ann (mapRep getAnn rep)) rep + diff --git a/src/Generics/MRSOP/Base.hs b/src/Generics/MRSOP/Base.hs --- a/src/Generics/MRSOP/Base.hs +++ b/src/Generics/MRSOP/Base.hs @@ -6,7 +6,19 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} --- | Re-exports everything from under @Generics.MRSOP.Base@ +-- | Re-exports everything from under @Generics.MRSOP.Base@ and +-- @Generics.MRSOP.Util@: +-- +-- - "Generics.MRSOP.Base.NS" +-- - "Generics.MRSOP.Base.NP" +-- - "Generics.MRSOP.Base.Universe" +-- - "Generics.MRSOP.Base.Class" +-- - "Generics.MRSOP.Base.Metadata" +-- - "Generics.MRSOP.Base.Combinators" +-- - "Generics.MRSOP.Util" +-- +-- For a lightweight example on how to use the library, please refer to "Generics.MRSOP.Examples.RoseTree" +-- or to the full for a more in-depth explanation module Generics.MRSOP.Base (module Export) where import Generics.MRSOP.Base.NS as Export diff --git a/src/Generics/MRSOP/Base/Universe.hs b/src/Generics/MRSOP/Base/Universe.hs --- a/src/Generics/MRSOP/Base/Universe.hs +++ b/src/Generics/MRSOP/Base/Universe.hs @@ -64,7 +64,7 @@ testEquality (NA_I _) (NA_K _) = Nothing testEquality (NA_K _) (NA_I _) = Nothing testEquality (NA_I i) (NA_I i') = - case testEquality (sNatFixIdx i) (sNatFixIdx i') of + case testEquality (snatFixIdx i) (snatFixIdx i') of Just Refl -> Just Refl Nothing -> Nothing testEquality (NA_K k) (NA_K k') = @@ -292,17 +292,25 @@ -- | Catamorphism over fixpoints cata :: (IsNat ix) - => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy) + => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy) -- ^ -> Fix ki codes ix -> phi ix cata f (Fix x) = f (mapRep (cata f) x) +-- |Monadic variant +cataM :: (Monad m , IsNat ix) + => (forall iy . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy)) -- ^ + -> Fix ki codes ix + -> m (phi ix) +cataM f (Fix x) = mapRepM (cataM f) x >>= f + -- |Retrieves the index of a 'Fix' proxyFixIdx :: phi ix -> Proxy ix proxyFixIdx _ = Proxy -sNatFixIdx :: IsNat ix => phi ix -> SNat ix -sNatFixIdx x = getSNat (proxyFixIdx x) +-- |Retrieves the index of a 'Fix' as a singleton. +snatFixIdx :: IsNat ix => phi ix -> SNat ix +snatFixIdx x = getSNat (proxyFixIdx x) -- |Maps over the values of opaque types within the -- fixpoint. diff --git a/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs b/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs --- a/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs +++ b/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs @@ -10,6 +10,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE PatternSynonyms #-} +{-# OPTIONS_HADDOCK hide, prune, ignore-exports #-} {-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-} {-# OPTIONS_GHC -Wno-missing-signatures #-} {-# OPTIONS_GHC -Wno-incomplete-patterns #-} diff --git a/src/Generics/MRSOP/Examples/RoseTree.hs b/src/Generics/MRSOP/Examples/RoseTree.hs --- a/src/Generics/MRSOP/Examples/RoseTree.hs +++ b/src/Generics/MRSOP/Examples/RoseTree.hs @@ -13,17 +13,37 @@ {-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-} {-# OPTIONS_GHC -Wno-incomplete-patterns #-} {-# OPTIONS_GHC -Wno-orphans #-} +{-# OPTIONS_GHC -Wno-unused-top-binds #-} -- |This module is analogous to 'Generics.MRSOP.Examples.RoseTreeTH', -- but we use no Template Haskell here. -module Generics.MRSOP.Examples.RoseTree where +module Generics.MRSOP.Examples.RoseTree ( + -- * Non-standard Rose-Tree datatype + -- $exp01 + R + -- ** Family Structure + -- $exp02 + , ListCode,RTCode,CodesRose,FamRose + -- ** 'Family' Instance + -- $exp03 + + -- * Generic Combinators + -- $exp04 + , testEq , normalize , sumTree + ) where + import Data.Function (on) import Generics.MRSOP.Base import Generics.MRSOP.Opaque --- * Standard Rose-Tree datatype +-- $exp01 +-- +-- Suppose we we have a mutually recursive family +-- consisting of RoseTree's with some redundant constructor: + +-- | Non-standard Rose-tree datatype. data R a = a :>: [R a] | Leaf a deriving Show @@ -33,16 +53,56 @@ value2 = 1 :>: [2 :>: [] , Leaf 12] value3 = 3 :>: [Leaf 23 , value1 , value2] --- ** Family Structure +-- $exp02 +-- +-- The @R Int@ family has many components, that must be encoded in +-- the generics-mrsop format. These are: + +-- |Codes for the @[R Int]@ type. type ListCode = '[ '[] , '[ 'I ('S 'Z) , 'I 'Z] ] + +-- |Codes for the @R Int@ type type RTCode = '[ '[ 'K 'KInt , 'I 'Z] , '[ 'K 'KInt] ] +-- |All codes packed in a type-level list type CodesRose = '[ListCode , RTCode] + +-- |The types corresponding the the codes in 'CodesRose' +-- appear in the same order. type FamRose = '[ [R Int] , R Int] -- ** Instance Decl +-- $exp03 +-- +-- Which in turn, allows us to write the 'Family' instance for +-- @R Int@. The @instance Family Singl FamRose CodesRose@ states that +-- the types in 'FamRose' follow the codes in 'CodesRose' with +-- its opaque parts represented by 'Singl' Check the source code for more details +-- on the instance. +-- +-- It is worth mentioning that 'Generics.MRSOP.TH.deriveFamily' will derive +-- this code automatically. +-- +-- >instance Family Singl FamRose CodesRose where +-- > sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0) +-- > sfrom' (SS SZ) (El (Leaf a)) = Rep $ There (Here (NA_K (SInt a) :* NP0)) +-- > sfrom' SZ (El []) = Rep $ Here NP0 +-- > sfrom' SZ (El (x:xs)) = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* NP0)) +-- > sfrom' _ _ = error "unreachable" +-- > +-- > sto' SZ (Rep (Here NP0)) +-- > = El [] +-- > sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0)))) +-- > = El (x : xs) +-- > sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0))) +-- > = El (a :>: as) +-- > sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0)))) +-- > = El (Leaf a) +-- > sto' _ _ = error "unreachable" + + instance Family Singl FamRose CodesRose where sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0) sfrom' (SS SZ) (El (Leaf a)) = Rep $ There (Here (NA_K (SInt a) :* NP0)) @@ -74,19 +134,41 @@ datatypeInfo _ _ = error "unreachable" --- * Eq Instance +-- $exp04 +-- +-- Next, we showcase some of the simpler generic combinators provided +-- out of the box with /generics-mrsop/ instance Eq (R Int) where (==) = geq eqSingl `on` (into @FamRose) +-- |We can use generic equality out of the box: +-- +-- > instance Eq (R Int) where +-- > (==) = geq eqSingl `on` (into @FamRose) +-- +-- If we run 'testEq' it must return @True@, naturally. testEq :: Bool testEq = value1 == value1 && value2 /= value1 --- * Compos test pattern RInt_ = SS SZ +-- |Here is an example of 'compos'; used to substitute the redundant 'Leaf' +-- constructor by its standard rose tree representation. +-- +-- > normalize :: R Int -> R Int +-- > normalize = unEl . go (SS SZ) . into +-- > where +-- > go :: forall iy. (IsNat iy) => SNat iy -> El FamRose iy -> El FamRose iy +-- > go (SS SZ) (El (Leaf a)) = El (a :>: []) -- (SS SZ) is the index of 'R Int' in 'CodesRose' +-- > go _ x = compos go x +-- +-- Then, for example, +-- +-- > normalize (42 :>: [Leaf 10 , 15 :>: [Leaf 20]]) == 42 :>: [10 :>: [] , 15 :>: [20 :>: []]] +-- normalize :: R Int -> R Int normalize = unEl . go (SS SZ) . into where @@ -94,8 +176,14 @@ go RInt_ (El (Leaf a)) = El (a :>: []) go _ x = compos go x --- * Crush test - +-- |Another generic combinator is 'crush'. We can 'crush' a rose tree and compute the sum +-- of all the ints stored within said tree. +-- +-- > sumTree :: R Int -> Int +-- > sumTree = crush k sum . (into @FamRose) +-- > where k :: Singl x -> Int +-- > k (SInt n) = n +-- sumTree :: R Int -> Int sumTree = crush k sum . (into @FamRose) where k :: Singl x -> Int diff --git a/src/Generics/MRSOP/Examples/RoseTreeTH.hs b/src/Generics/MRSOP/Examples/RoseTreeTH.hs --- a/src/Generics/MRSOP/Examples/RoseTreeTH.hs +++ b/src/Generics/MRSOP/Examples/RoseTreeTH.hs @@ -12,6 +12,7 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternSynonyms #-} +{-# OPTIONS_HADDOCK hide, prune, ignore-exports #-} {-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-} {-# OPTIONS_GHC -Wno-missing-signatures #-} {-# OPTIONS_GHC -Wno-incomplete-patterns #-} diff --git a/src/Generics/MRSOP/Examples/SimpTH.hs b/src/Generics/MRSOP/Examples/SimpTH.hs --- a/src/Generics/MRSOP/Examples/SimpTH.hs +++ b/src/Generics/MRSOP/Examples/SimpTH.hs @@ -11,6 +11,7 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternSynonyms #-} +{-# OPTIONS_HADDOCK hide, prune, ignore-exports #-} {-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-} {-# OPTIONS_GHC -Wno-missing-signatures #-} {-# OPTIONS_GHC -Wno-incomplete-patterns #-} @@ -20,8 +21,10 @@ module Generics.MRSOP.Examples.SimpTH where import Data.Function (on) +import Data.Functor.Const import Generics.MRSOP.Base +import Generics.MRSOP.Holes import Generics.MRSOP.Opaque import Generics.MRSOP.Zipper @@ -172,7 +175,6 @@ test4 n = DFun "test" "n" $ (SAssign "x" (EAdd (ELit 10) (ELit n))) `SSeq` (SReturn (EVar "x")) - test5 :: Maybe (Decl String) test5 = enter @@ -190,3 +192,16 @@ mk42 IdxExpString _ = El $ ELit 42 mk42 _ x = x +-- ** Holes test + +test6 :: Holes Singl CodesStmtString (Const Int) ('I ('S 'Z)) +test6 = HPeel' (CS (CS CZ)) + ( (HPeel' CZ (HOpq' (SString "lol") :* NP0)) + :* (Hole' (Const 42)) + :* NP0) + +test7 :: HolesAnn (Const Int) Singl CodesStmtString (Const Int) ('I ('S 'Z)) +test7 = HPeel (Const 1) (CS (CS CZ)) + ( (HPeel (Const 2) CZ (HOpq (Const 4) (SString "lol") :* NP0)) + :* (Hole (Const 3) (Const 42)) + :* NP0) diff --git a/src/Generics/MRSOP/Holes.hs b/src/Generics/MRSOP/Holes.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Holes.hs @@ -0,0 +1,409 @@ +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Generics.MRSOP.Holes where + +import Data.Proxy +import Data.Functor.Const +import Data.Type.Equality +import qualified Data.Set as S (insert , empty , Set) + +import Control.Monad.Identity +import Control.Monad.State + +import Generics.MRSOP.Base + +-- * Annotating a Mutually Recursive Family with Holes + +-- $withholes +-- +-- It is often the case that we must perform some sort of symbolic +-- processing over our datatype. Take /unification/ for example. +-- For that to work, we must either have a dedicated constructor +-- in the datatype for representing a /metavariable/, which would +-- be difficult to access in a generic fashion, or we must augment +-- the definition an add those. +-- +-- In this module we provide the 'Holes' datatype, which +-- enables this very functionality. Imagine the following +-- family: +-- +-- > data Exp = Add Exp Exp | Let Decls Exp | Var Exp +-- > data Decls = Decl VarDecl Decls | Empty +-- > data VarDecl = VarD String Exp +-- +-- The values that inhabit the type @Holes ki FamExp phi@ are +-- essentially isomorphic to: +-- +-- > data Exp' = Add Exp' Exp' | Let Decls' Exp' | Var Exp' | EHole (phi IdxExp) +-- > data Decls' = Decl VarDecl' Decls' | Empty | DHole (phi IdxDecls) +-- > data VarDecl' = VarD String Exp' | VHole (phi IdxVarDecl) +-- +-- If we want to, say, forbid holes on the declaration bit, we +-- can do so in the definition of phi. For example: +-- +-- > data OnlyExpAndVarHoles :: Atom kon -> * where +-- > ExpHole :: OnlyExpAndVarHoles ('I IdxExp) +-- > VarHole :: OnlyExpAndVarHoles ('I IdxVar) +-- +-- + +-- |A value of type 'HolesAnn' augments a mutually recursive +-- family with holes. This is useful for writing generic +-- unification-like algorithms. +-- +-- Essentially, we have the following isomorphism: +-- +-- > Holes ann ki codes phi at +-- > =~= (ann at :*: (phi :+: NA ki (Rep ki (Holes ann ki codes phi)))) +-- +-- That is, we are extending the representations with values of +-- type @phi@, and adding annotations of type @ann at@ everywhere. +-- A simpler variant of this type is given in 'Holes', where +-- the annotationsare defaulted to @Const ()@ +-- +-- The annotations are ignored in most of the functions and are here +-- only as a means of helping algorithms keep intermediate values +-- directly in the datatype. They have no semantic meaning. +-- +-- Note that @HolesAnn ann ki codes@, of kind @(Atom kon -> *) -> Atom kon -> *@ +-- forms an indexed free monad. +data HolesAnn :: (Atom kon -> *) + -> (kon -> *) + -> [[[Atom kon]]] + -> (Atom kon -> *) + -> Atom kon + -> * + where + -- |A "hole" contains something of type @phi@ + Hole :: ann at -> phi at -> HolesAnn ann ki codes phi at + -- |An opaque value + HOpq :: ann ('K k) -> ki k -> HolesAnn ann ki codes phi ('K k) + -- |A view over a constructor with its fields replaced + -- by treefixes. This already comes in a SOP flavour. + HPeel :: (IsNat n , IsNat i) + => ann ('I i) + -> Constr (Lkup i codes) n + -> NP (HolesAnn ann ki codes phi) (Lkup n (Lkup i codes)) + -> HolesAnn ann ki codes phi ('I i) + +-- |Extracts the annotation from the topmost 'HolesAnn' constructor. +holesAnn :: HolesAnn ann ki codes phi at -> ann at +holesAnn (Hole a _) = a +holesAnn (HOpq a _) = a +holesAnn (HPeel a _ _) = a + +-- * Mapping Over 'HolesAnn' + +-- |Our 'HolesAnn' is a higher order functor and can be mapped over. +holesMapAnnM :: (Monad m) + => (forall a . f a -> m (g a)) -- ^ Function to map over holes + -> (forall a . ann a -> m (bnn a)) -- ^ Function to map over annotations + -> HolesAnn ann ki codes f at + -> m (HolesAnn bnn ki codes g at) +holesMapAnnM f g (Hole a x) = Hole <$> g a <*> f x +holesMapAnnM _ g (HOpq a k) = flip HOpq k <$> g a +holesMapAnnM f g (HPeel a c p) = g a >>= \a' -> HPeel a' c <$> mapNPM (holesMapAnnM f g) p + +-- |Maps over the index part, not the annotation +holesMapM :: (Monad m) + => (forall a . f a -> m (g a)) + -> HolesAnn ann ki codes f at + -> m (HolesAnn ann ki codes g at) +holesMapM f = holesMapAnnM f return + +-- |Non-monadic version of 'holesMapM' +holesMapAnn :: (forall a . f a -> g a) + -> (forall a . ann a -> ann' a) + -> HolesAnn ann ki codes f at + -> HolesAnn ann' ki codes g at +holesMapAnn f g = runIdentity . holesMapAnnM (return . f) (return . g) + +-- |Non-monadic version of 'holesMapM' +holesMap :: (forall a . f a -> g a) + -> HolesAnn ann ki codes f at + -> HolesAnn ann ki codes g at +holesMap f = holesMapAnn f id + +-- |Since 'HolesAnn' is just a free monad, we can join them! +holesJoin :: HolesAnn ann ki codes (HolesAnn ann ki codes f) at + -> HolesAnn ann ki codes f at +holesJoin (Hole _ x) = x +holesJoin (HOpq a k) = HOpq a k +holesJoin (HPeel a c p) = HPeel a c (mapNP holesJoin p) + +-- * Extracting Annotations and HolesAnn from 'HolesAnn' + +-- |Returns the set of holes in a value of type 'HolesAnn'. The _getter_ +-- argument is there to handle the existantial type index present +-- in the holes and the insertion function is used to place +-- the holes in a datastructure of choice. The treefix is taversed +-- in a pre-order style and the holes inserted in the sturcture +-- as they are visited. +holesGetHolesAnnWith :: forall f r ann ki codes phi at + . f r -- ^ Empty structure + -> (r -> f r -> f r) -- ^ Insertion function + -> (forall ix . phi ix -> r) -- ^ How to get rid of the existential type + -> HolesAnn ann ki codes phi at + -> f r +holesGetHolesAnnWith empty ins tr + = flip execState empty . holesMapM getHole + where + getHole :: phi ix + -> State (f r) (phi ix) + getHole x = modify (ins $ tr x) >> return x + +-- |Instantiates 'holesGetHolesAnnWith' to use a list. +-- It's implementation is trivial: +-- +-- > holesGetHolesAnnWith' = holesGetHolesAnnWith [] (:) +holesGetHolesAnnWith' :: (forall ix . phi ix -> r) + -> HolesAnn ann ki codes phi at -> [r] +holesGetHolesAnnWith' = holesGetHolesAnnWith [] (:) + +-- |Instantiates 'holesGetHolesAnnWith' to use a set instead of a list. +holesGetHolesAnnWith'' :: (Ord r) + => (forall ix . phi ix -> r) + -> HolesAnn ann ki codes phi at -> S.Set r +holesGetHolesAnnWith'' = holesGetHolesAnnWith S.empty S.insert + +-- * Refining 'HolesAnn' + +-- |Similar to 'holesMapM', but allows to refine the structure of +-- a treefix if need be. One could implement 'holesMapM' as: +-- +-- > holesMapM f = holesRefineAnn (\a h -> Hole a <$> f h) HOpq' +-- +holesRefineAnnM :: (Monad m) + => (forall ix . ann ix -> f ix -> m (HolesAnn ann ki codes g ix)) + -> (forall k . ann ('K k) -> ki k -> m (HolesAnn ann ki codes g ('K k))) + -> HolesAnn ann ki codes f at + -> m (HolesAnn ann ki codes g at) +holesRefineAnnM f _ (Hole a x) = f a x +holesRefineAnnM _ g (HOpq a k) = g a k +holesRefineAnnM f g (HPeel a c holesnp) + = HPeel a c <$> mapNPM (holesRefineAnnM f g) holesnp + +-- |Just like 'holesRefineM', but only refines variables. One example is to implement +-- 'holesJoin' with it. +-- +-- > holesJoin = runIdentity . holesRefineVarsM (\_ -> return) +-- +holesRefineVarsM :: (Monad m) + => (forall ix . ann ix -> f ix -> m (HolesAnn ann ki codes g ix)) -- ^ How to produce a 'HolesAnn' from the previous hole. + -> HolesAnn ann ki codes f at + -> m (HolesAnn ann ki codes g at) +holesRefineVarsM f = holesRefineAnnM f (\a -> return . HOpq a) + +-- |Pure version of 'holesRefineM' +holesRefineAnn :: (forall ix . ann ix -> f ix -> HolesAnn ann ki codes g ix) -- ^ + -> (forall k . ann ('K k) -> ki k -> HolesAnn ann ki codes g ('K k)) + -> HolesAnn ann ki codes f at + -> HolesAnn ann ki codes g at +holesRefineAnn f g = runIdentity . holesRefineAnnM (\a -> return . f a) (\a -> return . g a) + +-- * Annotation Catamorphism and Synthesized Attributes + +-- |Standard monadic catamorphism for holes. The algebra can take the +-- annotation into account. +holesAnnCataM :: (Monad m) + => (forall at . ann at -> phi at -> m (res at)) -- ^ Action to perform at 'Hole' + -> (forall k . ann ('K k) -> ki k -> m (res ('K k))) -- ^ Action to perform at 'HOpq' + -> (forall i n . (IsNat i, IsNat n) + => ann ('I i) -> Constr (Lkup i codes) n + -> NP res (Lkup n (Lkup i codes)) + -> m (res ('I i))) -- ^ Action to perform at 'HPeel' + -> HolesAnn ann ki codes phi ix + -> m (res ix) +holesAnnCataM hF _ _ (Hole a x) = hF a x +holesAnnCataM _ oF _ (HOpq a x) = oF a x +holesAnnCataM hF oF cF (HPeel a c p) + = mapNPM (holesAnnCataM hF oF cF) p >>= cF a c + +-- |Pure variant of 'holesAnnCataM' +holesAnnCata :: (forall at . ann at -> phi at -> res at) -- ^ Action to perform at 'Hole' + -> (forall k . ann ('K k) -> ki k -> res ('K k)) -- ^ Action to perform at 'HOpq' + -> (forall i n . (IsNat i, IsNat n) + => ann ('I i) -> Constr (Lkup i codes) n + -> NP res (Lkup n (Lkup i codes)) + -> res ('I i)) -- ^ Action to perform at 'HPeel' + -> HolesAnn ann ki codes phi ix + -> res ix +holesAnnCata hF oF cF = runIdentity + . holesAnnCataM (\a phi -> return $ hF a phi) + (\a o -> return $ oF a o) + (\a c p -> return $ cF a c p) + +-- |Synthesizes attributes over a value of type 'HolesAnn'. This +-- is extremely useful for easily annotating a value with auxiliar +-- annotations. +holesSynthesizeM :: (Monad m) + => (forall at . ann at -> phi at -> m (res at)) -- ^ Action to perform at 'Hole' + -> (forall k . ann ('K k) -> ki k -> m (res ('K k))) -- ^ Action to perform at 'HOpq' + -> (forall i n . (IsNat i, IsNat n) + => ann ('I i) -> Constr (Lkup i codes) n + -> NP res (Lkup n (Lkup i codes)) + -> m (res ('I i))) -- ^ Action to perform at 'HPeel' + -> HolesAnn ann ki codes phi atom -- ^ Input value + -> m (HolesAnn res ki codes phi atom) +holesSynthesizeM hF oF cF + = holesAnnCataM (\a phi -> flip Hole phi <$> hF a phi) + (\a o -> flip HOpq o <$> oF a o) + (\a c p -> (\r -> HPeel r c p) <$> cF a c (mapNP holesAnn p)) + +-- |Pure variant of 'holesSynthesize' +holesSynthesize :: (forall at . ann at -> phi at -> res at) -- ^ + -> (forall k . ann ('K k) -> ki k -> res ('K k)) + -> (forall i n . (IsNat i, IsNat n) + => ann ('I i) -> Constr (Lkup i codes) n + -> NP res (Lkup n (Lkup i codes)) + -> res ('I i)) + -> HolesAnn ann ki codes phi ix + -> HolesAnn res ki codes phi ix +holesSynthesize hF oF cF = runIdentity + . holesSynthesizeM (\a phi -> return $ hF a phi) + (\a o -> return $ oF a o) + (\a c p -> return $ cF a c p) + +-- * Using 'Holes' with no annotations + +-- |Ignoring the annotations is easy; just use +-- @Const ()@ +type Holes = HolesAnn (Const ()) + +pattern Hole' :: phi at -> Holes ki codes phi at +pattern Hole' x = Hole (Const ()) x + +pattern HOpq' :: ki k -> Holes ki codes phi ('K k) +pattern HOpq' x = HOpq (Const ()) x + +pattern HPeel' :: () => (IsNat n, IsNat i) + => Constr (Lkup i codes) n + -> NP (Holes ki codes phi) (Lkup n (Lkup i codes)) + -> Holes ki codes phi ('I i) +pattern HPeel' c p = HPeel (Const ()) c p + +-- |Factors out the largest common prefix of two treefixes. +-- This is also known as the anti-unification of two +-- treefixes. +-- +-- It enjoys naturality properties with holesJoin: +-- +-- > holesJoin (holesMap fst (holesLCP p q)) == p +-- > holesJoin (holesMap snd (holesLCP p q)) == q +-- +-- We use a function to combine annotations in case it is +-- necessary. +holesLCP :: (EqHO ki) + => Holes ki codes f at + -> Holes ki codes g at + -> Holes ki codes (Holes ki codes f :*: Holes ki codes g) at +holesLCP (HOpq _ kx) (HOpq _ ky) + | eqHO kx ky = HOpq' kx + | otherwise = Hole' (HOpq' kx :*: HOpq' ky) +holesLCP (HPeel a cx px) (HPeel b cy py) + = case testEquality cx cy of + Nothing -> Hole' (HPeel a cx px :*: HPeel b cy py) + Just Refl -> HPeel' cx $ mapNP (uncurry' holesLCP) (zipNP px py) +holesLCP x y = Hole' (x :*: y) + +-- * Translating between 'NA' and 'HolesAnn' + +-- |A stiff treefix is one with no holes anywhere. +na2holes :: NA ki (Fix ki codes) at -> HolesAnn (Const ()) ki codes f at +na2holes (NA_K k) = HOpq' k +na2holes (NA_I x) = case sop (unFix x) of + Tag cx px -> HPeel' cx (mapNP na2holes px) + +-- |Reduces a treefix back to a tree; we use a monadic +-- function here to allow for custom failure confitions. +holes2naM :: (Monad m) + => (forall ix . f ix -> m (NA ki (Fix ki codes) ix)) -- ^ + -> Holes ki codes f at + -> m (NA ki (Fix ki codes) at) +holes2naM red (Hole _ x) = red x +holes2naM _ (HOpq _ k) = return (NA_K k) +holes2naM red (HPeel _ c p) = (NA_I . Fix . inj c) <$> mapNPM (holes2naM red) p + +-- |Returns how many holes are inside a treefix +holesArity :: HolesAnn ann ki codes f at -> Int +holesArity = length . holesGetHolesAnnWith' (const ()) + +-- |Returns the size of a treefix. Holes have size 0. +holesSize :: HolesAnn ann ki codes f at -> Int +holesSize (Hole _ _) = 0 +holesSize (HOpq _ _) = 1 +holesSize (HPeel _ _ p) = 1 + sum (elimNP holesSize p) + +-- |Returns the singleton identifying the index of a 'HolesAnn' +holesSNat :: (IsNat ix) + => HolesAnn ann ki codes f ('I ix) + -> SNat ix +holesSNat _ = getSNat (Proxy :: Proxy ix) + +-- -* Instances + +instance (EqHO phi , EqHO ki) => Eq (Holes ki codes phi ix) where + utx == uty = and $ holesGetHolesAnnWith' (uncurry' cmp) $ holesLCP utx uty + where + cmp :: HolesAnn ann ki codes phi at -> HolesAnn ann ki codes phi at -> Bool + cmp (Hole _ x) (Hole _ y) = eqHO x y + cmp (HOpq _ x) (HOpq _ y) = eqHO x y + cmp _ _ = False + +instance (EqHO phi , EqHO ki) => EqHO (Holes ki codes phi) where + eqHO utx uty = utx == uty + +holesShow :: forall ki ann f fam codes ix + . (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f) + => Proxy fam + -> (forall at . ann at -> ShowS) + -> HolesAnn ann ki codes f ix + -> ShowS +holesShow _ f (Hole a x) = ('`':) . f a . showString (showHO x) +holesShow _ f (HOpq a k) = f a . showString (showHO k) +holesShow p f h@(HPeel a c rest) + = showParen (needParens h) $ showString cname + . f a + . showString " " + . withSpaces (elimNP (holesShow p f) rest) + where + withSpaces :: [ShowS] -> ShowS + withSpaces ls = foldl (\r ss -> r . showString " " . ss) id ls + + cname = case constrInfoFor p (holesSNat h) c of + (Record name _) -> name + (Constructor name) -> name + (Infix name _ _) -> "(" ++ name ++ ")" + + needParens :: HolesAnn ann ki codes f iy -> Bool + needParens (Hole _ _) = False + needParens (HOpq _ _) = False + needParens (HPeel _ _ NP0) = False + needParens _ = True + +instance {-# OVERLAPPABLE #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f , ShowHO ann) + => ShowHO (HolesAnn ann ki codes f) where + showHO h = holesShow (Proxy :: Proxy fam) showsAnn h "" + where + showsAnn ann = showString "{" + . showString (showHO ann) + . showString "}" + +instance {-# OVERLAPPABLE #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f , ShowHO ann) + => Show (HolesAnn ann ki codes f at) where + show = showHO + +instance {-# OVERLAPPING #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f) + => ShowHO (Holes ki codes f) where + showHO h = holesShow (Proxy :: Proxy fam) (const id) h "" + +instance {-# OVERLAPPING #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f) + => Show (Holes ki codes f at) where + show = showHO diff --git a/src/Generics/MRSOP/Opaque.hs b/src/Generics/MRSOP/Opaque.hs --- a/src/Generics/MRSOP/Opaque.hs +++ b/src/Generics/MRSOP/Opaque.hs @@ -49,8 +49,16 @@ SChar :: Char -> Singl 'KChar SString :: String -> Singl 'KString -deriving instance Show (Singl k) deriving instance Eq (Singl k) + +instance Show (Singl k) where + show (SInt a) = show a + show (SInteger a) = show a + show (SFloat a) = show a + show (SDouble a) = show a + show (SBool a) = show a + show (SChar a) = show a + show (SString a) = show a instance EqHO Singl where eqHO = (==) diff --git a/src/Generics/MRSOP/TH.hs b/src/Generics/MRSOP/TH.hs --- a/src/Generics/MRSOP/TH.hs +++ b/src/Generics/MRSOP/TH.hs @@ -7,11 +7,144 @@ {-# OPTIONS_GHC -cpp #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} {-# OPTIONS_GHC -Wno-unused-pattern-binds #-} --- | Provides a simple way for the end-user deriving --- the mechanical, yet long, Element instances --- for a family. +-- | Provides a simple way for the end-user to derive +-- the 'Family' instance for a mutually recursive family. -- --- We are borrowing a some code from generic-sop +-- Let's take a simple example: +-- +-- > data Rose a = a :>: [Rose a] | Leaf a +-- > deriveFamily [t| Rose Int |] +-- +-- Will derive the following code: +-- +-- > type FamRoseInt = '[Rose Int, [Rose Int]] +-- > type CodesRoseInt = '['['[K KInt, I (S Z)], '[K KInt]], '['[], '[I Z, I (S Z)]]] +-- > +-- > -- Type index SNat synonyms +-- > pattern IdxRoseInt = SZ +-- > pattern IdxListRoseInt = SS SZ +-- > +-- > -- (:>:) pattern syn +-- > pattern RoseInt_Ifx0 :: kon KInt -> phi (S Z) -> View kon phi (Lkup Z CodesRoseInt) +-- > pattern RoseInt_Ifx0 p q = Tag CZ (NA_K p :* (NA_I q :* NP0)) +-- > +-- > -- Leaf pattern syn +-- > pattern RoseIntLeaf_ :: kon KInt -> View kon phi (Lkup Z CodesRoseInt) +-- > pattern RoseIntLeaf_ p = Tag (CS CZ) (NA_K p :* NP0) +-- > +-- > -- [] pattern syn +-- > pattern ListRoseInt_Ifx0 :: View kon phi (Lkup (S Z) CodesRoseInt) +-- > pattern ListRoseInt_Ifx0 = Tag CZ NP0 +-- > +-- > -- (:) pattern syn +-- > pattern ListRoseInt_Ifx1 :: phi Z -> phi (S Z) -> View kon phi (Lkup (S Z) CodesRoseInt) +-- > pattern ListRoseInt_Ifx1 p q = Tag (CS CZ) (NA_I p :* (NA_I q :* NP0)) +-- > +-- > instance Family Singl FamRose CodesRose where +-- > sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0) +-- > sfrom' (SS SZ) (El (Leaf a)) = Rep $ There (Here (NA_K (SInt a) :* NP0)) +-- > sfrom' SZ (El []) = Rep $ Here NP0 +-- > sfrom' SZ (El (x:xs)) = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* NP0)) +-- > sfrom' _ _ = error "unreachable" +-- > +-- > sto' SZ (Rep (Here NP0)) +-- > = El [] +-- > sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0)))) +-- > = El (x : xs) +-- > sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0))) +-- > = El (a :>: as) +-- > sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0)))) +-- > = El (Leaf a) +-- > sto' _ _ = error "unreachable" +-- > +-- > instance HasDatatypeInfo Singl FamRose CodesRose where +-- > datatypeInfo _ SZ +-- > = ADT "module" (Name "[]" :@: (Name "R" :@: Name "Int")) +-- > $ (Constructor "[]") +-- > :* (Infix ":" RightAssociative 5) +-- > :* NP0 +-- > datatypeInfo _ (SS SZ) +-- > = ADT "module" (Name "R" :@: Name "Int") +-- > $ (Infix ":>:" NotAssociative 0) +-- > :* (Constructor "Leaf") +-- > :* NP0 +-- > datatypeInfo _ _ +-- > = error "unreachable" +-- +-- To illustrate the pattern synonym generation, let us look at a selection +-- of a more involved example +-- +-- Consider the following family: +-- +-- > data Stmt var +-- > = SAssign var (Exp var) +-- > | SIf (Exp var) (Stmt var) (Stmt var) +-- > | SSeq (Stmt var) (Stmt var) +-- > | SReturn (Exp var) +-- > | SDecl (Decl var) +-- > | SSkip +-- > deriving Show +-- > +-- > data Decl var +-- > = DVar var +-- > | DFun var var (Stmt var) +-- > deriving Show +-- > +-- > data Exp var +-- > = EVar var +-- > | ECall var (Exp var) +-- > | EAdd (Exp var) (Exp var) +-- > | ESub (Exp var) (Exp var) +-- > | ELit Int +-- > deriving Show +-- > +-- +-- In this case, running @deriveFamily [t| Stmt String |]@ will +-- generate the following types: +-- +-- > type FamStmtString = '[Stmt String, Exp String, Decl String] +-- > type CodesStmtString = +-- > '['['[K KString, I (S Z)], +-- > '[I (S Z), I Z, I Z], +-- > '[I Z, I Z], +-- > '[I (S Z)], +-- > '[I (S (S Z))], +-- > '[]], +-- > '['[K KString], +-- > '[K KString, I (S Z)], +-- > '[I (S Z), I (S Z)], +-- > '[I (S Z), I (S Z)], +-- > '[K KInt]], +-- > '['[K KString], '[K KString, K KString, I Z]]] +-- > pattern IdxStmtString = SZ +-- > pattern IdxExpString = SS SZ +-- > pattern IdxDeclString = SS (SS SZ) +-- > +-- > -- Here are the declared patterns for 'View' +-- > pattern StmtStringSAssign_ +-- > pattern StmtStringSIf_ +-- > pattern StmtStringSSeq_ +-- > pattern StmtStringSReturn_ +-- > pattern StmtStringSDecl_ +-- > pattern StmtStringSSkip_ +-- > pattern ExpStringEVar_ +-- > pattern ExpStringECall_ +-- > pattern ExpStringEAdd_ +-- > pattern ExpStringESub_ +-- > pattern ExpStringELit_ +-- > pattern DeclStringDVar_ +-- > pattern DeclStringDFun_ +-- +-- We did ommit the definitions and 'Family' and 'HasDatatypeInfo' instances +-- for brevity here. If you want to see the actual generated code, compile with +-- +-- > stack build ghc-options="-ddump-splices -ddump-to-file" +-- +-- You can find the spliced files with +-- +-- > find -name "*.dump-splices" +-- +-- This module was based in the TH generication from /generic-sop/ -- ( https://hackage.haskell.org/package/generics-sop-0.3.2.0/docs/src/Generics-SOP-TH.html ) -- module Generics.MRSOP.TH @@ -68,9 +201,9 @@ -- types m' <- mapM extractDTI (M.toList m) let final = sortBy (compare `on` second) m' - dbg <- genFamilyDebug sty final + -- dbg <- genFamilyDebug sty final res <- genFamily opqData sty final - return (dbg ++ res) + return res -- (dbg ++ res) where second (_ , x , _) = x @@ -79,6 +212,7 @@ extractDTI (sty , (ix , Just dti)) = return (sty , ix , dti) +-- |Reifies the type given for opaque types, then calls 'deriveFamilyWith' deriveFamilyWithTy :: Q Type -> Q Type -> Q [Dec] deriveFamilyWithTy opq ty = do opqTy <- opq @@ -86,6 +220,7 @@ ConT opqName -> deriveFamilyWith opqName ty _ -> fail $ "Type " ++ show opqTy ++ " must be a name!" +-- |Same as @deriveFamilyWith ''Singl@ deriveFamily :: Q Type -> Q [Dec] deriveFamily = deriveFamilyWith (mkName "Singl") @@ -616,14 +751,13 @@ genPiece1 :: STy -> Input -> Q [Dec] genPiece1 first ls - = do -- nums <- inputToTySynNums ls -- TODO: Remove this hack - codes <- TySynD <$> codesName first + = do codes <- TySynD <$> codesName first <*> return [] <*> inputToCodes ls fam <- TySynD <$> familyName first <*> return [] <*> inputToFam ls - return [fam , codes] -- (nums ++ [fam , codes]) + return [fam , codes] idxPatSynName :: STy -> Name idxPatSynName = styToName . (AppST (ConST (mkName "Idx"))) @@ -861,13 +995,15 @@ match pat bdy = Match pat (NormalB bdy) [] -- Adds a matchall clause; for instance: +-- VCM: Jul24: We used this to try to bypass the coverage checker, with no luck. +-- I'll comment this out -- -- > matchAll [Just x -> 1] = [Just x -> 1 , _ -> error "matchAll"] -- -matchAll :: [Match] -> [Match] -matchAll = (++ [match WildP err]) - where - err = AppE (VarE (mkName "error")) (LitE (StringL "matchAll")) +-- matchAll :: [Match] -> [Match] +-- matchAll = (++ [match WildP err]) +-- where +-- err = AppE (VarE (mkName "error")) (LitE (StringL "matchAll")) genPiece3_1 :: OpaqueData -> Input -> Q Exp genPiece3_1 opq input @@ -883,16 +1019,17 @@ genPiece3_2 :: OpaqueData -> Input -> Q Exp genPiece3_2 opq input - = LamCaseE . matchAll <$> mapM (\(sty , ix , dti) -> clauseForIx sty ix dti) input + = LamCaseE <$> mapM (\(sty , ix , dti) -> clauseForIx sty ix dti) input where clauseForIx :: STy -> Int -> DTI IK -> Q Match clauseForIx sty ix dti = match (idxPatSyn sty) - <$> (LamCaseE . matchAll <$> genMatchFor ix dti) + <$> (LamCaseE <$> genMatchFor ix dti) genMatchFor :: Int -> DTI IK -> Q [Match] genMatchFor ix dti = map (uncurry match) <$> mapM (uncurry $ ci2ExpPat opq ix) (zip [0..] $ dti2ci dti) +-- Metadata generation genPiece4 :: OpaqueData -> STy -> Input -> Q [Dec] genPiece4 opq first ls = [d| instance Meta.HasDatatypeInfo $opqName @@ -951,18 +1088,19 @@ -- |@genFamily opq init fam@ generates a type-level list -- of the codes for the family. It also generates --- the necessary 'Element' instances. +-- the necessary 'Family' and 'HasDatatypeInfo' instances. -- -- Precondition, input is sorted on second component. genFamily :: OpaqueData -> STy -> Input -> Q [Dec] genFamily opq first ls - = do p1 <- genPiece1 first ls - p2 <- genPiece2 opq first ls - p3 <- genPiece3 opq first ls - p4 <- genPiece4 opq first ls + = do p1 <- genPiece1 first ls -- Family and codes + p2 <- genPiece2 opq first ls -- Pattern Synonyms + p3 <- genPiece3 opq first ls -- Family instance + p4 <- genPiece4 opq first ls -- Metadata instance return $ p1 ++ p2 ++ [p3] ++ p4 -- |Generates a bunch of strings for debug purposes. +-- The generated strings are named @tyInfo_0, tyInfo_1, ...@ genFamilyDebug :: STy -> [(STy , Int , DTI IK)] -> Q [Dec] genFamilyDebug _ ms = concat <$> mapM genDec ms where