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

14757 commits

This branch
This branch
All branches
Author SHA1 Message Date
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.

Lists are efficient enough and make it easier to customize the trie construction.

Keep the `donotinline` though.
 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
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