when renaming, give precedence to recent context entries over old ones

src/coq_elpi_HOAS.ml

@@ -399,7 +399,7 @@ let in_coq_fresh ~id_only =
   let mk_fresh dbl =
     Id.of_string_soft
       (Printf.sprintf "elpi_ctx_entry_%d_" dbl) in
-fun ~depth dbl name ~coq_ctx:{names}->
+fun ~depth dbl name ~names ->
   match in_coq_name ~depth name with
   | Name.Anonymous when id_only -> Name.Name (mk_fresh dbl)
   | Name.Anonymous as x -> x
@@ -409,11 +409,11 @@ fun ~depth dbl name ~coq_ctx:{names}->
 let in_coq_annot ~depth t = Context.make_annot (in_coq_name ~depth t) Sorts.Relevant
 
 let in_coq_fresh_annot_name ~depth ~coq_ctx dbl t =
-  Context.make_annot (in_coq_fresh ~id_only:false ~depth ~coq_ctx dbl t) Sorts.Relevant
+  Context.make_annot (in_coq_fresh ~id_only:false ~depth ~names:coq_ctx.names dbl t) Sorts.Relevant
 
-let in_coq_fresh_annot_id ~depth ~coq_ctx dbl t =
+let in_coq_fresh_annot_id ~depth ~names dbl t =
   let get_name = function Name.Name x -> x | Name.Anonymous -> assert false in
-  Context.make_annot (in_coq_fresh ~id_only:true ~depth ~coq_ctx dbl t |> get_name) Sorts.Relevant
+  Context.make_annot (in_coq_fresh ~id_only:true ~depth ~names dbl t |> get_name) Sorts.Relevant
 
 let unspec2opt = function Elpi.Builtin.Given x -> Some x | Elpi.Builtin.Unspec -> None
 let opt2unspec = function Some x -> Elpi.Builtin.Given x | None -> Elpi.Builtin.Unspec
@@ -874,6 +874,34 @@ module UVMap = struct
       let ruv = UVRawMap.elpi ev (S.get UVRawMap.uvmap s) in
       f ev ruv uv sol acc)
     (S.get UVElabMap.uvmap s) acc
+
+  exception Return of Evar.t
+
+  let rec morally_same_uvar ~depth uv bo =
+    match E.look ~depth bo with
+    | E.Lam x -> morally_same_uvar ~depth:(depth+1) uv x
+    | E.UnifVar(ev,_) -> F.Elpi.equal ev uv
+    | _ -> false
+
+  let host_upto_assignment f s =
+    try
+      UVElabMap.fold (fun ev _ sol _ ->
+        match sol with
+        | None -> () (* the fast lookup can only fail if the uvar was instantiated (as is expanded or pruned)*)
+        | Some sol ->
+            if f ev sol then raise (Return ev) else ())
+      (S.get UVElabMap.uvmap s) ();
+      raise Not_found
+    with Return a -> a
+
+  let host_failsafe elab s =
+    try
+      UVElabMap.host elab (S.get UVElabMap.uvmap s)
+    with Not_found ->
+    try
+      UVRawMap.host elab (S.get UVRawMap.uvmap s)
+    with Not_found ->
+      host_upto_assignment (fun evar bo -> morally_same_uvar ~depth:0 elab bo) s
 
   let remove_host evar s =
     let s = S.update UVRawMap.uvmap s (UVRawMap.remove_host evar) in
@@ -1716,40 +1744,53 @@ let is_global_or_pglobal ~depth t =
 let rec of_elpi_ctx ~calldepth syntactic_constraints depth dbl2ctx state initial_coq_ctx =
 
   let aux coq_ctx depth state t =
-    lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state t in
-
-  let of_elpi_ctx_entry dbl coq_ctx ~depth e state =
+    lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state t
+  in
+  let of_elpi_ctx_entry id dbl coq_ctx ~depth e state =
     match e with
-    | `Decl(name,ty) ->
-        debug Pp.(fun () -> str "decl name: " ++ str(pp2string (P.term depth) name));
+    | `Decl(name_hint,ty) ->
+        debug Pp.(fun () -> str "decl name (hint/actual): " ++ str(pp2string (P.term depth) name_hint) ++ spc () ++ Id.print (Context.binder_name id));
         debug Pp.(fun () -> str "decl ty: " ++ str(pp2string (P.term depth) ty));
-        let id = in_coq_fresh_annot_id ~depth ~coq_ctx dbl name in
         let state, ty, gls = aux coq_ctx depth state ty in
         state, Context.Named.Declaration.LocalAssum(id,ty), gls
-    | `Def(name,ty,bo) ->
-        debug Pp.(fun () -> str "def name: " ++ str(pp2string (P.term depth) name));
+    | `Def(name_hint,ty,bo) ->
+        debug Pp.(fun () -> str "def name (hint/actual): " ++ str(pp2string (P.term depth) name_hint) ++ spc () ++ Id.print (Context.binder_name id));
         debug Pp.(fun () -> str "def ty: " ++ str(pp2string (P.term depth) ty));
         debug Pp.(fun () -> str "def bo: " ++ str(pp2string (P.term depth) bo));
-        let id = in_coq_fresh_annot_id ~depth ~coq_ctx dbl name in
         let state, ty, gl1 = aux coq_ctx depth state ty in
         let state, bo, gl2 = aux coq_ctx depth state bo in
         state, Context.Named.Declaration.LocalDef(id,bo,ty), gl1 @ gl2
   in
-
-  let rec ctx_entries coq_ctx state gls i =
-    if i = depth then state, coq_ctx, List.(concat (rev gls))
+  let of_elpi_ctx_entry_name dbl names ~depth e =
+    match e with
+    | `Decl(name_hint,_) -> in_coq_fresh_annot_id ~depth ~names dbl name_hint
+    | `Def(name_hint,_,_) -> in_coq_fresh_annot_id ~depth ~names dbl name_hint
+  in
+  let rec build_ctx_entry coq_ctx state gls = function
+    | [] -> state, coq_ctx, List.(concat (rev gls))
+    | (i,id,d,e) :: rest ->
+      debug Pp.(fun () -> str "<<< context entry for DBL "++ int i ++ str" at depth" ++ int d);
+      let state, e, gl1 = of_elpi_ctx_entry id i coq_ctx ~depth:d e state in
+      debug Pp.(fun () -> str "<<< context entry for DBL "++ int i ++ str" at depth" ++ int d);
+      let coq_ctx = push_coq_ctx_proof i e coq_ctx in
+      build_ctx_entry coq_ctx state (gl1 :: gls) rest
+  in
+  (* we go from the bottom (most recent addition) to the top in order to
+     give precedence to the name recently introduced *)
+  let rec ctx_entries_names names i =
+    if i < 0 then []
     else (* context entry for the i-th variable *)
       if not (Int.Map.mem i dbl2ctx)
-      then ctx_entries coq_ctx state gls (i+1)
+      then ctx_entries_names names (i - 1)
       else
         let d, e = Int.Map.find i dbl2ctx in
-        debug Pp.(fun () -> str "<<< context entry for DBL "++ int i ++ str" at depth" ++ int d);
-        let state, e, gl1 = of_elpi_ctx_entry i coq_ctx ~depth:d e state in
-        debug Pp.(fun () -> str "context entry >>>");
-        let coq_ctx = push_coq_ctx_proof i e coq_ctx in
-        ctx_entries coq_ctx state (gl1 :: gls) (i+1)
+        let id = of_elpi_ctx_entry_name i names ~depth:d e in
+        let names = Id.Set.add (Context.binder_name id) names in
+        (i,id,d,e) :: ctx_entries_names names (i - 1)
   in
-    ctx_entries initial_coq_ctx state [] 0
+    ctx_entries_names Id.Set.empty (depth-1) |>
+    List.rev |> (* we need to readback the context from top to bottom *)
+    build_ctx_entry initial_coq_ctx state []
 
 (* ***************************************************************** *)
 (* <-- depth -->                                                     *)
@@ -2236,8 +2277,10 @@ let get_goal_ref ~depth syntactic_constraints state t =
      | E.UnifVar(ev,scope) ->
        begin try
          let uv = find_evar ev syntactic_constraints in
-         Open {ctx; evar = UVMap.host uv state; scope; args = U.lp_list_to_list ~depth i}
-       with Not_found -> Not_a_goal
+         let evar = UVMap.host_failsafe uv state in
+         Open {ctx; evar; scope; args = U.lp_list_to_list ~depth i}
+       with Not_found -> 
+         Not_a_goal
        end
      | _ -> Closed_by_side_effect
      end
@@ -3362,7 +3405,8 @@ let get_global_env_current_sigma ~depth hyps constraints state =
 
 let lp2goal ~depth hyps syntactic_constraints state t =
   match get_goal_ref ~depth (E.constraints syntactic_constraints) state t with
-  | Closed_by_side_effect | Not_a_goal -> assert false
+  | Closed_by_side_effect -> assert false
+  | Not_a_goal -> assert false
   | Open {ctx; evar = k; scope; args} ->
     let state, _, changed, gl1 =
       elpi_solution_to_coq_solution ~calldepth:depth syntactic_constraints state in

tests/test_tactic.v

@@ -1,5 +1,21 @@
 From elpi Require Import elpi.
 
+Elpi Tactic double_open.
+Elpi Accumulate lp:{{
+  solve (goal _Ctx _Trigger Type _Proof [] as G) GL :-
+    @no-tc! => refine {{ id _ }} G [G2],
+    coq.ltac.open (refine {{ id _ }}) G2 GL,
+    coq.say G2.
+}}.
+Elpi Typecheck.
+
+Lemma foo (P : Prop) :
+P -> P.
+Proof.
+  elpi double_open.
+  match goal with |- P -> P => idtac end. (* no renaming *)
+Abort.
+
 Elpi Command foo.
 Elpi Print foo.
 Elpi Tactic foobar.