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

10369 commits

Author SHA1 Message Date
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
10b99a678c chore(util/list_ref): add objects a list of objects 2018-10-15 11:57:12 -07:00
Leonardo de Moura
8837217a2e chore(kernel/expr): dead decls 2018-10-15 11:10:11 -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
Leonardo de Moura
e75d8eacb6 fix(frontends/lean/elaborator): compilation erros with g++ 4.9 2018-10-08 11:54:28 -07:00
Sebastian Ullrich
305984bab5 feat(frontends/lean/elaborator): show context of unassigned mvars 2018-10-08 09:32:41 -07:00
Sebastian Ullrich
50e6b42f8c fix(frontends/lean/elaborator): ensure_no_unassigned_metavars: only check mvars in parameter 
Had forgotten to re-check the standard lib...
 2018-10-07 21:11:02 -07:00
Sebastian Ullrich
aea86eb828 feat(frontends/lean/elaborator): simple, accurate mvar error position tracking 
The accuracy of `m_last_pos` still needs to be improved at some point
 2018-10-05 21:25:39 -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
Leonardo de Moura
d93b2a2656 chore(library/compiler): remove dead code 2018-10-05 17:30:27 -07:00
Leonardo de Moura
335b37d480 chore(library/compiler): remove old reduce_arity 2018-10-05 17:30:27 -07:00
Leonardo de Moura
6b8008a222 feat(library/compiler): new compiler entry point (skeleton) 2018-10-05 17:30:27 -07:00
Leonardo de Moura
d29e95af08 fix(util/list_ref): typo 2018-10-05 17:30:27 -07:00
Leonardo de Moura
be6324e183 chore(util/list_ref): missing include 2018-10-05 17:30:27 -07:00
Leonardo de Moura
1d1efdd5f3 chore(library/compiler/preprocess): remove dead global 2018-10-05 17:30:27 -07:00
Leonardo de Moura
a21dac4384 chore(library/compiler/vm_compiler): remove option 2018-10-05 17:30:27 -07:00
Leonardo de Moura
135a8d7508 chore(library/compiler): remove old compiler steps that have already been replaced 2018-10-05 17:30:27 -07:00