Leonardo de Moura
baec9a1b78
chore(library/init/lean/compiler/ir): minor
2019-03-08 09:14:54 -08:00
Sebastian Ullrich
6a96d94259
chore(boot): update
2019-03-08 17:26:02 +01:00
Sebastian Ullrich
d0929c93cd
perf(library/init/lean/frontend): make file_map construction explicit, do it only once
2019-03-08 17:17:27 +01:00
Sebastian Ullrich
ef7053dac9
chore(boot): update
2019-03-08 17:05:42 +01:00
Sebastian Ullrich
4333ab620c
refactor(library/init/lean/frontend): use direct unbounded recursion instead of iterate_eio
2019-03-08 17:04:46 +01:00
Sebastian Ullrich
0580ce7cfa
chore(boot): update
2019-03-08 15:34:37 +01:00
Sebastian Ullrich
e0bbc094ad
chore(library/init): remove coroutines from stdlib
2019-03-08 15:34:17 +01:00
Sebastian Ullrich
234e4d1e8a
refactor(library/init/lean/elaborator): replace coroutines with explicit state
2019-03-08 15:23:01 +01:00
Leonardo de Moura
9962441b7b
chore(boot): update
2019-03-07 15:44:43 -08:00
Leonardo de Moura
db6f08e66d
feat(library/init/lean/compiler/ir): collect fnbody free variables
2019-03-07 15:37:45 -08:00
Leonardo de Moura
27028309a3
feat(library/init/lean/kvmap): add == for kvmap
2019-03-07 14:12:10 -08:00
Leonardo de Moura
a836bcc204
feat(library/init/lean/compiler/ir): alpha equivalence
2019-03-07 13:50:35 -08:00
Leonardo de Moura
29770d73b3
chore(boot): update
2019-03-07 12:49:53 -08:00
Leonardo de Moura
67f4698593
feat(library/compiler): do not generate code for decls that have irrelevant types
...
We were generating hundreds of definitions that just return
`lean::box(0)`.
2019-03-07 12:48:16 -08:00
Leonardo de Moura
057d90b7ff
chore(runtime/object): track number of external objects allocated
2019-03-07 12:31:05 -08:00
Leonardo de Moura
06be451110
chore(boot): update
2019-03-07 11:30:51 -08:00
Leonardo de Moura
9fc813e601
fix(library/compiler/llnf): polymorphic projection resulting type
2019-03-07 11:24:08 -08:00
Sebastian Ullrich
81615fc856
refactor(library/init/lean/parser/module): replace coroutines with explicit snapshot state
2019-03-07 10:32:28 -08:00
Leonardo de Moura
4744d12e38
chore(boot): update
2019-03-07 10:26:05 -08:00
Leonardo de Moura
0d4da4bc76
fix(library/init/lean/elaborator): borrow annotations
...
@kha I see you found this problem too :)
2019-03-07 10:26:40 -08:00
Leonardo de Moura
b5b2adea49
refactor(runtime): proper external objects without vtable
...
A C++ vtable at `external_object` is bad because it prevents users
from implementing external object in different programming languages.
Another problem was memory leaks because of the vtable in the
beginning of the object.
cc @kha
2019-03-07 10:26:05 -08:00
Leonardo de Moura
4e04d373e4
feat(library/init): unicode notation for heq: ≅
2019-03-07 10:21:14 -08:00
Leonardo de Moura
819d17ebbd
chore(library/init/lean/compiler/ir): use has_beq
2019-03-07 10:21:14 -08:00
Leonardo de Moura
79521e7e49
feat(library/init/core): add has_beq type class
2019-03-07 10:21:14 -08:00
Leonardo de Moura
67b01cddd0
chore(library/init): heq notation == ==> ~=
2019-03-07 10:21:14 -08:00
Leonardo de Moura
626d155c81
feat(library/init/lean/compiler/ir): alpha eqv for lean.ir.expr
2019-03-07 10:21:14 -08:00
Leonardo de Moura
2984d6838c
chore(library/compiler/ll_infer_type): dead variable
2019-03-07 10:21:14 -08:00
Sebastian Ullrich
1e248013f7
chore(runtime/alloc): don't init heap if LEAN_SMALL_ALLOCATOR is off
...
makes tracking down leaks a bit nicer
2019-03-07 15:52:06 +01:00
Sebastian Ullrich
35be90b3a1
chore(boot): update
2019-03-07 15:51:55 +01:00
Sebastian Ullrich
0e01871182
fix(library/init/lean/elaborator): re-add borrow annotations
2019-03-07 15:51:40 +01:00
Sebastian Ullrich
430fb81f69
fix(library/init/lean/parser/term,frontends/lean/builtin_exprs): @& should have higher rbp than ->
2019-03-07 14:35:25 +01:00
Sebastian Ullrich
a37dd02a41
perf(library/init/lean/frontend): do not hold on to outputs (syntax trees etc.) by default
2019-03-07 12:56:48 +01:00
Sebastian Ullrich
473e998ef6
chore(boot): update
2019-03-07 11:29:19 +01:00
Sebastian Ullrich
6f83faaee0
perf(library/init/lean/parser/command): index command parsers by first token
2019-03-07 11:28:42 +01:00
Leonardo de Moura
ae95a3b6ef
chore(boot): update
2019-03-06 17:27:40 -08:00
Leonardo de Moura
8e9b0d2799
fix(library/compiler): inferred types for stage2 declarations
2019-03-06 17:24:43 -08:00
Leonardo de Moura
89f692f548
chore(boot): update
2019-03-06 17:06:54 -08:00
Leonardo de Moura
35459664ad
fix(library/compiler/emit_cpp): handle new unreachable terminal
2019-03-06 17:03:56 -08:00
Leonardo de Moura
515556a718
feat(library/init/lean/compiler/ir): add new terminal: unreachable
2019-03-06 17:00:50 -08:00
Leonardo de Moura
3e0c90d17d
fix(frontends/lean/vm_elaborator): incorrect arity
2019-03-06 16:52:03 -08:00
Leonardo de Moura
110c727237
feat(library/compiler/llfn): rename to_llnf_fn => to_lambda_pure_fn, and make sure it produce valid terminal expressions
...
A terminal must be a variable, jump or cases.
This commit also makes sure `explicit_boxing_fn` preserve valid terminals.
2019-03-06 16:42:51 -08:00
Leonardo de Moura
b32ba9cb9d
feat(library/compiler/compiler): add compiler trace option ll_infer_type
2019-03-06 14:53:27 -08:00
Leonardo de Moura
d0c1c40cc1
feat(library/init/lean/compiler/ir): started alpha equivalence
...
I will continue this module later, after I fix a bug in the compiler
exposed by these new functions.
2019-03-06 12:32:30 -08:00
Leonardo de Moura
50476328ff
feat(library/init/lean/name): add name_map
2019-03-06 12:32:08 -08:00
Leonardo de Moura
801f55faf0
chore(boot): update
2019-03-06 11:07:02 -08:00
Leonardo de Moura
6d7411cc07
perf(library/init/data/option/basic): missing [inline]
2019-03-06 10:58:12 -08:00
Sebastian Ullrich
1ad5450853
perf(library/init/control/coroutine): mark as [inline_as_reduce]
2019-03-06 17:30:20 +01:00
Sebastian Ullrich
c17cabf58b
chore(boot): update
2019-03-06 16:28:55 +01:00
Sebastian Ullrich
ed4a0d904d
feat(library/init/lean/elaborator): make meta, remove max_commands
2019-03-06 16:26:21 +01:00
Leonardo de Moura
5f46ca210d
chore(boot): update
2019-03-06 07:09:57 -08:00
