michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library): remove unnecessary files

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-22 23:20:21 -08:00
parent d836e45452
commit 0b3599851d
2 changed files with 0 additions and 119 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
src/library/context_to_lambda.cpp
View file

@ -1,59 +0,0 @@
/*
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 "library/context_to_lambda.h"
namespace lean {
static expr g_fake = Const(name::mk_internal_unique_name());
expr context_to_lambda(context::iterator it, context::iterator const & end, expr const & e) {
if (it == end) {
return e;
} else {
context_entry const & entry = *it;
optional<expr> t;
optional<expr> const & d = entry.get_domain();
optional<expr> const & b = entry.get_body();
lean_assert(b || d);
if (b && d)
t = mk_app(g_fake, *d, *b);
else if (d)
t = mk_app(g_fake, *d, g_fake);
else
t = mk_app(g_fake, g_fake, *b);
lean_assert(t);
return context_to_lambda(++it, end, mk_lambda(entry.get_name(), *t, e));
}
}
expr context_to_lambda(context const & c, expr const & e) {
return context_to_lambda(c.begin(), c.end(), e);
}
bool is_fake_context(expr const & e) {
return is_lambda(e) && is_app(abst_domain(e)) && arg(abst_domain(e), 0) == g_fake;
}
name const & fake_context_name(expr const & e) {
lean_assert(is_fake_context(e));
return abst_name(e);
}
optional<expr> fake_context_domain(expr const & e) {
lean_assert(is_fake_context(e));
expr r = arg(abst_domain(e), 1);
if (!is_eqp(r, g_fake))
return some_expr(r);
else
return none_expr();
}
optional<expr> fake_context_value(expr const & e) {
lean_assert(is_fake_context(e));
expr r = arg(abst_domain(e), 2);
if (!is_eqp(r, g_fake))
return some_expr(r);
else
return none_expr();
}
expr const & fake_context_rest(expr const & e) {
return abst_body(e);
}
}

60
src/library/context_to_lambda.h
View file

@ -1,60 +0,0 @@
/*
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 "kernel/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 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
The constant "fake" 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 (fake T_i).
*/
expr context_to_lambda(context const & c, expr const & e);
/**
\brief Return true if \c e is a fake context created using
context_to_lambda.
(lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
*/
bool is_fake_context(expr const & e);
/**
\brief Return the name n_1 of the head of the (fake) context
(lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
\pre is_fake_context(e)
*/
name const & fake_context_name(expr const & e);
/**
\brief Return the domain T_1 of the head of the (fake) context
(lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
\pre is_fake_context(e)
*/
optional<expr> fake_context_domain(expr const & e);
/**
\brief Return (if available) the value V_1 of the head of the (fake) context
(lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
\pre is_fake_context(e)
*/
optional<expr> fake_context_value(expr const & e);
/**
\brief Return the rest (lambda (n_2 : (fake T_2 V_2)) ... (lambda (n_k : (fake T_k V_k)) e)) of the fake context
(lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
\pre is_fake_context(e)
*/
expr const & fake_context_rest(expr const & e);
}