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
Leonardo de Moura
d7fb0aa908
feat(library/init/lean/parser/parser): simpler cache
...
cc @kha
2019-06-19 16:48:18 -07:00
Leonardo de Moura
f180b3f32e
feat(library/init/lean/parser/parser): improve error messages on prattParser
2019-06-19 16:36:18 -07:00
Leonardo de Moura
4db487fb42
fix(library/init/lean/parser/parser): sepBy1
2019-06-19 16:34:49 -07:00
Leonardo de Moura
cf9a29152d
fix(library/init/lean/parser/parser): ParserInfo for ident, strLit, and numLit
2019-06-19 16:19:00 -07:00
Leonardo de Moura
401de35b6c
chore(library/init/lean/parser/parser): remove unnecessary import
...
It turns out we don't need evalConst for implementing `builtinParsers`.
2019-06-19 10:53:51 -07:00
Leonardo de Moura
5f014415a9
feat(library/init/lean/parser/parser): add helper functions for invoking builting parsers
...
TODO: add scoped attributes for dynamically extending parsers.
2019-06-19 10:48:19 -07:00
Leonardo de Moura
89dae7f877
fix(library/init/lean/parser/parser): missing result
2019-06-19 10:33:53 -07:00
Leonardo de Moura
451ab72eea
fix(library/init/lean/attributes): typo
2019-06-19 10:21:40 -07:00
Leonardo de Moura
a55251618a
fix(library/init/lean): missing file
2019-06-19 09:53:34 -07:00
Leonardo de Moura
697f69020f
fix(library/init/lean/parser/parser): new registerBuiltinParserAttribute
...
It is still broken since we apply attributes before we compile code.
Recall that attributes such as `@[export]` and `@[extern]` must be applied before we
compile code.
On the other hand, any attribute `attrName`
```
@[attrName] def foo := ...
```
which creates auxiliary definitions that depend on `foo` must be applied
AFTER we generate code for `foo`. Otherwise, we will fail to compile the
auxiliary definition since we don't have code for `foo` yet.
I will fix the issue above by allowing attributes to specify when they
should be applied. I will start with only two options: before and after
code compilation. In the future, we may need more options (e.g., before
elaboration), but I don't see the need yet.
cc @kha
2019-06-19 09:52:56 -07:00
Leonardo de Moura
08cdb757b4
feat(library/init/lean/environment): add Environment.addAndCompile
...
To fix `BuiltinParserAttribute`, we need to be able to add auxiliary declarations programmatically.
2019-06-18 18:20:17 -07:00
