From 5af07fff8de0864e905b07cc3ac45f844ccb54f9 Mon Sep 17 00:00:00 2001
From: Adrien Vannson <adrien.vannson@protonmail.com>
Date: Tue, 10 May 2022 11:11:03 +0200
Subject: [PATCH] Apply

---
 lexer.mll  |  1 +
 main.ml    | 13 +++++++++++++
 parser.mly |  3 ++-
 tactic.ml  |  3 ++-
 4 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/lexer.mll b/lexer.mll
index e1d8c5c..f6f533a 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -18,5 +18,6 @@ and token_tactic = parse
   | eof                         { EOF }
   | "intro"                     { INTRO }
   | "assumption"                { ASSUMPTION }
+  | "apply"                     { APPLY }
   | ['a'-'z']+['0'-'9']* as s   { VAR_NAME s }
   | '.'                         { DOT }
diff --git a/main.ml b/main.ml
index 4240964..323d2e8 100644
--- a/main.ml
+++ b/main.ml
@@ -119,6 +119,19 @@ while !subgoals <> [] do
             in
             explore hyps
         )
+      | Apply var -> (
+            let rec explore = function
+              | (var_hyp, TImpl (t1, t2)) :: _ when var_hyp = var && t2 = ty -> (
+                    subgoals := (t1, hyps) :: !subgoals;
+                    fill_holes := function
+                      | hole :: holes -> f ((LApp (LVar var_hyp, hole)) :: holes)
+                      | [] -> fail ()
+                )
+              | [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable")
+              | _ :: hyps -> explore hyps
+            in
+            explore hyps;
+        )
 done;
 
 Printf.printf "Final proof :\n%s\n" (string_of_lam (!fill_holes []));;
diff --git a/parser.mly b/parser.mly
index 84d2a16..7d52621 100644
--- a/parser.mly
+++ b/parser.mly
@@ -10,7 +10,7 @@
 %token <string> VAR_NAME
 %token <string> TYPE_NAME
 
-%token DOT INTRO ASSUMPTION
+%token DOT INTRO ASSUMPTION APPLY
 
 /* L'ordre de définition définit la priorité */
 %right RARROW
@@ -39,3 +39,4 @@ main_tactic:
 tactic:
   | INTRO VAR_NAME DOT                    { Intro $2 }
   | ASSUMPTION DOT                        { Assumption }
+  | APPLY VAR_NAME DOT                    { Apply $2 }
diff --git a/tactic.ml b/tactic.ml
index b5b76c9..2f9dbfb 100644
--- a/tactic.ml
+++ b/tactic.ml
@@ -2,4 +2,5 @@ open Structs;;
 
 type tactic =
   | Intro of var_lambda
-  | Assumption;;
+  | Assumption
+  | Apply of var_lambda;;