From 8cfe40dbc02156228a529c01190c50d825495013 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 22 Mar 2017 19:06:54 +0100 Subject: Ensuring static invariants about handling of pending evars in Pretyping. All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component. --- pretyping/pretyping.ml | 10 +++++----- pretyping/pretyping.mli | 4 ++-- pretyping/unification.ml | 4 ++-- pretyping/unification.mli | 4 ++-- 4 files changed, 11 insertions(+), 11 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f92110ea56..2e215b605d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -333,8 +333,8 @@ let check_evars_are_solved env current_sigma frozen pending = (* Try typeclasses, hooks, unification heuristics ... *) -let solve_remaining_evars flags env current_sigma pending = - let frozen,pending = frozen_and_pending_holes pending in +let solve_remaining_evars flags env current_sigma init_sigma = + let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in let evdref = ref current_sigma in if flags.use_typeclasses then apply_typeclasses env evdref frozen false; if Option.has_some flags.use_hook then @@ -343,12 +343,12 @@ let solve_remaining_evars flags env current_sigma 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,pending = frozen_and_pending_holes pending in +let check_evars_are_solved env current_sigma init_sigma = + let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in 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 + let sigma = solve_remaining_evars flags env sigma initial_sigma in let c = if flags.expand_evars then nf_evar sigma c else c in sigma,c diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 2c6aa7a21b..23957d5575 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -129,13 +129,13 @@ val type_uconstr : [pending], however, it can contain more evars than the pending ones. *) val solve_remaining_evars : inference_flags -> - env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map + env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map (** Checking evars and pending conversion problems are all solved, reporting an appropriate error message *) val check_evars_are_solved : - env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit + env -> (* current map: *) evar_map -> (* initial map: *) evar_map -> unit (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a91c30df6f..11771f7bac 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1520,7 +1520,7 @@ let default_matching_merge_flags sigma = use_pattern_unification = true; } -let default_matching_flags (sigma,_) = +let default_matching_flags sigma = let flags = default_matching_core_flags sigma in { core_unify_flags = flags; merge_unify_flags = default_matching_merge_flags sigma; @@ -1658,7 +1658,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * (evar_map * constr) * clause * bool | AbstractExact of Name.t * constr * types option * clause * bool type 'r abstraction_result = diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0ad882a9ff..c63502eae1 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -71,11 +71,11 @@ exception PatternNotFound type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * (evar_map * constr) * Locus.clause * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> - env -> 'r Sigma.t -> pending_constr -> (constr, 'r) Sigma.sigma + env -> 'r Sigma.t -> (evar_map * constr) -> (constr, 'r) Sigma.sigma type 'r abstraction_result = Names.Id.t * named_context_val * -- cgit v1.2.3 From 055ff65ac0da60ec76d0f382dab316c3a3302a06 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 23 Mar 2017 09:53:04 +0100 Subject: Fast path in computation of frozen evars in Pretyping. Most of the time, undefined evars are not modified by the considered function, which leads to the costly recomputation of a trivial partition of evars. We simply take advantage of physical equality to discriminate when this is useless and special-case it in the type of frozen evars. --- pretyping/pretyping.ml | 53 +++++++++++++++++++++++++++++++++++--------------- 1 file changed, 37 insertions(+), 16 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2e215b605d..88853045fc 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -257,16 +257,33 @@ type inference_flags = { [sigma'] into those already in [sigma] or deriving from an evar in [sigma] by restriction, and the evars properly created in [sigma'] *) +type frozen = +| FrozenId of evar_info Evar.Map.t + (** No pending evars. We do not put a set here not to reallocate like crazy, + but the actual data of the map is not used, only keys matter. All + functions operating on this type must have the same behaviour on + [FrozenId map] and [FrozenProgress (Evar.Map.domain map, Evar.Set.empty)] *) +| FrozenProgress of Evar.Set.t * Evar.Set.t + (** Proper partition of the evar map as described above. *) + let frozen_and_pending_holes (sigma, sigma') = - let add_derivative_of evk evi acc = - match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in - let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in - let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in - let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in - (frozen,pending) + let undefined0 = Evd.undefined_map sigma in + (** Fast path when the undefined evars where not modified *) + if undefined0 == Evd.undefined_map sigma' then + FrozenId undefined0 + else + let add_derivative_of evk evi acc = + match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in + let frozen = Evar.Map.fold add_derivative_of undefined0 Evar.Set.empty in + let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in + let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in + FrozenProgress (frozen, pending) let apply_typeclasses env evdref frozen fail_evar = - let filter_frozen evk = Evar.Set.mem evk frozen in + let filter_frozen = match frozen with + | FrozenId map -> fun evk -> Evar.Map.mem evk map + | FrozenProgress (frozen, _) -> fun 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 && not (filter_frozen evk)) @@ -276,7 +293,9 @@ let apply_typeclasses env evdref frozen fail_evar = evdref := Typeclasses.resolve_typeclasses ~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 = +let apply_inference_hook hook evdref frozen = match frozen with +| FrozenId _ -> () +| FrozenProgress (_, pending) -> evdref := Evar.Set.fold (fun evk sigma -> if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then @@ -299,7 +318,9 @@ let check_typeclasses_instances_are_solved env current_sigma frozen = (* Naive way, call resolution again with failure flag *) apply_typeclasses env (ref current_sigma) frozen true -let check_extra_evars_are_solved env current_sigma pending = +let check_extra_evars_are_solved env current_sigma frozen = match frozen with +| FrozenId _ -> () +| FrozenProgress (_, pending) -> Evar.Set.iter (fun evk -> if not (Evd.is_defined current_sigma evk) then @@ -326,26 +347,26 @@ let check_evars env initial_sigma sigma c = | _ -> Constr.iter proc_rec c in proc_rec c -let check_evars_are_solved env current_sigma frozen pending = +let check_evars_are_solved env current_sigma frozen = 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 + check_extra_evars_are_solved env current_sigma frozen (* Try typeclasses, hooks, unification heuristics ... *) let solve_remaining_evars flags env current_sigma init_sigma = - let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in + let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in let evdref = ref current_sigma in 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; + apply_inference_hook (Option.get flags.use_hook env) evdref frozen; if flags.solve_unification_constraints then apply_heuristics env evdref false; - if flags.fail_evar then check_evars_are_solved env !evdref frozen pending; + if flags.fail_evar then check_evars_are_solved env !evdref frozen; !evdref let check_evars_are_solved env current_sigma init_sigma = - let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in - check_evars_are_solved env current_sigma frozen pending + let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in + check_evars_are_solved env current_sigma frozen let process_inference_flags flags env initial_sigma (sigma,c) = let sigma = solve_remaining_evars flags env sigma initial_sigma in -- cgit v1.2.3 From 0df06c3778951402c994756a6c20b043bbf2d25f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 23 Mar 2017 11:17:49 +0100 Subject: Make the computation of frozen evars lazy in Pretyping. A lot of tactic calls actually use the open_constr_no_classes_flags option which does not require checking anything about frozen evars. Computing it upfront is useless in this case. --- pretyping/pretyping.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 88853045fc..9ed2786602 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -263,7 +263,7 @@ type frozen = but the actual data of the map is not used, only keys matter. All functions operating on this type must have the same behaviour on [FrozenId map] and [FrozenProgress (Evar.Map.domain map, Evar.Set.empty)] *) -| FrozenProgress of Evar.Set.t * Evar.Set.t +| FrozenProgress of (Evar.Set.t * Evar.Set.t) Lazy.t (** Proper partition of the evar map as described above. *) let frozen_and_pending_holes (sigma, sigma') = @@ -272,17 +272,20 @@ let frozen_and_pending_holes (sigma, sigma') = if undefined0 == Evd.undefined_map sigma' then FrozenId undefined0 else + let data = lazy begin let add_derivative_of evk evi acc = match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in let frozen = Evar.Map.fold add_derivative_of undefined0 Evar.Set.empty in let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in - FrozenProgress (frozen, pending) + (frozen, pending) + end in + FrozenProgress data let apply_typeclasses env evdref frozen fail_evar = let filter_frozen = match frozen with | FrozenId map -> fun evk -> Evar.Map.mem evk map - | FrozenProgress (frozen, _) -> fun evk -> Evar.Set.mem evk frozen + | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen in evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () @@ -295,7 +298,7 @@ let apply_typeclasses env evdref frozen fail_evar = let apply_inference_hook hook evdref frozen = match frozen with | FrozenId _ -> () -| FrozenProgress (_, pending) -> +| FrozenProgress (lazy (_, pending)) -> evdref := Evar.Set.fold (fun evk sigma -> if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then @@ -320,7 +323,7 @@ let check_typeclasses_instances_are_solved env current_sigma frozen = let check_extra_evars_are_solved env current_sigma frozen = match frozen with | FrozenId _ -> () -| FrozenProgress (_, pending) -> +| FrozenProgress (lazy (_, pending)) -> Evar.Set.iter (fun evk -> if not (Evd.is_defined current_sigma evk) then -- cgit v1.2.3 From 8131e35caaacf86cd52262329ab1b0aaa1b8c5b3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 23 Mar 2017 11:29:00 +0100 Subject: Better algorithm for Evarconv.max_undefined_with_candidates. Instead of crawling the whole undefined evar map, we use the fold_right function to process evars in decreasing order. --- pretyping/evarconv.ml | 28 +++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 88ea08c840..d18b437a33 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1196,20 +1196,22 @@ let check_problems_are_solved env evd = | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 | _ -> () +exception MaxUndefined of (Evar.t * evar_info * constr list) + let max_undefined_with_candidates evd = - (* If evar were ordered with highest index first, fold_undefined - would be going decreasingly and we could use fold_undefined to - find the undefined evar of maximum index (alternatively, - max_bindings from ocaml 3.12 could be used); instead we traverse - the whole map *) - let l = Evd.fold_undefined - (fun evk ev_info evars -> - match ev_info.evar_candidates with - | None -> evars - | Some l -> (evk,ev_info,l)::evars) evd [] in - match l with - | [] -> None - | a::l -> Some (List.last (a::l)) + let fold evk evi () = match evi.evar_candidates with + | None -> () + | Some l -> raise (MaxUndefined (evk, evi, l)) + in + (** [fold_right] traverses the undefined map in decreasing order of indices. + The evar with candidates of maximum index is thus the first evar with + candidates found by a [fold_right] traversal. This has a significant impact on + performance. *) + try + let () = Evar.Map.fold_right fold (Evd.undefined_map evd) () in + None + with MaxUndefined ans -> + Some ans let rec solve_unconstrained_evars_with_candidates ts evd = (* max_undefined is supposed to return the most recent, hence -- cgit v1.2.3