From cb8a5bb09019146eb66208d4c38a001ea98e4668 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 7 Nov 2024 10:25:46 +0100 Subject: [PATCH 1/3] rm problematic variables under lambdas and evars for evar instantiation --- pretyping/evarsolve.ml | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 97f86c6df72f..76a0c7578399 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1753,6 +1753,20 @@ let rec invert_definition unify flags choose imitate_defs map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1) imitate envk t with _ -> progress := p; imitate envk (whd_beta env' !evdref t)) + | App (f, args) when EConstr.isEvar !evdref f -> + progress := true; + (* Tries to imitate the arguments. If this fails, i is Some i' with i' the index of the last argument we fail to imitate *) + let i, args' = Array.fold_left_map_i (fun i k a -> + try let a' = imitate envk a in (k, a') + with ex -> (Some i, a)) None args in + (match i with + | None -> + let f' = imitate envk f in + if f' == f && Array.for_all2 (==) args args' then t else EConstr.mkApp (f', args') + | Some i -> + let args, args' = Array.chop (i+1) args in + let evd, e = Evardefine.evar_absorb_arguments env !evdref (EConstr.destEvar !evdref f) (Array.to_list args) in + evdref := evd; imitate envk (EConstr.mkApp (EConstr.mkEvar e, args'))) | _ -> progress := true; match From 89ffb3f06bf76c67f924c61a363950368b95d6e0 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 14 Nov 2024 18:06:30 +0100 Subject: [PATCH 2/3] rm beta-redex case --- pretyping/evarsolve.ml | 7 ------- 1 file changed, 7 deletions(-) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 76a0c7578399..965ce6b9fcce 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1746,13 +1746,6 @@ let rec invert_definition unify flags choose imitate_defs add_conv_oriented_pb (None,env',mkEvar ev'',mkEvar ev') evd in evdref := evd; evar'') - | App (f, args) when EConstr.isLambda !evdref f -> - let p = !progress in - progress := true; - (try - map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1) - imitate envk t - with _ -> progress := p; imitate envk (whd_beta env' !evdref t)) | App (f, args) when EConstr.isEvar !evdref f -> progress := true; (* Tries to imitate the arguments. If this fails, i is Some i' with i' the index of the last argument we fail to imitate *) From bbabba05702cfbc1da424a17b37fae81a3a8074c Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 5 Dec 2024 13:44:07 +0100 Subject: [PATCH 3/3] shelve new variable when instantiating old shelved variable with the new one in `evarsolve/instantiate_evar` --- pretyping/evarsolve.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 965ce6b9fcce..bd47ead48550 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1579,6 +1579,13 @@ let instantiate_evar unify flags env evd evk body = 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 + let evd' = try + let evk' = match EConstr.kind evd' body with + | Evar (e, _) -> e + | App (f, _) -> fst (EConstr.destEvar evd' f) + | _ -> raise DestKO in + if List.mem evk (Evd.shelf evd') then Evd.shelve evd' [evk'] else evd' + with DestKO -> evd' in Evd.define evk body evd' (* We try to instantiate the evar assuming the body won't depend