API: coq.ltac.fresh-id

Author: gares

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.

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

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;

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.
+
+