summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Test.hs113
1 files changed, 113 insertions, 0 deletions
diff --git a/Test.hs b/Test.hs
new file mode 100644
index 0000000..aaa8636
--- /dev/null
+++ b/Test.hs
@@ -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]
+