[stm] move par: implementation to vernac/comTactic and stm/partac

The current implementation of par: is still in the STM, but is optional.
If the STM does not take over it, it defaults to the implementation of
in comTactic which is based on all: (i.e. sequential).

This commit also moved the interpretation of a tactic from g_ltac to
vernac/comTactic which is more appropriate.

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

1 files changed, 82 insertions, 0 deletions

diff --git a/vernac/comTactic.ml b/vernac/comTactic.ml
new file mode 100644
index 0000000000..8a9a412362
--- /dev/null
+++ b/vernac/comTactic.ml
@@ -0,0 +1,82 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Goptions
+
+module Dyn = Dyn.Make()
+
+module DMap = Dyn.Map(struct type 'a t = 'a -> unit Proofview.tactic end)
+
+let interp_map = ref DMap.empty
+
+type 'a tactic_interpreter = 'a Dyn.tag
+type interpretable = I : 'a tactic_interpreter * 'a -> interpretable
+
+let register_tactic_interpreter na f =
+  let t = Dyn.create na in
+  interp_map := DMap.add t f !interp_map;
+  t
+
+let interp_tac (I (tag,t)) =
+  let f = DMap.find tag !interp_map in
+  f t
+
+type parallel_solver =
+  pstate:Declare.Proof.t ->
+  info:int option ->
+  interpretable ->
+  abstract:bool ->
+  with_end_tac:bool ->
+  Declare.Proof.t
+
+let print_info_trace =
+  declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"]
+
+let solve_core ~pstate n ~info t ~with_end_tac:b =
+  let pstate, status = Declare.Proof.map_fold_endline ~f:(fun etac p ->
+      let with_end_tac = if b then Some etac else None in
+      let info = Option.append info (print_info_trace ()) in
+      let (p,status) = Proof.solve n info t ?with_end_tac p in
+      (* in case a strict subtree was completed,
+         go back to the top of the prooftree *)
+      let p = Proof.maximal_unfocus Vernacentries.command_focus p in
+      p,status) pstate in
+  if not status then Feedback.feedback Feedback.AddedAxiom;
+  pstate
+
+let solve ~pstate n ~info t ~with_end_tac =
+  let t = interp_tac t in
+  solve_core ~pstate n ~info t ~with_end_tac
+
+let check_par_applicable pstate =
+  Declare.Proof.fold pstate ~f:(fun p ->
+    (Proof.data p).Proof.goals |> List.iter (fun goal ->
+    let is_ground =
+      let { Proof.sigma = sigma0 } = Declare.Proof.fold pstate ~f:Proof.data in
+      let g = Evd.find sigma0 goal in
+      let concl, hyps = Evd.evar_concl g, Evd.evar_context g in
+      Evarutil.is_ground_term sigma0 concl &&
+      List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) hyps in
+    if not is_ground then
+      CErrors.user_err
+        Pp.(strbrk("The par: goal selector does not support goals with existential variables"))))
+
+let par_implementation = ref (fun ~pstate ~info t ~abstract ~with_end_tac ->
+  let t = interp_tac t in
+  let t = Proofview.Goal.enter (fun _ ->
+    if abstract then Abstract.tclABSTRACT None ~opaque:true t else t) 
+  in
+  solve_core ~pstate Goal_select.SelectAll ~info t ~with_end_tac)
+
+let set_par_implementation f = par_implementation := f
+
+let solve_parallel ~pstate ~info t ~abstract ~with_end_tac =
+  check_par_applicable pstate;
+  !par_implementation ~pstate ~info t ~abstract ~with_end_tac