Leonardo de Moura
f1fe5c8d8b
test(tests/playground/termparsertest1): new tests
2019-07-05 12:10:22 -07:00
Leonardo de Moura
e946f79e82
test(tests/playground/termparsertest1): add new tests
2019-07-05 10:46:37 -07:00
Leonardo de Moura
0bee94886e
feat(frontends/lean/builtin_exprs): , from ==> from, and cleanup suffices
2019-07-02 17:22:50 -07:00
Leonardo de Moura
9f24e77200
chore(library/init/lean/parser/term): add show and have parsers
2019-07-02 16:59:43 -07:00
Leonardo de Moura
44730314ff
feat(library/init/lean/parser/term): add ifTerm
2019-07-02 16:32:09 -07:00
Leonardo de Moura
d4a5306d82
feat(library/init/lean/parser/term): explicit universe notation in the new parser
2019-07-02 09:00:58 -07:00
Leonardo de Moura
9d50b3ca47
feat(library/init/lean/parser/term): paren parser
2019-07-01 19:44:13 -07:00
Leonardo de Moura
13b5747713
fix(library/init/lean/parser/parser): prattParser
2019-07-01 16:00:58 -07:00
Leonardo de Moura
531ef5d700
feat(library/init/lean/parser): universe level parser and bug fixes
2019-06-30 09:02:06 -07:00
Leonardo de Moura
da09ef4f66
feat(frontends/lean/builtin_exprs): minor improvement
2019-06-24 15:48:11 -07:00
Leonardo de Moura
24e3bff429
feat(frontends/lean): add simple parser! macro
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
7f3543096a
test(tests/playground/parser2): proof of concept
2019-06-20 16:48:17 -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
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
f180b3f32e
feat(library/init/lean/parser/parser): improve error messages on prattParser
2019-06-19 16:36:18 -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
86e1af2066
test(tests/playground/parser1): minor
2019-06-19 14:17:55 -07:00
Leonardo de Moura
5ccbb1ec1c
test(tests/playground/parser1): add first test
...
We use `attribute [testParser] ...` instead of `@[testParser]` as a
workaround for the issue described at 697f69020f
2019-06-19 10:52:22 -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
ff86159297
test(tests/playground/eval): proof of concept for a safe eval function
2019-06-06 17:06:32 -07:00
Leonardo de Moura
e90a79f996
chore(tests/playground/parser/syntax): fix test
2019-06-05 14:19:24 -07:00
Leonardo de Moura
30a6a2ade8
feat(library/init/data, runtime): remove parray support from runtime, and implement them in Lean using Scala/Clojure Radix trees
...
The Scala/Clojure approach for persistent arrays works great with our
`reset/reuse`. We seem to be much more efficient than their
implementations because of `reset/reuse`. The new approach also seems
better than the old one implemented in the runtime, and has a few
advantages:
1- The reroot procedure used in the old approach required
synchronization for multi-threaded code, or we would need to perform
deep copies when sending `parray` objects between threads.
2- We don't need any runtime extension for the new approach.
3- The old approach used "trail lists" for undoing array updates.
This works well for bactracking search use cases, but it is bad
in use cases where we are simultaneously updating the persistent
arrays that have shared nodes.
2019-06-02 09:18:19 -07:00
Leonardo de Moura
9d00a8d262
feat(tests/playground/radixtree): use bit shift and land instead instead of / and %
2019-06-01 11:06:45 -07:00
Leonardo de Moura
336761d787
feat(tests/playground/radixtree): add stats
2019-06-01 09:47:57 -07:00
Leonardo de Moura
e87c471e7f
test(tests/playground/radixtree): Scala/Clojure inspired persistent arrays
...
@kha It is a pity we didn't use this example in our paper. It works
really well with `reset`/`reuse`.
2019-05-31 21:55:57 -07:00
Leonardo de Moura
30fefdb188
chore(tests/playground): add zipper
2019-05-29 14:33:47 -07:00
Leonardo de Moura
0009435add
chore(tests/playground/lazylist): fix test
2019-05-29 14:33:47 -07:00
Sebastian Ullrich
9b9465d299
chore(tests/bench): move out from playground/
2019-05-29 16:33:50 +02:00
Sebastian Ullrich
d082a7e42f
fix(tests/playground/Makefile): fix rbmap_shared input size
2019-05-29 15:03:44 +02:00
Sebastian Ullrich
1ad692eb77
chore(tests/playground/Makefile): retire unionfind1
2019-05-29 14:58:58 +02:00
Sebastian Ullrich
423b087782
chore(tests/playground/Makefile): build *.tex by default
2019-05-29 10:08:39 +02:00
Sebastian Ullrich
adc462789a
chore(tests/playground/Makefile): output tables after benchmarking
2019-05-29 10:08:39 +02:00
Sebastian Ullrich
9e22ae1f12
chore(tests/playground): update temci
2019-05-29 09:59:53 +02:00
Sebastian Ullrich
bebbb8413e
chore(tests/playground/Makefile): benchmark scaling
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
f25669666b
chore(tests/playground/temci): update temci
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
ff16feb661
chore(tests/playground): fix frontend benchmark
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
0644835a7b
chore(tests/playground/Makefile): disable broken benchmark
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
8114e88639
fix(tests/playground/bench): build 2 stages
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
d15cc74c13
chore(tests/playground/temci): update temci settings
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
af85733a6d
chore(tests/playground/temci): update temci
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
609c27c31f
fix(tests/playground/Makefile): create correct .cpp files when called directly
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
fff2899176
feat(tests/playground/Makefile): add TEMCI_FLAGS
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
e50b2040b6
feat(tests/playground/Makefile): more output polishing
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
90430e9696
chore(tests/playground): delete intermediate files
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
c1ba216bcc
feat(tests/playground): Lean variant benchmarks
2019-05-28 19:12:45 +02:00
Sebastian Ullrich
5302a40763
feat(tests/playground): MLKit GC%
2019-05-28 19:12:45 +02:00
Leonardo de Moura
ccf400506a
test(tests/playground/rbmap_checkpoint2): modified length
2019-05-28 08:21:38 -07:00
