module Term.UnitTests (tests) 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
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
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
testsSubst :: Test
testsSubst = TestLabel "Tests for Substitution" $
TestList
[
testEqual "a" (substFromListVFresh [(lx1, p1), (lx2, x6), (lx3,x6), (lx5, p1)])
(composeVFresh (substFromListVFresh [(lx5, p1)])
(substFromList [(lx1, x5), (lx2, x3)]))
, testEqual "b" s1b_o_s3f (composeVFresh s1b 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)]))
, 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
[(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
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
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))
]
where
tcn e1 e2 = testEqual ("norm "++ppLTerm e2) e1 (norm' e2 `runReader` hnd)
t1 = (p1 *: p2) *: (p3 *: p4)
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) ]
tests :: FilePath -> IO Test
tests maudePath = do
mhnd <- startMaude maudePath allMaudeSig
return $ TestList [ testsVariant mhnd
, tcompare mhnd
, testsSubs mhnd
, testsTerm
, testsSubst
, testsNorm mhnd
, testsUnify mhnd
, testsSimple mhnd
, testsMatching mhnd
]
allMaudeSig :: MaudeSig
allMaudeSig = mconcat
[ dhMaudeSig, xorMaudeSig, msetMaudeSig
, pairMaudeSig, symEncMaudeSig, asymEncMaudeSig, signatureMaudeSig, hashMaudeSig ]
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)]
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