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

5744 commits

Author SHA1 Message Date
Leonardo de Moura
b27f215b9a chore(library/local_context): simplify pp 2019-08-06 10:27:10 -07:00
Leonardo de Moura
f1eaebba31 fix(library/compiler/csimp): bug at float_cases_on 
The scope of the expr2ctor cache updates was incorrect.
This bug affects code of the form
```
let x := C.cases_on y ...; K[x]
```
when we try to float the `cases_on` application, and the continuation
`K[x]` contains another `cases_on` application with major `y`.
The new test exposes the bug.
This commit also fixes the case where the continuation `K[x]` projects `y`.

Fixes #26
 2019-08-05 13:23:27 -07:00
Leonardo de Moura
99e90f0410 chore(library/compiler): add trace.compiler.simp_float_cases option 2019-08-05 13:13:18 -07:00
Leonardo de Moura
215a3ac8fd chore(library/tactic/clear_tactic): remove dead code 2019-08-05 08:58:59 -07:00
Leonardo de Moura
7f142ac7e3 chore(kernel/expr): hide get_weight and get_depth 2019-08-03 10:57:30 -07:00
Sebastian Ullrich
55104ad0c6 chore(library/compiler/csimp): remove wrong assertion 2019-07-30 17:52:43 -07:00
Sebastian Ullrich
d09c512784 chore(library/module): lsan: ignore module objects 2019-07-30 17:52:43 -07:00
Leonardo de Moura
fb14110b22 fix(library/compiler/llnf): sort scalar fields by size to avoid UB 2019-07-28 09:53:53 -07:00
Leonardo de Moura
ff6b868440 chore(library/module): remove dead code 2019-07-27 19:03:07 -07:00
Sebastian Ullrich
7b18bc94fd fix(library/module): make sure header length preserves alignment 2019-07-26 12:39:35 -07:00
Sebastian Ullrich
53a26b94ff chore(util/lean_path): remove leanpkg.path support 
Because Lean 4 will not compile dependencies by itself, there is not much of a
point in it resolving them by itself either. The build tool that ensures that
all dependencies have been built should call `lean` with the `LEAN_PATH`
environment variable set accordingly.
 2019-07-25 17:46:40 -07:00
Leonardo de Moura
cf8daf4b24 feat(library/init/lean/elaborator): process header 
TODO:
- improve/fix `setSearchPath`
- add `IO.getEnv`
- add support for relative imports at `absolutizeModuleName`
 2019-07-24 07:37:33 -07:00
Leonardo de Moura
022d22cac4 feat(library/compiler/extract_closed): fine grain extraction 
Motivation: increase reuse
 2019-07-10 11:14:20 -07:00
Leonardo de Moura
17cc34def5 feat(library/compiler/compiler): add option compiler.extract_closed 
It is useful when using `unsafeIO`
 2019-07-10 11:08:34 -07:00
Leonardo de Moura
85d151a335 feat(library/compiler): use eta expansion at eager_lambda_lifting 2019-07-09 16:34:20 -07:00
Leonardo de Moura
f1a2c83e8c feat(library/compiler/eager_lambda_lifting): do not pass closed terms as arguments to lifted decl 2019-07-09 14:06:14 -07:00
Leonardo de Moura
0f873b7ba2 fix(library/compiler/eager_lambda_lifting): collect type dependencies 2019-07-09 13:32:41 -07:00
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