Merge pull request #780 from ejgallego/run_memo

[petanque] Allow memoization control on `petanque/run`

CHANGES.md

@@ -54,6 +54,8 @@
    `Qed` time (@ejgallego, #773)
  - [fleche] Support meta-command `Abort All` (@ejgallego, #774, fixes
    #550)
+ - [petanque] Allow memoization control on `petanque/run` via a new
+   parameter `memo` (@ejgallego, #780)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

petanque/agent.ml

@@ -69,19 +69,25 @@ let parse ~loc tac st =
   let str = Coq.Parsing.Parsable.make ?loc str in
   Coq.Parsing.parse ~st str
 
-let parse_and_execute_in ~token ~loc tac st =
+(* Adaptor, should be supported in memo directly *)
+let eval_no_memo ~token (st, cmd) =
+  Coq.Interp.interp ~token ~intern:Vernacinterp.fs_intern ~st cmd
+
+let parse_and_execute_in ~token ~loc ~memo tac st =
+  (* To improve in memo *)
+  let eval = if memo then Fleche.Memo.Interp.eval else eval_no_memo in
   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)
+  | Some ast -> eval ~token (st, ast)
   | None -> Coq.Protect.E.ok st
 
-let execute_precommands ~token ~pre_commands ~(node : Fleche.Doc.Node.t) =
+let execute_precommands ~token ~memo ~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* st = parse_and_execute_in ~token ~loc:None pre_commands st in
+    let* st = parse_and_execute_in ~token ~memo ~loc:None pre_commands st in
     (* We re-interpret the lemma statement *)
     Fleche.Memo.Interp.eval ~token (st, ast.v)
   | _, _, _ -> Coq.Protect.E.ok node.state
@@ -102,7 +108,9 @@ let start ~token ~uri ?pre_commands ~thm () =
   | Ok doc ->
     let open Coq.Compat.Result.O in
     let* node = find_thm ~doc ~thm in
-    execute_precommands ~token ~pre_commands ~node |> protect_to_result
+    (* Usually single shot, so we don't memoize *)
+    let memo = false in
+    execute_precommands ~token ~memo ~pre_commands ~node |> protect_to_result
   | Error err -> Error err
 
 let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } =
@@ -115,12 +123,12 @@ let analyze_after_run st =
   | Some goals when proof_finished goals -> Run_result.Proof_finished st
   | _ -> Run_result.Current_state st
 
-let run_tac ~token ~st ~tac : (_ Run_result.t, Error.t) Result.t =
+let run ~token ?(memo = true) ~st ~tac () : (_ Run_result.t, Error.t) Result.t =
   (* Improve with thm? *)
   let loc = None in
   let f st =
     let open Coq.Protect.E.O in
-    let+ st = parse_and_execute_in ~token ~loc tac st in
+    let+ st = parse_and_execute_in ~token ~memo ~loc tac st in
     analyze_after_run st
   in
   Coq.State.in_stateM ~token ~st ~f st |> protect_to_result

petanque/agent.mli

@@ -55,11 +55,15 @@ val start :
   -> unit
   -> State.t R.t
 
-(** [run_tac ~token ~st ~tac] tries to run [tac] over state [st] *)
-val run_tac :
+(** [run ~token ?memo ~st ~tac] tries to run [tac] over state [st]. [memo] (by
+    default true) controls whether the command execution will be memoized in
+    Flèche incremental engine. *)
+val run :
      token:Coq.Limits.Token.t
+  -> ?memo:bool
   -> st:State.t
   -> tac:string
+  -> unit
   -> State.t Run_result.t R.t
 
 (** [goals ~token ~st] return the list of goals for a given [st] *)

petanque/json_shell/protocol.ml

@@ -80,7 +80,9 @@ module RunTac = struct
 
   module Params = struct
     type t =
-      { st : int
+      { memo : bool option
+            [@default None] (* Whether to memoize the execution, server-side *)
+      ; st : int
       ; tac : string
       }
     [@@deriving yojson]
@@ -93,7 +95,9 @@ module RunTac = struct
   module Handler = struct
     module Params = struct
       type t =
-        { st : State.t
+        { memo : bool option
+              [@default None] (* Whether to memoize the execution *)
+        ; st : State.t
         ; tac : string
         }
       [@@deriving yojson]
@@ -103,7 +107,8 @@ module RunTac = struct
       type t = State.t Run_result.t [@@deriving yojson]
     end
 
-    let handler ~token { Params.st; tac } = Agent.run_tac ~token ~st ~tac
+    let handler ~token { Params.memo; st; tac } =
+      Agent.run ~token ?memo ~st ~tac ()
   end
 end
 

petanque/test/basic_api.ml

@@ -38,11 +38,11 @@ let main () =
   let token = Coq.Limits.create_atomic () in
   let r ~st ~tac =
     let st = extract_st st in
-    Agent.run_tac ~token ~st ~tac
+    Agent.run ~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 ~token ~st ~tac:"induction l." () in
   let* st = r ~st ~tac:"-" in
   let* st = r ~st ~tac:"reflexivity." in
   let* st = r ~st ~tac:"-" in

petanque/test/json_api.ml

@@ -47,8 +47,9 @@ let run (ic, oc) =
     let message = message
   end) in
   let r ~st ~tac =
+    let memo = None in
     let st = extract_st st in
-    S.run_tac { st; tac }
+    S.run_tac { memo; st; tac }
   in
   (* Will this work on Windows? *)
   let root, uri = prepare_paths () in
@@ -57,7 +58,7 @@ let run (ic, oc) =
   let* premises = S.premises { st } in
   (if print_premises then
      Format.(eprintf "@[%a@]@\n%!" (pp_print_list pp_premise) premises));
-  let* st = S.run_tac { st; tac = "induction l." } in
+  let* st = S.run_tac { memo = None; st; tac = "induction l." } in
   let* st = r ~st ~tac:"-" in
   let* st = r ~st ~tac:"reflexivity." in
   let* st = r ~st ~tac:"-" in

petanque/test/json_api_failure.ml

@@ -27,15 +27,16 @@ let run (ic, oc) =
     let message = message
   end) in
   let r ~st ~tac =
+    let memo = None in
     let st = extract_st st in
-    S.run_tac { st; tac }
+    S.run_tac { memo; st; tac }
   in
   (* Will this work on Windows? *)
   let root, uri = prepare_paths () in
   let* _env = S.set_workspace { debug; root } in
   let* st = S.start { 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 = S.run_tac { memo = None; st; tac = "induction l." } in
   let* st = r ~st ~tac:"-" in
   (* Introduce an error *)
   (* let* st = r ~st ~tac:"reflexivity." in *)