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

refactor(kernel): delete update_expr

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-18 23:15:12 -08:00
parent b5f0f28009
commit 101888e079
2 changed files with 0 additions and 131 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

78
src/kernel/update_expr.cpp
View file

@ -1,78 +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 "util/buffer.h"
#include "kernel/update_expr.h"
namespace lean {
expr update_app(expr const & app, unsigned i, expr const & new_arg) {
if (is_eqp(arg(app, i), new_arg)) {
return app;
} else {
buffer<expr> new_args;
unsigned num = num_args(app);
for (unsigned j = 0; j < num; j++) {
if (i == j)
new_args.push_back(new_arg);
else
new_args.push_back(arg(app, j));
}
return mk_app(new_args);
}
}
expr update_app(expr const & app, unsigned num_new_args, expr const * new_args) {
unsigned i;
unsigned num = num_args(app);
if (num != num_new_args)
return mk_app(num_new_args, new_args);
for (i = 0; i < num; i++) {
if (!is_eqp(arg(app, i), new_args[i]))
break;
}
if (i < num)
return mk_app(num, new_args);
else
return app;
}
expr update_lambda(expr const & lambda, expr const & d, expr const & b) {
if (is_eqp(abst_domain(lambda), d) && is_eqp(abst_body(lambda), b))
return lambda;
else
return mk_lambda(abst_name(lambda), d, b);
}
expr update_pi(expr const & pi, expr const & d, expr const & b) {
if (is_eqp(abst_domain(pi), d) && is_eqp(abst_body(pi), b))
return pi;
else
return mk_pi(abst_name(pi), d, b);
}
expr update_sigma(expr const & sig, expr const & d, expr const & b) {
if (is_eqp(abst_domain(sig), d) && is_eqp(abst_body(sig), b))
return sig;
else
return mk_sigma(abst_name(sig), d, b);
}
expr update_abstraction(expr const & abst, expr const & d, expr const & b) {
switch (abst.kind()) {
case expr_kind::Lambda: return update_lambda(abst, d, b);
case expr_kind::Pi: return update_pi(abst, d, b);
case expr_kind::Sigma: return update_sigma(abst, d, b);
default: lean_unreachable();
}
}
expr update_let(expr const & let, optional<expr> const & t, expr const & v, expr const & b) {
if (is_eqp(let_type(let), t) && is_eqp(let_value(let), v) && is_eqp(let_body(let), b))
return let;
else
return mk_let(let_name(let), t, v, b);
}
}

53
src/kernel/update_expr.h
View file

@ -1,53 +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/expr.h"
namespace lean {
/**
\brief Return an application equal to \c app but argument \c i has been replaced with \c new_arg.
\remark Return \c app if <tt>is_eqp(new_arg, app[i])</tt>.
*/
expr update_app(expr const & app, unsigned i, expr const & new_arg);
expr update_app(expr const & app, unsigned num_args, expr const * new_args);
inline expr update_app(expr const & app, buffer<expr> const & new_args) { return update_app(app, new_args.size(), new_args.data()); }
/**
\brief Return a lambda expression based on \c lambda with domain \c d and \c body b.
\remark Return \c lambda if the given domain and body are (pointer) equal to the ones in \c lambda.
*/
expr update_lambda(expr const & lambda, expr const & d, expr const & b);
/**
\brief Return a Pi expression based on \c pi with domain \c d and \c body b.
\remark Return \c pi if the given domain and body are (pointer) equal to the ones in \c pi.
*/
expr update_pi(expr const & pi, expr const & d, expr const & b);
/**
\brief Return a Sigma expression based on \c sig with domain \c d and \c body b.
\remark Return \c sig if the given domain and body are (pointer) equal to the ones in \c sig.
*/
expr update_sigma(expr const & sig, expr const & d, expr const & b);
/**
\brief Return a lambda/pi expression based on \c abst with domain \c d and \c body b.
*/
expr update_abstraction(expr const & abst, expr const & d, expr const & b);
/**
\brief Return a let expression based on \c let with type \c t value \c v and \c body b.
\remark Return \c let if the given value and body are (pointer) equal to the ones in \c let.
*/
expr update_let(expr const & let, optional<expr> const & t, expr const & v, expr const & b);
/**
\brief Return a new equality with lhs \c l and rhs \c r.
\remark Return \c eq if the given lhs and rhs are (pointer) equal to the ones in \c eq.
*/
expr update_heq(expr const & eq, expr const & l, expr const & r);
}