Leonardo de Moura
2ff301babd
chore(library/persistent_context_cache): style
2018-02-21 15:04:20 -08:00
Leonardo de Moura
028bd8c6c6
fix(library/type_context): performance bug
2018-02-21 15:04:20 -08:00
Leonardo de Moura
d581fb10a8
chore(library/abstract_context_cache): missing override annotations
2018-02-21 15:04:20 -08:00
Leonardo de Moura
20db4edf27
feat(library): add persistent_context_cache
2018-02-21 15:04:20 -08:00
Leonardo de Moura
1aeaed0cae
feat(library/abstract_context_cache): make it fully abstract
2018-02-21 15:04:20 -08:00
Leonardo de Moura
70b6e5c958
feat(library): unique token generator
2018-02-21 15:04:20 -08:00
Leonardo de Moura
8a93d2770e
feat(library/equations_compiler): add new cache support to equation compiler
2018-02-21 15:04:20 -08:00
Leonardo de Moura
ada4932507
feat(library/compiler): add new cache support to compiler
2018-02-21 15:04:20 -08:00
Leonardo de Moura
9d9ac16e7a
feat(library): add implementation of abstract_context_cache
2018-02-21 15:04:20 -08:00
Leonardo de Moura
89bd571b53
chore(library): adjust include files
2018-02-21 15:04:20 -08:00
Leonardo de Moura
a175e9393e
refactor(library): context_cache ==> abstract_context_cache
2018-02-21 15:04:20 -08:00
Leonardo de Moura
7762dc381a
feat(library/type_context): use context_cache interface
2018-02-21 15:04:20 -08:00
Leonardo de Moura
c97134760d
feat(library): add new context_cache interface
2018-02-21 15:04:20 -08:00
Leonardo de Moura
46ed0ad677
refactor(library/congr_lemma): remove mk_rel_iff_congr_lemma and mk_rel_eq_congr_lemma
2018-02-21 15:04:20 -08:00
Leonardo de Moura
8f25f903da
chore(library/app_builder): remove unnecessary caching
2018-02-21 15:04:19 -08:00
Leonardo de Moura
f8aa9e6bd4
doc(library/type_context): alternative approach for tactic_state cache
2018-02-21 15:04:19 -08:00
Leonardo de Moura
5428767f11
refactor(library/tactic): remove two thread local caches
...
The AC manager cache will be rewritten for the AC matcher.
The congruence closure module has to be rewritten for performance
reasons. During the rewrite, we should evaluate whether we need
a new cache management policy or not.
2018-02-21 15:04:19 -08:00
Leonardo de Moura
6c2f65d541
doc(library/type_context): document new cache management for type_context/app_builder/fun_info
2018-02-21 15:04:19 -08:00
Leonardo de Moura
3535b0f870
refactor(library/equations_compiler/structural_rec): do no use mk_fresh_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
d54d759d56
refactor(library): do not use mk_fresh_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
11e87545be
chore(frontends/lean): remove dead variables
2018-02-21 15:04:19 -08:00
Leonardo de Moura
f8e0916c64
feat(library/tactic, frontends/lean): replace a few mk_tagged_fresh_name with mk_unused_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
73eda00ba3
refactor(library/compiler): mk_unused_name ==> mk_compiler_unused_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
058520d6e4
feat(frontends/lean/pp,library/local_context): use sanitize_name_generator_name
...
Remark: we should remove `sanitize_if_fresh` as soon as we delete `::lean::mk_fresh_name`
2018-02-21 15:04:19 -08:00
Leonardo de Moura
49e8867d29
feat(util/name_generator): mk_tagged_child ==> mk_child_with
...
This commit also adds assertions to make sure only registered prefixes
are used to create name generators.
2018-02-21 15:04:19 -08:00
Leonardo de Moura
b16f641179
feat(util/name_generator): name generator prefix bookkeeping
2018-02-21 15:04:19 -08:00
Leonardo de Moura
ce028d651d
refactor(kernel): abstract_type_context::mk_fresh_name ==> abstract_type_context::next_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
28d6326228
refactor(frontends/lean/parser): add name_generator
2018-02-21 15:04:19 -08:00
Leonardo de Moura
fa2e67e8f3
refactor(library/compiler/vm_compiler): do not use mk_fresh_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
6ba4607c28
refactor(library/compiler): rename compiler mk_fresh_name to mk_unused_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
c0ded37f24
refactor(library/inductive_compiler): do not use fresh names in the inductive compiler
2018-02-21 15:04:19 -08:00
Leonardo de Moura
e06c3cbd8f
chore(library/type_context): fix compilation warning
2018-02-21 15:04:19 -08:00
Leonardo de Moura
21e52408b2
refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
c176faed32
feat(kernel/inductive): make sure constructor types do not contain local constants nor metavariables
2018-02-21 15:04:19 -08:00
Leonardo de Moura
cc8eb83507
refactor(library/util,util): move is_internal_name to util/
2018-02-21 15:04:19 -08:00
Leonardo de Moura
2e5b66a5f1
refactor(kernel): make sure kernel does not use global ::lean::mk_fresh_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
60d04987c8
chore(kernel/inductive/inductive): remove dead global variable
2018-02-21 15:04:19 -08:00
Leonardo de Moura
1547d47387
feat(util/fresh_name): add fresh_name_scope
2018-02-21 15:04:19 -08:00
Leonardo de Moura
8eb34a39cb
feat(frontends/lean): save/restore fresh name_generator state in parser snapshots
2018-02-21 15:04:19 -08:00
Leonardo de Moura
799cc9b03d
feat(util/fresh_name): implement mk_fresh_name using name_generator
2018-02-21 15:04:19 -08:00
Leonardo de Moura
05fc306550
feat(util): add name_generator back
2018-02-21 15:04:19 -08:00
Leonardo de Moura
78d8ff8031
feat(*): add reset_thread_local
2018-02-21 15:04:19 -08:00
Leonardo de Moura
505042b8c0
chore(library/tactic/smt/congruence_closure): simplify cache management
2018-02-21 15:04:18 -08:00
Leonardo de Moura
40a0465cca
chore(library/tactic/simp_lemmas): fix typo
2018-02-21 15:04:18 -08:00
Leonardo de Moura
02231477f9
chore(library/tactic/ac_tactics): simplify cache management
2018-02-21 15:04:18 -08:00
Leonardo de Moura
bf4d47b560
chore(library/cache_helper): remove dead code
2018-02-21 15:04:18 -08:00
Leonardo de Moura
9e08cab381
chore(library/type_context): simplify cache management
2018-02-21 15:04:18 -08:00
Leonardo de Moura
da032ccc3b
feat(library/init/data/nat/lemmas): add lemma for termination proofs
2018-02-21 10:37:07 -08:00
Leonardo de Moura
afb65f3d3d
feat(library/init/meta/comp_value_tactics): add comp_val interactive tactic
2018-02-21 10:35:26 -08:00
Leonardo de Moura
61930c3d85
fix(library/init/meta/comp_value_tactics): instantiate metavars
2018-02-21 10:28:27 -08:00
