32 files changed, 343 insertions, 0 deletions

diff --git a/test/absterm.art b/test/absterm.art
new file mode 100644
index 0000000..94446fc
--- /dev/null
+++ b/test/absterm.art
@@ -0,0 +1,12 @@
+"variablename"
+"variabletype"
+varType
+var
+"constname"
+const
+"consttype"
+typeOp
+nil
+opType
+constTerm
+absTerm
diff --git a/test/absthm.art b/test/absthm.art
new file mode 100644
index 0000000..359a4cd
--- /dev/null
+++ b/test/absthm.art
@@ -0,0 +1,14 @@
+"bool"
+"bool"
+varType
+var
+#varTerm
+"bool"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+refl
+absThm
diff --git a/test/appterm.art b/test/appterm.art
new file mode 100644
index 0000000..3d566c0
--- /dev/null
+++ b/test/appterm.art
@@ -0,0 +1,25 @@
+"f"
+const
+"->"
+typeOp
+"bool"
+typeOp
+nil
+opType
+1
+def
+1
+remove
+nil
+cons
+cons
+opType
+constTerm
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+appTerm
diff --git a/test/appthm.art b/test/appthm.art
new file mode 100644
index 0000000..7e54c8c
--- /dev/null
+++ b/test/appthm.art
@@ -0,0 +1,27 @@
+"f"
+const
+"->"
+typeOp
+"bool"
+typeOp
+nil
+opType
+1
+def
+1
+remove
+nil
+cons
+cons
+opType
+constTerm
+refl
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+refl
+appThm
diff --git a/test/assume.art b/test/assume.art
new file mode 100644
index 0000000..ef47474
--- /dev/null
+++ b/test/assume.art
@@ -0,0 +1,8 @@
+"bool"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+assume
diff --git a/test/axiom.art b/test/axiom.art
new file mode 100644
index 0000000..bcf79bf
--- /dev/null
+++ b/test/axiom.art
@@ -0,0 +1,9 @@
+nil
+"name"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+axiom
diff --git a/test/betaconv.art b/test/betaconv.art
new file mode 100644
index 0000000..f0d051c
--- /dev/null
+++ b/test/betaconv.art
@@ -0,0 +1,21 @@
+"x"
+"bool"
+typeOp
+nil
+opType
+1
+def
+var
+"c"
+const
+1
+ref
+constTerm
+absTerm
+"a"
+const
+1
+remove
+constTerm
+appTerm
+betaConv
diff --git a/test/cons.art b/test/cons.art
new file mode 100644
index 0000000..b2c48b9
--- /dev/null
+++ b/test/cons.art
@@ -0,0 +1,4 @@
+"bool"
+typeOp
+nil
+cons
diff --git a/test/const.art b/test/const.art
new file mode 100644
index 0000000..8a94755
--- /dev/null
+++ b/test/const.art
@@ -0,0 +1,2 @@
+"name"
+const
diff --git a/test/constterm.art b/test/constterm.art
new file mode 100644
index 0000000..ac94e2b
--- /dev/null
+++ b/test/constterm.art
@@ -0,0 +1,7 @@
+"bool"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
diff --git a/test/deductantisym.art b/test/deductantisym.art
new file mode 100644
index 0000000..80a6eea
--- /dev/null
+++ b/test/deductantisym.art
@@ -0,0 +1,13 @@
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+assume
+1
+def
+1
+remove
+deductAntisym
diff --git a/test/def.art b/test/def.art
new file mode 100644
index 0000000..18cad67
--- /dev/null
+++ b/test/def.art
@@ -0,0 +1,6 @@
+"bool"
+typeOp
+nil
+opType
+1
+def
diff --git a/test/defineconst.art b/test/defineconst.art
new file mode 100644
index 0000000..739f9c9
--- /dev/null
+++ b/test/defineconst.art
@@ -0,0 +1,9 @@
+"y"
+"x"
+const
+"bool"
+typeOp
+nil
+opType
+constTerm
+defineConst
diff --git a/test/definetypeop.art b/test/definetypeop.art
new file mode 100644
index 0000000..706bd3e
--- /dev/null
+++ b/test/definetypeop.art
@@ -0,0 +1,28 @@
+"n"
+"abs"
+"rep"
+"xtype"
+nil
+cons
+"x"
+"xtype"
+varType
+var
+"c"
+const
+"bool"
+typeOp
+nil
+opType
+1
+def
+constTerm
+absTerm
+"a"
+const
+1
+remove
+constTerm
+appTerm
+assume
+defineTypeOp
diff --git a/test/eqmp.art b/test/eqmp.art
new file mode 100644
index 0000000..b7c63c6
--- /dev/null
+++ b/test/eqmp.art
@@ -0,0 +1,37 @@
+"x"
+"bool"
+typeOp
+nil
+opType
+1
+def
+var
+"c"
+const
+1
+ref
+constTerm
+2
+def
+absTerm
+"a"
+const
+1
+ref
+constTerm
+3
+def
+appTerm
+refl
+"y"
+1
+remove
+var
+2
+remove
+absTerm
+3
+remove
+appTerm
+assume
+eqMp
diff --git a/test/name.art b/test/name.art
new file mode 100644
index 0000000..bb89c74
--- /dev/null
+++ b/test/name.art
@@ -0,0 +1 @@
+"bool"
diff --git a/test/name2.art b/test/name2.art
new file mode 100644
index 0000000..a439e52
--- /dev/null
+++ b/test/name2.art
@@ -0,0 +1 @@
+"->"
diff --git a/test/nil.art b/test/nil.art
new file mode 100644
index 0000000..607602c
--- /dev/null
+++ b/test/nil.art
@@ -0,0 +1 @@
+nil
diff --git a/test/null.art b/test/null.art
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/test/null.art
diff --git a/test/number.art b/test/number.art
new file mode 100644
index 0000000..f599e28
--- /dev/null
+++ b/test/number.art
@@ -0,0 +1 @@
+10
diff --git a/test/opType.art b/test/opType.art
new file mode 100644
index 0000000..237dbd6
--- /dev/null
+++ b/test/opType.art
@@ -0,0 +1,4 @@
+"name"
+typeOp
+nil
+opType
diff --git a/test/pop.art b/test/pop.art
new file mode 100644
index 0000000..e111fc2
--- /dev/null
+++ b/test/pop.art
@@ -0,0 +1,2 @@
+nil
+pop
diff --git a/test/ref.art b/test/ref.art
new file mode 100644
index 0000000..acd59ea
--- /dev/null
+++ b/test/ref.art
@@ -0,0 +1,8 @@
+"bool"
+typeOp
+nil
+opType
+1
+def
+1
+ref
diff --git a/test/refl.art b/test/refl.art
new file mode 100644
index 0000000..418ac89
--- /dev/null
+++ b/test/refl.art
@@ -0,0 +1,6 @@
+"bool"
+"bool"
+varType
+var
+varTerm
+refl
diff --git a/test/remove.art b/test/remove.art
new file mode 100644
index 0000000..88cadad
--- /dev/null
+++ b/test/remove.art
@@ -0,0 +1,8 @@
+"bool"
+typeOp
+nil
+opType
+1
+def
+1
+remove
diff --git a/test/subst.art b/test/subst.art
new file mode 100644
index 0000000..8fdc934
--- /dev/null
+++ b/test/subst.art
@@ -0,0 +1,47 @@
+"ytype"
+"xtype"
+varType
+nil
+cons
+cons
+nil
+cons
+"y"
+"xtype"
+varType
+var
+"z"
+"xtype"
+varType
+var
+varTerm
+nil
+cons
+cons
+nil
+cons
+nil
+cons
+cons
+"y"
+"ytype"
+varType
+var
+"c"
+const
+"bool"
+typeOp
+nil
+opType
+1
+def
+constTerm
+absTerm
+"a"
+const
+1
+remove
+constTerm
+appTerm
+assume
+subst
diff --git a/test/thm.art b/test/thm.art
new file mode 100644
index 0000000..4fee8b2
--- /dev/null
+++ b/test/thm.art
@@ -0,0 +1,23 @@
+"x"
+"bool"
+typeOp
+nil
+opType
+1
+def
+var
+varTerm
+assume
+"y"
+1
+ref
+var
+varTerm
+nil
+cons
+"z"
+1
+remove
+var
+varTerm
+thm
diff --git a/test/timer.sh b/test/timer.sh
new file mode 100644
index 0000000..2a1e7c3
--- /dev/null
+++ b/test/timer.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+for i in {1..1}
+do
+  $1 $2 > /dev/null
+done
diff --git a/test/typeop.art b/test/typeop.art
new file mode 100644
index 0000000..6b85dd7
--- /dev/null
+++ b/test/typeop.art
@@ -0,0 +1,2 @@
+"bool"
+typeOp
diff --git a/test/var.art b/test/var.art
new file mode 100644
index 0000000..4c915e7
--- /dev/null
+++ b/test/var.art
@@ -0,0 +1,4 @@
+"bool"
+"bool"
+varType
+var
diff --git a/test/varterm.art b/test/varterm.art
new file mode 100644
index 0000000..5bbc768
--- /dev/null
+++ b/test/varterm.art
@@ -0,0 +1,5 @@
+"bool"
+"bool"
+varType
+var
+varTerm
diff --git a/test/vartype.art b/test/vartype.art
new file mode 100644
index 0000000..72e6b3c
--- /dev/null
+++ b/test/vartype.art
@@ -0,0 +1,2 @@
+"bool"
+varType