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

15237 commits

This branch
This branch
All branches
Author SHA1 Message Date
Sebastian Ullrich
cd287629cb feat(library/init/lean/elaborator): initial version of translating syntax trees to preterms 2018-11-19 13:38:45 +01:00
Sebastian Ullrich
9e8dfbad79 perf(library/init/lean/parser): reintroduce separate syntax.ident constructor with much simpler and more efficient encoding 2018-11-18 16:55:04 +01:00
Sebastian Ullrich
68dad5e77c chore(library/init/lean/parser/token): raw: unnecessary try 2018-11-18 16:11:41 +01:00
Sebastian Ullrich
6d0b3afa7e fix(library/compiler/compiler): do not silently abort on user-given sorrys 2018-11-17 18:00:55 +01:00
Leonardo de Moura
3d24c6466b feat(library/compiler/llnf): generate _boxed version eagerly 2018-11-15 18:10:20 -08:00
Leonardo de Moura
ae037c2a23 fix(library/compiler/builtin): incorrect assertion 2018-11-15 18:09:02 -08:00
Leonardo de Moura
da92557076 chore(library/vm/vm_int): missing builtin in the old VM 2018-11-15 16:58:05 -08:00
Leonardo de Moura
b55b1deaf5 chore(library/compiler): remove ir.cpp 
There is only one missing transformation: insert explicit reference counting instructions.
We will implement this transformation at `llnf.cpp`. After that, we are
ready to emit C++ code.
 2018-11-15 16:53:44 -08:00
Leonardo de Moura
e5666b3464 feat(library/compiler): remove another reference to vm.h 2018-11-15 16:38:01 -08:00
Leonardo de Moura
db5d976278 feat(library/compiler): use new builtin module 2018-11-15 16:30:42 -08:00
Leonardo de Moura
7937f1e010 chore(library/init/util): remove util.lean 
At least initially, we will not support these primitives in the new compiler.
 2018-11-15 16:27:52 -08:00
Leonardo de Moura
3a7d407d6c feat(library/compiler/builtin): register io primitives 
TODO: implement `io` primitives in the new runtime
 2018-11-15 16:14:50 -08:00
Leonardo de Moura
4f2997d691 feat(library/compiler/builtin): use std::unordered_map 2018-11-15 13:48:11 -08:00
Leonardo de Moura
4b65e0bace refactor(library/compiler/builtin): do not store pointer to functions 
The interface between the (to be implemented) new interpreter and the
compiled code will be automatically generated.
 2018-11-15 13:39:04 -08:00
Leonardo de Moura
5acdd68ad5 feat(library/compiler/init_module): initialize builtin module 2018-11-15 13:33:02 -08:00
Leonardo de Moura
b501613f8c feat(library/compiler/builtin): register string primitive functions 2018-11-15 13:26:41 -08:00
Leonardo de Moura
70c4e33cf2 feat(runtime/object): missing string.iterator builtin functions 2018-11-15 13:05:29 -08:00
Leonardo de Moura
4a0a3f8d85 feat(library/compiler/builtin): register int primitives 2018-11-15 12:39:35 -08:00
Leonardo de Moura
d0e96ee600 feat(runtime/object): missing int builtins 2018-11-15 12:31:34 -08:00
Leonardo de Moura
04227701d6 chore(tests/lean/run): fix the tests 
@kha I found the real issue with these two tests.
You have modified the compiler to ignore definitions containing `sorry` :)
 2018-11-15 11:21:12 -08:00
Leonardo de Moura
a3db4e8e09 chore(*): style 2018-11-15 10:59:17 -08:00
Leonardo de Moura
d0ccaa1083 chore(tests/lean): fix tests 
TODO: `io` modifications performed yesterday may have affected `eval`.
 2018-11-15 10:56:03 -08:00
Leonardo de Moura
efa703d2b5 feat(runtime): implement string.iterator primitives in the new runtime 
Some of the primitives do not have optimal implementation.

@Kha Could you please check if everything we use in the parser has a
reasonable implementation?
 2018-11-15 10:42:23 -08:00
Leonardo de Moura
ed4eeddf0a feat(runtime/object): add more string primitives 2018-11-14 16:51:10 -08:00
Leonardo de Moura
a551fbe892 chore(library): remove dead code: comp_val 2018-11-14 16:50:21 -08:00
Leonardo de Moura
23202bada1 chore(runtime/object): allow shared objects at string_append and string_push 2018-11-14 16:30:23 -08:00
Leonardo de Moura
9258a12ed4 feat(library/compiler): add new builtin management module 
TODO: register `int`, `string` and `io` primitives
 2018-11-14 15:58:12 -08:00
Leonardo de Moura
2fa938220b chore(library/init/data/string): cleanup 2018-11-14 14:09:45 -08:00
Leonardo de Moura
dfdf42ce34 chore(library/init/io): minimize io interface 
We are moving to new compiler stack.
 2018-11-14 13:59:25 -08:00
Leonardo de Moura
c599d78639 feat(library/init/io): implement io.iterate in Lean 
cc @kha
 2018-11-14 13:43:02 -08:00
Leonardo de Moura
439d0319f0 fix(library/compiler/specialize): array out of bounds 2018-11-14 13:42:50 -08:00
Leonardo de Moura
835b3a10cc chore(library/init): consistent names 2018-11-14 13:08:57 -08:00
Leonardo de Moura
49d779e3a6 fix(library/vm/vm_string): we were not using the builtin implementation for string.decidable_eq 2018-11-14 09:48:43 -08:00
Sebastian Ullrich
600b7ceb28 fix(library/init/lean/parser/syntax): make sure macro scopes are not pushed inside of ident nodes 2018-11-14 17:23:32 +01:00
Sebastian Ullrich
8d25c6edc5 fix(library/compiler/llnf): fix out-of-bounds access 
@leodemoura is this correct?
 2018-11-14 09:52:22 +01:00
Sebastian Ullrich
2f8e6cc975 chore(frontends/lean/elaborator,library/compiler/compiler): avoid error recovery errors 2018-11-14 09:52:22 +01:00
Leonardo de Moura
2271d4bccc chore(library/compiler): fix debug build 2018-11-13 15:26:25 -08:00
Leonardo de Moura
7365b9ed30 feat(library/compiler/lambda_lifting): cache names for lifted lambdas 
We were creating hundreds of different names for simple lambdas. Example:
```
λ a, @coroutine.done a
```
 2018-11-13 15:13:55 -08:00
Leonardo de Moura
a2817c3644 refactor(library/compiler): move closed term cache to separate module 2018-11-13 15:01:57 -08:00
Leonardo de Moura
1e5e28a933 fix(library/compiler/csimp): apply app-of-cases eagerly before other floating *-of-cases variants 
Motivation: consider the following example

```
let m := if b then m1 else m2,
state.bind m (fun p, BIG p.1 p.2)
```
we first eta-expand the term, put in LCNF and inline state.bind
```
fun s,
let m   := decidable.cases_on b (fun h, m1) (fun h, m2) in
let x_1 := m s in
prod.cases_on x_1 (fun a s', BIG a s')
```
then, we apply `*-of-cases` at `m := ...` and its continuation, but we
need a joint point since the continuation is big. Then, we get
```
fun s,
let j_1 := fun x_1,
    let x_1 := m s in
    prod.cases_on x_1 (fun a s', BIG a s') in
decidable.cases_on b
  (fun h, let y := m1 in j_1 y)
  (fun h, let y := m2 in j_1 y)
```
This code is not good if `m1` and `m2` are functions. At runtime, we
need to create a closure and pass it to the join point.
If we apply `app-of-cases` before other floating `cases` variants we
avoid this problem.
Here is the sequence of transformations if we apply `app-of-cases`
eagerly. We get
```
fun s,
let m   := decidable.cases_on b (fun h, m1) (fun h, m2) in
let x_1 := m s in
prod.cases_on x_1 (fun a s', BIG a s')
```
as before. Then, we apply `app-of-cases` at `m s`, and get
```
fun s,
let x_1 := decidable.cases_on b (fun h, m1 s) (fun h, m2 s) in
prod.cases_on x_1 (fun a s', BIG a s')
```
Then, we apply `cases-of-cases`, but we again create a join point.
```
fun s,
let j_1 := fun x_1, prod.cases_on x_1 (fun a s', BIG a s') in
decidable.cases_on b
  (fun h, let y := m1 s in j_1 y)
  (fun h, let y := m2 s in j_1 y)
```
However, this time we are passing a value to `j_1` instead of a closure.

`app-of-cases` has two benefits:
1- It never creates new join points since applications are always small in LCNF
2- It may reduce a `cases` that returns a closure into a `cases` that
returns a value.
 2018-11-13 09:14:46 -08:00
Leonardo de Moura
4136bad252 feat(library/compiler): insert boxing/unboxing instructions 2018-11-12 17:17:09 -08:00
Leonardo de Moura
3ae908f8de feat(library/compiler): add _jmp instruction, and skeleton for explicit boxing introduction step 2018-11-12 10:51:42 -08:00
Leonardo de Moura
c0ac39f7f0 chore(tests/lean/parser1): fix test output 2018-11-12 08:53:57 -08:00
Sebastian Ullrich
54b330ea66 feat(library/init/lean/expander): recursive, hygienic expansion 
Not optimized yet. Some performance numbers:
  352ms    11.0%      75ms     2.4%   expand_core
  339ms    10.6%      58ms     1.8%   list.mmap._main._at._private.1829070809.expand_core
   52ms     1.6%      38ms     1.2%   lean.parser.syntax.flip_scopes
 2018-11-12 13:15:14 +01:00
Leonardo de Moura
c111590adf fix(library/compiler/reduce_arity): incorrect assertion 2018-11-11 11:58:19 -08:00
Leonardo de Moura
95830a385d feat(src/library/compiler/reduce_arity): add temporary workaround 2018-11-09 16:09:25 -08:00
Leonardo de Moura
dc54f68222 feat(library/compiler): (try to) improve reduce_arity 2018-11-09 15:53:45 -08:00
Leonardo de Moura
5ab69262c4 chore(library/compiler/util): remove leftover 2018-11-09 15:10:28 -08:00
Leonardo de Moura
7c86a4dae7 feat(library/compiler): add reduce_arity compilation step 2018-11-09 14:30:33 -08:00
Leonardo de Moura
19bf71eb9c chore(library/compiler/simp_app_args): use ll_infer_type 2018-11-09 13:18:28 -08:00