Commit graph

17 commits

Author SHA1 Message Date
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
72a6e64d8f chore(library/compiler/specialize): leftovers 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
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
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
27e6f7f424 feat(library/compiler): invoke specialize skeleton 2018-10-09 15:23:42 -07:00
Leonardo de Moura
e18af852c8 feat(library/compiler): add code specialization skeleton 2018-10-05 17:30:27 -07:00