unbound 0.4.4 → 0.5.0
raw patch · 21 files changed
+858/−102 lines, 21 filesdep +QuickCheckdep +parsecdep +prettydep ~binarydep ~transformers
Dependencies added: QuickCheck, parsec, pretty, template-haskell, unbound
Dependency ranges changed: binary, transformers
Files
- CHANGES +29/−0
- Unbound/DynR.hs +37/−0
- Unbound/LocallyNameless.hs +1/−1
- Unbound/LocallyNameless/Alpha.hs +37/−17
- Unbound/LocallyNameless/Fresh.hs +1/−1
- Unbound/LocallyNameless/Ops.hs +40/−43
- Unbound/LocallyNameless/Subst.hs +87/−9
- Unbound/LocallyNameless/Types.hs +25/−5
- Unbound/PermM.hs +2/−1
- Unbound/Util.hs +1/−1
- examples/Abstract.hs +1/−1
- examples/Basic.hs +5/−5
- examples/F.hs +0/−1
- examples/LC.hs +8/−5
- examples/Main.hs +6/−5
- examples/STLC.hs +1/−1
- test/Abstract.hs +21/−0
- test/F.hs +324/−0
- test/Perf.hs +17/−0
- test/Util.hs +190/−0
- unbound.cabal +25/−6
CHANGES view
@@ -88,3 +88,32 @@ Version 0.4.3.1: 8 May 2014 * Allow transformers-0.4 and mtl-2.2++Version 0.4.4: 18 May 2015++ * Update to work with GHC 7.10+ +Version 0.4.5: 2 Oct 2015++ * Test suite in cabal file+ * New optimized function for immediately substitution w/o naming+ Only works for patterns with a single variable:+ substBind :: Subst a b => Bind (Name a) b -> a -> b++Version 0.5: August 2016++ * Remove Show superclass for Alpha (potentially breaking change)+ * Remove permValid function from Unbound.PermM+ + * New function in Unbound.LocallyNameless.Ops+ patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t + * More sensible Show instance for bind, shows as code that+ can be directly parsed to Haskell.+ old: <a> (Var 0@0)+ new: (bind (string2Name "a") (Var (string2Name "a"))+ * works with GHC-8.0.1+ * Error message if don't override aeq' / acompare' for abstract types+ * More correctness tests+ +Planned extensions:+ * Cache free variables at binders
+ Unbound/DynR.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE GADTs, ScopedTypeVariables+ #-}++----------------------------------------------------------------------+-- |+-- Module : Unbound.RepR+-- License : BSD-like (see LICENSE)+-- Maintainer : sweirich@cis.upenn.edu+-- Portability : GHC only (-XKitchenSink)+--+-- A Dynamic type based on type representations.+-- This module should probably be added to RepLib instead of Unbound+-- However, it is currently used only in an experimental function+-- (Unbound.Subst.substPats).+module Unbound.DynR (Dyn, toDyn, fromDyn, fromDynR) where++import Generics.RepLib++-- | Dynamic type based on type representations (replib)+data Dyn where + Dyn :: Rep a => a -> Dyn++-- | Coerce to a Dynamic type +toDyn :: Rep a => a -> Dyn +toDyn = Dyn ++-- | Coerce using an explicit type representation+toDynR :: R a -> a -> Dyn+toDynR ra = withRep ra toDyn++-- | Dynamic cast from the dynamic type (could fail)+fromDyn :: forall a. Rep a => Dyn -> Maybe a +fromDyn (Dyn x) = cast x++-- | Dyynamic cast using explicit type representation+fromDynR :: forall a. R a -> Dyn -> Maybe a+fromDynR r1 (Dyn x) = castR rep r1 x
Unbound/LocallyNameless.hs view
@@ -186,7 +186,7 @@ -- ** Substitution -- | Capture-avoiding substitution. - Subst(..), SubstName(..), + Subst(..), SubstName(..),substBind, -- ** Permutations
Unbound/LocallyNameless/Alpha.hs view
@@ -8,7 +8,7 @@ -- | -- Module : Unbound.LocallyNameless.Alpha -- License : BSD-like (see LICENSE) --- Maintainer : Brent Yorgey <byorgey@cis.upenn.edu> +-- Maintainer : Stephanie Weirich <sweirich@cis.upenn.edu> -- Portability : GHC only (-XKitchenSink) -- ---------------------------------------------------------------------- @@ -106,8 +106,19 @@ -- -- Note how the call to 'aeqR1' handles all the other cases generically. -- -class (Show a, Rep1 AlphaD a) => Alpha a where +-- If you use "Abstract" types (i.e. those with representations derived via +-- derive_abstract) then you must provide a definition of aeq' and +-- acompare'. In these cases, Unbound has no information about the +-- structure of the type and cannot do anything sensible. +-- swaps' -- identity function +-- fv' -- const mempty +-- freshen' -- identity function +-- lfreshen' -- identity function +-- open/close -- treat like constants + +class (Rep1 AlphaD a) => Alpha a where + -- | See 'swaps'. swaps' :: AlphaCtx -> Perm AnyName -> a -> a swaps' = swapsR1 rep1 @@ -215,7 +226,7 @@ | NamesSeen Integer -- ^ We haven't found the name -- (yet), but have seen this many -- others while looking for it - deriving (Eq, Ord, Show) + deriving (Eq, Ord) -- | @FindResult@ forms a monoid which combines information from -- several 'findpatrec' operations. @mappend@ takes the leftmost @@ -272,7 +283,7 @@ nthpat x i = case runNthCont (nthpatrec x) i of CurIndex j -> error ("BUG: pattern index " ++ show i ++ - " out of bounds by " ++ show j ++ "in" ++ show x) + " out of bounds by " ++ show j ++ "in") Found nm -> nm ------------------------------------------------------------ @@ -289,21 +300,25 @@ -- the context on. data AlphaCtx = AC { mode :: Mode , level :: Integer } +-- | Toplevel alpha-contexts initial :: AlphaCtx initial = AC Term 0 +-- | Call when going under a binder incr :: AlphaCtx -> AlphaCtx incr c = c { level = level c + 1 } +-- | Call when going in an embedding decr :: AlphaCtx -> AlphaCtx decr c = -- if level c == 0 then error "Too many outers" -- else c { level = level c - 1 } - +-- | Call when entering a pattern pat :: AlphaCtx -> AlphaCtx pat c = c { mode = Pat } +-- | Call when entering a term embedded in a pattern term :: AlphaCtx -> AlphaCtx term c = c { mode = Term } @@ -357,6 +372,7 @@ -- that take representations end in 'R1'.) ---------------------------------------------------------------------- +-- | Generic version of close closeR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a closeR1 (Data1 _ cons) = \i a d -> case (findCon cons d) of @@ -364,7 +380,7 @@ to c (map_l (\z -> closeD z i a) rec kids) closeR1 _ = \_ _ d -> d - +-- | Generic version of open openR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a openR1 (Data1 _ cons) = \i a d -> case (findCon cons d) of @@ -372,24 +388,24 @@ to c (map_l (\z -> openD z i a) rec kids) openR1 _ = \_ _ d -> d - +-- | Generic version of swaps swapsR1 :: R1 AlphaD a -> AlphaCtx -> Perm AnyName -> a -> a swapsR1 (Data1 _ cons) = \ p x d -> case (findCon cons d) of Val c rec kids -> to c (map_l (\z -> swapsD z p x) rec kids) swapsR1 _ = \ _ _ d -> d - +-- | Generic version of fv fvR1 :: Collection f => R1 (AlphaD) a -> AlphaCtx -> a -> f AnyName fvR1 (Data1 _ cons) = \ p d -> case (findCon cons d) of - Val _ rec kids -> fv1 rec p kids + Val _ rec kids -> fv1 rec p kids where + fv1 :: Collection f => MTup (AlphaD) l -> AlphaCtx -> l -> f AnyName + fv1 MNil _ Nil = emptyC + fv1 (r :+: rs) p (p1 :*: t1) = + fvD r p p1 `union` fv1 rs p t1 fvR1 _ = \ _ _ -> emptyC -fv1 :: Collection f => MTup (AlphaD) l -> AlphaCtx -> l -> f AnyName -fv1 MNil _ Nil = emptyC -fv1 (r :+: rs) p (p1 :*: t1) = - fvD r p p1 `union` fv1 rs p t1 {- matchR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName) @@ -413,6 +429,7 @@ (l1 `join` l2) -} +-- | Generic version of aeq aeqR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Bool aeqR1 (Data1 _ cons) = loop cons where loop (Con emb reps : rest) p x y = @@ -424,13 +441,16 @@ aeqR1 Int1 = \ _ x y -> x == y aeqR1 Integer1 = \ _ x y -> x == y aeqR1 Char1 = \ _ x y -> x == y +aeqR1 (Abstract1 _) = \ _ x y -> error "Must override aeq' for abstract types" aeqR1 _ = \ _ _ _ -> False +-- | Generic list version of aeq aeq1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Bool aeq1 MNil _ Nil Nil = True aeq1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) = do aeqD r c p1 p2 && aeq1 rs c t1 t2 +-- | Generic version of freshen freshenR1 :: Fresh m => R1 (AlphaD) a -> AlphaCtx -> a -> m (a,Perm AnyName) freshenR1 (Data1 _ cons) = \ p d -> case findCon cons d of @@ -439,6 +459,7 @@ return (to c l, p') freshenR1 _ = \ _ n -> return (n, empty) +-- | Generic list version of freshen freshenL :: Fresh m => MTup (AlphaD) l -> AlphaCtx -> l -> m (l, Perm AnyName) freshenL MNil _ Nil = return (Nil, empty) freshenL (r :+: rs) p (t :*: ts) = do @@ -515,8 +536,7 @@ (Nothing, Nothing) -> loop rest loop [] = error "acompareR1 found no constructors! Please report this as a bug." in loop cons -acompareR1 (Abstract1 _) _ = \_ _ -> EQ -acompareR1 r1 _ = error ("acompareR1 not supported for " ++ show r1) +acompareR1 r1 _ = error ("acompare' not supported for " ++ show r1) compareTupM :: MTup AlphaD l -> AlphaCtx -> l -> l -> Ordering compareTupM MNil _ Nil Nil = EQ @@ -707,8 +727,8 @@ acompare' c (B p1 t1) (B p2 t2) = mappend (acompare' (pat c) p1 p2) (acompare' (incr c) t1 t2) - findpatrec _ b = error $ "Binding " ++ show b ++ " used as a pattern" - nthpatrec b = error $ "Binding " ++ show b ++ " used as a pattern" + findpatrec _ b = error $ "Binding used as a pattern" + nthpatrec b = error $ "Binding used as a pattern" instance (Alpha p, Alpha q) => Alpha (Rebind p q) where isTerm _ = False
Unbound/LocallyNameless/Fresh.hs view
@@ -82,7 +82,7 @@ class Monad m => Fresh m where -- | Generate a new globally unique name based on the given one. - fresh :: Name a -> m (Name a) + fresh :: Rep a => Name a -> m (Name a) -- | The @FreshM@ monad transformer. Keeps track of the lowest index -- still globally unused, and increments the index every time it is
Unbound/LocallyNameless/Ops.hs view
@@ -8,7 +8,7 @@ -- | -- Module : Unbound.LocallyNameless.Ops -- License : BSD-like (see LICENSE)--- Maintainer : Brent Yorgey <byorgey@cis.upenn.edu>+-- Maintainer : Stephanie Weirich <sweirich@cis.upenn.edu> -- Portability : GHC only (-XKitchenSink) -- -- Generic operations defined in terms of the RepLib framework and the@@ -46,11 +46,6 @@ bind :: (Alpha p, Alpha t) => p -> t -> Bind p t bind p t = B p (closeT p t) --- | A destructor for binders that does /not/ guarantee fresh--- names for the binders.-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 readPrec = R.parens $ (R.prec app_prec $ do R.Ident "<" <- R.lexP@@ -66,18 +61,8 @@ -- 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+-- | 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@@ -86,7 +71,6 @@ -- 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) @@ -94,6 +78,19 @@ . map (strength . (\n -> (n, findpat t (AnyName n)))) $ ns +-- | Variant of permClose for dynamically typed names+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++ -- | Bind the pattern in the term \"up to permutation\" of bound variables. -- For example, the following 4 terms are /all/ alpha-equivalent: --@@ -318,29 +315,6 @@ swaps (pm' <> pm) p2, openT p1' t2) Nothing -> return Nothing -{- -unbind2translate :: (Fresh m, MonadPlus m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) =>- GenBind order card p1 t1 -> GenBind order card p2 t2 - -> m (p1,t1,p2,t2)-unbind2translate (B p1 t1) (B p2 t2) = do- do fv2' <- translates fv1 fv2 - pm <- mkPerm fv2' fv1 - (p1', pm') <- freshen p1- return $ Just (p1', openT p1' t1,- swaps (pm' <> pm) p2, openT p1' t2)- Nothing -> return Nothing - where fv1 = fvAny p1 - fv2 = fvAny p2--translates :: MonadPlus m => [AnyName] -> [AnyName] -> m [AnyName]-translates ((AnyName (n1 :: Name a)):n1s) ((AnyName n2):n2s) = - liftM (AnyName n2 :) (translates n1s n2s) where- n2' :: Name a- n2' = translate n2-translates [] [] = return [] -translates _ _ = mzero--}- -- | Unbind three terms with the same fresh names, provided the -- binders have the same number of binding variables. See the -- documentation for 'unbind2' for more details.@@ -401,27 +375,50 @@ -- A few extra simultaneous l/unbinds, specialized to MonadPlus monads. -+-- | Unbind two binders with the same names, fail if the number of required+-- names and their sorts does not match. See 'unbind2' unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> m (p1, t1, p2, t2) unbind2Plus bnd bnd' = maybe mzero return =<< unbind2 bnd bnd' +-- | Unbind three binders with the same names, fail if the number of required+-- names and their sorts does not match. See 'unbind3' unbind3Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> m (p1,t1,p2,t2,p3,t3) unbind3Plus b1 b2 b3 = maybe mzero return =<< unbind3 b1 b2 b3 +-- | See 'lunbind2' lunbind2Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> ((p1, t1, p2, t2) -> m r) -> m r lunbind2Plus bnd bnd' k = lunbind2 bnd bnd' $ maybe mzero k - ++-- | See 'lunbind3' lunbind3Plus :: (MonadPlus m, LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 -> ((p1,t1,p2,t2,p3,t3) -> m r) -> m r lunbind3Plus b1 b2 b3 = lunbind3 b1 b2 b3 . maybe mzero+++------------------------------------------------------------+-- Opening binders, without freshness+------------------------------------------------------------+++-- | A destructor for binders that does /not/ guarantee fresh names +-- for the binders. Instead it uses the names in the provided pattern.+patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t+patUnbind p (B _ t) = openT p t+++-- | A destructor for binders that does /not/ guarantee fresh+-- names for the binders. Instead, it uses the original names from+-- when the binder was constructed.+unsafeUnbind :: (Alpha a, Alpha b) => GenBind order card a b -> (a,b)+unsafeUnbind (B a b) = (a, openT a b)
Unbound/LocallyNameless/Subst.hs view
@@ -20,6 +20,10 @@ import Data.List (find) import Generics.RepLib++import Data.Proxy++import Unbound.DynR import Unbound.LocallyNameless.Types import Unbound.LocallyNameless.Alpha @@ -35,6 +39,12 @@ data SubstCoerce a b where SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b +-- | Immediately substitute for a (single) bound variable+-- in a binder, without first naming that variable.+substBind :: Subst a b => Bind (Name a) b -> a -> b+substBind (B _ t) u = substPat initial u t++ -- | The @Subst@ class governs capture-avoiding substitution. To -- derive this class, you only need to indicate where the variables -- are in the data type, by overriding the method 'isvar'.@@ -85,15 +95,39 @@ | otherwise = error $ "Cannot substitute for bound variable in: " ++ show (map fst ss) ++ -- Pattern substitution (single variable)+ -- call this using the top level function (substBind)+ substPat ::AlphaCtx -> b -> a -> a+ substPat ctx u x = + case (isvar x :: Maybe (SubstName a b)) of+ Just (SubstName (Bn r j 0)) | level ctx == j -> u+ _ -> substPatR1 rep1 ctx u x++ -- Pattern substitution (all variables in a single pattern)+ -- TODO: make this return Maybe when the dynamic chack fails+ -- i.e. when there aren't the right number/sort of arguments+ -- for the pattern. This function isn't yet exposed.+ substPats :: Proxy b -> AlphaCtx -> [ Dyn ] -> a -> a+ substPats p ctx us x = + case (isvar x :: Maybe (SubstName a b)) of+ Just (SubstName (Bn r j i)) | level ctx == j && fromInteger i < length us ->+ case fromDynR r (us !! fromInteger i) of+ Just tm -> tm+ Nothing -> error "internal error: sort mismatch"+ _ -> substPatsR1 rep1 p ctx us x+ -- | Reified class dictionary for 'Subst'. data SubstD b a = SubstD { isvarD :: a -> Maybe (SubstName a b), substD :: Name b -> b -> a -> a ,- substsD :: [(Name b, b)] -> a -> a+ substsD :: [(Name b, b)] -> a -> a ,+ substPatD :: AlphaCtx -> b -> a -> a ,+ substPatsD :: Proxy b -> AlphaCtx -> [ Dyn ] -> a -> a } instance Subst b a => Sat (SubstD b a) where- dict = SubstD isvar subst substs+ dict = SubstD isvar subst substs substPat substPats substDefault :: Rep1 (SubstD b) a => Name b -> b -> a -> a substDefault = substR1 rep1@@ -114,6 +148,56 @@ in (to c z) substsR1 _ = \ _ c -> c +substPatsR1 :: R1 (SubstD b) a -> Proxy b -> AlphaCtx -> [ Dyn ] -> a -> a+substPatsR1 (Data1 _dt cons) = \ p ct s d ->+ case (findCon cons d) of+ Val c rec kids ->+ let z = map_l (\ w -> substPatsD w p ct s) rec kids+ in (to c z)+substPatsR1 _ = \ _ _ _ c -> c++substPatR1 :: R1 (SubstD b) a -> AlphaCtx -> b -> a -> a+substPatR1 (Data1 _dt cons) = \ ct s d ->+ case (findCon cons d) of+ Val c rec kids ->+ let z = map_l (\ w -> substPatD w ct s) rec kids+ in (to c z)+substPatR1 _ = \ _ _ c -> c+++-- instances for types that change the de Bruijn levels of the context++instance (Rep order, Rep card, Alpha p, Alpha t, Subst b p, Subst b t) => Subst b (GenBind order card p t) where+ substPat c us (B p t) = + B (substPat (pat c) us p) (substPat (incr c) us t)+ substPats pr c us (B p t) = + B (substPats pr (pat c) us p) (substPats pr (incr c) us t)+ +instance (Alpha p, Alpha q, Subst b p, Subst b q) => Subst b (Rebind p q) where+ substPat c us (R p q) = R (substPat c us p) (substPat (incr c) us q)+ substPats pr c us (R p q) = R (substPats pr c us p) (substPats pr (incr c) us q)+ +instance (Alpha p, Subst b p) => Subst b (Rec p) where+ substPat c us (Rec p) = Rec (substPat (incr c) us p)+ substPats pr c us (Rec p) = Rec (substPats pr (incr c) us p)++instance (Alpha t, Subst b t) => Subst b (Embed t) where+ substPat c us (Embed x) = case mode c of+ Pat -> Embed (substPat (term c) us x)+ Term -> error "substPat on Embed"+ substPats pr c us (Embed x) = case mode c of+ Pat -> Embed (substPats pr (term c) us x)+ Term -> error "substPat on Embed"++instance (Alpha a, Subst b a) => Subst b (Shift a) where+ substPat c us (Shift x) = Shift (substPat (decr c) us x)+ substPats pr c us (Shift x) = Shift (substPats pr (decr c) us x)++ ++++ instance Subst b Int instance Subst b Bool instance Subst b ()@@ -135,11 +219,5 @@ instance (Subst c a) => Subst c (Maybe a) instance (Subst c a, Subst c b) => Subst c (Either 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) -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)+
Unbound/LocallyNameless/Types.hs view
@@ -45,33 +45,53 @@ ------------------------------------------------------------ -- Basic types ------------------------------------------------------------+-- Note: can't use DataKinds here because RepLib does not support+-- representations of them. +-- | Type level flag for binder that allows permutation data RelaxedOrder+-- | Type level flag for binder that does not allow permutation data StrictOrder +-- | Type level flag for binder that allows extra unused variables data RelaxedCard+-- | Type level flag for binder that does not allow weakening data StrictCard +-------------------------------------------------- -- Bind -------------------------------------------------- --- XXX update documentation+-- | Generic binding combinator for a pattern @p@ within a term @t@.+-- Flexible over the order and cardinality of the variables bound+-- in the pattern+data GenBind order card p t = B p t++ -- | 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 GenBind order card p t = B p t- type Bind p t = GenBind StrictOrder StrictCard p t++++-- | A variant of 'Bind' where alpha-equivalence allows multiple+-- variables bound in the same pattern to be reordered type SetBind p t = GenBind RelaxedOrder StrictCard p t+-- | A variant of 'Bind' where alpha-equivalence allows multiple+-- variables bound in the same pattern to be reordered, and+-- allows the binding of unused variables+-- For example, \{ a b c } . a b `aeq` \ { b a } . a b 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)+ (showString "bind " . showsPrec 11 a . showsPrec 11 b) +-------------------------------------------------- -- Rebind -------------------------------------------------- @@ -84,7 +104,7 @@ instance (Show a, Show b) => Show (Rebind a b) where showsPrec p (R a b) = showParen (p>0)- (showString "<<" . showsPrec p a . showString ">> " . showsPrec 0 b)+ (showString "rebind " . showsPrec 11 a . showsPrec 11 b) -- Rec --------------------------------------------------
Unbound/PermM.hs view
@@ -11,7 +11,7 @@ ---------------------------------------------------------------------- module Unbound.PermM (- Perm(..), permValid, single, compose, apply, support, isid, join, empty, restrict, mkPerm+ Perm(..), single, compose, apply, support, isid, join, empty, restrict, mkPerm ) where import Data.Monoid@@ -27,6 +27,7 @@ -- form the basis for nominal approaches to binding, but can -- also be useful in general. newtype Perm a = Perm (Map a a)+ permValid :: Ord a => Perm a -> Bool permValid (Perm p) = all (\(_,v) -> M.member v p) (M.assocs p)
Unbound/Util.hs view
@@ -9,7 +9,6 @@ -- -- Various utilities for the Unbound library. ----------------------------------------------------------------------- module Unbound.Util where import Data.Maybe (catMaybes)@@ -99,6 +98,7 @@ union = S.union cmap = S.map +-- | Determine whether two sets have an empty intersection disjoint :: Ord a => S.Set a -> S.Set a -> Bool disjoint s1 s2 = S.null( S.intersection s1 s2 )
examples/Abstract.hs view
@@ -21,7 +21,7 @@ -- -- Suppose we wish to include Source positions in our Abstract Syntax ---module Abstract where+module Examples.Abstract where import Generics.RepLib import Unbound.LocallyNameless
examples/Basic.hs view
@@ -13,10 +13,10 @@ -- ----------------------------------------------------------------------------- -module Basic where+module Examples.Basic where import Generics.RepLib-import Language.Haskell.TH+--import Language.Haskell.TH -- For each datatype that we define, we need to also create its representation.@@ -48,9 +48,9 @@ ''Dept, ''CUnit, ''Employee,- ''Manager,- ''Person,- ''Salary])+ ''Manager,+ ''Person,+ ''Salary]) --
examples/F.hs view
@@ -9,7 +9,6 @@ module F where import Unbound.LocallyNameless-import Unbound.LocallyNameless.NameInstances import Control.Monad import Control.Monad.Trans.Error
examples/LC.hs view
@@ -18,12 +18,14 @@ -- | A very simple example demonstration of the binding library -- based on the untyped lambda calculus.-module LC where+module Examples.LC where import Unbound.LocallyNameless import Control.Monad.Reader (Reader, runReader) import Data.Set as S +import System.Exit (exitFailure)+ -- | A Simple datatype for the Lambda Calculus data Exp = Var (Name Exp) | Lam (Bind (Name Exp) Exp)@@ -74,8 +76,9 @@ case e1' of -- look for a beta-reduction Lam bnd -> do- (x, e1'') <- unbind bnd- return $ subst x e2' e1''+ -- (x, e1'') <- unbind bnd+ -- return $ subst x e2' e1''+ return $ substBind bnd e2' otherwise -> return $ App e1' e2' red (Lam bnd) = do (x, e) <- unbind bnd@@ -92,12 +95,12 @@ assert :: String -> Bool -> IO () assert s True = return ()-assert s False = print ("Assertion " ++ s ++ " failed")+assert s False = print ("Assertion " ++ s ++ " failed") >> exitFailure assertM :: String -> M Bool -> IO () assertM s c = if (runFreshM c) then return ()- else print ("Assertion " ++ s ++ " failed")+ else print ("Assertion " ++ s ++ " failed") >> exitFailure x :: Name Exp x = string2Name "x"
examples/Main.hs view
@@ -16,16 +16,17 @@ module Main where -import qualified Basic-import qualified LC-import qualified STLC-import qualified Abstract+import qualified Examples.Basic as Basic+import qualified Examples.LC as LC+import qualified Examples.STLC as STLC+-- import qualified Examples.Abstract as Abstract main = do Basic.main LC.main STLC.main- Abstract.main+ -- Abstract.main+ -- F.main print "Tests completed"
examples/STLC.hs view
@@ -16,7 +16,7 @@ -- ----------------------------------------------------------------------------- -module STLC where+module Examples.STLC where import Unbound.LocallyNameless import Data.Set as S
+ test/Abstract.hs view
@@ -0,0 +1,21 @@+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,+ TemplateHaskell, UndecidableInstances #-}+module Lib+ where++import Unbound.LocallyNameless++data Term = Word Word+ deriving Show++$(derive_abstract [''Word]) -- No type structure information available+$(derive [''Term])+instance Alpha Word+instance Alpha Term++t1 :: Term+t1 = Word 5++wrong :: Bool+wrong = t1 `aeq` t1 -- should throw an error as Word is "abstract"+
+ test/F.hs view
@@ -0,0 +1,324 @@+{-# LANGUAGE TemplateHaskell,+ ScopedTypeVariables,+ FlexibleInstances,+ MultiParamTypeClasses,+ FlexibleContexts,+ UndecidableInstances,+ GADTs #-}++module F where++import Unbound.LocallyNameless hiding (prec,empty,Data,Refl)++import Control.Monad+import Control.Monad.Trans.Except+import qualified Data.List as List+import qualified Data.Set as Set++import Test.QuickCheck++import Util+import Text.PrettyPrint as PP++------------------------------------------------------+-- System F with type and term variables+------------------------------------------------------++type TyName = Name Ty+type TmName = Name Tm++data Ty = TyVar TyName+ | TyInt+ | Arr Ty Ty+ | All (Bind TyName Ty)+ | TyProd [Ty]+ deriving Show++data Tm = TmInt Int+ | TmVar TmName+ | Fix (Bind (TmName, TmName, Embed (Ty, Ty)) Tm)+ | App Tm Tm+ | TmProd [Tm]+ | TmPrj Tm Int+ | TmPrim Tm Prim Tm + | TmIf0 Tm Tm Tm+ | TLam (Bind TyName Tm)+ | TApp Tm Ty+ | Ann Tm Ty+ deriving Show+++$(derive [''Ty, ''Tm])++------------------------------------------------------+instance Alpha Ty +instance Alpha Tm ++instance Subst Tm Prim +instance Subst Tm Ty+instance Subst Ty Prim+instance Subst Ty Tm+instance Subst Tm Tm where+ isvar (TmVar x) = Just (SubstName x)+ isvar _ = Nothing+instance Subst Ty Ty where+ isvar (TyVar x) = Just (SubstName x)+ isvar _ = Nothing+++-----------------------------------------------------------------+-- Arbitrary +-----------------------------------------------------------------++arbTyName :: Gen (Name Ty)+arbTyName = liftM string2Name (elements (map (:[]) ['a' .. 'z']))++arbAll :: Gen Ty -> Gen Ty+arbAll gty = do+ ty <- gty+ let fvs = fv ty+ if Set.null fvs + then return ty+ else do + i <- choose (0, Set.size fvs - 1) + let v = Set.elemAt i fvs+ return $ All (bind v ty)+ ++genTy :: Int -> Gen Ty +genTy 1 = oneof [ return TyInt, liftM TyVar arbTyName ]+genTy n = frequency [(1, return TyInt),+ (3, liftM TyVar arbTyName),+ (4, liftM2 Arr go go),+ (20, arbAll go),+ (4, liftM TyProd (listOf go))] where+ go = genTy (n `div` 2)++instance Arbitrary Ty where+ arbitrary = sized genTy++-----------------------------------------------------------------+-- Typechecker+-----------------------------------------------------------------+type Delta = [ TyName ]+type Gamma = [ (TmName, Ty) ]++data Ctx = Ctx { getDelta :: Delta , getGamma :: Gamma }+emptyCtx = Ctx { getDelta = [], getGamma = [] }++checkTyVar :: Ctx -> TyName -> M ()+checkTyVar g v = do+ if List.elem v (getDelta g) then+ return ()+ else+ throwE "NotFound"++lookupTmVar :: Ctx -> TmName -> M Ty+lookupTmVar g v = do+ case lookup v (getGamma g) of+ Just s -> return s+ Nothing -> throwE "NotFound"++extendTy :: TyName -> Ctx -> Ctx+extendTy n ctx = ctx { getDelta = n : (getDelta ctx) }++extendTm :: TmName -> Ty -> Ctx -> Ctx+extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) }++-- could be replaced with fv+tcty :: Ctx -> Ty -> M ()+tcty g (TyVar x) =+ checkTyVar g x+tcty g (All b) = do+ (x, ty') <- unbind b+ tcty (extendTy x g) ty'+tcty g (Arr ty1 ty2) = do+ tcty g ty1+ tcty g ty2+tcty g TyInt = return ()+tcty g (TyProd tys) = do+ _ <- mapM (tcty g) tys+ return ()++typecheck :: Ctx -> Tm -> M Tm+typecheck g e@(TmVar x) = do + ty <- lookupTmVar g x+ return $ Ann e ty+typecheck g (Fix bnd) = do+ ((f, x, Embed (ty1, ty2)), e1) <- unbind bnd+ tcty g ty1+ tcty g ty2+ ae1@(Ann _ ty2') <- typecheck (extendTm f (Arr ty1 ty2) (extendTm x ty1 g)) e1+ if not (ty2 `aeq` ty2')+ then throwE $ "Type Error: Can't match " ++ pp ty2 ++ " and " ++ pp ty2'+ else return $ Ann + (Fix (bind (f,x, Embed (ty1, ty2)) ae1))+ (Arr ty1 ty2)+typecheck g e@(App e1 e2) = do+ ae1@(Ann _ ty1) <- typecheck g e1+ ae2@(Ann _ ty2) <- typecheck g e2+ case ty1 of+ Arr ty11 ty21 | ty2 `aeq` ty11 ->+ return (Ann (App ae1 ae2) ty21)+ _ -> throwE "TypeError"+typecheck g (TLam bnd) = do+ (x, e) <- unbind bnd+ ae@(Ann _ ty) <- typecheck (extendTy x g) e+ return $ Ann (TLam (bind x ae)) (All (bind x ty))+typecheck g (TApp e ty) = do+ ae@(Ann _ tyt) <- typecheck g e+ case tyt of+ (All b) -> do+ tcty g ty+ (n1, ty1) <- unbind b+ return $ Ann (TApp ae ty) (subst n1 ty ty1)+typecheck g (TmProd es) = do + atys <- mapM (typecheck g) es+ let tys = map (\(Ann _ ty) -> ty) atys+ return $ Ann (TmProd atys) (TyProd tys)+typecheck g (TmPrj e i) = do+ ae@(Ann _ ty) <- typecheck g e+ case ty of + TyProd tys | i < length tys -> return $ Ann (TmPrj ae i) (tys !! i)+ _ -> throwE "TypeError"+typecheck g (TmInt i) = return (Ann (TmInt i) TyInt)+typecheck g (TmPrim e1 p e2) = do+ ae1@(Ann _ ty1) <- typecheck g e1+ ae2@(Ann _ ty2) <- typecheck g e2 + case (ty1 , ty2) of + (TyInt, TyInt) -> return (Ann (TmPrim ae1 p ae2) TyInt)+ _ -> throwE "TypeError"+typecheck g (TmIf0 e0 e1 e2) = do+ ae0@(Ann _ ty0) <- typecheck g e0+ ae1@(Ann _ ty1) <- typecheck g e1+ ae2@(Ann _ ty2) <- typecheck g e2+ if ty1 `aeq` ty2 && ty0 `aeq` TyInt then + return (Ann (TmIf0 ae0 ae1 ae2) ty1)+ else + throwE "TypeError"++-----------------------------------------------------------------+-- Small-step semantics+-----------------------------------------------------------------++value :: Tm -> Bool+value (TmInt _) = True+value (Fix _) = True+value (TmProd es) = all value es+value (TLam _) = True+value _ = False++steps :: [Tm] -> M [Tm]+steps [] = throwE "can't step empty list"+steps (e:es) | value e = do+ es' <- steps es+ return (e : es')+steps (e:es) = do + e' <- step e+ return (e' : es)+ +step :: Tm -> M Tm+step e | value e = throwE "can't step value"+step (TmVar _) = throwE "unbound variable" +step (App e1@(Fix bnd) e2) = + if value e2 + then do+ ((f, x, _), t) <- unbind bnd+ return $ substs [ (x, e2), (f,e1) ] t+ else do + e2' <- step e2+ return (App e1 e2') +step (App e1 e2) = do+ e1' <- step e1+ return (App e1' e2)+step (TmPrj e1@(TmProd es) i) | value e1 && i < length es = return $ es !! i+step (TmPrj e1 i) = do + e1' <- step e1+ return (TmPrj e1' i) +step (TmProd es) = do+ es' <- steps es+ return (TmProd es')+step (TmPrim (TmInt i1) p (TmInt i2)) = + return (TmInt ((evalPrim p) i1 i2))+step (TmPrim e1 p e2) | value e1 = do+ e2' <- step e2+ return (TmPrim e1 p e2')+ | otherwise = do+ e1' <- step e1+ return (TmPrim e1' p e2)+step (TmIf0 (TmInt i) e1 e2) = if i==0 then return e1 else return e2+step (TmIf0 e0 e1 e2) = do + e0' <- step e0+ return (TmIf0 e0' e1 e2)+step (TApp (TLam bnd) ty) = do+ (a, e) <- unbind bnd+ return $ subst a ty e+step (TApp e ty) = do+ e' <- step e + return $ TApp e' ty+step (Ann e ty) = return e+ +evaluate :: Tm -> M Tm+evaluate e = if value e then return e else do+ e' <- step e+ evaluate e'++-----------------------------------------------------------------+-- Pretty-printer+-----------------------------------------------------------------++instance Display Ty where+ display (TyVar n) = display n+ display (TyInt) = return $ text "Int"+ display (Arr ty1 ty2) = do + d1 <- withPrec (precedence "->" + 1) $ display ty1+ d2 <- withPrec (precedence "->") $ display ty2+ binop d1 "->" d2+ display (All bnd) = lunbind bnd $ \ (a,ty) -> do+ da <- display a+ dt <- display ty+ prefix "forall" (da <> text "." <+> dt)+ display (TyProd tys) = displayTuple tys+ +instance Display Tm where+ display (TmInt i) = return $ int i+ display (TmVar n) = display n+ display (Fix bnd) = lunbind bnd $ \((f,x,Embed (ty1,ty2)), e) -> do+ df <- display f + dx <- display x + d1 <- display ty1 + d2 <- display ty2+ de <- withPrec (precedence "fix") $ display e+ let arg = parens (dx <> colon <> d1)+ --if f `elem` (fv e :: [F.TmName])+ -- then + prefix "fix" (df <+> arg <> colon <> d2 <> text "." <+> de)+ -- else prefix "\\" (arg <> text "." <+> de)+ display (App e1 e2) = do+ d1 <- withPrec (precedence " ") $ display e1+ d2 <- withPrec (precedence " " + 1) $ display e2+ binop d1 " " d2+ display (TmProd es) = displayTuple es++ display (TmPrj e i) = do+ de <- display e + return $ text "Pi" <> int i <+> de+ display (TmPrim e1 p e2) = do + let str = show p+ d1 <- withPrec (precedence str) $ display e1 + d2 <- withPrec (precedence str + 1) $ display e2 + binop d1 str d2+ display (TmIf0 e0 e1 e2) = do+ d0 <- display e0+ d1 <- display e1+ d2 <- display e2+ prefix "if0" $ sep [d0 , text "then" <+> d1 , text "else" <+> d2]+ display (TLam bnd) = lunbind bnd $ \(a,e) -> do+ da <- display a+ de <- withPrec (precedence "/\\") $ display e+ prefix "/\\" (da <> text "." <+> de)+ display (TApp e ty) = do+ d1 <- withPrec (precedence " ") $ display e+ d2 <- withPrec (precedence " " + 1) $ display ty+ binop d1 " " d2+ display (Ann e ty) = display e
+ test/Perf.hs view
@@ -0,0 +1,17 @@++import Criterion.Main (defaultMain)++import F+++--- alpha equivalence (System F types)++--- substitution++--- type checking (System F programs)++++main = defaultMain [+ , bench "fib 35" $ \n -> fib (35+n-n)+ ]
+ test/Util.hs view
@@ -0,0 +1,190 @@+{-# LANGUAGE TypeSynonymInstances,FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Util where++import Text.PrettyPrint as PP+import Control.Applicative+import Control.Monad.Identity+import Control.Monad.Trans.Except+import Control.Monad.Reader+import qualified Data.Set as Set+import qualified Data.List as List++import Unbound.LocallyNameless hiding (prec,empty,Data,Refl,Val)+import Unbound.LocallyNameless.Alpha+import Unbound.LocallyNameless.Types+++import Test.QuickCheck++------------------+-- should move to Unbound.LocallyNameless.Ops+patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t+patUnbind p (B _ t) = openT p t+------------------+++-------------------------------------------------------------------------+-- Primitives+-------------------------------------------------------------------------++data Prim = Plus | Minus | Times deriving (Eq, Ord, Enum)++instance Show Prim where+ show Plus = "+"+ show Minus = "-"+ show Times = "*"++$(derive [''Prim])++instance Alpha Prim++evalPrim :: Prim -> Int -> Int -> Int+evalPrim Plus = (+)+evalPrim Times = (*)+evalPrim Minus = (-)++instance Arbitrary Prim where+ arbitrary = elements [Plus ..]++++-------------------------------------------------------------------------+-- Monad for evaluation, typechecking and translation.+-------------------------------------------------------------------------+++type M = ExceptT String FreshM++runM :: M a -> a+runM m = case (runFreshM (runExceptT m)) of+ Left s -> error s+ Right a -> a+++-------------------------------------------------------------------------+-- The Display class and other pretty printing helper functions+-------------------------------------------------------------------------++-- | pretty-print +pp :: Display t => t -> String+pp d = render (runIdentity (runReaderT (runDM (display d)) initDI))+ +class Display t where+ -- | Convert a value to a 'Doc'.+ display :: t -> DM Doc + +newtype DM a = DM { runDM :: (ReaderT DispInfo Identity) a } + deriving (Functor,Applicative,Monad)++++maybeParens :: Bool -> Doc -> Doc+maybeParens b d = if b then parens d else d+ + +prefix :: String -> Doc -> DM Doc +prefix str d = do+ di <- ask+ return $ maybeParens (precedence str < prec di) (text str <+> d)+ +binop :: Doc -> String -> Doc -> DM Doc+binop d1 str d2 = do + di <- ask+ let dop = if str == " " then sep [d1, d2] else sep [d1, text str, d2]+ return $ maybeParens (precedence str < prec di) dop++ + +precedence :: String -> Int +precedence "->" = 10+precedence " " = 10+precedence "forall" = 9+precedence "if0" = 9+precedence "fix" = 9+precedence "\\" = 9+precedence "*" = 8+precedence "+" = 7+precedence "-" = 7+precedence _ = 0+ +++instance MonadReader DispInfo DM where+ ask = DM ask+ local f (DM m) = DM (local f m) ++-- | The data structure for information about the display+-- +data DispInfo = DI+ {+ prec :: Int, -- ^ precedence level + showTypes :: Bool, -- ^ should we show types? + dispAvoid :: Set.Set AnyName -- ^ names that have been used+ }++instance LFresh DM where+ lfresh nm = do+ let s = name2String nm+ di <- ask;+ return $ head (filter (\x -> AnyName x `Set.notMember` (dispAvoid di))+ (map (makeName s) [0..]))+ getAvoids = dispAvoid <$> ask+ avoid names = local upd where+ upd di = di { dispAvoid = + (Set.fromList names) `Set.union` (dispAvoid di) }+++-- | An empty 'DispInfo' context+initDI :: DispInfo+initDI = DI 10 False Set.empty++withPrec :: Int -> DM a -> DM a+withPrec i = + local $ \ di -> di { prec = i }+ +getPrec :: DM Int +getPrec = do+ di <- ask+ return (prec di)+ + +intersperse :: Doc -> [Doc] -> [Doc]+intersperse _ [] = []+intersperse _ [x] = [x]+intersperse sep (x:xs) = x <> sep : intersperse sep xs++displayList :: Display t => [t] -> DM Doc +displayList es = do+ ds <- mapM (withPrec 0 . display) es+ return $ cat (intersperse comma ds)+ +displayTuple :: Display t => [t] -> DM Doc +displayTuple es = do + ds <- displayList es+ return $ text "<" <> ds <> text ">" ++--------------------------------------------++instance Rep a => Display (Name a) where+ display n = return $ (text . show) n+ +--------------------------------------------++instance Display String where+ display = return . text+instance Display Int where+ display = return . text . show+instance Display Integer where+ display = return . text . show+instance Display Double where+ display = return . text . show+instance Display Float where+ display = return . text . show+instance Display Char where+ display = return . text . show+instance Display Bool where+ display = return . text . show+
unbound.cabal view
@@ -1,12 +1,12 @@ name: unbound-version: 0.4.4+version: 0.5.0 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, GHC == 7.8.3, GHC == 7.10+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, GHC == 8.0.1 author: Stephanie Weirich, Brent Yorgey-maintainer: Stephanie Weirich <sweirich@cis.upenn.edu>, Brent Yorgey <byorgey@cis.upenn.edu> +maintainer: Stephanie Weirich <sweirich@cis.upenn.edu> homepage: https://github.com/sweirich/replib category: Language, Generics, Compilers/Interpreters extra-source-files: README,@@ -31,9 +31,9 @@ build-depends: base >= 4.3 && < 5, RepLib >= 0.5.3 && < 0.6, mtl >= 2.0 && < 2.3,- transformers >= 0.2.2.0 && < 0.5,+ transformers >= 0.2.2.0 && < 0.6, containers >= 0.3 && < 0.6,- binary >= 0.7 && < 0.8+ binary >= 0.7 && < 0.9 exposed-modules: Unbound.LocallyNameless, Unbound.LocallyNameless.Name,@@ -43,7 +43,8 @@ Unbound.LocallyNameless.Subst, Unbound.LocallyNameless.Ops, Unbound.PermM,- Unbound.Util+ Unbound.Util,+ Unbound.DynR other-extensions: CPP EmptyDataDecls ExistentialQuantification@@ -60,3 +61,21 @@ TypeSynonymInstances UndecidableInstances default-language: Haskell2010++Test-Suite lambda-calculus+ default-language: Haskell2010+ build-depends: base >= 4.3 && < 5,+ RepLib >= 0.5.3 && < 0.6,+ mtl >= 2.0 && < 2.3,+ transformers >= 0.2.2.0 && < 0.6,+ containers >= 0.3 && < 0.6,+ binary >= 0.7 && < 0.9,+ unbound >= 0.5,+ template-haskell >= 2.11,+ parsec >= 3.1.9 && < 3.2,+ pretty>= 1.1.2 && < 1.2,+ QuickCheck>=2.8.2 && < 2.9+++ type: exitcode-stdio-1.0+ main-is: examples/Main.hs