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

88 commits

Author SHA1 Message Date
Leonardo de Moura
6e7b4129e7 chore(library): add helper functions 2016-06-09 16:01:39 -07:00
Leonardo de Moura
2df6fb35e6 feat(library/vm): avoid list<A> eager conversion to vm_obj (for A in {name, level, expr}) 2016-06-09 14:16:32 -07:00
Leonardo de Moura
831a887bdb feat(library/init/meta/format): add trace_fmt 2016-06-09 10:51:49 -07:00
Leonardo de Moura
dde4a46fe3 feat(library/vm): add 'trace' 2016-06-08 16:32:20 -07:00
Leonardo de Moura
a90926a2d0 feat(library/vm/vm_environment): add rest of environment API 2016-06-07 17:51:04 -07:00
Leonardo de Moura
8f10e18f53 feat(library/vm/vm_environment): expose 'environment.add_inductive' 2016-06-07 17:24:43 -07:00
Leonardo de Moura
b28e724709 feat(library/vm): expose 'environment' C++ object 2016-06-07 17:01:17 -07:00
Leonardo de Moura
376bc8a090 feat(library/vm): expose 'declaration' C++ object 2016-06-07 15:38:48 -07:00
Leonardo de Moura
7ff06e1b2c feat(library/meta): exceptional monad 2016-06-07 15:19:43 -07:00
Leonardo de Moura
36c61bc0fb refactor(library/init): cmp_result => ordering 2016-06-07 10:14:07 -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
fb6c9f2879 feat(library/vm/vm_expr): add more functions to 'expr' API 2016-06-06 11:26:19 -07:00
Leonardo de Moura
a55a936db2 feat(library/vm): expose C++ 'expr' object 2016-06-05 21:13:00 -07:00
Leonardo de Moura
1f8c58415e feat(library/vm): expose C++ 'level' object 2016-06-05 12:55:57 -07:00
Leonardo de Moura
7da3fe024a feat(library/vm/vm_rb_map): add rb_map.fold 2016-06-03 17:32:53 -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
163a650ede chore(library/vm): fix style 2016-06-03 16:22:14 -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
1834cab3f2 feat(library/meta): add has_cmp type class 2016-06-03 14:06:46 -07:00
Leonardo de Moura
9a14f7543c feat(library/vm): expose rb_map object 2016-06-03 13:45:06 -07:00
Leonardo de Moura
fe4fafd95d chore(library/vm): remove unnecessary includes 2016-06-03 13:07:06 -07:00
Leonardo de Moura
eafc78f02d feat(library/meta/name): add extra name functions 2016-06-03 09:36:42 -07:00
Leonardo de Moura
3b57246a62 feat(library/meta/format): add 'pp' helper function 2016-06-02 17:57:29 -07:00
Leonardo de Moura
801a57dba1 feat(library/vm): expose C++ 'format' object 2016-06-02 17:37:27 -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
06cb26176c feat(library/vm): expose C++ options object 2016-06-02 11:46:17 -07:00
Leonardo de Moura
417e5ec604 chore(library/vm/vm): typo 2016-06-02 11:46:07 -07:00
Leonardo de Moura
a6a7daff59 refactor(library/vm): avoid constants.txt when creating bindings 2016-06-02 11:45:56 -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
6f02d30185 feat(library/vm): add basic support for C++ name objects in the VM 
We still need to add support for the recursor
 2016-06-01 13:10:24 -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
8bccfc23da feat(library/vm): add example of C function invoking Lean closure 2016-05-31 18:45:14 -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
Leonardo de Moura
e843062be7 feat(library/vm/vm): add support to builtin c-like functions that use the system stack to pass arguments 2016-05-31 16:19:43 -07:00
Leonardo de Moura
3a4a2828d2 chore(library/vm): style 2016-05-26 12:57:34 -07:00
Leonardo de Moura
e89082a97e feat(library/vm,library/init): add builtin timeit primitive for profiling 2016-05-26 12:44:49 -07:00
Leonardo de Moura
93ca755e56 fix(library/vm/vm): vm::execute 2016-05-26 12:41:40 -07:00
Leonardo de Moura
cc4b70e5e5 feat(library/vm/vm_nat): add native support for nat.to_string 2016-05-26 10:55:22 -07:00
Leonardo de Moura
05837a2558 refactor(library/vm): move vm_obj <=> string conversion functions to separate module 2016-05-26 10:47:19 -07:00
Leonardo de Moura
53811822d4 chore(*): style 2016-05-25 18:10:15 -07:00
Leonardo de Moura
bf2d2b9feb fix(library/vm,library/compiler,frontends/lean): IO monad support 2016-05-25 13:30:43 -07:00
Leonardo de Moura
e40c54013a feat(library/vm): add basic support for IO monad 2016-05-24 17:52:22 -07:00
Leonardo de Moura
fd1141d999 fix(library/vm/vm,library/compiler/vm_compiler): invoke n ==> apply 
This change fixes a bug in the VM and simplifies the VM instruction semantics.
 2016-05-23 16:45:42 -07:00
Leonardo de Moura
c3805a9a81 fix(library/vm/optimize): bytecode optimization 2016-05-23 14:35:10 -07:00
Leonardo de Moura
17e3223467 chore(library/vm/vm): add debugging helper procedure 2016-05-23 14:14:43 -07:00