From b00b9e1545488e5580ff5888b5667f433de4c315 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Sun, 14 Jul 2019 14:37:13 +0200 Subject: [PATCH 01/15] Preparing to work on version 2.1.0 --- generics-mrsop.cabal | 4 +++- src/Generics/MRSOP/Holes.hs | 0 src/Generics/MRSOP/Holes/Simple.hs | 0 3 files changed, 3 insertions(+), 1 deletion(-) create mode 100644 src/Generics/MRSOP/Holes.hs create mode 100644 src/Generics/MRSOP/Holes/Simple.hs diff --git a/generics-mrsop.cabal b/generics-mrsop.cabal index 10f74e4..e6c8157 100644 --- 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,8 @@ library Generics.MRSOP.Base, Generics.MRSOP.Opaque, Generics.MRSOP.Util, + Generics.MRSOP.Holes.Simple + Generics.MRSOP.Holes Generics.MRSOP.TH, Generics.MRSOP.Zipper, Generics.MRSOP.Zipper.Deep, diff --git a/src/Generics/MRSOP/Holes.hs b/src/Generics/MRSOP/Holes.hs new file mode 100644 index 0000000..e69de29 diff --git a/src/Generics/MRSOP/Holes/Simple.hs b/src/Generics/MRSOP/Holes/Simple.hs new file mode 100644 index 0000000..e69de29 From 16cef487bf927813d7c07be9e50d5f4e88a2a9b8 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Sun, 14 Jul 2019 16:06:36 +0200 Subject: [PATCH 02/15] Brought in a number of functionalities over holed families --- src/Generics/MRSOP/Holes.hs | 240 ++++++++++++++++++++++++++++++++++++ 1 file changed, 240 insertions(+) diff --git a/src/Generics/MRSOP/Holes.hs b/src/Generics/MRSOP/Holes.hs index e69de29..5ad4467 100644 --- a/src/Generics/MRSOP/Holes.hs +++ b/src/Generics/MRSOP/Holes.hs @@ -0,0 +1,240 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Generics.MRSOP.Holes where + +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.Util +import Generics.MRSOP.Base + +-- * Questions + +-- Maybe the 'Hole' constructor should have no annotation + +-- * Generic Treefixes + +-- |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. +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. + 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)) + -> (forall a . ann a -> m (bnn a)) + -> 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 + -> (r -> f r -> f r) + -> (forall ix . phi ix -> r) + -> 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. +holesGetHolesAnnWith' :: (forall ix . phi ix -> r) -> HolesAnn ann ki codes phi at -> [r] +holesGetHolesAnnWith' = holesGetHolesAnnWith [] (:) + +-- |Instantiates 'holesGetHolesAnnWith' to use a set. +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. +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. +holesRefineVarsM :: (Monad m) + => (forall ix . ann ix -> f ix -> m (HolesAnn ann ki codes g ix)) + -> 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) + +-- * Using 'Holes' with no annotations + +-- |Ignoring the annotations is easy; just use +-- @Const ()@ +type Holes = HolesAnn (Const ()) + +hole :: phi at -> Holes ki codes phi at +hole = Hole (Const ()) + +hopq :: ki k -> Holes ki codes phi ('K k) +hopq = HOpq (Const ()) + +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) +hpeel = HPeel (Const ()) + +-- |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 + +-- * 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 + From b89ec499d9a0ce603804db6793c3341a3f43dcf7 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Sun, 14 Jul 2019 16:07:38 +0200 Subject: [PATCH 03/15] turns out we will not need a 'simple' variant --- generics-mrsop.cabal | 1 - src/Generics/MRSOP/Holes/Simple.hs | 0 2 files changed, 1 deletion(-) delete mode 100644 src/Generics/MRSOP/Holes/Simple.hs diff --git a/generics-mrsop.cabal b/generics-mrsop.cabal index e6c8157..b1a27bb 100644 --- a/generics-mrsop.cabal +++ b/generics-mrsop.cabal @@ -36,7 +36,6 @@ library Generics.MRSOP.Base, Generics.MRSOP.Opaque, Generics.MRSOP.Util, - Generics.MRSOP.Holes.Simple Generics.MRSOP.Holes Generics.MRSOP.TH, Generics.MRSOP.Zipper, diff --git a/src/Generics/MRSOP/Holes/Simple.hs b/src/Generics/MRSOP/Holes/Simple.hs deleted file mode 100644 index e69de29..0000000 From 1c6caa45bd8a7b82731175c08467349efcb7e7da Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Mon, 15 Jul 2019 11:01:34 +0200 Subject: [PATCH 04/15] Brougt in more functionality for 'Holes' --- src/Generics/MRSOP/Holes.hs | 86 +++++++++++++++++++++++++++++++------ 1 file changed, 72 insertions(+), 14 deletions(-) diff --git a/src/Generics/MRSOP/Holes.hs b/src/Generics/MRSOP/Holes.hs index 5ad4467..abf2ed3 100644 --- a/src/Generics/MRSOP/Holes.hs +++ b/src/Generics/MRSOP/Holes.hs @@ -1,12 +1,9 @@ {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE TupleSections #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} module Generics.MRSOP.Holes where @@ -20,10 +17,6 @@ import Control.Monad.State import Generics.MRSOP.Util import Generics.MRSOP.Base --- * Questions - --- Maybe the 'Hole' constructor should have no annotation - -- * Generic Treefixes -- |A value of type 'HolesAnn' augments a mutually recursive @@ -116,11 +109,11 @@ holesJoin (HPeel a c p) = HPeel a c (mapNP holesJoin p) -- 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 - -> (r -> f r -> f r) - -> (forall ix . phi ix -> r) - -> HolesAnn ann ki codes phi at - -> f r + . f r + -> (r -> f r -> f r) + -> (forall ix . phi ix -> r) + -> HolesAnn ann ki codes phi at + -> f r holesGetHolesAnnWith empty ins tr = flip execState empty . holesMapM getHole where @@ -129,12 +122,14 @@ holesGetHolesAnnWith empty ins tr getHole x = modify (ins $ tr x) >> return x -- |Instantiates 'holesGetHolesAnnWith' to use a list. -holesGetHolesAnnWith' :: (forall ix . phi ix -> r) -> HolesAnn ann ki codes phi at -> [r] +holesGetHolesAnnWith' :: (forall ix . phi ix -> r) + -> HolesAnn ann ki codes phi at -> [r] holesGetHolesAnnWith' = holesGetHolesAnnWith [] (:) -- |Instantiates 'holesGetHolesAnnWith' to use a set. holesGetHolesAnnWith'' :: (Ord r) - => (forall ix . phi ix -> r) -> HolesAnn ann ki codes phi at -> S.Set r + => (forall ix . phi ix -> r) + -> HolesAnn ann ki codes phi at -> S.Set r holesGetHolesAnnWith'' = holesGetHolesAnnWith S.empty S.insert -- * Refining 'HolesAnn' @@ -165,6 +160,69 @@ holesRefineAnn :: (forall ix . ann ix -> f ix -> HolesAnn ann ki codes g ix) -> 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)) + -> (forall k . ann ('K k) -> ki k -> m (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)) + -> m (res ('I i))) + -> 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) + -> (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 + -> 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)) + -> (forall k . ann ('K k) -> ki k -> m (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)) + -> m (res ('I i))) + -> HolesAnn ann ki codes phi atom + -> 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 From 1c8b08d42030f08f97041b4b4a597400078170c1 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Mon, 15 Jul 2019 15:12:52 +0200 Subject: [PATCH 05/15] Added pattern synonyms for better use of the un-annotated holes --- src/Generics/MRSOP/Holes.hs | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/src/Generics/MRSOP/Holes.hs b/src/Generics/MRSOP/Holes.hs index abf2ed3..98a70e0 100644 --- a/src/Generics/MRSOP/Holes.hs +++ b/src/Generics/MRSOP/Holes.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeOperators #-} @@ -229,17 +230,17 @@ holesSynthesize hF oF cF = runIdentity -- @Const ()@ type Holes = HolesAnn (Const ()) -hole :: phi at -> Holes ki codes phi at -hole = Hole (Const ()) +pattern Hole' :: phi at -> Holes ki codes phi at +pattern Hole' x = Hole (Const ()) x -hopq :: ki k -> Holes ki codes phi ('K k) -hopq = HOpq (Const ()) +pattern HOpq' :: ki k -> Holes ki codes phi ('K k) +pattern HOpq' x = HOpq (Const ()) x -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) -hpeel = HPeel (Const ()) +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 @@ -257,21 +258,21 @@ holesLCP :: (EqHO ki) -> 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) + | 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) + 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_K k) = HOpq' k na2holes (NA_I x) = case sop (unFix x) of - Tag cx px -> hpeel cx (mapNP na2holes px) + 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. From d8b8e9564ee7de3cff65d5790c03799b1046f7d2 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Mon, 15 Jul 2019 15:17:36 +0200 Subject: [PATCH 06/15] closes #48 --- src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs | 1 + src/Generics/MRSOP/Examples/RoseTree.hs | 1 + src/Generics/MRSOP/Examples/RoseTreeTH.hs | 1 + src/Generics/MRSOP/Examples/SimpTH.hs | 1 + 4 files changed, 4 insertions(+) diff --git a/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs b/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs index 50f93d2..ffb0f6f 100644 --- 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 index 204e610..f755443 100644 --- a/src/Generics/MRSOP/Examples/RoseTree.hs +++ b/src/Generics/MRSOP/Examples/RoseTree.hs @@ -10,6 +10,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE PatternSynonyms #-} +{-# OPTIONS_HADDOCK hide, prune, ignore-exports #-} {-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-} {-# OPTIONS_GHC -Wno-incomplete-patterns #-} {-# OPTIONS_GHC -Wno-orphans #-} diff --git a/src/Generics/MRSOP/Examples/RoseTreeTH.hs b/src/Generics/MRSOP/Examples/RoseTreeTH.hs index 451cde1..59ece95 100644 --- 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 index 47474ec..c06a90b 100644 --- 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 #-} From b22aeb8f1c7c46019b9290b20d5290836e881f25 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Mon, 15 Jul 2019 15:46:34 +0200 Subject: [PATCH 07/15] consistent naming --- src/Generics/MRSOP/Base/Universe.hs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Generics/MRSOP/Base/Universe.hs b/src/Generics/MRSOP/Base/Universe.hs index af34bfb..ce49634 100644 --- a/src/Generics/MRSOP/Base/Universe.hs +++ b/src/Generics/MRSOP/Base/Universe.hs @@ -64,7 +64,7 @@ instance (TestEquality ki) => TestEquality (NA ki phi) where 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') = @@ -301,8 +301,9 @@ cata f (Fix x) = f (mapRep (cata f) x) 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. From 987e5a3eef4d59422ef724e92497339664435d13 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Wed, 17 Jul 2019 15:05:58 +0200 Subject: [PATCH 08/15] Major documentation update --- src/Generics/MRSOP/AG.hs | 116 ++++++++++++++++-------- src/Generics/MRSOP/Base.hs | 14 ++- src/Generics/MRSOP/Examples/RoseTree.hs | 103 +++++++++++++++++++-- src/Generics/MRSOP/Holes.hs | 97 ++++++++++++++------ src/Generics/MRSOP/TH.hs | 52 ++++++++++- 5 files changed, 306 insertions(+), 76 deletions(-) diff --git a/src/Generics/MRSOP/AG.hs b/src/Generics/MRSOP/AG.hs index eef040e..cb5228e 100644 --- a/src/Generics/MRSOP/AG.hs +++ b/src/Generics/MRSOP/AG.hs @@ -11,36 +11,78 @@ module Generics.MRSOP.AG where 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 + +-- |Example of using 'synthesize' to annotate a tree with its size +-- at every node. +synthesize :: forall ki phi codes ix + . (IsNat ix) + => (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 + where + alg :: forall iy + . (IsNat iy) + => Rep ki (AnnFix ki codes phi) (Lkup iy codes) + -> AnnFix ki codes phi iy + alg xs = AnnFix (f (mapRep getAnn xs)) 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) + => (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 @@ -51,35 +93,37 @@ synthesizeAnn f = annCata alg -> AnnFix ki codes phi iy alg ann rep = AnnFix (f ann (mapRep getAnn rep)) rep +-- * Monadic Variants --- |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 +-- $monadicvariants -- -synthesize :: forall ki phi codes ix - . (IsNat ix) - => (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 +-- These will rarely be needed. And are not /catamorphisms/ or /synthesized attributes/ +-- per se, but have shown to be incredibly useful in some other internal projects +-- where we use /generics-mrsop/. We are leaving them in the library in case +-- they see some other usecases. + +-- |Generalized catamorphism, with an auxiliary function that can +-- modify the result or perform a monadic action based on the value +-- being processed. Care must be taken to /not/ consume the value in the +-- first argument. +cataM' :: (Monad m , IsNat ix) + => (forall iy a. IsNat iy => Fix ki codes iy -> m a -> m a) -- ^ + -> (forall iy . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy)) + -> Fix ki codes ix + -> m (phi ix) +cataM' p f xo@(Fix x) = mapRepM (p xo . cataM' p f) x >>= f + +-- |Synthesizes an annotated fixpoint based on 'cataM'' +synthesizeM' :: forall ki phi codes ix m + . (Monad m , IsNat ix) + => (forall iy a. IsNat iy => Fix ki codes iy -> m a -> m a) -- ^ + -> (forall iy . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy)) + -> Fix ki codes ix + -> m (AnnFix ki codes phi ix) +synthesizeM' p f = cataM' p alg where alg :: forall iy . (IsNat iy) => Rep ki (AnnFix ki codes phi) (Lkup iy codes) - -> AnnFix ki codes phi iy - alg xs = AnnFix (f (mapRep getAnn xs)) xs - + -> m (AnnFix ki codes phi iy) + alg xs = flip AnnFix xs <$> f (mapRep getAnn xs) diff --git a/src/Generics/MRSOP/Base.hs b/src/Generics/MRSOP/Base.hs index bba4946..99de923 100644 --- 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/Examples/RoseTree.hs b/src/Generics/MRSOP/Examples/RoseTree.hs index f755443..f86073c 100644 --- a/src/Generics/MRSOP/Examples/RoseTree.hs +++ b/src/Generics/MRSOP/Examples/RoseTree.hs @@ -10,21 +10,40 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE PatternSynonyms #-} -{-# OPTIONS_HADDOCK hide, prune, ignore-exports #-} {-# 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 @@ -34,16 +53,56 @@ value1 = 1 :>: [2 :>: [], 3 :>: []] 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)) @@ -75,19 +134,41 @@ instance HasDatatypeInfo Singl FamRose CodesRose where 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 @@ -95,8 +176,14 @@ normalize = unEl . go (SS SZ) . into 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/Holes.hs b/src/Generics/MRSOP/Holes.hs index 98a70e0..098d3ba 100644 --- a/src/Generics/MRSOP/Holes.hs +++ b/src/Generics/MRSOP/Holes.hs @@ -18,7 +18,40 @@ import Control.Monad.State import Generics.MRSOP.Util import Generics.MRSOP.Base --- * Generic Treefixes +-- * 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 @@ -49,10 +82,10 @@ data HolesAnn :: (Atom kon -> *) -- |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. + -- by treefixes. This already comes in a SOP flavour. HPeel :: (IsNat n , IsNat i) => ann ('I i) - -> Constr (Lkup i codes) n + -> Constr (Lkup i codes) n -> NP (HolesAnn ann ki codes phi) (Lkup n (Lkup i codes)) -> HolesAnn ann ki codes phi ('I i) @@ -66,8 +99,8 @@ holesAnn (HPeel a _ _) = a -- |Our 'HolesAnn' is a higher order functor and can be mapped over. holesMapAnnM :: (Monad m) - => (forall a . f a -> m (g a)) - -> (forall a . ann a -> m (bnn a)) + => (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 @@ -110,10 +143,10 @@ holesJoin (HPeel a c p) = HPeel a c (mapNP holesJoin p) -- 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 - -> (r -> f r -> f r) - -> (forall ix . phi ix -> r) - -> HolesAnn 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 @@ -123,11 +156,14 @@ holesGetHolesAnnWith empty ins tr 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. +-- |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 @@ -136,7 +172,10 @@ holesGetHolesAnnWith'' = holesGetHolesAnnWith S.empty S.insert -- * Refining 'HolesAnn' -- |Similar to 'holesMapM', but allows to refine the structure of --- a treefix if need be. +-- 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))) @@ -147,15 +186,19 @@ 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. +-- |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)) + => (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) +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 @@ -166,12 +209,12 @@ holesRefineAnn f g = runIdentity . holesRefineAnnM (\a -> return . f a) (\a -> r -- |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)) - -> (forall k . ann ('K k) -> ki k -> m (res ('K k))) + => (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))) + -> 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 @@ -180,12 +223,12 @@ 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) - -> (forall k . ann ('K k) -> ki k -> res ('K k)) +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)) + -> res ('I i)) -- ^ Action to perform at 'HPeel' -> HolesAnn ann ki codes phi ix -> res ix holesAnnCata hF oF cF = runIdentity @@ -197,13 +240,13 @@ holesAnnCata hF oF cF = runIdentity -- is extremely useful for easily annotating a value with auxiliar -- annotations. holesSynthesizeM :: (Monad m) - => (forall at . ann at -> phi at -> m (res at)) - -> (forall k . ann ('K k) -> ki k -> m (res ('K k))) + => (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))) - -> HolesAnn ann ki codes phi atom + -> 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) @@ -211,7 +254,7 @@ holesSynthesizeM hF oF cF (\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) +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 @@ -277,14 +320,14 @@ na2holes (NA_I x) = case sop (unFix x) of -- |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)) + => (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 --- * Instances +-- -* Instances instance (EqHO phi , EqHO ki) => Eq (Holes ki codes phi ix) where utx == uty = and $ holesGetHolesAnnWith' (uncurry' cmp) $ holesLCP utx uty diff --git a/src/Generics/MRSOP/TH.hs b/src/Generics/MRSOP/TH.hs index 1c01ed6..dd02df3 100644 --- a/src/Generics/MRSOP/TH.hs +++ b/src/Generics/MRSOP/TH.hs @@ -7,11 +7,55 @@ {-# 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 +-- For example, +-- +-- > data Rose a = a :>: [Rose a] | Leaf a +-- > deriveFamily [t| Rose Int |] +-- +-- Will derive the following code: +-- +-- > type ListCode = '[ '[] , '[ 'I ('S 'Z) , 'I 'Z] ] +-- > type RTCode = '[ '[ 'K 'KInt , 'I 'Z] , '[ 'K 'KInt] ] +-- > +-- > type CodesRose = '[ListCode , RTCode] +-- > type FamRose = '[ [R Int] , R Int] +-- > +-- > 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" +-- +-- +-- We did inspire this module 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 From 2c6af5a5ea286ddc6f4fef1c441a06ab49f2ced0 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Wed, 17 Jul 2019 16:04:21 +0200 Subject: [PATCH 09/15] Added decent show instances to 'Holes' --- src/Generics/MRSOP/Examples/SimpTH.hs | 16 ++++++- src/Generics/MRSOP/Holes.hs | 66 ++++++++++++++++++++++++++- src/Generics/MRSOP/Opaque.hs | 10 +++- 3 files changed, 89 insertions(+), 3 deletions(-) diff --git a/src/Generics/MRSOP/Examples/SimpTH.hs b/src/Generics/MRSOP/Examples/SimpTH.hs index c06a90b..642081b 100644 --- a/src/Generics/MRSOP/Examples/SimpTH.hs +++ b/src/Generics/MRSOP/Examples/SimpTH.hs @@ -21,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 @@ -173,7 +175,6 @@ test4 :: Int -> Decl String test4 n = DFun "test" "n" $ (SAssign "x" (EAdd (ELit 10) (ELit n))) `SSeq` (SReturn (EVar "x")) - test5 :: Maybe (Decl String) test5 = enter @@ -191,3 +192,16 @@ test5 = enter 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 index 098d3ba..b92a1fa 100644 --- a/src/Generics/MRSOP/Holes.hs +++ b/src/Generics/MRSOP/Holes.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE RankNTypes #-} @@ -8,6 +9,7 @@ {-# 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) @@ -15,7 +17,6 @@ import qualified Data.Set as S (insert , empty , Set) import Control.Monad.Identity import Control.Monad.State -import Generics.MRSOP.Util import Generics.MRSOP.Base -- * Annotating a Mutually Recursive Family with Holes @@ -327,6 +328,22 @@ 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 @@ -340,3 +357,50 @@ instance (EqHO phi , EqHO ki) => Eq (Holes ki codes phi ix) where 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 -> ss . showString " " . r) 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 index acefe4c..549b727 100644 --- a/src/Generics/MRSOP/Opaque.hs +++ b/src/Generics/MRSOP/Opaque.hs @@ -49,9 +49,17 @@ data Singl (kon :: Kon) :: * where 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 = (==) From 29f3f2f4e1a0689023af2a0f8c1403db37970916 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Thu, 18 Jul 2019 10:12:30 +0200 Subject: [PATCH 10/15] fixed comments --- src/Generics/MRSOP/AG.hs | 5 +++-- src/Generics/MRSOP/Holes.hs | 3 +++ 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Generics/MRSOP/AG.hs b/src/Generics/MRSOP/AG.hs index cb5228e..2a91176 100644 --- a/src/Generics/MRSOP/AG.hs +++ b/src/Generics/MRSOP/AG.hs @@ -64,8 +64,9 @@ mapAnn :: (IsNat ix) mapAnn f = synthesizeAnn (\x _ -> f x) --- |Example of using 'synthesize' to annotate a tree with its size --- at every node. +-- |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) -- ^ diff --git a/src/Generics/MRSOP/Holes.hs b/src/Generics/MRSOP/Holes.hs index b92a1fa..d22af10 100644 --- a/src/Generics/MRSOP/Holes.hs +++ b/src/Generics/MRSOP/Holes.hs @@ -71,6 +71,9 @@ import Generics.MRSOP.Base -- 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]]] From a7986713bb929b2166e1dc07e2b6e478ad39ee62 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Thu, 18 Jul 2019 10:30:39 +0200 Subject: [PATCH 11/15] Removed the monadic not-so-catamorphism and not-so-synthesize. Added monadic catamorphism and monadic synthesize. --- src/Generics/MRSOP/AG.hs | 51 +++++++++-------------------- src/Generics/MRSOP/Base/Universe.hs | 10 +++++- 2 files changed, 25 insertions(+), 36 deletions(-) diff --git a/src/Generics/MRSOP/AG.hs b/src/Generics/MRSOP/AG.hs index 2a91176..08c97be 100644 --- a/src/Generics/MRSOP/AG.hs +++ b/src/Generics/MRSOP/AG.hs @@ -80,6 +80,21 @@ synthesize f = cata alg -> 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) @@ -93,38 +108,4 @@ synthesizeAnn f = annCata alg -> Rep ki (AnnFix ki codes phi) (Lkup iy codes) -> AnnFix ki codes phi iy alg ann rep = AnnFix (f ann (mapRep getAnn rep)) rep - --- * Monadic Variants - --- $monadicvariants --- --- These will rarely be needed. And are not /catamorphisms/ or /synthesized attributes/ --- per se, but have shown to be incredibly useful in some other internal projects --- where we use /generics-mrsop/. We are leaving them in the library in case --- they see some other usecases. - --- |Generalized catamorphism, with an auxiliary function that can --- modify the result or perform a monadic action based on the value --- being processed. Care must be taken to /not/ consume the value in the --- first argument. -cataM' :: (Monad m , IsNat ix) - => (forall iy a. IsNat iy => Fix ki codes iy -> m a -> m a) -- ^ - -> (forall iy . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy)) - -> Fix ki codes ix - -> m (phi ix) -cataM' p f xo@(Fix x) = mapRepM (p xo . cataM' p f) x >>= f - --- |Synthesizes an annotated fixpoint based on 'cataM'' -synthesizeM' :: forall ki phi codes ix m - . (Monad m , IsNat ix) - => (forall iy a. IsNat iy => Fix ki codes iy -> m a -> m a) -- ^ - -> (forall iy . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy)) - -> Fix ki codes ix - -> m (AnnFix ki codes phi ix) -synthesizeM' p f = cataM' p 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) + diff --git a/src/Generics/MRSOP/Base/Universe.hs b/src/Generics/MRSOP/Base/Universe.hs index ce49634..e33c7ce 100644 --- a/src/Generics/MRSOP/Base/Universe.hs +++ b/src/Generics/MRSOP/Base/Universe.hs @@ -292,11 +292,19 @@ instance EqHO ki => Eq (Fix ki codes ix) where -- | 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 From 7800072296ccfd260c9f3989f7e31f368705391b Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Wed, 24 Jul 2019 10:43:25 +0200 Subject: [PATCH 12/15] Changed order of argument display --- src/Generics/MRSOP/Holes.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Generics/MRSOP/Holes.hs b/src/Generics/MRSOP/Holes.hs index d22af10..3269a6c 100644 --- a/src/Generics/MRSOP/Holes.hs +++ b/src/Generics/MRSOP/Holes.hs @@ -375,7 +375,7 @@ holesShow p f h@(HPeel a c rest) . withSpaces (elimNP (holesShow p f) rest) where withSpaces :: [ShowS] -> ShowS - withSpaces ls = foldl (\r ss -> ss . showString " " . r) id ls + withSpaces ls = foldl (\r ss -> r . showString " " . ss) id ls cname = case constrInfoFor p (holesSNat h) c of (Record name _) -> name From fd80da65c199a03d102896bdda34c7194318bd00 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Wed, 24 Jul 2019 11:22:01 +0200 Subject: [PATCH 13/15] documentation and small additions --- src/Generics/MRSOP/Base/Universe.hs | 1 - src/Generics/MRSOP/TH.hs | 136 +++++++++++++++++++++++----- 2 files changed, 115 insertions(+), 22 deletions(-) diff --git a/src/Generics/MRSOP/Base/Universe.hs b/src/Generics/MRSOP/Base/Universe.hs index e33c7ce..aac90db 100644 --- a/src/Generics/MRSOP/Base/Universe.hs +++ b/src/Generics/MRSOP/Base/Universe.hs @@ -304,7 +304,6 @@ cataM :: (Monad m , IsNat 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 diff --git a/src/Generics/MRSOP/TH.hs b/src/Generics/MRSOP/TH.hs index dd02df3..0bea042 100644 --- a/src/Generics/MRSOP/TH.hs +++ b/src/Generics/MRSOP/TH.hs @@ -10,18 +10,35 @@ -- | Provides a simple way for the end-user to derive -- the 'Family' instance for a mutually recursive family. -- --- For example, +-- Let's take a simple example: -- -- > data Rose a = a :>: [Rose a] | Leaf a -- > deriveFamily [t| Rose Int |] -- -- Will derive the following code: -- --- > type ListCode = '[ '[] , '[ 'I ('S 'Z) , 'I 'Z] ] --- > type RTCode = '[ '[ 'K 'KInt , 'I 'Z] , '[ 'K 'KInt] ] +-- > type FamRoseInt = '[Rose Int, [Rose Int]] +-- > type CodesRoseInt = '['['[K KInt, I (S Z)], '[K KInt]], '['[], '[I Z, I (S Z)]]] -- > --- > type CodesRose = '[ListCode , RTCode] --- > type FamRose = '[ [R Int] , R Int] +-- > -- 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) @@ -54,8 +71,80 @@ -- > 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 +-- > -- --- We did inspire this module in the TH generication from generic-sop +-- 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 @@ -112,7 +201,7 @@ deriveFamilyWith opqName t -- 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) where @@ -123,6 +212,7 @@ deriveFamilyWith opqName t 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 @@ -130,6 +220,7 @@ deriveFamilyWithTy opq ty 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") @@ -660,14 +751,13 @@ familyName = return . onBaseName ("Fam" ++) . styToName 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"))) @@ -905,13 +995,15 @@ match :: Pat -> Exp -> Match 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 @@ -927,16 +1019,17 @@ genPiece3_1 opq input 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 @@ -995,18 +1088,19 @@ genPiece4 opq first ls -- |@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 From f8d4ebc59b507202b201ae4269a1d40d0ccb9190 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Wed, 24 Jul 2019 11:36:59 +0200 Subject: [PATCH 14/15] Bumped tag version --- generics-mrsop.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/generics-mrsop.cabal b/generics-mrsop.cabal index b1a27bb..fb6f5c0 100644 --- a/generics-mrsop.cabal +++ b/generics-mrsop.cabal @@ -81,4 +81,4 @@ source-repository head source-repository this type: git location: https://github.com/VictorCMiraldo/generics-mrsop - tag: v2.0.0 + tag: v2.1.0 From 7333619900ce0ada1ed53669815db35c7971ff80 Mon Sep 17 00:00:00 2001 From: Victor Miraldo Date: Wed, 24 Jul 2019 11:38:30 +0200 Subject: [PATCH 15/15] Fixed TH file --- src/Generics/MRSOP/TH.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Generics/MRSOP/TH.hs b/src/Generics/MRSOP/TH.hs index 0bea042..0ceb4e3 100644 --- a/src/Generics/MRSOP/TH.hs +++ b/src/Generics/MRSOP/TH.hs @@ -203,7 +203,7 @@ deriveFamilyWith opqName t let final = sortBy (compare `on` second) m' -- dbg <- genFamilyDebug sty final res <- genFamily opqData sty final - return (dbg ++ res) + return res -- (dbg ++ res) where second (_ , x , _) = x