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

chore(library/init/lean/compiler/llnf): disable

Browse source 
I am going to refactor the interface with the new IR compiler.
This commit is contained in:
Leonardo de Moura 2019-05-15 19:00:06 -07:00
parent 77768c504e
commit 739008f8d4
1 changed files with 0 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/compiler/llnf.cpp
View file

@ -2415,20 +2415,12 @@ public:
}
};
static void display_ir(environment const & env, comp_decl const & decl) {
ir::decl d = to_ir_decl(env, decl);
ir::test(d);
}
pair<environment, comp_decls> to_llnf(environment const & env, comp_decls const & ds, bool unboxed) {
environment new_env = env;
buffer<comp_decl> rs;
buffer<comp_decl> bs;
for (comp_decl const & d : ds) {
expr new_v = to_lambda_pure_fn(new_env, unboxed)(d.snd());
if (unboxed) {
lean_trace(name({"compiler", "lambda_pure"}), tout() << "\n"; display_ir(new_env, comp_decl(d.fst(), new_v)););
}
new_v = push_proj_fn(new_env)(new_v);
new_v = insert_reset_reuse_fn(new_env, unboxed)(new_v);
new_v = simp_cases(new_env, new_v);