From ccb173a440fa2eb7105a692c979253edbfe475ee Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 19 Oct 2016 13:33:28 +0200 Subject: Unification constraint handling (#4763, #5149) Refine fix for bug #4763, fixing #5149 Tactic [Refine.solve_constraints] and global option Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of unification constraints and evar candidates to be solved. run_tactic now calls [solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics. The option allows to unset the forced solving unification constraints at each ".", letting the user control the places where the use of heuristics is done. Fix test-suite files too. --- engine/proofview.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index 855235d2b..c01879765 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1157,10 +1157,6 @@ let tclLIFT = Proof.lift let tclCHECKINTERRUPT = tclLIFT (NonLogical.make Control.check_for_interrupt) - - - - (*** Compatibility layer with <= 8.2 tactics ***) module V82 = struct type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma -- cgit v1.2.3 From a79a62c9fb5690ff1043d9c0dd44f61cd535cc12 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Mon, 26 Sep 2016 09:11:42 +0200 Subject: tclDISPATCH: more informative error message "expected _n_ tactics" -> "exected _n_ tactics, was given _k_". Also affect other similar tacticals from `Proofview`. I used that for debugging once, I thought I might as well propose it for mergeing. --- engine/proofview.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index 21227ed19..660f737c6 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -423,11 +423,11 @@ let tclFOCUSID id t = exception SizeMismatch of int*int let _ = CErrors.register_handler begin function - | SizeMismatch (i,_) -> + | SizeMismatch (i,j) -> let open Pp in let errmsg = str"Incorrect number of goals" ++ spc() ++ - str"(expected "++int i++str(String.plural i " tactic") ++ str")." + str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." in CErrors.user_err errmsg | _ -> raise CErrors.Unhandled -- cgit v1.2.3 From f30822ba46d08d65597e0e3230ea6ad86c98453f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Nov 2016 16:03:53 +0100 Subject: Proofview: tclINDEPENDENTL --- engine/proofview.ml | 29 ++++++++++++++++++++++++++++- engine/proofview.mli | 1 + tactics/tacticals.ml | 13 +++++++++++++ tactics/tacticals.mli | 1 + 4 files changed, 43 insertions(+), 1 deletion(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index 2fbabb749..721389af4 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -453,6 +453,25 @@ let iter_goal i = Solution.get >>= fun evd -> Comb.set CList.(undefined evd (flatten (rev subgoals))) +(** List iter but allocates a list of results *) +let map_goal i = + let rev = List.rev in (* hem... Proof masks List... *) + let open Proof in + Comb.get >>= fun initial -> + Proof.List.fold_left begin fun (acc, subgoals as cur) goal -> + Solution.get >>= fun step -> + match Evarutil.advance step goal with + | None -> return cur + | Some goal -> + Comb.set [goal] >> + i goal >>= fun res -> + Proof.map (fun comb -> comb :: subgoals) Comb.get >>= fun x -> + return (res :: acc, x) + end ([],[]) initial >>= fun (results_rev, subgoals) -> + Solution.get >>= fun evd -> + Comb.set CList.(undefined evd (flatten (rev subgoals))) >> + return (rev results_rev) + (** A variant of [Monad.List.fold_left2] where the first list is the list of focused goals. The argument tactic is executed in a focus comprising only of the current goal, a goal which has been solved @@ -585,7 +604,15 @@ let tclINDEPENDENT tac = let tac = InfoL.tag (Info.DBranch) tac in InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac)) - +let tclINDEPENDENTL tac = + let open Proof in + Pv.get >>= fun initial -> + match initial.comb with + | [] -> tclUNIT [] + | [_] -> tac >>= fun x -> return [x] + | _ -> + let tac = InfoL.tag (Info.DBranch) tac in + InfoL.tag (Info.Dispatch) (map_goal (fun _ -> tac)) (** {7 Goal manipulation} *) diff --git a/engine/proofview.mli b/engine/proofview.mli index 90be2f90a..294b03dca 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -292,6 +292,7 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact independent of backtracking in another. It is equivalent to [tclEXTEND [] tac []]. *) val tclINDEPENDENT : unit tactic -> unit tactic +val tclINDEPENDENTL: 'a tactic -> 'a list tactic (** {7 Goal manipulation} *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 93c04e373..c5562b326 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -368,6 +368,16 @@ module New = struct catch_failerror e <*> t2 end end + + let tclORELSE0L t1 t2 = + tclINDEPENDENTL begin + tclORELSE + t1 + begin fun e -> + catch_failerror e <*> t2 + end + end + let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 @@ -419,6 +429,9 @@ module New = struct let tclTRY t = tclORELSE0 t (tclUNIT ()) + + let tclTRYb t = + tclORELSE0L (t <*> tclUNIT true) (tclUNIT false) let tclIFTHENELSE t1 t2 t3 = tclINDEPENDENT begin diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 18cf03c51..7aacc52f3 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -209,6 +209,7 @@ module New : sig val tclMAP : ('a -> unit tactic) -> 'a list -> unit tactic val tclTRY : unit tactic -> unit tactic + val tclTRYb : unit tactic -> bool list tactic val tclFIRST : unit tactic list -> unit tactic val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic -- cgit v1.2.3