Leonardo de Moura
bd23f5d63d
feat(frontends/lean/builtin_cmd): improve vm_eval command
2016-05-13 16:15:44 -07:00
Leonardo de Moura
6142fbb1c6
feat(library/vm/vm): check interruptions and memory at invocation
2016-05-13 15:38:48 -07:00
Leonardo de Moura
9e7d8c10ae
perf(library/vm/vm): small optimizations
2016-05-13 15:33:58 -07:00
Leonardo de Moura
11b63b0fcd
fix(util/small_object_allocator): warning
2016-05-13 15:20:32 -07:00
Leonardo de Moura
0c0dec8aa6
feat(library/vm/vm): use small object allocator for VM objects
2016-05-13 14:56:53 -07:00
Leonardo de Moura
92bc367c5c
feat(util): add small object allocator
2016-05-13 14:41:31 -07:00
Leonardo de Moura
752c81a166
fix(library/compiler/nat_value): add expand method, otherwise we may fail to type check terms using nat_value_macro
2016-05-13 12:50:28 -07:00
Leonardo de Moura
f75caddc35
feat(library/vm/vm): rename cases1 to destruct
2016-05-13 12:30:47 -07:00
Leonardo de Moura
4f53cfe5e8
fix(library/vm/vm): std::copy issue
2016-05-13 12:22:28 -07:00
Leonardo de Moura
00bc55af3e
feat(library/vm/vm): improve trace
2016-05-13 12:13:47 -07:00
Leonardo de Moura
dc3d7597ee
chore(library/vm/vm): document VM instructions
2016-05-13 11:54:11 -07:00
Leonardo de Moura
56ec91284b
chore(library/vm/vm): cleanup
2016-05-13 11:06:25 -07:00
Leonardo de Moura
35cf7bf8e2
feat(library/vm/vm): remove atomic from VM object reference counter
...
VM objects should not be shared between different threads.
So, the atomic<unsigned> in the reference counter produces an
unnecessary performance penalty.
2016-05-13 11:00:33 -07:00
Leonardo de Moura
2bd400964c
feat(library/vm/vm): store arguments in reverse order on the stack
...
It simplifies the code for handling closures.
2016-05-13 10:54:29 -07:00
Leonardo de Moura
dbcd609aff
feat(library/vm/vm): disable VM trace in release mode
2016-05-13 10:33:25 -07:00
Leonardo de Moura
039e960799
feat(library/vm/vm): add InvokeBuiltin instruction
2016-05-13 10:28:05 -07:00
Leonardo de Moura
2c0dee5b41
feat(library/vm/vm): cases2 and casesn take pc of first branch too
2016-05-13 10:15:20 -07:00
Leonardo de Moura
7bdf2d4a5a
feat(library/vm/vm): avoid macros
2016-05-13 09:50:07 -07:00
Leonardo de Moura
437fee1919
feat(frontends/lean/builtin_cmds): track runtime
2016-05-13 09:38:18 -07:00
Leonardo de Moura
990d2dc06e
fix(library/vm/vm): typo
2016-05-13 00:45:18 -07:00
Leonardo de Moura
b8b32c2a3b
fix(library/vm/vm): typo
2016-05-13 00:43:09 -07:00
Leonardo de Moura
843f3a69ba
fix(library/vm/vm): memory management
2016-05-13 00:29:20 -07:00
Leonardo de Moura
46c50831fd
fix(library/vm/vm): initialization bug
2016-05-12 23:43:44 -07:00
Leonardo de Moura
06039d95b4
feat(library/vm/vm): add tracing
2016-05-12 23:43:30 -07:00
Leonardo de Moura
8a0b2534bb
fix(library/vm/vm): builtin function invocation
2016-05-12 19:35:28 -07:00
Leonardo de Moura
a533cc56ec
fix(library/vm/vm_nat): typo
2016-05-12 19:34:06 -07:00
Leonardo de Moura
38320fa07c
refactor(library/vm/vm): use locals
2016-05-12 19:06:14 -07:00
Leonardo de Moura
505ab4c0ba
fix(library/vm/vm): uninit var
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2016-05-12 19:03:32 -07:00
Leonardo de Moura
4e9cafb67f
feat(library/vm/vm): add missing swap
2016-05-12 19:01:25 -07:00
Leonardo de Moura
682407b54d
fix(library/vm/vm): incorrect assertion
2016-05-12 18:59:18 -07:00
Leonardo de Moura
8c1238637a
feat(frontends/lean): add vm_eval command
2016-05-12 18:56:31 -07:00
Leonardo de Moura
8a8cafdcdb
fix(library/vm/vm): support for builtin functions
2016-05-12 18:56:13 -07:00
Leonardo de Moura
474737bfb9
feat(library/vm/vm): add very basic display for vm_obj
2016-05-12 18:42:17 -07:00
Leonardo de Moura
6febe9677d
feat(library/vm/vm): add main loop
2016-05-12 18:36:29 -07:00
Leonardo de Moura
9fbf3f2921
feat(library/vm): encode small numerals using scnstr instead of num operation
2016-05-12 16:43:21 -07:00
Leonardo de Moura
de327c0c20
feat(library/vm/vm_nat): add builtin support for nat lt
2016-05-12 16:36:37 -07:00
Leonardo de Moura
df9352ea6e
feat(library/compiler): better support for numeric constants
2016-05-12 16:33:37 -07:00
Leonardo de Moura
f2af5828ba
refactor(library/compiler): preprocess_rec ==> preprocess
2016-05-12 16:03:39 -07:00
Leonardo de Moura
1393238c9d
fix(library/vm/vm_nat): fix constant name
2016-05-12 15:29:14 -07:00
Leonardo de Moura
c48a17563c
feat(library/vm/optimize): add basic bytecode optimizations
2016-05-12 15:24:58 -07:00
Leonardo de Moura
5a7f96a995
refactor(library/vm): simplify initialization
2016-05-12 14:49:06 -07:00
Leonardo de Moura
399b83122c
refactor(library): move vm to a separate directory
2016-05-12 14:45:06 -07:00
Leonardo de Moura
7852247376
feat(compiler/simp_inductive): add optimization for inductive datatypes that have only one constructor C, and C has only one relevant field
2016-05-12 14:24:14 -07:00
Leonardo de Moura
a9f05abbe7
feat(library/compiler,library/vm): add unreachable instruction
2016-05-12 14:01:58 -07:00
Leonardo de Moura
670e7117a2
feat(library/vm): throw error if VM already has code for the given function
2016-05-12 13:50:46 -07:00
Leonardo de Moura
0558214b7c
fix(library/compiler/vm_compiler): emit code for neutral expr
2016-05-12 13:45:05 -07:00
Leonardo de Moura
324ca84b27
feat(frontends/lean/builtin_cmds): keep bytecode
2016-05-12 13:44:45 -07:00
Leonardo de Moura
38bd7e6d10
fix(library/compiler/vm_compiler): typo
2016-05-12 11:54:38 -07:00
Leonardo de Moura
7e7129272f
fix(library/annotation): memory leak
2016-05-12 11:43:45 -07:00
Leonardo de Moura
41786f41f0
fix(library/vm): did not use copy constructor
2016-05-12 11:41:28 -07:00
