From 739008f8d4582607d3282cfcf8f49ee6832fd5d3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 May 2019 19:00:06 -0700 Subject: [PATCH] chore(library/init/lean/compiler/llnf): disable I am going to refactor the interface with the new IR compiler. --- src/library/compiler/llnf.cpp | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp index 78b7431360..a4fd348c2c 100644 --- a/src/library/compiler/llnf.cpp +++ b/src/library/compiler/llnf.cpp @@ -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 to_llnf(environment const & env, comp_decls const & ds, bool unboxed) { environment new_env = env; buffer rs; buffer 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);