feat(library/init/meta): add helper functions

library/init/meta/base_tactic.lean

@@ -105,6 +105,12 @@ meta_definition returnex (e : exceptional A) : base_tactic S A :=
 | exceptional.exception A f := base_tactic_result.exception A f s
 end
 
+meta_definition returnopt (e : option A) : base_tactic S A :=
+λ s, match e with
+| some a     := base_tactic_result.success a s
+| none       := base_tactic_result.exception A (λ o, to_fmt "failed") s
+end
+
 /- Decorate t's exceptions with msg -/
 meta_definition decorate_ex (msg : format) (t : base_tactic S A) : base_tactic S A :=
 λ s, base_tactic_result.cases_on (t s)

library/init/meta/environment.lean

@@ -32,6 +32,8 @@ meta_constant is_constructor  : environment → name → bool
 meta_constant is_recursor     : environment → name → bool
 /- Return tt iff the given name is a recursive inductive datatype -/
 meta_constant is_recursive    : environment → name → bool
+/- Return the name of the inductive datatype of the given constructor. -/
+meta_constant inductive_type_of : environment → name → option name
 /- Return the constructors of the inductive datatype with the given name -/
 meta_constant constructors_of : environment → name → list name
 /- Return the recursor of the given inductive datatype -/

library/init/meta/name.lean

@@ -53,3 +53,6 @@ attribute [instance] name.has_decidable_eq
 
 meta_definition name_has_ordering [instance] : has_ordering name :=
 has_ordering.mk name.cmp
+
+/- (name.append_after n i) return a name of the form n_i -/
+meta_constant name.append_after : name → nat → name

library/init/meta/tactic.lean

@@ -422,18 +422,22 @@ do u ← mk_meta_univ,
    t ← mk_meta_var (expr.sort u),
    mk_meta_var t
 
-private meta_definition get_arity_aux : expr → tactic nat
+private meta_definition get_pi_arity_aux : expr → tactic nat
 | (expr.pi n bi d b) :=
   do m     ← mk_fresh_name,
      l     ← return (expr.local_const m n bi d),
      new_b ← whnf (expr.instantiate_var b l),
-     r     ← get_arity_aux new_b,
+     r     ← get_pi_arity_aux new_b,
      return (r + 1)
 | _                  := return 0
 
+/- Compute the arity of the given (Pi-)type -/
+meta_definition get_pi_arity (type : expr) : tactic nat :=
+whnf type >>= get_pi_arity_aux
+
 /- Compute the arity of the given function -/
 meta_definition get_arity (fn : expr) : tactic nat :=
-infer_type fn >>= whnf >>= get_arity_aux
+infer_type fn >>= get_pi_arity
 
 meta_definition triv : tactic unit := mk_const `trivial >>= exact
 

src/library/vm/vm_environment.cpp

@@ -102,6 +102,13 @@ vm_obj environment_is_constructor(vm_obj const & env, vm_obj const & n) {
     return mk_vm_bool(static_cast<bool>(inductive::is_intro_rule(to_env(env), to_name(n))));
 }
 
+vm_obj environment_inductive_type_of(vm_obj const & env, vm_obj const & n) {
+    if (auto I = inductive::is_intro_rule(to_env(env), to_name(n)))
+        return mk_vm_some(to_obj(*I));
+    else
+        return mk_vm_none();
+}
+
 vm_obj environment_is_recursor(vm_obj const & env, vm_obj const & n) {
     return mk_vm_bool(static_cast<bool>(inductive::is_elim_rule(to_env(env), to_name(n))));
 }
@@ -195,6 +202,7 @@ void initialize_vm_environment() {
     DECLARE_VM_BUILTIN(name({"environment", "is_constructor"}),        environment_is_constructor);
     DECLARE_VM_BUILTIN(name({"environment", "is_recursor"}),           environment_is_recursor);
     DECLARE_VM_BUILTIN(name({"environment", "is_recursive"}),          environment_is_recursive);
+    DECLARE_VM_BUILTIN(name({"environment", "inductive_type_of"}),     environment_inductive_type_of);
     DECLARE_VM_BUILTIN(name({"environment", "constructors_of"}),       environment_constructors_of);
     DECLARE_VM_BUILTIN(name({"environment", "recursor_of"}),           environment_recursor_of);
     DECLARE_VM_BUILTIN(name({"environment", "inductive_num_params"}),  environment_inductive_num_params);

src/library/vm/vm_name.cpp

@@ -69,6 +69,10 @@ vm_obj name_lex_cmp(vm_obj const & o1, vm_obj const & o2) {
     return int_to_ordering(cmp(to_name(o1), to_name(o2)));
 }
 
+vm_obj name_append_after(vm_obj const & n, vm_obj const & i) {
+    return to_obj(to_name(n).append_after(force_to_unsigned(i, 0)));
+}
+
 void initialize_vm_name() {
     DECLARE_VM_BUILTIN(name({"name", "anonymous"}),        name_anonymous);
     DECLARE_VM_BUILTIN(name({"name", "mk_string"}),        name_mk_string);
@@ -76,6 +80,7 @@ void initialize_vm_name() {
     DECLARE_VM_BUILTIN(name({"name", "has_decidable_eq"}), name_has_decidable_eq);
     DECLARE_VM_BUILTIN(name({"name", "cmp"}),              name_cmp);
     DECLARE_VM_BUILTIN(name({"name", "lex_cmp"}),          name_lex_cmp);
+    DECLARE_VM_BUILTIN(name({"name", "append_after"}),     name_append_after);
     DECLARE_VM_CASES_BUILTIN(name({"name", "cases_on"}),   name_cases_on);
 }