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

5376 commits

Author SHA1 Message Date
Leonardo de Moura
65e7e785ff fix(library/compiler/llnf): include closures at is_unboxed 2019-02-03 10:04:21 -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
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
ec5a326157 fix(library/compiler/emit_cpp): include runtime/io.h 2019-02-01 15:12:30 -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
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
Leonardo de Moura
42ee42b732 fix(library/compiler/emit_cpp): bug at quote_string 2019-02-01 14:15:38 -08:00
Leonardo de Moura
4fa06e38b2 chore(*): add skeleton for new builtin primitives, update src/boot 2019-02-01 14:03:03 -08:00
Leonardo de Moura
51343a0e3a chore(library/compiler/builtin): rename primitives 2019-02-01 13:39:35 -08:00
Leonardo de Moura
7c32e04f9c chore(library/compiler/emit_cpp): avoid line breaks when declaring blocks of variables 2019-02-01 13:36:43 -08:00
Leonardo de Moura
d154b45d4c chore(library/compiler/builtin): avoid unused variable warning on clang++ 2019-02-01 13:33:52 -08:00
Leonardo de Moura
1212207446 fix(library/compiler/reduce_arity): we should not create auxiliary definitions with 0 arguments at reduce_arity 2019-02-01 11:15:51 -08:00
Sebastian Ullrich
64ab576dbf fix(shell/lean,library/messages): print messages in correct order (and immediately) when --json was not given 2019-02-01 17:10:14 +01:00
Leonardo de Moura
150555e03f chore(library/compiler/emit_cpp): temporarily comment line 
See new comment to understand motivation for the change.
 2019-01-31 18:24:31 -08:00
Leonardo de Moura
3af0d91bbb fix(library/compiler/llnf): missing cases at explicit_boxing_fn 2019-01-31 18:16:36 -08:00
Leonardo de Moura
ddc5cf05c4 fix(library/compiler/llnf): user numeric literals to store enum type values in LLNF 2019-01-31 17:58:03 -08:00
Leonardo de Moura
7a322340cb fix(library/compiler/llnf): in LLNF, the _box.n argument must be a variable 2019-01-31 17:54:06 -08:00
Leonardo de Moura
39f45beec0 chore(library/compiler/llnf): fix typo 2019-01-31 17:52:59 -08:00
Leonardo de Moura
0f47787a06 fix(library/compiler/llnf): remove bad optimization 
It may destroy boxed value information. Moreover, we want
terminals to be jmp, variable or cases.
 2019-01-31 17:52:28 -08:00
Leonardo de Moura
94d7b4e094 fix(library/compiler/emit_cpp): support for _unreachable 2019-01-31 17:05:52 -08:00
Leonardo de Moura
a1b65acf3d fix(library/compiler/builtin): add lean:: prefix 
TODO: we will need to revise this for the LLVM backend.
In principle, builtins that are used by LLVM and C++ backends should be
`extern "C"` in a global namespace.
 2019-01-31 16:57:25 -08:00
Leonardo de Moura
353d16f5f6 fix(library/compiler/emit_cpp): mpz ==> lean::mpz 2019-01-31 16:57:07 -08:00
Leonardo de Moura
5f29b1003b fix(library/compiler/emit_cpp): missing enf_unreachable case 2019-01-31 16:37:02 -08:00
Leonardo de Moura
4166851574 feat(library/compiler/emit_cpp): emit_box and emit_unbox 2019-01-31 16:16:30 -08:00
Leonardo de Moura
78842d8d03 feat(library/compiler/emit_cpp): emit_proj, emit_sproj, emit_uproj, emit_sset, emit_uset 2019-01-31 15:38:53 -08:00
Leonardo de Moura
80754e84c5 feat(library/compiler/emit_cpp): emit_closure 2019-01-31 15:06:04 -08:00
Leonardo de Moura
74079cb591 feat(library/compiler/emit_cpp): emit_lit 2019-01-31 14:54:43 -08:00
Leonardo de Moura
34256795d7 feat(library/compiler/emit_cpp): emit_reuse 2019-01-31 14:54:35 -08:00
Leonardo de Moura
7c3354f15f feat(library/compiler/emit_cpp): emit_reset 2019-01-31 12:33:17 -08:00
Leonardo de Moura
909a8d7c6d fix(library/compiler/llnf): bug at to_llnf when boxing is enabled 2019-01-30 16:48:04 -08:00
Leonardo de Moura
d63bbb3728 feat(library/compiler/emit_cpp): emit_cnstr 2019-01-30 15:47:38 -08:00
Leonardo de Moura
d2cbf9584f feat(library/compiler/emit_cpp): emit _apply instruction 2019-01-30 14:37:21 -08:00
Leonardo de Moura
efcc459c3b fix(library/compiler/emit_cpp): emit_constant should handle neutral 2019-01-30 14:36:14 -08:00
Leonardo de Moura
1673775c6e fix(library/compiler/cse): make sure cse produces correct result in LLNF expressions 
In LLNF, we must take the type of a let-declaration into account. For
example, we cannot merge the following declarations:

```
x_1 : uint8 := _cnstr.0.0.0
x_2 : _obj  := _cnstr.0.0.0
```

We were producing incorrect C++ code for
library/init/lean/parser/token.lean because of this bug.
 2019-01-30 13:52:43 -08:00
Leonardo de Moura
69eea3d225 fix(library/compiler/emit_cpp): missing collect_dependencies 2019-01-29 16:41:32 -08:00
Leonardo de Moura
38172c8f1c feat(library/compiler/emit_cpp): use if statement when cases has only 2 cases 2019-01-29 16:32:23 -08:00
Leonardo de Moura
e4c4eab48e fix(library/compiler/emit_cpp): collect_dependencies was not handling _closure instruction 2019-01-29 16:31:29 -08:00
Leonardo de Moura
20641731e3 feat(library/compiler/emit_cpp): add emit_instr skeleton 2019-01-29 16:04:50 -08:00
Leonardo de Moura
706f4cb01b fix(library/compiler/builtin): incorrect builtin type 2019-01-29 16:04:02 -08:00
Leonardo de Moura
48b03672cc feat(library/compiler/emit_cpp): emit terminals 2019-01-29 15:15:05 -08:00
Leonardo de Moura
9f8760d936 fix(library/compiler/llnf): LLNF terminal is variable, jmp, or cases 2019-01-29 14:59:12 -08:00
Leonardo de Moura
61e51ba402 fix(library/compiler/llnf): adjust code, now type must match arity 
We recently modified the type of closures in LLNF.
This commit fixes a mismatch.
 2019-01-28 15:55:01 -08:00
Leonardo de Moura
0e8067e191 fix(library/compiler/compiler): ensure_arity bug 2019-01-28 15:42:23 -08:00
Leonardo de Moura
371baf2002 fix(library/compiler/compiler): typo 2019-01-28 15:34:58 -08:00
Leonardo de Moura
1f3201dca1 feat(library/compiler): add emit_fn_fn skeleton 2019-01-28 15:04:56 -08:00
Leonardo de Moura
d3756fd915 feat(library/compiler): add _void type for LLNF format 2019-01-28 13:06:25 -08:00
Leonardo de Moura
274aeed30f fix(library/compiler/compiler): make sure that the type of functions that return closures match their arity 
Before this commit, we could have a LLNF function `f` of arity 0 and
type `_obj -> _obj`. Now, this kind of function has type `_obj`.
 2019-01-25 15:40:25 -08:00