th-alpha 0.1.0.2 → 0.2.0.0
raw patch · 3 files changed
+303/−129 lines, 3 filesdep +containersdep +derivedep +mmorph
Dependencies added: containers, derive, mmorph, mtl, tasty-quickcheck, transformers
Files
- src/Language/Haskell/TH/Alpha.hs +258/−123
- tests/tests.hs +27/−3
- th-alpha.cabal +18/−3
src/Language/Haskell/TH/Alpha.hs view
@@ -1,5 +1,10 @@-{-# LANGUAGE NoMonomorphismRestriction, TypeFamilies, FlexibleInstances- , MultiParamTypeClasses, FunctionalDependencies #-}+{-# LANGUAGE+ FunctionalDependencies+ , GeneralizedNewtypeDeriving+ , RankNTypes+ , FlexibleContexts+ , BangPatterns+ #-} {-| Module : Language.Haskell.TH.Alpha Description : Alpha equivalence in TH@@ -28,42 +33,121 @@ module Language.Haskell.TH.Alpha ( areExpAEq,- exp_equal,+ expEqual,+ (@=), AlphaEq(..) ) where import Language.Haskell.TH-import Language.Haskell.TH.Syntax (Quasi, returnQ)+import Language.Haskell.TH.Syntax (Quasi) import Language.Haskell.TH.Desugar import Data.Function (on)-import Control.Monad (liftM, liftM2, liftM3, join, foldM)-import Data.Data (toConstr, Data)+import Control.Monad.State+import Control.Monad.Identity+import Control.Monad.Trans.Maybe+import Control.Monad.Morph import Data.Maybe (isJust)+import qualified Data.Map as Map+import Control.Applicative -- A poor man's bound variable lookup table.-type Lookup = ([(Name,Int)], [(Name,Int)], Int)+type Lookup = (Map.Map Name Int, Map.Map Name Int, Int) +emptyLookup :: Lookup+emptyLookup = (Map.empty, Map.empty, 0)++data LookupTbl = LookupTbl+ { insertLR :: Name -> Name -> LookupTbl+ , eqInTbl :: Name -> Name -> Bool+ , isInL :: Name -> Bool+ , isInR :: Name -> Bool+ }++mapLookup :: Lookup -> LookupTbl+mapLookup !(ls,rs,cnt) = LookupTbl+ { insertLR = \a b -> mapLookup (Map.insert a cnt ls,+ Map.insert b cnt rs,+ cnt + 1)+ , eqInTbl = \a b -> Map.lookup a ls == Map.lookup b rs+ , isInL = \a -> isJust $ Map.lookup a ls+ , isInR = \b -> isJust $ Map.lookup b rs+ }+++-- Monad holding lookup table if alpha equivalence is still possible,+-- Nothing otherwise. Parametrized also on an extra monad 'm', which is+-- needed for a single, unified interface for th and th-desugar types (the+-- former will use a Quasi monad, the latter Identity).+newtype LookupSTM m b = LookupST {+ unLookupST :: StateT LookupTbl (MaybeT m) b+ } deriving (Functor, Applicative, Monad, MonadState LookupTbl+ , MonadPlus, Alternative)++---------------------------------------------------------------------------+-- Lifting and hoisting+--+-- This section is primarily concerned with making moving from a pure+-- (Identity) context to other monads easy. We do this because desugaring+-- (and other TH-related activities) end us up in some Quasi monad, so+-- when a AlphaEq instance uses th-desugar for its arguments, but a pure+-- function for its subexpressions, it ends up crossing a signature+-- boundary that ideally shouldn't be annoying.+---------------------------------------------------------------------------+instance MonadTrans (LookupSTM) where+ -- Laws:+ -- 1. lift . return == return+ -- LookupST $ StateT (\tbl -> MaybeT $ return n >>= \x -> return $ Just (x, tbl))+ -- LookupST $ StateT (\tbl -> MaybeT $ Just (n, tbl))+ -- 2. lift (m >>= f) == lift m >>= (lift . f)+ lift m = LookupST $ StateT (\tbl -> MaybeT $ m >>= \x -> return $ Just (x, tbl))+++-- This is ugly, but the signature and name should explain it well enough.+hoist' :: (Monad m) => (forall a . m a -> n a) -> LookupSTM m b -> LookupSTM n b+hoist' nat lkstm = LookupST $ StateT (\tbl -> MaybeT . nat . runMaybeT $ runStateT (unLookupST lkstm) tbl)++instance MFunctor LookupSTM where+ hoist = hoist'++toQ :: LookupST b -> LookupSTQ b+toQ = hoist generalize++type LookupST b = LookupSTM Identity b+type LookupSTQ b = LookupSTM Q b+++runLookupST :: Monad m => LookupSTM m a -> LookupTbl -> m (Maybe (a, LookupTbl))+runLookupST st tbl = runMaybeT $ runStateT (unLookupST st) tbl++runLookupST' :: LookupST a -> LookupTbl -> Maybe (a, LookupTbl)+runLookupST' = (runIdentity .) . runLookupST+ -- | The main Alpha Equivalence class. '@=' is by default defined in terms -- of 'lkEq'. 'lkEq' is exposed for composability: it is easy to -- recursively build 'AlphaEq' instances from other 'AlphaEq' instances by -- delegating the lookup update to the subinstances.-class AlphaEq a where- -- | Compares its arguments for alpha equivalence.- (@=) :: a -> a -> Bool+class AlphaEq a m | a -> m where -- | Given a variable binding lookup compares arguments for alpha- -- equivalence, returning Just of updated lookup in case of+ -- equivalence, setting the state to Just of updated lookup in case of -- equivalence, Nothing otherwise.- lkEq :: a -> a -> Lookup -> Maybe Lookup- x @= y = isJust $ lkEq x y ([], [], 0)+ lkEq :: a -> a -> LookupSTM m () +-- | Compares its arguments for alpha equivalence. The default+-- implementation uses Lookup for its LookupTbl, but more efficient+-- datatypes can be used.+(@=) :: (Monad m, AlphaEq a m) => a -> a -> m Bool+x @= y = liftM isJust $ runLookupST (lkEq x y) (mapLookup emptyLookup) +infix 4 @= -- Same as (==)++ --------------------------------------------------------------------------- -- Exp --------------------------------------------------------------------------- --- | Convenience function that uses 'runQ' on 'exp_equal'.+-- | Convenience function that uses 'runQ' on 'expEqual'. -- -- >>> areExpAEq [| let x = 5 in x |] [| let y = 5 in y |] -- True@@ -71,144 +155,195 @@ => ExpQ -- ^ Quoted expression -> ExpQ -- ^ Quoted expression -> m Bool-areExpAEq e1 e2 = let expM = (join .) . liftM2 exp_equal+areExpAEq e1 e2 = let expM = (join .) . liftM2 expEqual in expM (runQ e1) (runQ e2) --- | Compare two expressions for alpha-equivalence. Since this uses--- th-desugar to desugar the expressions, returns a Bool in the Quasi--- context.-exp_equal :: Quasi m => Exp -> Exp -> m Bool-exp_equal t1 t2 = (liftM3 exp_equal') (dsExp t1) (dsExp t2) (return ([], [], 0))+instance AlphaEq Exp Q where+ lkEq e1 e2 = do+ e1' <- lift $ dsExp e1+ e2' <- lift $ dsExp e2+ toQ $ expEqual' e1' e2' -instance AlphaEq DExp where- lkEq a b lk = if exp_equal' a b lk then Just lk else Nothing -exp_equal' :: DExp -> DExp -> Lookup -> Bool-exp_equal' (DVarE a) (DVarE b) (m1,m2,_) = lookup a m1 == lookup b m2-exp_equal' (DConE a) (DConE b) (m1,m2,_) = lookup a m1 == lookup b m2- && (isJust $ lookup a m1)-exp_equal' (DLitE l1) (DLitE l2) _ = l1 == l2-exp_equal' (DAppE a1 a2) (DAppE b1 b2) c = (exp_equal' a1 b1 c)- && (exp_equal' a2 b2 c)-exp_equal' (DLamE a1 a2) (DLamE b1 b2) (m1,m2,cnt) =- if ((/=) `on` length) a1 b1- then False- else exp_equal' a2 b2 ((ato a1 ++ m1),(ato b1 ++ m2), l)- where ato x = zip x [cnt..]- l = cnt + length a1-exp_equal' (DCaseE a1 a2) (DCaseE b1 b2) c =- if length a2 == length b2- then exp_equal' a1 b1 c && (any id $ zipWith mec a2 b2)- else False- where mec x y = match_equal x y c-exp_equal' (DLetE a1 a2) (DLetE b1 b2) c =- isJust (foldM lkEqC c (zip a1 b1) >>= lkEq a2 b2)- where lkEqC l (a,b) = lkEq a b l-exp_equal' (DSigE a1 a2) (DSigE b1 b2) c@(m1,m2,_) =- lkEqB a1 b1 c && lkEqB a2 b2 c-exp_equal' _ _ _ = False+{--- | Compare two expressions for alpha-equivalence. Since this uses-}+{--- th-desugar to desugar the expressions, returns a Bool in the Quasi-}+{--- context.-}+expEqual :: Quasi m => Exp -> Exp -> m Bool+expEqual t1 t2 = do+ t1' <- dsExp t1+ t2' <- dsExp t2+ let lkt = mapLookup emptyLookup+ return $ isJust $ runLookupST' (lkEq t1' t2') lkt ------------------------------------------------------------------------------- Match---------------------------------------------------------------------------- -match_equal :: DMatch -> DMatch -> Lookup -> Bool-match_equal (DMatch pat1 exp1) (DMatch pat2 exp2) c =- case lkEq pat1 pat2 c of- Just d -> exp_equal' exp1 exp2 d- Nothing -> False+instance AlphaEq DExp Identity where+ lkEq = expEqual' ------------------------------------------------------------------------------- LetDec---------------------------------------------------------------------------- -instance AlphaEq DLetDec where- lkEq = letDec_equal+expEqual' :: DExp -> DExp -> LookupST ()+expEqual' (DVarE a1 ) (DVarE a2 ) = a1 ~=~ a2+expEqual' (DConE a1 ) (DConE a2 ) = a1 ~=~ a2+expEqual' (DLitE l1 ) (DLitE l2 ) = guard $ l1 == l2+expEqual' (DAppE a1 b1 ) (DAppE a2 b2 ) = lkEq a1 a2 >> lkEq b1 b2+expEqual' (DLamE a1 b1 ) (DLamE a2 b2 ) = do+ guard $ ((==) `on` length) a1 a2+ zipWithM_ insertLRLST a1 a2+ lkEq b1 b2+ return ()+expEqual' (DCaseE a1 b1) (DCaseE a2 b2) = do+ guard $ length b1 == length b2+ lkEq a1 a2+ zipWithM_ lkEq b1 b2+ return ()+expEqual' (DLetE a1 b1 ) (DLetE a2 b2 ) = zipWithM_ lkEq a1 a2 >> lkEq b1 b2+expEqual' (DSigE a1 b1 ) (DSigE a2 b2 ) = lkEq a1 a2 >> lkEq b1 b2+expEqual' _ _ = mzero -letDec_equal :: DLetDec -> DLetDec -> Lookup -> Maybe Lookup-letDec_equal (DFunD n1 cls1) (DFunD n2 cls2) c =- if n1 == n2 then foldM lkEqC c (zip cls1 cls2) else Nothing- where lkEqC l (a,b) = lkEq a b l-letDec_equal (DValD pat1 exp1) (DValD pat2 exp2) c =- lkEq exp1 exp2 c >>= lkEq pat1 pat2-letDec_equal (DSigD name1 typ1) (DSigD name2 typ2) c@(m1,m2,_) =- -- Hard to tell how the name will be bound, so just check types- lkEq typ1 typ2 c-letDec_equal (DInfixD fx1 name1) (DInfixD fx2 name2) c =- if fx1 == fx2 && name1 == name2 then Just c else Nothing-letDec_equal _ _ _ = Nothing+{-----------------------------------------------------------------------------}+{--- Match-}+{-----------------------------------------------------------------------------}+instance AlphaEq DMatch Identity where+ lkEq = matchEqual ------------------------------------------------------------------------------- LetDec----------------------------------------------------------------------------+matchEqual :: DMatch -> DMatch -> LookupST ()+matchEqual (DMatch pat1 exp1) (DMatch pat2 exp2) = lkEq pat1 pat2+ >> lkEq exp1 exp2 -instance AlphaEq DType where- lkEq = type_equal+{-----------------------------------------------------------------------------}+{--- LetDec-}+{-----------------------------------------------------------------------------} --- TODO:-type_equal :: DType -> DType -> Lookup -> Maybe Lookup-type_equal (DForallT tybs1 ctx1 typ1) (DForallT tybs2 ctx2 typ2) c = do- nlk <- type_equal typ1 typ2 c- if all (\y -> cmpTYvar y nlk) (zip tybs1 tybs2)- then Just nlk- else Nothing- where cmpTYvar ((DPlainTV n1),(DPlainTV n2)) c' = cmpLk n1 n2 c'- cmpTYvar ((DKindedTV n1 k1),(DKindedTV n2 k2)) c' =- cmpLk n1 n2 c' && lkEqB k1 k2 c'- cmpTYvar _ _ = False-type_equal (DAppT ty1 arg1) (DAppT ty2 arg2) c = undefined-type_equal (DSigT ty1 knd1) (DAppT ty2 knd2) c = undefined-type_equal (DVarT n1) (DVarT n2) c = undefined+instance AlphaEq DLetDec Identity where+ lkEq = letDecEqual +letDecEqual :: DLetDec -> DLetDec -> LookupST ()+letDecEqual (DFunD n1 cls1 ) (DFunD n2 cls2 ) = do+ guard $ n1 == n2+ zipWithM_ lkEq cls1 cls2+letDecEqual (DValD pat1 exp1 ) (DValD pat2 exp2 ) =+ lkEq exp1 exp2 >> lkEq pat1 pat2+letDecEqual (DSigD _name1 typ1) (DSigD _name2 typ2) =+ -- Hard to tell how the name will be bound, so just check types+ lkEq typ1 typ2+letDecEqual (DInfixD fx1 name1) (DInfixD fx2 name2) = guard $ fx1 == fx2+ && name1 == name2+letDecEqual _ _ = mzero++{-----------------------------------------------------------------------------}+{--- Type-}+{-----------------------------------------------------------------------------}++instance AlphaEq DType Identity where+ lkEq = typeEqual++{--- TODO:-}+typeEqual :: DType -> DType -> LookupST ()+-- Type-level and value-level variable names don't conflict, so we can keep+-- both in the same mapping+typeEqual (DForallT tybs1 ctx1 typ1) (DForallT tybs2 ctx2 typ2) = do+ zipWithM_ insertLRLSTty tybs1 tybs2+ zipWithM_ lkEq ctx1 ctx2+ lkEq typ1 typ2+typeEqual (DAppT ty1 arg1 ) (DAppT ty2 arg2 ) =+ lkEq ty1 ty2 >> lkEq arg1 arg2+typeEqual (DSigT ty1 knd1 ) (DSigT ty2 knd2 ) = do+ guard $ show knd1 == show knd2+ lkEq ty1 ty2+typeEqual (DConT n1 ) (DConT n2 ) =+ guard $ show n1 == show n2+typeEqual (DVarT n1 ) (DVarT n2 ) =+ n1 ~=~ n2+typeEqual _ _ = mzero+ --------------------------------------------------------------------------- -- Kind ------------------------------------------------------------------------------ TODO:-instance AlphaEq DKind where- lkEq = undefined+instance AlphaEq DKind Identity where+ lkEq = kindEqual +kindEqual :: DKind -> DKind -> LookupST ()+kindEqual (DForallK ns1 typ1 ) (DForallK ns2 typ2 ) = do+ zipWithM_ insertLRLST ns1 ns2+ lkEq typ1 typ2+kindEqual (DVarK n1 ) (DVarK n2 ) = n1 ~=~ n2+{-kindEqual (DConK n1 knds1 ) (DConK n2 knds2 ) = n1 ~=~ n2-}+kindEqual (DArrowK knda1 kndb1) (DArrowK knda2 kndb2) = lkEq knda1 knda2+ >> lkEq kndb1 kndb2+kindEqual DStarK DStarK = return ()+kindEqual _ _ = mzero+ --------------------------------------------------------------------------- -- Clause ----------------------------------------------------------------------------instance AlphaEq DClause where- lkEq = clause_equal+instance AlphaEq DClause Identity where+ lkEq = clauseEqual -clause_equal :: DClause -> DClause -> Lookup -> Maybe Lookup-clause_equal (DClause pats1 exp1) (DClause pats2 exp2) lk =- pat_res >>= lkEq exp1 exp2- where lkEqC l (a,b) = lkEq a b l- pat_res = foldM lkEqC lk (zip pats1 pats2)+clauseEqual :: DClause -> DClause -> LookupST ()+clauseEqual (DClause pats1 exp1) (DClause pats2 exp2) =+ zipWithM_ lkEq pats1 pats2 >> lkEq exp1 exp2 ---------------------------------------------------------------------------+-- Clause+---------------------------------------------------------------------------+instance AlphaEq DPred Identity where+ lkEq = predEqual++predEqual :: DPred -> DPred -> LookupST ()+predEqual (DAppPr pred1 typ1 ) (DAppPr pred2 typ2 ) = lkEq pred1 pred2+ >> lkEq typ1 typ2+predEqual (DSigPr pred1 kind1) (DSigPr pred2 kind2) = lkEq pred1 pred2+ >> lkEq kind1 kind2+predEqual (DVarPr n1 ) (DVarPr n2 ) = n1 ~=~ n2+predEqual (DConPr n1 ) (DConPr n2 ) = n1 ~=~ n2+predEqual _ _ = mzero++--------------------------------------------------------------------------- -- Pat --------------------------------------------------------------------------- -instance AlphaEq DPat where- lkEq = pat_equal+instance AlphaEq DPat Identity where+ lkEq = patEqual -pat_equal :: DPat -> DPat -> Lookup -> Maybe Lookup-pat_equal (DLitPa lit1) (DLitPa lit2) c = if lit1 == lit2- then Just c- else Nothing-pat_equal (DVarPa n1) (DVarPa n2) c = Just (addn n1 n2 c)- where addn x y (m1,m2,i) = ((x,i):m1,(y,i):m2,i+1)-pat_equal (DConPa n1 p1) (DConPa n2 p2) c@(m1,m2,i) =- if (lookup n1 m1 == lookup n2 m2 && length p1 == length p2)- then foldM cmbn c (zip p1 p2) -- Does this allow bindings across patterns?- else Nothing- where cmbn cn (x,y) = pat_equal x y c-pat_equal (DTildePa pat1) (DTildePa pat2) c = pat_equal pat1 pat2 c-pat_equal (DBangPa pat1) (DBangPa pat2) c = pat_equal pat1 pat2 c-pat_equal DWildPa DWildPa c = Just c-pat_equal _ _ _ = Nothing+patEqual :: DPat -> DPat -> LookupST ()+patEqual (DLitPa lit1 ) (DLitPa lit2 ) = guard $ lit1 == lit2+patEqual (DVarPa n1 ) (DVarPa n2 ) = insertLRLST n1 n2+patEqual (DConPa n1 p1 ) (DConPa n2 p2 ) = do+ n1 ~=~ n2+ guard $ length p1 == length p2+ zipWithM_ lkEq p1 p2 -- Does this allow bindings across+ -- patterns?+patEqual (DTildePa pat1) (DTildePa pat2) = lkEq pat1 pat2+patEqual (DBangPa pat1 ) (DBangPa pat2 ) = lkEq pat1 pat2+patEqual DWildPa DWildPa = return ()+patEqual _ _ = mzero --------------------------------------------------------------------------- -- Utils --------------------------------------------------------------------------- -fst3 (a,_,_) = a-snd3 (_,b,_) = b-thrd3 (_,_,c) = c-cmpLk a b (m1,m2,_) = lookup a m1 == lookup b m2-cmpLkC (a,b) c = cmpLk a b c-lkEqB a b c = isJust $ lkEq a b c+(~=~) :: Name -> Name -> LookupST ()+a ~=~ b = do+ tbl <- get+ guard $ eqInTbl tbl a b+ bol <- isInL' a+ unless bol $ guard $ show a == show b+++isInL' :: Name -> LookupST Bool+isInL' n = do+ tbl <- get+ return $ isInL tbl n+++insertLRLST :: Name -> Name -> LookupST ()+insertLRLST a b = modify $ \tbl -> insertLR tbl a b++insertLRLSTty :: DTyVarBndr -> DTyVarBndr -> LookupST ()+insertLRLSTty (DPlainTV n1 ) (DPlainTV n2 ) = insertLRLST n1 n2+insertLRLSTty (DKindedTV n1 k1) (DKindedTV n2 k2) = do+ guard $ show k1 == show k2 -- Duck-show-template-kinding:+ -- If it shows like a duck, it is+ -- a duck+ insertLRLST n1 n2+insertLRLSTty _ _ = mzero+
tests/tests.hs view
@@ -1,25 +1,31 @@-{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TemplateHaskell #-} module Main where import Test.Tasty import Test.Tasty.HUnit -import Language.Haskell.TH-import Control.Monad (liftM2, join) +import Language.Haskell.TH import Language.Haskell.TH.Alpha +main :: IO () main = defaultMain tests tests :: TestTree tests = testGroup "Tests" [unitTests] +unitTests :: TestTree unitTests = testGroup "Unit tests" [ testCase "Lambda expressions with different bound variables" $ do b <- areExpAEq [| \x -> x|] [| \y -> y|] assertBool "Expressions not considered equal!" b+ , testCase "Nested lambda expressions with different bound variables" $+ do+ b <- areExpAEq [| \f -> \a -> \b -> f a b |] [| \g -> \x -> \y -> g x y|]+ assertBool "Expressions not considered equal!" b+ , testCase "Equal literals" $ do b <- areExpAEq [| 5 |] [| 5 |]@@ -31,6 +37,24 @@ , testCase "Let bindings" $ do b <- areExpAEq [| let x = 5 in x |] [| let y = 5 in y |]+ assertBool "Expressions not considered equal!" b+ , testCase "Different open terms" $+ do+ b <- areExpAEq [| tail |] [| head |]+ assertBool "Expressions considered equal!" (not b)+ , testCase "Same open terms" $+ do+ b <- areExpAEq [| tail |] [| tail |]+ assertBool "Expressions not considered equal!" b+ , testCase "Same lambda'd terms" $+ do+ b <- areExpAEq [| \x -> tail x |] [| \y -> tail y |]+ assertBool "Expressions not considered equal!" b+ , testCase "@=" $+ do+ let x = mkName "x"+ let y = mkName "y"+ b <- runQ $ (LamE [VarP x] (VarE x)) @= (LamE [VarP y] (VarE y)) assertBool "Expressions not considered equal!" b ]
th-alpha.cabal view
@@ -2,17 +2,24 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: th-alpha-version: 0.1.0.2+version: 0.2.0.0 synopsis: Alpha equivalence for TH Exp description: Compare TH expressions (or clauses, patterns, etc.) for alpha equivalence. That is, compare for equality modulo the renaming of bound variables. .- >>> areExpAEq [| \x -> x |] [| \y -> y |]- True+ > areExpAEq [| \x -> x |] [| \y -> y |]+ > -- True .+ > do+ > let x = mkName "x"+ > let y = mkName "y"+ > runQ $ (LamE [VarP x] (VarE x)) @= (LamE [VarP y] (VarE y))+ > -- True+ . This can be useful when for instance testing libraries that use Template Haskell - usually correctness is only defined up to alpha equivalence.+ license: BSD3 license-file: LICENSE author: Julian K. Arni@@ -29,17 +36,25 @@ exposed-modules: Language.Haskell.TH.Alpha build-depends: base >=4 && <5 , template-haskell + , containers , th-desugar+ , mtl >=2 && <3+ , transformers+ , mmorph hs-source-dirs: src+ ghc-options: -Wall default-language: Haskell2010 Test-Suite test type: exitcode-stdio-1.0 hs-source-dirs: tests+ ghc-options: -Wall main-is: tests.hs build-depends: base >= 4 && < 5 , th-alpha , template-haskell , tasty >= 0.8 , tasty-hunit+ , tasty-quickcheck+ , derive default-language: Haskell2010