summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlejandroSerrano <>2019-09-10 21:15:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2019-09-10 21:15:00 (GMT)
commitd52ac75f8d759c9f83e7380af98756ad7b1320e0 (patch)
tree907c7b8a5163e4bcdf0c8444ef6332d720b24fdf
parentda2d373b5d5b62b356c54117aabb62eb3251b2d3 (diff)
version 0.2.1.0HEAD0.2.1.0master
-rw-r--r--src/Unbound/Generics/LocallyNameless/Kind/Derive.hs27
-rw-r--r--src/Unbound/Generics/LocallyNameless/Kind/Example.hs10
-rw-r--r--unbound-kind-generics.cabal4
3 files changed, 33 insertions, 8 deletions
diff --git a/src/Unbound/Generics/LocallyNameless/Kind/Derive.hs b/src/Unbound/Generics/LocallyNameless/Kind/Derive.hs
index 4cdcbd0..91ea566 100644
--- a/src/Unbound/Generics/LocallyNameless/Kind/Derive.hs
+++ b/src/Unbound/Generics/LocallyNameless/Kind/Derive.hs
@@ -11,8 +11,10 @@
{-# language TypeApplications #-}
{-# language ConstraintKinds #-}
module Unbound.Generics.LocallyNameless.Kind.Derive (
+ -- For use with DerivingVia
+ AutoAlpha(..)
-- Default definitions for 'Alpha'
- aeqDefK
+, aeqDefK
, fvAnyDefK
, closeDefK
, openDefK
@@ -50,6 +52,29 @@ import Generics.Kind
type GenericAlpha a = (GenericK a, GAlphaK (RepK a) LoT0 LoT0)
+newtype AutoAlpha a = AutoAlpha { unAutoAlpha :: a }
+ deriving (Eq, Show)
+
+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)
+ = AutoAlpha <$> fvAnyDefK ctx nfn x
+ close ctx npf = AutoAlpha . closeDefK ctx npf . unAutoAlpha
+ open ctx npf = AutoAlpha . openDefK ctx npf . unAutoAlpha
+ isPat = isPatDefK . unAutoAlpha
+ isTerm = isTermDefK . unAutoAlpha
+ isEmbed = isEmbedDefK . unAutoAlpha
+ 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)
+ freshen' ctx (AutoAlpha x)
+ = (\(y, p) -> (AutoAlpha y, p)) <$> 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)
diff --git a/src/Unbound/Generics/LocallyNameless/Kind/Example.hs b/src/Unbound/Generics/LocallyNameless/Kind/Example.hs
index 8a8594c..f331044 100644
--- a/src/Unbound/Generics/LocallyNameless/Kind/Example.hs
+++ b/src/Unbound/Generics/LocallyNameless/Kind/Example.hs
@@ -9,6 +9,7 @@
{-# language TypeApplications #-}
{-# language ScopedTypeVariables #-}
{-# language TemplateHaskell #-}
+{-# language DerivingVia #-}
-- | Example of how to use `unbound-kind-generics`
module Unbound.Generics.LocallyNameless.Kind.Example where
@@ -31,7 +32,7 @@ data Expr t where
$(deriveGenericK ''Expr)
eval :: Typeable t => Expr t -> FreshM (Expr t)
-eval (V x) = fail $ "unbound variable " ++ show x
+eval (V x) = error $ "unbound variable " ++ show x
eval e@(Lam {}) = return e
eval (App e1 e2) = do
v1 <- eval e1
@@ -42,7 +43,7 @@ eval (App e1 e2) = do
(x, body) <- unbind bnd
let body' = subst x v2 body
eval body'
- _ -> fail "application of non-lambda"
+ _ -> error "application of non-lambda"
example :: forall a. Typeable a => Expr (a -> a)
example =
@@ -55,8 +56,6 @@ example =
deriving instance Show (Expr t)
-
-
{-
instance GenericK (Expr t) LoT0 where
type RepK (Expr t) =
@@ -96,10 +95,11 @@ instance Typeable t => Alpha (Expr t) where
lfreshen' = lfreshenDefK
freshen' = freshenDefK
acompare' = acompareDefK
+-- deriving via (AutoAlpha (Expr t)) instance Typeable t => Alpha (Expr t)
instance (Typeable small, Typeable big)
=> Subst (Expr small) (Expr big) where
isvar (V x) = buildSubstName x
isvar _ = Nothing
subst = gsubstDefK
- substs = gsubstsDefK \ No newline at end of file
+ substs = gsubstsDefK
diff --git a/unbound-kind-generics.cabal b/unbound-kind-generics.cabal
index ea00ac3..c7f42f4 100644
--- a/unbound-kind-generics.cabal
+++ b/unbound-kind-generics.cabal
@@ -4,14 +4,14 @@ cabal-version: >=1.10
-- http://haskell.org/cabal/users-guide/
name: unbound-kind-generics
-version: 0.2.0.0
+version: 0.2.1.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.
+ @Unbound.Generics.LocallyNameless.Kind.Derive@ 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>