Leonardo de Moura
92466272ed
fix(library/init/lean/compiler/ir/emitcpp): incorrectly emitting unicode characters in the range [128, 255]
...
For example, "·" was being stored as `\xb7` which is not the valid UTF8.
2019-07-02 15:56:32 -07:00
Leonardo de Moura
5691450b5b
feat(library/init/lean/parser): term parser skeleton
2019-07-01 15:04:13 -07:00
Leonardo de Moura
7049f4a889
feat(library/init/lean/class): register attributes and export functions
2019-06-27 13:27:13 -07:00
Leonardo de Moura
235b4c02c1
feat(library/init/lean/compiler/specialize): implement specExtension in Lean
2019-06-27 09:58:19 -07:00
Leonardo de Moura
4bc0346c17
chore(library/init/lean/compiler): specializeattrs.lean ==> specialize.lean
2019-06-27 09:38:21 -07:00
Leonardo de Moura
cf6f6bc96d
chore(stage0): update
2019-06-27 09:30:53 -07:00
Leonardo de Moura
9037595ead
chore(stage0): update
2019-06-26 19:09:20 -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
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
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
1972f9a426
fix(stage0): missing files
2019-06-25 11:23:34 -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
d870b8af85
chore(stage0): update
2019-06-25 09:18:38 -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
00ad43fcfe
chore(stage0): update
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
4c8420406d
chore(stage0): update
2019-06-24 15:48:11 -07:00
Leonardo de Moura
b225112234
chore(stage0): update
2019-06-24 15:48:11 -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
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
8ad653ae2d
chore(stage0): update
2019-06-20 09:55:55 -07:00
Leonardo de Moura
db325cb924
fix(stag0): missing file
2019-06-20 09:23:41 -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
766467d095
fix(stage0): missing files
2019-06-18 18:35:18 -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
Leonardo de Moura
0dfca42f6d
chore(library/init/lean/compiler/initattr): remove unnecessary @[export]
2019-06-18 16:15:48 -07:00
Leonardo de Moura
9da080d398
feat(library/compiler/init_attribute): switch to @[init] attribute in Lean
2019-06-18 16:03:52 -07:00
Leonardo de Moura
36aa33091b
chore(stage0): update
2019-06-07 17:16:36 -07:00
Leonardo de Moura
f176a7963c
feat(library/init/lean/compiler/ir/emitcpp): register arity 0 declarations
2019-06-07 17:15:16 -07:00
Leonardo de Moura
3651dc7618
feat(library/init/lean): add evalConst
...
The implementation is good enough for implementing extensible parsers,
elaborators and tactics, but there are a few TODOs
1- We should have a better story for standalone applications.
Most of them don't need `evalConst`, and the global table is
just initialization overhead.
2- The global table introduces a dependency on the `Lean.Name`
implementation. So, all standalone applications will depend on it.
3- We are not storing arity 0 constants in the table.
This one should be easy to fix in the future.
2019-06-07 16:31:28 -07:00
Leonardo de Moura
c3a7cc4617
feat(library/init/lean/compiler/ir/emitcpp): register functions
2019-06-07 15:34:55 -07:00
Leonardo de Moura
373011bc20
chore(library/init/lean/format): export group
2019-06-07 10:35:04 -07:00
Leonardo de Moura
452485a706
chore(library/init/lean/format): export functions
2019-06-07 10:10:13 -07:00
Leonardo de Moura
b292fc13cc
chore(library/init/lean/compiler/inline): export typo
2019-06-06 15:28:20 -07:00
Leonardo de Moura
e4063f5eec
chore(stage0): update
2019-06-06 15:20:13 -07:00
Leonardo de Moura
57e250a768
chore(stage0): remove leftover
2019-06-06 15:09:41 -07:00
Leonardo de Moura
9b457cc77c
feat(library/init/lean/compiler/inline): implement tester functions and export them
2019-06-06 15:07:08 -07:00
Leonardo de Moura
72290483e4
chore(library/init/lean/compiler): attributes.lean ==> inline.lean
2019-06-06 14:08:13 -07:00
Leonardo de Moura
e05cdc2b08
feat(library/init/lean/compiler): declare function inlining attributes in Lean
...
Remark: they are not active yet since we haven't removed the ones
defined in C++ yet.
2019-06-06 11:05:54 -07:00
Leonardo de Moura
c8a972c57b
fix(library/init/lean/attributes): typos at @[export]
2019-06-06 10:41:17 -07:00
Leonardo de Moura
fb77d71d23
feat(library/init/lean/attributes): export attribute API
2019-06-05 16:55:47 -07:00
Leonardo de Moura
d212abb9ee
feat(library/init/lean/syntax): export helper functions for creating syntax in C++
2019-06-05 16:49:58 -07:00
