diff options
| -rw-r--r-- | lib/util.ml | 3 | ||||
| -rw-r--r-- | lib/util.mli | 1 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 3 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 48 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 7 | ||||
| -rw-r--r-- | test-suite/success/evars.v | 12 |
6 files changed, 63 insertions, 11 deletions
diff --git a/lib/util.ml b/lib/util.ml index 2bbdc76cf..a87b9f510 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -457,6 +457,9 @@ let list_map4 f l1 l2 l3 l4 = in map (l1,l2,l3,l4) +let list_map_to_array f l = + Array.of_list (List.map f l) + let rec list_smartfilter f l = match l with [] -> l | h::tl -> diff --git a/lib/util.mli b/lib/util.mli index 8f8475afd..380f58eab 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -101,6 +101,7 @@ val list_map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list val list_map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list +val list_map_to_array : ('a -> 'b) -> 'a list -> 'b array val list_filter_i : (int -> 'a -> bool) -> 'a list -> 'a list diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index dc7d10b47..cddfbd5d1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -743,6 +743,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = | Evar (evk1,args1), Evar (evk2,args2) when evk1 = evk2 -> let f env evd pbty x y = (evd,is_trans_fconv pbty ts env evd x y) in solve_refl ~can_drop:true f env evd evk1 args1 args2, true + | Evar ev1, Evar ev2 -> + solve_evar_evar ~force:true + (evar_define (evar_conv_x ts)) (evar_conv_x ts) env evd ev1 ev2, true | Evar ev1,_ when List.length l1 <= List.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) (* and otherwise second-order matching *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 371e37bc8..00501a893 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -136,6 +136,16 @@ let whd_head_evar_stack sigma c = let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c) +let noccur_evar evd evk c = + let rec occur_rec c = match kind_of_term c with + | Evar (evk',_ as ev') -> + (match safe_evar_value evd ev' with + | Some c -> occur_rec c + | None -> if evk = evk' then raise Occur) + | _ -> iter_constr occur_rec c + in + try occur_rec c; true with Occur -> false + (**********************) (* Creating new metas *) (**********************) @@ -704,7 +714,7 @@ let is_unification_pattern_meta env nb m l t = None let is_unification_pattern_evar env evd (evk,args) l t = - if List.for_all (fun x -> isRel x || isVar x) l & not (occur_evar evk t) then + if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar evd evk t then let args = remove_instance_local_defs evd evk (Array.to_list args) in let n = List.length args in match find_unification_pattern_args env (args @ l) t with @@ -1078,8 +1088,10 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_ let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders = let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in match res with - | Invertible (UniqueProjection (c,_)) when occur_evar evk c -> CannotInvert - | _ -> res + | Invertible (UniqueProjection (c,_)) when not (noccur_evar evd evk c) -> + CannotInvert + | _ -> + res let effective_projections = map_succeed (function Invertible c -> c | _ -> failwith"") @@ -1320,6 +1332,19 @@ let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t = | Rel n -> n <= k || Intset.mem n fv_rels | _ -> is_constrainable_in k (ev,fvs) t +let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)= + let filter1 = + restrict_upon_filter evd evk1 (noccur_evar evd evk2) (Array.to_list argsv1) + in + let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in + let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in + let filter2 = + restrict_upon_filter evd evk2 (noccur_evar evd evk1) (Array.to_list argsv2) + in + let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in + let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in + evd,ev1,ev2 + exception EvarSolvedOnTheFly of evar_map * constr let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) = @@ -1350,13 +1375,17 @@ let solve_evar_evar_l2r f g env evd aliases ev1 (evk2,_ as ev2) = with EvarSolvedOnTheFly (evd,c) -> f env evd ev2 c -let solve_evar_evar f g env evd (evk1,args1 as ev1) (evk2,args2 as ev2) = +let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 as ev2) = if are_canonical_instances args1 args2 env then (* If instances are canonical, we solve the problem in linear time *) let sign = evar_filtered_context (Evd.find evd evk2) in - let subst = List.map (fun (id,_,_) -> mkVar id) sign in - Evd.define evk2 (mkEvar(evk1,Array.of_list subst)) evd + let id_inst = list_map_to_array (fun (id,_,_) -> mkVar id) sign in + Evd.define evk2 (mkEvar(evk1,id_inst)) evd else + let evd,ev1,ev2 = + (* If an evar occurs in the instance of the other evar and the + use of an heuristic is forced, we restrict *) + if force then ensure_evar_independent g env evd ev1 ev2 else (evd,ev1,ev2) in let aliases = make_alias_map env in try solve_evar_evar_l2r f g env evd aliases ev1 ev2 with CannotProject filter1 -> @@ -1599,8 +1628,11 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs = match kind_of_term rhs with | Evar (evk2,argsv2 as ev2) -> - if evk = evk2 then solve_refl conv_algo env evd evk argsv argsv2 - else solve_evar_evar (evar_define conv_algo) conv_algo env evd ev ev2 + if evk = evk2 then + solve_refl ~can_drop:choose conv_algo env evd evk argsv argsv2 + else + solve_evar_evar ~force:choose + (evar_define conv_algo) conv_algo env evd ev ev2 | _ -> try solve_candidates conv_algo env evd ev rhs with NoCandidates -> diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 59c1c7120..bef5398aa 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -17,9 +17,6 @@ open Evd open Environ open Reductionops -val restrict_upon_filter : Evd.evar_map -> - Evd.evar -> (constr -> bool) -> constr list -> bool list option - (** {5 This modules provides useful functions for unification modulo evars } *) (** {6 Metas} *) @@ -91,6 +88,10 @@ val is_ground_term : evar_map -> constr -> bool val is_ground_env : evar_map -> env -> bool val solve_refl : ?can_drop:bool -> conv_fun -> env -> evar_map -> existential_key -> constr array -> constr array -> evar_map +val solve_evar_evar : ?force:bool -> + (env -> evar_map -> existential -> constr -> evar_map) -> conv_fun -> + env -> evar_map -> existential -> existential -> evar_map + val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> bool option * existential * constr -> evar_map * bool val reconsider_conv_pbs : conv_fun -> evar_map -> evar_map * bool diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 906eb0fc9..e6088091b 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -367,3 +367,15 @@ Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth_with_letin _ _ _ _ rI _ _)) (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx. End Bigop. + +(* Check the use of (at least) an heuristic to solve problems of the form + "?x[t] = ?y" where ?y occurs in t without easily knowing if ?y can + eventually be erased in t *) + +Section evar_evar_occur. + Variable id : nat -> nat. + Variable f : forall x, id x = 0 -> id x = 0 -> x = 1 /\ x = 2. + Variable g : forall y, id y = 0 /\ id y = 0. + (* Still evars in the resulting type, but constraints should be solved *) + Check match g _ with conj a b => f _ a b end. +End evar_evar_occur. |