{-# LANGUAGE ScopedTypeVariables, FlexibleContexts #-} {-# OPTIONS_GHC -fno-warn-unused-binds #-} -- | -- Copyright : (c) 2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt -- -- Unit tests for the functions dealing with term algebra and related notions. module Term.UnitTests (main) where import Term.Substitution import Term.Subsumption import Term.Builtin.Convenience import Term.Unification import Term.Rewriting.Norm import Term.Narrowing.Variants import Term.Positions import Text.PrettyPrint.Class import Data.List import Data.Maybe import Prelude hiding ( catch ) import Test.HUnit import Control.Monad.Reader import Data.Monoid testEqual :: (Eq a, Show a) => String -> a -> a -> Test testEqual t a b = TestLabel t $ TestCase $ assertEqual t b a testTrue :: String -> Bool -> Test testTrue t a = TestLabel t $ TestCase $ assertBool t a -- ***************************************************************************** -- Tests for Matching -- ***************************************************************************** testsMatching :: MaudeHandle -> Test testsMatching hnd = TestLabel "Tests for Matching" $ TestList [ testTrue "a" (propMatchSound hnd f1 f2) , testTrue "b" (propMatchSound hnd (pair(f1,inv(f2))) (pair(f1,inv(f2)))) , testTrue "c" (propMatchSound hnd t1 t2) , testTrue "d" (propMatchSound hnd (x1 # f1) f1) , testTrue "e" $ null (solveMatchLNTerm (pair(x1,x2) `matchWith` pair(x1,x1)) `runReader` hnd) ] where t1 = expo (inv(pair(f1,f2)), f2 # (inv f2) # f3 # f4 # f2) t2 = expo (inv(pair(f1,f2)), f3 # (inv f2) # f2 # x1 # f5 # f2) propMatchSound :: MaudeHandle -> LNTerm -> LNTerm -> Bool propMatchSound mhnd t1 p = all (\s -> applyVTerm s t1 == applyVTerm s p) substs where substs = solveMatchLNTerm (t1 `matchWith` p) `runReader` mhnd -- ***************************************************************************** -- Tests for Unification -- ***************************************************************************** testsUnify :: MaudeHandle -> Test testsUnify mhnd = TestLabel "Tests for Unify" $ TestList [ testTrue "a" (propUnifySound mhnd f1 f2) , testTrue "b" (propUnifySound mhnd (pair(f1,inv(f2))) (pair(f1,inv(f2)))) , testTrue "c" (propUnifySound mhnd t1 t2) , testTrue "d" (propUnifySound mhnd u1 u2) , testTrue "f" (propUnifySound mhnd (sdec(x1,y1)) (sdec(senc(x2,x3), x4))) ] where t1 = expo (inv(pair(f1,f2)), f2 *: (inv f2) *: f3 *: f4 *: x2) t2 = expo (inv(pair(f1,f2)), f3 *: (inv f2) *: f2 *: f4 *: f5 *: f2) u1 = (f2 *: (inv f2) *: f3 *: f4 *: x2) u2 = (f3 *: (inv f2) *: f2 *: f4 *: f5 *: f2) propUnifySound :: MaudeHandle -> LNTerm -> LNTerm -> Bool propUnifySound hnd t1 t2 = all (\s -> let s' = freshToFreeAvoiding s [t1,t2]in applyVTerm s' t1 == applyVTerm s' t2) substs where substs = unifyLNTerm [Equal t1 t2] `runReader` hnd -- ***************************************************************************** -- Tests for Substitutions -- ***************************************************************************** testsSubst :: Test testsSubst = TestLabel "Tests for Substitution" $ TestList [ -- introduce renaming for x3 testEqual "a" (substFromListVFresh [(lx1, p1), (lx2, x6), (lx3,x6), (lx5, p1)]) (composeVFresh (substFromListVFresh [(lx5, p1)]) (substFromList [(lx1, x5), (lx2, x3)])) -- rename (fresh) x6 in s1b and do not mix up with x6 in s3f , testEqual "b" s1b_o_s3f (composeVFresh s1b s3f) -- drop x1 |-> p1 mapping from s1b, but apply to x2 |-> pair(x3,x1) in s3f , testEqual "c" s1b_o_s4f (composeVFresh s1b s4f) , testEqual "d" s4f_o_s3f (compose s4f s3f) , testEqual "e" (substFromList [(lx1,f1), (lx2,f1)]) (mapRange (const f1) s4f) , testTrue "f" (isRenaming (substFromListVFresh [(lx1,x3), (lx2,x2), (lx3,x1)])) , testEqual "g" (substFromListVFresh [(lx1, f1)]) (extendWithRenaming [lx1] (substFromListVFresh [(lx1, f1)])) , testEqual "h" (substFromListVFresh [(lx2, x1), (lx1, x2)]) (extendWithRenaming [lx1] (substFromListVFresh [(lx2, x1)])) -- trivial, increase coverage , testTrue "i" ((>0) . length $ show s1b) , testTrue "j" ((>0) . length $ (render $ prettyLSubstVFresh s1b)) , testTrue "k" (not . null $ domVFresh s1b) , testTrue "l" (not . null $ varsRangeVFresh s1b) , testTrue "m" ((>0) . length $ show $ substToListOn [lx1] s4f) , testTrue "n" ((<100) . size $ emptySubst) , testTrue "o" ((<10000) . size $ s1b) , testTrue "p" ((<100) . size $ emptySubstVFresh) ] where s1b = substFromListVFresh [(lx1, p1), (lx2, x6), (lx3, x6), (lx4, f1)] s3f = substFromList [(lx8, x6), (lx2, pair(x2,x1))] s1b_o_s3f = substFromListVFresh -- x2 not identified with x8 [(lx1, p1), (lx2, pair(x9, p1)), (lx3, x9), (lx4, f1), (lx6, x10), (lx8, x10)] s4f = substFromList [(lx1, x6), (lx2, pair(x3,x1))] s1b_o_s4f = substFromListVFresh [(lx1, x8), (lx2, pair(x7, p1)), (lx3, x7), (lx4, f1), (lx6, x8)] s4f_o_s3f = substFromList [(lx1, x6), (lx2, pair(pair(x3,x1),x6)), (lx8, x6)] x15 = varTerm $ LVar "x" LSortMsg 15 x13 = varTerm $ LVar "x" LSortMsg 13 x20 = varTerm $ LVar "x" LSortMsg 20 x22 = varTerm $ LVar "x" LSortMsg 22 -- ***************************************************************************** -- Tests for Subsumption -- ***************************************************************************** testsSubs :: MaudeHandle -> Test testsSubs mhnd = TestLabel "Tests for Subsumption" $ TestList [ tct Nothing f1 f2 , tct (Just EQ) x1 x2 , tct (Just LT) x1 (x1 *: x1) , tct (Just GT) (x1 *: x1) x1 , tct (Just GT) (pair(f1 *: f2,f1)) (pair(f2 *: f1,x2)) , testEqual "a" [substFromList [(lx2, pair(x6,x7)), (lx3, p1)]] (factorSubstVia [lx1] (substFromList [(lx1,pair(pair(x6,x7),p1))]) (substFromList [(lx1,pair(x2,x3))]) `runReader` mhnd) , testEqual "b" [substFromList [(lx2, pair(x6,x7)), (lx3, p1), (lx5, f1), (lx6,f2)]] (factorSubstVia [lx1, lx5, lx6] (substFromList [(lx1,pair(pair(x6,x7),p1)), (lx5,f1), (lx6,f2)]) (substFromList [(lx1,pair(x2,x3))]) `runReader` mhnd) , testTrue "c" (eqTermSubs p1 p1 `runReader` mhnd) ] where tct res e1 e2 = testEqual ("termCompareSubs "++ppLTerm e1++" "++ppLTerm e2) res (compareTermSubs e1 e2 `runReader` mhnd) ppLTerm :: LNTerm -> String ppLTerm = render . prettyNTerm ppLSubst :: LNSubst -> String ppLSubst = render . prettyLNSubst -- ***************************************************************************** -- Tests for Norm -- ***************************************************************************** testsNorm :: MaudeHandle -> Test testsNorm hnd = TestLabel "Tests for normalization" $ TestList [ tcn normBigTerm bigTerm , tcn (expo(f3,f1 *: f4)) (expo(expo(f3,f4),f1 *: f1 *: f2 *: inv (inv (inv f1)) *: one *: expo(inv f2,one))) , tcn (mult [f1, f1, f2]) (f1 *: (f1 *: f2)) , tcn (inv (f1 *: f2)) (inv f2 *: inv f1) , tcn (f1 *: inv f2) (f1 *: inv f2) , tcn (one::LNTerm) one , tcn x6 (expo(expo(x6,inv x3),x3)) -- , testEqual "a" (normAC (p3 *: (p1 *: p2))) (mult [p1, p2, p3]) -- , testEqual "b" (normAC (p3 *: (p1 *: inv p3))) (mult [p1, p3, inv p3]) -- , testEqual "c" (normAC ((p1 *: p2) *: p3)) (mult [p1, p2, p3]) -- , testEqual "d" (normAC t1) (mult [p1, p2, p3, p4]) -- , testEqual "e" (normAC ((p1 # p2) *: p3)) (p3 *: (p1 # p2)) -- , testEqual "f" (normAC (p3 *: (p1 # p2))) (p3 *: (p1 # p2)) -- , testEqual "g" (normAC ((p3 *: p4) *: (p1 # p2))) (mult [p3, p4, p1 # p2]) ] where tcn e1 e2 = testEqual ("norm "++ppLTerm e2) e1 (norm' e2 `runReader` hnd) t1 = (p1 *: p2) *: (p3 *: p4) -- ***************************************************************************** -- Tests for Term -- ***************************************************************************** testsTerm :: Test testsTerm = TestLabel "Tests for Terms" $ TestList [ uncurry (testEqual "Terms: propSubtermReplace") (propSubtermReplace bigTerm [1,0]) ] propSubtermReplace :: Ord a => Term a -> Position -> (Term a, Term a) propSubtermReplace t p = (t,(t `replacePos` (t `atPos` p,p))) bigTerm :: LNTerm bigTerm = pair(pk(x1), expo(expo (inv x3, x2 *: x4 *: f1 *: one *: inv (f3 *: f4) *: f3 *: f4 *: inv one), inv(expo(x2,one)) *: f2)) normBigTerm :: LNTerm normBigTerm = pair(pk(x1),expo(inv x3,mult [f1, f2, x4])) tcompare :: MaudeHandle -> Test tcompare hnd = TestLabel "Tests for variant order" $ TestList [ testTrue "a" (run $ isNormalInstance t su1 su2) , testTrue "b" $ not (run $ isNormalInstance t su1 su3) , testTrue "c" $ (run $ leqSubstVariant t su5 su4) , testTrue "d" $ not (run $ leqSubstVariant t su6 su4) , testEqual "e" (run $ compareSubstVariant t su4 su4) (Just EQ) , testEqual "f" (run $ compareSubstVariant t su5 su4) (Just LT) , testEqual "g" (run $ compareSubstVariant t su4 su5) (Just GT) , testEqual "h" (run $ compareSubstVariant t su6 su4) Nothing ] where run :: WithMaude a -> a run m = runReader m hnd t = pair(inv(x1) *: x2, inv(x3) *: x2) su1 = substFromList [(lx1, x2)] su2 = substFromList [(lx2, p1)] su3 = substFromList [(lx3, x2)] su4 = substFromListVFresh [(lx1, x4), (lx2, x4)] su5 = substFromListVFresh [(lx1, p1), (lx2, p1)] su6 = substFromListVFresh [(lx1, x4), (lx2, x4), (lx3, x4)] testsVariant :: MaudeHandle -> Test testsVariant hnd = TestLabel "Tests for variant computation" $ TestList [ testEqual "a" (computeVariantsCheck (sdec(x1, p1)) `runReader` hnd) (toSubsts [ [] , [(lx1, senc(x1, p1))] ]) , testEqual "b" (computeVariantsCheck (x1 *: p1) `runReader` hnd) (toSubsts [ [] , [(lx1, one)] , [(lx1, inv(p1))] , [(lx1, inv(p1 *: x1))] , [(lx1, x1 *: inv(p1))] , [(lx1, x1 *: inv(p1 *: x2))] ]) , testEqual "c" (sort $ computeVariantsCheck (fAppList [x1, x2, x1 +: x2]) `runReader` hnd) (sort $ toSubsts [ [] , [(lx1, x1), (lx2,x1) ] , [(lx2,zero)] , [(lx1,zero)] , [(lx2, x1 +: x2), (lx1, x2)] , [(lx1, x1 +: x2), (lx2, x2)] , [(lx1, x2 +: x3), (lx2, x1 +: x3)] ]) , testEqual "d" (computeVariantsCheck (fAppList [s1, s2, s1 # s2]) `runReader` hnd) (toSubsts [ [] , [(ls1, emptyMSet)] , [(ls2, emptyMSet) ] ]) , testTrue "e" $ not (checkComplete (sdec(x1, p1)) (toSubsts [[]]) `runReader` hnd) , testTrue "f" $ (checkComplete (sdec(x1, p1)) (toSubsts [[], [(lx1, senc(x1,p1))]]) `runReader` hnd) ] where toSubsts = map substFromListVFresh testsSimple :: MaudeHandle -> Test testsSimple _hnd = TestLabel "Tests for simple functions" $ TestList [ testTrue "" (size [bigTerm] > 0) ] -- | Execute all unification infrastructure unit tests. main :: FilePath -- ^ Path to maude executable. -> IO Counts main maudePath = do mhnd <- startMaude maudePath allMaudeSig runTestTT $ TestList [ testsVariant mhnd , tcompare mhnd , testsSubs mhnd , testsTerm , testsSubst , testsNorm mhnd , testsUnify mhnd , testsSimple mhnd , testsMatching mhnd ] -- | Maude signatures with all builtin symbols. allMaudeSig :: MaudeSig allMaudeSig = mconcat [ dhMaudeSig, xorMaudeSig, msetMaudeSig , pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig, hashMaudeSig ] -- testing in ghci ---------------------------------------------------------------------------------- te :: LNTerm te = pair(inv(x1) *: x2, inv(x3) *: x2) sub4, sub6 :: LNSubstVFresh sub4 = substFromListVFresh [(lx1, x4), (lx2, x4)] sub6 = substFromListVFresh [(lx1, x4), (lx2, x4), (lx3, x4)] sub4', sub6' :: LNSubst sub4' = freshToFreeAvoiding sub4 te sub6' = freshToFreeAvoiding sub6 te tevs :: [LVar] tevs = frees te runTest :: WithMaude a -> IO a runTest m = do hnd <- startMaude "maude" allMaudeSig return $ m `runReader` hnd ts1 :: LNSubstVFresh ts1 = substFromListVFresh [(lx1, xor [x2,x3]), (lx2, xor [x1,x2,x3]) ] ts2 :: LNSubstVFresh ts2 = substFromListVFresh [(lx1, x2), (lx2, xor [x1,x2]) ] ts1' :: LNSubst ts1' = substFromList [(lx1, xor [x5,x6]), (lx2, xor [x4,x5,x6]) ] ts2' :: LNSubst ts2' = substFromList [(lx1, y2), (lx2, xor [y1, y2]) ] ts2'' :: LNSubst ts2'' = substFromList [(lx1, x5), (lx2, xor [x5, x6]) ] tterm :: LNTerm tterm = fAppList [x1, x2, (x1 +: x2)] {- runTest $ matchLNTerm [ pair(xor [x5,x6],xor [x4,x5,x6]) `MatchWith` pair(x5,xor [x5,x4]) ] should be matchable if next matchable also runTest $ matchLNTerm [ pair(xor [x5,x6],xor [x4,x5,x6]) `MatchWith` pair(x5,xor [x5,x6]) ] -} -- convenience abbreviations ---------------------------------------------------------------------------------- pair, expo :: (Term a, Term a) -> Term a expo = fAppExp pair = fAppPair inv :: Term a -> Term a inv = fAppInv xor, union, mult :: Ord a => [Term a] -> Term a xor = fAppXor union = fAppUnion mult = fAppMult one, zero, emptyMSet :: Term a one = fAppOne zero = fAppZero emptyMSet = fAppEmpty