unbound 0.4.3.1 → 0.4.4

raw patch · 9 files changed

+122/−25 lines, 9 filesnew-uploader

Files

• README +2/−2
• Unbound/LocallyNameless/Alpha.hs +10/−9
• Unbound/LocallyNameless/Fresh.hs +29/−2
• Unbound/LocallyNameless/Name.hs +1/−1
• Unbound/LocallyNameless/Subst.hs +1/−0
• Unbound/Util.hs +3/−2
• examples/Issue28.hs +65/−0
• test/Test.hs +4/−1
• unbound.cabal +7/−8

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

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

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

@@ -12,7 +12,7 @@ -- |
 -- Module      :  Unbound.LocallyNameless.Name
 -- License     :  BSD-like (see LICENSE)
--- Maintainer  :  Brent Yorgey <byorgey@cis.upenn.edu>
+-- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>
 -- Portability :  GHC only
 --
 -- An implementation of names in a locally nameless representation.

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

@@ -4,7 +4,7 @@ -- | -- Module      :  Unbound.Util -- License     :  BSD-like (see LICENSE)--- Maintainer  :  Brent Yorgey <byorgey@cis.upenn.edu>+-- Maintainer  :  Brent Yorgey <byorgey@cis.upenn.edu>, Stephanie Weirich <sweirich@cis.upenn.edu> -- 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.

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

@@ -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."+       

@@ -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 <byorgey@cis.upenn.edu>-                Stephanie Weirich <sweirich@cis.upenn.edu>-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 <sweirich@cis.upenn.edu>, Brent Yorgey <byorgey@cis.upenn.edu> +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,