diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,5 @@ +# Revision history for generics-mrsop + +## 1.0.0.0 -- May 2018 + +* First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/generics-mrsop.cabal b/generics-mrsop.cabal new file mode 100644 --- /dev/null +++ b/generics-mrsop.cabal @@ -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 diff --git a/src/Generics/MRSOP/Base.hs b/src/Generics/MRSOP/Base.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Base.hs @@ -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 + diff --git a/src/Generics/MRSOP/Base/Class.hs b/src/Generics/MRSOP/Base/Class.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Base/Class.hs @@ -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 diff --git a/src/Generics/MRSOP/Base/Combinators.hs b/src/Generics/MRSOP/Base/Combinators.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Base/Combinators.hs @@ -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) diff --git a/src/Generics/MRSOP/Base/Metadata.hs b/src/Generics/MRSOP/Base/Metadata.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Base/Metadata.hs @@ -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 + + diff --git a/src/Generics/MRSOP/Base/NP.hs b/src/Generics/MRSOP/Base/NP.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Base/NP.hs @@ -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 + diff --git a/src/Generics/MRSOP/Base/NS.hs b/src/Generics/MRSOP/Base/NS.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Base/NS.hs @@ -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 + diff --git a/src/Generics/MRSOP/Base/Show.hs b/src/Generics/MRSOP/Base/Show.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Base/Show.hs @@ -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 diff --git a/src/Generics/MRSOP/Base/Universe.hs b/src/Generics/MRSOP/Base/Universe.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Base/Universe.hs @@ -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) diff --git a/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs b/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Examples/LambdaAlphaEqTH.hs @@ -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])))) diff --git a/src/Generics/MRSOP/Examples/RoseTree.hs b/src/Generics/MRSOP/Examples/RoseTree.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Examples/RoseTree.hs @@ -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) diff --git a/src/Generics/MRSOP/Examples/RoseTreeTH.hs b/src/Generics/MRSOP/Examples/RoseTreeTH.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Examples/RoseTreeTH.hs @@ -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) diff --git a/src/Generics/MRSOP/Examples/SimpTH.hs b/src/Generics/MRSOP/Examples/SimpTH.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Examples/SimpTH.hs @@ -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 + diff --git a/src/Generics/MRSOP/Opaque.hs b/src/Generics/MRSOP/Opaque.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Opaque.hs @@ -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 = (==) + diff --git a/src/Generics/MRSOP/TH.hs b/src/Generics/MRSOP/TH.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/TH.hs @@ -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) diff --git a/src/Generics/MRSOP/Util.hs b/src/Generics/MRSOP/Util.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Util.hs @@ -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 + diff --git a/src/Generics/MRSOP/Zipper.hs b/src/Generics/MRSOP/Zipper.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/Zipper.hs @@ -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