diff options
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 63 |
1 files changed, 44 insertions, 19 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 79839099f7..4d5715a391 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -25,14 +25,43 @@ open Reductionops open Evarutil open Pretype_errors +module AllowedEvars = struct + + type t = + | AllowAll + | AllowFun of (Evar.t -> bool) * Evar.Set.t + + let mem allowed evk = + match allowed with + | AllowAll -> true + | AllowFun (f,except) -> f evk && not (Evar.Set.mem evk except) + + let remove evk = function + | AllowAll -> AllowFun ((fun _ -> true), Evar.Set.singleton evk) + | AllowFun (f,except) -> AllowFun (f, Evar.Set.add evk except) + + let all = AllowAll + + let except evars = + AllowFun ((fun _ -> true), evars) + + let from_pred f = + AllowFun (f, Evar.Set.empty) + +end + type unify_flags = { modulo_betaiota: bool; open_ts : TransparentState.t; closed_ts : TransparentState.t; subterm_ts : TransparentState.t; - frozen_evars : Evar.Set.t; + allowed_evars : AllowedEvars.t; allow_K_at_toplevel : bool; - with_cs : bool } + with_cs : bool +} + +let is_evar_allowed flags evk = + AllowedEvars.mem flags.allowed_evars evk type unification_kind = | TypeUnification @@ -216,9 +245,6 @@ type 'a update = | UpdateWith of 'a | NoUpdate -open Context.Named.Declaration -let inst_of_vars sign = List.map (get_id %> mkVar) sign - let restrict_evar_key evd evk filter candidates = match filter, candidates with | None, NoUpdate -> evd, evk @@ -701,8 +727,7 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si let (evd, evk) = new_pure_evar sign evd ty_t_in_sign ~filter ~src in let t_in_env = whd_evar evd t_in_env in let evd = define_fun env evd None (evk, inst_in_env) t_in_env in - let ctxt = named_context_of_val sign in - let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in + let inst_in_sign = evar_identity_subst (Evd.find evd evk) in let evar_in_sign = mkEvar (evk, inst_in_sign) in (evd,whd_evar evd evar_in_sign) @@ -735,9 +760,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let sign1 = evar_hyps evi1 in let filter1 = evar_filter evi1 in let src = subterm_source evk1 evi1.evar_source in - let ids1 = List.map get_id (named_context_of_val sign1) in let avoid = Environ.ids_of_named_context_val sign1 in - let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in + let inst_in_sign = evar_identity_subst evi1 in let open Context.Rel.Declaration in let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) = List.fold_right (fun d (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) -> @@ -1312,24 +1336,24 @@ let preferred_orientation evd evk1 evk2 = let solve_evar_evar_aux force f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env evd in - let frozen_ev1 = Evar.Set.mem evk1 flags.frozen_evars in - let frozen_ev2 = Evar.Set.mem evk2 flags.frozen_evars in + let allowed_ev1 = is_evar_allowed flags evk1 in + let allowed_ev2 = is_evar_allowed flags evk2 in if preferred_orientation evd evk1 evk2 then - try if not frozen_ev1 then + try if allowed_ev1 then solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 else raise (CannotProject (evd,ev2)) with CannotProject (evd,ev2) -> - try if not frozen_ev2 then + try if allowed_ev2 then solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 else raise (CannotProject (evd,ev1)) with CannotProject (evd,ev1) -> add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd else - try if not frozen_ev2 then + try if allowed_ev2 then solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 else raise (CannotProject (evd,ev1)) with CannotProject (evd,ev1) -> - try if not frozen_ev1 then + try if allowed_ev1 then solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 else raise (CannotProject (evd,ev2)) with CannotProject (evd,ev2) -> @@ -1395,15 +1419,15 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 = let candidates = filter_candidates evd evk untypedfilter NoUpdate in let filter = closure_of_filter evd evk untypedfilter in let evd',ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in - let frozen = Evar.Set.mem evk flags.frozen_evars in - if Evar.equal (fst ev1) evk && (frozen || can_drop) then + let allowed = is_evar_allowed flags evk in + if Evar.equal (fst ev1) evk && (not allowed || can_drop) then (* No refinement needed *) evd' else (* either progress, or not allowed to drop, e.g. to preserve possibly *) (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *) (* if e can depend on x until ?y is not resolved, or, conversely, we *) (* don't know if ?y has to be unified with ?y, until e is resolved *) - if frozen then + if not allowed then (* We cannot prune a frozen evar *) add_conv_oriented_pb (pbty,env,mkEvar (evk, argsv1),mkEvar (evk,argsv2)) evd else @@ -1460,7 +1484,8 @@ let occur_evar_upto_types sigma n c = let instantiate_evar unify flags env evd evk body = (* Check instance freezing the evar to be defined, as checking could involve the same evar definition problem again otherwise *) - let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in + let allowed_evars = AllowedEvars.remove evk flags.allowed_evars in + let flags = { flags with allowed_evars } in let evd' = check_evar_instance unify flags env evd evk body in Evd.define evk body evd' |