From 4841b790bbe517deefac11e8df1a7a1494d56bec Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 12 Jan 2016 17:02:09 +0100 Subject: Fix essential bug in new Keyed Unification mode reported by R. Krebbers. [rewrite] was calling find_suterm using the wrong unification flags, not allowing full delta in unification of terms with the right keys as desired. --- pretyping/unification.ml | 2 ++ pretyping/unification.mli | 2 ++ 2 files changed, 4 insertions(+) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 9758aa43c4..510d5761b7 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -37,6 +37,8 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> keyed_unification:=a); } +let is_keyed_unification () = !keyed_unification + let debug_unification = ref (false) let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optdepr = false; diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 119b1a7590..9246c10f90 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -42,6 +42,8 @@ val default_no_delta_unify_flags : unit -> unify_flags val elim_flags : unit -> unify_flags val elim_no_delta_flags : unit -> unify_flags +val is_keyed_unification : unit -> bool + (** The "unique" unification fonction *) val w_unify : env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -- cgit v1.2.3 From fc642ca962dd5228a5a714b8e41506dcbc3b6520 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 12 Jan 2016 19:27:02 +0100 Subject: Extend last commit: keyed unification uses full conversions on the applied constant and arguments _separately_. --- pretyping/unification.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 510d5761b7..48638474a8 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1649,8 +1649,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = let cl = strip_outer_cast cl in (try if closed0 cl && not (isEvar cl) && keyed_unify env evd kop cl then - (try w_typed_unify env evd CONV flags op cl,cl - with ex when Pretype_errors.unsatisfiable_exception ex -> + (try + if !keyed_unification then + let f1, l1 = decompose_app_vect op in + let f2, l2 = decompose_app_vect cl in + w_typed_unify_array env evd flags f1 l1 f2 l2,cl + else w_typed_unify env evd CONV flags op cl,cl + with ex when Pretype_errors.unsatisfiable_exception ex -> bestexn := Some ex; error "Unsat") else error "Bound 1" with ex when precatchable_exception ex -> -- cgit v1.2.3 From be4bfc78c493464cb0af40d7fae08ba86295a6f9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Jan 2016 20:49:34 +0100 Subject: Fixing #4256 and #4484 (changes in evar-evar resolution made that new evars were created making in turn that evars formerly recognized as pending were not anymore in the list of pending evars). This also fixes the reopening of #3848. See comments on #4484 for details. --- pretyping/pretyping.ml | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index faba5c7563..521fa2247b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -183,22 +183,26 @@ type inference_flags = { expand_evars : bool } +let frozen_holes (sigma, sigma') = + let fold evk _ accu = Evar.Set.add evk accu in + Evd.fold_undefined fold sigma Evar.Set.empty + let pending_holes (sigma, sigma') = let fold evk _ accu = if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu in Evd.fold_undefined fold sigma' Evar.Set.empty -let apply_typeclasses env evdref pending fail_evar = - let filter_pending evk = Evar.Set.mem evk pending in +let apply_typeclasses env evdref frozen fail_evar = + let filter_frozen evk = Evar.Set.mem evk frozen in evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () - then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && filter_pending evk) - else (fun evk evi -> Typeclasses.no_goals evk evi && filter_pending evk)) + then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk)) + else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen evk))) ~split:true ~fail:fail_evar env !evdref; if Flags.is_program_mode () then (* Try optionally solving the obligations *) evdref := Typeclasses.resolve_typeclasses - ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && filter_pending evk) ~split:true ~fail:false env !evdref + ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env !evdref let apply_inference_hook hook evdref pending = evdref := Evar.Set.fold (fun evk sigma -> @@ -219,9 +223,9 @@ let apply_heuristics env evdref fail_evar = with e when Errors.noncritical e -> let e = Errors.push e in if fail_evar then iraise e -let check_typeclasses_instances_are_solved env current_sigma pending = +let check_typeclasses_instances_are_solved env current_sigma frozen = (* Naive way, call resolution again with failure flag *) - apply_typeclasses env (ref current_sigma) pending true + apply_typeclasses env (ref current_sigma) frozen true let check_extra_evars_are_solved env current_sigma pending = Evar.Set.iter @@ -233,26 +237,28 @@ let check_extra_evars_are_solved env current_sigma pending = | _ -> error_unsolvable_implicit loc env current_sigma evk None) pending -let check_evars_are_solved env current_sigma pending = - check_typeclasses_instances_are_solved env current_sigma pending; +let check_evars_are_solved env current_sigma frozen pending = + check_typeclasses_instances_are_solved env current_sigma frozen; check_problems_are_solved env current_sigma; check_extra_evars_are_solved env current_sigma pending (* Try typeclasses, hooks, unification heuristics ... *) let solve_remaining_evars flags env current_sigma pending = + let frozen = frozen_holes pending in let pending = pending_holes pending in let evdref = ref current_sigma in - if flags.use_typeclasses then apply_typeclasses env evdref pending false; + if flags.use_typeclasses then apply_typeclasses env evdref frozen false; if Option.has_some flags.use_hook then apply_inference_hook (Option.get flags.use_hook env) evdref pending; if flags.use_unif_heuristics then apply_heuristics env evdref false; - if flags.fail_evar then check_evars_are_solved env !evdref pending; + if flags.fail_evar then check_evars_are_solved env !evdref frozen pending; !evdref let check_evars_are_solved env current_sigma pending = + let frozen = frozen_holes pending in let pending = pending_holes pending in - check_evars_are_solved env current_sigma pending + check_evars_are_solved env current_sigma frozen pending let process_inference_flags flags env initial_sigma (sigma,c) = let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in -- cgit v1.2.3