diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 8 | ||||
| -rw-r--r-- | pretyping/evd.mli | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 23 | ||||
| -rw-r--r-- | pretyping/unification.mli | 1 |
4 files changed, 30 insertions, 6 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 9d3e4225db..5125b21cc1 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -495,6 +495,14 @@ let evar_list evd c = | _ -> fold_constr evrec acc c in evrec [] c +let collect_evars c = + let rec collrec acc c = + match kind_of_term c with + | Evar (evk,_) -> ExistentialSet.add evk acc + | _ -> fold_constr collrec acc c + in + collrec ExistentialSet.empty c + (**********************************************************) (* Sort variables *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index c0efdb9f82..8131837d81 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -200,8 +200,6 @@ val evar_source : existential_key -> evar_map -> hole_kind located [evar_merge evd ev1] extends the evars of [evd] with [evd1] *) val evar_merge : evar_map -> evar_map -> evar_map -val evar_list : evar_map -> constr -> existential list - (** Unification constraints *) type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * env * constr * constr @@ -214,6 +212,8 @@ val extract_changed_conv_pbs : evar_map -> evar_map * evar_constraint list val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list +val evar_list : evar_map -> constr -> existential list +val collect_evars : constr -> ExistentialSet.t (** Metas *) val find_meta : evar_map -> metavariable -> clbinding diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 47fec14963..d09e5f2451 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -163,6 +163,7 @@ type unify_flags = { modulo_delta_types : Names.transparent_state; resolve_evars : bool; use_evars_pattern_unification : bool; + frozen_evars : ExistentialSet.t; modulo_betaiota : bool; modulo_eta : bool; allow_K_in_toplevel_higher_order_unification : bool @@ -175,6 +176,7 @@ let default_unify_flags = { modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = true; + frozen_evars = ExistentialSet.empty; modulo_betaiota = false; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = false @@ -187,6 +189,7 @@ let default_no_delta_unify_flags = { modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = false; + frozen_evars = ExistentialSet.empty; modulo_betaiota = false; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = false @@ -199,6 +202,7 @@ let elim_flags = { modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = true; + frozen_evars = ExistentialSet.empty; modulo_betaiota = false; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = true @@ -211,6 +215,7 @@ let elim_no_delta_flags = { modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = false; + frozen_evars = ExistentialSet.empty; modulo_betaiota = false; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = true @@ -251,6 +256,10 @@ let do_reduce env sigma c = let (t, l) = whd_betaiota_deltazeta_for_iota_state env sigma (c, empty_stack) in applist (t, list_of_stack l) +let isAllowedEvar flags c = match kind_of_term c with + | Evar (evk,_) -> not (ExistentialSet.mem evk flags.frozen_evars) + | _ -> false + let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n = let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn = let cM = Evarutil.whd_head_evar sigma curm @@ -280,8 +289,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst, evarsubst) else error_cannot_unify_local curenv sigma (m,n,cM) - | Evar ev, _ -> sigma,metasubst,((curenv, ev,cN)::evarsubst) - | _, Evar ev -> sigma,metasubst,((curenv, ev,cM)::evarsubst) + | Evar (evk,_ as ev), _ + when not (ExistentialSet.mem evk flags.frozen_evars) -> + sigma,metasubst,((curenv, ev,cN)::evarsubst) + | _, Evar (evk,_ as ev) + when not (ExistentialSet.mem evk flags.frozen_evars) -> + sigma,metasubst,((curenv, ev,cM)::evarsubst) | Sort s1, Sort s2 -> (try @@ -318,13 +331,15 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag reduce curenvnb pb b substn cM cN) | App (f1,l1), _ when - (isMeta f1 || use_evars_pattern_unification flags && isEvar f1) & + (isMeta f1 || use_evars_pattern_unification flags && + isAllowedEvar flags f1) & is_unification_pattern curenvnb f1 l1 cN & not (dependent f1 cN) -> solve_pattern_eqn_array curenvnb f1 l1 cN substn | _, App (f2,l2) when - (isMeta f2 || use_evars_pattern_unification flags && isEvar f2) & + (isMeta f2 || use_evars_pattern_unification flags && + isAllowedEvar flags f2) & is_unification_pattern curenvnb f2 l2 cM & not (dependent f2 cM) -> solve_pattern_eqn_array curenvnb f2 l2 cM substn diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0f7eec6925..aa0267698e 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -17,6 +17,7 @@ type unify_flags = { modulo_delta_types : Names.transparent_state; resolve_evars : bool; use_evars_pattern_unification : bool; + frozen_evars : ExistentialSet.t; modulo_betaiota : bool; modulo_eta : bool; allow_K_in_toplevel_higher_order_unification : bool |