From a7af70da2e3f914a60cfa63d490bcffcc22572e2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Nov 2016 11:50:38 -0800 Subject: [PATCH] feat(library/vm): add expr.copy_pos_info --- library/init/meta/expr.lean | 14 ++++++++------ src/library/vm/vm_expr.cpp | 6 ++++++ 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index b1c06f1a82..4ae0a387fb 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -73,12 +73,14 @@ meta def expr.abstract : expr → expr → expr meta constant expr.instantiate_var : expr → expr → expr meta constant expr.instantiate_vars : expr → list expr → expr -meta constant expr.has_var : expr → bool -meta constant expr.has_var_idx : expr → nat → bool -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 +meta constant expr.has_var : expr → bool +meta constant expr.has_var_idx : expr → nat → bool +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 +/- (copy_pos_info src tgt) copy position information from src to tgt. -/ +meta constant expr.copy_pos_info : expr → expr → expr namespace expr open decidable diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 4fc92c1b91..b087074d9d 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" #include "kernel/replace_fn.h" #include "library/expr_lt.h" +#include "library/deep_copy.h" #include "library/vm/vm.h" #include "library/vm/vm_nat.h" #include "library/vm/vm_string.h" @@ -313,6 +314,10 @@ vm_obj expr_hash(vm_obj const & e) { return mk_vm_simple(r); // make sure it is a simple value } +vm_obj expr_copy_pos_info(vm_obj const & src, vm_obj const & tgt) { + return to_obj(copy_tag(to_expr(src), copy(to_expr(tgt)))); +} + void initialize_vm_expr() { DECLARE_VM_BUILTIN(name({"expr", "var"}), expr_var); DECLARE_VM_BUILTIN(name({"expr", "sort"}), expr_sort); @@ -344,6 +349,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", "copy_pos_info"}), expr_copy_pos_info); DECLARE_VM_CASES_BUILTIN(name({"expr", "cases_on"}), expr_cases_on); }