From bd7138349a6417d0af110d3deeb0ef3ffae49148 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 5 Jun 2018 16:28:12 -0700
Subject: [PATCH] chore(library/init/meta/pexpr): remove pexpr primitives

---
 library/init/meta/pexpr.lean | 19 ------------
 src/library/vm/vm_pexpr.cpp  | 57 ------------------------------------
 2 files changed, 76 deletions(-)

diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean
index 8fc648c855..5fa8854050 100644
--- a/library/init/meta/pexpr.lean
+++ b/library/init/meta/pexpr.lean
@@ -11,25 +11,6 @@ universe u
 @[reducible] meta def pexpr := expr ff
 protected meta constant pexpr.of_expr  : expr → pexpr
 
-meta constant pexpr.is_placeholder : pexpr → bool
-meta constant pexpr.mk_placeholder : pexpr
-meta constant pexpr.mk_field_macro : pexpr → name → pexpr
-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       : option name := none)
-(field_names  : list name)
-(field_values : list pexpr)
-(sources      : list pexpr := [])
-
-/-- Create a structure instance expression. -/
-meta constant pexpr.mk_structure_instance : structure_instance_info → 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 e8c46d975d..d42e4c1f88 100644
--- a/src/library/vm/vm_pexpr.cpp
+++ b/src/library/vm/vm_pexpr.cpp
@@ -21,65 +21,8 @@ vm_obj pexpr_of_expr(vm_obj const & e) {
     return to_obj(mk_as_is(to_expr(e)));
 }
 
-vm_obj pexpr_is_placeholder(vm_obj const & e) {
-    return mk_vm_bool(is_placeholder(to_expr(e)));
-}
-
-vm_obj pexpr_mk_placeholder() {
-    return to_obj(mk_expr_placeholder());
-}
-
-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)));
-}
-
-vm_obj pexpr_is_choice_macro(vm_obj const & e) {
-    return mk_vm_bool(is_choice(to_expr(e)));
-}
-
-vm_obj pexpr_mk_structure_instance(vm_obj const & info) {
-    name struct_name;
-    buffer<name> field_names;
-    buffer<expr> field_values;
-    buffer<expr> sources;
-    if (!is_none(cfield(info, 0))) {
-        struct_name = to_name(get_some_value(cfield(info, 0)));
-    }
-    to_buffer_name(cfield(info, 1), field_names);
-    to_buffer_expr(cfield(info, 2), field_values);
-    to_buffer_expr(cfield(info, 3), sources);
-    return to_obj(mk_structure_instance(struct_name, field_names, field_values, sources));
-}
-
-vm_obj pexpr_get_structure_instance_info(vm_obj const & e) {
-    if (!is_structure_instance(to_expr(e))) {
-        return mk_vm_none();
-    }
-    auto info = get_structure_instance_info(to_expr(e));
-    optional<name> opt_struct_name;
-    if (info.m_struct_name) {
-        opt_struct_name = info.m_struct_name;
-    }
-    return mk_vm_some(mk_vm_constructor(0, to_obj(opt_struct_name), to_obj(info.m_field_names),
-                                        to_obj(info.m_field_values), to_obj(info.m_sources)));
-}
-
 void initialize_vm_pexpr() {
     DECLARE_VM_BUILTIN(name({"pexpr", "of_expr"}),        pexpr_of_expr);
-    DECLARE_VM_BUILTIN(name({"pexpr", "is_placeholder"}), pexpr_is_placeholder);
-    DECLARE_VM_BUILTIN(name({"pexpr", "mk_placeholder"}), pexpr_mk_placeholder);
-
-    DECLARE_VM_BUILTIN(name("pexpr", "mk_explicit"),      pexpr_mk_explicit);
-    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", "mk_structure_instance"), pexpr_mk_structure_instance);
-    DECLARE_VM_BUILTIN(name("pexpr", "get_structure_instance_info"), pexpr_get_structure_instance_info);
 }
 
 void finalize_vm_pexpr() {