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

feat(library/fo_unify): unify heterogeneous - homogeneous equality

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-05 19:00:31 -08:00
parent e1d44eec6b
commit c1afefb873
3 changed files with 22 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/kernel/expr.cpp
View file

@ -232,6 +232,16 @@ bool is_arrow(expr const & t) {
return is_pi(t) && !has_free_var(abst_body(t), 0);
}
bool is_eq(expr const & e, expr & lhs, expr & rhs) {
if (is_eq(e)) {
lhs = eq_lhs(e);
rhs = eq_rhs(e);
return true;
} else {
return false;
}
}
expr copy(expr const & a) {
switch (a.kind()) {
case expr_kind::Var: return mk_var(var_idx(a));

2
src/kernel/expr.h
View file

@ -504,6 +504,8 @@ inline name const & metavar_name(expr const & e) { return to_metavar(e)
inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e)->get_lctx(); }
inline bool has_metavar(expr const & e) { return e.has_metavar(); }
bool is_eq(expr const & e, expr & lhs, expr & rhs);
// =======================================
// =======================================

13
src/library/fo_unify.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include "kernel/builtin.h"
#include "library/fo_unify.h"
#include "library/expr_pair.h"
#include "library/kernel_bindings.h"
@ -19,11 +20,16 @@ static bool is_metavar_wo_local_context(expr const & e) {
return is_metavar(e) && !metavar_lctx(e);
}
static bool is_eq_heq(expr const & e, expr & lhs, expr & rhs) {
return is_eq(e, lhs, rhs) || is_homo_eq(e, lhs, rhs);
}
optional<substitution> fo_unify(expr e1, expr e2) {
lean_assert(e1);
lean_assert(e2);
substitution s;
unsigned i;
expr lhs1, rhs1, lhs2, rhs2;
buffer<expr_pair> todo;
todo.emplace_back(e1, e2);
while (!todo.empty()) {
@ -36,6 +42,9 @@ optional<substitution> fo_unify(expr e1, expr e2) {
assign(s, e1, e2);
} else if (is_metavar_wo_local_context(e2)) {
assign(s, e2, e1);
} else if (is_eq_heq(e1, lhs1, rhs1) && is_eq_heq(e2, lhs2, rhs2)) {
todo.emplace_back(lhs1, lhs2);
todo.emplace_back(rhs1, rhs2);
} else {
if (e1.kind() != e2.kind())
return optional<substitution>();
@ -52,9 +61,7 @@ optional<substitution> fo_unify(expr e1, expr e2) {
}
break;
case expr_kind::Eq:
todo.emplace_back(eq_rhs(e1), eq_rhs(e2));
todo.emplace_back(eq_lhs(e1), eq_lhs(e2));
break;
lean_unreachable(); break; // LCOV_EXCL_LINE
case expr_kind::Lambda: case expr_kind::Pi:
todo.emplace_back(abst_body(e1), abst_body(e2));
todo.emplace_back(abst_domain(e1), abst_domain(e2));