Leonardo de Moura
c7e68e57cf
fix(frontends/lean/structure_cmd): fixes #1681
...
@kha I'm not sure if this is the right fix. I just avoided the loop that adds
`mk_expr_placeholder` if the function is not a projection.
I didn't spend time investigating why we need `mk_proj_app`.
I know the library doesn't compile if we don't use it, and just use
```
return mk_app(copy_tag(ref, mk_constant(S_name + fname)), e);
```
:)
2017-06-19 16:22:38 -07:00
Leonardo de Moura
ddb6b38d88
fix(frontends/lean/elaborator): fixes #1682
...
@kha Could you please double check whether this is right fix?
2017-06-19 16:04:24 -07:00
Leonardo de Moura
0f64b6088c
chore(frontends/lean): remove then have ... notation
...
This notation was a leftover from Lean 0.1.
2017-06-19 14:20:52 -07:00
Sebastian Ullrich
91c77680c8
refactor(init/meta/coinductive_predicates,frontends/lean/inductive_cmds): declare coinductive in Lean
2017-06-19 11:27:12 -07:00
Sebastian Ullrich
018ebdd115
feat(frontends/lean/user_command): add user-defined commands
2017-06-19 11:27:12 -07:00
Sebastian Ullrich
492cb20438
feat(init/meta/{interactive_base,parser}): decl_attributes, decl_meta_info, parser.set_env
2017-06-19 11:27:12 -07:00
Leonardo de Moura
582aa3338b
fix(frontends/lean): compilation warnings with older versions of gcc
2017-06-19 11:14:22 -07:00
Sebastian Ullrich
95b317fa64
refactor(frontends/lean): do not hard code commands accepting attributes & modifiers
2017-06-19 11:09:26 -07:00
Gabriel Ebner
95f8a50a03
fix(frontends/lean/scanner): use platform-independent end-of-file marker
2017-06-19 10:39:08 +02:00
Leonardo de Moura
dc1a1c8540
refactor(library): has_to_string ==> has_repr
...
See issue #1664
This is just the first step to implement proposal described at issue #1664 .
2017-06-18 18:29:19 -07:00
Leonardo de Moura
c33fd8b0fd
fix(frontends/lean/elaborator): fixes #1669
2017-06-18 16:14:48 -07:00
Leonardo de Moura
9b250a2fb8
fix(frontends/lean/interactive): hole_commands
2017-06-15 17:03:40 -07:00
Leonardo de Moura
bf0d785888
feat(library/messages, frontends/lean): optional end position for messages
...
We need this information to be able to fix issues with the transient
message boxes feature (#1667 ).
2017-06-15 10:47:58 -07:00
Leonardo de Moura
5cb96c7fa3
feat(frontends/lean): add option for pretty printing metavars, sorry and delayed abstractions as holes
...
This option is false by default, but true when executing hole commands
2017-06-15 10:24:26 -07:00
Leonardo de Moura
f0e5cc33c3
fix(frontends/lean/interactive): issue at https://github.com/leanprover/lean/pull/1671#discussion_r122243609
2017-06-15 09:43:08 -07:00
Gabriel Ebner
028c31779d
fix(frontends/lean/interactive): revert hole end column
...
I have tested this change in both emacs and vscode, and replacements
work correctly.
This reverts commit 6c2a144950
2017-06-15 17:01:10 +02:00
Leonardo de Moura
e99786afcd
fix(frontends/lean): do not store duplicate holes
2017-06-15 07:53:38 -07:00
Leonardo de Moura
6c2a144950
fix(frontends/lean/interactive): hole end column
2017-06-15 07:36:11 -07:00
Leonardo de Moura
ba25d4876e
feat(frontends/lean/info_manager): multi-line holes
2017-06-15 07:23:06 -07:00
Gabriel Ebner
a001e85d82
fix(frontends/lean/builtin_exprs): set hole position after final token
2017-06-15 11:35:43 +02:00
Gabriel Ebner
437ab1fc27
feat(server): add command to get all holes in a file
2017-06-15 10:23:26 +02:00
Gabriel Ebner
b09fee680c
fix(frontends/lean/info_manager): only store holes once
2017-06-15 10:22:48 +02:00
Leonardo de Moura
3700bb4568
chore(library/tactic/hole_command,frontends/lean/interactive): fix style
2017-06-14 22:23:25 -07:00
Leonardo de Moura
7557a9e000
feat(shell/server,frontends/lean): add "hole_commands" server command
...
The new command returns the list of registered/applicable hole
commands.
2017-06-14 22:16:34 -07:00
Leonardo de Moura
7528e14e68
feat(frontends/lean,shell/server): "hole" command
2017-06-14 21:56:17 -07:00
Leonardo de Moura
55c8627f2c
feat(frontends/lean): {! ... !} takes a list of pre-terms
2017-06-13 22:19:17 -07:00
Leonardo de Moura
bb2c39b471
feat(frontends/lean): add hole notation {! ... !}
...
Holes {! ... !} are elaborated using `sorry`.
We report an error if their value is fixed by typing and/or
elaboration rules.
We store the tactic_state and the optional attribute in the
info_manager. The idea is to allow users to execute commands with
respect to the stored tactic state and optional attribute.
The optional attribute is a pre term.
We are planning to add commands such as:
- Check type of the given argument.
- Reduce the given argument.
- Synthesize the hole automatically, where the given argument encodes
hint to the synthesizer.
- Use the given argument to fill the hole.
2017-06-13 18:53:05 -07:00
Johannes Hölzl
1352d4a5b3
feat(src/frontents/lean): support for coinduction command in frontend
2017-06-12 20:42:48 -07:00
Leonardo de Moura
2a51fc4458
fix(frontends/lean): anonymous constructor and structure instances for private structures
2017-06-07 17:51:23 -07:00
Sebastian Ullrich
dd91630a83
feat(frontends/lean/user_notation): more error checking
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
db08f3f139
fix(frontends/lean/user_notation): check for closedness before evaluating term
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
01c430cd62
fix(frontends/lean/{parser_config,user_notation): persisting user notations
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
56995348d3
hack(frontends/lean/parser): allow input to be substituted and use it to implement interpolating format macro
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
c49f6f7873
refactor(frontends/lean/user_notation): use parser instead of tactic monad
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
20ab8feeae
feat(init/meta/lean/parser): pexpr parser that does not use quoted mode
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
18063fa9ba
feat(frontends/lean): user-defined notation parsers
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
be6f2eada7
chore(*): typos
2017-06-07 10:09:38 -07:00
Sebastian Ullrich
283d8ade1a
fix(library/quote): use opaque macro for elaborated expr quotations
2017-06-07 10:00:17 -07:00
Leonardo de Moura
748eb856c3
fix(frontends/lean): fixes #1649
...
This issue is yet another reason for refactoring how parameters are
represented in Lean.
2017-06-06 21:33:24 -07:00
Gabriel Ebner
1e7e440951
fix(library/module_mgr): actually cancel invalidated tasks
2017-06-05 19:36:09 +02:00
Gabriel Ebner
d03b61635c
fix(frontends/lean/module_parser): end-of-file position
2017-06-05 09:08:38 +02:00
Leonardo de Moura
ca5439c698
feat(frontends/lean/tactic_notation): add support for tac ; [tac_1, ..., tac_n] notation in interactive tactic mode
...
closes #1634
This commit also changes the semantic of `tactic.focus [tac_1, ..., tac_n]`.
It now fails if the number of goals is not `n`.
Before it would only fail if there were more tactics than goals.
@Armael: See tests/lean/run/handthen.lean for examples of the new notation.
2017-06-02 11:38:04 -07:00
Leonardo de Moura
a8173c8194
feat(library/init): heterogeneous andthen type class, and tactic.seq_focus implementation
2017-06-02 10:38:27 -07:00
Leonardo de Moura
d7ab5cd8a1
feat(frontends/lean/tactic_notation): allow show keyword to be used as syntax sugar for the show_goal tactic
...
@kha @gebner I added the `show_goal` tactic for selecting arbitrary
subgoals. This feature is similar to the one available in Isabelle.
This commit allows us to use the `show` keyword as syntax sugar for
`show_goal`. The test `show_goal.lean` has a small example.
What do you think?
@Armael: you can use `show` to structure your proofs in tactic mode.
See `tests/lean/run/show_goal.lean` for a small example.
2017-06-01 18:52:54 -07:00
Sebastian Ullrich
09987df06e
fix(frontends/lean/structure_cmd): do not collect m_ctx_locals multiple times
2017-06-01 07:38:30 -07:00
Sebastian Ullrich
1977b5bfc9
refactor(frontends/lean/structure_cmd): also simplify collecting ctx levels
2017-06-01 07:38:30 -07:00
Sebastian Ullrich
25152bc80d
fix(frontends/lean/structure_cmd): use collect_implicit_locals to catch more context locals
...
Fixes #1623
2017-06-01 07:38:30 -07:00
Leonardo de Moura
e90bb65c7a
fix(frontends/lean/elaborator): make sure coercions from (reflected t) to expr fire when t contains metavariables that can be synthesized by type class resolution
2017-05-31 23:33:48 -07:00
Leonardo de Moura
56215b36e8
fix(*): [[fallthrough]] ==> /* fall-thru */
...
Older gcc compilers generate a warning when the attribute is used.
I found out that GCC 7 will not produce a warning if comments
such as /* fall-thru */ or /* FALLTHRU */ are used instead of the
attribute [[fallthrough]]
2017-05-31 21:18:47 -07:00
Leonardo de Moura
24048c4258
fix(*): gcc 7 weird uninitialized warnings
...
I think most of them are incorrect.
I didn't find a workaround for the one at json.hpp.
So, I just disabled this warning at server.cpp
2017-05-31 18:05:03 -07:00
