Sebastian Ullrich
ae70158c09
fix(frontends/lean/elaborator): position information for callees
2018-09-02 18:08:41 -07:00
Sebastian Ullrich
39cdae50ee
feat(library,frontends/lean): use mdata instead of hacky cache for position information in preterms
2018-09-02 18:08:41 -07:00
Sebastian Ullrich
0220af69b8
feat(library/print): print mdata
...
Not sure if helpful or annoying for the future...
2018-09-02 18:08:41 -07:00
Leonardo de Moura
f9d87e7a98
feat(kernel/inductive): add inductive postprocessor
...
We still need to restore recursors and their rules
2018-09-02 17:44:19 -07:00
Leonardo de Moura
41a87f6856
feat(kernel/inductive): normalize parameter names
2018-09-02 16:40:31 -07:00
Leonardo de Moura
7d4097818b
feat(kernel/inductive): add recursor rules
2018-09-02 15:55:29 -07:00
Leonardo de Moura
f30cb0635f
chore(kernel/inductive): cleanup
2018-09-02 09:26:58 -07:00
Leonardo de Moura
98f035088c
chore(kernel/inductive): cleanup
2018-08-31 18:01:26 -07:00
Leonardo de Moura
517923d362
feat(kernel/inductive): generate recursors in the new inductive datatype module
2018-08-31 17:47:22 -07:00
Leonardo de Moura
2fb677f1d0
feat(kernel/inductive): add positivity check to new inductive datatype module
2018-08-31 09:52:38 -07:00
Leonardo de Moura
706d7045c3
feat(kernel/inductive): add nested => mutual preprocessor
2018-08-30 18:05:43 -07:00
Leonardo de Moura
f1105e108a
fix(kernel/inductive): bug at check_inductive_types
2018-08-30 18:05:43 -07:00
Sebastian Ullrich
93d13ffea3
chore(library/init/lean): lean.parser.reader ~> lean.parser
2018-08-30 16:34:47 -07:00
Sebastian Ullrich
2528aee72b
refactor(library/init/lean/parser/reader): use different monad stacks for different parts of the reader
2018-08-29 16:42:24 -07:00
Sebastian Ullrich
3bdc0db397
feat(library/derive_attribute): allow implicit parameters in class signature
2018-08-29 16:42:24 -07:00
Sebastian Ullrich
f4a9798f9b
fix(library/derive_attribute): avoid segfault on sorry input
2018-08-29 16:42:24 -07:00
Leonardo de Moura
b79794e601
feat(frontends/lean/print_cmd): add basic support for testing new inductive datatype module
2018-08-29 09:36:47 -07:00
Leonardo de Moura
863355c6a0
feat(kernel/inductive): continue new inductive datatype module
...
Add more validation, and create new inductive_val and constant_val objects.
2018-08-29 09:27:06 -07:00
Leonardo de Moura
f765eec626
fix(kernel/type_checker): typo in error message
2018-08-29 09:21:35 -07:00
Leonardo de Moura
d1d56776ad
feat(kernel): invoke add_inductive for inductive datatype declarations
2018-08-28 15:54:46 -07:00
Leonardo de Moura
101886ffae
feat(kernel): proper constant_info and declaration objects for quot type
2018-08-28 13:46:31 -07:00
Sebastian Ullrich
46f734b1b1
refactor(library/init/lean/parser/reader): replace macro with syntax_node_kind
...
Also make sure that the name inside a node kind is the full name of the
declaration. This way, we cannot have accidentally conflicting node kind names.
2018-08-28 13:13:14 -07:00
Leonardo de Moura
3770df2a48
fix(runtime/apply): must use free_heap_obj instead of free
2018-08-28 12:29:14 -07:00
Leonardo de Moura
5c3678482f
chore(runtime/object): cleanup
2018-08-28 12:29:04 -07:00
Leonardo de Moura
3e528a9b67
chore(runtime): fix assertions
2018-08-28 10:33:22 -07:00
Leonardo de Moura
4d6da3dd69
fix(runtime/compact): bug at read
2018-08-28 10:30:51 -07:00
Leonardo de Moura
161431e995
feat(kernel): implement new mutual_definition declaration object
...
This commit also removes the old `environment::add_meta` hackish method.
2018-08-28 10:30:44 -07:00
Leonardo de Moura
cdb2824d86
fix(library/module): debug build
2018-08-28 08:09:57 -07:00
Leonardo de Moura
b63b05e5fd
fix(runtime/thread): MULTI_THREAD=OFF build
2018-08-28 08:08:55 -07:00
Leonardo de Moura
030669ea4d
feat(runtime): do not waste space with RC for region and stack allocated objects
...
The modification introduces an overhead of 1.5% on the
execution time. Here is the the time for compiling the corelib
Before: 8.61 secs (avg of 3 runs)
After: 8.74 secs (avg of 3 runs)
On the other hand, the size of the compacted region for the command
`#compact_tst 10` is smaller.
Before: 176687728
After: 153794704
The size before this change was 14.8% bigger.
For reference, using the old serializer we generate a buffer of size 105291117.
cc @kha
2018-08-28 07:41:55 -07:00
Leonardo de Moura
805e45bba5
chore(tests/shell): fix test
2018-08-27 17:54:43 -07:00
Leonardo de Moura
776c977742
refactor(kernel): continue constant_info/declaration refactoring
2018-08-27 17:23:26 -07:00
Leonardo de Moura
96ff6b1718
feat(util/object_ref): add helper functions
2018-08-27 16:28:37 -07:00
Leonardo de Moura
ae18cee0ea
chore(library/module): remove pos_info tracking
...
We will use a completely different approach in Lean4
2018-08-27 15:55:57 -07:00
Leonardo de Moura
2ab2265d22
chore(library/module): remove dead APIs
2018-08-27 15:40:20 -07:00
Leonardo de Moura
dec166b387
chore(library/module): remove dead info
2018-08-27 15:35:10 -07:00
Leonardo de Moura
d27a360912
chore(library/update_declaration): remove dead file
2018-08-27 15:18:23 -07:00
Leonardo de Moura
27ef29a50f
refactor(kernel/declaration): continue constant_info/declaration refactoring
2018-08-27 13:22:10 -07:00
Leonardo de Moura
7bf032d6fe
chore(frontends/lean): remove calc-expression
2018-08-27 12:20:54 -07:00
Leonardo de Moura
4917ab0c65
chore(library): remove congr_lemma
2018-08-23 16:48:43 -07:00
Leonardo de Moura
e0f7fa3bd9
chore(library/tactic): remove leftovers
2018-08-23 16:00:34 -07:00
Leonardo de Moura
d334bb1fa7
chore(*): remove more stuff
2018-08-23 15:56:31 -07:00
Leonardo de Moura
17ae59b5b0
chore(*): remove more stuff
2018-08-23 15:27:12 -07:00
Leonardo de Moura
c21555240a
chore(library/tactic): remove more stuff
2018-08-23 15:20:07 -07:00
Leonardo de Moura
5f65b3a6f1
chore(library/tactic): remove unused bindings
2018-08-23 15:04:23 -07:00
Leonardo de Moura
e2b912237d
chore(library/native_compiler): remove leftovers
2018-08-23 14:58:57 -07:00
Leonardo de Moura
a7f6d1d38d
chore(library/tactic): remove tactic/eval.cpp and tactic/gexpr.cpp
2018-08-23 14:54:41 -07:00
Leonardo de Moura
22101a2c55
chore(library/tactic): remove assert_tactic and change_tactic
2018-08-23 14:50:55 -07:00
Leonardo de Moura
05a6d8a791
chore(library/tactic): remove destruct_tactic, generalize_tactic and fun_info_tactics
2018-08-23 14:47:51 -07:00
Leonardo de Moura
ed5d884d8f
chore(library/tactic): remove app_builder_tactics
2018-08-23 14:22:00 -07:00
