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

81 commits

Author SHA1 Message Date
Leonardo de Moura
b1c187f717 feat(library/compiler): allow io unit as main function result type 
When `io unit` is used, we use `return 0` for `result.ok`, and `return
1` for `result.except`.
 2019-03-16 16:05:45 -07:00
Leonardo de Moura
6d0ec3a8c9 refactor(library/init/io): implement io monad using estate monad 2019-03-16 15:34:58 -07:00
Leonardo de Moura
35459664ad fix(library/compiler/emit_cpp): handle new unreachable terminal 2019-03-06 17:03:56 -08:00
Leonardo de Moura
6276d1a7f1 feat(library/compiler/emit_cpp): avoid reset field instructions when reuse instruction is guaranteed to be executed 
expr_const_folding.lean takes 3 secs now.
 2019-02-19 13:44:46 -08:00
Leonardo de Moura
fe1d17583c feat(library/compiler/emit_cpp): special support for (proj|inc)*;reset sequences 
We save inc/dec operations. It improved the performance of
`expr_const_folding.lean`. On my Linux desktop
Before: 3.7 secs
After:  3.1 secs

cc @kha
 2019-02-19 13:06:22 -08:00
Leonardo de Moura
b752dd1984 fix(library/compiler/emit_cpp): mark global objects as persistent 
They may be used by tasks, but they are not directly reachable from
task starting point.
 2019-02-17 11:45:51 -08:00
Leonardo de Moura
fca40151b2 fix(library/compiler/emit_cpp): is_shared should only be used on heap objects 2019-02-17 10:51:51 -08:00
Leonardo de Moura
75f4eb2f84 feat(library/compiler/emit_cpp): initialize task_manager at generated main function 2019-02-17 09:21:17 -08:00
Leonardo de Moura
e98acc86b8 feat(library/compiler/emit_cpp): "merge" the case with most occurrences as default: 2019-02-16 12:27:25 -08:00
Leonardo de Moura
0cb3ac683d feat(library/compiler): connect new const_folding module implemented in Lean with csimp 2019-02-15 14:37:48 -08:00
Leonardo de Moura
a8ac25e1ef fix(library/compiler/emit_cpp): bug at emitting exported function headers 2019-02-14 14:35:51 -08:00
Leonardo de Moura
19e111c2ff feat(library/compiler): allow main function to also have type io uint32 2019-02-13 16:29:10 -08:00
Leonardo de Moura
6ccdd18260 feat(library/compiler/emit_cpp): initialize the whole system if main module depends directly/indirectly of lean. declarations 2019-02-13 16:16:43 -08:00
Leonardo de Moura
6afad35aac feat(library/compiler): emit extern "C" for extern/foreign dependencies when needed 2019-02-13 07:58:06 -08:00
Leonardo de Moura
a82eab824a fix(library/compiler/emit_cpp): skip inline and adhoc extern declarations 2019-02-12 16:05:49 -08:00
Leonardo de Moura
09d194d5b7 feat(library/compiler): emit external declarations 
We only skip `inline` and `adhoc` externs.
 2019-02-12 15:42:59 -08:00
Leonardo de Moura
8acb2d4ed8 chore(library/compiler): minor modifications before builtin ==> extern refactor 2019-02-11 13:29:39 -08:00
Leonardo de Moura
57411ed039 refactor(library/compiler/extern_attribute): new interface 2019-02-11 12:48:37 -08:00
Leonardo de Moura
befa53ec70 feat(library/compiler/emit_cpp): use new extern_attribute module 2019-02-11 11:03:56 -08:00
Leonardo de Moura
bf15ee48fd refactor(library/compiler): export_name ==> export_attribute 2019-02-09 17:59:46 -08:00
Leonardo de Moura
9aed74a5e0 refactor(library/compiler): move extension for storing LLNF code 2019-02-09 17:59:46 -08:00
Leonardo de Moura
b09be6d0a5 fix(library/compiler/emit_cpp): missing { } 2019-02-08 11:06:29 -08:00
Leonardo de Moura
4339afc802 chore(library/compiler): [extname] ==> [export] 2019-02-08 10:25:21 -08:00
Max Wagner
e663f75fb2 chore(library/compiler): move builtins into the environment 2019-02-08 09:56:03 -08:00
Sebastian Ullrich
25ffbdda57 chore(src/*): fix style 2019-02-07 15:41:12 +01:00
Leonardo de Moura
14dd0d4907 feat(library/compiler): treat a function named main as the main function 2019-02-06 17:20:23 -08:00
Leonardo de Moura
16c0e62fa1 feat(library/compiler/emit_cpp): emit main 2019-02-06 14:34:52 -08:00
Leonardo de Moura
b4a7bb4f4c refactor(library/compiler): [cppname] ==> [extname] 
We will use this atttribute for all backends.
 2019-02-06 12:53:12 -08:00
Leonardo de Moura
f38de694b0 feat(frontends/lean/definition_cmds): compile code after attributes have been applied 
@kha do you see any problem with this change?
 2019-02-06 12:14:53 -08:00
Leonardo de Moura
d103ff70fe feat(library/compiler): avoid cnstr_set_scalar when possible 2019-02-06 10:49:58 -08:00
Sebastian Ullrich
58830be91f chore(library/compiler/emit_cpp): ignore warnings under GCC 2019-02-06 09:35:51 -08:00
Sebastian Ullrich
11860a65eb fix(library/compiler/emit_cpp): replace constructor tag on reuse 2019-02-06 09:34:14 -08:00
Sebastian Ullrich
eb85081a03 fix(library/compiler/emit_cpp): let y = f x; let z = ...; y is not a tail call 2019-02-06 09:33:38 -08:00
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