Flip order of the arguments for instance and abstract. Simplify type_checker.

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

src/kernel/abstract.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "replace.h"
 
 namespace lean {
-expr abstract(unsigned n, expr const * s, expr const & e) {
+expr abstract(expr const & e, unsigned n, expr const * s) {
     lean_assert(std::all_of(s, s+n, closed));
 
     auto f = [=](expr const & e, unsigned offset) -> expr {
@@ -24,7 +24,7 @@ expr abstract(unsigned n, expr const * s, expr const & e) {
 
     return replace_fn<decltype(f)>(f)(e);
 }
-expr abstract_p(unsigned n, expr const * s, expr const & e) {
+expr abstract_p(expr const & e, unsigned n, expr const * s) {
     lean_assert(std::all_of(s, s+n, closed));
 
     auto f = [=](expr const & e, unsigned offset) -> expr {

src/kernel/abstract.h

@@ -15,8 +15,8 @@ namespace lean {
 
    \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables).
 */
-expr abstract(unsigned n, expr const * s, expr const & e);
+expr abstract(expr const & e, unsigned n, expr const * s);
-inline expr abstract(expr const & s, expr const & e) { return abstract(1, &s, e); }
+inline expr abstract(expr const & e, expr const & s) { return abstract(e, 1, &s); }
 
 /**
    \brief Replace the expressions s[0], ..., s[n-1] in e with var(n-1), ..., var(0).
@@ -25,17 +25,17 @@ inline expr abstract(expr const & s, expr const & e) { return abstract(1, &s, e)
 
    \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables).
 */
-expr abstract_p(unsigned n, expr const * s, expr const & e);
+expr abstract_p(expr const & e, unsigned n, expr const * s);
-inline expr abstract_p(expr const & s, expr const & e) { return abstract_p(1, &s, e); }
+inline expr abstract_p(expr const & e, expr const & s) { return abstract_p(e, 1, &s); }
 
 /**
-   \brief Create a lambda expression (lambda (x : t) b), the term b is abstracted using abstract(constant(x), b).
+   \brief Create a lambda expression (lambda (x : t) b), the term b is abstracted using abstract(b, constant(x)).
 */
-inline expr fun(name const & n, expr const & t, expr const & b) { return lambda(n, t, abstract(constant(n), b)); }
+inline expr fun(name const & n, expr const & t, expr const & b) { return lambda(n, t, abstract(b, constant(n))); }
 inline expr fun(char const * n, expr const & t, expr const & b) { return fun(name(n), t, b); }
 /**
-   \brief Create a Pi expression (pi (x : t) b), the term b is abstracted using abstract(constant(x), b).
+   \brief Create a Pi expression (pi (x : t) b), the term b is abstracted using abstract(b, constant(x)).
 */
-inline expr Fun(name const & n, expr const & t, expr const & b) { return pi(n, t, abstract(constant(n), b)); }
+inline expr Fun(name const & n, expr const & t, expr const & b) { return pi(n, t, abstract(b, constant(n))); }
 inline expr Fun(char const * n, expr const & t, expr const & b) { return Fun(name(n), t, b); }
 }

src/kernel/instantiate.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "replace.h"
 
 namespace lean {
-expr instantiate_with_closed(unsigned n, expr const * s, expr const & e) {
+expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) {
     lean_assert(std::all_of(s, s+n, closed));
 
     auto f = [=](expr const & e, unsigned offset) -> expr {
@@ -26,7 +26,7 @@ expr instantiate_with_closed(unsigned n, expr const * s, expr const & e) {
     };
     return replace_fn<decltype(f)>(f)(e);
 }
-expr instantiate(unsigned n, expr const * s, expr const & e) {
+expr instantiate(expr const & e, unsigned n, expr const * s) {
     auto f = [=](expr const & e, unsigned offset) -> expr {
         if (is_var(e)) {
             unsigned vidx = var_idx(e);

src/kernel/instantiate.h

@@ -13,13 +13,13 @@ namespace lean {
 
    \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables).
 */
-expr instantiate_with_closed(unsigned n, expr const * s, expr const & e);
+expr instantiate_with_closed(expr const & e, unsigned n, expr const * s);
-inline expr instantiate_with_closed(expr const & s, expr const & e) { return instantiate_with_closed(1, &s, e); }
+inline expr instantiate_with_closed(expr const & e, expr const & s) { return instantiate_with_closed(e, 1, &s); }
 
 /**
    \brief Replace the free variables with indices 0,...,n-1 with s[n-1],...,s[0] in e.
 */
-expr instantiate(unsigned n, expr const * s, expr const & e);
+expr instantiate(expr const & e, unsigned n, expr const * s);
-inline expr instantiate(expr const & s, expr const & e) { return instantiate(1, &s, e); }
+inline expr instantiate(expr const & e, expr const & s) { return instantiate(e, 1, &s); }
 
 }

src/kernel/type_check.cpp

@@ -41,16 +41,21 @@ class infer_type_fn {
         throw exception(buffer.str());
     }
 
-    expr infer_pi(expr const & e, context const & ctx) {
+    expr check_pi(expr const & e, context const & ctx) {
-        lean_trace("type_check", tout << "infer pi\n" << e << "\n";);
+        if (is_pi(e))
-        expr p = normalize(infer_type(e, ctx), ctx);
+            return e;
-        if (is_pi(p))
+        expr r = normalize(e, ctx);
-            return p;
+        if (is_pi(r))
+            return r;
         std::ostringstream buffer;
         buffer << "function expected, in context:\n" << ctx << "\ngiven:\n" << e;
         throw exception(buffer.str());
     }
 
+    expr infer_pi(expr const & e, context const & ctx) {
+        return check_pi(infer_type(e, ctx), ctx);
+    }
+
     bool check_type_core(expr const & expected, expr const & given) {
         if (expected == given)
             return true;
@@ -84,19 +89,19 @@ class infer_type_fn {
         case expr_kind::Var:      return lookup(ctx, var_idx(e));
         case expr_kind::Type:     return type(ty_level(e) + 1);
         case expr_kind::App: {
-            expr f       = arg(e, 0);
+            expr f_t     = infer_pi(arg(e, 0), ctx);
             unsigned i   = 1;
             unsigned num = num_args(e);
             lean_assert(num >= 2);
             while (true) {
                 expr const & c = arg(e, i);
-                expr f_t       = infer_pi(f, ctx);
                 expr c_t       = infer_type(c, ctx);
                 check_type(e, i, abst_domain(f_t), c_t, ctx);
-                f = instantiate(abst_body(f_t), c);
+                f_t = instantiate(abst_body(f_t), c);
                 i++;
                 if (i == num)
-                    return f;
+                    return f_t;
+                check_pi(f_t, ctx);
             }
         }
         case expr_kind::Lambda: {

src/tests/kernel/expr.cpp

@@ -284,8 +284,8 @@ void tst10() {
 
    \pre s and t must be closed expressions (i.e., no free variables)
 */
-inline expr substitute(expr const & s, expr const & t, expr const & e) {
+inline expr substitute(expr const & e, expr const & s, expr const & t) {
-    return instantiate(t, abstract(s, e));
+    return instantiate(abstract(e, s), t);
 }
 
 void tst11() {
@@ -295,20 +295,20 @@ void tst11() {
     expr x = var(0);
     expr y = var(1);
     expr t = type(level());
-    std::cout << instantiate(f(a), lambda("x", t, f(f(y, b), f(x, y)))) << "\n";
+    std::cout << instantiate(lambda("x", t, f(f(y, b), f(x, y))), f(a)) << "\n";
-    lean_assert(instantiate(f(a), lambda("x", t, f(f(y, b), f(x, y)))) ==
+    lean_assert(instantiate(lambda("x", t, f(f(y, b), f(x, y))), f(a)) ==
                 lambda("x", t, f(f(f(a), b), f(x, f(a)))));
-    std::cout << abstract(constant("a"), lambda("x", t, f(a, lambda("y", t, f(b, a))))) << "\n";
+    std::cout << abstract(lambda("x", t, f(a, lambda("y", t, f(b, a)))), constant("a")) << "\n";
-    lean_assert(abstract(constant("a"), lambda("x", t, f(a, lambda("y", t, f(b, a))))) ==
+    lean_assert(abstract(lambda("x", t, f(a, lambda("y", t, f(b, a)))), constant("a")) ==
                 lambda("x", t, f(var(1), lambda("y", t, f(b, var(2))))));
-    std::cout << abstract_p(constant("a"), lambda("x", t, f(a, lambda("y", t, f(b, a))))) << "\n";
+    std::cout << abstract_p(lambda("x", t, f(a, lambda("y", t, f(b, a)))), constant("a")) << "\n";
-    lean_assert(abstract_p(constant("a"), lambda("x", t, f(a, lambda("y", t, f(b, a))))) ==
+    lean_assert(abstract_p(lambda("x", t, f(a, lambda("y", t, f(b, a)))), constant("a")) ==
                 lambda("x", t, f(a, lambda("y", t, f(b, a)))));
-    std::cout << abstract_p(a, lambda("x", t, f(a, lambda("y", t, f(b, a))))) << "\n";
+    std::cout << abstract_p(lambda("x", t, f(a, lambda("y", t, f(b, a)))), a) << "\n";
-    lean_assert(abstract_p(a, lambda("x", t, f(a, lambda("y", t, f(b, a))))) ==
+    lean_assert(abstract_p(lambda("x", t, f(a, lambda("y", t, f(b, a)))), a) ==
                 lambda("x", t, f(var(1), lambda("y", t, f(b, var(2))))));
 
-    lean_assert(substitute(f(a), b, f(f(f(a)))) == f(f(b)));
+    lean_assert(substitute(f(f(f(a))), f(a), b) == f(f(b)));
 }
 
 void tst12() {

src/tests/kernel/replace.cpp

@@ -24,21 +24,24 @@ static void tst1() {
     expr r = mk_big(f, 16, 0);
     expr n = constant(name(0u));
     for (unsigned i = 0; i < 20; i++) {
-        r = abstract(n, r);
+        r = abstract(r, n);
     }
 }
 
 static void tst2() {
     expr r = lambda("x", type(level()), app(var(0), var(1), var(2)));
-    std::cout << instantiate_with_closed(constant("a"), r) << std::endl;
+    std::cout << instantiate_with_closed(r, constant("a")) << std::endl;
-    lean_assert(instantiate_with_closed(constant("a"), r) == lambda("x", type(level()), app(var(0), constant("a"), var(1))));
+    lean_assert(instantiate_with_closed(r, constant("a")) == lambda("x", type(level()), app(var(0), constant("a"), var(1))));
-    lean_assert(instantiate_with_closed(constant("b"), instantiate_with_closed(constant("a"), r)) ==
+    lean_assert(instantiate_with_closed(instantiate_with_closed(r, constant("a")), constant("b")) ==
                 lambda("x", type(level()), app(var(0), constant("a"), constant("b"))));
-    std::cout << instantiate_with_closed(constant("a"), abst_body(r)) << std::endl;
+    std::cout << instantiate_with_closed(abst_body(r), constant("a")) << std::endl;
-    lean_assert(instantiate_with_closed(constant("a"), abst_body(r)) == app(constant("a"), var(0), var(1)));
+    lean_assert(instantiate_with_closed(abst_body(r), constant("a")) == app(constant("a"), var(0), var(1)));
-    std::cout << instantiate(var(10), r) << std::endl;
+    std::cout << instantiate(r, var(10)) << std::endl;
-    lean_assert(instantiate(var(10), r) == lambda("x", type(level()), app(var(0), var(11), var(1))));
+    lean_assert(instantiate(r, var(10)) == lambda("x", type(level()), app(var(0), var(11), var(1))));
- }
+    std::cout << pi("_", var(3), var(4)) << std::endl;
+    std::cout << instantiate(pi("_", var(3), var(4)), var(0)) << std::endl;
+    lean_assert(instantiate(pi("_", var(3), var(4)), var(0)) == pi("_", var(2), var(3)));
+}
 
 int main() {
     continue_on_violation(true);

src/tests/kernel/threads.cpp

@@ -31,7 +31,7 @@ static void mk(expr const & a) {
         h = max_sharing(h);
         lean_assert(closed(h));
         h = normalize(h);
-        h = abstract(a, h);
+        h = abstract(h, a);
         lean_assert(!closed(h));
         h = deep_copy(h);
     }