diff --git a/Changelog.md b/Changelog.md --- a/Changelog.md +++ b/Changelog.md @@ -1,2 +1,11 @@ -* 0.0.0.90 - Initial (re-)implementation effort. +# 0.0.1 + +* Add 'lunbind2' function. + +* Doc updates. + +* Switch from 'HUnit' to 'Tasty' for testing. + +# 0.0.0.90 + +* Initial (re-)implementation effort. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -16,5 +16,5 @@ 2. `isPat :: Alpha t => t -> DisjointSet AnyName` - You should olnly notice this if you're implementing an instance of `Alpha` by hand (rather than by using the default + You should only notice this if you're implementing an instance of `Alpha` by hand (rather than by using the default generic instance). The original `unbound` returned a `Maybe [AnyName]` here with the same interpretation as `DisjointSet`: `Nothing` means an inconsistency was encountered, or `Just` the free variables of the pattern. diff --git a/examples/LC.hs b/examples/LC.hs new file mode 100644 --- /dev/null +++ b/examples/LC.hs @@ -0,0 +1,107 @@ +{-# LANGUAGE DeriveGeneric, + DeriveDataTypeable, + FlexibleInstances, + FlexibleContexts, + MultiParamTypeClasses, + ScopedTypeVariables + #-} + +module LC where + +import Unbound.Generics.LocallyNameless +import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf) + +import GHC.Generics +import Data.Typeable (Typeable) + +import Control.Monad.Reader (Reader, runReader) +import Data.Set as S + +data Exp = Var (Name Exp) + | Lam (Bind (Name Exp) Exp) + | App Exp Exp + deriving (Show, Generic, Typeable) + +instance Alpha Exp + +instance Subst Exp Exp where + isvar (Var x) = Just (SubstName x) + isvar _ = Nothing + +fvSet :: (Alpha a, Typeable b) => a -> S.Set (Name b) +fvSet = S.fromList . toListOf fv + +type M a = FreshM a + +(=~) :: Exp -> Exp -> M Bool +e1 =~ e2 | e1 `aeq` e2 = return True +e1 =~ e2 = do + e1' <- red e1 + e2' <- red e2 + if e1' `aeq` e1 && e2' `aeq` e2 + then return False + else e1' =~ e2' + +red :: Exp -> M Exp +red (App e1 e2) = do + e1' <- red e1 + e2' <- red e2 + case e1' of + Lam bnd -> do + (x, e1'') <- unbind bnd + return $ subst x e2' e1'' + otherwise -> return $ App e1' e2' +red (Lam bnd) = do + (x, e) <- unbind bnd + e' <- red e + case e of + App e1 (Var y) | y == x && x `S.notMember` fvSet e1 -> return e1 + otherwise -> return (Lam (bind x e')) +red (Var x) = return $ (Var x) + + +x :: Name Exp +x = string2Name "x" + +y :: Name Exp +y = string2Name "y" + +z :: Name Exp +z = string2Name "z" + +s :: Name Exp +s = string2Name "s" + +lam :: Name Exp -> Exp -> Exp +lam x y = Lam (bind x y) + +zero = lam s (lam z (Var z)) +one = lam s (lam z (App (Var s) (Var z))) +two = lam s (lam z (App (Var s) (App (Var s) (Var z)))) +three = lam s (lam z (App (Var s) (App (Var s) (App (Var s) (Var z))))) + +plus = lam x (lam y (lam s (lam z (App (App (Var x) (Var s)) (App (App (Var y) (Var s)) (Var z)))))) + +true = lam x (lam y (Var x)) +false = lam x (lam y (Var y)) +if_ x y z = (App (App x y) z) + + +assert :: String -> Bool -> IO () +assert s True = return () +assert s False = print ("Assertion " ++ s ++ " failed") + +assertM :: String -> M Bool -> IO () +assertM s c = + if (runFreshM c) then return () + else print ("Assertion " ++ s ++ " failed") + +main :: IO () +main = do + assert "a1" $ lam x (Var x) `aeq` lam y (Var y) + assert "a2" $ not (lam x (Var y) `aeq` lam x (Var x)) + assertM "be1" $ lam x (App (lam y (Var x)) (lam y (Var y))) =~ (lam y (Var y)) + assertM "be2" $ lam x (App (Var y) (Var x)) =~ Var y + assertM "be3" $ if_ true (Var x) (Var y) =~ Var x + assertM "be4" $ if_ false (Var x) (Var y) =~ Var y + assertM "be5" $ App (App plus one) two =~ three diff --git a/src/Unbound/Generics/LocallyNameless/Operations.hs b/src/Unbound/Generics/LocallyNameless/Operations.hs --- a/src/Unbound/Generics/LocallyNameless/Operations.hs +++ b/src/Unbound/Generics/LocallyNameless/Operations.hs @@ -21,6 +21,7 @@ , unbind , lunbind , unbind2 + , lunbind2 , unbind2Plus -- * Rebinding, embedding , Rebind @@ -129,6 +130,22 @@ swaps (pm' <> pm) p2, open initialCtx p1' t2) Nothing -> return Nothing +-- | Simultaneously 'lunbind' two patterns in two terms in the 'LFresh' monad, +-- passing @Just (p1, t1, p2, t2)@ to the continuation such that the patterns +-- are permuted such that they introduce the same free names, or 'Nothing' if +-- the number of variables differs. +lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) + => Bind p1 t1 + -> Bind p2 t2 + -> (Maybe (p1, t1, p2, t2) -> m c) + -> m c +lunbind2 (B p1 t1) (B p2 t2) cont = + case mkPerm (toListOf fvAny p2) (toListOf fvAny p1) of + Just pm -> + lfreshen p1 $ \p1' pm' -> + cont $ Just (p1', open initialCtx p1' t1, + swaps (pm' <> pm) p2, open initialCtx p1' t2) + Nothing -> cont Nothing -- | Simultaneously unbind two patterns in two terms, returning 'mzero' if -- the patterns don't bind the same number of variables. diff --git a/test/TestCalc.hs b/test/TestCalc.hs new file mode 100644 --- /dev/null +++ b/test/TestCalc.hs @@ -0,0 +1,58 @@ +-- | +-- Module : test-stlc +-- Copyright : (c) 2014, Aleksey Kliger +-- License : BSD3 (See LICENSE) +-- Maintainer : Aleksey Kliger +-- Stability : experimental +-- +{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-} +module TestCalc (test_calc) where + +import Unbound.Generics.LocallyNameless + +import Calc + +import Test.Tasty +import Test.Tasty.HUnit + +assertAeq :: (Alpha t, Show t) => t -> t -> Assertion +assertAeq x y = assertBool (show x ++ " not alpha equivalent to " ++ show y) (x `aeq` y) + +test_ex1 :: TestTree +test_ex1 = testCase "example 1" $ assertAeq (runWhnf emptyEnv ex1) (Just $ C 3) + +test_ex2_open :: TestTree +test_ex2_open = testCase "example 2 (open)" $ assertBool "alpha equivalent" (not $ aeq ex2x ex2y) + +test_ex2_closed :: TestTree +test_ex2_closed = testCase "example 2 (closed)" $ assertAeq ex2xc ex2yc + +test_ex3 :: TestTree +test_ex3 = testCase "example 3" $ assertAeq ex3x ex3y + +test_ex4 :: TestTree +test_ex4 = testCase "example 4 (let scoping)" $ assertAeq (runWhnf emptyEnv ex4) (Just ex4_ans) + +test_ex5 :: TestTree +test_ex5 = testCase "example 5 (let* scoping)" $ assertAeq (runWhnf emptyEnv ex5) (Just ex5_ans) + +test_ex6 :: TestTree +test_ex6 = testCase "example 6 (free variables)" $ assertAeq (anyFreeVarList ex6) ex6_ans + +test_ex7 :: TestTree +test_ex7 = testCase "example 7 (sorted free variables)" $ assertAeq (freeVarList ex7) ex7_ans + + +test_calc :: TestTree +test_calc = + testGroup "calc" + [test_ex1 + , test_ex2_open + , test_ex2_closed + , test_ex3 + , test_ex4 + , test_ex5 + , test_ex6 + , test_ex7 + ] + diff --git a/test/TestParallelReduction.hs b/test/TestParallelReduction.hs new file mode 100644 --- /dev/null +++ b/test/TestParallelReduction.hs @@ -0,0 +1,26 @@ +module TestParallelReduction (test_parallelReduction) where + +import Test.Tasty +import Test.Tasty.HUnit + +import Unbound.Generics.LocallyNameless (Alpha, subst, aeq) + +import ParallelReduction + + +assertAeq :: (Alpha t, Show t) => t -> t -> Assertion +assertAeq x y = assertBool (show x ++ " not alpha equivalent to " ++ show y) (x `aeq` y) + +test_ex1 :: TestTree +test_ex1 = testCase "simple substitution" $ assertAeq (subst (fst ex1') (Lam ex1) (snd ex1')) (Lam ex1) + +test_ex2 :: TestTree +test_ex2 = testCase "parallel reduction" $ assertAeq (run (parSteps ex2)) (run (parSteps ex2_alt)) + +test_parallelReduction :: TestTree +test_parallelReduction = + testGroup "parallel reduction" + [test_ex1 + , test_ex2 + ] + diff --git a/test/test-calc.hs b/test/test-calc.hs deleted file mode 100644 --- a/test/test-calc.hs +++ /dev/null @@ -1,55 +0,0 @@ --- | --- Module : test-stlc --- Copyright : (c) 2014, Aleksey Kliger --- License : BSD3 (See LICENSE) --- Maintainer : Aleksey Kliger --- Stability : experimental --- -{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-} -module Main where - -import Unbound.Generics.LocallyNameless - -import Calc - -import Test.HUnit - -test_ex1 :: Test -test_ex1 = TestCase $ assertBool "example 1" (runWhnf emptyEnv ex1 `aeq` (Just $ C 3)) - -test_ex2_open :: Test -test_ex2_open = TestCase $ assertBool "example 2 (open)" (not $ aeq ex2x ex2y) - -test_ex2_closed :: Test -test_ex2_closed = TestCase $ assertBool "example 2 (closed)" (aeq ex2xc ex2yc) - -test_ex3 :: Test -test_ex3 = TestCase $ assertBool "example 3" (aeq ex3x ex3y) - -test_ex4 :: Test -test_ex4 = TestCase $ assertBool "example 4 (let scoping)" (runWhnf emptyEnv ex4 `aeq` Just ex4_ans) - -test_ex5 :: Test -test_ex5 = TestCase $ assertBool "example 5 (let* scoping)" (runWhnf emptyEnv ex5 `aeq` Just ex5_ans) - -test_ex6 :: Test -test_ex6 = TestCase $ assertBool "example 6 (free variables)" (anyFreeVarList ex6 `aeq` ex6_ans) - -test_ex7 :: Test -test_ex7 = TestCase $ assertBool "example 7 (sorted free variables)" (freeVarList ex7 `aeq` ex7_ans) - - -main :: IO () -main = do - result <- runTestTT $ TestList [test_ex1 - , test_ex2_open - , test_ex2_closed - , test_ex3 - , test_ex4 - , test_ex5 - , test_ex6 - , test_ex7 - ] - if failures result > 0 - then fail "Some tests failed!" - else return () diff --git a/test/test-main.hs b/test/test-main.hs new file mode 100644 --- /dev/null +++ b/test/test-main.hs @@ -0,0 +1,12 @@ +module Main where + +import Test.Tasty + +import TestCalc +import TestParallelReduction + +main = defaultMain $ testGroup "unboundGenerics" + [ + test_calc + , test_parallelReduction + ] diff --git a/test/test-parallelreduction.hs b/test/test-parallelreduction.hs deleted file mode 100644 --- a/test/test-parallelreduction.hs +++ /dev/null @@ -1,25 +0,0 @@ -module Main where - -import Test.HUnit - -import Unbound.Generics.LocallyNameless (subst, aeq) - -import ParallelReduction - - - - -test_ex1 :: Test -test_ex1 = TestCase $ assertBool "simple substitution" (subst (fst ex1') (Lam ex1) (snd ex1') `aeq` (Lam ex1)) - -test_ex2 :: Test -test_ex2 = TestCase $ assertBool "parallel reduction" (run (parSteps ex2) `aeq` run (parSteps ex2_alt)) - -main :: IO () -main = do - result <- runTestTT $ TestList [test_ex1 - , test_ex2 - ] - if failures result > 0 - then fail "Some tests failed!" - else return () diff --git a/unbound-generics.cabal b/unbound-generics.cabal --- a/unbound-generics.cabal +++ b/unbound-generics.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: unbound-generics -version: 0.0.0.90 +version: 0.0.1 synopsis: Reimplementation of Unbound using GHC Generics description: Specify the binding structure of your data type with an expressive set of type combinators, and unbound-generics @@ -13,7 +13,7 @@ . This is an independent re-implementation of but using - instead of . + instead of . See the accompanying README for some porting notes. homepage: http://github.com/lambdageek/unbound-generics @@ -55,24 +55,17 @@ default-language: Haskell2010 ghc-options: -Wall -Test-Suite test-calc +Test-Suite test-unbound-generics type: exitcode-stdio-1.0 - main-is: test-calc.hs + main-is: test-main.hs other-modules: Calc - build-depends: base, - HUnit == 1.2.*, - unbound-generics - hs-source-dirs: test - default-language: Haskell2010 - ghc-options: -Wall - -Test-Suite test-parallelreduction - type: exitcode-stdio-1.0 - main-is: test-parallelreduction.hs - other-modules: ParallelReduction + TestCalc + ParallelReduction + TestParallelReduction build-depends: base, - HUnit == 1.2.*, - mtl >= 2.1, + mtl, + tasty, + tasty-hunit, unbound-generics hs-source-dirs: test default-language: Haskell2010