diff --git a/doc/changelog/02-specification-language/19611-cs-save-key.rst b/doc/changelog/02-specification-language/19611-cs-save-key.rst new file mode 100644 index 000000000000..5b324b103a5e --- /dev/null +++ b/doc/changelog/02-specification-language/19611-cs-save-key.rst @@ -0,0 +1,6 @@ +- **Changed:** + The unification algorithm does not solve unification problems of the + form `proj _ ~ _` using canonical structures when the LHS reduces or + is ground + (`#19611 `_, + by ). diff --git a/engine/evarutil.ml b/engine/evarutil.ml index f92900270f94..66630c85b4f0 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -100,6 +100,14 @@ let has_undefined_evars evd t = try let _ = f h t in false with (Not_found | NotInstantiatedEvar) -> true +let has_undefined_evars_or_metas evd t = + let rec has_ev t = + match EConstr.kind evd t with + | Evar _ | Meta _ -> raise NotInstantiatedEvar + | _ -> EConstr.iter evd has_ev t in + try let _ = has_ev t in false + with (Not_found | NotInstantiatedEvar) -> true + let is_ground_term evd t = not (has_undefined_evars evd t) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 5be7115d4306..b4ef2b096483 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -75,6 +75,7 @@ val whd_head_evar : evar_map -> constr -> constr (* An over-approximation of [has_undefined (nf_evars evd c)] *) val has_undefined_evars : evar_map -> constr -> bool +val has_undefined_evars_or_metas : evar_map -> constr -> bool val is_ground_term : evar_map -> constr -> bool val is_ground_env : evar_map -> env -> bool diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3dda8978b5ae..535769a53ab3 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -272,35 +272,17 @@ let apply_hooks env sigma proj pat = try CString.Map.get name !all_hooks env sigma proj pat with e when CErrors.noncritical e -> anomaly Pp.(str "CS hook " ++ str name ++ str " exploded")) !active_hooks -(* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose - the problem (t1 stack1) = (t2 stack2) into a problem - - stack1 = params1@[c1]@extra_args1 - stack2 = us2@extra_args2 - t1 params1 c1 = proji params (c xs) - t2 us2 = head us - extra_args1 = extra_args2 - - by finding a record R and an object c := [xs:bs](Build_R params v1..vn) - with vi = (head us), for which we know that the i-th projection proji - satisfies - - proji params (c xs) = head us - - Rem: such objects, usable for conversion, are defined in the objdef - table; practically, it amounts to "canonically" equip t2 into a - object c in structure R (since, if c1 were not an evar, the - projection would have been reduced) *) - -let check_conv_record ?metas env sigma (t1,sk1) (t2,sk2) = +let decompose_proj ?metas env sigma (t1, sk1) = (* I only recognize ConstRef projections since these are the only ones for which I know how to obtain the number of parameters. *) let (proji, u), arg = match Termops.global_app_of_constr sigma t1 with | (Names.GlobRef.ConstRef proji, u), arg -> (proji, u), arg - | _ -> raise Not_found in + | _ -> raise Not_found + | exception _ -> raise Not_found in (* Given a ConstRef projection, I obtain the structure it is a projection from. *) - let structure = Structures.Structure.find_from_projection proji in + let structure = try Structures.Structure.find_from_projection proji + with _ -> raise Not_found in (* Knowing the structure and hence its number of arguments, I can cut sk1 into pieces. *) let params1, c1, extra_args1 = match arg with @@ -323,6 +305,29 @@ let check_conv_record ?metas env sigma (t1,sk1) (t2,sk2) = match Reductionops.Stack.strip_n_app structure.nparams sk1 with | Some (params1, c1, extra_args1) -> (Reductionops.Stack.list_of_app_stack params1), c1, extra_args1 | _ -> raise Not_found in + ((proji, u), (params1, c1, extra_args1)) + +(* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose + the problem (t1 stack1) = (t2 stack2) into a problem + + stack1 = params1@[c1]@extra_args1 + stack2 = us2@extra_args2 + t1 params1 c1 = proji params (c xs) + t2 us2 = head us + extra_args1 = extra_args2 + + by finding a record R and an object c := [xs:bs](Build_R params v1..vn) + with vi = (head us), for which we know that the i-th projection proji + satisfies + + proji params (c xs) = head us + + Rem: such objects, usable for conversion, are defined in the objdef + table; practically, it amounts to "canonically" equip t2 into a + object c in structure R (since, if c1 were not an evar, the + projection would have been reduced) *) + +let check_conv_record env sigma ((proji, u), (params1, c1, extra_args1)) (t2,sk2) = let h2, sk2' = decompose_app sigma (shrink_eta sigma t2) in let sk2 = Stack.append_app sk2' sk2 in let k = Reductionops.Stack.args_size sk2 - Reductionops.Stack.args_size extra_args1 in @@ -642,6 +647,32 @@ let infer_conv_noticing_evars ~pb ~ts env sigma t1 t2 = if !has_evar then None else Some (UnifFailure (sigma, UnifUnivInconsistency e)) +module Cs_keys_cache = struct + type t = (Names.GlobRef.t Queue.t * state Names.GlobRef.Map.t) * (Names.GlobRef.t Queue.t * state Names.GlobRef.Map.t) + + let empty () : t = ((Queue.create (), Names.GlobRef.Map.empty), (Queue.create (), Names.GlobRef.Map.empty)) + + let flip (c1, c2) = (c2, c1) + + let add_left sigma appr (((c1, m1), c2) as c) = + match fst @@ EConstr.destRef sigma (fst appr) with + | k when not (Names.GlobRef.Map.mem k m1) -> + let () = Queue.push k c1 in + ((c1, Names.GlobRef.Map.add k appr m1), c2) + | _ | exception DestKO -> c + + let add sigma l2r appr c = + if l2r then add_left sigma appr c else flip (add_left sigma appr (flip c)) + + let fold_left f acc ((c, m), _) = Queue.fold (fun acc k -> f acc (Names.GlobRef.Map.find k m)) acc c + let fold l2r f acc c = fold_left f acc (if l2r then c else flip c) + + let clear_left ((c, _), _) = Queue.clear c + + let clear l2r c = + if l2r then clear_left c else clear_left (flip c) +end + let rec evar_conv_x flags env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in @@ -662,7 +693,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 = let term2 = apprec_nohdbeta flags env evd term2 in let default () = match - evar_eqappr_x flags env evd pbty + evar_eqappr_x flags env evd pbty (Cs_keys_cache.empty ()) None (whd_nored_state env evd (term1,Stack.empty)) (whd_nored_state env evd (term2,Stack.empty)) with @@ -699,6 +730,8 @@ let rec evar_conv_x flags env evd pbty term1 term2 = end and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty + keys (* canonical structure keys cache *) + lastUnfolded (* tells which side was last unfolded, if any *) (term1, sk1 as appr1) (term2, sk2 as appr2) = let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) @@ -736,8 +769,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty flags.open_ts env' evd (c'1, Stack.empty) in let out2 = whd_nored_state env' evd (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty) in - if onleft then evar_eqappr_x flags env' evd CONV out1 out2 - else evar_eqappr_x flags env' evd CONV out2 out1 + if onleft then evar_eqappr_x flags env' evd CONV keys None out1 out2 + else evar_eqappr_x flags env' evd CONV (Cs_keys_cache.flip keys) None out2 out1 in let rigids env evd sk term sk' term' = let nargs = Stack.args_size sk in @@ -777,7 +810,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty 3. reduce the redex into M and recursively solve E[?n[inst]] =? E'[M] *) let switch f a b = if l2r then f a b else f b a in let delta i = - switch (evar_eqappr_x flags env i pbty) apprF + switch (evar_eqappr_x flags env i pbty keys None) apprF (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vskM) in let default i = ise_try i [miller l2r ev apprF apprM; @@ -800,7 +833,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd (termM',skM) in let delta' i = - switch (evar_eqappr_x flags env i pbty) apprF apprM' + switch (evar_eqappr_x flags env i pbty keys None) apprF apprM' in fun i -> ise_try i [miller l2r ev apprF apprM'; consume l2r apprF apprM'; delta'] @@ -867,7 +900,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (position_problem true pbty,destEvar i' ev1',term2) else (* HH: Why not to drop sk1 and sk2 since they unified *) - evar_eqappr_x flags env evd pbty + evar_eqappr_x flags env evd pbty keys None (ev1', sk1) (term2, sk2) | Some (r,[]), Success i' -> (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) @@ -877,7 +910,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty solve_simple_eqn (conv_fun evar_conv_x) flags env i' (position_problem false pbty,destEvar i' ev2',Stack.zip i' (term1,r)) else - evar_eqappr_x flags env evd pbty + evar_eqappr_x flags env evd pbty keys None (ev2', sk1) (term2, sk2) | Some ([],r), Success i' -> (* Symmetrically *) @@ -889,7 +922,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r)) else (* HH: Why not to drop sk1 and sk2 since they unified *) - evar_eqappr_x flags env evd pbty + evar_eqappr_x flags env evd pbty keys None (ev1', sk1) (term2, sk2) | None, (UnifFailure _ as x) -> (* sk1 and sk2 have no common outer part *) @@ -923,6 +956,42 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) + let keys = Cs_keys_cache.add evd true appr1 keys in + let keys = Cs_keys_cache.add evd false appr2 keys in + let get_cs env sigma l2r keys nokey appr1 appr2 = + let appr1, appr2 = if l2r then appr1, appr2 else appr2, appr1 in + try + let (_, (_, c1, _)) as p1 = decompose_proj env sigma appr1 in + let kill, reduce = + (* TOTHINK: Should I keep c1 simplified? *) + let c1 = whd_all env sigma c1 in + (* [proj (ctor ...)]: don't use CS *) + match kind sigma c1 with + | App (h,_) when isConstruct sigma h -> true, true + | Construct _ -> true, true + | _ -> not (has_undefined_evars_or_metas sigma c1), false in + let x = + if nokey then + (try Some (check_conv_record env sigma p1 appr2) + with Not_found -> None) + else + let x = Cs_keys_cache.fold (not l2r) (fun r appr -> + match r with + | None -> + (try Some (check_conv_record env sigma p1 appr) + with | Not_found -> None) + | _ -> r) None keys in + (* If t is not a reference, it was not added to the keys cache, so we take care of it now. *) + match x with + | None when not (EConstr.isRef sigma (fst appr2)) -> + (try Some (check_conv_record env sigma p1 appr2) + with Not_found -> None) + | _ -> x in + if kill then Inr (reduce && (match x with | None -> false | _ -> true)) else + (* The projection constant will not change, so there is no point in keeping the keys anymore. *) + let () = Cs_keys_cache.clear (not l2r) keys in + match x with | Some x -> Inl x | _ -> Inr false + with _ -> Inr false in let () = debug_unification (fun () -> Pp.(v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ()))) in match (flex_kind_of_term flags env evd term1 sk1, flex_kind_of_term flags env evd term2 sk2) with @@ -991,7 +1060,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty and f2 i = let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk1' and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk2' - in evar_eqappr_x flags env i pbty out1 out2 + in evar_eqappr_x flags env i pbty keys None out1 out2 in ise_try evd [f1; f2] @@ -1003,7 +1072,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty and f2 i = let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk1' and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk2' - in evar_eqappr_x flags env i pbty out1 out2 + in evar_eqappr_x flags env i pbty keys None out1 out2 in ise_try evd [f1; f2] @@ -1015,7 +1084,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in (match res with | Some (f1,args1) -> - evar_eqappr_x flags env evd pbty (f1,Stack.append_app args1 sk1) + evar_eqappr_x flags env evd pbty keys None (f1,Stack.append_app args1 sk1) appr2 | None -> UnifFailure (evd,NotSameHead)) @@ -1026,10 +1095,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in (match res with | Some (f2,args2) -> - evar_eqappr_x flags env evd pbty appr1 (f2,Stack.append_app args2 sk2) + evar_eqappr_x flags env evd pbty keys None appr1 (f2,Stack.append_app args2 sk2) | None -> UnifFailure (evd,NotSameHead)) | _, _ -> + (* We remember if the LHS is a reducible projection to decide if we unfold left first. *) + let no_cs1 = ref false in let f1 i = (* Gather the universe constraints that would make term1 and term2 equal. If these only involve unifications of flexible universes to other universes, @@ -1050,8 +1121,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (try if not flags.with_cs then raise Not_found else conv_record flags env - (try check_conv_record env i appr1 appr2 - with Not_found -> check_conv_record env i appr2 appr1) + (match get_cs env i true keys (lastUnfolded = Some true) appr1 appr2 with + | Inl x -> x + | Inr b -> + let () = no_cs1 := b in + (match get_cs env i false keys (lastUnfolded = Some false) appr1 appr2 with + | Inl x -> x + | Inr _ -> raise Not_found)) with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f3 i = (* heuristic: unfold second argument first, exception made @@ -1079,16 +1155,21 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let rhs_is_already_stuck = rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in - if (EConstr.isLambda i term1 || rhs_is_already_stuck) - && (not (Stack.not_purely_applicative sk1')) then - evar_eqappr_x ~rhs_is_already_stuck flags env i pbty - (whd_betaiota_deltazeta_for_iota_state - flags.open_ts env i vsk1') - appr2 - else - evar_eqappr_x flags env i pbty appr1 - (whd_betaiota_deltazeta_for_iota_state - flags.open_ts env i vsk2') + let b = EConstr.isLambda i term1 || rhs_is_already_stuck + && (not (Stack.not_purely_applicative sk1')) in + ise_try i [ + (fun i -> + if b || !no_cs1 then + evar_eqappr_x flags env i pbty keys (Some false) + (whd_betaiota_deltazeta_for_iota_state + flags.open_ts env i vsk1') + appr2 + else quick_fail i); + fun i -> + if b then quick_fail i else + evar_eqappr_x flags env i pbty keys (Some true) appr1 + (whd_betaiota_deltazeta_for_iota_state + flags.open_ts env i vsk2')] in ise_try evd [f1; f2; f3] end @@ -1112,10 +1193,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let f3 i = (try if not flags.with_cs then raise Not_found - else conv_record flags env (check_conv_record env i appr1 appr2) + else conv_record flags env ( + match get_cs env i true keys false appr1 appr2 with + | Inl x -> x + | Inr _ -> raise Not_found) with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = - evar_eqappr_x flags env i pbty + evar_eqappr_x flags env i pbty keys (Some false) (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk1') appr2 @@ -1126,10 +1210,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let f3 i = (try if not flags.with_cs then raise Not_found - else conv_record flags env (check_conv_record env i appr2 appr1) + else conv_record flags env ( + match get_cs env i false keys false appr1 appr2 with + | Inl x -> x + | Inr _ -> raise Not_found) with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = - evar_eqappr_x flags env i pbty appr1 + evar_eqappr_x flags env i pbty keys (Some true) appr1 (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk2') in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index d6432094968f..e55230469e53 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -90,10 +90,14 @@ val activate_hook : name:CString.Map.key -> unit val apply_hooks : hook -(** Check if a canonical structure is applicable *) - -val check_conv_record : ?metas:(Constr.metavariable -> types option) -> env -> evar_map -> - state -> state -> +(** Check if a canonical structure is applicable. *) + +val decompose_proj : ?metas:(Constr.metavariable -> types option) -> env -> evar_map -> state -> (Names.Constant.t * EConstr.EInstance.t) * + (EConstr.t list option * EConstr.t * Reductionops.Stack.t) +val check_conv_record : env -> evar_map -> + (Names.Constant.t * EConstr.EInstance.t) * + (EConstr.t list option * EConstr.t * Reductionops.Stack.t) -> + state -> evar_map * (constr * constr) * constr * constr list * (EConstr.t list * EConstr.t list option) * (EConstr.t list * EConstr.t list) * @@ -150,9 +154,12 @@ val evar_unify : Evarsolve.unifier (**/**) (* For debugging *) +module Cs_keys_cache : sig type t end + val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags -> - env -> evar_map -> - conv_pb -> state -> state -> + env -> evar_map -> conv_pb -> + Cs_keys_cache.t -> + bool option -> state -> state -> Evarsolve.unification_result val occur_rigidly : Evarsolve.unify_flags -> diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 54f5f5fbe397..3eef6e65c4db 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1537,7 +1537,7 @@ let rec unify_0_with_initial_metas (subst : subst0) conv_at_top env cv_pb flags | Clval (_, _, b) -> Some b.rebus | exception Not_found -> None in - try Evarconv.check_conv_record ~metas (fst curenvnb) sigma f1l1 f2l2 + try Evarconv.check_conv_record (fst curenvnb) sigma (Evarconv.decompose_proj ~metas (fst curenvnb) sigma f1l1) f2l2 with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN) in if Reductionops.Stack.compare_shape ts ts1 then diff --git a/test-suite/success/telescope_canonical.v b/test-suite/success/telescope_canonical.v index 73df5ca993e6..9035e93a245b 100644 --- a/test-suite/success/telescope_canonical.v +++ b/test-suite/success/telescope_canonical.v @@ -19,7 +19,7 @@ Definition test_fix n := (refl_equal _ : W (my_getp _) = W (n + 1)). Definition pred n := match n with 0 => 0 | S m => m end. Canonical Structure predSS n := mkP (pred n). Definition test_case x := (refl_equal _ : W (my_getp _) = W (pred x)). -Fail Definition test_case' := (refl_equal _ : W (my_getp _) = W (pred 0)). +Definition test_case' := (refl_equal _ : W (my_getp _) = W (pred 0)). Canonical Structure letPnat' := mkP 0. Definition letin := (let n := 0 in n).