max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(compiler/preprocess_rec): use tout

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-02 18:18:53 -07:00
parent da79cd7d95
commit ea3fae060f
1 changed files with 4 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/compiler/preprocess_rec.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include "kernel/declaration.h"
#include "kernel/type_checker.h"
#include "kernel/instantiate.h"
#include "library/trace.h"
#include "library/aux_recursors.h"
#include "library/user_recursors.h"
#include "library/util.h"
@ -17,9 +18,6 @@ Author: Leonardo de Moura
#include "compiler/inliner.h"
#include "compiler/lambda_lifting.h"
void pp_detail(lean::environment const & env, lean::expr const & e);
void pp(lean::environment const & env, lean::expr const & e);
namespace lean {
class expand_aux_recursors_fn : public compiler_step_visitor {
bool is_aux_recursor(expr const & e) {
@ -67,12 +65,11 @@ class preprocess_rec_fn {
void display(expr const & v) {
for (name const & n : m_aux_decls) {
std::cout << ">> " << n << "\n";
tout() << ">> " << n << "\n";
declaration d = m_env.get(n);
::pp_detail(m_env, d.get_value());
tout() << d.get_value() << "\n";
}
std::cout << ">> main\n";
::pp_detail(m_env, v);
tout() << ">> main\n" << v << "\n";
}
public: