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

15790 commits

This branch
This branch
All branches
Author SHA1 Message Date
Sebastian Ullrich
5e7970dca3 test(tests/playground/deriv): Haskell version 2019-02-28 14:57:57 +01:00
Leonardo de Moura
b25c0db35d tests(tests/playground/deriv): deriv in OCaml 2019-02-27 11:15:52 -08:00
Leonardo de Moura
f4302a5f48 test(tests/playground): new versions of unionfind1 
@kha I'm just trying to understand the performance numbers.
 2019-02-26 16:47:53 -08:00
Leonardo de Moura
2a0f5186e8 fix(runtime/object): bug at array_push 
Small object allocator was masking this bug.
 2019-02-26 14:19:37 -08:00
Leonardo de Moura
d128af10f9 test(tests/playground): add union find examples 
@kha I tried to make the examples self contained.

- unionfind1.lean uses the modified StateT and ExceptT
- unionfind2.lean uses the standard StateT and ExceptT
 2019-02-26 13:44:16 -08:00
Sebastian Ullrich
f366af76ac test(tests/playground/rbmap): consistent naming 2019-02-26 20:27:23 +01:00
Sebastian Ullrich
850001b996 test(tests/playground): rbmap.hs, Makefile 2019-02-26 20:26:55 +01:00
Sebastian Ullrich
c4bc783ef4 test(tests/playground/run.sh): split out compile.sh 2019-02-26 20:25:30 +01:00
Leonardo de Moura
6f73f19d19 chore(tests/playground/rbmap_standalone): make sure lean version mirrors the OCaml one 2019-02-26 10:37:12 -08:00
Leonardo de Moura
b883388d66 chore(tests/playground/rbmap_standalone): add missing [specialize] and remove alias 2019-02-26 10:06:18 -08:00
Leonardo de Moura
397be6d1c0 test(tests/playground/rbmap_standalone): add standalone rbmap benchmark 2019-02-26 09:56:59 -08:00
Leonardo de Moura
5635057549 feat(runtime/object): improve m_queue 2019-02-26 09:15:00 -08:00
Sebastian Ullrich
d258f325f1 test(tests/playground/binarytrees.lean): further opt 2019-02-26 18:08:09 +01:00
Sebastian Ullrich
24ad2e2b89 test(tests/playground/binarytrees.lean): optimize 2019-02-26 17:47:14 +01:00
Sebastian Ullrich
8e212ef9d9 test(tests/playground/Makefile): these ocamlopt parameters do nothing 2019-02-26 17:26:37 +01:00
Sebastian Ullrich
70a5c6d585 test(tests/playground/binarytrees.lean): more coarse parallelization 2019-02-26 17:21:45 +01:00
Leonardo de Moura
f2ef0eb597 fix(runtime/alloc): bug at import_objs 2019-02-26 07:34:26 -08:00
Leonardo de Moura
a9458fdcb3 chore(runtime/alloc): remove incorrect assertion 2019-02-26 07:33:53 -08:00
Sebastian Ullrich
9724491dc2 test(tests/playground/binarytrees.lean): parallelize 2019-02-26 16:16:34 +01:00
Leonardo de Moura
f556423ae2 chore(library/compiler/llnf): add TODO 2019-02-25 17:43:21 -08:00
Leonardo de Moura
1f3de14f9c fix(runtime/object): embarrassing bug at del_core 2019-02-25 17:42:56 -08:00
Leonardo de Moura
3a252f5b55 chore(runtime/object): avoid overhead when SMALL_ALLOCATOR is disabled 2019-02-25 15:32:59 -08:00
Sebastian Ullrich
cf0bf911c8 test(tests/playground): binarytrees benchmarks game benchmark in Lean, OCaml & Haskell 2019-02-25 23:46:10 +01:00
Sebastian Ullrich
c4740b7295 test(tests/playground/rbmap.ml): take the same input as Lean version 2019-02-25 14:51:16 +01:00
Leonardo de Moura
0f9c52367d feat(library/equations_compiler/elim_match): prune equations occurring after equation that contains only pattern variables 2019-02-24 18:21:22 -08:00
Leonardo de Moura
e82632cbe4 chore(boot): update 2019-02-24 15:44:11 -08:00
Leonardo de Moura
2ff3899d62 fix(library/compiler/llnf): missing case at push_proj_fn 
We were not pushing projections over scalar projections.
 2019-02-24 15:39:53 -08:00
Leonardo de Moura
66b55d9d12 chore(CMakeLists.txt): add options for enabling/disabling LAZY_RC and SMALL_ALLOCATOR 2019-02-24 15:11:48 -08:00
Leonardo de Moura
67d197a2e0 fix(runtime/object): correct support for objects without RC 
Lean was not crashing because we do not have region objects yet, and
the persistent objects still have a RC.
 2019-02-24 09:29:20 -08:00
Leonardo de Moura
ccea4c2043 chore(tests/playground/rbmap): use +1 instead of +k to avoid big number arithmetic when we increase number of elements inserted 2019-02-24 08:49:38 -08:00
Leonardo de Moura
935d90e77c chore(runtime/object): disable lazy RC to collect data at speedcenter 2019-02-23 17:37:11 -08:00
Leonardo de Moura
abd0f89820 feat(runtime): avoid extra switch 2019-02-23 17:35:21 -08:00
Leonardo de Moura
4b44c5ce36 feat(runtime/object): small object allocator 2019-02-23 17:17:56 -08:00
Leonardo de Moura
a9276c8834 fix(runtime/object): incorrect { 2019-02-23 17:16:49 -08:00
Leonardo de Moura
61f06fbf8e chore(boot): update 2019-02-23 09:16:29 -08:00
Leonardo de Moura
313fd69e8c feat(library/compiler/borrowed_annotation): mark objects as owned when stored in constructors 
@kha
 2019-02-23 09:12:53 -08:00
Leonardo de Moura
483125f828 test(tests/playground/rbmap): rbmap in OCaml 2019-02-22 17:43:27 -08:00
Leonardo de Moura
b971db6c11 chore(boot): update 2019-02-22 16:09:48 -08:00
Leonardo de Moura
d23216e3ee fix(library/compiler/llnf): bug at explicit_rc_fn 2019-02-22 16:01:52 -08:00
Leonardo de Moura
07aa990f22 fix(library/compiler/borrowed_annotation): ensure that exported functions do not take borrowed arguments 
In the future, we should automatically generate wrappers that make all
adjustments for us.
 2019-02-22 15:32:30 -08:00
Leonardo de Moura
b1b75c7c2e feat(library/compiler): borrow inference procedure 2019-02-22 15:23:42 -08:00
Leonardo de Moura
ba43d355b7 feat(library/compiler): add borrowed annotation inference skeleton 2019-02-22 11:14:38 -08:00
Leonardo de Moura
6646d7d62c chore(boot): update 2019-02-22 10:19:39 -08:00
Leonardo de Moura
01922794c5 fix(library/compiler/llnf): mk_boxed_version must take care of borrowed arguments and result 2019-02-22 10:18:17 -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
f91a37e686 chore(boot): update 2019-02-20 17:06:02 -08:00
Leonardo de Moura
ac9e37ed86 feat(library/compiler/llnf): we postpone the simplification of 1-reachable and all-eq cases_on expressions 
Reason: the `cases_on`-expressions are used to guide
`insert_reset_reuse_fn`. The new `simp_cases` simplifier applies the
1-reachable and all-eq cases_on expression simplifications after
`insert_reset_reuse_fn` is executed.
 2019-02-20 17:00:50 -08:00
Leonardo de Moura
35adf5f540 feat(library/compiler/llnf): avoid unfruitful reuse instruction replacements 2019-02-20 16:34:46 -08:00