Leonardo de Moura
cfa21d6875
chore(boot): update
2019-02-05 14:41:42 -08:00
Leonardo de Moura
2058d33d07
feat(runtime,library/compiler): add name.dec_eq builtin
2019-02-05 14:36:02 -08:00
Leonardo de Moura
eb57a904af
chore(runtime): avoid overloads
2019-02-05 14:04:29 -08:00
Leonardo de Moura
103a616f57
chore(boot): update
2019-02-05 13:42:02 -08:00
Leonardo de Moura
ff54bf337a
fix(library/init/data/repr): ultra inefficient to_digits
...
It was very inefficient, and was producing stack overflows for big numbers.
2019-02-05 13:36:13 -08:00
Leonardo de Moura
60c8b1870e
chore(boot): update
2019-02-05 13:08:59 -08:00
Leonardo de Moura
3444a295e7
feat(library/compiler,runtime): builtin support for lean.name
2019-02-05 12:57:46 -08:00
Leonardo de Moura
f17101cfbe
chore(src/CMakeLists): update version number
2019-02-05 10:15:11 -08:00
Leonardo de Moura
fe3be7a80d
chore(boot): update
2019-02-04 16:23:38 -08:00
Leonardo de Moura
c5b0258e49
feat(library/compiler/util): do not box unit
2019-02-04 16:19:48 -08:00
Leonardo de Moura
a6645645e3
chore(boot): update
2019-02-04 16:07:31 -08:00
Leonardo de Moura
e57401232c
fix(library/compiler/emit_cpp): bug at emit 0-ary constructor of non enum type (e.g., list.nil)
2019-02-04 16:07:31 -08:00
Leonardo de Moura
16f6da6a62
chore(boot): update
2019-02-04 15:28:15 -08:00
Leonardo de Moura
7c355d3ba6
feat(library/compiler): thunk support
2019-02-04 15:22:18 -08:00
Leonardo de Moura
579ac58b62
chore(runtime/object): expose thunk_map and thunk_bind
2019-02-04 13:11:37 -08:00
Leonardo de Moura
fc4505884b
chore(boot): update
2019-02-04 12:56:11 -08:00
Leonardo de Moura
4d66836255
fix(library/compiler/llnf): bug at process_cases
...
We should not decrement the RC of borrowed variables.
2019-02-04 12:51:51 -08:00
Leonardo de Moura
7eb9c46bc6
fix(library/compiler): functions marked as @[noinline] were not being replaced by their reduced arity version
2019-02-04 12:23:37 -08:00
Leonardo de Moura
4696f603e2
chore(boot): update
2019-02-04 10:36:02 -08:00
Leonardo de Moura
25ec21b498
feat(library/compiler/name_mangling): new name mangling procedure that produces more readable output
2019-02-04 10:31:38 -08:00
Leonardo de Moura
5b3f3178ae
feat(src/CMakeLists): copy static library to bin directory
2019-02-04 09:55:22 -08:00
Leonardo de Moura
98edae152a
fix(runtime): replace lean::alloca with macro
...
Functions using `alloca` are not inlined even when marked with
`inline` in some compilers.
Remark: GCC will _not_ inline a function calling alloca unless it is
annotated with always_inline.
2019-02-04 09:36:53 -08:00
Leonardo de Moura
b4a78a0280
chore(src/boot): update
2019-02-03 19:22:01 -08:00
Leonardo de Moura
67f4fb603d
chore(library/compiler/emit_cpp): unnecessary line break
2019-02-03 19:19:01 -08:00
Leonardo de Moura
79e8358f9c
fix(library/compiler/emit_cpp): tail call optimization
2019-02-03 19:16:50 -08:00
Leonardo de Moura
628c377673
chore(src/boot): update
2019-02-03 10:45:48 -08:00
Leonardo de Moura
e5e245d0f2
chore(library/compiler/emit_cpp): missing space
2019-02-03 10:41:41 -08:00
Leonardo de Moura
b5f20f0b73
chore(src/boot): update
2019-02-03 10:38:57 -08:00
Leonardo de Moura
5aab81d773
chore(library/compiler/emit_cpp): ignore unused labels
2019-02-03 10:37:34 -08:00
Leonardo de Moura
73f4100a46
feat(library/compiler/emit_cpp): tail call optimization
2019-02-03 10:31:39 -08:00
Leonardo de Moura
fb0562e107
chore(src/boot): update
2019-02-03 10:06:47 -08:00
Leonardo de Moura
65e7e785ff
fix(library/compiler/llnf): include closures at is_unboxed
2019-02-03 10:04:21 -08:00
Sebastian Ullrich
3cf5241208
chore(boot): do not diff or eol-convert autogenerated files
2019-02-02 14:35:58 +01:00
Leonardo de Moura
b210215d3a
feat(src/CMakeLists): build src/boot
...
@kha We can now compile and link all C++ generated files.
We may still have many bugs, but the basic infrastructure for
generating C++ from Lean files is finally working.
2019-02-01 17:59:50 -08:00
Leonardo de Moura
065c3b991c
chore(src/boot): update
2019-02-01 17:59:29 -08:00
Leonardo de Moura
c097f1c1e0
fix(kernel/builtin): add extern
2019-02-01 17:58:55 -08:00
Leonardo de Moura
90499abd94
fix(library/compiler/llnf): inc is only needed if variable has type _obj
2019-02-01 17:53:58 -08:00
Leonardo de Moura
e31f026bb2
fix(library/compiler/emit_cpp): add extern for constants declared in other modules
2019-02-01 17:26:12 -08:00
Leonardo de Moura
0fb01a3369
chore(src/boot): update
2019-02-01 17:17:51 -08:00
Leonardo de Moura
0918a599ae
feat(*): builtin support for uint functions
...
@kha The VM versions just throw exceptions. They are just stubs to
make sure we can compile Lean.
I implemented the uint functions in the new runtime, but there are a
few missing cases marked with TODO.
I needed these builtins to be able to compile the C++ generated code for
corelib.
2019-02-01 17:04:24 -08:00
Leonardo de Moura
54f501594d
chore(library/init/data/uint,library/init/data/usize): simplify
2019-02-01 15:41:55 -08:00
Leonardo de Moura
9017fd3658
chore(src/boot): update
2019-02-01 15:13:06 -08:00
Leonardo de Moura
ec5a326157
fix(library/compiler/emit_cpp): include runtime/io.h
2019-02-01 15:12:30 -08:00
Leonardo de Moura
ac53080ced
fix(kernel/builtin): incorrect signature
2019-02-01 15:06:57 -08:00
Leonardo de Moura
0c36b8c4d8
chore(src/boot): update
2019-02-01 15:02:24 -08:00
Leonardo de Moura
6e8f8a8cdc
fix(library/compiler/emit_cpp): another bug in emit_quoted_string
2019-02-01 14:59:51 -08:00
Leonardo de Moura
8c1d6c49c5
chore(src/boot): update
2019-02-01 14:40:22 -08:00
Leonardo de Moura
d12667fb6b
fix(library/compiler/emit_cpp): bug handling 0-ary _cnstr
2019-02-01 14:35:40 -08:00
Leonardo de Moura
d461833fcd
fix(library/compiler/llnf): _sset and _uset were taking invalid LLNF arguments
2019-02-01 14:31:08 -08:00
Leonardo de Moura
b6f7472dd7
fix(library/compiler/emit_cpp): remove leftover
2019-02-01 14:21:17 -08:00
