Sebastian Ullrich
7fdfdb1784
chore(library/init/lean/parser): remove unnecessary class constraints
2018-11-06 21:45:08 +01:00
Sebastian Ullrich
a551c0d8c9
fix(library/module_mgr): compiling a file with a failed transitive dependency may have succeeded without output
2018-11-06 21:31:02 +01:00
Sebastian Ullrich
5a286f5e46
test(tests/lean/macro_scopes): macro scopes propagation test
2018-11-06 17:33:16 +01:00
Sebastian Ullrich
090c4c0ce7
feat(library/init/lean/syntax): add lazily propagated macro scopes to syntax_node
2018-11-06 16:46:50 +01:00
Leonardo de Moura
c108fc95cb
feat(library/compiler/ir): basics
2018-11-05 17:04:23 -08:00
Leonardo de Moura
8de7637f75
feat(library/compiler): add to_ir skeleton
2018-11-05 17:04:23 -08:00
Sebastian Ullrich
fc4dcd19cf
refactor(library/init/lean/parser): use ident.view in syntax.to_format
2018-11-05 17:57:00 +01:00
Sebastian Ullrich
dcb7566e53
fix(tests/lean/parser1): fix test
2018-11-05 17:40:11 +01:00
Sebastian Ullrich
7d6048c795
fix(library/message_builder): fix output of nested kernel exceptions
2018-11-05 17:37:21 +01:00
Sebastian Ullrich
507509b336
chore(library/Makefile.in): suppress comment output
...
I hate make
2018-11-05 17:15:01 +01:00
Sebastian Ullrich
c9bebb7411
feat(library/time_task): do not report inclusive times
2018-11-05 17:06:32 +01:00
Sebastian Ullrich
8c27f0aac6
refactor(frontends/lean/elaborator,library/init/lean): finish no_kind refactoring
2018-11-04 20:24:40 +01:00
Sebastian Ullrich
58df9cb813
chore(library/Makefile.in): prevent infinite make cycles
2018-11-04 20:24:40 +01:00
Sebastian Ullrich
09aa4f9ab3
chore(frontends/lean/elaborator): don't try to recover from errors in patterns
2018-11-04 19:03:00 +01:00
Leonardo de Moura
733bbc521f
feat(library/init/core): mark thunk and task primitives with [noinline]
...
In the future, we should use the `[builtin]` attribute which cannot be
overwritten by the user.
2018-11-02 13:54:40 -07:00
Leonardo de Moura
b23251fd6e
feat(library/compiler/lambda_lifting): preserve join points when performing lambda lifting
2018-11-01 16:04:25 -07:00
Leonardo de Moura
adff01bba4
fix(library/vm/vm): handle InvokeJP at pc manipulation methods
2018-11-01 16:01:36 -07:00
Leonardo de Moura
e11fe27de2
chore(library/compiler/lambda_lifting): temporary hack
...
Make sure that a join point that has been lambda lifted is not tagged as
a join point anymore.
2018-11-01 15:21:14 -07:00
Leonardo de Moura
f27ab2bb38
chore(library/compiler/emit_bytecode): remove dead code
2018-11-01 14:21:20 -07:00
Leonardo de Moura
e5432f5fb2
fix(library/type_context): memory access violation in the new type class inference optimization
2018-11-01 14:16:57 -07:00
Leonardo de Moura
f22bdec775
feat(library/vm): add support for join-points in the old VM
...
Motivation: to make progress in the new compiler stack, we have
to preserve join points during lambda lifting. Right now, they are
lifted as regular lambdas. So, to keep them, we need some basic
support for them in the old VM. The implementation here is quick and
dirty. This is not an issue since this code will be deleted soon.
2018-11-01 14:07:59 -07:00
Leonardo de Moura
ae30b16f0d
fix(library/compiler/lcnf): nat.zero ==> literal
2018-11-01 11:59:17 -07:00
Leonardo de Moura
5d89347241
feat(library/compiler/llnf): improve memory cell reuse heuristic
2018-10-31 14:44:33 -07:00
Leonardo de Moura
34f01ff32e
chore(library/init/data/nat/basic): missing [specialize]
2018-10-31 14:44:23 -07:00
Leonardo de Moura
e21608d456
chore(library/compiler/csimp): style
2018-10-31 13:25:54 -07:00
Leonardo de Moura
189b037358
chore(tests/lean/run/new_compiler): fix test
2018-10-31 13:25:01 -07:00
Leonardo de Moura
e68372cfd9
fix(library/compiler/csimp): another join point related bug
2018-10-31 13:22:20 -07:00
Leonardo de Moura
39c2ee2931
chore(library/compiler/llnf): typo
2018-10-31 13:22:14 -07:00
Leonardo de Moura
12a01d101c
refactor(library/compiler/llnf): memory cell reuse instruction set
2018-10-31 09:35:22 -07:00
Leonardo de Moura
67a78d1c76
chore(library/compiler/llnf): cleanup
2018-10-31 08:36:09 -07:00
Leonardo de Moura
d98a1d1da3
feat(library/compiler/llnf): refine reset operation placement
...
This is not a perfect solution yet. I have identified two problems:
1) The heuristic used at `mark_to_reset_fields` is too weak.
Suppose we have
```
let ...
_x := prod.mk field_1 0
in some _x
```
The current implementation will mark `field_1` to be reset since it
occurs in a non tail call `prod.mk field_1 0`. However, we can
assume `prod.mk field_1 0` is part of the return value.
2) The current semantics of the reset instruction may produce
unnecessary memory allocation. Consider the following example
```
let _x_1 := x.1,
_x_2 := x.2,
_x_3 := _reset.2 x
in @bool.cases_on y
(_cnstr.0.0)
(let _x_4 := f _x_2,
in _updt.2 _x_3 _x_4)
```
The memory cell `_x_3` is only used in the second branch of
the `bool.cases_on`. So, if `y` is `ff`, and `x` is a shared
object, we will allocate memory at `_reset.2 x` for nothing.
2018-10-30 17:34:36 -07:00
Leonardo de Moura
abc107d963
chore(library/vm/vm): remove dead code
2018-10-30 14:27:47 -07:00
Leonardo de Moura
d3c37fee7a
perf(library/vm/vm): inline Updt/UpdtCidx/Reset
2018-10-30 14:01:32 -07:00
Leonardo de Moura
b6bc0bb284
feat(library/compiler/llnf): add reset.idx obj primitive
...
The idea is to make it clear the intent, and simplify the IR conversion.
2018-10-30 13:48:09 -07:00
Leonardo de Moura
5c3639a5c0
feat(library/compiler/llnf): avoid unnecessary resets
2018-10-30 13:32:50 -07:00
Leonardo de Moura
8527fdc338
refactor(library/compiler/llnf): memory reuse optimization
2018-10-30 10:28:56 -07:00
Sebastian Ullrich
93fc1fd1de
fix(library/init/lean/parser/combinators): node: do not wrap error in first argument
2018-10-30 17:43:05 +01:00
Sebastian Ullrich
74bd182bc8
perf(library/init/lean/parser/combinators): make node semireducible
2018-10-30 17:43:05 +01:00
Sebastian Ullrich
0d7ea62f9a
perf(frontends/lean/elaborator,library/init/lean): put out_params first to benefit from instance pre-filtering
2018-10-30 17:43:05 +01:00
Sebastian Ullrich
2e0d6649be
perf(library/init/lean/parser/basic): make basic_parser_m semireducible
2018-10-30 17:43:05 +01:00
Sebastian Ullrich
ab2e66e4a3
perf(library/type_context): simple instance pre-filtering
2018-10-30 17:43:05 +01:00
Sebastian Ullrich
0a92fea14c
feat(library/type_context): profile typeclass inference
2018-10-30 17:43:05 +01:00
Sebastian Ullrich
188ab30a9c
fix(library/init/lean/parser/declaration): precedence for attribute arguments
2018-10-30 17:43:05 +01:00
Sebastian Ullrich
8a3e7821d7
fix(frontends/lean/elaborator): weaken assertion
...
There are still some cases like errors in nested equations that leak
metavariables, but as long as we report at least one error, that probably isn't
a high-priority issue.
2018-10-30 17:43:05 +01:00
Leonardo de Moura
bcc4956ca5
feat(library/compiler/llnf): reuse constructor memory cells
...
This commit also add two new instructions to the old VM: `updt` and
`updt_cidx`.
They allow us to test the new new memory reuse technique.
TODO: We need to reset fields after we project. Otherwise, we prevent
destructive updates on nested objects.
2018-10-29 18:46:26 -07:00
Leonardo de Moura
998293b8ca
feat(library/compiler/llnf): eliminate cases term where all reachable branches are equal
2018-10-29 14:57:37 -07:00
Leonardo de Moura
91b59a2f12
fix(library/compiler/extract_closed): do not extract is_enf_unreachable
2018-10-29 14:41:12 -07:00
Leonardo de Moura
c076ac8e1a
feat(library/compiler/llnf): remove identity cases terms
...
Example: a term such as
```
decidable.cases_on t _cnstr.0.0 _cnstr.1.0
```
is replaced with `t`
2018-10-29 14:29:03 -07:00
Leonardo de Moura
c3d700ece1
feat(library/compiler/csimp): nat.succ x ==> x + 1
2018-10-29 13:53:59 -07:00
Leonardo de Moura
ecf30e93a3
chore(library/vm): remove Destruct instruction
2018-10-29 13:18:33 -07:00
