diff --git a/src/Unbound/Generics/LocallyNameless/Kind/Derive.hs b/src/Unbound/Generics/LocallyNameless/Kind/Derive.hs --- a/src/Unbound/Generics/LocallyNameless/Kind/Derive.hs +++ b/src/Unbound/Generics/LocallyNameless/Kind/Derive.hs @@ -1,15 +1,15 @@ -{-# language TypeOperators #-} +{-# language ConstraintKinds #-} +{-# language DataKinds #-} +{-# language FlexibleContexts #-} +{-# language FlexibleInstances #-} +{-# language GADTs #-} {-# language MultiParamTypeClasses #-} -{-# language FlexibleInstances #-} -{-# language FlexibleContexts #-} -{-# language PolyKinds #-} -{-# language DataKinds #-} -{-# language UndecidableInstances #-} +{-# language PolyKinds #-} {-# language QuantifiedConstraints #-} -{-# language GADTs #-} -{-# language ScopedTypeVariables #-} -{-# language TypeApplications #-} -{-# language ConstraintKinds #-} +{-# language ScopedTypeVariables #-} +{-# language TypeApplications #-} +{-# language TypeOperators #-} +{-# language UndecidableInstances #-} module Unbound.Generics.LocallyNameless.Kind.Derive ( -- For use with DerivingVia AutoAlpha(..) @@ -31,26 +31,27 @@ , buildSubstName , gsubstDefK , gsubstsDefK +, gsubstBvsDefK ) where -import Control.Arrow (first) -import Control.Monad (liftM) -import Data.Function (on) -import Data.Functor.Contravariant (Contravariant(..)) -import Data.Kind -import Data.List (find) -import Data.Monoid (All(..)) -import Type.Reflection +import Control.Arrow (first) +import Data.Function (on) +import Data.Functor.Contravariant (Contravariant (..)) +import Data.Kind (Type) +import Data.List (find) +import Data.Maybe (fromMaybe) +import Data.Monoid (All (..)) +import Type.Reflection -import Unbound.Generics.LocallyNameless.Alpha -import Unbound.Generics.LocallyNameless.Name -import Unbound.Generics.LocallyNameless.Fresh -import Unbound.Generics.LocallyNameless.LFresh -import Unbound.Generics.LocallyNameless.Subst -import Unbound.Generics.PermM -import Generics.Kind +import Generics.Kind +import Unbound.Generics.LocallyNameless.Alpha +import Unbound.Generics.LocallyNameless.Fresh +import Unbound.Generics.LocallyNameless.LFresh +import Unbound.Generics.LocallyNameless.Name +import Unbound.Generics.LocallyNameless.Subst +import Unbound.Generics.PermM -type GenericAlpha a = (GenericK a, GAlphaK (RepK a) LoT0 LoT0) +type GenericAlpha a = (GenericK a, GAlphaK (RepK a) 'LoT0 'LoT0) newtype AutoAlpha a = AutoAlpha { unAutoAlpha :: a } deriving (Eq, Show) @@ -58,7 +59,7 @@ instance (Typeable a, GenericAlpha a, Show a) => Alpha (AutoAlpha a) where aeq' ctx (AutoAlpha x) (AutoAlpha y) = aeqDefK ctx x y - fvAny' ctx nfn (AutoAlpha x) + fvAny' ctx nfn (AutoAlpha x) = AutoAlpha <$> fvAnyDefK ctx nfn x close ctx npf = AutoAlpha . closeDefK ctx npf . unAutoAlpha open ctx npf = AutoAlpha . openDefK ctx npf . unAutoAlpha @@ -68,54 +69,54 @@ nthPatFind = nthPatFindDefK . unAutoAlpha namePatFind = namePatFindDefK . unAutoAlpha swaps' ctx perm = AutoAlpha . swapsDefK ctx perm . unAutoAlpha - lfreshen' ctx (AutoAlpha x) cont - = lfreshenDefK ctx x (\y p -> cont (AutoAlpha y) p) + lfreshen' ctx (AutoAlpha x) cont + = lfreshenDefK ctx x (cont . AutoAlpha) freshen' ctx (AutoAlpha x) - = (\(y, p) -> (AutoAlpha y, p)) <$> freshenDefK ctx x + = first AutoAlpha <$> freshenDefK ctx x acompare' ctx (AutoAlpha x) (AutoAlpha y) = acompareDefK ctx x y aeqDefK :: forall a. (GenericAlpha a) => AlphaCtx -> a -> a -> Bool -aeqDefK c = (gaeqK c) `on` (fromK @_ @a @LoT0) +aeqDefK c = gaeqK c `on` fromK @_ @a @'LoT0 fvAnyDefK :: forall g a. (GenericAlpha a, Contravariant g, Applicative g) - => AlphaCtx -> (AnyName -> g AnyName) -> a -> g a -fvAnyDefK c nfn = fmap (toK @_ @a @LoT0) . gfvAnyK c nfn . fromK @_ @a @LoT0 + => AlphaCtx -> (AnyName -> g AnyName) -> a -> g a +fvAnyDefK c nfn = fmap (toK @_ @a @'LoT0) . gfvAnyK c nfn . fromK @_ @a @'LoT0 closeDefK :: forall a. (GenericAlpha a) - => AlphaCtx -> NamePatFind -> a -> a -closeDefK c b = toK @_ @a @LoT0 . gcloseK c b . fromK @_ @a @LoT0 + => AlphaCtx -> NamePatFind -> a -> a +closeDefK c b = toK @_ @a @'LoT0 . gcloseK c b . fromK @_ @a @'LoT0 openDefK :: forall a. (GenericAlpha a) - => AlphaCtx -> NthPatFind -> a -> a -openDefK c b = toK @_ @a @LoT0 . gopenK c b . fromK @_ @a @LoT0 + => AlphaCtx -> NthPatFind -> a -> a +openDefK c b = toK @_ @a @'LoT0 . gopenK c b . fromK @_ @a @'LoT0 isPatDefK :: forall a. (GenericAlpha a) => a -> DisjointSet AnyName -isPatDefK = gisPatK . fromK @_ @a @LoT0 +isPatDefK = gisPatK . fromK @_ @a @'LoT0 isTermDefK :: forall a. (GenericAlpha a) => a -> All -isTermDefK = gisTermK . fromK @_ @a @LoT0 +isTermDefK = gisTermK . fromK @_ @a @'LoT0 isEmbedDefK :: a -> Bool isEmbedDefK _ = False nthPatFindDefK :: forall a. (GenericAlpha a) => a -> NthPatFind -nthPatFindDefK = gnthPatFindK . fromK @_ @a @LoT0 +nthPatFindDefK = gnthPatFindK . fromK @_ @a @'LoT0 namePatFindDefK :: forall a. (GenericAlpha a) => a -> NamePatFind -namePatFindDefK = gnamePatFindK . fromK @_ @a @LoT0 +namePatFindDefK = gnamePatFindK . fromK @_ @a @'LoT0 swapsDefK :: forall a. (GenericAlpha a) - => AlphaCtx -> Perm AnyName -> a -> a -swapsDefK ctx perm = toK @_ @a @LoT0 . gswapsK ctx perm . fromK @_ @a @LoT0 + => AlphaCtx -> Perm AnyName -> a -> a +swapsDefK ctx perm = toK @_ @a @'LoT0 . gswapsK ctx perm . fromK @_ @a @'LoT0 lfreshenDefK :: forall m a b. (LFresh m, GenericAlpha a) - => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b -lfreshenDefK ctx m cont = glfreshenK ctx (fromK @_ @a @LoT0 m) (cont . toK @_ @a @LoT0) + => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b +lfreshenDefK ctx m cont = glfreshenK ctx (fromK @_ @a @'LoT0 m) (cont . toK @_ @a @'LoT0) freshenDefK :: forall m a. (Fresh m, GenericAlpha a) - => AlphaCtx -> a -> m (a, Perm AnyName) -freshenDefK ctx = retractFFM . liftM (first (toK @_ @a @LoT0)) . gfreshenK ctx . fromK @_ @a @LoT0 + => AlphaCtx -> a -> m (a, Perm AnyName) +freshenDefK ctx = retractFFM . fmap (first (toK @_ @a @'LoT0)) . gfreshenK ctx . fromK @_ @a @'LoT0 acompareDefK :: forall a. (GenericAlpha a) => AlphaCtx -> a -> a -> Ordering -acompareDefK c = (gacompareK c) `on` (fromK @_ @a @LoT0) +acompareDefK c = gacompareK c `on` fromK @_ @a @'LoT0 -- | The "Generic" representation version of 'Alpha' -class GAlphaK (f :: LoT k -> *) (a :: LoT k) (b :: LoT k) where +class GAlphaK (f :: LoT k -> Type) (a :: LoT k) (b :: LoT k) where gaeqK :: AlphaCtx -> f a -> f b -> Bool gfvAnyK :: (a ~ b, Contravariant g, Applicative g) @@ -167,7 +168,7 @@ gswapsK ctx perm = Field . swaps' ctx perm . unField {-# INLINE gswapsK #-} - gfreshenK ctx = liftM (first Field) . liftFFM . freshen' ctx . unField + gfreshenK ctx = fmap (first Field) . liftFFM . freshen' ctx . unField {-# INLINE gfreshenK #-} glfreshenK ctx (Field c) cont = lfreshen' ctx c (cont . Field) @@ -203,7 +204,7 @@ gswapsK ctx perm = M1 . gswapsK ctx perm . unM1 {-# INLINE gswapsK #-} - gfreshenK ctx = liftM (first M1) . gfreshenK ctx . unM1 + gfreshenK ctx = fmap (first M1) . gfreshenK ctx . unM1 {-# INLINE gfreshenK #-} glfreshenK ctx (M1 f) cont = @@ -241,7 +242,7 @@ {-# INLINE gaeqK #-} gfvAnyK ctx nfn (f :*: g) = (:*:) <$> gfvAnyK ctx nfn f - <*> gfvAnyK ctx nfn g + <*> gfvAnyK ctx nfn g {-# INLINE gfvAnyK #-} gcloseK ctx b (f :*: g) = gcloseK ctx b f :*: gcloseK ctx b g @@ -276,7 +277,7 @@ {-# INLINE glfreshenK #-} gacompareK ctx (f1 :*: g1) (f2 :*: g2) = - (gacompareK ctx f1 f2) <> (gacompareK ctx g1 g2) + gacompareK ctx f1 f2 <> gacompareK ctx g1 g2 instance (GAlphaK f a b, GAlphaK g a b) => GAlphaK (f :+: g) a b where gaeqK ctx (L1 f1) (L1 f2) = gaeqK ctx f1 f2 @@ -315,8 +316,8 @@ gswapsK ctx perm (R1 f) = R1 (gswapsK ctx perm f) {-# INLINE gswapsK #-} - gfreshenK ctx (L1 f) = liftM (first L1) (gfreshenK ctx f) - gfreshenK ctx (R1 f) = liftM (first R1) (gfreshenK ctx f) + gfreshenK ctx (L1 f) = fmap (first L1) (gfreshenK ctx f) + gfreshenK ctx (R1 f) = fmap (first R1) (gfreshenK ctx f) {-# INLINE gfreshenK #-} glfreshenK ctx (L1 f) cont = @@ -359,7 +360,7 @@ gswapsK ctx perm (SuchThat f) = SuchThat (gswapsK ctx perm f) {-# INLINE gswapsK #-} - gfreshenK ctx (SuchThat f) = liftM (first SuchThat) (gfreshenK ctx f) + gfreshenK ctx (SuchThat f) = fmap (first SuchThat) (gfreshenK ctx f) {-# INLINE gfreshenK #-} glfreshenK ctx (SuchThat f) cont = glfreshenK ctx f (cont . SuchThat) @@ -368,7 +369,7 @@ gacompareK ctx (SuchThat f1) (SuchThat f2) = gacompareK ctx f1 f2 {-# INLINE gacompareK #-} -instance (forall (t1 :: k) (t2 :: k). GAlphaK f (t1 :&&: a) (t2 :&&: b)) +instance (forall (t1 :: k) (t2 :: k). GAlphaK f (t1 ':&&: a) (t2 ':&&: b)) => GAlphaK (Exists k f) a b where gaeqK ctx (Exists f1) (Exists f2) = gaeqK ctx f1 f2 @@ -397,7 +398,7 @@ gswapsK ctx perm (Exists f) = Exists (gswapsK ctx perm f) {-# INLINE gswapsK #-} - gfreshenK ctx (Exists f) = liftM (first Exists) (gfreshenK ctx f) + gfreshenK ctx (Exists f) = fmap (first Exists) (gfreshenK ctx f) {-# INLINE gfreshenK #-} glfreshenK ctx (Exists f) cont = glfreshenK ctx f (cont . Exists) @@ -405,54 +406,66 @@ gacompareK ctx (Exists f1) (Exists f2) = gacompareK ctx f1 f2 -gsubstDefK :: forall a b. (GenericK a, GSubstK b (RepK a) LoT0, Subst b a) +gsubstDefK :: forall a b. (GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a) => Name b -> b -> a -> a gsubstDefK n u x = - if (isFreeName n) + if isFreeName n then case (isvar x :: Maybe (SubstName a b)) of Just (SubstName m) | m == n -> u _ -> case (isCoerceVar x :: Maybe (SubstCoerce a b)) of - Just (SubstCoerce m f) | m == n -> maybe x id (f u) - _ -> toK @_ @a @LoT0 $ gsubstK n u (fromK @_ @a @LoT0 x) + Just (SubstCoerce m f) | m == n -> fromMaybe x (f u) + _ -> toK @_ @a @'LoT0 $ gsubstK n u (fromK @_ @a @'LoT0 x) else error $ "Cannot substitute for bound variable " ++ show n -gsubstsDefK :: forall a b. (GenericK a, GSubstK b (RepK a) LoT0, Subst b a) +gsubstsDefK :: forall a b. (GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a) => [(Name b, b)] -> a -> a gsubstsDefK ss x | all (isFreeName . fst) ss = case (isvar x :: Maybe (SubstName a b)) of Just (SubstName m) | Just (_, u) <- find ((==m) . fst) ss -> u _ -> case isCoerceVar x :: Maybe (SubstCoerce a b) of - Just (SubstCoerce m f) | Just (_, u) <- find ((==m) . fst) ss -> maybe x id (f u) - _ -> toK @_ @a @LoT0 $ gsubstsK ss (fromK @_ @a @LoT0 x) + Just (SubstCoerce m f) | Just (_, u) <- find ((==m) . fst) ss -> fromMaybe x (f u) + _ -> toK @_ @a @'LoT0 $ gsubstsK ss (fromK @_ @a @'LoT0 x) | otherwise = error $ "Cannot substitute for bound variable in: " ++ show (map fst ss) +gsubstBvsDefK :: forall a b. (GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a) + => AlphaCtx -> [b] -> a -> a +gsubstBvsDefK ctx bs x = + case (isvar x :: Maybe (SubstName a b)) of + Just (SubstName (Bn j k)) | ctxLevel ctx == j, fromInteger k < length bs -> bs !! fromInteger k + _ -> toK @_ @a @'LoT0 $ gsubstBvsK ctx bs (fromK @_ @a @'LoT0 x) + buildSubstName :: forall a b. (Typeable a, Typeable b) => Name a -> Maybe (SubstName a b) buildSubstName x = case eqTypeRep (typeRep @a) (typeRep @b) of Nothing -> Nothing Just HRefl -> Just (SubstName x) -class GSubstK b (f :: LoT k -> *) (a :: LoT k) where +class GSubstK b (f :: LoT k -> Type) (a :: LoT k) where gsubstK :: Name b -> b -> f a -> f a gsubstsK :: [(Name b, b)] -> f a -> f a + gsubstBvsK :: AlphaCtx -> [b] -> f a -> f a instance Subst b (Interpret t a) => GSubstK b (Field t) a where gsubstK nm val = Field . subst nm val . unField gsubstsK ss = Field . substs ss . unField + gsubstBvsK ctx ss = Field . substBvs ctx ss . unField instance GSubstK b f a => GSubstK b (M1 i c f) a where gsubstK nm val = M1 . gsubstK nm val . unM1 gsubstsK ss = M1 . gsubstsK ss . unM1 + gsubstBvsK ctx ss = M1 . gsubstBvsK ctx ss . unM1 instance GSubstK b U1 a where gsubstK _nm _val _ = U1 gsubstsK _ss _ = U1 + gsubstBvsK _ctx _ss _ = U1 instance (GSubstK b f a, GSubstK b g a) => GSubstK b (f :*: g) a where gsubstK nm val (f :*: g) = gsubstK nm val f :*: gsubstK nm val g gsubstsK ss (f :*: g) = gsubstsK ss f :*: gsubstsK ss g + gsubstBvsK ctx ss (f :*: g) = gsubstBvsK ctx ss f :*: gsubstBvsK ctx ss g instance (GSubstK b f a, GSubstK b g a) => GSubstK b (f :+: g) a where gsubstK nm val (L1 f) = L1 $ gsubstK nm val f @@ -461,10 +474,15 @@ gsubstsK ss (L1 f) = L1 $ gsubstsK ss f gsubstsK ss (R1 g) = R1 $ gsubstsK ss g + gsubstBvsK ctx ss (L1 f) = L1 $ gsubstBvsK ctx ss f + gsubstBvsK ctx ss (R1 g) = R1 $ gsubstBvsK ctx ss g + instance ((Interpret c a) => GSubstK b f a) => GSubstK b (c :=>: f) a where gsubstK nm val (SuchThat f) = SuchThat $ gsubstK nm val f gsubstsK ss (SuchThat f) = SuchThat $ gsubstsK ss f + gsubstBvsK ctx ss (SuchThat f) = SuchThat $ gsubstBvsK ctx ss f -instance (forall (t :: k). GSubstK b f (t :&&: a)) => GSubstK b (Exists k f) a where +instance (forall (t :: k). GSubstK b f (t ':&&: a)) => GSubstK b (Exists k f) a where gsubstK nm val (Exists f) = Exists $ gsubstK nm val f gsubstsK ss (Exists f) = Exists $ gsubstsK ss f + gsubstBvsK ctx ss (Exists f) = Exists $ gsubstBvsK ctx ss f diff --git a/src/Unbound/Generics/LocallyNameless/Kind/Example.hs b/src/Unbound/Generics/LocallyNameless/Kind/Example.hs --- a/src/Unbound/Generics/LocallyNameless/Kind/Example.hs +++ b/src/Unbound/Generics/LocallyNameless/Kind/Example.hs @@ -1,24 +1,22 @@ -{-# language GADTs #-} -{-# language StandaloneDeriving #-} -{-# language TypeOperators #-} +{-# language DataKinds #-} +{-# language DerivingVia #-} +{-# language FlexibleInstances #-} +{-# language GADTs #-} {-# language MultiParamTypeClasses #-} -{-# language FlexibleInstances #-} -{-# language TypeFamilies #-} -{-# language DataKinds #-} {-# language QuantifiedConstraints #-} -{-# language TypeApplications #-} -{-# language ScopedTypeVariables #-} -{-# language TemplateHaskell #-} -{-# language DerivingVia #-} +{-# language ScopedTypeVariables #-} +{-# language StandaloneDeriving #-} +{-# language TemplateHaskell #-} +{-# language TypeApplications #-} +{-# language TypeFamilies #-} +{-# language TypeOperators #-} -- | Example of how to use `unbound-kind-generics` module Unbound.Generics.LocallyNameless.Kind.Example where -import Data.Typeable (Typeable) -import qualified Data.Typeable as T -import Generics.Kind -import Generics.Kind.TH -import Unbound.Generics.LocallyNameless -import Unbound.Generics.LocallyNameless.Kind.Derive +import Data.Typeable (Typeable) +import Generics.Kind.TH +import Unbound.Generics.LocallyNameless +import Unbound.Generics.LocallyNameless.Kind.Derive -- | Variables stand for expressions type Var t = Name (Expr t) @@ -26,14 +24,14 @@ -- | Well-typed lambda expressions data Expr t where V :: Var t -> Expr t - Lam :: (Typeable a, Typeable b) => (Bind (Var a) (Expr b)) -> Expr (a -> b) + Lam :: (Typeable a, Typeable b) => Bind (Var a) (Expr b) -> Expr (a -> b) App :: (Typeable a) => Expr (a -> b) -> Expr a -> Expr b $(deriveGenericK ''Expr) eval :: Typeable t => Expr t -> FreshM (Expr t) eval (V x) = error $ "unbound variable " ++ show x -eval e@(Lam {}) = return e +eval e@Lam {} = return e eval (App e1 e2) = do v1 <- eval e1 v2 <- eval e2 @@ -61,13 +59,13 @@ type RepK (Expr t) = ((Field (Kon (Name (Expr t))))) :+: - (Exists (*) {- Var1 = a -} ((Typeable :$: Var0) :=>: - (Exists (*) {- Var0 = b -} ((Typeable :$: Var0) :=>: + (Exists Type {- Var1 = a -} ((Typeable :$: Var0) :=>: + (Exists Type {- Var0 = b -} ((Typeable :$: Var0) :=>: (((Kon t) :~: ((->) :$: Var1 :@: Var0)) :=>: (Field (Bind :$: (Name :$: (Expr :$: Var1)) :@: (Expr :$: Var0)))) )))) :+: - (Exists (*) {- Var0 = a -} ( + (Exists Type {- Var0 = a -} ( (Typeable :$: Var0) :=>: ((Field (Expr :$: ((->) :$: Var0 :@: (Kon t)))) :*: Field (Expr :$: Var0)) )) @@ -103,3 +101,4 @@ isvar _ = Nothing subst = gsubstDefK substs = gsubstsDefK + substBvs = gsubstBvsDefK diff --git a/unbound-kind-generics.cabal b/unbound-kind-generics.cabal --- a/unbound-kind-generics.cabal +++ b/unbound-kind-generics.cabal @@ -4,7 +4,7 @@ -- http://haskell.org/cabal/users-guide/ name: unbound-kind-generics -version: 0.2.1.0 +version: 0.2.1.1 synopsis: Support for programming with names and binders using kind-generics description: Specify the binding structure of your data type with an expressive set of type combinators, and unbound-generics @@ -31,6 +31,7 @@ Unbound.Generics.LocallyNameless.Kind.Example -- other-modules: -- other-extensions: - build-depends: base >= 4.12 && < 5, unbound-generics, kind-generics >= 0.4, kind-generics-th + build-depends: base >= 4.12 && < 5, unbound-generics >= 0.4, kind-generics >= 0.4, kind-generics-th hs-source-dirs: src default-language: Haskell2010 + ghc-options: -Wall