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 ---- engine/proofview.mli | 1 - 2 files changed, 5 deletions(-) (limited to 'engine') diff --git a/engine/proofview.ml b/engine/proofview.ml index 855235d2b0..c01879765b 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 diff --git a/engine/proofview.mli b/engine/proofview.mli index 725445251d..90be2f90ab 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -373,7 +373,6 @@ val mark_as_unsafe : unit tactic with given up goals cannot be closed. *) val give_up : unit tactic - (** {7 Control primitives} *) (** [tclPROGRESS t] checks the state of the proof after [t]. It it is -- cgit v1.2.3 From 1f36cdefd841526f804bd2dd51c1d88309333376 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 7 Nov 2016 14:47:15 +0100 Subject: Fixes to compile with ocaml 4.01 --- engine/termops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/termops.ml b/engine/termops.ml index 35cacc65b2..697b9a5f15 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -980,7 +980,7 @@ let smash_rel_context sign = let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init let mem_named_context_val id ctxt = - try Environ.lookup_named_val id ctxt; true with Not_found -> false + try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false let compact_named_context_reverse sign = let compact l decl = -- 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') diff --git a/engine/proofview.ml b/engine/proofview.ml index 21227ed198..660f737c69 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 25c82d55497db43bf2cd131f10d2ef366758bbe1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 18 Nov 2016 13:25:05 +0100 Subject: Fix UGraph.check_eq! Universes are kept in normal form w.r.t. equality but not the <= relation, so the previous check worked almost always but was actually too strict! In cases like (max(Set,u) = u) when u is declared >= Set it was failing to find an equality. Applying the KISS principle: u = v <-> u <= v /\ v <= u. Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of a colon in a typing judgment), this was not the case when an algebraic universe instantiated an evar that appeared in the term. We force their universe variable status to change in refresh_universes to avoid this. Fix ind sort inference: Use syntactic universe equality for inductive sort inference instead of check_leq (which now correctly takes constraints into account) and simplify code --- engine/evd.ml | 7 +++++++ engine/evd.mli | 3 ++- 2 files changed, 9 insertions(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index aa91fc5222..a6b6f742b7 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -854,6 +854,13 @@ let is_eq_sort s1 s2 = if Univ.Universe.equal u1 u2 then None else Some (u1, u2) +(* Precondition: l is not defined in the substitution *) +let universe_rigidity evd l = + let uctx = evd.universes in + if Univ.LSet.mem l (Univ.ContextSet.levels (UState.context_set uctx)) then + UnivFlexible (Univ.LSet.mem l (UState.algebraics uctx)) + else UnivRigid + let normalize_universe evd = let vars = ref (UState.subst evd.universes) in let normalize = Universes.normalize_universe_opt_subst vars in diff --git a/engine/evd.mli b/engine/evd.mli index b47b389d1b..89dcd92cee 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -514,7 +514,8 @@ val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_ val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts val add_global_univ : evar_map -> Univ.Level.t -> evar_map - + +val universe_rigidity : evar_map -> Univ.Level.t -> rigid val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map val is_sort_variable : evar_map -> sorts -> Univ.universe_level option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is -- cgit v1.2.3 From b8c0f76e507dc0c5dbae3ea7a89d78f16b4a7acb Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 2 Dec 2016 18:00:18 +0100 Subject: Document changes --- engine/evd.mli | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/evd.mli b/engine/evd.mli index 89dcd92cee..86887f3dcc 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -467,7 +467,17 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map (********************************************************* Sort/universe variables *) -(** Rigid or flexible universe variables *) +(** Rigid or flexible universe variables. + + [UnivRigid] variables are user-provided or come from an explicit + [Type] in the source, we do not minimize them or unify them eagerly. + + [UnivFlexible alg] variables are fresh universe variables of + polymorphic constants or generated during refinement, sometimes in + algebraic position (i.e. not appearing in the term at the moment of + creation). They are the candidates for minimization (if alg, to an + algebraic universe) and unified eagerly in the first-order + unification heurstic. *) type rigid = UState.rigid = | UnivRigid -- cgit v1.2.3 From d6bcc6ebe4f65d0555414851f7e4fb6fa1fb22a4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Jan 2017 15:05:08 +0100 Subject: Adding a new evar source to remember the name of evars which were named in the original term. Useful at least for debugging, useful to give a better message than "this placeholder", even if in the loc is known in this case. --- engine/evd.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index bffb407274..7006fde3cc 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1299,6 +1299,7 @@ let pr_decl (decl,ok) = print_constr c ++ str (if ok then ")" else "}") let pr_evar_source = function + | Evar_kinds.NamedHole id -> pr_id id | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType false -> str "pattern-matching return predicate" | Evar_kinds.CasesType true -> -- 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 + 2 files changed, 29 insertions(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/proofview.ml b/engine/proofview.ml index 2fbabb7492..721389af4f 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 90be2f90ab..294b03dca2 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} *) -- cgit v1.2.3