From e8fa54cc516e3aceaf8c0b3488d8040ce690a3ea Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Feb 2017 19:01:28 +0100 Subject: [PATCH] refactor(init/meta): move macro creation defs from expr to pexpr --- library/init/meta/expr.lean | 3 --- library/init/meta/pexpr.lean | 4 ++++ library/init/meta/quote.lean | 11 ++++------- src/library/vm/vm_expr.cpp | 20 +------------------- src/library/vm/vm_pexpr.cpp | 20 ++++++++++++++++++++ 5 files changed, 29 insertions(+), 29 deletions(-) diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 94c64174a8..b816fd3c6f 100644 --- a/library/init/meta/expr.lean +++ b/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 diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean index 3f5bcb4385..707334c199 100644 --- a/library/init/meta/pexpr.lean +++ b/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⟩ diff --git a/library/init/meta/quote.lean b/library/init/meta/quote.lean index 139300371c..73ddb72439 100644 --- a/library/init/meta/quote.lean +++ b/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)) diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 24519096e7..11cb089d1d 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -6,9 +6,6 @@ Author: Leonardo de Moura */ #include #include -#include -#include -#include #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); diff --git a/src/library/vm/vm_pexpr.cpp b/src/library/vm/vm_pexpr.cpp index 99907052ee..f444a3b516 100644 --- a/src/library/vm/vm_pexpr.cpp +++ b/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() {