unbound 0.3.1 → 0.4

raw patch · 8 files changed

+69/−65 lines, 8 files

Files

• CHANGES +8/−0
• Unbound/LocallyNameless.hs +1/−1
• Unbound/LocallyNameless/Fresh.hs +26/−7
• Unbound/LocallyNameless/Ops.hs +5/−0
• Unbound/LocallyNameless/Subst.hs +20/−2
• Unbound/Util.hs +7/−0
• examples/LCTyped.hs +0/−53
• unbound.cabal +2/−2

@@ -41,3 +41,11 @@ Version 0.3.1: 25 August 2011    * Update to build on GHC 7.2.1++Version 0.4: 15 March 2012++  * Update to build on GHC 7.4.1+  +  * add MonadWriter instances for FreshMT and LFreshMT++  * Make 'getAvoids' function into a method of the LFresh class

@@ -239,7 +239,7 @@     --   can be freely combined with other standard monads and monad
     --   transformers from the @transformers@ library.
 
-    LFreshM, runLFreshM, getAvoids,
+    LFreshM, runLFreshM,
     LFreshMT, runLFreshMT,
 
     -- * The @Alpha@ class

@@ -32,7 +32,7 @@ 
     LFresh(..),
 
-    LFreshM, runLFreshM, contLFreshM, getAvoids,
+    LFreshM, runLFreshM, contLFreshM,
     LFreshMT(..), runLFreshMT, contLFreshMT
 
   ) where
@@ -64,6 +64,7 @@ import qualified Control.Monad.Error.Class as EC
 import qualified Control.Monad.State.Class as StC
 import qualified Control.Monad.Reader.Class as RC
+import qualified Control.Monad.Writer.Class as WC
 
 ------------------------------------------------------------
 -- Fresh
@@ -164,8 +165,11 @@   ask   = lift RC.ask
   local f = FreshMT . RC.local f . unFreshMT
 
----------------------------------------------------
--- LFresh
+instance WC.MonadWriter w m => WC.MonadWriter w (FreshMT m) where
+  tell   = lift . WC.tell
+  listen = FreshMT . WC.listen . unFreshMT
+  pass   = FreshMT . WC.pass . unFreshMT
+
 ---------------------------------------------------
 
 -- | This is the class of monads that support freshness in an
@@ -177,6 +181,8 @@   -- | Avoid the given names when freshening in the subcomputation,
   --   that is, add the given names to the in-scope set.
   avoid   :: [AnyName] -> m a -> m a
+  -- | Get the set of names currently being avoided.
+  getAvoids :: m (Set AnyName)
 
 -- | The LFresh monad transformer.  Keeps track of a set of names to
 -- avoid, and when asked for a fresh one will choose the first numeric
@@ -192,10 +198,6 @@ contLFreshMT :: LFreshMT m a -> Set AnyName -> m a
 contLFreshMT (LFreshMT m) = runReaderT m
 
--- | Get the set of names currently being avoided.
-getAvoids :: Monad m => LFreshMT m (Set AnyName)
-getAvoids = LFreshMT ask
-
 instance Monad m => LFresh (LFreshMT m) where
   lfresh nm = LFreshMT $ do
     let s = name2String nm
@@ -204,6 +206,8 @@                           (map (makeName s) [0..]))
   avoid names = LFreshMT . local (S.union (S.fromList names)) . unLFreshMT
 
+  getAvoids = LFreshMT ask
+
 -- | A convenient monad which is an instance of 'LFresh'.  It keeps
 --   track of a set of names to avoid, and when asked for a fresh one
 --   will choose the first unused numerical name.
@@ -220,42 +224,52 @@ instance LFresh m => LFresh (ContT r m) where
   lfresh = lift . lfresh
   avoid  = mapContT . avoid
+  getAvoids = lift getAvoids
 
 instance (Error e, LFresh m) => LFresh (ErrorT e m) where
   lfresh = lift . lfresh
   avoid  = mapErrorT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (IdentityT m) where
   lfresh = lift . lfresh
   avoid  = mapIdentityT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (ListT m) where
   lfresh = lift . lfresh
   avoid  = mapListT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (MaybeT m) where
   lfresh = lift . lfresh
   avoid  = mapMaybeT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (ReaderT r m) where
   lfresh = lift . lfresh
   avoid  = mapReaderT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (Lazy.StateT s m) where
   lfresh = lift . lfresh
   avoid  = Lazy.mapStateT . avoid
+  getAvoids = lift getAvoids
 
 instance LFresh m => LFresh (Strict.StateT s m) where
   lfresh = lift . lfresh
   avoid  = Strict.mapStateT . avoid
+  getAvoids = lift getAvoids
 
 instance (Monoid w, LFresh m) => LFresh (Lazy.WriterT w m) where
   lfresh = lift . lfresh
   avoid  = Lazy.mapWriterT . avoid
+  getAvoids = lift getAvoids
 
 instance (Monoid w, LFresh m) => LFresh (Strict.WriterT w m) where
   lfresh = lift . lfresh
   avoid  = Strict.mapWriterT . avoid
+  getAvoids = lift getAvoids
 
 -- Instances for applying LFreshMT to other monads
 
@@ -276,3 +290,8 @@ instance RC.MonadReader r m => RC.MonadReader r (LFreshMT m) where
   ask   = lift RC.ask
   local f = LFreshMT . mapReaderT (RC.local f) . unLFreshMT
+
+instance WC.MonadWriter w m => WC.MonadWriter w (LFreshMT m) where
+  tell   = lift . WC.tell
+  listen = LFreshMT . WC.listen . unLFreshMT
+  pass   = LFreshMT . WC.pass . unLFreshMT

@@ -1,5 +1,6 @@ {-# LANGUAGE TypeSynonymInstances            , FlexibleInstances+           , CPP   #-} {-# OPTIONS_GHC -fno-warn-orphans #-} ----------------------------------------------------------------------@@ -25,6 +26,10 @@ import Data.Maybe (catMaybes) import Data.List  (sortBy) import Data.Ord   (comparing)++#if MIN_VERSION_base(4,5,0)+import Data.Monoid+#endif  import Control.Monad (liftM) import qualified Text.Read as R

@@ -30,6 +30,10 @@ -- | See 'isvar'. data SubstName a b where   SubstName :: (a ~ b) => Name a -> SubstName a b+  +-- | See 'isCoerceVar'  +data SubstCoerce a b where  +  SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b  -- | The @Subst@ class governs capture-avoiding substitution.  To --   derive this class, you only need to indicate where the variables@@ -43,6 +47,13 @@   --   returns 'Nothing'.   isvar :: a -> Maybe (SubstName a b)   isvar _ = Nothing+  +  -- | This is an alternative version to 'isvar', useable in the case +  --   that the substituted argument doesn't have *exactly* the same type+  --   as the term it should be substituted into.+  --   The default implementation always returns 'Nothing'.+  isCoerceVar :: a -> Maybe (SubstCoerce a b)+  isCoerceVar _ = Nothing    -- | @'subst' nm sub tm@ substitutes @sub@ for @nm@ in @tm@.  It has   --   a default generic implementation in terms of @isvar@.@@ -50,7 +61,9 @@   subst n u x | isFree n =      case (isvar x :: Maybe (SubstName a b)) of         Just (SubstName m) -> if  m == n then u else x-        Nothing -> substR1 rep1 n u x+        Nothing -> case (isCoerceVar x :: Maybe (SubstCoerce a b)) of +           Just (SubstCoerce m f) -> if m == n then maybe x id (f u) else x+           Nothing -> substR1 rep1 n u x   subst m _ _ = error $ "Cannot substitute for bound variable " ++ show m    -- | Perform several simultaneous substitutions.  This method also@@ -63,7 +76,12 @@           case find ((==m) . fst) ss of             Just (_, u) -> u             Nothing     -> x-        Nothing -> substsR1 rep1 ss x+        Nothing -> case isCoerceVar x :: Maybe (SubstCoerce a b) of +            Just (SubstCoerce m f) ->+              case find ((==m) . fst) ss of +                  Just (_, u) -> maybe x id (f u)+                  Nothing -> x+            Nothing -> substsR1 rep1 ss x     | otherwise =       error $ "Cannot substitute for bound variable in: " ++ show (map fst ss) 

@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ ---------------------------------------------------------------------- -- | -- Module      :  Unbound.Util@@ -21,8 +23,13 @@ -- Convenient Monoid syntax ------------------------------------------------------------ +-- As of base-4.5, (<>) is exported by Data.Monoid.++#if MIN_VERSION_base(4,5,0)+#else (<>) :: Monoid m => m -> m -> m (<>) = mappend+#endif  ------------------------------------------------------------ -- Collections

@@ -1,53 +0,0 @@-{-# LANGUAGE GADTs-           , TemplateHaskell-           , KindSignatures-           , ScopedTypeVariables-           , TypeOperators-  #-}--module LCTyped where--import Unbound.LocallyNameless-import Data.Type.Equality--import Unsafe.Coerce (unsafeCoerce)------------------------------------------------------------------data Res1 c a where-  Result1   :: Rep b => a :=: (c b) -> Res1 c a-  NoResult1 :: Res1 c a--destr1 :: R a -> R (c d) -> Res1 c a-destr1 (Data (DT s1 ((_ :: R b) :+: MNil)) _)-       (Data (DT s2 _) _)-  | s1 == s2  = Result1 (unsafeCoerce Refl :: a :=: (c b))-  | otherwise = NoResult1-destr1 _ _ = NoResult1--data Res2 c2 a where-  Result2   :: (Rep d, Rep e) => a :=: (c2 d e) -> Res2 c2 a-  NoResult2 :: Res2 c2 a--destr2 :: R a -> R (c2 d e) -> Res2 c2 a-destr2 (Data (DT s1 ((_ :: R d) :+: (_ :: R e) :+: MNil)) _)-       (Data (DT s2 _) _)-  | s1 == s2  = Result2 (unsafeCoerce Refl :: a :=: (c2 d e))-  | otherwise = NoResult2-destr2 _ _ = NoResult2-----------------------------------------------------------------data V :: * -> * -> * where-  VZ :: V (a,env) a-  VS :: V env a -> V (b,env) a--data Tm :: * -> * -> * where-  Var :: V env a -> Tm env a-  Lam :: Tm (a,env) b -> Tm env (a -> b)-  App :: Tm env (a -> b) -> Tm env a -> Tm env b--$(derive [''V, ''Tm])

@@ -1,10 +1,10 @@ name:           unbound-version:        0.3.1+version:        0.4 license:        BSD3 license-file:   LICENSE build-type:     Simple cabal-version:  >= 1.6-tested-with:    GHC == 7.0.1, GHC == 7.0.3, GHC == 7.0.4, GHC == 7.2.1+tested-with:    GHC == 7.0.4, GHC == 7.2.1, GHC == 7.4.1 author:         Stephanie Weirich maintainer:     Brent Yorgey <byorgey@cis.upenn.edu>                 Stephanie Weirich <sweirich@cis.upenn.edu>