From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- proofs/clenvtac.ml | 81 ++++++++++++++++++++++++++++-------------------------- 1 file changed, 42 insertions(+), 39 deletions(-) (limited to 'proofs/clenvtac.ml') diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index b54e2323..18883df2 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -1,30 +1,20 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* crec_hd u | Cast (c,_,_) when isMeta c -> u + | Proj (p, c) -> mkProj (p, crec_hd c) | _ -> map_constr crec u and crec_hd u = @@ -53,6 +44,7 @@ let clenv_cast_meta clenv = | App(f,args) -> mkApp (crec_hd f, Array.map crec args) | Case(ci,p,c,br) -> mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) + | Proj (p, c) -> mkProj (p, crec_hd c) | _ -> u in crec @@ -62,67 +54,78 @@ let clenv_value_cast_meta clenv = let clenv_pose_dependent_evars with_evars clenv = let dep_mvs = clenv_dependent clenv in - if dep_mvs <> [] & not with_evars then + if not (List.is_empty dep_mvs) && not with_evars then raise (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); clenv_pose_metas_as_evars clenv dep_mvs -let clenv_refine with_evars ?(with_classes=true) clenv gls = +let clenv_refine with_evars ?(with_classes=true) clenv = + (** ppedrot: a Goal.enter here breaks things, because the tactic below may + solve goals by side effects, while the compatibility layer keeps those + useless goals. That deserves a FIXME. *) + Proofview.V82.tactic begin fun gl -> let clenv = clenv_pose_dependent_evars with_evars clenv in let evd' = if with_classes then - Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars + let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:(not with_evars) clenv.env clenv.evd + in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd' else clenv.evd in let clenv = { clenv with evd = evd' } in tclTHEN - (tclEVARS evd') - (refine (clenv_cast_meta clenv (clenv_value clenv))) - gls + (tclEVARS (Evd.clear_metas evd')) + (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl + end open Unification let dft = default_unify_flags -let res_pf clenv ?(with_evars=false) ?(flags=dft) gls = - clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls - -let elim_res_pf_THEN_i clenv tac gls = - let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in - tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls - -let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft - +let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = + Proofview.Goal.enter begin fun gl -> + let clenv gl = clenv_unique_resolver ~flags clenv gl in + clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl)) + end (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en particulier ne semblent pas vérifier que des instances différentes d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) -let fail_quick_unif_flags = { +let fail_quick_core_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly_in_conv_on_closed_terms = false; + use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; - modulo_delta_in_merge = None; check_applied_meta_types = false; - resolve_evars = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) - frozen_evars = ExistentialSet.empty; + frozen_evars = Evar.Set.empty; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; - allow_K_in_toplevel_higher_order_unification = false } -(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) -let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = - let env = pf_env gls in - let evd = create_goal_evar_defs (project gls) in - let evd' = w_unify env evd CONV ~flags m n in - tclIDTAC {it = gls.it; sigma = evd'} +let fail_quick_unif_flags = { + core_unify_flags = fail_quick_core_unif_flags; + merge_unify_flags = fail_quick_core_unif_flags; + subterm_unify_flags = fail_quick_core_unif_flags; + allow_K_in_toplevel_higher_order_unification = false; + resolve_evars = false +} -let unify ?(flags=fail_quick_unif_flags) m gls = - let n = pf_concl gls in unifyTerms ~flags m n gls +(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) +let unify ?(flags=fail_quick_unif_flags) m = + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let n = Tacmach.New.pf_nf_concl gl in + let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in + try + let evd' = w_unify env evd CONV ~flags m n in + Proofview.Unsafe.tclEVARSADVANCE evd' + with e when Errors.noncritical e -> + (** This is Tacticals.tclFAIL *) + Proofview.tclZERO (FailError (0, lazy (Errors.print e))) + end -- cgit v1.2.3