e doit typecheck dans exact e pour que la tactique réussisse

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;

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, _, _) ->
+  | 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' ->
+      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

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) ->