generics-mrsop 2.1.0 → 2.2.0

raw patch · 16 files changed

+342/−495 lines, 16 filesdep +sop-coredep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: sop-core

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• ChangeLog.md +0/−29
• README.md +0/−8
• generics-mrsop.cabal +50/−78
• src/Generics/MRSOP/Base/Class.hs +1/−1
• src/Generics/MRSOP/Base/Metadata.hs +13/−10
• src/Generics/MRSOP/Base/NP.hs +27/−32
• src/Generics/MRSOP/Base/NS.hs +34/−31
• src/Generics/MRSOP/Base/Universe.hs +20/−30
• src/Generics/MRSOP/Examples/RoseTree.hs +18/−18
• src/Generics/MRSOP/Examples/SimpTH.hs +14/−5
• src/Generics/MRSOP/Holes.hs +26/−29
• src/Generics/MRSOP/Opaque.hs +0/−7
• src/Generics/MRSOP/TH.hs +93/−65
• src/Generics/MRSOP/Util.hs +37/−45
• src/Generics/MRSOP/Zipper.hs +9/−9
• src/Generics/MRSOP/Zipper/Deep.hs +0/−98

@@ -1,29 +0,0 @@-# Revision history for generics-mrsop--## 2.1.0 -- Jul 2019--- Added datatype `Holes` for representing families annotated with holes.-- Brought in some monadic attribute grammar combinators-- Big documentation update on a number of places--## 2.0.0 -- Mar 2019--- `Eq1` and `Show1` are now called `EqHO` and `ShowHO`. This avoids clashing with the-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.

@@ -1,8 +0,0 @@-# generics-mrsop--Generic Programming, with combinators, for Mutually Recursive Families in the-Sums of Products style.--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.-

@@ -1,84 +1,56 @@-name:                generics-mrsop-version:             2.1.0--synopsis:            Generic Programming with Mutually Recursive Sums of Products.--description:-  A library that supports generic programming for mutually-  recursive families in the sum-of-products style.-  .-  A couple usage examples can be found under "Generics.MRSOP.Examples"-  .--license:             MIT-license-file:        LICENSE-author:              Victor Miraldo and Alejandro Serrano-maintainer:          v.cacciarimiraldo@gmail.com--- copyright:           --category:            Generics-build-type:          Simple--extra-source-files:  ChangeLog.md, README.md-cabal-version:       1.24-tested-with:         GHC == 8.2.2, GHC == 8.4.2---library-  -- Modules exported by the library.-  exposed-modules: -    Generics.MRSOP.Base.NS,-    Generics.MRSOP.Base.NP,-    Generics.MRSOP.Base.Universe,-    Generics.MRSOP.Base.Class,-    Generics.MRSOP.Base.Combinators,-    Generics.MRSOP.Base.Metadata,-    Generics.MRSOP.Base,-    Generics.MRSOP.Opaque,-    Generics.MRSOP.Util,-    Generics.MRSOP.Holes-    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.AG--  other-extensions: -    MultiParamTypeClasses,-    FlexibleInstances,-    FlexibleContexts,-    TypeSynonymInstances,-    RankNTypes,-    TypeFamilies,-    TypeOperators,-    DataKinds,-    PolyKinds,-    GADTs,-    TypeApplications,-    ConstraintKinds,-    FunctionalDependencies,-    ScopedTypeVariables+cabal-version: 1.12 -  ghc-options: -Wall+-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 6e4f3e6671cfaeff58301e7f3a59013225b8995b0e8cb2fbb43c1d48c1158cf0 -  build-depends:       base >= 4.9 && <= 5,-                       containers,-                       template-haskell,-                       mtl-  -  hs-source-dirs:      src-  -  default-language:    Haskell2010-  +name:           generics-mrsop+version:        2.2.0+synopsis:       Generic Programming with Mutually Recursive Sums of Products.+description:    A library that supports generic programming for mutually recursive families in the sum-of-products style. . A couple usage examples can be found under "Generics.MRSOP.Examples" .+category:       Generics+homepage:       https://github.com/VictorCMiraldo/generics-mrsop#readme+bug-reports:    https://github.com/VictorCMiraldo/generics-mrsop/issues+author:         Victor Miraldo and Alejandro Serrano+maintainer:     Victor Miraldo <v.cacciarimiraldo@gmail.com>+license:        MIT+license-file:   LICENSE+build-type:     Simple  source-repository head-  type:     git+  type: git   location: https://github.com/VictorCMiraldo/generics-mrsop -source-repository this-  type:     git-  location: https://github.com/VictorCMiraldo/generics-mrsop-  tag: v2.1.0+library+  exposed-modules:+      Generics.MRSOP.AG+      Generics.MRSOP.Base+      Generics.MRSOP.Base.Class+      Generics.MRSOP.Base.Combinators+      Generics.MRSOP.Base.Metadata+      Generics.MRSOP.Base.NP+      Generics.MRSOP.Base.NS+      Generics.MRSOP.Base.Universe+      Generics.MRSOP.Examples.LambdaAlphaEqTH+      Generics.MRSOP.Examples.RoseTree+      Generics.MRSOP.Examples.RoseTreeTH+      Generics.MRSOP.Examples.SimpTH+      Generics.MRSOP.Holes+      Generics.MRSOP.Opaque+      Generics.MRSOP.TH+      Generics.MRSOP.Util+      Generics.MRSOP.Zipper+  other-modules:+      Paths_generics_mrsop+  hs-source-dirs:+      src/+  ghc-options: -Wall+  build-depends:+      base >=4.9 && <5+    , containers+    , mtl+    , sop-core+    , template-haskell+  default-language: Haskell2010

@@ -39,7 +39,7 @@ sfrom el = sfrom' (getElSNat el) el  -- |For 'sto'' there is a similar more general combinator.---  If 'ix' implements 'IsNat' we can cast it.+--  If @ix@ implements 'IsNat' we can cast it. sto :: forall fam ki codes ix      . (Family ki fam codes , IsNat ix)     => Rep ki (El fam) (Lkup ix codes) -> El fam ix  

@@ -1,3 +1,5 @@+{-# LANGUAGE UndecidableInstances   #-}+{-# LANGUAGE FlexibleContexts       #-} {-# LANGUAGE RankNTypes             #-} {-# LANGUAGE FlexibleInstances      #-} {-# LANGUAGE FunctionalDependencies #-}@@ -10,6 +12,7 @@ module Generics.MRSOP.Base.Metadata where  import Data.Proxy+import Data.SOP.Constraint  import Generics.MRSOP.Util import Generics.MRSOP.Base.NP@@ -39,17 +42,20 @@   New :: ModuleName -> DatatypeName -> ConstructorInfo '[ c ]       -> DatatypeInfo '[ '[ c ]] +-- |Returns the name of a module moduleName :: DatatypeInfo code -> ModuleName moduleName (ADT m _ _) = m moduleName (New m _ _) = m +-- |Returns the name of a datatype datatypeName :: DatatypeInfo code -> DatatypeName datatypeName (ADT _ d _) = d datatypeName (New _ d _) = d +-- |Returns information about the constructor fields constructorInfo :: DatatypeInfo code -> NP ConstructorInfo code constructorInfo (ADT _ _ c) = c-constructorInfo (New _ _ c) = c :* NP0+constructorInfo (New _ _ c) = c :* Nil  -- |Associativity information for infix constructors. data Associativity@@ -67,6 +73,7 @@   Infix       :: ConstructorName -> Associativity -> Fixity -> ConstructorInfo '[ x , y ]   Record      :: ConstructorName -> NP FieldInfo xs -> ConstructorInfo xs +-- |Returns the name of a constructor constructorName :: ConstructorInfo con -> ConstructorName constructorName (Constructor c) = c constructorName (Infix c _ _)   = c@@ -78,18 +85,14 @@  deriving instance Show (FieldInfo atom) -instance ShowHO FieldInfo where-  showHO = show--deriving instance Show (ConstructorInfo code)--instance ShowHO ConstructorInfo where-  showHO = show+deriving instance (All (Compose Show FieldInfo) code)+  => Show (ConstructorInfo code) -deriving instance Show (DatatypeInfo code)+deriving instance (All (Compose Show ConstructorInfo) code)+  => Show (DatatypeInfo code)  -- |Given a 'Family', provides the 'DatatypeInfo' for the type---  with index @ix@ in family 'fam'.+--  with index @ix@ in family @fam@. class (Family ki fam codes) => HasDatatypeInfo ki fam codes     | fam -> codes ki where   datatypeInfo :: Proxy fam -> SNat ix -> DatatypeInfo (Lkup ix codes)

@@ -7,74 +7,69 @@ {-# LANGUAGE DataKinds         #-} {-# LANGUAGE PolyKinds         #-} -- | Standard representation of n-ary products.-module Generics.MRSOP.Base.NP where+module Generics.MRSOP.Base.NP+  ( SOP.NP(..)+  , appendNP+  , listPrfNP+  , mapNP+  , mapNPM+  , elimNP+  , elimNPM+  , zipNP+  , unzipNP+  , cataNP+  , cataNPM+  , eqNP+  ) where +import           Data.SOP.NP (NP(..))+import qualified Data.SOP.NP as SOP import Generics.MRSOP.Util -infixr 5 :*--- |Indexed n-ary products. This is analogous to the @All@ datatype---  in Agda. -data NP :: (k -> *) -> [k] -> * where-  NP0  :: NP p '[]-  (:*) :: p x -> NP p xs -> NP p (x : xs)--instance EqHO phi => EqHO (NP phi) where-  eqHO = eqNP eqHO--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' appendNP :: NP p xs -> NP p ys -> NP p (xs :++: ys)-appendNP NP0        ays = ays+appendNP Nil        ays = ays appendNP (a :* axs) ays = a :* appendNP axs ays  -- |Proves that the index of a value of type 'NP' is a list. --  This is useful for pattern matching on said list without --  having to carry the product around. listPrfNP :: NP p xs -> ListPrf xs-listPrfNP NP0       = Nil-listPrfNP (_ :* xs) = Cons $ listPrfNP xs+listPrfNP Nil       = LP_Nil+listPrfNP (_ :* xs) = LP_Cons $ listPrfNP xs  -- * Map, Elim and Zip  -- |Maps a natural transformation over a n-ary product mapNP :: f :-> g -> NP f ks -> NP g ks-mapNP _ NP0       = NP0+mapNP _ Nil       = Nil 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 _ NP0       = return NP0+mapNPM _ Nil       = return Nil 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 _ NP0       = []+elimNP _ Nil       = [] 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 _ NP0       = return []+elimNPM _ Nil       = return [] elimNPM f (k :* ks) = (:) <$> f k <*> elimNPM f ks  -- |Combines two products into one. zipNP :: NP f xs -> NP g xs -> NP (f :*: g) xs-zipNP NP0       NP0       = NP0+zipNP Nil       Nil       = Nil 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 Nil               = (Nil , Nil)  unzipNP (Pair f g :* fgs) = (f :*) *** (g :*) $ unzipNP fgs  -- * Catamorphism@@ -83,7 +78,7 @@ 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 Nil       = fNil cataNP fCons  fNil (k :* ks) = fCons k (cataNP fCons fNil ks)  -- |Consumes a value of type 'NP'.@@ -91,7 +86,7 @@         => (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 Nil      = fNil cataNPM fCons fNil (k :* ks) = cataNPM fCons fNil ks >>= fCons k   

@@ -1,42 +1,45 @@-{-# LANGUAGE RankNTypes             #-}-{-# LANGUAGE FlexibleContexts       #-}-{-# LANGUAGE FlexibleInstances      #-}-{-# LANGUAGE GADTs                  #-}-{-# LANGUAGE TypeOperators          #-}-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE PolyKinds              #-}-{-# LANGUAGE ScopedTypeVariables    #-}-{-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# LANGUAGE PatternSynonyms             #-}+{-# LANGUAGE RankNTypes                  #-}+{-# LANGUAGE FlexibleContexts            #-}+{-# LANGUAGE FlexibleInstances           #-}+{-# LANGUAGE GADTs                       #-}+{-# LANGUAGE TypeOperators               #-}+{-# LANGUAGE DataKinds                   #-}+{-# LANGUAGE PolyKinds                   #-}+{-# LANGUAGE ScopedTypeVariables         #-}+{-# LANGUAGE ScopedTypeVariables         #-}+{-# OPTIONS_GHC -Wno-name-shadowing      #-}  -- | Standard representation of n-ary sums.-module Generics.MRSOP.Base.NS where+module Generics.MRSOP.Base.NS+  ( SOP.NS , pattern Here , pattern There+  , mapNS+  , mapNSM+  , elimNS +  , zipNS+  , cataNS+  , eqNS+  ) where +import qualified Data.SOP.NS as SOP+import           Data.SOP.NS (NS(..))+ import Control.Monad import Generics.MRSOP.Util ---- |Indexed n-ary sums. This is analogous to the @Any@ datatype---  in @Agda@. ---  Combinations of 'Here' and 'There's are also called injections.-data NS :: (k -> *) -> [k] -> * where-  There :: NS p xs -> NS p (x : xs)-  Here  :: p x     -> NS p (x : xs)--instance EqHO phi => EqHO (NS phi) where-  eqHO = eqNS eqHO--instance EqHO phi => Eq (NS phi xs) where-  (==) = eqHO+-- |Pattern synonym to 'SOP.S'+pattern There :: forall k (a :: k -> *) (b :: [k]). ()+              => forall (xs :: [k]) (x :: k). (b ~ (x : xs))+              => NS a xs -> NS a b+pattern There x = SOP.S x -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+-- |Pattern synonym to 'SOP.Z'+pattern Here :: forall k (a :: k -> *) (b :: [k]). ()+             => forall (x :: k) (xs :: [k]). (b ~ (x : xs))+             => a x -> NS a b+pattern Here x = SOP.Z x -instance ShowHO phi => Show (NS phi xs) where-  show = showHO+{-# COMPLETE Here, There #-}  -- * Map, Zip and Elim 

@@ -1,13 +1,15 @@-{-# LANGUAGE RankNTypes           #-}-{-# LANGUAGE FlexibleContexts     #-}-{-# LANGUAGE FlexibleInstances    #-}-{-# LANGUAGE GADTs                #-}-{-# LANGUAGE TypeOperators        #-}-{-# LANGUAGE DataKinds            #-}-{-# LANGUAGE PolyKinds            #-}-{-# LANGUAGE PatternSynonyms      #-}-{-# LANGUAGE ScopedTypeVariables  #-}-{-# LANGUAGE TypeApplications     #-}+{-# LANGUAGE QuantifiedConstraints       #-}+{-# LANGUAGE RankNTypes                  #-}+{-# LANGUAGE FlexibleContexts            #-}+{-# LANGUAGE FlexibleInstances           #-}+{-# LANGUAGE GADTs                       #-}+{-# LANGUAGE TypeOperators               #-}+{-# LANGUAGE DataKinds                   #-}+{-# LANGUAGE PolyKinds                   #-}+{-# LANGUAGE PatternSynonyms             #-}+{-# LANGUAGE ScopedTypeVariables         #-}+{-# LANGUAGE TypeApplications            #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- |Wraps the definitions of 'NP' and 'NS' --  into Representations ('Rep'), essentially providing --  the universe view over sums-of-products.@@ -47,18 +49,12 @@   NA_I :: (IsNat k) => phi k -> NA ki phi ('I k)    NA_K ::              ki  k -> NA ki phi ('K k) -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 (EqHO phi , EqHO ki) => Eq (NA ki phi at) where+  (==) = eqNA (==) (==) -instance (ShowHO phi, ShowHO ki) => Show (NA ki phi at) where-  show = showHO+instance (ShowHO phi , ShowHO ki) => Show (NA ki phi at) where+  show (NA_I i) = "(NA_I " ++ show i ++ ")"+  show (NA_K k) = "(NA_K " ++ show k ++ ")"  instance (TestEquality ki) => TestEquality (NA ki phi) where   testEquality (NA_I _) (NA_K _) = Nothing@@ -128,11 +124,8 @@ newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]])   = Rep { unRep :: NS (PoA ki phi) code } -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+  (==) = eqRep (==) (==)    -- |Product of Atoms is a handy synonym to have. type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)@@ -277,18 +270,15 @@ -- -- Finally we tie the recursive knot. Given an interpretation -- for the constant types, a family of sums-of-products and--- an index ix into such family, we take the least fixpoint of+-- an index @ix@ into such family, we take the least fixpoint of -- the representation of the code indexed by ix  -- |Indexed least fixpoints newtype Fix (ki :: kon -> *) (codes :: [[[ Atom kon ]]]) (n :: Nat)   = Fix { unFix :: Rep ki (Fix ki codes) (Lkup n codes) } -instance EqHO ki => EqHO (Fix ki codes) where-  eqHO = eqFix eqHO- instance EqHO ki => Eq (Fix ki codes ix) where-  (==) = eqFix eqHO+  (==) = eqFix (==)  -- | Catamorphism over fixpoints cata :: (IsNat ix)

@@ -86,37 +86,37 @@ -- this code automatically. -- -- >instance Family Singl FamRose CodesRose where--- >   sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0)--- >   sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* NP0))--- >   sfrom' SZ (El [])              = Rep $ Here NP0--- >   sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))+-- >   sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* Nil)+-- >   sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* Nil))+-- >   sfrom' SZ (El [])              = Rep $ Here Nil+-- >   sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* Nil)) -- >   sfrom' _ _ = error "unreachable" -- > --- >   sto' SZ (Rep (Here NP0))+-- >   sto' SZ (Rep (Here Nil)) -- >     = El []--- >   sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))))+-- >   sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* Nil)))) -- >     = El (x : xs)--- >   sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0)))+-- >   sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* Nil))) -- >     = El (a :>: as)--- >   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0))))+-- >   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* Nil)))) -- >     = El (Leaf a) -- >   sto' _ _ = error "unreachable"   instance Family Singl FamRose CodesRose where-  sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0)-  sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* NP0))-  sfrom' SZ (El [])              = Rep $ Here NP0-  sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))+  sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* Nil)+  sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* Nil))+  sfrom' SZ (El [])              = Rep $ Here Nil+  sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* Nil))   sfrom' _ _ = error "unreachable" -  sto' SZ (Rep (Here NP0))+  sto' SZ (Rep (Here Nil))     = El []-  sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))))+  sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* Nil))))     = El (x : xs)-  sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0)))+  sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* Nil)))     = El (a :>: as)-  sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0))))+  sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* Nil))))     = El (Leaf a)   sto' _ _ = error "unreachable" @@ -125,12 +125,12 @@     = ADT "module" (Name "[]" :@: (Name "R" :@: Name "Int"))       $  (Constructor "[]")       :* (Infix ":" RightAssociative 5)-      :* NP0+      :* Nil   datatypeInfo _ (SS SZ)     = ADT "module" (Name "R" :@: Name "Int")       $  (Infix ":>:" NotAssociative 0)       :* (Constructor "Leaf")-      :* NP0+      :* Nil   datatypeInfo _ _     = error "unreachable" 

@@ -45,11 +45,19 @@   | SSkip   deriving Show -data Decl var+-- Below is a little type synonym fun, to make sure+-- generation is working+data ODecl var   = DVar var   | DFun var var (Stmt var)   deriving Show +-- Note that since we use 'Decl' directly in the family;+-- there won't be pattern-synonyms generated for 'ODecl' or 'TDecl'+type Decl x = TDecl x++type TDecl x = ODecl x+ data Exp var   = EVar  var   | ECall var (Exp var)@@ -157,6 +165,7 @@  -} + test3 :: String -> String -> String -> Decl String test3 n1 n2 z = DFun "f" n1               $ SDecl (DFun "g" n2@@ -196,12 +205,12 @@  test6 :: Holes Singl CodesStmtString (Const Int) ('I ('S 'Z)) test6 = HPeel' (CS (CS CZ))-          (  (HPeel' CZ (HOpq' (SString "lol") :* NP0))+          (  (HPeel' CZ (HOpq' (SString "lol") :* Nil))           :* (Hole' (Const 42))-          :* NP0)+          :* Nil)  test7 :: HolesAnn (Const Int) Singl CodesStmtString (Const Int) ('I ('S 'Z)) test7 = HPeel (Const 1) (CS (CS CZ))-          (  (HPeel (Const 2) CZ (HOpq (Const 4) (SString "lol") :* NP0))+          (  (HPeel (Const 2) CZ (HOpq (Const 4) (SString "lol") :* Nil))           :* (Hole (Const 3) (Const 42))-          :* NP0)+          :* Nil)

@@ -1,4 +1,5 @@-{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE UndecidableInstances  #-} {-# LANGUAGE PatternSynonyms       #-} {-# LANGUAGE FlexibleInstances     #-} {-# LANGUAGE RankNTypes            #-}@@ -190,7 +191,7 @@ holesRefineAnnM f g (HPeel a c holesnp)   = HPeel a c <$> mapNPM (holesRefineAnnM f g) holesnp --- |Just like 'holesRefineM', but only refines variables. One example is to implement+-- |Just like 'holesRefineAnnM', but only refines variables. One example is to implement -- 'holesJoin' with it. -- -- > holesJoin = runIdentity . holesRefineVarsM (\_ -> return)@@ -201,7 +202,7 @@                  -> m (HolesAnn ann ki codes g at) holesRefineVarsM f = holesRefineAnnM f (\a -> return . HOpq a) --- |Pure version of 'holesRefineM'+-- |Pure version of 'holesRefineAnnM' holesRefineAnn :: (forall ix . ann ix     -> f ix -> HolesAnn ann ki codes g ix) -- ^                -> (forall k  . ann ('K k) -> ki k -> HolesAnn ann ki codes g ('K k))                -> HolesAnn ann ki codes f at @@ -277,18 +278,25 @@ --  @Const ()@ type Holes = HolesAnn (Const ()) +-- |Synonym to @Hole (Const ())@ pattern Hole' :: phi at -> Holes ki codes phi at pattern Hole' x = Hole (Const ()) x ++-- |Synonym to @HOpq (Const ())@ pattern HOpq' :: ki k -> Holes ki codes phi ('K k) pattern HOpq' x = HOpq (Const ()) x ++-- |Synonym to @HPeel (Const ())@ pattern HPeel' :: () => (IsNat n, IsNat i)                => Constr (Lkup i codes) n                -> NP (Holes ki codes phi) (Lkup n (Lkup i codes))                -> Holes ki codes phi ('I i) pattern HPeel' c p = HPeel (Const ()) c p +{-# COMPLETE Hole' , HOpq' , HPeel' #-}+ -- |Factors out the largest common prefix of two treefixes. --  This is also known as the anti-unification of two --  treefixes.@@ -300,13 +308,13 @@ -- --  We use a function to combine annotations in case it is --  necessary.-holesLCP :: (EqHO ki)+holesLCP :: (forall k . Eq (ki k))          => Holes ki codes f at          -> Holes ki codes g at          -> Holes ki codes (Holes ki codes f :*: Holes ki codes g) at holesLCP (HOpq _ kx) (HOpq _ ky)-  | eqHO kx ky = HOpq' kx-  | otherwise  = Hole' (HOpq' kx :*: HOpq' ky)+  | kx == ky  = HOpq' kx+  | otherwise = Hole' (HOpq' kx :*: HOpq' ky) holesLCP (HPeel a cx px) (HPeel b cy py)   = case testEquality cx cy of       Nothing   -> Hole'  (HPeel a cx px :*: HPeel b cy py)@@ -353,21 +361,18 @@   utx == uty = and $ holesGetHolesAnnWith' (uncurry' cmp) $ holesLCP utx uty     where       cmp :: HolesAnn ann ki codes phi at -> HolesAnn ann ki codes phi at -> Bool-      cmp (Hole _ x) (Hole _ y) = eqHO x y-      cmp (HOpq _ x) (HOpq _ y) = eqHO x y+      cmp (Hole _ x) (Hole _ y) = x == y+      cmp (HOpq _ x) (HOpq _ y) = x == y       cmp _           _         = False -instance (EqHO phi , EqHO ki) => EqHO (Holes ki codes phi) where-  eqHO utx uty = utx == uty- holesShow :: forall ki ann f fam codes ix            . (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f)           => Proxy fam           -> (forall at . ann at -> ShowS)           -> HolesAnn ann ki codes f ix           -> ShowS-holesShow _ f (Hole a x)       = ('`':) . f a . showString (showHO x) -holesShow _ f (HOpq a k)       = f a . showString (showHO k)+holesShow _ f (Hole a x)       = ('`':) . f a . showString (show x) +holesShow _ f (HOpq a k)       = f a . showString (show k) holesShow p f h@(HPeel a c rest)   = showParen (needParens h) $ showString cname                              . f a@@ -383,27 +388,19 @@       (Infix name _ _)   -> "(" ++ name ++ ")"       needParens :: HolesAnn ann ki codes f iy -> Bool-    needParens (Hole _ _) = False-    needParens (HOpq _ _) = False-    needParens (HPeel _ _ NP0) = False-    needParens _          = True+    needParens (Hole _ _)      = False+    needParens (HOpq _ _)      = False+    needParens (HPeel _ _ Nil) = False+    needParens _               = True  instance {-# OVERLAPPABLE #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f , ShowHO ann)-    => ShowHO (HolesAnn ann ki codes f) where-  showHO h = holesShow (Proxy :: Proxy fam) showsAnn h ""+    => Show (HolesAnn ann ki codes f ix) where+  show h = holesShow (Proxy :: Proxy fam) showsAnn h ""     where       showsAnn ann = showString "{"-                   . showString (showHO ann)+                   . showString (show ann)                    . showString "}" -instance {-# OVERLAPPABLE #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f , ShowHO ann)-    => Show (HolesAnn ann ki codes f at) where-  show = showHO- instance {-# OVERLAPPING #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f)-    => ShowHO (Holes ki codes f) where-  showHO h = holesShow (Proxy :: Proxy fam) (const id) h ""--instance {-# OVERLAPPING #-} (HasDatatypeInfo ki fam codes , ShowHO ki , ShowHO f)     => Show (Holes ki codes f at) where-  show = showHO+  show h = holesShow (Proxy :: Proxy fam) (const id) h ""

@@ -14,7 +14,6 @@ module Generics.MRSOP.Opaque where  import Data.Type.Equality-import Generics.MRSOP.Util  -- * Opaque Types --@@ -59,12 +58,6 @@  show (SBool     a) = show a  show (SChar     a) = show a  show (SString   a) = show a--instance EqHO Singl where-  eqHO = (==)--instance ShowHO Singl where-  showHO = show  -- |Equality over singletons eqSingl :: Singl k -> Singl k -> Bool

@@ -26,34 +26,34 @@ --  >  --  > -- (:>:) pattern syn --  > pattern RoseInt_Ifx0 :: kon KInt -> phi (S Z) -> View kon phi (Lkup Z CodesRoseInt)---  > pattern RoseInt_Ifx0 p q = Tag CZ (NA_K p :* (NA_I q :* NP0))+--  > pattern RoseInt_Ifx0 p q = Tag CZ (NA_K p :* (NA_I q :* Nil)) --  >  --  > -- Leaf pattern syn --  > pattern RoseIntLeaf_ :: kon KInt -> View kon phi (Lkup Z CodesRoseInt)---  > pattern RoseIntLeaf_ p = Tag (CS CZ) (NA_K p :* NP0)+--  > pattern RoseIntLeaf_ p = Tag (CS CZ) (NA_K p :* Nil) --  >  --  > -- [] pattern syn --  > pattern ListRoseInt_Ifx0 :: View kon phi (Lkup (S Z) CodesRoseInt)---  > pattern ListRoseInt_Ifx0 = Tag CZ NP0+--  > pattern ListRoseInt_Ifx0 = Tag CZ Nil --  >  --  > -- (:) pattern syn --  > pattern ListRoseInt_Ifx1 :: phi Z -> phi (S Z) -> View kon phi (Lkup (S Z) CodesRoseInt)---  > pattern ListRoseInt_Ifx1 p q = Tag (CS CZ) (NA_I p :* (NA_I q :* NP0))+--  > pattern ListRoseInt_Ifx1 p q = Tag (CS CZ) (NA_I p :* (NA_I q :* Nil)) --  >  --  > instance Family Singl FamRose CodesRose where---  >   sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* NP0)---  >   sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* NP0))---  >   sfrom' SZ (El [])              = Rep $ Here NP0---  >   sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))+--  >   sfrom' (SS SZ) (El (a :>: as)) = Rep $ Here (NA_K (SInt a) :* NA_I (El as) :* Nil)+--  >   sfrom' (SS SZ) (El (Leaf a))   = Rep $ There (Here (NA_K (SInt a) :* Nil))+--  >   sfrom' SZ (El [])              = Rep $ Here Nil+--  >   sfrom' SZ (El (x:xs))          = Rep $ There (Here (NA_I (El x) :* NA_I (El xs) :* Nil)) --  >   sfrom' _ _ = error "unreachable" --  > ---  >   sto' SZ (Rep (Here NP0))+--  >   sto' SZ (Rep (Here Nil)) --  >     = El []---  >   sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))))+--  >   sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* Nil)))) --  >     = El (x : xs)---  >   sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0)))+--  >   sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* Nil))) --  >     = El (a :>: as)---  >   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0))))+--  >   sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* Nil)))) --  >     = El (Leaf a) --  >   sto' _ _ = error "unreachable" --  > @@ -62,12 +62,12 @@ --  >     = ADT "module" (Name "[]" :@: (Name "R" :@: Name "Int")) --  >       $  (Constructor "[]") --  >       :* (Infix ":" RightAssociative 5)---  >       :* NP0+--  >       :* Nil --  >   datatypeInfo _ (SS SZ) --  >     = ADT "module" (Name "R" :@: Name "Int") --  >       $  (Infix ":>:" NotAssociative 0) --  >       :* (Constructor "Leaf")---  >       :* NP0+--  >       :* Nil --  >   datatypeInfo _ _ --  >     = error "unreachable" --@@ -135,7 +135,7 @@ --  > pattern DeclStringDVar_  --  > pattern DeclStringDFun_  -----  We did ommit the definitions and 'Family' and 'HasDatatypeInfo' instances+--  We did ommit the definitions and 'Family' and 'Generics.MRSOP.Base.Metadata.HasDatatypeInfo' instances --  for brevity here. If you want to see the actual generated code, compile with --   --  > stack build ghc-options="-ddump-splices -ddump-to-file"@@ -157,6 +157,7 @@ import Data.Function (on) import Data.Char (isAlphaNum) import Data.List (sortBy)+import qualified Data.SOP.NS as SOP (NS(..))  import Control.Monad import Control.Monad.State@@ -168,7 +169,6 @@  import Generics.MRSOP.Util import Generics.MRSOP.Base.Class-import Generics.MRSOP.Base.NS import Generics.MRSOP.Base.NP import Generics.MRSOP.Base.Universe hiding (match) import qualified Generics.MRSOP.Base.Metadata as Meta@@ -187,16 +187,16 @@ -- |Given the name of the first element in the family, --  derives: -----    1. The other types in the family and Konstant types one needs.+--    1. The other types in the family and opaque types one needs. --    2. the SOP code for each of the datatypes involved---    3. One 'Element' instance per datatype+--    3. The 'Family' instance --    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 -       opqData          <- reifyOpaqueType opqName-       (_ , (Idxs _ m)) <- runIdxsM (reifySTy opqData sty)+  = do sty                <- t >>= convertType +       opqData            <- reifyOpaqueType opqName+       (_ , (Idxs _ m _)) <- runIdxsM (reifySTy opqData sty)        -- Now we make sure we have processed all        -- types        m' <- mapM extractDTI (M.toList m)@@ -445,17 +445,18 @@ data Idxs    = Idxs { idxsNext :: Int          , idxsMap  :: M.Map STy (Int , Maybe (DTI IK))+         , idxsSyns :: M.Map STy STy          }   deriving (Show)  onMap :: (M.Map STy (Int , Maybe (DTI IK)) -> M.Map STy (Int , Maybe (DTI IK)))       -> Idxs -> Idxs-onMap f (Idxs n m) = Idxs n (f m)+onMap f (Idxs n m eqs) = Idxs n (f m) eqs  type IdxsM = StateT Idxs  runIdxsM :: (Monad m) => IdxsM m a -> m (a , Idxs)-runIdxsM = flip runStateT (Idxs 0 M.empty)+runIdxsM = flip runStateT (Idxs 0 M.empty M.empty)  -- |The actual monad we need to run all of this; type M = IdxsM Q@@ -466,11 +467,16 @@ indexOf :: (Monad m) => STy -> IdxsM m Int indexOf name   = do st <- get-       case M.lookup name (idxsMap st) of-         Just i  -> return (fst i)-         Nothing -> let i = idxsNext st-                     in put (Idxs (i + 1) (M.insert name (i , Nothing) (idxsMap st)))-                     >> return i+       case M.lookup name (idxsSyns st) of+         Just orig -> indexOf orig -- TODO: make sure orig is in the map! :P+         Nothing ->+           case M.lookup name (idxsMap st) of+             Just i  -> return (fst i)+             Nothing -> let i = idxsNext st+                         in put (Idxs (i + 1)+                                      (M.insert name (i , Nothing) (idxsMap st))+                                      (idxsSyns st))+                         >> return i  -- |Register some Datatype Information for a given STy register :: (Monad m) => STy -> DTI IK -> IdxsM m ()@@ -482,6 +488,12 @@ lkup :: (Monad m) => STy -> IdxsM m (Maybe (Int , Maybe (DTI IK))) lkup ty = M.lookup ty . idxsMap <$> get ++-- | Adds another type with the same index as the previous+addTySynEquiv :: (Monad m) => STy -> STy -> IdxsM m ()+addTySynEquiv orig new = +  modify (\st -> st { idxsSyns = M.insert new orig (idxsSyns st) })+ -- defined but not used -- lkupInfo :: (Monad m) => STy -> IdxsM m (Maybe Int) -- lkupInfo ty = fmap fst <$> lkup ty@@ -537,23 +549,39 @@      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 :: OpaqueData -> STy -> M ()-reifySTy opq sty-  = do _ <- indexOf sty -- we don't care about the index of sty now, but we+reifySTy opq sty0+  = do _ <- indexOf sty0 -- we don't care about the index of sty now, but we                         -- need to register it-       uncurry go (styFlatten sty)+       (dec , args) <- preprocess sty0+       go dec args   where-    go :: STy -> [STy] -> M ()-    go (ConST name) args-      = do dec <- lift (reifyDec name >>= decInfo)-           -- TODO: Check that the precondition holds.+    preprocess :: STy -> M (DTI STy , [STy])+    preprocess ty = +      let (head , args) = styFlatten ty+       in case head of+         ConST name -> do+           dec <- lift (reifyDec name)+           resolveTySyn (addTySynEquiv ty) dec args+         _ -> fail "I can't convert appST or varST in reifySTy"++    resolveTySyn :: (STy -> M ()) -> Dec -> [STy] -> M (DTI STy , [STy])+    resolveTySyn upd8 (TySynD _ defargs def) localargs = do+      sdef <- convertType def+      let dict = zip (map argInfo defargs) localargs+      let res = styReduce dict sdef+      upd8 res+      preprocess res+    resolveTySyn _ def localargs = (,localargs) <$> lift (decInfo def)+    +    go :: DTI STy -> [STy] -> M ()+    go dec args+      = do -- TODO: Check that the precondition holds.            let res = dtiReduce dec args            (final , todo) <- runWriterT $ dtiMapM (convertSTy (opaqueTable opq)) res-           register sty final+           register sty0 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.@@ -561,7 +589,7 @@     convertSTy opqTable ty       -- We remove sty from the list of todos       -- otherwise we get an infinite loop-      | ty == sty = AtomI <$> lift (indexOf ty)+      | ty == sty0 = AtomI <$> lift (indexOf ty)       | isClosed ty       = case makeCons opqTable ty of           Just k  -> return (AtomK k)@@ -571,7 +599,7 @@                         return (AtomI ix)       | otherwise       = fail $ "I can't convert type variable " ++ show ty-              ++ " when converting " ++ show sty+              ++ " when converting " ++ show sty0      makeCons :: M.Map Name Name -> STy -> Maybe Name     makeCons opqTable (ConST n) = M.lookup n opqTable@@ -616,33 +644,33 @@ --   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)--- > pattern nil_      = Tag CZ NP0--- > pattern a :_ as   = Tag (CS CZ) (NA_I a :* NA_I (El as) :* NP0)+-- > pattern a :>:_ as = Tag CZ      (NA_K a :* NA_I (El as) :* Nil)+-- > pattern Leaf_ a   = Tag (CS CZ) (NA_K a :* Nil)+-- > pattern nil_      = Tag CZ Nil+-- > pattern a :_ as   = Tag (CS CZ) (NA_I a :* NA_I (El as) :* Nil) -- -- 3. The instance: -- > instance Family Singl FamRose CodesRose where -- -- 3.1. for each type in (1) -- >   sfrom' (SS SZ) (El (a :>: as))--- >     = Rep $ HT0_ (NA_K (SInt a) :* NA_I (El as) :* NP0)+-- >     = Rep $ HT0_ (NA_K (SInt a) :* NA_I (El as) :* Nil) -- >   sfrom' (SS SZ) (El (Leaf a))--- >     = Rep $ HT1_ (NA_K (SInt a) :* NP0)+-- >     = Rep $ HT1_ (NA_K (SInt a) :* Nil) -- >   sfrom' SZ (El [])--- >     = Rep $ HT0_ NP0+-- >     = Rep $ HT0_ Nil -- >   sfrom' SZ (El (x:xs))--- >     = Rep $ HT1_ (NA_I (El x) :* NA_I (El xs) :* NP0)+-- >     = Rep $ HT1_ (NA_I (El x) :* NA_I (El xs) :* Nil) -- -- 3.2. -- > --- >   sto' SZ (Rep (HT0_ NP0))+-- >   sto' SZ (Rep (HT0_ Nil)) -- >     = El []--- >   sto' SZ (Rep (HT1_ (NA_I (El x) :* NA_I (El xs) :* NP0)))+-- >   sto' SZ (Rep (HT1_ (NA_I (El x) :* NA_I (El xs) :* Nil))) -- >     = El (x : xs)--- >   sto' (SS SZ) (Rep (HT0_ (NA_K (SInt a) :* NA_I (El as) :* NP0)))+-- >   sto' (SS SZ) (Rep (HT0_ (NA_K (SInt a) :* NA_I (El as) :* Nil))) -- >     = El (a :>: as)--- >   sto' (SS SZ) (Rep (HT1_ (NA_K (SInt a) :* NP0)))+-- >   sto' (SS SZ) (Rep (HT1_ (NA_K (SInt a) :* Nil))) -- >     = El (Leaf a) -- -- 4. Metadata for each type in (1)@@ -728,7 +756,7 @@   where     first (x , _ , _) = x --- | @styToName "List (R Int)" == "ListRInt"@+-- | @styToName "[R Int]" == "ListRInt"@ styToName :: STy -> Name styToName = mkName . styFold (++) nameBase (fixList . nameBase)   where@@ -912,7 +940,7 @@     ciHasIllegalName ci = any (not . isAlphaNum) $ nameBase (ciName ci)      tagPatSynProd :: [(IK , Name)] -> Q Pat-    tagPatSynProd []     = [p| NP0 |]+    tagPatSynProd []     = [p| Nil |]     tagPatSynProd (h:hs) = [p| $(tagPatSynProdHead h) :* ( $(tagPatSynProd hs) ) |]      int2Constr :: Int -> Q Pat@@ -937,7 +965,7 @@ -- --  > ci2PatExp opq IdxBinTree 3 (Normal "Bin" [VarT a , VarT a]) --  >   = ( El (Bin x_1 x_2)---  >     , Rep (There (There (Here (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) :* Nil)))) --  >     ) ci2PatExp :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp) ci2PatExp opq _dtiIx cIdx ci@@ -946,11 +974,11 @@        return (ConP (mkName "El") [pat] , bdy)   where     mkInj :: Int -> Q Exp -> Q Exp-    mkInj 0 e = [e| Here $e                |]-    mkInj n e = [e| There $(mkInj (n-1) e) |]+    mkInj 0 e = [e| SOP.Z $e               |]+    mkInj n e = [e| SOP.S $(mkInj (n-1) e) |]      genBdy :: [(Name , IK)] -> Q Exp-    genBdy []       = [e| NP0 |]+    genBdy []       = [e| Nil |]     genBdy (x : xs) = [e| $(mkHead x) :* ( $(genBdy xs) ) |]  @@ -961,7 +989,7 @@ -- | Just like 'ci2PatExp', but the other way around. -- --  > 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))))+--  >   = ( Rep (There (There (Here (NA_I (El x_1) :* NA_I (El x_2) :* Nil)))) --        , El (Bin x_1 x_2) --  >     ) ci2ExpPat :: OpaqueData -> Int -> Int -> CI IK -> Q (Pat , Exp)@@ -971,11 +999,11 @@        return (pat , AppE (ConE $ mkName "El") myexp)   where     mkInj :: Int -> Q Pat -> Q Pat-    mkInj 0 e = [p| Here $e                |]-    mkInj n e = [p| There $(mkInj (n-1) e) |]+    mkInj 0 e = [p| SOP.Z $e                |]+    mkInj n e = [p| SOP.S $(mkInj (n-1) e) |]          genBdy :: [(Name , IK)] -> Q Pat-    genBdy []       = [p| NP0 |]+    genBdy []       = [p| Nil |]     genBdy (x : xs) = [p| $(mkHead x) :* ( $(genBdy xs) ) |]  @@ -1079,16 +1107,16 @@         genFix (Fixity i _) = return . LitE . IntegerL . fromIntegral $ i      genFieldInfo :: [ FieldName ] -> Q Exp-    genFieldInfo []     = [e| NP0 |]+    genFieldInfo []     = [e| Nil |]     genFieldInfo (f:fs) = [e| Meta.FieldInfo $(strlit . nameBase $ f) :* ( $(genFieldInfo fs) ) |]      genConInfoNP :: [ CI IK ] -> Q Exp-    genConInfoNP []       = [e| NP0 |]+    genConInfoNP []       = [e| Nil |]     genConInfoNP (ci:cis) = [e| $(genConInfo ci) :* ( $(genConInfoNP cis) ) |]  -- |@genFamily opq init fam@ generates a type-level list --  of the codes for the family. It also generates---  the necessary 'Family' and 'HasDatatypeInfo' instances.+--  the necessary 'Family' and 'Generics.MRSOP.Base.Metadata.HasDatatypeInfo' instances. -- --  Precondition, input is sorted on second component. genFamily :: OpaqueData -> STy -> Input -> Q [Dec]

@@ -1,13 +1,16 @@-{-# LANGUAGE ConstraintKinds     #-}-{-# LANGUAGE GADTs               #-}-{-# LANGUAGE TypeFamilies        #-}-{-# LANGUAGE DataKinds           #-}-{-# LANGUAGE PolyKinds           #-}-{-# LANGUAGE TypeOperators       #-}-{-# LANGUAGE RankNTypes          #-}-{-# LANGUAGE TypeApplications    #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE PatternSynonyms     #-}+{-# LANGUAGE TypeSynonymInstances  #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE PatternSynonyms       #-}+{-# OPTIONS_GHC -Wno-orphans       #-} -- |Useful utilities we need accross multiple modules. module Generics.MRSOP.Util   ( -- * Utility Functions and Types@@ -34,7 +37,7 @@   , Lkup , Idx , El(..) , getElSNat , into      -- * Higher-order Eq and Show-  , EqHO(..) , ShowHO(..)+  , EqHO , ShowHO   ) where  import Data.Proxy@@ -45,10 +48,13 @@ import GHC.TypeLits (TypeError , ErrorMessage(..)) import Control.Arrow ((***) , (&&&)) +-- |Convenient type synonym for 'Product' type    (:*:)     = Product +-- |Convnient pattern synonym for 'Pair' pattern (:*:) :: f a -> g a -> Product f g a pattern (:*:) x y = Pair x y+{-# COMPLETE (:*:) #-}  -- |Lifted curry curry' :: (Product f g x -> a) -> f x -> g x -> a@@ -86,6 +92,7 @@ data Nat = S Nat | Z   deriving (Eq , Show) +-- |Typelevel predecessor operation proxyUnsuc :: Proxy ('S n) -> Proxy n proxyUnsuc _ = Proxy @@ -94,6 +101,7 @@   SZ ::           SNat 'Z   SS :: SNat n -> SNat ('S n) +-- |Returns @n@ as a first class integer. snat2int :: SNat n -> Integer snat2int SZ     = 0 snat2int (SS n) = 1 + snat2int n@@ -151,22 +159,22 @@ --  This is useful since it enables us to pattern match on --  type-level lists whenever we see fit. data ListPrf :: [k] -> * where-  Nil ::  ListPrf '[]-  Cons :: ListPrf l ->  ListPrf (x ': l)+  LP_Nil  :: ListPrf '[]+  LP_Cons :: ListPrf l ->  ListPrf (x ': l)  -- |The @IsList@ class allows us to construct --  'ListPrf's in a straight forward fashion. class IsList (xs :: [k]) where   listPrf :: ListPrf xs instance IsList '[] where-  listPrf = Nil+  listPrf = LP_Nil instance IsList xs => IsList (x ': xs) where-  listPrf = Cons listPrf+  listPrf = LP_Cons listPrf  -- |Concatenation of lists is also a list. appendIsListLemma :: ListPrf xs -> ListPrf ys -> ListPrf (xs :++: ys)-appendIsListLemma Nil         isys = isys-appendIsListLemma (Cons isxs) isys = Cons (appendIsListLemma isxs isys)+appendIsListLemma LP_Nil         isys = isys+appendIsListLemma (LP_Cons isxs) isys = LP_Cons (appendIsListLemma isxs isys)  -- |Appending type-level lists type family (:++:) (txs :: [k]) (tys :: [k]) :: [k] where@@ -179,35 +187,19 @@ type L3 xs ys zs    = (IsList xs, IsList ys, IsList zs)  type L4 xs ys zs as = (IsList xs, IsList ys, IsList zs, IsList as)  --- TODO: VCM: looking at the implementation for the instances---            in Generics.MRSOP.Opaque, it seems like we don't really need this.---- |Higher order version of 'Eq'-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 ShowHO (f :: ki -> *) where-  showHO :: forall k . f k -> String+-- |Constraint synonym replacing the old @EqHO@ hack.+-- @since 2.2.0+type EqHO   f = forall x . Eq   (f x) -instance Show a => ShowHO (Const a) where-  showHO (Const a) = show a+-- |Constraint synonym replacing the old @ShowHO@ hack.+-- @since 2.2.0+type ShowHO f = forall x . Show (f x) -instance (ShowHO f , ShowHO g) => ShowHO (Product f g) where-  showHO (Pair x y) = "(" ++ showHO x ++ ", " ++ showHO y ++ ")"+instance (EqHO f , EqHO g) => Eq ((f :*: g) x) where+  (fx :*: gx) == (fy :*: gy) = fx == fy && gx == gy -instance (ShowHO f , ShowHO g) => ShowHO (Sum f g) where-  showHO (InL fx) = "InL " ++ showHO fx-  showHO (InR gx) = "InR " ++ showHO gx+instance (EqHO f , EqHO g) => Eq (Sum f g x) where+  (InL x) == (InL y) = x == y+  (InR x) == (InR y) = x == y+  _       == _       = False 

@@ -12,7 +12,7 @@ --  universe. module Generics.MRSOP.Zipper where -import Generics.MRSOP.Base hiding (Cons , Nil)+import Generics.MRSOP.Base   -- |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@@ -24,7 +24,7 @@ -- |A @Ctxs ki fam codes ix iy@ represents a value of type @El fam ix@ --  with a @El fam iy@-typed hole in it. data Ctxs :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> Nat -> * where-  Nil  :: Ctxs ki fam cs ix ix+  CNil :: Ctxs ki fam cs ix ix   Cons :: (IsNat ix , IsNat a , IsNat b)        => Ctx ki fam (Lkup ix cs) b -> Ctxs ki fam cs a ix        -> Ctxs ki fam cs a b@@ -52,7 +52,7 @@ --  with the existential because we don't know, a priori, what --  will be the type of such hole. mkNPHole :: PoA ki (El fam) xs -> Maybe (NPHoleE ki fam xs)-mkNPHole NP0 = Nothing+mkNPHole Nil = Nothing mkNPHole (NA_I x :* xs) = Just (ExistsIX x (H xs)) mkNPHole (NA_K k :* xs)   = do (ExistsIX el c) <- mkNPHole xs@@ -93,7 +93,7 @@ -- 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 CNil = h fillCtxs h (Cons ctx ctxs) =   fillCtxs (sto @fam @ki @c $ fill h ctx) ctxs @@ -117,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 _  Nil)             = Nothing+up (Loc _  CNil)            = 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 _  Nil)             = Nothing+right (Loc _  CNil)            = Nothing right (Loc el (Cons ctx ctxs)) = next (\el' ctx' -> Loc el' (Cons ctx' ctxs)) el ctx  -- * Interface@@ -131,13 +131,13 @@ -- |Initializes the zipper enter :: (Family ki fam codes , IsNat ix)       => El fam ix -> Loc ki fam codes ix-enter el = Loc el Nil+enter el = Loc el CNil  -- |Exits the zipper leave :: (Family ki fam codes , IsNat ix)       => Loc ki fam codes ix -> El fam ix-leave (Loc x Nil) = x-leave loc         = maybe undefined leave $ up loc -- up returns a just!+leave (Loc x CNil) = x+leave loc          = maybe undefined leave $ up loc -- up returns a just!  -- |Updates the value in the hole. update :: (Family ki fam codes , IsNat ix)

@@ -1,98 +0,0 @@-{-# 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.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---- |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 :: (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-           . (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 :: (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 $ eqHO xs ys-  pure x-removeNPHole (T y ys) (x :* xs) = do-  guard $ eqHO x y-  removeNPHole ys xs