From 00aef04b81f8df9d8801a6b32aa95e4327cfe462 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 1 Jun 2017 17:04:21 -0700
Subject: [PATCH] feat(library/init/meta/rec_util): add
 mk_constructors_fresh_names

@Armael @jroesch this commit implements the
`mk_constructors_fresh_names` tactic.
The new test file has a few examples.
---
 library/init/meta/rec_util.lean               | 51 +++++++++++++++++++
 tests/lean/mk_constructor_fresh_names.lean    | 24 +++++++++
 ..._constructor_fresh_names.lean.expected.out |  3 ++
 3 files changed, 78 insertions(+)
 create mode 100644 tests/lean/mk_constructor_fresh_names.lean
 create mode 100644 tests/lean/mk_constructor_fresh_names.lean.expected.out

diff --git a/library/init/meta/rec_util.lean b/library/init/meta/rec_util.lean
index 487350e1de..f7e00acfe1 100644
--- a/library/init/meta/rec_util.lean
+++ b/library/init/meta/rec_util.lean
@@ -67,4 +67,55 @@ do env ← get_env,
    cs  ← return $ env.constructors_of I,
    mk_constructors_arg_names_aux cs p 1 []
 
+private meta def mk_fresh_arg_name_aux : name → nat → name_set → tactic (name × name_set)
+| n i s :=
+  do r ← get_unused_name n (some i),
+     if s.contains r then
+        mk_fresh_arg_name_aux n (i+1) s
+     else
+        return (r, s.insert r)
+
+private meta def mk_fresh_arg_name (n : name) (s : name_set) : tactic (name × name_set) :=
+do r ← get_unused_name n,
+   if s.contains r then
+      mk_fresh_arg_name_aux n 1 s
+   else
+      return (r, s.insert r)
+
+private meta def mk_constructor_fresh_names_aux : nat → expr → name_set → tactic (list name × name_set)
+| nparams ty s := do
+  ty ← whnf ty,
+  match ty with
+  | expr.pi n bi d b :=
+     if nparams = 0 then do {
+       (n', s') ← mk_fresh_arg_name n s,
+       x        ← mk_local' n' bi d,
+       let ty' := b.instantiate_var x,
+       (ns, s'') ← mk_constructor_fresh_names_aux 0 ty' s',
+       return (n'::ns, s'')
+     } else do {
+       x        ← mk_local' n bi d,
+       let ty' := b.instantiate_var x,
+       mk_constructor_fresh_names_aux (nparams - 1) ty' s
+     }
+  | _ := return ([], s)
+  end
+
+meta def mk_constructor_fresh_names (nparams : nat) (c : name) (s : name_set) : tactic (list name × name_set) :=
+do d    ← get_decl c,
+   let t := d.type,
+   mk_constructor_fresh_names_aux nparams t s
+
+private meta def mk_constructors_fresh_names_aux : nat → list name → name_set → list (list name) → tactic (list (list name))
+| np []      s r := return (list.reverse r)
+| np (c::cs) s r := do
+  (ns, s') ← mk_constructor_fresh_names np c s,
+  mk_constructors_fresh_names_aux np cs s' (ns::r)
+
+meta def mk_constructors_fresh_names (I : name) : tactic (list (list name)) :=
+do env ← get_env,
+   let cs := env.constructors_of I,
+   let nparams := env.inductive_num_params I,
+   mk_constructors_fresh_names_aux nparams cs mk_name_set []
+
 end tactic
diff --git a/tests/lean/mk_constructor_fresh_names.lean b/tests/lean/mk_constructor_fresh_names.lean
new file mode 100644
index 0000000000..2e69904373
--- /dev/null
+++ b/tests/lean/mk_constructor_fresh_names.lean
@@ -0,0 +1,24 @@
+open tactic
+
+example (fst fst_1 : nat) : fst = fst :=
+by do
+  ns ← mk_constructors_fresh_names `prod,
+  trace ns, -- [[fst_2, snd]]
+  constructor
+
+example (a : nat) : a = a :=
+by do
+  ns ← mk_constructors_fresh_names `acc,
+  trace ns, -- [[x, a_1]
+  constructor
+
+inductive Foo
+| mk₁ (a b c : nat)  : Foo
+| mk₂ (d e : bool)   : Foo
+| mk₃ (f g : Foo)    : Foo
+
+example (a d d_1 e : bool) : a = a :=
+by do
+  ns ← mk_constructors_fresh_names `Foo,
+  trace ns, -- [[a_1, b, c], [d_2, e_1], [f, g]]
+  constructor
diff --git a/tests/lean/mk_constructor_fresh_names.lean.expected.out b/tests/lean/mk_constructor_fresh_names.lean.expected.out
new file mode 100644
index 0000000000..cd0e732033
--- /dev/null
+++ b/tests/lean/mk_constructor_fresh_names.lean.expected.out
@@ -0,0 +1,3 @@
+[[fst_2, snd]]
+[[x, a_1]]
+[[a_1, b, c], [d_2, e_1], [f, g]]