From 880a83169c1d1df8726d301a9f8a9fc845cc7d1e Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 21 Apr 2008 13:57:03 +0000 Subject: - Parameterize unification by two sets of transparent_state, one for open term unification (for constant and variable delta unfolding) and one to parameterize closed-term conversion. Most of the time conversion uses full delta and unification does no delta. This fine-grain is used in rewrite/setoid_rewrite, where only closed-term delta on global constants is allowed. - Interpret Hint Unfold as a directive for delta conversion in auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints). - Remove ad-hoc support for this in typeclasses. Now setoid_rewrite works correctly w.r.t. the old version regarding local definitions. - Fix closed bugs which needed updating due to syntax modifications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10824 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/unification.ml | 37 ++++++++++++++++++------------------- pretyping/unification.mli | 5 ++--- 2 files changed, 20 insertions(+), 22 deletions(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f11ed36da..c5e9dff8b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -117,31 +117,28 @@ let sort_eqns = unify_r2l *) type unify_flags = { - modulo_conv_on_closed_terms : bool; + modulo_conv_on_closed_terms : Names.transparent_state option; use_metas_eagerly : bool; - modulo_delta : Cpred.t; - modulo_zeta : bool; + modulo_delta : Names.transparent_state; } let default_unify_flags = { - modulo_conv_on_closed_terms = true; + modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; - modulo_delta = Cpred.full; - modulo_zeta = true; + modulo_delta = full_transparent_state; } let default_no_delta_unify_flags = { - modulo_conv_on_closed_terms = true; + modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; - modulo_delta = Cpred.empty; - modulo_zeta = true; + modulo_delta = empty_transparent_state; } let expand_constant env flags c = let (ids,csts) = Conv_oracle.freeze() in match kind_of_term c with - | Const cst when Cpred.mem cst csts && Cpred.mem cst flags.modulo_delta -> constant_opt_value env cst - | Var id when flags.modulo_zeta && Idpred.mem id ids -> named_body id env + | Const cst when Cpred.mem cst csts && Cpred.mem cst (snd flags.modulo_delta) -> constant_opt_value env cst + | Var id when Idpred.mem id ids && Idpred.mem id (fst flags.modulo_delta) -> named_body id env | _ -> None let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n = @@ -149,9 +146,10 @@ let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n = let trivial_unify pb (metasubst,_) m n = match subst_defined_metas metas m with | Some m -> - if flags.modulo_conv_on_closed_terms - then is_fconv (conv_pb_of pb) env sigma m n - else eq_constr m n + (match flags.modulo_conv_on_closed_terms with + Some flags -> + is_trans_fconv (conv_pb_of pb) flags env sigma m n + | None -> eq_constr m n) | _ -> false in let rec unirec_rec curenv pb b ((metasubst,evarsubst) as substn) curm curn = let cM = Evarutil.whd_castappevar sigma curm @@ -224,7 +222,7 @@ let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n = and expand curenv pb b substn cM f1 l1 cN f2 l2 = if trivial_unify pb substn cM cN then substn - else if b & not (Cpred.is_empty flags.modulo_delta) then + else if b then match expand_constant curenv flags f1 with | Some c -> unirec_rec curenv pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN @@ -239,9 +237,10 @@ let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n = in if (not(occur_meta m)) && - (if flags.modulo_conv_on_closed_terms - then is_fconv (conv_pb_of cv_pb) env sigma m n - else eq_constr m n) + (match flags.modulo_conv_on_closed_terms with + Some flags -> + is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n + | None -> eq_constr m n) then (metas,[]) else @@ -637,7 +636,7 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd = let secondOrderAbstraction env flags allow_K typ (p, oplist) evd = (* Remove delta when looking for a subterm *) - let flags = { flags with modulo_delta = Cpred.empty } in + let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in let (evd',cllist) = w_unify_to_subterm_list env flags allow_K oplist typ evd in let typp = Typing.meta_type evd' p in diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 8e8168e5c..9156623f5 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -15,10 +15,9 @@ open Evd (*i*) type unify_flags = { - modulo_conv_on_closed_terms : bool; + modulo_conv_on_closed_terms : Names.transparent_state option; use_metas_eagerly : bool; - modulo_delta : Names.Cpred.t; - modulo_zeta : bool; + modulo_delta : Names.transparent_state; } val default_unify_flags : unify_flags -- cgit v1.2.3