Merge pull request #769 from ejgallego/petanque_pre

[petanque] Allow to instrument with extra commands before proof start

CHANGES.md

@@ -36,6 +36,9 @@
    @gbdrt, #766)
  - [petanque] Faster query for goals status after `run_tac`
    (@ejgallego, #768)
+ - [petanque] New parameter `pre_commands` to `start` which allows
+   instrumenting the goal before starting the proof (@ejgallego, Alex
+   Sanchez-Stern #769)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

petanque/agent.ml

@@ -109,7 +109,7 @@ let find_thm ~(doc : Fleche.Doc.t) ~thm =
   | Some node ->
     if pet_debug then Format.eprintf "@[[find_thm] Theorem found!@\n@]%!";
     (* let point = (range.start.line, range.start.character) in *)
-    Ok (Fleche.Doc.Node.state node)
+    Ok node
 
 let pp_diag fmt { Lang.Diagnostic.message; _ } =
   Format.fprintf fmt "%a" Pp.pp_with message
@@ -140,19 +140,6 @@ let init ~token ~debug ~root =
   in
   setup_workspace ~token ~init ~debug ~root
 
-let start ~token ~env ~uri ~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
@@ -175,6 +162,20 @@ let parse_and_execute_in ~token ~loc tac st =
     | _ -> Run_result.Current_state st)
   | None -> Coq.Protect.E.ok (Run_result.Current_state st)
 
+let execute_precommands ~token ~pre_commands ~(node : Fleche.Doc.Node.t) =
+  match (pre_commands, node.prev, node.ast) with
+  | Some pre_commands, Some prev, Some ast ->
+    let st = prev.state in
+    let open Coq.Protect.E.O in
+    let* res = parse_and_execute_in ~token ~loc:None pre_commands st in
+    let st =
+      match res with
+      | Run_result.Current_state st | Run_result.Proof_finished st -> st
+    in
+    (* We re-interpret the lemma statement *)
+    Fleche.Memo.Interp.eval ~token (st, ast.v)
+  | _, _, _ -> Coq.Protect.E.ok node.state
+
 let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
   match r with
   | { r = Interrupted; feedback = _ } -> Error Error.Interrupted
@@ -184,6 +185,21 @@ 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 start ~token ~env ~uri ?pre_commands ~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
+    let open Coq.Compat.Result.O in
+    let* node = find_thm ~doc ~thm in
+    execute_precommands ~token ~pre_commands ~node |> protect_to_result
+  | Error err ->
+    let msg = Format.asprintf "@[[read_raw] File not found %s@]" err in
+    Error (Error.Theorem_not_found msg)
+
 let run_tac ~token ~st ~tac : (_ Run_result.t, Error.t) Result.t =
   (* Improve with thm? *)
   let loc = None in

petanque/agent.mli

@@ -57,12 +57,18 @@ val message_ref : (lvl:Fleche.Io.Level.t -> message:string -> unit) ref
 val init :
   token:Coq.Limits.Token.t -> debug:bool -> root:Lang.LUri.File.t -> Env.t R.t
 
-(** [start uri thm] start a new proof for theorem [thm] in file [uri]. *)
+(** [start ~token ~env ~uri ~pre_commands ~thm] start a new proof for theorem
+    [thm] in file [uri] under [env]. [token] can be used to interrupt the
+    computation. Returns the proof state or error otherwise. [pre_commands] is a
+    string of dot-separated Coq commands that will be executed before the proof
+    starts. *)
 val start :
      token:Coq.Limits.Token.t
   -> env:Env.t
   -> uri:Lang.LUri.File.t
+  -> ?pre_commands:string
   -> thm:string
+  -> unit
   -> State.t R.t
 
 (** [run_tac ~token ~st ~tac] tries to run [tac] over state [st] *)

petanque/json_shell/protocol.ml

@@ -73,6 +73,7 @@ module Start = struct
     type t =
       { env : int
       ; uri : Lsp.JLang.LUri.File.t
+      ; pre_commands : string option [@default None]
       ; thm : string
       }
     [@@deriving yojson]
@@ -87,6 +88,7 @@ module Start = struct
       type t =
         { env : Env.t
         ; uri : Lsp.JLang.LUri.File.t
+        ; pre_commands : string option [@default None]
         ; thm : string
         }
       [@@deriving yojson]
@@ -96,8 +98,8 @@ module Start = struct
       type t = State.t [@@deriving yojson]
     end
 
-    let handler ~token { Params.env; uri; thm } =
-      Agent.start ~token ~env ~uri ~thm
+    let handler ~token { Params.env; uri; pre_commands; thm } =
+      Agent.start ~token ~env ~uri ?pre_commands ~thm ()
   end
 end
 

petanque/test/basic_api.ml

@@ -26,7 +26,7 @@ let start ~token =
   (* Twice to test for #766 *)
   let* _env = Agent.init ~token ~debug ~root in
   let* env = Agent.init ~token ~debug ~root in
-  Agent.start ~token ~env ~uri ~thm:"rev_snoc_cons"
+  Agent.start ~token ~env ~uri ~thm:"rev_snoc_cons" ()
 
 let extract_st (st : _ Agent.Run_result.t) =
   match st with

petanque/test/json_api.ml

@@ -55,7 +55,7 @@ let run (ic, oc) =
   (* Will this work on Windows? *)
   let root, uri = prepare_paths () in
   let* env = S.init { debug; root } in
-  let* st = S.start { env; uri; thm = "rev_snoc_cons" } in
+  let* st = S.start { env; uri; pre_commands = None; thm = "rev_snoc_cons" } in
   let* premises = S.premises { st } in
   (if print_premises then
      Format.(eprintf "@[%a@]@\n%!" (pp_print_list pp_premise) premises));

petanque/test/json_api_failure.ml

@@ -33,7 +33,7 @@ let run (ic, oc) =
   (* Will this work on Windows? *)
   let root, uri = prepare_paths () in
   let* env = S.init { debug; root } in
-  let* st = S.start { env; uri; thm = "rev_snoc_cons" } in
+  let* st = S.start { env; uri; pre_commands = None; thm = "rev_snoc_cons" } in
   let* _premises = S.premises { st } in
   let* st = S.run_tac { st; tac = "induction l." } in
   let* st = r ~st ~tac:"-" in