unbound-generics 0.0.1 → 0.0.2

raw patch · 13 files changed

+399/−14 lines, 13 filesdep +QuickCheckdep +tasty-quickcheckPVP ok

version bump matches the API change (PVP)

Dependencies added: QuickCheck, tasty-quickcheck

API changes (from Hackage documentation)

Files

• Changelog.md +6/−0
• README.md +1/−1
• src/Unbound/Generics/LocallyNameless.hs +2/−0
• src/Unbound/Generics/LocallyNameless/Alpha.hs +5/−1
• src/Unbound/Generics/LocallyNameless/Internal/Fold.hs +4/−2
• src/Unbound/Generics/LocallyNameless/Operations.hs +30/−4
• src/Unbound/Generics/LocallyNameless/Rebind.hs +3/−5
• src/Unbound/Generics/LocallyNameless/Rec.hs +67/−0
• src/Unbound/Generics/LocallyNameless/Subst.hs +5/−0
• test/PropOpenClose.hs +114/−0
• test/TinyLam.hs +151/−0
• test/test-main.hs +5/−0
• unbound-generics.cabal +6/−1

@@ -1,3 +1,9 @@+# 0.0.2++* Add 'Rec' pattern and 'TRec' term combinators.++* Alpha instance for '()'+ # 0.0.1  * Add 'lunbind2' function.

@@ -9,7 +9,7 @@  For the most part, I tried to keep the same methods with the same signatures.  However there are a few differences. -1. `fv :: Alpha t => t -> Fold t (Name n)`+1. `fv :: Alpha t => Fold t (Name n)`     The `fv` method returns a `Fold` (in the sense of the [lens](http://hackage.haskell.org/package/lens) library),    rather than an `Unbound.Util.Collection` instance.  That means you will generally have to write `toListOf fv t` or some    other summary operation.

@@ -14,6 +14,7 @@   module Unbound.Generics.LocallyNameless.Bind,   module Unbound.Generics.LocallyNameless.Embed,   module Unbound.Generics.LocallyNameless.Rebind,+  module Unbound.Generics.LocallyNameless.Rec,   module Unbound.Generics.LocallyNameless.Fresh,   module Unbound.Generics.LocallyNameless.LFresh,   module Unbound.Generics.LocallyNameless.Subst@@ -24,6 +25,7 @@ import Unbound.Generics.LocallyNameless.Bind hiding (B) import Unbound.Generics.LocallyNameless.Embed import Unbound.Generics.LocallyNameless.Rebind hiding (Rebnd)+import Unbound.Generics.LocallyNameless.Rec import Unbound.Generics.LocallyNameless.Fresh import Unbound.Generics.LocallyNameless.LFresh import Unbound.Generics.LocallyNameless.Operations

@@ -124,7 +124,10 @@   aeq' c = (gaeq c) `on` from    -- | See 'Unbound.Generics.LocallyNameless.Operations.fvAny'.-  -- @@@ fvAny' :: AlphaCtx -> Fold a AnyName @@@+  --+  -- @+  --  fvAny' :: Fold a AnyName+  -- @   fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a   default fvAny' :: (Generic a, GAlpha (Rep a), Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a   fvAny' c nfn = fmap to . gfvAny c nfn . from@@ -481,6 +484,7 @@  instance Alpha a => Alpha (Maybe a) instance Alpha a => Alpha [a]+instance Alpha () instance (Alpha a,Alpha b) => Alpha (Either a b) instance (Alpha a,Alpha b) => Alpha (a,b) instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c)

@@ -5,9 +5,11 @@ -- Maintainer : Aleksey Kliger -- Stability  : experimental ----- | Some utilities for working with Folds.+-- Some utilities for working with Folds.+--+-- If you are using <http://hackage.haskell.org/package/lens lens>, you don't need this module. {-# LANGUAGE RankNTypes #-}-module Unbound.Generics.LocallyNameless.Internal.Fold (Fold, Traversal', toListOf, filtered, justFiltered) where+module Unbound.Generics.LocallyNameless.Internal.Fold (Fold, Traversal', toListOf, filtered, justFiltered, foldMapOf) where  import Control.Applicative import Data.Maybe (fromJust)

@@ -30,6 +30,14 @@        , Embed(..)        , embed        , unembed+         -- * Recursive bindings+       , Rec+       , Unbound.Generics.LocallyNameless.Rec.rec+       , Unbound.Generics.LocallyNameless.Rec.unrec+       , TRec(..)+       , trec+       , untrec+       , luntrec        ) where  import Control.Applicative (Applicative)@@ -44,6 +52,7 @@ import Unbound.Generics.LocallyNameless.Bind import Unbound.Generics.LocallyNameless.Embed (Embed(..)) import Unbound.Generics.LocallyNameless.Rebind+import Unbound.Generics.LocallyNameless.Rec import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf, justFiltered) import Unbound.Generics.PermM @@ -51,18 +60,18 @@ aeq :: Alpha a => a -> a -> Bool aeq = aeq' initialCtx --- | @'fvAny' t@ returns the free variables of the term @t@.+-- | @'fvAny'@ returns a fold over any names in a term @a@. -- -- @---   fvAny :: Alpha a => a -> Fold a AnyName+--   fvAny :: Alpha a => Fold a AnyName -- @ fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a fvAny = fvAny' initialCtx --- | @'fv' t@ returns the free @b@ variables of term @t@.+-- | @'fv'@ returns the free @b@ variables of term @a@. -- -- @---  fv :: (Alpha a, Typeable b) => a -> Fold a (Name b)+--  fv :: (Alpha a, Typeable b) => Fold a (Name b) -- @ fv :: forall a f b . (Alpha a, Typeable b, Contravariant f, Applicative f)       => (Name b -> f (Name b)) -> a -> f a@@ -177,3 +186,20 @@ -- | @'unembed' p@ extracts the term embedded in the pattern @p@. unembed :: Embed t -> t unembed (Embed t) = t++-- | Constructor for recursive abstractions.+trec :: Alpha p => p -> TRec p+trec p = TRec (bind (rec p) ())++-- | Destructor for recursive abstractions which picks globally fresh+--   names for the binders.+untrec :: (Alpha p, Fresh m) => TRec p -> m p+untrec (TRec b) = do+  (p, ()) <- unbind b+  return (unrec p)++-- | Destructor for recursive abstractions which picks /locally/ fresh+--   names for binders (see 'LFresh').+luntrec :: (Alpha p, LFresh m) => TRec p -> m p+luntrec (TRec b) =+  lunbind b $ \(p, ()) -> return (unrec p)

@@ -31,12 +31,10 @@ -- -- @ -- type Var = Name Expr--- data Lets = EmptyLets---           | Bind (Rebind (Var, Embed Expr) Lets)+-- data Lets = EmptyLs+--           | ConsLs (Rebind (Var, Embed Expr) Lets) -- data Expr = ...---           | LetStar { letStarBindings :: Lets---                     , letStarBody :: Expr---                     }+--           | LetStar (Bind Lets Expr) --           | ... -- @ data Rebind p1 p2 = Rebnd p1 p2

@@ -0,0 +1,67 @@+{-# OPTIONS_HADDOCK show-extensions #-}+-- |+-- Module     : Unbound.Generics.LocallyNameless.Rec+-- Copyright  : (c) 2014, Aleksey Kliger+-- License    : BSD3 (See LICENSE)+-- Maintainer : Aleksey Kliger+-- Stability  : experimental+--+-- The pattern @'Rec' p@ binds the names in @p@ like @p@ itself would,+-- but additinoally, the names in @p@ are scope over @p@.+--+-- The term @'TRec' p@ is shorthand for @'Bind' (Rec p) ()@+{-# LANGUAGE DeriveGeneric #-}+module Unbound.Generics.LocallyNameless.Rec+       (+         Rec+       , rec+       , unrec+       , TRec (..)+       ) where++import GHC.Generics (Generic)++import Unbound.Generics.LocallyNameless.Alpha+import Unbound.Generics.LocallyNameless.Bind++-- | If @p@ is a pattern type, then @Rec p@ is also a pattern type,+-- which is /recursive/ in the sense that @p@ may bind names in terms+-- embedded within itself.  Useful for encoding e.g. lectrec and+-- Agda's dot notation.+newtype Rec p = Rec p+              deriving (Generic, Eq)++instance Show a => Show (Rec a) where+  showsPrec _ (Rec a) = showString "[" . showsPrec 0 a . showString "]"++-- | @TRec@ is a standalone variant of 'Rec': the only difference is+--   that whereas @'Rec' p@ is a pattern type, @TRec p@+--   is a /term type/.  It is isomorphic to @'Bind' ('Rec' p) ()@.+--+--   Note that @TRec@ corresponds to Pottier's /abstraction/ construct+--   from alpha-Caml.  In this context, @'Embed' t@ corresponds to+--   alpha-Caml's @inner t@, and @'Shift' ('Embed' t)@ corresponds to+--   alpha-Caml's @outer t@.+newtype TRec p = TRec (Bind (Rec p) ())+                 deriving (Generic)++instance Show a => Show (TRec a) where+  showsPrec _ (TRec (B (Rec p) ())) = showString "[" . showsPrec 0 p . showString "]"+++instance Alpha p => Alpha (Rec p) where+  isTerm _ = False+  isPat (Rec p) = isPat p++  open ctx b (Rec p) = Rec (open (incrLevelCtx ctx) b p)+  close ctx b (Rec p) = Rec (close (incrLevelCtx ctx) b p)++instance Alpha p => Alpha (TRec p)++-- | Constructor for recursive patterns.+rec :: Alpha p => p -> Rec p+rec p = Rec (close (patternCtx initialCtx) p p)++-- | Destructor for recursive patterns.+unrec :: Alpha p => Rec p -> p+unrec (Rec p) = open (patternCtx initialCtx) p p

@@ -57,6 +57,7 @@ import Unbound.Generics.LocallyNameless.Embed import Unbound.Generics.LocallyNameless.Bind import Unbound.Generics.LocallyNameless.Rebind+import Unbound.Generics.LocallyNameless.Rec  -- | See 'isVar' data SubstName a b where@@ -175,3 +176,7 @@ instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)  instance (Subst c p1, Subst c p2) => Subst c (Rebind p1 p2)++instance (Subst c p) => Subst c (Rec p)++instance (Alpha p, Subst c p) => Subst c (TRec p)

@@ -0,0 +1,114 @@+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}+module PropOpenClose (test_openClose) where++import Control.Applicative (Applicative(..), (<$>))+import Data.Monoid (Any(..))+import Data.Typeable (Typeable)+import GHC.Generics (Generic)++import Test.QuickCheck+import Test.Tasty (testGroup, TestTree)+import Test.Tasty.QuickCheck (testProperty)++import Unbound.Generics.LocallyNameless+import Unbound.Generics.LocallyNameless.Internal.Fold (foldMapOf, toListOf)++----------------------------------------+-- Property testing utilities++isFreeIn :: (Typeable a, Alpha b) => Name a -> b -> Bool+isFreeIn = elementOf fv+  where+    elementOf l = anyOf l . (==)+    anyOf l f = getAny . foldMapOf l (Any . f)++notFreeIn :: (Typeable a, Alpha b) => Name a -> b -> Bool+notFreeIn v = not . isFreeIn v++(=~=) :: (Alpha a, Show a) => a -> a -> Property+x =~= y = counterexample (show x ++ " not alpha equivalent to " ++ show y) (x `aeq` y)++(/~@) :: (Typeable a, Alpha b, Show b) => Name a -> b -> Property+v /~@ t = counterexample (show v ++ " is free in " ++ show t) (v `notFreeIn` t)++-- Wrapper around 'Name a' that has an Arbitrary instance that generates free names.+-- Note that this doesn't guarantee /freshness/.  The name may clash with some other one.+-- But it will never be a bound name.+newtype FreeName a = FreeName {getFreeName :: Name a}+                     deriving (Show)++instance Arbitrary (FreeName a) where+  arbitrary = do+    s <- listOf1 (elements ['a'..'z'])+    n <- arbitrary+    return $ FreeName $ makeName s n+  shrink = const []++----------------------------------------+-- example data structure, with no bound names.++data T a = Leaf !a+         | V !(Name (T a))+         | B !(T a) !(T a)+         deriving (Show, Typeable, Generic)++instance (Typeable a, Alpha a) => Alpha (T a)++instance Arbitrary a => Arbitrary (T a) where+  arbitrary =+    oneof+    [+      Leaf <$> arbitrary+    ,(V . getFreeName) <$> arbitrary+    , B <$> arbitrary <*> arbitrary+    ]++-- generator that picks out one of the free variables of a tree+arbVarsOf :: (Alpha a, Typeable a) => T a -> Gen (Name (T a))+arbVarsOf t =+  let vs = toListOf fv t+  in  elements vs++-- spec for free variables of a tree.+-- fvSpec :: Traversal' (T a) (Name (T a))+fvSpec :: Applicative f => (Name (T a) -> f (Name (T a))) -> T a -> f (T a)+fvSpec f t =+  case t of+   Leaf {} -> pure t+   V v -> V <$> f v+   B t1 t2 -> B <$> fvSpec f t1 <*> fvSpec f t2++----------------------------------------+-- Properties++-- every tree is alpha-equivalent to itself+prop_refl :: T Int -> Property+prop_refl x = x =~= x++-- generic fv gives the same answer as fvSpec+prop_fv_spec :: T Int -> Property+prop_fv_spec t = toListOf fv t === toListOf fvSpec t+  +-- if a name is already free opening it has no effect+prop_open_idempotent :: T Int -> Property+prop_open_idempotent t =+  forAll (arbVarsOf t) $ \v -> open initialCtx v t =~= t++-- if you close over a variable, then it is no longer free.+prop_close_binds :: T Int -> Property+prop_close_binds t =+  (not $ null $ toListOf fvAny t) ==>+  forAll (arbVarsOf t) $ \v -> v /~@ close initialCtx v t++----------------------------------------+-- Test group++test_openClose :: TestTree+test_openClose =+  testGroup "QuickCheck properties"+  [+    testProperty "reflexivity" prop_refl+  , testProperty "fv specification" prop_fv_spec+  , testProperty "open idempotency" prop_open_idempotent+  , testProperty "closing binds variables" prop_close_binds+  ]

@@ -0,0 +1,151 @@+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric, FlexibleContexts #-}+module TinyLam where++import GHC.Generics (Generic)+import Data.Typeable (Typeable)++import Control.Applicative (Applicative(..))+import Control.Monad.Reader+import Data.Monoid (Monoid(..))+import qualified Data.List ++import Test.Tasty+import Test.Tasty.HUnit++import Unbound.Generics.LocallyNameless+++type Var = Name Expr++data ArithOp = ArithOp String (Int -> Int -> Int)+             deriving (Typeable, Generic)++instance Show ArithOp where+  show (ArithOp f _) = f++data Expr = V Var+          | I Int+          | Arith ArithOp Expr Expr+          | Lam Fun+          | App Expr Expr+          | If0 Expr Expr Expr+          | Letrec (Bind (Rec (Var, Embed Fun)) Expr)+          deriving (Typeable, Generic, Show)++newtype Fun = Fun (Bind Var Expr)+            deriving (Typeable, Generic, Show)++instance Eq Expr where+  (==) = aeq++instance Eq Fun where+  (==) = aeq++-- leaf instance for ArithOp+instance Alpha ArithOp where+  aeq' _ctx (ArithOp s1 _) (ArithOp s2 _) = s1 == s2+  fvAny' _ctx _nfn x = pure x+  close _ctx _b x = x+  open _ctx _b x = x+  isPat _ = mempty+  isTerm _ = True+  nthPatFind _ = Left+  namePatFind _ _ = Left 0++  swaps' _ctx _p x = x+  freshen' _ctx x = return (x, mempty)+  lfreshen' _ctx x cont = cont x mempty++instance Alpha Expr+instance Alpha Fun++type Env = [(Var, Value)]++data Value = VI !Int+           | VClo !Env !Fun+           deriving (Eq, Show) +++emptyEnv :: Env+emptyEnv = []++extendEnv :: Var -> Value -> Env -> Env+extendEnv x v rho = (x,v) : rho++env :: MonadReader Env m => m Env+env = ask++lookupV :: MonadReader Env m => Var -> m Value+lookupV x = env >>= \rho ->+  case Data.List.lookup x rho of+   Just v -> return v+   Nothing -> error $ "unbound variable " ++ show x++eval :: (Fresh m, MonadReader Env m) => Expr -> m Value+eval (V x) = lookupV x+eval (I i) = return $ VI i+eval (Lam f) = env >>= \rho -> return (VClo rho f)+eval (App e1 e2) = do+  v1 <- eval e1+  case v1 of+   (VClo rho (Fun bnd)) -> do+     v2 <- eval e2+     (x, e3) <- unbind bnd+     local (const $ extendEnv x v2 rho) $ eval e3+   _ -> error ("expected a function, but got " ++ show v1)+eval (Arith (ArithOp _ op) e1 e2) = do+  v1 <- eval e1+  v2 <- eval e2+  case (v1, v2) of+   (VI n1, VI n2) -> return $ VI (op n1 n2)+   _ -> error ("expected pair of ints, but got " ++ show v1+               ++ " and " ++ show v2)+eval (If0 e1 e2 e3) = do+  v1 <- eval e1+  case v1 of+   VI 0 -> eval e2+   VI _ -> eval e3+   _ -> error ("expected int, but got " ++ show v1)+eval (Letrec bnd) = do+  (r, ebody) <- unbind bnd+  rho0 <- ask+  let (f, Embed fun) = unrec r+      -- N.B. knot tying+      rho = extendEnv f vclo rho0+      vclo = VClo rho fun+  local (extendEnv f vclo) $ eval ebody++runEval :: Expr -> Value+runEval e = runReader (runFreshMT (eval e)) emptyEnv++ex_f :: Int -> Expr+ex_f n = let+  (/*/) = Arith (ArithOp "*" (*))+  (/-/) = Arith (ArithOp "-" (-))+  fact = s2n "fact"+  x = s2n "x"+  body = If0 (V x)+         {-then-} (I 1)+         {-else-} (V x+                   /*/ +                   App (V fact) (V x /-/ I 1))+  factfun = Fun (bind x body)+  in Letrec $ bind (rec (fact, Embed factfun))+     (App (V fact) (I n))++test_ex_f0 :: TestTree+test_ex_f0 =+  testCase "eval (fact 0) = 1"+  $ assertEqual "" (runEval (ex_f 0)) (VI 1)++test_ex_f5 :: TestTree+test_ex_f5 =+  testCase "eval (fact 5) = 120"+  $ assertEqual "" (runEval (ex_f 5)) (VI 120)++test_tinyLam :: TestTree+test_tinyLam =+  testGroup "tinyLam"+  [ test_ex_f0+  , test_ex_f5+  ]

@@ -4,9 +4,14 @@  import TestCalc import TestParallelReduction+import PropOpenClose+import TinyLam +main :: IO () main = defaultMain $ testGroup "unboundGenerics"        [          test_calc        , test_parallelReduction+       , test_openClose+       , test_tinyLam        ]

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                unbound-generics-version:             0.0.1+version:             0.0.2 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@@ -42,6 +42,7 @@                        Unbound.Generics.LocallyNameless.Operations                        Unbound.Generics.LocallyNameless.Unsafe                        Unbound.Generics.LocallyNameless.Internal.Fold+                       Unbound.Generics.LocallyNameless.Rec                        Unbound.Generics.PermM                        Unbound.Generics.LocallyNameless.Subst   -- other-modules:       @@ -62,10 +63,14 @@                        TestCalc                        ParallelReduction                        TestParallelReduction+                       PropOpenClose+                       TinyLam   build-depends:       base,                        mtl,                        tasty,                        tasty-hunit,+                       tasty-quickcheck,+                       QuickCheck >= 2.7 && < 3,                        unbound-generics   hs-source-dirs:      test   default-language:    Haskell2010