feat(library/fo_unify): first order unification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/CMakeLists.txt

@@ -1,5 +1,6 @@
 add_library(library kernel_bindings.cpp basic_thms.cpp deep_copy.cpp
   max_sharing.cpp context_to_lambda.cpp io_state.cpp update_expr.cpp
-  type_inferer.cpp placeholder.cpp expr_lt.cpp hidden_defs.cpp)
+  type_inferer.cpp placeholder.cpp expr_lt.cpp hidden_defs.cpp
+  substitution.cpp fo_unify.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/fo_unify.cpp

@@ -0,0 +1,93 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <utility>
+#include "library/fo_unify.h"
+#include "library/expr_pair.h"
+#include "library/kernel_bindings.h"
+
+namespace lean {
+static void assign(substitution & s, expr const & mvar, expr const & e) {
+    lean_assert(is_metavar(mvar));
+    s.insert(metavar_name(mvar), e);
+}
+
+static bool is_metavar_wo_local_context(expr const & e) {
+    return is_metavar(e) && !metavar_lctx(e);
+}
+
+optional<substitution> fo_unify(expr e1, expr e2) {
+    lean_assert(e1);
+    lean_assert(e2);
+    substitution s;
+    unsigned i;
+    buffer<expr_pair> todo;
+    todo.emplace_back(e1, e2);
+    while (!todo.empty()) {
+        auto p = todo.back();
+        todo.pop_back();
+        e1 = find(s, p.first);
+        e2 = find(s, p.second);
+        if (e1 != e2) {
+            if (is_metavar_wo_local_context(e1)) {
+                assign(s, e1, e2);
+            } else if (is_metavar_wo_local_context(e2)) {
+                assign(s, e2, e1);
+            } else {
+                if (e1.kind() != e2.kind())
+                    return optional<substitution>();
+                switch (e1.kind()) {
+                case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::MetaVar:
+                    return optional<substitution>();
+                case expr_kind::App:
+                    if (num_args(e1) != num_args(e2))
+                        return optional<substitution>();
+                    i = num_args(e1);
+                    while (i > 0) {
+                        --i;
+                        todo.emplace_back(arg(e1, i), arg(e2, i));
+                    }
+                    break;
+                case expr_kind::Eq:
+                    todo.emplace_back(eq_rhs(e1), eq_rhs(e2));
+                    todo.emplace_back(eq_lhs(e1), eq_lhs(e2));
+                    break;
+                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));
+                    break;
+                case expr_kind::Let:
+                    todo.emplace_back(let_body(e1), let_body(e2));
+                    todo.emplace_back(let_value(e1), let_value(e2));
+                    if (static_cast<bool>(let_type(e1)) != static_cast<bool>(let_type(e2)))
+                        return optional<substitution>();
+                    if (let_type(e1)) {
+                        lean_assert(let_type(e2));
+                        todo.emplace_back(let_type(e1), let_type(e2));
+                    }
+                    break;
+                }
+            }
+        }
+    }
+    return optional<substitution>(s);
+}
+
+
+static int fo_unify(lua_State * L) {
+    optional<substitution> r = fo_unify(to_expr(L, 1), to_expr(L, 2));
+    if (!r) {
+        lua_pushnil(L);
+        return 1;
+    } else {
+        return push_substitution(L, *r);
+    }
+}
+
+void open_fo_unify(lua_State * L) {
+    SET_GLOBAL_FUN(fo_unify, "fo_unify");
+}
+}

src/library/fo_unify.h

@@ -0,0 +1,14 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/optional.h"
+#include "library/substitution.h"
+
+namespace lean {
+optional<substitution> fo_unify(expr e1, expr e2);
+void open_fo_unify(lua_State * L);
+}

src/library/register_module.h

@@ -10,6 +10,8 @@ Author: Leonardo de Moura
 #include "library/io_state.h"
 #include "library/type_inferer.h"
 #include "library/hidden_defs.h"
+#include "library/substitution.h"
+#include "library/fo_unify.h"
 
 namespace lean {
 inline void open_core_module(lua_State * L) {
@@ -17,6 +19,8 @@ inline void open_core_module(lua_State * L) {
     open_io_state(L);
     open_type_inferer(L);
     open_hidden_defs(L);
+    open_substitution(L);
+    open_fo_unify(L);
 }
 inline void register_core_module() {
     script_state::register_module(open_core_module);

src/library/substitution.cpp

@@ -0,0 +1,99 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/replace.h"
+#include "kernel/metavar.h"
+#include "library/substitution.h"
+#include "library/kernel_bindings.h"
+
+namespace lean {
+expr find(substitution & s, expr e) {
+    while (true) {
+        if (is_metavar(e)) {
+            expr * it = s.splay_find(metavar_name(e));
+            if (it == nullptr)
+                return e;
+            e = *it;
+        } else {
+            return e;
+        }
+    }
+}
+
+expr apply(substitution & s, expr const & e) {
+    auto f = [&](expr const & e, unsigned) -> expr {
+        if (is_metavar(e)) {
+            expr r = find(s, e);
+            if (r != e) {
+                if (has_metavar(r)) {
+                    r = apply(s, r);
+                    s.insert(metavar_name(e), r);
+                }
+                return apply_local_context(r, metavar_lctx(e));
+            } else {
+                return e;
+            }
+        } else {
+            return e;
+        }
+    };
+    return replace_fn<decltype(f)>(f)(e);
+}
+
+DECL_UDATA(substitution)
+
+static int substitution_size(lua_State * L) {
+    lua_pushinteger(L, to_substitution(L, 1).size());
+    return 1;
+}
+
+static int substitution_empty(lua_State * L) {
+    lua_pushboolean(L, to_substitution(L, 1).empty());
+    return 1;
+}
+
+static int substitution_find(lua_State * L) {
+    substitution & s = to_substitution(L, 1);
+    expr * it;
+    if (is_expr(L, 2)) {
+        expr const & e = to_expr(L, 2);
+        if (is_metavar(e))
+            it = s.splay_find(metavar_name(e));
+        else
+            throw exception("arg #2 must be a metavariable");
+    } else {
+        it = s.splay_find(to_name_ext(L, 2));
+    }
+    if (it)
+        push_expr(L, find(s, *it));
+    else
+        lua_pushnil(L);
+    return 1;
+}
+
+static int substitution_apply(lua_State * L) {
+    return push_expr(L, apply(to_substitution(L, 1), to_expr(L, 2)));
+}
+
+static const struct luaL_Reg substitution_m[] = {
+    {"__gc",              substitution_gc}, // never throws
+    {"__len",             safe_function<substitution_size>},
+    {"find",              safe_function<substitution_find>},
+    {"empty",             safe_function<substitution_empty>},
+    {"size",              safe_function<substitution_size>},
+    {"apply",             safe_function<substitution_apply>},
+    {0, 0}
+};
+
+void open_substitution(lua_State * L) {
+    luaL_newmetatable(L, substitution_mt);
+    lua_pushvalue(L, -1);
+    lua_setfield(L, -2, "__index");
+    setfuncs(L, substitution_m, 0);
+
+    SET_GLOBAL_FUN(substitution_pred, "is_substitution");
+}
+}

src/library/substitution.h

@@ -0,0 +1,26 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/lua.h"
+#include "util/splay_map.h"
+#include "util/name.h"
+#include "kernel/expr.h"
+
+namespace lean {
+/**
+   \brief Simpler version of metavar_env.
+   It is used in fo_unify
+*/
+typedef splay_map<name, expr, name_quick_cmp> substitution;
+/**
+   \brief Apply substitution \c s to \c e
+*/
+expr apply(substitution & s, expr const & e);
+expr find(substitution & s, expr e);
+UDATA_DEFS_CORE(substitution)
+void open_substitution(lua_State * L);
+}

tests/lua/unify1.lua

@@ -0,0 +1,30 @@
+local f, g, a, b, c, x = Consts("f, g, a, b, c, x")
+local m1 = mk_metavar("m1")
+local m2 = mk_metavar("m2")
+local m3 = mk_metavar("m3")
+local s  = fo_unify(f(m1, g(m2, c)), f(g(m2, a), g(m3, m3)))
+assert(s)
+assert(#s == 3)
+assert(s:find(m2) == c)
+assert(s:apply(f(m1, g(m2, c))) == s:apply(f(g(m2, a), g(m3, m3))))
+assert(not fo_unify(f(a), g(m2)))
+function must_unify(t1, t2)
+   local s = fo_unify(t1, t2)
+   assert(s)
+   print(t1, t2, s:apply(t1))
+   assert(s:apply(t1) == s:apply(t2))
+end
+Bool = Const("Bool")
+must_unify(Eq(a, m1), Eq(m2, m2))
+must_unify(Type(), m1)
+must_unify(fun(x, Bool, x), fun(x, Bool, m1))
+must_unify(Pi(x, Bool, x), Pi(x, Bool, m1))
+must_unify(Var(0), m1)
+must_unify(f(m1, m2, m3), f(m1, m1, m2))
+must_unify(mk_let("x", f(b), Var(0)), mk_let("y", f(m1), Var(0)))
+assert(not fo_unify(mk_let("x", Bool, f(b), Var(0)), mk_let("y", f(m1), Var(0))))
+assert(not fo_unify(mk_let("x", f(b), Var(0)), mk_let("y", Bool, f(m1), Var(0))))
+must_unify(mk_let("x", Bool, f(b), Var(0)), mk_let("y", Bool, f(m1), Var(0)))
+assert(not fo_unify(mk_let("x", Bool, f(b), Var(0)), fun(x, Bool, x)))
+must_unify(iVal(10), m1)
+must_unify(iVal(10), iVal(10))