generics-mrsop (empty) → 1.0.0.1

raw patch · 21 files changed

+2589/−0 lines, 21 filesdep +basedep +containersdep +mtlsetup-changed

Dependencies added: base, containers, mtl, template-haskell

Files

• ChangeLog.md +5/−0
• LICENSE +21/−0
• README.md +6/−0
• Setup.hs +2/−0
• generics-mrsop.cabal +79/−0
• src/Generics/MRSOP/Base.hs +19/−0
• src/Generics/MRSOP/Base/Class.hs +93/−0
• src/Generics/MRSOP/Base/Combinators.hs +96/−0
• src/Generics/MRSOP/Base/Metadata.hs +116/−0
• src/Generics/MRSOP/Base/NP.hs +78/−0
• src/Generics/MRSOP/Base/NS.hs +63/−0
• src/Generics/MRSOP/Base/Show.hs +50/−0
• src/Generics/MRSOP/Base/Universe.hs +264/−0
• src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs +132/−0
• src/Generics/MRSOP/Examples/RoseTree.hs +101/−0
• src/Generics/MRSOP/Examples/RoseTreeTH.hs +89/−0
• src/Generics/MRSOP/Examples/SimpTH.hs +206/−0
• src/Generics/MRSOP/Opaque.hs +66/−0
• src/Generics/MRSOP/TH.hs +795/−0
• src/Generics/MRSOP/Util.hs +169/−0
• src/Generics/MRSOP/Zipper.hs +139/−0

@@ -0,0 +1,5 @@+# Revision history for generics-mrsop++## 1.0.0.0  -- May 2018++* First version. Released on an unsuspecting world.

@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2018, Victor Miraldo and Alejandro Serrano++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.

@@ -0,0 +1,6 @@+# generics-mrsop++Generic Programming for Mutually Recursive Families in the+Sums of Products style.++Check the `Generics.MRSOP.Examples.RoseTreeTH` for a quick start.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,79 @@+name:                generics-mrsop+version:             1.0.0.1++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:       2.0+++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.Show,+    Generics.MRSOP.Base,+    Generics.MRSOP.Opaque,+    Generics.MRSOP.Util,+    Generics.MRSOP.TH,+    Generics.MRSOP.Zipper,+    Generics.MRSOP.Examples.RoseTree,+    Generics.MRSOP.Examples.RoseTreeTH,+    Generics.MRSOP.Examples.LambdaAlphaEqTH,+    Generics.MRSOP.Examples.SimpTH++  other-extensions: +    MultiParamTypeClasses,+    FlexibleInstances,+    FlexibleContexts,+    TypeSynonymInstances,+    RankNTypes,+    TypeFamilies,+    TypeOperators,+    DataKinds,+    PolyKinds,+    GADTs,+    TypeApplications,+    ConstraintKinds,+    FunctionalDependencies,+    ScopedTypeVariables++  build-depends:       base >= 4.9 && <= 4.12,+                       containers,+                       template-haskell,+                       mtl+  +  hs-source-dirs:      src+  +  default-language:    Haskell2010+  ++source-repository head+  type:     git+  location: https://github.com/VictorCMiraldo/generics-mrsop++source-repository this+  type:     git+  location: https://github.com/VictorCMiraldo/generics-mrsop+  tag:      1.0.0.0

@@ -0,0 +1,19 @@+{-# LANGUAGE RankNTypes           #-}+{-# LANGUAGE FlexibleContexts     #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE ScopedTypeVariables  #-}+-- | Re-exports everything from under @Generics.MRSOP.Base@+module Generics.MRSOP.Base (module Export) where++import Generics.MRSOP.Base.NS          as Export+import Generics.MRSOP.Base.NP          as Export+import Generics.MRSOP.Base.Universe    as Export+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+

@@ -0,0 +1,93 @@+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE FlexibleContexts        #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE GADTs                   #-}+{-# LANGUAGE TypeOperators           #-}+{-# LANGUAGE DataKinds               #-}+{-# LANGUAGE PolyKinds               #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# LANGUAGE TypeApplications        #-}+{-# LANGUAGE FunctionalDependencies  #-}+-- |Provides the main class of the library, 'Family'.+module Generics.MRSOP.Base.Class where++import Data.Function (on)++import Generics.MRSOP.Base.Universe+import Generics.MRSOP.Util++-- * Main Type Class ++-- |A Family consists of a list of types and a list of codes of the same length.+--  The idea is that the code of @Lkup n fam@ is @Lkup n code@.+--  We also parametrize on the interpretation of constants.+--  The class family provides primitives for performing a shallow conversion.+--  The 'deep' conversion is easy to obtain: @deep = map deep . shallow@+class Family (ki :: kon -> *) (fam :: [*]) (codes :: [[[Atom kon]]])+      | fam -> ki codes , ki codes -> fam+  where++    sfrom' :: SNat ix -> El fam ix -> Rep ki (El fam) (Lkup ix codes)+    sto'   :: SNat ix -> Rep ki (El fam) (Lkup ix codes) -> El fam ix++-- ** Shallow Conversion ++-- |A Smarter variant of 'sfrom'', since 'El' is a GADT,+--  we can extract the term-level rep of @ix@ from there.+sfrom :: forall fam ki codes ix+       . (Family ki fam codes)+      => El fam ix -> Rep ki (El fam) (Lkup ix codes)+sfrom el = sfrom' (getElSNat el) el++-- |For 'sto'' there is a similar more general combinator.+--  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  +sto = sto' (getSNat' @ix) ++-- ** Deep Conversion+--+-- $deepConversion+--+-- The deep translation is obtained by simply+-- recursing the shallow translation at every+-- point in the (generic) tree.+--+-- @dfrom = map dfrom . sfrom@++-- |Converts an entire element of our family+--  into +dfrom :: forall ix ki fam codes+       . (Family ki fam codes)+      => El fam ix+      -> Fix ki codes ix+dfrom = Fix . mapRep dfrom . sfrom @fam++-- |Converts an element back from a deep encoding.+--  This is the dual of 'dfrom'.+--+--  @dto = sto . map dto@+--+dto :: forall ix ki fam codes+     . (Family ki fam codes , IsNat ix)+    => Rep ki (Fix ki codes) (Lkup ix codes)+    -> El fam ix+dto = sto . mapRep (dto . unFix)++-- ** Smarter conversions into SOP++-- |Converts a type into its shallow representation.+shallow :: forall fam ty ki codes ix+         . (Family ki fam codes,+           ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix)+        => ty -> Rep ki (El fam) (Lkup ix codes)+shallow = sfrom . into++-- |Converts a type into its deep representation.+deep :: forall fam ty ki codes ix+      . (Family ki fam codes,+         ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix)+     => ty -> Fix ki codes ix+deep = dfrom . into

@@ -0,0 +1,96 @@+{-# LANGUAGE RankNTypes           #-}+{-# LANGUAGE FlexibleContexts     #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE TypeApplications     #-}+-- | A collection of combinators+--   for operating over sums of products.+module Generics.MRSOP.Base.Combinators where++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++-- * Equality+--+-- $equality+--+-- Compares two elements for equality.++-- |Given a way to compare the constant types+--  within two values, compare the outer values for+--  syntatical equality.+geq :: forall ki fam codes ix+     . (Family ki fam codes)+    => (forall k . ki k -> ki k -> Bool)+    -> El fam ix -> El fam ix -> Bool+geq kp = eqFix kp `on` dfrom ++-- * Compos+--+-- $compos+--+-- Applies a morphism everywhere in a structure.+--+-- Conceptually one can think of 'compos' as+-- having type @(b -> b) -> a -> a@. The semantics+-- is applying the morphism over @b@s wherever possible+-- inside a value of type @a@.+--+-- For our case, we need @a@ and @b@ to be elements of+-- the same family.++-- |Given a morphism for the @iy@ element of the family,+--  applies it everywhere in another element of+--  the family.+composM :: forall ki fam codes ix m+         . (Monad m , Family ki fam codes, IsNat ix)+        => (forall iy . IsNat iy => SNat iy -> El fam iy -> m (El fam iy))+        -> El fam ix -> m (El fam ix)+composM f = (sto @fam <$>)+          . mapRepM (\x -> f (getElSNat x) x)+          . sfrom @fam++-- |Non monadic version from above.+compos :: forall ki fam codes ix+        . (Family ki fam codes, IsNat ix)+       => (forall iy . IsNat iy => SNat iy -> El fam iy -> El fam iy)+       -> El fam ix -> El fam ix+compos f = runIdentity . composM (\iy -> return . f iy)++-- * Crush+--+-- $crush+--+-- Crush will collapse an entire value given only+-- an action to perform on the leaves and a way+-- of combining results.++-- | 'crushM' Applies its first parameter to all leaves,+--   combines the results with its second parameter.+crushM :: forall ki fam codes ix r m+        . (Monad m , Family ki fam codes)+       => (forall k. ki k -> m r) -> ([r] -> m r)+       -> El fam ix -> m r+crushM kstep combine+  = elimRep kstep (crushM kstep combine) (combine <.> sequence) . sfrom++-- | Non-monadic version+crush :: forall ki fam codes ix r+       . (Family ki fam codes)+      => (forall k. ki k -> r) -> ([r] -> r)+      -> El fam ix -> r+crush kstep combine = runIdentity . crushM (return . kstep) (return . combine)

@@ -0,0 +1,116 @@+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE StandaloneDeriving     #-}+-- |Metadata maintenance; usefull for pretty-printing values.+module Generics.MRSOP.Base.Metadata where++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++type ModuleName      = String+type FamilyName      = String+type ConstructorName = String+type FieldName       = String++-- |Since we only handled fully saturated datatypes, a 'DatatypeName'+--  needs to remember what were the arguments applied to a type.+--+--  The type @[Int]@ is represented by @Name "[]" :@@: Name "Int"@+--+infixl 5 :@:+data DatatypeName+  = Name String+  | DatatypeName :@: DatatypeName+  deriving (Eq , Show)++-- |Provides information about the declaration of a datatype.+data DatatypeInfo :: [[Atom kon]] -> * where+  ADT :: ModuleName -> DatatypeName -> NP ConstructorInfo c+      -> DatatypeInfo c+  New :: ModuleName -> DatatypeName -> ConstructorInfo '[ c ]+      -> DatatypeInfo '[ '[ c ]]++moduleName :: DatatypeInfo code -> ModuleName+moduleName (ADT m _ _) = m+moduleName (New m _ _) = m++datatypeName :: DatatypeInfo code -> DatatypeName+datatypeName (ADT _ d _) = d+datatypeName (New _ d _) = d++constructorInfo :: DatatypeInfo code -> NP ConstructorInfo code+constructorInfo (ADT _ _ c) = c+constructorInfo (New _ _ c) = c :* NP0++-- |Associativity information for infix constructors.+data Associativity+  = LeftAssociative+  | RightAssociative+  | NotAssociative+  deriving (Eq , Show)++-- |Fixity information for infix constructors.+type Fixity = Int++-- |Constructor metadata.+data ConstructorInfo :: [Atom kon] -> * where+  Constructor :: ConstructorName -> ConstructorInfo xs+  Infix       :: ConstructorName -> Associativity -> Fixity -> ConstructorInfo '[ x , y ]+  Record      :: ConstructorName -> NP FieldInfo xs -> ConstructorInfo xs++constructorName :: ConstructorInfo con -> ConstructorName+constructorName (Constructor c) = c+constructorName (Infix c _ _)   = c+constructorName (Record c _)    = c++-- |Record fields metadata+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 (ConstructorInfo code)+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'.+class (Family ki fam codes) => HasDatatypeInfo ki fam codes ix+    | fam -> codes ki where+  datatypeInfo :: (IsNat ix)+               => Proxy fam -> Proxy ix -> DatatypeInfo (Lkup ix codes)++-- |Sometimes it is more convenient to use a proxy of the type+--  in the family instead of indexes.+datatypeInfoFor :: forall ki fam codes ix ty+                 . ( HasDatatypeInfo ki fam codes ix+                   , ix ~ Idx ty fam , Lkup ix fam ~ ty , IsNat ix)+                => Proxy fam -> Proxy ty -> DatatypeInfo (Lkup ix codes)+datatypeInfoFor pf pty = datatypeInfo pf (proxyIdx pf pty)+  where+    proxyIdx :: Proxy fam -> Proxy ty -> Proxy (Idx ty fam)+    proxyIdx _ _ = Proxy++-- ** Name Lookup++-- |This is essentially a list lookup, but needs significant type+--  information to go through. Returns the name of the @c@th constructor+--  of a sum-type.+constrInfoLkup :: Constr sum c -> DatatypeInfo sum -> ConstructorInfo (Lkup c sum)+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++

@@ -0,0 +1,78 @@+{-# LANGUAGE RankNTypes        #-}+{-# LANGUAGE FlexibleContexts  #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs             #-}+{-# LANGUAGE TypeOperators     #-}+{-# LANGUAGE DataKinds         #-}+{-# LANGUAGE PolyKinds         #-}+-- | Standard representation of n-ary products.+module Generics.MRSOP.Base.NP where++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)++-- * 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 (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++-- * Map, Elim and Zip++-- |Maps a natural transformation over a n-ary product+mapNP :: f :-> g -> NP f ks -> NP g ks+mapNP f 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 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 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 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 (f :* fs) (g :* gs) = (f :*: g) :* zipNP fs gs++-- * Catamorphism++-- |Consumes a value of type 'NP'.+cataNP :: (forall x xs . f x  -> r xs -> r (x : xs))+       -> r '[]+       -> NP f xs -> r xs+cataNP fCons fNil NP0       = fNil+cataNP fCons fNil (k :* ks) = fCons k (cataNP fCons fNil ks)++-- * Equality++-- |Compares two 'NP's pairwise with the provided function and+--  return the conjunction of the results.+eqNP :: (forall x. p x -> p x -> Bool)+     -> NP p xs -> NP p xs -> Bool+eqNP p x = and . elimNP (uncurry' p) . zipNP x+

@@ -0,0 +1,63 @@+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE FlexibleInstances   #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE PolyKinds           #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- | Standard representation of n-ary sums.+module Generics.MRSOP.Base.NS where++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)++-- * Map, Zip and Elim++-- |Maps over a sum+mapNS :: f :-> g -> NS f ks -> NS g ks+mapNS f (Here  p) = Here (f p)+mapNS f (There p) = There (mapNS f p)++-- |Maps a monadic function over a sum+mapNSM :: (Monad m) => (forall x . f x -> m (g x)) -> NS f ks -> m (NS g ks)+mapNSM f (Here  p) = Here  <$> f p+mapNSM f (There p) = There <$> mapNSM f p++-- |Eliminates a sum+elimNS :: (forall x . f x -> a) -> NS f ks -> a+elimNS f (Here p)  = f p+elimNS f (There p) = elimNS f p++-- |Combines two sums. Note that we have to fail if they are+--  constructed from different injections.+zipNS :: (MonadPlus m) => NS ki xs -> NS kj xs -> m (NS (ki :*: kj) xs)+zipNS (Here  p) (Here  q) = return (Here (p :*: q))+zipNS (There p) (There q) = There <$> zipNS p q+zipNS _         _         = mzero++-- * 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)++-- * Equality++-- |Compares two values of type 'NS' using the provided function+--  in case they are made of the same injection.+eqNS :: (forall x. p x -> p x -> Bool)+     -> NS p xs -> NS p xs -> Bool+eqNS p x = maybe False (elimNS $ uncurry' p) . zipNS x+

@@ -0,0 +1,50 @@+{-# 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) = show x++instance Show (NS (PoA ki (Fix ki codes)) (Lkup ix codes))+      => Show (Fix ki codes ix)+    where+  show (Fix x) = show x

@@ -0,0 +1,264 @@+{-# LANGUAGE RankNTypes           #-}+{-# LANGUAGE FlexibleContexts     #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE TypeApplications     #-}+-- |Wraps the definitions of 'NP' and 'NS'+--  into Representations ('Rep'), essentially providing+--  the universe view over sums-of-products.+module Generics.MRSOP.Base.Universe where++import Data.Function (on)+import Data.Type.Equality+import Data.Proxy++import Control.Monad++import Generics.MRSOP.Base.NS+import Generics.MRSOP.Base.NP+import Generics.MRSOP.Util++-- * Universe of Codes+--+-- $universeOfCodes+--+-- We will use nested lists to represent the Sums-of-Products+-- structure. The atoms, however, will be parametrized by a kind+-- used to index what are the types that are opaque to the library.+--++-- |Atoms can be either opaque types, @kon@, or+--  type variables, @Nat@.+data Atom kon+  = K kon+  | I Nat+  deriving (Eq, Show)++-- |@NA ki phi a@ provides an interpretation for an atom @a@,+--  using either @ki@ or @phi@ to interpret the type variable+--  or opaque type.+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)++-- ** Map, Elim and Zip++-- |Maps a natural transformation over an atom interpretation+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)++-- |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++-- |Eliminates an atom interpretation+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++-- |Combines two atoms into one+zipNA :: NA ki f a -> NA kj g a -> NA (ki :*: kj) (f :*: g) a+zipNA (NA_I fk) (NA_I gk) = NA_I (fk :*: gk)+zipNA (NA_K ki) (NA_K kj) = NA_K (ki :*: kj)++-- |Compares atoms provided we know how to compare+--  the leaves, both recursive and constant.+eqNA :: (forall k  . ki  k  -> ki  k  -> Bool)+     -> (forall ix . fam ix -> fam ix -> Bool)+     -> NA ki fam l -> NA ki fam l -> Bool+eqNA kp fp x = elimNA (uncurry' kp) (uncurry' fp) . zipNA x++-- * Representation of Codes+--+-- $representationOfCodes+--+-- Codes are represented using the 'Rep' newtype,+-- which wraps an n-ary sum of n-ary products. Note it receives two+-- functors: @ki@ and @phi@, to interpret opaque types and type variables+-- respectively.++-- |Representation of codes.+newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]])+  = Rep { unRep :: NS (PoA ki phi) code }++-- |Product of Atoms is a handy synonym to have.+type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)++-- ** Map, Elim and Zip+--+-- $mapElimAndZip+--+-- Just like for 'NS', 'NP' and 'NA', we provide+-- a couple convenient functions working over+-- a 'Rep'. These are just the cannonical combination+-- of their homonym versions in 'NS', 'NP' or 'NA'.++-- |Maps over a representation.+mapRep :: (forall ix . IsNat ix => f  ix -> g ix)+       -> Rep ki f c -> Rep ki g c+mapRep = bimapRep id++-- |Maps a monadic function over a representation.+mapRepM :: (Monad m)+        => (forall ix . IsNat ix => f  ix -> m (g  ix))+        -> Rep ki f c -> m (Rep ki g c)+mapRepM = bimapRepM return++-- |Maps over both indexes of a representation.+bimapRep :: (forall k  .             ki k  -> kj k)+         -> (forall ix . IsNat ix => f  ix -> g ix)+         -> Rep ki f c -> Rep kj g c+bimapRep fk fi = Rep . mapNS (mapNP (mapNA fk fi)) . unRep++-- |Monadic version of 'bimapRep'+bimapRepM :: (Monad m)+          => (forall k  .             ki k  -> m (kj k))+          -> (forall ix . IsNat ix => f  ix -> m (g  ix))+          -> Rep ki f c -> m (Rep kj g c)+bimapRepM fk fi = (Rep <$>) . mapNSM (mapNPM (mapNAM fk fi)) . unRep++-- |Zip two representations together, in case they are made with the same+--  constructor.+--+--  > zipRep (Here (NA_I x :* NP0)) (Here (NA_I y :* NP0))+--  >   = return $ Here (NA_I (x :*: y) :* NP0)+--+--  > zipRep (Here (NA_I x :* NP0)) (There (Here ...))+--  >   = mzero+--+zipRep :: (MonadPlus m)+       => Rep ki f c -> Rep kj g c+       -> m (Rep (ki :*: kj) (f :*: g) c)+zipRep (Rep t) (Rep u)+  = Rep . mapNS (mapNP (uncurry' zipNA) . uncurry' zipNP) <$> zipNS t u++-- |Monadic eliminator; This is just the cannonical combination of+--  'elimNS', 'elimNPM' and 'elimNA'.+elimRepM :: (Monad m)+         => (forall k . ki k -> m a)+         -> (forall k . IsNat k => f  k -> m a)+         -> ([a] -> m b)+         -> Rep ki f c -> m b+elimRepM fk fi cat+  = cat <.> elimNS (elimNPM (elimNA fk fi)) . unRep++-- |Pure eliminator.+elimRep :: (forall k . ki k -> a)+        -> (forall k . f  k -> a)+        -> ([a] -> b)+        -> Rep ki f c -> b+elimRep kp fp cat+  = elimNS (cat . elimNP (elimNA kp fp)) . unRep++-- |Compares two 'Rep' for equality; again, cannonical combination+--  of 'eqNS', 'eqNP' and 'eqNA'+eqRep :: (forall k  . ki  k  -> ki  k  -> Bool)+      -> (forall ix . fam ix -> fam ix -> Bool)+      -> Rep ki fam c -> Rep ki fam c -> Bool+eqRep kp fp t = maybe False (elimRep (uncurry' kp) (uncurry' fp) and)+              . zipRep t ++-- * SOP functionality+--+-- $sopFunctionality+--+-- It is often more convenient to view a value of 'Rep'+-- as a constructor and its fields, instead of having to+-- traverse the inner 'NS' structure.++-- |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++instance TestEquality (Constr codes) where+  testEquality CZ     CZ     = Just Refl+  testEquality (CS x) (CS y) = apply (Refl :: S :~: S) <$> testEquality x y+  testEquality _      _      = Nothing++instance (IsNat n) => Show (Constr xs n) where+  show _ = "C" ++ show (getNat (Proxy :: Proxy n))++-- |We can define injections into an n-ary sum from+--  its 'Constr'uctors+injNS :: Constr sum n -> PoA ki fam (Lkup n sum) -> NS (NP (NA ki fam)) sum+injNS CZ     poa = Here poa+injNS (CS c) poa = There (injNS c poa)++-- |Wrap it in a 'Rep' for convenience.+inj :: Constr sum n -> PoA ki fam (Lkup n sum) -> Rep ki fam sum+inj c = Rep . injNS c++-- | Inverse of 'injNS'.  Given some Constructor, see if Rep is of this constructor+matchNS :: Constr sum c -> NS (NP (NA ki fam)) sum -> Maybe (PoA ki fam (Lkup c sum))+matchNS CZ (Here ps) = Just ps+matchNS (CS c) (There x) = matchNS c x+matchNS _ _ = Nothing++-- | Inverse of 'inj'. Given some Constructor, see if Rep is of this constructor+match :: Constr sum c -> Rep ki fam sum -> Maybe (PoA ki fam (Lkup c sum))+match c (Rep x) = matchNS c x++-- |Finally, we can view a sum-of-products as a constructor+--  and a product-of-atoms.+data View :: (kon -> *) -> (Nat -> *) -> [[ Atom kon ]] -> * where+  Tag :: Constr sum n -> PoA ki fam (Lkup n sum) -> View ki fam sum++-- |Unwraps a 'Rep' into a 'View'+sop :: Rep ki fam sum -> View ki fam sum+sop = go . unRep+  where+    go :: NS (NP (NA ki fam)) sum -> View ki fam sum+    go (Here  poa) = Tag CZ poa+    go (There s)   = case go s of+                        Tag c poa -> Tag (CS c) poa++-- * Least Fixpoints+--+-- $leastFixpoints+--+-- 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+-- 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) }++-- |Retrieves the index of a 'Fix'+proxyFixIdx :: Fix ki fam ix -> Proxy ix+proxyFixIdx _ = Proxy++-- |Maps over the values of opaque types within the+--  fixpoint.+mapFixM :: (Monad m)+        => (forall k . ki k -> m (kj k))+        -> Fix ki fam ix -> m (Fix kj fam ix)+mapFixM fk = (Fix <$>) . bimapRepM fk (mapFixM fk) . unFix++-- |Compare two values of a same fixpoint for equality.+eqFix :: (forall k. ki k -> ki k -> Bool)+      -> Fix ki fam ix -> Fix ki fam ix -> Bool+eqFix p = eqRep p (eqFix p) `on` unFix++-- |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)

@@ -0,0 +1,132 @@+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE TypeSynonymInstances  #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE TemplateHaskell       #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE PatternSynonyms       #-}+-- 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+import Generics.MRSOP.Base+import Generics.MRSOP.Opaque+import Generics.MRSOP.TH++-- |Standard Lambda Calculus.+data Term = Var String+          | Abs String Term+          | App Term Term+++deriveFamily [t| Term |]++-- * The alpha-eq monad+--+-- $alphaeqmonad+--+-- We will use an abstract monad for keeping track of scopes and name equivalences+--++-- |Interface needed for deciding alpha equivalence.+class Monad m => MonadAlphaEq m where+  -- |Runs a computation under a new scope.+  onNewScope   :: m a -> m a++  -- |Registers a name equivalence under the current scope.+  addRule      :: String -> String -> m ()+  +  -- |Checks for a name equivalence under all scopes.+  (=~=)        :: String -> String -> m Bool++onHead :: (a -> a) -> [a] -> [a]+onHead f (x : xs) = f x : xs+onHead f []       = []++-- |Given a list of scopes, which consist in a list of pairs each, checks+--  whether or not two names are equivalent.+onScope :: String -> String -> [[(String , String)]] -> Bool+onScope v1 v2 [] = v1 == v2+onScope v1 v2 (s:ss)+  = case filter (\(x1 , x2) -> x1 == v1 || x2 == v2) s of+      []          -> onScope v1 v2 ss+      [(x1 , x2)] -> x1 == v1 && x2 == v2+      _           -> False++-- |One of the simplest monads that implement 'MonadAlphaEq'+instance MonadAlphaEq (State [[(String, String)]]) where+  onNewScope s+    = modify ([]:) >> s <* modify tail++  addRule v1 v2+    = modify (onHead ((v1 , v2):))++  v1 =~= v2+    = get >>= return . onScope v1 v2++-- |Runs a computation.+runAlpha :: State [[(String , String)]] a -> a+runAlpha = flip evalState [[]]++-- * Alpha equivalence for Lambda terms++type FIX = Fix Singl CodesTerm++pattern Term_    = SZ+pattern Var_ s   = Tag CZ (NA_K s :* NP0)+pattern Abs_ x t = Tag (CS CZ) (NA_K x :* NA_I t :* NP0)++-- |Decides whether or not two terms are alpha equivalent.+alphaEq :: Term -> Term -> Bool+alphaEq x y = runAlpha $ galphaEqT (deep @FamTerm x) (deep @FamTerm y)+  where+    galphaEqT :: forall ix m . (MonadAlphaEq m , IsNat ix)+              => FIX ix -> FIX ix+              -> m Bool+    galphaEqT x y = galphaEq (getSNat' @ix) x y++    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)++    step :: forall m c . (MonadAlphaEq m)+         => Rep (Singl :*: Singl) (FIX :*: FIX) c -> m Bool+    step = elimRepM (return . uncurry' eqSingl)+                    (uncurry' galphaEqT)+                    (return . and)++    go :: forall ix m . (MonadAlphaEq m)+       => SNat ix -> Rep (Singl :*: Singl) (FIX :*: FIX)+                         (Lkup ix CodesTerm)+       -> m Bool+    go Term_ x = case sop x of+      -- Without -XPolyKinds this is impossible; weird errors all over the place.+      Var_ (SString v1 :*: SString v2)+        -> v1 =~= v2+      Abs_ (SString v1 :*: SString v2) (t1 :*: t2)+        -> onNewScope (addRule v1 v2 >> galphaEq Term_ t1 t2)+      _ -> step x++-- * Tests+--+-- Arguments of type 'String' will be bound+-- by an abstraction, arguments of type 'Char'+-- will be unbound variables.++t1 :: String -> String -> Term+t1 x y = Abs x (Abs y (App (Var x) (Var y)))++t2 :: String -> String -> String -> Char -> Term+t2 a b c d+  = Abs a (App (Abs b (App (Var b) (Var [d]))) (Abs c (App (Var c) (Var [d]))))

@@ -0,0 +1,101 @@+{-# LANGUAGE TypeApplications        #-}+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE FlexibleContexts        #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE GADTs                   #-}+{-# LANGUAGE TypeOperators           #-}+{-# LANGUAGE DataKinds               #-}+{-# LANGUAGE PolyKinds               #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# LANGUAGE FunctionalDependencies  #-}+{-# LANGUAGE PatternSynonyms         #-}+-- |This module is analogous to 'Generics.MRSOP.Examples.RoseTreeTH',+--  but we use no Template Haskell here.+module Generics.MRSOP.Examples.RoseTree where++import Data.Function (on)++import Generics.MRSOP.Base+import Generics.MRSOP.Opaque+import Generics.MRSOP.Util++-- * Standard Rose-Tree datatype++data R a = a :>: [R a]+         | Leaf a+         deriving Show++value1, value2 :: 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 CodesRose = '[ListCode , RTCode]+type FamRose   = '[ [R Int] , R Int] ++-- ** Instance Decl++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))++  sto' SZ (Rep (Here NP0))+    = El []+  sto' SZ (Rep (There (Here (NA_I (El x) :* NA_I (El xs) :* NP0))))+    = El (x : xs)+  sto' (SS SZ) (Rep (Here (NA_K (SInt a) :* NA_I (El as) :* NP0)))+    = El (a :>: as)+  sto' (SS SZ) (Rep (There (Here (NA_K (SInt a) :* NP0))))+    = El (Leaf a)++instance HasDatatypeInfo Singl FamRose CodesRose Z where+  datatypeInfo _ _+    = ADT "module" (Name "[]" :@: (Name "R" :@: Name "Int"))+      $  (Constructor "[]")+      :* (Infix ":" RightAssociative 5)+      :* NP0++instance HasDatatypeInfo Singl FamRose CodesRose (S Z) where+  datatypeInfo _ _+    = ADT "module" (Name "R" :@: Name "Int")+      $  (Infix ":>:" NotAssociative 0)+      :* (Constructor "Leaf")+      :* NP0++-- * Eq Instance++instance Eq (R Int) where+  (==) = geq eqSingl `on` (into @FamRose)++testEq :: Bool+testEq = value1 == value1+      && value2 /= value1++-- * Compos test++pattern RInt_ = SS SZ++normalize :: R Int -> R Int+normalize = unEl . go (SS SZ) . into+  where+    go :: forall iy. (IsNat iy) => SNat iy -> El FamRose iy -> El FamRose iy+    go RInt_ (El (Leaf a)) = El (a :>: [])+    go _       x           = compos go x++-- * Crush test++sumTree :: R Int -> Int+sumTree = crush k sum . (into @FamRose)+  where k :: Singl x -> Int+        k (SInt n) = n++testSum :: Bool+testSum = sumTree value3 == sumTree (normalize value3)

@@ -0,0 +1,89 @@+{-# LANGUAGE TypeApplications        #-}+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE FlexibleContexts        #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE GADTs                   #-}+{-# LANGUAGE TypeOperators           #-}+{-# LANGUAGE DataKinds               #-}+{-# LANGUAGE PolyKinds               #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# LANGUAGE FunctionalDependencies  #-}+{-# LANGUAGE TemplateHaskell         #-}+{-# LANGUAGE LambdaCase              #-}+{-# LANGUAGE PatternSynonyms         #-}+-- |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+--+-- $definingthedatatype+--+-- First, we will start off defining a variant of your standard Rose trees.+-- The 'Leaf' constructor adds some redundancy on purpose, so we can+-- later use the combinators in the library to remove that redundancy.++-- |Rose trees with redundancy.+data Rose a = a :>: [Rose a]+            | Leaf a+  deriving Show++-- |Sample values.+value1, value2, value3 :: Rose Int+value1 = 1 :>: [2 :>: [], 3 :>: []]+value2 = 1 :>: [2 :>: []]+value3 = 3 :>: [Leaf 23 , value1 , value2]++value4 :: Rose Int+value4 = 12 :>: [value3 , value3 , value2]++deriveFamily [t| Rose Int |]++-- * Eq Instance++-- |Equality is defined using 'geq'+instance Eq (Rose Int) where+  (==) = geq eqSingl `on` (into @FamRoseInt)++-- |Equality test; should return 'True'!+testEq :: Bool+testEq = value1 == value1+      && value2 /= value1++-- * Compos test++-- |This function removes the redundant 'Leaf' constructor+--  by the means of a 'compos'. Check the source for details.+normalize :: Rose Int -> Rose Int+normalize = unEl . go SZ . into+  where+    go :: forall iy. (IsNat iy)+       => SNat iy -> El FamRoseInt iy -> El FamRoseInt iy+    go SZ (El (Leaf a)) = El (a :>: [])+    go _  x             = compos go x++-- * Crush test++-- |Sums up the values in a rose tree using a 'crush'+sumTree :: Rose Int -> Int+sumTree = crush k sum . (into @FamRoseInt)+  where k :: Singl x -> Int+        k (SInt n) = n++-- |The sum of a tree should be the same as the sum of a normalized tree;+--  This should return 'True'.+testSum :: Bool+testSum = sumTree value3 == sumTree (normalize value3)

@@ -0,0 +1,206 @@+{-# LANGUAGE TypeApplications        #-}+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE FlexibleContexts        #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE GADTs                   #-}+{-# LANGUAGE TypeOperators           #-}+{-# LANGUAGE DataKinds               #-}+{-# LANGUAGE PolyKinds               #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# LANGUAGE FunctionalDependencies  #-}+{-# LANGUAGE TemplateHaskell         #-}+{-# LANGUAGE LambdaCase              #-}+{-# LANGUAGE PatternSynonyms         #-}+-- |Uses a more involved example to test some+--  of the functionalities of @generics-mrsop@.+module Generics.MRSOP.Examples.SimpTH where++import Data.Function (on)++import Generics.MRSOP.Base+import Generics.MRSOP.Opaque+import Generics.MRSOP.Util+import Generics.MRSOP.Zipper++import Generics.MRSOP.Examples.LambdaAlphaEqTH hiding (FIX, alphaEq)++import Generics.MRSOP.TH++import Control.Monad+import Control.Monad.State++-- * Simple IMPerative Language:++data Stmt var+  = SAssign var (Exp var)+  | SIf     (Exp var) (Stmt var) (Stmt var)+  | SSeq    (Stmt var) (Stmt var)+  | SReturn (Exp var)+  | SDecl (Decl var)+  | SSkip+  deriving Show++data Decl var+  = DVar var+  | DFun var var (Stmt var)+  deriving Show++data Exp var+  = EVar  var+  | ECall var (Exp var)+  | EAdd (Exp var) (Exp var)+  | ESub (Exp var) (Exp var)+  | ELit Int+  deriving Show++deriveFamily [t| Stmt String |]++pattern Decl_ = SS (SS SZ)+pattern Exp_  = SS SZ+pattern Stmt_ = SZ++pattern SAssign_ v e = Tag CZ (NA_K v :* NA_I e :* NP0)++pattern DVar_ v     = Tag CZ (NA_K v :* NP0)+pattern DFun_ f x s = Tag (CS CZ) (NA_K f :* NA_K x :* NA_I s :* NP0)++pattern EVar_ v    = Tag CZ      (NA_K v :* NP0)+pattern ECall_ f x = Tag (CS CZ) (NA_K f :* NA_I x :* NP0)++type FIX = Fix Singl CodesStmtString++-- * Alpha Equality Functionality++alphaEqD :: Decl String -> Decl String -> Bool+alphaEqD = (galphaEq Decl_) `on` (deep @FamStmtString)+  where+    -- Generic programming boilerplate;+    -- could be removed. WE are just passing SNat+    -- and Proxies around.+    galphaEq :: forall iy . (IsNat iy)+             => SNat iy -> FIX iy -> FIX iy -> Bool+    galphaEq iy x y = runAlpha (galphaEq' iy x y) ++    galphaEqT :: forall iy m . (MonadAlphaEq m , IsNat iy)+              => FIX iy -> FIX iy -> m Bool+    galphaEqT x y = galphaEq' (getSNat' @iy) x y+    +    galphaEq' :: forall iy m . (MonadAlphaEq m , IsNat iy)+              => SNat iy -> FIX iy -> FIX iy -> m Bool+    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.+    step :: forall m c . (MonadAlphaEq m)+         => Rep (Singl :*: Singl) (FIX :*: FIX) c+         -> m Bool+    step = elimRepM (return . uncurry' eqSingl)+                    (uncurry' galphaEqT)+                    (return . and)++    -- The actual important 'patterns'; everything+    -- else is done by 'step'.+    go :: forall iy m . (MonadAlphaEq m)+       => SNat iy+       -> Rep (Singl :*: Singl) (FIX :*: FIX)+              (Lkup iy CodesStmtString)+       -> m Bool+    go Stmt_ x+      = case sop x of+          SAssign_ (SString v1 :*: SString v2) e1e2+            -> addRule v1 v2 >> uncurry' (galphaEq' Exp_) e1e2+          otherwise+            -> step x+    go Decl_ x+      = case sop x of+          DVar_ (SString v1 :*: SString v2)+            -> addRule v1 v2 >> return True+          DFun_ (SString f1 :*: SString f2) (SString x1 :*: SString x2) s+            -> addRule f1 f2 >> onNewScope (addRule x1 x2 >> uncurry' galphaEqT s)+          _ -> step x+    go Exp_ x+      = case sop x of+          EVar_ (SString v1 :*: SString v2)+            -> v1 =~= v2+          ECall_ (SString f1 :*: SString f2) e+            -> (&&) <$> (f1 =~= f2) <*> uncurry' galphaEqT e+          _ -> step x +    go _ x = step x+++{- EXAMPLE++decl fib(n):+  aux = fib(n-1) + fib(n-2);+  return aux;++is alpha eq to++decl fib(x):+  r = fib(x-1) + fib(x-2);+  return r;+-}++test1 :: String -> String -> String -> Decl String+test1 fib n aux = DFun fib n+      $ (SAssign aux (EAdd (ECall fib (ESub (EVar n) (ELit 1)))+                             (ECall fib (ESub (EVar n) (ELit 2)))))+      `SSeq` (SReturn (EVar aux))++test2 :: String -> String -> String -> Decl String+test2 fib n aux = DFun fib n+      $ (SAssign aux (EAdd (ECall fib (ESub (EVar n) (ELit 2)))+                           (ECall fib (ESub (EVar n) (ELit 1)))))+      `SSeq` (SReturn (EVar aux))++{- EXAMPLE++decl f(n):+  decl g(n):+    z = n + 1+    return z+  return g(n)++-}++test3 :: String -> String -> String -> Decl String+test3 n1 n2 z = DFun "f" n1+              $ SDecl (DFun "g" n2+                      $ SAssign z (EAdd (EVar n2) (ELit 1))+                      `SSeq` (SReturn $ EVar z))+         `SSeq` (SReturn $ ECall "g" (EVar n1))+++-- ** Zipper test++infixr 4 >>>+(>>>) :: (a -> b) -> (b -> c) -> a -> c+(>>>) = flip (.)++test4 :: Int -> Decl String+test4 n = DFun "test" "n"+        $ (SAssign "x" (EAdd (ELit 10) (ELit n)))+        `SSeq` (SReturn (EVar "x"))+        ++test5 :: Maybe (Decl String)+test5 = enter+    >>> down+    >=> down+    >=> down+    >=> down+    >=> right+    >=> update mk42+    >>> leave+    >>> return . unEl+      $ into @FamStmtString (test4 10)+  where+    mk42 :: SNat ix -> El FamStmtString ix -> El FamStmtString ix+    mk42 Exp_ _ = El $ ELit 42+    mk42 _    x = x+

@@ -0,0 +1,66 @@+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE RankNTypes           #-}+{-# LANGUAGE FlexibleContexts     #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE StandaloneDeriving   #-}+-- | A curation of base types commonly used+--   by the everyday Haskell programmer.+module Generics.MRSOP.Opaque where++import Data.Function (on)+import Data.Proxy++import Generics.MRSOP.Util++-- * Opaque Types+--+-- $opaquetypes+--+-- In order to plug in custom opaque types, the programmer+-- must provide their own 'Kon' and 'Singl'. This module serves+-- more as an example.++-- | Types with kind 'Kon' will be used to+--   index a 'Singl' type with their values inside.+data Kon+  = KInt+  | KInteger+  | KFloat+  | KDouble+  | KBool+  | KChar+  | KString+  deriving (Eq , Show)++-- Vim macro to easily generate: nlywea :: pa -> Singl Kp+-- needs a /S before hand, though.++-- |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++deriving instance Show (Singl k)+deriving instance Eq   (Singl k)++instance Eq1 Singl where+  eq1 = (==)++instance Show1 Singl where+  show1 = show++-- |Equality over singletons+eqSingl :: Singl k -> Singl k -> Bool+eqSingl = (==)+

@@ -0,0 +1,795 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TupleSections     #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE DeriveFunctor     #-}+{-# LANGUAGE TemplateHaskell   #-}+{-# OPTIONS_GHC -cpp           #-}+-- | Provides a simple way for the end-user deriving+--   the mechanical, yet long, Element instances+--   for a family.+--+--   We are borrowing a some code from generic-sop+--   ( https://hackage.haskell.org/package/generics-sop-0.3.2.0/docs/src/Generics-SOP-TH.html )+--+module Generics.MRSOP.TH (deriveFamily, genFamilyDebug) where++import Data.Function (on)+import Data.Char (ord , isAlphaNum)+import Data.List (sortBy, foldl')++import Control.Monad+import Control.Monad.State+import Control.Monad.Writer+import Control.Monad.Identity++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+import Generics.MRSOP.Base.Universe hiding (match)+import qualified Generics.MRSOP.Base.Metadata as Meta++import qualified Data.Map as M++-- |Given the name of the first element in the family,+--  derives:+--+--    1. The other types in the family and Konstant types one needs.+--    2. the SOP code for each of the datatypes involved+--    3. One 'Element' instance per datatype+--    TODO: 4. Metadada information for each of the datatypes involved+deriveFamily :: Q Type -> Q [Dec]+deriveFamily t+  = do sty              <- t >>= convertType +       (_ , (Idxs _ m)) <- runIdxsM (reifySTy sty)+       -- Now we make sure we have processed all+       -- types+       m' <- mapM extractDTI (M.toList m)+       let final = sortBy (compare `on` second) m' +       dbg <- genFamilyDebug sty final+       res <- genFamily sty final +       return (dbg ++ res)+  where+    second (_ , x , _) = x+    +    extractDTI (sty , (ix , Nothing))+      = fail $ "Type " ++ show sty ++ " has no datatype information."+    extractDTI (sty , (ix , Just dti))+      = return (sty , ix , dti)++-- Sketch;+--+--   Given a module:+--+--    > module Test where+--    > data Rose a = Fork a [Rose a]+--    > $(deriveFamily [t| Rose Int |])+--+--  We will see we are looking into deriving a family+--  for an AppT (ConT Rose) (ConT Int).+--+--  Working with a (M.Map STy (Int , DInfo (K + I))) in a state;+--+--  0) Translate to a simpler Type-expression, call it STy.+--  1) Register (AppST (ConST Rose) (ConST Int)) as family index Z+--  2) reify lhs: [d| data Rose a = Fork a [Rose a] |]+--      a) reduce rhs of (1): (\a -> Fork a [Rose a]) @ (ConT Int)+--                        == Fork Int [Rose Int]+--      b) Take the fields that require processing: [ConT Int , AppST List (AppST Rose Int)]+--      c) Somehow figure out that (ConT Int) is a Konstant.+--      d) Look into (AppST List (AppST Rose Int))+--      e) Is it already processed?+--      f) If yes, we are done.+--  3) Register (AppST List (AppST Rose Int))as family index (S Z)+--  4) reify lhs: [d| data List a = Nil | Cons a (List a) |]+--      a) reduce rhs of (4): (\a -> Nil | Cons a (List a)) @ (AppST Rose Int)+--      b) Take the fields of each constructor:+--           [] , [AppST Rose Int , AppST List (AppST Rose Int)]+--      c) Notice that both fields of 'Cons' have already+--         been registered; hence they become: [I Z , I (S Z)]+--++-- * Data Structures++type DataName  = Name+type ConName   = Name+type FieldName = Name+type Args      = [Name]++-- |Datatype information, parametrized by the type of Type-expressions+--  that appear on the fields of the constructors.+data DTI ty+  = ADT DataName Args [ CI ty ]+  | New DataName Args (CI ty)+  deriving (Eq , Show , Functor)++-- |Constructor information+data CI ty+  = Normal ConName [ty]+  | Infix  ConName Fixity ty ty+  | Record ConName [ (FieldName , ty) ]+  deriving (Eq , Show , Functor)++-- ** Monadic Maps++ciMapM :: (Monad m) => (ty -> m tw) -> CI ty -> m (CI tw)+ciMapM f (Normal name tys)  = Normal name  <$> mapM f tys+ciMapM f (Infix name x l r) = Infix name x <$> f l <*> f r+ciMapM f (Record name tys)  = Record name  <$> mapM (rstr . (id *** f)) tys+  where+    rstr (a , b) = b >>= return . (a,)++dtiMapM :: (Monad m) => (ty -> m tw) -> DTI ty -> m (DTI tw)+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++dti2ci :: DTI ty -> [CI ty]+dti2ci (ADT _ _ cis) = cis+dti2ci (New _ _ ci)  = [ ci ]++ci2ty :: CI ty -> [ty]+ci2ty (Normal _ tys)  = tys+ci2ty (Infix _ _ a b) = [a , b]+ci2ty (Record _ tys)  = map snd tys++ciName :: CI ty -> Name+ciName (Normal n _)    = n+ciName (Infix n _ _ _) = n+ciName (Record n _)    = n++ci2Pat :: CI ty -> Q ([Name] , Pat)+ci2Pat ci+  = do ns <- mapM (const (newName "x")) (ci2ty ci)+       return (ns , (ConP (ciName ci) (map VarP ns)))++ci2Exp :: CI ty -> Q ([Name], Exp)+ci2Exp ci+  = do ns <- mapM (const (newName "y")) (ci2ty ci)+       return (ns , foldl (\e n -> AppE e (VarE n)) (ConE (ciName ci)) ns)++-- * Simpler STy Language++-- A Simplified version of Language.Haskell.TH+data STy+  = AppST STy STy+  | VarST Name+  | ConST Name+  deriving (Eq , Show, Ord)++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++-- |Does a STy have a varible name?+isClosed :: STy -> Bool+isClosed = styFold (&&) (const False) (const True)++-- ** Back and Forth conversion++convertType :: (Monad m) => Type -> m STy+convertType (AppT a b)  = AppST <$> convertType a <*> convertType b+convertType (SigT t _)  = convertType t+convertType (VarT n)    = return (VarST n)+convertType (ConT n)    = return (ConST n)+convertType (ParensT t) = convertType t+convertType ListT       = return (ConST (mkName "[]"))+convertType (TupleT n)  = return (ConST (mkName $ '(':replicate (n-1) ',' ++ ")"))+convertType t           = fail ("convertType: Unsupported Type: " ++ show t)++trevnocType :: STy -> Type+trevnocType (AppST a b) = AppT (trevnocType a) (trevnocType b)+trevnocType (VarST n)   = VarT n+trevnocType (ConST n)+  | n == mkName "[]" = ListT+  | isTupleN n       = TupleT $ length (show n) - 1+  | otherwise        = ConT n+  where isTupleN n = take 2 (show n) == "(,"++-- |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 (VarST x)   m n+  | x == m    = n+  | otherwise = VarST x++-- |Just like subst, but applies a list of substitutions+styReduce :: [(Name , STy)] -> STy -> STy+styReduce parms t = foldr (\(n , m) ty -> stySubst ty n m) t parms++-- |Flattens an application into a list of arguments;+--+--  @styFlatten (AppST (AppST Tree A) B) == (Tree , [A , B])@+styFlatten :: STy -> (STy , [STy])+styFlatten (AppST a b) = id *** (++ [b]) $ styFlatten a+styFlatten sty         = (sty , [])++-- * Parsing Haskell's AST++reifyDec :: Name -> Q Dec+reifyDec name =+  do info <- reify name+     case info of TyConI dec -> return dec+                  _          -> fail $ show name ++ " is not a declaration"++argInfo :: TyVarBndr -> Name+argInfo (PlainTV  n)   = n+argInfo (KindedTV n _) = n++-- Extracts a DTI from a Dec+decInfo :: Dec -> Q (DTI STy)+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"++-- Extracts a CI from a Con+conInfo :: Con -> Q (CI STy)+conInfo (NormalC  name ty) = Normal name <$> mapM (convertType . snd) ty+conInfo (RecC     name ty) = Record name <$> mapM (\(s , _ , t) -> (s,) <$> convertType t) ty+conInfo (InfixC l name r)+  = do info <- reifyFixity name+       let fixity = maybe defaultFixity id $ info+       Infix name fixity <$> convertType (snd l) <*> convertType (snd r)+conInfo (ForallC _ _ _) = fail "Existentials not supported"+#if MIN_VERSION_template_haskell(2,11,0)+conInfo (GadtC _ _ _)    = fail "GADTs not supported"+conInfo (RecGadtC _ _ _) = fail "GADTs not supported"+#endif++-- |Reduces the rhs of a datatype declaration+--  with some provided arguments. Step (2.a) of our sketch.+--+--  Precondition: application is fully saturated;+--  ie, args and parms have the same length+--+dtiReduce :: DTI STy -> [STy] -> DTI STy+dtiReduce (ADT name args cons) parms+  = ADT name [] (map (ciReduce (zip args parms)) cons)+dtiReduce (New name args con)  parms+  = New name [] (ciReduce (zip args parms) con)++ciReduce :: [(Name , STy)] -> CI STy -> CI STy+ciReduce parms ci = runIdentity (ciMapM (return . styReduce parms) ci)  ++-- * Monad+--+-- Keeks the (M.Map STy (Int , DTI Sty)) in a state.++data IK+  = AtomI Int+  | 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++data Idxs +  = Idxs { idxsNext :: Int+         , idxsMap  :: M.Map STy (Int , Maybe (DTI IK))+         }+  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)++type IdxsM = StateT Idxs++runIdxsM :: (Monad m) => IdxsM m a -> m (a , Idxs)+runIdxsM = flip runStateT (Idxs 0 M.empty)++-- |The actual monad we need to run all of this;+type M = IdxsM Q++-- |Returns the index of a "Name" within the family.+--  If this name has not been registered yet, returns+--  a fresh index.+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++-- |Register some Datatype Information for a given STy+register :: (Monad m) => STy -> DTI IK -> IdxsM m ()+register ty info = indexOf ty -- the call to indexOf guarantees the+                              -- adjust will do something;+                >> modify (onMap $ M.adjust (id *** const (Just info)) ty)++-- | All the necessary lookups:+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++lkupData :: (Monad m) => STy -> IdxsM m (Maybe (DTI IK))+lkupData ty = join . fmap snd <$> lkup ty++hasData :: (Monad m) => STy -> IdxsM m Bool+hasData ty = maybe False (const True) <$> lkupData ty++----------------------------+-- * Preprocessing Data * --+----------------------------++-- |Performs step 2 of the sketch;+reifySTy :: STy -> M ()+reifySTy sty+  = do ix <- indexOf sty+       uncurry go (styFlatten sty)+  where+    go :: STy -> [STy] -> M ()+    go (ConST name) args+      = do dec <- lift (reifyDec name >>= decInfo)+           -- TODO: Check that the precondition holds.+           let res = dtiReduce dec args+           (final , todo) <- runWriterT $ dtiMapM convertSTy res+           register sty final+           mapM_ reifySTy todo+    +    -- Convert the STy's in the fields of the constructors;+    -- tells a list of STy's we still need to process.+    convertSTy :: STy -> WriterT [STy] M IK+    convertSTy ty+      -- We remove sty from the list of todos+      -- otherwise we get an infinite loop+      | ty == sty = AtomI <$> lift (indexOf ty)+      | isClosed ty+      = case makeCons ty of+          Just k  -> return (AtomK k)+          Nothing -> do ix     <- lift (indexOf ty)+                        hasDti <- lift (hasData ty)+                        when (not hasDti) (tell [ty])+                        return (AtomI ix)+      | otherwise+      = fail $ "I can't convert type variable " ++ show ty+              ++ " when converting " ++ show sty++    makeCons :: STy -> Maybe Name+    makeCons (ConST n) = M.lookup n consTable+    makeCons _         = Nothing++    consTable = M.fromList . map (id *** mkName)+      $ [ ( ''Int     , "KInt")+        , ( ''Char    , "KChar")+        , ( ''Integer , "KInteger")+        , ( ''Float   , "KFloat")+        , ( ''Bool    , "KBool")+        , ( ''String  , "KString")+        , ( ''Double  , "KDouble")+        ]++-----------------------------+-- * Generating the Code * --+-----------------------------++-- Code generation happens in a few separate parts.+-- Given a datatype:+-- +-- > data R a = a :>: [R a]+-- >          | Leaf a+-- >          deriving Show+--+-- We need to generate:+--+-- 1. The Family and the codes+-- 1.1 > type FamRose   = '[ [R Int] , R Int ]+-- 1.2 > type D0_ = Z+--     > type D1_ = S Z+-- 1.3 > type CodesRose = '[ '[ '[] , '[I D1_ , I D0_] ]+--     >                   , '[ '[K KInt , I D0_] , '[K KInt] ]+--     >                   ]+--+-- 2. The index of each type in the family.+-- 2.1 types+-- > pattern IdxRInt     = SZ+-- > pattern IdxListInt  = SS SZ+--+-- 2.1.1 Here-There Synonyms+-- > pattern HT0_ d = Here d+-- > pattern HT1_ d = There (Here d)+--+-- 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)+--+-- 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)+-- >   sfrom' (SS SZ) (El (Leaf a))+-- >     = Rep $ HT1_ (NA_K (SInt a) :* NP0)+-- >   sfrom' SZ (El [])+-- >     = Rep $ HT0_ NP0+-- >   sfrom' SZ (El (x:xs))+-- >     = Rep $ HT1_ (NA_I (El x) :* NA_I (El xs) :* NP0)+--+-- 3.2.+-- > +-- >   sto' SZ (Rep (HT0_ NP0))+-- >     = El []+-- >   sto' SZ (Rep (HT1_ (NA_I (El x) :* NA_I (El xs) :* NP0)))+-- >     = El (x : xs)+-- >   sto' (SS SZ) (Rep (HT0_ (NA_K (SInt a) :* NA_I (El as) :* NP0)))+-- >     = El (a :>: as)+-- >   sto' (SS SZ) (Rep (HT1_ (NA_K (SInt a) :* NP0)))+-- >     = El (Leaf a)+--+-- 4. Metadata for each type in (1)+-- > instance HasDatatypeInfo Singl FamRose CodesRose Z where ...+-- > instance HasDatatypeInfo Singl FamRose codesRose (S Z) where ...+-- ++-- |The input data for the generation is an ordered list+--  (on the second component of the tuple) of STy's and+--  their datatype info.+type Input = [(STy , Int , DTI IK)]++-- Generates a type-level list of 'a's+tlListOf :: (a -> Type) -> [a] -> Type+tlListOf f = foldr (\h r -> AppT (AppT PromotedConsT (f h)) r) PromotedNilT++-- generate a type-level Nat+int2Type :: Int -> Type+int2Type 0 = tyZ+int2Type n = AppT tyS (int2Type (n - 1))++-- generate the name of the type synonym corresponding to+-- this int.+int2TySynName :: Int -> Name+int2TySynName i = mkName $ "D" ++ show i ++ "_"++-- generates a Snat for the given Int+int2SNatPat :: Int -> Pat+int2SNatPat 0 = ConP (mkName "SZ") []+int2SNatPat n = ConP (mkName "SS") [int2SNatPat $ n-1]++-- Our promoted type constructors+tyS = PromotedT (mkName "S")+tyZ = PromotedT (mkName "Z")+tyI = PromotedT (mkName "I")+tyK = PromotedT (mkName "K")++-- Generate rhs of piece (1.3)+inputToCodes :: Input -> Q Type+inputToCodes = return . tlListOf dti2Codes . map third+  where+    third (_ , _ , x) = x++dti2Codes :: DTI IK -> Type+dti2Codes = tlListOf ci2Codes . dti2ci++ci2Codes :: CI IK -> Type+ci2Codes = tlListOf ik2Codes . ci2ty++ik2Codes :: IK -> Type+-- VCM: int pattern synonyms make too many name clashes+--      if we mix up modules.+ik2Codes (AtomI n) = AppT tyI $ int2Type n -- ConT (int2TySynName n)+ik2Codes (AtomK k) = AppT tyK $ PromotedT k++-- Generates piece (1.2); we do so by+-- finding what's the maximum type index used+-- in all DatatypeInformation we have and then generate+-- all type synonyms up to it.+inputToTySynNums :: Input -> Q [Dec]+inputToTySynNums input+  = let maxI = maximum $ map (localMax . third) input+     in return $ map genTySynNum [0..maxI]+  where+    third (_ , _ , x) = x++    localMax :: DTI IK -> Int+    localMax = foldr (\ci aux -> aux `max` getMaxIdx (ci2ty ci)) 0 . dti2ci++    getMaxIdx :: [IK] -> Int+    getMaxIdx = foldr (ikElim max (const id)) 0++    genTySynNum i = TySynD (int2TySynName i) [] (int2Type i)++-- generates rhs of piece (1.1)+inputToFam :: Input -> Q Type+inputToFam = return . tlListOf trevnocType . map first+  where+    first (x , _ , _) = x++-- | @styToName "List (R Int)" == "ListRInt"@+styToName :: STy -> Name+styToName = mkName . styFold (++) nameBase (fixList . nameBase)+  where+    -- VCM: ugly hack; but list is a reserved name.+    --      The hack is needed either here or in reify.+    fixList :: String -> String+    fixList n+      | n == "[]"        = "List"+      | take 2 n == "(," = "Tup" ++ show (length n - 2) +      | otherwise        = n++onBaseName :: (String -> String) -> Name -> Name+onBaseName f = mkName . f . nameBase++codesName :: STy -> Q Name+codesName = return . onBaseName ("Codes" ++) . styToName++familyName :: STy -> Q Name+familyName = return . onBaseName ("Fam" ++) . styToName++genPiece1 :: STy -> Input -> Q [Dec]+genPiece1 first ls+  = do -- nums  <- inputToTySynNums ls+       codes <- TySynD <$> codesName first+                       <*> return []+                       <*> inputToCodes ls+       fam   <- TySynD <$> familyName first+                       <*> return []+                       <*> inputToFam ls+       return [fam , codes] -- (nums ++ [fam , codes])++idxPatSynName :: STy -> Name+idxPatSynName = styToName . (AppST (ConST (mkName "Idx")))+       +idxPatSyn :: STy -> Pat+idxPatSyn = flip ConP [] . idxPatSynName++-- |@htPatSynName ci@ will generate the+--  pattern synonym name for constructor ci.+--+--  Since all our patterns are supposed to be @PrefixPatSyn@s,+--  we need to translate the infix names to something+--  Haskell will accept.+htPatSynName :: Int -> CI IK -> Name+htPatSynName dtiIx ci = mkName . translate . nameBase . ciName $ ci+  where+    translate = ("Pat" ++) . foldl' (\str l -> str ++ tr l ) (show dtiIx)+    tr l | isAlphaNum l = l:[]+         | otherwise    = show $ ord l++htPatSynExp :: Int -> CI IK -> Q Exp+htPatSynExp dtiIx = return . ConE . htPatSynName dtiIx++genIdxPatSyn :: STy -> Int -> Q Dec+genIdxPatSyn sty ix+  = return (PatSynD (idxPatSynName sty) (PrefixPatSyn []) ImplBidir (int2SNatPat ix))++genHereTherePatSyn :: STy -> Input -> Q [Dec]+genHereTherePatSyn first ls+  = flat . concat <$> mapM (\(_ , ix , dti) -> genHereThereFor ix dti) ls+  where+    flat             = foldl' (\ac (x , y) -> x:y:ac) []+    third (_ , _, x) = x++    famName = ConT <$> familyName first++    inj :: Int -> Q Pat -> Q Pat+    inj 0 p = [p| Here $p                  |]+    inj n p = [p| There ( $(inj (n-1) p) ) |]++    -- Returns one pattern synonym for each constructor in+    -- the datatype and a type signature for it.+    genHereThereFor :: Int -> DTI IK -> Q [(Dec , Dec)]+    genHereThereFor dtiIx dti+      = do let dtiCode = dti2Codes dti+           let cisIx   = zip [0..] (dti2ci dti)+           forM cisIx $ \ (ix , ci)+             -> (,) <$> genHT_decl dtiCode dtiIx ix ci+                    <*> genHT_def          dtiIx ix ci++    genHT_decl dtiCode dtiIx ix ci+      = PatSynSigD (htPatSynName dtiIx ci)+          <$> [t| PoA Singl (El $famName) $(return $ ci2Codes ci)+                -> NS (PoA Singl (El $famName)) $(return dtiCode) |]++    genHT_def dtiIx ix ci+      = do var <- newName "d"+           PatSynD (htPatSynName dtiIx ci) (PrefixPatSyn [var]) ImplBidir+             <$> inj ix (return $ VarP var)+           ++-- |Generating pattern sinonyms for the type indexes+--  and the 'Here/There' combinations. (pieces 2.1 and 2.1.1)+--+--  > pattern IdxRInt = SZ+--  > pattern IdxListRInt = SS SZ+--+genPiece2 :: STy -> Input -> Q [Dec]+genPiece2 first ls+  = do p21  <- mapM (\(sty , ix , dti) -> genIdxPatSyn sty ix) ls+       p211 <- genHereTherePatSyn first ls+       return $ p21 ++ p211++genPiece3 :: STy -> Input -> Q Dec+genPiece3 first ls+  = head <$> [d| instance Family Singl+                                 $(ConT <$> familyName first)+                                 $(ConT <$> codesName first)+                   where sfrom' = $(genPiece3_1 ls)+                         sto'   = $(genPiece3_2 ls) |]++-- |Given a datatype information, generates a pattern+--  and an expression from it. The int here+--  indicates the number of the constructor.+--+--  > ci2PatExp IdxBinTree (Normal "Bin" [VarT a , VarT a])+--  >   = ( El (Bin x_1 x_2)+--  >     , Rep (PatBin_IdxBinTree (NA_I (El x_1) :* NA_I (El x_2) :* NP0))+--  >     )+ci2PatExp :: Int -> CI IK -> Q (Pat , Exp)+ci2PatExp dtiIx ci+  = do (vars , pat) <- ci2Pat ci+       bdy          <- [e| Rep $(inj $ genBdy (zip vars (ci2ty ci))) |]+       return (ConP (mkName "El") [pat] , bdy)+  where+    inj :: Q Exp -> Q Exp+    -- inj 0 e = [e| Here $e              |]+    -- inj n e = [e| There $(inj (n-1) e) |]+    inj e = [e| $(htPatSynExp dtiIx ci) $e |]++    genBdy :: [(Name , IK)] -> Q Exp+    genBdy []       = [e| NP0 |]+    genBdy (x : xs) = [e| $(mkHead x) :* ( $(genBdy xs) ) |]+++    mkHead (x , AtomI _) = [e| NA_I (El $(return (VarE x))) |]+    mkHead (x , AtomK k) = [e| NA_K $(return (AppE (ConE (mkK k)) (VarE x))) |]++    mkK k = mkName $ 'S':tail (nameBase k)++-- | Just like 'ci2PatExp', but the other way around.+--+--  > ci2ExpPat IdxBinTree (Normal "Bin" [VarT a , VarT a])+--  >   = ( Rep (PatBin_IdxBinTree (NA_I (El x_1) :* NA_I (El x_2) :* NP0))+--        , El (Bin x_1 x_2)+--  >     )+ci2ExpPat :: Int -> CI IK -> Q (Pat , Exp)+ci2ExpPat dtiIx ci+  = do (vars , exp) <- ci2Exp ci+       pat          <- [p| Rep $(inj $ genBdy (zip vars (ci2ty ci))) |]+       return (pat , AppE (ConE $ mkName "El") exp)+  where+    inj :: Q Pat -> Q Pat+    -- inj 0 e = [p| Here $e              |]+    -- inj n e = [p| There $(inj (n-1) e) |]+    inj e = ConP (htPatSynName dtiIx ci) . (:[]) <$> e+    +    genBdy :: [(Name , IK)] -> Q Pat+    genBdy []       = [p| NP0 |]+    genBdy (x : xs) = [p| $(mkHead x) :* ( $(genBdy xs) ) |]+++    mkHead (x , AtomI _) = [p| NA_I (El $(return (VarP x))) |]+    mkHead (x , AtomK k) = [p| NA_K $(return (ConP (mkK k) [VarP x])) |]++    mkK k = mkName $ 'S':tail (nameBase k)+++match :: Pat -> Exp -> Match+match pat bdy = Match pat (NormalB bdy) []++-- Adds a matchall clause; for instance:+--+-- > matchAll [Just x -> 1] = [Just x -> 1 , _ -> error "matchAll"]+--+matchAll :: [Match] -> [Match]+matchAll = (++ [match WildP err])+  where+    err = AppE (VarE (mkName "error")) (LitE (StringL "matchAll"))++genPiece3_1 :: Input -> Q Exp+genPiece3_1 input+  = LamCaseE <$> mapM (\(sty , ix , dti) -> clauseForIx sty ix dti) input+  where+    clauseForIx :: STy -> Int -> DTI IK -> Q Match+    clauseForIx sty ix dti = match (idxPatSyn sty)+                       <$> (LamCaseE <$> genMatchFor ix dti)+    +    genMatchFor :: Int -> DTI IK -> Q [Match]+    genMatchFor ix dti = map (uncurry match) <$> mapM (ci2PatExp ix) (dti2ci dti)+      +genPiece3_2 :: Input -> Q Exp+genPiece3_2 input+  = LamCaseE . matchAll <$> mapM (\(sty , ix , dti) -> clauseForIx sty ix dti) input+  where    +    clauseForIx :: STy -> Int -> DTI IK -> Q Match+    clauseForIx sty ix dti = match (idxPatSyn sty)+                       <$> (LamCaseE . matchAll <$> genMatchFor ix dti)+      +    genMatchFor :: Int -> DTI IK -> Q [Match]+    genMatchFor ix dti = map (uncurry match) <$> mapM (ci2ExpPat ix) (dti2ci dti)++genPiece4 :: STy -> Input -> Q [Dec]+genPiece4 first ls = concat <$> mapM genDatatypeInfoInstance ls+  where+    genDatatypeInfoInstance :: (STy , Int , DTI IK) -> Q [Dec]+    genDatatypeInfoInstance (sty , idx , dti)+      = [d| instance Meta.HasDatatypeInfo Singl $(ConT <$> familyName first)+                                                $(ConT <$> codesName first)+                                                $(return (int2Type idx))+              where datatypeInfo _ _ = $(genInfo sty dti) |]++    genMod :: Name -> Q Exp+    genMod = strlit . maybe "" id . nameModule++    strlit :: String -> Q Exp+    strlit = return . LitE . StringL++    genDatatypeName :: STy -> Q Exp+    genDatatypeName = styFold (\e1 e2 -> [e| ( $e1 Meta.:@: $e2 ) |])+                              (\n -> [e| Meta.Name $(strlit (nameBase n)) |] )+                              (\n -> [e| Meta.Name $(strlit (nameBase n)) |] )++    genInfo :: STy -> DTI IK -> Q Exp+    genInfo sty (ADT name _ cis)+      = [e| Meta.ADT $(genMod name) $(genDatatypeName sty) $(genConInfoNP cis) |]+    genInfo sty (New name _ ci)+      = [e| Meta.New $(genMod name) $(genDatatypeName sty) $(genConInfo ci) |]++    genConInfo :: CI IK -> Q Exp+    genConInfo (Record conname fields)+      = [e| Meta.Record $(strlit $ nameBase conname) $(genFieldInfo $ map fst fields) |]+    genConInfo (Normal conname _)+      = [e| Meta.Constructor $(strlit $ nameBase conname) |]+    genConInfo (Infix conname fix _ _)+      = [e| Meta.Infix $(strlit $ nameBase conname) $(genAssoc fix) $(genFix fix) |]+      where+        genAssoc (Fixity _ InfixL) = [e| Meta.LeftAssociative  |]+        genAssoc (Fixity _ InfixR) = [e| Meta.RightAssociative |]+        genAssoc (Fixity _ InfixN) = [e| Meta.NotAssociative   |]++        genFix (Fixity i _) = return . LitE . IntegerL . fromIntegral $ i++    genFieldInfo :: [ FieldName ] -> Q Exp+    genFieldInfo []     = [e| NP0 |]+    genFieldInfo (f:fs) = [e| Meta.FieldInfo $(strlit . nameBase $ f) :* ( $(genFieldInfo fs) ) |]++    genConInfoNP :: [ CI IK ] -> Q Exp+    genConInfoNP []       = [e| NP0 |]+    genConInfoNP (ci:cis) = [e| $(genConInfo ci) :* ( $(genConInfoNP cis) ) |]++-- |@genFamily init fam@ generates a type-level list+--  of the codes for the family. It also generates+--  the necessary 'Element' instances.+--  TODO: generate the 'HasDatatypeInfo' instances too!+--+--  Precondition, input is sorted on second component.+genFamily :: STy -> Input -> Q [Dec]+genFamily first ls+  = do p1 <- genPiece1 first ls+       p2 <- genPiece2 first ls+       p3 <- genPiece3 first ls+       p4 <- genPiece4 first ls+       return $ p1 ++ p2 ++ [p3] ++ p4++-- |Generates a bunch of strings for debug purposes.+genFamilyDebug :: STy -> [(STy , Int , DTI IK)] -> Q [Dec]+genFamilyDebug _ ms = concat <$> mapM genDec ms+  where+    genDec :: (STy , Int , DTI IK) -> Q [Dec]+    genDec (sty , ix , dti)+      = [d| $( genPat ix ) = $(mkBody dti) |]++    mkBody :: DTI IK -> Q Exp+    mkBody dti = [e| $(liftString $ show dti) |]++    genPat :: Int -> Q Pat+    genPat n = genName n >>= \name -> return (VarP name)++    genName :: Int -> Q Name+    genName n = return (mkName $ "tyInfo_" ++ show n)

@@ -0,0 +1,169 @@+{-# LANGUAGE ConstraintKinds     #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE PolyKinds           #-}+{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE TypeApplications    #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- |Useful utilities we need accross multiple modules.+module Generics.MRSOP.Util+  ( -- * Utility Functions and Types+    (&&&) , (***)+  , (:->) , (<.>)++    -- * Poly-kind indexed product+  , (:*:)(..) , curry' , uncurry'++    -- * Type-level Naturals+  , Nat(..) , proxyUnsuc+  , SNat(..) , snat2int+  , IsNat(..) , getNat , getSNat'++    -- * Type-level Lists+  , ListPrf(..) , IsList(..)+  , L1 , L2 , L3 , L4+  , (:++:) , appendIsListLemma++    -- * Type-level List Lookup+  , Lkup , Idx , El(..) , getElSNat , into++    -- * Higher-order Eq and Show+  , Eq1(..) , Show1(..)+  ) where++import Data.Proxy+import Data.Type.Equality+import GHC.TypeLits (TypeError , ErrorMessage(..))+import Control.Arrow ((***) , (&&&))++-- |Poly-kind-indexed product+data (:*:) (f :: k -> *) (g :: k -> *) (x :: k)+  = f x :*: g x++-- |Lifted curry+curry' :: ((f :*: g) x -> a) -> f x -> g x -> a+curry' f fx gx = f (fx :*: gx)++-- |Lifted uncurry+uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a+uncurry' f (fx :*: gx) = f fx gx++-- |Natural transformations+type f :-> g = forall n . f n -> g n++infixr 8 <.>+-- |Kleisli Composition+(<.>) :: (Monad m) => (b -> m c) -> (a -> m b) -> a -> m c+f <.> g = (>>= f) . g++-- |Type-level Peano Naturals+data Nat = S Nat | Z+  deriving (Eq , Show)++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)++snat2int :: SNat n -> Integer+snat2int SZ     = 0+snat2int (SS n) = 1 + snat2int n++-- |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+  getSNat p = SS (getSNat $ proxyUnsuc p)++getNat :: (IsNat n) => Proxy n -> Integer+getNat = snat2int . getSNat++getSNat' :: forall (n :: Nat). IsNat n => SNat n+getSNat' = getSNat (Proxy :: Proxy n)++instance TestEquality SNat where+  testEquality SZ     SZ     = Just Refl+  testEquality (SS n) (SS m)+    = case testEquality n m of+        Nothing   -> Nothing+        Just Refl -> Just Refl+  testEquality _      _      = Nothing++-- |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")++-- |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")++-- |Also list lookup, but for kind * only.+data El :: [*] -> Nat -> * where+  El :: IsNat ix => {unEl :: Lkup ix fam} -> El fam ix++-- | Convenient way to cast an 'El' index to term-level.+getElSNat :: forall ix ls. El ls ix -> SNat ix+getElSNat (El _) = getSNat' @ix++-- |Smart constructor into 'El'+into :: forall fam ty ix+      . (ix ~ Idx ty fam , Lkup ix fam ~ ty , IsNat ix)+     => 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+--  type-level lists whenever we see fit.+data ListPrf :: [k] -> * where+  Nil ::  ListPrf '[]+  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+instance IsList xs => IsList (x ': xs) where+  listPrf = 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)++-- |Appending type-level lists+type family (:++:) (txs :: [k]) (tys :: [k]) :: [k] where+  (:++:) '[] tys = tys+  (:++:) (tx ': txs) tys = tx ': (txs :++: tys)++-- |Convenient constraint synonyms+type L1 xs          = (IsList xs) +type L2 xs ys       = (IsList xs, IsList ys) +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 Eq1 (f :: k -> *) where+  eq1 :: forall k . f k -> f k -> Bool++-- |Higher order version of 'Show'+class Show1 (f :: k -> *) where+  show1 :: forall k . f k -> String+

@@ -0,0 +1,139 @@+{-# LANGUAGE RankNTypes           #-}+{-# LANGUAGE FlexibleContexts     #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE TypeApplications     #-}+-- |Provides Zippers (aka One-hole contexts) for our+--  universe.+module Generics.MRSOP.Zipper where++import Data.Type.Equality++import Generics.MRSOP.Util 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+--  fashion, it consists of a choice of constructor and+--  a position in the type of that constructor.+data Loc :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> * where+  Loc :: IsNat ix => El fam ix -> Ctxs ki fam cs iy ix -> Loc ki fam cs iy++-- |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+  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++-- |A @Ctx ki fam c ix@ is a choice of constructor for @c@+--  with a hole of type @ix@ inside.+data Ctx :: (kon -> *) -> [*] -> [[Atom kon]] -> Nat -> * where+  Ctx :: Constr c n+      -> NPHole ki fam ix (Lkup n c)+      -> Ctx ki fam c ix++-- |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)+  T :: NA ki (El fam) x -> NPHole ki fam ix xs -> NPHole ki fam ix (x : xs)++-- |Existential abstraction; needed for walking the possible+--  holes in a product. We must be able to hide the type.+data NPHoleE :: (kon -> *) -> [*] -> [Atom kon] -> * where+  ExistsIX :: IsNat ix => El fam ix -> NPHole ki fam ix xs -> NPHoleE ki fam xs++-- |Given a 'PoA' (product of atoms), returns a one with a hole+--  in the first seen 'NA_I'. Note that we need the 'NPHoleE'+--  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 (NA_I x :* xs) = Just (ExistsIX x (H xs))+mkNPHole (NA_K k :* xs)+  = do (ExistsIX el c) <- mkNPHole xs+       return (ExistsIX el (T (NA_K k) c))++-- |Given a hole and an element, put both together to form+--  the 'PoA' again.+fillNPHole :: (IsNat ix) => El fam ix -> NPHole ki fam ix xs -> PoA ki (El fam) xs+fillNPHole x (H xs)   = NA_I x :* xs+fillNPHole x (T y xs) = y :* fillNPHole x xs++-- |Given an hole and an element, return the next hole, if any.+walkNPHole :: (IsNat ix) => El fam ix -> NPHole ki fam ix xs -> Maybe (NPHoleE ki fam xs)+walkNPHole el (H xs)+  = do (ExistsIX el' c) <- mkNPHole xs+       return (ExistsIX el' (T (NA_I el) c))+walkNPHole el (T na xs)+  = do (ExistsIX el' c) <- walkNPHole el xs+       return (ExistsIX el' (T na c))++-- * Primitives++-- |Executes an action in the first hole within the given 'Rep' value,+--  if such hole can be constructed.+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))++-- |Fills up a hole.+fill :: (IsNat ix) => El fam ix -> Ctx ki fam c ix -> Rep ki (El fam) c+fill el (Ctx c nphole) = inj c (fillNPHole el nphole)++-- |Walks to the next hole and execute an action.+next :: (IsNat ix)+     => (forall iy . IsNat iy => El fam iy -> Ctx ki fam c iy -> a)+     -> El fam ix -> Ctx ki fam c ix -> Maybe a+next f el (Ctx c nphole)+  = do (ExistsIX el' nphole') <- walkNPHole el nphole+       return (f el' (Ctx c nphole'))++-- * Navigation++-- |Move one layer deeper within the recursive structure.+down :: (Family ki fam codes , IsNat ix)+     => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix)+down (Loc el ctx)+  = first (\el' ctx' -> Loc el' (Cons ctx' ctx))+          (sfrom el)++-- |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 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 el (Cons ctx ctxs)) = next (\el' ctx' -> Loc el' (Cons ctx' ctxs)) el ctx++-- * Interface++-- |Initializes the zipper+enter :: (Family ki fam codes , IsNat ix)+      => El fam ix -> Loc ki fam codes ix+enter el = Loc el Nil++-- |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!++-- |Updates the value in the hole.+update :: (Family ki fam codes , IsNat ix)+       => (forall ix . SNat ix -> El fam ix -> El fam ix)+       -> Loc ki fam codes ix -> Loc ki fam codes ix+update f (Loc el ctxs) = Loc (f (getElSNat el) el) ctxs