packages feed

generics-mrsop 1.2.2 → 2.0.0

raw patch · 20 files changed

+372/−483 lines, 20 files

Files

ChangeLog.md view
@@ -1,5 +1,23 @@ # Revision history for generics-mrsop +## 2.0.0 -- Mar 2019++- `Eq1` and `Show1` are now called `EqHO` and `ShowHO`. This avoids clashing with the+already existing `Eq1` in `Prelude`. +- A number of functions received a `IsNat` constraint.+- `Generics.MRSOP.Util` is now re-exported by `Generics.MRSOP.Base`.+- Support for inheritted attributes no longer exists in `Generics.MRSOP.AG`+- `Fix` is no longer implemented by `AnnFix`. The later now lives in `Generics.MRSOP.AG`++## 1.2.2 -- Sep 2018++- added monadic catamorphism for NP+- added pattern signature generation for TH+- require `TestEqualiy` for opaque types singleton+- Zippers over deep representations+- Refined `Metadata` handling+- `Fix` is implemented as `AnnFix`+ ## 1.0.0.0  -- May 2018  * First version. Released on an unsuspecting world.
generics-mrsop.cabal view
@@ -1,5 +1,5 @@ name:                generics-mrsop-version:             1.2.2+version:             2.0.0  synopsis:            Generic Programming with Mutually Recursive Sums of Products. @@ -33,7 +33,6 @@     Generics.MRSOP.Base.Class,     Generics.MRSOP.Base.Combinators,     Generics.MRSOP.Base.Metadata,-    Generics.MRSOP.Base.Show,     Generics.MRSOP.Base,     Generics.MRSOP.Opaque,     Generics.MRSOP.Util,@@ -62,6 +61,8 @@     FunctionalDependencies,     ScopedTypeVariables +  ghc-options: -Wall+   build-depends:       base >= 4.9 && <= 5,                        containers,                        template-haskell,@@ -79,4 +80,4 @@ source-repository this   type:     git   location: https://github.com/VictorCMiraldo/generics-mrsop-  tag: v1.2.2+  tag: v2.0.0
src/Generics/MRSOP/AG.hs view
@@ -1,146 +1,75 @@-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE PolyKinds           #-}+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE TypeApplications    #-}+{-# LANGUAGE KindSignatures      #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE GADTs #-}+{-# 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+-- | 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)) -instance (Show1 f, Show1 g) => Show1 (Product f g) where-  show1 (Pair x y) = "(" ++ show1 x ++ ", " ++ show1 y ++ ")"+getAnn :: AnnFix ki codes ann ix -> ann ix+getAnn (AnnFix a _) = a --- | Inherited attributes+annCata :: IsNat ix+        => (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) -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)+-- | Forget the annotations+forgetAnn :: AnnFix ki codes a ix -> Fix ki codes ix+forgetAnn (AnnFix _ rep) = Fix (mapRep forgetAnn rep) -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)+mapAnn :: (IsNat ix)+       => (forall iy. chi iy -> phi iy)+       -> AnnFix ki codes chi ix+       -> AnnFix ki codes phi ix+mapAnn f = synthesizeAnn (\x _ -> f x)  -- | Synthesized attributes--synthesizeAnn ::-     forall ki codes chi phi ix.-     (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy)-  -> AnnFix ki codes chi ix-  -> AnnFix ki codes phi ix+synthesizeAnn :: forall ki codes chi phi ix+               . (IsNat ix)+              => +                 (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy)+              -> AnnFix ki codes chi ix+              -> AnnFix ki codes phi ix synthesizeAnn f = annCata alg   where-    alg ::-         forall iy.-         chi iy-      -> Rep ki (AnnFix ki codes phi) (Lkup iy codes)-      -> AnnFix ki codes phi iy+    alg :: forall iy+         . chi iy+        -> Rep ki (AnnFix ki codes phi) (Lkup iy codes)+        -> AnnFix ki codes phi iy     alg ann rep = AnnFix (f ann (mapRep getAnn rep)) rep      +-- |Example of using 'synthesize' to annotate a tree with its size+-- at every node.+--+--   > sizeAlgebra :: Rep ki (Const (Sum Int)) xs -> Const (Sum Int) iy+--   > sizeAlgebra = (Const 1 <>) . monoidAlgebra+--+-- Annotate each node with the number of subtrees+--+--   > sizeGeneric' :: (IsNat ix)+--   >              => Fix ki codes ix -> AnnFix ki codes (Const (Sum Int)) ix+--   > sizeGeneric' = synthesize sizeAlgebra+--+-- Note how using just 'cata' will simply count the number of nodes+--+--   > sizeGeneric :: (IsNat ix)+--   >             => Fix ki codes ix -> Const (Sum Int) ix+--   > sizeGeneric = cata sizeAlgebra+-- synthesize :: forall ki phi codes ix             . (IsNat ix)            => (forall iy . (IsNat iy) => Rep ki phi (Lkup iy codes) -> phi iy)@@ -154,26 +83,3 @@         -> 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.hs view
@@ -15,5 +15,5 @@ import Generics.MRSOP.Base.Class       as Export import Generics.MRSOP.Base.Metadata    as Export import Generics.MRSOP.Base.Combinators as Export-import Generics.MRSOP.Base.Show        as Export+import Generics.MRSOP.Util             as Export
src/Generics/MRSOP/Base/Class.hs view
@@ -12,9 +12,6 @@ -- |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 import Generics.MRSOP.Util @@ -90,5 +87,5 @@ deep :: forall fam ty ki codes ix       . (Family ki fam codes,          ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix)-     => ty -> AnnFix ki codes (Const ()) ix+     => ty -> Fix ki codes ix deep = dfrom . into
src/Generics/MRSOP/Base/Combinators.hs view
@@ -14,12 +14,8 @@  import Data.Function (on) -import Control.Applicative-import Control.Monad import Control.Monad.Identity -import Generics.MRSOP.Base.NS          -import Generics.MRSOP.Base.NP           import Generics.MRSOP.Base.Universe     import Generics.MRSOP.Base.Class        import Generics.MRSOP.Util
src/Generics/MRSOP/Base/Metadata.hs view
@@ -12,7 +12,6 @@ import Data.Proxy  import Generics.MRSOP.Util-import Generics.MRSOP.Base.NS import Generics.MRSOP.Base.NP import Generics.MRSOP.Base.Universe import Generics.MRSOP.Base.Class@@ -77,11 +76,17 @@ data FieldInfo :: Atom kon -> * where   FieldInfo :: { fieldName :: FieldName } -> FieldInfo k -deriving instance Show (NP ConstructorInfo code)-deriving instance Show (NP FieldInfo code)+deriving instance Show (FieldInfo atom)++instance ShowHO FieldInfo where+  showHO = show+ deriving instance Show (ConstructorInfo code)++instance ShowHO ConstructorInfo where+  showHO = show+ deriving instance Show (DatatypeInfo code)-deriving instance Show (FieldInfo atom)  -- |Given a 'Family', provides the 'DatatypeInfo' for the type --  with index @ix@ in family 'fam'.@@ -109,8 +114,8 @@ constrInfoLkup c = go c . constructorInfo   where     go :: Constr sum c -> NP ConstructorInfo sum -> ConstructorInfo (Lkup c sum)-    go CZ     (ci :* _)   = ci-    go (CS c) (_  :* cis) = go c cis+    go CZ      (ci :* _)   = ci+    go (CS c0) (_  :* cis) = go c0 cis   -- |Returns the constructor information for a given
src/Generics/MRSOP/Base/NP.hs view
@@ -18,11 +18,19 @@   NP0  :: NP p '[]   (:*) :: p x -> NP p xs -> NP p (x : xs) +instance EqHO phi => EqHO (NP phi) where+  eqHO = eqNP eqHO -instance Eq1 ki => Eq1 (NP ki) where-  eq1 = eqNP eq1-  +instance EqHO phi => Eq (NP phi xs) where+  (==) = eqHO +instance ShowHO phi => ShowHO (NP phi) where+  showHO NP0 = "NP0"+  showHO (a :* b) = showHO a ++ " :* " ++ showHO b++instance ShowHO phi => Show (NP phi xs) where+  show = showHO+ -- * Relation to IsList predicate  -- |Append two values of type 'NP'@@ -41,22 +49,22 @@  -- |Maps a natural transformation over a n-ary product mapNP :: f :-> g -> NP f ks -> NP g ks-mapNP f NP0       = NP0+mapNP _ NP0       = NP0 mapNP f (k :* ks) = f k :* mapNP f ks  -- |Maps a monadic natural transformation over a n-ary product mapNPM :: (Monad m) => (forall x . f x -> m (g x)) -> NP f ks -> m (NP g ks)-mapNPM f NP0       = return NP0+mapNPM _ NP0       = return NP0 mapNPM f (k :* ks) = (:*) <$> f k <*> mapNPM f ks  -- |Eliminates the product using a provided function. elimNP :: (forall x . f x -> a) -> NP f ks -> [a]-elimNP f NP0       = []+elimNP _ NP0       = [] elimNP f (k :* ks) = f k : elimNP f ks  -- |Monadic eliminator elimNPM :: (Monad m) => (forall x . f x -> m a) -> NP f ks -> m [a]-elimNPM f NP0       = return []+elimNPM _ NP0       = return [] elimNPM f (k :* ks) = (:) <$> f k <*> elimNPM f ks  -- |Combines two products into one.@@ -66,25 +74,24 @@  -- |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+unzipNP NP0               = (NP0 , NP0) +unzipNP (Pair f g :* fgs) = (f :*) *** (g :*) $ unzipNP fgs  -- * Catamorphism  -- |Consumes a value of type 'NP'.-cataNP :: (forall x xs . f x  -> r xs -> r (x : xs))+cataNP :: (forall a as . f a  -> r as -> r (a : as))        -> r '[]        -> NP f xs -> r xs-cataNP fCons fNil NP0       = fNil-cataNP fCons fNil (k :* ks) = fCons k (cataNP fCons fNil ks)-+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)))+        => (forall a as . f a  -> r as -> m (r (a : as)))         -> m (r '[])         -> NP f xs -> m (r xs)-cataNPM fCons fNil NP0       = fNil+cataNPM _fCons fNil NP0       = fNil cataNPM fCons fNil (k :* ks) = cataNPM fCons fNil ks >>= fCons k
src/Generics/MRSOP/Base/NS.hs view
@@ -1,11 +1,13 @@-{-# LANGUAGE RankNTypes          #-}-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE FlexibleInstances   #-}-{-# LANGUAGE GADTs               #-}-{-# LANGUAGE TypeOperators       #-}-{-# LANGUAGE DataKinds           #-}-{-# LANGUAGE PolyKinds           #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}+ -- | Standard representation of n-ary sums. module Generics.MRSOP.Base.NS where @@ -20,9 +22,22 @@   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+instance EqHO phi => EqHO (NS phi) where+  eqHO = eqNS eqHO +instance EqHO phi => Eq (NS phi xs) where+  (==) = eqHO++instance ShowHO phi => ShowHO (NS phi) where+  showHO x = concat ["(" , go 0 x , ")"]+    where+      go :: ShowHO phi => Int -> NS phi xs -> String+      go n (Here r)  = "C" ++ show n ++ " " ++ showHO r+      go n (There r) = go (n+1) r++instance ShowHO phi => Show (NS phi xs) where+  show = showHO+ -- * Map, Zip and Elim  -- |Maps over a sum@@ -49,12 +64,13 @@  -- * Catamorphism + -- |Consumes a value of type 'NS' cataNS :: (forall x xs . f x  -> r (x ': xs))        -> (forall x xs . r xs -> r (x ': xs))        -> NS f xs -> r xs-cataNS fHere fThere (Here x)  = fHere x-cataNS fHere fThere (There x) = fThere (cataNS fHere fThere x)+cataNS fHere _fThere (Here x)  = fHere x+cataNS fHere fThere  (There x) = fThere (cataNS fHere fThere x)  -- * Equality
− src/Generics/MRSOP/Base/Show.hs 
@@ -1,78 +0,0 @@-{-# LANGUAGE RankNTypes           #-}-{-# LANGUAGE FlexibleContexts     #-}-{-# LANGUAGE FlexibleInstances    #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE GADTs                #-}-{-# LANGUAGE TypeOperators        #-}-{-# LANGUAGE DataKinds            #-}-{-# LANGUAGE PolyKinds            #-}-{-# LANGUAGE ScopedTypeVariables  #-}-{-# LANGUAGE TypeApplications     #-}--- |Implements a rudimentary show instance for our representations.---  We keep this isolated because the instance for @Show (Rep ki phi code)@---  requires undecidable instances. Isolating this allows us to turn on this---  extension for this module only.-module Generics.MRSOP.Base.Show where--import Generics.MRSOP.Base.NS-import Generics.MRSOP.Base.NP-import Generics.MRSOP.Base.Universe-import Generics.MRSOP.Util---- https://stackoverflow.com/questions/9082642/implementing-the-show-class-{-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--instance Show (NP p '[]) where-  show NP0 = "NP0"-instance (Show (p x), Show (NP p xs)) => Show (NP p (x : xs)) where-  showsPrec p (v :* vs)-    = let consPrec = 5-       in showParen (p > consPrec)-        $ showsPrec (consPrec + 1) v . showString " :* " . showsPrec consPrec vs--instance Show (NS p '[]) where-  show _ = error "This code is unreachable"-instance (Show (p x), Show (NS p xs)) => Show (NS p (x : xs)) where-  showsPrec p (Here  x) = showParen (p > 10) $ showString "H " . showsPrec 11 x-  showsPrec p (There x) = showString "T " . showsPrec p x---- 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) =--}---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
@@ -17,7 +17,6 @@ import Data.Type.Equality import Data.Proxy -import Data.Functor.Const import Control.Monad  import Generics.MRSOP.Base.NS@@ -45,16 +44,25 @@ --  using either @ki@ or @phi@ to interpret the type variable --  or opaque type. data NA  :: (kon -> *) -> (Nat -> *) -> Atom kon -> * where-  NA_I :: (IsNat k) => phi k -> NA ki phi (I k) -  NA_K ::              ki  k -> NA ki phi (K k)+  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 (EqHO phi, EqHO ki) => EqHO (NA ki phi) where+  eqHO = eqNA eqHO eqHO +instance (EqHO phi, EqHO ki) => Eq (NA ki phi at) where+  (==) = eqHO +instance (ShowHO phi, ShowHO ki) => ShowHO (NA ki phi) where+  showHO (NA_I i) = "(NA_I " ++ showHO i ++ ")"+  showHO (NA_K k) = "(NA_K " ++ showHO k ++ ")"++instance (ShowHO phi, ShowHO ki) => Show (NA ki phi at) where+  show = showHO+ 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 _) (NA_K _) = Nothing+  testEquality (NA_K _) (NA_I _) = Nothing   testEquality (NA_I i) (NA_I i') =     case testEquality (sNatFixIdx i) (sNatFixIdx i') of       Just Refl -> Just Refl@@ -77,23 +85,23 @@ mapNA :: (forall k  .             ki k  -> kj k)       -> (forall ix . IsNat ix => f  ix -> g  ix)       -> NA ki f a -> NA kj g a-mapNA fk fi (NA_I f) = NA_I (fi f)-mapNA fk fi (NA_K k) = NA_K (fk k)+mapNA _  fi (NA_I f) = NA_I (fi f)+mapNA fk _  (NA_K k) = NA_K (fk k)  -- |Maps a monadic natural transformation over an atom interpretation mapNAM :: (Monad m)        => (forall k  .             ki k  -> m (kj k))        -> (forall ix . IsNat ix => f  ix -> m (g  ix))        -> NA ki f a -> m (NA kj g a)-mapNAM fk fi (NA_K k) = NA_K <$> fk k-mapNAM fk fi (NA_I f) = NA_I <$> fi f+mapNAM fk _  (NA_K k) = NA_K <$> fk k+mapNAM _  fi (NA_I f) = NA_I <$> fi f  -- |Eliminates an atom interpretation-elimNA :: (forall k . ki  k -> b)+elimNA :: (forall k .            ki  k -> b)        -> (forall k . IsNat k => phi k -> b)        -> NA ki phi a -> b-elimNA kp fp (NA_I x) = fp x-elimNA kp fp (NA_K x) = kp x+elimNA _  fp (NA_I x) = fp x+elimNA kp _  (NA_K x) = kp x  -- |Combines two atoms into one zipNA :: NA ki f a -> NA kj g a -> NA (ki :*: kj) (f :*: g) a@@ -120,8 +128,11 @@ 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+instance (EqHO phi, EqHO ki) => EqHO (Rep ki phi) where+  eqHO = eqRep eqHO eqHO++instance (EqHO phi, EqHO ki) => Eq (Rep ki phi at) where+  (==) = eqHO    -- |Product of Atoms is a handy synonym to have. type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)@@ -211,12 +222,12 @@ -- |A value @c :: Constr ks n@ specifies a position --  in a type-level list. It is, in fact, isomorphic to @Fin (length ks)@. data Constr :: [k] -> Nat -> * where-  CS :: Constr xs n -> Constr (x : xs) (S n)-  CZ ::                Constr (x : xs) Z+  CS :: Constr xs n -> Constr (x : xs) ('S n)+  CZ ::                Constr (x : xs) 'Z  instance TestEquality (Constr codes) where   testEquality CZ     CZ     = Just Refl-  testEquality (CS x) (CS y) = apply (Refl :: S :~: S) <$> testEquality x y+  testEquality (CS x) (CS y) = apply (Refl :: 'S :~: 'S) <$> testEquality x y   testEquality _      _      = Nothing  instance (IsNat n) => Show (Constr xs n) where@@ -270,23 +281,14 @@ -- 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+instance EqHO ki => EqHO (Fix ki codes) where+  eqHO = eqFix eqHO -unFix :: Fix ki codes ix -> Rep ki (Fix ki codes) (Lkup ix codes)-unFix (Fix x) = x+instance EqHO ki => Eq (Fix ki codes ix) where+  (==) = eqFix eqHO  -- | Catamorphism over fixpoints cata :: (IsNat ix)@@ -295,22 +297,6 @@   -> 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 :: phi ix -> Proxy ix proxyFixIdx _ = Proxy@@ -330,13 +316,10 @@       -> 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)+heqFixIx _fa _fb = testEquality (getSNat Proxy) (getSNat Proxy)
src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs view
@@ -10,12 +10,15 @@ {-# LANGUAGE GADTs                 #-} {-# LANGUAGE TypeApplications      #-} {-# LANGUAGE PatternSynonyms       #-}+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}+{-# OPTIONS_GHC -Wno-missing-signatures                 #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns                #-}+{-# OPTIONS_GHC -Wno-orphans                            #-} -- This is the minimun language extensions we -- need for using the library. -- |Provide a generic alpha equality decider for the lambda calculus. module Generics.MRSOP.Examples.LambdaAlphaEqTH where -import Control.Monad import Control.Monad.State  import Generics.MRSOP.Util@@ -28,7 +31,6 @@           | Abs String Term           | App Term Term - deriveFamily [t| Term |]  -- * The alpha-eq monad@@ -51,7 +53,7 @@  onHead :: (a -> a) -> [a] -> [a] onHead f (x : xs) = f x : xs-onHead f []       = []+onHead _ []       = []  -- |Given a list of scopes, which consist in a list of pairs each, checks --  whether or not two names are equivalent.@@ -89,12 +91,12 @@     galphaEqT :: forall ix m . (MonadAlphaEq m , IsNat ix)               => FIX ix -> FIX ix               -> m Bool-    galphaEqT x y = galphaEq (getSNat' @ix) x y+    galphaEqT i j = galphaEq (getSNat' @ix) i j      galphaEq :: forall ix m . (MonadAlphaEq m , IsNat ix)              => SNat ix -> FIX ix -> FIX ix              -> m Bool-    galphaEq ix (Fix x) (Fix y) = maybe (return False) (go ix) (zipRep x y)+    galphaEq ix (Fix x0) (Fix y0) = maybe (return False) (go ix) (zipRep x0 y0)      step :: forall m c . (MonadAlphaEq m)          => Rep (Singl :*: Singl) (FIX :*: FIX) c -> m Bool@@ -106,13 +108,13 @@        => SNat ix -> Rep (Singl :*: Singl) (FIX :*: FIX)                          (Lkup ix CodesTerm)        -> m Bool-    go IdxTerm x = case sop x of+    go IdxTerm x0 = case sop x0 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 IdxTerm t1 t2)-      _ -> step x+      Abs_ (SString v1 :*: SString v2) (c1 :*: c2)+        -> onNewScope (addRule v1 v2 >> galphaEq IdxTerm c1 c2)+      _ -> step x0  -- * Tests --
src/Generics/MRSOP/Examples/RoseTree.hs view
@@ -10,6 +10,9 @@ {-# LANGUAGE ScopedTypeVariables     #-} {-# LANGUAGE FunctionalDependencies  #-} {-# LANGUAGE PatternSynonyms         #-}+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns                #-}+{-# OPTIONS_GHC -Wno-orphans                            #-} -- |This module is analogous to 'Generics.MRSOP.Examples.RoseTreeTH', --  but we use no Template Haskell here. module Generics.MRSOP.Examples.RoseTree where@@ -18,7 +21,6 @@  import Generics.MRSOP.Base import Generics.MRSOP.Opaque-import Generics.MRSOP.Util  -- * Standard Rose-Tree datatype @@ -26,15 +28,15 @@          | Leaf a          deriving Show -value1, value2 :: R Int+value1, value2, value3 :: R Int value1 = 1 :>: [2 :>: [], 3 :>: []] value2 = 1 :>: [2 :>: [] , Leaf 12] value3 = 3 :>: [Leaf 23 , value1 , value2]  -- ** Family Structure -type ListCode = '[ '[] , '[I (S Z) , I Z] ]-type RTCode   = '[ '[K KInt , I Z] , '[K KInt] ]+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] @@ -46,6 +48,7 @@   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 []@@ -55,6 +58,7 @@     = 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@@ -67,6 +71,8 @@       $  (Infix ":>:" NotAssociative 0)       :* (Constructor "Leaf")       :* NP0+  datatypeInfo _ _+    = error "unreachable"  -- * Eq Instance
src/Generics/MRSOP/Examples/RoseTreeTH.hs view
@@ -12,21 +12,20 @@ {-# LANGUAGE TemplateHaskell         #-} {-# LANGUAGE LambdaCase              #-} {-# LANGUAGE PatternSynonyms         #-}+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}+{-# OPTIONS_GHC -Wno-missing-signatures                 #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns                #-}+{-# OPTIONS_GHC -Wno-orphans                            #-} -- |Usage example with template haskell support. module Generics.MRSOP.Examples.RoseTreeTH where  {-# OPTIONS_GHC -ddump-splices #-} import Data.Function (on)-import Data.Proxy  import Generics.MRSOP.Base import Generics.MRSOP.Opaque-import Generics.MRSOP.Util  import Generics.MRSOP.TH--import Control.Monad-  -- * Defining the datatype --
src/Generics/MRSOP/Examples/SimpTH.hs view
@@ -11,6 +11,10 @@ {-# LANGUAGE TemplateHaskell         #-} {-# LANGUAGE LambdaCase              #-} {-# LANGUAGE PatternSynonyms         #-}+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}+{-# OPTIONS_GHC -Wno-missing-signatures                 #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns                #-}+{-# OPTIONS_GHC -Wno-orphans                            #-} -- |Uses a more involved example to test some --  of the functionalities of @generics-mrsop@. module Generics.MRSOP.Examples.SimpTH where@@ -19,7 +23,6 @@  import Generics.MRSOP.Base import Generics.MRSOP.Opaque-import Generics.MRSOP.Util import Generics.MRSOP.Zipper  import Generics.MRSOP.Examples.LambdaAlphaEqTH hiding (FIX, alphaEq)@@ -27,7 +30,6 @@ import Generics.MRSOP.TH  import Control.Monad-import Control.Monad.State  -- * Simple IMPerative Language: @@ -78,9 +80,6 @@     galphaEq' iy (Fix x)       = maybe (return False) (go iy) . zipRep x . unFix -    unSString :: Singl k -> String-    unSString (SString s) = s-     -- Performs one default ste by eliminating the topmost Rep     -- using galphaEqT on the recursive positions and isEqv     -- on the atoms.@@ -102,8 +101,7 @@       = case sop x of           StmtStringSAssign_ (SString v1 :*: SString v2) e1e2             -> addRule v1 v2 >> uncurry' (galphaEq' IdxExpString) e1e2-          otherwise-            -> step x+          _ -> step x     go IdxDeclString x       = case sop x of           DeclStringDVar_ (SString v1 :*: SString v2)
src/Generics/MRSOP/Opaque.hs view
@@ -13,10 +13,7 @@ --   by the everyday Haskell programmer. module Generics.MRSOP.Opaque where -import Data.Function (on)-import Data.Proxy import Data.Type.Equality- import Generics.MRSOP.Util  -- * Opaque Types@@ -44,22 +41,22 @@  -- |A singleton GADT for the allowed 'Kon'stants. data Singl (kon :: Kon) :: * where-  SInt     :: Int     -> Singl KInt-  SInteger :: Integer -> Singl KInteger-  SFloat   :: Float   -> Singl KFloat-  SDouble  :: Double  -> Singl KDouble-  SBool    :: Bool    -> Singl KBool-  SChar    :: Char    -> Singl KChar-  SString  :: String  -> Singl KString+  SInt     :: Int     -> Singl 'KInt+  SInteger :: Integer -> Singl 'KInteger+  SFloat   :: Float   -> Singl 'KFloat+  SDouble  :: Double  -> Singl 'KDouble+  SBool    :: Bool    -> Singl 'KBool+  SChar    :: Char    -> Singl 'KChar+  SString  :: String  -> Singl 'KString  deriving instance Show (Singl k) deriving instance Eq   (Singl k) -instance Eq1 Singl where-  eq1 = (==)+instance EqHO Singl where+  eqHO = (==) -instance Show1 Singl where-  show1 = show+instance ShowHO Singl where+  showHO = show  -- |Equality over singletons eqSingl :: Singl k -> Singl k -> Bool
src/Generics/MRSOP/TH.hs view
@@ -4,7 +4,9 @@ {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE DeriveFunctor     #-} {-# LANGUAGE TemplateHaskell   #-}-{-# OPTIONS_GHC -cpp           #-}+{-# 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.@@ -20,19 +22,18 @@   ) where  import Data.Function (on)-import Data.Char (ord , isAlphaNum)-import Data.List (sortBy, foldl')+import Data.Char (isAlphaNum)+import Data.List (sortBy)  import Control.Monad import Control.Monad.State-import Control.Monad.Writer-import Control.Monad.Identity+import Control.Monad.Writer   (WriterT, tell, runWriterT)+import Control.Monad.Identity (runIdentity)  import Language.Haskell.TH hiding (match) import Language.Haskell.TH.Syntax (liftString)  import Generics.MRSOP.Util-import Generics.MRSOP.Opaque import Generics.MRSOP.Base.Class import Generics.MRSOP.Base.NS import Generics.MRSOP.Base.NP@@ -73,7 +74,7 @@   where     second (_ , x , _) = x     -    extractDTI (sty , (ix , Nothing))+    extractDTI (sty , (_ix , Nothing))       = fail $ "Type " ++ show sty ++ " has no datatype information."     extractDTI (sty , (ix , Just dti))       = return (sty , ix , dti)@@ -155,9 +156,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+-- defined but not used+-- dtiName :: DTI ty -> DataName+-- dtiName (ADT name _ _) = name+-- dtiName (New name _ _) = name  dti2ci :: DTI ty -> [CI ty] dti2ci (ADT _ _ cis) = cis@@ -194,8 +196,8 @@  styFold :: (a -> a -> a) -> (Name -> a) -> (Name -> a) -> STy -> a styFold app var con (AppST a b) = app (styFold app var con a) (styFold app var con b)-styFold app var con (VarST n)   = var n-styFold app var con (ConST n)   = con n+styFold _   var _   (VarST n)   = var n+styFold _   _   con (ConST n)   = con n  -- |Does a STy have a varible name? isClosed :: STy -> Bool@@ -220,14 +222,14 @@   | n == mkName "[]" = ListT   | isTupleN n       = TupleT $ length (show n) - 1   | otherwise        = ConT n-  where isTupleN n = take 2 (show n) == "(,"+  where isTupleN n0 = take 2 (show n0) == "(,"  -- |Handy substitution function. -- --  @stySubst t m n@ substitutes m for n within t, that is: t[m/n] stySubst :: STy -> Name -> STy -> STy stySubst (AppST a b) m n = AppST (stySubst a m n) (stySubst b m n)-stySubst (ConST a)   m n = ConST a+stySubst (ConST a)   _ _ = ConST a stySubst (VarST x)   m n   | x == m    = n   | otherwise = VarST x@@ -257,7 +259,7 @@  -- Extracts a DTI from a Dec decInfo :: Dec -> Q (DTI STy)-decInfo (TySynD     name args      ty)     = fail "Type Synonyms not supported"+decInfo (TySynD     _name _args _ty)       = fail "Type Synonyms not supported" decInfo (DataD    _ name args    _ cons _) = ADT name (map argInfo args) <$> mapM conInfo cons decInfo (NewtypeD _ name args    _ con _)  = New name (map argInfo args) <$> conInfo con decInfo _                                  = fail "Only type declarations are supported"@@ -300,9 +302,10 @@   | AtomK Name   deriving (Eq , Show) -ikElim :: (Int -> a) -> (Name -> a) -> IK -> a-ikElim i k (AtomI n) = i n-ikElim i k (AtomK n) = k n+-- defined but not used+-- ikElim :: (Int -> a) -> (Name -> a) -> IK -> a+-- ikElim i k (AtomI n) = i n+-- ikElim i k (AtomK n) = k n  data Idxs    = Idxs { idxsNext :: Int@@ -344,8 +347,9 @@ lkup :: (Monad m) => STy -> IdxsM m (Maybe (Int , Maybe (DTI IK))) lkup ty = M.lookup ty . idxsMap <$> get -lkupInfo :: (Monad m) => STy -> IdxsM m (Maybe Int)-lkupInfo ty = fmap fst <$> lkup ty+-- defined but not used+-- lkupInfo :: (Monad m) => STy -> IdxsM m (Maybe Int)+-- lkupInfo ty = fmap fst <$> lkup ty  lkupData :: (Monad m) => STy -> IdxsM m (Maybe (DTI IK)) lkupData ty = join . fmap snd <$> lkup ty@@ -402,7 +406,8 @@ -- |Performs step 2 of the sketch; reifySTy :: OpaqueData -> STy -> M () reifySTy opq sty-  = do ix <- indexOf sty+  = do _ <- indexOf sty -- we don't care about the index of sty now, but we+                        -- need to register it        uncurry go (styFlatten sty)   where     go :: STy -> [STy] -> M ()@@ -413,6 +418,7 @@            (final , todo) <- runWriterT $ dtiMapM (convertSTy (opaqueTable opq)) res            register sty final            mapM_ (reifySTy opq) todo+    go _ _ = fail "I can't convert appST or varST in reifySTy"          -- Convert the STy's in the fields of the constructors;     -- tells a list of STy's we still need to process.@@ -434,7 +440,7 @@      makeCons :: M.Map Name Name -> STy -> Maybe Name     makeCons opqTable (ConST n) = M.lookup n opqTable-    makeCons opqTable _         = Nothing+    makeCons _        _         = Nothing  ----------------------------- -- * Generating the Code * --@@ -525,8 +531,8 @@  -- generate the name of the type synonym corresponding to -- this int.-int2TySynName :: Int -> Name-int2TySynName i = mkName $ "D" ++ show i ++ "_"+-- int2TySynName :: Int -> Name+-- int2TySynName i = mkName $ "D" ++ show i ++ "_"  -- generates a Snat for the given Int int2SNatPat :: Int -> Pat@@ -534,6 +540,7 @@ int2SNatPat n = ConP (mkName "SS") [int2SNatPat $ n-1]  -- Our promoted type constructors+tyS , tyZ , tyI , tyK :: Type tyS = PromotedT (mkName "S") tyZ = PromotedT (mkName "Z") tyI = PromotedT (mkName "I")@@ -697,7 +704,7 @@ -- genPiece2 :: OpaqueData -> STy -> Input -> Q [Dec] genPiece2 opq first ls-  = do p21  <- mapM (\(sty , ix , dti) -> genIdxPatSyn sty ix) ls+  = do p21  <- mapM (\(sty , ix , _dti) -> genIdxPatSyn sty ix) ls        p22  <- genPiece2_2 opq first ls        -- p211 <- genHereTherePatSyn opq first ls        return $ p21 ++ p22@@ -715,7 +722,7 @@ --  will be named @OpInt_Ifx4@. -- genPiece2_2 :: OpaqueData -> STy -> Input -> Q [Dec]-genPiece2_2 opq first ls+genPiece2_2 _opq first ls   = concat <$> mapM (\(sty , ix , dti) -> genTagPatSyns sty ix dti) ls   where     genTagPatSyns :: STy -> Int -> DTI IK -> Q [Dec]@@ -799,14 +806,14 @@ --  >     , Rep (There (There (Here (NA_I (El x_1) :* NA_I (El x_2) :* NP0)))) --  >     ) ci2PatExp :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp)-ci2PatExp opq dtiIx cIdx ci+ci2PatExp opq _dtiIx cIdx ci   = do (vars , pat) <- ci2Pat ci-       bdy          <- [e| Rep $(inj cIdx $ genBdy (zip vars (ci2ty ci))) |]+       bdy          <- [e| Rep $(mkInj cIdx $ genBdy (zip vars (ci2ty ci))) |]        return (ConP (mkName "El") [pat] , bdy)   where-    inj :: Int -> Q Exp -> Q Exp-    inj 0 e = [e| Here $e              |]-    inj n e = [e| There $(inj (n-1) e) |]+    mkInj :: Int -> Q Exp -> Q Exp+    mkInj 0 e = [e| Here $e                |]+    mkInj n e = [e| There $(mkInj (n-1) e) |]      genBdy :: [(Name , IK)] -> Q Exp     genBdy []       = [e| NP0 |]@@ -824,14 +831,14 @@ --        , El (Bin x_1 x_2) --  >     ) ci2ExpPat :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp)-ci2ExpPat opq dtiIx cIdx ci -  = do (vars , exp) <- ci2Exp ci-       pat          <- [p| Rep $(inj cIdx $ genBdy (zip vars (ci2ty ci))) |]-       return (pat , AppE (ConE $ mkName "El") exp)+ci2ExpPat opq _dtiIx cIdx ci +  = do (vars , myexp) <- ci2Exp ci+       pat            <- [p| Rep $(mkInj cIdx $ genBdy (zip vars (ci2ty ci))) |]+       return (pat , AppE (ConE $ mkName "El") myexp)   where-    inj :: Int -> Q Pat -> Q Pat-    inj 0 e = [p| Here $e              |]-    inj n e = [p| There $(inj (n-1) e) |]+    mkInj :: Int -> Q Pat -> Q Pat+    mkInj 0 e = [p| Here $e                |]+    mkInj n e = [p| There $(mkInj (n-1) e) |]          genBdy :: [(Name , IK)] -> Q Pat     genBdy []       = [p| NP0 |]@@ -960,7 +967,7 @@ genFamilyDebug _ ms = concat <$> mapM genDec ms   where     genDec :: (STy , Int , DTI IK) -> Q [Dec]-    genDec (sty , ix , dti)+    genDec (_sty , ix , dti)       = [d| $( genPat ix ) = $(mkBody dti) |]      mkBody :: DTI IK -> Q Exp
src/Generics/MRSOP/Util.hs view
@@ -7,15 +7,19 @@ {-# LANGUAGE RankNTypes          #-} {-# LANGUAGE TypeApplications    #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE PatternSynonyms     #-} -- |Useful utilities we need accross multiple modules. module Generics.MRSOP.Util   ( -- * Utility Functions and Types     (&&&) , (***)   , (:->) , (<.>) -    -- * Poly-kind indexed product-  , (:*:)(..) , curry' , uncurry' , delta'+    -- * Poly-kind indexed product functionality+  , Product(..), (:*:), pattern (:*:) , Delta , curry' , uncurry' , delta +    -- * Poly-kind indexed sums+  , Sum(..) , either' , either''+     -- * Type-level Naturals   , Nat(..) , proxyUnsuc   , SNat(..) , snat2int@@ -30,33 +34,49 @@   , Lkup , Idx , El(..) , getElSNat , into      -- * Higher-order Eq and Show-  , Eq1(..) , Show1(..)+  , EqHO(..) , ShowHO(..)   ) where  import Data.Proxy import Data.Type.Equality+import Data.Functor.Product+import Data.Functor.Sum+import Data.Functor.Const import GHC.TypeLits (TypeError , ErrorMessage(..)) import Control.Arrow ((***) , (&&&)) --- |Poly-kind-indexed product-data (:*:) (f :: k -> *) (g :: k -> *) (x :: k)-  = f x :*: g x+type    (:*:)     = Product --- |Distributes the index over the product-delta' :: (f :*: g) x -> (f x , g x)-delta' (f :*: g) = (f , g)+pattern (:*:) :: f a -> g a -> Product f g a+pattern (:*:) x y = Pair x y  -- |Lifted curry-curry' :: ((f :*: g) x -> a) -> f x -> g x -> a-curry' f fx gx = f (fx :*: gx)+curry' :: (Product f g x -> a) -> f x -> g x -> a+curry' f fx gx = f (Pair fx gx)  -- |Lifted uncurry-uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a-uncurry' f (fx :*: gx) = f fx gx+uncurry' :: (f x -> g x -> a) -> Product f g x -> a+uncurry' f (Pair fx gx) = f fx gx  -- |Natural transformations type f :-> g = forall n . f n -> g n +-- |Diagonal indexed functor+type Delta f = Product f f++-- |Duplicates its argument+delta :: f :-> Delta f+delta fx = Pair fx fx++-- |Higher-order sum eliminator+either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r+either' f _ (InL x) = f x+either' _ g (InR x) = g x++-- |Just like 'either'', but the result type is of kind Star+either'' :: (forall x . f x -> a) -> (forall y . g y -> a) -> Sum f g r -> a+either'' f g = getConst . either' (Const . f) (Const . g)+ infixr 8 <.> -- |Kleisli Composition (<.>) :: (Monad m) => (b -> m c) -> (a -> m b) -> a -> m c@@ -66,13 +86,13 @@ data Nat = S Nat | Z   deriving (Eq , Show) -proxyUnsuc :: Proxy (S n) -> Proxy n+proxyUnsuc :: Proxy ('S n) -> Proxy n proxyUnsuc _ = Proxy  -- |Singleton Term-level natural data SNat :: Nat -> * where-  SZ ::           SNat Z-  SS :: SNat n -> SNat (S n)+  SZ ::           SNat 'Z+  SS :: SNat n -> SNat ('S n)  snat2int :: SNat n -> Integer snat2int SZ     = 0@@ -81,9 +101,9 @@ -- |And their conversion to term-level integers. class IsNat (n :: Nat) where   getSNat :: Proxy n -> SNat n-instance IsNat Z where-  getSNat p = SZ-instance IsNat n => IsNat (S n) where+instance IsNat 'Z where+  getSNat _ = SZ+instance IsNat n => IsNat ('S n) where   getSNat p = SS (getSNat $ proxyUnsuc p)  getNat :: (IsNat n) => Proxy n -> Integer@@ -102,15 +122,15 @@  -- |Type-level list lookup type family Lkup (n :: Nat) (ks :: [k]) :: k where-  Lkup Z     (k : ks) = k-  Lkup (S n) (k : ks) = Lkup n ks-  Lkup _     '[]      = TypeError (Text "Lkup index too big")+  Lkup 'Z     (k : ks) = k+  Lkup ('S n) (k : ks) = Lkup n ks+  Lkup _      '[]      = TypeError ('Text "Lkup index too big")  -- |Type-level list index type family Idx (ty :: k) (xs :: [k]) :: Nat where-  Idx x (x ': ys) = Z-  Idx x (y ': ys) = S (Idx x ys)-  Idx x '[]       = TypeError (Text "Element not found")+  Idx x (x ': ys) = 'Z+  Idx x (y ': ys) = 'S (Idx x ys)+  Idx x '[]       = TypeError ('Text "Element not found")  -- |Also list lookup, but for kind * only. data El :: [*] -> Nat -> * where@@ -126,7 +146,6 @@      => ty -> El fam ix into = El - -- |An inhabitant of @ListPrf ls@ is *not* a singleton! --  It only proves that @ls@ is, in fact, a type level list. --  This is useful since it enables us to pattern match on@@ -164,10 +183,31 @@ --            in Generics.MRSOP.Opaque, it seems like we don't really need this.  -- |Higher order version of 'Eq'-class Eq1 (f :: k -> *) where-  eq1 :: forall k . f k -> f k -> Bool+class EqHO (f :: ki -> *) where+  eqHO :: forall k . f k -> f k -> Bool +instance Eq a => EqHO (Const a) where+  eqHO (Const a) (Const b) = a == b++instance (EqHO f, EqHO g) => EqHO (Product f g) where+  eqHO (Pair fx gx) (Pair fy gy) = eqHO fx fy && eqHO gx gy++instance (EqHO f, EqHO g) => EqHO (Sum f g) where+  eqHO (InL fx) (InL fy) = eqHO fx fy+  eqHO (InR gx) (InR gy) = eqHO gx gy+  eqHO _        _        = False+ -- |Higher order version of 'Show'-class Show1 (f :: k -> *) where-  show1 :: forall k . f k -> String+class ShowHO (f :: ki -> *) where+  showHO :: forall k . f k -> String++instance Show a => ShowHO (Const a) where+  showHO (Const a) = show a++instance (ShowHO f , ShowHO g) => ShowHO (Product f g) where+  showHO (Pair x y) = "(" ++ showHO x ++ ", " ++ showHO y ++ ")"++instance (ShowHO f , ShowHO g) => ShowHO (Sum f g) where+  showHO (InL fx) = "InL " ++ showHO fx+  showHO (InR gx) = "InR " ++ showHO gx
src/Generics/MRSOP/Zipper.hs view
@@ -12,10 +12,7 @@ --  universe. module Generics.MRSOP.Zipper where -import Data.Type.Equality--import Generics.MRSOP.Util hiding (Cons , Nil)-import Generics.MRSOP.Base+import Generics.MRSOP.Base hiding (Cons , Nil)  -- |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@@ -42,7 +39,7 @@ -- |A @NPHole ki fam ix prod@ is a recursive position --  of type @ix@ in @prod@. data NPHole :: (kon -> *) -> [*] -> Nat -> [Atom kon] -> * where-  H :: PoA ki (El fam) xs -> NPHole ki fam ix (I ix : xs)+  H :: PoA ki (El fam) xs -> NPHole ki fam ix ('I ix : xs)   T :: NA ki (El fam) x -> NPHole ki fam ix xs -> NPHole ki fam ix (x : xs)  -- |Existential abstraction; needed for walking the possible@@ -83,8 +80,8 @@ first :: (forall ix . IsNat ix => El fam ix -> Ctx ki fam c ix -> a)       -> Rep ki (El fam) c -> Maybe a first f el | Tag c p <- sop el-  = do (ExistsIX el nphole) <- mkNPHole p-       return (f el (Ctx c nphole))+  = do (ExistsIX el0 nphole) <- mkNPHole p+       return (f el0 (Ctx c nphole))   -- |Fills up a hole.@@ -120,13 +117,13 @@ -- |Move one layer upwards within the recursive structure up :: (Family ki fam codes, IsNat ix)    => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix)-up (Loc el Nil)             = Nothing+up (Loc _  Nil)             = Nothing up (Loc el (Cons ctx ctxs)) = Just (Loc (sto $ fill el ctx) ctxs)  -- |More one hole to the right right :: (Family ki fam codes, IsNat ix)       => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix)-right (Loc el Nil)             = Nothing+right (Loc _  Nil)             = Nothing right (Loc el (Cons ctx ctxs)) = next (\el' ctx' -> Loc el' (Cons ctx' ctxs)) el ctx  -- * Interface@@ -144,6 +141,6 @@  -- |Updates the value in the hole. update :: (Family ki fam codes , IsNat ix)-       => (forall ix . SNat ix -> El fam ix -> El fam ix)+       => (forall iy . SNat iy -> El fam iy -> El fam iy)        -> Loc ki fam codes ix -> Loc ki fam codes ix update f (Loc el ctxs) = Loc (f (getElSNat el) el) ctxs
src/Generics/MRSOP/Zipper/Deep.hs view
@@ -18,29 +18,25 @@ import Control.Monad (guard) import Data.Proxy -import Generics.MRSOP.Util hiding (Cons , Nil)-import Generics.MRSOP.Base+import Generics.MRSOP.Base hiding (Cons , Nil)  -- |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+  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+  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+  T :: NA ki (Fix ki codes) x     -> NPHole ki codes ix xs     -> NPHole ki codes ix (x ': xs) @@ -51,56 +47,52 @@ -- a product -- -- dual of 'removeNPHole'-fillNPHole ::-     IsNat ix-  => Fix ki codes ix-  -> NPHole ki codes ix xs-  -> PoA ki (Fix ki codes) xs+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 :: (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 :: (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 :: (EqHO 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 :: forall ix ki codes c+           . (EqHO 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 :: (EqHO 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+  guard $ eqHO xs ys   pure x removeNPHole (T y ys) (x :* xs) = do-  guard $ eq1 x y+  guard $ eqHO x y   removeNPHole ys xs