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

522 commits

Author SHA1 Message Date
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
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
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
Leonardo de Moura
d3ad1cbfe1 feat(library/compiler): add type inference for ENF and LLNF 2018-11-09 13:17:11 -08:00
Leonardo de Moura
37df96e3e7 feat(library/compiler/csimp): inline recursive functions marked with [inline_if_reduce] 2018-11-09 10:15:47 -08:00
Leonardo de Moura
f38cbeda5f perf(library/compiler/csimp): avoid unnecessary local decl 2018-11-08 17:03:34 -08:00
Leonardo de Moura
b56674cc25 fix(library/compiler/specialize): remove bogus optimization 2018-11-07 18:00:28 -08:00
Leonardo de Moura
df39be927d feat(library/compiler): make sure application arguments are free variables or neutral terms in LLNF 2018-11-07 17:25:20 -08:00
Leonardo de Moura
f9236592cc chore(library/compiler/llnf): remove dead code 2018-11-07 16:48:32 -08:00
Leonardo de Moura
474c743d8a fix(library/compiler/llnf): do not expand atomic values 2018-11-07 16:43:46 -08:00
Leonardo de Moura
17679799a2 fix(library/compiler/cse): must take a flag indicating whether we are applying optimization after/before erasure 2018-11-07 16:38:24 -08:00
Leonardo de Moura
1191dd4deb refactor(library/compiler): move mk_runtime_type to util 2018-11-07 15:19:24 -08:00
Leonardo de Moura
c285d48c96 feat(library/compiler/erase_irrelevant): simplify mk_runtime_type 2018-11-07 15:10:41 -08:00
Leonardo de Moura
687e9d076d feat(library/compiler): add _apply and _closure instructions to LLNF 2018-11-07 13:30:28 -08:00
Leonardo de Moura
330e2700b1 chore(library/compiler/compiler): add trace.compiler.boxed option for debugging purposes 2018-11-06 16:55:02 -08:00
Leonardo de Moura
5acb5e63b1 feat(library/compiler): revise llnf instructions 
Motivation: make sure we can generate "portable" C++ code. "Portable"
here means we can compile the generated code using 32 and 64 bit machines.
 2018-11-06 16:55:02 -08:00
Leonardo de Moura
8af0c85d4f feat(library/compiler/erase_irrelevant): convert enumeration types into uint* types 2018-11-06 16:55:02 -08:00
Leonardo de Moura
83ebacb8af chore(library/compiler/util): style 2018-11-06 16:55:02 -08:00
Leonardo de Moura
9f3544aaa4 feat(library/compiler/erase_irrelevant): preserve enumeration types 2018-11-06 16:55:02 -08:00
Leonardo de Moura
6f03df871b chore(library/compiler): remove whnf_upto_runtime_type 
It is not needed anymore.
 2018-11-06 16:55:02 -08:00
Leonardo de Moura
e63721958b refactor(library/compiler): add is_enum_type auxiliary function 2018-11-06 16:55:02 -08:00
Leonardo de Moura
216a3632cc refactor(library/compiler/llnf): simplify llnf primitive instructions 2018-11-06 16:55:02 -08:00
Leonardo de Moura
39850d3b84 chore(library/compiler/llnf): remove dead global 2018-11-06 16:55:02 -08:00
Leonardo de Moura
c108fc95cb feat(library/compiler/ir): basics 2018-11-05 17:04:23 -08:00
Leonardo de Moura
8de7637f75 feat(library/compiler): add to_ir skeleton 2018-11-05 17:04:23 -08:00
Leonardo de Moura
733bbc521f feat(library/init/core): mark thunk and task primitives with [noinline] 
In the future, we should use the `[builtin]` attribute which cannot be
overwritten by the user.
 2018-11-02 13:54:40 -07:00
Leonardo de Moura
b23251fd6e feat(library/compiler/lambda_lifting): preserve join points when performing lambda lifting 2018-11-01 16:04:25 -07:00
Leonardo de Moura
e11fe27de2 chore(library/compiler/lambda_lifting): temporary hack 
Make sure that a join point that has been lambda lifted is not tagged as
a join point anymore.
 2018-11-01 15:21:14 -07:00
Leonardo de Moura
f27ab2bb38 chore(library/compiler/emit_bytecode): remove dead code 2018-11-01 14:21:20 -07:00
Leonardo de Moura
f22bdec775 feat(library/vm): add support for join-points in the old VM 
Motivation: to make progress in the new compiler stack, we have
to preserve join points during lambda lifting. Right now, they are
lifted as regular lambdas. So, to keep them, we need some basic
support for them in the old VM. The implementation here is quick and
dirty. This is not an issue since this code will be deleted soon.
 2018-11-01 14:07:59 -07:00
Leonardo de Moura
ae30b16f0d fix(library/compiler/lcnf): nat.zero ==> literal 2018-11-01 11:59:17 -07:00
Leonardo de Moura
5d89347241 feat(library/compiler/llnf): improve memory cell reuse heuristic 2018-10-31 14:44:33 -07:00
Leonardo de Moura
e21608d456 chore(library/compiler/csimp): style 2018-10-31 13:25:54 -07:00
Leonardo de Moura
e68372cfd9 fix(library/compiler/csimp): another join point related bug 2018-10-31 13:22:20 -07:00
Leonardo de Moura
39c2ee2931 chore(library/compiler/llnf): typo 2018-10-31 13:22:14 -07:00
Leonardo de Moura
12a01d101c refactor(library/compiler/llnf): memory cell reuse instruction set 2018-10-31 09:35:22 -07:00
Leonardo de Moura
67a78d1c76 chore(library/compiler/llnf): cleanup 2018-10-31 08:36:09 -07:00