unbound-kind-generics 0.2.1.0 → 0.2.1.1

raw patch · 3 files changed

+108/−90 lines, 3 filesdep ~unbound-genericsPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: unbound-generics

API changes (from Hackage documentation)

Files

• src/Unbound/Generics/LocallyNameless/Kind/Derive.hs +85/−67
• src/Unbound/Generics/LocallyNameless/Kind/Example.hs +20/−21
• unbound-kind-generics.cabal +3/−2

@@ -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

@@ -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

@@ -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