Leonardo de Moura
079980f0d6
fix(library/compiler/csimp): fix inlining
2018-09-18 22:03:31 -07:00
Leonardo de Moura
d3e225ec65
fix(library/init): missing @[inline]
2018-09-18 21:42:22 -07:00
Leonardo de Moura
17a779c36f
fix(library/compiler/csimp): inlining at projections
2018-09-18 21:09:49 -07:00
Leonardo de Moura
d0e804b780
feat(library/compiler): add support for inlining to new compiler stack
...
We also delay the simplification of lambdas in the right hand side of let-declarations.
2018-09-18 17:24:25 -07:00
Leonardo de Moura
54f04dca9f
feat(library/init/core): use cases_on instead of rec_on
2018-09-18 15:25:15 -07:00
Leonardo de Moura
39d9a709d5
feat(library/compiler): improve simplification
2018-09-18 14:51:58 -07:00
Leonardo de Moura
4f53e505b0
fix(library/compiler): we need to unfold auxiliary nested _match applications eagerly
2018-09-18 14:17:37 -07:00
Leonardo de Moura
8e1a6dc81b
chore(library/compiler/preprocess): add trace.compiler.state1 option
2018-09-18 08:23:53 -07:00
Leonardo de Moura
2a13ea484e
chore(library/init/lean/ir/extract_cpp): add space
2018-09-18 08:23:32 -07:00
Leonardo de Moura
ff725b8329
feat(library/compiler): simplify cheap beta reduction
...
The LCNF format contained may `let`-declarations of the form
```
x : (fun y, c) a := t
```
where `c` does not depend on `y`.
We reduce them to
```
x : c := t
```
2018-09-17 19:58:54 -07:00
Leonardo de Moura
c23411e1ca
chore(library/compiler/preprocess): display function name
2018-09-17 19:58:54 -07:00
Sebastian Ullrich
1f239c9f2a
feat(library/init/lean/parser/syntax): pretty-print ident nodes
...
Painfully, because `ident.view` is not defined yet
2018-09-17 18:47:50 -07:00
Sebastian Ullrich
fa0148e5b8
feat(library/init/lean/parser): declarations and binders
2018-09-17 18:47:50 -07:00
Sebastian Ullrich
a6f25e2ae7
refactor(library/init/lean/parser/token): id ~> ident, ident ~> ident.parser
2018-09-17 18:47:50 -07:00
Sebastian Ullrich
ea4d7af66d
refactor(library/init/lean/parser/command): move out notations
2018-09-17 18:47:50 -07:00
Sebastian Ullrich
6b28162eee
chore(library/init/lean/parser/combinators): move out combinators
2018-09-17 18:47:50 -07:00
Sebastian Ullrich
7012583245
feat(library/init/lean/parser/term): universes on identifiers
2018-09-17 18:47:50 -07:00
Leonardo de Moura
9b29572604
feat(kernel/type_checker): improve infer_let
...
Before this commit, given a term `let x : t := v in b`, `infer_type`
would return `let x : t := v in T` where `T` is the type of `b` in
the local context extended with declaration `x : t := v`.
This is correct, but it produces unnecessarily large terms
in the new compiler stack which makes a heavy use of let-expressions.
We noticed the problem when the size of some .olean files were 100x
bigger. For example, `repr.olean` increased from 136Kb to
13Mb after we started saving the `._cstage1` (code after after
simplification) in the `.olean` files.
The new implementation relies on the fact that `T` seldom depends on
`x`. So, in most cases, the result is just `T` instead of `let x : t := v in T`
After this change, the new .olean files are at most 56% bigger than
.olean files not containing `._cstate1` code. This seems reasonable
since most of our .olean files only contain code and we are storing a
copy of each function.
@kha The new lcnf format keeps exposing problems :)
2018-09-17 18:25:27 -07:00
Leonardo de Moura
4fd2e71bc9
chore(library/init/data/ordering/basic): mark cmp_using as [inline]
2018-09-17 14:56:31 -07:00
Leonardo de Moura
5d455bf10a
chore(library/compiler): skip type checking for _cstage1 declarations
...
This is a temporary hack for speeding up build time.
2018-09-17 14:45:04 -07:00
Leonardo de Moura
b07c718425
refactor(library/init/core): change ite signature
2018-09-17 14:27:28 -07:00
Leonardo de Moura
faf4561723
feat(library/compiler/lcnf): expand nested f._match_<idx> applications at to_lcnf
2018-09-17 13:41:03 -07:00
Leonardo de Moura
f9fb1fec88
fix(library/compiler/csimp): bug at distrib_app_cases
...
The result could contain type errors.
2018-09-17 13:31:50 -07:00
Leonardo de Moura
ca176259f4
feat(library/compiler): treat f._meta_rec applications as f applications in the new compiler stack
2018-09-17 09:56:06 -07:00
Leonardo de Moura
3ebf1db2dc
feat(library/compiler): treat f._meta_rec applications as f applications
2018-09-17 09:48:14 -07:00
Leonardo de Moura
b1e80f8f4d
chore(library/compiler/cse): fix style
2018-09-17 09:47:58 -07:00
Leonardo de Moura
2abe11ce63
chore(library): _meta_aux ==> _meta_rec
2018-09-17 09:08:12 -07:00
Leonardo de Moura
5a8ddb2817
fix(library/message_builder): compilation warning
2018-09-17 08:53:03 -07:00
Leonardo de Moura
33821f399c
chore(library/compiler): lc_util.* ==> util.*
2018-09-17 08:50:50 -07:00
Leonardo de Moura
81067d355d
chore(library/compiler): util.* ==> old_util.*
2018-09-17 08:44:45 -07:00
Leonardo de Moura
f0e24e73f4
feat(kernel/expr): missing constructor
2018-09-16 14:30:43 -07:00
Leonardo de Moura
499ab0baa3
feat(library/compiler/preprocess): save declarations after csimp
...
We inline functions using these auxiliary declarations.
2018-09-16 14:07:42 -07:00
Leonardo de Moura
59652e885a
fix(kernel/type_checker): whnf_fvar
2018-09-16 13:49:35 -07:00
Leonardo de Moura
000db32e40
chore(kernel/type_checker): remove dead branch
2018-09-16 12:22:28 -07:00
Leonardo de Moura
871e7de673
chore(library/init/core): move auxiliary constants to beginning of the file
2018-09-16 11:02:17 -07:00
Leonardo de Moura
d378e95467
feat(library/compiler/csimp): eliminate cases over structures
2018-09-15 16:12:11 -07:00
Leonardo de Moura
512c7b6ab6
fix(library/compiler/old_cse): linker issue with clang on OSX
2018-09-14 17:58:16 -07:00
Leonardo de Moura
c60be8c6e3
fix(library/compiler/csimp): debug build
2018-09-14 17:55:45 -07:00
Leonardo de Moura
52d1abf0bc
feat(library/compiler): add cse to new compiler stack
2018-09-14 17:48:18 -07:00
Leonardo de Moura
ef21f069bd
refactor(library/compiler): add is_cases_on_app helper function
2018-09-14 17:33:03 -07:00
Leonardo de Moura
8571430a34
chore(library/compiler): cse ==> old_cse
2018-09-14 16:58:37 -07:00
Leonardo de Moura
9e265f8c7f
chore(library/compiler/csimp): remove unused var
2018-09-14 16:46:25 -07:00
Leonardo de Moura
e8ab46619b
chore(tests/lean/run/new_compiler): fix test
2018-09-14 16:42:53 -07:00
Leonardo de Moura
242ab16d1c
feat(library/compiler/csimp): simplify cases minor premises
2018-09-14 16:40:22 -07:00
Leonardo de Moura
8380035a6c
fix(library/compiler/csimp): bug at find
2018-09-14 16:40:22 -07:00
Leonardo de Moura
768a45b7f9
feat(library/compiler/csimp): avoid unnecessary let-decls
2018-09-14 16:40:22 -07:00
Leonardo de Moura
8840f340aa
feat(library/compiler/csimp): add reduction for application over cast
2018-09-14 16:40:22 -07:00
Sebastian Ullrich
65816d8b87
chore(library/message_builder): handle nested kernel exceptions
2018-09-14 16:33:04 -07:00
Sebastian Ullrich
906f59e16e
fix(library/init/lean/parser/token): token': do not ignore source_info
2018-09-14 16:33:04 -07:00
Sebastian Ullrich
ae7df32428
refactor(library/init/lean/parser/syntax): setting source_info.leading is much easier after parsing
2018-09-14 16:33:04 -07:00
