feat(library/bin_app): uniform foldr, add helper methods for synthesizing recursive functions

foldr combinator is used to define brec_on recursor.
It is easier to access the brec_on "dictionary" if the representation is
uniform.

library/init/meta/mk_dec_eq_instance.lean

@@ -8,6 +8,7 @@ Helper tactic for showing that a type has decidable equality.
 prelude
 import init.meta.contradiction_tactic init.meta.constructor_tactic
 import init.meta.injection_tactic init.meta.relation_tactics
+import init.meta.rec_util
 
 namespace tactic
 open expr environment list
@@ -45,27 +46,6 @@ do lhs_type ← infer_type lhs,
      f ← pp dec_type,
      fail $ to_fmt "mk_dec_eq_instance failed, failed to generate instance for" ++ format.nest 2 (format.line ++ f) }
 
-private meta_definition is_rec_arg (I_name : name) (e : expr) : tactic bool :=
-do t ← infer_type e,
-   return $ is_constant_of (get_app_fn t) I_name
-
-/- Auxiliary function for using brec_on "dictionary" -/
-private meta_definition mk_rec_inst_aux : expr → nat → tactic expr
-| F 0     := do
-   F' ← mk_app `prod.pr1 [F],
-   F_type ← infer_type F' >>= whnf,
-   if is_pi F_type = tt
-   then return F'
-   else mk_app `prod.pr1 [F']
-| F (n+1) := do
-  F' ← mk_app `prod.pr2 [F],
-  mk_rec_inst_aux F' n
-
-/- Use brec_on F_name (dictionary) argument to create an decidable_eq instance for (i+1)-th recursive argument. -/
-private meta_definition mk_rec_inst (F_name : name) (i : nat) : tactic expr :=
-do F ← get_local F_name,
-   mk_rec_inst_aux F i
-
 /- Target is of the form (decidable (C ... = C ...)) where C is a constructor -/
 private meta_definition dec_eq_same_constructor (I_name : name) (F_name : name) (num_rec : nat) : tactic unit :=
 do
@@ -78,10 +58,10 @@ do
     rhs_list : list expr ← return $ get_app_args rhs,
     when (length lhs_list ≠ length rhs_list) (fail "mk_dec_eq_instance failed, constructor applications have different number of arguments"),
     (lhs_arg,  rhs_arg) ← find_next_target lhs_list rhs_list,
-    rec ← is_rec_arg I_name lhs_arg,
+    rec ← is_type_app_of lhs_arg I_name,
     inst ← if rec = tt
     then do {
-      inst_fn : expr ← mk_rec_inst F_name num_rec,
+      inst_fn : expr ← mk_brec_on_rec_value F_name num_rec,
       return $ inst_fn rhs_arg }
     else do {
       mk_dec_eq_for lhs_arg rhs_arg

library/init/meta/rec_util.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+Helper tactic for showing that a type has decidable equality.
+-/
+prelude
+import init.meta.tactic
+
+namespace tactic
+open expr
+
+/- Return tt iff e's type is of the form `(I_name ...)` -/
+meta_definition is_type_app_of (e : expr) (I_name : name) : tactic bool :=
+do t ← infer_type e,
+   return $ is_constant_of (get_app_fn t) I_name
+
+/- Auxiliary function for using brec_on "dictionary" -/
+private meta_definition mk_rec_inst_aux : expr → nat → tactic expr
+| F 0     := do
+  P ← mk_app `prod.pr1 [F],
+  mk_app `prod.pr1 [P]
+| F (n+1) := do
+  F' ← mk_app `prod.pr2 [F],
+  mk_rec_inst_aux F' n
+
+/- Construct brec_on "recursive value". F_name is the name of the brec_on "dictionary".
+   Type of the F_name hypothesis should be of the form (below (C ...)) where C is a constructor.
+   The result is the "recursive value" for the (i+1)-th recursive value of the constructor C. -/
+meta_definition mk_brec_on_rec_value (F_name : name) (i : nat) : tactic expr :=
+do F ← get_local F_name,
+   mk_rec_inst_aux F i
+
+meta_definition constructor_num_fields (c : name) : tactic nat :=
+do env     ← get_env,
+   decl    ← returnex $ environment.get env c,
+   ctype   ← return $ declaration.type decl,
+   arity   ← get_pi_arity ctype,
+   I       ← returnopt $ environment.inductive_type_of env c,
+   nparams ← return (environment.inductive_num_params env I),
+   return $ arity - nparams
+
+private meta_definition mk_name_list_aux : name → nat → nat → list name → list name × nat
+| p i 0     l := (list.reverse l, i)
+| p i (j+1) l := mk_name_list_aux p (i+1) j (mk_num_name p i :: l)
+
+private meta_definition mk_name_list (p : name) (i : nat) (n : nat) : list name × nat :=
+mk_name_list_aux p i n []
+
+/- Return a list of names of the form [p.i, ..., p.{i+n}] where n is
+   the number of fields of the constructor c -/
+meta_definition mk_constructor_arg_names (c : name) (p : name) (i : nat) : tactic (list name × nat) :=
+do nfields ← constructor_num_fields c,
+   return $ mk_name_list p i nfields
+
+private meta_definition mk_constructors_arg_names_aux : list name → name → nat → list (list name) → tactic (list (list name))
+| []      p i r := return (list.reverse r)
+| (c::cs) p i r := do
+  v : list name × nat ← mk_constructor_arg_names c p i,
+  match v with (l, i') := mk_constructors_arg_names_aux cs p i' (l :: r) end
+
+/- Given an inductive datatype I with k constructors and where constructor i has n_i fields,
+   return the list [[p.1, ..., p.n_1], [p.{n_1 + 1}, ..., p.{n_1 + n_2}], ..., [..., p.{n_1 + ... + n_k}]] -/
+meta_definition mk_constructors_arg_names (I : name) (p : name) : tactic (list (list name)) :=
+do env ← get_env,
+   cs  ← return $ environment.constructors_of env I,
+   mk_constructors_arg_names_aux cs p 1 []
+
+end tactic

src/library/bin_app.h

@@ -13,15 +13,14 @@ bool is_bin_app(expr const & t, expr const & f);
 /** \brief Return true iff \c t is of the form <tt>((f s1) s2)</tt>, if the result is true, then store a1 -> lhs, a2 -> rhs */
 bool is_bin_app(expr const & t, expr const & f, expr & lhs, expr & rhs);
 
-/**
-   \brief Return unit if <tt>num_args == 0</tt>, args[0] if <tt>num_args == 1</tt>, and
-   <tt>(op args[0] (op args[1] (op ... )))</tt>
-*/
+/** \brief Return unit if <tt>num_args == 0</tt>, args[0] if <tt>num_args == 1</tt>, and
+    <tt>(op args[0] (op args[1] (op ... )))</tt> */
 expr mk_bin_rop(expr const & op, expr const & unit, unsigned num_args, expr const * args);
 expr mk_bin_rop(expr const & op, expr const & unit, std::initializer_list<expr> const & l);
 
+/** \brief Version of foldr that only uses unit when num_args == 0 */
 template<typename MkBin, typename MkUnit>
-expr foldr(MkBin && mkb, MkUnit && mku, unsigned num_args, expr const * args) {
+expr foldr_compact(MkBin && mkb, MkUnit && mku, unsigned num_args, expr const * args) {
     if (num_args == 0) {
         return mku();
     } else {
@@ -35,10 +34,20 @@ expr foldr(MkBin && mkb, MkUnit && mku, unsigned num_args, expr const * args) {
     }
 }
 
-/**
-   \brief Return unit if <tt>num_args == 0</tt>, args[0] if <tt>num_args == 1</tt>, and
-   <tt>(op ... (op (op args[0] args[1]) args[2]) ...)</tt>
-*/
+/** \brief Version of foldr that only uses unit when num_args == 0 */
+template<typename MkBin, typename MkUnit>
+expr foldr(MkBin && mkb, MkUnit && mku, unsigned num_args, expr const * args) {
+    expr r = mku();
+    unsigned i = num_args;
+    while (i > 0) {
+        --i;
+        r = mkb(args[i], r);
+    }
+    return r;
+}
+
+/** \brief Return unit if <tt>num_args == 0</tt>, args[0] if <tt>num_args == 1</tt>, and
+    <tt>(op ... (op (op args[0] args[1]) args[2]) ...)</tt> */
 expr mk_bin_lop(expr const & op, expr const & unit, unsigned num_args, expr const * args);
 expr mk_bin_lop(expr const & op, expr const & unit, std::initializer_list<expr> const & l);
 }