From fc846d2233622f9087c6b7e15a7903cf299dc361 Mon Sep 17 00:00:00 2001
From: augustin64 <me.git@augustin64.fr>
Date: Wed, 1 May 2024 10:44:36 +0200
Subject: [PATCH] Add tactic intros

---
 lexer.mll  |  1 +
 main.ml    | 23 ++++++-----------------
 parser.mly |  3 ++-
 proof.ml   |  9 +++++++--
 4 files changed, 16 insertions(+), 20 deletions(-)

diff --git a/lexer.mll b/lexer.mll
index 36ad565..65ea1ee 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -31,6 +31,7 @@ rule token = parse
   | "Goal"          { GOAL }
   | "exact"         { EXACT }
   | "assumption"    { ASSUMPTION }
+  | "intros"        { INTROS }
   | "intro"         { INTRO }
   | "cut"           { CUT }
   | "apply"         { APPLY }
diff --git a/main.ml b/main.ml
index 4ecec9b..f519bf7 100644
--- a/main.ml
+++ b/main.ml
@@ -50,28 +50,14 @@ let rec interactive ((g, gs) : proof) : proof =
     in
 
     let _ = match g with
-    None -> print_string "No more goals.\n"
-    | Some g' -> print_goal g'
+    None -> print_string "\nNo more goals.\n"
+    | Some g' -> print_newline (); print_goal g'
     in
 
     try
       match parse_cmd (Lexing.from_string ((read_line ())^"\n")) with
       Goal ty -> fresh_proof ty |> interactive
-      | Tact t ->
-        begin match t with
-          Exact_term e ->
-            tact_exact_term (g, gs) e |> interactive
-          | Exact_proof s ->
-              tact_exact_proof (g, gs) s |> interactive
-          | Assumption ->
-            tact_assumption (g, gs) |> interactive
-          | Intro ->
-            tact_intro (g, gs) |> interactive
-          | Cut ty ->
-            tact_cut (g, gs) ty |> interactive
-          | Apply id ->
-            tact_apply (g, gs) id |> interactive
-        end
+      | Tact t -> apply_tactic (g, gs) t |> interactive
     with
       Parser.Error ->
         print_string "Invalid input.\n";
@@ -79,6 +65,9 @@ let rec interactive ((g, gs) : proof) : proof =
       | End_of_file ->
         print_string "Bye!\n";
         (g, gs)
+      | TacticFailed ->
+        print_string "Tactic failed.\n";
+        interactive (g, gs)
   end
 
 let interpret e =
diff --git a/parser.mly b/parser.mly
index c44037d..de6e43c 100644
--- a/parser.mly
+++ b/parser.mly
@@ -13,7 +13,7 @@ open Parser_entry
 %token <string> VARID
 %token <string> TYID
 
-%token GOAL EXACT ASSUMPTION INTRO CUT APPLY
+%token GOAL EXACT ASSUMPTION INTRO INTROS CUT APPLY
 
 %token EOL
 
@@ -36,6 +36,7 @@ command:
   | EXACT e=expression    { Tact (Exact_term e) }
   | EXACT s=TYID          { Tact (Exact_proof s) }
   | ASSUMPTION            { Tact (Assumption) }
+  | INTROS                { Tact (Intros) }
   | INTRO                 { Tact (Intro) }
   | CUT t=ty              { Tact (Cut t) }
   | APPLY s=TYID          { Tact (Apply s) }
diff --git a/proof.ml b/proof.ml
index 07115d0..61bf00e 100644
--- a/proof.ml
+++ b/proof.ml
@@ -19,6 +19,7 @@ type tactic =
   Exact_term of lam
   | Exact_proof of id
   | Assumption
+  | Intros
   | Intro
   | Cut of ty
   | Apply of id
@@ -167,13 +168,17 @@ let tact_intros : proof -> proof =
     with TacticFailed -> p
   in push
 
-let tact_try (p : proof) (t : tactic) : proof =
-  try
+let apply_tactic (p : proof) (t : tactic) : proof =
   match t with
   Exact_term e -> tact_exact_term p e
   | Exact_proof hyp -> tact_exact_proof p hyp
+  | Intros -> tact_intros p
   | Intro -> tact_intro p
   | Assumption -> tact_assumption p
   | Cut t -> tact_cut p t
   | Apply h -> tact_apply p h
+
+
+let tact_try (p : proof) (t : tactic) : proof =
+  try apply_tactic p t
   with TacticFailed -> p