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

fix(library/compiler/llnf): user numeric literals to store enum type values in LLNF

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-31 17:58:03 -08:00
parent 7a322340cb
commit ddc5cf05c4
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/compiler/llnf.cpp
View file

@ -768,6 +768,12 @@ class to_llnf_fn {
cnstr_info k_info = get_cnstr_info(const_name(k));
unsigned nparams = k_val.get_nparams();
unsigned cidx = k_info.m_cidx;
name const & I = const_name(k).get_prefix();
if (optional<unsigned> r = ::lean::is_enum_type(env(), I)) {
/* We use a literal for enumeration types. */
expr x = mk_let_decl(*to_uint_type(*r), mk_lit(literal(nat(cidx))));
return x;
}
buffer<expr> obj_args;
unsigned j = nparams;
for (field_info const & info : k_info.m_field_info) {