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
|
53811822d4
|
chore(*): style
|
2016-05-25 18:10:15 -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 |
|
Leonardo de Moura
|
76e2f92d9c
|
feat(frontends/lean/pp): pretty print let-expressions
|
2016-05-25 14:04:28 -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
|
174fba9dbd
|
feat(frontends/lean): add support for monadic 'do'-notation
|
2016-05-24 17:18:15 -07:00 |
|
Leonardo de Moura
|
6a9e5079c9
|
feat(library,frontends/lean/pp): add support for new string encoding
|
2016-05-24 16:20:43 -07:00 |
|
Leonardo de Moura
|
af1908be94
|
feat(frontends/lean/decl_cmds): do not generate warning for definitions that are implemented in the VM
|
2016-05-13 18:17:20 -07:00 |
|
Leonardo de Moura
|
65b9cab9b4
|
feat(frontends/lean/decl_cmds): generate bytecode when adding definitions
Remark: when the code generator fails we just generate a warning.
Reason: code generator does not support wellfounded recursion yet.
|
2016-05-13 18:05:47 -07:00 |
|
Leonardo de Moura
|
c2959dc77b
|
feat(frontends/lean/builtin_cmds): improve error message
|
2016-05-13 16:27:44 -07:00 |
|
Leonardo de Moura
|
bd23f5d63d
|
feat(frontends/lean/builtin_cmd): improve vm_eval command
|
2016-05-13 16:15:44 -07:00 |
|
Leonardo de Moura
|
dc3d7597ee
|
chore(library/vm/vm): document VM instructions
|
2016-05-13 11:54:11 -07:00 |
|
Leonardo de Moura
|
437fee1919
|
feat(frontends/lean/builtin_cmds): track runtime
|
2016-05-13 09:38:18 -07:00 |
|
Leonardo de Moura
|
8a0b2534bb
|
fix(library/vm/vm): builtin function invocation
|
2016-05-12 19:35:28 -07:00 |
|
Leonardo de Moura
|
8c1238637a
|
feat(frontends/lean): add vm_eval command
|
2016-05-12 18:56:31 -07:00 |
|
Leonardo de Moura
|
324ca84b27
|
feat(frontends/lean/builtin_cmds): keep bytecode
|
2016-05-12 13:44:45 -07:00 |
|
Leonardo de Moura
|
705317ae77
|
feat(library/compiler): generate bytecode
|
2016-05-11 19:21:47 -07:00 |
|
Leonardo de Moura
|
dd4d115cc5
|
fix(frontends/lean/structure_cmd): mark recursors generated by structure cmd as auxiliary
|
2016-05-11 14:18:29 -07:00 |
|
Leonardo de Moura
|
ca891c176e
|
feat(frontends/lean/pp): add option pp.hide_comp_irrelevant
It is true by default
|
2016-05-11 11:31:38 -07:00 |
|
Leonardo de Moura
|
de9df69ef6
|
refactor(src): move compiler folder to library
|
2016-05-09 13:28:00 -07:00 |
|
Leonardo de Moura
|
94be486ade
|
fix(frontends/lean/builtin_cmds): generate error if declaration is not a definition
|
2016-05-07 18:39:40 -07:00 |
|
Leonardo de Moura
|
93aa264060
|
feat(frontends/lean/pp): pretty print neutral/unreachable terms
|
2016-05-07 18:30:19 -07:00 |
|
Leonardo de Moura
|
a322f5fe60
|
feat(compiler): start erase_irrelevant
|
2016-05-07 15:27:24 -07:00 |
|
Leonardo de Moura
|
454ec00f17
|
feat(frontends/lean/pp): pretty print recursive calls
|
2016-05-05 18:10:55 -07:00 |
|
Leonardo de Moura
|
a4ec6a3a17
|
feat(compiler, frontends/lean): add 'inline' definitions, and add compiler preprocessing step for unfolding them
|
2016-05-04 16:53:25 -07:00 |
|
Leonardo de Moura
|
da79cd7d95
|
feat(frontends/lean/pp): add option pp.hide_binder_types
|
2016-05-02 18:16:27 -07:00 |
|
Leonardo de Moura
|
85e7003524
|
refactor(compiler): expose primitive for marking computationally irrelevant terms
|
2016-05-02 17:33:49 -07:00 |
|
Leonardo de Moura
|
da8f37d7cc
|
feat(compiler): mark computationally irrelevant terms
|
2016-05-02 16:23:54 -07:00 |
|
Leonardo de Moura
|
bf5e443418
|
feat(frontends/lean): add #compile command back
|
2016-04-28 15:59:38 -07:00 |
|
Leonardo de Moura
|
54f68226f4
|
chore(frontends/lean): disable old tactic framework and blast
|
2016-04-25 16:22:15 -07:00 |
|
Leonardo de Moura
|
fdea718d9d
|
chore(frontends/lean): remove all #include "library/tactic.*" from frontends/lean
|
2016-04-25 15:41:12 -07:00 |
|
Leonardo de Moura
|
d88098f38d
|
chore(frontends/lean): remove some of the tactic support
|
2016-04-25 15:26:56 -07:00 |
|
Leonardo de Moura
|
de64750621
|
chore(frontends/lean): disable expressions that use tactic framework
|
2016-04-25 15:07:26 -07:00 |
|
Leonardo de Moura
|
d66406a1f4
|
feat(frontends/lean): add #elab command for testing new elaborator
|
2016-04-05 17:03:23 -07:00 |
|
Leonardo de Moura
|
03809e7973
|
refactor(frontends/lean): elaborator_context
|
2016-04-05 16:19:06 -07:00 |
|
Leonardo de Moura
|
2577be6344
|
chore(frontends/lean): remove useless elaborator options
|
2016-04-05 16:03:10 -07:00 |
|
Leonardo de Moura
|
a1bc662eca
|
dev(frontends/lean/parser): add local_context
|
2016-03-30 16:33:17 -07:00 |
|
Leonardo de Moura
|
e806700648
|
fix(frontends/lean/builtin_cmds): redeclare_aliases
|
2016-03-30 16:30:18 -07:00 |
|
Leonardo de Moura
|
06ef0ad7be
|
refactor(frontends/lean): add local_level_decls
Remark: the template local_decls will be deleted in the future.
The instances local_expr_decls will be replace by local_context.
|
2016-03-30 15:47:32 -07:00 |
|
Leonardo de Moura
|
c4f25cf15b
|
refactor(frontends/lean): rename elaborate methods
|
2016-03-30 15:05:24 -07:00 |
|
Leonardo de Moura
|
75549bafd7
|
refactor(frontends/lean/elaborator): rename elaborator to old_elaborator
|
2016-03-30 14:59:18 -07:00 |
|
Leonardo de Moura
|
3d238ee943
|
feat(frontends/lean/builtin_cmds): implement #unify using new type_context
|
2016-03-25 15:38:13 -07:00 |
|
Leonardo de Moura
|
c98f1bfd24
|
refactor(library): remove type_util module and implement get_num_args using abstract_type_context
|
2016-03-21 16:30:08 -07:00 |
|
Leonardo de Moura
|
8dde1489f9
|
refactor(library/util): isolate util procedures that depend on old_type_checker
|
2016-03-21 13:36:08 -07:00 |
|
Leonardo de Moura
|
487a1e7f89
|
refactor(kernel): remove extension_context
We replaced it with abstract_type_context
|
2016-03-19 15:15:39 -07:00 |
|
Leonardo de Moura
|
63d8a0ed45
|
refactor(kernel): move justification/constraint/metavar to library
These files will be eventually deleted
|
2016-03-19 14:39:15 -07:00 |
|
Leonardo de Moura
|
e7f1f409c4
|
refactor(kernel): simplify kernel type_checker
TODO: cleanup, move justification/metavar/constraints to library
|
2016-03-18 16:28:42 -07:00 |
|
Leonardo de Moura
|
d8079aa16a
|
refactor(library): create copy of the kernel type_checker in library
Motivation: it will allow us to simplify the kernel type_checker and
make sure it implements the same API provided by type_context
|
2016-03-18 14:34:10 -07:00 |
|
Leonardo de Moura
|
c679c3a8d4
|
dev(kernel/abstract_type_context): extend abstract_type_context API
|
2016-03-08 11:40:36 -08:00 |
|
Leonardo de Moura
|
eaac6ba721
|
chore(library/type_context): rename default_type_context to legacy_type_context and move it to different file
|
2016-03-04 10:26:50 -08:00 |
|