From b70061097644fb3eb7bc7f961a80229341e24884 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Tue, 28 Nov 2023 15:28:34 +0100
Subject: [PATCH] API: coq.ltac.fresh-id

---
 Changelog.md             |  1 +
 coq-builtin.elpi         |  3 +++
 src/coq_elpi_builtins.ml | 14 ++++++++++++++
 tests/test_tactic.v      | 26 ++++++++++++++++++++++++++
 4 files changed, 44 insertions(+)

diff --git a/Changelog.md b/Changelog.md
index 00d7a5b15..02537f8b0 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -10,6 +10,7 @@
 - New `tc-priority`, contains the priority of an instance and if the priority
   has been given by the user or computed by `coq`
 - Change `tc-instance`, now the type is `gref -> tc-priority -> tc-instance` i.e. the priority is not an integer anymore
+- New `coq.ltac.fresh-id` to generate fresh names in the proof context
 
 ### Apps 
 - New `tc` app providing an implementation of a type class solver written in elpi.
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index 3e4ddc084..3af4898eb 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -1572,6 +1572,9 @@ external pred coq.ltac.call-ltac1 i:any, i:goal, o:list sealed-goal.
 % 
 external pred coq.ltac.id-free? i:id, i:goal.
 
+% [coq.ltac.fresh-id Default Ty FreshID] TODO
+external pred coq.ltac.fresh-id i:id, i:term, o:id.
+
 % -- Coq's options system --------------------------------------------
 
 % Coq option value
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index f1b173f92..85ab3d366 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -3789,6 +3789,20 @@ an elpi tactic.|})))),
      else raise No_clause)),
   DocAbove);
 
+  MLCode(Pred("coq.ltac.fresh-id",
+  In(B.unspec id, "Default",
+  CIn(B.unspecC term, "Ty",
+  Out(id,"FreshID",
+  Read(proof_context, "TODO")))),
+  (fun id ty _ ~depth proof_context  _ _ ->
+     let id = match id with Unspec -> "x" | Given x -> x in
+     let id =
+       match ty with
+       | Unspec -> Namegen.next_ident_away (Names.Id.of_string_soft id) proof_context.names
+       | Given ty -> Namegen.next_name_away_with_default_using_types id Name.Anonymous proof_context.names ty in
+     !: (Id.to_string id))),
+  DocAbove);
+
   LPDoc "-- Coq's options system --------------------------------------------";
 
   MLData goption;
diff --git a/tests/test_tactic.v b/tests/test_tactic.v
index d5a56ad20..fb88cf908 100644
--- a/tests/test_tactic.v
+++ b/tests/test_tactic.v
@@ -389,3 +389,29 @@ Goal forall n, n + 1 = 1.
     trivial.
     match goal with |- S m + 1 = 1 => idtac end.
 Abort.  
+
+
+
+Elpi Tactic fresh1.
+Elpi Accumulate lp:{{
+  solve (goal _ _ {{ forall _ : lp:Ty, _ }} _ _ as G) GL :-
+    coq.ltac.fresh-id "x" Ty ID,
+    coq.id->name ID N,
+    refine (fun N _ _) G GL.
+}}.
+Elpi Typecheck.
+Goal forall x z y, x = 1 + y + z.
+intros x x0.
+elpi fresh1.
+Check x1.
+Abort.
+
+Implicit Type (w : nat).
+
+Goal forall x z y, x = 1 + y + z.
+intros ??.
+elpi fresh1.
+Check w.
+Abort.
+
+