unbound-generics 0.0.0.90 → 0.0.1

raw patch · 10 files changed

+242/−100 lines, 10 filesdep +tastydep +tasty-hunitdep −HUnitdep ~basedep ~mtlPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: tasty, tasty-hunit

Dependencies removed: HUnit

Dependency ranges changed: base, mtl

API changes (from Hackage documentation)

Files

• Changelog.md +11/−2
• README.md +1/−1
• examples/LC.hs +107/−0
• src/Unbound/Generics/LocallyNameless/Operations.hs +17/−0
• test/TestCalc.hs +58/−0
• test/TestParallelReduction.hs +26/−0
• test/test-calc.hs +0/−55
• test/test-main.hs +12/−0
• test/test-parallelreduction.hs +0/−25
• unbound-generics.cabal +10/−17

@@ -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.

@@ -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.

@@ -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

@@ -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.

@@ -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+  ]+

@@ -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+  ]+

@@ -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 ()

@@ -0,0 +1,12 @@+module Main where++import Test.Tasty++import TestCalc+import TestParallelReduction++main = defaultMain $ testGroup "unboundGenerics"+       [+         test_calc+       , test_parallelReduction+       ]

@@ -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 ()

@@ -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 <http://hackage.haskell.org/package/unbound Unbound>                      but using <http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.7.0.1/GHC-Generics.html GHC.Generics>-                     instead of <http://http://hackage.haskell.org/package/RepLib RepLib>.+                     instead of <http://hackage.haskell.org/package/RepLib RepLib>.                      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