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

881 commits

Author SHA1 Message Date
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
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
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
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
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
Leonardo de Moura
739008f8d4 chore(library/init/lean/compiler/llnf): disable 
I am going to refactor the interface with the new IR compiler.
 2019-05-15 19:02:51 -07:00
Leonardo de Moura
9b3421b63b feat(library/compiler/closed_term_cache): remove C++ implementation and use Lean one 2019-05-15 15:33:46 -07:00
Leonardo de Moura
edeae776da chore(library/module): module::add for declarations is not needed anymore 2019-05-14 11:23:35 -07:00
Leonardo de Moura
3b3e50d315 chore(library/module): std::shared_ptr<modification> ==> modification* 
Remark: this commit introduce memory leaks, but this is just an
intermediate step to get modification objects in Lean.
Recall that, we will eventually remove modification objects from Lean.
 2019-05-13 15:05:21 -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
f1d16c261d fix(library/compiler/csimp): do not inline constants with [init] attribute 2019-05-11 17:51:46 -07:00
Leonardo de Moura
fd2a5dd45e feat(library/init/io): add IO.initializing 2019-05-10 11:26:49 -07:00
Leonardo de Moura
f6b3bc868a fix(library/init/lean/environment, library/compiler): compilation error and add [implementedBy] attribute 2019-05-10 07:22:56 -07:00
Leonardo de Moura
fd487d8db7 chore(*): remove old VM 2019-05-08 15:15:44 -07:00
Leonardo de Moura
74fb8e627a feat(library/init/lean/compiler/ir/checker): improve IR checker 2019-05-08 05:47:25 -07:00
Leonardo de Moura
b41d7ec98b chore(library/compiler/ir): style 2019-05-07 15:20:56 -07:00
Leonardo de Moura
2363fdf544 refactor(library/init/lean/compiler/ir): remove redundant field from FnBody.jdecl 
The result type of a join point is always equal to the function return
type. Moreover, the extra bookkeeping introduces extra work, and doesn't
really help.
 2019-05-07 12:26:11 -07:00
Leonardo de Moura
0d1a0c8b6e chore(library): toBool ==> decide 
We want to define a type class similar to Haskell's `ToBool`.
 2019-05-06 14:02:15 -07:00
Leonardo de Moura
04670c4127 fix(library/compiler/struct_cases_on): bug and missing case 2019-05-03 20:03:03 -07:00
Leonardo de Moura
9b50e9d003 feat(library/compiler/find_jp): locate (and preserve) join points created by user 2019-05-02 17:20:19 -07:00
Leonardo de Moura
76a49ec256 chore(library/compiler): add ir::test 2019-05-02 14:40:04 -07:00