From 93ab18df714acafeb347bcd6636fe132ded8a58a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 16 Aug 2013 18:59:56 -0700 Subject: [PATCH] Add context_to_lambda hack Signed-off-by: Leonardo de Moura --- src/exprlib/CMakeLists.txt | 2 +- src/exprlib/context_to_lambda.cpp | 24 ++++++++++++++++++++++++ src/exprlib/context_to_lambda.h | 26 ++++++++++++++++++++++++++ 3 files changed, 51 insertions(+), 1 deletion(-) create mode 100644 src/exprlib/context_to_lambda.cpp create mode 100644 src/exprlib/context_to_lambda.h diff --git a/src/exprlib/CMakeLists.txt b/src/exprlib/CMakeLists.txt index 902eaffc72..f7da763eba 100644 --- a/src/exprlib/CMakeLists.txt +++ b/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}) diff --git a/src/exprlib/context_to_lambda.cpp b/src/exprlib/context_to_lambda.cpp new file mode 100644 index 0000000000..4c66528b70 --- /dev/null +++ b/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)); + } +} +} diff --git a/src/exprlib/context_to_lambda.h b/src/exprlib/context_to_lambda.h new file mode 100644 index 0000000000..db83ade851 --- /dev/null +++ b/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); +}