max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
15043 commits 1 branch 0 tags 5.3 GiB
Commit graph

5138 commits

Author SHA1 Message Date
Leonardo de Moura
dbe2678795 fix(library/compiler/specialize): we should specialize even if only a few "specialization arguments" have been provided 
This fixes a performance bottleneck at `term_parser.run`.
The `longest_match` application there was not being specialized.
 2018-10-20 09:37:21 -07:00
Leonardo de Moura
4929af1dd3 feat(library/compiler/extract_closed): extract_closed is working 2018-10-19 18:32:49 -07:00
Leonardo de Moura
356928c873 feat(library/compiler): add extract_closed skeleton 2018-10-19 16:14:59 -07:00
Leonardo de Moura
eb02add3de feat(library/compiler): simplify again after lambda lifting 
Motivation: we avoid the creation of closures at join point declarations.
 2018-10-19 15:17:07 -07:00
Leonardo de Moura
ad4e04685c fix(library/compiler/specialize): we must consider lambdas at FixedInst arguments 
Otherwise, we will never specialize type class arguments such as `[decidable_rel lt]`
 2018-10-19 14:56:18 -07:00
Leonardo de Moura
d623c6ef43 chore(library/compiler/lambda_lifting): do not need type_checker::state 2018-10-19 14:41:39 -07:00
Leonardo de Moura
17b9b21555 feat(library/compiler/csimp): allow csimp to be used after erasure 2018-10-19 12:02:29 -07:00
Leonardo de Moura
c35ee19353 feat(library/compiler/specialize): eta-expand specialization 2018-10-18 14:28:22 -07:00
Leonardo de Moura
4d5252525d feat(library/compiler/specialize): cache specialization results 
Specialization is still disabled. I will continue testing it, and enable
it in a future commit.
 2018-10-18 13:09:19 -07:00
Leonardo de Moura
3fa4b1600d fix(library/compiler/specialize): register auxiliary declarations created by the specializer in the environment 2018-10-18 07:32:16 -07:00
Leonardo de Moura
69070f43eb chore(library/local_context): remove user_name indexing 
The datastructures at `local_context` used to manage used user_names
introduce a lot of overhead. They do guarantee that `get_unused_name` is
`O(log(n))`, but they slowdown much more common operations such as:
local declaration creation/deletion. We create/delete local declarations
much more often than we use `get_unused_name`.

The corelib build time is now 34.18 secs on my desktop. It was 39.5 secs.
 2018-10-17 09:24:40 -07:00
Leonardo de Moura
72a6e64d8f chore(library/compiler/specialize): leftovers 2018-10-17 08:38:30 -07:00
Leonardo de Moura
a40c526e48 feat(library/compiler/csimp): add basic constant folding for nat operations 2018-10-17 08:38:30 -07:00
Leonardo de Moura
2a4dc2cb5b fix(library/compiler/specialize): incorrect abstraction order 2018-10-16 16:15:47 -07:00
Leonardo de Moura
611f6ae780 feat(library/compiler/specialize): code specialization 
TODO:
- Cache results at `specialize_ext`
- Cleanup

It is not feasible to run code specializer without cache: code explosion.
 2018-10-16 15:50:42 -07:00
Leonardo de Moura
af682a0981 feat(library/compiler/specialize): refine candidate selection heuristics 2018-10-16 15:50:42 -07:00
Leonardo de Moura
f80ea590ba fix(library/compiler/specialize): typo 2018-10-16 15:50:42 -07:00
Leonardo de Moura
88de81077c feat(library/compiler/specialize): do not specialize instances unless they are marked with [specialize] 
@kha: I changed the specialization candidate selection procedure.
Now, instances are not considered for specializations unless we mark
them with `[specialize]`. The idea is that an instance application is
morally just creating the "dictionary" for invoking a polymorphic
function.
 2018-10-15 18:29:29 -07:00
Leonardo de Moura
4cfe44bed0 feat(library/compiler/specialize): add nospecialize attribute 
@kha I had to add this attribute because the specializer was generated
many specialization candidates for functions that take `[has_tokens ...]`
as an argument. Moreover, these candidates had a lot of
dependencies. I am trying to workaround this issue by marking the
instances with the new attribute `[nospecialize]`.
I did not mark instances created by `[derive]`. It is quite tedious to
do it.

BTW, when I was investigating the problem I stumbled at `node.view`.
Its type is:
```
node.view :
  Π {α : Type} {m : Type → Type} [_inst_1 : monad m] [_inst_2 : monad_except (parsec.message syntax) m]
  [_inst_3 : monad_parsec syntax m] [_inst_4 : alternative m] (k : syntax_node_kind) (rs : list (m syntax))
  [i : @has_view syntax_node_kind k α], @has_view (m syntax) (@node m _inst_1 _inst_2 _inst_3 _inst_4 k rs) α
```
This looks wrong: the view depends on `[monad_parsec syntax m]`

We should also make sure definitions do not have unnecessary type
class instances. Otherwise, we will put additional stress on the code
specializer. One option is to change the frontend and filter unused
instances.
 2018-10-15 17:44:26 -07:00
Leonardo de Moura
3f2c5c8b75 chore(library/compiler/csimp): fix assertion 2018-10-15 17:39:44 -07:00
Leonardo de Moura
ba55ecf063 chore(library/compiler/specialize): fix debug build 2018-10-15 17:19:28 -07:00
Leonardo de Moura
777119ceab feat(library/compiler/specialize): collect dependencies 2018-10-15 17:15:42 -07:00
Leonardo de Moura
4f73cb18bb feat(library/compiler/specialize): more detailed spec_info 2018-10-15 15:48:02 -07:00
Leonardo de Moura
9bd09de9e2 feat(library/compiler/specialize): find candidates for specialization 2018-10-15 15:29:38 -07:00
Leonardo de Moura
42c056862d feat(library/compiler/compiler): cache stage1 result before specialization 2018-10-15 13:08:48 -07:00
Leonardo de Moura
8f76df4823 feat(library/compiler): add [specialize] attribute 2018-10-15 13:02:11 -07:00
Leonardo de Moura
9ca4c362ae feat(library/compiler/specialize): add spec_info 
Store which arguments can be specialized.
 2018-10-15 12:54:34 -07:00
Leonardo de Moura
611af5c186 feat(library/compiler/csimp): improve heuristic for deciding whether we should apply float_cases_on or not. 2018-10-15 09:50:02 -07:00
Leonardo de Moura
4788c8c52c chore(library/type_context): remove dead code 2018-10-12 11:57:41 -07:00
Leonardo de Moura
15a25d5aa9 chore(library/init/lean/parser): add a few comments 2018-10-11 15:54:57 -07:00
Leonardo de Moura
c74f4c16ca feat(library/kernel,library/compiler/csimp): make sure nat.rec and nat.cases_on reduce when major premise is a nat literal 2018-10-10 18:35:15 -07:00
Leonardo de Moura
338038a05e feat(library/init/core): add inline identity function 2018-10-10 18:17:29 -07:00
Leonardo de Moura
be0b4c998f fix(library/compiler/lcnf): avoid unnecessary let-decl 2018-10-10 17:33:57 -07:00
Leonardo de Moura
bbb45bfc95 fix(library/compiler/csimp): another join-point management bug 2018-10-10 13:42:32 -07:00
Leonardo de Moura
18093f3f24 feat(library/compiler/csimp): eta-expand lambda-expressions during simplification 2018-10-09 19:16:41 -07:00
Leonardo de Moura
e958f20874 fix(library/compiler/csimp): beta_reduce was not preserving the "join-point" invariant 2018-10-09 19:11:16 -07:00
Leonardo de Moura
256112be5b chore(library/compiler/lcnf): disable lambda eta-expansion during LCNF conversion 
We should do it at `csimp`
 2018-10-09 15:25:57 -07:00
Leonardo de Moura
27e6f7f424 feat(library/compiler): invoke specialize skeleton 2018-10-09 15:23:42 -07:00
Leonardo de Moura
5d726eb210 feat(library/compiler/compiler): switch to new compiler frontend 
We also rename `vm_compiler` module to `emit_bytecode`.
We will eventually replace this module with the new IR emitter.
 2018-10-08 17:38:17 -07:00
Leonardo de Moura
662c0ebb31 feat(library/compiler/compiler): cache stage1 2018-10-08 17:06:45 -07:00
Leonardo de Moura
124b4d37fe feat(library/compiler): port simp_inductive to the new compiler stack 
This commit also fixes a bug in the old `simp_inductive` module, and
removes now obsolete files (`compiler_step_visitor` and `old_util`).
 2018-10-08 16:58:43 -07:00
Leonardo de Moura
d2fcb7af39 chore(library/compiler/compiler): add tracing to new compiler frontend 2018-10-08 15:22:36 -07:00
Leonardo de Moura
787d1ecb93 feat(library/compiler/lambda_lifting): new lambda lifting 2018-10-08 15:04:59 -07:00
Sebastian Ullrich
305984bab5 feat(frontends/lean/elaborator): show context of unassigned mvars 2018-10-08 09:32:41 -07:00
Leonardo de Moura
fc62e8f3a4 chore(library/compiler): cdecl ==> comp_decl 2018-10-05 17:30:27 -07:00
Leonardo de Moura
d75b1c57bf chore(library/compiler/preprocess): remove dependency 2018-10-05 17:30:27 -07:00
Leonardo de Moura
b1f98e8f38 feat(library/compiler/lcnf): eta expand lambdas 2018-10-05 17:30:27 -07:00
Leonardo de Moura
4fd546c132 feat(library/compiler): remove old extract_values 2018-10-05 17:30:27 -07:00
Leonardo de Moura
2eea3d4c4b chore(library/compiler): simplify procedure class 
Remark: `procedure` will be deleted soon.
 2018-10-05 17:30:27 -07:00
Leonardo de Moura
dc5dbb3b81 chore(library/compiler): remove dead code 2018-10-05 17:30:27 -07:00