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

feat(library/compiler/lcnf): nat literals

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-29 16:52:25 -07:00
parent 54b4908349
commit 86d5ccf8f5
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/compiler/lcnf.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "kernel/replace_fn.h"
#include "library/expr_lt.h"
#include "library/util.h"
#include "library/num.h"
#include "library/aux_recursors.h"
#include "library/constants.h"
#include "library/projection.h"
@ -337,6 +338,13 @@ public:
}
expr visit_app(expr const & e, bool root) {
/* TODO(Leo): remove after we add support for literals in the front-end */
if (optional<mpz> v = to_num(e)) {
expr type = whnf_infer_type(e);
if (is_nat_type(type)) {
return mk_lit(literal(*v));
}
}
buffer<expr> args;
expr fn = get_app_args(e, args);
if (is_constant(fn)) {