feat(init/meta/{environment,pexpr}): expose some structure APIs

library/init/meta/environment.lean

@@ -80,6 +80,8 @@ 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
+/- 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)
 open expr
 
 meta constant unfold_untrusted_macros : environment → expr → expr

library/init/meta/pexpr.lean

@@ -22,6 +22,8 @@ meta constant pexpr.pos : pexpr → option pos
 meta constant pexpr.mk_quote_macro : pexpr → pexpr
 meta constant pexpr.mk_prenum_macro : nat → pexpr
 meta constant pexpr.mk_string_macro : string → pexpr
+meta constant pexpr.mk_field_macro : pexpr → name → pexpr
+meta constant pexpr.mk_explicit : pexpr → pexpr
 
 meta constant pexpr.to_string : pexpr → string
 meta instance : has_to_string pexpr :=

src/library/vm/vm_environment.cpp

@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_exceptional.h"
 #include "library/vm/vm_list.h"
 #include "library/vm/vm_pos_info.h"
+#include "frontends/lean/structure_cmd.h"
 
 namespace lean {
 struct vm_environment : public vm_external {
@@ -216,6 +217,14 @@ vm_obj environment_is_namespace(vm_obj const & env, vm_obj const & n) {
     return mk_vm_bool(is_namespace(to_env(env), to_name(n)));
 }
 
+vm_obj environment_structure_fields(vm_obj const & env, vm_obj const & n) {
+    try {
+        return mk_vm_some(to_obj(get_structure_fields(to_env(env), to_name(n))));
+    } catch (exception &) {
+        return mk_vm_none();
+    }
+}
+
 /*
 structure projection_info :=
 (cname : name)
@@ -263,6 +272,7 @@ void initialize_vm_environment() {
     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", "unfold_untrusted_macros"}), environment_unfold_untrusted_macros);
+    DECLARE_VM_BUILTIN(name({"environment", "structure_fields"}),      environment_structure_fields);
 }
 
 void finalize_vm_environment() {

src/library/vm/vm_pexpr.cpp

@@ -8,14 +8,17 @@ Author: Leonardo de Moura
 #include "kernel/scope_pos_info_provider.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
+#include "library/quote.h"
+#include "library/string.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_expr.h"
+#include "library/vm/vm_name.h"
 #include "library/vm/vm_string.h"
 #include "library/vm/vm_option.h"
 #include "library/vm/vm_pos_info.h"
-#include "library/quote.h"
 #include "frontends/lean/prenum.h"
-#include "library/string.h"
+#include "frontends/lean/structure_cmd.h"
+#include "frontends/lean/util.h"
 
 namespace lean {
 vm_obj pexpr_of_expr(vm_obj const & e) {
@@ -58,6 +61,14 @@ vm_obj pexpr_mk_string_macro(vm_obj const & s) {
     return to_obj(from_string(to_string(s)));
 }
 
+vm_obj pexpr_mk_explicit(vm_obj const & e) {
+    return to_obj(mk_explicit(to_expr(e)));
+}
+
+vm_obj pexpr_mk_field_macro(vm_obj const & e, vm_obj const & fname) {
+    return to_obj(mk_field_notation(to_expr(e), to_name(fname)));
+}
+
 void initialize_vm_pexpr() {
     DECLARE_VM_BUILTIN(name({"pexpr", "subst"}),          expr_subst);
     DECLARE_VM_BUILTIN(name({"pexpr", "of_expr"}),        pexpr_of_expr);
@@ -71,6 +82,8 @@ void initialize_vm_pexpr() {
     DECLARE_VM_BUILTIN(name("pexpr", "mk_quote_macro"),   pexpr_mk_quote_macro);
     DECLARE_VM_BUILTIN(name("pexpr", "mk_prenum_macro"),  pexpr_mk_prenum_macro);
     DECLARE_VM_BUILTIN(name("pexpr", "mk_string_macro"),  pexpr_mk_string_macro);
+    DECLARE_VM_BUILTIN(name("pexpr", "mk_explicit"),      pexpr_mk_explicit);
+    DECLARE_VM_BUILTIN(name("pexpr", "mk_field_macro"),   pexpr_mk_field_macro);
 }
 
 void finalize_vm_pexpr() {