summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--GeneratorTest.hs10
-rw-r--r--TermNetTest.hs25
-rw-r--r--writetest.hs43
3 files changed, 78 insertions, 0 deletions
diff --git a/GeneratorTest.hs b/GeneratorTest.hs
new file mode 100644
index 0000000..419e904
--- /dev/null
+++ b/GeneratorTest.hs
@@ -0,0 +1,10 @@
+import Library.Parse
+import Library.Generator
+import Library.Term
+import Library.TypeVar
+
+
+main = do
+ let s = substitutionGen ([],[])
+ let t = substitutionGen ( [(Name [] "tyvar", AType [] (TypeOp (Name [] "atype")))], [] )
+ output t
diff --git a/TermNetTest.hs b/TermNetTest.hs
new file mode 100644
index 0000000..6588a93
--- /dev/null
+++ b/TermNetTest.hs
@@ -0,0 +1,25 @@
+import Library.Theorem
+import Library.Term
+import qualified Library.TermNet as Net
+import Test.DataTypes
+import qualified Data.Set as Set
+import Data.List
+
+
+
+main = do
+ let thm1 = Theorem (Set.empty) stdConstTerm
+ thm2 = Theorem (Set.empty) (stdVarTerm "b")
+ thm3 = Theorem (Set.empty) (stdVarTerm "c")
+
+ (net1, matches1) = Net.addThm Net.empty thm1 0
+ (net2, matches2) = Net.addThm net1 thm2 1
+ (net3, matches3) = Net.addThm net2 thm3 2
+
+
+ putStrLn (show net3)
+ putStrLn ""
+ putStrLn (show matches3)
+ putStrLn (intercalate " " . Net.thmToTermString $ thm1)
+ putStrLn (intercalate " " . Net.thmToTermString $ thm2)
+ putStrLn (intercalate " " . Net.thmToTermString $ thm3)
diff --git a/writetest.hs b/writetest.hs
new file mode 100644
index 0000000..81df3d7
--- /dev/null
+++ b/writetest.hs
@@ -0,0 +1,43 @@
+import Library.WriteProof
+import Library.ProofGraph
+
+
+list = [-- create a var term, define a constant to it
+ "\"const\"","\"x\"","const","\"t1\"","typeOp","nil","opType","1","def","constTerm","0","def","defineConst",
+
+ -- hypothesis list for theorem
+ "nil",
+
+ -- equals name
+ "\"=\"","const",
+
+ -- equals type
+ "\"->\"","typeOp","1","ref","\"->\"","typeOp","1","ref","\"bool\"","typeOp","nil","opType","nil","cons","cons","opType",
+ "nil","cons","cons","opType",
+
+ -- equals term
+ "constTerm",
+
+ -- the constant
+ "\"const\"","const","1","remove","constTerm",
+
+ -- construct the equation of constant = variable
+ "appTerm",
+ "0","remove",
+ "appTerm",
+
+ "thm","pop"]
+
+graph = doGraphGen list
+
+fst3 :: (a,b,c) -> a
+fst3 (a,_,_) = a
+
+snd3 :: (a,b,c) -> b
+snd3 (_,b,_) = b
+
+thd3 :: (a,b,c) -> c
+thd3 (_,_,c) = c
+
+edgeCheck :: (Ord d) => (a,b,(c,d)) -> (e,f,(g,d)) -> Ordering
+edgeCheck = (\a b -> compare (snd . thd3 $ a) (snd . thd3 $ b))