Leonardo de Moura
7cfd3b4129
feat(library/compiler/lcnf): modify lcnf format
...
We should not require the body of a let-decl to be atomic.
2018-09-21 10:59:46 -07:00
Leonardo de Moura
097aa7ef14
chore(library/compiler): cleanup cce
2018-09-21 10:25:35 -07:00
Leonardo de Moura
ff2e28e557
feat(library/compiler): add cce: common case elimination
2018-09-20 21:38:57 -07:00
Leonardo de Moura
1534f17a89
feat(library/compiler/lcnf): add better support for complete-transition used in the equation compiler and x@ patterns
2018-09-20 21:38:57 -07:00
Leonardo de Moura
f556e0947b
fix(library/compiler/lcnf): bug, minor premise must have a lambda for each field in LCNF
2018-09-20 21:38:57 -07:00
Sebastian Ullrich
896b45239e
feat(library/module_mgr,shell/lean): abort on import with errors
2018-09-20 15:46:47 -07:00
Sebastian Ullrich
f21609c93d
chore(CMakeLists): relwithdebinfo build: disable assertions, frame pointer
...
(We don't really have any method for setting those just locally)
2018-09-20 15:46:47 -07:00
Leonardo de Moura
79c8e37cdf
fix(library/compiler/csimp): incorrect assertions
2018-09-20 15:33:57 -07:00
Leonardo de Moura
e55b65ad78
chore(library/compiler/lcnf): make it clear when we create the let-expr
2018-09-20 15:33:57 -07:00
Leonardo de Moura
0ee6d80b3c
feat(library/compiler/preprocess): add mode for llvm-profdata
2018-09-20 15:33:57 -07:00
Sebastian Ullrich
15d11cc483
feat(library/module_mgr): profile .olean serialization/deserialization
2018-09-20 13:54:17 -07:00
Leonardo de Moura
1efdd1a65d
feat(library/compiler/csimp): improve inliner
2018-09-20 12:05:49 -07:00
Leonardo de Moura
8d4f7bb8ec
feat(util/timeit): add simpler type for threshold
2018-09-20 12:05:48 -07:00
Leonardo de Moura
0ff1f16bf0
feat(frontends/lean/pp): add pp.compact_let option
...
It helps to debug the new compiler stack.
2018-09-20 12:05:48 -07:00
Sebastian Ullrich
65ddca1510
perf(library/init/lean/parser/syntax): avoid quadratic behavior in update_leading
2018-09-20 09:40:21 -07:00
Sebastian Ullrich
b859560a83
feat(library/init/lean/parser/term): @/@@ notation
2018-09-20 09:40:21 -07:00
Sebastian Ullrich
0a8d0a6870
feat(library/init/lean/parser/term): projection notation
2018-09-20 09:40:21 -07:00
Sebastian Ullrich
b8bd0cc5e6
feat(library/init/lean/parser/term): parentheses and tuples
2018-09-20 09:40:21 -07:00
Sebastian Ullrich
d7d968cead
feat(library/init/lean/parser/basic): merge explicit and default (0) token precedences
2018-09-20 09:40:21 -07:00
Sebastian Ullrich
6f68a0d1eb
feat(library/init/lean/parser/basic): check for conflicting tokens
2018-09-20 09:40:21 -07:00
Sebastian Ullrich
64a5d0f240
refactor(library/init/lean/parser): has_tokens default
2018-09-20 09:38:10 -07:00
Sebastian Ullrich
c7c459d47b
Revert "perf(library/init/lean/parser): collect tokens in trie instead of list, do not inline"
...
This reverts commit e4c50b2b09
2018-09-20 09:38:10 -07:00
Sebastian Ullrich
b7f7f257c5
feat(library/init/lean/parser/declaration): inductive, structure
2018-09-20 09:38:10 -07:00
Leonardo de Moura
f640b1bbac
feat(library/init/lean/ir/extract_cpp): missing inlines
2018-09-20 08:39:25 -07:00
Leonardo de Moura
38c9a2d28a
feat(library/compiler/csimp): do not invoke reduce_cases_cases until we implement it
2018-09-20 08:39:25 -07:00
Leonardo de Moura
a3a8165388
feat(library/init/control/monad): provide seq_right default implementation for monad
...
It was using the `seq_right` from `applicative` which is
```
(seq_right := λ α β a b, const α id <$> a <*> b)
```
and horrible code was being generated.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2018-09-20 08:39:25 -07:00
Leonardo de Moura
5ff9e24b17
feat(library/init/control): do not use unnecessary structures
...
It confuses the compiler.
2018-09-20 08:39:25 -07:00
Leonardo de Moura
28877282ce
fix(library/init/function): missing @[inline]
2018-09-20 08:39:25 -07:00
Leonardo de Moura
d3f4b8198b
fix(library/compiler/csimp): disable problematic optimization
2018-09-20 08:39:25 -07:00
Leonardo de Moura
94f01c90fd
feat(library/compiler/csimp): process lambda's lazily and combine dead-let-elimination
2018-09-20 08:39:25 -07:00
Sebastian Ullrich
623a6603cb
feat(library/init/lean/parser/term): lambda, pi, arrow
2018-09-19 12:36:34 -07:00
Sebastian Ullrich
e4c50b2b09
perf(library/init/lean/parser): collect tokens in trie instead of list, do not inline
2018-09-19 12:36:34 -07:00
Sebastian Ullrich
fc97c63c72
fix(library/derive_attribute): vm_compile synthesized instances
2018-09-19 12:36:34 -07:00
Sebastian Ullrich
e3afe02786
feat(library/init/lean/parser/declaration): doc comments and axioms
2018-09-19 12:36:34 -07:00
Sebastian Ullrich
80e37aa8c5
chore(library/init/lean/parser): improve error messages
2018-09-19 12:36:34 -07:00
Leonardo de Moura
8a8f1a6821
fix(library/compiler/util): has_inline_attribute
2018-09-19 09:33:54 -07:00
Leonardo de Moura
11f98a409e
chore(library/init/control/except): missing @[inline] annotations
2018-09-19 09:13:49 -07:00
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
