diff options
| -rw-r--r-- | pretyping/evarutil.ml | 5 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 7 | ||||
| -rw-r--r-- | pretyping/evd.ml | 29 | ||||
| -rw-r--r-- | pretyping/evd.mli | 7 | ||||
| -rw-r--r-- | proofs/proofview.ml | 66 |
5 files changed, 70 insertions, 44 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d286b98e8..0b8cbff36 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -838,3 +838,8 @@ let subterm_source evk (loc,k) = | Evar_kinds.SubEvar (evk) -> evk | _ -> evk in (loc,Evar_kinds.SubEvar evk) + + +(** Term exploration up to isntantiation. *) +let kind_of_term_upto sigma t = + Constr.kind (Reductionops.whd_evar sigma t) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index f89266a60..92a3984ba 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -199,6 +199,13 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr) exception Uninstantiated_evar of existential_key val flush_and_check_evars : evar_map -> constr -> constr +(** {6 Term manipulation up to instantiation} *) + +(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t] + as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the + value of [e] in [sigma] is (recursively) used. *) +val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term + (** {6 debug pretty-printer:} *) val pr_tycon : env -> type_constraint -> Pp.std_ppcmds diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 4e38bd4e6..454c51195 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -568,14 +568,6 @@ type evar_map = { (*** Lifting primitive from Evar.Map. ***) -(* HH: The progress tactical now uses this function. *) -let progress_evar_map d1 d2 = - let is_new k v = - assert (v.evar_body == Evar_empty); - EvMap.mem k d2.defn_evars - in - not (d1 == d2) && EvMap.exists is_new d1.undf_evars - let add_name_newly_undefined naming evk evi (evtoid,idtoev) = let id = match naming with | Misctypes.IntroAnonymous -> @@ -1303,27 +1295,6 @@ let e_eq_constr_univs evdref t u = let eq_constr_univs_test evd t u = snd (eq_constr_univs evd t u) -let eq_named_context_val d ctx1 ctx2 = - ctx1 == ctx2 || - let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in - let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = - Id.equal i1 i2 && Option.equal (eq_constr_univs_test d) c1 c2 - && (eq_constr_univs_test d) t1 t2 - in List.equal eq_named_declaration c1 c2 - -let eq_evar_body d b1 b2 = match b1, b2 with -| Evar_empty, Evar_empty -> true -| Evar_defined t1, Evar_defined t2 -> eq_constr_univs_test d t1 t2 -| _ -> false - -let eq_evar_info d ei1 ei2 = - ei1 == ei2 || - eq_constr_univs_test d ei1.evar_concl ei2.evar_concl && - eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) && - eq_evar_body d ei1.evar_body ei2.evar_body - (** ppedrot: [eq_constr] may be a bit too permissive here *) - - (**********************************************************) (* Accessing metas *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 48704f75b..0765b951f 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -126,10 +126,6 @@ type evar_map (** Type of unification state. Essentially a bunch of state-passing data needed to handle incremental term construction. *) -val progress_evar_map : evar_map -> evar_map -> bool -(** Assuming that the second map extends the first one, this says if - some existing evar has been refined *) - val empty : evar_map (** The empty evar map. *) @@ -204,9 +200,6 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map val undefined_map : evar_map -> evar_info Evar.Map.t (** Access the undefined evar mapping directly. *) -val eq_evar_info : evar_map -> evar_info -> evar_info -> bool -(** Compare the evar_info's up to the universe constraints of the evar map. *) - val drop_all_defined : evar_map -> evar_map (** {6 Instantiating partial terms} *) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index b6861fd49..6f6263413 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -719,22 +719,72 @@ let give_up = (** {7 Control primitives} *) -(** Equality function on goals *) -let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in - Evd.eq_evar_info evars2 evi1 evi2 + +module Progress = struct + + (** equality function up to evar instantiation in heterogeneous + contexts. *) + (* spiwack (2015-02-19): In the previous version of progress an + equality which considers two universes equal when it is consistent + tu unify them ([Evd.eq_constr_univs_test]) was used. Maybe this + behaviour has to be restored as well. This has to be established by + practice. *) + + let rec eq_constr sigma1 sigma2 t1 t2 = + Constr.equal_with + (fun t -> Evarutil.kind_of_term_upto sigma1 t) + (fun t -> Evarutil.kind_of_term_upto sigma2 t) + t1 t2 + + (** equality function on hypothesis contexts *) + let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = + let open Environ in + let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in + let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = + Names.Id.equal i1 i2 && Option.equal (eq_constr sigma1 sigma2) c1 c2 + && (eq_constr sigma1 sigma2) t1 t2 + in List.equal eq_named_declaration c1 c2 + + let eq_evar_body sigma1 sigma2 b1 b2 = + let open Evd in + match b1, b2 with + | Evar_empty, Evar_empty -> true + | Evar_defined t1, Evar_defined t2 -> eq_constr sigma1 sigma2 t1 t2 + | _ -> false + + let eq_evar_info sigma1 sigma2 ei1 ei2 = + let open Evd in + eq_constr sigma1 sigma2 ei1.evar_concl ei2.evar_concl && + eq_named_context_val sigma1 sigma2 (ei1.evar_hyps) (ei2.evar_hyps) && + eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body + + (** Equality function on goals *) + let goal_equal evars1 gl1 evars2 gl2 = + let evi1 = Evd.find evars1 gl1 in + let evi2 = Evd.find evars2 gl2 in + eq_evar_info evars1 evars2 evi1 evi2 + +end let tclPROGRESS t = let open Proof in Pv.get >>= fun initial -> t >>= fun res -> Pv.get >>= fun final -> + (* [*_test] test absence of progress. [quick_test] is approximate + whereas [exhaustive_test] is complete. *) + let quick_test = + initial.solution == final.solution && initial.comb == final.comb + in + let exhaustive_test = + Util.List.for_all2eq begin fun i f -> + Progress.goal_equal initial.solution i final.solution f + end initial.comb final.comb + in let test = - Evd.progress_evar_map initial.solution final.solution && - not (Util.List.for_all2eq (fun i f -> goal_equal initial.solution i final.solution f) initial.comb final.comb) + quick_test || exhaustive_test in - if test then + if not test then tclUNIT res else tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) |