max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/library
History
Leonardo de Moura fabf7f6380 perf(library/equations_compiler, library/compiler): expand auxiliary _match_idx definitions when generating byte code 
We use the auxiliary procedure pull_nested_rec_fn to pull recursive
application in nested match expressions. This is needed because the
nested match expression is compiled before we process the recursive
procedure that contains it. This transformation may produce
performance problems if the recursive application does not depend on
the data being matched. Here is an example from the new test:

```
def tst : tree → nat
| (tree.leaf v) := v
| (tree.node v l r) :=
  match f v with
  | tt := tst l
  | ff := tst r
  end
```

pull_nested_rec_fn will convert it into

```
def tst : tree → nat
| (tree.leaf v)     := v
| (tree.node v l r) := tst._match_1 (f v) (tst l) (tst r)
```

Since our interpreter uses eager evaluation, both `(tst l)` and `(tst r)`
are executed. This commit fixes this issue by expanding `tst._match_1`
during code generation.
2017-11-09 11:14:57 -08:00
..
compiler perf(library/equations_compiler, library/compiler): expand auxiliary _match_idx definitions when generating byte code 2017-11-09 11:14:57 -08:00
constructions fix(kernel/expr,library/constructions/projection): preserve instance-implicitness in structure parameters 2017-08-27 16:47:04 +02:00
equations_compiler perf(library/equations_compiler, library/compiler): expand auxiliary _match_idx definitions when generating byte code 2017-11-09 11:14:57 -08:00
inductive_compiler feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
native_compiler feat(library/vm/process): add basic process support 2017-03-28 18:08:06 -07:00
tactic chore(init/meta/attribute): rename user_attribute.set_param to user_attribute.set 2017-09-14 18:48:18 +02:00
vm feat(library/init/meta): move rb_tree and rb_map to native namespace 2017-11-07 13:41:45 -08:00
abstract_parser.h chore(library/abstract_parser,frontends/lean/parser): remove dead code 2017-03-28 11:51:50 -07:00
aliases.cpp feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs 2017-02-08 17:41:44 -08:00
aliases.h feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs 2017-02-08 17:41:44 -08:00
annotation.cpp chore(library, frontends/lean): use override 2017-06-22 16:15:21 -07:00
annotation.h
app_builder.cpp fix(library/equations_compiler): performance problem reported by @dselsam 2017-06-27 15:24:12 -07:00
app_builder.h fix(library/equations_compiler): performance problem reported by @dselsam 2017-06-27 15:24:12 -07:00
arith_instance.cpp refactor(library/init/algebra): remove order_pair classes 2017-08-02 14:41:35 +01:00
arith_instance.h refactor(library/init/algebra): remove order_pair classes 2017-08-02 14:41:35 +01:00
attribute_manager.cpp feat(init/meta/attribute,library/tactic/attribute): user_attribute apply handlers 2017-08-02 14:32:39 +01:00
attribute_manager.h feat(library/tactic/user_attribute,init/meta/attribute): implement parameterized user attributes 2017-09-05 23:14:34 +02:00
aux_definition.cpp feat(library/equations_compiler): meta mutual definitions 2017-10-30 15:06:12 -07:00
aux_definition.h feat(library/equations_compiler): meta mutual definitions 2017-10-30 15:06:12 -07:00
aux_recursors.cpp feat(library/module): intermediary data structure for environment modifications 2016-12-20 10:15:19 -08:00
aux_recursors.h
bin_app.cpp
bin_app.h
cache_helper.h feat(library): instances are not reducible by default anymore 2017-04-26 14:10:11 -07:00
check.cpp fix(library/check): improve ensure_type 2017-06-25 14:51:09 -07:00
check.h fix(library/tactic/rewrite_tactic): fixes #1277 2017-01-23 16:34:07 -08:00
choice.cpp feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
choice.h
class.cpp feat(library/tactic): start algebraic normalizer 2017-05-15 21:46:19 -07:00
class.h feat(library/class): add attribute for tracking symbols occurring in instances of type classes 2017-05-01 18:02:30 -07:00
CMakeLists.txt refactor(frontends/lean/definition_cmds): make profiling threshold configurable 2017-04-23 11:22:41 -07:00
comp_val.cpp feat(library/init/data/char): char as an unicode scalar value 2017-10-23 10:55:26 -07:00
comp_val.h feat(library/tactic/congruence/congruence_closure): interpreted values in the same equivalence class 2016-12-25 11:09:55 -08:00
congr_lemma.cpp fix(library/congr_lemma): always return heq in mk_hcongr_lemma 2017-08-29 16:36:37 +02:00
congr_lemma.h feat(library/congr_lemma, library/fun_info): make sure opt_param gadget do not confuse the simplifier, fun_info, congr_lemma, etc 2017-01-30 20:23:45 -08:00
constants.cpp feat(library/init/data/char): char as an unicode scalar value 2017-10-23 10:55:26 -07:00
constants.h feat(library/init/data/char): char as an unicode scalar value 2017-10-23 10:55:26 -07:00
constants.txt feat(library/init/data/char): char as an unicode scalar value 2017-10-23 10:55:26 -07:00
deep_copy.cpp feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
deep_copy.h
defeq_canonizer.cpp feat(library): instances are not reducible by default anymore 2017-04-26 14:10:11 -07:00
defeq_canonizer.h refactor(library/tactic): move defeq_canonizer::state to tactic_state 2017-01-07 10:17:51 -08:00
delayed_abstraction.cpp fix(library/delayed_abstraction): fixes #1728 2017-07-05 17:10:18 -07:00
delayed_abstraction.h fix(library/delayed_abstraction): fixes #1728 2017-07-05 17:10:18 -07:00
discr_tree.cpp chore(library): define rb_expr_tree and rb_expr_map 2016-12-27 20:29:31 -08:00
discr_tree.h
documentation.cpp fix(*): more gcc 7 warnings 2017-05-31 17:29:30 -07:00
documentation.h
eval_helper.cpp fix(*): gcc 7 linking errors 2017-05-31 16:35:09 -07:00
eval_helper.h feat(library/system/io,shell/lean): add --run switch 2017-04-11 16:41:30 -07:00
exception.cpp refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
exception.h feat(frontends/lean/definition_cmds): when the kernel fails to type check a declaration include the fully elaborated term in the error message 2017-09-13 16:43:54 -07:00
explicit.cpp
explicit.h
export.cpp feat(library/export): add option to only export a single declaration 2017-07-14 09:49:24 +01:00
export.h feat(library/export): add option to only export a single declaration 2017-07-14 09:49:24 +01:00
export_decl.cpp feat(library/module): intermediary data structure for environment modifications 2016-12-20 10:15:19 -08:00
export_decl.h
expr_lt.cpp fix(library/expr_lt): make sure find_local_decl is not tested in the Meta case, and add /* fall-thru */ 2017-06-20 13:47:30 -07:00
expr_lt.h fix(library/tactic/simplify): fixes #1685 2017-06-20 12:27:46 -07:00
expr_pair.h
expr_pair_maps.h
expr_unsigned_map.h
fingerprint.cpp
fingerprint.h
fun_info.cpp feat(library/congr_lemma, library/fun_info): make sure opt_param gadget do not confuse the simplifier, fun_info, congr_lemma, etc 2017-01-30 20:23:45 -08:00
fun_info.h feat(library/congr_lemma, library/fun_info): make sure opt_param gadget do not confuse the simplifier, fun_info, congr_lemma, etc 2017-01-30 20:23:45 -08:00
handle.cpp fix(library/handle): handle double close 2017-04-11 16:42:17 -07:00
handle.h feat(library/vm/process): add basic process support 2017-03-28 18:08:06 -07:00
head_map.cpp
head_map.h
idx_metavar.cpp feat(library/idx_metavar): add helper function for converting metavariables occurring in an expression into temporary metavariables 2017-06-28 18:06:33 -07:00
idx_metavar.h feat(library/idx_metavar): add helper function for converting metavariables occurring in an expression into temporary metavariables 2017-06-28 18:06:33 -07:00
init_module.cpp refactor(init/meta/expr): unify expr and pexpr 2017-05-17 10:38:12 -07:00
init_module.h
inverse.cpp feat(library/module): intermediary data structure for environment modifications 2016-12-20 10:15:19 -08:00
inverse.h
io_state.cpp feat(*): C++ code generator 2016-12-05 16:11:41 -08:00
io_state.h refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
io_state_stream.cpp refactor(frontends/lean/definition_cmds): make profiling threshold configurable 2017-04-23 11:22:41 -07:00
io_state_stream.h refactor(frontends/lean/definition_cmds): make profiling threshold configurable 2017-04-23 11:22:41 -07:00
kernel_serializer.cpp fix(library/kernel_serializer): fix build error 2017-07-16 16:29:30 +01:00
kernel_serializer.h
library_task_builder.cpp fix(library/library_task_builder): prevent uninitialized task results when cancelled 2017-06-30 08:32:34 +02:00
library_task_builder.h feat(util/log_tree): annotate nodes with detail levels 2017-03-23 09:03:43 +01:00
local_context.cpp perf(library/local_context): fix performance bottleneck at local_const 2017-06-06 10:01:08 -07:00
local_context.h perf(library/local_context): fix performance bottleneck at local_const 2017-06-06 10:01:08 -07:00
locals.cpp feat(library/init/meta/expr): add expr.has_local_in 2017-07-01 20:23:37 -07:00
locals.h feat(library/init/meta/expr): add expr.has_local_in 2017-07-01 20:23:37 -07:00
max_sharing.cpp feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs 2017-02-08 17:41:44 -08:00
max_sharing.h
message_builder.cpp feat(library/messages, frontends/lean): optional end position for messages 2017-06-15 10:47:58 -07:00
message_builder.h feat(library/messages, frontends/lean): optional end position for messages 2017-06-15 10:47:58 -07:00
messages.cpp feat(library/messages, frontends/lean): optional end position for messages 2017-06-15 10:47:58 -07:00
messages.h feat(library/messages, frontends/lean): optional end position for messages 2017-06-15 10:47:58 -07:00
metavar_context.cpp feat(library/metavar_context): add method for setting metavar user facing name 2017-08-17 16:03:32 -07:00
metavar_context.h feat(library/metavar_context): add method for setting metavar user facing name 2017-08-17 16:03:32 -07:00
metavar_util.h chore(library/delayed_abstraction): clarify delayed_abstraction API 2017-07-05 16:40:45 -07:00
module.cpp fix(library/module): unfold macros in inductive types 2017-06-30 17:49:50 +02:00
module.h refactor(util/serializer,library/module): use basic_ostream::write for the olean code 2017-06-23 15:13:40 +02:00
module_mgr.cpp fix(library/module_mgr): error handling in cyclic imports 2017-09-12 17:22:47 +02:00
module_mgr.h feat(library/module_mgr): skip reverse dependency rebuild if file content is unchanged 2017-05-23 11:14:30 -07:00
mpq_macro.cpp refactor(library/arith_instance): add mk_num 2017-02-12 19:44:02 -08:00
mpq_macro.h
mt_task_queue.cpp fix(library/mt_task_queue): work around non-recursive lock 2017-06-06 19:57:04 +02:00
mt_task_queue.h feat(util/log_tree): annotate nodes with detail levels 2017-03-23 09:03:43 +01:00
noncomputable.cpp fix(library/noncomputable): fixes #1631 2017-05-31 23:16:37 -07:00
noncomputable.h
norm_num.cpp refactor(library/init/algebra): remove order_pair classes 2017-08-02 14:41:35 +01:00
norm_num.h refactor(library/init/algebra): remove order_pair classes 2017-08-02 14:41:35 +01:00
normalize.cpp
normalize.h
num.cpp fix(library/num): fixes #1862 2017-11-09 09:49:53 -08:00
num.h chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
parray.cpp feat(library/parray): add trace option for tracking destructive updates 2017-03-07 10:57:40 -08:00
parray.h fix(library/parray): missing lock 2017-05-09 13:57:28 -07:00
pattern_attribute.cpp
pattern_attribute.h
phash_map.h feat(library/phash_map): add name_hash_map 2017-05-09 13:57:28 -07:00
phashtable.h fix(*): more gcc 7 warnings 2017-05-31 17:29:30 -07:00
pipe.cpp feat(library/vm/process): add basic process support 2017-03-28 18:08:06 -07:00
pipe.h feat(library/vm/process): add basic process support 2017-03-28 18:08:06 -07:00
placeholder.cpp feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
placeholder.h
pp_options.cpp feat(frontends/lean): add option for pretty printing metavars, sorry and delayed abstractions as holes 2017-06-15 10:24:26 -07:00
pp_options.h feat(frontends/lean): add option for pretty printing metavars, sorry and delayed abstractions as holes 2017-06-15 10:24:26 -07:00
print.cpp feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
print.h
private.cpp fix(library/equations_compiler,frontends/lean): private name support and alias generation for auxialiary declarations 2017-09-11 16:46:56 -07:00
private.h fix(library/equations_compiler,frontends/lean): private name support and alias generation for auxialiary declarations 2017-09-11 16:46:56 -07:00
process.cpp feat(library/process,system/io): set environment variables for spawned processes 2017-05-04 16:41:11 -07:00
process.h feat(library/process,system/io): set environment variables for spawned processes 2017-05-04 16:41:11 -07:00
profiling.cpp refactor(frontends/lean/definition_cmds): make profiling threshold configurable 2017-04-23 11:22:41 -07:00
profiling.h refactor(frontends/lean/definition_cmds): make profiling threshold configurable 2017-04-23 11:22:41 -07:00
projection.cpp feat(library/module): intermediary data structure for environment modifications 2016-12-20 10:15:19 -08:00
projection.h
protected.cpp feat(library/module): intermediary data structure for environment modifications 2016-12-20 10:15:19 -08:00
protected.h
quote.cpp chore(library, frontends/lean): use override 2017-06-22 16:15:21 -07:00
quote.h fix(library/quote): use opaque macro for elaborated expr quotations 2017-06-07 10:00:17 -07:00
reducible.cpp
reducible.h
register_module.h
relation_manager.cpp feat(library/module): intermediary data structure for environment modifications 2016-12-20 10:15:19 -08:00
relation_manager.h
replace_visitor.cpp chore(library): make sure replace_visitor behavior is not compiler dependent, and remove code duplication 2017-06-12 20:18:11 -07:00
replace_visitor.h
replace_visitor_with_tc.cpp
replace_visitor_with_tc.h
scoped_ext.cpp feat(frontends/lean/{builtin_cmds,interactive}): complete namespace/section after end 2017-04-23 11:26:31 -07:00
scoped_ext.h fix(frontends/lean/{parser_config,user_notation): persisting user notations 2017-06-07 10:09:38 -07:00
shared_environment.cpp
shared_environment.h
sorry.cpp feat(frontends/lean/elaborator,library/sorry): suppress error message that mention synthetic sorrys 2017-05-23 11:14:30 -07:00
sorry.h feat(frontends/lean/elaborator,library/sorry): suppress error message that mention synthetic sorrys 2017-05-23 11:14:30 -07:00
st_task_queue.cpp refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
st_task_queue.h refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
string.cpp fix(library/string): unicode char literals 2017-10-27 09:48:09 -07:00
string.h fix(library/string): unicode char literals 2017-10-27 09:48:09 -07:00
trace.cpp feat(frontends/lean,shell/server): "hole" command 2017-06-14 21:56:17 -07:00
trace.h feat(frontends/lean,shell/server): "hole" command 2017-06-14 21:56:17 -07:00
type_context.cpp fix(library/type_context): zeta-expand reflected quotations before trying to substitute local refs 2017-11-07 11:27:39 +01:00
type_context.h feat(frontends/lean): recursive equation preprocessor 2017-08-18 15:06:11 -07:00
typed_expr.cpp refactor(frontends/lean/elaborator,kernel/error_msgs): remove duplicate code 2017-07-21 01:46:31 -07:00
typed_expr.h
unfold_macros.cpp fix(library/unfold_macros): recursively unfold macros 2017-03-27 13:42:08 -07:00
unfold_macros.h
unification_hint.cpp feat(library/unification_hint): improve unification_hint matcher 2017-03-21 10:19:34 -07:00
unification_hint.h refactor(library): avoid auxiliary definitions such as add/mul/le/etc 2017-05-01 08:52:19 -07:00
update_declaration.cpp
update_declaration.h
user_recursors.cpp chore(library/user_recursors): add drec_on and dcases_on 2017-03-01 15:56:06 -08:00
user_recursors.h
util.cpp feat(library/equations_compiler/compiler): generate meta auxiliary definitions for regular (recursive) definitions 2017-11-01 11:58:45 -07:00
util.h feat(library/equations_compiler/compiler): generate meta auxiliary definitions for regular (recursive) definitions 2017-11-01 11:58:45 -07:00