[petanque] Run_tac: check if proof are finished

petanque/agent.ml

@@ -39,6 +39,12 @@ module R = struct
   type 'a t = ('a, Error.t) Result.t
 end
 
+module Run_result = struct
+  type t =
+    | Proof_finished of State.t
+    | Current_state of State.t
+end
+
 let init_coq ~debug =
   let load_module = Dynlink.loadfile in
   let load_plugin = Coq.Loader.plugin_handler None in
@@ -131,14 +137,22 @@ let parse ~loc tac st =
   let str = Coq.Parsing.Parsable.make ?loc str in
   Coq.Parsing.parse ~st str
 
+let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } =
+  List.for_all CList.is_empty [ goals; shelf; given_up ] && CList.is_empty stack
+
 let parse_and_execute_in ~token ~loc tac st =
   let open Coq.Protect.E.O in
   let* ast = parse ~token ~loc tac st in
   match ast with
-  | Some ast -> Fleche.Memo.Interp.eval ~token (st, ast)
-  (* On EOF we return the previous state, the command was the empty string or a
-     comment *)
-  | None -> Coq.Protect.E.ok st
+  | Some ast -> (
+    let open Coq.Protect.E.O in
+    let* st = Fleche.Memo.Interp.eval ~token (st, ast) in
+    let+ goals = Fleche.Info.Goals.goals ~token ~st in
+    match goals with
+    | None -> Run_result.Proof_finished st
+    | Some goals when proof_finished goals -> Run_result.Proof_finished st
+    | _ -> Run_result.Current_state st)
+  | None -> Coq.Protect.E.ok (Run_result.Current_state st)
 
 let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
   match r with
@@ -149,7 +163,7 @@ let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
     Error (Error.Anomaly (Pp.string_of_ppcmds msg))
   | { r = Completed (Ok r); feedback = _ } -> Ok r
 
-let run_tac ~token ~st ~tac : (Coq.State.t, Error.t) Result.t =
+let run_tac ~token ~st ~tac : (Run_result.t, Error.t) Result.t =
   (* Improve with thm? *)
   let loc = None in
   Coq.State.in_stateM ~token ~st ~f:(parse_and_execute_in ~token ~loc tac) st

petanque/agent.mli

@@ -36,6 +36,12 @@ module R : sig
   type 'a t = ('a, Error.t) Result.t
 end
 
+module Run_result : sig
+  type t =
+    | Proof_finished of State.t
+    | Current_state of State.t
+end
+
 (** I/O handling, by default, print to stderr *)
 
 (** [trace header extra message] *)
@@ -60,7 +66,7 @@ val start :
 
 (** [run_tac ~token ~st ~tac] tries to run [tac] over state [st] *)
 val run_tac :
-  token:Coq.Limits.Token.t -> st:State.t -> tac:string -> State.t R.t
+  token:Coq.Limits.Token.t -> st:State.t -> tac:string -> Run_result.t R.t
 
 (** [goals ~token ~st] return the list of goals for a given [st] *)
 val goals :

petanque/json_shell/protocol.ml

@@ -17,6 +17,10 @@ module R = struct
   type 'a t = [%import: 'a Petanque.Agent.R.t] [@@deriving yojson]
 end
 
+module Run_result = struct
+  type t = [%import: Petanque.Agent.Run_result.t] [@@deriving yojson]
+end
+
 (* We follow the methodology of SerAPI, we have a shell *)
 module Command = struct
   type t =
@@ -46,7 +50,7 @@ module Answer = struct
   type t =
     | Init of Env.t R.t
     | Start of State.t R.t
-    | Run_tac of State.t R.t
+    | Run_tac of Run_result.t R.t
     | Goals of Goals.t R.t
     | Premises of string list R.t
   [@@deriving to_yojson]

petanque/test/basic_api.ml

@@ -26,18 +26,26 @@ let start ~token =
   let* env = Agent.init ~token ~debug ~root in
   Agent.start ~token ~env ~uri ~thm:"rev_snoc_cons"
 
+let extract_st (st : Agent.Run_result.t) =
+  match st with
+  | Proof_finished st | Current_state st -> st
+
 let main () =
   let open Fleche.Compat.Result.O in
   let token = Coq.Limits.create_atomic () in
+  let r ~st ~tac =
+    let st = extract_st st in
+    Agent.run_tac ~token ~st ~tac
+  in
   let* st = start ~token in
   let* _premises = Agent.premises ~token ~st in
   let* st = Agent.run_tac ~token ~st ~tac:"induction l." in
-  let* st = Agent.run_tac ~token ~st ~tac:"-" in
-  let* st = Agent.run_tac ~token ~st ~tac:"reflexivity." in
-  let* st = Agent.run_tac ~token ~st ~tac:"-" in
-  let* st = Agent.run_tac ~token ~st ~tac:"now simpl; rewrite IHl." in
-  let* st = Agent.run_tac ~token ~st ~tac:"Qed." in
-  Agent.goals ~token ~st
+  let* st = r ~st ~tac:"-" in
+  let* st = r ~st ~tac:"reflexivity." in
+  let* st = r ~st ~tac:"-" in
+  let* st = r ~st ~tac:"now simpl; rewrite IHl." in
+  let* st = r ~st ~tac:"Qed." in
+  Agent.goals ~token ~st:(extract_st st)
 
 let check_no_goals = function
   | Error err ->