Leonardo de Moura
b56674cc25
fix(library/compiler/specialize): remove bogus optimization
2018-11-07 18:00:28 -08:00
Leonardo de Moura
df39be927d
feat(library/compiler): make sure application arguments are free variables or neutral terms in LLNF
2018-11-07 17:25:20 -08:00
Leonardo de Moura
f9236592cc
chore(library/compiler/llnf): remove dead code
2018-11-07 16:48:32 -08:00
Leonardo de Moura
474c743d8a
fix(library/compiler/llnf): do not expand atomic values
2018-11-07 16:43:46 -08:00
Leonardo de Moura
17679799a2
fix(library/compiler/cse): must take a flag indicating whether we are applying optimization after/before erasure
2018-11-07 16:38:24 -08:00
Leonardo de Moura
1191dd4deb
refactor(library/compiler): move mk_runtime_type to util
2018-11-07 15:19:24 -08:00
Leonardo de Moura
c285d48c96
feat(library/compiler/erase_irrelevant): simplify mk_runtime_type
2018-11-07 15:10:41 -08:00
Leonardo de Moura
687e9d076d
feat(library/compiler): add _apply and _closure instructions to LLNF
2018-11-07 13:30:28 -08:00
Sebastian Ullrich
e2bf92ec21
feat(library/module_mgr,shell/lean): identify correct file on error in transitive import
2018-11-07 14:07:51 +01:00
Sebastian Ullrich
80a79336f2
chore(.gitignore): ignore library/Makefile
2018-11-07 09:30:32 +01:00
Sebastian Ullrich
0026b59a88
fix(tests/lean/macro_scopes): expected output
2018-11-07 09:11:49 +01:00
Leonardo de Moura
330e2700b1
chore(library/compiler/compiler): add trace.compiler.boxed option for debugging purposes
2018-11-06 16:55:02 -08:00
Leonardo de Moura
5acb5e63b1
feat(library/compiler): revise llnf instructions
...
Motivation: make sure we can generate "portable" C++ code. "Portable"
here means we can compile the generated code using 32 and 64 bit machines.
2018-11-06 16:55:02 -08:00
Leonardo de Moura
8af0c85d4f
feat(library/compiler/erase_irrelevant): convert enumeration types into uint* types
2018-11-06 16:55:02 -08:00
Leonardo de Moura
83ebacb8af
chore(library/compiler/util): style
2018-11-06 16:55:02 -08:00
Leonardo de Moura
9f3544aaa4
feat(library/compiler/erase_irrelevant): preserve enumeration types
2018-11-06 16:55:02 -08:00
Leonardo de Moura
6f03df871b
chore(library/compiler): remove whnf_upto_runtime_type
...
It is not needed anymore.
2018-11-06 16:55:02 -08:00
Leonardo de Moura
e63721958b
refactor(library/compiler): add is_enum_type auxiliary function
2018-11-06 16:55:02 -08:00
Leonardo de Moura
f404c5c446
refactor(library/init/data): make sure uint* and usize are irreducible
...
Remark: this commit breaks the support for `uint*` and `usize` in the old VM.
2018-11-06 16:55:02 -08:00
Leonardo de Moura
216a3632cc
refactor(library/compiler/llnf): simplify llnf primitive instructions
2018-11-06 16:55:02 -08:00
Leonardo de Moura
39850d3b84
chore(library/compiler/llnf): remove dead global
2018-11-06 16:55:02 -08:00
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
