Merge pull request #581 from LPCIC/fix-evar-loss

fix sigma pruning when calling ltac, reachability is not correct

Author: gares

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.

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.

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.

src/coq_elpi_HOAS.ml

@@ -2414,7 +2414,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 =
@@ -2432,13 +2435,14 @@ 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);
   Evd.fold_undefined (fun k _ sigma ->
-    if Evar.Set.mem k all_goals || Evd.mem sigma0 k then sigma
+    if Evar.Set.mem k reachable_undefined_evars then sigma
     else Evd.remove sigma k
     ) sigma sigma,
   declared_goals,