Leonardo de Moura
ffbccf1ee9
fix(library/compiler): ByteArray bug
2019-06-03 15:01:16 -07:00
Leonardo de Moura
edeae776da
chore(library/module): module::add for declarations is not needed anymore
2019-05-14 11:23:35 -07:00
Leonardo de Moura
35317139fd
chore(library/compiler/util): style
2019-04-26 16:34:22 -07:00
Leonardo de Moura
f222dc7cca
feat(library/compiler): destructive updates for {x with ...} expressions
2019-04-22 13:35:11 -07:00
Leonardo de Moura
35d54c17bd
chore(library/compiler): remove [inline2] attribute
...
We may add it back in the future if we find compelling applications for
it. Right now, we don't have any.
2019-04-18 13:24:20 -07:00
Leonardo de Moura
89874edc14
feat(library/compiler/eager_lambda_lifting): lift selected lambdas
2019-04-17 18:10:21 -07:00
Leonardo de Moura
d662f312df
fix(library/compiler/util): loose bvars
2019-04-17 07:57:30 -07:00
Leonardo de Moura
8612c1ecae
chore(library/compiler/util): add debugging helper function
2019-04-16 17:12:09 -07:00
Leonardo de Moura
da00dae9df
fix(library/compiler/util): typo at has_inline2_attribute
2019-04-11 14:28:54 -07:00
Leonardo de Moura
0c9fe3c7d4
feat(library/compiler): add [inline2] attribute, and stage2 inlining
...
This feature is useful since it allows us to perform inlining
after lambda lifting has been performed.
2019-04-06 08:00:58 -07:00
Leonardo de Moura
c54589007e
feat(library/compiler): extract closed terms after caching stage2 decls
2019-04-06 07:19:19 -07:00
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
