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

518 commits

Author SHA1 Message Date
Leonardo de Moura
9afee85919 fix(library/vm/vm_aux): remove old code 
Remark: `vm_timeit` was for the Lean 3 `timeit` primitive which is
different from the Lean 4 one. It has a different arity, and was
producing an assertion violation at emit_bytecode.cpp
 2019-03-14 16:04:10 -07:00
Leonardo de Moura
68ebc2a5c5 feat(library/init/data/string/basic): implement iterators using uft8 low level API 2019-03-12 06:56:05 -07:00
Leonardo de Moura
ff3bf508aa feat(library/init/fix, runtime): add fixpoint2, ..., fixpoint6 
The idea is to avoid allocating tuples when creating the fixpoint of
nary functions. For example, consider the new tests:
- tests/playground/fix.lean
- tests/playground/fix_with_tuples.lean

The second one (`fix_with_tuples`) uses the `fix` operator and tuples. For input = 20,
it creates more than 1 million extra objects. The first implementation
(`fix.lean`) using `fix₂` avoids this overhead.

TODO: Add support for pattern #N with N > 9 at
```
def expand_extern_pattern_aux (args : list string) : nat → string.iterator → string → string
```
 2019-03-10 11:19:02 -07:00
Leonardo de Moura
c862ce4a75 feat(runtime, library/init/data/string/basic): add utf8_pos 
`utf8_pos` is a low level alternative for `string.iterator`.
TODO: implement `string.iterator` using it.
 2019-03-09 12:30:19 -08:00
Leonardo de Moura
90260e005e feat(library/compiler/emit_bytecode): ignore unknown decls 
cc @kha
 2019-02-13 10:31:52 -08:00
Leonardo de Moura
456ed23cc2 feat(library/init): use extern when declarating nat primitives 2019-02-12 18:12:29 -08:00
Leonardo de Moura
425a4b70d1 feat(library/init/data/int/basic): use extern attribute, and fix div/mod mess 
Now, int.div and int.mod behave like C++ `/` and `%` for int,
moreover, they satisfy

          (a/b)*b + (a%b) = a
 2019-02-12 11:41:46 -08:00
Max Wagner
3164801a83 fix(library/vm): unary op dummies copy-paste error 2019-02-08 09:56:20 -08:00
Sebastian Ullrich
25ffbdda57 chore(src/*): fix style 2019-02-07 15:41:12 +01:00
Leonardo de Moura
2058d33d07 feat(runtime,library/compiler): add name.dec_eq builtin 2019-02-05 14:36:02 -08:00
Leonardo de Moura
3444a295e7 feat(library/compiler,runtime): builtin support for lean.name 2019-02-05 12:57:46 -08:00
Leonardo de Moura
7c355d3ba6 feat(library/compiler): thunk support 2019-02-04 15:22:18 -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
da92557076 chore(library/vm/vm_int): missing builtin in the old VM 2018-11-15 16:58:05 -08:00
Leonardo de Moura
ed4eeddf0a feat(runtime/object): add more string primitives 2018-11-14 16:51:10 -08:00
Leonardo de Moura
2fa938220b chore(library/init/data/string): cleanup 2018-11-14 14:09:45 -08:00
Leonardo de Moura
dfdf42ce34 chore(library/init/io): minimize io interface 
We are moving to new compiler stack.
 2018-11-14 13:59:25 -08:00
Leonardo de Moura
c599d78639 feat(library/init/io): implement io.iterate in Lean 
cc @kha
 2018-11-14 13:43:02 -08:00
Leonardo de Moura
835b3a10cc chore(library/init): consistent names 2018-11-14 13:08:57 -08:00
Leonardo de Moura
49d779e3a6 fix(library/vm/vm_string): we were not using the builtin implementation for string.decidable_eq 2018-11-14 09:48:43 -08:00
Leonardo de Moura
687e9d076d feat(library/compiler): add _apply and _closure instructions to LLNF 2018-11-07 13:30:28 -08: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
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
12a01d101c refactor(library/compiler/llnf): memory cell reuse instruction set 2018-10-31 09:35:22 -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
bcc4956ca5 feat(library/compiler/llnf): reuse constructor memory cells 
This commit also add two new instructions to the old VM: `updt` and
`updt_cidx`.
They allow us to test the new new memory reuse technique.

TODO: We need to reset fields after we project. Otherwise, we prevent
destructive updates on nested objects.
 2018-10-29 18:46:26 -07:00
Leonardo de Moura
c3d700ece1 feat(library/compiler/csimp): nat.succ x ==> x + 1 2018-10-29 13:53:59 -07:00
Leonardo de Moura
ecf30e93a3 chore(library/vm): remove Destruct instruction 2018-10-29 13:18:33 -07:00
Leonardo de Moura
d871c4f7d8 feat(library/compiler): replace simp_inductive with llnf 2018-10-29 13:07:46 -07:00
Leonardo de Moura
70746b499e chore(library/vm): remove BuiltinCases and NatCases instructions 
They are not needed anymore.
 2018-10-23 15:09:55 -07:00
Leonardo de Moura
3ee863da68 feat(library/compiler/erase_irrelevant): eliminate cases_on for builtin types 2018-10-23 14:58:38 -07:00
Leonardo de Moura
cbbae4b331 chore(library/vm): remove vm_platform and vm_pos_info 2018-10-23 12:55:34 -07:00
Leonardo de Moura
de1dc3be88 chore(library/vm): remove vm_array 
We are currently not using arrays in the old VM.
 2018-10-23 12:49:25 -07:00
Leonardo de Moura
9256618d67 chore(library/vm): remove vm_name 2018-10-23 11:32:56 -07:00
Leonardo de Moura
243b6a70e1 chore(library/vm): remove vm_options 2018-10-23 11:32:56 -07:00
Leonardo de Moura
8d47d2a026 chore(library/vm,library/init/meta): remove vm_format, and some obsolete meta objects 2018-10-23 11:32:56 -07:00
Leonardo de Moura
65815c512c chore(library/vm): remove interaction_state 2018-10-23 11:32:56 -07:00
Sebastian Ullrich
d9208e2b8b feat(library/vm/vm): add profiler.perf_script_file option 
sample usage:
$ lean -Dprofiler.perf_script_file=parser1.script parser1.lean
$ gprof2dot -f perf < parser1.script > parser1.dot
 2018-10-22 15:01:49 +02:00
Leonardo de Moura
5d726eb210 feat(library/compiler/compiler): switch to new compiler frontend 
We also rename `vm_compiler` module to `emit_bytecode`.
We will eventually replace this module with the new IR emitter.
 2018-10-08 17:38:17 -07:00
Leonardo de Moura
2eea3d4c4b chore(library/compiler): simplify procedure class 
Remark: `procedure` will be deleted soon.
 2018-10-05 17:30:27 -07:00
Leonardo de Moura
a21dac4384 chore(library/compiler/vm_compiler): remove option 2018-10-05 17:30:27 -07:00
Leonardo de Moura
cf5141f8ad chore(library/vm/vm): fix style 2018-10-03 13:25:54 -07:00
Leonardo de Moura
13f0a7cd81 chore(frontends/lean, library/vm): save some debugging help code 2018-10-03 13:20:24 -07:00
Leonardo de Moura
85c58e8f0e feat(library/compiler): add support for string literals in the old VM 2018-10-02 18:56:13 -07:00
Leonardo de Moura
dc937281b3 chore(library/init/string): remove string.iterator_imp 2018-10-02 13:46:01 -07:00
Leonardo de Moura
3ac6eab393 chore(library/vm): remove vm_list 2018-10-02 08:44:05 -07:00
Leonardo de Moura
3a4acbee9e chore(library/init/data/string): remove string_imp 
We will use the (to be implemented) `opaque` keyword
 2018-10-01 14:17:11 -07:00
Leonardo de Moura
990fbe3c30 feat(library/compiler): provide options to vm_compile 2018-09-30 08:50:40 -07:00