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

10999 commits

Author SHA1 Message Date
Leonardo de Moura
b320452f70 chore(runtime/object): remove iterator primitives from runtime 
They are now implemented in Lean.
 2019-03-12 07:09:48 -07:00
Leonardo de Moura
2a2f3c1429 chore(boot): update 2019-03-12 06:56:05 -07:00
Leonardo de Moura
68ebc2a5c5 feat(library/init/data/string/basic): implement iterators using uft8 low level API 2019-03-12 06:56:05 -07:00
Leonardo de Moura
cf3bbd7e25 feat(runtime): add utf8_prev and utf8_set 
Next goal: implement string.iterator in Lean
 2019-03-11 18:05:40 -07:00
Leonardo de Moura
609b8e87e5 feat(library/compiler/csimp): add fix_core_n => fix_core_m "eta-expansion-like" optimization 
After this commit, `fix_1.lean` is not slower than `fix.lean` anymore.
 2019-03-11 14:41:23 -07:00
Leonardo de Moura
1e821d4057 chore(library/init/fix): rename primitives 2019-03-11 13:41:13 -07:00
Leonardo de Moura
a1cbd39d74 feat(library/init/lean/extern): remove restriction from expand_extern_pattern 2019-03-10 11:42:39 -07:00
Leonardo de Moura
ff3bf508aa feat(library/init/fix, runtime): add fixpoint2, ..., fixpoint6 
The idea is to avoid allocating tuples when creating the fixpoint of
nary functions. For example, consider the new tests:
- tests/playground/fix.lean
- tests/playground/fix_with_tuples.lean

The second one (`fix_with_tuples`) uses the `fix` operator and tuples. For input = 20,
it creates more than 1 million extra objects. The first implementation
(`fix.lean`) using `fix₂` avoids this overhead.

TODO: Add support for pattern #N with N > 9 at
```
def expand_extern_pattern_aux (args : list string) : nat → string.iterator → string → string
```
 2019-03-10 11:19:02 -07:00
Leonardo de Moura
4ca9c6f22e feat(runtime): add efficient fixpoint implementation 2019-03-10 10:09:57 -07:00
Leonardo de Moura
eb2633a5f2 fix(runtime/alloc): segment recycling 2019-03-09 13:42:55 -08:00
Leonardo de Moura
8f6998acac fix(runtime/alloc): we may deallocate in a new thread before we allocated anything 2019-03-09 13:20:06 -08:00
Leonardo de Moura
01b4983fa2 fix(runtime/object): string_utf8_extract 2019-03-09 12:57:51 -08:00
Leonardo de Moura
ab73553bf2 chore(boot): update 2019-03-09 12:40:43 -08:00
Leonardo de Moura
c862ce4a75 feat(runtime, library/init/data/string/basic): add utf8_pos 
`utf8_pos` is a low level alternative for `string.iterator`.
TODO: implement `string.iterator` using it.
 2019-03-09 12:30:19 -08:00
Leonardo de Moura
402034df1f chore(library/init/data): move usize to uint 2019-03-09 10:32:23 -08:00
Leonardo de Moura
2032b10482 feat(library/init/data): bitwise operations 2019-03-09 10:19:35 -08:00
Leonardo de Moura
d2ef708763 feat(library/compiler/ll_infer_type): _unreachable 2019-03-09 07:49:51 -08:00
Leonardo de Moura
8799056607 chore(boot): update 2019-03-08 12:13:06 -08:00
Leonardo de Moura
b43ebab32c fix(library/compiler/specialize): we should not lambda abstract join points 2019-03-08 11:54:51 -08:00
Leonardo de Moura
7b1d15ec43 fix(library/compiler/specialize): avoid work duplication in the specializer 2019-03-08 11:21:49 -08:00
Sebastian Ullrich
6a96d94259 chore(boot): update 2019-03-08 17:26:02 +01:00
Sebastian Ullrich
ef7053dac9 chore(boot): update 2019-03-08 17:05:42 +01:00
Sebastian Ullrich
0580ce7cfa chore(boot): update 2019-03-08 15:34:37 +01:00
Leonardo de Moura
9962441b7b chore(boot): update 2019-03-07 15:44:43 -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
Leonardo de Moura
4744d12e38 chore(boot): update 2019-03-07 10:26:05 -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
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
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
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
801f55faf0 chore(boot): update 2019-03-06 11:07:02 -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
Leonardo de Moura
5f46ca210d chore(boot): update 2019-03-06 07:09:57 -08:00
Leonardo de Moura
5e39a711fc chore(init/lean/ir): remove old IR 2019-03-06 07:04:47 -08:00