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

15165 commits

This branch
This branch
All branches
Author SHA1 Message Date
Sebastian Ullrich
80a79336f2 chore(.gitignore): ignore library/Makefile 2018-11-07 09:30:32 +01:00
Sebastian Ullrich
0026b59a88 fix(tests/lean/macro_scopes): expected output 2018-11-07 09:11:49 +01:00
Leonardo de Moura
330e2700b1 chore(library/compiler/compiler): add trace.compiler.boxed option for debugging purposes 2018-11-06 16:55:02 -08:00
Leonardo de Moura
5acb5e63b1 feat(library/compiler): revise llnf instructions 
Motivation: make sure we can generate "portable" C++ code. "Portable"
here means we can compile the generated code using 32 and 64 bit machines.
 2018-11-06 16:55:02 -08:00
Leonardo de Moura
8af0c85d4f feat(library/compiler/erase_irrelevant): convert enumeration types into uint* types 2018-11-06 16:55:02 -08:00
Leonardo de Moura
83ebacb8af chore(library/compiler/util): style 2018-11-06 16:55:02 -08:00
Leonardo de Moura
9f3544aaa4 feat(library/compiler/erase_irrelevant): preserve enumeration types 2018-11-06 16:55:02 -08:00
Leonardo de Moura
6f03df871b chore(library/compiler): remove whnf_upto_runtime_type 
It is not needed anymore.
 2018-11-06 16:55:02 -08:00
Leonardo de Moura
e63721958b refactor(library/compiler): add is_enum_type auxiliary function 2018-11-06 16:55:02 -08:00
Leonardo de Moura
f404c5c446 refactor(library/init/data): make sure uint* and usize are irreducible 
Remark: this commit breaks the support for `uint*` and `usize` in the old VM.
 2018-11-06 16:55:02 -08:00
Leonardo de Moura
216a3632cc refactor(library/compiler/llnf): simplify llnf primitive instructions 2018-11-06 16:55:02 -08:00
Leonardo de Moura
39850d3b84 chore(library/compiler/llnf): remove dead global 2018-11-06 16:55:02 -08:00
Sebastian Ullrich
7fdfdb1784 chore(library/init/lean/parser): remove unnecessary class constraints 2018-11-06 21:45:08 +01:00
Sebastian Ullrich
a551c0d8c9 fix(library/module_mgr): compiling a file with a failed transitive dependency may have succeeded without output 2018-11-06 21:31:02 +01:00
Sebastian Ullrich
5a286f5e46 test(tests/lean/macro_scopes): macro scopes propagation test 2018-11-06 17:33:16 +01:00
Sebastian Ullrich
090c4c0ce7 feat(library/init/lean/syntax): add lazily propagated macro scopes to syntax_node 2018-11-06 16:46:50 +01:00
Leonardo de Moura
c108fc95cb feat(library/compiler/ir): basics 2018-11-05 17:04:23 -08:00
Leonardo de Moura
8de7637f75 feat(library/compiler): add to_ir skeleton 2018-11-05 17:04:23 -08:00
Sebastian Ullrich
fc4dcd19cf refactor(library/init/lean/parser): use ident.view in syntax.to_format 2018-11-05 17:57:00 +01:00
Sebastian Ullrich
dcb7566e53 fix(tests/lean/parser1): fix test 2018-11-05 17:40:11 +01:00
Sebastian Ullrich
7d6048c795 fix(library/message_builder): fix output of nested kernel exceptions 2018-11-05 17:37:21 +01:00
Sebastian Ullrich
507509b336 chore(library/Makefile.in): suppress comment output 
I hate make
 2018-11-05 17:15:01 +01:00
Sebastian Ullrich
c9bebb7411 feat(library/time_task): do not report inclusive times 2018-11-05 17:06:32 +01:00
Sebastian Ullrich
8c27f0aac6 refactor(frontends/lean/elaborator,library/init/lean): finish no_kind refactoring 2018-11-04 20:24:40 +01:00
Sebastian Ullrich
58df9cb813 chore(library/Makefile.in): prevent infinite make cycles 2018-11-04 20:24:40 +01:00
Sebastian Ullrich
09aa4f9ab3 chore(frontends/lean/elaborator): don't try to recover from errors in patterns 2018-11-04 19:03:00 +01:00
Leonardo de Moura
733bbc521f feat(library/init/core): mark thunk and task primitives with [noinline] 
In the future, we should use the `[builtin]` attribute which cannot be
overwritten by the user.
 2018-11-02 13:54:40 -07:00
Leonardo de Moura
b23251fd6e feat(library/compiler/lambda_lifting): preserve join points when performing lambda lifting 2018-11-01 16:04:25 -07:00
Leonardo de Moura
adff01bba4 fix(library/vm/vm): handle InvokeJP at pc manipulation methods 2018-11-01 16:01:36 -07:00
Leonardo de Moura
e11fe27de2 chore(library/compiler/lambda_lifting): temporary hack 
Make sure that a join point that has been lambda lifted is not tagged as
a join point anymore.
 2018-11-01 15:21:14 -07:00
Leonardo de Moura
f27ab2bb38 chore(library/compiler/emit_bytecode): remove dead code 2018-11-01 14:21:20 -07:00
Leonardo de Moura
e5432f5fb2 fix(library/type_context): memory access violation in the new type class inference optimization 2018-11-01 14:16:57 -07:00
Leonardo de Moura
f22bdec775 feat(library/vm): add support for join-points in the old VM 
Motivation: to make progress in the new compiler stack, we have
to preserve join points during lambda lifting. Right now, they are
lifted as regular lambdas. So, to keep them, we need some basic
support for them in the old VM. The implementation here is quick and
dirty. This is not an issue since this code will be deleted soon.
 2018-11-01 14:07:59 -07:00
Leonardo de Moura
ae30b16f0d fix(library/compiler/lcnf): nat.zero ==> literal 2018-11-01 11:59:17 -07:00
Leonardo de Moura
5d89347241 feat(library/compiler/llnf): improve memory cell reuse heuristic 2018-10-31 14:44:33 -07:00
Leonardo de Moura
34f01ff32e chore(library/init/data/nat/basic): missing [specialize] 2018-10-31 14:44:23 -07:00
Leonardo de Moura
e21608d456 chore(library/compiler/csimp): style 2018-10-31 13:25:54 -07:00
Leonardo de Moura
189b037358 chore(tests/lean/run/new_compiler): fix test 2018-10-31 13:25:01 -07:00
Leonardo de Moura
e68372cfd9 fix(library/compiler/csimp): another join point related bug 2018-10-31 13:22:20 -07:00
Leonardo de Moura
39c2ee2931 chore(library/compiler/llnf): typo 2018-10-31 13:22:14 -07:00
Leonardo de Moura
12a01d101c refactor(library/compiler/llnf): memory cell reuse instruction set 2018-10-31 09:35:22 -07:00
Leonardo de Moura
67a78d1c76 chore(library/compiler/llnf): cleanup 2018-10-31 08:36:09 -07:00
Leonardo de Moura
d98a1d1da3 feat(library/compiler/llnf): refine reset operation placement 
This is not a perfect solution yet. I have identified two problems:
1) The heuristic used at `mark_to_reset_fields` is too weak.
   Suppose we have
   ```
      let ...
          _x := prod.mk field_1 0
      in some _x
   ```
   The current implementation will mark `field_1` to be reset since it
   occurs in a non tail call `prod.mk field_1 0`. However, we can
   assume `prod.mk field_1 0` is part of the return value.

2) The current semantics of the reset instruction may produce
   unnecessary memory allocation. Consider the following example
   ```
   let _x_1 := x.1,
       _x_2 := x.2,
       _x_3 := _reset.2 x
   in @bool.cases_on y
      (_cnstr.0.0)
      (let _x_4 := f _x_2,
       in _updt.2 _x_3 _x_4)
   ```
   The memory cell `_x_3` is only used in the second branch of
   the `bool.cases_on`. So, if `y` is `ff`, and `x` is a shared
   object, we will allocate memory at `_reset.2 x` for nothing.
 2018-10-30 17:34:36 -07:00
Leonardo de Moura
abc107d963 chore(library/vm/vm): remove dead code 2018-10-30 14:27:47 -07:00
Leonardo de Moura
d3c37fee7a perf(library/vm/vm): inline Updt/UpdtCidx/Reset 2018-10-30 14:01:32 -07:00
Leonardo de Moura
b6bc0bb284 feat(library/compiler/llnf): add reset.idx obj primitive 
The idea is to make it clear the intent, and simplify the IR conversion.
 2018-10-30 13:48:09 -07:00
Leonardo de Moura
5c3639a5c0 feat(library/compiler/llnf): avoid unnecessary resets 2018-10-30 13:32:50 -07:00
Leonardo de Moura
8527fdc338 refactor(library/compiler/llnf): memory reuse optimization 2018-10-30 10:28:56 -07:00
Sebastian Ullrich
93fc1fd1de fix(library/init/lean/parser/combinators): node: do not wrap error in first argument 2018-10-30 17:43:05 +01:00
Sebastian Ullrich
74bd182bc8 perf(library/init/lean/parser/combinators): make node semireducible 2018-10-30 17:43:05 +01:00