diff --git a/tests.sh b/tests.sh new file mode 100755 index 0000000..b37093e --- /dev/null +++ b/tests.sh @@ -0,0 +1,21 @@ +#!/bin/bash + +make + +echo "=== Alpha-équivalence ===" +for file in tests/alpha_equiv/*; do + echo "-- $file" + ./pieuvre -alpha $file >/dev/null +done + +echo "=== Bêta-réduction ===" +for file in tests/lam/*; do + echo "-- $file" + ./pieuvre -reduce $file >/dev/null +done + +echo "=== Preuves ===" +for file in tests/8pus/*; do + echo "-- $file" + ./pieuvre $file >/dev/null +done \ No newline at end of file diff --git a/tests/and.8pus b/tests/8pus/and.8pus similarity index 100% rename from tests/and.8pus rename to tests/8pus/and.8pus diff --git a/tests/8pus/apply.8pus b/tests/8pus/apply.8pus new file mode 100644 index 0000000..6145a6c --- /dev/null +++ b/tests/8pus/apply.8pus @@ -0,0 +1,6 @@ +Goal (A -> B -> C) -> A -> B -> C. +intros. +apply H0. + exact H2. + exact H1. +Qed. diff --git a/tests/exact.8pus b/tests/8pus/exact.8pus similarity index 100% rename from tests/exact.8pus rename to tests/8pus/exact.8pus diff --git a/tests/or.8pus b/tests/8pus/or.8pus similarity index 100% rename from tests/or.8pus rename to tests/8pus/or.8pus diff --git a/tests/arrow_types.lam b/tests/lam/arrow_types.lam similarity index 100% rename from tests/arrow_types.lam rename to tests/lam/arrow_types.lam diff --git a/tests/basic.lam b/tests/lam/basic.lam similarity index 100% rename from tests/basic.lam rename to tests/lam/basic.lam diff --git a/tests/betared1.lam b/tests/lam/betared1.lam similarity index 100% rename from tests/betared1.lam rename to tests/lam/betared1.lam diff --git a/tests/betared2.lam b/tests/lam/betared2.lam similarity index 100% rename from tests/betared2.lam rename to tests/lam/betared2.lam diff --git a/tests/betared_rename.lam b/tests/lam/betared_rename.lam similarity index 100% rename from tests/betared_rename.lam rename to tests/lam/betared_rename.lam diff --git a/tests/exfalso1.lam b/tests/lam/exfalso1.lam similarity index 100% rename from tests/exfalso1.lam rename to tests/lam/exfalso1.lam diff --git a/tests/exfalso2.lam b/tests/lam/exfalso2.lam similarity index 100% rename from tests/exfalso2.lam rename to tests/lam/exfalso2.lam diff --git a/tests/exfalso3.lam b/tests/lam/exfalso3.lam similarity index 100% rename from tests/exfalso3.lam rename to tests/lam/exfalso3.lam diff --git a/tests/free_or_not.lam b/tests/lam/free_or_not.lam similarity index 100% rename from tests/free_or_not.lam rename to tests/lam/free_or_not.lam diff --git a/tests/id_function.lam b/tests/lam/id_function.lam similarity index 100% rename from tests/id_function.lam rename to tests/lam/id_function.lam diff --git a/tests/neg.lam b/tests/lam/neg.lam similarity index 100% rename from tests/neg.lam rename to tests/lam/neg.lam diff --git a/tests/nested_arrow.lam b/tests/lam/nested_arrow.lam similarity index 100% rename from tests/nested_arrow.lam rename to tests/lam/nested_arrow.lam diff --git a/tests/nested_function.lam b/tests/lam/nested_function.lam similarity index 100% rename from tests/nested_function.lam rename to tests/lam/nested_function.lam diff --git a/tests/one.lam b/tests/lam/one.lam similarity index 100% rename from tests/one.lam rename to tests/lam/one.lam diff --git a/tests/three.lam b/tests/lam/three.lam similarity index 100% rename from tests/three.lam rename to tests/lam/three.lam diff --git a/tests/zero.lam b/tests/lam/zero.lam similarity index 100% rename from tests/zero.lam rename to tests/lam/zero.lam