Sebastian Ullrich
cbed0d232d
fix(frontends/lean/definition_cmds): collect implicit locals in both frontends
2019-01-17 18:55:43 +01:00
Leonardo de Moura
c268796545
fix(frontends/lean): clang errors and warnings
...
cc @kha
2019-01-15 13:48:08 -08:00
Sebastian Ullrich
93d8431d00
fix(frontends/lean/definition_cmds): fix build
2019-01-14 11:24:11 +01:00
Sebastian Ullrich
84e9dd9b1a
feat(library/init/lean/elaborator,frontends/lean/vm_elaborator): implement def/theorem/abbreviation
2019-01-12 15:10:00 +01:00
Leonardo de Moura
e0bb21ba0b
chore(library): remove noncomputable module
2018-10-22 09:39:03 -07:00
Leonardo de Moura
77e3c18cb0
feat(library/module): noncomputable keyword is now used only to disable code generation
...
We do not try to check whether code generation will succeed or not for
some declaration. In the future, we should probably rename it to
`nocode` or something similar.
cc @kha
2018-10-22 09:35:05 -07:00
Leonardo de Moura
5d726eb210
feat(library/compiler/compiler): switch to new compiler frontend
...
We also rename `vm_compiler` module to `emit_bytecode`.
We will eventually replace this module with the new IR emitter.
2018-10-08 17:38:17 -07:00
Leonardo de Moura
990fbe3c30
feat(library/compiler): provide options to vm_compile
2018-09-30 08:50:40 -07:00
Sebastian Ullrich
15d11cc483
feat(library/module_mgr): profile .olean serialization/deserialization
2018-09-20 13:54:17 -07:00
Sebastian Ullrich
af55cb13e7
fix(library/messages,library/init/lean/message): wrap message_log in structure, reverse in the end
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
38208802c6
refactor(*): replace log_tree with simple message_log list, make module_mgr synchronous
2018-09-11 13:55:25 -07:00
Leonardo de Moura
fabfe32ca5
chore(*): remove unnecessary scoped_ext dependencies
2018-09-08 15:42:48 -07:00
Leonardo de Moura
85465885f3
chore(library/type_context): remove "frozen local instances"
...
We will re-implement the type class resolution algorithm, and the new
implementation will not rely on a persistent cache. We will improve
performance by:
1) Using better indexing data-structures.
2) Using a local cache during the search.
2018-09-07 13:17:37 -07:00
Leonardo de Moura
2315bc4653
chore(library): remove documentation environment extension
2018-09-07 12:09:41 -07:00
Leonardo de Moura
58e91559d0
feat(*): use new inductive datatype module
2018-09-06 18:09:22 -07:00
Leonardo de Moura
78f4edaf57
chore(frontends/lean): remove info_manager and interactive modules
2018-09-04 17:22:16 -07:00
Leonardo de Moura
dd03747d22
chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies
2018-09-03 13:05:42 -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
Leonardo de Moura
776c977742
refactor(kernel): continue constant_info/declaration refactoring
2018-08-27 17:23:26 -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
88c8c560a9
chore(library/equations_compiler): do not generate equation lemmas
2018-08-23 14:04:37 -07:00
Leonardo de Moura
82095cc018
refactor(kernel): split declaration into declaration and constant_info
...
This is just another step towards the design described at commit 16598391a07d4a
2018-08-22 17:53:11 -07:00
Leonardo de Moura
f3e99286bb
chore(kernel): remove certified_declaration
2018-08-22 12:11:34 -07:00
Leonardo de Moura
ec1aa2553c
refactor(kernel/declaration): implement definition/constant/axiom/theorem using runtime/object
...
TODO: inductive, constructor, recursor
2018-06-25 10:05:45 -07:00
Leonardo de Moura
e9f843ddf6
refactor(kernel/expr): remove mlocal_* functions
...
The constructors `mvar` and `fvar` have different memory layouts.
2018-06-22 14:25:31 -07:00
Leonardo de Moura
ede1a51d60
refactor(kernel/declaration): remove self_opt flag from reducibility hints
...
This flag was used by the kernel to decide whether the following
heuristic should be used to avoid unfolding `f` at `is_def_eq`.
f a =?= f b
-----------
a =?= b
This heuristic was introduced at Lean1 after a discussion with
Georges Gontier. Since this discussion, we added support for
caching failures of this heuristic. This proved to be much more
effective to attack the performance problems.
Moreover, we do not even use this flag in the `type_context::is_def_eq`
used during elaboration.
The current codebase contains only one place where this flag was set to
`false`: coercions generated at structure_cmd. This change was
made at commit
1c70514231
2018-06-22 09:02:50 -07:00
Leonardo de Moura
01ea596aea
refactor(kernel/expr): implement expr using runtime/object
2018-06-21 16:05:33 -07:00
Leonardo de Moura
c5714c2fac
chore(kernel): remove expr.macro constructor
...
We are now ready to implement `expr` using `runtime/object`.
2018-06-19 17:54:43 -07:00
Leonardo de Moura
4c370e4558
refactor(kernel/expr): fix binder_info
2018-06-13 12:20:58 -07:00
Leonardo de Moura
a6250840d5
chore(kernel): rename some expr functions
2018-06-09 07:18:24 -07:00
Leonardo de Moura
818170d780
refactor(kernel): remove tag from kernel expressions
...
We are temporarily storing position information in a global table.
2018-06-08 10:29:22 -07:00
Leonardo de Moura
2a79da1ab6
refactor(kernel): move formatting stuff out of the kernel
2018-06-07 16:28:54 -07:00
Leonardo de Moura
e90585737f
refactor(*): use C++11 std::current_exception and std::rethrow_exception
...
With these new C++11 APIs, we can delete the `clone` and `rethrow`
methods from our exception classes.
2018-06-07 16:28:54 -07:00
Leonardo de Moura
c0e1d05199
chore(kernel): type_checker ==> old_type_checker
2018-06-06 16:10:40 -07:00
Leonardo de Moura
9a671d7c7d
chore(library/compiler): delete rec_fn_macro
2018-05-31 17:11:25 -07:00
Leonardo de Moura
3c1ccc9b74
refactor(kernel): use m_meta instead of m_trusted
2018-05-31 11:18:00 -07:00
Leonardo de Moura
12a03f7784
chore(frontends/lean/definition_cmds): remove dependency
2018-05-30 14:46:54 -07:00
Leonardo de Moura
1332fbabd6
feat(library,frontends): remove sorry macro
...
Lean4 will not have macros.
2018-05-24 14:00:30 -07:00
Leonardo de Moura
75c63ec921
refactor(*): list<name> ==> obj_list<name>
2018-05-23 15:48:43 -07:00
Leonardo de Moura
4af1f31877
feat(util, kernel): add obj_list wrapper for Lean list objects, and use it to implement list of universe levels
2018-05-23 14:48: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
Sebastian Ullrich
a7688a10b8
feat(frontends/lean/definition_cmds): elaborate a def's type separately when explicit return type is given
2018-04-20 09:59:09 -07:00
Leonardo de Moura
429edd7a5e
fix(frontends/lean/definition_cmds): fixes #1956
2018-04-11 16:48:04 -07:00
Leonardo de Moura
c08a3bc557
refactor(library/typed_expr): move typed_expr to frontends/lean
2018-04-09 15:25:40 -07:00
Leonardo de Moura
bdea7d420d
chore(*): type_context ==> type_context_old
2018-03-05 12:38:24 -08:00
Leonardo de Moura
7762dc381a
feat(library/type_context): use context_cache interface
2018-02-21 15:04:20 -08:00
Sebastian Ullrich
f247363305
feat(library/time_task): print cumulative times on --profile
2018-02-19 09:13:24 -08:00
Sebastian Ullrich
2f2540dc3b
fix(frontends/lean/definition_cmds): hide kernel exceptions triggered by error recovery
...
They are never helpful compared to the original error
2018-02-02 08:58:52 -08:00
Sebastian Ullrich
c600bca747
feat(frontends/lean/definition_cmds): hide scary kernel exception on duplicate declaration
2018-02-02 08:58:52 -08:00
Leonardo de Moura
0c5c1a27c6
refactor(frontends/lean, library/equations_compiler): move smart unfolding auxiliary function generation to equations_compiler module
2018-01-09 16:27:36 -08:00
