diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comTactic.ml | 82 | ||||
| -rw-r--r-- | vernac/comTactic.mli | 47 | ||||
| -rw-r--r-- | vernac/himsg.ml | 6 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 2 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 1 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 3 | ||||
| -rw-r--r-- | vernac/vernacextend.mli | 1 |
7 files changed, 135 insertions, 7 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 diff --git a/vernac/comTactic.mli b/vernac/comTactic.mli new file mode 100644 index 0000000000..f1a75e1b6a --- /dev/null +++ b/vernac/comTactic.mli @@ -0,0 +1,47 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(** Tactic interpreters have to register their interpretation function *) +type 'a tactic_interpreter +type interpretable = I : 'a tactic_interpreter * 'a -> interpretable + +(** ['a] should be marshallable if ever used with [par:] *) +val register_tactic_interpreter : + string -> ('a -> unit Proofview.tactic) -> 'a tactic_interpreter + +(** Entry point for toplevel tactic expression execution. It calls Proof.solve + after having interpreted the tactic, and after the tactic runs it + unfocus as much as needed to put a goal under focus. *) +val solve : + pstate:Declare.Proof.t -> + Goal_select.t -> + info:int option -> + interpretable -> + with_end_tac:bool -> + Declare.Proof.t + +(** [par: tac] runs tac on all goals, possibly in parallel using a worker pool. + If tac is [abstract tac1], then [abstract] is passed + explicitly to the solver and [tac1] passed to worker since it is up to + master to opacify the sub proofs produced by the workers. *) +type parallel_solver = + pstate:Declare.Proof.t -> + info:int option -> + interpretable -> + abstract:bool -> (* the tactic result has to be opacified as per abstract *) + with_end_tac:bool -> + Declare.Proof.t + +(** Entry point when the goal selector is par: *) +val solve_parallel : parallel_solver + +(** By default par: is implemented with all: (sequential). + The STM and LSP document manager provide "more parallel" implementations *) +val set_par_implementation : parallel_solver -> unit diff --git a/vernac/himsg.ml b/vernac/himsg.ml index c16eaac516..a9de01bfd0 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -831,7 +831,7 @@ let pr_constraints printenv env sigma evars cstrs = (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++ str " : " ++ pr_leconstr_env env' sigma evi.evar_concl ++ fnl ()) l in - h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs) + h (pe ++ evs ++ pr_evar_constraints sigma cstrs) else let filter evk _ = Evar.Map.mem evk evars in pr_evar_map_filter ~with_univs:false filter env sigma @@ -973,8 +973,8 @@ let explain_not_match_error = function (UContext.instance uctx) (UContext.constraints uctx) in - str "incompatible polymorphic binders: got" ++ spc () ++ h 0 (pr_auctx got) ++ spc() ++ - str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++ + str "incompatible polymorphic binders: got" ++ spc () ++ h (pr_auctx got) ++ spc() ++ + str "but expected" ++ spc() ++ h (pr_auctx expect) ++ (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else fnl() ++ str "(incompatible constraints)") | IncompatibleVariance -> diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 8b00484b4a..06f7c32cdc 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -216,7 +216,7 @@ let print_polymorphism ref = (if poly then str "universe polymorphic" else if template_poly then str "template universe polymorphic " - ++ h 0 (pr_template_variables template_variables) + ++ h (pr_template_variables template_variables) else str "not universe polymorphic") ] let print_type_in_type ref = diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 994592a88a..cd0dd5e9a6 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -43,4 +43,5 @@ Topfmt Loadpath ComArguments Vernacentries +ComTactic Vernacinterp diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index eacb7fe6cb..ed63332861 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -30,7 +30,6 @@ type vernac_classification = | VtQed of vernac_qed_type (* A proof step *) | VtProofStep of { - parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; proof_block_detection : proof_block_name option } (* Queries are commands assumed to be "pure", that is to say, they @@ -124,7 +123,7 @@ let declare_vernac_classifier name f = let classify_as_query = VtQuery let classify_as_sideeff = VtSideff ([], VtLater) -let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None} +let classify_as_proofstep = VtProofStep { proof_block_detection = None} type (_, _) ty_sig = | TyNil : (vernac_command, vernac_classification) ty_sig diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 5ef137cfc0..e1e3b4cfe5 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -46,7 +46,6 @@ type vernac_classification = | VtQed of vernac_qed_type (* A proof step *) | VtProofStep of { - parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; proof_block_detection : proof_block_name option } (* Queries are commands assumed to be "pure", that is to say, they |