Leonardo de Moura
08cdb757b4
feat(library/init/lean/environment): add Environment.addAndCompile
...
To fix `BuiltinParserAttribute`, we need to be able to add auxiliary declarations programmatically.
2019-06-18 18:20:17 -07:00
Leonardo de Moura
d664486eca
chore(util): move format to src/util
2019-06-07 10:58:23 -07:00
Leonardo de Moura
3afa4f7ab0
chore(util/safe_arith): remove dead code
2019-06-07 09:52:31 -07:00
Leonardo de Moura
fd29b7e45d
feat(util/io): add helper functions for consuming IO results in C++
2019-06-05 13:53:38 -07:00
Leonardo de Moura
4a26f0028c
chore(library/init/lean/environment): remove unnecessary function
2019-06-03 15:17:40 -07:00
Leonardo de Moura
cd73105dff
refactor(kernel/environment,library/private,library/init/lean/environment): move main module name to header
2019-06-03 09:14:23 -07:00
Leonardo de Moura
aa138fe686
chore(*): get_obj_arg => to_obj_arg
2019-05-16 14:42:02 -07:00
Leonardo de Moura
9d9f546ad8
refactor(util/sexpr): move options and option_declarations to util
2019-05-16 14:37:24 -07:00
Leonardo de Moura
816e83970b
refactor(util/object_ref, kernel/environment): move to_optional
2019-05-15 15:16:29 -07:00
Leonardo de Moura
3193e91aff
feat(library/init/lean/environment): add Environment.displayStats and --stats command line argument
2019-05-15 11:01:25 -07:00
Leonardo de Moura
bc809643ec
feat(library/init/lean/expr): add Expr.quickLt, Expr.eqv
2019-05-15 11:01:25 -07:00
Leonardo de Moura
99e3cdc01b
chore(frontends/lean): delete lean_environment
2019-05-13 13:05:04 -07:00
Leonardo de Moura
edb4d76ecd
feat(kernel/environment): environment as a Lean object
2019-05-13 12:41:33 -07:00
Leonardo de Moura
8ca1b7b2cb
chore(kernel/environment): dead code
2019-05-11 14:13:40 -07:00
Leonardo de Moura
06727e9ca4
chore(kernel/environment): remove dead code
2019-05-10 16:37:13 -07:00
Leonardo de Moura
0d5ac5288a
feat(runtime): increase small nat size
...
In 64-bit machines, the max small nat value should now be (2^63 - 1), and on 32-bit
machines (2^32 - 1).
The main motivation for this modification are the array indexing
operations. With the new representation, if a Nat index is not small,
then it must not be a valid index. This was not true in 64-bit
machines. Example: an array of size 2^33 would fit in memory, and but
an index `i` > 2^32 - 1 would not be a small nat value.
2019-03-26 14:21:03 -07:00
Leonardo de Moura
ac27bd092b
chore(*): small fixes
2019-03-21 15:06:44 -07:00
Leonardo de Moura
e0b0ca4830
chore(*): adapt C++ code to camelCase
2019-03-21 15:06:43 -07:00
Leonardo de Moura
5f54b5887b
chore(kernel/declaration): fix compilation warnings
2019-03-19 11:25:55 -07:00
Leonardo de Moura
aa56578a29
fix(library/compiler/compiler): assertion violations
2019-03-19 11:25:55 -07:00
Leonardo de Moura
20ba4c4b04
feat(kernel): opaque constants
...
They are very similar to `theorems`, but they are never ever unfolded.
2019-03-15 15:45:06 -07:00
Leonardo de Moura
0888dee25e
chore(*): meta ==> unsafe
2019-03-15 15:04:40 -07:00
Leonardo de Moura
d3ba9ef7fa
feat(library/compiler/csimp): eliminate join points that are used only once
2019-03-14 10:43:35 -07:00
Leonardo de Moura
818f2f2d4a
chore(kernel): remove old #include
2019-03-06 06:56:16 -08:00
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
