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. --- proofs/refine.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'proofs/refine.ml') diff --git a/proofs/refine.ml b/proofs/refine.ml index e5114a2ec..2f2142890 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -149,3 +149,14 @@ let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> } in refine ?unsafe f end } + +(** {7 solve_constraints} + + Ensure no remaining unification problems are left. Run at every "." by default. *) + +let solve_constraints = + let open Proofview in + tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> + try let sigma = Evarconv.consider_remaining_unif_problems env sigma in + Unsafe.tclEVARSADVANCE sigma + with e -> tclZERO e -- cgit v1.2.3 From be11ab322fa73804118738e7a08e9910fdf4600d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 22 Oct 2016 11:03:13 +0200 Subject: Renamings to avoid confusion deprecating old names reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics --- plugins/ssrmatching/ssrmatching.ml4 | 2 +- plugins/ssrmatching/ssrmatching.mli | 2 +- pretyping/evarconv.ml | 8 +++++--- pretyping/evarconv.mli | 3 +++ pretyping/evarsolve.ml | 6 ++++-- pretyping/evarsolve.mli | 3 +++ pretyping/pretyping.ml | 2 +- pretyping/unification.ml | 6 +++--- proofs/refine.ml | 2 +- tactics/class_tactics.ml | 2 +- tactics/equality.ml | 3 ++- toplevel/command.ml | 2 +- toplevel/vernacentries.ml | 2 +- 13 files changed, 27 insertions(+), 16 deletions(-) (limited to 'proofs/refine.ml') diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index a34fa4cae..88f028b4b 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -355,7 +355,7 @@ let nf_open_term sigma0 ise c = !s', Evd.evar_universe_context s, c' let unif_end env sigma0 ise0 pt ok = - let ise = Evarconv.consider_remaining_unif_problems env ise0 in + let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in let s, uc, t = nf_open_term sigma0 ise pt in let ise1 = create_evar_defs s in let ise1 = Evd.set_universe_context ise1 uc in diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 74a603e51..288a04e60 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -213,7 +213,7 @@ val assert_done : 'a option ref -> 'a (** Very low level APIs. these are calls to evarconv's [the_conv_x] followed by - [consider_remaining_unif_problems] and [resolve_typeclasses]. + [solve_unif_constraints_with_heuristics] and [resolve_typeclasses]. In case of failure they raise [NoMatch] *) val unify_HO : env -> evar_map -> constr -> constr -> evar_map diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3680cd777..07f6d9d38 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1081,7 +1081,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = match evar_conv_x ts env_evar evd CUMUL idty evty with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> - match reconsider_conv_pbs (evar_conv_x ts) evd with + match reconsider_unif_constraints (evar_conv_x ts) evd with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> evd @@ -1208,7 +1208,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = let conv_algo = evar_conv_x ts in let evd = check_evar_instance evd evk a conv_algo in let evd = Evd.define evk a evd in - match reconsider_conv_pbs conv_algo evd with + match reconsider_unif_constraints conv_algo evd with | Success evd -> solve_unconstrained_evars_with_candidates ts evd | UnifFailure _ -> aux l with @@ -1231,7 +1231,7 @@ let solve_unconstrained_impossible_cases env evd = Evd.define evk ty evd' | _ -> evd') evd evd -let consider_remaining_unif_problems env +let solve_unif_constraints_with_heuristics env ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd = let evd = solve_unconstrained_evars_with_candidates ts evd in let rec aux evd pbs progress stuck = @@ -1263,6 +1263,8 @@ let consider_remaining_unif_problems env check_problems_are_solved env heuristic_solved_evd; solve_unconstrained_impossible_cases env heuristic_solved_evd +let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics + (* Main entry points *) exception UnableToUnify of evar_map * unification_error diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 14947c892..2231e5bc3 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -33,7 +33,10 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr - (** Try heuristics to solve pending unification problems and to solve evars with candidates *) +val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map + val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map +(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *) (** Check all pending unification problems are solved and raise an error otherwise *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f1526facc..f0aa9b564 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1603,7 +1603,7 @@ let status_changed lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) -let reconsider_conv_pbs conv_algo evd = +let reconsider_unif_constraints conv_algo evd = let (evd,pbs) = extract_changed_conv_pbs evd status_changed in List.fold_left (fun p (pbty,env,t1,t2 as x) -> @@ -1616,6 +1616,8 @@ let reconsider_conv_pbs conv_algo evd = (Success evd) pbs +let reconsider_conv_pbs = reconsider_unif_constraints + (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None @@ -1626,7 +1628,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) try let t2 = whd_betaiota evd t2 in (* includes whd_evar *) let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in - reconsider_conv_pbs conv_algo evd + reconsider_unif_constraints conv_algo evd with | NotInvertibleUsingOurAlgorithm t -> UnifFailure (evd,NotClean (ev1,env,t)) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index f94c83b6d..b6bdc0788 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -54,7 +54,10 @@ val solve_evar_evar : ?force:bool -> val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> bool option * existential * constr -> unification_result +val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result + val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result +(** @deprecated Alias for [reconsider_unif_constraints] *) val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> constr -> constr list option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6afa55862..95d854323 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -290,7 +290,7 @@ let apply_inference_hook hook evdref pending = let apply_heuristics env evdref fail_evar = (* Resolve eagerly, potentially making wrong choices *) - try evdref := consider_remaining_unif_problems + try evdref := solve_unif_constraints_with_heuristics ~ts:(Typeclasses.classes_transparent_state ()) env !evdref with e when CErrors.noncritical e -> let e = CErrors.push e in if fail_evar then iraise e diff --git a/pretyping/unification.ml b/pretyping/unification.ml index fc63015a8..259318693 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1220,7 +1220,7 @@ let is_mimick_head ts f = let try_to_coerce env evd c cty tycon = let j = make_judge c cty in let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in - let evd' = Evarconv.consider_remaining_unif_problems env evd' in + let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in (evd',j'.uj_val) @@ -1272,8 +1272,8 @@ let solve_simple_evar_eqn ts env evd ev rhs = | Success evd -> if Flags.version_less_or_equal Flags.V8_5 then (* We used to force solving unrelated problems at arbitrary times *) - Evarconv.consider_remaining_unif_problems env evd - else (* solve_simple_eqn calls reconsider_conv_pbs itself *) + Evarconv.solve_unif_constraints_with_heuristics env evd + else (* solve_simple_eqn calls reconsider_unif_constraints itself *) evd (* [w_merge env sigma b metas evars] merges common instances in metas diff --git a/proofs/refine.ml b/proofs/refine.ml index 2f2142890..3f5527060 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -157,6 +157,6 @@ end } let solve_constraints = let open Proofview in tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> - try let sigma = Evarconv.consider_remaining_unif_problems env sigma in + try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in Unsafe.tclEVARSADVANCE sigma with e -> tclZERO e diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 0944cbe38..9ea402726 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1437,7 +1437,7 @@ let initial_select_evars filter = let resolve_typeclass_evars debug depth unique env evd filter split fail = let evd = - try Evarconv.consider_remaining_unif_problems + try Evarconv.solve_unif_constraints_with_heuristics ~ts:(Typeclasses.classes_transparent_state ()) env evd with e when CErrors.noncritical e -> evd in diff --git a/tactics/equality.ml b/tactics/equality.ml index e9d08d737..bb3cbad92 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1163,7 +1163,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let dflt_typ = unsafe_type_of env sigma dflt in try let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in - let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in + let () = + evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in dflt with Evarconv.UnableToUnify _ -> error "Cannot solve a unification problem." diff --git a/toplevel/command.ml b/toplevel/command.ml index 12c387dcf..7ffe680e5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1129,7 +1129,7 @@ let interp_recursive isfix fixl notations = () in (* Instantiate evars and check all are resolved *) - let evd = consider_remaining_unif_problems env_rec !evdref in + let evd = solve_unif_constraints_with_heuristics env_rec !evdref in let evd, nf = nf_evars_and_universes evd in let fixdefs = List.map (Option.map nf) fixdefs in let fixtypes = List.map nf fixtypes in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f69bac437..9d3837d2e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1497,7 +1497,7 @@ let get_current_context_of_args = function let vernac_check_may_eval redexp glopt rc = let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in - let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in + let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in let pl, uctx = Evd.universe_context sigma' in -- cgit v1.2.3