summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Test.hs42
-rw-r--r--Test/DataTypes.hs59
-rw-r--r--makefile6
3 files changed, 66 insertions, 41 deletions
diff --git a/Test.hs b/Test.hs
index 040bb87..835bd89 100644
--- a/Test.hs
+++ b/Test.hs
@@ -2,50 +2,12 @@ import Test.HUnit
import Library.Command
import Library.TypeVar
import Library.Term
-import LibraryTheorem
+import Library.Theorem
+import Test.DataTypes
import qualified Data.Set as Set
-stdName :: String -> Name
-stdName s = Name [] s
-
-stdType :: Type
-stdType = AType [] (TypeOp (stdName "atype"))
-
-stdConst :: Const
-stdConst = Const (stdName "const")
-
-stdConstTerm :: Term
-stdConstTerm = TConst stdConst stdType
-
-stdTypeVarName :: Name
-stdTypeVarName = stdName "typevar"
-
-altTypeVarName :: Name
-altTypeVarName = stdName "alttypevar"
-
-stdTypeVar :: Type
-stdTypeVar = TypeVar stdTypeVarName
-
-altTypeVar :: Type
-altTypeVar = TypeVar altTypeVarName
-
-stdVar :: String -> Var
-stdVar s = Var (stdName s) stdTypeVar
-
-stdVarTerm :: String -> Term
-stdVarTerm s = TVar (stdVar s)
-
-altVar :: String -> Var
-altVar s = Var (stdName s) altTypeVar
-
-altVarTerm :: String -> Term
-altVarTerm s = TVar (altVar s)
-
-
-
-
name1 = TestCase (assertEqual "for (name \"abc\")"
(Just (Name [] "abc"))
(name "\"abc\""))
diff --git a/Test/DataTypes.hs b/Test/DataTypes.hs
new file mode 100644
index 0000000..d0fbfde
--- /dev/null
+++ b/Test/DataTypes.hs
@@ -0,0 +1,59 @@
+module Test.DataTypes(
+ stdName,
+ stdType,
+ stdConst,
+ stdConstTerm,
+ stdTypeVarName,
+ altTypeVarName,
+ stdTypeVar,
+ altTypeVar,
+ stdVar,
+ stdVarTerm,
+ altVar,
+ altVarTerm
+ ) where
+
+
+
+import Library.TypeVar
+import Library.Term
+
+
+
+stdName :: String -> Name
+stdName s = Name [] s
+
+stdType :: Type
+stdType = AType [] (TypeOp (stdName "atype"))
+
+stdConst :: Const
+stdConst = Const (stdName "const")
+
+stdConstTerm :: Term
+stdConstTerm = TConst stdConst stdType
+
+stdTypeVarName :: Name
+stdTypeVarName = stdName "typevar"
+
+altTypeVarName :: Name
+altTypeVarName = stdName "alttypevar"
+
+stdTypeVar :: Type
+stdTypeVar = TypeVar stdTypeVarName
+
+altTypeVar :: Type
+altTypeVar = TypeVar altTypeVarName
+
+stdVar :: String -> Var
+stdVar s = Var (stdName s) stdTypeVar
+
+stdVarTerm :: String -> Term
+stdVarTerm s = TVar (stdVar s)
+
+altVar :: String -> Var
+altVar s = Var (stdName s) altTypeVar
+
+altVarTerm :: String -> Term
+altVarTerm s = TVar (altVar s)
+
+
diff --git a/makefile b/makefile
index 07ca71a..d04dd06 100644
--- a/makefile
+++ b/makefile
@@ -3,7 +3,7 @@ OUTPUTDIR = ./bin
-all: semantic syntactic proofgraph writeproof delete concat listthm
+all: semantic syntactic proofgraph writeproof delete concat listthm meaningsubst unittest
clean:
find . -name '*.hi' -delete
@@ -31,4 +31,8 @@ concat:
listthm:
ghc --make ./ListThm.hs -o ${OUTPUTDIR}/ListThm
+meaningsubst:
+ ghc --make ./MeaningSubst.hs -o ${OUTPUTDIR}/MeaningSubst
+unittest:
+ ghc --make ./Test.hs -o ${OUTPUTDIR}/UnitTest