diff options
| -rw-r--r-- | Test.hs | 42 | ||||
| -rw-r--r-- | Test/DataTypes.hs | 59 | ||||
| -rw-r--r-- | makefile | 6 |
3 files changed, 66 insertions, 41 deletions
@@ -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) + + @@ -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 |