diff --git a/CHANGES b/CHANGES --- a/CHANGES +++ b/CHANGES @@ -19,3 +19,12 @@ - examples/STLC.hs Thanks to Ki Yung Ahn for the reports. + +Version 0.2.4: 13 July 2011 + + * Fix bug in mkPerm which caused unbind2 to unexpectedly fail when + dealing with binders with non-disjoint sets of names. + + Thanks to Sean Leather for the report. + + * Clean up some compiler warnings. diff --git a/Unbound/LocallyNameless.hs b/Unbound/LocallyNameless.hs --- a/Unbound/LocallyNameless.hs +++ b/Unbound/LocallyNameless.hs @@ -37,8 +37,8 @@ -- of the library source package: @cabal unpack unbound@) and the -- examples in the @example@ directory. -- --- See also: Stephanie Weirich, Brent Yorgey, and Tim Sheard. --- /Binders Unbound/. Submitted, March 2011. . +-- See also: Stephanie Weirich, Brent A. Yorgey, and Tim Sheard. +-- /Binders Unbound/. To appear in ICFP'11, September 2011, Tokyo, Japan. . ---------------------------------------------------------------------- module Unbound.LocallyNameless diff --git a/Unbound/LocallyNameless/Alpha.hs b/Unbound/LocallyNameless/Alpha.hs --- a/Unbound/LocallyNameless/Alpha.hs +++ b/Unbound/LocallyNameless/Alpha.hs @@ -463,20 +463,20 @@ findpatR1 :: R1 AlphaD b -> b -> AnyName -> FindResult -findpatR1 (Data1 dt cons) = \ d n -> +findpatR1 (Data1 _dt cons) = \ d n -> case findCon cons d of - Val c rec kids -> findpatL rec kids n -findpatR1 _ = \ x n -> mempty + Val _c rec kids -> findpatL rec kids n +findpatR1 _ = \ _ _ -> mempty findpatL :: MTup AlphaD l -> l -> AnyName -> FindResult -findpatL MNil Nil n = mempty +findpatL MNil Nil _ = mempty findpatL (r :+: rs) (t :*: ts) n = findpatD r t n <> findpatL rs ts n nthpatR1 :: R1 AlphaD b -> b -> NthCont -nthpatR1 (Data1 dt cons) = \ d -> +nthpatR1 (Data1 _dt cons) = \ d -> case findCon cons d of - Val c rec kids -> nthpatL rec kids -nthpatR1 _ = \ x -> mempty + Val _c rec kids -> nthpatL rec kids +nthpatR1 _ = \ _ -> mempty nthpatL :: MTup AlphaD l -> l -> NthCont nthpatL MNil Nil = mempty @@ -488,43 +488,39 @@ combine _ _ = Nothing isPatR1 :: R1 AlphaD b -> b -> Maybe [AnyName] -isPatR1 (Data1 dt cons) = \ d -> +isPatR1 (Data1 _dt cons) = \ d -> case findCon cons d of - Val c rec kids -> + Val _c rec kids -> foldl_l (\ c b a -> combine (isPatD c a) b) (Just []) rec kids -isPatR1 _ = \ d -> Just [] +isPatR1 _ = \ _ -> Just [] isTermR1 :: R1 AlphaD b -> b -> Bool -isTermR1 (Data1 dt cons) = \ d -> +isTermR1 (Data1 _dt cons) = \ d -> case findCon cons d of - Val c rec kids -> foldl_l (\ c b a -> isTermD c a && b) True rec kids -isTermR1 _ = \ d -> True + Val _c rec kids -> foldl_l (\ c b a -> isTermD c a && b) True rec kids +isTermR1 _ = \ _ -> True -- Exactly like the generic Ord instance defined in Generics.RepLib.PreludeLib, -- except that the comparison operation takes an AlphaCtx acompareR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Ordering -acompareR1 Int1 c = \x y -> compare x y -acompareR1 Char1 c = \x y -> compare x y -acompareR1 (Data1 str cons) c = \x y -> +acompareR1 Int1 _ = \x y -> compare x y +acompareR1 Char1 _ = \x y -> compare x y +acompareR1 (Data1 _ cons) c = \x y -> let loop (Con emb rec : rest) = case (from emb x, from emb y) of (Just t1, Just t2) -> compareTupM rec c t1 t2 - (Just t1, Nothing) -> LT - (Nothing, Just t2) -> GT + (Just _ , Nothing) -> LT + (Nothing, Just _ ) -> GT (Nothing, Nothing) -> loop rest + loop [] = error "acompareR1 found no constructors! Please report this as a bug." in loop cons -acompareR1 r1 c = error ("compareR1 not supported for " ++ show r1) - -lexord :: Ordering -> Ordering -> Ordering -lexord LT ord = LT -lexord EQ ord = ord -lexord GT ord = GT +acompareR1 r1 _ = error ("compareR1 not supported for " ++ show r1) compareTupM :: MTup AlphaD l -> AlphaCtx -> l -> l -> Ordering -compareTupM MNil c Nil Nil = EQ +compareTupM MNil _ Nil Nil = EQ compareTupM (x :+: xs) c (y :*: ys) (z :*: zs) = - lexord (acompareD x c y z) (compareTupM xs c ys zs) + mappend (acompareD x c y z) (compareTupM xs c ys zs) ------------------------------------------------------------ @@ -553,12 +549,12 @@ case gcastR (getR y) (getR x) y of Just y' -> y' Nothing -> error "Internal error in swaps': sort mismatch" - swaps' c p x | mode c == Pat = x + swaps' _ _ x = x - aeq' _ x y | x == y = True - aeq' c n1 n2 | mode c == Term = False - aeq' c _ _ | mode c == Pat = True + aeq' c x y | mode c == Term = x == y + aeq' _ _ _ = True + {- match' _ x y | x == y = Just empty match' c n1 n2 | mode c == Term = Just $ single (AnyName n1) (AnyName n2) @@ -567,8 +563,9 @@ freshen' c nm | mode c == Pat = do x <- fresh nm return (x, single (AnyName nm) (AnyName x)) - freshen' c nm | mode c == Term = error "freshen' on Name in Term mode" + freshen' _ _ = error "freshen' on Name in Term mode" + lfreshen' c nm f = case mode c of Pat -> do x <- lfresh nm avoid [AnyName x] $ f x (single (AnyName nm) (AnyName x)) @@ -581,7 +578,7 @@ Nothing -> error "Internal error in open: sort mismatch" open _ _ n = n - close c a nm@(Nm r n) | mode c == Term = + close c a nm@(Nm r _) | mode c == Term = case findpat a (AnyName nm) of Just x -> Bn r (level c) x Nothing -> nm @@ -595,15 +592,16 @@ nthpatrec = nthName . AnyName acompare' c (Nm r1 n1) (Nm r2 n2) - | mode c == Term = lexord (compare r1 r2) (compare n1 n2) + | mode c == Term = mconcat [compare r1 r2, compare n1 n2] acompare' c (Bn r1 m1 n1) (Bn r2 m2 n2) - | mode c == Term = lexord (compare r1 r2) (lexord (compare m1 m2) (compare n1 n2)) + | mode c == Term = mconcat [compare r1 r2, compare m1 m2, compare n1 n2] acompare' c (Nm _ _) (Bn _ _ _) | mode c == Term = LT acompare' c (Bn _ _ _) (Nm _ _) | mode c == Term = GT - acompare' c _ _ | mode c == Pat = EQ + acompare' _ _ _ = EQ + instance Alpha AnyName where isTerm _ = True @@ -620,8 +618,9 @@ aeq' _ x y | x == y = True aeq' c _ _ | mode c == Term = False - aeq' c _ _ | mode c == Pat = True + aeq' _ _ _ = True + {- match' _ x y | x == y = Just empty match' c (AnyName n1) (AnyName n2) @@ -639,9 +638,8 @@ EQ -> case gcastR (getR n1) (getR n2) n1 of Just n1' -> acompare' c n1' n2 Nothing -> error "impossible" - otherwise -> otherwise - acompare' c _ _ | mode c == Pat = EQ - + neq -> neq + acompare' _ _ _ = EQ freshen' c (AnyName nm) = case mode c of Pat -> do x <- fresh nm @@ -656,7 +654,7 @@ open c a (AnyName (Bn _ j x)) | level c == j = nthpat a x open _ _ n = n - close c a nm@(AnyName (Nm r n)) = + close c a nm@(AnyName (Nm r _)) = case findpat a nm of Just x -> AnyName (Bn r (level c) x) Nothing -> nm @@ -706,7 +704,7 @@ -- Comparing two binding terms. acompare' c (B p1 t1) (B p2 t2) = - lexord (acompare' (pat c) p1 p2) (acompare' (incr c) t1 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" @@ -744,7 +742,7 @@ -} acompare' c (R a1 a2) (R b1 b2) = - lexord (acompare' c a1 b1) (acompare' (incr c) a2 b2) + mappend (acompare' c a1 b1) (acompare' (incr c) a2 b2) open c a (R p q) = R (open c a p) (open (incr c) a q) @@ -778,14 +776,18 @@ -- and we generally should treat the annots as constants instance Alpha t => Alpha (Embed t) where isPat (Embed t) = if (isTerm t) then Just [] else Nothing - isTerm t = False + isTerm _ = False isEmbed (Embed t) = isTerm t - swaps' c pm (Embed t) | mode c == Pat = Embed (swaps' (term c) pm t) - swaps' c pm (Embed t) | mode c == Term = Embed t + swaps' c pm (Embed t) = + case mode c of + Pat -> Embed (swaps' (term c) pm t) + Term -> Embed t - fv' c (Embed t) | mode c == Pat = fv' (term c) t - fv' c _ | mode c == Term = emptyC + fv' c (Embed t) = + case mode c of + Pat -> fv' (term c) t + Term -> emptyC freshen' c p | mode c == Term = error "freshen' called on a term" | otherwise = return (p, empty) @@ -805,11 +807,13 @@ else Nothing -} - close c b (Embed x) | mode c == Pat = Embed (close (term c) b x) - | mode c == Term = error "close on Embed" + close c b (Embed x) = case mode c of + Pat -> Embed (close (term c) b x) + Term -> error "close on Embed" - open c b (Embed x) | mode c == Pat = Embed (open (term c) b x) - | mode c == Term = error "open on Embed" + open c b (Embed x) = case mode c of + Pat -> Embed (open (term c) b x) + Term -> error "open on Embed" findpatrec _ _ = mempty nthpatrec _ = mempty @@ -824,7 +828,7 @@ -- The contents of Shift may only be an Embed or another Shift. isPat (Shift a) = if (isEmbed a) then Just [] else Nothing - isTerm a = False + isTerm _ = False isEmbed (Shift a) = isEmbed a close c b (Shift x) = Shift (close (decr c) b x) diff --git a/Unbound/LocallyNameless/Fresh.hs b/Unbound/LocallyNameless/Fresh.hs --- a/Unbound/LocallyNameless/Fresh.hs +++ b/Unbound/LocallyNameless/Fresh.hs @@ -25,14 +25,14 @@ Fresh(..), - FreshM(..), runFreshM, contFreshM, + FreshM, runFreshM, contFreshM, FreshMT(..), runFreshMT, contFreshMT, -- * The 'LFresh' class LFresh(..), - LFreshM(..), runLFreshM, contLFreshM, getAvoids, + LFreshM, runLFreshM, contLFreshM, getAvoids, LFreshMT(..), runLFreshMT, contLFreshMT ) where @@ -55,7 +55,6 @@ import Control.Monad.Trans.Identity import Control.Monad.Trans.List import Control.Monad.Trans.Maybe -import Control.Monad.Trans.Reader (ReaderT) import Control.Monad.Trans.State.Lazy as Lazy import Control.Monad.Trans.State.Strict as Strict import Control.Monad.Trans.Writer.Lazy as Lazy @@ -65,7 +64,6 @@ 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.IO.Class as IC ------------------------------------------------------------ -- Fresh @@ -98,6 +96,8 @@ n <- St.get St.put (n+1) return $ Nm r (s,n) + + fresh (Bn {}) = error "fresh encountered bound name! Please report this as a bug." -- | A convenient monad which is an instance of 'Fresh'. It keeps -- track of a global index used for generating fresh names, which is diff --git a/Unbound/LocallyNameless/Name.hs b/Unbound/LocallyNameless/Name.hs --- a/Unbound/LocallyNameless/Name.hs +++ b/Unbound/LocallyNameless/Name.hs @@ -7,6 +7,7 @@ , MultiParamTypeClasses , ScopedTypeVariables #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} ---------------------------------------------------------------------- -- | -- Module : Unbound.LocallyNameless.Name diff --git a/Unbound/LocallyNameless/Ops.hs b/Unbound/LocallyNameless/Ops.hs --- a/Unbound/LocallyNameless/Ops.hs +++ b/Unbound/LocallyNameless/Ops.hs @@ -1,4 +1,4 @@ - +{-# OPTIONS_GHC -fno-warn-orphans #-} ---------------------------------------------------------------------- -- | -- Module : Unbound.LocallyNameless.Ops diff --git a/Unbound/LocallyNameless/Subst.hs b/Unbound/LocallyNameless/Subst.hs --- a/Unbound/LocallyNameless/Subst.hs +++ b/Unbound/LocallyNameless/Subst.hs @@ -42,7 +42,7 @@ -- non-variable arguments. The default implementation always -- returns 'Nothing'. isvar :: a -> Maybe (SubstName a b) - isvar x = Nothing + isvar _ = Nothing -- | @'subst' nm sub tm@ substitutes @sub@ for @nm@ in @tm@. It has -- a default generic implementation in terms of @isvar@. @@ -51,7 +51,7 @@ case (isvar x :: Maybe (SubstName a b)) of Just (SubstName m) -> if m == n then u else x Nothing -> substR1 rep1 n u x - subst m u x = error $ "Cannot substitute for bound variable " ++ show m + subst m _ _ = error $ "Cannot substitute for bound variable " ++ show m -- | Perform several simultaneous substitutions. This method also -- has a default generic implementation in terms of @isvar@. @@ -81,20 +81,20 @@ substDefault = substR1 rep1 substR1 :: R1 (SubstD b) a -> Name b -> b -> a -> a -substR1 (Data1 dt cons) = \ x y d -> +substR1 (Data1 _dt cons) = \ x y d -> case (findCon cons d) of Val c rec kids -> let z = map_l (\ w -> substD w x y) rec kids in (to c z) -substR1 r = \ x y c -> c +substR1 _ = \ _ _ c -> c substsR1 :: R1 (SubstD b) a -> [(Name b, b)] -> a -> a -substsR1 (Data1 dt cons) = \ s d -> +substsR1 (Data1 _dt cons) = \ s d -> case (findCon cons d) of Val c rec kids -> let z = map_l (\ w -> substsD w s) rec kids in (to c z) -substsR1 r = \ s c -> c +substsR1 _ = \ _ c -> c instance Subst b Int instance Subst b Bool diff --git a/Unbound/LocallyNameless/Test.hs b/Unbound/LocallyNameless/Test.hs deleted file mode 100644 --- a/Unbound/LocallyNameless/Test.hs +++ /dev/null @@ -1,153 +0,0 @@ -{-# LANGUAGE TemplateHaskell - , MultiParamTypeClasses - , FlexibleInstances - , FlexibleContexts - , ScopedTypeVariables - , UndecidableInstances - #-} - -module Unbound.LocallyNameless.Test where - -import qualified Data.Set as S - -import Unbound.LocallyNameless hiding (GT) -import Unbound.LocallyNameless.Alpha -import Unbound.LocallyNameless.Name -import Unbound.PermM - --------------------- TESTING CODE -------------------------------- -data Exp = V (Name Exp) - | A Exp Exp - | L (Bind (Name Exp) Exp) deriving (Show) - -$(derive [''Exp]) - -instance Alpha Exp -instance Subst Exp Exp where - isvar (V n) = Just (SubstName n) - isvar _ = Nothing - -nameA, nameB, nameC :: Name Exp -nameA = integer2Name 1 -nameB = integer2Name 2 -nameC = integer2Name 3 - -assert :: String -> Bool -> IO () -assert s True = return () -assert s False = print ("Assertion " ++ s ++ " failed") - -do_tests :: IO () -do_tests = do - tests_aeq - tests_fv - tests_big - tests_nth - tests_acompare - -perm = single nameA nameB - -naeq x y = not (aeq x y) - -tests_aeq = do - assert "a1" $ (bind nameA nameA) `naeq` (bind nameA nameB) - assert "a2" $ (bind nameA nameA) `aeq` (bind nameA nameA) - assert "a3" $ (bind nameA nameA) `aeq` (bind nameB nameB) - assert "a4" $ (bind nameA nameB) `naeq` (bind nameB nameA) - assert "a5" $ (bind (nameA, Embed nameB) nameA) `naeq` - (bind (nameA, Embed nameC) nameA) - assert "a6" $ (bind (nameA, Embed nameB) nameA) `aeq` - (bind (nameA, Embed nameB) nameA) - assert "a7" $ (bind (nameA, Embed nameB) nameA) `aeq` - (bind (nameB, Embed nameB) nameB) - assert "a8" $ rebind nameA nameB `naeq` rebind nameB nameB - assert "a9" $ rebind nameA nameA `naeq` rebind nameB nameB - assert "a9" $ (bind (rebind nameA (Embed nameA)) nameA) `aeq` - (bind (rebind nameB (Embed nameB)) nameB) - assert "a10" $ bind (rebind (nameA, Embed nameA) ()) nameA `aeq` - bind (rebind (nameB, Embed nameA) ()) nameB - assert "a11" $ bind (rebind (nameA, Embed nameA) ()) nameA `naeq` - bind (rebind (nameB, Embed nameB) ()) nameB - assert "a12" $ bind (Embed nameA) () `naeq` bind (Embed nameB) () - assert "a13" $ bind (Embed nameA) () `aeq` bind (Embed nameA) () - assert "a14" $ bind (rebind (Embed nameA) ()) () `naeq` - bind (rebind (Embed nameB) ()) () - assert "a15" $ (rebind (nameA, Embed nameA) ()) `naeq` - (rebind (nameA, Embed nameC) ()) - assert "a16" $ bind (nameA, nameB) nameA `naeq` bind (nameB, nameA) nameA - assert "a17" $ bind (nameA, nameB) nameA `naeq` bind (nameA, nameB) nameB - assert "a18" $ (nameA, nameA) `naeq` (nameA, nameB) --- assert "a19" $ match (nameA, nameA) (nameB, nameC) == Nothing - -emptyNE :: S.Set (Name Exp) -emptyNE = S.empty - -tests_fv = do - assert "f1" $ fv (bind nameA nameA) == emptyNE - assert "f2" $ fv' (pat initial) (bind nameA nameA) == S.empty - assert "f4" $ fv (bind nameA nameB) == S.singleton nameB - assert "f5" $ fv (bind (nameA, Embed nameB) nameA) == S.singleton nameB - assert "f7" $ fv (bind (nameB, Embed nameB) nameB) == S.singleton nameB - assert "f8" $ fv (rebind nameA nameB) == S.fromList [nameA, nameB] - assert "f9" $ fv' (pat initial) (rebind nameA nameA) == S.empty - assert "f3" $ fv (bind (rebind nameA (Embed nameA)) nameA) == emptyNE - assert "f10" $ fv (rebind (nameA, Embed nameA) ()) == S.singleton nameA - assert "f11" $ fv' (pat initial) (rebind (nameA, Embed nameA) ()) == S.singleton (AnyName nameA) - assert "f12" $ fv (bind (Embed nameA) ()) == S.singleton nameA - assert "f14" $ fv (rebind (Embed nameA) ()) == emptyNE - -mkbig :: [Name Exp] -> Exp -> Exp -mkbig (n : names) body = - L (bind n (mkbig names (A (V n) body))) -mkbig [] body = body - -big1 = mkbig (map integer2Name (take 100 [1 ..])) (V nameA) -big2 = mkbig (map integer2Name (take 101 [1 ..])) (V nameA) - - -tests_nth = do - assert "n1" $ nthpat ([nameA],nameB) 0 == AnyName nameA - assert "n2" $ nthpat ([nameA],nameB) 1 == AnyName nameB - assert "n3" $ nthpat (nameA, nameB) 0 == AnyName nameA - assert "p1" $ findpat ([nameA],nameB) (AnyName nameA) == Just 0 - assert "p2" $ findpat ([nameA],nameB) (AnyName nameB) == Just 1 - assert "p3" $ findpat ([nameA],nameB) (AnyName nameC) == Nothing - -tests_big = do - assert "b1" $ big1 `naeq` big2 - assert "b2" $ fv big1 == emptyNE - assert "b3" $ big1 `aeq` subst nameA (V nameA) big1 - -tests_acompare = do - -- Names compare in the obvious way. - assert "ac1" $ acompare nameA nameB == LT - assert "ac2" $ acompare nameB nameB == EQ - assert "ac3" $ acompare nameB nameA == GT - -- structured date compares lexicographically - assert "ac4" $ acompare (A (V nameA) (V nameA)) (A (V nameA) (V nameA)) == EQ - assert "ac5" $ acompare (A (V nameA) (V nameA)) (A (V nameA) (V nameB)) == LT - assert "ac6" $ acompare (A (V nameA) (V nameB)) (A (V nameA) (V nameA)) == GT - assert "ac7" $ acompare (A (V nameA) (V nameA)) (A (V nameB) (V nameA)) == LT - assert "ac8" $ acompare (A (V nameB) (V nameA)) (A (V nameA) (V nameA)) == GT - assert "ac9" $ acompare (A (V nameB) (V nameA)) (A (V nameA) (V nameB)) == GT - -- comparison goes under binders, alpha-respectingly. - assert "ac10" $ acompare (bind nameA (A (V nameA) (V nameA))) (bind nameA (A (V nameA) (V nameA))) == EQ - assert "ac11" $ acompare (bind nameA (A (V nameA) (V nameA))) (bind nameA (A (V nameA) (V nameB))) == GT - assert "ac12" $ acompare (bind nameC (A (V nameC) (V nameA))) (bind nameA (A (V nameA) (V nameB))) == LT - -- non-matching binders handled alpha-respectingly. - assert "ac13" $ acompare (bind [nameA] nameA) (bind [nameA,nameB] nameA) - == acompare (bind [nameC] nameC) (bind [nameA,nameB] nameA) - assert "ac14" $ acompare (bind [nameA,nameB] nameA) (bind [nameA] nameA) - == acompare (bind [nameC,nameB] nameC) (bind [nameA] nameA) - -- non-binding stuff in patterns gets compared - assert "ac15" $ acompare (Embed nameA) (Embed nameB) == LT - assert "ac16" $ acompare (bind (nameC, Embed nameA) (A (V nameC) (V nameC))) - (bind (nameC, Embed nameB) (A (V nameC) (V nameC))) == LT - assert "ac17" $ acompare (bind (nameC, Embed nameA) (A (V nameB) (V nameB))) - (bind (nameC, Embed nameB) (A (V nameA) (V nameA))) == LT - -- TODO: do we need anything special for rebind? For AnyName? - --- properties --- if match t1 t2 = Some p then swaps p t1 = t2 - -main :: IO () -main = do_tests diff --git a/Unbound/LocallyNameless/Types.hs b/Unbound/LocallyNameless/Types.hs --- a/Unbound/LocallyNameless/Types.hs +++ b/Unbound/LocallyNameless/Types.hs @@ -120,7 +120,7 @@ newtype Embed t = Embed t deriving Eq instance Show a => Show (Embed a) where - showsPrec p (Embed a) = showString "{" . showsPrec 0 a . showString "}" + showsPrec _ (Embed a) = showString "{" . showsPrec 0 a . showString "}" -- Shift -------------------------------------------------- @@ -129,7 +129,7 @@ newtype Shift p = Shift p deriving Eq instance Show a => Show (Shift a) where - showsPrec p (Shift a) = showString "{" . showsPrec 0 a . showString "}" + showsPrec _ (Shift a) = showString "{" . showsPrec 0 a . showString "}" -- Pay no attention... diff --git a/Unbound/Nominal.hs b/Unbound/Nominal.hs deleted file mode 100644 --- a/Unbound/Nominal.hs +++ /dev/null @@ -1,70 +0,0 @@ ----------------------------------------------------------------------- --- | --- Module : Unbound.Nominal --- License : BSD-like (see LICENSE) --- Maintainer : Stephanie Weirich --- Stability : experimental --- Portability : non-portable (-XKitchenSink) --- --- A generic implementation of standard functions dealing with names --- and binding structure (alpha equivalence, free variable --- calculation, capture-avoiding substitution, name permutation, ...) --- using a nominal representation. --- --- DISCLAIMER: this module almost certainly contains bugs and may be --- slower than "Unbound.LocallyNameless". The documentation is also --- sparse and likely out of date. At this point we recommend it only --- for the curious or intrepid. We are actively working on bringing --- it up to speed as a viable alternative to --- "Unbound.LocallyNameless". --- --------------------------------------------------------------------------- -module Unbound.Nominal - (-- * Basic types - Name, AnyName(..), Bind, Embed(..), Rebind, Rec, Shift, - - -- ** Utilities - integer2Name, string2Name, name2Integer, name2String, makeName, - name1,name2,name3,name4,name5,name6,name7,name8,name9,name10, - translate, - - -- * The 'Alpha' class - Alpha(..), - swaps, -- is a bit wonky - match, - binders, patfv, fv, - aeq, - - -- * Binding operations - bind, unsafeUnbind, - - -- * The 'Fresh' class - Fresh(..), freshen, - unbind, unbind2, unbind3, - - -- * The 'LFresh' class - HasNext(..), LFresh(..), - lfreshen, - lunbind, lunbind2, lunbind3, - - -- * Rebinding operations - rebind, reopen, - - -- * Rec operations - rec, unrec, - - -- * Substitution - Subst(..), - - -- * Advanced - AlphaCtx, matchR1, - - -- * Pay no attention to the man behind the curtain - - -- | 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) where - -import Unbound.Nominal.Name -import Unbound.Nominal.Internal diff --git a/Unbound/Nominal/Internal.hs b/Unbound/Nominal/Internal.hs deleted file mode 100644 --- a/Unbound/Nominal/Internal.hs +++ /dev/null @@ -1,977 +0,0 @@ -{-# LANGUAGE FlexibleInstances, UndecidableInstances, FlexibleContexts, MultiParamTypeClasses, TemplateHaskell, TypeOperators, ScopedTypeVariables, TypeSynonymInstances, RankNTypes, GADTs, EmptyDataDecls, StandaloneDeriving #-} - ----------------------------------------------------------------------- --- | --- Module : Unbound.Nominal.Internal --- License : BSD-like (see LICENSE) --- --------------------------------------------------------------------------- -module Unbound.Nominal.Internal where - -import Generics.RepLib -import Unbound.Nominal.Name -import Unbound.PermM - -import qualified Data.List as List -import qualified Text.Read as R -import Data.Set (Set) -import Data.Maybe -import qualified Data.Set as S -import Prelude hiding (or) -import Data.Monoid -import qualified Control.Monad as Monad -import Control.Monad.Reader (Reader,ask,local,runReader) -import System.IO.Unsafe (unsafePerformIO) - -(<>) :: Monoid m => m -> m -> m -(<>) = mappend - ---------------------------------------------------- - -$(derive_abstract [''R]) --- The above only works with GHC 7. - - --- | Type of a binding. Morally, the type a should be in the --- class 'Pattern' and the type b should be in the class 'Alpha'. --- The Pattern class contains the constructor and a safe --- destructor for these types. --- We can Bind an "a" object in a "b" object if we --- can create "fresh" a objects, and Names can be --- swapped in "b" objects. Often "a" is Name --- but that need not be the case. -data Bind a b = B a b - --- | An annotation is a 'hole' in a pattern where variables --- can be used, but not bound. For example patterns may include --- type annotations, and those annotations can reference variables --- without binding them. --- Annotations do nothing special when they appear elsewhere in terms -newtype Embed a = Embed a deriving (Read, Eq) - --- | Shift the scope of an embedded term one level outwards. -newtype Shift a = Shift a deriving Eq - --- | Rebinding is for telescopes --- i.e. to support patterns that --- also bind variables that appear later -data Rebind a b = R a (Bind [AnyName] b) - --- | 'Rec' supports recursive patterns --- that is, patterns where --- any variables anywhere in the pattern are bound in the pattern --- itself. Useful for lectrec (and Agda's dot notation). -data Rec a = Rec a - -$(derive [''Bind, ''Name, ''Embed, ''Rebind, ''Rec, ''Shift]) - ----------------------------------------------------------- --- Binding operations & instances ----------------------------------------------------------- - --- | Smart constructor for binders -bind :: (Alpha b,Alpha c) => b -> c -> Bind b c -bind a b = B a b - --- | A destructor for binders that does not guarantee fresh --- names for the binders. -unsafeUnbind :: Bind a b -> (a,b) -unsafeUnbind (B a b) = (a,b) - -instance (Show a, Show b) => Show (Bind a b) where - showsPrec p (B a b) = showParen (p>0) - (showString "<" . showsPrec p a . showString "> " . showsPrec 0 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 "B" <- R.lexP - m1 <- R.step R.readPrec - m2 <- R.step R.readPrec - return (bind m1 m2)) - where app_prec = 10 - - readListPrec = R.readListPrecDefault - ----------------------------------------------------------- --- Rebinding operations ----------------------------------------------------------- - --- | Constructor for binding in patterns -rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b -rebind a b = R a (bind (binders a) b) - -instance (Alpha a, Show a, Show b) => Show (Rebind a b) where - showsPrec p (R a (B a' b)) = showParen (p>0) - (showString "<<" . showsPrec p a . sa' . showString ">> " . showsPrec 0 b) - where sa' = if binders' initial a == a' then showString "" - else showString "/" . showsPrec p a' - --- | destructor for binding patterns, the external names --- should have already --- been freshen'ed. We swap the internal names so that they use the --- external names -reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b) -reopen (R a1 (B names b)) = (a1, swaps p b) where - p = fromJust $ Monad.foldM join empty - (zipWith single (binders' initial a1) names) - ----------------------------------------------------------- --- Rec operations ----------------------------------------------------------- - -rec :: (Alpha a) => a -> Rec a -rec a = Rec a where - -unrec :: (Alpha a) => Rec a -> a -unrec (Rec a) = a - -instance Show a => Show (Rec a) where - showsPrec p (Rec a) = showString "[" . showsPrec 0 a . showString "]" - ----------------------------------------------------------- --- Embed ----------------------------------------------------------- -instance (Show a) => Show (Embed a) where - showsPrec p (Embed a) = - (showString "{" . showsPrec 0 a . showString "}") - ----------------------------------------------------------- --- Wrappers for operations in the Alpha class ----------------------------------------------------------- - -aeq :: Alpha a => a -> a -> Bool -aeq t1 t2 = -- aeq' initial t1 t2 - case match t1 t2 of - Just p -> isid p - _ -> False - - --- | calculate the free variables of the term -fv :: (Rep b, Alpha a) => a -> Set (Name b) -fv = S.map fromJust . S.filter isJust . S.map toSortedName . fv' initial - --- | List the binding variables in a pattern -binders :: (Rep b, Alpha b) => b -> [AnyName] -binders = binders' initial - --- | Set of variables that occur freely in annotations (not binding) -patfv :: (Rep a, Alpha b) => b -> Set (Name a) -patfv = S.map fromJust . S.filter isJust . S.map toSortedName . fv' (pat initial) - --- | The method "swaps" applys a permutation to all free variables --- in the term. -swaps :: Alpha a => Perm AnyName -> a -> a -swaps = swaps' initial - --- | Apply a permutation to the binding variables in a pattern. --- Embedded terms are left alone by the permutation. -swapsBinders :: Alpha a => Perm AnyName -> a -> a -swapsBinders = swaps' initial - --- | Apply a permutation to the annotations in a pattern. Binding --- names are left alone by the permutation. -swapsEmbeds :: Alpha a => Perm AnyName -> a -> a -swapsEmbeds = swaps' (pat initial) - - --- | "Locally" freshen an object -lfreshen :: Alpha a => LFresh m => a -> (a -> Perm AnyName -> m b) -> m b -lfreshen = lfreshen' initial - --- | A pattern of type "b" can be freshened if a new --- copy of "b" can be produced where all old *binding* Names --- in "b" are replaced with new fresh Names, and the --- permutation reports which Names were swapped by others. -freshen :: (Fresh m, Alpha a) => a -> m (a, Perm AnyName) -freshen = freshen' initial - --- | Match compares two data structures and produces a permutation --- of their Names that will make them alpha-equivalent to --- eachother. (Names that appear in annotations must match exactly.) --- Also note that two terms are alpha-equivalent when the empty --- permutation is returned. -match :: Alpha a => a -> a -> Maybe (Perm AnyName) -match = match' initial - - --- | Compare two patterns, ignoring the names of binders, and produce --- a permutation of their annotations to make them alpha-equivalent --- to eachother. Return 'Nothing' if no such renaming is possible. -matchEmbeds :: Alpha a => a -> a -> Maybe (Perm AnyName) -matchEmbeds = match' (pat initial) - --- | Compare two patterns for equality and produce a permutation of --- their binding 'Names' to make them alpha-equivalent to each other --- ('Name's that appear in annotations must match exactly). Return --- 'Nothing' if no such renaming is possible. -matchBinders :: Alpha a => a -> a -> Maybe (Perm AnyName) -matchBinders = match' initial - ---------------------------------------------------------------- --- | Many of the operations in the 'Alpha' class take an 'AlphaCtx': --- stored information about the iteration as it progresses. This type --- is abstract, as classes that override these operations should just pass --- the context on. -data AlphaCtx = Term | Pat deriving (Show, Eq, Read) - -initial :: AlphaCtx -initial = Term - -pat :: AlphaCtx -> AlphaCtx -pat c = Pat - -term :: AlphaCtx -> AlphaCtx -term c = Term - -mode :: AlphaCtx -> AlphaCtx -mode = id - ------------------------------------------------------------- --- The Alpha class ------------------------------------------------------------- --- | The Alpha class is for all terms that may contain binders --- The 'Rep1' class constraint means that we can only --- make instances of this class for types that have --- generic representations. (Derive these using TH and --- RepLib.) - -class (Rep1 (AlphaD) a) => Alpha a where - - aeq' :: AlphaCtx -> a -> a -> Bool - aeq' = aeqR1 rep1 - - -- | swap everything, including bound and free variables, - -- parts in annots, etc. - swapall' :: AlphaCtx -> Perm AnyName -> a -> a - swapall' = swapallR1 rep1 - - -- | The method "swaps'" applys a compound permutation - swaps' :: AlphaCtx -> Perm AnyName -> a -> a - swaps' = swapsR1 rep1 - - -- | calculate the free variables (aka support) - fv' :: AlphaCtx -> a -> Set AnyName - fv' = fvR1 rep1 - - -- | list the binding variables in a pattern, in order - binders' :: AlphaCtx -> a -> [AnyName] - binders' = bindersR1 rep1 - - -- | Match' compares two data structures and produces a - -- permutation of their free variables that will make them - -- alpha-equivalent to eachother. - match' :: AlphaCtx -> a -> a -> Maybe (Perm AnyName) - match' = matchR1 rep1 - - -- | An object of type "a" can be freshened if a new - -- copy of "a" can be produced where all old Names - -- in "a" are replaced with new fresh Names, and the - -- permutation reports which names were swapped by others. - freshen' :: Fresh m => AlphaCtx -> a -> m (a,Perm AnyName) - freshen' = freshenR1 rep1 - - -- | See 'lfreshen' - lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b - lfreshen' = lfreshenR1 rep1 - - --- class constraint hackery to allow us to override the --- default definitions for certain classes -data AlphaD a = AlphaD { - aeqD :: AlphaCtx -> a -> a -> Bool, - swapallD :: AlphaCtx -> (Perm AnyName) -> a -> a, - swapsD :: AlphaCtx -> (Perm AnyName) -> a -> a, - fvD :: AlphaCtx -> a -> Set AnyName, - bindersD :: AlphaCtx -> a -> [AnyName], - - matchD :: AlphaCtx -> a -> a -> Maybe (Perm AnyName), - freshenD :: forall m. Fresh m => AlphaCtx -> a -> m (a,Perm AnyName), - lfreshenD :: forall b m. LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b - } - -instance Alpha a => Sat (AlphaD a) where - dict = AlphaD aeq' swapall' swaps' fv' binders' match' freshen' lfreshen' - --- Generic definitions of the class functions. --- (All functions that take representations end --- in 'R1') -aeqR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Bool -aeqR1 (Data1 _ cons) = loop cons where - loop (Con emb reps : rest) p x y = - case (from emb x, from emb y) of - (Just p1, Just p2) -> aeq1 reps p p1 p2 - (Nothing, Nothing) -> loop rest p x y - (_,_) -> False - loop [] _ _ _ = error "Impossible" -aeqR1 Int1 = \ _ x y -> x == y -aeqR1 Integer1 = \ _ x y -> x == y -aeqR1 Char1 = \ _ x y -> x == y -aeqR1 _ = \ _ _ _ -> error "Cannot aeq this type" - -aeq1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Bool -aeq1 MNil _ Nil Nil = True -aeq1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) = - aeqD r c p1 p2 && aeq1 rs c t1 t2 - -swapsR1 :: R1 (AlphaD) a -> AlphaCtx -> (Perm AnyName) -> a -> a -swapsR1 Char1 = \ _ _ c -> c -swapsR1 Int1 = \ _ _ c -> c -swapsR1 Float1 = \ _ _ c -> c -swapsR1 Integer1 = \ _ _ c -> c -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 r = error ("Cannot swap type " ++ (show r)) - - -swapallR1 :: R1 (AlphaD) a -> AlphaCtx -> (Perm AnyName) -> a -> a -swapallR1 Char1 = \ _ _ c -> c -swapallR1 Int1 = \ _ _ c -> c -swapallR1 Float1 = \ _ _ c -> c -swapallR1 Integer1 = \ _ _ c -> c -swapallR1 (Data1 _ cons) = \ p x d -> - case (findCon cons d) of - Val c rec kids -> to c (map_l (\z -> swapallD z p x) rec kids) -swapallR1 r = error ("Cannot swap type " ++ (show r)) - -fvR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> Set AnyName -fvR1 (Data1 _ cons) = \ p d -> - case (findCon cons d) of - Val _ rec kids -> fv1 rec p kids -fvR1 _ = \ _ _ -> S.empty - -fv1 :: MTup (AlphaD) l -> AlphaCtx -> l -> Set AnyName -fv1 MNil _ Nil = S.empty -fv1 (r :+: rs) p (p1 :*: t1) = - fvD r p p1 `S.union` fv1 rs p t1 - -bindersR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> [AnyName] -bindersR1 (Data1 _ cons) = \ p d -> - case (findCon cons d) of - Val _ rec kids -> binders1 rec p kids -bindersR1 _ = \ _ _ -> [] - -binders1 :: MTup (AlphaD) l -> AlphaCtx -> l -> [AnyName] -binders1 MNil _ Nil = [] -binders1 (r :+: rs) p (p1 :*: t1) = - bindersD r p p1 ++ binders1 rs p t1 - - -matchR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName) -matchR1 (Data1 _ cons) = loop cons where - loop (Con emb reps : rest) p x y = - case (from emb x, from emb y) of - (Just p1, Just p2) -> match1 reps p p1 p2 - (Nothing, Nothing) -> loop rest p x y - (_,_) -> Nothing - loop [] _ _ _ = error "Impossible" -matchR1 Int1 = \ _ x y -> if x == y then Just empty else Nothing -matchR1 Integer1 = \ _ x y -> if x == y then Just empty else Nothing -matchR1 Char1 = \ _ x y -> if x == y then Just empty else Nothing -matchR1 _ = \ _ _ _ -> Nothing - -match1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Maybe (Perm AnyName) -match1 MNil _ Nil Nil = Just empty -match1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) = do - l1 <- matchD r c p1 p2 - l2 <- match1 rs c t1 t2 - (l1 `join` l2) - - -freshenR1 :: R1 (AlphaD) a -> Fresh m => AlphaCtx -> a -> m (a,Perm AnyName) -freshenR1 (Data1 _ cons) = \ p d -> - case findCon cons d of - Val c rec kids -> do - (l, p') <- freshenL rec p kids - return (to c l, p') -freshenR1 _ = \ _ n -> return (n, empty) - -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 - (xs, p2) <- freshenL rs p ts - (x, p1) <- freshenD r p (swapsD r p p2 t) - return ( x :*: xs, p1 <> p2) - -lfreshenR1 :: LFresh m => R1 AlphaD a -> AlphaCtx -> a -> - (a -> Perm AnyName -> m b) -> m b -lfreshenR1 (Data1 _ cons) = \p d f -> - case findCon cons d of - Val c rec kids -> lfreshenL rec p kids (\ l p' -> f (to c l) p') -lfreshenR1 _ = \ _ n f -> f n empty - -lfreshenL :: LFresh m => MTup (AlphaD) l -> AlphaCtx -> l -> - (l -> Perm AnyName -> m b) -> m b -lfreshenL MNil _ Nil f = f Nil empty -lfreshenL (r :+: rs) p (t :*: ts) f = - lfreshenL rs p ts ( \ y p2 -> - lfreshenD r p (swapsD r p p2 t) ( \ x p1 -> - f (x :*: y) (p1 <> p2))) - - -instance (Rep a) => Alpha (Name a) where - fv' c n@(Nm _ _) | mode c == Term = S.singleton (AnyName n) - fv' c n | mode c == Pat = S.empty - - binders' c n@(Nm _ _) | mode c == Term = [AnyName n] - binders' c n | mode c == Pat = [] - - swapall' c p x = - case apply p (AnyName x) of - AnyName y -> - case cast y of - Just y' -> y' - Nothing -> error "Internal error in swaps': sort mismatch" - - swaps' c p x | mode c == Term = - case apply p (AnyName x) of - AnyName y -> - case cast y of - Just y' -> y' - Nothing -> error "Internal error in swaps': sort mismatch" - swaps' c p x | mode c == Pat = x - - aeq' c x y = x == y - - match' c x y | x == y = Just empty - match' c x y | mode c == Term = - Just $ single (AnyName x) (AnyName y) - match' c _ _ | mode c == Pat = Just empty - - freshen' c nm = case mode c of - Term -> do x <- fresh nm - return (x, single (AnyName nm) (AnyName x)) - Pat -> return (nm, empty) - - lfreshen' c nm f = case mode c of - Term -> do x <- lfresh nm - avoid [AnyName x] $ - f x (single (AnyName nm) (AnyName x)) - Pat -> f nm empty - - -instance Alpha AnyName where - - fv' Term n = S.singleton n - fv' Pat n = S.empty - - binders' Term n = [n] - binders' Pat n = [] - - swapall' c p x = apply p x - - swaps' Term p x = apply p x - swaps' Pat perm x = x - - aeq' c x y = x == y - - match' Term x y = if x == y then Just empty else Just (single x y) - match' Pat x y = Just empty - - freshen' Term (AnyName nm) = do { x <- fresh nm; return(AnyName x, - (single (AnyName nm) (AnyName x))) } - freshen' Pat nm = return (nm, empty) - - lfreshen' c (AnyName nm) f = case mode c of - Term -> do { x <- lfresh nm; avoid [AnyName x] $ f (AnyName x) - (single (AnyName nm) (AnyName x)) } - Pat -> f (AnyName nm) empty - -instance (Alpha a, Alpha b) => Alpha (Bind a b) where - -- default definition of swapall - - -- to swap in a binder, swap the free variables in the - -- pattern, then remove the binders from the permutation - -- and swap in the body - -- ? why don't we just swap everywhere? we need to be - -- able to freshen patterns with annotations - swaps' p pm (B x y) = - B (swaps' (pat p) pm x) (swaps' p pm' y) where - pm' = restrict pm (binders x) - - -- free variables of a binder are the free variables in - -- the annotations in the pattern plus the free variables - -- of the body, minus the binders. - fv' p (B x y) = fv' Pat x `S.union` (fv' p y S.\\ fv' Term x) - - binders' p (B x y) = binders' Pat x ++ - (binders' p y List.\\ binders' Term x) - - -- default definition of freshen' -{- - freshen' p (B x y) = do --- (x', p1) <- freshen' (all p) x -- freshen the binders & annots - (y', p3) <- freshen' p (swaps' p p1 y) -- freshen body - return (B x' y', p1 <> p3) --} - - lfreshen' c (B x y) f = - avoid (S.elems $ fv' c x) $ - lfreshen' (pat c) x (\ x' pm1 -> - lfreshen' c (swaps' c pm1 y) (\ y' pm2 -> - f (B x' y') (pm1 <> pm2))) - - -- this version of aeq seems to work - aeq' p (B x1 y1) (B x2 y2) - -- if the binders match, compare the patterns & bodies - | bx1 == bx2 = aeq' p x1 x2 && aeq' p y1 y2 - -- if any binders of the first appear freely in the - -- second body, not aeq - | (S.fromList bx1) `S.intersection` - (fv' Term y2 S.\\ fv' Term y1) /= S.empty = False - -- otherwise swap the binding variables in the pattern - -- and *all* of the variables in the body - | True = aeq' p x1 (swaps' Term pm x2) && - aeq' p y1 (swapall' Term pm y2) - where bx1 = binders' Term x1 - bx2 = binders' Term x2 - pm = foldl (<>) empty (zipWith single bx1 bx2) - - - -- basic idea of match - -- if binders x1 == binders x2 then - --- match the annots in x1 and x2 and match the bodies y1 y2 - -- if binders x1 /= binders x2 then - -- make sure binders of x1 are not free in the body of y2 - -- swap (x1,x2) in y2 - -- match the annots & match the bodies - -- make sure none of the binders escapes in the resulting match - -- ingredients: - -- match the binders, ignoring the annots - -- match the annots, ignoring the binders - -- list the binding variables - match' p (B x1 y1) (B x2 y2) - | bx1 == bx2 = do - pm1 <- match' Pat x1 x2 - pm2 <- match' p y1 y2 - pm1 `join` pm2 - | (S.fromList bx1) `S.intersection` - (fv' Term y2 S.\\ fv' Term y1) - /= S.empty = Nothing - | True = do - -- make sure that we can match up the binders - -- this will fail if there are repeated vars - pm <- Monad.foldM join empty (zipWith single bx1 bx2) - let x2' = swaps' initial pm x2 - let y2' = swapall' initial pm y2 - pm1 <- match' Pat x1 x2' - pm2 <- match' p y1 y2' - -- note pm2 should not permute binders - -- (see a16) Dropping would give us "set binding" - if S.fromList bx1 `S.intersection` - S.fromList (support pm2) /= S.empty - then Nothing - else pm1 `join` pm2 - where bx1 = binders' Term x1 - bx2 = binders' Term x2 - -instance (Alpha a, Alpha b) => Alpha (Rebind a b) where - - -- free variables of the external binder - -- plus free vars of the annots in the binder - -- plus free vars of the body minus any - -- binding vars of internal binder - fv' p (R x (B ns y)) = fv' p x `S.union` - (fv' p y S.\\ S.fromList ns) - - binders' p (R x (B ns y)) = binders' p x ++ - (binders' p y List.\\ ns) - - - swaps' Term pm (R x (B ns y)) = - R (swaps' Term pm x) (B ns (swaps' Term pm' y)) where - pm' = restrict pm ns - - match' p (R x1 (B n1 y1)) (R x2 (B n2 y2)) = do - px <- match' p x1 x2 -- external names - pb <- match' p (B n1 y1) (B n2 y2) - px `join` pb - - freshen' p (R x (B x1 y)) = do - (x', pm1) <- freshen' p x - (y', pm2) <- freshen' p (swaps' p pm1 y) - return (R x (B x1 y'), pm1 <> pm2) - - -instance (Eq a, Alpha a) => Alpha (Embed a) where - - swaps' Pat pm (Embed t) = Embed (swaps' Term pm t) - swaps' Term pm (Embed t) = Embed t - - fv' Pat (Embed t) = fv' Term t - fv' Term _ = S.empty - - binders' Pat (Embed t) = binders' Term t - binders' Term _ = [] - - - freshen' Pat (Embed t) = do - (t', p) <- freshen' Term t - return (Embed t', p) - freshen' Term a = return (a, empty) - - match' Pat (Embed x) (Embed y) = match' Term x y - match' Term (Embed x) (Embed y) = if x `aeq` y - then Just empty - else Nothing - --- Instances for other types (mostly) use the default definitions. -instance Alpha Bool where -instance Alpha Float where -instance Alpha () where -instance Alpha a => Alpha [a] where -instance Alpha Int where -instance Alpha Integer where -instance Alpha Double where -instance Alpha Char where -instance Alpha a => Alpha (Maybe a) where -instance (Alpha a,Alpha b) => Alpha (Either a b) where -instance (Alpha a,Alpha b) => Alpha (a,b) where -instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c) where -instance (Alpha a, Alpha b,Alpha c, Alpha d) => Alpha (a,b,c,d) -instance (Alpha a, Alpha b,Alpha c, Alpha d, Alpha e) => - Alpha (a,b,c,d,e) -instance (Rep a) => Alpha (R a) where - - --- Definitions of the class members for abstract types. -{- -abs_swaps' :: Alpha a => AlphaCtx -> Perm Name -> a -> a -abs_swaps' _ p s = s -abs_fv' :: Alpha a => AlphaCtx -> a -> [Name] -abs_fv' _ s = [] -abs_freshen' :: (Fresh m, Alpha a) => AlphaCtx -> a -> m (a, Perm Name) -abs_freshen' _ b = return (b, empty) -abs_match' :: (Eq a, Alpha a) => AlphaCtx -> a -> a -> Maybe (Perm Name) -abs_match' _ x1 x2 = if x1 == x2 then Just empty else Nothing --} - -------------------------------------------------------- --- | A monad "m" supports the nextInteger operation if it --- can generate new fresh integers - -class Monad m => HasNext m where - nextInteger :: m Integer - resetNext :: Integer -> m () - --- | A monad "m" supports the "fresh" operation if it --- can generate a new unique names. - -class (Monad m, HasNext m) => Fresh m where - fresh :: Name a -> m (Name a) - fresh (Nm r (s,j)) = do { i <- nextInteger; return (Nm r (s,i)) } - -instance HasNext m => Fresh m where - fresh (Nm r (s,j)) = do { n <- nextInteger; return (Nm r (s,n)) } - --- | Unbind is the destructor of a binding. It ensures that --- the names in the binding b are fresh. -unbind :: (Alpha b,Fresh m,Alpha c) => Bind b c -> m (b,c) -unbind (B x y) = do - (x',perm) <- freshen x - return(x', swaps perm y) - --- | Destruct two bindings simultanously, if they match, using the --- same list of fresh names -unbind2 :: (Fresh m,Alpha b,Alpha c, Alpha d) => - Bind b c -> Bind b d -> m (Maybe (b,c,d)) -unbind2 (B x1 y1) (B x2 y2) = do - (x1', perm1) <- freshen x1 - case match x1' x2 of - (Just perm2) -> - return $ Just (x1', swaps perm1 y1, swaps perm2 y2) - Nothing -> return Nothing - -unbind3 :: (Fresh m,Alpha b,Alpha c, Alpha d, Alpha e) => - Bind b c -> Bind b d -> Bind b e -> m (Maybe (b,c,d,e)) -unbind3 (B x1 y1) (B x2 y2) (B x3 y3) = do - (x1', perm1) <- freshen x1 - case (match x1' x2, match x1' x3) of - (Just perm2, Just perm3) -> - return $ Just (x1', swaps perm1 y1, swaps perm2 y2, swaps perm3 y3) - _ -> return Nothing - ------------------------------------------------------------------ --- | Locally fresh monad --- This is the class of --- monads that support freshness in an (implicit) local scope. Names --- drawn are fresh for this particular scope, but not globally fresh. --- This class has a basic instance based on the reader monad. -class Monad m => LFresh m where - -- | pick a new name that is fresh for the current (implicit) scope. - lfresh :: Rep a => Name a -> m (Name a) - -- | avoid these names when freshening in the subcomputation. - avoid :: [AnyName] -> m a -> m a - --- | Reader monad instance for local freshness class. -instance LFresh (Reader Integer) where - lfresh (Nm r (s,j)) = do { n <- ask; return (Nm r (s, max j (n+1))) } - avoid [] = id - avoid names = local (max k) where - k = maximum (map anyName2Integer names) - --- | Destruct a binding in the LFresh monad. -lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> m (a, b) -lunbind (B a b) = - avoid (S.elems $ fv' initial b) $ error "UNIMP" - - -lunbind2 :: (LFresh m, Alpha b, Alpha c, Alpha d) => - Bind b c -> Bind b d -> m (Maybe (b,c,d)) -lunbind2 (B b1 c) (B b2 d) = do - case match b1 b2 of - Just _ -> do - (b', c') <- lunbind (B b1 c) - return $ error "UNIMP" - Nothing -> return Nothing - -lunbind3 :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) => - Bind b c -> Bind b d -> Bind b e -> m (Maybe (b,c,d,e)) -lunbind3 (B b1 c) (B b2 d) (B b3 e) = do - case (match b1 b2, match b1 b3) of - (Just _, Just _) -> do - (b', c') <- lunbind (B b1 c) - return $ error "UNIMP" - _ -> return Nothing - - ---------------------------------------------------------------- - --- | Capture-avoiding substitution, in a monad so that we can rename --- variables at binding locations and avoid capture - -subst :: (Alpha a, Alpha b, Subst b a) => Name b -> b -> a -> a -subst n u x = - runReader (avoid ([AnyName n] ++ (S.elems $ fv' initial u)++(S.elems $ fv' initial x)) $ lsubst n u x) (0 :: Integer) - -substs :: (Alpha a, Alpha b, Subst b a) => [Name b] -> [b] -> a -> a -substs ns us x = - runReader (avoid ((map AnyName ns) ++ (concatMap (S.elems . (fv' initial)) us)++(S.elems $ fv' initial x)) $ lsubsts ns us x) - (0 :: Integer) - - -class (Rep1 (SubstD b) a) => Subst b a where - isvar :: a -> Maybe (Name b, b -> a) - isvar x = Nothing - - lsubst :: LFresh m => Name b -> b -> a -> m a - lsubst n u x = - case isvar x of - Just (m, f) | m == n -> return (f u) - Just (_, _) -> return x - Nothing -> substR1 rep1 n u x - - - lsubsts :: LFresh m => [Name b] -> [b] -> a -> m a - lsubsts ns us x = - case isvar x of - Just (m, f) -> case m `List.elemIndex` ns of - Just i -> return (f (us !! i)) - Nothing -> return x - Nothing -> substsR1 rep1 ns us x - - -data SubstD b a = SubstD { - substD :: LFresh m => Name b -> b -> a -> m a - ,substsD :: LFresh m => [Name b] -> [b] -> a -> m a -} - -instance Subst b a => Sat (SubstD b a) where - dict = SubstD lsubst lsubsts - -substR1 :: LFresh m => R1 (SubstD b) a -> Name b -> b -> a -> m a -substR1 (Data1 _ cons) = \ x y d -> - case (findCon cons d) of - Val c rec kids -> do - w <- mapM_l (\z -> substD z x y) rec kids - return (to c w) -substR1 _ = \ _ _ c -> return c - -substsR1 :: LFresh m => R1 (SubstD b) a -> [Name b] -> [b] -> a -> m a -substsR1 (Data1 _ cons) = \ x y d -> - case (findCon cons d) of - Val c rec kids -> do - z <- mapM_l (\ w -> substsD w x y) rec kids - return (to c z) -substsR1 _ = \ _ _ c -> return c - -instance Subst c AnyName where - -instance Subst b Int where -instance Subst b Bool where -instance Subst b () where -instance Subst b Char where -instance Subst b Integer where -instance Subst b Float where -instance Subst b Double where -instance (Subst c a, Subst c b) => Subst c (a,b) where -instance (Subst c a, Subst c b, Subst c d) => Subst c (a,b,d) where -instance (Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a,b,d,e) where -instance (Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a,b,d,e,f) where - -instance (Subst c a) => Subst c [a] where -instance (Subst c a) => Subst c (Maybe a) where -instance (Subst c a, Subst c b) => Subst c (Either a b) where - -instance Rep a => Subst b (R a) where -instance Rep a => Subst b (Name a) where - - -instance (Subst c a, Alpha a, Subst c b, Alpha b) => - Subst c (Bind a b) where - lsubst n u (B a b) = - lfreshen' Term a ( \ a' p -> do - let b' = swapall' Term p b - a'' <- lsubst n u a' - b'' <- lsubst n u b' - return (B a'' b'')) - - lsubsts n u (B a b) = - lfreshen' Term a ( \ a' p -> do - a'' <- lsubsts n u a' - let b' = swaps' Pat p (swaps' Term p b) - b'' <- lsubsts n u b' - return (B a'' b'')) - -instance (Subst c b, Subst c a, Alpha a, Alpha b) => - Subst c (Rebind a b) where -instance (Subst c a) => Subst c (Embed a) where - - --------------------- TESTING CODE -------------------------------- -data Exp = V (Name Exp) - | A Exp Exp - | L (Bind (Name Exp) Exp) deriving (Show) - -$(derive [''Exp]) - -instance Alpha Exp -instance Subst Exp Exp where - isvar (V n) = Just (n, id) - isvar _ = Nothing - --- deriving instance Eq Exp --- deriving instance Ord Exp - -nameA, nameB, nameC :: Name Exp -nameA = string2Name "A" -nameB = string2Name "B" -nameC = string2Name "C" - -assert :: String -> Bool -> IO () -assert s True = return () -assert s False = print ("Assertion " ++ s ++ " failed") - -do_tests :: () -do_tests = - unsafePerformIO $ do - tests_aeq - tests_fv - tests_big - tests_subst - -perm = single (AnyName nameA)(AnyName nameB) - -naeq x y = not (aeq x y) - -a10a = bind (rebind (nameA, Embed nameC) ()) nameA -a10b = bind (rebind (nameB, Embed nameC) ()) nameB - -a10c = bind (rebind (nameA, Embed nameA) ()) nameA -a10d = bind (rebind (nameB, Embed nameA) ()) nameB - -tests_aeq = do - assert "a1" $ (bind nameA nameA) `naeq` (bind nameA nameB) - assert "a2" $ (bind nameA nameA) `aeq` (bind nameA nameA) - assert "a3" $ (bind nameA nameA) `aeq` (bind nameB nameB) - assert "a4" $ (bind nameA nameB) `naeq` (bind nameB nameA) - assert "a5" $ (bind (nameA, Embed nameB) nameA) `naeq` - (bind (nameA, Embed nameC) nameA) - assert "a6" $ (bind (nameA, Embed nameB) nameA) `aeq` - (bind (nameA, Embed nameB) nameA) - assert "a7" $ (bind (nameA, Embed nameB) nameA) `aeq` - (bind (nameB, Embed nameB) nameB) - assert "a8" $ rebind nameA nameB `naeq` rebind nameB nameB - assert "a9" $ rebind nameA nameA `naeq` rebind nameB nameB - assert "a9a" $ (bind (rebind nameA (Embed nameA)) nameA) `aeq` - (bind (rebind nameB (Embed nameB)) nameB) - assert "a10" $ bind (rebind (nameA, Embed nameA) ()) nameA `aeq` - bind (rebind (nameB, Embed nameA) ()) nameB - assert "a10a" $ a10a `aeq` a10b - assert "a11" $ bind (rebind (nameA, Embed nameA) ()) nameA `naeq` - bind (rebind (nameB, Embed nameB) ()) nameB - assert "a12" $ bind (Embed nameA) () `naeq` bind (Embed nameB) () - assert "a13" $ bind (Embed nameA) () `aeq` bind (Embed nameA) () - assert "a14" $ bind (rebind (Embed nameA) ()) () `naeq` - bind (rebind (Embed nameB) ()) () - assert "a15" $ (rebind (nameA, Embed nameA) ()) `naeq` - (rebind (name4, Embed nameC) ()) - assert "a16" $ bind (nameA, nameB) nameA `naeq` - bind (nameB, nameA) nameA - assert "a17" $ bind (nameA, nameB) nameA `naeq` bind (nameA, nameB) nameB - assert "a18" $ (nameA, nameA) `naeq` (nameA, nameB) - assert "a19" $ match (nameA, nameA) (nameB, nameC) == Nothing - assert "a20" $ (L (bind name2 (L (bind name3 (L (bind name4 (A (V name2) (A (V name3) (V name4))))))))) `aeq` (L (bind name1 (L (bind name2 (L (bind name3 (A (V name1) (A (V name2) (V name3))))))))) - -emptyNE :: Set (Name Exp) -emptyNE = S.empty - -tests_fv = do - assert "f1" $ fv (bind nameA nameA) == emptyNE - assert "f2" $ fv' Pat (bind nameA nameA) == S.empty - assert "f3" $ fv (bind (rebind nameA (Embed nameA)) nameA) == emptyNE - assert "f4" $ fv (bind nameA nameB) == S.singleton nameB - assert "f5" $ fv (bind (nameA, Embed nameB) nameA) == S.singleton nameB - assert "f7" $ fv (bind (nameB, Embed nameB) nameB) == S.singleton nameB - assert "f8" $ fv (rebind nameA nameB) == S.fromList [nameA, nameB] - assert "f9" $ fv' Pat (rebind nameA nameA) == S.empty - assert "f9a" $ fv (rebind nameA (Embed nameA)) == S.singleton nameA - assert "f9b" $ fv' Pat (rebind nameA (Embed nameA)) == S.empty - assert "f10" $ fv (rebind (nameA, Embed nameA) ()) == S.singleton nameA - assert "f11" $ fv' Pat (rebind (nameA, Embed nameA) ()) == S.singleton (AnyName nameA) - assert "f10a" $ fv (rebind (nameA, Embed nameB) ()) == S.singleton nameA - assert "f11a" $ fv' Pat (rebind (nameA, Embed nameB) ()) == S.singleton (AnyName nameB) - - - assert "f12" $ fv (bind (Embed nameA) ()) == S.singleton nameA - assert "f12a" $ fv' Pat (bind (Embed nameA) ()) == S.singleton (AnyName nameA) - - assert "f14" $ fv (rebind (Embed nameA) ()) == emptyNE - assert "f14a" $ fv' Pat (rebind (Embed nameA) ()) == S.singleton (AnyName nameA) - -tests_subst = do - assert "s1" $ subst nameA (V nameB) (V nameA) `aeq` (V nameB) - assert "s2" $ subst nameA (V nameB) (V nameC) `aeq` (V nameC) - assert "s3" $ subst nameA (V nameB) (L (bind nameA (V nameA))) `aeq` - (L (bind nameA (V nameA))) - - assert "s4" $ subst nameA (V nameB) (L (bind nameB (V nameB))) `aeq` - (L (bind nameA (V nameA))) - - assert "s5" $ subst nameA (V nameB) (L (bind nameC (V nameA))) `aeq` - (L (bind nameC (V nameB))) - - assert "s6" $ subst nameA (V nameA) (L (bind nameC (V nameA))) `aeq` - (L (bind nameC (V nameA))) - - assert "s7" $ subst nameA (V nameA) (L (bind nameA (V nameB))) `aeq` - (L (bind nameA (V nameB))) - assert "s9" $ subst name1 (V name1) - (L (bind name1 (L (bind name2 (L (bind name3 - (A (V name1) (A (V name2) (V name3))))))))) `aeq` - (L (bind name1 (L (bind name2 (L (bind name3 - (A (V name1) (A (V name2) (V name3))))))))) - - -mkbig :: [Name Exp] -> Exp -> Exp -mkbig (n : names) body = - L (bind n (mkbig names (A (V n) body))) -mkbig [] body = body - -big1 = mkbig (map integer2Name (take 100 [1 ..])) (V name11) -big2 = mkbig (map integer2Name (take 101 [1 ..])) (V name11) - -tests_big = do - assert "b1" $ big1 `naeq` big2 - assert "b2" $ fv big1 == emptyNE - assert "b3" $ big1 `aeq` subst name11 (V name11) big1 - - diff --git a/Unbound/Nominal/Name.hs b/Unbound/Nominal/Name.hs deleted file mode 100644 --- a/Unbound/Nominal/Name.hs +++ /dev/null @@ -1,130 +0,0 @@ -{-# LANGUAGE RankNTypes - , TemplateHaskell - , GADTs - , FlexibleInstances - , MultiParamTypeClasses - #-} ----------------------------------------------------------------------- --- | --- Module : Unbound.Nominal.Name --- License : BSD-like (see LICENSE) --- --- Maintainer : Stephanie Weirich --- Stability : experimental --- Portability : XXX --- --- XXX write me ----------------------------------------------------------------------- - -module Unbound.Nominal.Name where --- XXX todo make explicit export list - -import Generics.RepLib - --- | 'Name's are things that get bound. This type is intentionally --- abstract; to create a 'Name' you can use 'string2Name' or --- 'integer2Name'. The type parameter is a tag, or /sort/, which tells --- us what sorts of things this name may stand for. The sort must --- be an instance of the 'Rep' type class. -data Name a - = Nm (R a) (String, Integer) -- free names - deriving (Eq, Ord) - --- | A name with a hidden (existentially quantified) sort. -data AnyName = forall a. Rep a => AnyName (Name a) - --- AnyName has an existential in it, so we cannot create a complete --- representation for it, unfortunately. - -$(derive_abstract [''AnyName]) - -instance Show AnyName where - show (AnyName n1) = show n1 - -instance Eq AnyName where - (AnyName n1) == (AnyName n2) = - case gcastR (getR n1) (getR n2) n1 of - Just n1' -> n1' == n2 - Nothing -> False - -instance Ord AnyName where - compare (AnyName n1) (AnyName n2) = - case compareR (getR n1) (getR n2) of - EQ -> case gcastR (getR n1) (getR n2) n1 of - Just n1' -> compare n1' n2 - Nothing -> error "Panic: equal types are not equal in Ord AnyName instance!" - ord -> ord - ------------------------------------------------------------- --- Utilities ------------------------------------------------------------- - --- some convenient names for testing -name1, name2, name3, name4, name5, name6, name7, name8, name9, name10, name11 - :: Rep a => Name a -name1 = integer2Name 1 -name2 = integer2Name 2 -name3 = integer2Name 3 -name4 = integer2Name 4 -name5 = integer2Name 5 -name6 = integer2Name 6 -name7 = integer2Name 7 -name8 = integer2Name 8 -name9 = integer2Name 9 -name10 = integer2Name 10 -name11 = integer2Name 11 - ---instance Read Name where --- read s = error "FIXME" - -instance Show (Name a) where - show (Nm _ ("",n)) = "_" ++ (show n) - show (Nm _ (x,0)) = x - show (Nm _ (x,n)) = x ++ (show n) - --- | Get the integer index of a 'Name'. -name2Integer :: Name a -> Integer -name2Integer (Nm _ (_,x)) = x - - --- | Get the string part of a 'Name'. -name2String :: Name a -> String -name2String (Nm _ (s,_)) = s - - --- | Get the integer index of an 'AnyName'. -anyName2Integer :: AnyName -> Integer -anyName2Integer (AnyName nm) = name2Integer nm - --- | Get the string part of an 'AnyName'. -anyName2String :: AnyName -> String -anyName2String (AnyName nm) = name2String nm - -toSortedName :: Rep a => AnyName -> Maybe (Name a) -toSortedName (AnyName n) = gcastR (getR n) rep n - --- | Create a 'Name' from an 'Integer'. -integer2Name :: Rep a => Integer -> Name a -integer2Name n = makeName "" n - --- | Create a 'Name' from a 'String'. -string2Name :: Rep a => String -> Name a -string2Name s = makeName s 0 - --- | Convenient synonym for 'string2Name'. -s2n :: Rep a => String -> Name a -s2n = string2Name - --- | Create a 'Name' from a @String@ and an @Integer@ index. -makeName :: Rep a => String -> Integer -> Name a -makeName s i = Nm rep (s,i) - --- | Determine the sort of a 'Name'. -getR :: Name a -> R a -getR (Nm r _) = r - - --- | Change the sort of a name -translate :: (Rep b) => Name a -> Name b -translate (Nm _ x) = Nm rep x - diff --git a/Unbound/PermM.hs b/Unbound/PermM.hs --- a/Unbound/PermM.hs +++ b/Unbound/PermM.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE PatternGuards #-} ---------------------------------------------------------------------- -- | -- Module : Unbound.Perm @@ -10,17 +11,17 @@ ---------------------------------------------------------------------- module Unbound.PermM ( - Perm, single, compose, apply, support, isid, join, empty, restrict, mkPerm + Perm(..), permValid, single, compose, apply, support, isid, join, empty, restrict, mkPerm ) where import Data.Monoid import Data.List import Data.Map (Map) -import qualified Data.Map as Map -import System.IO.Unsafe - -(<>) :: Monoid m => m -> m -> m -(<>) = mappend +import Data.Function (on) +import qualified Data.Map as M +import qualified Data.Set as S +import Control.Arrow ((&&&)) +import Control.Monad ((>=>)) -- | A /permutation/ is a bijective function from names to names -- which is the identity on all but a finite set of names. They @@ -28,33 +29,39 @@ -- 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) + -- a Map sends every key uniquely to a value by construction. So if + -- every value is also a key, the sizes of the domain and range must + -- be equal and hence the mapping is a bijection. + instance Ord a => Eq (Perm a) where (Perm p1) == (Perm p2) = - all (\x -> Map.findWithDefault x x p1 == Map.findWithDefault x x p2) (Map.keys p1) && - all (\x -> Map.findWithDefault x x p1 == Map.findWithDefault x x p2) (Map.keys p2) + all (\x -> M.findWithDefault x x p1 == M.findWithDefault x x p2) (M.keys p1) && + all (\x -> M.findWithDefault x x p1 == M.findWithDefault x x p2) (M.keys p2) instance Show a => Show (Perm a) where show (Perm p) = show p -- | Apply a permutation to an element of the domain. apply :: Ord a => Perm a -> a -> a -apply (Perm p) x = Map.findWithDefault x x p +apply (Perm p) x = M.findWithDefault x x p -- | Create a permutation which swaps two elements. single :: Ord a => a -> a -> Perm a -single x y = if x == y then Perm Map.empty else - Perm (Map.insert x y (Map.insert y x Map.empty)) +single x y = if x == y then Perm M.empty else + Perm (M.insert x y (M.insert y x M.empty)) -- | The empty (identity) permutation. empty :: Perm a -empty = Perm Map.empty +empty = Perm M.empty -- | Compose two permutations. The right-hand permutation will be -- applied first. compose :: Ord a => Perm a -> Perm a -> Perm a compose (Perm b) (Perm a) = - Perm (Map.fromList ([ (x,Map.findWithDefault y y b) | (x,y) <- Map.toList a] - ++ [ (x, Map.findWithDefault x x b) | x <- Map.keys b, Map.notMember x a])) + Perm (M.fromList ([ (x,M.findWithDefault y y b) | (x,y) <- M.toList a] + ++ [ (x, M.findWithDefault x x b) | x <- M.keys b, M.notMember x a])) -- | Permutations form a monoid under composition. instance Ord a => Monoid (Perm a) where @@ -64,79 +71,61 @@ -- | Is this the identity permutation? isid :: Ord a => Perm a -> Bool isid (Perm p) = - Map.foldrWithKey (\ a b r -> r && a == b) True p + M.foldrWithKey (\ a b r -> r && a == b) True p -- | /Join/ two permutations by taking the union of their relation -- graphs. Fail if they are inconsistent, i.e. map the same element -- to two different elements. join :: Ord a => Perm a -> Perm a -> Maybe (Perm a) join (Perm p1) (Perm p2) = - let overlap = Map.intersectionWith (==) p1 p2 in - if Map.fold (&&) True overlap then - Just (Perm (Map.union p1 p2)) + let overlap = M.intersectionWith (==) p1 p2 in + if M.fold (&&) True overlap then + Just (Perm (M.union p1 p2)) else Nothing -- | The /support/ of a permutation is the set of elements which are -- not fixed. support :: Ord a => Perm a -> [a] -support (Perm p) = [ x | x <- Map.keys p, Map.findWithDefault x x p /= x] +support (Perm p) = [ x | x <- M.keys p, M.findWithDefault x x p /= x] -- | Restrict a permutation to a certain domain. restrict :: Ord a => Perm a -> [a] -> Perm a -restrict (Perm p) l = Perm (foldl' (\p' k -> Map.delete k p') p l) +restrict (Perm p) l = Perm (foldl' (\p' k -> M.delete k p') p l) +-- | A partial permutation consists of two maps, one in each direction +-- (inputs -> outputs and outputs -> inputs). +data PartialPerm a = PP (M.Map a a) (M.Map a a) + deriving Show + +emptyPP :: PartialPerm a +emptyPP = PP M.empty M.empty + +extendPP :: Ord a => a -> a -> PartialPerm a -> Maybe (PartialPerm a) +extendPP x y pp@(PP mfwd mrev) + | Just y' <- M.lookup x mfwd = if y == y' then Just pp + else Nothing + | Just x' <- M.lookup y mrev = if x == x' then Just pp + else Nothing + | otherwise = Just $ PP (M.insert x y mfwd) (M.insert y x mrev) + +-- | Convert a partial permutation into a full permutation by closing +-- off any remaining open chains into a cycles. +ppToPerm :: Ord a => PartialPerm a -> Perm a +ppToPerm (PP mfwd mrev) = Perm $ foldr (uncurry M.insert) mfwd + (map (findEnd &&& id) chainStarts) + -- beginnings of open chains are elements which map to + -- something in the forward direction but have no ancestor. + where chainStarts = S.toList (M.keysSet mfwd `S.difference` M.keysSet mrev) + findEnd x = case M.lookup x mfwd of + Nothing -> x + Just x' -> findEnd x' + -- | @mkPerm l1 l2@ creates a permutation that sends @l1@ to @l2@. -- Fail if there is no such permutation, either because the lists -- have different lengths or because they are inconsistent (which -- can only happen if @l1@ or @l2@ have repeated elements). mkPerm :: Ord a => [a] -> [a] -> Maybe (Perm a) mkPerm xs ys - | length xs == length ys = foldl' (\mp p -> mp >>= join p) - (Just empty) - (zipWith single xs ys) - | otherwise = Nothing - ---------------------------------------------------------------------- -seteq :: Ord a => [a] -> [a] -> Bool -seteq x y = nub (sort x) == nub (sort y) - - -assert :: String -> Bool -> IO () -assert s True = return () -assert s False = print ("Assertion " ++ s ++ " failed") - -do_tests :: () -do_tests = - unsafePerformIO $ do - tests_apply - tests_isid - tests_support - tests_join - -tests_join = do - assert "j1" $ join empty (empty :: Perm Int) == Just empty - assert "j2" $ join (single 1 2) empty == Just (single 1 2) - assert "j3" $ join (single 1 2) (single 2 1) == Just (single 1 2) - assert "j4" $ join (single 1 2) (single 1 3) == Nothing - -tests_apply = do - assert "a1" $ apply empty 1 == 1 - assert "a2" $ apply (single 1 2) 1 == 2 - assert "a3" $ apply (single 2 1) 1 == 2 - assert "a4" $ apply ((single 1 2) <> (single 2 1)) 1 == 1 - -tests_isid = do - assert "i1" $ isid (empty :: Perm Int) == True - assert "i2" $ isid (single 1 2) == False - assert "i3" $ isid (single 1 1) == True - assert "i4" $ isid ((single 1 2) <> (single 1 2)) == True - assert "i5" $ isid ((single 1 2) <> (single 2 1)) == True - assert "i6" $ isid ((single 1 2) <> (single 3 2)) == False - -tests_support = do - assert "s1" $ support (empty :: Perm Int) `seteq` [] - assert "s2" $ support (single 1 2) `seteq` [1,2] - assert "s3" $ support (single 1 1) `seteq` [] - assert "s4" $ support ((single 1 2) <> (single 1 2)) `seteq` [] - assert "s5" $ support ((single 1 2) <> (single 2 1)) `seteq` [] - assert "s6" $ support ((single 1 2) <> (single 3 2)) `seteq` [1,2,3] + | length xs /= length ys = Nothing + | otherwise = + fmap ppToPerm . ($emptyPP) . foldr (>=>) return $ zipWith extendPP xs ys diff --git a/examples/Basic.hs b/examples/Basic.hs --- a/examples/Basic.hs +++ b/examples/Basic.hs @@ -147,11 +147,11 @@ -- -- finally, we define generalized versions of fold left and -- fold right for the Tree type constructor. -instance Fold Tree where - foldRight op = rreduceR1 (rTree1 (RreduceD { rreduceD = op }) - (RreduceD { rreduceD = foldRight op})) - foldLeft op = lreduceR1 (rTree1 (LreduceD { lreduceD = op }) - (LreduceD { lreduceD = foldLeft op })) +-- instance Fold Tree where +-- foldRight op = rreduceR1 (rTree1 ( RreduceD { rreduceD = op } +-- , RreduceD { rreduceD = foldRight op})) +-- foldLeft op = lreduceR1 (rTree1 ( LreduceD { lreduceD = op } +-- , LreduceD { lreduceD = foldLeft op })) assert :: String -> Bool -> IO () assert s True = return () @@ -172,13 +172,13 @@ -- assert "s1" (subtrees t1 == [Node (Leaf 3) (Leaf 4),Node (Leaf 5) (Leaf 6)]) - assert "s2" (gsum t1 == 18) - assert "s3" (gsum t2 == 27) +-- assert "s2" (gsum t1 == 18) +-- assert "s3" (gsum t2 == 27) -- assert "i1" (increase 0.1 s1 == C [D "Types" (M (E (P "Stephanie") (S 1100.0))) [PU (E (P "Michael") (S 55.0)),PU (E (P "Samuel") (S 55.0)),PU (E (P "Theodore") (S 55.0))],D "Terms" (M (E (P "Stephanie") (S 220.0))) [DU (D "Shipping" (M (E (P "Alice") (S 3300.0))) [])]]) assert "i2" (s1 < (increase 0.2 s1)) -- - assert "f1" (gproduct t1 == 360) - assert "f2" (count t1 == 4) +-- assert "f1" (gproduct t1 == 360) +-- assert "f2" (count t1 == 4) diff --git a/test/PermTest.hs b/test/PermTest.hs new file mode 100644 --- /dev/null +++ b/test/PermTest.hs @@ -0,0 +1,93 @@ +import Unbound.PermM + +import Data.Maybe (isJust) +import Data.Monoid +import Data.List (nub, sort) +import qualified Data.Map as M +import System.IO.Unsafe + +import Test.QuickCheck + +instance (Ord a, Arbitrary a) => Arbitrary (Perm a) where + arbitrary = (mconcat . map (uncurry single)) `fmap` arbitrary + +--------------------------------------------------------------------- +(<>) :: Monoid m => m -> m -> m +(<>) = mappend + +seteq :: Ord a => [a] -> [a] -> Bool +seteq x y = nub (sort x) == nub (sort y) + + +assert :: String -> Bool -> IO () +assert s True = return () +assert s False = print ("Assertion " ++ s ++ " failed") + +do_tests :: () +do_tests = + unsafePerformIO $ do + tests_apply + tests_isid + tests_support + tests_join + +tests_join = do + assert "j1" $ join empty (empty :: Perm Int) == Just empty + assert "j2" $ join (single 1 2) empty == Just (single 1 2) + assert "j3" $ join (single 1 2) (single 2 1) == Just (single 1 2) + assert "j4" $ join (single 1 2) (single 1 3) == Nothing + +tests_apply = do + assert "a1" $ apply empty 1 == 1 + assert "a2" $ apply (single 1 2) 1 == 2 + assert "a3" $ apply (single 2 1) 1 == 2 + assert "a4" $ apply ((single 1 2) <> (single 2 1)) 1 == 1 + +tests_isid = do + assert "i1" $ isid (empty :: Perm Int) == True + assert "i2" $ isid (single 1 2) == False + assert "i3" $ isid (single 1 1) == True + assert "i4" $ isid ((single 1 2) <> (single 1 2)) == True + assert "i5" $ isid ((single 1 2) <> (single 2 1)) == True + assert "i6" $ isid ((single 1 2) <> (single 3 2)) == False + +prop_isid :: Perm Int -> Bool +prop_isid p = isid p == (all (\x -> apply p x == x) $ support p) + +tests_support = do + assert "s1" $ support (empty :: Perm Int) `seteq` [] + assert "s2" $ support (single 1 2) `seteq` [1,2] + assert "s3" $ support (single 1 1) `seteq` [] + assert "s4" $ support ((single 1 2) <> (single 1 2)) `seteq` [] + assert "s5" $ support ((single 1 2) <> (single 2 1)) `seteq` [] + assert "s6" $ support ((single 1 2) <> (single 3 2)) `seteq` [1,2,3] + +prop_support :: Perm Int -> Int -> Bool +prop_support p i = (apply p i /= i) == (i `elem` support p) + +------------------------------------------------------------ + +prop_support_empty :: Bool +prop_support_empty = support (empty :: Perm Int) == [] + +prop_compose_empty_l :: Perm Int -> Int -> Bool +prop_compose_empty_l p i = apply p i == apply (compose empty p) i + +prop_compose_empty_r :: Perm Int -> Int -> Bool +prop_compose_empty_r p i = apply p i == apply (compose p empty) i + +prop_compose :: Perm Int -> Perm Int -> Int -> Bool +prop_compose p1 p2 i = apply (compose p1 p2) i == apply p1 (apply p2 i) + +prop_mkPerm_perm :: [Int] -> [Int] -> Bool +prop_mkPerm_perm xs ys | Just p <- mkPerm xs ys = map (apply p) xs == ys + | otherwise = True + +prop_mkPerm_fail :: [Int] -> [Int] -> Property +prop_mkPerm_fail xs ys = length xs == length ys && nub xs == xs && nub ys == ys ==> isJust (mkPerm xs ys) + +prop_mkPerm_valid :: [Int] -> [Int] -> Bool +prop_mkPerm_valid xs ys = maybe True permValid (mkPerm xs ys) + +prop_valid :: Perm Int -> Bool +prop_valid = permValid diff --git a/test/Test.hs b/test/Test.hs new file mode 100644 --- /dev/null +++ b/test/Test.hs @@ -0,0 +1,153 @@ +{-# LANGUAGE TemplateHaskell + , MultiParamTypeClasses + , FlexibleInstances + , FlexibleContexts + , ScopedTypeVariables + , UndecidableInstances + #-} + +module Unbound.LocallyNameless.Test where + +import qualified Data.Set as S + +import Unbound.LocallyNameless hiding (GT) +import Unbound.LocallyNameless.Alpha +import Unbound.LocallyNameless.Name +import Unbound.PermM + +-------------------- TESTING CODE -------------------------------- +data Exp = V (Name Exp) + | A Exp Exp + | L (Bind (Name Exp) Exp) deriving (Show) + +$(derive [''Exp]) + +instance Alpha Exp +instance Subst Exp Exp where + isvar (V n) = Just (SubstName n) + isvar _ = Nothing + +nameA, nameB, nameC :: Name Exp +nameA = integer2Name 1 +nameB = integer2Name 2 +nameC = integer2Name 3 + +assert :: String -> Bool -> IO () +assert s True = return () +assert s False = print ("Assertion " ++ s ++ " failed") + +do_tests :: IO () +do_tests = do + tests_aeq + tests_fv + tests_big + tests_nth + tests_acompare + +perm = single nameA nameB + +naeq x y = not (aeq x y) + +tests_aeq = do + assert "a1" $ (bind nameA nameA) `naeq` (bind nameA nameB) + assert "a2" $ (bind nameA nameA) `aeq` (bind nameA nameA) + assert "a3" $ (bind nameA nameA) `aeq` (bind nameB nameB) + assert "a4" $ (bind nameA nameB) `naeq` (bind nameB nameA) + assert "a5" $ (bind (nameA, Embed nameB) nameA) `naeq` + (bind (nameA, Embed nameC) nameA) + assert "a6" $ (bind (nameA, Embed nameB) nameA) `aeq` + (bind (nameA, Embed nameB) nameA) + assert "a7" $ (bind (nameA, Embed nameB) nameA) `aeq` + (bind (nameB, Embed nameB) nameB) + assert "a8" $ rebind nameA nameB `naeq` rebind nameB nameB + assert "a9" $ rebind nameA nameA `naeq` rebind nameB nameB + assert "a9" $ (bind (rebind nameA (Embed nameA)) nameA) `aeq` + (bind (rebind nameB (Embed nameB)) nameB) + assert "a10" $ bind (rebind (nameA, Embed nameA) ()) nameA `aeq` + bind (rebind (nameB, Embed nameA) ()) nameB + assert "a11" $ bind (rebind (nameA, Embed nameA) ()) nameA `naeq` + bind (rebind (nameB, Embed nameB) ()) nameB + assert "a12" $ bind (Embed nameA) () `naeq` bind (Embed nameB) () + assert "a13" $ bind (Embed nameA) () `aeq` bind (Embed nameA) () + assert "a14" $ bind (rebind (Embed nameA) ()) () `naeq` + bind (rebind (Embed nameB) ()) () + assert "a15" $ (rebind (nameA, Embed nameA) ()) `naeq` + (rebind (nameA, Embed nameC) ()) + assert "a16" $ bind (nameA, nameB) nameA `naeq` bind (nameB, nameA) nameA + assert "a17" $ bind (nameA, nameB) nameA `naeq` bind (nameA, nameB) nameB + assert "a18" $ (nameA, nameA) `naeq` (nameA, nameB) +-- assert "a19" $ match (nameA, nameA) (nameB, nameC) == Nothing + +emptyNE :: S.Set (Name Exp) +emptyNE = S.empty + +tests_fv = do + assert "f1" $ fv (bind nameA nameA) == emptyNE + assert "f2" $ fv' (pat initial) (bind nameA nameA) == S.empty + assert "f4" $ fv (bind nameA nameB) == S.singleton nameB + assert "f5" $ fv (bind (nameA, Embed nameB) nameA) == S.singleton nameB + assert "f7" $ fv (bind (nameB, Embed nameB) nameB) == S.singleton nameB + assert "f8" $ fv (rebind nameA nameB) == S.fromList [nameA, nameB] + assert "f9" $ fv' (pat initial) (rebind nameA nameA) == S.empty + assert "f3" $ fv (bind (rebind nameA (Embed nameA)) nameA) == emptyNE + assert "f10" $ fv (rebind (nameA, Embed nameA) ()) == S.singleton nameA + assert "f11" $ fv' (pat initial) (rebind (nameA, Embed nameA) ()) == S.singleton (AnyName nameA) + assert "f12" $ fv (bind (Embed nameA) ()) == S.singleton nameA + assert "f14" $ fv (rebind (Embed nameA) ()) == emptyNE + +mkbig :: [Name Exp] -> Exp -> Exp +mkbig (n : names) body = + L (bind n (mkbig names (A (V n) body))) +mkbig [] body = body + +big1 = mkbig (map integer2Name (take 100 [1 ..])) (V nameA) +big2 = mkbig (map integer2Name (take 101 [1 ..])) (V nameA) + + +tests_nth = do + assert "n1" $ nthpat ([nameA],nameB) 0 == AnyName nameA + assert "n2" $ nthpat ([nameA],nameB) 1 == AnyName nameB + assert "n3" $ nthpat (nameA, nameB) 0 == AnyName nameA + assert "p1" $ findpat ([nameA],nameB) (AnyName nameA) == Just 0 + assert "p2" $ findpat ([nameA],nameB) (AnyName nameB) == Just 1 + assert "p3" $ findpat ([nameA],nameB) (AnyName nameC) == Nothing + +tests_big = do + assert "b1" $ big1 `naeq` big2 + assert "b2" $ fv big1 == emptyNE + assert "b3" $ big1 `aeq` subst nameA (V nameA) big1 + +tests_acompare = do + -- Names compare in the obvious way. + assert "ac1" $ acompare nameA nameB == LT + assert "ac2" $ acompare nameB nameB == EQ + assert "ac3" $ acompare nameB nameA == GT + -- structured date compares lexicographically + assert "ac4" $ acompare (A (V nameA) (V nameA)) (A (V nameA) (V nameA)) == EQ + assert "ac5" $ acompare (A (V nameA) (V nameA)) (A (V nameA) (V nameB)) == LT + assert "ac6" $ acompare (A (V nameA) (V nameB)) (A (V nameA) (V nameA)) == GT + assert "ac7" $ acompare (A (V nameA) (V nameA)) (A (V nameB) (V nameA)) == LT + assert "ac8" $ acompare (A (V nameB) (V nameA)) (A (V nameA) (V nameA)) == GT + assert "ac9" $ acompare (A (V nameB) (V nameA)) (A (V nameA) (V nameB)) == GT + -- comparison goes under binders, alpha-respectingly. + assert "ac10" $ acompare (bind nameA (A (V nameA) (V nameA))) (bind nameA (A (V nameA) (V nameA))) == EQ + assert "ac11" $ acompare (bind nameA (A (V nameA) (V nameA))) (bind nameA (A (V nameA) (V nameB))) == GT + assert "ac12" $ acompare (bind nameC (A (V nameC) (V nameA))) (bind nameA (A (V nameA) (V nameB))) == LT + -- non-matching binders handled alpha-respectingly. + assert "ac13" $ acompare (bind [nameA] nameA) (bind [nameA,nameB] nameA) + == acompare (bind [nameC] nameC) (bind [nameA,nameB] nameA) + assert "ac14" $ acompare (bind [nameA,nameB] nameA) (bind [nameA] nameA) + == acompare (bind [nameC,nameB] nameC) (bind [nameA] nameA) + -- non-binding stuff in patterns gets compared + assert "ac15" $ acompare (Embed nameA) (Embed nameB) == LT + assert "ac16" $ acompare (bind (nameC, Embed nameA) (A (V nameC) (V nameC))) + (bind (nameC, Embed nameB) (A (V nameC) (V nameC))) == LT + assert "ac17" $ acompare (bind (nameC, Embed nameA) (A (V nameB) (V nameB))) + (bind (nameC, Embed nameB) (A (V nameA) (V nameA))) == LT + -- TODO: do we need anything special for rebind? For AnyName? + +-- properties +-- if match t1 t2 = Some p then swaps p t1 = t2 + +main :: IO () +main = do_tests diff --git a/unbound.cabal b/unbound.cabal --- a/unbound.cabal +++ b/unbound.cabal @@ -1,10 +1,10 @@ name: unbound -version: 0.2.3 +version: 0.2.4 license: BSD3 license-file: LICENSE build-type: Simple cabal-version: >= 1.6 -tested-with: GHC == 7.0.1 +tested-with: GHC == 7.0.1, GHC == 7.0.3 author: Stephanie Weirich maintainer: Brent Yorgey Stephanie Weirich @@ -15,7 +15,7 @@ examples/*.hs, tutorial/Makefile, tutorial/Tutorial.lhs, - Unbound/LocallyNameless/Test.hs + test/*.hs synopsis: Generic support for programming with names and binders description: Specify the binding structure of your data type with an @@ -24,6 +24,10 @@ alpha-equivalence, free variable calculation, capture-avoiding substitution, and more. See "Unbound.LocallyNameless" to get started. +source-repository head + type: svn + location: https://replib.googlecode.com/svn/trunk/ + Library build-depends: base >= 4.3 && < 5, RepLib >= 0.4.0, @@ -37,8 +41,5 @@ Unbound.LocallyNameless.Alpha, Unbound.LocallyNameless.Subst, Unbound.LocallyNameless.Ops, - Unbound.Nominal, - Unbound.Nominal.Name, - Unbound.Nominal.Internal, Unbound.PermM, Unbound.Util