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

fix(library/normalize): bug in the "eval" command

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-14 18:49:48 -08:00
parent 8ad9b84c85
commit 5a9cd9eed4
1 changed files with 16 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/library/normalize.cpp
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "kernel/inductive/inductive.h"
#include "library/reducible.h"
namespace lean {
@ -28,10 +29,22 @@ class normalize_fn {
expr normalize_app(expr const & e) {
buffer<expr> args;
bool modified = false;
expr f = get_app_rev_args(e, args);
for (expr & a : args)
a = normalize(a);
return mk_rev_app(f, args);
for (expr & a : args) {
expr new_a = normalize(a);
if (new_a != a)
modified = true;
a = new_a;
}
if (!modified)
return e;
expr r = mk_rev_app(f, args);
if (is_constant(f) && inductive::is_elim_rule(m_tc.env(), const_name(f))) {
return normalize(r);
} else {
return r;
}
}
expr normalize(expr e) {