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

10183 commits

Author SHA1 Message Date
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
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
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
fea637288d fix(library/init/data/nat/basic,library/vm/vm_nat): regression in old compiler: primitive for nat equality was ignored 
Improves parser performance by 26%
 2018-09-14 16:33:04 -07:00
Leonardo de Moura
1cc60fdeac feat(library/compiler): add helper functions 2018-09-14 15:41:01 -07:00
Leonardo de Moura
964e2f3efb feat(library/compiler/csimp): merge application-application 2018-09-14 15:23:50 -07:00
Leonardo de Moura
7174d53820 feat(library/compiler/csimp): distribute application over cases 2018-09-14 15:14:40 -07:00
Leonardo de Moura
1c0ff0db72 fix(library/compiler/lcnf): make sure lc_cast applications are not overapplied 2018-09-14 15:08:35 -07:00
Leonardo de Moura
24de0e95f1 feat(library/compiler/lcnf): make test complete 2018-09-14 14:45:51 -07:00
Leonardo de Moura
75b494e33d feat(library/compiler): use new constructor info 2018-09-14 13:51:53 -07:00
Leonardo de Moura
4874e25715 feat(kernel): save constructor idx and nfields at constructor_val 2018-09-14 13:45:58 -07:00
Leonardo de Moura
a2c5daeded feat(library/compiler/lcnf): modify LCNF format 
Now, the body of a let-expression is atomic.
 2018-09-14 13:26:24 -07:00
Leonardo de Moura
eb2d8543f7 chore(library/compiler/lcnf): add comment 2018-09-14 12:03:17 -07:00
Leonardo de Moura
dc1b3aceda fix(library/compiler/csimp): missing simplification 2018-09-14 09:36:13 -07:00
Leonardo de Moura
2638a77a79 feat(library/compiler/csimp): reduce cases of constructor 2018-09-14 09:24:48 -07:00
Leonardo de Moura
3cf0d0f77a chore(library/compiler): lcsimp ==> csimp 2018-09-14 09:07:35 -07:00
Leonardo de Moura
1c0a6367c8 feat(library/compiler): new dead let removal 2018-09-14 08:41:55 -07:00
Leonardo de Moura
960eab96b3 chore(library/compiler): minor changes 2018-09-13 18:13:53 -07:00
Leonardo de Moura
4cca030251 chore(library/compiler/lcnf): do not beta reduce at to_lcnf 2018-09-13 18:13:53 -07:00
Leonardo de Moura
31d98caa0f feat(library/compiler): add compiler simplifier skeleton 2018-09-13 18:13:53 -07:00
Sebastian Ullrich
647f40763c feat(library/message_builder): pretty-print kernel_exceptions 2018-09-13 16:38:40 -07:00
Sebastian Ullrich
98e09c274f feat(library/init/lean/parser/{pratt,level}): factor out pratt combinator, implement level parsers 2018-09-13 16:38:40 -07:00
Sebastian Ullrich
b7c3f517a9 feat(frontends/lean/builtin_exprs): support for precedence annotations in node!/node_choice! 2018-09-13 16:38:40 -07:00
Leonardo de Moura
b8dceda9b7 chore(kernel): type_checker::context ==> type_checker::state 2018-09-13 14:06:57 -07:00
Leonardo de Moura
c02e2d3b56 feat(library/compiler/lcnf): split cases followed by application 2018-09-13 12:57:08 -07:00
Leonardo de Moura
23e5136ea2 fix(library/equations_compiler/wf_rec): do not generate code for auxiliary *._pack functions added by equation compiler 
In the new equation compiler, we should not generate code in the
equation compiler.
 2018-09-12 22:05:52 -07:00
Leonardo de Moura
20f31c85bf chore(kernel/type_checker): we don't use the kernel type checker for elaboration anymore 2018-09-12 20:36:32 -07:00