diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-13 11:32:04 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-13 11:32:04 +0000 |
commit | 5b5e0694d6e55b07c38e9d654206aef2b0964ea5 (patch) | |
tree | 26d059be23064ab343499168773191bf1620a311 /proofs | |
parent | cc12224f791a011a9e495cb3dbd35956abb7ed0d (diff) |
Essai de prise en compte de delta dans unify_0 (même sur termes non clos).
- Pour éviter de pénaliser auto, eauto, autorewrite, mise en place
d'une option "modulo_conv" pour contrôler l'usage de cette delta.
- Pour éviter que rewrite ne réussise trop souvent, la delta est
désactivée pour les tactiques d'élimination (une étude fine reste à faire).
- On n'utilise aussi delta que sur les sous-termes du problème
d'unification initial. C'est une heuristique qui est intuitive mais qui
reste à être évaluée.
- Au bilan, le surcoût en temps de compilation des theories est d'un
peu moins d'1%.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10557 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/clenvtac.ml | 20 | ||||
-rw-r--r-- | proofs/clenvtac.mli | 3 |
2 files changed, 17 insertions, 6 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ad19bd9b6..ced684965 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -67,15 +67,17 @@ let clenv_refine with_evars clenv gls = (refine (clenv_cast_meta clenv (clenv_value clenv))) gls +let dft = Unification.default_unify_flags -let res_pf clenv ?(with_evars=false) ?(allow_K=false) gls = - clenv_refine with_evars (clenv_unique_resolver allow_K clenv gls) gls +let res_pf clenv ?(with_evars=false) ?(allow_K=false) ?(flags=dft) gls = + clenv_refine with_evars + (clenv_unique_resolver allow_K ~flags:flags clenv gls) gls -let elim_res_pf_THEN_i clenv tac gls = +let elim_res_pf_THEN_i clenv tac gls = let clenv' = (clenv_unique_resolver true clenv gls) in tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls -let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false +let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en @@ -83,11 +85,19 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) +open Unification + +let fail_quick_unif_flags = { + modulo_conv_on_closed_terms = true; + use_metas_eagerly = false; + modulo_conv = false; +} + (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) let unifyTerms m n gls = let env = pf_env gls in let evd = create_goal_evar_defs (project gls) in - let evd' = Unification.w_unify false env CONV m n evd in + let evd' = w_unify false env CONV ~flags:fail_quick_unif_flags m n evd in tclIDTAC {it = gls.it; sigma = evars_of evd'} let unify m gls = diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 038f84f01..90d010c80 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -17,12 +17,13 @@ open Evd open Clenv open Proof_type open Tacexpr +open Unification (*i*) (* Tactics *) val unify : constr -> tactic val clenv_refine : evars_flag -> clausenv -> tactic -val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> tactic +val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic (* Compatibility, use res_pf ?with_evars:true instead *) |