Merge pull request #733 from ejgallego/petanque_tweaks

[petanque] Several tweaks from pet-server PR

petanque/agent.ml

@@ -47,6 +47,12 @@ module R = struct
   type 'a t = ('a, Error.t) Result.t
 end
 
+module Run_result = struct
+  type 'a t =
+    | Proof_finished of 'a
+    | Current_state of 'a
+end
+
 let init_coq ~debug =
   let load_module = Dynlink.loadfile in
   let load_plugin = Coq.Loader.plugin_handler None in
@@ -82,7 +88,8 @@ let io =
 
 let read_raw ~uri =
   let file = Lang.LUri.File.to_string_file uri in
-  Fleche.Compat.Ocaml_414.In_channel.(with_open_text file input_all)
+  try Ok Fleche.Compat.Ocaml_414.In_channel.(with_open_text file input_all)
+  with Sys_error err -> Error err
 
 let find_thm ~(doc : Fleche.Doc.t) ~thm =
   let { Fleche.Doc.toc; _ } = doc in
@@ -113,27 +120,39 @@ let init ~token ~debug ~root =
   |> Result.map_error (fun msg -> Error.Coq msg)
 
 let start ~token ~env ~uri ~thm =
-  let raw = read_raw ~uri in
-  (* Format.eprintf "raw: @[%s@]%!" raw; *)
-  let doc = Fleche.Doc.create ~token ~env ~uri ~version:0 ~raw in
-  print_diags doc;
-  let target = Fleche.Doc.Target.End in
-  let doc = Fleche.Doc.check ~io ~token ~target ~doc () in
-  find_thm ~doc ~thm
+  match read_raw ~uri with
+  | Ok raw ->
+    (* Format.eprintf "raw: @[%s@]%!" raw; *)
+    let doc = Fleche.Doc.create ~token ~env ~uri ~version:0 ~raw in
+    print_diags doc;
+    let target = Fleche.Doc.Target.End in
+    let doc = Fleche.Doc.check ~io ~token ~target ~doc () in
+    find_thm ~doc ~thm
+  | Error err ->
+    let msg = Format.asprintf "@[[read_raw] File not found %s@]" err in
+    Error (Error.Theorem_not_found msg)
 
 let parse ~loc tac st =
   let str = Gramlib.Stream.of_string tac in
   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
@@ -144,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

@@ -37,6 +37,12 @@ module R : sig
   type 'a t = ('a, Error.t) Result.t
 end
 
+module Run_result : sig
+  type 'a t =
+    | Proof_finished of 'a
+    | Current_state of 'a
+end
+
 (** I/O handling, by default, print to stderr *)
 
 (** [trace header extra message] *)
@@ -61,7 +67,10 @@ 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
+  -> State.t Run_result.t R.t
 
 (** [goals ~token ~st] return the list of goals for a given [st] *)
 val goals :

petanque/json_shell/client.ml

@@ -48,22 +48,22 @@ let get_id () =
   !id_counter
 
 module Wrap (R : Protocol.Request.S) (C : Chans) : sig
-  val call : R.Params_.t -> (R.Response_.t, string) Result.t
+  val call : R.Params.t -> (R.Response.t, string) Result.t
 end = struct
   let trace = C.trace
   let message = C.message
 
   let call params =
     let id = get_id () in
     let method_ = R.method_ in
-    let params = Yojson.Safe.Util.to_assoc (R.Params_.to_yojson params) in
+    let params = Yojson.Safe.Util.to_assoc (R.Params.to_yojson params) in
     let request =
       Lsp.Base.Request.(make ~id ~method_ ~params () |> to_yojson)
     in
     let () = Lsp.Io.send_json C.oc request in
     read_response ~trace ~message C.ic |> fun r ->
     Result.bind r (function
-      | Ok { id = _; result } -> R.Response_.of_yojson result
+      | Ok { id = _; result } -> R.Response.of_yojson result
       | Error { id = _; code = _; message; data = _ } -> Error message)
 end
 

petanque/json_shell/client.mli

@@ -8,9 +8,9 @@ end
 open Protocol
 
 module S (C : Chans) : sig
-  val init : Init.Params_.t -> (Init.Response_.t, string) result
-  val start : Start.Params_.t -> (Start.Response_.t, string) result
-  val run_tac : RunTac.Params_.t -> (RunTac.Response_.t, string) result
-  val goals : Goals.Params_.t -> (Goals.Response_.t, string) result
-  val premises : Premises.Params_.t -> (Premises.Response_.t, string) result
+  val init : Init.Params.t -> (Init.Response.t, string) result
+  val start : Start.Params.t -> (Start.Response.t, string) result
+  val run_tac : RunTac.Params.t -> (RunTac.Response.t, string) result
+  val goals : Goals.Params.t -> (Goals.Response.t, string) result
+  val premises : Premises.Params.t -> (Premises.Response.t, string) result
 end

petanque/json_shell/interp.ml

@@ -2,11 +2,11 @@ open Protocol
 module A = Petanque.Agent
 
 let do_request ~token (module R : Request.S) ~id ~params =
-  match R.Params.of_yojson (`Assoc params) with
+  match R.Handler.Params.of_yojson (`Assoc params) with
   | Ok params -> (
-    match R.handler ~token params with
+    match R.Handler.handler ~token params with
     | Ok result ->
-      let result = R.Response.to_yojson result in
+      let result = R.Handler.Response.to_yojson result in
       Lsp.Base.Response.mk_ok ~id ~result
     | Error err ->
       let message = A.Error.to_string err in

petanque/json_shell/jAgent.ml

@@ -22,6 +22,10 @@ module Error = struct
   type t = [%import: Petanque.Agent.Error.t] [@@deriving yojson]
 end
 
+module Run_result = struct
+  type 'a t = [%import: 'a Petanque.Agent.Run_result.t] [@@deriving yojson]
+end
+
 module R = struct
   type 'a t = [%import: 'a Petanque.Agent.R.t] [@@deriving yojson]
 end