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

48 commits

Author SHA1 Message Date
Leonardo de Moura
a35a951374 chore(library/compiler/emit_cpp): add uint* aliases 2019-02-05 17:01:10 -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
7c355d3ba6 feat(library/compiler): thunk support 2019-02-04 15:22:18 -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
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
e5e245d0f2 chore(library/compiler/emit_cpp): missing space 2019-02-03 10:41:41 -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
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
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
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
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
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
94d7b4e094 fix(library/compiler/emit_cpp): support for _unreachable 2019-01-31 17:05:52 -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
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
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
48b03672cc feat(library/compiler/emit_cpp): emit terminals 2019-01-29 15:15:05 -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
dd30cac8aa feat(library/compiler/emit_cpp): emit module initialization function 2019-01-25 15:24:55 -08:00
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
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
320917cca5 feat(library/compiler): add emit_cpp skeleton 2019-01-23 14:01:43 -08:00