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

Add normalization a = b for values (aka semantic attachments)

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-04 14:54:33 -07:00
parent f0ccb2a03e
commit 95447deea3
2 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/normalize.cpp
View file

@ -169,8 +169,9 @@ class normalize_fn {
expr new_r = reify(normalize(eq_rhs(a), s, k), k);
if (new_l == new_r) {
return svalue(bool_value(true));
} else if (is_value(new_l) && is_value(new_r)) {
return svalue(bool_value(false));
} else {
// TODO: Invoke semantic attachments.
return svalue(eq(new_l, new_r));
}
}

10
src/tests/kernel/arith.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include "environment.h"
#include "type_check.h"
#include "builtin.h"
#include "arith.h"
#include "normalize.h"
#include "abstract.h"
@ -74,11 +75,20 @@ static void tst4() {
lean_assert(normalize(e2, env) == fun("a", int_type(), app(int_sub(), constant("a"), int_value(-20))));
}
static void tst5() {
environment env;
expr e = eq(int_value(3), int_value(4));
std::cout << e << " --> " << normalize(e, env) << "\n";
lean_assert(normalize(e, env) == bool_value(false));
lean_assert(normalize(eq(constant("a"), int_value(3)), env) == eq(constant("a"), int_value(3)));
}
int main() {
continue_on_violation(true);
tst1();
tst2();
tst3();
tst4();
tst5();
return has_violations() ? 1 : 0;
}