From 89703ce6694ed01871b5dcdcf1002b1df1ccd4f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 Oct 2016 09:23:40 -0700 Subject: [PATCH] feat(library/vm/vm_expr): expose replace --- library/init/meta/expr.lean | 3 ++- src/library/vm/vm_expr.cpp | 14 ++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index db00b7a3b3..3d0677f7f9 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -55,7 +55,8 @@ if expr.lt a b then ordering.lt else if a = b then ordering.eq else ordering.gt -meta constant expr.fold {A : Type} : expr → A → (expr → unsigned → A → A) → A +meta constant expr.fold {A : Type} : expr → A → (expr → nat → A → A) → A +meta constant expr.replace : expr → (expr → nat → option expr) → expr meta constant expr.abstract_local : expr → name → expr meta constant expr.abstract_locals : expr → list name → expr diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index c5874f1840..2008ed5ec6 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/for_each_fn.h" +#include "kernel/replace_fn.h" #include "library/expr_lt.h" #include "library/vm/vm.h" #include "library/vm/vm_nat.h" @@ -18,6 +19,7 @@ Author: Leonardo de Moura #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" @@ -223,6 +225,17 @@ vm_obj expr_fold(vm_obj const &, vm_obj const & e, vm_obj const & a, vm_obj cons return r; } +vm_obj expr_replace(vm_obj const & e, vm_obj const & fn) { + expr r = replace(to_expr(e), [&](expr const & o, unsigned d) { + vm_obj new_o = invoke(fn, to_obj(o), mk_vm_nat(d)); + if (is_none(new_o)) + return none_expr(); + else + return some_expr(to_expr(get_some_value(new_o))); + }); + return to_obj(r); +} + vm_obj expr_instantiate_var(vm_obj const & e, vm_obj const & v) { return to_obj(instantiate(to_expr(e), to_expr(v))); } @@ -315,6 +328,7 @@ void initialize_vm_expr() { DECLARE_VM_BUILTIN(name({"expr", "lt"}), expr_lt); DECLARE_VM_BUILTIN(name({"expr", "lex_lt"}), expr_lex_lt); DECLARE_VM_BUILTIN(name({"expr", "fold"}), expr_fold); + DECLARE_VM_BUILTIN(name({"expr", "replace"}), expr_replace); DECLARE_VM_BUILTIN(name({"expr", "instantiate_var"}), expr_instantiate_var); DECLARE_VM_BUILTIN(name({"expr", "instantiate_vars"}), expr_instantiate_vars); DECLARE_VM_BUILTIN(name({"expr", "abstract_local"}), expr_abstract_local);