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

5526 commits

Author SHA1 Message Date
Leonardo de Moura
1935986f3c fix(library/compiler/compiler): we must compile (non external) opaque constants 2019-03-16 18:41:58 -07:00
Leonardo de Moura
b1c187f717 feat(library/compiler): allow io unit as main function result type 
When `io unit` is used, we use `return 0` for `result.ok`, and `return
1` for `result.except`.
 2019-03-16 16:05:45 -07:00
Leonardo de Moura
6d0ec3a8c9 refactor(library/init/io): implement io monad using estate monad 2019-03-16 15:34:58 -07:00
Leonardo de Moura
20ba4c4b04 feat(kernel): opaque constants 
They are very similar to `theorems`, but they are never ever unfolded.
 2019-03-15 15:45:06 -07:00
Leonardo de Moura
0888dee25e chore(*): meta ==> unsafe 2019-03-15 15:04:40 -07:00
Leonardo de Moura
9afee85919 fix(library/vm/vm_aux): remove old code 
Remark: `vm_timeit` was for the Lean 3 `timeit` primitive which is
different from the Lean 4 one. It has a different arity, and was
producing an assertion violation at emit_bytecode.cpp
 2019-03-14 16:04:10 -07:00
Leonardo de Moura
65441a79ca fix(library/compiler/llnf): neutral element 2019-03-14 16:01:42 -07:00
Leonardo de Moura
590e40cb7b chore(library/compiler/csimp): leftover 2019-03-14 16:00:59 -07:00
Leonardo de Moura
d3ba9ef7fa feat(library/compiler/csimp): eliminate join points that are used only once 2019-03-14 10:43:35 -07:00
Leonardo de Moura
b1e812ea9d feat(library/compiler/specialize): restrict the kind of argument that can be specialized 2019-03-13 16:39:30 -07:00
Leonardo de Moura
3fe6858a93 feat(library/compiler/csimp): make csimp simplifies unreachable branches 
`let x := lc_unreachable in e` => `lc_unreachable`
`let x := e in lc_unreachable` => `lc_unreachable`
 2019-03-13 11:45:40 -07:00
Leonardo de Moura
88453f037c feat(library/compiler/csimp): erase base argument from fix_core 2019-03-12 18:05:41 -07:00
Leonardo de Moura
62df218a8e fix(library/compiler/specialize): another bug 2019-03-12 14:08:52 -07:00
Leonardo de Moura
e858d7f5b8 fix(library/compiler/specialize): yet another specializer bug 
@kha I found yet another bug in the specializer code :(
The bug is related to the previous bug fix where we try avoid
duplication of work by lambda abstracting let-variables.
We knew this could introduce type errors, but I thought it would only
happen in very complicated programs that make a heavy use of dependent
types. Actually, this is not the case. I just found an instance when
I was playing with the new parser.
 2019-03-12 12:25:32 -07:00
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
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
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
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
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
d2ef708763 feat(library/compiler/ll_infer_type): _unreachable 2019-03-09 07:49:51 -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
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