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

83 commits

Author SHA1 Message Date
Leonardo de Moura
e248577e1c feat(library/vm): allow vm bytecode to invoke native closures 2016-12-14 19:16:55 -08:00
Leonardo de Moura
b0ce461fcd feat(library/vm): native closures that do not depend on vm_state 
Remark: native_closures are used in the C++ code generator.
 2016-12-14 18:51:24 -08:00
Leonardo de Moura
fe3396e1ae perf(library/vm/vm): cache the result of 0-ary vm_decls 2016-12-12 09:12:06 -08:00
Leonardo de Moura
e59515df5f chore(*): fix style 2016-12-05 16:39:58 -08:00
Jared Roesch
e65d90ac79 feat(*): C++ code generator 
in progress move of Lean.native to init
 2016-12-05 16:11:41 -08:00
Gabriel Ebner
7db2b8d014 fix(library/vm/vm): do not segfault in single-threaded builds 2016-12-02 16:51:10 -08:00
Gabriel Ebner
a8df381d20 feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
Leonardo de Moura
31e159b80c fix(library/vm/vm): bug at add_native 2016-11-21 16:58:22 -08:00
Leonardo de Moura
91c8ff746f feat(cli_debugger): add commands for traversing stack frames 2016-11-16 12:37:18 -08:00
Leonardo de Moura
3628870121 feat(library/tactic/vm_monitor): extend VM introspection API 2016-11-15 15:05:46 -08:00
Leonardo de Moura
fffe69fdf9 feat(library/vm,library/tactic/vm_monitor): use optionT to define vm monad 2016-11-14 16:13:56 -08:00
Leonardo de Moura
7232e3a076 feat(library/vm/vm): invoke debugger (aka vm_monitor) 2016-11-14 14:45:49 -08:00
Leonardo de Moura
a7344671e1 feat(library/vm/vm): add stack_info 2016-11-13 12:20:02 -08:00
Leonardo de Moura
381b2edaf7 feat(library/vm/vm): store .olean file name at vm_decl's 2016-11-11 16:19:19 -08:00
Leonardo de Moura
e673fa65ba feat(library/vm/vm): Store position information at vm_decl's 2016-11-11 15:39:32 -08:00
Leonardo de Moura
b79b76db83 feat(library/compiler/vm_compiler): improve local_info collection 2016-11-09 12:18:44 -08:00
Leonardo de Moura
6b3da2daf4 feat(library/compiler/vm_compiler): save local_info for let-expressions 2016-11-08 15:50:38 -08:00
Leonardo de Moura
d66584f390 feat(library/vm,library/compiler): save argument names 2016-11-08 15:10:04 -08:00
Gabriel Ebner
e88b97d46d fix(library/vm/vm): initialize m_total_time field 2016-11-07 15:03:25 -08:00
Leonardo de Moura
1dcc21525a chore(library/vm/vm): style 2016-11-04 09:55:20 -07:00
Leonardo de Moura
5075891f66 chore(library/vm/vm): fix gcc 4.8 warning 2016-11-04 09:46:16 -07:00
Gabriel Ebner
ef1fc9871b feat(library/vm/vm): profiler: show cumulative runtimes 2016-11-04 09:39:12 -07:00
Leonardo de Moura
9465f25f09 feat(library/vm): profiler for VM bytecode 2016-11-03 21:15:29 -07:00
Leonardo de Moura
6b582ca6c3 fix(library/vm/vm): bug at get_constant 2016-10-04 01:58:39 -07:00
Leonardo de Moura
545b89d556 fix(library/vm): memory violation 2016-10-04 00:09:52 -07:00
Leonardo de Moura
4ee9554c96 fix(library/vm/vm): reference may be invalidated when the vector is resized 2016-10-03 21:31:17 -07:00
Leonardo de Moura
a0a7e22bb7 fix(library/vm/vm): uninitialized variable 2016-10-03 21:25:30 -07:00
Leonardo de Moura
4a2946f5dd feat(library/tactic/eval): eval_expr for arbitrary expressions 2016-10-03 19:01:22 -07:00
Leonardo de Moura
12eb886f49 refactor(library/vm/vm): remove parray 2016-10-03 17:26:03 -07:00
Leonardo de Moura
7465529445 feat(library/tactic): 'eval_expr' tactic skeleton 2016-10-03 16:26:28 -07:00
Leonardo de Moura
199decea51 fix(library/tactic/tactic_state): remove problematic get_tactic_vm_state 2016-08-23 07:38:44 -07:00
Leonardo de Moura
7bb6ccc089 refactor(library/init/meta): qexpr ==> pexpr 2016-08-05 17:04:36 -07:00
Leonardo de Moura
5ffbc2f94e fix(library/vm/vm): memory leak 2016-08-01 23:06:53 -07:00
Leonardo de Moura
a30603405c feat(library/vm/vm): add scope_vm_state 2016-07-15 15:10:04 -04:00
Leonardo de Moura
d604cb8b4e feat(library/vm/vm): add friendly invoke method 2016-06-24 15:49:40 -07:00
Leonardo de Moura
586baa4118 feat(library,frontends/lean): support for quoted expressions in the VM, compiler and frontend 
TODO: invoke elaborator at tactic.to_expr
 2016-06-15 16:06:39 -07:00
Leonardo de Moura
6e7b4129e7 chore(library): add helper functions 2016-06-09 16:01:39 -07:00
Leonardo de Moura
6157c66ac3 feat(library/vm/vm): allow vm_external subclasses to use their own memory allocation policy 2016-06-06 12:50:55 -07:00
Leonardo de Moura
a55a936db2 feat(library/vm): expose C++ 'expr' object 2016-06-05 21:13:00 -07:00
Leonardo de Moura
9eb9be2911 fix(library/vm/vm): make sure objects are not garbage collected at invoke_cfun when the VM stack is resized 2016-06-03 17:31:47 -07:00
Leonardo de Moura
b5ca231cdf fix(library/vm/vm): problems detected when using valgrind 2016-06-03 16:55:01 -07:00
Leonardo de Moura
5a9a5dabd6 perf(library/vm/vm): improve performance of invoke_closure 2016-06-03 15:39:18 -07:00
Leonardo de Moura
924f3629ee feat(library/vm): expose name of the C++ functions that implement builtins 2016-06-02 12:48:43 -07:00
Leonardo de Moura
81947e145e feat(library/vm,library/compiler): add support for builtin cases_on 2016-06-01 19:06:52 -07:00
Leonardo de Moura
e72a8f4a9b feat(library/vm/vm): add support for builtin constants 2016-06-01 13:05:39 -07:00
Leonardo de Moura
d1e37f1948 fix(library/vm/vm): invoke_closure 2016-05-31 18:44:53 -07:00
Leonardo de Moura
032750f4cb feat(library/vm/vm): add dynamic declare_vm_builtin 2016-05-31 17:42:42 -07:00
Leonardo de Moura
b31a7bd3e7 feat(library/vm): use cfunction style for nat and IO primitives 2016-05-31 17:22:27 -07:00
Leonardo de Moura
faf70ed58c feat(library/vm/vm): add support for declaring builtin cfunctions 2016-05-31 16:48:11 -07:00
Leonardo de Moura
25903645a7 feat(library/vm/vm): add some sanity checking 2016-05-31 16:29:01 -07:00