max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/library/compiler
History
Leonardo de Moura cd8c154bcd feat(library/compiler/vm_compiler): clear runtime cost model 
The equation compiler uses different strategies for processing
recursive equations. Some of them may produce unclear runtime cost
model. For example, the following fibonacci functions was running in
linear time instead of exponential time because the equation compiler
used the brec_on recursor.

def fib : nat → nat
| 0     := 1
| 1     := 1
| (n+2) := fib (n+1) + fib n

@dselsam and @jroesch have reported examples were the equation compiler
produces a negative performance impact. The new test (`eval` function)
captures the problem reported by @jroesch. In this example, the runtime
should not depend on the "amount of fuel".

This commit addresses this issue.
2017-11-01 14:11:09 -07:00
..
CMakeLists.txt feat(library/compiler): create declarations for nested values 2016-12-12 10:37:58 -08:00
comp_irrelevant.cpp fix(library/quote): use opaque macro for elaborated expr quotations 2017-06-07 10:00:17 -07:00
comp_irrelevant.h
compiler_step_visitor.cpp fix(library/quote): use opaque macro for elaborated expr quotations 2017-06-07 10:00:17 -07:00
compiler_step_visitor.h feat(library/type_context): improved (and simplified) cache management for type_context 2016-08-23 17:56:58 -07:00
cse.cpp fix(library): change API and make sure we don't crash when searching for a non existing local decl 2017-02-07 09:38:19 -08:00
cse.h perf(library/compiler): add common subexpression elimination 2016-12-11 14:43:51 -08:00
elim_recursors.cpp perf(library/compiler/elim_recursors): beta_reduce ==> head_beta_reduce 2017-07-21 03:32:23 -07:00
elim_recursors.h feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information 2016-11-09 16:51:48 -08:00
elim_unused_lets.cpp chore(library/compiler/elim_unused_lets): style 2016-12-12 08:32:42 -08:00
elim_unused_lets.h feat(library/compiler): eliminate unused let declarations 2016-12-12 08:23:37 -08:00
erase_irrelevant.cpp fix(library/quote): use opaque macro for elaborated expr quotations 2017-06-07 10:00:17 -07:00
erase_irrelevant.h feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information 2016-11-09 16:51:48 -08:00
eta_expansion.cpp feat(library/compiler/eta_expansion): also eta-expand expressions containing sorry 2017-05-23 11:14:31 -07:00
eta_expansion.h perf(library/compiler/eta_expansion): conservative eta_expansion 2017-01-12 11:18:16 -08:00
extract_values.cpp feat(library/compiler/eta_expansion): also eta-expand expressions containing sorry 2017-05-23 11:14:31 -07:00
extract_values.h feat(library/compiler): create declarations for nested values 2016-12-12 10:37:58 -08:00
init_module.cpp feat(*): C++ code generator 2016-12-05 16:11:41 -08:00
init_module.h
inliner.cpp fix(library/compiler/inliner): inline auxiliary declarations 2017-08-06 10:24:26 +02:00
inliner.h fix(library/noncomputable): fixes #1631 2017-05-31 23:16:37 -07:00
lambda_lifting.cpp perf(library/compiler/elim_recursors): beta_reduce ==> head_beta_reduce 2017-07-21 03:32:23 -07:00
lambda_lifting.h feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information 2016-11-09 16:51:48 -08:00
nat_value.cpp chore(library, frontends/lean): use override 2017-06-22 16:15:21 -07:00
nat_value.h chore(util/sexpr): remove mpz and mpq cases 2017-01-31 09:39:31 +01:00
preprocess.cpp feat(library/equations_compiler): meta mutual definitions 2017-10-30 15:06:12 -07:00
preprocess.h feat(library/equations_compiler): meta mutual definitions 2017-10-30 15:06:12 -07:00
procedure.h fix(library/compiler): missing file 2016-11-10 09:34:32 -08:00
rec_fn_macro.cpp chore(library, frontends/lean): use override 2017-06-22 16:15:21 -07:00
rec_fn_macro.h fix(frontends/lean/elaborator): postprocess rec_fn_macros used in meta_definitions 2016-09-18 13:01:50 -07:00
reduce_arity.cpp feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information 2016-11-09 16:51:48 -08:00
reduce_arity.h feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information 2016-11-09 16:51:48 -08:00
simp_inductive.cpp fix(library/compiler/simp_inductive): array^.data should not be treated as a regular projection 2017-03-09 19:11:51 -08:00
simp_inductive.h perf(library/compiler): add common subexpression elimination 2016-12-11 14:43:51 -08:00
simp_pr1_rec.cpp feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
simp_pr1_rec.h refactor(library): rename pr1/pr2 ==> fst/snd 2016-09-21 09:48:39 -07:00
util.cpp feat(library/compiler): avoid pack/unpack overhead produced by the inductive_compiler in the code generator 2017-03-04 13:54:44 -08:00
util.h feat(library/compiler): avoid pack/unpack overhead produced by the inductive_compiler in the code generator 2017-03-04 13:54:44 -08:00
vm_compiler.cpp feat(library/compiler/vm_compiler): clear runtime cost model 2017-11-01 14:11:09 -07:00
vm_compiler.h feat(library/equations_compiler): meta mutual definitions 2017-10-30 15:06:12 -07:00