Leonardo de Moura
feea8ecccd
feat(library/compiler/llnf): avoid inc/dec operations on persistent objects
...
inc/dec operations are noop's for persistent objects.
2019-02-18 20:22:18 -08:00
Leonardo de Moura
ab45af5936
fix(library/compiler/csimp): avoid potential expensive reduction at csimp
...
`whnf_core(e)` uses `whnf` to reduce the major premise of recursors and
projections, and `whnf` unfolds arbitrary definitions.
This commit adds a new option (`cheap`) to `whnf_core`. When
`whnf_core(e, true)` is used, the type checker will not unfolding
definitions when reducing the major premises.
2019-02-15 17:43:21 -08:00
Sebastian Ullrich
a6ac98966a
refactor(library/attribute_manager): parse attribute data from pexpr instead of abstract_parser
2019-02-15 12:13:45 -08:00
Sebastian Ullrich
7cffe6935e
feat(frontends/lean/vm_elaborator): port to new runtime
2019-02-14 14:07:05 -08:00
Leonardo de Moura
9cb2005e8e
feat(library/init/lean): add hash functions and dbg_to_string
2019-02-13 16:19:25 -08:00
Leonardo de Moura
811a480d77
feat(kernel/expr): low level API for expr
2019-02-13 14:59:18 -08:00
Leonardo de Moura
71f5290567
feat(kernel): expose level primitives
2019-02-13 10:37:13 -08:00
Leonardo de Moura
4627929a83
refactor(boot,runtime,util): move name runtime implementation to util/name, and use "extern C" ABI
2019-02-13 08:27:23 -08:00
Leonardo de Moura
b3f0ce5355
fix(kernel/runtime): use extern "C"
2019-02-13 08:04:47 -08:00
Leonardo de Moura
19b6a5d0d1
chore(kernel): builtin => runtime
...
We don't need builtin.h anymore
2019-02-13 07:56:14 -08:00
Leonardo de Moura
f20c132ced
feat(library/init/lean/elaborator): use extern attribute
2019-02-12 11:40:21 -08:00
Leonardo de Moura
bc4e06666b
chore(*): avoid 0-ary extern declarations
2019-02-11 13:21:17 -08:00
Leonardo de Moura
bd38fc530f
refactor(kernel/level): low level API for level
2019-02-07 15:04:12 -08:00
Sebastian Ullrich
25ffbdda57
chore(src/*): fix style
2019-02-07 15:41:12 +01:00
Leonardo de Moura
3444a295e7
feat(library/compiler,runtime): builtin support for lean.name
2019-02-05 12:57:46 -08:00
Leonardo de Moura
c097f1c1e0
fix(kernel/builtin): add extern
2019-02-01 17:58:55 -08:00
Leonardo de Moura
ac53080ced
fix(kernel/builtin): incorrect signature
2019-02-01 15:06:57 -08:00
Leonardo de Moura
4fa06e38b2
chore(*): add skeleton for new builtin primitives, update src/boot
2019-02-01 14:03:03 -08:00
Leonardo de Moura
9e7d1d5bd2
chore(kernel/expr): remove leftover
2018-11-09 11:55:02 -08:00
Leonardo de Moura
43ceb6bfbe
refactor(kernel/local_ctx): simplify local_ctx
...
Remark: we still need to revise the classes: `type_context` and `local_context`.
2018-10-24 10:02:38 -07:00
Leonardo de Moura
83abbcb9a6
fix(library/compiler/erase_irrelevant): preserve builtin runtime types
...
`uint32` is a definition, and `type_checker::whnf` unfolds it.
To preserve the information at `erase_irrelevant`, we use a custom
`whnf_type` method that stops reduction as soon as a builtin runtime
type is found.
2018-10-22 13:58:08 -07:00
Leonardo de Moura
db647139a2
feat(kernel): use cheap_beta_reduce at infer_lambda too
2018-10-20 17:28:45 -07:00
Leonardo de Moura
0b38547e97
feat(kernel): move cheap_beta_reduce to kernel and use it at infer_let
2018-10-20 17:13:41 -07:00
Leonardo de Moura
a40c526e48
feat(library/compiler/csimp): add basic constant folding for nat operations
2018-10-17 08:38:30 -07:00
Leonardo de Moura
611f6ae780
feat(library/compiler/specialize): code specialization
...
TODO:
- Cache results at `specialize_ext`
- Cleanup
It is not feasible to run code specializer without cache: code explosion.
2018-10-16 15:50:42 -07:00
Leonardo de Moura
8837217a2e
chore(kernel/expr): dead decls
2018-10-15 11:10:11 -07:00
Leonardo de Moura
c74f4c16ca
feat(library/kernel,library/compiler/csimp): make sure nat.rec and nat.cases_on reduce when major premise is a nat literal
2018-10-10 18:35:15 -07:00
Leonardo de Moura
9f161e6968
fix(library,kernel): the new proj_sname field must be taken into account during comparisons
...
`proj_sname` is not just for enabling better pretty printing. It is
necessary in the compiler when type information is lost, and we can't
infer the type of a `proj`-term argument (field `proj_expr`).
2018-10-03 13:11:46 -07:00
Leonardo de Moura
c3569dc72d
feat(kernel): store structure name in proj-expressions
2018-10-02 09:23:11 -07:00
Leonardo de Moura
2c4139d5e5
feat(library/compiler): eta expand quot primitives, add support for eq.rec_on
2018-09-30 08:24:18 -07:00
Leonardo de Moura
751cdd7c42
feat(kernel/type_checker): avoid unnecessary lambdas
2018-09-29 17:24:49 -07:00
Leonardo de Moura
6e9e9c0012
feat(library/compiler): eta expand definitions
2018-09-23 19:27:06 -07:00
Leonardo de Moura
1534f17a89
feat(library/compiler/lcnf): add better support for complete-transition used in the equation compiler and x@ patterns
2018-09-20 21:38:57 -07:00
Leonardo de Moura
9b29572604
feat(kernel/type_checker): improve infer_let
...
Before this commit, given a term `let x : t := v in b`, `infer_type`
would return `let x : t := v in T` where `T` is the type of `b` in
the local context extended with declaration `x : t := v`.
This is correct, but it produces unnecessarily large terms
in the new compiler stack which makes a heavy use of let-expressions.
We noticed the problem when the size of some .olean files were 100x
bigger. For example, `repr.olean` increased from 136Kb to
13Mb after we started saving the `._cstage1` (code after after
simplification) in the `.olean` files.
The new implementation relies on the fact that `T` seldom depends on
`x`. So, in most cases, the result is just `T` instead of `let x : t := v in T`
After this change, the new .olean files are at most 56% bigger than
.olean files not containing `._cstate1` code. This seems reasonable
since most of our .olean files only contain code and we are storing a
copy of each function.
@kha The new lcnf format keeps exposing problems :)
2018-09-17 18:25:27 -07:00
Leonardo de Moura
f0e24e73f4
feat(kernel/expr): missing constructor
2018-09-16 14:30:43 -07:00
Leonardo de Moura
59652e885a
fix(kernel/type_checker): whnf_fvar
2018-09-16 13:49:35 -07:00
Leonardo de Moura
000db32e40
chore(kernel/type_checker): remove dead branch
2018-09-16 12:22:28 -07:00
Leonardo de Moura
4874e25715
feat(kernel): save constructor idx and nfields at constructor_val
2018-09-14 13:45:58 -07:00
Sebastian Ullrich
647f40763c
feat(library/message_builder): pretty-print kernel_exceptions
2018-09-13 16:38:40 -07:00
Leonardo de Moura
b8dceda9b7
chore(kernel): type_checker::context ==> type_checker::state
2018-09-13 14:06:57 -07:00
Leonardo de Moura
20f31c85bf
chore(kernel/type_checker): we don't use the kernel type checker for elaboration anymore
2018-09-12 20:36:32 -07:00
Leonardo de Moura
c49ad19736
refactor(kernel/type_checker): type_checker::cache ==> type_checker::context
...
We also move `environment` and `name_generator` to
`type_checker::context`. Reason: the cache assumes the environment did
not change. The (cache) correctness relies on the fact that we don't
reuse free variable identifiers.
2018-09-12 20:34:30 -07:00
Leonardo de Moura
d814ee612a
chore(kernel/local_ctx): typo
2018-09-11 18:10:10 -07:00
Sebastian Ullrich
904d7c4a88
chore(*): remove old task API and task queues
2018-09-11 13:55:25 -07:00
Leonardo de Moura
4863ca071a
chore(runtime): make sure we use the same naming convention for getters and setters
2018-09-09 10:07:00 -07:00
Leonardo de Moura
03a99986bb
feat(kernel): implement local_decl using runtime
2018-09-08 16:25:43 -07:00
Leonardo de Moura
3b07eeec47
fix(kernel/inductive): name generator was not being consistenly used
2018-09-08 16:21:33 -07:00
Leonardo de Moura
5503bd113b
chore(kernel/type_checker): assume m_cache != nullptr will continue to hold in future versions
2018-09-08 09:13:08 -07:00
Leonardo de Moura
7479d6e55b
refactor(kernel/type_checker): allow type_checker::cache to be reused
2018-09-08 08:43:19 -07:00
Leonardo de Moura
dacc4c9cd6
chore(kernel): move abstract_type_context to library
2018-09-08 08:29:51 -07:00
