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

5727 commits

Author SHA1 Message Date
Leonardo de Moura
557dd16864 chore(library,frontends/lean): remove old attribute manager 2019-06-27 14:01:34 -07:00
Leonardo de Moura
4e444a283d feat(library/class): switch to Lean implementation 2019-06-27 13:51:09 -07:00
Leonardo de Moura
8399e41a5b feat(library/class): simpler get_class function 
It does not depend on `type_context.h`, and we will used it as a
template to implement the Lean version.
 2019-06-27 10:42:14 -07:00
Leonardo de Moura
6727c1fa68 feat(library/compiler/specialize): switch to specExtension in Lean 2019-06-27 10:08:39 -07:00
Leonardo de Moura
3c0caee73b chore(library/compiler/specialize): cleanup 
Preparing to implement environment extension in Lean.
 2019-06-27 09:32:25 -07:00
Leonardo de Moura
bd58525080 chore(library/class): simplify 2019-06-26 16:51:36 -07:00
Leonardo de Moura
14f05d2001 feat(library/init/lean/compiler): register [implementedBy] attribute using new attribute manager 2019-06-26 15:55:51 -07:00
Leonardo de Moura
1f53c4fd33 feat(library/init/lean/eqncompiler): register [matchPattern] attribute using new attribute manager 2019-06-26 15:38:14 -07:00
Leonardo de Moura
14d77f8204 feat(library/compiler/specialize): use new attribute manager 2019-06-26 15:09:14 -07:00
Leonardo de Moura
34ca44cca1 chore(frontends/lean,library): remove unnecessary #includes and dead code 2019-06-26 11:36:23 -07:00
Leonardo de Moura
e00dc873a8 chore(library/pattern_attribute): [pattern] ==> [matchPattern] 2019-06-26 11:26:49 -07:00
Leonardo de Moura
7e60c6063e chore(library/compiler): remove dead code 2019-06-26 11:08:23 -07:00
Leonardo de Moura
16d423dab6 feat(frontends/lean): switch to [extern] implemented in Lean 
This commit also changes how we represent attribute parameters as
Syntax objects.
 2019-06-26 10:57:33 -07:00
Leonardo de Moura
ff07ec70f4 core(library/projection): switch to Lean implementation 2019-06-26 08:12:06 -07:00
Leonardo de Moura
8a1e2bf79b chore(library/projection): preparing to port projection_info to Lean 2019-06-25 13:17:59 -07:00
Leonardo de Moura
5148497e8c feat(library/init/lean/compiler/externattr): add mkExternAttr skeleton 2019-06-25 13:16:11 -07:00
Leonardo de Moura
8206ef0dab feat(library/reducible): use new Lean implementation 2019-06-24 15:48:12 -07:00
Leonardo de Moura
061e13eaea chore(library/reducible): remove dead code 2019-06-24 15:48:12 -07:00
Leonardo de Moura
45dc2cd49a feat(library/init/lean/compiler): [export] attribute in Lean 2019-06-24 15:48:12 -07:00
Leonardo de Moura
da09ef4f66 feat(frontends/lean/builtin_exprs): minor improvement 2019-06-24 15:48:11 -07:00
Leonardo de Moura
24e3bff429 feat(frontends/lean): add simple parser! macro 2019-06-24 15:48:11 -07:00
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