Leonardo de Moura
9d325515d4
chore(library/compiler/util): reduce term size if possible
2019-03-28 17:35:12 -07:00
Leonardo de Moura
42fbe3c18c
chore(library/init,runtime,library/compiler): add fix primitive back
...
The new `partial def`s allow us to define `fix` in Lean, but the Lean
implementation is not as efficient as the native one. The native one
in C++ use weak pointers to prevent a closure allocation at every
recursive invocation.
This commit also fixes the `fixCore` helper functions that were broken
after we switched to camelCase.
We have updated the test `fix1.lean` to demonstrate the native
implementation is faster. Here are the numbers on my desktop.
```
./run.sh fix1.lean 24
721420279
Time for 'native fix': 816ms
721420279
Time for 'fix in lean': 1.34s
```
2019-03-27 17:13:53 -07:00
Leonardo de Moura
e0b0ca4830
chore(*): adapt C++ code to camelCase
2019-03-21 15:06:43 -07:00
Leonardo de Moura
bc75a24127
chore(library, frontends): use camelCase for attribute names
2019-03-21 15:06:43 -07:00
Leonardo de Moura
039e7fab48
refactor(library): add suffixes.h with commonly used suffixes such as brec_on
2019-03-21 15:06:43 -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
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
b1b75c7c2e
feat(library/compiler): borrow inference procedure
2019-02-22 15:23:42 -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
170579c803
feat(library/init/core): task builting primitives
2019-02-17 08:45:46 -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
0cb3ac683d
feat(library/compiler): connect new const_folding module implemented in Lean with csimp
2019-02-15 14:37:48 -08:00
Leonardo de Moura
07ed77e724
fix(library/compiler/util): decidable A missing at mk_runtime_type
2019-02-11 15:51:09 -08:00
Leonardo de Moura
03ecc363a0
fix(library/compiler/util): missing case
2019-02-11 15:14:02 -08:00
Sebastian Ullrich
34110945f2
refactor(library/compiler/llnf): replace is_runtime_builtin_cnstr with just is_builtin_constant
2019-02-06 09:35:16 -08:00
Leonardo de Moura
914b023920
feat(library/compiler): treat decidable as an enumeration type
...
Before this commit, `decidable` was not being treated as an
enumeration type, and this was very inconvenient because `bool` and
`decidable` were using a different representation at runtime.
This commit does not complete the modification. We still have to
regenerate `boot`, and then fix the builtin declarations at `runtime`.
cc @kha
2019-02-05 16:08:23 -08:00
Leonardo de Moura
3444a295e7
feat(library/compiler,runtime): builtin support for lean.name
2019-02-05 12:57:46 -08:00
Leonardo de Moura
c5b0258e49
feat(library/compiler/util): do not box unit
2019-02-04 16:19:48 -08:00
Leonardo de Moura
7c355d3ba6
feat(library/compiler): thunk support
2019-02-04 15:22:18 -08:00
Leonardo de Moura
d3756fd915
feat(library/compiler): add _void type for LLNF format
2019-01-28 13:06:25 -08:00
Leonardo de Moura
1293d976f7
fix(library/compiler/util): usize case was missing at to_uint_type
2019-01-18 15:50:14 -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
5ab69262c4
chore(library/compiler/util): remove leftover
2018-11-09 15:10:28 -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
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
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
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
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
c3d700ece1
feat(library/compiler/csimp): nat.succ x ==> x + 1
2018-10-29 13:53:59 -07:00
Leonardo de Moura
d871c4f7d8
feat(library/compiler): replace simp_inductive with llnf
2018-10-29 13:07:46 -07:00
Leonardo de Moura
7dcc12ba6f
feat(library/compiler/util): add is_runtime_builtin_cnstr
2018-10-27 17:09:12 -07:00
Leonardo de Moura
74b92cd419
feat(library/compiler/llnf): collect constructor info
2018-10-27 16:58:51 -07:00
Leonardo de Moura
a161eec8f2
feat(library/compiler): add llnf (low level normal form) skeleton
2018-10-27 12:36:30 -07:00
Leonardo de Moura
628b0c7919
feat(library/compiler): add [inline_if_reduce] attribute
2018-10-25 10:01:26 -07:00
Leonardo de Moura
de1dc3be88
chore(library/vm): remove vm_array
...
We are currently not using arrays in the old VM.
2018-10-23 12:49:25 -07:00
Leonardo de Moura
d07f115f21
chore(library/compiler/util): fix style
2018-10-23 11:32:56 -07:00
Leonardo de Moura
17377c55f3
feat(library/compiler/extract_closed): create an auxiliary constant of arity 0 for constant with arity > 0
...
This transformation is useful for caching the construction of closures
at runtime. For example, consider the following piece of code
```
λ α a,
@tree.cases_on a visit._main._lambda_1
(λ a_a a_a_1 a_a_2,
let _x_1 := visit._main ◾ a_a,
_x_2 := visit._main._lambda_5 a_a_1 a_a_2
in bind._main ◾ ◾ ◾ ◾ _x_1 _x_2)
```
where `visit._main._lambda_1` is of the form
```
visit._main._lambda_1 :=
λ _x, ...
```
At runtime, we will create a closure object for `visit._main._lambda_1`
since it has arity 1, but no arguments have been provided.
This commit implements a new transformation that creates an auxiliary
declaration with arity 0.
```
visit._main._closed_1 :=
visit._main._lambda_1
```
Its value is cached by the runtime. That is, the closure is created only
once.
@kha This optimizations reduces the number of closures by another 200k
at `parser1.lean`. We are now under 2million :)
2018-10-22 16:13:58 -07:00
Leonardo de Moura
0b38547e97
feat(kernel): move cheap_beta_reduce to kernel and use it at infer_let
2018-10-20 17:13:41 -07:00
Leonardo de Moura
4929af1dd3
feat(library/compiler/extract_closed): extract_closed is working
2018-10-19 18:32:49 -07:00
Leonardo de Moura
17b9b21555
feat(library/compiler/csimp): allow csimp to be used after erasure
2018-10-19 12:02:29 -07:00
Leonardo de Moura
78842d4b9b
fix(library/compiler/util): macro_inline was ignoring constants
2018-10-04 15:25:03 -07:00
Leonardo de Moura
c9aab6ef50
feat(library/compiler): register noinline attribute
2018-10-02 18:56:13 -07:00
Leonardo de Moura
dc937281b3
chore(library/init/string): remove string.iterator_imp
2018-10-02 13:46:01 -07:00
Leonardo de Moura
c05e7a31a3
chore(library/compiler): add is_runtime_scalar_type and is_runtime_builtin_type
2018-10-02 09:03:53 -07:00
Leonardo de Moura
25b45d6f9e
feat(library/compiler): add erase_irrelevant transformation to new compiler stack
2018-10-01 17:06:56 -07:00
