unbound-kind-generics (empty) → 0.2.0.0
raw patch · 6 files changed
+623/−0 lines, 6 filesdep +basedep +kind-genericsdep +kind-generics-thsetup-changed
Dependencies added: base, kind-generics, kind-generics-th, unbound-generics
Files
- CHANGELOG.md +5/−0
- LICENSE +30/−0
- Setup.hs +2/−0
- src/Unbound/Generics/LocallyNameless/Kind/Derive.hs +445/−0
- src/Unbound/Generics/LocallyNameless/Kind/Example.hs +105/−0
- unbound-kind-generics.cabal +36/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for unbound-kind-generics++## 0.1.0.0 -- YYYY-mm-dd++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2018, Alejandro Serrano++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Alejandro Serrano nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Unbound/Generics/LocallyNameless/Kind/Derive.hs view
@@ -0,0 +1,445 @@+{-# language TypeOperators #-}+{-# language MultiParamTypeClasses #-}+{-# language FlexibleInstances #-}+{-# language FlexibleContexts #-}+{-# language PolyKinds #-}+{-# language DataKinds #-}+{-# language UndecidableInstances #-}+{-# language QuantifiedConstraints #-}+{-# language GADTs #-}+{-# language ScopedTypeVariables #-}+{-# language TypeApplications #-}+{-# language ConstraintKinds #-}+module Unbound.Generics.LocallyNameless.Kind.Derive (+ -- Default definitions for 'Alpha'+ aeqDefK+, fvAnyDefK+, closeDefK+, openDefK+, isPatDefK+, isTermDefK+, isEmbedDefK+, nthPatFindDefK+, namePatFindDefK+, swapsDefK+, lfreshenDefK+, freshenDefK+, acompareDefK+ -- Default definitions for 'Subst'+, buildSubstName+, gsubstDefK+, gsubstsDefK+) 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 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++type GenericAlpha a = (GenericK a, GAlphaK (RepK a) LoT0 LoT0)++aeqDefK :: forall a. (GenericAlpha a)+ => AlphaCtx -> a -> a -> Bool+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+closeDefK :: forall a. (GenericAlpha a)+ => 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+isPatDefK :: forall a. (GenericAlpha a)+ => a -> DisjointSet AnyName+isPatDefK = gisPatK . fromK @_ @a @LoT0+isTermDefK :: forall a. (GenericAlpha a)+ => a -> All+isTermDefK = gisTermK . fromK @_ @a @LoT0+isEmbedDefK :: a -> Bool+isEmbedDefK _ = False+nthPatFindDefK :: forall a. (GenericAlpha a)+ => a -> NthPatFind+nthPatFindDefK = gnthPatFindK . fromK @_ @a @LoT0+namePatFindDefK :: forall a. (GenericAlpha a)+ => a -> NamePatFind+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+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)+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+acompareDefK :: forall a. (GenericAlpha a)+ => AlphaCtx -> a -> a -> Ordering+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+ gaeqK :: AlphaCtx -> f a -> f b -> Bool++ gfvAnyK :: (a ~ b, Contravariant g, Applicative g)+ => AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)++ gcloseK :: a ~ b => AlphaCtx -> NamePatFind -> f a -> f a+ gopenK :: a ~ b => AlphaCtx -> NthPatFind -> f a -> f a++ gisPatK :: a ~ b => f a -> DisjointSet AnyName+ gisTermK :: a ~ b => f a -> All++ gnthPatFindK :: a ~ b => f a -> NthPatFind+ gnamePatFindK :: a ~ b => f a -> NamePatFind++ gswapsK :: a ~ b => AlphaCtx -> Perm AnyName -> f a -> f a+ gfreshenK :: (a ~ b, Fresh m) => AlphaCtx -> f a -> FFM m (f a, Perm AnyName)++ glfreshenK :: (a ~ b, LFresh m) => AlphaCtx -> f a -> (f a -> Perm AnyName -> m c) -> m c++ gacompareK :: AlphaCtx -> f a -> f b -> Ordering++instance forall t a b.+ (Alpha (Interpret t a), Alpha (Interpret t b),+ Typeable (Interpret t a), Typeable (Interpret t b))+ => GAlphaK (Field t) a b where+ gaeqK ctx (Field c1) (Field c2) =+ case eqTypeRep (typeRep @(Interpret t a)) (typeRep @(Interpret t b)) of+ Nothing -> False+ Just HRefl -> aeq' ctx c1 c2+ {-# INLINE gaeqK #-}++ gfvAnyK ctx nfn = fmap Field . fvAny' ctx nfn . unField+ {-# INLINE gfvAnyK #-}++ gcloseK ctx b = Field . close ctx b . unField+ {-# INLINE gcloseK #-}+ gopenK ctx b = Field . open ctx b . unField+ {-# INLINE gopenK #-}++ gisPatK = isPat . unField+ {-# INLINE gisPatK #-}+ gisTermK = isTerm . unField+ {-# INLINE gisTermK #-}++ gnthPatFindK = nthPatFind . unField+ {-# INLINE gnthPatFindK #-}+ gnamePatFindK = namePatFind . unField+ {-# INLINE gnamePatFindK #-}++ gswapsK ctx perm = Field . swaps' ctx perm . unField+ {-# INLINE gswapsK #-}+ gfreshenK ctx = liftM (first Field) . liftFFM . freshen' ctx . unField+ {-# INLINE gfreshenK #-}++ glfreshenK ctx (Field c) cont = lfreshen' ctx c (cont . Field)+ {-# INLINE glfreshenK #-}++ gacompareK ctx (Field c1) (Field c2) =+ case eqTypeRep (typeRep @(Interpret t a)) (typeRep @(Interpret t b)) of+ Nothing -> compare (SomeTypeRep (typeRep @(Interpret t a)))+ (SomeTypeRep (typeRep @(Interpret t b)))+ Just HRefl -> acompare' ctx c1 c2++instance GAlphaK f a b => GAlphaK (M1 i d f) a b where+ gaeqK ctx (M1 f1) (M1 f2) = gaeqK ctx f1 f2+ {-# INLINE gaeqK #-}++ gfvAnyK ctx nfn = fmap M1 . gfvAnyK ctx nfn . unM1+ {-# INLINE gfvAnyK #-}++ gcloseK ctx b = M1 . gcloseK ctx b . unM1+ {-# INLINE gcloseK #-}+ gopenK ctx b = M1 . gopenK ctx b . unM1+ {-# INLINE gopenK #-}++ gisPatK = gisPatK . unM1+ {-# INLINE gisPatK #-}+ gisTermK = gisTermK . unM1+ {-# INLINE gisTermK #-}++ gnthPatFindK = gnthPatFindK . unM1+ {-# INLINE gnthPatFindK #-}+ gnamePatFindK = gnamePatFindK . unM1+ {-# INLINE gnamePatFindK #-}++ gswapsK ctx perm = M1 . gswapsK ctx perm . unM1+ {-# INLINE gswapsK #-}+ gfreshenK ctx = liftM (first M1) . gfreshenK ctx . unM1+ {-# INLINE gfreshenK #-}++ glfreshenK ctx (M1 f) cont =+ glfreshenK ctx f (cont . M1)+ {-# INLINE glfreshenK #-}++ gacompareK ctx (M1 f1) (M1 f2) = gacompareK ctx f1 f2++instance GAlphaK U1 a b where+ gaeqK _ctx _ _ = True+ {-# INLINE gaeqK #-}++ gfvAnyK _ctx _nfn _ = pure U1++ gcloseK _ctx _b _ = U1+ gopenK _ctx _b _ = U1++ gisPatK _ = mempty+ gisTermK _ = mempty++ gnthPatFindK _ = mempty+ gnamePatFindK _ = mempty++ gswapsK _ctx _perm _ = U1+ gfreshenK _ctx _ = return (U1, mempty)+ {-# INLINE gfreshenK #-}++ glfreshenK _ctx _ cont = cont U1 mempty++ gacompareK _ctx _ _ = EQ++instance (GAlphaK f a b, GAlphaK g a b) => GAlphaK (f :*: g) a b where+ gaeqK ctx (f1 :*: g1) (f2 :*: g2) =+ gaeqK ctx f1 f2 && gaeqK ctx g1 g2+ {-# INLINE gaeqK #-}++ gfvAnyK ctx nfn (f :*: g) = (:*:) <$> gfvAnyK ctx nfn f+ <*> gfvAnyK ctx nfn g+ {-# INLINE gfvAnyK #-}++ gcloseK ctx b (f :*: g) = gcloseK ctx b f :*: gcloseK ctx b g+ {-# INLINE gcloseK #-}+ gopenK ctx b (f :*: g) = gopenK ctx b f :*: gopenK ctx b g+ {-# INLINE gopenK #-}++ gisPatK (f :*: g) = gisPatK f <> gisPatK g+ {-# INLINE gisPatK #-}+ gisTermK (f :*: g) = gisTermK f <> gisTermK g+ {-# INLINE gisTermK #-}++ gnthPatFindK (f :*: g) = gnthPatFindK f <> gnthPatFindK g+ {-# INLINE gnthPatFindK #-}+ gnamePatFindK (f :*: g) = gnamePatFindK f <> gnamePatFindK g+ {-# INLINE gnamePatFindK #-}++ gswapsK ctx perm (f :*: g) =+ gswapsK ctx perm f :*: gswapsK ctx perm g+ {-# INLINE gswapsK #-}++ gfreshenK ctx (f :*: g) = do+ ~(g', perm2) <- gfreshenK ctx g+ ~(f', perm1) <- gfreshenK ctx (gswapsK ctx perm2 f)+ return (f' :*: g', perm1 <> perm2)+ {-# INLINE gfreshenK #-}++ glfreshenK ctx (f :*: g) cont =+ glfreshenK ctx g $ \g' perm2 ->+ glfreshenK ctx (gswapsK ctx perm2 f) $ \f' perm1 ->+ cont (f' :*: g') (perm1 <> perm2)+ {-# INLINE glfreshenK #-}++ gacompareK ctx (f1 :*: g1) (f2 :*: 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+ gaeqK ctx (R1 g1) (R1 g2) = gaeqK ctx g1 g2+ gaeqK _ctx _ _ = False+ {-# INLINE gaeqK #-}++ gfvAnyK ctx nfn (L1 f) = fmap L1 (gfvAnyK ctx nfn f)+ gfvAnyK ctx nfn (R1 g) = fmap R1 (gfvAnyK ctx nfn g)+ {-# INLINE gfvAnyK #-}++ gcloseK ctx b (L1 f) = L1 (gcloseK ctx b f)+ gcloseK ctx b (R1 g) = R1 (gcloseK ctx b g)+ {-# INLINE gcloseK #-}+ gopenK ctx b (L1 f) = L1 (gopenK ctx b f)+ gopenK ctx b (R1 g) = R1 (gopenK ctx b g)+ {-# INLINE gopenK #-}++ gisPatK (L1 f) = gisPatK f+ gisPatK (R1 g) = gisPatK g+ {-# INLINE gisPatK #-}++ gisTermK (L1 f) = gisTermK f+ gisTermK (R1 g) = gisTermK g+ {-# INLINE gisTermK #-}++ gnthPatFindK (L1 f) = gnthPatFindK f+ gnthPatFindK (R1 g) = gnthPatFindK g+ {-# INLINE gnthPatFindK #-}++ gnamePatFindK (L1 f) = gnamePatFindK f+ gnamePatFindK (R1 g) = gnamePatFindK g+ {-# INLINE gnamePatFindK #-}++ gswapsK ctx perm (L1 f) = L1 (gswapsK ctx perm f)+ 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)+ {-# INLINE gfreshenK #-}++ glfreshenK ctx (L1 f) cont =+ glfreshenK ctx f (cont . L1)+ glfreshenK ctx (R1 g) cont =+ glfreshenK ctx g (cont . R1)+ {-# INLINE glfreshenK #-}++ gacompareK _ctx (L1 _) (R1 _) = LT+ gacompareK _ctx (R1 _) (L1 _) = GT+ gacompareK ctx (L1 f1) (L1 f2) = gacompareK ctx f1 f2+ gacompareK ctx (R1 g1) (R1 g2) = gacompareK ctx g1 g2+ {-# INLINE gacompareK #-}++instance ((Interpret c a, Interpret c b) => GAlphaK f a b)+ => GAlphaK (c :=>: f) a b where+ gaeqK ctx (SuchThat f1) (SuchThat f2) = gaeqK ctx f1 f2+ {-# INLINE gaeqK #-}++ gfvAnyK ctx nfn (SuchThat f) = fmap SuchThat (gfvAnyK ctx nfn f)+ {-# INLINE gfvAnyK #-}++ gcloseK ctx b (SuchThat f) = SuchThat (gcloseK ctx b f)+ {-# INLINE gcloseK #-}+ gopenK ctx b (SuchThat f) = SuchThat (gopenK ctx b f)+ {-# INLINE gopenK #-}++ gisPatK (SuchThat f) = gisPatK f+ {-# INLINE gisPatK #-}++ gisTermK (SuchThat f) = gisTermK f+ {-# INLINE gisTermK #-}++ gnthPatFindK (SuchThat f) = gnthPatFindK f+ {-# INLINE gnthPatFindK #-}++ gnamePatFindK (SuchThat f) = gnamePatFindK f+ {-# INLINE gnamePatFindK #-}++ gswapsK ctx perm (SuchThat f) = SuchThat (gswapsK ctx perm f)+ {-# INLINE gswapsK #-}++ gfreshenK ctx (SuchThat f) = liftM (first SuchThat) (gfreshenK ctx f)+ {-# INLINE gfreshenK #-}++ glfreshenK ctx (SuchThat f) cont = glfreshenK ctx f (cont . SuchThat)+ {-# INLINE glfreshenK #-}++ gacompareK ctx (SuchThat f1) (SuchThat f2) = gacompareK ctx f1 f2+ {-# INLINE gacompareK #-}++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+ {-# INLINE gaeqK #-}++ gfvAnyK ctx nfn (Exists f) = fmap Exists (gfvAnyK ctx nfn f)+ {-# INLINE gfvAnyK #-}++ gcloseK ctx b (Exists f) = Exists (gcloseK ctx b f)+ {-# INLINE gcloseK #-}+ gopenK ctx b (Exists f) = Exists (gopenK ctx b f)+ {-# INLINE gopenK #-}++ gisPatK (Exists f) = gisPatK f+ {-# INLINE gisPatK #-}++ gisTermK (Exists f) = gisTermK f+ {-# INLINE gisTermK #-}++ gnthPatFindK (Exists f) = gnthPatFindK f+ {-# INLINE gnthPatFindK #-}++ gnamePatFindK (Exists f) = gnamePatFindK f+ {-# INLINE gnamePatFindK #-}++ gswapsK ctx perm (Exists f) = Exists (gswapsK ctx perm f)+ {-# INLINE gswapsK #-}++ gfreshenK ctx (Exists f) = liftM (first Exists) (gfreshenK ctx f)+ {-# INLINE gfreshenK #-}++ glfreshenK ctx (Exists f) cont = glfreshenK ctx f (cont . Exists)+ {-# INLINE glfreshenK #-}++ gacompareK ctx (Exists f1) (Exists f2) = gacompareK ctx f1 f2++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)+ 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)+ else error $ "Cannot substitute for bound variable " ++ show n++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)+ | otherwise =+ error $ "Cannot substitute for bound variable in: " ++ show (map fst ss)++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+ gsubstK :: Name b -> b -> f a -> f a+ gsubstsK :: [(Name b, 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++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++instance GSubstK b U1 a where+ gsubstK _nm _val _ = U1+ gsubstsK _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++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+ gsubstK nm val (R1 g) = R1 $ gsubstK nm val g++ gsubstsK ss (L1 f) = L1 $ gsubstsK ss f+ gsubstsK ss (R1 g) = R1 $ gsubstsK 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++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
+ src/Unbound/Generics/LocallyNameless/Kind/Example.hs view
@@ -0,0 +1,105 @@+{-# language GADTs #-}+{-# language StandaloneDeriving #-}+{-# language TypeOperators #-}+{-# language MultiParamTypeClasses #-}+{-# language FlexibleInstances #-}+{-# language TypeFamilies #-}+{-# language DataKinds #-}+{-# language QuantifiedConstraints #-}+{-# language TypeApplications #-}+{-# language ScopedTypeVariables #-}+{-# language TemplateHaskell #-}+-- | 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++-- | Variables stand for expressions+type Var t = Name (Expr t)++-- | 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)+ App :: (Typeable a) => Expr (a -> b) -> Expr a -> Expr b++$(deriveGenericK ''Expr)++eval :: Typeable t => Expr t -> FreshM (Expr t)+eval (V x) = fail $ "unbound variable " ++ show x+eval e@(Lam {}) = return e+eval (App e1 e2) = do+ v1 <- eval e1+ v2 <- eval e2+ case v1 of+ (Lam bnd) -> do+ -- open the lambda by picking a fresh name for the bound variable x in body+ (x, body) <- unbind bnd+ let body' = subst x v2 body+ eval body'+ _ -> fail "application of non-lambda"++example :: forall a. Typeable a => Expr (a -> a)+example =+ let x = s2n "x"+ y = s2n "y"+ e1 = Lam @(a -> a) $ bind x (Lam @(a -> a) $ bind y (V x)) -- \x y -> x+ z = s2n "z"+ e2 = Lam @a $ bind z (V z) -- \z -> z+ in runFreshM $ eval (App (App e1 e2) e2)++deriving instance Show (Expr t)++++{-+instance GenericK (Expr t) LoT0 where+ type RepK (Expr t) =+ ((Field (Kon (Name (Expr t)))))+ :+:+ (Exists (*) {- Var1 = a -} ((Typeable :$: Var0) :=>:+ (Exists (*) {- Var0 = b -} ((Typeable :$: Var0) :=>:+ (((Kon t) :~: ((->) :$: Var1 :@: Var0))+ :=>:+ (Field (Bind :$: (Name :$: (Expr :$: Var1)) :@: (Expr :$: Var0)))) ))))+ :+:+ (Exists (*) {- Var0 = a -} (+ (Typeable :$: Var0)+ :=>:+ ((Field (Expr :$: ((->) :$: Var0 :@: (Kon t)))) :*: Field (Expr :$: Var0)) ))++ fromK (V v) = L1 (Field v)+ fromK (Lam b) = R1 (L1 (Exists (SuchThat (Exists (SuchThat (SuchThat (Field b)))))))+ fromK (App x y) = R1 (R1 (Exists (SuchThat (Field x :*: Field y))))++ toK (L1 (Field v)) = V v+ toK (R1 (L1 (Exists (SuchThat (Exists (SuchThat (SuchThat (Field b)))))))) = Lam b+ toK (R1 (R1 (Exists (SuchThat (Field x :*: Field y))))) = App x y+-}++instance Typeable t => Alpha (Expr t) where+ aeq' = aeqDefK+ fvAny' = fvAnyDefK+ close = closeDefK+ open = openDefK+ isPat = isPatDefK+ isTerm = isTermDefK+ isEmbed = isEmbedDefK+ nthPatFind = nthPatFindDefK+ namePatFind = namePatFindDefK+ swaps' = swapsDefK+ lfreshen' = lfreshenDefK+ freshen' = freshenDefK+ acompare' = acompareDefK++instance (Typeable small, Typeable big)+ => Subst (Expr small) (Expr big) where+ isvar (V x) = buildSubstName x+ isvar _ = Nothing+ subst = gsubstDefK+ substs = gsubstsDefK
+ unbound-kind-generics.cabal view
@@ -0,0 +1,36 @@+cabal-version: >=1.10+-- Initial package description 'unbound-kind-generics.cabal' generated by+-- 'cabal init'. For further documentation, see+-- http://haskell.org/cabal/users-guide/++name: unbound-kind-generics+version: 0.2.0.0+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+ handles the rest! Automatically derives+ alpha-equivalence, free variable calculation,+ capture-avoiding substitution, and more. See+ @Unbound.Generics.LocallyNameless.Kind@ to get started.+ .+ This is an independent re-implementation of <http://hackage.haskell.org/package/unbound-generics unbound-generics>+ but using <https://hackage.haskell.org/package/kind-generics kind-generics>+ instead of <https://hackage.haskell.org/package/base/docs/GHC-Generics.html GHC Generics>.+-- bug-reports:+license: BSD3+license-file: LICENSE+author: Alejandro Serrano+maintainer: trupill@gmail.com+-- copyright:+category: Language+build-type: Simple+extra-source-files: CHANGELOG.md++library+ exposed-modules: Unbound.Generics.LocallyNameless.Kind.Derive,+ Unbound.Generics.LocallyNameless.Kind.Example+ -- other-modules:+ -- other-extensions:+ build-depends: base >= 4.12 && < 5, unbound-generics, kind-generics >= 0.4, kind-generics-th+ hs-source-dirs: src+ default-language: Haskell2010