From 6b758c51c24c143284b6463f6187cf2aa40bc825 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 26 Jan 2024 16:44:22 +0100 Subject: [PATCH 1/2] fix sigma pruning when calling ltac, reachability is not correct --- coq-builtin-synterp.elpi | 4 +++- coq-builtin.elpi | 4 +++- src/coq_elpi_HOAS.ml | 4 ++-- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/coq-builtin-synterp.elpi b/coq-builtin-synterp.elpi index 7a2904b9a..c02b80a78 100644 --- a/coq-builtin-synterp.elpi +++ b/coq-builtin-synterp.elpi @@ -306,10 +306,12 @@ external pred coq.env.current-section-path o:list string. kind clause type. type clause id -> grafting -> prop -> clause. -% Specify if the clause has to be grafted before or after a named clause +% Specify if the clause has to be grafted before, grafted after or replace +% a named clause kind grafting type. type before id -> grafting. type after id -> grafting. +type replace id -> grafting. % Specify to which module the clause should be attached to kind scope type. diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 3ab751e67..d5a2085af 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -1711,10 +1711,12 @@ external pred coq.extra-dep i:id, o:option id. kind clause type. type clause id -> grafting -> prop -> clause. -% Specify if the clause has to be grafted before or after a named clause +% Specify if the clause has to be grafted before, grafted after or replace +% a named clause kind grafting type. type before id -> grafting. type after id -> grafting. +type replace id -> grafting. % Specify to which module the clause should be attached to kind scope type. diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 8c72470b8..af3df1c3e 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -2434,10 +2434,10 @@ let solution2evd sigma0 { API.Data.constraints; assignments; state; pp_ctx } roo get_declared_goals (Evar.Set.diff all_goals solved_goals) constraints state assignments pp_ctx in debug Pp.(fun () -> str "Goals: " ++ prlist_with_sep spc Evar.print declared_goals); debug Pp.(fun () -> str "Shelved Goals: " ++ prlist_with_sep spc Evar.print shelved_goals); - Evd.fold_undefined (fun k _ sigma -> +(* wrong: Evd.fold_undefined (fun k _ sigma -> if Evar.Set.mem k all_goals || Evd.mem sigma0 k then sigma else Evd.remove sigma k - ) sigma sigma, + ) sigma*) sigma, declared_goals, shelved_goals From 849a95d8afb37a945a64670f04ba66b0016df03c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 26 Jan 2024 20:56:20 +0100 Subject: [PATCH 2/2] fix reachability test --- examples/example_abs_evars.v | 2 +- src/coq_elpi_HOAS.ml | 16 ++++++++++------ 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/examples/example_abs_evars.v b/examples/example_abs_evars.v index f9879ee37..96fb4e4c3 100644 --- a/examples/example_abs_evars.v +++ b/examples/example_abs_evars.v @@ -88,7 +88,7 @@ solve (goal _ _ _ _ [trm T] as G) GL :- solve (goal _ _ T _ [] as G) GL :- std.assert! (abs-evars T ClosedT N) "closure fails", coq.mk-app {{ (fun x : lp:ClosedT => x) _ }} {coq.mk-n-holes N} R, -refine R G GL. + refine R G GL. }}. Elpi Typecheck. diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index af3df1c3e..cedbf7c8e 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -2411,7 +2411,10 @@ let get_declared_goals all_goals constraints state assignments pp_ctx = let rec reachable1 sigma root acc = let EvarInfo info = Evd.find sigma root in - let res = match Evd.evar_body info with Evd.Evar_empty -> Evar.Set.add root acc | Evd.Evar_defined _ -> acc in + let res = + match Evd.evar_body info with + | Evd.Evar_empty -> Evar.Set.add root acc + | Evd.Evar_defined d -> acc in let res = Evar.Set.union res @@ Evarutil.filtered_undefined_evars_of_evar_info sigma info in if Evar.Set.equal res acc then acc else reachable sigma res res and reachable sigma roots acc = @@ -2429,15 +2432,16 @@ let reachable sigma roots acc = let solution2evd sigma0 { API.Data.constraints; assignments; state; pp_ctx } roots = let state, solved_goals, _, _gls = elpi_solution_to_coq_solution ~calldepth:0 constraints state in let sigma = get_sigma state in - let all_goals = reachable sigma roots Evar.Set.empty in + let roots = Evd.fold_undefined (fun k _ acc -> Evar.Set.add k acc) sigma0 roots in + let reachable_undefined_evars = reachable sigma roots Evar.Set.empty in let declared_goals, shelved_goals = - get_declared_goals (Evar.Set.diff all_goals solved_goals) constraints state assignments pp_ctx in + get_declared_goals (Evar.Set.diff reachable_undefined_evars solved_goals) constraints state assignments pp_ctx in debug Pp.(fun () -> str "Goals: " ++ prlist_with_sep spc Evar.print declared_goals); debug Pp.(fun () -> str "Shelved Goals: " ++ prlist_with_sep spc Evar.print shelved_goals); -(* wrong: Evd.fold_undefined (fun k _ sigma -> - if Evar.Set.mem k all_goals || Evd.mem sigma0 k then sigma + Evd.fold_undefined (fun k _ sigma -> + if Evar.Set.mem k reachable_undefined_evars then sigma else Evd.remove sigma k - ) sigma*) sigma, + ) sigma sigma, declared_goals, shelved_goals