Leonardo de Moura
fb00f9a780
fix(runtime/object): missing free
2018-05-22 16:50:07 -07:00
Leonardo de Moura
b2f3d3f456
chore(*): remove redundant code
2018-05-22 16:46:04 -07:00
Leonardo de Moura
5b17a30203
feat(runtime): add object serializer
...
Any type implemented on top of `object` gets the serializer/deserializer for free
2018-05-22 16:34:41 -07:00
Leonardo de Moura
67b59a0a3c
fix(util): memory leaks
2018-05-22 11:05:51 -07:00
Leonardo de Moura
914e702356
chore(kernel/level): remove unnecessary friend annotation
2018-05-22 09:46:17 -07:00
Leonardo de Moura
eb54a4f551
chore(kernel/cache_stack): compilation warning
2018-05-22 09:46:00 -07:00
Leonardo de Moura
160b7e8847
refactor(library/init/meta/expr): local_const will have only one field
...
In Lean3, we supported two kinds of local constant:
context-less (inherited from Lean2) and context-based (type,
binder-info and pretty printing name are stored in the context).
The context-less was used in the kernel and a few modules we kept when
we moved from Lean2 to Lean3. Even if we keep the hybrind
representation, we should not expose the context-less to users.
2018-05-21 15:36:09 -07:00
Leonardo de Moura
92ff42776c
chore(library/tactic): remove match_tactic
2018-05-20 17:33:31 -07:00
Leonardo de Moura
abf9d8fe37
fix(runtime/object): assertion violation
2018-05-20 13:51:31 -07:00
Leonardo de Moura
df26e10609
fix(util): assertion violations
2018-05-20 13:42:22 -07:00
Leonardo de Moura
ce29de1b49
chore(util): style
2018-05-20 13:26:59 -07:00
Leonardo de Moura
256a1f720c
refactor(util/name): implement name using object
2018-05-20 13:22:34 -07:00
Leonardo de Moura
4de9b8c177
chore(library/vm): rename constants
2018-05-20 12:30:15 -07:00
Leonardo de Moura
b78e9df869
chore(runtime/object): tag => obj_tag
...
`tag` at `object.h` conflicts with `tag` at `expr.h`
2018-05-20 12:00:59 -07:00
Leonardo de Moura
dd6e56f3bf
feat(util/object_ref): add smart pointer for object
2018-05-20 11:46:53 -07:00
Leonardo de Moura
2944f7a027
chore(runtime): lean_obj.* ==> object.*
2018-05-20 10:17:15 -07:00
Leonardo de Moura
2d604e7d25
chore(runtime/lean_obj): remove lean_ prefix
2018-05-20 10:13:44 -07:00
Leonardo de Moura
e081f9ad78
chore(runtime/lean_obj): cleanup
2018-05-20 10:02:19 -07:00
Leonardo de Moura
d92679f969
refactor(*): replace name with lean.name
2018-05-20 09:42:44 -07:00
Leonardo de Moura
a52b418452
refactor(*): mk sure old name has same shape of new lean.name type
2018-05-20 08:48:48 -07:00
Leonardo de Moura
fde4e15cb4
fix(runtime/lean_obj): OSX issue
2018-05-20 08:18:03 -07:00
Sebastian Ullrich
3a2fbe2d2f
fix(util/init_module): segfault using clang
2018-05-20 11:01:37 +02:00
Leonardo de Moura
2ebf8ab8f1
chore(*): unnecessary #includes
2018-05-18 13:19:22 -07:00
Leonardo de Moura
1bc7c0812c
chore(kernel,library): remove task from the kernel and library
2018-05-18 09:06:03 -07:00
Leonardo de Moura
acdcbdb71e
feat(library/init/lean/ir): add instructions for (big) integer arithmetic
2018-05-17 18:17:23 -07:00
Leonardo de Moura
dfc5adbd2a
feat(runtime/lean_obj): add integer primitives
2018-05-17 17:47:22 -07:00
Leonardo de Moura
0aadb27327
perf(runtime/lean_obj): improve nat comparison
2018-05-17 17:41:03 -07:00
Leonardo de Moura
b4fb4385a2
fix(runtime/lean_obj): test
2018-05-17 17:14:24 -07:00
Leonardo de Moura
5d8501acf5
chore(runtime/lean_obj): consistent naming convention
2018-05-17 16:45:27 -07:00
Leonardo de Moura
a4583e23ea
chore(gen/apply): fix bogus style warning
2018-05-17 16:09:20 -07:00
Leonardo de Moura
dede61b122
feat(library/init/lean/ir): add tag and tag_ref instructions
2018-05-17 14:51:41 -07:00
Leonardo de Moura
74b7ae0734
fix(runtime/apply): the trick to avoid alloca is not thread safe
2018-05-17 13:34:00 -07:00
Leonardo de Moura
aadb5a8481
chore(runtime/lean_obj): missing primitives
2018-05-17 13:11:47 -07:00
Leonardo de Moura
5d53eccb59
feat(runtime): string support
2018-05-17 13:11:47 -07:00
Sebastian Ullrich
696ba77b53
feat(frontends/lean/elaborator): anonymous constructor notation for ginductives
2018-05-17 14:14:00 +02:00
Leonardo de Moura
53d459911f
refactor(library/init/lean/ir): RC instructions
2018-05-16 10:28:51 -07:00
Leonardo de Moura
8cb7511a91
feat(runtime/lean_obj): natural number support
2018-05-16 10:28:51 -07:00
Leonardo de Moura
3708a22484
feat(runtime/lean_obj): add lean_dbg_print_num
2018-05-15 11:57:53 -07:00
Leonardo de Moura
b1d8a17f1b
fix(runtime): add init_module
2018-05-14 20:38:21 -07:00
Leonardo de Moura
168e7fa0cd
chore(runtime/lean_obj): style
2018-05-14 17:27:25 -07:00
Leonardo de Moura
8ee2f4fea1
feat(*): basic runtime string support
2018-05-14 16:52:55 -07:00
Leonardo de Moura
aa1006d01b
feat(library/init/lean/ir/extract_cpp): generate libleanruntime.a
2018-05-14 14:34:10 -07:00
Leonardo de Moura
0556412f8d
refactor(*): add runtime folder
...
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
2018-05-14 14:23:56 -07:00
Leonardo de Moura
095d100a38
chore(util/debug): remove logtree dependency
2018-05-14 11:09:07 -07:00
Leonardo de Moura
4fa1022388
fix(gen/apply): emit #pragma once
2018-05-14 11:08:45 -07:00
Leonardo de Moura
914f6907dc
chore(util/lean_obj): remove unnecessary includes
2018-05-14 11:08:16 -07:00
Leonardo de Moura
1ab4c9f8bf
feat(gen/apply): simplify over-application case and avoid quadratic blowup
...
The over-application doesn't occur very often in practice.
The new version adds an extra "copy" step, but it avoids the quadratic
blowup in code size.
Xavier Leroy reports that only 5% of all calls are over-applications
in his experiments.
In Lean3, 6.59% of all calls performed to compile corelib are "over",
and we did not implement any fancy optimization.
2018-05-12 15:10:26 -07:00
Leonardo de Moura
d02c36df18
chore(gen/apply): style
2018-05-11 18:01:58 -07:00
Leonardo de Moura
1d69493b83
feat(gen/apply): add generator for apply
...
It generates the functions at `util/apply.h` that are used by
the Lean runtime.
2018-05-11 17:54:09 -07:00
Leonardo de Moura
60c8ff2472
feat(util/lean_obj): add some missing primitives
2018-05-09 17:43:40 -07:00
