packages feed

generics-mrsop 1.0.0.1 → 1.2.2

raw patch · 17 files changed

+768/−154 lines, 17 filesdep ~base

Dependency ranges changed: base

Files

README.md view
@@ -1,6 +1,8 @@ # generics-mrsop -Generic Programming for Mutually Recursive Families in the+Generic Programming, with combinators, for Mutually Recursive Families in the Sums of Products style. -Check the `Generics.MRSOP.Examples.RoseTreeTH` for a quick start.+Check the `Generics.MRSOP.Examples.RoseTreeTH` for a simple quick start,+or read our [paper](https://icfp18.sigplan.org/event/tyde-2018-sums-of-products-for-mutually-recursive-datatypes), "Sums of Products for Mutually Recursive Datatypes", for a more detailed description.+
generics-mrsop.cabal view
@@ -1,5 +1,5 @@ name:                generics-mrsop-version:             1.0.0.1+version:             1.2.2  synopsis:            Generic Programming with Mutually Recursive Sums of Products. @@ -20,7 +20,8 @@ build-type:          Simple  extra-source-files:  ChangeLog.md, README.md-cabal-version:       2.0+cabal-version:       1.24+tested-with:         GHC == 8.2.2, GHC == 8.4.2   library@@ -38,10 +39,12 @@     Generics.MRSOP.Util,     Generics.MRSOP.TH,     Generics.MRSOP.Zipper,+    Generics.MRSOP.Zipper.Deep,     Generics.MRSOP.Examples.RoseTree,     Generics.MRSOP.Examples.RoseTreeTH,     Generics.MRSOP.Examples.LambdaAlphaEqTH,-    Generics.MRSOP.Examples.SimpTH+    Generics.MRSOP.Examples.SimpTH,+    Generics.MRSOP.AG    other-extensions:      MultiParamTypeClasses,@@ -59,7 +62,7 @@     FunctionalDependencies,     ScopedTypeVariables -  build-depends:       base >= 4.9 && <= 4.12,+  build-depends:       base >= 4.9 && <= 5,                        containers,                        template-haskell,                        mtl@@ -76,4 +79,4 @@ source-repository this   type:     git   location: https://github.com/VictorCMiraldo/generics-mrsop-  tag:      1.0.0.0+  tag: v1.2.2
+ src/Generics/MRSOP/AG.hs view
@@ -0,0 +1,179 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE GADTs #-}++-- | Attribute grammars over mutual recursive datatypes+module Generics.MRSOP.AG where++import Data.Coerce+import Data.Foldable (fold)+import Data.Functor.Const+import Data.Functor.Product+import Data.Monoid (Sum(..), (<>))+import Generics.MRSOP.Base+import Generics.MRSOP.Util++zipAnn :: forall phi1 phi2 phi3 ki codes ix.+          (forall iy. phi1 iy -> phi2 iy -> phi3 iy)+       -> AnnFix ki codes phi1 ix+       -> AnnFix ki codes phi2 ix+       -> AnnFix ki codes phi3 ix+zipAnn f (AnnFix a1 t1) (AnnFix a2 t2) = AnnFix (f a1 a2) (zipWithRep t1 t2)+  where+    zipWithRep :: Rep ki (AnnFix ki codes phi1) xs+               -> Rep ki (AnnFix ki codes phi2) xs+               -> Rep ki (AnnFix ki codes phi3) xs+    zipWithRep (Rep x) (Rep y) = Rep $ zipWithNS x y+    zipWithNS :: NS (PoA ki (AnnFix ki codes phi1)) ys+              -> NS (PoA ki (AnnFix ki codes phi2)) ys+              -> NS (PoA ki (AnnFix ki codes phi3)) ys+    zipWithNS (Here x) (Here y)   = Here $ zipWithNP x y+    zipWithNS (There x) (There y) = There $ zipWithNS x y+    zipWithNP :: PoA ki (AnnFix ki codes phi1) zs+              -> PoA ki (AnnFix ki codes phi2) zs+              -> PoA ki (AnnFix ki codes phi3) zs+    zipWithNP NP0 NP0 = NP0+    zipWithNP (a :* as) (b :* bs) = zipWithNA a b :* zipWithNP as bs+    zipWithNA :: NA ki (AnnFix ki codes phi1) ws+              -> NA ki (AnnFix ki codes phi2) ws+              -> NA ki (AnnFix ki codes phi3) ws+    zipWithNA (NA_I t1) (NA_I t2) = NA_I (zipAnn f t1 t2)+    zipWithNA (NA_K i1) (NA_K i2) = NA_K i1  -- Should be the same!++mapAnn :: (forall iy. chi iy -> phi iy)+       -> AnnFix ki codes chi ix+       -> AnnFix ki codes phi ix+mapAnn f = synthesizeAnn (\x _ -> f x)++-- HACK. why doesn't haskell have this instance?+instance Show k => Show1 (Const k) where+  show1 (Const x) = show x++instance (Show1 f, Show1 g) => Show1 (Product f g) where+  show1 (Pair x y) = "(" ++ show1 x ++ ", " ++ show1 y ++ ")"++-- | Inherited attributes++inheritAnn ::+     forall ki codes chi phi ix.+     (forall iy. chi iy -> Rep ki (Const ()) (Lkup iy codes) -> phi iy -> Rep ki phi (Lkup iy codes))+  -> phi ix+  -> AnnFix ki codes chi ix+  -> AnnFix ki codes phi ix+inheritAnn f start (AnnFix ann rep) =+  let newFix = f ann (mapRep (const (Const ())) rep) start+      zipWithRep ::+           Rep ki (AnnFix ki codes chi) xs+        -> Rep ki phi xs+        -> Rep ki (AnnFix ki codes phi) xs+      zipWithRep (Rep x) (Rep y) = Rep $ zipWithNS x y+      zipWithNS ::+           NS (PoA ki (AnnFix ki codes chi)) ys+        -> NS (PoA ki phi) ys+        -> NS (PoA ki (AnnFix ki codes phi)) ys+      zipWithNS (Here x) (Here y) = Here $ zipWithNP x y+      zipWithNS (There x) (There y) = There $ zipWithNS x y+      zipWithNP ::+           PoA ki (AnnFix ki codes chi) zs+        -> PoA ki phi zs+        -> PoA ki (AnnFix ki codes phi) zs+      zipWithNP NP0 NP0 = NP0+      zipWithNP (a :* as) (b :* bs) = zipWithNA a b :* zipWithNP as bs+      zipWithNA ::+           NA ki (AnnFix ki codes chi) ws+        -> NA ki phi ws+        -> NA ki (AnnFix ki codes phi) ws+      zipWithNA (NA_I i1) (NA_I i2) = NA_I (inheritAnn f i2 i1)+      zipWithNA (NA_K i1) (NA_K i2) = NA_K i1+   in AnnFix start (zipWithRep rep newFix)++inherit ::+     forall ki phi codes ix.+     (forall iy. Rep ki (Const ()) (Lkup iy codes) -> phi iy -> Rep ki phi (Lkup iy codes))+  -> phi ix+  -> Fix ki codes ix+  -> AnnFix ki codes phi ix+inherit f start (Fix rep) =+  let newFix = (f (mapRep (const (Const ())) rep) start)+      zipWithRep ::+           Rep ki (Fix ki codes) xs+        -> Rep ki phi xs+        -> Rep ki (AnnFix ki codes phi) xs+      zipWithRep (Rep x) (Rep y) = Rep $ zipWithNS x y+      zipWithNS ::+           NS (PoA ki (Fix ki codes)) ys+        -> NS (PoA ki phi) ys+        -> NS (PoA ki (AnnFix ki codes phi)) ys+      zipWithNS (Here x) (Here y) = Here $ zipWithNP x y+      zipWithNS (There x) (There y) = There $ zipWithNS x y+      zipWithNP ::+           PoA ki (Fix ki codes) zs+        -> PoA ki phi zs+        -> PoA ki (AnnFix ki codes phi) zs+      zipWithNP NP0 NP0 = NP0+      zipWithNP (a :* as) (b :* bs) = zipWithNA a b :* zipWithNP as bs+      zipWithNA ::+           NA ki (Fix ki codes) ws+        -> NA ki phi ws+        -> NA ki (AnnFix ki codes phi) ws+      zipWithNA (NA_I i1) (NA_I i2) = NA_I (inherit f i2 i1)+      zipWithNA (NA_K i1) (NA_K i2) = NA_K i1+   in AnnFix start (zipWithRep rep newFix)++-- | Synthesized attributes++synthesizeAnn ::+     forall ki codes chi phi 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+    ++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++monoidAlgebra :: Monoid m => Rep ki (Const m) xs -> Const m iy+monoidAlgebra = elimRep mempty coerce fold++-- If haskell had semirings in base, or edward kmett had a package for it+-- we could do :+-- semiringAlgebra :: Semiring w => Rep ki (Const w) xs -> Const w iy+-- semiringAlgebra = (one <>) . monoidAlgebra+--+-- sizeAlgebra :: Rep ki (Const (Sum Int)) xs -> Const (Sum Int) iy+-- sizeAlgebra = semiringAlgebra++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++-- | Count the number of nodes+sizeGeneric :: (IsNat ix)+            => Fix ki codes ix -> Const (Sum Int) ix+sizeGeneric = cata sizeAlgebra
src/Generics/MRSOP/Base/Class.hs view
@@ -12,6 +12,7 @@ -- |Provides the main class of the library, 'Family'. module Generics.MRSOP.Base.Class where +import Data.Functor.Const import Data.Function (on)  import Generics.MRSOP.Base.Universe@@ -89,5 +90,5 @@ deep :: forall fam ty ki codes ix       . (Family ki fam codes,          ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix)-     => ty -> Fix ki codes ix+     => ty -> AnnFix ki codes (Const ()) ix deep = dfrom . into
src/Generics/MRSOP/Base/Metadata.hs view
@@ -85,18 +85,17 @@  -- |Given a 'Family', provides the 'DatatypeInfo' for the type --  with index @ix@ in family 'fam'.-class (Family ki fam codes) => HasDatatypeInfo ki fam codes ix+class (Family ki fam codes) => HasDatatypeInfo ki fam codes     | fam -> codes ki where-  datatypeInfo :: (IsNat ix)-               => Proxy fam -> Proxy ix -> DatatypeInfo (Lkup ix codes)+  datatypeInfo :: Proxy fam -> SNat ix -> DatatypeInfo (Lkup ix codes)  -- |Sometimes it is more convenient to use a proxy of the type --  in the family instead of indexes. datatypeInfoFor :: forall ki fam codes ix ty-                 . ( HasDatatypeInfo ki fam codes ix+                 . ( HasDatatypeInfo ki fam codes                    , ix ~ Idx ty fam , Lkup ix fam ~ ty , IsNat ix)                 => Proxy fam -> Proxy ty -> DatatypeInfo (Lkup ix codes)-datatypeInfoFor pf pty = datatypeInfo pf (proxyIdx pf pty)+datatypeInfoFor pf pty = datatypeInfo pf (getSNat $ proxyIdx pf pty)   where     proxyIdx :: Proxy fam -> Proxy ty -> Proxy (Idx ty fam)     proxyIdx _ _ = Proxy@@ -113,4 +112,14 @@     go CZ     (ci :* _)   = ci     go (CS c) (_  :* cis) = go c cis ++-- |Returns the constructor information for a given+--  type in the family.+constrInfoFor :: (HasDatatypeInfo ki fam codes)+              => Proxy fam+              -> SNat ix+              -> Constr (Lkup ix codes) c+              -> ConstructorInfo (Lkup c (Lkup ix codes))+constrInfoFor pfam six c = constrInfoLkup c (datatypeInfo pfam six)+
src/Generics/MRSOP/Base/NP.hs view
@@ -18,6 +18,11 @@   NP0  :: NP p '[]   (:*) :: p x -> NP p xs -> NP p (x : xs) ++instance Eq1 ki => Eq1 (NP ki) where+  eq1 = eqNP eq1+  + -- * Relation to IsList predicate  -- |Append two values of type 'NP'@@ -59,6 +64,11 @@ zipNP NP0       NP0       = NP0 zipNP (f :* fs) (g :* gs) = (f :*: g) :* zipNP fs gs +-- |Unzips a combined product into two separate products+unzipNP :: NP (f :*: g) xs -> (NP f xs , NP g xs)+unzipNP NP0                = (NP0 , NP0) +unzipNP ((f :*: g) :* fgs) = (f :*) *** (g :*) $ unzipNP fgs+ -- * Catamorphism  -- |Consumes a value of type 'NP'.@@ -67,6 +77,16 @@        -> NP f xs -> r xs cataNP fCons fNil NP0       = fNil cataNP fCons fNil (k :* ks) = fCons k (cataNP fCons fNil ks)+++-- |Consumes a value of type 'NP'.+cataNPM :: (Monad m)+        => (forall x xs . f x  -> r xs -> m (r (x : xs)))+        -> m (r '[])+        -> NP f xs -> m (r xs)+cataNPM fCons fNil NP0       = fNil+cataNPM fCons fNil (k :* ks) = cataNPM fCons fNil ks >>= fCons k +  -- * Equality
src/Generics/MRSOP/Base/NS.hs view
@@ -20,6 +20,9 @@   There :: NS p xs -> NS p (x : xs)   Here  :: p x     -> NS p (x : xs) +instance Eq1 ki => Eq1 (NS ki) where+  eq1 = eqNS eq1+ -- * Map, Zip and Elim  -- |Maps over a sum
src/Generics/MRSOP/Base/Show.hs view
@@ -20,7 +20,7 @@ import Generics.MRSOP.Util  -- https://stackoverflow.com/questions/9082642/implementing-the-show-class-instance (Show (fam k)) => Show (NA ki fam (I k)) where+{-instance (Show (fam k)) => Show (NA ki fam (I k)) where   showsPrec p (NA_I v) = showParen (p > 10) $ showString "I " . showsPrec 11 v instance (Show (ki  k)) => Show (NA ki fam (K k)) where   showsPrec p (NA_K v) = showParen (p > 10) $ showString "K " . showsPrec 11 v@@ -42,9 +42,37 @@ -- TODO: -- This needs undecidable instances. We don't like undecidable instances instance Show (NS (PoA ki phi) code) => Show (Rep ki phi code) where-  show (Rep x) = show x+  show (Rep x) =+-} -instance Show (NS (PoA ki (Fix ki codes)) (Lkup ix codes))-      => Show (Fix ki codes ix)-    where-  show (Fix x) = show x++instance (Show1 phi, Show1 ki) => Show (NA ki (AnnFix ki codes phi) a) where+  show = showNA++showNA :: (Show1 phi, Show1 ki) => NA ki (AnnFix ki codes phi) a -> String+showNA (NA_I i) = "(NA_I " ++ showFix i ++ ")"+showNA (NA_K k) = "(NA_K " ++ show1 k ++ ")"++instance (Show1 phi, Show1 ki) => Show (PoA ki (AnnFix ki codes phi) xs) where+  show = showNP++showNP :: (Show1 phi, Show1 ki) => PoA ki (AnnFix ki codes phi) xs -> String+showNP NP0 = "NP0"+showNP (a :* b) = showNA a ++ " :* " ++ showNP b++instance (Show1 phi, Show1 ki) => Show (Rep ki (AnnFix ki codes phi) xs) where+  show = showRep+  +showRep :: (Show1 phi, Show1 ki) => Rep ki (AnnFix ki codes phi) xs -> String+showRep x =+  case sop x of+    Tag c poa -> +      "(" ++ show c ++ " " ++ showNP poa ++ ")"+   ++instance (Show1 phi, Show1 ki) => Show (AnnFix ki codes phi ix) where+  show = showFix++showFix :: (Show1 phi, Show1 ki) => AnnFix ki codes phi ix -> String+showFix (AnnFix a x) = "(" ++ show1 a ++  " " ++ showRep x  ++ ")"+
src/Generics/MRSOP/Base/Universe.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE TypeOperators        #-} {-# LANGUAGE DataKinds            #-} {-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE PatternSynonyms      #-} {-# LANGUAGE ScopedTypeVariables  #-} {-# LANGUAGE TypeApplications     #-} -- |Wraps the definitions of 'NP' and 'NS'@@ -16,6 +17,7 @@ import Data.Type.Equality import Data.Proxy +import Data.Functor.Const import Control.Monad  import Generics.MRSOP.Base.NS@@ -38,6 +40,7 @@   | I Nat   deriving (Eq, Show) + -- |@NA ki phi a@ provides an interpretation for an atom @a@, --  using either @ki@ or @phi@ to interpret the type variable --  or opaque type.@@ -45,6 +48,29 @@   NA_I :: (IsNat k) => phi k -> NA ki phi (I k)    NA_K ::              ki  k -> NA ki phi (K k) +instance (Eq1 phi, Eq1 ki) => Eq1 (NA ki phi) where+  eq1 = eqNA eq1 eq1+++instance (TestEquality ki) => TestEquality (NA ki phi) where+  testEquality (NA_I i) (NA_K k) = Nothing+  testEquality (NA_K i) (NA_I k) = Nothing+  testEquality (NA_I i) (NA_I i') =+    case testEquality (sNatFixIdx i) (sNatFixIdx i') of+      Just Refl -> Just Refl+      Nothing -> Nothing+  testEquality (NA_K k) (NA_K k') =+    -- we learn that+    -- a ~ (K k1)+    -- b ~ (K k2)+    case testEquality k k' of+      -- we learn that  k1 ~ k2+      Just Refl ->+        -- thus we learn that a ~ b. Q.e.d+        Just Refl+      Nothing -> Nothing++ -- ** Map, Elim and Zip  -- |Maps a natural transformation over an atom interpretation@@ -94,6 +120,9 @@ newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]])   = Rep { unRep :: NS (PoA ki phi) code } +instance (Eq1 phi, Eq1 ki) => Eq1 (Rep ki phi) where+  eq1 = eqRep eq1 eq1+   -- |Product of Atoms is a handy synonym to have. type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi) @@ -156,8 +185,8 @@   = cat <.> elimNS (elimNPM (elimNA fk fi)) . unRep  -- |Pure eliminator.-elimRep :: (forall k . ki k -> a)-        -> (forall k . f  k -> a)+elimRep :: (forall k .            ki k -> a)+        -> (forall k . IsNat k => f  k -> a)         -> ([a] -> b)         -> Rep ki f c -> b elimRep kp fp cat@@ -216,7 +245,7 @@ -- |Finally, we can view a sum-of-products as a constructor --  and a product-of-atoms. data View :: (kon -> *) -> (Nat -> *) -> [[ Atom kon ]] -> * where-  Tag :: Constr sum n -> PoA ki fam (Lkup n sum) -> View ki fam sum+  Tag :: IsNat n => Constr sum n -> PoA ki fam (Lkup n sum) -> View ki fam sum  -- |Unwraps a 'Rep' into a 'View' sop :: Rep ki fam sum -> View ki fam sum@@ -227,6 +256,10 @@     go (There s)   = case go s of                         Tag c poa -> Tag (CS c) poa +-- |Wraps a 'View' into a 'Rep'+fromView :: View ki fam sum -> Rep ki fam sum+fromView (Tag c x) = inj c x+ -- * Least Fixpoints -- -- $leastFixpoints@@ -237,13 +270,54 @@ -- the representation of the code indexed by ix  -- |Indexed least fixpoints-newtype Fix (ki :: kon -> *) (codes :: [[[ Atom kon ]]]) (n :: Nat)+{-newtype Fix (ki :: kon -> *) (codes :: [[[ Atom kon ]]]) (n :: Nat)   = Fix { unFix :: Rep ki (Fix ki codes) (Lkup n codes) }+-} ++-- | 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))++type Fix ki codes = AnnFix ki codes (Const ())++pattern Fix x = AnnFix (Const ()) x++unFix :: Fix ki codes ix -> Rep ki (Fix ki codes) (Lkup ix codes)+unFix (Fix x) = x++-- | Catamorphism over fixpoints+cata :: (IsNat ix)+  => (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)+++getAnn :: AnnFix ki codes ann ix -> ann ix+getAnn (AnnFix a x) = a++annCata :: (forall 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+forgetAnn :: AnnFix ki codes a ix -> Fix ki codes ix+forgetAnn (AnnFix _ rep) = Fix (mapRep forgetAnn rep)++instance Eq1 ki => Eq1 (Fix ki codes) where+  eq1 = eqFix eq1+ -- |Retrieves the index of a 'Fix'-proxyFixIdx :: Fix ki fam ix -> Proxy ix+proxyFixIdx :: phi ix -> Proxy ix proxyFixIdx _ = Proxy +sNatFixIdx :: IsNat ix => phi ix -> SNat ix+sNatFixIdx x = getSNat (proxyFixIdx x)+ -- |Maps over the values of opaque types within the --  fixpoint. mapFixM :: (Monad m)@@ -256,9 +330,13 @@       -> Fix ki fam ix -> Fix ki fam ix -> Bool eqFix p = eqRep p (eqFix p) `on` unFix +instance Eq1 ki => Eq  (Fix ki codes ix) where+  (==) = eqFix eq1+ -- |Compare two indexes of two fixpoints --  Note we can't use a 'testEquality' instance because --  of the 'IsNat' constraint. heqFixIx :: (IsNat ix , IsNat ix')          => Fix ki fam ix -> Fix ki fam ix' -> Maybe (ix :~: ix') heqFixIx fa fb = testEquality (getSNat Proxy) (getSNat Proxy)+
src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs view
@@ -82,10 +82,6 @@  type FIX = Fix Singl CodesTerm -pattern Term_    = SZ-pattern Var_ s   = Tag CZ (NA_K s :* NP0)-pattern Abs_ x t = Tag (CS CZ) (NA_K x :* NA_I t :* NP0)- -- |Decides whether or not two terms are alpha equivalent. alphaEq :: Term -> Term -> Bool alphaEq x y = runAlpha $ galphaEqT (deep @FamTerm x) (deep @FamTerm y)@@ -110,12 +106,12 @@        => SNat ix -> Rep (Singl :*: Singl) (FIX :*: FIX)                          (Lkup ix CodesTerm)        -> m Bool-    go Term_ x = case sop x of+    go IdxTerm x = case sop x of       -- Without -XPolyKinds this is impossible; weird errors all over the place.       Var_ (SString v1 :*: SString v2)         -> v1 =~= v2       Abs_ (SString v1 :*: SString v2) (t1 :*: t2)-        -> onNewScope (addRule v1 v2 >> galphaEq Term_ t1 t2)+        -> onNewScope (addRule v1 v2 >> galphaEq IdxTerm t1 t2)       _ -> step x  -- * Tests
src/Generics/MRSOP/Examples/RoseTree.hs view
@@ -56,15 +56,13 @@   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0))))     = El (Leaf a) -instance HasDatatypeInfo Singl FamRose CodesRose Z where-  datatypeInfo _ _+instance HasDatatypeInfo Singl FamRose CodesRose where+  datatypeInfo _ SZ     = ADT "module" (Name "[]" :@: (Name "R" :@: Name "Int"))       $  (Constructor "[]")       :* (Infix ":" RightAssociative 5)       :* NP0--instance HasDatatypeInfo Singl FamRose CodesRose (S Z) where-  datatypeInfo _ _+  datatypeInfo _ (SS SZ)     = ADT "module" (Name "R" :@: Name "Int")       $  (Infix ":>:" NotAssociative 0)       :* (Constructor "Leaf")
src/Generics/MRSOP/Examples/SimpTH.hs view
@@ -55,24 +55,12 @@  deriveFamily [t| Stmt String |] -pattern Decl_ = SS (SS SZ)-pattern Exp_  = SS SZ-pattern Stmt_ = SZ--pattern SAssign_ v e = Tag CZ (NA_K v :* NA_I e :* NP0)--pattern DVar_ v     = Tag CZ (NA_K v :* NP0)-pattern DFun_ f x s = Tag (CS CZ) (NA_K f :* NA_K x :* NA_I s :* NP0)--pattern EVar_ v    = Tag CZ      (NA_K v :* NP0)-pattern ECall_ f x = Tag (CS CZ) (NA_K f :* NA_I x :* NP0)- type FIX = Fix Singl CodesStmtString  -- * Alpha Equality Functionality  alphaEqD :: Decl String -> Decl String -> Bool-alphaEqD = (galphaEq Decl_) `on` (deep @FamStmtString)+alphaEqD = (galphaEq IdxDeclString) `on` (deep @FamStmtString)   where     -- Generic programming boilerplate;     -- could be removed. WE are just passing SNat@@ -110,24 +98,24 @@        -> Rep (Singl :*: Singl) (FIX :*: FIX)               (Lkup iy CodesStmtString)        -> m Bool-    go Stmt_ x+    go IdxStmtString x       = case sop x of-          SAssign_ (SString v1 :*: SString v2) e1e2-            -> addRule v1 v2 >> uncurry' (galphaEq' Exp_) e1e2+          StmtStringSAssign_ (SString v1 :*: SString v2) e1e2+            -> addRule v1 v2 >> uncurry' (galphaEq' IdxExpString) e1e2           otherwise             -> step x-    go Decl_ x+    go IdxDeclString x       = case sop x of-          DVar_ (SString v1 :*: SString v2)+          DeclStringDVar_ (SString v1 :*: SString v2)             -> addRule v1 v2 >> return True-          DFun_ (SString f1 :*: SString f2) (SString x1 :*: SString x2) s+          DeclStringDFun_ (SString f1 :*: SString f2) (SString x1 :*: SString x2) s             -> addRule f1 f2 >> onNewScope (addRule x1 x2 >> uncurry' galphaEqT s)           _ -> step x-    go Exp_ x+    go IdxExpString x       = case sop x of-          EVar_ (SString v1 :*: SString v2)+          ExpStringEVar_ (SString v1 :*: SString v2)             -> v1 =~= v2-          ECall_ (SString f1 :*: SString f2) e+          ExpStringECall_ (SString f1 :*: SString f2) e             -> (&&) <$> (f1 =~= f2) <*> uncurry' galphaEqT e           _ -> step x      go _ x = step x@@ -201,6 +189,6 @@       $ into @FamStmtString (test4 10)   where     mk42 :: SNat ix -> El FamStmtString ix -> El FamStmtString ix-    mk42 Exp_ _ = El $ ELit 42-    mk42 _    x = x+    mk42 IdxExpString _ = El $ ELit 42+    mk42 _            x = x
src/Generics/MRSOP/Opaque.hs view
@@ -15,6 +15,7 @@  import Data.Function (on) import Data.Proxy+import Data.Type.Equality  import Generics.MRSOP.Util @@ -64,3 +65,13 @@ eqSingl :: Singl k -> Singl k -> Bool eqSingl = (==) +instance TestEquality Singl where+  testEquality (SInt _) (SInt _)         = Just Refl+  testEquality (SInteger _) (SInteger _) = Just Refl+  testEquality (SFloat _) (SFloat _)     = Just Refl+  testEquality (SDouble _) (SDouble _)   = Just Refl+  testEquality (SBool _) (SBool _)       = Just Refl+  testEquality (SChar _) (SChar _)       = Just Refl+  testEquality (SString _) (SString _)   = Just Refl+  testEquality _ _                       = Nothing+
src/Generics/MRSOP/TH.hs view
@@ -12,7 +12,12 @@ --   We are borrowing a some code from generic-sop --   ( https://hackage.haskell.org/package/generics-sop-0.3.2.0/docs/src/Generics-SOP-TH.html ) ---module Generics.MRSOP.TH (deriveFamily, genFamilyDebug) where+module Generics.MRSOP.TH+  ( deriveFamilyWith+  , deriveFamilyWithTy+  , deriveFamily+  , genFamilyDebug+  ) where  import Data.Function (on) import Data.Char (ord , isAlphaNum)@@ -36,23 +41,34 @@  import qualified Data.Map as M +data OpaqueData = OpaqueData+  { opaqueName   :: Name+  -- | Map assigning a Haskell type to its corresponding promoted+  --   Kon+  , opaqueTable  :: M.Map Name Name+  -- | Map assigning a promoted Kon to the constructor it uses+  , opaqueCons   :: M.Map Name Name+  } deriving (Eq , Show)+ -- |Given the name of the first element in the family, --  derives: -- --    1. The other types in the family and Konstant types one needs. --    2. the SOP code for each of the datatypes involved --    3. One 'Element' instance per datatype---    TODO: 4. Metadada information for each of the datatypes involved-deriveFamily :: Q Type -> Q [Dec]-deriveFamily t+--    4. Metadada information for each of the datatypes involved+--    5. Uses the opaque-type universe provided.+deriveFamilyWith :: Name -> Q Type -> Q [Dec]+deriveFamilyWith opqName t   = do sty              <- t >>= convertType -       (_ , (Idxs _ m)) <- runIdxsM (reifySTy sty)+       opqData          <- reifyOpaqueType opqName+       (_ , (Idxs _ m)) <- runIdxsM (reifySTy opqData sty)        -- Now we make sure we have processed all        -- types        m' <- mapM extractDTI (M.toList m)        let final = sortBy (compare `on` second) m'         dbg <- genFamilyDebug sty final-       res <- genFamily sty final +       res <- genFamily opqData sty final         return (dbg ++ res)   where     second (_ , x , _) = x@@ -62,6 +78,17 @@     extractDTI (sty , (ix , Just dti))       = return (sty , ix , dti) +deriveFamilyWithTy :: Q Type -> Q Type -> Q [Dec]+deriveFamilyWithTy opq ty+  = do opqTy <- opq+       case opqTy of+         ConT opqName -> deriveFamilyWith opqName ty+         _            -> fail $ "Type " ++ show opqTy ++ " must be a name!"++deriveFamily :: Q Type -> Q [Dec]+deriveFamily = deriveFamilyWith (mkName "Singl")++ -- Sketch; -- --   Given a module:@@ -128,6 +155,10 @@ dtiMapM f (ADT name args ci) = ADT name args <$> mapM (ciMapM f) ci dtiMapM f (New name args ci) = New name args <$> ciMapM f ci +dtiName :: DTI ty -> DataName+dtiName (ADT name _ _) = name+dtiName (New name _ _) = name+ dti2ci :: DTI ty -> [CI ty] dti2ci (ADT _ _ cis) = cis dti2ci (New _ _ ci)  = [ ci ]@@ -326,9 +357,51 @@ -- * Preprocessing Data * -- ---------------------------- +-- |Given an opaque type name, return the name of the constructors+--  that wrap which Haskell types.+--+--  This provides a way to customize what the generation engine+--  sees as opaque types.+--+--  For instance, suppose,+--+--  > data MySingl :: * -> * where+--  >   MyInt  :: Int  -> MySingl KInt+--  >   MyBool :: Bool -> MySingl KBool+--+--  Then,+--+--  > reifyOpaqueType ''MySingl+--  >  = M.fromList [(''Int , "KInt") , (''Bool, "KBool")]+--  >  , M.fromList [("KInt" , "MyInt") , ("KBool" , "MyBool")]+--+reifyOpaqueType :: Name -> Q OpaqueData+reifyOpaqueType opq+  = do triples <- (extract <.> reifyDec) opq+       let (hsTyMap , consMap) = genMaps triples+       return $ OpaqueData opq hsTyMap consMap+  where+    genMaps :: [(Name , Name , Name)] -> (M.Map Name Name , M.Map Name Name)+    genMaps xys = (M.fromList (map (\(x , y , _) -> (x , y)) xys)+                 ,M.fromList (map (\(_ , x , y) -> (x , y)) xys))+    +    extract :: Dec -> Q [(Name , Name , Name)]+    extract (DataD _ _ _ _ cs _) = mapM extractCon cs+    extract _+      = failMsg++    extractCon :: Con -> Q (Name , Name , Name)+    extractCon (GadtC [opqC] [(_ , ConT hsTy)] (AppT _ (PromotedT ty)))+      = return (hsTy , ty , opqC)+    extractCon _+      = failMsg++    failMsg = fail $ "The opaque-type universe you provided is of the wrong form;"+                  ++ "Check documentation for Generics.MRSOP.TH.reifyOpaqueType"+ -- |Performs step 2 of the sketch;-reifySTy :: STy -> M ()-reifySTy sty+reifySTy :: OpaqueData -> STy -> M ()+reifySTy opq sty   = do ix <- indexOf sty        uncurry go (styFlatten sty)   where@@ -337,19 +410,19 @@       = do dec <- lift (reifyDec name >>= decInfo)            -- TODO: Check that the precondition holds.            let res = dtiReduce dec args-           (final , todo) <- runWriterT $ dtiMapM convertSTy res+           (final , todo) <- runWriterT $ dtiMapM (convertSTy (opaqueTable opq)) res            register sty final-           mapM_ reifySTy todo+           mapM_ (reifySTy opq) todo          -- Convert the STy's in the fields of the constructors;     -- tells a list of STy's we still need to process.-    convertSTy :: STy -> WriterT [STy] M IK-    convertSTy ty+    convertSTy :: M.Map Name Name -> STy -> WriterT [STy] M IK+    convertSTy opqTable ty       -- We remove sty from the list of todos       -- otherwise we get an infinite loop       | ty == sty = AtomI <$> lift (indexOf ty)       | isClosed ty-      = case makeCons ty of+      = case makeCons opqTable ty of           Just k  -> return (AtomK k)           Nothing -> do ix     <- lift (indexOf ty)                         hasDti <- lift (hasData ty)@@ -359,19 +432,9 @@       = fail $ "I can't convert type variable " ++ show ty               ++ " when converting " ++ show sty -    makeCons :: STy -> Maybe Name-    makeCons (ConST n) = M.lookup n consTable-    makeCons _         = Nothing--    consTable = M.fromList . map (id *** mkName)-      $ [ ( ''Int     , "KInt")-        , ( ''Char    , "KChar")-        , ( ''Integer , "KInteger")-        , ( ''Float   , "KFloat")-        , ( ''Bool    , "KBool")-        , ( ''String  , "KString")-        , ( ''Double  , "KDouble")-        ]+    makeCons :: M.Map Name Name -> STy -> Maybe Name+    makeCons opqTable (ConST n) = M.lookup n opqTable+    makeCons opqTable _         = Nothing  ----------------------------- -- * Generating the Code * --@@ -403,6 +466,14 @@ -- > pattern HT0_ d = Here d -- > pattern HT1_ d = There (Here d) --+--  TODO:+--   This has an issue; if we import two modules with code generation+--   the HT0, HT1, ... HTn names will clash.+--   Same with D0_, D1_, Dn_ in part (1.2) above.+--   These were an effort in circumventing the GHC memory leak,+--   but since it does not solve the problem, we should consider+--   dropping that.+-- -- 2.2. constructors -- > pattern a :>:_ as = Tag CZ      (NA_K a :* NA_I (El as) :* NP0) -- > pattern Leaf_ a   = Tag (CS CZ) (NA_K a :* NP0)@@ -434,9 +505,9 @@ -- >     = El (Leaf a) -- -- 4. Metadata for each type in (1)--- > instance HasDatatypeInfo Singl FamRose CodesRose Z where ...--- > instance HasDatatypeInfo Singl FamRose codesRose (S Z) where ...--- +-- > instance HasDatatypeInfo Singl FamRose CodesRose where+-- >   datatypeInfo Proxy CZ = ...+-- >   datatypeInfo Proxy (CS CZ) = ...   -- |The input data for the generation is an ordered list --  (on the second component of the tuple) of STy's and@@ -486,6 +557,9 @@ ik2Codes (AtomI n) = AppT tyI $ int2Type n -- ConT (int2TySynName n) ik2Codes (AtomK k) = AppT tyK $ PromotedT k +{-+  VCM: GHC performance HACK+ -- Generates piece (1.2); we do so by -- finding what's the maximum type index used -- in all DatatypeInformation we have and then generate@@ -504,6 +578,7 @@     getMaxIdx = foldr (ikElim max (const id)) 0      genTySynNum i = TySynD (int2TySynName i) [] (int2Type i)+-}  -- generates rhs of piece (1.1) inputToFam :: Input -> Q Type@@ -534,7 +609,7 @@  genPiece1 :: STy -> Input -> Q [Dec] genPiece1 first ls-  = do -- nums  <- inputToTySynNums ls+  = do -- nums  <- inputToTySynNums ls -- TODO: Remove this hack        codes <- TySynD <$> codesName first                        <*> return []                        <*> inputToCodes ls@@ -549,6 +624,9 @@ idxPatSyn :: STy -> Pat idxPatSyn = flip ConP [] . idxPatSynName +{-+  VCM: HACK+ -- |@htPatSynName ci@ will generate the --  pattern synonym name for constructor ci. --@@ -565,12 +643,14 @@ htPatSynExp :: Int -> CI IK -> Q Exp htPatSynExp dtiIx = return . ConE . htPatSynName dtiIx -genIdxPatSyn :: STy -> Int -> Q Dec-genIdxPatSyn sty ix-  = return (PatSynD (idxPatSynName sty) (PrefixPatSyn []) ImplBidir (int2SNatPat ix))+-}+{-+  We tried this in order to help the exhaustiveness checker in GHC.+  I'm removing this hack to avoid name clashes. Our experiments+  showed that this did not help at all. -genHereTherePatSyn :: STy -> Input -> Q [Dec]-genHereTherePatSyn first ls+genHereTherePatSyn :: OpaqueData -> STy -> Input -> Q [Dec]+genHereTherePatSyn opq first ls   = flat . concat <$> mapM (\(_ , ix , dti) -> genHereThereFor ix dti) ls   where     flat             = foldl' (\ac (x , y) -> x:y:ac) []@@ -592,55 +672,141 @@              -> (,) <$> genHT_decl dtiCode dtiIx ix ci                     <*> genHT_def          dtiIx ix ci +    opqName = return (ConT $ opaqueName opq)+     genHT_decl dtiCode dtiIx ix ci       = PatSynSigD (htPatSynName dtiIx ci)-          <$> [t| PoA Singl (El $famName) $(return $ ci2Codes ci)-                -> NS (PoA Singl (El $famName)) $(return dtiCode) |]+          <$> [t| PoA $opqName (El $famName) $(return $ ci2Codes ci)+                -> NS (PoA $opqName (El $famName)) $(return dtiCode) |]      genHT_def dtiIx ix ci       = do var <- newName "d"            PatSynD (htPatSynName dtiIx ci) (PrefixPatSyn [var]) ImplBidir              <$> inj ix (return $ VarP var)-           +-} --- |Generating pattern sinonyms for the type indexes---  and the 'Here/There' combinations. (pieces 2.1 and 2.1.1)+genIdxPatSyn :: STy -> Int -> Q Dec+genIdxPatSyn sty ix+  = return (PatSynD (idxPatSynName sty) (PrefixPatSyn []) ImplBidir (int2SNatPat ix))++-- |Generating pattern synonyms for the type indexes+--  and the pattern synonyms for the constructors. -- --  > pattern IdxRInt = SZ --  > pattern IdxListRInt = SS SZ ---genPiece2 :: STy -> Input -> Q [Dec]-genPiece2 first ls+genPiece2 :: OpaqueData -> STy -> Input -> Q [Dec]+genPiece2 opq first ls   = do p21  <- mapM (\(sty , ix , dti) -> genIdxPatSyn sty ix) ls-       p211 <- genHereTherePatSyn first ls-       return $ p21 ++ p211+       p22  <- genPiece2_2 opq first ls+       -- p211 <- genHereTherePatSyn opq first ls+       return $ p21 ++ p22 -genPiece3 :: STy -> Input -> Q Dec-genPiece3 first ls-  = head <$> [d| instance Family Singl+-- |Generating pattern synonyms for constructors with 'Tag'+--+--  This is trickier than it looks at first sight.+--  If we have occurences of @Maybe A@ and @Maybe B@ in our+--  mutually recursive family, we have to generate two sets of+--  @Just@s and @Nothing@s, otherwise we will have a name clash.+--+--  Infix constructors also receive special treatment.+--  suppose @(:*:)@ is the 4th constructor of a type @Op x@,+--  The pattern syn for an instantiation of @x@ to @Int@, @Op Int@,+--  will be named @OpInt_Ifx4@.+--+genPiece2_2 :: OpaqueData -> STy -> Input -> Q [Dec]+genPiece2_2 opq first ls+  = concat <$> mapM (\(sty , ix , dti) -> genTagPatSyns sty ix dti) ls+  where+    genTagPatSyns :: STy -> Int -> DTI IK -> Q [Dec]+    genTagPatSyns sty ix dti+      = concat <$> mapM (uncurry $ genTagPatSynFor ix sty)+                        (zip [0..] $ dti2ci dti)++    genTagPatSynFor :: Int -> STy -> Int -> CI IK -> Q [Dec]+    genTagPatSynFor ix sty cidx ci+      = let fields = ci2ty ci+         in do vars <- mapM (const (newName "p")) fields+               let namedFields = zip fields vars+               name <- patSynName sty cidx ci+               pat <- [p| Tag $(int2Constr cidx) $(tagPatSynProd namedFields) |]+               let pDef = PatSynD name (PrefixPatSyn vars) ImplBidir pat+               phiN <- newName "phi"+               konN <- newName "kon"+               patTy <- genTagPatType ix phiN konN fields+               let pTy = PatSynSigD name patTy+               return [pTy , pDef]++    genTagPatType :: Int -> Name -> Name -> [IK] -> Q Type+    genTagPatType tyIx phi kon (AtomK konst : rest)+      = [t| $(return $ VarT kon) $(return (ConT konst))+            -> $(genTagPatType tyIx phi kon rest) |] +    genTagPatType tyIx phi kon (AtomI ni : rest)+      = [t| $(return (VarT phi)) $(return $ int2Type ni)+            -> $(genTagPatType tyIx phi kon rest) |]+    genTagPatType tyIx phi kon []+      = [t| View $(return $ VarT kon)+                 $(return $ VarT phi)+                 (Lkup $(return $ int2Type tyIx)+                       $(ConT <$> codesName first))+        |]++    patSynName :: STy -> Int -> CI IK -> Q Name+    patSynName sty cidx ci+      | ciHasIllegalName ci+      = let styname = nameBase $ styToName sty+         in return . mkName $ styname ++ "_Ifx" ++ show cidx+    -- This is a constructor of a type that is not applied+    -- to any argument; hence there is no risk of name clashing.+      | ConST _ <- sty+      = return . mkName $ nameBase (ciName ci) ++ "_"+    -- Here we will preffix the the constructor name with the+    -- type it belongs to.+      | otherwise+      = let styname = nameBase $ styToName sty+         in return . mkName $ styname ++ nameBase (ciName ci) ++ "_"++    ciHasIllegalName :: CI ty -> Bool+    ciHasIllegalName (Infix _ _ _ _) = True+    ciHasIllegalName ci = any (not . isAlphaNum) $ nameBase (ciName ci)++    tagPatSynProd :: [(IK , Name)] -> Q Pat+    tagPatSynProd []     = [p| NP0 |]+    tagPatSynProd (h:hs) = [p| $(tagPatSynProdHead h) :* ( $(tagPatSynProd hs) ) |]++    int2Constr :: Int -> Q Pat+    int2Constr 0 = [p| CZ |]+    int2Constr n = [p| CS $(int2Constr (n-1)) |]++    tagPatSynProdHead :: (IK , Name) -> Q Pat+    tagPatSynProdHead (AtomI _ , name) = [p| NA_I $(return . VarP $ name) |]+    tagPatSynProdHead (AtomK _ , name) = [p| NA_K $(return . VarP $ name) |]++genPiece3 :: OpaqueData -> STy -> Input -> Q Dec+genPiece3 opq first ls+  = head <$> [d| instance Family $(return $ ConT $ opaqueName opq)                                  $(ConT <$> familyName first)                                  $(ConT <$> codesName first)-                   where sfrom' = $(genPiece3_1 ls)-                         sto'   = $(genPiece3_2 ls) |]+                   where sfrom' = $(genPiece3_1 opq ls)+                         sto'   = $(genPiece3_2 opq ls) |]  -- |Given a datatype information, generates a pattern --  and an expression from it. The int here --  indicates the number of the constructor. -----  > ci2PatExp IdxBinTree (Normal "Bin" [VarT a , VarT a])+--  > ci2PatExp opq IdxBinTree 3 (Normal "Bin" [VarT a , VarT a]) --  >   = ( El (Bin x_1 x_2)---  >     , Rep (PatBin_IdxBinTree (NA_I (El x_1) :* NA_I (El x_2) :* NP0))+--  >     , Rep (There (There (Here (NA_I (El x_1) :* NA_I (El x_2) :* NP0)))) --  >     )-ci2PatExp :: Int -> CI IK -> Q (Pat , Exp)-ci2PatExp dtiIx ci+ci2PatExp :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp)+ci2PatExp opq dtiIx cIdx ci   = do (vars , pat) <- ci2Pat ci-       bdy          <- [e| Rep $(inj $ genBdy (zip vars (ci2ty ci))) |]+       bdy          <- [e| Rep $(inj cIdx $ genBdy (zip vars (ci2ty ci))) |]        return (ConP (mkName "El") [pat] , bdy)   where-    inj :: Q Exp -> Q Exp-    -- inj 0 e = [e| Here $e              |]-    -- inj n e = [e| There $(inj (n-1) e) |]-    inj e = [e| $(htPatSynExp dtiIx ci) $e |]+    inj :: Int -> Q Exp -> Q Exp+    inj 0 e = [e| Here $e              |]+    inj n e = [e| There $(inj (n-1) e) |]      genBdy :: [(Name , IK)] -> Q Exp     genBdy []       = [e| NP0 |]@@ -648,26 +814,24 @@       mkHead (x , AtomI _) = [e| NA_I (El $(return (VarE x))) |]-    mkHead (x , AtomK k) = [e| NA_K $(return (AppE (ConE (mkK k)) (VarE x))) |]--    mkK k = mkName $ 'S':tail (nameBase k)+    mkHead (x , AtomK k) = [e| NA_K $(makeK opq k (\r -> AppE (ConE r) (VarE x))) |]+    -- mkHead (x , AtomK k) = [e| NA_K $(return (AppE (ConE (mkK k)) (VarE x))) |]  -- | Just like 'ci2PatExp', but the other way around. -----  > ci2ExpPat IdxBinTree (Normal "Bin" [VarT a , VarT a])---  >   = ( Rep (PatBin_IdxBinTree (NA_I (El x_1) :* NA_I (El x_2) :* NP0))+--  > ci2ExpPat opq IdxBinTree 2 (Normal "Bin" [VarT a , VarT a])+--  >   = ( Rep (There (There (Here (NA_I (El x_1) :* NA_I (El x_2) :* NP0)))) --        , El (Bin x_1 x_2) --  >     )-ci2ExpPat :: Int -> CI IK -> Q (Pat , Exp)-ci2ExpPat dtiIx ci+ci2ExpPat :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp)+ci2ExpPat opq dtiIx cIdx ci    = do (vars , exp) <- ci2Exp ci-       pat          <- [p| Rep $(inj $ genBdy (zip vars (ci2ty ci))) |]+       pat          <- [p| Rep $(inj cIdx $ genBdy (zip vars (ci2ty ci))) |]        return (pat , AppE (ConE $ mkName "El") exp)   where-    inj :: Q Pat -> Q Pat-    -- inj 0 e = [p| Here $e              |]-    -- inj n e = [p| There $(inj (n-1) e) |]-    inj e = ConP (htPatSynName dtiIx ci) . (:[]) <$> e+    inj :: Int -> Q Pat -> Q Pat+    inj 0 e = [p| Here $e              |]+    inj n e = [p| There $(inj (n-1) e) |]          genBdy :: [(Name , IK)] -> Q Pat     genBdy []       = [p| NP0 |]@@ -675,11 +839,17 @@       mkHead (x , AtomI _) = [p| NA_I (El $(return (VarP x))) |]-    mkHead (x , AtomK k) = [p| NA_K $(return (ConP (mkK k) [VarP x])) |]+    mkHead (x , AtomK k) = [p| NA_K $(makeK opq k (flip ConP [VarP x])) |]+    -- mkHead (x , AtomK k) = [p| NA_K $(return (ConP (mkK k) [VarP x])) |] -    mkK k = mkName $ 'S':tail (nameBase k) +makeK :: OpaqueData -> Name -> (Name -> a) -> Q a+makeK opq n cont+  = case M.lookup n (opaqueCons opq) of+      Nothing -> fail $  "makeK: Can't find constructor for " ++ show n ++ " in opaque def"+      Just c  -> return $ cont c + match :: Pat -> Exp -> Match match pat bdy = Match pat (NormalB bdy) [] @@ -692,8 +862,8 @@   where     err = AppE (VarE (mkName "error")) (LitE (StringL "matchAll")) -genPiece3_1 :: Input -> Q Exp-genPiece3_1 input+genPiece3_1 :: OpaqueData -> Input -> Q Exp+genPiece3_1 opq input   = LamCaseE <$> mapM (\(sty , ix , dti) -> clauseForIx sty ix dti) input   where     clauseForIx :: STy -> Int -> DTI IK -> Q Match@@ -701,10 +871,11 @@                        <$> (LamCaseE <$> genMatchFor ix dti)          genMatchFor :: Int -> DTI IK -> Q [Match]-    genMatchFor ix dti = map (uncurry match) <$> mapM (ci2PatExp ix) (dti2ci dti)+    genMatchFor ix dti = map (uncurry match) <$> mapM (uncurry $ ci2PatExp opq ix)+                                                      (zip [0..] $ dti2ci dti)       -genPiece3_2 :: Input -> Q Exp-genPiece3_2 input+genPiece3_2 :: OpaqueData -> Input -> Q Exp+genPiece3_2 opq input   = LamCaseE . matchAll <$> mapM (\(sty , ix , dti) -> clauseForIx sty ix dti) input   where         clauseForIx :: STy -> Int -> DTI IK -> Q Match@@ -712,18 +883,26 @@                        <$> (LamCaseE . matchAll <$> genMatchFor ix dti)            genMatchFor :: Int -> DTI IK -> Q [Match]-    genMatchFor ix dti = map (uncurry match) <$> mapM (ci2ExpPat ix) (dti2ci dti)+    genMatchFor ix dti = map (uncurry match) <$> mapM (uncurry $ ci2ExpPat opq ix)+                                                      (zip [0..] $ dti2ci dti) -genPiece4 :: STy -> Input -> Q [Dec]-genPiece4 first ls = concat <$> mapM genDatatypeInfoInstance ls+genPiece4 :: OpaqueData -> STy -> Input -> Q [Dec]+genPiece4 opq first ls+  = [d| instance Meta.HasDatatypeInfo $opqName+                                      $(ConT <$> familyName first)+                                      $(ConT <$> codesName first)+          where datatypeInfo _ = $(genDatatypeInfoClauses ls) |]   where-    genDatatypeInfoInstance :: (STy , Int , DTI IK) -> Q [Dec]-    genDatatypeInfoInstance (sty , idx , dti)-      = [d| instance Meta.HasDatatypeInfo Singl $(ConT <$> familyName first)-                                                $(ConT <$> codesName first)-                                                $(return (int2Type idx))-              where datatypeInfo _ _ = $(genInfo sty dti) |]+    opqName = return (ConT $ opaqueName opq) +    genDatatypeInfoClauses :: Input -> Q Exp+    genDatatypeInfoClauses input+      = LamCaseE <$> mapM genDatatypeInfoMatch input+    +    genDatatypeInfoMatch :: (STy , Int , DTI IK) -> Q Match+    genDatatypeInfoMatch (sty , idx , dti)+      = match (int2SNatPat idx) <$> genInfo sty dti +     genMod :: Name -> Q Exp     genMod = strlit . maybe "" id . nameModule @@ -763,18 +942,17 @@     genConInfoNP []       = [e| NP0 |]     genConInfoNP (ci:cis) = [e| $(genConInfo ci) :* ( $(genConInfoNP cis) ) |] --- |@genFamily init fam@ generates a type-level list+-- |@genFamily opq init fam@ generates a type-level list --  of the codes for the family. It also generates --  the necessary 'Element' instances.---  TODO: generate the 'HasDatatypeInfo' instances too! -- --  Precondition, input is sorted on second component.-genFamily :: STy -> Input -> Q [Dec]-genFamily first ls+genFamily :: OpaqueData -> STy -> Input -> Q [Dec]+genFamily opq first ls   = do p1 <- genPiece1 first ls-       p2 <- genPiece2 first ls-       p3 <- genPiece3 first ls-       p4 <- genPiece4 first ls+       p2 <- genPiece2 opq first ls+       p3 <- genPiece3 opq first ls+       p4 <- genPiece4 opq first ls        return $ p1 ++ p2 ++ [p3] ++ p4  -- |Generates a bunch of strings for debug purposes.
src/Generics/MRSOP/Util.hs view
@@ -14,7 +14,7 @@   , (:->) , (<.>)      -- * Poly-kind indexed product-  , (:*:)(..) , curry' , uncurry'+  , (:*:)(..) , curry' , uncurry' , delta'      -- * Type-level Naturals   , Nat(..) , proxyUnsuc@@ -41,6 +41,10 @@ -- |Poly-kind-indexed product data (:*:) (f :: k -> *) (g :: k -> *) (x :: k)   = f x :*: g x++-- |Distributes the index over the product+delta' :: (f :*: g) x -> (f x , g x)+delta' (f :*: g) = (f , g)  -- |Lifted curry curry' :: ((f :*: g) x -> a) -> f x -> g x -> a
src/Generics/MRSOP/Zipper.hs view
@@ -19,7 +19,7 @@  -- |In a @Zipper@, a Location is a a pair of a one hole context --  and whatever was supposed to be there. In a sums of products---  fashion, it consists of a choice of constructor and+--  fashion, it consists of a choice of constructor and  --  a position in the type of that constructor. data Loc :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> * where   Loc :: IsNat ix => El fam ix -> Ctxs ki fam cs iy ix -> Loc ki fam cs iy@@ -86,9 +86,19 @@   = do (ExistsIX el nphole) <- mkNPHole p        return (f el (Ctx c nphole)) + -- |Fills up a hole. fill :: (IsNat ix) => El fam ix -> Ctx ki fam c ix -> Rep ki (El fam) c fill el (Ctx c nphole) = inj c (fillNPHole el nphole)++-- |Recursively fills a stack of holes+-- however, the Family constraint ain't so nice. so we perhaps want to+-- take zippers over a deep representation+fillCtxs :: forall ix fam iy ki c. (IsNat ix, Family ki fam c) => El fam iy -> Ctxs ki fam c ix iy -> El fam ix+-- not sure if this should be h or Nothing+fillCtxs h Nil = h+fillCtxs h (Cons ctx ctxs) =+  fillCtxs (sto @fam @ki @c $ fill h ctx) ctxs  -- |Walks to the next hole and execute an action. next :: (IsNat ix)
+ src/Generics/MRSOP/Zipper/Deep.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE RankNTypes           #-}+{-# LANGUAGE FlexibleContexts     #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE TypeApplications     #-}+-- | Provides one-hole contexts for our universe, but over+--   deep encoded datatypes. These are a bit easier to use+--   computationally.+--+--   This module follows the very same structure as 'Generics.MRSOP.Zipper'.+--   Refer there for further documentation.+module Generics.MRSOP.Zipper.Deep where+import Control.Monad (guard)+import Data.Proxy++import Generics.MRSOP.Util hiding (Cons , Nil)+import Generics.MRSOP.Base++-- |Analogous to 'Generics.MRSOP.Zipper.Ctxs'+data Ctxs (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> Nat -> * where+  Nil :: Ctxs ki codes ix ix+  Cons+    :: (IsNat ix, IsNat a, IsNat b)+    => Ctx ki codes (Lkup ix codes) b+    -> Ctxs ki codes a ix+    -> Ctxs ki codes a b++-- |Analogous to 'Generics.MRSOP.Zipper.Ctx'+data Ctx (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [[Atom kon]] -> Nat -> * where+  Ctx+    :: Constr c n -> NPHole ki codes ix (Lkup n c) -> Ctx ki codes c ix++-- |Analogous to 'Generics.MRSOP.Zipper.NPHole', but uses a deep representation+--  for generic values.+data NPHole (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> [Atom kon] -> * where+  H :: PoA ki (Fix ki codes) xs -> NPHole ki codes ix ('I ix ': xs)+  T+    :: NA ki (Fix ki codes) x+    -> NPHole ki codes ix xs+    -> NPHole ki codes ix (x ': xs)++getCtxsIx :: Ctxs ki codes iy ix -> Proxy ix+getCtxsIx _ = Proxy++-- | Given a product with a hole in it, and an element, get back+-- a product+--+-- dual of 'removeNPHole'+fillNPHole ::+     IsNat ix+  => Fix ki codes ix+  -> NPHole ki codes ix xs+  -> PoA ki (Fix ki codes) xs+fillNPHole x (H xs) = NA_I x :* xs+fillNPHole x (T y ys) = y :* fillNPHole x ys++-- |Given a value that fits in a context, fills the context hole.+fillCtxs ::+     (IsNat ix) => Fix ki codes iy -> Ctxs ki codes ix iy -> Fix ki codes ix+fillCtxs h Nil = h+fillCtxs h (Cons ctx ctxs) = fillCtxs (Fix $ fillCtx h ctx) ctxs++fillCtx ::+     (IsNat ix)+  => Fix ki codes ix+  -> Ctx ki codes c ix+  -> Rep ki (Fix ki codes) c+fillCtx x (Ctx c nphole) = inj c (fillNPHole x nphole)++-- |Given a value and a context, tries to match to context+-- in the value and, upon success, returns whatever overlaps with+-- the hole.+removeCtxs ::+     (Eq1 ki, IsNat ix)+  => Ctxs ki codes ix iy+  -> Fix ki codes ix+  -> Maybe (Fix ki codes iy)+removeCtxs Nil f = pure f+removeCtxs (Cons ctx ctxs) (Fix r) = do+    (Fix t) <- removeCtxs ctxs (Fix r)+    removeCtx t ctx+  +removeCtx :: forall ix ki codes c.+     (Eq1 ki, IsNat ix)+  => Rep ki (Fix ki codes) c+  -> Ctx ki codes c ix+  -> Maybe (Fix ki codes ix)+removeCtx x (Ctx c npHole) =+  match c x >>= removeNPHole npHole++removeNPHole ::+     (Eq1 ki, IsNat ix)+  => NPHole ki codes ix xs+  -> PoA ki (Fix ki codes) xs+  -> Maybe (Fix ki codes ix)+removeNPHole (H ys) (NA_I x :* xs) = do+  guard $ eq1 xs ys+  pure x+removeNPHole (T y ys) (x :* xs) = do+  guard $ eq1 x y+  removeNPHole ys xs