michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/kernel_serializer): add assertions for invalid uses of anonymous names

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-07 08:26:45 -07:00
parent 955d7d2659
commit 6d6c62461f
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/kernel_serializer.cpp
View file

@ -159,6 +159,7 @@ class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp
s << var_idx(a);
break;
case expr_kind::Constant:
lean_assert(!const_name(a).is_anonymous());
s << const_name(a) << const_levels(a);
break;
case expr_kind::Sort:
@ -175,13 +176,17 @@ class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp
write_core(app_fn(a)); write_core(app_arg(a));
break;
case expr_kind::Lambda: case expr_kind::Pi:
lean_assert(!binding_name(a).is_anonymous());
write_binder_name(s, binding_name(a));
s << binding_info(a); write_core(binding_domain(a)); write_core(binding_body(a));
break;
case expr_kind::Meta:
lean_assert(!mlocal_name(a).is_anonymous());
s << mlocal_name(a); write_core(mlocal_type(a));
break;
case expr_kind::Local:
lean_assert(!mlocal_name(a).is_anonymous());
lean_assert(!local_pp_name(a).is_anonymous());
s << mlocal_name(a) << local_pp_name(a) << local_info(a); write_core(mlocal_type(a));
break;
}