Add context_to_lambda hack

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

src/exprlib/CMakeLists.txt

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

src/exprlib/context_to_lambda.cpp

@@ -0,0 +1,24 @@
+/*
+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 "context_to_lambda.h"
+
+namespace lean {
+static expr g_foo = Const("foo");
+expr context_to_lambda(context const & c, expr const & e) {
+    if (!c) {
+        return e;
+    } else {
+        context_entry const & entry = head(c);
+        expr t;
+        if (entry.get_body())
+            t = g_foo(entry.get_domain(), entry.get_body());
+        else
+            t = g_foo(entry.get_domain());
+        return context_to_lambda(tail(c), mk_lambda(entry.get_name(), t, e));
+    }
+}
+}

src/exprlib/context_to_lambda.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 "context.h"
+namespace lean {
+/**
+   \brief Given the context (n_1 : T_1 [:= V_1]) ... (n_k : T_k [:= V_k]) and expression e into,
+   return the "meaningless" lambda expression:
+
+   (lambda (n_1 : (foo T_1 V_1)) ... (lambda (n_k : (foo T_k V_k)) e))
+
+   The constant "foo" is irrelevant, it is just used as a marker.
+   It is used to "glue" T_i and V_i.
+
+   This little hack allows us to use the machinery for instantiating
+   lambdas with contexts.
+
+   \remark If a context entry (n_i : T_i [:= V_i]) does not have a
+   value V_i, then we just use (foo T_i).
+*/
+expr context_to_lambda(context const & c, expr const & e);
+}