tactique try et intro

proof.ml

@@ -1,6 +1,8 @@
 open Lam
 open Types
 
+exception TacticFailed
+
 type hlam = (* hollow lam *)
   HFun of (id * Types.ty) * hlam
   | HApp of hlam * hlam
@@ -77,13 +79,15 @@ let next_goal (gs : goal list) : (goal option * goal list) =
   [] -> None, []
   | g :: gs -> Some g, gs
 
-let tact_exact ((g, gs) : proof) (e : lam) : proof =
+let tact_exact_term ((g, gs) : proof) (e : lam) : proof =
   match g with
   None -> failwith "no current goal"
   | Some (h, _, _) ->
     fill h (hlam_of_lam e);
     next_goal gs
 
+let tact_exact_proof ((g, gs) : proof) (h : id) : proof =
+
 let tact_assumption ((g, gs) : proof) : proof =
   match g with
   None -> failwith "no current goal"
@@ -105,7 +109,8 @@ let tact_intro ((g, gs) : proof) : proof =
       let new_h = Ref (ref Hole) in
       fill h (HFun ((var_id, t1), new_h));
       Some (new_h, t2, cs), gs
-    | _ -> (* failwith "expected function" *) (g, gs)
+    | _ -> (* failwith "expected function" *) (* (g, gs) *)
+            raise TacticFailed
 
 let tact_cut ((g, gs) : proof) (new_t : Types.ty) : proof =
   match g with
@@ -137,3 +142,21 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
       Some (new_h, t1, cs), gs
     | Arr _ -> (* failwith "wrong types" *) (g, gs)
     | _ -> (* failwith "expected ->" *) (g, gs)
+
+let tact_intros : proof -> proof =
+  let rec push (p : proof) =
+    try
+      let p = tact_intro p in
+      push p
+    with TacticFailed -> p
+  in push
+
+let tact_try (p : proof) (t : tactic) : proof =
+  try
+  match t with
+  Exact e -> tact_exact p e
+  | Intro -> tact_intro p
+  | Assumption -> tact_assumption p
+  | Cut t -> tact_cut p t
+  | Apply h -> tact_apply p e
+  with TacticFailed -> p