Sebastian Ullrich
188ab30a9c
fix(library/init/lean/parser/declaration): precedence for attribute arguments
2018-10-30 17:43:05 +01:00
Sebastian Ullrich
8a3e7821d7
fix(frontends/lean/elaborator): weaken assertion
...
There are still some cases like errors in nested equations that leak
metavariables, but as long as we report at least one error, that probably isn't
a high-priority issue.
2018-10-30 17:43:05 +01:00
Leonardo de Moura
bcc4956ca5
feat(library/compiler/llnf): reuse constructor memory cells
...
This commit also add two new instructions to the old VM: `updt` and
`updt_cidx`.
They allow us to test the new new memory reuse technique.
TODO: We need to reset fields after we project. Otherwise, we prevent
destructive updates on nested objects.
2018-10-29 18:46:26 -07:00
Leonardo de Moura
998293b8ca
feat(library/compiler/llnf): eliminate cases term where all reachable branches are equal
2018-10-29 14:57:37 -07:00
Leonardo de Moura
91b59a2f12
fix(library/compiler/extract_closed): do not extract is_enf_unreachable
2018-10-29 14:41:12 -07:00
Leonardo de Moura
c076ac8e1a
feat(library/compiler/llnf): remove identity cases terms
...
Example: a term such as
```
decidable.cases_on t _cnstr.0.0 _cnstr.1.0
```
is replaced with `t`
2018-10-29 14:29:03 -07:00
Leonardo de Moura
c3d700ece1
feat(library/compiler/csimp): nat.succ x ==> x + 1
2018-10-29 13:53:59 -07:00
Leonardo de Moura
ecf30e93a3
chore(library/vm): remove Destruct instruction
2018-10-29 13:18:33 -07:00
Leonardo de Moura
91022dd62e
chore(library/compiler/llnf): style
2018-10-29 13:10:23 -07:00
Leonardo de Moura
d871c4f7d8
feat(library/compiler): replace simp_inductive with llnf
2018-10-29 13:07:46 -07:00
Leonardo de Moura
ca1e2d3d1d
fix(library/compiler/llnf): typo and missing case
2018-10-29 13:05:09 -07:00
Leonardo de Moura
6fe50bd298
fix(library/compiler/llnf): missing mk_let
2018-10-29 11:48:14 -07:00
Leonardo de Moura
28c21b4340
fix(library/compiler/csimp): make sure constants (of arity 0) marked with [inline] or [inline_if_reduce] are inlined
2018-10-29 11:46:56 -07:00
Leonardo de Moura
388b4ea6ac
feat(library/compiler/llnf): basic llnf module with support for unboxed types
...
TODO: support for reusing memory cells
2018-10-29 11:02:04 -07:00
Leonardo de Moura
28a34e798a
feat(library/compiler/csimp): projection to field
...
The new test demonstrations this transformation.
2018-10-28 09:38:45 -07:00
Leonardo de Moura
a368ed2185
test(tests/util/object): add map test
2018-10-27 20:50:09 -07:00
Leonardo de Moura
6607720b5f
feat(library/compiler/llnf): store offset and size for scalar fields
2018-10-27 17:27:53 -07:00
Leonardo de Moura
7a3fb4d32a
feat(library/compiler/llnf): add updt_cidx
2018-10-27 17:16:09 -07:00
Leonardo de Moura
7dcc12ba6f
feat(library/compiler/util): add is_runtime_builtin_cnstr
2018-10-27 17:09:12 -07:00
Leonardo de Moura
74b92cd419
feat(library/compiler/llnf): collect constructor info
2018-10-27 16:58:51 -07:00
Leonardo de Moura
a161eec8f2
feat(library/compiler): add llnf (low level normal form) skeleton
2018-10-27 12:36:30 -07:00
Leonardo de Moura
cc3767e6a5
refactor(library/init/data): avoid indirection at rbmap
...
Now, the nodes in a `rbmap` contain the key and value, and we avoid
one level of indirection. `rbmap`s are more common than `rbtree`.
We implement `rbtree A` as `rbmap A unit`.
2018-10-26 17:14:09 -07:00
Leonardo de Moura
571be8616a
refactor(library/compiler/erase_irrelevant): postpone simplification
...
Remove transformations such as
```
prod.cases_on M (\fun a b, t)
```
==>
```
let a := M.0 in
let b := M.1 in
t
```
We will perform this kind of transformation in a later stage.
2018-10-26 15:59:04 -07:00
Leonardo de Moura
76ba67a290
chore(library/compiler/simp_inductive): remove dead code
2018-10-26 15:02:34 -07:00
Leonardo de Moura
76b6188a3e
chore(library/compiler/emit_bytecode): remove useless instruction
...
The VM based debugger was never used in practice.
2018-10-26 14:23:15 -07:00
Leonardo de Moura
f336dde4ef
chore(library/compiler/simp_inductive): don't need type_checker::state
2018-10-26 14:16:06 -07:00
Leonardo de Moura
7d2a507824
fix(library/compiler/csimp): bug at move_to_entries
2018-10-25 17:07:31 -07:00
Leonardo de Moura
7ec00c97e9
feat(library/compiler/csimp): float all cases
...
Motivation: explicit control flow graph
TODO: disabled `split_entries` for now.
I believe the new feature exposed a bug at `move_to_entries`.
I will fix this new issue in another commit.
2018-10-25 15:41:11 -07:00
Leonardo de Moura
4ba3cc390f
fix(library/compiler/specialize): assertion violation lean_assert(!has_fvar(code));
...
We were getting assertion violations when compiling corelib in debug
mode. There were two problems:
1- We were not capturing free variables occurring in types.
2- A paremeter could depend on a free variable associated with a let-declaration.
2018-10-25 13:23:43 -07:00
Leonardo de Moura
8175dab1a6
chore(library/compiler/csimp): remove leftover assertion used yesterday when debugging code
2018-10-25 12:55:25 -07:00
Leonardo de Moura
b18135a4c8
feat(library/compiler/csimp): cheap float cases
2018-10-25 11:15:21 -07:00
Leonardo de Moura
96ef30e827
chore(library/init/lean/parser/parsec): remove private
...
Motivation: allow us to change the attribute in other files
2018-10-25 10:55:32 -07:00
Leonardo de Moura
370f67b27b
feat(library/init/lean/parser/parsec): mark *_mk_res functions as [inline_if_reduce]
2018-10-25 10:10:54 -07:00
Leonardo de Moura
628b0c7919
feat(library/compiler): add [inline_if_reduce] attribute
2018-10-25 10:01:26 -07:00
Leonardo de Moura
a1798a2c24
feat(library/compiler/csimp): new joint point placement and preservation algorithm
2018-10-24 16:46:16 -07: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
5eaed3a21a
chore(library/compiler/csimp): make sure local_ctx is monotonically increasing
...
We need this feature to implement the new join point management system
for csimp.
2018-10-24 08:55:00 -07:00
Leonardo de Moura
70746b499e
chore(library/vm): remove BuiltinCases and NatCases instructions
...
They are not needed anymore.
2018-10-23 15:09:55 -07:00
Leonardo de Moura
3ee863da68
feat(library/compiler/erase_irrelevant): eliminate cases_on for builtin types
2018-10-23 14:58:38 -07:00
Leonardo de Moura
cbbae4b331
chore(library/vm): remove vm_platform and vm_pos_info
2018-10-23 12:55:34 -07:00
Leonardo de Moura
392f019184
chore(tests/lean/parsec1): fix test
2018-10-23 12:54:29 -07:00
Leonardo de Moura
de1dc3be88
chore(library/vm): remove vm_array
...
We are currently not using arrays in the old VM.
2018-10-23 12:49:25 -07:00
Leonardo de Moura
9256618d67
chore(library/vm): remove vm_name
2018-10-23 11:32:56 -07:00
Leonardo de Moura
243b6a70e1
chore(library/vm): remove vm_options
2018-10-23 11:32:56 -07:00
Leonardo de Moura
f7f981285b
chore(tests/lean/run/display_hw_term_hack_deps): remove old test
2018-10-23 11:32:56 -07:00
Leonardo de Moura
9d32aff0c6
chore(library/init/meta): remove rest of old meta folder
2018-10-23 11:32:56 -07:00
Leonardo de Moura
8d47d2a026
chore(library/vm,library/init/meta): remove vm_format, and some obsolete meta objects
2018-10-23 11:32:56 -07:00
Leonardo de Moura
65815c512c
chore(library/vm): remove interaction_state
2018-10-23 11:32:56 -07:00
Leonardo de Moura
4cb6b1f9d5
chore(library/tactic): reduce dependencies
2018-10-23 11:32:56 -07:00
Leonardo de Moura
d07f115f21
chore(library/compiler/util): fix style
2018-10-23 11:32:56 -07:00
