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

feat(library/print): print mdata

Browse source 
Not sure if helpful or annoying for the future...
This commit is contained in:
Sebastian Ullrich 2018-09-02 16:18:03 -07:00
parent 3090826326
commit 0220af69b8
1 changed files with 20 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/library/print.cpp
View file

@ -208,6 +208,25 @@ struct print_expr_fn {
}
}
void print_mdata(expr const & a) {
out() << "[mdata ";
auto k = mdata_data(a);
while (!empty(k)) {
out() << head(k).fst() << ":";
auto const & v = head(k).snd();
switch (v.kind()) {
case data_value_kind::Bool: out() << v.get_bool(); break;
case data_value_kind::Name: out() << v.get_name(); break;
case data_value_kind::Nat: out() << v.get_nat(); break;
case data_value_kind::String: out() << escaped(v.get_string().data()); break;
}
out() << " ";
k = tail(k);
}
print(mdata_expr(a));
out() << "]";
}
void print(expr const & a) {
switch (a.kind()) {
case expr_kind::MVar:
@ -217,7 +236,7 @@ struct print_expr_fn {
out() << fix_name(local_pp_name(a));
break;
case expr_kind::MData:
out() << "[mdata "; print(mdata_expr(a)); out() << "]";
print_mdata(a);
break;
case expr_kind::Proj:
print(proj_expr(a)); out() << "." << proj_idx(a).to_mpz();