From d40f4081c47a0047bc15f574e402003c63639910 Mon Sep 17 00:00:00 2001
From: augustin64 <me.git@augustin64.fr>
Date: Mon, 20 May 2024 10:57:55 +0200
Subject: [PATCH] Add bad 8pus files

---
 main.ml                           |  9 ++++++---
 tests.sh                          | 33 +++++++++++++++++++++++++------
 tests/8pus/bad/badtype_exact.8pus |  5 +++++
 tests/8pus/bad/no_apply.8pus      |  2 ++
 tests/8pus/bad/no_goal.8pus       |  3 +++
 tests/8pus/bad/no_intro.8pus      |  2 ++
 tests/8pus/bad/no_left_right.8pus |  8 ++++++++
 tests/8pus/bad/no_split.8pus      |  6 ++++++
 tests/8pus/bad/no_such_hyp.8pus   |  6 ++++++
 tests/8pus/bad/type_apply.8pus    |  3 +++
 10 files changed, 68 insertions(+), 9 deletions(-)
 create mode 100644 tests/8pus/bad/badtype_exact.8pus
 create mode 100644 tests/8pus/bad/no_apply.8pus
 create mode 100644 tests/8pus/bad/no_goal.8pus
 create mode 100644 tests/8pus/bad/no_intro.8pus
 create mode 100644 tests/8pus/bad/no_left_right.8pus
 create mode 100644 tests/8pus/bad/no_split.8pus
 create mode 100644 tests/8pus/bad/no_such_hyp.8pus
 create mode 100644 tests/8pus/bad/type_apply.8pus

diff --git a/main.ml b/main.ml
index 0421af8..cb5b6a0 100644
--- a/main.ml
+++ b/main.ml
@@ -5,6 +5,7 @@ open Types
 open Hlam
 open Lam
 
+exception InputError of string
 
 type entry =
   Simple of (unit -> instr)
@@ -18,12 +19,11 @@ module StringMap = Map.Make(String)
 let parse_lam t =
   match Parser.main Lexer.token t with
   | Lam l -> l
-  | Instr _ -> failwith "entry must be a lam"
-
+  | Instr _ -> raise (InputError "entry must be a lam")
 let parse_cmd t =
   match Parser.main Lexer.token t with
   | Instr is -> is
-  | Lam _ -> failwith "entry must be a cmd"
+  | Lam _ -> raise (InputError "entry must be an instruction")
 
 let show_beta_reduction e =
   let rec aux = function
@@ -171,6 +171,9 @@ let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list)
       | TacticFailed arg ->
         print_error "Tactic failed" arg;
         (cg, (g, gs))::sq |> interactive get_instr
+      | InputError arg ->
+        print_error "Invalid input" arg;
+        (cg, (g, gs))::sq |> interactive get_instr
       | End_of_file | Lexer.Eof ->
         print_string "Bye!\n";
         (g, gs)
diff --git a/tests.sh b/tests.sh
index b37093e..aea6f01 100755
--- a/tests.sh
+++ b/tests.sh
@@ -2,20 +2,41 @@
 
 make
 
-echo "=== Alpha-équivalence ==="
-for file in tests/alpha_equiv/*; do
+echo_title () {
+    echo -e "\033[0;34m$@\033[0m"
+}
+
+echo_title "=== Alpha-équivalence ==="
+for file in tests/alpha_equiv/*.lam; do
     echo "-- $file"
     ./pieuvre -alpha $file >/dev/null
 done
 
-echo "=== Bêta-réduction ==="
-for file in tests/lam/*; do
+echo_title "=== Bêta-réduction ==="
+for file in tests/lam/*.lam; do
     echo "-- $file"
     ./pieuvre -reduce $file >/dev/null
 done
 
-echo "=== Preuves ==="
-for file in tests/8pus/*; do
+echo_title "=== Preuves ==="
+for file in tests/8pus/*.8pus; do
     echo "-- $file"
     ./pieuvre $file >/dev/null
+done
+
+echo_title "-== Preuves avec erreurs ==-"
+for file in tests/8pus/bad/*.8pus; do
+    # On vérifie deux choses:
+    # - Un message d'erreur s'affiche bien
+    # - Le code de sortie est bien 0
+    echo "-- $file"
+    error=$(./pieuvre $file 2>&1 1>/dev/null)
+
+    retVal=$?
+    if [ $retVal -ne 0 ]; then
+        echo -e "\033[0;31mNon-0 exit code, see stderr:\033[0m"
+        echo $error
+    elif [[ $error == "" ]]; then
+        echo -e "\033[0;31mNo message in stderr\033[0m"
+    fi
 done
\ No newline at end of file
diff --git a/tests/8pus/bad/badtype_exact.8pus b/tests/8pus/bad/badtype_exact.8pus
new file mode 100644
index 0000000..a4271ce
--- /dev/null
+++ b/tests/8pus/bad/badtype_exact.8pus
@@ -0,0 +1,5 @@
+Goal A -> B -> A.
+intro.
+exact H1.
+exact H0.
+Qed.
\ No newline at end of file
diff --git a/tests/8pus/bad/no_apply.8pus b/tests/8pus/bad/no_apply.8pus
new file mode 100644
index 0000000..ccc4107
--- /dev/null
+++ b/tests/8pus/bad/no_apply.8pus
@@ -0,0 +1,2 @@
+Goal A -> (B -> A).
+apply H0.
\ No newline at end of file
diff --git a/tests/8pus/bad/no_goal.8pus b/tests/8pus/bad/no_goal.8pus
new file mode 100644
index 0000000..1a70539
--- /dev/null
+++ b/tests/8pus/bad/no_goal.8pus
@@ -0,0 +1,3 @@
+intro.
+left.
+right.
\ No newline at end of file
diff --git a/tests/8pus/bad/no_intro.8pus b/tests/8pus/bad/no_intro.8pus
new file mode 100644
index 0000000..05c5c6c
--- /dev/null
+++ b/tests/8pus/bad/no_intro.8pus
@@ -0,0 +1,2 @@
+Goal A /\ B.
+intro.
\ No newline at end of file
diff --git a/tests/8pus/bad/no_left_right.8pus b/tests/8pus/bad/no_left_right.8pus
new file mode 100644
index 0000000..336ebce
--- /dev/null
+++ b/tests/8pus/bad/no_left_right.8pus
@@ -0,0 +1,8 @@
+Goal A -> B -> (A /\ B).
+intros.
+left.
+right.
+split.
+    exact H0.
+    exact H1.
+Qed.
\ No newline at end of file
diff --git a/tests/8pus/bad/no_split.8pus b/tests/8pus/bad/no_split.8pus
new file mode 100644
index 0000000..0d90ebc
--- /dev/null
+++ b/tests/8pus/bad/no_split.8pus
@@ -0,0 +1,6 @@
+Goal A -> (A \/ B).
+intro.
+split.
+left.
+exact H0.
+Qed.
\ No newline at end of file
diff --git a/tests/8pus/bad/no_such_hyp.8pus b/tests/8pus/bad/no_such_hyp.8pus
new file mode 100644
index 0000000..932f345
--- /dev/null
+++ b/tests/8pus/bad/no_such_hyp.8pus
@@ -0,0 +1,6 @@
+Goal A -> B -> A.
+intros.
+    exact H3.
+    apply H5.
+exact H0.
+Qed.
\ No newline at end of file
diff --git a/tests/8pus/bad/type_apply.8pus b/tests/8pus/bad/type_apply.8pus
new file mode 100644
index 0000000..30152bd
--- /dev/null
+++ b/tests/8pus/bad/type_apply.8pus
@@ -0,0 +1,3 @@
+Goal (A -> B) -> A -> C.
+intros.
+apply H0.
\ No newline at end of file