Sebastian Ullrich
add8836ab2
fix(frontends/lean/{elaborator,parser}): use position of '.' for field notation position
...
Note that flycheck will still highlight the entire word...
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
b92af074c0
feat(kernel/pos_info_provider): add save_pos_info
...
Allows the elaborator to contribute new info locations
2017-03-31 09:40:48 -07:00
Leonardo de Moura
ad859817b1
feat(frontends/lean): allow local decls to shadow namespaces
2017-03-29 16:09:45 -07:00
Leonardo de Moura
71685e4dd6
feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term
...
Replace `^.` with `.` in the stdlib
2017-03-28 17:47:49 -07:00
Leonardo de Moura
87932f1c56
feat(frontends/lean): change notation for inaccessible patterns
...
The following are accepted
.(t)
._
We don't accept .t anymore because it will conflict with the field
access notation.
2017-03-28 16:09:15 -07:00
Leonardo de Moura
6183c7676e
feat(frontends/lean): use . for field access
2017-03-28 15:29:54 -07:00
Leonardo de Moura
07c29c0779
chore(library/abstract_parser,frontends/lean/parser): remove dead code
2017-03-28 11:51:50 -07:00
Sebastian Ullrich
e63c1d3347
refactor(frontends/lean/info_manager): use pos_info
2017-03-27 14:01:19 -07:00
Gabriel Ebner
318910f99b
refactor(frontends/lean/parser): store snapshots in a lazy async list
2017-03-27 14:00:53 -07:00
Gabriel Ebner
2c7b6fc48f
fix(frontends/lean/parser): only show sorry warning once per import
2017-03-24 09:19:17 +01:00
Gabriel Ebner
7442aa0752
fix(frontends/lean/parser): better task description
2017-03-24 07:22:28 +01:00
Gabriel Ebner
a6f7f31e85
refactor(shell,emacs): handle different checking modes in server
2017-03-23 09:07:09 +01:00
Gabriel Ebner
c7ca21625c
feat(util/log_tree): annotate nodes with detail levels
2017-03-23 09:03:43 +01:00
Gabriel Ebner
98f86ccabd
chore(frontends/lean/parser): remove obsolete option
2017-03-23 09:01:00 +01:00
Gabriel Ebner
26ba9c23a7
refactor(util/task): add eager execution
2017-03-23 08:57:56 +01:00
Gabriel Ebner
5f872912e0
refactor(shell/lean): set exit status 1 iff at least one error was reported
2017-03-23 08:57:56 +01:00
Gabriel Ebner
595cbb8fe9
refactor(*): task<T>, log_tree, cancellation_token
2017-03-23 08:57:52 +01:00
Leonardo de Moura
e6c5ba29d6
fix(library/message_builder): remove unnecessary field
...
see #1473
2017-03-22 08:23:29 -07:00
Sebastian Ullrich
f9854be13f
feat(frontends/lean/parser): save id info for non-overloaded constants
2017-03-22 07:35:14 -07:00
Leonardo de Moura
fdadada3a9
fix(frontends/lean): fixes #1468
...
@kha I had to add yet another hack to fix this issue.
In notation declarations, names are resolved at notation declaration time.
So, users do not expect them to be resolved again at tactic execution time.
I addressed this problem by wrapping constants occurring in notation
declarations with a "frozen_name" annotation. This transformation is
only performed if m_in_quote is true.
Then resolve_names_fn at elaborator.cpp will not try to resolve the
names again.
This change broke two other modules. `-` notation for inverting
equations at `rw`, and `calc` expressions inside quotes.
The broke for the same reason. They were not expecting the constants
to be wrapped with an annotation.
2017-03-18 13:48:21 -07:00
Sebastian Ullrich
e0856284b0
feat(frontends/lean,emacs): tactic info before elaboration, fix many edge cases
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
421a6d6f01
feat(frontends/lean/interactive,emacs): highlight current tactic parameter
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
0792bc13db
feat(frontends/lean/elaborator,init/meta/interactive): relax expr pattern elaboration and use it to implement a tactic signature pretty printer
2017-03-17 18:20:44 -07:00
Leonardo de Moura
23935ee390
feat(frontends/lean): allow auto_param notation in structure declarations
...
See #1422
TODO: take the auto_param into account in the `{ ... }` notation.
2017-03-08 15:41:30 -08:00
Sebastian Ullrich
5d68938a9c
feat(frontends/lean): expr literals ```(...)
2017-03-05 08:37:16 -08:00
Leonardo de Moura
1fa1312c57
chore(CMakeLists,frontends/lean): add SAVE_SNAPSHOT=OFF SAVE_INFO=OFF compilation options
2017-02-28 12:09:19 -08:00
Sebastian Ullrich
dfe1874365
refactor(frontends/lean/{parser,util}): extract quote functions
...
Also fixes ``f when f is private
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
1c7ca3f20a
feat(frontends/lean/parser): ignore implicit arguments in expr patterns
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
908a7bd9f3
feat(frontends/lean/parser): expr patterns
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
b9424975b3
refactor(init/meta): replace dynamically-checked quotes where possible
2017-02-17 19:59:57 -08:00
Sebastian Ullrich
9d8c84713c
refactor(*): reduce exception context info from expr to pos_info
2017-02-17 13:45:57 +01:00
Sebastian Ullrich
d15591a2d8
feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters
2017-02-17 13:45:56 +01:00
Leonardo de Moura
6334ff24eb
fix(frontends/lean/tactic_notation): erase position information quoted terms occurring inside `[...]
...
See new test for understanding the problem.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2017-02-09 19:06:56 -08:00
Leonardo de Moura
898894ffaa
feat(frontends/lean/parser): syntax sugar for auto_param gadget
2017-02-09 16:06:55 -08:00
Leonardo de Moura
3d603ec28e
feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs
2017-02-08 17:41:44 -08:00
Leonardo de Moura
32e6442d0a
feat(frontends/lean): no global universes in the frontend
2017-02-08 17:23:04 -08:00
Leonardo de Moura
aa5eea6416
feat(frontends/lean): add scope management to parser_state, remove unnecessary undef_ids
2017-02-08 11:58:14 -08:00
Leonardo de Moura
54f7bf9391
fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages
...
Summary:
We minimize the number of "'sorry' used warning messages". We also
re-target the error to the main declaration. Example: foo._main ==> foo
We do not report for auxiliary declarations such as "_example" and
"foo.equations._eqn_1"
Get rid of the redundant error message "error : failed" for tactics.
We added "silent failures" in the tactic framework.
We do not store line/col information for tactics nested in notation
declarations. Before this commit, we would have tactics such
as (tactic.save_info line col) nested inside of notation declarations.
2017-02-07 20:25:28 -08:00
Gabriel Ebner
cbc0bb1f7c
feat(library/module): store whether we used sorry in olean
2017-02-05 16:35:32 +01:00
Gabriel Ebner
95068e4e79
feat(library/sorry): make sorry a macro
2017-02-05 14:01:03 +01:00
Leonardo de Moura
91b68b6b90
chore(frontends/lean/parser): remove dead variable
2017-02-03 19:55:19 -08:00
Leonardo de Moura
01414cf21c
feat(frontends/lean): add token class, and procedure for consuming the tokens
2017-02-03 18:11:06 -08:00
Leonardo de Moura
3a4ef00f66
feat(frontends/lean): allow constructor parameters to be declared before ':'
2017-01-31 15:11:39 -08:00
Gabriel Ebner
0f96809f7a
fix(frontends/lean/parser): save noncomputable theory flag in snapshots
2017-01-31 11:05:11 -08:00
Leonardo de Moura
4d3ff955d3
feat(frontends/lean): nicer syntax for default parameter values
...
See #1340
2017-01-30 15:54:26 -08:00
Leonardo de Moura
4fe73d3f87
fix(frontends/lean/elaborator, kernel/error_msgs): (re-)activate distinguishing_pp_options
2017-01-30 11:54:00 -08:00
Leonardo de Moura
bf9f7560f7
feat(frontends/lean): (Type u) can't be a proposition
...
(Type u) is the old (Type (u+1))
(PType u) is the old (Type u)
Type* is the old (Type (_+1))
PType* is the old Type*
The stdlib can be compiled, but we still have > 70 broken tests
See discussion at #1341
2017-01-30 11:54:00 -08:00
Gabriel Ebner
5fdc737dfc
feat(library/tactic): store name of current declaration in tactic_state
2017-01-28 08:27:19 +01:00
Leonardo de Moura
0048d0490b
fix(frontends/lean/parser): structure followed by doc string
2017-01-23 10:35:07 -08:00
Leonardo de Moura
c62014df7a
chore(frontends/lean/parser): style
2017-01-20 18:38:58 -08:00
