unbound-generics 0.0.3 → 0.1
raw patch · 10 files changed
+183/−5 lines, 10 files
Files
- Changelog.md +7/−0
- src/Unbound/Generics/LocallyNameless/Alpha.hs +65/−4
- src/Unbound/Generics/LocallyNameless/Bind.hs +3/−0
- src/Unbound/Generics/LocallyNameless/Embed.hs +2/−0
- src/Unbound/Generics/LocallyNameless/Operations.hs +5/−0
- src/Unbound/Generics/LocallyNameless/Rebind.hs +3/−0
- test/TestACompare.hs +93/−0
- test/TinyLam.hs +1/−0
- test/test-main.hs +2/−0
- unbound-generics.cabal +2/−1
Changelog.md view
@@ -1,3 +1,10 @@+# 0.1++* Add `acompare` functiona and `acompare'` method to `Alpha` typeclass. (christiaanb)++ Handwritten `Alpha` instances will need to define this additional+ method now. Major version bump.+ # 0.0.3 * Add 'name2Integer' method (christiaanb)
src/Unbound/Generics/LocallyNameless/Alpha.hs view
@@ -39,6 +39,7 @@ , gswaps , gfreshen , glfreshen+ , gacompare ) where import Control.Applicative (Applicative(..), (<$>))@@ -50,7 +51,7 @@ import Data.List (intersect) import Data.Monoid (Monoid(..), (<>)) import Data.Ratio (Ratio)-import Data.Typeable (Typeable, gcast)+import Data.Typeable (Typeable, gcast, typeOf) import GHC.Generics import Unbound.Generics.LocallyNameless.Name@@ -201,6 +202,11 @@ default freshen' :: (Generic a, GAlpha (Rep a), Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName) freshen' ctx = liftM (first to) . gfreshen ctx . from + -- | See 'Unbound.Generics.LocallyNameless.Operations.acompare'. An alpha-respecting total order on terms involving binders.+ acompare' :: AlphaCtx -> a -> a -> Ordering+ default acompare' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Ordering+ acompare' c = (gacompare c) `on` from+ -- | The result of @'nthPatFind' a i@ is @Left k@ where @k@ is the -- number of names in pattern @a@ with @k < i@ or @Right x@ where @x@ -- is the @i@th name in @a@@@ -231,7 +237,9 @@ gfreshen :: Fresh m => AlphaCtx -> f a -> m (f a, Perm AnyName) glfreshen :: LFresh m => AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b- ++ gacompare :: AlphaCtx -> f a -> f a -> Ordering+ instance (Alpha c) => GAlpha (K1 i c) where gaeq ctx (K1 c1) (K1 c2) = aeq' ctx c1 c2 @@ -251,6 +259,8 @@ glfreshen ctx (K1 c) cont = lfreshen' ctx c (cont . K1) + gacompare ctx (K1 c1) (K1 c2) = acompare' ctx c1 c2+ instance GAlpha f => GAlpha (M1 i c f) where gaeq ctx (M1 f1) (M1 f2) = gaeq ctx f1 f2 @@ -264,13 +274,15 @@ gnthPatFind = gnthPatFind . unM1 gnamePatFind = gnamePatFind . unM1- + gswaps ctx perm = M1 . gswaps ctx perm . unM1 gfreshen ctx = liftM (first M1) . gfreshen ctx . unM1 glfreshen ctx (M1 f) cont = glfreshen ctx f (cont . M1) + gacompare ctx (M1 f1) (M1 f2) = gacompare ctx f1 f2+ instance GAlpha U1 where gaeq _ctx _ _ = True @@ -290,6 +302,8 @@ glfreshen _ctx _ cont = cont U1 mempty + gacompare _ctx _ _ = EQ+ instance GAlpha V1 where gaeq _ctx _ _ = False @@ -309,6 +323,8 @@ glfreshen _ctx _ cont = cont undefined mempty + gacompare _ctx _ _ = error "LocallyNameless.gacompare: undefined for empty data types"+ instance (GAlpha f, GAlpha g) => GAlpha (f :*: g) where gaeq ctx (f1 :*: g1) (f2 :*: g2) = gaeq ctx f1 f2 && gaeq ctx g1 g2@@ -344,6 +360,9 @@ glfreshen ctx (gswaps ctx perm2 f) $ \f' perm1 -> cont (f' :*: g') (perm1 <> perm2) + gacompare ctx (f1 :*: g1) (f2 :*: g2) =+ (gacompare ctx f1 f2) <> (gacompare ctx g1 g2)+ instance (GAlpha f, GAlpha g) => GAlpha (f :+: g) where gaeq ctx (L1 f1) (L1 f2) = gaeq ctx f1 f2 gaeq ctx (R1 g1) (R1 g2) = gaeq ctx g1 g2@@ -379,8 +398,12 @@ glfreshen ctx f (cont . L1) glfreshen ctx (R1 g) cont = glfreshen ctx g (cont . R1)- + gacompare _ctx (L1 _) (R1 _) = LT+ gacompare _ctx (R1 _) (L1 _) = GT+ gacompare ctx (L1 f1) (L1 f2) = gacompare ctx f1 f2+ gacompare ctx (R1 g1) (R1 g2) = gacompare ctx g1 g2+ -- ============================================================ -- Alpha instances for the usual types @@ -402,6 +425,8 @@ freshen' _ctx i = return (i, mempty) lfreshen' _ctx i cont = cont i mempty + acompare' _ctx i j = compare i j+ instance Alpha Char where aeq' _ctx i j = i == j @@ -420,6 +445,8 @@ freshen' _ctx i = return (i, mempty) lfreshen' _ctx i cont = cont i mempty + acompare' _ctx i j = compare i j+ instance Alpha Integer where aeq' _ctx i j = i == j @@ -438,6 +465,8 @@ freshen' _ctx i = return (i, mempty) lfreshen' _ctx i cont = cont i mempty + acompare' _ctx i j = compare i j+ instance Alpha Float where aeq' _ctx i j = i == j @@ -456,6 +485,8 @@ freshen' _ctx i = return (i, mempty) lfreshen' _ctx i cont = cont i mempty + acompare' _ctx i j = compare i j+ instance Alpha Double where aeq' _ctx i j = i == j @@ -474,6 +505,8 @@ freshen' _ctx i = return (i, mempty) lfreshen' _ctx i cont = cont i mempty + acompare' _ctx i j = compare i j+ instance (Integral n, Alpha n) => Alpha (Ratio n) where aeq' _ctx i j = i == j @@ -492,6 +525,8 @@ freshen' _ctx i = return (i, mempty) lfreshen' _ctx i cont = cont i mempty + acompare' _ctx i j = compare i j+ instance Alpha Bool instance Alpha a => Alpha (Maybe a)@@ -575,6 +610,20 @@ avoid [AnyName nm'] $ cont nm' $ single (AnyName nm) (AnyName nm') else error "lfreshen' on a Name in term position" + acompare' ctx (Fn s1 i1) (Fn s2 i2)+ | isTermCtx ctx = (compare s1 s2) <> (compare i1 i2)++ acompare' ctx n1@(Bn i1 j1) n2@(Bn i2 j2)+ | isTermCtx ctx = mconcat [ compare (typeOf n1) (typeOf n2)+ , compare i1 i2+ , compare j1 j2+ ]++ acompare' ctx (Fn _ _) (Bn _ _) | isTermCtx ctx = LT+ acompare' ctx (Bn _ _) (Fn _ _) | isTermCtx ctx = GT++ acompare' _ _ _ = EQ+ instance Alpha AnyName where aeq' ctx x y = if x == y@@ -624,3 +673,15 @@ if nmHave == nmWant then Right 0 else Left 1++ acompare' _ x y | x == y = EQ++ acompare' ctx (AnyName n1) (AnyName n2)+ | isTermCtx ctx =+ case compare (typeOf n1) (typeOf n2) of+ EQ -> case gcast n2 of+ Just n2' -> acompare' ctx n1 n2'+ Nothing -> error "LocallyNameless.acompare': Equal type representations, but gcast failed in comparing two AnyName values"+ ord -> ord++ acompare' _ _ _ = EQ
src/Unbound/Generics/LocallyNameless/Bind.hs view
@@ -75,3 +75,6 @@ lfreshen' (patternCtx ctx) p $ \p' pm1 -> lfreshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) pm1 t) $ \t' pm2 -> cont (B p' t') (pm1 <> pm2)++ acompare' ctx (B p1 t1) (B p2 t2) =+ acompare' (patternCtx ctx) p1 p2 <> acompare' (incrLevelCtx ctx) t1 t2
src/Unbound/Generics/LocallyNameless/Embed.hs view
@@ -75,3 +75,5 @@ nthPatFind _ = Left namePatFind _ _ = Left 0++ acompare' ctx (Embed x) (Embed y) = acompare' (termCtx ctx) x y
src/Unbound/Generics/LocallyNameless/Operations.hs view
@@ -10,6 +10,7 @@ module Unbound.Generics.LocallyNameless.Operations (-- * Equivalence, free variables, freshness aeq+ , acompare , fvAny , fv , freshen@@ -59,6 +60,10 @@ -- | @'aeq' t1 t2@ returns @True@ iff @t1@ and @t2@ are alpha-equivalent terms. aeq :: Alpha a => a -> a -> Bool aeq = aeq' initialCtx++-- | An alpha-respecting total order on terms involving binders.+acompare :: Alpha a => a -> a -> Ordering+acompare = acompare' initialCtx -- | @'fvAny'@ returns a fold over any names in a term @a@. --
src/Unbound/Generics/LocallyNameless/Rebind.hs view
@@ -81,3 +81,6 @@ open ctx b (Rebnd p1 p2) = Rebnd (open ctx b p1) (open (incrLevelCtx ctx) b p2) close ctx b (Rebnd p1 p2) = Rebnd (close ctx b p1) (close (incrLevelCtx ctx) b p2)++ acompare' ctx (Rebnd p1 p2) (Rebnd q1 q2) =+ acompare' ctx p1 q1 <> acompare' (incrLevelCtx ctx) p2 q2
+ test/TestACompare.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}+module TestACompare where++import Data.Typeable+import GHC.Generics+import Unbound.Generics.LocallyNameless++import Test.Tasty+import Test.Tasty.HUnit++data Expr+ = V (Name Expr)+ | Add Expr Expr+ | L (Bind (Name Expr) Expr)+ deriving (Show,Generic,Typeable)++instance Alpha Expr++assertAcompare :: (Alpha t, Show t) => t -> t -> Ordering -> Assertion+assertAcompare x y o =+ let o' = acompare x y+ in assertBool (show x ++ " not alpha-" ++ show o' ++ " to " ++ show y ++ ", but alpha-" ++ show o) (o' == o)++nameA, nameB, nameC :: Name Expr+nameA = s2n "a"+nameB = s2n "b"+nameC = s2n "c"++test_acompare :: TestTree+test_acompare = testGroup "acompare"+ -- Names compare in the obvious way.+ [ testGroup "obvious"+ [testCase "ac1 (a < b)" $ assertAcompare nameA nameB LT+ ,testCase "ac2 (b = b)" $ assertAcompare nameB nameB EQ+ ,testCase "ac3 (b > a)" $ assertAcompare nameB nameA GT+ ]+ -- structured date compares lexicographically+ , testGroup "lexicographically"+ [testCase "ac4 (a + a = a + a)" $+ assertAcompare (Add (V nameA) (V nameA)) (Add (V nameA) (V nameA)) EQ+ ,testCase "ac5 (a + a < a + b)" $+ assertAcompare (Add (V nameA) (V nameA)) (Add (V nameA) (V nameB)) LT+ ,testCase "ac6 (a + b > a + a)" $+ assertAcompare (Add (V nameA) (V nameB)) (Add (V nameA) (V nameA)) GT+ ,testCase "ac7 (a + a < b + a)" $+ assertAcompare (Add (V nameA) (V nameA)) (Add (V nameB) (V nameA)) LT+ ,testCase "ac8 (b + a > a + a)" $+ assertAcompare (Add (V nameB) (V nameA)) (Add (V nameA) (V nameA)) GT+ ,testCase "ac9 (b + a > a + b)" $+ assertAcompare (Add (V nameB) (V nameA)) (Add (V nameA) (V nameB)) GT+ ]+ -- comparison goes under binders, alpha-respectingly.+ , testGroup "binders"+ [testCase "ac10 (\\a.a+a = \\b.b+b)" $+ assertAcompare (bind nameA (Add (V nameA) (V nameA)))+ (bind nameB (Add (V nameB) (V nameB)))+ EQ+ ,testCase "ac11 (\\a.a+a > \\a.a+b)" $+ assertAcompare (bind nameA (Add (V nameA) (V nameA)))+ (bind nameA (Add (V nameA) (V nameB)))+ GT+ ,testCase "ac12 (\\c.c+a < \\a.a+b)" $+ assertAcompare (bind nameC (Add (V nameC) (V nameA)))+ (bind nameA (Add (V nameA) (V nameB)))+ LT+ ]+ -- non-matching binders handled alpha-respectingly.+ , testGroup "non-matching binders"+ [testCase "ac13 ((\\a.a `ac` \\a b.a) = (\\c.c `ac` \\a b.a))" $+ assertAcompare (bind [nameA] nameA)+ (bind [nameA,nameB] nameA)+ (acompare (bind [nameC] nameC) (bind [nameA,nameB] nameA))+ ,testCase "ac14 ((\\a b.a `ac` \\a.a) = (\\c b.c `ac` \\a.a))" $+ assertAcompare (bind [nameA,nameB] nameA)+ (bind [nameA] nameA)+ (acompare (bind [nameC,nameB] nameC) (bind [nameA] nameA))+ ]+ -- non-binding stuff in patterns gets compared+ , testGroup "non-binding stuff"+ [testCase "ac15 (<a> < <b>)" $+ assertAcompare (Embed nameA) (Embed nameB) LT+ ,testCase "ac16 (\\c<a>.c+c < \\c<b>.c+c)" $+ assertAcompare+ (bind (nameC, Embed nameA) (Add (V nameC) (V nameC)))+ (bind (nameC, Embed nameB) (Add (V nameC) (V nameC)))+ LT+ ,testCase "ac17 (\\c<a>.b+b < \\c<b>.a+a)" $+ assertAcompare+ (bind (nameC, Embed nameA) (Add (V nameB) (V nameB)))+ (bind (nameC, Embed nameB) (Add (V nameA) (V nameA)))+ LT+ ]+ ]
test/TinyLam.hs view
@@ -55,6 +55,7 @@ swaps' _ctx _p x = x freshen' _ctx x = return (x, mempty) lfreshen' _ctx x cont = cont x mempty+ acompare' _ctx (ArithOp s1 _) (ArithOp s2 _) = compare s1 s2 instance Alpha Expr instance Alpha Fun
test/test-main.hs view
@@ -6,6 +6,7 @@ import TestParallelReduction import PropOpenClose import TinyLam+import TestACompare main :: IO () main = defaultMain $ testGroup "unboundGenerics"@@ -14,4 +15,5 @@ , test_parallelReduction , test_openClose , test_tinyLam+ , test_acompare ]
unbound-generics.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: unbound-generics-version: 0.0.3+version: 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@@ -66,6 +66,7 @@ TestParallelReduction PropOpenClose TinyLam+ TestACompare build-depends: base, mtl, tasty,