Leonardo de Moura
|
f5c35f8d76
|
chore(*): fix compilation warnings
|
2016-08-10 18:03:13 -07:00 |
|
Leonardo de Moura
|
7bb6ccc089
|
refactor(library/init/meta): qexpr ==> pexpr
|
2016-08-05 17:04:36 -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
|
81947e145e
|
feat(library/vm,library/compiler): add support for builtin cases_on
|
2016-06-01 19:06:52 -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
|
f9624b4c49
|
fix(library/compiler/vm_compiler): ignore applications of the form (neutral ...) during code generation
|
2016-05-25 17:52:42 -07:00 |
|
Leonardo de Moura
|
bf9300686c
|
feat(library/compiler/vm_compiler): ignore macro annotations
|
2016-05-25 17:26:15 -07:00 |
|
Leonardo de Moura
|
be7a736a42
|
feat(library/compiler/vm_compiler): trace bytecode after/before optimization
|
2016-05-25 15:45:16 -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
|
5333e07eb9
|
fix(library/compiler/vm_compiler): incorrect assertion
|
2016-05-23 15:10:50 -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
|
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
|
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
|
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
|
c48a17563c
|
feat(library/vm/optimize): add basic bytecode optimizations
|
2016-05-12 15:24:58 -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
|
a9f05abbe7
|
feat(library/compiler,library/vm): add unreachable instruction
|
2016-05-12 14:01:58 -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
|
38bd7e6d10
|
fix(library/compiler/vm_compiler): typo
|
2016-05-12 11:54:38 -07:00 |
|
Leonardo de Moura
|
705317ae77
|
feat(library/compiler): generate bytecode
|
2016-05-11 19:21:47 -07:00 |
|