From bb4920fcbc07a2da0818bcddcf2f6f883eb46007 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Wed, 15 Feb 2017 23:54:27 -0500 Subject: [PATCH] feat(library/vm/vm_expr): export instantiate_univ_params --- library/init/meta/expr.lean | 5 +++-- src/library/vm/vm_expr.cpp | 13 +++++++++++++ 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index b816fd3c6f..87f4d86cd2 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -83,8 +83,9 @@ meta def expr.abstract : expr → expr → expr | e (expr.local_const n m bi t) := e^.abstract_local n | e _ := e -meta constant expr.instantiate_var : expr → expr → expr -meta constant expr.instantiate_vars : expr → list expr → expr +meta constant expr.instantiate_univ_params : expr → list (name × level) → 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 diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 11cb089d1d..dd00fbc1e0 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -258,6 +258,18 @@ vm_obj expr_replace(vm_obj const & e, vm_obj const & fn) { return to_obj(r); } +vm_obj expr_instantiate_univ_params(vm_obj const & e, vm_obj const & nls) { + list names = to_list(nls, [](vm_obj const & p) { + lean_assert(csize(p) == 2); + return to_name(cfield(p, 0)); + } ); + list levels = to_list(nls, [](vm_obj const & p) { + lean_assert(csize(p) == 2); + return to_level(cfield(p, 1)); + } ); + return to_obj(instantiate_univ_params(to_expr(e), names, levels)); +} + vm_obj expr_instantiate_var(vm_obj const & e, vm_obj const & v) { return to_obj(instantiate(to_expr(e), to_expr(v))); } @@ -452,6 +464,7 @@ void initialize_vm_expr() { 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_univ_params"}), expr_instantiate_univ_params); 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);