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

5506 commits

Author SHA1 Message Date
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
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
9fc813e601 fix(library/compiler/llnf): polymorphic projection resulting type 2019-03-07 11:24:08 -08:00
Leonardo de Moura
2984d6838c chore(library/compiler/ll_infer_type): dead variable 2019-03-07 10:21:14 -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
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
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
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
f2a161e5a9 feat(library/init/lean/util): Lean API for profiler 2019-03-06 10:37:38 +01:00
Leonardo de Moura
e067d82ab3 fix(library/compiler/llnf): nasty bug at explicit_rc_fn 
@kha I found this nasty bug today after I tried a small modification
at lean.parser.token. It is crazy that it didn't manifest itself before.
 2019-03-04 15:39:21 -08:00
Leonardo de Moura
f556423ae2 chore(library/compiler/llnf): add TODO 2019-02-25 17:43:21 -08: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
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
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
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
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
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
Leonardo de Moura
54a89dabb7 feat(library/compiler/llnf): new reset/reuse insertion procedure 2019-02-20 16:12:58 -08:00
Leonardo de Moura
937b947938 feat(library/compiler/llnf): decorate _cnstr instruction with inductive type name 2019-02-20 14:45:35 -08:00
Leonardo de Moura
b8cee758a5 feat(library/compiler/llnf): add push_proj_fn 2019-02-20 13:20:27 -08:00
Leonardo de Moura
2f218f7ec0 refactor(library/compiler/llnf): remove reset/reuse insertion from to_llnf_fn 
`to_llnf_fn` now produces an IR similar to the \lambda_pure in our paper.
 2019-02-20 11:16:29 -08:00
Leonardo de Moura
75ad042c66 feat(library/compiler/llnf): improve reuse/reset insertion 
It is now closer to the procedure at reuse.txt
 2019-02-19 22:14:29 -08:00
Leonardo de Moura
6276d1a7f1 feat(library/compiler/emit_cpp): avoid reset field instructions when reuse instruction is guaranteed to be executed 
expr_const_folding.lean takes 3 secs now.
 2019-02-19 13:44:46 -08:00
Leonardo de Moura
fe1d17583c feat(library/compiler/emit_cpp): special support for (proj|inc)*;reset sequences 
We save inc/dec operations. It improved the performance of
`expr_const_folding.lean`. On my Linux desktop
Before: 3.7 secs
After:  3.1 secs

cc @kha
 2019-02-19 13:06:22 -08:00
Leonardo de Moura
00aa78fffc feat(library/compiler/llnf): given y := _unbox.n x, mark x as an unboxed scalar if n < sizeof(void*) 2019-02-18 20:52:02 -08:00
Leonardo de Moura
feea8ecccd feat(library/compiler/llnf): avoid inc/dec operations on persistent objects 
inc/dec operations are noop's for persistent objects.
 2019-02-18 20:22:18 -08:00
Leonardo de Moura
b752dd1984 fix(library/compiler/emit_cpp): mark global objects as persistent 
They may be used by tasks, but they are not directly reachable from
task starting point.
 2019-02-17 11:45:51 -08:00
Leonardo de Moura
fca40151b2 fix(library/compiler/emit_cpp): is_shared should only be used on heap objects 2019-02-17 10:51:51 -08:00
Leonardo de Moura
75f4eb2f84 feat(library/compiler/emit_cpp): initialize task_manager at generated main function 2019-02-17 09:21:17 -08:00
Leonardo de Moura
170579c803 feat(library/init/core): task builting primitives 2019-02-17 08:45:46 -08:00
Leonardo de Moura
243d7c08e3 feat(library/compiler/llnf): avoid inc and dec operations on (boxed) small nat literals 2019-02-17 07:31:14 -08:00
Leonardo de Moura
3c60af74ae feat(library/compiler/llnf): avoid inc and dec instructions on neutral elements 2019-02-17 07:17:54 -08:00
Leonardo de Moura
78440919e8 feat(library/compiler/llnf): avoid unnecessary inc x and dec x instructions 
Example:
```
x = lean::box(0);
...
lean::inc(x);
...
lean::inc(x);
...
lean::dec(x);
...
```
In the example above, the `inc` and `dec` operations are unnecessary
since `x` is known to be a (boxed) scalar value. This commit fixes this.
 2019-02-17 06:50:25 -08:00
Leonardo de Moura
221704900a feat(library/compiler/llnf): avoid inc x and dec x instructions in branches where x is known to be a scalar value 2019-02-17 06:25:00 -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
Leonardo de Moura
e98acc86b8 feat(library/compiler/emit_cpp): "merge" the case with most occurrences as default: 2019-02-16 12:27:25 -08:00
Leonardo de Moura
54985b5a0e fix(library/compiler/csimp): accidentally removed nat.succ x ==> x + 1 transformation from csimp 2019-02-16 12:05:17 -08:00
Leonardo de Moura
e84f7744c3 feat(library/init/lean/compiler/const_folding): const fold nat.succ and char.of_nat 2019-02-16 11:15:19 -08:00
Leonardo de Moura
61274c7d35 feat(library/init/data/char): use uint32 instead of nat for defining char 2019-02-15 18:07:55 -08:00
Leonardo de Moura
38c7ec133d fix(library/compiler/llnf): missing case 2019-02-15 17:51:08 -08:00
Leonardo de Moura
ab45af5936 fix(library/compiler/csimp): avoid potential expensive reduction at csimp 
`whnf_core(e)` uses `whnf` to reduce the major premise of recursors and
projections, and `whnf` unfolds arbitrary definitions.
This commit adds a new option (`cheap`) to `whnf_core`. When
`whnf_core(e, true)` is used, the type checker will not unfolding
definitions when reducing the major premises.
 2019-02-15 17:43:21 -08:00
Leonardo de Moura
e0fd89e165 feat(library/init/lean/compiler): fold nat predicates 2019-02-15 16:17:16 -08:00
Leonardo de Moura
1080edd490 fix(library/compiler/lambda_lifting): make sure auxiliary _lambda declarations come before the declarations that use them 
This fixes a nasty initialization bug where an auxiliary `_closed`
declaration for an auxiliary `_lambda` is accessed before it is
initialized.
 2019-02-15 15:23:46 -08:00