refactor(init/meta): move macro creation defs from expr to pexpr

library/init/meta/expr.lean

@@ -41,9 +41,6 @@ meta constant expr.macro_def_name (d : macro_def) : name
 meta def expr.mk_var (n : nat) : expr :=
 expr.var (unsigned.of_nat n)
 
-meta constant expr.mk_quote_macro : expr → expr
-meta constant expr.mk_prenum_macro : nat → expr
-meta constant expr.mk_string_macro : string → expr
 /- Choice macros are used to implement overloading. -/
 meta constant expr.is_choice_macro : expr → bool
 

library/init/meta/pexpr.lean

@@ -17,6 +17,10 @@ protected meta constant pexpr.to_raw_expr : pexpr → expr
 protected meta constant pexpr.of_raw_expr : expr → pexpr
 meta constant pexpr.mk_placeholder : pexpr
 
+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.to_string : pexpr → string
 meta instance : has_to_string pexpr :=
 ⟨pexpr.to_string⟩

library/init/meta/quote.lean

@@ -14,14 +14,14 @@ meta class has_quote (α : Type) :=
 @[inline] meta def quote {α : Type} [has_quote α] : α → pexpr :=
 has_quote.quote
 
-meta instance : has_quote nat := ⟨pexpr.of_raw_expr ∘ expr.mk_prenum_macro⟩
+meta instance : has_quote nat := ⟨pexpr.mk_prenum_macro⟩
+@[priority std.priority.default + 1]
+meta instance : has_quote string := ⟨pexpr.mk_string_macro⟩
+meta instance : has_quote pexpr := ⟨pexpr.mk_quote_macro⟩
 
 meta instance : has_quote char :=
 ⟨λ ⟨n, pr⟩, ``(char.of_nat %%(quote n))⟩
 
-@[priority std.priority.default + 1]
-meta instance : has_quote string := ⟨pexpr.of_raw_expr ∘ expr.mk_string_macro⟩
-
 meta instance : has_quote unsigned :=
 ⟨λ ⟨n, pr⟩, ``(unsigned.of_nat %%(quote n))⟩
 
@@ -32,9 +32,6 @@ meta def name.quote : name → pexpr
 
 meta instance : has_quote name := ⟨name.quote⟩
 
---meta instance : has_quote expr  := ⟨expr.mk_quote_macro⟩
-meta instance : has_quote pexpr := ⟨pexpr.of_raw_expr ∘ expr.mk_quote_macro ∘ pexpr.to_raw_expr⟩
-
 private meta def list.quote {α : Type} [has_quote α] : list α → pexpr
 | []     := ``([])
 | (h::t) := ``(%%(quote h) :: %%(list.quote t))

src/library/vm/vm_expr.cpp

@@ -6,9 +6,6 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include <iostream>
-#include <library/quote.h>
-#include <frontends/lean/prenum.h>
-#include <library/string.h>
 #include "kernel/expr.h"
 #include "kernel/free_vars.h"
 #include "kernel/instantiate.h"
@@ -24,13 +21,13 @@ Author: Leonardo de Moura
 #include "library/choice.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_nat.h"
-#include "library/vm/vm_string.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_format.h"
 #include "library/vm/vm_options.h"
 #include "library/vm/vm_option.h"
 #include "library/vm/vm_level.h"
 #include "library/vm/vm_list.h"
+#include "library/vm/vm_string.h"
 #include "library/compiler/simp_inductive.h"
 #include "library/compiler/nat_value.h"
 
@@ -421,18 +418,6 @@ vm_obj expr_is_choice_macro(vm_obj const & e) {
     return mk_vm_bool(is_choice(to_expr(e)));
 }
 
-vm_obj expr_mk_quote_macro(vm_obj const & e) {
-    return to_obj(mk_quote(to_expr(e)));
-}
-
-vm_obj expr_mk_prenum_macro(vm_obj const & n) {
-    return to_obj(mk_prenum(is_simple(n) ? mpz{cidx(n)} : to_mpz(n)));
-}
-
-vm_obj expr_mk_string_macro(vm_obj const & s) {
-    return to_obj(from_string(to_string(s)));
-}
-
 vm_obj expr_mk_sorry(vm_obj const & t) {
     return to_obj(mk_sorry(to_expr(t)));
 }
@@ -492,9 +477,6 @@ void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name("mk_int_val_ne_proof"),        vm_mk_int_val_ne_proof);
 
     DECLARE_VM_BUILTIN(name("expr", "is_choice_macro"),    expr_is_choice_macro);
-    DECLARE_VM_BUILTIN(name("expr", "mk_quote_macro"),     expr_mk_quote_macro);
-    DECLARE_VM_BUILTIN(name("expr", "mk_prenum_macro"),    expr_mk_prenum_macro);
-    DECLARE_VM_BUILTIN(name("expr", "mk_string_macro"),    expr_mk_string_macro);
 
     DECLARE_VM_BUILTIN(name("expr", "mk_sorry"), expr_mk_sorry);
     DECLARE_VM_BUILTIN(name("expr", "is_sorry"), expr_is_sorry);

src/library/vm/vm_pexpr.cpp

@@ -9,6 +9,10 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_expr.h"
+#include "library/vm/vm_string.h"
+#include "library/quote.h"
+#include "frontends/lean/prenum.h"
+#include "library/string.h"
 
 namespace lean {
 vm_obj pexpr_subst(vm_obj const & _e1, vm_obj const & _e2) {
@@ -43,6 +47,18 @@ vm_obj pexpr_mk_placeholder() {
     return to_obj(mk_expr_placeholder());
 }
 
+vm_obj pexpr_mk_quote_macro(vm_obj const & e) {
+    return to_obj(mk_quote(to_expr(e)));
+}
+
+vm_obj pexpr_mk_prenum_macro(vm_obj const & n) {
+    return to_obj(mk_prenum(is_simple(n) ? mpz{cidx(n)} : to_mpz(n)));
+}
+
+vm_obj pexpr_mk_string_macro(vm_obj const & s) {
+    return to_obj(from_string(to_string(s)));
+}
+
 void initialize_vm_pexpr() {
     DECLARE_VM_BUILTIN(name({"pexpr", "subst"}),          pexpr_subst);
     DECLARE_VM_BUILTIN(name({"pexpr", "of_expr"}),        pexpr_of_expr);
@@ -50,6 +66,10 @@ void initialize_vm_pexpr() {
     DECLARE_VM_BUILTIN(name({"pexpr", "of_raw_expr"}),    pexpr_of_raw_expr);
     DECLARE_VM_BUILTIN(name({"pexpr", "to_raw_expr"}),    pexpr_to_raw_expr);
     DECLARE_VM_BUILTIN(name({"pexpr", "mk_placeholder"}), pexpr_mk_placeholder);
+
+    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);
 }
 
 void finalize_vm_pexpr() {