From 3062c6feb793dd125f48cb3a021f55eb78b40a02 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 22 Aug 2017 16:52:12 +0200
Subject: [PATCH] feat(init/meta): expose `pexpr.get_structure_instance_info`

---
 library/init/meta/pexpr.lean |  9 +++++++++
 src/library/vm/vm_pexpr.cpp  | 17 +++++++++++++++++
 2 files changed, 26 insertions(+)

diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean
index 052dcc61a7..a05ba3321c 100644
--- a/library/init/meta/pexpr.lean
+++ b/library/init/meta/pexpr.lean
@@ -18,6 +18,15 @@ meta constant pexpr.mk_explicit : pexpr → pexpr
 /-- Choice macros are used to implement overloading. -/
 meta constant pexpr.is_choice_macro : pexpr → bool
 
+/-- Information about unelaborated structure instance expressions. -/
+meta structure structure_instance_info :=
+(struct       : name)
+(source       : option pexpr)
+(field_names  : list name)
+(field_values : list pexpr)
+
+meta constant pexpr.get_structure_instance_info : pexpr → option structure_instance_info
+
 meta class has_to_pexpr (α : Sort u) :=
 (to_pexpr : α → pexpr)
 
diff --git a/src/library/vm/vm_pexpr.cpp b/src/library/vm/vm_pexpr.cpp
index 85f9bd25c5..0b0b8ebb4f 100644
--- a/src/library/vm/vm_pexpr.cpp
+++ b/src/library/vm/vm_pexpr.cpp
@@ -11,7 +11,10 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_name.h"
+#include "library/vm/vm_list.h"
+#include "library/vm/vm_option.h"
 #include "frontends/lean/util.h"
+#include "frontends/lean/structure_instance.h"
 
 namespace lean {
 vm_obj pexpr_of_expr(vm_obj const & e) {
@@ -34,6 +37,19 @@ vm_obj pexpr_is_choice_macro(vm_obj const & e) {
     return mk_vm_bool(is_choice(to_expr(e)));
 }
 
+vm_obj pexpr_get_structure_instance_info(vm_obj const & e) {
+    if (!is_structure_instance(to_expr(e))) {
+        return mk_vm_none();
+    }
+    name struct_name;
+    optional<expr> source;
+    buffer<name> field_names;
+    buffer<expr> field_values;
+
+    get_structure_instance_info(to_expr(e), struct_name, source, field_names, field_values);
+    return mk_vm_some(mk_vm_constructor(0, to_obj(struct_name), to_obj(source), to_obj(field_names), to_obj(field_values)));
+}
+
 void initialize_vm_pexpr() {
     DECLARE_VM_BUILTIN(name({"pexpr", "of_expr"}),        pexpr_of_expr);
     DECLARE_VM_BUILTIN(name({"pexpr", "mk_placeholder"}), pexpr_mk_placeholder);
@@ -42,6 +58,7 @@ void initialize_vm_pexpr() {
     DECLARE_VM_BUILTIN(name("pexpr", "mk_field_macro"),   pexpr_mk_field_macro);
 
     DECLARE_VM_BUILTIN(name("pexpr", "is_choice_macro"),  pexpr_is_choice_macro);
+    DECLARE_VM_BUILTIN(name("pexpr", "get_structure_instance_info"), pexpr_get_structure_instance_info);
 }
 
 void finalize_vm_pexpr() {