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

5249 commits

Author SHA1 Message Date
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
Sebastian Ullrich
e2bf92ec21 feat(library/module_mgr,shell/lean): identify correct file on error in transitive import 2018-11-07 14:07:51 +01: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
Sebastian Ullrich
a551c0d8c9 fix(library/module_mgr): compiling a file with a failed transitive dependency may have succeeded without output 2018-11-06 21:31:02 +01: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
Sebastian Ullrich
7d6048c795 fix(library/message_builder): fix output of nested kernel exceptions 2018-11-05 17:37:21 +01:00
Sebastian Ullrich
c9bebb7411 feat(library/time_task): do not report inclusive times 2018-11-05 17:06:32 +01: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
adff01bba4 fix(library/vm/vm): handle InvokeJP at pc manipulation methods 2018-11-01 16:01:36 -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
e5432f5fb2 fix(library/type_context): memory access violation in the new type class inference optimization 2018-11-01 14:16:57 -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