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

577 commits

Author SHA1 Message Date
Leonardo de Moura
5bed81078a feat(library/compiler/emit_cpp): generate function skeletons 2019-01-25 14:26:32 -08:00
Leonardo de Moura
b36b4f0d80 feat(library/compiler/emit_cpp): emit function headers 2019-01-25 14:26:32 -08:00
Leonardo de Moura
2016e1bce5 feat(library/compiler/llnf): unique names for lambda arguments 2019-01-25 14:26:32 -08:00
Leonardo de Moura
4b66b442c9 chore(library/compiler/emit_cpp): just store a list of decls 2019-01-25 14:26:32 -08:00
Leonardo de Moura
bb9e7aceb3 feat(library/compiler/emit_cpp): add environment extension for emit_cpp 2019-01-24 16:04:31 -08:00
Leonardo de Moura
70bb89b213 feat(library/compiler): add [cppname] attribute 2019-01-24 14:40:12 -08:00
Leonardo de Moura
eace1bacb3 refactor(library/compiler): move name mangling procedures to separate file 
We will need them to implement the LLVM IR backend.
 2019-01-24 13:57:13 -08:00
Leonardo de Moura
f5f6a7f85e feat(library/compiler/emit_cpp): take module name and (direct) dependencies as arguments 2019-01-23 16:34:04 -08:00
Leonardo de Moura
02849a3cf6 feat(library/compiler/emit_cpp): add name mangling functions 2019-01-23 14:46:04 -08:00
Leonardo de Moura
8bcc965dc0 feat(library/compiler): make sure we emit bytecode and C++ 2019-01-23 14:13:04 -08:00
Leonardo de Moura
320917cca5 feat(library/compiler): add emit_cpp skeleton 2019-01-23 14:01:43 -08:00
Leonardo de Moura
afd30d73c1 chore(library/compiler/compiler): generate Lean IR with explicit boxing and RC instructions 
This is just for testing. These two steps are not used by `emit_bytecode`,
but they will be used to generate C++ code.
We can now compile the whole corelib in debug mode with these two extra
transformation without any assertion violation.
 2019-01-18 16:01:47 -08:00
Leonardo de Moura
fe68547086 fix(library/compiler/llnf): missing instruction _uproj at explicit_rc_fn 2019-01-18 16:00:08 -08:00
Leonardo de Moura
1293d976f7 fix(library/compiler/util): usize case was missing at to_uint_type 2019-01-18 15:50:14 -08:00
Leonardo de Moura
a001806996 feat(library/compiler/compiler): generate boxed version of builtin constants 2019-01-18 15:43:06 -08:00
Leonardo de Moura
aaf1966a87 fix(library/compiler/llnf): explicit boxing should treat variables with function type (e.g., _obj -> _obj) as _obj 2019-01-18 15:07:01 -08:00
Leonardo de Moura
9ea7b77fe0 fix(library/compiler/llnf): typo 2019-01-17 17:10:52 -08:00
Leonardo de Moura
1d0d17d4ae fix(library/compiler/llnf): bug at explicit boxing transformation 2019-01-17 16:58:22 -08:00
Leonardo de Moura
1b59fed1d9 fix(library/compiler/llnf): bug at x := _proj y 
We must increment `x`'s RC before (if needed) we decrement `y`'s RC
 2019-01-17 15:23:52 -08:00
Leonardo de Moura
10456f1607 fix(library/compiler/llnf): constructors are not global constants 2019-01-17 14:18:58 -08:00
Leonardo de Moura
a82731fb23 fix(library/compiler/llnf): literals are created with RC = 1 2019-01-17 14:08:40 -08:00
Leonardo de Moura
ad13d04b1d chore(library/compiler/llnf): use _ to name _inc and _dec instructions 2019-01-17 14:04:05 -08:00
Leonardo de Moura
0f28d3187a fix(library/compiler/llnf): avoid unnecessary _dec instruction 2019-01-17 13:57:13 -08:00
Leonardo de Moura
f315823bee fix(library/compiler/llnf): missing ensure_terminal 2019-01-17 13:51:39 -08:00
Leonardo de Moura
244079a4cc feat(library/compiler/llnf): add process_cases 2019-01-17 13:29:38 -08:00
Leonardo de Moura
0451a53b54 doc(library/compiler/llnf): document explicit_rc_fn 2019-01-15 16:26:09 -08:00
Leonardo de Moura
54fe7e7be9 feat(library/compiler/llnf): explicit_rc_fn 
TODO: cases_on terms
 2019-01-15 15:54:38 -08:00
Leonardo de Moura
579d462776 feat(library/compiler/llnf): add process_app 2019-01-15 12:49:08 -08:00
Sebastian Ullrich
49f580f190 feat(library/compiler/builtin,frontends/lean/vm_elaborator): add temporary expr.local primitive 
This makes it possible (or at least much easier) to interface with old
parser/elaborator code using local_consts for e.g. `def` parameters.
 2019-01-12 14:16:43 +01:00
Leonardo de Moura
e0da13128e refactor(library/compiler/llnf): explicit_rc_fn 2019-01-09 16:57:38 -08:00
Leonardo de Moura
7b4b92702f feat(library/compiler/llnf): cancel _unbox over _box and _box over _unbox 2019-01-09 16:57:38 -08:00
Leonardo de Moura
78379e2224 fix(library/compiler/llnf): avoid unnecessary let-decl at cast_if_needed 2019-01-09 16:57:38 -08:00
Leonardo de Moura
c1fd3e6062 fix(library/compiler/llnf): unnecessary let-decl 2019-01-09 16:57:38 -08:00
Leonardo de Moura
8111aaad8a fix(library/compiler/llnf): missing case 2019-01-09 16:57:37 -08:00
Sebastian Ullrich
d2de703e51 feat(frontends/lean/vm_elaborator): add primitive environment.contains 2019-01-06 15:47:06 +01:00
Sebastian Ullrich
db6b1d6e85 feat(frontends/lean/vm_elaborator,library/init/lean/elaborator): pass parser_state between languages, create parser object on C++ side to existing functions (that don't actually parse anything) 2018-12-18 15:30:38 +01:00
Sebastian Ullrich
d9a22d43b2 feat(library/vm/vm_aux): add primitive for calling old elaborator 2018-12-14 17:36:56 +01:00
Leonardo de Moura
607d22ae58 fix(library/compiler/csimp): bug at float_cases_on_core 
The bug occurs when floating `cases_on` application in code of the form
```
let x := C.cases_on ...
in t
```
and when the type of `t` depends on `x`.
The issue here is that the `x` declaration disappears after the float, but the resulting type still depends on it.
We fix the bug by replacing `x` with its value in the type.

cc @kha
 2018-11-30 11:40:41 -08:00
Leonardo de Moura
eae421c506 feat(library/compiler/llnf): explicit_rc skeleton 2018-11-28 15:44:55 -08:00
Leonardo de Moura
05d25d92c0 feat(library/compiler): only create _boxed version if needed 2018-11-28 09:46:48 -08:00
Sebastian Ullrich
6d0b3afa7e fix(library/compiler/compiler): do not silently abort on user-given sorrys 2018-11-17 18:00:55 +01:00
Leonardo de Moura
3d24c6466b feat(library/compiler/llnf): generate _boxed version eagerly 2018-11-15 18:10:20 -08:00
Leonardo de Moura
ae037c2a23 fix(library/compiler/builtin): incorrect assertion 2018-11-15 18:09:02 -08:00
Leonardo de Moura
b55b1deaf5 chore(library/compiler): remove ir.cpp 
There is only one missing transformation: insert explicit reference counting instructions.
We will implement this transformation at `llnf.cpp`. After that, we are
ready to emit C++ code.
 2018-11-15 16:53:44 -08:00
Leonardo de Moura
e5666b3464 feat(library/compiler): remove another reference to vm.h 2018-11-15 16:38:01 -08:00
Leonardo de Moura
db5d976278 feat(library/compiler): use new builtin module 2018-11-15 16:30:42 -08:00
Leonardo de Moura
3a7d407d6c feat(library/compiler/builtin): register io primitives 
TODO: implement `io` primitives in the new runtime
 2018-11-15 16:14:50 -08:00
Leonardo de Moura
4f2997d691 feat(library/compiler/builtin): use std::unordered_map 2018-11-15 13:48:11 -08:00
Leonardo de Moura
4b65e0bace refactor(library/compiler/builtin): do not store pointer to functions 
The interface between the (to be implemented) new interpreter and the
compiled code will be automatically generated.
 2018-11-15 13:39:04 -08:00
Leonardo de Moura
5acdd68ad5 feat(library/compiler/init_module): initialize builtin module 2018-11-15 13:33:02 -08:00