feat(library/noncomputable): add vm_decl.noncomputable_reason (#638)

This exposes whether and why a definition is noncomputable.

library/init/meta/environment.lean

@@ -165,6 +165,12 @@ meta constant trans_for : environment → name → option name
 meta constant decl_olean : environment → name → option string
 /-- `decl_pos env d` returns the source location of d if available. -/
 meta constant decl_pos : environment → name → option pos
+/-- `decl_pos env d` returns the name of a declaration that d inherits
+noncomputability from, or `none` if it is computable.
+
+Note that this also returns `none` on `axiom`s and `constant`s. These can be detected by using
+`environment.get_decl` and `declaration.is_axiom` and `declaration.is_constant`. -/
+meta constant decl_noncomputable_reason : environment → name → option name
 /-- Return the fields of the structure with the given name, or `none` if it is not a structure -/
 meta constant structure_fields : environment → name → option (list name)
 /-- `get_class_attribute_symbols env attr_name` return symbols

src/library/vm/vm_environment.cpp

@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "library/inductive_compiler/add_decl.h"
 #include "library/inductive_compiler/ginductive.h"
 #include "library/inductive_compiler/util.h"
+#include "library/noncomputable.h"
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_option.h"
@@ -276,6 +277,10 @@ vm_obj environment_decl_pos(vm_obj const & env, vm_obj const & n) {
     }
 }
 
+vm_obj environment_decl_noncomputable_reason(vm_obj const & env, vm_obj const & n) {
+    return to_obj(get_noncomputable_reason(to_env(env), to_name(n)));
+}
+
 vm_obj environment_add_namespace(vm_obj const & env, vm_obj const & n) {
     return to_obj(add_namespace(to_env(env), to_name(n)));
 }
@@ -374,6 +379,7 @@ void initialize_vm_environment() {
     DECLARE_VM_BUILTIN(name({"environment", "trans_for"}),              environment_trans_for);
     DECLARE_VM_BUILTIN(name({"environment", "decl_olean"}),             environment_decl_olean);
     DECLARE_VM_BUILTIN(name({"environment", "decl_pos"}),               environment_decl_pos);
+    DECLARE_VM_BUILTIN(name({"environment", "decl_noncomputable_reason"}), environment_decl_noncomputable_reason);
     DECLARE_VM_BUILTIN(name({"environment", "unfold_untrusted_macros"}), environment_unfold_untrusted_macros);
     DECLARE_VM_BUILTIN(name({"environment", "unfold_all_macros"}),      environment_unfold_all_macros);
     DECLARE_VM_BUILTIN(name({"environment", "structure_fields"}),       environment_structure_fields);

tests/lean/noncomputable_reason.lean

@@ -0,0 +1,12 @@
+constant foo : ℕ
+
+noncomputable def bar : ℕ := foo
+
+def baz : ℕ := 0
+
+open tactic
+run_cmd do
+  e ← get_env,
+  trace $ e.decl_noncomputable_reason `foo,
+  trace $ e.decl_noncomputable_reason `bar,
+  trace $ e.decl_noncomputable_reason `baz

tests/lean/noncomputable_reason.lean.expected.out

@@ -0,0 +1,3 @@
+none
+(some foo)
+none