{-# LANGUAGE ScopedTypeVariables, FlexibleContexts #-}
{-# OPTIONS_GHC -fno-warn-unused-binds #-}
-- |
-- Copyright : (c) 2012 Benedikt Schmidt
-- License : GPL v3 (see LICENSE)
--
-- Maintainer : Benedikt Schmidt <beschmi@gmail.com>
--
-- 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 (matchLNTerm [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 = matchLNTerm [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, x9), (lx3,x9), (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, x3)])
(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(x15, p1)), (lx3, x15), (lx4, f1), (lx6, x22), (lx8, x22)]
s4f = substFromList [(lx1, x6), (lx2, pair(x3,x1))]
s1b_o_s4f = substFromListVFresh
[(lx1, x20), (lx2, pair(x13, p1)), (lx3, x13), (lx4, f1), (lx6, x20)]
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