diff --git a/README b/README --- a/README +++ b/README @@ -1,6 +1,6 @@ ----------------------------------------------------------------------------- -- --- Copyright : (c) 2010-2011, Unbound team (see LICENSE) +-- Copyright : (c) 2010-2015, Unbound team (see LICENSE) -- License : BSD3 -- -- Maintainer : sweirich@cis.upenn.edu, byorgey@cis.upenn.edu @@ -14,7 +14,7 @@ derives alpha-equivalence, free variable calculation, capture-avoiding substitution, and more. -To install (requires GHC 7), just +To install: cabal install unbound diff --git a/Unbound/LocallyNameless/Alpha.hs b/Unbound/LocallyNameless/Alpha.hs --- a/Unbound/LocallyNameless/Alpha.hs +++ b/Unbound/LocallyNameless/Alpha.hs @@ -296,8 +296,9 @@ incr c = c { level = level c + 1 } decr :: AlphaCtx -> AlphaCtx -decr c = if level c == 0 then error "Too many outers" - else c { level = level c - 1 } +decr c = -- if level c == 0 then error "Too many outers" + -- else + c { level = level c - 1 } pat :: AlphaCtx -> AlphaCtx @@ -336,13 +337,13 @@ isTermD :: a -> Bool, isEmbedD :: a -> Bool, swapsD :: AlphaCtx -> Perm AnyName -> a -> a, - fvD :: Collection f => AlphaCtx -> a -> f AnyName, - freshenD :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName), - lfreshenD :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b, + fvD :: forall f. Collection f => AlphaCtx -> a -> f AnyName, + freshenD :: forall m. Fresh m => AlphaCtx -> a -> m (a, Perm AnyName), + lfreshenD :: forall m b. LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b, aeqD :: AlphaCtx -> a -> a -> Bool, acompareD :: AlphaCtx -> a -> a -> Ordering, - closeD :: Alpha b => AlphaCtx -> b -> a -> a, - openD :: Alpha b => AlphaCtx -> b -> a -> a, + closeD :: forall b. Alpha b => AlphaCtx -> b -> a -> a, + openD :: forall b. Alpha b => AlphaCtx -> b -> a -> a, findpatD :: a -> AnyName -> FindResult, nthpatD :: a -> NthCont } @@ -578,7 +579,7 @@ Nothing -> error "Internal error in open: sort mismatch" open _ _ n = n - close c a nm@(Nm r _) | mode c == Term = + close c a nm@(Nm r _) | mode c == Term && level c >= 0 = case findpat a (AnyName nm) of Just x -> Bn r (level c) x Nothing -> nm @@ -857,4 +858,4 @@ instance (Alpha a, Alpha b,Alpha c, Alpha d, Alpha e) => Alpha (a,b,c,d,e) -instance (Rep a) => Alpha (R a) +instance (Rep a) => Alpha (R a) diff --git a/Unbound/LocallyNameless/Fresh.hs b/Unbound/LocallyNameless/Fresh.hs --- a/Unbound/LocallyNameless/Fresh.hs +++ b/Unbound/LocallyNameless/Fresh.hs @@ -2,10 +2,13 @@ , FlexibleInstances , FlexibleContexts , GeneralizedNewtypeDeriving - , OverlappingInstances , MultiParamTypeClasses , UndecidableInstances + , CPP #-} +#if __GLASGOW_HASKELL__ < 710 +{-# LANGUAGE OverlappingInstances #-} +#endif ---------------------------------------------------------------------- -- | -- Module : Unbound.LocallyNameless.Fresh @@ -48,10 +51,14 @@ import Control.Monad.Reader import qualified Control.Monad.State as St import Control.Monad.Identity -import Control.Applicative (Applicative) +import Control.Applicative (Applicative, Alternative) import Control.Monad.Trans.Cont +#if MIN_VERSION_transformers(0,4,0) +import Control.Monad.Trans.Except +#else import Control.Monad.Trans.Error +#endif import Control.Monad.Trans.Identity import Control.Monad.Trans.List import Control.Monad.Trans.Maybe @@ -81,7 +88,11 @@ -- still globally unused, and increments the index every time it is -- asked for a fresh name. newtype FreshMT m a = FreshMT { unFreshMT :: St.StateT Integer m a } +#if __GLASGOW_HASKELL__ >= 710 + deriving (Functor, Applicative, Alternative, Monad, MonadPlus, MonadIO, MonadFix) +#else deriving (Functor, Applicative, Monad, MonadPlus, MonadIO, MonadFix) +#endif -- | Run a 'FreshMT' computation (with the global index starting at zero). runFreshMT :: Monad m => FreshMT m a -> m a @@ -118,8 +129,13 @@ instance Fresh m => Fresh (ContT r m) where fresh = lift . fresh +#if MIN_VERSION_transformers(0,4,0) +instance Fresh m => Fresh (ExceptT e m) where + fresh = lift . fresh +#else instance (Error e, Fresh m) => Fresh (ErrorT e m) where fresh = lift . fresh +#endif instance Fresh m => Fresh (IdentityT m) where fresh = lift . fresh @@ -188,7 +204,11 @@ -- avoid, and when asked for a fresh one will choose the first numeric -- prefix of the given name which is currently unused. newtype LFreshMT m a = LFreshMT { unLFreshMT :: ReaderT (Set AnyName) m a } +#if __GLASGOW_HASKELL__ >= 710 + deriving (Functor, Applicative, Alternative, Monad, MonadIO, MonadPlus, MonadFix) +#else deriving (Functor, Applicative, Monad, MonadIO, MonadPlus, MonadFix) +#endif -- | Run an 'LFreshMT' computation in an empty context. runLFreshMT :: LFreshMT m a -> m a @@ -226,10 +246,17 @@ avoid = mapContT . avoid getAvoids = lift getAvoids +#if MIN_VERSION_transformers(0,4,0) +instance LFresh m => LFresh (ExceptT e m) where + lfresh = lift . lfresh + avoid = mapExceptT . avoid + getAvoids = lift getAvoids +#else instance (Error e, LFresh m) => LFresh (ErrorT e m) where lfresh = lift . lfresh avoid = mapErrorT . avoid getAvoids = lift getAvoids +#endif instance LFresh m => LFresh (IdentityT m) where lfresh = lift . lfresh diff --git a/Unbound/LocallyNameless/Name.hs b/Unbound/LocallyNameless/Name.hs --- a/Unbound/LocallyNameless/Name.hs +++ b/Unbound/LocallyNameless/Name.hs @@ -12,7 +12,7 @@ -- | -- Module : Unbound.LocallyNameless.Name -- License : BSD-like (see LICENSE) --- Maintainer : Brent Yorgey +-- Maintainer : Stephanie Weirich -- Portability : GHC only -- -- An implementation of names in a locally nameless representation. diff --git a/Unbound/LocallyNameless/Subst.hs b/Unbound/LocallyNameless/Subst.hs --- a/Unbound/LocallyNameless/Subst.hs +++ b/Unbound/LocallyNameless/Subst.hs @@ -140,5 +140,6 @@ instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b) +instance (Subst c a) => Subst c (Shift a) instance (Subst c a) => Subst c (Embed a) instance (Alpha a, Subst c a) => Subst c (Rec a) diff --git a/Unbound/Util.hs b/Unbound/Util.hs --- a/Unbound/Util.hs +++ b/Unbound/Util.hs @@ -4,7 +4,7 @@ -- | -- Module : Unbound.Util -- License : BSD-like (see LICENSE) --- Maintainer : Brent Yorgey +-- Maintainer : Brent Yorgey , Stephanie Weirich -- Portability : GHC only (-XKitchenSink) -- -- Various utilities for the Unbound library. @@ -80,7 +80,8 @@ newtype Multiset a = Multiset (M.Map a Int) instance F.Foldable Multiset where - fold (Multiset m) = M.foldrWithKey (\a n x -> mconcat (x : replicate n a)) mempty m + fold (Multiset m) = M.foldrWithKey (\a n x -> mconcat (x : replicate n a)) mempty m + foldMap f (Multiset m) = M.foldrWithKey (\a n x -> mconcat (x : replicate n (f a))) mempty m -- | Multisets are containers which preserve multiplicity but not -- ordering. diff --git a/examples/Issue28.hs b/examples/Issue28.hs new file mode 100644 --- /dev/null +++ b/examples/Issue28.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses #-} + +module Issue28 where + +import Unbound.LocallyNameless + +type Var = Name Term + +data Term + = V Var + | Unit + | Pi (Bind (Var, Embed Term) Term) + | LetRec (Bind (Rec Decl) Term) + deriving (Show) + +data Decl = + -- a recursive declaration x : A = m + -- where x may occur in m but not in A + Decl { + declVar :: Var + , declClass :: Shift (Embed Term) + , declVal :: Embed Term + } + deriving (Show) + +$(derive [''Term, ''Decl]) + +instance Alpha Term +instance Alpha Decl +instance Subst Term Decl +instance Subst Term Term where + isvar (V x) = Just (SubstName x) + isvar _ = Nothing + +x :: Var +x = s2n "x" + +letrec :: Decl -> Term -> Term +letrec d e = LetRec $ bind (rec d) e + +decl :: Var -> Term -> Term -> Decl +decl v klass e = Decl v (Shift (Embed klass)) (embed e) + + +m0 = letrec (decl x Unit Unit) Unit + +-- >> show m1 +-- "LetRec (<[Decl {declVar = x, declClass = {{V x}}, declVal = {V 0@0}}]> V 0@0)" +m1 = letrec (decl x (V x) (V x)) (V x) + +-- substitution shows that binding is as we expect, +-- >> subst x Unit m1 +-- "LetRec (<[Decl {declVar = x, declClass = {{Unit}}, declVal = {V 0@0}}]> V 0@0)" + + +-- >> show m2 +-- "Pi (<(x,{Unit})> LetRec (<[Decl {declVar = x, declClass = {{V 0@0}}, declVal = {V 0@0}}]> V 0@0))" +-- +-- looks a little strange, but the shift is still there +m2 = Pi (bind (x, embed Unit) m1) + + + + + diff --git a/test/Test.hs b/test/Test.hs --- a/test/Test.hs +++ b/test/Test.hs @@ -150,4 +150,7 @@ -- if match t1 t2 = Some p then swaps p t1 = t2 main :: IO () -main = do_tests +main = do + do_tests + putStrLn "Testing complete." + diff --git a/unbound.cabal b/unbound.cabal --- a/unbound.cabal +++ b/unbound.cabal @@ -1,14 +1,13 @@ name: unbound -version: 0.4.3.1 +version: 0.4.4 license: BSD3 license-file: LICENSE build-type: Simple cabal-version: >= 1.10 -tested-with: GHC == 7.0.4, GHC == 7.2.1, GHC == 7.4.1, GHC == 7.6.3 -author: Stephanie Weirich -maintainer: Brent Yorgey - Stephanie Weirich -homepage: http://code.google.com/p/replib/ +tested-with: GHC == 7.0.4, GHC == 7.2.1, GHC == 7.4.1, GHC == 7.6.3, GHC == 7.8.3, GHC == 7.10 +author: Stephanie Weirich, Brent Yorgey +maintainer: Stephanie Weirich , Brent Yorgey +homepage: https://github.com/sweirich/replib category: Language, Generics, Compilers/Interpreters extra-source-files: README, CHANGES, @@ -25,8 +24,8 @@ capture-avoiding substitution, and more. See "Unbound.LocallyNameless" to get started. source-repository head - type: svn - location: https://replib.googlecode.com/svn/trunk/ + type: git + location: https://github.com/sweirich/replib Library build-depends: base >= 4.3 && < 5,