From fb6c9f28795debe200cdcd0e12ee73bebd2799bc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Jun 2016 11:26:19 -0700 Subject: [PATCH] feat(library/vm/vm_expr): add more functions to 'expr' API --- library/meta/expr.lean | 7 +++ src/library/vm/vm_expr.cpp | 92 ++++++++++++++++++++++++++++++++++ src/library/vm/vm_name.cpp | 16 ++++++ src/library/vm/vm_name.h | 2 + src/library/vm/vm_nat.cpp | 12 +++++ src/library/vm/vm_nat.h | 1 + tests/lean/run/meta_expr1.lean | 40 ++++++++++++++- 7 files changed, 169 insertions(+), 1 deletion(-) diff --git a/library/meta/expr.lean b/library/meta/expr.lean index cf045de7c6..f28b75b801 100644 --- a/library/meta/expr.lean +++ b/library/meta/expr.lean @@ -50,3 +50,10 @@ meta_constant expr.abstract_fvs : expr → list name → 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_free_var : 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 diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index dfa0f78f8f..688320ace0 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -7,6 +7,10 @@ Author: Leonardo de Moura #include #include #include "kernel/expr.h" +#include "kernel/free_vars.h" +#include "kernel/instantiate.h" +#include "kernel/abstract.h" +#include "kernel/for_each_fn.h" #include "library/expr_lt.h" #include "library/vm/vm.h" #include "library/vm/vm_nat.h" @@ -237,6 +241,83 @@ vm_obj expr_lex_lt(vm_obj const & o1, vm_obj const & o2) { return mk_vm_bool(is_lt(to_expr(o1), to_expr(o2), false)); } +vm_obj expr_fold(vm_obj const &, vm_obj const & e, vm_obj const & a, vm_obj const & fn) { + vm_obj r = a; + for_each(to_expr(e), [&](expr const & o, unsigned d) { + r = invoke(fn, to_obj(o), mk_vm_nat(d), r); + return true; + }); + return r; +} + +vm_obj expr_instantiate_var(vm_obj const & e, vm_obj const & v) { + return to_obj(instantiate(to_expr(e), to_expr(v))); +} + +vm_obj expr_instantiate_vars(vm_obj const & e, vm_obj const & vs) { + buffer vs_buf; + to_buffer_expr(vs, vs_buf); + return to_obj(instantiate(to_expr(e), vs_buf.size(), vs_buf.data())); +} + +vm_obj expr_abstract_fv(vm_obj const & e, vm_obj const & n) { + return to_obj(abstract_local(to_expr(e), to_name(n))); +} + +static void list_name_to_buffer_local(vm_obj const & o, buffer & r) { + if (is_simple(o)) { + return; + } else { + expr dummy = mk_Prop(); + r.push_back(mk_local(to_name(cfield(o, 0)), dummy)); + list_name_to_buffer_local(cfield(o, 1), r); + } +} + +vm_obj expr_abstract_fvs(vm_obj const & e, vm_obj const & ns) { + buffer locals; + list_name_to_buffer_local(ns, locals); + return to_obj(abstract_locals(to_expr(e), locals.size(), locals.data())); +} + +vm_obj expr_has_var(vm_obj const & e) { + return mk_vm_bool(!closed(to_expr(e))); +} + +vm_obj expr_has_var_idx(vm_obj const & e, vm_obj const & u) { + if (auto n = try_to_unsigned(u)) { + return mk_vm_bool(has_free_var(to_expr(e), *n)); + } else { + return mk_vm_false(); + } +} + +vm_obj expr_has_free_var(vm_obj const & e) { + return mk_vm_bool(has_local(to_expr(e))); +} + +vm_obj expr_has_meta_var(vm_obj const & e) { + return mk_vm_bool(has_metavar(to_expr(e))); +} + +vm_obj expr_lift_vars(vm_obj const & e, vm_obj const & n1, vm_obj const & n2) { + auto u1 = try_to_unsigned(n1); + auto u2 = try_to_unsigned(n2); + if (u1 && u2) + return to_obj(lift_free_vars(to_expr(e), *u1, *u2)); + else + return e; +} + +vm_obj expr_lower_vars(vm_obj const & e, vm_obj const & n1, vm_obj const & n2) { + auto u1 = try_to_unsigned(n1); + auto u2 = try_to_unsigned(n2); + if (u1 && u2) + return to_obj(lower_free_vars(to_expr(e), *u1, *u2)); + else + return e; +} + void initialize_vm_expr() { DECLARE_VM_BUILTIN(name({"expr", "var"}), expr_var); DECLARE_VM_BUILTIN(name({"expr", "sort"}), expr_sort); @@ -255,6 +336,17 @@ void initialize_vm_expr() { DECLARE_VM_BUILTIN(name({"expr", "to_string"}), expr_to_string); 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", "instantiate_var"}), expr_instantiate_var); + DECLARE_VM_BUILTIN(name({"expr", "instantiate_vars"}), expr_instantiate_vars); + DECLARE_VM_BUILTIN(name({"expr", "abstract_fv"}), expr_abstract_fv); + DECLARE_VM_BUILTIN(name({"expr", "abstract_fvs"}), expr_abstract_fvs); + DECLARE_VM_BUILTIN(name({"expr", "has_var"}), expr_has_var); + DECLARE_VM_BUILTIN(name({"expr", "has_var_idx"}), expr_has_var_idx); + DECLARE_VM_BUILTIN(name({"expr", "has_free_var"}), expr_has_free_var); + DECLARE_VM_BUILTIN(name({"expr", "has_meta_var"}), expr_has_meta_var); + DECLARE_VM_BUILTIN(name({"expr", "lift_vars"}), expr_lift_vars); + DECLARE_VM_BUILTIN(name({"expr", "lower_vars"}), expr_lower_vars); DECLARE_VM_CASES_BUILTIN(name({"expr", "cases_on"}), expr_cases_on); } diff --git a/src/library/vm/vm_name.cpp b/src/library/vm/vm_name.cpp index a0f8e000cb..225cb24d49 100644 --- a/src/library/vm/vm_name.cpp +++ b/src/library/vm/vm_name.cpp @@ -28,6 +28,22 @@ vm_obj to_obj(name const & n) { return mk_vm_external(new vm_name(n)); } +list to_list_name(vm_obj const & o) { + if (is_simple(o)) + return list(); + else + return list(to_name(cfield(o, 0)), to_list_name(cfield(o, 1))); +} + +void to_buffer_name(vm_obj const & o, buffer & r) { + if (is_simple(o)) { + return; + } else { + r.push_back(to_name(cfield(o, 0))); + to_buffer_name(cfield(o, 1), r); + } +} + vm_obj name_anonymous() { return to_obj(name()); } diff --git a/src/library/vm/vm_name.h b/src/library/vm/vm_name.h index 6cbbd65aaa..5881b54363 100644 --- a/src/library/vm/vm_name.h +++ b/src/library/vm/vm_name.h @@ -10,6 +10,8 @@ Author: Leonardo de Moura namespace lean { name const & to_name(vm_obj const & o); vm_obj to_obj(name const & n); +list to_list_name(vm_obj const & o); +void to_buffer_name(vm_obj const & o, buffer & r); void initialize_vm_name(); void finalize_vm_name(); } diff --git a/src/library/vm/vm_nat.cpp b/src/library/vm/vm_nat.cpp index b737b67965..a63e26621f 100644 --- a/src/library/vm/vm_nat.cpp +++ b/src/library/vm/vm_nat.cpp @@ -33,6 +33,18 @@ unsigned to_unsigned(vm_obj const & o) { return to_mpz(o).get_unsigned_int(); } +optional try_to_unsigned(vm_obj const & o) { + if (is_simple(o)) { + return optional(cidx(o)); + } else { + mpz const & v = to_mpz(o); + if (v.is_unsigned_int()) + return optional(v.get_unsigned_int()); + else + return optional(); + } +} + MK_THREAD_LOCAL_GET_DEF(mpz, get_mpz1); MK_THREAD_LOCAL_GET_DEF(mpz, get_mpz2); diff --git a/src/library/vm/vm_nat.h b/src/library/vm/vm_nat.h index bf6c0b338b..e55ca9d365 100644 --- a/src/library/vm/vm_nat.h +++ b/src/library/vm/vm_nat.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura namespace lean { unsigned to_unsigned(vm_obj const & o); +optional try_to_unsigned(vm_obj const & o); void initialize_vm_nat(); void finalize_vm_nat(); } diff --git a/tests/lean/run/meta_expr1.lean b/tests/lean/run/meta_expr1.lean index 8f12fef6ab..66e2ad8529 100644 --- a/tests/lean/run/meta_expr1.lean +++ b/tests/lean/run/meta_expr1.lean @@ -1,4 +1,42 @@ import meta open unsigned list -vm_eval expr.app (expr.app (expr.const "f" []) (expr.mk_var 1)) (expr.const "a" []) +meta_definition e1 := expr.app (expr.app (expr.const "f" []) (expr.mk_var 1)) (expr.const "a" []) + +vm_eval e1 + +vm_eval expr.fold e1 (0:nat) (λ e d n, n+1) + +meta_definition l1 := expr.lam "a" binder_info.default (expr.sort level.zero) (expr.mk_var 0) +meta_definition l2 := expr.lam "b" binder_info.default (expr.sort level.zero) (expr.mk_var 0) +meta_definition l3 := expr.lam "a" binder_info.default (expr.const "nat" []) (expr.mk_var 0) + +vm_eval l1 +vm_eval l2 +vm_eval l3 +vm_eval decidable.to_bool (l1 = l2) +vm_eval decidable.to_bool (l1 =ₐ l2) + +vm_eval expr.lex_lt (expr.const "a" []) (expr.const "b" []) +vm_eval expr.lt (expr.const "a" []) (expr.const "b" []) + +meta_definition v1 := expr.app (expr.app (expr.const "f" []) (expr.mk_var 0)) (expr.mk_var 1) + +vm_eval v1 +vm_eval expr.instantiate_var v1 (expr.const "a" []) + +vm_eval expr.instantiate_vars v1 [expr.const "a" [], expr.const "b" []] + +meta_definition fv1 := expr.app (expr.app (expr.const "f" []) + (expr.free_var "a" "a" binder_info.default (expr.sort level.zero))) + (expr.free_var "b" "b" binder_info.default (expr.sort level.zero)) + +vm_eval fv1 + +vm_eval expr.abstract_fv (expr.abstract_fv fv1 "a") "b" +vm_eval expr.abstract_fvs fv1 ["a", "b"] +vm_eval expr.abstract_fvs fv1 ["b", "a"] +vm_eval expr.lift_vars (expr.abstract_fvs fv1 ["b", "a"]) 1 1 +vm_eval expr.has_free_var fv1 +vm_eval expr.has_var fv1 +vm_eval expr.has_var (expr.abstract_fvs fv1 ["b", "a"])