From 52ecb564fb6537ffab2a48d155f89b9ffada6e42 Mon Sep 17 00:00:00 2001
From: Marwan <marwan.azizi@ens-lyon.fr>
Date: Fri, 10 May 2024 18:40:33 +0200
Subject: [PATCH] =?UTF-8?q?apply=20g=C3=A9n=C3=A9ralis=C3=A9?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 proof.ml | 32 ++++++++++++++++++++++++--------
 1 file changed, 24 insertions(+), 8 deletions(-)

diff --git a/proof.ml b/proof.ml
index da14201..d5d7438 100644
--- a/proof.ml
+++ b/proof.ml
@@ -192,7 +192,27 @@ let tact_cut ((g, gs) : proof) (new_t : Types.ty) : proof =
     Some (new_h, new_t, cs), gs
 
 let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
-  let rec get_hyp = function
+  let rec is_implied (goal_ty : ty) (t : ty) : bool =
+    match t with
+    t when t = goal_ty -> true
+    | Arr (_, t2) -> is_implied goal_ty t2
+    | _ -> false
+  in
+  let rec generate_goals (goal_ty : ty) (t : ty) (cs : context)
+  (h' : hlam) (h : hlam) (gs : goal list) : proof =
+    match t with
+    Arr (t1, t2) when t2 = goal_ty ->
+      let new_h = Ref (ref Hole) in
+      fill h (HApp (h', new_h));
+      Some (new_h, t1, cs), gs
+    | Arr (t1, t2) ->
+      let new_h = Ref (ref Hole) in
+      let _ = fill h (HApp (h', new_h)) in
+      let gs = (new_h, t1, cs) :: gs in
+      generate_goals goal_ty t2 cs h' new_h gs
+    | _ -> failwith "cannot happen"
+  in
+  let rec get_hyp : context -> (hlam * ty) = function
     [] -> raise (TacticFailed "no such hypothesis in context")
     | (hyp_id', _, h', t') :: _ when hyp_id = hyp_id' -> (h', t')
     | _ :: cs -> get_hyp cs
@@ -201,13 +221,9 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
   None -> raise (TacticFailed "no current goal")
   | Some (h, goal_ty, cs) ->
     let h', t' = get_hyp cs in
-    match t' with
-    Arr (t1, t2) when t2 = goal_ty ->
-      let new_h = Ref (ref Hole) in
-      fill h (HApp (h', new_h));
-      Some (new_h, t1, cs), gs
-    | Arr _ -> (* failwith "wrong types" *) (g, gs)
-    | _ -> (* failwith "expected ->" *) (g, gs)
+    if is_implied goal_ty t'
+    then generate_goals goal_ty t' cs h' h gs
+    else raise (TacticFailed "not an implication")
 
 let tact_intros : proof -> proof =
   let rec push (p : proof) =