diff options
| -rw-r--r-- | Test.hs | 113 |
1 files changed, 113 insertions, 0 deletions
@@ -0,0 +1,113 @@ +import Test.HUnit +import Command +import TypeVar +import Term +import Theorem +import qualified Data.Set as Set + + + +stdName :: String -> Name +stdName s = Name [] s + +stdConst :: Const +stdConst = Const (stdName "const") + +stdTypeVar :: Type +stdTypeVar = TypeVar (stdName "typevar") + +stdVar :: String -> Var +stdVar s = Var (stdName s) stdTypeVar + +stdVarTerm :: String -> Term +stdVarTerm s = TVar (stdVar s) + +altVarTerm :: String -> Term +altVarTerm s = TVar (Var (stdName s) (TypeVar (stdName "alttypevar"))) + + + + +name1 = TestCase (assertEqual "for (name \"abc\")" + (Just (Name [] "abc")) + (name "\"abc\"")) + +name2 = TestCase (assertEqual "for (name \"first.second.third\")" + (Just (Name ["first","second"] "third")) + (name "\"first.second.third\"")) + +name3 = TestCase (assertEqual "for (name \"firs\\t.se\\cond.\\t\\h\\ird\")" + (Just (Name ["first","second"] "third")) + (name "\"firs\\t.se\\cond.\\t\\h\\ird\"")) + +name4 = TestCase (assertEqual "for (name abc)" Nothing (name "abc")) + + + +number1 = TestCase (assertEqual "for (number \"90\")" (Just 90) (number "90")) +number2 = TestCase (assertEqual "for (number \"0\")" (Just 0) (number "0")) +number3 = TestCase (assertEqual "for (number \"-1\")" (Just (-1)) (number "-1")) +number4 = TestCase (assertEqual "for (number \"-0\")" Nothing (number "-0")) +number5 = TestCase (assertEqual "for (number \"1.2\")" Nothing (number "1.2")) + + + +assume1 = TestCase (assertEqual "for (assume (TConst ...)" + (Just (Theorem (Set.singleton (TConst stdConst typeBool)) + (TConst stdConst typeBool))) + (assume (TConst stdConst typeBool))) + +assume2 = TestCase (assertEqual "for (assume (TConst ...) --with wrong type" + Nothing + (assume (TConst stdConst stdTypeVar))) + + + +axiom1 = TestCase (assertEqual "for (axiom (TConst ...) [])" + (Just (Theorem Set.empty (TConst stdConst stdTypeVar))) + (axiom (TConst stdConst stdTypeVar) [])) + +axiom2 = TestCase (assertEqual "for (axiom (TConst ...) [term1, term2] --term1 has wrong type" + Nothing + (axiom (TConst stdConst stdTypeVar) + [(TConst stdConst stdTypeVar),(TConst stdConst typeBool)])) + + + +alphaEquiv1 = TestCase (assertEqual "for ((\\xy -> x) `alphaEquiv` (\\yx -> x))" + False + (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x"))) + (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "x"))))) + +alphaEquiv2 = TestCase (assertEqual "for ((\\xy -> x) `alphaEquiv` (\\xy -> x))" + True + (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x"))) + (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x"))))) + +alphaEquiv3 = TestCase (assertEqual "for ((\\xyx -> x) `alphaEquiv` (\\yxx -> x))" + True + (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "x")))) + (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "x") (stdVarTerm "x")))))) + +alphaEquiv4 = TestCase (assertEqual "for ((\\xyz -> y) `alphaEquiv` (\\zyx -> y))" + True + (alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "z") (stdVarTerm "y")))) + (TAbs (stdVarTerm "z") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "y")))))) + +alphaEquiv5 = TestCase (assertEqual "for ((\\x -> x) `alphaEquiv` (\\x -> x)) --x of lhs is different type to x of rhs" + False + (alphaEquiv (TAbs (stdVarTerm "x") (stdVarTerm "x")) + (TAbs (altVarTerm "x") (altVarTerm "x")))) + +alphaEquiv6 = TestCase (assertEqual "for ((TAbs ...) `alphaEquiv` (TConst ...))" + False + (alphaEquiv (TAbs (stdVarTerm "x") (stdVarTerm "x")) + (TConst stdConst typeBool))) + +main = + runTestTT $ TestList [name1,name2,name3,name4, + number1,number2,number3,number4,number5, + assume1,assume2, + axiom1,axiom2, + alphaEquiv1,alphaEquiv2,alphaEquiv3,alphaEquiv4,alphaEquiv5,alphaEquiv6] + |