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

443 commits

Author SHA1 Message Date
Sebastian Ullrich
5b44a6f93d feat(library/init/lean/parser/parsec): structured doc_comment syntax nodes 2018-12-19 14:42:33 +01:00
Sebastian Ullrich
0cf88598d2 feat(library/init/lean/parser/declaration): stricter grammar for universe parameters and non-optional declaration types 2018-12-19 14:41:17 +01:00
Sebastian Ullrich
4f7be93e87 feat(library/init/lean): remove support for section aliases 2018-12-18 17:04:04 +01:00
Sebastian Ullrich
db6b1d6e85 feat(frontends/lean/vm_elaborator,library/init/lean/elaborator): pass parser_state between languages, create parser object on C++ side to existing functions (that don't actually parse anything) 2018-12-18 15:30:38 +01:00
Sebastian Ullrich
4e96f092f9 feat(library/init/lean/elaborator): delegate elaboration of attribute 2018-12-14 17:38:19 +01:00
Sebastian Ullrich
0a63d39247 refactor(library/init/lean): syntax.mk_app'/mk_app ~> syntax.mk_app/mk_capp 2018-12-14 17:37:37 +01:00
Sebastian Ullrich
d9a22d43b2 feat(library/vm/vm_aux): add primitive for calling old elaborator 2018-12-14 17:36:56 +01:00
Sebastian Ullrich
ad11a8807f refactor(library/init/lean/elaborator): also use locally in elab_scope 2018-12-12 10:58:27 +01:00
Sebastian Ullrich
83e73cd04f feat(library/init/lean/elaborator): register declaration universe params 2018-12-12 10:42:18 +01:00
Sebastian Ullrich
009e499e95 feat(library/init/lean/elaborator): name lookup for universes 2018-12-11 19:01:56 +01:00
Sebastian Ullrich
94dec2cb9f feat(library/init/lean/elaborator): elaborate universe 2018-12-11 19:01:41 +01:00
Sebastian Ullrich
86b4261b1d refactor(library/init/lean/elaborator): store locally scoped data in the elab state instead of config, manually reset at scope end 2018-12-11 18:48:35 +01:00
Sebastian Ullrich
e5fec1ab00 feat(library/init/lean/elaborator): elaborate trivial headers 2018-12-07 10:32:09 +01:00
Sebastian Ullrich
306da89551 feat(library/init/lean/expander): expand universe( variable)s to multiple universe( variable) commands 2018-12-07 10:31:14 +01:00
Sebastian Ullrich
d372139d27 feat(library/init/lean/elaborator): recursively elaborate lists of commands 
This allows the expander to expand a single command to multiple commands
 2018-12-07 10:29:58 +01:00
Sebastian Ullrich
599d5c6c76 feat(library/init/lean/elaborator): log error on unknown command 2018-12-06 17:04:06 +01:00
Sebastian Ullrich
e7a6746b6a refactor(library/init/lean): share error function between expander and elaborator 2018-12-06 17:03:01 +01:00
Sebastian Ullrich
9c9e642210 feat(library/init/lean/elaborator): universe operators, subtype 2018-12-06 13:23:12 +01:00
Sebastian Ullrich
4b3995fac3 refactor(library/init/lean/parser/term): factor out opt_type parser 2018-12-06 13:23:12 +01:00
Sebastian Ullrich
8d3c0d4889 feat(library/init/lean/elaborator): also check to_pexpr on decl types 2018-12-06 13:23:12 +01:00
Sebastian Ullrich
143ac0e58a feat(library/init/lean/expander): also normalize bracketed binders in e.g. declarations 2018-12-06 13:23:12 +01:00
Sebastian Ullrich
cf1aa13a2c feat(library/init/lean/elaborator): to_pexpr: translate match nodes to pre_equations pexpr 
Building a proper `equations` pexpr in Lean is not feasible right now because we
need global+local name resolution, [pattern] attribute retrieval, ... to
reimplement `patexpr_to_pattern`. The `pre_equations` will instead be converted
by the old elaborator using this function (TBD).

With this change, `to_pexpr` can now translate every basic definition body in
`core.lean`.
 2018-12-05 12:57:41 +01:00
Sebastian Ullrich
79b7a29d3f fix(library/init/lean/parser/syntax): syntax.to_format: reverse scope stack 2018-12-04 13:44:46 +01:00
Sebastian Ullrich
ad27da3209 perf(library/init/lean/parser/syntax): optimize syntax.flip_scopes 2018-12-04 13:16:45 +01:00
Leonardo de Moura
607d22ae58 fix(library/compiler/csimp): bug at float_cases_on_core 
The bug occurs when floating `cases_on` application in code of the form
```
let x := C.cases_on ...
in t
```
and when the type of `t` depends on `x`.
The issue here is that the `x` declaration disappears after the float, but the resulting type still depends on it.
We fix the bug by replacing `x` with its value in the type.

cc @kha
 2018-11-30 11:40:41 -08:00
Sebastian Ullrich
c3f8e219c0 feat(library/init/lean/expander): preresolve global references (not actually used anywhere yet) 2018-11-27 18:02:51 +01:00
Sebastian Ullrich
d9dc4edd31 refactor(library/init/lean/parser/combinators): improve sep_by view 2018-11-27 17:11:14 +01:00
Sebastian Ullrich
ba0feb5daa chore(library/init/lean/expander): comments, minor refactoring 2018-11-27 16:35:20 +01:00
Sebastian Ullrich
89b67a0367 fix(library/init/lean/expander): mk_notation_transformer: reverse substitution list 2018-11-23 17:36:34 +01:00
Sebastian Ullrich
ee9c26947c feat(library/init/lean/elaborator): structure instances 2018-11-22 17:28:19 +01:00
Sebastian Ullrich
5043a6b9b3 feat(library/init/lean/{expander,elaborator}): show, let, choice 2018-11-22 17:25:46 +01:00
Sebastian Ullrich
7003fb6447 feat(library/init/lean/expander): command-level notations 2018-11-21 18:13:38 +01:00
Sebastian Ullrich
fd121f03bd feat(library/init/lean/expander): make set of transformers configurable 2018-11-21 18:13:38 +01:00
Sebastian Ullrich
32e3e8a336 feat(library/init/lean/elaborator): sort_app, explicit 2018-11-21 18:13:38 +01:00
Sebastian Ullrich
d1098534b2 feat(library/init/lean/expander): arrow, if 2018-11-21 18:13:38 +01:00
Sebastian Ullrich
cc93a2eb89 feat(library/init/lean/expander): extend "simple binders" to pi, expand pi 2018-11-21 18:13:38 +01:00
Sebastian Ullrich
a4b9cc83b8 feat(library/init/lean/{expander,elaborator}): progress 2018-11-21 18:13:38 +01:00
Sebastian Ullrich
222fff8862 refactor(library/init/lean/elaborator): introduce simple lambda binder 2018-11-21 18:13:38 +01:00
Sebastian Ullrich
8763e66f30 feat(library/init/lean/expander): allow macros not to unfold 2018-11-19 18:47:17 +01:00
Sebastian Ullrich
c8eaee74b4 feat(frontends/lean,library/init/lean/parser/combinators): add node_longest_choice! macro 2018-11-19 18:02:28 +01:00
Sebastian Ullrich
4ec98a4595 feat(library/init/lean/expander): unfold lambdas into normal form 2018-11-19 17:27:01 +01:00
Sebastian Ullrich
d10ff29bea fix(library/init/lean/parser/term): placeholder binder after bracketed binder 2018-11-19 13:38:45 +01:00
Sebastian Ullrich
cd287629cb feat(library/init/lean/elaborator): initial version of translating syntax trees to preterms 2018-11-19 13:38:45 +01:00
Sebastian Ullrich
9e8dfbad79 perf(library/init/lean/parser): reintroduce separate syntax.ident constructor with much simpler and more efficient encoding 2018-11-18 16:55:04 +01:00
Sebastian Ullrich
68dad5e77c chore(library/init/lean/parser/token): raw: unnecessary try 2018-11-18 16:11:41 +01:00
Leonardo de Moura
7937f1e010 chore(library/init/util): remove util.lean 
At least initially, we will not support these primitives in the new compiler.
 2018-11-15 16:27:52 -08:00
Sebastian Ullrich
600b7ceb28 fix(library/init/lean/parser/syntax): make sure macro scopes are not pushed inside of ident nodes 2018-11-14 17:23:32 +01:00
Sebastian Ullrich
54b330ea66 feat(library/init/lean/expander): recursive, hygienic expansion 
Not optimized yet. Some performance numbers:
  352ms    11.0%      75ms     2.4%   expand_core
  339ms    10.6%      58ms     1.8%   list.mmap._main._at._private.1829070809.expand_core
   52ms     1.6%      38ms     1.2%   lean.parser.syntax.flip_scopes
 2018-11-12 13:15:14 +01:00
Leonardo de Moura
182812a278 chore(library/init/lean/parser/token): make sure generate code does contain partially applied reader_t.or_else and reader_t.bind 
@kha This one was crazy, the compiler created a join point for the
continuation of the match-expression. Each case of the match was
invoking the join point with a different parser. Two of the branches
were the partially applied `reader_t.bind` and `reader_t.orelse`.
This change did not improve the performance much, but it makes sure we
don't waste time trying to figure out why we have these two partial
applications in the call graph.
 2018-11-08 17:39:46 -08:00
Leonardo de Moura
6eca6bdb0e perf(library/init/lean/parser/term): avoid eta-expansion issues 
cc @kha
 2018-11-08 16:21:37 -08:00