From 5ecf82920f9983f941b93c2e5f2230c99a1f768f Mon Sep 17 00:00:00 2001
From: Marwan <marwan.azizi@ens-lyon.fr>
Date: Tue, 14 May 2024 11:41:10 +0200
Subject: [PATCH] =?UTF-8?q?d=C3=A9but=20de=20correction=20d'apply=20g?=
 =?UTF-8?q?=C3=A9n=C3=A9ralis=C3=A9?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 proof.ml | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

diff --git a/proof.ml b/proof.ml
index d5d7438..e832183 100644
--- a/proof.ml
+++ b/proof.ml
@@ -198,19 +198,22 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
     | 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
+  let rec generate_goals (goal_ty : ty) (impl_ty : ty) (impl_h : hlam)
+  (goal_h : hlam) (cs : context) (gs : goal list) : proof =
+    match impl_ty 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
+      let sub_h = Ref (ref Hole) in
+      let _ = fill goal_h (HApp (impl_h, sub_h)) in
+      Some (sub_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"
+      (* nouveau sous but *)
+      let sub_h = Ref (ref Hole) in (* preuve de t1 *)
+      let new_h = Ref (ref Hole) in (* suite de l'implication *)
+      let _ = fill impl_h (HApp (HApp (impl_h, sub_h), new_h)) in
+      let gs = (sub_h, t1, cs) :: gs in
+      generate_goals goal_ty t2 new_h goal_h cs gs
+    | _ -> failwith "impossible"
+      
   in
   let rec get_hyp : context -> (hlam * ty) = function
     [] -> raise (TacticFailed "no such hypothesis in context")
@@ -222,7 +225,7 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
   | Some (h, goal_ty, cs) ->
     let h', t' = get_hyp cs in
     if is_implied goal_ty t'
-    then generate_goals goal_ty t' cs h' h gs
+    then generate_goals goal_ty t' h' h cs gs
     else raise (TacticFailed "not an implication")
 
 let tact_intros : proof -> proof =