Leonardo de Moura
|
a6a7daff59
|
refactor(library/vm): avoid constants.txt when creating bindings
|
2016-06-02 11:45:56 -07:00 |
|
Leonardo de Moura
|
a05f8719df
|
fix(library/definitional/equations): fix missing case
|
2016-06-01 19:28:48 -07:00 |
|
Leonardo de Moura
|
35ed68e3c2
|
feat(library/meta): add has_to_string instance for 'name'
|
2016-06-01 19:24:03 -07:00 |
|
Leonardo de Moura
|
4ae7afd8c4
|
fix(library/definitional/equations): potential non-termination
|
2016-06-01 19:23:36 -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
|
4ab84f7374
|
feat(library/init): add unsigned integer
|
2016-06-01 13:06:28 -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
|
e0035f8d29
|
feat(frontends/lean/print_cmd): do not display meta constants when executing 'print axioms' cmd
|
2016-06-01 09:58:23 -07:00 |
|
Leonardo de Moura
|
5382a5a556
|
feat(frontends/lean): allow unbounded recursion in meta_definitions
|
2016-06-01 09:55:07 -07:00 |
|
Leonardo de Moura
|
e7b47a504e
|
feat(frontends/lean): add meta_definition and meta_constant commands
|
2016-06-01 09:12:41 -07:00 |
|
Leonardo de Moura
|
a2c1372d45
|
feat(frontends/lean/builtin_cmds): generate better error message when vm_eval result is a function
|
2016-05-31 19:12:02 -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
|
4e5b8e8d0e
|
fix(library/string): conversion from std::string to lean expr
|
2016-05-31 16:19:01 -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
|
29728c0443
|
feat(library/init/to_string): add fin.has_to_string
|
2016-05-26 12:02:47 -07:00 |
|
Leonardo de Moura
|
62b8c24c7a
|
feat(library/init/to_string): add decidable.has_to_string
|
2016-05-26 11:59:54 -07:00 |
|
Leonardo de Moura
|
c9c08ab833
|
feat(frontends/lean/builtin_cmds): only display vm_eval runtime if --profile is used
|
2016-05-26 11:46:48 -07:00 |
|
Leonardo de Moura
|
3806792866
|
feat(frontends/lean/builtin_cmds): use 'to_string' automatically at vm_eval if type has an instance of has_to_string
|
2016-05-26 11:41:53 -07:00 |
|
Leonardo de Moura
|
6eb377033b
|
chore(library/system/IO): suppress unnecessary universe
|
2016-05-26 11:41:41 -07:00 |
|
Leonardo de Moura
|
a5908ad671
|
feat(library/type_context): process arguments before function in def_eq
|
2016-05-26 11:15:49 -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
|
f60d088572
|
feat(library/init): add 'has_to_string' type class
|
2016-05-26 10:43:26 -07:00 |
|
Leonardo de Moura
|
53811822d4
|
chore(*): style
|
2016-05-25 18:10:15 -07:00 |
|
Leonardo de Moura
|
713c97a3be
|
fix(library/compiler/preprocess): make sure no_confusion is not expanded by expand_aux
|
2016-05-25 17:57:17 -07:00 |
|
Leonardo de Moura
|
d96b3e0172
|
chore(library/data/hlist): make sure we can generate code for hlist.get
|
2016-05-25 17:53:17 -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
|
856f6bcbdf
|
fix(library/compiler/erase_irrelevant): missing case
|
2016-05-25 17:49:02 -07:00 |
|
Leonardo de Moura
|
9530f716f9
|
refactor(library): move list.is_inhabited instance to init folder
|
2016-05-25 17:26: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
|
abd2bbab78
|
feat(library/compiler/preprocess): expand auxiliary declarations automatically created by Lean (e.g., transitivite instances)
These declarations do not have VM bytecode associated with them.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2016-05-25 17:09:16 -07:00 |
|
Leonardo de Moura
|
d763ea1abf
|
chore(tests/lean/run/IO3): remove unnecessary 'open'
|
2016-05-25 16:05:39 -07:00 |
|
Leonardo de Moura
|
4b002e5bf0
|
test(tests/lean/run): add IO test
|
2016-05-25 16:04:54 -07:00 |
|
Leonardo de Moura
|
d4a8d14a9c
|
feat(library/init/nat): put nat instances in the top-level
|
2016-05-25 16:03:21 -07:00 |
|
Leonardo de Moura
|
0239860ad6
|
test(tests/lean/run): add another IO test
|
2016-05-25 15:47:02 -07:00 |
|
Leonardo de Moura
|
c5616969e0
|
fix(library/compiler/simp_inductive): distribute extra cases_on arguments over minor premises in the simp_inductive step
|
2016-05-25 15:46:01 -07:00 |
|
Leonardo de Moura
|
1b8d9deb37
|
chore(library/compiler/erase_irrelevant): style
|
2016-05-25 15:45:43 -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
|
e2d3abd995
|
feat(emacs/lean-syntax): highlight 'return'
|
2016-05-25 15:17:02 -07:00 |
|
Leonardo de Moura
|
1bce20c322
|
feat(library/init): make sure list, char and string decidable_eq instances are defined in the init folder
|
2016-05-25 15:16:12 -07:00 |
|
Leonardo de Moura
|
7c97d88be5
|
feat(frontends/lean/builtin_exprs): add optional curly braces for do-notation
|
2016-05-25 15:15:39 -07:00 |
|