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

105 commits

Author SHA1 Message Date
Leonardo de Moura
9a71c2dbb6 feat(library/init/lean/ir): remove support for functions with multiple return values 
This feature was originally added to implement the state monad.
It is not needed anymore since we have a better encoding that doesn't
require this feature and avoids memory allocations.
 2018-10-22 17:39:40 -07:00
Leonardo de Moura
85160e1baa feat(library/init/lean/ir/format): missing [inline] 2018-10-22 14:58:23 -07:00
Leonardo de Moura
5810418ddd perf(library/init/lean/ir/extract_cpp): use derive to speedup type class resolution 
This modification reduced processing time for this file to 1.49 secs
from 2.30 secs on my office desktop.
 2018-10-12 12:27:08 -07:00
Leonardo de Moura
17d6ef3abe chore(library/init/lean/ir/parser): minimize <|> inlining 2018-10-12 11:57:42 -07:00
Leonardo de Moura
f640b1bbac feat(library/init/lean/ir/extract_cpp): missing inlines 2018-09-20 08:39:25 -07:00
Leonardo de Moura
2a13ea484e chore(library/init/lean/ir/extract_cpp): add space 2018-09-18 08:23:32 -07:00
Leonardo de Moura
afd54039ab chore(library): remove >>, we should use *> 2018-09-12 17:31:21 -07:00
Leonardo de Moura
9e305a5f26 chore(library): remove return, we should use pure 2018-09-12 16:51:11 -07:00
Leonardo de Moura
71dd8653bc feat(library/init/core): decidable_eq is a proper class 
We need this to take advantage of the new indexing structure we are
going to add to improve performance.
 2018-09-07 16:38:11 -07:00
Sebastian Ullrich
eda9e4bb3f feat(library/derive_attribute): temporary, hacky C++ implementation of @[derive] 2018-08-01 18:44:23 -07:00
Sebastian Ullrich
2823bebd23 refactor(library/init/lean/parser/parsec): message.pos: replace with iterator 
This allows efficient recovery from a parse error as well as implementing
`has_to_string` for `message`
 2018-07-30 10:38:00 -07:00
Sebastian Ullrich
65fd050b83 feat(library/init/lean/parser/parsec): add custom error message type 2018-07-27 14:29:50 -07:00
Sebastian Ullrich
72b255d4e1 chore(library/init/lean/parser/parser_t): rename module and type to parsec to avoid nested use of parser 2018-07-12 10:35:20 +02:00
Sebastian Ullrich
e57117a9b3 chore(library/init/lean/parser/parser_t): revert introduction of parser_t 2018-07-11 18:44:04 +02:00
Sebastian Ullrich
7ae87705c2 feat(library/init/lean/parser/parser_t): introduce monad_parser 2018-06-15 17:48:20 +02:00
Leonardo de Moura
1bae8f8eab refactor(library/init/lean/ir/parser): parser.lean => parser_t.lean 2018-06-05 08:00:13 -07:00
Sebastian Ullrich
0f7c0ac8bf feat(init/lean/parser/parser): make a monad transformer 
Also move parser combinators into the more specific namespace `init.lean.parser.parser_t`.
 2018-06-04 12:57:23 +02:00
Leonardo de Moura
b78e9df869 chore(runtime/object): tag => obj_tag 
`tag` at `object.h` conflicts with `tag` at `expr.h`
 2018-05-20 12:00:59 -07:00
Leonardo de Moura
2944f7a027 chore(runtime): lean_obj.* ==> object.* 2018-05-20 10:17:15 -07:00
Leonardo de Moura
2d604e7d25 chore(runtime/lean_obj): remove lean_ prefix 2018-05-20 10:13:44 -07:00
Leonardo de Moura
acdcbdb71e feat(library/init/lean/ir): add instructions for (big) integer arithmetic 2018-05-17 18:17:23 -07:00
Leonardo de Moura
5d8501acf5 chore(runtime/lean_obj): consistent naming convention 2018-05-17 16:45:27 -07:00
Leonardo de Moura
217fa0e8c9 feat(library/init/lean/ir/lirc): add option to specify whether input is in SSA or not 2018-05-17 15:53:49 -07:00
Leonardo de Moura
af1a5fe874 feat(library/init/lean/ir): add x : ty := y instruction 
It is useful when we are not producing IR in SSA.
 2018-05-17 15:44:13 -07:00
Leonardo de Moura
b14f7e2fa4 chore(library/init/lean/ir/reserved): update list of reserved words 2018-05-17 15:44:01 -07:00
Leonardo de Moura
dede61b122 feat(library/init/lean/ir): add tag and tag_ref instructions 2018-05-17 14:51:41 -07:00
Leonardo de Moura
5d53eccb59 feat(runtime): string support 2018-05-17 13:11:47 -07:00
Leonardo de Moura
53d459911f refactor(library/init/lean/ir): RC instructions 2018-05-16 10:28:51 -07:00
Leonardo de Moura
8cb7511a91 feat(runtime/lean_obj): natural number support 2018-05-16 10:28:51 -07:00
Leonardo de Moura
ade8cb7296 chore(library/init/lean/ir): make it clear that big number may be a tagged pointer 2018-05-15 15:58:58 -07:00
Leonardo de Moura
6e1a64a3ed fix(library/init/lean/ir): change semantics of big number operations 
Remark: only `inc`, `dec` and `decs` should modify the reference counters.
 2018-05-15 15:52:54 -07:00
Leonardo de Moura
65b9da7a29 doc(library/init/lean/ir/ir): document operators 2018-05-15 15:31:27 -07:00
Leonardo de Moura
cf36d8b08e refactor(library/init/lean/ir): rename ir.instr constructors 2018-05-15 14:48:12 -07:00
Leonardo de Moura
272f80c799 feat(library/init/lean/ir): add string_push and string_append instructions 2018-05-15 14:27:10 -07:00
Leonardo de Moura
74767df5ff feat(library/init/lean/ir/extract_cpp): add initialize_prefix and finalize_prefix 2018-05-15 14:09:38 -07:00
Leonardo de Moura
be74e3f974 refactor(library/init/lean/ir): add init/lean/ir/instances.lean 2018-05-15 12:14:36 -07:00
Leonardo de Moura
0f2a8f09c2 chore(library/init/lean/ir): cleanup 2018-05-15 12:09:04 -07:00
Leonardo de Moura
5cfb442f2c feat(library/init/lean/ir): add compilation unit initializer/finalizer 2018-05-15 11:57:53 -07:00
Leonardo de Moura
52b5ab1514 doc(library/init/lean/ir/ir): document unary operators 2018-05-14 20:29:28 -07:00
Leonardo de Moura
59f9de720d feat(library/init/lean/ir/lirc): we should support only C external names without mangling 2018-05-14 16:32:18 -07:00
Leonardo de Moura
d166b69e2c feat(library/init/lean/ir/parser): add support for functions that do not return anything 2018-05-14 16:05:15 -07:00
Leonardo de Moura
aa1006d01b feat(library/init/lean/ir/extract_cpp): generate libleanruntime.a 2018-05-14 14:34:10 -07:00
Leonardo de Moura
31ce1a23e7 fix(library/init/lean/ir/extract_cpp): add support for bignum literals 2018-05-14 11:12:49 -07:00
Leonardo de Moura
37201b9192 feat(library/init/lean/ir/extract_cpp): add emit_closure 2018-05-14 09:53:45 -07:00
Leonardo de Moura
c6de7ae4d1 fix(library/init/lean/ir/type_check): typo 2018-05-14 09:53:29 -07:00
Leonardo de Moura
ba76d86a38 feat(library/init/lean/ir/extract_cpp): add emit_app, fix assignment 2018-05-14 09:28:17 -07:00
Leonardo de Moura
11270591ff fix(library/init/lean/ir/extract_cpp): missing case at collect_used 2018-05-13 14:49:57 -07:00
Leonardo de Moura
12854dc944 feat(library/init/lean/ir/extract_cpp): include uncurry 2018-05-13 14:47:54 -07:00
Leonardo de Moura
c00117a269 fix(library/init/lean/ir/ssa_check): bug 2018-05-13 14:43:13 -07:00
Leonardo de Moura
344de0e42e feat(library/init/lean/ir/extract_cpp): emit header of all functions used in a compilation unit 2018-05-13 14:40:52 -07:00