From 5e13eb48b17a4a7440c3fc9de5d292b059eec16d Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Thu, 27 Sep 2012 00:14:22 +1000 Subject: The rest of the article files for testing specific commands --- Test/absterm.art | 9 ++++----- Test/absthm.art | 4 ++-- Test/appterm.art | 4 ++-- Test/appthm.art | 27 +++++++++++++++++++++++++++ Test/betaconv.art | 21 +++++++++++++++++++++ Test/deductantisym.art | 13 +++++++++++++ Test/defineconst.art | 9 +++++++++ Test/definetypeop.art | 28 ++++++++++++++++++++++++++++ Test/eqmp.art | 37 +++++++++++++++++++++++++++++++++++++ Test/null.art | 0 Test/subst.art | 47 +++++++++++++++++++++++++++++++++++++++++++++++ Test/thm.art | 23 +++++++++++++++++++++++ Test/timer.sh | 4 ++-- 13 files changed, 215 insertions(+), 11 deletions(-) create mode 100644 Test/appthm.art create mode 100644 Test/betaconv.art create mode 100644 Test/deductantisym.art create mode 100644 Test/defineconst.art create mode 100644 Test/definetypeop.art create mode 100644 Test/eqmp.art create mode 100644 Test/null.art create mode 100644 Test/subst.art create mode 100644 Test/thm.art diff --git a/Test/absterm.art b/Test/absterm.art index d68ddc6..94446fc 100644 --- a/Test/absterm.art +++ b/Test/absterm.art @@ -1,11 +1,10 @@ -"bool" -"bool" +"variablename" +"variabletype" varType var -varTerm -"bool" +"constname" const -"bool" +"consttype" typeOp nil opType diff --git a/Test/absthm.art b/Test/absthm.art index 6fd12ba..359a4cd 100644 --- a/Test/absthm.art +++ b/Test/absthm.art @@ -1,8 +1,8 @@ "bool" "bool" -var varType -varTerm +var +#varTerm "bool" const "bool" diff --git a/Test/appterm.art b/Test/appterm.art index 42f0da9..3d566c0 100644 --- a/Test/appterm.art +++ b/Test/appterm.art @@ -1,4 +1,4 @@ -"name" +"f" const "->" typeOp @@ -15,7 +15,7 @@ cons cons opType constTerm -"name" +"x" const "bool" typeOp 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/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/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/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/null.art b/Test/null.art new file mode 100644 index 0000000..e69de29 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 index 637b80a..c95aff5 100644 --- a/Test/timer.sh +++ b/Test/timer.sh @@ -1,6 +1,6 @@ #!/bin/bash -for i in (1..1000) +for i in {1..1000} do - $1 $2 + $1 $2 > /dev/null done -- cgit