max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
16786 commits 1 branch 0 tags 5.3 GiB
Commit graph

5706 commits

Author SHA1 Message Date
Leonardo de Moura
00aa2a3ffe chore(library/user_recursors): remove [recursor] attribute and environment extension 2019-06-20 11:25:53 -07:00
Leonardo de Moura
6b5408b69c chore(library/derive_attribute): remove derive_attribute 
We will reimplement it in Lean after we have the new frontend working.
 2019-06-20 10:55:53 -07:00
Leonardo de Moura
b502f178c2 chore(library/compiler/reduce_arity): fix typo 2019-06-19 09:53:00 -07:00
Leonardo de Moura
697f69020f fix(library/init/lean/parser/parser): new registerBuiltinParserAttribute 
It is still broken since we apply attributes before we compile code.

Recall that attributes such as `@[export]` and `@[extern]` must be applied before we
compile code.

On the other hand, any attribute `attrName`
```
@[attrName] def foo := ...
```
which creates auxiliary definitions that depend on `foo` must be applied
AFTER we generate code for `foo`. Otherwise, we will fail to compile the
auxiliary definition since we don't have code for `foo` yet.

I will fix the issue above by allowing attributes to specify when they
should be applied. I will start with only two options: before and after
code compilation. In the future, we may need more options (e.g., before
elaboration), but I don't see the need yet.

cc @kha
 2019-06-19 09:52:56 -07:00
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
66e3f68dbc chore(library/compiler/procedure): remove dead code 2019-06-18 17:29:19 -07:00
Leonardo de Moura
9da080d398 feat(library/compiler/init_attribute): switch to @[init] attribute in Lean 2019-06-18 16:03:52 -07:00
Leonardo de Moura
d664486eca chore(util): move format to src/util 2019-06-07 10:58:23 -07:00
Leonardo de Moura
f6b9a0fe9c chore(util/sexpr/format): preparing to switch to Lean implementation 2019-06-07 09:46:34 -07:00
Leonardo de Moura
0553d60dbf feat(library/compiler/util): switch to new attributes implemented in Lean 2019-06-06 15:40:39 -07:00
Leonardo de Moura
8f9b73399b feat(library/compiler/eager_lambda_lifting): implement using Lean version 2019-06-06 15:09:57 -07:00
Leonardo de Moura
e081332ef8 feat(library/scoped_ext): switch to new scope manager implemented in Lean 
We still invoke the old `scoped_ext`s implemented in C++.
 2019-06-05 14:12:27 -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
1cdadba4b2 fix(library/compiler/csimp): type error 
@kha This is another instance of a problem we discussed last summer.
I guess there are many more instances like this one that we are not handling.
Recall that we want to preserve types at `csimp` because we eventually
want to allow users to use equational theorems as rewriting rules during
compilation.
However, some of the transformations that `csimp` perform do not
preserve typeability in CIC.
Moreover, some of the optimizations require type inference.

I see the possible long term solutions:

1- Erase types and proofs as soon as possible. The main drawback here is
that we would have to develop an approach for translating Lean theorems
into valid rewriting rules for lambda pure. For example, the following
theorem should not be used as a rewriting rule after we erase types.
```
forall (xs : List Unit) (f : Unit -> Unit), List.map f xs = List.map id xs
```
BTW, I don't want to abandon the idea of using lemmas as rewriting rules in
the compiler.

2- Go over `csimp` and other compiler steps and make sure they work
properly even when `type_checker::infer_type` fails.
 2019-06-03 17:36:40 -07:00
Leonardo de Moura
ffbccf1ee9 fix(library/compiler): ByteArray bug 2019-06-03 15:01:16 -07:00
Leonardo de Moura
9310c807e6 feat(library/private): use environment extension in Lean 
Remark: we don't need the `m_inv_map` anymore.
 2019-06-03 11:50:33 -07:00
Leonardo de Moura
377b1ca042 chore(library/private): cleanup 2019-06-03 09:38:10 -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
b86d9422b6 chore(library/compiler/borrowed_annotation): remove old borrow inference code 2019-05-27 21:28:22 -07:00
Leonardo de Moura
f67bc39ce4 chore(library/compiler/llnf): remove old IR compiler 2019-05-27 21:28:22 -07:00
Leonardo de Moura
51a9208ea9 chore(library/compiler): remove environment extension: llnf_code 
We don't need it anymore. It was used by the old IR compiler
 2019-05-27 21:28:22 -07:00
Leonardo de Moura
356a4fafcd chore(library/compiler): remove old code 
@kha I am removing the old IR compiler. If there is a disaster with
the new one implemented in Lean, I will put it back.
 2019-05-27 21:28:22 -07:00
Leonardo de Moura
fc0ce5b97e chore(library/aliases, frontends/lean): remove local_ref's 
We don't need them since we removed parameters
 2019-05-27 21:28:22 -07:00
Leonardo de Moura
9aa40e2491 chore(library/aliases): remove dead code 2019-05-27 21:28:22 -07:00
Leonardo de Moura
8c6ae127c9 chore(library/scoped_ext): remove dead code 2019-05-27 21:28:22 -07:00
Leonardo de Moura
0f43c2e2d9 feat(library/init/data/array/basic): efficient heterogeneous Array.map 
This commit also removes Array.hmap.
Motivation: I wanted to use Array.hmap as an example in the paper, but
I found it would be too distracting to explain why we had `Array.hmap`
and `Array.map`.

cc @kha
 2019-05-25 16:32:59 -07:00
Leonardo de Moura
bf3575a316 feat(library/init/lean/compiler/ir): improve expandresetreuse 2019-05-23 17:23:50 -07:00
Leonardo de Moura
f9f4e6c14b feat(library/init/lean/compiler/ir): add expandresetreuse 2019-05-23 08:58:16 -07:00
Leonardo de Moura
6bed0ca5b5 chore(library/compiler): style 2019-05-22 18:46:37 -07:00
Leonardo de Moura
4d2837430a fix(library/compiler/emit_cpp): tail call 
Add temporary hack to fix `emit_tail_call`.
TODO: find a cleaner solution for the new IR compiler.
 2019-05-21 23:07:10 -07:00
Leonardo de Moura
f1fbe5cd61 feat(library/compiler/ir): add boxed version for extern constants 2019-05-21 17:55:58 -07:00
Leonardo de Moura
5b3aec088e feat(library/init/lean/compiler/ir/emitcpp): emit module initialization code 2019-05-21 16:06:10 -07:00
Leonardo de Moura
9f604ee0a1 fix(library/compiler/extern_attribute): register @[extern] projections in the new IR compiler 2019-05-21 13:42:42 -07:00
Leonardo de Moura
3b5093ebe0 fix(library/compiler/ir): fix ret irrelevant 2019-05-21 13:32:11 -07:00
Leonardo de Moura
63d2c03403 fix(library/compiler/ir): lambda IR translator 2019-05-21 13:01:43 -07:00
Leonardo de Moura
dbe2bebc06 fix(library/compiler/extern_attribute): register extern constructors in the new IR compiler 2019-05-21 08:09:05 -07:00
Leonardo de Moura
4ed803c564 feat(library/init/lean/compiler/ir/emitcpp): emit skeletons 2019-05-20 19:08:21 -07:00
Leonardo de Moura
f852cd774f feat(library/init/lean/compiler/ir): expose C++ primitives for accessing export and extern attributes 2019-05-20 15:49:03 -07:00
Leonardo de Moura
3ffe0e22c8 feat(shel/lean): add temporary option for testing new IR compiler code emitter 2019-05-20 10:19:09 -07:00
Leonardo de Moura
c0b3c71c4d chore(library/compiler): remove dead code 2019-05-20 08:13:52 -07:00
Leonardo de Moura
83692eef6d feat(library/init/lean/compiler/ir): explicit RC 2019-05-19 16:46:51 -07:00
Leonardo de Moura
300c251b49 feat(library/init/lean/compiler/ir): add explicitBoxing to new IR compiler stack 2019-05-19 08:10:45 -07:00
Leonardo de Moura
b0c6d1c6a7 fix(library/compiler/ir): assertion violation 2019-05-18 11:33:35 -07:00
Leonardo de Moura
ca818e6850 feat(library/init/lean/compiler/ir): add borrow inference 2019-05-18 10:48:26 -07:00
Leonardo de Moura
c9bcd4990c feat(library/compiler): register extern constants into the new IR 2019-05-17 17:12:51 -07:00
Leonardo de Moura
9a3a01fa6e feat(library/compiler/compiler): invoke new IR compiler implemented in Lean 2019-05-16 16:08:52 -07:00
Leonardo de Moura
9d7191feca chore(library/compiler): remove support for fully boxed 2019-05-16 15:48:33 -07:00
Leonardo de Moura
ac69f802e1 feat(library/compiler): interface with new IR compiler entry point 2019-05-16 15:41:47 -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