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

4724 commits

Author SHA1 Message Date
Leonardo de Moura
1a40a38bf1 feat(library/init/lean/class): add helper functions 2019-06-26 19:43:12 -07:00
Leonardo de Moura
14e6a62a19 feat(library/init/lean/class): class extension in Lean 
TODO: declare attributes
 2019-06-26 19:07:48 -07:00
Leonardo de Moura
f05df7c511 fix(library/init/lean/compiler/ir/simpcase): missing optimization 2019-06-26 19:07:07 -07:00
Leonardo de Moura
d55f99d345 chore(library/init/env_ext): remove leftover 2019-06-26 15:57:52 -07:00
Leonardo de Moura
14f05d2001 feat(library/init/lean/compiler): register [implementedBy] attribute using new attribute manager 2019-06-26 15:55:51 -07:00
Leonardo de Moura
1f53c4fd33 feat(library/init/lean/eqncompiler): register [matchPattern] attribute using new attribute manager 2019-06-26 15:38:14 -07:00
Leonardo de Moura
3a1aff1687 feat(library/init/lean/compiler): register [specialize] and [nospecialize] attributes using new attribute manager 2019-06-26 15:08:12 -07:00
Leonardo de Moura
e6e71a1f79 chore(init/lean/compiler): inline.lean ==> inlineattrs.lean 2019-06-26 14:10:00 -07:00
Leonardo de Moura
105ca4f76b feat(library/init/lean/compiler/inline): use EnumAttributes to declare inlining attributes 2019-06-26 14:01:30 -07:00
Leonardo de Moura
9f358649ec feat(library/init/core): avoid [macroInline] + [inline] in same declaration 
It will be rejected in the future.
 2019-06-26 13:54:58 -07:00
Leonardo de Moura
e00dc873a8 chore(library/pattern_attribute): [pattern] ==> [matchPattern] 2019-06-26 11:26:49 -07:00
Leonardo de Moura
5cfdd2452a chore(library/init/lean/compiler/externattr): remove unnecessary [export] annotations 2019-06-26 11:06:38 -07:00
Leonardo de Moura
16d423dab6 feat(frontends/lean): switch to [extern] implemented in Lean 
This commit also changes how we represent attribute parameters as
Syntax objects.
 2019-06-26 10:57:33 -07:00
Leonardo de Moura
c7597b8975 fix(library/init/lean/syntax): typo at isNatLit 2019-06-26 10:48:47 -07:00
Leonardo de Moura
64ee4e01a8 refactor(library/init/lean/attributes): split getParam into getParam and afterSet 2019-06-26 10:09:57 -07:00
Leonardo de Moura
be6ca5ba30 feat(library/init/lean/compiler/externattr): @[extern] attribute in Lean 2019-06-26 08:42:57 -07:00
Leonardo de Moura
0e86ae7a8c feat(library/init/lean): projection info in Lean 2019-06-26 07:57:10 -07:00
Leonardo de Moura
7ca4607ef3 chore(library/init/lean): move name_mangling.lean to compiler directory 2019-06-26 07:05:23 -07:00
Leonardo de Moura
2c39ecdbff chore(library/init/lean/disjoint_set): remove dead code 2019-06-26 06:30:24 -07:00
Leonardo de Moura
5148497e8c feat(library/init/lean/compiler/externattr): add mkExternAttr skeleton 2019-06-25 13:16:11 -07:00
Leonardo de Moura
5188eb2d3b feat(library/init/lean/compiler/externattr): decode [extern ...] parameters 2019-06-25 12:05:34 -07:00
Leonardo de Moura
aa111df0ec feat(library/init/lean/syntax): add Syntax.isIdOrAtom 2019-06-25 11:20:31 -07:00
Leonardo de Moura
2e01ac508a feat(library/init/lean/syntax): primitives for creating and testing string and nat literals 2019-06-25 10:39:23 -07:00
Leonardo de Moura
1ff6ee3155 feat(library/init/lean/attributes): allow getParam at ParametricAttribute registration to update environment 2019-06-25 09:15:55 -07:00
Leonardo de Moura
70a1589817 refactor(library/init/lean): move extern.lean to compiler subdirectory 2019-06-25 08:59:55 -07:00
Leonardo de Moura
74f0c77915 feat(library/init/lean/elaborator): implement elaborator strategy attributes in Lean 2019-06-25 08:24:56 -07:00
Leonardo de Moura
34586b185c feat(library/init/lean): implement reducibility attributes in Lean 2019-06-24 15:48:12 -07:00
Leonardo de Moura
5d27fd279b feat(library/init/lean/attributes): add EnumAttributes 2019-06-24 15:48:12 -07:00
Leonardo de Moura
45dc2cd49a feat(library/init/lean/compiler): [export] attribute in Lean 2019-06-24 15:48:12 -07:00
Leonardo de Moura
714468dc60 chore(frontends/lean): remove include and omit commands 2019-06-24 15:48:11 -07:00
Leonardo de Moura
af2d6dbd45 chore(library/init): avoid local attribute 2019-06-24 15:48:11 -07:00
Leonardo de Moura
94bca2b9d8 chore(library/init): mimize use of notations 2019-06-24 15:48:11 -07:00
Leonardo de Moura
dda0e38802 chore(library/init): avoid local notation 2019-06-24 15:48:11 -07:00
Leonardo de Moura
da09ef4f66 feat(frontends/lean/builtin_exprs): minor improvement 2019-06-24 15:48:11 -07:00
Leonardo de Moura
8f1345dc53 chore(library/init/lean/syntax): simplify SyntaxNodeKind 2019-06-21 14:24:44 -07:00
Leonardo de Moura
e4344b0c94 chore(library/init/lean/parser/default): update default 2019-06-21 14:20:40 -07:00
Leonardo de Moura
0fe8fd1307 feat(library/init/lean/parser/parser): notation 2019-06-21 14:20:22 -07:00
Leonardo de Moura
43fd0eeb94 chore(library/init/coe): minor 2019-06-21 14:15:26 -07:00
Leonardo de Moura
bc9e460f62 fix(library/init/lean/compiler/ir): collectUsedDecls must take initialization functions into account 
Move builtin parser level to its own directory
 2019-06-21 13:34:42 -07:00
Leonardo de Moura
93e5746739 chore(library/init/lean/parser/parser): naming consistency 2019-06-20 16:47:55 -07:00
Leonardo de Moura
98879f1580 refactor(library/init/lean/parser/parser): simplify SyntaxNodeKind 
The numeric `id` generation is works well for builtin parsers, but it
creates problems when defining dynamic ones.
 2019-06-20 14:51:59 -07:00
Leonardo de Moura
4ab31275a4 chore(library/init, frontends/lean): remove foldl and foldr notation, and implement list notation in the old parser 2019-06-20 14:32:08 -07:00
Leonardo de Moura
9e73d92e42 chore(library/init): remove instances of scoped notation 2019-06-20 14:08:35 -07:00
Leonardo de Moura
00aa2a3ffe chore(library/user_recursors): remove [recursor] attribute and environment extension 2019-06-20 11:25:53 -07:00
Leonardo de Moura
1e30f76511 chore(frontends/lean/pp): remove ppAsAnonymousCtor attribute 2019-06-20 11:03:20 -07:00
Leonardo de Moura
ac43b82668 chore(library/init): remove [derive] uses 
Trying to minimize the number of features we need to support in the new
frontend, and attributes we need to port to the new attribute manager.
 2019-06-20 10:53:15 -07:00
Leonardo de Moura
0b99a18f97 chore(library): use >> as notation for andthen 
We have other plans for `;`.
 2019-06-20 09:54:53 -07:00
Leonardo de Moura
8724a8cfd5 feat(library/init/lean/parser/parser): builtin parser attributes must be applied after compilation 2019-06-20 09:22:03 -07:00
Leonardo de Moura
e0ddacfd3e feat(library/init/lean/attributes,frontends/lean): allow attributes to specify when they should be applied 2019-06-20 09:17:03 -07:00
Leonardo de Moura
e86e6af049 feat(library/init/lean/attributes): add applicationTime field and remove unnecessary parameters 2019-06-20 08:48:26 -07:00