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

928 commits

Author SHA1 Message Date
Sebastian Ullrich
2d04ecc704 refactor(util/object_ref): move and adjust cnstr_get_ref_t 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
3ee59aa17f feat(library/compiler/ir_interpreter): add Windows support 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
1732461a66 doc(library/compiler/ir_interpreter): add a few comments 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
d27cbe2dc5 perf(library/compiler/ir_interpreter): cache symbol lookup 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
2d4276e819 feat(library/compiler/ir_interpreter): tail recursion 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
bdb7152768 feat(library/compiler/ir_interpreter): cache constants 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
9015fc1e34 chore(library/compiler/ir_interpreter): add step-level trace 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
558d9ad837 feat(library/compiler/ir_interpreter): add call-level trace 2019-09-12 18:22:02 +02:00
Sebastian Ullrich
795359ee49 feat(shell/lean): re-add --run flag 2019-09-12 18:22:02 +02:00
Sebastian Ullrich
99bc069fdd feat(library/compiler/ir_interpreter): implement IR interpreter 2019-09-12 18:22:02 +02:00
Leonardo de Moura
8e47b6396f chore(library/init/lean/compiler/ir): simplify mkCase, the xType field is set by explicitBoxing 2019-09-12 08:55:09 -07:00
Leonardo de Moura
0284d4a7a2 chore(library/compiler/ir): use new mkCase 2019-09-12 08:23:29 -07:00
Leonardo de Moura
3e6736b374 feat(library/compiler/util): add support for trivial structures at mk_runtime_type 2019-09-11 13:41:41 -07:00
Leonardo de Moura
1062dcbbea refactor(src/library/compiler/erase_irrelevant): move has_trivial_structure to util 2019-09-11 13:04:08 -07:00
Leonardo de Moura
f7af9a73bd chore(library/init/lean/compiler/ir): move addBoxedVersion to entry point file 2019-09-09 10:35:52 -07:00
Leonardo de Moura
a188bb8497 chore(library/init/lean/compiler/ir): remove emitcpp 2019-09-07 19:46:22 -07:00
Leonardo de Moura
6d6cb14f9e feat(library/init/lean/compiler/ir/emitc,shell/lean): add --c=<filename> option 2019-08-20 10:13:40 -07:00
Leonardo de Moura
66304d83a0 chore(library/init/lean/compiler): export as C functions 2019-08-17 06:58:36 -07:00
Leonardo de Moura
4429aac0b3 chore(library/compiler/ir): remove box(13) hack 2019-08-16 20:58:30 -07:00
Leonardo de Moura
ec0e74f5f8 chore(library/init/lean): export as C functions 2019-08-16 20:52:10 -07:00
Leonardo de Moura
dae30a4ea6 chore(library/compiler/specialize): remove broken assertions 2019-08-16 09:46:05 -07:00
Leonardo de Moura
61beb56a83 chore(*): fix some compilation warnings 2019-08-15 09:26:13 -07:00
Leonardo de Moura
bf2a365501 chore(library/compiler/compiler): remove dead code 2019-08-07 17:24:07 -07:00
Leonardo de Moura
73f96730bb feat(library/init/lean,kernel): add KernelException, addDecl and compileDecl 
This commit also refines the type of `addAndCompile`.
We also add `ElabException.kernel` constructor for kernel exceptions.
 2019-08-07 17:15:40 -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
Sebastian Ullrich
55104ad0c6 chore(library/compiler/csimp): remove wrong assertion 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
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
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
14f05d2001 feat(library/init/lean/compiler): register [implementedBy] attribute using new attribute manager 2019-06-26 15:55:51 -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
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
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
45dc2cd49a feat(library/init/lean/compiler): [export] attribute in Lean 2019-06-24 15:48:12 -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
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