refactor(init/meta/expr): unify expr and pexpr

library/init/meta/expr.lean

@@ -34,10 +34,10 @@ end⟩
 meta constant macro_def : Type
 
 /- Reflect a C++ expr object. The VM replaces it with the C++ implementation. -/
-meta inductive expr
-| var         : nat → expr
-| sort        : level → expr
-| const       : name → list level → expr
+meta inductive expr (elaborated : bool := tt)
+| var      {} : nat → expr
+| sort     {} : level → expr
+| const    {} : name → list level → expr
 | mvar        : name → expr → expr
 | local_const : name → name → binder_info → expr → expr
 | app         : expr → expr → expr
@@ -46,6 +46,8 @@ meta inductive expr
 | elet        : name → expr → expr → expr → expr
 | macro       : macro_def → list expr → expr
 
+variable {elab : bool}
+
 universes u v
 /-- (reflected a) is a special opaque container for a closed `expr` representing `a`.
     It can only be obtained via type class inference, which will use the representation
@@ -58,10 +60,11 @@ meta constant reflected {α : Type u} : α → Type u
 meta constant reflected.to_expr {α : Type u} {a : α} : reflected a → expr
 meta constant reflected.subst {α : Type u} {β : α → Type v} {f : Π a : α, β a} {a : α} :
   reflected f → reflected a → reflected (f a)
+meta constant expr.reflect (e : expr elab) : reflected e
 meta constant string.reflect (s : string) : reflected s
 
 attribute [class] reflected
-attribute [instance] string.reflect
+attribute [instance] expr.reflect string.reflect
 
 meta instance {α : Type u} (a : α) : has_coe (reflected a) expr :=
 ⟨reflected.to_expr⟩
@@ -75,14 +78,10 @@ meta constant expr.macro_def_name (d : macro_def) : name
 meta def expr.mk_var (n : nat) : expr :=
 expr.var n
 
-/- Choice macros are used to implement overloading.
-   TODO(Leo): should we change it to pexpr? -/
-meta constant expr.is_choice_macro : expr → bool
-
 /- Expressions can be annotated using the annotation macro. -/
-meta constant expr.is_annotation : expr → option (name × expr)
+meta constant expr.is_annotation : expr elab → option (name × expr elab)
 
-meta def expr.erase_annotations : expr → expr
+meta def expr.erase_annotations : expr elab → expr elab
 | e :=
   match e.is_annotation with
   | some (_, a) := expr.erase_annotations a
@@ -97,14 +96,14 @@ attribute [instance] expr.has_decidable_eq
 meta constant expr.alpha_eqv : expr → expr → bool
 notation a ` =ₐ `:50 b:50 := expr.alpha_eqv a b = bool.tt
 
-protected meta constant expr.to_string : expr → string
+protected meta constant expr.to_string : expr elab → string
 
-meta instance : has_to_string expr := ⟨expr.to_string⟩
-meta instance : has_to_format expr := ⟨λ e, e.to_string⟩
+meta instance : has_to_string (expr elab) := ⟨expr.to_string⟩
+meta instance : has_to_format (expr elab) := ⟨λ e, e.to_string⟩
 
 /- Coercion for letting users write (f a) instead of (expr.app f a) -/
-meta instance : has_coe_to_fun expr :=
-{ F := λ e, expr → expr, coe := λ e, expr.app e }
+meta instance : has_coe_to_fun (expr elab) :=
+{ F := λ e, expr elab → expr elab, coe := λ e, expr.app e }
 
 meta constant expr.hash : expr → nat
 
@@ -132,7 +131,7 @@ meta constant expr.instantiate_univ_params : expr → list (name × level) → e
 meta constant expr.instantiate_var         : expr → expr → expr
 meta constant expr.instantiate_vars        : expr → list expr → expr
 
-meta constant expr.subst                   : expr → expr → expr
+protected meta constant expr.subst : expr elab → expr elab → expr elab
 
 meta constant expr.has_var       : expr → bool
 meta constant expr.has_var_idx   : expr → nat → bool
@@ -140,6 +139,7 @@ meta constant expr.has_local     : expr → bool
 meta constant expr.has_meta_var  : expr → bool
 meta constant expr.lift_vars     : expr → nat → nat → expr
 meta constant expr.lower_vars    : expr → nat → nat → expr
+protected meta constant expr.pos : expr elab → option pos
 /- (copy_pos_info src tgt) copy position information from src to tgt. -/
 meta constant expr.copy_pos_info : expr → expr → expr
 
@@ -194,7 +194,7 @@ meta def app_arg : expr → expr
 | (app f a) := a
 | a         := a
 
-meta def get_app_fn : expr → expr
+meta def get_app_fn : expr elab → expr elab
 | (app f a) := get_app_fn f
 | a         := a
 
@@ -350,7 +350,7 @@ open format
 
 private meta def p := λ xs, paren (format.join (list.intersperse " " xs))
 
-meta def to_raw_fmt : expr → format
+meta def to_raw_fmt : expr elab → format
 | (var n) := p ["var", to_fmt n]
 | (sort l) := p ["sort", to_fmt l]
 | (const n ls) := p ["const", to_fmt n, to_fmt ls]

library/init/meta/interactive.lean

@@ -124,11 +124,6 @@ meta def param_desc : expr → tactic format
 end interactive
 
 namespace tactic
-meta def report_resolve_name_failure {α : Type} (e : expr) (n : name) : tactic α :=
-if e.is_choice_macro
-then fail ("failed to resolve name '" ++ to_string n ++ "', it is overloaded")
-else fail ("failed to resolve name '" ++ to_string n ++ "', unexpected result")
-
 /- allows metavars and report errors -/
 meta def i_to_expr (q : pexpr) : tactic expr :=
 to_expr q tt
@@ -259,9 +254,9 @@ do hs ← get_locals ids, revert_lst hs, skip
 private meta def resolve_name' (n : name) : tactic expr :=
 do {
   p ← resolve_name n,
-  match p.to_raw_expr with
-  | expr.const n _           := mk_const n -- create metavars for universe levels
-  | _                        := i_to_expr p
+  match p with
+  | expr.const n _ := mk_const n -- create metavars for universe levels
+  | _              := i_to_expr p
   end
 }
 
@@ -270,10 +265,9 @@ do {
    Example: the elaborator will force any unassigned ?A that must have be an instance of (has_one ?A) to nat.
    Remark: another benefit is that auxiliary temporary metavariables do not appear in error messages. -/
 private meta def to_expr' (p : pexpr) : tactic expr :=
-let e := p.to_raw_expr in
-match e with
-| (const c [])          := do new_e ← resolve_name' c, save_type_info new_e e, return new_e
-| (local_const c _ _ _) := do new_e ← resolve_name' c, save_type_info new_e e, return new_e
+match p with
+| (const c [])          := do new_e ← resolve_name' c, save_type_info new_e p, return new_e
+| (local_const c _ _ _) := do new_e ← resolve_name' c, save_type_info new_e p, return new_e
 | _                     := i_to_expr p
 end
 
@@ -577,11 +571,11 @@ private meta def add_simps : simp_lemmas → list name → tactic simp_lemmas
 private meta def report_invalid_simp_lemma {α : Type} (n : name): tactic α :=
 fail ("invalid simplification lemma '" ++ to_string n ++ "' (use command 'set_option trace.simp_lemmas true' for more details)")
 
-private meta def simp_lemmas.resolve_and_add (s : simp_lemmas) (n : name) (ref : expr) : tactic simp_lemmas :=
+private meta def simp_lemmas.resolve_and_add (s : simp_lemmas) (n : name) (ref : pexpr) : tactic simp_lemmas :=
 do
   p ← resolve_name n,
   -- unpack local refs
-  let e := p.to_raw_expr.erase_annotations.get_app_fn.erase_annotations,
+  let e := p.erase_annotations.get_app_fn.erase_annotations,
   match e with
   | const n _           :=
     (do b ← is_valid_simp_lemma_cnst reducible n, guard b, save_const_type_info n ref, s.add_simp n)
@@ -596,10 +590,9 @@ do
   end
 
 private meta def simp_lemmas.add_pexpr (s : simp_lemmas) (p : pexpr) : tactic simp_lemmas :=
-let e := p.to_raw_expr in
-match e with
-| (const c [])          := simp_lemmas.resolve_and_add s c e
-| (local_const c _ _ _) := simp_lemmas.resolve_and_add s c e
+match p with
+| (const c [])          := simp_lemmas.resolve_and_add s c p
+| (local_const c _ _ _) := simp_lemmas.resolve_and_add s c p
 | _                     := do new_e ← i_to_expr p, s.add new_e
 end
 

library/init/meta/pexpr.lean

@@ -8,26 +8,15 @@ import init.meta.expr
 universe u
 
 /- Quoted expressions. They can be converted into expressions by using a tactic. -/
-meta constant pexpr : Type
+@[reducible] meta def pexpr := expr ff
 protected meta constant pexpr.of_expr  : expr → pexpr
-protected meta constant pexpr.subst    : pexpr → pexpr → pexpr
 
-/- Low level primitives for accessing internal representation. -/
-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.pos : pexpr → option pos
-
 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 :=
-⟨pexpr.to_string⟩
-
-meta constant pexpr.reflect (p : pexpr) : reflected p
-attribute [instance] pexpr.reflect
+/- Choice macros are used to implement overloading. -/
+meta constant pexpr.is_choice_macro : pexpr → bool
 
 meta class has_to_pexpr (α : Type u) :=
 (to_pexpr : α → pexpr)

library/init/meta/smt/interactive.lean

@@ -137,20 +137,19 @@ open tactic (resolve_name transparency to_expr)
 private meta def report_invalid_em_lemma {α : Type} (n : name) : smt_tactic α :=
 fail ("invalid ematch lemma '" ++ to_string n ++ "'")
 
-private meta def add_lemma_name (md : transparency) (lhs_lemma : bool) (n : name) (ref : expr) : smt_tactic unit :=
+private meta def add_lemma_name (md : transparency) (lhs_lemma : bool) (n : name) (ref : pexpr) : smt_tactic unit :=
 do
   p ← resolve_name n,
-  match p.to_raw_expr with
+  match p with
   | expr.const n _           := (add_ematch_lemma_from_decl_core md lhs_lemma n >> tactic.save_const_type_info n ref) <|> report_invalid_em_lemma n
   | _                        := (do e ← to_expr p, add_ematch_lemma_core md lhs_lemma e >> try (tactic.save_type_info e ref)) <|> report_invalid_em_lemma n
   end
 
 
 private meta def add_lemma_pexpr (md : transparency) (lhs_lemma : bool) (p : pexpr) : smt_tactic unit :=
-let e := pexpr.to_raw_expr p in
-match e with
-| (expr.const c [])          := add_lemma_name md lhs_lemma c e
-| (expr.local_const c _ _ _) := add_lemma_name md lhs_lemma c e
+match p with
+| (expr.const c [])          := add_lemma_name md lhs_lemma c p
+| (expr.local_const c _ _ _) := add_lemma_name md lhs_lemma c p
 | _                          := do new_e ← to_expr p, add_ematch_lemma_core md lhs_lemma new_e
 end
 
@@ -168,7 +167,7 @@ private meta def add_eqn_lemmas_for_core (md : transparency) : list name → smt
 | []      := return ()
 | (c::cs) := do
   p ← resolve_name c,
-  match p.to_raw_expr with
+  match p with
   | expr.const n _           := add_ematch_eqn_lemmas_for_core md n >> add_eqn_lemmas_for_core cs
   | _                        := fail $ "'" ++ to_string c ++ "' is not a constant"
   end
@@ -179,10 +178,10 @@ add_eqn_lemmas_for_core reducible ids
 meta def add_eqn_lemmas (ids : parse ident*) : smt_tactic unit :=
 add_eqn_lemmas_for ids
 
-private meta def add_hinst_lemma_from_name (md : transparency) (lhs_lemma : bool) (n : name) (hs : hinst_lemmas) (ref : expr) : smt_tactic hinst_lemmas :=
+private meta def add_hinst_lemma_from_name (md : transparency) (lhs_lemma : bool) (n : name) (hs : hinst_lemmas) (ref : pexpr) : smt_tactic hinst_lemmas :=
 do
   p ← resolve_name n,
-  match p.to_raw_expr with
+  match p with
   | expr.const n _           :=
     (do h ← hinst_lemma.mk_from_decl_core md n lhs_lemma, tactic.save_const_type_info n ref, return $ hs.add h)
     <|>
@@ -196,10 +195,9 @@ do
   end
 
 private meta def add_hinst_lemma_from_pexpr (md : transparency) (lhs_lemma : bool) (p : pexpr) (hs : hinst_lemmas) : smt_tactic hinst_lemmas :=
-let e := pexpr.to_raw_expr p in
-match e with
-| (expr.const c [])          := add_hinst_lemma_from_name md lhs_lemma c hs e
-| (expr.local_const c _ _ _) := add_hinst_lemma_from_name md lhs_lemma c hs e
+match p with
+| (expr.const c [])          := add_hinst_lemma_from_name md lhs_lemma c hs p
+| (expr.local_const c _ _ _) := add_hinst_lemma_from_name md lhs_lemma c hs p
 | _                          := do new_e ← to_expr p, h ← hinst_lemma.mk_core md new_e lhs_lemma, return $ hs.add h
 end
 

library/init/meta/tactic.lean

@@ -429,7 +429,7 @@ try $ do
 meta constant decl_name : tactic name
 
 /- (save_type_info e ref) save (typeof e) at position associated with ref -/
-meta constant save_type_info : expr → expr → tactic unit
+meta constant save_type_info {elab : bool} : expr → expr elab → tactic unit
 meta constant save_info_thunk : pos → (unit → format) → tactic unit
 /-- Return list of currently open namespaces -/
 meta constant open_namespaces : tactic (list name)
@@ -501,7 +501,7 @@ meta def intro_lst : list name → tactic (list expr)
 
 /-- Returns n fully qualified if it refers to a constant, or else fails. -/
 meta def resolve_constant (n : name) : tactic name :=
-do (expr.const n _) ← pexpr.to_raw_expr <$> resolve_name n,
+do (expr.const n _) ← resolve_name n,
    pure n
 
 meta def to_expr_strict (q : pexpr) : tactic expr :=
@@ -776,7 +776,7 @@ do env  ← get_env,
 meta def applyc (c : name) : tactic unit :=
 mk_const c >>= apply
 
-meta def save_const_type_info (n : name) (ref : expr) : tactic unit :=
+meta def save_const_type_info (n : name) {elab : bool} (ref : expr elab) : tactic unit :=
 try (do c ← mk_const n, save_type_info c ref)
 
 /- Create a fresh universe ?u, a metavariable (?T : Type.{?u}),
@@ -1008,7 +1008,7 @@ end list
 -/
 run_cmd do
  let l  := level.param `l,
- let Ty := expr.sort l,
+ let Ty : pexpr := expr.sort l,
  type ← to_expr ``(Π (α : %%Ty), α → α),
  val  ← to_expr ``(λ (α : %%Ty) (a : α), a),
  add_decl (declaration.defn `id_locked [`l] type val reducibility_hints.opaque tt)

library/init/meta/transfer.lean

@@ -174,11 +174,11 @@ meta def transfer (ds : list name) : tactic unit := do
   (guard (¬ tgt.has_meta_var) <|>
     fail "Target contains (universe) meta variables. This is not supported by transfer."),
 
-  (new_tgt, pr, ms) ← compute_transfer rds [] (const `iff [] tgt),
+  (new_tgt, pr, ms) ← compute_transfer rds [] ((const `iff [] : expr) tgt),
   new_pr ← mk_meta_var new_tgt,
 
   /- Setup final tactic state -/
-  exact (const `iff.mpr [] tgt new_tgt pr new_pr),
+  exact ((const `iff.mpr [] : expr) tgt new_tgt pr new_pr),
   ms ← monad.for ms (λm, (get_assignment m >> return []) <|> return [m]),
   gs ← get_goals,
   set_goals (list.join ms ++ new_pr :: gs)

src/frontends/lean/elaborator.cpp

@@ -2834,7 +2834,7 @@ expr elaborator::visit_expr_quote(expr const & e, optional<expr> const & expecte
             throw elaborator_exception(e, "invalid quotation, contains local constant");
         q = mk_expr_quote(new_s);
         q = mk_as_is(q);
-        expr subst_fn = mk_constant(get_expr_subst_name());
+        expr subst_fn = mk_app(mk_explicit(mk_constant(get_expr_subst_name())), mk_bool_tt());
         for (expr const & subst : substs) {
             q = mk_app(subst_fn, q, subst);
         }
@@ -3862,7 +3862,7 @@ expr resolve_names(environment const & env, local_context const & lctx, expr con
     return resolve_names_fn(env, lctx)(e);
 }
 
-static vm_obj tactic_save_type_info(vm_obj const & _e, vm_obj const & ref, vm_obj const & _s) {
+static vm_obj tactic_save_type_info(vm_obj const &, vm_obj const & _e, vm_obj const & ref, vm_obj const & _s) {
     expr const & e = to_expr(_e);
     tactic_state const & s = tactic::to_state(_s);
     if (!get_global_info_manager() || !get_pos_info_provider()) return tactic::mk_success(s);

src/frontends/lean/parser.cpp

@@ -1709,7 +1709,7 @@ expr elaborate_quote(expr e, environment const & env, options const & opts) {
 
     e = instantiate_rev(body, aqs.size(), aqs.data());
     e = quote(e);
-    return e;
+    return mk_typed_expr(mk_app(mk_constant(get_expr_name()), mk_bool_tt()), e);
 }
 
 expr parser::patexpr_to_pattern(expr const & pat_or_expr, bool skip_main_fn, buffer<expr> & new_locals) {

src/frontends/lean/tactic_notation.cpp

@@ -143,7 +143,7 @@ static expr parse_interactive_param(parser & p, expr const & ty, expr const & qu
     vm_state S(env, p.get_options());
     auto vm_res = S.invoke(n, vm_parsed);
     expr r = to_expr(vm_res);
-    if (is_app_of(r, get_pexpr_subst_name())) {
+    if (is_app_of(r, get_expr_subst_name())) {
         return r; // HACK
     } else {
         return mk_as_is(r);

src/library/constants.cpp

@@ -294,8 +294,6 @@ name const * g_pprod_mk = nullptr;
 name const * g_pprod_fst = nullptr;
 name const * g_pprod_snd = nullptr;
 name const * g_propext = nullptr;
-name const * g_pexpr = nullptr;
-name const * g_pexpr_subst = nullptr;
 name const * g_to_pexpr = nullptr;
 name const * g_quot_mk = nullptr;
 name const * g_quot_lift = nullptr;
@@ -665,8 +663,6 @@ void initialize_constants() {
     g_pprod_fst = new name{"pprod", "fst"};
     g_pprod_snd = new name{"pprod", "snd"};
     g_propext = new name{"propext"};
-    g_pexpr = new name{"pexpr"};
-    g_pexpr_subst = new name{"pexpr", "subst"};
     g_to_pexpr = new name{"to_pexpr"};
     g_quot_mk = new name{"quot", "mk"};
     g_quot_lift = new name{"quot", "lift"};
@@ -1037,8 +1033,6 @@ void finalize_constants() {
     delete g_pprod_fst;
     delete g_pprod_snd;
     delete g_propext;
-    delete g_pexpr;
-    delete g_pexpr_subst;
     delete g_to_pexpr;
     delete g_quot_mk;
     delete g_quot_lift;
@@ -1408,8 +1402,6 @@ name const & get_pprod_mk_name() { return *g_pprod_mk; }
 name const & get_pprod_fst_name() { return *g_pprod_fst; }
 name const & get_pprod_snd_name() { return *g_pprod_snd; }
 name const & get_propext_name() { return *g_propext; }
-name const & get_pexpr_name() { return *g_pexpr; }
-name const & get_pexpr_subst_name() { return *g_pexpr_subst; }
 name const & get_to_pexpr_name() { return *g_to_pexpr; }
 name const & get_quot_mk_name() { return *g_quot_mk; }
 name const & get_quot_lift_name() { return *g_quot_lift; }

src/library/constants.h

@@ -296,8 +296,6 @@ name const & get_pprod_mk_name();
 name const & get_pprod_fst_name();
 name const & get_pprod_snd_name();
 name const & get_propext_name();
-name const & get_pexpr_name();
-name const & get_pexpr_subst_name();
 name const & get_to_pexpr_name();
 name const & get_quot_mk_name();
 name const & get_quot_lift_name();

src/library/constants.txt

@@ -289,8 +289,6 @@ pprod.mk
 pprod.fst
 pprod.snd
 propext
-pexpr
-pexpr.subst
 to_pexpr
 quot.mk
 quot.lift

src/library/init_module.cpp

@@ -87,7 +87,6 @@ void initialize_library_module() {
     initialize_string();
     initialize_num();
     initialize_annotation();
-    initialize_quote();
     initialize_explicit();
     initialize_protected();
     initialize_private();
@@ -97,6 +96,7 @@ void initialize_library_module() {
     initialize_sorry();
     initialize_class();
     initialize_library_util();
+    initialize_quote();
     initialize_pp_options();
     initialize_projection();
     initialize_relation_manager();
@@ -140,6 +140,7 @@ void finalize_library_module() {
     finalize_relation_manager();
     finalize_projection();
     finalize_pp_options();
+    finalize_quote();
     finalize_library_util();
     finalize_class();
     finalize_sorry();
@@ -149,7 +150,6 @@ void finalize_library_module() {
     finalize_private();
     finalize_protected();
     finalize_explicit();
-    finalize_quote();
     finalize_annotation();
     finalize_num();
     finalize_string();

src/library/quote.cpp

@@ -141,8 +141,8 @@ expr mk_pexpr_quote_and_substs(expr const & e, bool is_strict) {
             return none_expr();
         });
     expr r        = mk_pexpr_quote(Fun(locals, s));
-    expr subst    = mk_constant(get_pexpr_subst_name());
-    expr to_pexpr = mk_constant(get_to_pexpr_name(), {mk_level_zero()});
+    expr subst    = mk_constant(get_expr_subst_name());
+    expr to_pexpr = mk_constant(get_to_pexpr_name());
     for (expr const & aq : aqs) {
         r = mk_app(subst, r, mk_app(to_pexpr, aq));
     }
@@ -154,8 +154,8 @@ void initialize_quote() {
     g_pexpr_quote_macro   = new name("pexpr_quote_macro");
     g_expr_quote_opcode   = new std::string("Quote");
     g_pexpr_quote_opcode  = new std::string("PQuote");
-    g_expr           = new expr(Const(get_expr_name()));
-    g_pexpr          = new expr(Const(get_pexpr_name()));
+    g_expr           = new expr(mk_app(Const(get_expr_name()), mk_bool_tt()));
+    g_pexpr          = new expr(mk_app(Const(get_expr_name()), mk_bool_ff()));
 
     g_antiquote  = new name("antiquote");
     register_annotation(*g_antiquote);

src/library/util.cpp

@@ -1050,7 +1050,7 @@ void finalize_bool() {
 
 expr mk_bool() { return *g_bool; }
 expr mk_bool_tt() { return *g_bool_tt; }
-expr mk_bool_ff() { return *g_bool_tt; }
+expr mk_bool_ff() { return *g_bool_ff; }
 expr to_bool_expr(bool b) { return b ? mk_bool_tt() : mk_bool_ff(); }
 
 name get_dep_recursor(environment const & env, name const & n) {

src/library/vm/vm_expr.cpp

@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_level.h"
 #include "library/vm/vm_list.h"
 #include "library/vm/vm_string.h"
+#include "library/vm/vm_pos_info.h"
 #include "library/compiler/simp_inductive.h"
 #include "library/compiler/nat_value.h"
 
@@ -109,43 +110,43 @@ vm_obj to_obj(binder_info const & bi) {
         return mk_vm_simple(0);
 }
 
-vm_obj expr_var(vm_obj const & n) {
+vm_obj expr_var(vm_obj const &, vm_obj const & n) {
     return to_obj(mk_var(to_unsigned(n)));
 }
 
-vm_obj expr_sort(vm_obj const & l) {
+vm_obj expr_sort(vm_obj const &, vm_obj const & l) {
     return to_obj(mk_sort(to_level(l)));
 }
 
-vm_obj expr_const(vm_obj const & n, vm_obj const & ls) {
+vm_obj expr_const(vm_obj const &, vm_obj const & n, vm_obj const & ls) {
     return to_obj(mk_constant(to_name(n), to_list_level(ls)));
 }
 
-vm_obj expr_mvar(vm_obj const & n, vm_obj const & t) {
+vm_obj expr_mvar(vm_obj const &, vm_obj const & n, vm_obj const & t) {
     return to_obj(mk_metavar(to_name(n), to_expr(t)));
 }
 
-vm_obj expr_local_const(vm_obj const & n, vm_obj const & ppn, vm_obj const & bi, vm_obj const & t) {
+vm_obj expr_local_const(vm_obj const &, vm_obj const & n, vm_obj const & ppn, vm_obj const & bi, vm_obj const & t) {
     return to_obj(mk_local(to_name(n), to_name(ppn), to_expr(t), to_binder_info(bi)));
 }
 
-vm_obj expr_app(vm_obj const & f, vm_obj const & a) {
+vm_obj expr_app(vm_obj const &, vm_obj const & f, vm_obj const & a) {
     return to_obj(mk_app(to_expr(f), to_expr(a)));
 }
 
-vm_obj expr_lam(vm_obj const & n, vm_obj const & bi, vm_obj const & t, vm_obj const & b) {
+vm_obj expr_lam(vm_obj const &, vm_obj const & n, vm_obj const & bi, vm_obj const & t, vm_obj const & b) {
     return to_obj(mk_lambda(to_name(n), to_expr(t), to_expr(b), to_binder_info(bi)));
 }
 
-vm_obj expr_pi(vm_obj const & n, vm_obj const & bi, vm_obj const & t, vm_obj const & b) {
+vm_obj expr_pi(vm_obj const &, vm_obj const & n, vm_obj const & bi, vm_obj const & t, vm_obj const & b) {
     return to_obj(mk_pi(to_name(n), to_expr(t), to_expr(b), to_binder_info(bi)));
 }
 
-vm_obj expr_elet(vm_obj const & n, vm_obj const & t, vm_obj const & v, vm_obj const & b) {
+vm_obj expr_elet(vm_obj const &, vm_obj const & n, vm_obj const & t, vm_obj const & v, vm_obj const & b) {
     return to_obj(mk_let(to_name(n), to_expr(t), to_expr(v), to_expr(b)));
 }
 
-vm_obj expr_macro(vm_obj const & d, vm_obj const & es) {
+vm_obj expr_macro(vm_obj const &, vm_obj const & d, vm_obj const & es) {
     buffer<expr> args;
     to_buffer_expr(es, args);
     return to_obj(mk_macro(to_macro_definition(d), args.size(), args.data()));
@@ -213,7 +214,7 @@ vm_obj expr_alpha_eqv(vm_obj const & o1, vm_obj const & o2) {
     return mk_vm_bool(to_expr(o1) == to_expr(o2));
 }
 
-vm_obj expr_to_string(vm_obj const & l) {
+vm_obj expr_to_string(vm_obj const &, vm_obj const & l) {
     std::ostringstream out;
     out << to_expr(l);
     return to_obj(out.str());
@@ -415,10 +416,6 @@ vm_obj vm_mk_int_val_ne_proof(vm_obj const & a, vm_obj const & b) {
     return to_obj(mk_int_val_ne_proof(to_expr(a), to_expr(b)));
 }
 
-vm_obj expr_is_choice_macro(vm_obj const & e) {
-    return mk_vm_bool(is_choice(to_expr(e)));
-}
-
 vm_obj expr_mk_sorry(vm_obj const & t) {
     return to_obj(mk_sorry(to_expr(t)));
 }
@@ -432,7 +429,7 @@ vm_obj expr_occurs(vm_obj const & e1, vm_obj const & e2) {
     return mk_vm_bool(occurs(to_expr(e1), to_expr(e2)));
 }
 
-vm_obj expr_subst(vm_obj const & _e1, vm_obj const & _e2) {
+vm_obj expr_subst(vm_obj const &, vm_obj const & _e1, vm_obj const & _e2) {
     expr const & e1 = to_expr(_e1);
     expr const & e2 = to_expr(_e2);
     if (is_lambda(e1)) {
@@ -442,7 +439,7 @@ vm_obj expr_subst(vm_obj const & _e1, vm_obj const & _e2) {
     }
 }
 
-vm_obj expr_is_annotation(vm_obj const & _e) {
+vm_obj expr_is_annotation(vm_obj const &, vm_obj const & _e) {
     expr const & e = to_expr(_e);
     if (is_annotation(e)) {
         return mk_vm_some(mk_vm_pair(to_obj(get_annotation_kind(e)), to_obj(get_annotation_arg(e))));
@@ -455,19 +452,28 @@ vm_obj reflected_to_expr(vm_obj const &, vm_obj const &, vm_obj const & r) {
     return r;
 }
 
-vm_obj reflected_subst(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const & e1,
+vm_obj reflected_subst(vm_obj const & _dummy, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const & e1,
                        vm_obj const & e2) {
-    return expr_subst(e1, e2);
+    return expr_subst(_dummy, e1, e2);
 }
 
-vm_obj reflect_pexpr(vm_obj const & e) {
-    return to_obj(mk_pexpr_quote_and_substs(to_expr(e), /* is_strict */ false));
+vm_obj reflect_expr(vm_obj const & elab, vm_obj const & e) {
+    if (to_bool(elab))
+        return to_obj(mk_expr_quote(to_expr(e)));
+    else
+        return to_obj(mk_pexpr_quote_and_substs(to_expr(e), /* is_strict */ false));
 }
 
 vm_obj reflect_string(vm_obj const & s) {
     return to_obj(from_string(to_string(s)));
 }
 
+vm_obj expr_pos(vm_obj const &, vm_obj const & e) {
+    if (auto p = get_pos_info(to_expr(e)))
+        return mk_vm_some(to_obj(*p));
+    return mk_vm_none();
+}
+
 void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"expr", "var"}),              expr_var);
     DECLARE_VM_BUILTIN(name({"expr", "sort"}),             expr_sort);
@@ -500,6 +506,7 @@ void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"expr", "lift_vars"}),        expr_lift_vars);
     DECLARE_VM_BUILTIN(name({"expr", "lower_vars"}),       expr_lower_vars);
     DECLARE_VM_BUILTIN(name({"expr", "hash"}),             expr_hash);
+    DECLARE_VM_BUILTIN(name({"expr", "pos"}),              expr_pos);
     DECLARE_VM_BUILTIN(name({"expr", "copy_pos_info"}),    expr_copy_pos_info);
     DECLARE_VM_BUILTIN(name({"expr", "occurs"}),           expr_occurs);
     DECLARE_VM_BUILTIN(name({"expr", "collect_univ_params"}), expr_collect_univ_params);
@@ -508,7 +515,7 @@ void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"reflected", "to_expr"}),     reflected_to_expr);
     DECLARE_VM_BUILTIN(name({"reflected", "subst"}),       reflected_subst);
     DECLARE_VM_BUILTIN(name("string", "reflect"),          reflect_string);
-    DECLARE_VM_BUILTIN(name("pexpr", "reflect"),           reflect_pexpr);
+    DECLARE_VM_BUILTIN(name("expr", "reflect"),            reflect_expr);
 
     DECLARE_VM_BUILTIN(name("mk_nat_val_ne_proof"),        vm_mk_nat_val_ne_proof);
     DECLARE_VM_BUILTIN(name("mk_nat_val_lt_proof"),        vm_mk_nat_val_lt_proof);
@@ -518,7 +525,6 @@ void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name("mk_string_val_ne_proof"),     vm_mk_string_val_ne_proof);
     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", "is_annotation"),      expr_is_annotation);
 
     DECLARE_VM_BUILTIN(name("expr", "mk_sorry"), expr_mk_sorry);

src/library/vm/vm_expr.h

@@ -17,7 +17,6 @@ bool is_expr(vm_obj const & o);
 expr const & to_expr(vm_obj const & o);
 vm_obj to_obj(expr const & e);
 vm_obj to_obj(optional<expr> const & e);
-vm_obj expr_subst(vm_obj const & _e1, vm_obj const & _e2);
 void initialize_vm_expr();
 void finalize_vm_expr();
 void initialize_vm_expr_builtin_idxs();

src/library/vm/vm_pexpr.cpp

@@ -5,19 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/instantiate.h"
-#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/choice.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 "frontends/lean/prenum.h"
-#include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/util.h"
 
 namespace lean {
@@ -25,30 +18,10 @@ vm_obj pexpr_of_expr(vm_obj const & e) {
     return to_obj(mk_as_is(to_expr(e)));
 }
 
-vm_obj expr_to_string(vm_obj const &);
-
-vm_obj pexpr_to_string(vm_obj const & e) {
-    return expr_to_string(e);
-}
-
-vm_obj pexpr_to_raw_expr(vm_obj const & e) {
-    return e;
-}
-
-vm_obj pexpr_of_raw_expr(vm_obj const & e) {
-    return e;
-}
-
 vm_obj pexpr_mk_placeholder() {
     return to_obj(mk_expr_placeholder());
 }
 
-vm_obj pexpr_pos(vm_obj const & e) {
-    if (auto p = get_pos_info(to_expr(e)))
-        return mk_vm_some(to_obj(*p));
-    return mk_vm_none();
-}
-
 vm_obj pexpr_mk_explicit(vm_obj const & e) {
     return to_obj(mk_explicit(to_expr(e)));
 }
@@ -57,18 +30,18 @@ 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);
-    DECLARE_VM_BUILTIN(name({"pexpr", "to_string"}),      pexpr_to_string);
-    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);
+vm_obj pexpr_is_choice_macro(vm_obj const & e) {
+    return mk_vm_bool(is_choice(to_expr(e)));
+}
 
-    DECLARE_VM_BUILTIN(name("pexpr", "pos"),              pexpr_pos);
+void initialize_vm_pexpr() {
+    DECLARE_VM_BUILTIN(name({"pexpr", "of_expr"}),        pexpr_of_expr);
+    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("expr", "is_choice_macro"),   pexpr_is_choice_macro);
 }
 
 void finalize_vm_pexpr() {

tests/lean/coe5.lean.expected.out

@@ -2,4 +2,4 @@
 ⇑(⇑f a) b : expr
 ⇑(⇑(⇑f a) b) a : expr
 f a b a : expr
-@coe_fn.{1 1} expr expr_to_app (@coe_fn.{1 1} expr expr_to_app f a) b : expr
+@coe_fn.{1 1} (expr bool.tt) expr_to_app (@coe_fn.{1 1} (expr bool.tt) expr_to_app f a) b : expr bool.tt

tests/lean/macro_args.lean

@@ -1 +1 @@
-#eval ``({pos . line := has_zero.zero, col := 1}).to_raw_expr.to_raw_fmt
+#eval ``({pos . line := has_zero.zero, col := 1}).to_raw_fmt

tests/lean/run/check_constants.lean

@@ -294,8 +294,6 @@ run_cmd script_check_id `pprod.mk
 run_cmd script_check_id `pprod.fst
 run_cmd script_check_id `pprod.snd
 run_cmd script_check_id `propext
-run_cmd script_check_id `pexpr
-run_cmd script_check_id `pexpr.subst
 run_cmd script_check_id `to_pexpr
 run_cmd script_check_id `quot.mk
 run_cmd script_check_id `quot.lift

tests/lean/run/meta_expr1.lean

@@ -30,7 +30,7 @@ meta definition v1 := expr.app (expr.app (expr.const `f []) (expr.mk_var 0)) (ex
 
 #eval expr.instantiate_vars v1 [expr.const `a [], expr.const `b []]
 
-meta definition fv1 :=
+meta definition fv1 : expr :=
 expr.app
   (expr.app (expr.const `f [])
             (expr.local_const `a `a binder_info.default (expr.sort level.zero)))