diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 72 |
1 files changed, 61 insertions, 11 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a25683bf..6f626341 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -192,8 +192,8 @@ let unfocus c sp = succeed). Another benefit is that it is possible to write tactics that can be executed even if there are no focused goals. - Tactics form a monad ['a tactic], in a sense a tactic can be - seens as a function (without argument) which returns a value of - type 'a and modifies the environement (in our case: the view). + seen as a function (without argument) which returns a value of + type 'a and modifies the environment (in our case: the view). Tactics of course have arguments, but these are given at the meta-level as OCaml functions. Most tactics in the sense we are used to return [()], that is no really interesting values. But @@ -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.")) @@ -1126,7 +1176,7 @@ module V82 = struct (* Returns the open goals of the proofview together with the evar_map to - interprete them. *) + interpret them. *) let goals { comb = comb ; solution = solution; } = { Evd.it = comb ; sigma = solution } |