Misc test files

1 files changed, 43 insertions, 0 deletions

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))