max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/meta/pexpr): remove pexpr primitives

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-05 16:28:12 -07:00
parent ab481d7e7b
commit bd7138349a
2 changed files with 0 additions and 76 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
library/init/meta/pexpr.lean
View file

@ -11,25 +11,6 @@ universe u
@[reducible] meta def pexpr := expr ff
protected meta constant pexpr.of_expr : expr → pexpr
meta constant pexpr.is_placeholder : pexpr → bool
meta constant pexpr.mk_placeholder : pexpr
meta constant pexpr.mk_field_macro : pexpr → name → pexpr
meta constant pexpr.mk_explicit : pexpr → pexpr
/-- Choice macros are used to implement overloading. -/
meta constant pexpr.is_choice_macro : pexpr → bool
/-- Information about unelaborated structure instance expressions. -/
meta structure structure_instance_info :=
(struct : option name := none)
(field_names : list name)
(field_values : list pexpr)
(sources : list pexpr := [])
/-- Create a structure instance expression. -/
meta constant pexpr.mk_structure_instance : structure_instance_info → pexpr
meta constant pexpr.get_structure_instance_info : pexpr → option structure_instance_info
meta class has_to_pexpr (α : Sort u) :=
(to_pexpr : α → pexpr)

57
src/library/vm/vm_pexpr.cpp
View file

@ -21,65 +21,8 @@ vm_obj pexpr_of_expr(vm_obj const & e) {
return to_obj(mk_as_is(to_expr(e)));
}
vm_obj pexpr_is_placeholder(vm_obj const & e) {
return mk_vm_bool(is_placeholder(to_expr(e)));
}
vm_obj pexpr_mk_placeholder() {
return to_obj(mk_expr_placeholder());
}
vm_obj pexpr_mk_explicit(vm_obj const & e) {
return to_obj(mk_explicit(to_expr(e)));
}
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)));
}
vm_obj pexpr_is_choice_macro(vm_obj const & e) {
return mk_vm_bool(is_choice(to_expr(e)));
}
vm_obj pexpr_mk_structure_instance(vm_obj const & info) {
name struct_name;
buffer<name> field_names;
buffer<expr> field_values;
buffer<expr> sources;
if (!is_none(cfield(info, 0))) {
struct_name = to_name(get_some_value(cfield(info, 0)));
}
to_buffer_name(cfield(info, 1), field_names);
to_buffer_expr(cfield(info, 2), field_values);
to_buffer_expr(cfield(info, 3), sources);
return to_obj(mk_structure_instance(struct_name, field_names, field_values, sources));
}
vm_obj pexpr_get_structure_instance_info(vm_obj const & e) {
if (!is_structure_instance(to_expr(e))) {
return mk_vm_none();
}
auto info = get_structure_instance_info(to_expr(e));
optional<name> opt_struct_name;
if (info.m_struct_name) {
opt_struct_name = info.m_struct_name;
}
return mk_vm_some(mk_vm_constructor(0, to_obj(opt_struct_name), to_obj(info.m_field_names),
to_obj(info.m_field_values), to_obj(info.m_sources)));
}
void initialize_vm_pexpr() {
DECLARE_VM_BUILTIN(name({"pexpr", "of_expr"}), pexpr_of_expr);
DECLARE_VM_BUILTIN(name({"pexpr", "is_placeholder"}), pexpr_is_placeholder);
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("pexpr", "is_choice_macro"), pexpr_is_choice_macro);
DECLARE_VM_BUILTIN(name("pexpr", "mk_structure_instance"), pexpr_mk_structure_instance);
DECLARE_VM_BUILTIN(name("pexpr", "get_structure_instance_info"), pexpr_get_structure_instance_info);
}
void finalize_vm_pexpr() {