Add head_beta function

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

src/library/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp
-  formatter.cpp context_to_lambda.cpp state.cpp)
+  formatter.cpp context_to_lambda.cpp state.cpp beta.cpp)
 target_link_libraries(library ${LEAN_LIBS})

src/library/beta.cpp

@@ -0,0 +1,41 @@
+/*
+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 "beta.h"
+#include "instantiate.h"
+
+namespace lean {
+bool is_head_beta(expr const & e) {
+    return is_app(e) && is_lambda(arg(e, 0));
+}
+expr head_beta(expr const & e) {
+    if (!is_head_beta(e)) {
+        return e;
+    } else {
+        unsigned num  = num_args(e);
+        unsigned num1 = num - 1;
+        expr const * f = &arg(e, 0);
+        lean_assert(is_lambda(*f));
+        unsigned m = 1;
+        while (is_lambda(abst_body(*f)) && m < num1) {
+            f = &abst_body(*f);
+            m++;
+        }
+        lean_assert(m <= num1);
+        expr r = instantiate(abst_body(*f), m, &arg(e, 1));
+        if (m == num1) {
+            return r;
+        } else {
+            buffer<expr> args;
+            args.push_back(r);
+            m++;
+            for (; m < num; m++)
+                args.push_back(arg(e, m));
+            return mk_app(args.size(), args.data());
+        }
+    }
+}
+}

src/library/beta.h

@@ -0,0 +1,19 @@
+/*
+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 "expr.h"
+
+namespace lean {
+/**
+    \brief Return true iff the given expression is of the form:
+
+    ((fun (x : A), B) Arg)
+*/
+bool is_head_beta(expr const & e);
+/** \brief Apply head beta-reduction to the given expression. */
+expr head_beta(expr const & e);
+};