Leonardo de Moura
|
a74f02546b
|
refactor(*): remove abbreviation command
|
2016-09-03 17:11:29 -07:00 |
|
Leonardo de Moura
|
a93eada058
|
feat(library/type_context): improved (and simplified) cache management for type_context
|
2016-08-23 17:56:58 -07:00 |
|
Leonardo de Moura
|
803c956d18
|
feat(util/sexpr/option_declarations): allow options to be registered after initialization
|
2016-08-19 16:58:30 -07:00 |
|
Leonardo de Moura
|
cd77f7167e
|
chore(frontends/lean): run_tactic ==> run_command
add `command` as alias for `tactic unit`
|
2016-08-18 12:53:21 -07:00 |
|
Leonardo de Moura
|
ddc3789929
|
feat(frontends/lean): add run_tactic command
This commit also adds the tactic `add_decl`.
|
2016-08-18 10:56:18 -07:00 |
|
Daniel Selsam
|
a9b01991c2
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
Conflicts:
src/frontends/lean/CMakeLists.txt
src/frontends/lean/structure_cmd.h
|
2016-08-17 07:34:03 -07:00 |
|
Sebastian Ullrich
|
751f2d8b02
|
refactor(frontends/lean): delegate all attribute parsing to decl_attributes
|
2016-08-16 13:49:03 -07:00 |
|
Leonardo de Moura
|
11043bc888
|
chore(frontends/lean/builtin_cmds): remove dead code
|
2016-08-11 08:38:39 -07:00 |
|
Leonardo de Moura
|
8ba17af50b
|
fix(frontends/lean/builtin_cmds): non-determinism
|
2016-08-11 08:01:44 -07:00 |
|
Leonardo de Moura
|
594c7ca4c5
|
chore(frontends/lean/find_cmd): remove find_decl command
|
2016-08-03 17:32:47 -07:00 |
|
Leonardo de Moura
|
186d82d58d
|
chore(frontends/lean/builtin_cmds): remove dead code
|
2016-08-02 15:18:05 -07:00 |
|
Leonardo de Moura
|
8993d0738a
|
feat(frontends/lean): remove #elab command
The check command is now using the new elaborator.
|
2016-08-02 15:05:24 -07:00 |
|
Leonardo de Moura
|
9fc222b9af
|
chore(library/pp_options): remove option pp.metavar_args
|
2016-07-31 16:00:21 -07:00 |
|
Leonardo de Moura
|
1aeda0e74b
|
feat(frontends/lean/elaborator): invoke tactics
|
2016-07-31 11:56:52 -07:00 |
|
Sebastian Ullrich
|
e69b508492
|
refactor(library/export_decl): Re-implement for new scoped_ext
Use environment_extension to persist mapping from namespaces to export
decls, use new scoped_ext to keep track of currently active export decls.
|
2016-07-29 23:44:22 -04:00 |
|
Sebastian Ullrich
|
c4edad0372
|
feat(frontends/lean, library): remove attribute and metaclass scoping
All data is now part of either a global, permanent scope or a local,
temporary one
|
2016-07-29 23:44:21 -04:00 |
|
Leonardo de Moura
|
931251d403
|
feat(frontends/lean): remove local_context from parser
|
2016-07-28 16:19:31 -07:00 |
|
Leonardo de Moura
|
de9075b19d
|
chore(frontends/lean/builtin_cmds): support 'sorry' at #elab command
|
2016-07-27 17:09:36 -07:00 |
|
Leonardo de Moura
|
3a5f6f2e64
|
feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result
|
2016-07-27 15:29:25 -07:00 |
|
Leonardo de Moura
|
461b5f289c
|
feat(frontends/lean/elaborator): new elaborator skeleton
|
2016-07-23 19:02:17 -07:00 |
|
Leonardo de Moura
|
d8e6915366
|
fix(frontends/lean/builtin_cmds): fail if expression contain metavars
|
2016-07-19 13:22:10 -04:00 |
|
Leonardo de Moura
|
579f643d1d
|
refactor(library): move kabstract to tactic folder
|
2016-07-18 09:57:02 -04:00 |
|
Leonardo de Moura
|
fbefda9b1c
|
feat(frontends/lean): add commands 'add_key_equivalence' and 'print key_equivalences'
|
2016-07-16 15:41:32 -04:00 |
|
Daniel Selsam
|
9c3b7ad979
|
feat(simplifier/simp_extensions): basic bookkeeping
|
2016-07-04 17:13:19 -07:00 |
|
Leonardo de Moura
|
bd69aacfa8
|
chore(frontends/lean): remove old '#simplify' command
We can use the new tactic framework for testing the simplifier.
|
2016-06-28 11:55:02 +01:00 |
|
Leonardo de Moura
|
e16dbac0db
|
feat(frontends/lean): add declare_trace command
It allows users to define their own tracing classes.
|
2016-06-28 11:45:56 +01:00 |
|
Leonardo de Moura
|
77286e6abb
|
fix(frontends/lean): replay exported decls in imported files
|
2016-06-25 12:13:36 -07:00 |
|
Leonardo de Moura
|
2b43f591c9
|
fix(library/type_context): remove m_cache_owner field
This idiom creates problem if we use (even accidentally) the copy constructor.
|
2016-06-23 14:03:46 -07:00 |
|
Daniel Selsam
|
9327d85f6c
|
chore(library/defeq_simplifier): move to new module inside library/tactic
|
2016-06-22 17:18:57 -07:00 |
|
Leonardo de Moura
|
16c050b66c
|
reactor(library): port fun_info_manager to new type_context (and rename module to fun_info)
|
2016-06-21 10:42:38 -07:00 |
|
Leonardo de Moura
|
f4695c4a1d
|
chore(frontends/lean): remove #defeq_simplify command
|
2016-06-17 10:16:53 -07:00 |
|
Daniel Selsam
|
a4692671e2
|
fix(src/library/defeq_simplifier): incorrect assertion
|
2016-06-14 11:31:46 -07:00 |
|
Daniel Selsam
|
6435dad371
|
fix(src/frontends/lean/builtin_cmds): typo in error message
|
2016-06-14 11:29:03 -07:00 |
|
Leonardo de Moura
|
2279807baf
|
chore(frontends/lean): remove #tactic command
|
2016-06-14 11:28:52 -07:00 |
|
Leonardo de Moura
|
26c10c368a
|
refactor(library): instantiate ==> instantiate_mvars
Motivation: avoid confusion with 'instantiate' procedure for variables
|
2016-06-14 10:29:47 -07:00 |
|
Leonardo de Moura
|
a16e3343a0
|
chore(library,frontends/lean): disable modules that need to be refactored
|
2016-06-14 10:02:11 -07:00 |
|
Leonardo de Moura
|
b821a521b2
|
fix(frontends/lean/builtin_cmds): propagate options
|
2016-06-09 10:56:33 -07:00 |
|
Leonardo de Moura
|
586e9447d1
|
feat(frontends/lean/builtin_cmds): add command #tactic for testing new tactic framework
|
2016-06-08 16:19:41 -07:00 |
|
Leonardo de Moura
|
224203f215
|
feat(library,frontends/lean/builtin_cmds): store export cmds and replay them
see #603
closes #723
|
2016-06-03 12:51:12 -07:00 |
|
Leonardo de Moura
|
0726db6e19
|
refactor(frontends/lean/builtin_cmds): separate open/export parsing from execution
|
2016-06-03 10:57:06 -07:00 |
|
Sebastian Ullrich
|
9561b45af1
|
fix(frontends/lean): uniform handling of declaration compound names
* allow compound names in `namespace` and `structure`
* adjust error messages
Conflicts:
src/frontends/lean/builtin_tactics.cpp
|
2016-06-02 18:13:50 -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
|
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
|
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
|
bf2d2b9feb
|
fix(library/vm,library/compiler,frontends/lean): IO monad support
|
2016-05-25 13:30:43 -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 |
|