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

4229 commits

Author SHA1 Message Date
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
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
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
2c3cfcf1dd feat(library/init/data/char/basic): add char.utf8_size 2019-03-09 10:46:29 -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
4828df1c7a chore(library/init/lean/frontend): revert 4333ab620 
The specializer has been fixed. So, we don't need this workaround
anymore.
 2019-03-08 12:06:49 -08:00
Leonardo de Moura
baec9a1b78 chore(library/init/lean/compiler/ir): minor 2019-03-08 09:14:54 -08: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
4333ab620c refactor(library/init/lean/frontend): use direct unbounded recursion instead of iterate_eio 2019-03-08 17:04:46 +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
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
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
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
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
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
6f83faaee0 perf(library/init/lean/parser/command): index command parsers by first token 2019-03-07 11:28:42 +01: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
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
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
ed4a0d904d feat(library/init/lean/elaborator): make meta, remove max_commands 2019-03-06 16:26:21 +01:00
Leonardo de Moura
5e39a711fc chore(init/lean/ir): remove old IR 2019-03-06 07:04:47 -08:00
Leonardo de Moura
6defbf82bd feat(library/init/lean/compiler/ir): add meta data, fix names and declarations 
cc @kha
 2019-03-06 06:56:16 -08:00
Sebastian Ullrich
cfce916438 perf(library/init/lean/parser/module): make sure commands_aux is tail-recursive 2019-03-06 13:58:26 +01:00
Sebastian Ullrich
85bc52b9f2 feat(library/init/lean/frontend): profile frontend 2019-03-06 11:08:38 +01:00
Sebastian Ullrich
f2a161e5a9 feat(library/init/lean/util): Lean API for profiler 2019-03-06 10:37:38 +01:00
Leonardo de Moura
ed4cd39d59 feat(library/init/lean/compiler/ir): new IR for Lean 
It is currently implemented in C++. The plan is to move the procedures
for inserting inc/dec, reset/reuse, and inferring borrow inferences to
Lean. Another goal is to make sure new IR optimizations can be
implemented in Lean, and to avoid backend optimizations that would
have to be duplicated in each backend (e.g., `emit_proj_inc_reset_seq`
at `emit_cpp.cpp`).

cc @kha
 2019-03-04 16:46:10 -08:00
Leonardo de Moura
3f50df70bc perf(library/init/lean/name): use hash code to speedup name.quick_lt 
We use the same trick in the C++ version of this function.

I measured the impact using `lean --new-frontend core.lean` and checking
the number of instructions executed reported by Valgrind.
Before:  4,891,642,264
After:   4,847,313,330
 2019-03-04 12:48:06 -08:00
Leonardo de Moura
20c877b277 chore(library/init/io): add inline 2019-02-22 09:55:36 -08:00
Leonardo de Moura
778e7e41f9 refactor(library/init/data/rbmap/basic): pass ins node-cell to balance1 and balance2. 
The idea is to reuse the cell. The trick is like the one we used for
improving state_t. It seems to work pretty well. Now, the Lean
version is 29% slower than the C++ one.

cc @kha
 2019-02-20 18:27:58 -08:00
Leonardo de Moura
835718955f refactor(library/init/data/rbmap/basic): store color in the node 
@kha Now the Lean version is approx. 50% slower than the C++ version.
 2019-02-20 17:52:03 -08:00
Leonardo de Moura
7623f64b5e feat(runtime,library/init/util): add some debugging helper function 2019-02-17 09:22:37 -08:00
Leonardo de Moura
170579c803 feat(library/init/core): task builting primitives 2019-02-17 08:45:46 -08:00
Leonardo de Moura
9e0b28d8ce feat(library/init/data/array/basic): improve 2019-02-16 16:08:10 -08:00
Leonardo de Moura
3c73c43ab2 feat(runtime,library/init/data/array/basic): add builtin support for arrays 2019-02-16 15:27:23 -08:00