unbound 0.2.5 → 0.3

raw patch · 11 files changed

+305/−22 lines, 11 filesdep ~RepLib

Dependency ranges changed: RepLib

Files

• CHANGES +9/−0
• Unbound/LocallyNameless.hs +6/−2
• Unbound/LocallyNameless/Alpha.hs +1/−1
• Unbound/LocallyNameless/Ops.hs +86/−7
• Unbound/LocallyNameless/Subst.hs +2/−2
• Unbound/LocallyNameless/Types.hs +19/−7
• Unbound/PermM.hs +0/−1
• examples/Set.hs +67/−0
• examples/TaggedTerm.hs +59/−0
• examples/Vec.hs +54/−0
• unbound.cabal +2/−2

@@ -28,3 +28,12 @@     Thanks to Sean Leather for the report.    * Clean up some compiler warnings.++Version 0.2.6: 24 August 2011++  * New permutation- and set-binding functions, for creating binders+    which don't care about the order of multiple bound names, and/or+    about unused bound names.++  * Bump RepLib dependency to 0.5, which now has support for GADTs+    without existential type variables.

@@ -100,9 +100,13 @@ 
     Bind,
 
-    -- *** Bind constructor
+    -- *** Bind constructors
     bind,
+    permbind,
+    setbind,
+    setbindAny,
 
+
     -- *** Bind destructors
 
     -- | Directly pattern-matching on 'Bind' values is not allowed,
@@ -250,7 +254,7 @@     -- | These type representation objects are exported so they can be
     --   referenced by auto-generated code.  Please pretend they do not
     --   exist.
-    rName, rBind, rRebind, rEmbed, rRec, rShift
+    rName, rGenBind, rRebind, rEmbed, rRec, rShift
 ) where
 
 import Unbound.LocallyNameless.Name

@@ -666,7 +666,7 @@ 
   nthpatrec = nthName
 
-instance (Alpha p, Alpha t) => Alpha (Bind p t) where
+instance (Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t) where
     isPat _ = Nothing
     isTerm (B p t) = isJust (isPat p) && isTerm t
 

@@ -1,3 +1,4 @@+{-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} ---------------------------------------------------------------------- -- |@@ -19,6 +20,10 @@ import Unbound.Util import Unbound.PermM +import Data.Maybe (catMaybes)+import Data.List  (sortBy)+import Data.Ord   (comparing)+ import Control.Monad (liftM) import qualified Text.Read as R @@ -35,7 +40,7 @@  -- | A destructor for binders that does /not/ guarantee fresh --   names for the binders.-unsafeUnbind :: (Alpha a, Alpha b) => Bind a b -> (a,b)+unsafeUnbind :: (Alpha a, Alpha b) => GenBind order card a b -> (a,b) unsafeUnbind (B a b) = (a, openT a b)  instance (Alpha a, Alpha b, Read a, Read b) => Read (Bind a b) where@@ -50,6 +55,80 @@          readListPrec = R.readListPrecDefault  ----------------------------------------------------------+-- Set Binding operations+----------------------------------------------------------++permCloseAny :: (Alpha t) => [AnyName] -> t -> ([AnyName],t)+permCloseAny ns t = (ns', closeT ns' t) where+    -- find where the names occur in the body of the term+    ns' = map fst . sortBy (comparing snd) +        . catMaybes +        . map (strength . (\n -> (n, findpat t n))) +        $ ns++strength :: Functor f => (a, f b) -> f (a, b)+strength (a, fb) = fmap ((,) a) fb++-- Given a list of names and a term, close the term with those names+-- where the indices of the bound variables occur in sequential order+-- and return the equivalent ordering of the names, dropping those+-- that do not occur in the term at all+-- For example:+--    permClose [b,c]    (b,c)   =  ([b,c], (0,1))    -- standard close+--    permClose [b,c]    (c,b)   =  ([c,b], (0,1))    -- vars reordered+--    permClose [a,b,c]  (c,b)   =  ([c,b], (0,1))    -- var dropped+--    permClose [a,b,c]  (c,b,c) =  ([c,b], (0,1,0))  -- additional occurrence ok++permClose :: (Alpha a, Alpha t) => [Name a] -> t -> ([Name a],t)+permClose ns t = (ns', closeT ns' t) where+    ns' = map fst . sortBy (comparing snd) +        . catMaybes +        . map (strength . (\n -> (n, findpat t (AnyName n))))+        $ ns++-- | Bind the pattern in the term \"up to permutation\" of bound variables.+--   For example, the following 4 terms are /all/ alpha-equivalent:+--+--   > permbind [a,b] (a,b)+--   > permbind [a,b] (b,a)+--   > permbind [b,a] (a,b)+--   > permbind [b,a] (b,a)+--+--   Note that none of these terms is equivalent to a term with a+--   redundant pattern such as+--+--   > permbind [a,b,c] (a,b)+--+--   For binding constructors which /do/ render these equivalent,+--   see 'setbind' and 'setbindAny'.+permbind :: (Alpha p, Alpha t) => p -> t -> SetBind p t+permbind p t = B p (snd $ permCloseAny (bindersAny p) t)++-- | Bind the list of names in the term up to permutation and dropping+--   of unused variables.+--+--   For example, the following 5 terms are /all/ alpha-equivalent:+--+--   > setbind [a,b] (a,b)+--   > setbind [a,b] (b,a)+--   > setbind [b,a] (a,b)+--   > setbind [b,a] (b,a)+--   > setbind [a,b,c] (a,b)+--+--   There is also a variant, 'setbindAny', which ignores name sorts.+setbind ::(Alpha a, Alpha t) => [Name a] -> t -> SetPlusBind [Name a] t+setbind p t = B ns t' where+         (ns, t') = permClose (binders p) t++-- | Bind the list of (any-sorted) names in the term up to permutation+--   and dropping of unused variables.  See 'setbind'.+setbindAny :: (Alpha t) => [AnyName] -> t -> SetPlusBind [AnyName] t+setbindAny p t = B ns t' where+         (ns, t') = permCloseAny (bindersAny p) t++++---------------------------------------------------------- -- Rebinding operations ---------------------------------------------------------- @@ -210,7 +289,7 @@ --   bindings. It ensures that the names in the binding are globally --   fresh, using a monad which is an instance of the 'Fresh' type --   class.-unbind :: (Fresh m, Alpha p, Alpha t) => Bind p t -> m (p,t)+unbind :: (Fresh m, Alpha p, Alpha t) => GenBind order card p t -> m (p,t) unbind (B p t) = do       (p', _) <- freshen p       return (p', openT p' t)@@ -221,7 +300,7 @@ --   @Nothing@.  Otherwise, return the renamed patterns and the --   associated terms. unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) =>-            Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1,t1,p2,t2))+            GenBind order card p1 t1 -> GenBind order card p2 t2 -> m (Maybe (p1,t1,p2,t2)) unbind2 (B p1 t1) (B p2 t2) = do       case mkPerm (fvAny p2) (fvAny p1) of          Just pm -> do@@ -234,7 +313,7 @@ --   binders have the same number of binding variables.  See the --   documentation for 'unbind2' for more details. unbind3 :: (Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) =>-            Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 ->  m (Maybe (p1,t1,p2,t2,p3,t3))+            GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 ->  m (Maybe (p1,t1,p2,t2,p3,t3)) unbind3 (B p1 t1) (B p2 t2) (B p3 t3) = do       case ( mkPerm (fvAny p2) (fvAny p1)            , mkPerm (fvAny p3) (fvAny p1) ) of@@ -253,7 +332,7 @@ -- --   For more information, see the documentation for the 'LFresh' type --   class.-lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c+lunbind :: (LFresh m, Alpha p, Alpha t) => GenBind order card p t -> ((p, t) -> m c) -> m c lunbind (B p t) g =   lfreshen p (\x _ -> g (x, openT x t)) @@ -262,7 +341,7 @@ --   patterns have the same number of binding variables.  See the --   documentation for 'unbind2' and 'lunbind' for more details. lunbind2  :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) =>-            Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1,t1,p2,t2) -> m r) -> m r+            GenBind order card p1 t1 -> GenBind order card p2 t2 -> (Maybe (p1,t1,p2,t2) -> m r) -> m r lunbind2 (B p1 t1) (B p2 t2) g =   case mkPerm (fvAny p2) (fvAny p1) of     Just pm1 ->@@ -274,7 +353,7 @@ --   the binders have the same number of binding variables.  See the --   documentation for 'unbind2' and 'lunbind' for more details. lunbind3 :: (LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) =>-            Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 ->+            GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 ->             (Maybe (p1,t1,p2,t2,p3,t3) -> m r) ->             m r lunbind3 (B p1 t1) (B p2 t2) (B p3 t3) g =

@@ -117,8 +117,8 @@ instance (Subst c a) => Subst c (Maybe a) instance (Subst c a, Subst c b) => Subst c (Either a b) -instance (Subst c b, Subst c a, Alpha a,Alpha b) =>-    Subst c (Bind a b)+instance (Rep order, Rep card, Subst c b, Subst c a, Alpha a,Alpha b) =>+    Subst c (GenBind order card a b) instance (Subst c b, Subst c a, Alpha a, Alpha b) =>     Subst c (Rebind a b) 

@@ -3,6 +3,7 @@            , FlexibleInstances            , FlexibleContexts            , MultiParamTypeClasses+           , EmptyDataDecls   #-}  ----------------------------------------------------------------------@@ -18,7 +19,7 @@ ----------------------------------------------------------------------  module Unbound.LocallyNameless.Types-       ( Bind(..)+       ( GenBind(..), Bind, SetBind, SetPlusBind        , Rebind(..)        , Rec(..)        , TRec(..)@@ -32,7 +33,7 @@        --   referenced by auto-generated code.  Please pretend they do not        --   exist. -       , rBind, rRebind, rEmbed, rRec, rShift+       , rGenBind, rRebind, rEmbed, rRec, rShift        ) where  import Generics.RepLib@@ -42,23 +43,32 @@ -- Basic types ------------------------------------------------------------ +data RelaxedOrder+data StrictOrder++data RelaxedCard+data StrictCard+ -- Bind -------------------------------------------------- +-- XXX update documentation -- | The most fundamental combinator for expressing binding structure --   is 'Bind'.  The /term type/ @Bind p t@ represents a pattern @p@ --   paired with a term @t@, where names in @p@ are bound within @t@. -- --   Like 'Name', 'Bind' is also abstract. You can create bindings --   using 'bind' and take them apart with 'unbind' and friends.-data Bind p t = B p t+data GenBind order card p t = B p t -instance (Show a, Show b) => Show (Bind a b) where+type Bind p t        = GenBind StrictOrder StrictCard p t+type SetBind p t     = GenBind RelaxedOrder StrictCard p t+type SetPlusBind p t = GenBind RelaxedOrder RelaxedCard p t++instance (Show a, Show b) => Show (GenBind order card a b) where   showsPrec p (B a b) = showParen (p>0)       (showString "<" . showsPrec p a . showString "> " . showsPrec 0 b) --- XXX todo: make sure everything has write Read and Eq instances?- -- Rebind -------------------------------------------------- @@ -133,5 +143,7 @@  -- Pay no attention... -$(derive [''Bind, ''Embed, ''Rebind, ''Rec, ''Shift])+$(derive [''GenBind, ''Embed, ''Rebind, ''Rec, ''Shift])++$(derive [''RelaxedOrder, ''StrictOrder, ''RelaxedCard, ''StrictCard]) 

@@ -17,7 +17,6 @@ import Data.Monoid import Data.List import Data.Map (Map)-import Data.Function (on) import qualified Data.Map as M import qualified Data.Set as S import Control.Arrow ((&&&))

@@ -0,0 +1,67 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,+    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving+ #-}++module Set where++import Generics.RepLib+import Unbound.LocallyNameless+import Data.List+import Data.Set++data Ty = All (Bind [Name Ty] Ty)+        | Var (Name Ty)+        | Arr Ty Ty deriving Show++$(derive [''Ty])++$(derive_abstract [''Set])++instance Alpha Ty++a, b, c :: Name Ty+a = s2n "a"+b = s2n "b"+c = s2n "c"++sall :: [Name Ty] -> Ty -> Ty+sall ns t = All (setbind ns t)++s1 = sall [a, b] (Arr (Var a) (Var b))+s2 = sall [a, b] (Arr (Var b) (Var a))+s3 = sall [b, a] (Arr (Var a) (Var b))+s4 = sall [b, a] (Arr (Var b) (Var a))+s5 = sall [b, a, c] (Arr (Var b) (Var a))+s6 = sall [a, c] (Arr (Var a) (Var c))++pall :: [Name Ty] -> Ty -> Ty+pall ns t = All (permbind ns t)++p1 = pall [a, b] (Arr (Var a) (Var b))+p2 = pall [a, b] (Arr (Var b) (Var a))+p3 = pall [b, a] (Arr (Var a) (Var b))+p4 = pall [b, a] (Arr (Var b) (Var a))+p5 = pall [b, a, c] (Arr (Var b) (Var a))+p6 = pall [a, c] (Arr (Var a) (Var c))++++assert :: String -> Bool -> IO ()+assert s True  = return ()+assert s False = print ("Assertion " ++ s ++ " failed")++main :: IO ()+main = do+  assert "s1" $ s1 `aeq` s2+  assert "s2" $ s1 `aeq` s3+  assert "s3" $ s1 `aeq` s4+  assert "s4" $ s1 `aeq` s5+  assert "s5" $ s1 `aeq` s6++  assert "a11" $ p1 `aeq` p2+  assert "a12" $ p1 `aeq` p3+  assert "a13" $ p1 `aeq` p4+  assert "a14" $ not (p1 `aeq` p5)+  assert "a15" $ p1 `aeq` p6+

@@ -0,0 +1,59 @@+{-# LANGUAGE TemplateHaskell+           , UndecidableInstances+           , TypeOperators+           , GADTs+           , FlexibleInstances+           , ScopedTypeVariables+           , MultiParamTypeClasses+           , KindSignatures+           , RankNTypes+           , StandaloneDeriving+           , OverlappingInstances+ #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  TaggedTerm+-- Copyright   :  (c) the Unbound team (see LICENSE)+-- License     :  BSD-like (see LICENSE)+--+-- Maintainer  :  byorgey@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------++module TaggedTerm where++import Unbound.LocallyNameless hiding (Con)++data Term+data Pattern++data Expr :: * -> * where+         -- Note: be very careful here!  Name (Expr a) -> Expr a does+         -- not work since the names in patterns will not get+         -- connected up with names in terms.+  Var :: Name (Expr Term) -> Expr a+  App :: Expr a ->  Expr a -> Expr a+  Lam :: Bind (Expr Pattern) (Expr Term) -> Expr Term+  Con :: String -> [Expr a] -> Expr a++deriving instance Show (Expr a)++$(derive [''Term, ''Pattern, ''Expr])++instance (Rep t) => Alpha (Expr t)++instance Subst (Expr Term) (Expr Term) where+  isvar (Var x) = Just (SubstName x)+  isvar _       = Nothing++instance Subst (Expr Term) (Expr Pattern)++test1 :: Expr Term+test1 = Lam (bind (Con "Pair" [Var $ s2n "y", Var $ s2n "z"]) (Con "Pair" [Var (s2n "y"), Var (s2n "x")]))++test2 :: Expr Term+test2 = subst (s2n "y") (Con "Unit" [] :: Expr Term) test1++test3 :: Expr Term+test3 = subst (s2n "x") (Con "Unit" [] :: Expr Term) test1

@@ -0,0 +1,54 @@+{-# LANGUAGE TemplateHaskell+           , UndecidableInstances+           , TypeOperators+           , GADTs+           , FlexibleInstances+           , ScopedTypeVariables+           , MultiParamTypeClasses+           , KindSignatures+           , RankNTypes+           , StandaloneDeriving+           , OverlappingInstances+ #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Vec+-- Copyright   :  (c) the Unbound team (see LICENSE)+-- License     :  BSD-like (see LICENSE)+--+-- Maintainer  :  byorgey@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------++module Vec where++import Unbound.LocallyNameless hiding (Nil)++data Z+data S n++data Vec :: * -> * -> * where+  Nil   :: Vec Z a+  Cons  :: a -> Vec n a -> Vec (S n) a++deriving instance Show a => Show (Vec n a)++data Term = Var (Name Term) +          | Lit (Vec (S (S Z)) Int) +          | Pair Term Term+  deriving Show++$(derive [''Z, ''S, ''Vec, ''Term])++instance (Alpha a, Rep n) => Alpha (Vec n a)+instance Alpha Term++instance Subst Term Term where+  isvar (Var x) = Just (SubstName x)+  isvar _       = Nothing++instance (Rep n, Rep a) => Subst Term (Vec n a)++t :: Term+t = Pair (Var (s2n "x")) (Lit (Cons 1 (Cons 2 Nil)))

@@ -1,5 +1,5 @@ name:           unbound-version:        0.2.5+version:        0.3 license:        BSD3 license-file:   LICENSE build-type:     Simple@@ -30,7 +30,7 @@  Library   build-depends: base >= 4.3 && < 5,-                 RepLib >= 0.4.0,+                 RepLib >= 0.5,                  mtl >= 2.0 && < 2.1, transformers >= 0.2.2.0 && < 0.2.3,                  containers >= 0.3 && < 0.5   exposed-modules: