Binding primitives to generate fresh variables.

3 files changed, 71 insertions, 1 deletions

diff --git a/_CoqProject b/_CoqProject
index 4116d17554..ffe1dda032 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -36,6 +36,7 @@ theories/Control.v
 theories/Message.v
 theories/Constr.v
 theories/Pattern.v
+theories/Fresh.v
 theories/Std.v
 theories/Notations.v
 theories/Ltac2.v
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 5b752840a4..4a4f9afd88 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -66,7 +66,8 @@ let of_rec_declaration (nas, ts, cs) =
   Value.of_array Value.of_constr ts,
   Value.of_array Value.of_constr cs)
 
-let val_valexpr = Val.create "ltac2:valexpr"
+let val_valexpr : valexpr Val.typ = Val.create "ltac2:valexpr"
+let val_free : Id.Set.t Val.typ = Val.create "ltac2:free"
 
 (** Stdlib exceptions *)
 
@@ -593,6 +594,43 @@ let prm_check_interrupt : ml_tactic = function
 | [_] -> Proofview.tclCHECKINTERRUPT >>= fun () -> return v_unit
 | _ -> assert false
 
+(** Fresh *)
+
+let prm_free_union : ml_tactic = function
+| [set1; set2] ->
+  let set1 = Value.to_ext val_free set1 in
+  let set2 = Value.to_ext val_free set2 in
+  let ans = Id.Set.union set1 set2 in
+  return (Value.of_ext val_free ans)
+| _ -> assert false
+
+let prm_free_of_ids : ml_tactic = function
+| [ids] ->
+  let ids = Value.to_list Value.to_ident ids in
+  let free = List.fold_right Id.Set.add ids Id.Set.empty in
+  return (Value.of_ext val_free free)
+| _ -> assert false
+
+let prm_free_of_constr : ml_tactic = function
+| [c] ->
+  let c = Value.to_constr c in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let rec fold accu c = match EConstr.kind sigma c with
+  | Constr.Var id -> Id.Set.add id accu
+  | _ -> EConstr.fold sigma fold accu c
+  in
+  let ans = fold Id.Set.empty c in
+  return (Value.of_ext val_free ans)
+| _ -> assert false
+
+let prm_fresh : ml_tactic = function
+| [avoid; id] ->
+  let avoid = Value.to_ext val_free avoid in
+  let id = Value.to_ident id in
+  let nid = Namegen.next_ident_away_from id (fun id -> Id.Set.mem id avoid) in
+  return (Value.of_ident nid)
+| _ -> assert false
+
 (** Registering *)
 
 let () = Tac2env.define_primitive (pname "print") prm_print
@@ -656,6 +694,11 @@ let () = Tac2env.define_primitive (pname "abstract") prm_abstract
 let () = Tac2env.define_primitive (pname "time") prm_time
 let () = Tac2env.define_primitive (pname "check_interrupt") prm_check_interrupt
 
+let () = Tac2env.define_primitive (pname "fresh_fresh") prm_fresh
+let () = Tac2env.define_primitive (pname "fresh_free_union") prm_free_union
+let () = Tac2env.define_primitive (pname "fresh_free_of_ids") prm_free_of_ids
+let () = Tac2env.define_primitive (pname "fresh_free_of_constr") prm_free_of_constr
+
 (** ML types *)
 
 let constr_flags () =
diff --git a/theories/Fresh.v b/theories/Fresh.v
new file mode 100644
index 0000000000..5e876bb077
--- /dev/null
+++ b/theories/Fresh.v
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+Module Free.
+
+Ltac2 Type t.
+(** Type of sets of free variables *)
+
+Ltac2 @ external union : t -> t -> t := "ltac2" "fresh_free_union".
+
+Ltac2 @ external of_ids : ident list -> t := "ltac2" "fresh_free_of_ids".
+
+Ltac2 @ external of_constr : constr -> t := "ltac2" "fresh_free_of_constr".
+
+End Free.
+
+Ltac2 @ external fresh : Free.t -> ident -> ident := "ltac2" "fresh_fresh".
+(** Generate a fresh identifier with the given base name which is not a
+    member of the provided set of free variables. *)