From 5f28463a37cc8a981b1ebda5ada4a8e62c7c06e4 Mon Sep 17 00:00:00 2001
From: Marwan <marwan.azizi@ens-lyon.fr>
Date: Mon, 6 May 2024 00:10:23 +0200
Subject: [PATCH] =?UTF-8?q?e=20doit=20typecheck=20dans=20exact=20e=20pour?=
 =?UTF-8?q?=20que=20la=20tactique=20r=C3=A9ussisse?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 affichage.ml |  6 ++++--
 proof.ml     | 43 +++++++++++++++++++++++++++++++------------
 typing.ml    |  2 +-
 3 files changed, 36 insertions(+), 15 deletions(-)

diff --git a/affichage.ml b/affichage.ml
index fb39603..c3df528 100644
--- a/affichage.ml
+++ b/affichage.ml
@@ -42,7 +42,9 @@ let print_expr e =
 let print_goal ((_, ty, c) : goal) : unit =
   let rec print_hyps (c : context) : unit = match c with
     [] -> ()
-    | (id, _, ty)::q -> print_string (id^" : "^(string_of_ty ty)^"\n"); print_hyps q
+    | (hyp_id, _, _, ty)::q ->
+      print_string (hyp_id^" : "^(string_of_ty ty)^"\n");
+      print_hyps q
   in 
   print_string "\027[1m";
   print_hyps c;
@@ -53,4 +55,4 @@ let affiche_val _ = print_string "TODO"
 
 let print_error (error_type : string) (details : string) =
   output_string stderr ("\027[1;31mError:\027[0m \027[34m"^error_type^"\027[0m "^details^"\n");
-  flush stderr
\ No newline at end of file
+  flush stderr
diff --git a/proof.ml b/proof.ml
index d47215f..ae9ceba 100644
--- a/proof.ml
+++ b/proof.ml
@@ -11,7 +11,7 @@ type hlam = (* hollow lam *)
   | Ref of hlam ref
   | Hole
 
-type context = (id * hlam * Types.ty) list
+type context = (id * id * hlam * Types.ty) list
 type goal = hlam * Types.ty * context
 type proof = goal option * goal list
 
@@ -35,7 +35,7 @@ let get_fresh_hyp () =
   let var_id = "x_" ^ n in
   (hyp_id, var_id)
 
-let proof_is_over ((g, _) : proof) : bool =
+let goal_is_over ((g, _) : proof) : bool =
   match g with
   None -> true
   | Some _ -> false
@@ -74,16 +74,25 @@ let rec lam_of_hlam : hlam -> lam = function
   | Hole -> raise (TacticFailed "can not translate unclosed terms")
 
 
+let typecheck (e : lam) (expected_t : Types.ty) (cs : context) : bool =
+  let gam_of_ctx : context -> Types.gam =
+    let f = fun (_, var_id, _, ty) -> (var_id, ty) in
+    List.map f
+  in
+  let g = gam_of_ctx cs in
+  try Typing.typecheck g e expected_t
+  with _ -> raise (TacticFailed "unable to type")
+
 let rec get_term_by_id (hyp : id) : context -> hlam option =
   function
   [] -> None
-  | (hyp', h, _) :: _ when hyp' = hyp -> Some h
+  | (hyp',_,  h, _) :: _ when hyp' = hyp -> Some h
   | _ :: cs -> get_term_by_id hyp cs
 
 let rec get_term_by_type (ty : Types.ty) : context -> hlam option =
   function
   [] -> None
-  | (_, h, ty') :: _ when ty' = ty -> Some h
+  | (_, _, h, ty') :: _ when ty' = ty -> Some h
   | _ :: cs -> get_term_by_type ty cs
 
 let next_goal (gs : goal list) : (goal option * goal list) =
@@ -94,18 +103,28 @@ let next_goal (gs : goal list) : (goal option * goal list) =
 let tact_exact_term ((g, gs) : proof) (e : lam) : proof =
   match g with
   None -> raise (TacticFailed "no current goal")
-  | Some (h, _, _) ->
-    fill h (hlam_of_lam e);
-    next_goal gs
+  | Some (h, expected_t, cs) ->
+    if typecheck e expected_t cs
+    then
+      begin
+      fill h (hlam_of_lam e);
+      next_goal gs
+      end
+    else raise (TacticFailed "type mismatch")
 
 let tact_exact_proof ((g, gs) : proof) (hyp : id) : proof =
   match g with
   None -> raise (TacticFailed "no current goal")
-  | Some (h, _, cs) ->
+  | Some (h, expected_t, cs) ->
     match get_term_by_id hyp cs with
     Some h' ->
-      fill h h';
-      next_goal gs
+      if typecheck (lam_of_hlam h') expected_t cs
+      then
+        begin
+        fill h h';
+        next_goal gs
+        end
+      else raise (TacticFailed "type mismatch")
     | None -> raise (TacticFailed "")
 
 let tact_assumption ((g, gs) : proof) : proof =
@@ -125,7 +144,7 @@ let tact_intro ((g, gs) : proof) : proof =
     match goal_ty with
     Arr (t1, t2) ->
       let (hyp_id, var_id) = get_fresh_hyp () in
-      let cs = (hyp_id, HVar var_id, t1) :: cs in
+      let cs = (hyp_id, var_id, HVar var_id, t1) :: cs in
       let new_h = Ref (ref Hole) in
       fill h (HFun ((var_id, t1), new_h));
       Some (new_h, t2, cs), gs
@@ -148,7 +167,7 @@ let tact_cut ((g, gs) : proof) (new_t : Types.ty) : proof =
 let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
   let rec get_hyp = function
     [] -> raise (TacticFailed "no such hypothesis in context")
-    | (hyp_id', h', t') :: _ when hyp_id = hyp_id' -> (h', t')
+    | (hyp_id', _, h', t') :: _ when hyp_id = hyp_id' -> (h', t')
     | _ :: cs -> get_hyp cs
   in
   match g with
diff --git a/typing.ml b/typing.ml
index 86c1d25..4a3cb86 100644
--- a/typing.ml
+++ b/typing.ml
@@ -1,7 +1,7 @@
 open Types
 open Lam
 
-let rec typecheck (g : gam) (e : lam) (expected_t : ty) =
+let rec typecheck (g : gam) (e : lam) (expected_t : ty) : bool =
   match e with
   Var x -> (List.assoc x g) = expected_t
   | Fun ((x, actual_t1), e) ->