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
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
335c58f8a7
feat(kernel): add expr_kind::Quote
...
This is a temporary expr constructor. We need it to be able to eliminate
expr_macro, and then define expr using runtime/object
2018-06-12 17:40:00 -07:00
Leonardo de Moura
2d7b6ed12c
chore(library/compiler): remove copy_tag from old compiler
2018-06-07 16:28:54 -07:00
Leonardo de Moura
bdea7d420d
chore(*): type_context ==> type_context_old
2018-03-05 12:38:24 -08:00
Leonardo de Moura
ada4932507
feat(library/compiler): add new cache support to compiler
2018-02-21 15:04:20 -08:00
Leonardo de Moura
7762dc381a
feat(library/type_context): use context_cache interface
2018-02-21 15:04:20 -08:00
Sebastian Ullrich
283d8ade1a
fix(library/quote): use opaque macro for elaborated expr quotations
2017-06-07 10:00:17 -07:00
Sebastian Ullrich
8c0394b294
refactor(library,frontends/lean): separate expr and pexpr macros
2017-05-09 16:02:41 -07:00
Leonardo de Moura
d6000416f8
feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information
...
We will use this information in the debugger.
2016-11-09 16:51:48 -08:00
Leonardo de Moura
0ec22bb2cf
refactor(library/type_context): new type class instance cache
2016-09-01 17:37:30 -07:00
Leonardo de Moura
2b43f591c9
fix(library/type_context): remove m_cache_owner field
...
This idiom creates problem if we use (even accidentally) the copy constructor.
2016-06-23 14:03:46 -07:00
Leonardo de Moura
de9df69ef6
refactor(src): move compiler folder to library
2016-05-09 13:28:00 -07:00
