Leonardo de Moura
1150b19598
perf(frontends/lean/elaborator): do not invoke recursive equation compiler when equations still contain metavariables
2015-04-02 23:37:33 -07:00
Leonardo de Moura
242f8ba048
feat(frontends/lean/elaborator): include number of unsolved goals
...
See #509
2015-03-27 14:54:41 -07:00
Leonardo de Moura
bed0d6df6b
fix(frontends/lean/elaborator): inaccessible over coercion
2015-03-13 23:04:45 -07:00
Leonardo de Moura
71ce207080
fix(frontends/lean/elaborator): potential memory access violation
...
Before this commit, the modified method would crash if caching in the
whnf procedure was disabled.
2015-03-11 15:54:50 -07:00
Leonardo de Moura
1490bdad49
feat(frontends/lean): add version of 'exact' tactic (sexact) that enforces goal type during term elaboration
2015-03-06 17:34:45 -08:00
Leonardo de Moura
b73a931c70
fix(frontends/lean/elaborator): missing case 'no-equation' annotation
2015-03-05 14:37:29 -08:00
Leonardo de Moura
039afb4578
feat(frontends/lean): treat "proof t qed" as alias for "by exact t"
2015-03-05 11:12:39 -08:00
Leonardo de Moura
c81762970e
fix(frontends/lean/elaborator): revert commit ededf4fc6c
...
The instantiate_all are needed. See issue #457
2015-03-02 13:00:54 -08:00
Leonardo de Moura
ededf4fc6c
feat(frontends/lean): remove unnecessary instantiate_all's that were messing with error localization
2015-03-01 14:51:44 -08:00
Leonardo de Moura
c772d7bf84
fix(frontends/lean/elaborator): unassigned metavariable when using nested begin-end blocks
...
Closes #454
2015-02-28 09:03:56 -08:00
Leonardo de Moura
cf56935b01
feat(frontends/lean): improve support for user defined tactics
2015-02-27 16:58:25 -08:00
Leonardo de Moura
909ebfc5f1
feat(frontends/lean/elaborator): try coercions after each overload
...
We try only the easy cases since the more general case is too expensive.
closes #444
2015-02-24 17:41:20 -08:00
Leonardo de Moura
1ff6446a63
feat(frontends/lean): nested begin-end blocks
2015-02-24 11:59:27 -08:00
Leonardo de Moura
7fc216183e
feat(library/tactic): produce better error message when a tactic fails
...
closes #348
2015-02-16 18:42:15 -08:00
Leonardo de Moura
dbc8e9e13a
refactor(*): add method get_num_univ_params
2015-01-28 17:22:18 -08:00
Leonardo de Moura
e4b5e07498
fix(frontends/lean/elaborator): apply substitution before compiling pre-tactics into tactics
...
closes #415
2015-01-28 13:32:56 -08:00
Leonardo de Moura
4f2e0c6d7f
refactor(frontends/lean): add 'attribute' command
...
The new command provides a uniform way to set declaration attributes.
It replaces the commands: class, instance, coercion, multiple_instances,
reducible, irreducible
2015-01-24 20:23:21 -08:00
Leonardo de Moura
27f6bfd3f0
refactor(*): add file constants.txt with all constants used by the Lean binary
2015-01-23 16:50:32 -08:00
Leonardo de Moura
dfbe6662be
feat(frontends/lean/elaborator): add option 'elaborator.fail_if_missing_field'
2015-01-19 17:47:39 -08:00
Leonardo de Moura
f9d7480f5c
feat(frontends/lean): notation for creating structure instances
2015-01-16 17:14:30 -08:00
Leonardo de Moura
e48df78938
feat(frontends/lean/elaborator): do not apply delayed_coercions on equation lhs
...
The variables in the equation lhs do not have type at preprocessing
time (i.e., their type is a metavariable). So, they may seem candidates
for delayed_coercions. If the coercions are injected, we will not be
able to pattern match. Thus, we disable coercions in this case.
2015-01-13 18:05:22 -08:00
Leonardo de Moura
37e852ba61
feat(frontends/lean/elaborator): improve error message for metavariable in inaccessible position on equation lhs
2015-01-13 14:38:25 -08:00
Leonardo de Moura
4f519be55e
fix(frontends/lean/elaborator): compilation problem
2015-01-11 20:58:41 -08:00
Leonardo de Moura
5796640392
fix(frontends/lean): do report unassigned metavariables in equation lhs
2015-01-10 10:39:47 -08:00
Leonardo de Moura
6df9ffe5f6
fix(frontends/lean/elaborator): solve placeholders before invoking equantions compiler
2015-01-10 09:18:27 -08:00
Leonardo de Moura
a9b6e20a22
fix(frontends/lean): save equations position
2015-01-06 15:55:04 -08:00
Leonardo de Moura
4421069e34
refactor(library/tactic): rename placeholder_elaborator to class_instance_synth
2014-12-19 19:57:38 -08:00
Leonardo de Moura
ded869b7e0
refactor(frontends/lean): move placeholder_elaborator to library/tactic
2014-12-19 15:23:22 -08:00
Leonardo de Moura
69750c50c6
refactor(frontends/lean): move pp_options to library
2014-12-19 15:00:05 -08:00
Leonardo de Moura
02de288a51
refactor(frontends/lean): move choice_iterator to library
2014-12-19 14:29:32 -08:00
Leonardo de Moura
8939351903
refactor(library): add compile_equations function, generic_exception, and cleanup elaborator_exception
2014-12-15 19:22:17 -08:00
Leonardo de Moura
ab873cfff9
feat(frontends/lean/elaborator): replace metavariables in the equation lhs with fresh local constants before invoking compiler
2014-12-11 19:51:49 -08:00
Leonardo de Moura
91ce99d921
feat(frontends/lean): type check 'decreasing' proofs in definition using well-founded recursion
2014-12-11 18:13:35 -08:00
Leonardo de Moura
b8f665e561
feat(frontends/lean): elaborate recursive equations
...
Remark: we are not compiling them yet.
2014-12-10 22:25:40 -08:00
Leonardo de Moura
756fae7c2a
refactor(frontends/lean): move local_context to library
2014-12-10 12:43:32 -08:00
Leonardo de Moura
366bf70ccd
fix(frontends/lean/elaborator): do not display flycheck related messages when --flycheck is not on
2014-11-28 21:20:25 -08:00
Leonardo de Moura
8b804f1d22
feat(frontends/lean): add option 'elaborator.flycheck_goals'
2014-11-28 16:34:02 -08:00
Leonardo de Moura
9516cd9ee3
feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression
...
Actually, the elaborator is the one reporting the unassigned
placeholders. The 'exact' tactic just makes the request.
To implement this feature we had to extend the elaboration interface
expected by the tactic framework.
2014-11-28 14:59:35 -08:00
Leonardo de Moura
db9fd53b80
fix(library/tactic): pretty printer for proof states
2014-11-27 09:43:58 -08:00
Leonardo de Moura
ffdeb0edc4
fix(frontends/lean/elaborator): unsolved metavariables, fix #329
2014-11-26 11:56:39 -08:00
Leonardo de Moura
24a15b6c46
fix(frontends/lean): disable class-instance resolution when executing find_decl, fixes #343
2014-11-24 21:33:52 -08:00
Leonardo de Moura
76fb6893e1
feat(frontends/lean): add elaborator.trace_instances option
...
When on this option allows us to visualize "class-instance resolution"
2014-11-09 11:24:19 -08:00
Leonardo de Moura
3bfe5b0b7e
fix(frontends/lean): type information for "atomic" notation declaration, fixes #292
2014-11-04 18:01:20 -08:00
Leonardo de Moura
fa405d7884
refactor(frontends/lean): combine info annotations in a single module
2014-11-04 18:01:20 -08:00
Leonardo de Moura
57b19b787b
feat(frontends/lean/calc_proof_elaborator): when 'elaborator.calc_assistant' is on, generate same info that is generated if ! was used
2014-10-31 09:49:45 -07:00
Leonardo de Moura
dc7ab17d2a
feat(frontends/lean/calc_proof_elaborator): add 'elaborator.calc_assistant' option
2014-10-31 09:49:45 -07:00
Leonardo de Moura
c5a62f8abb
feat(frontends/lean): insert ! in calculational proofs when needed
...
This is part of #268
2014-10-30 22:22:04 -07:00
Leonardo de Moura
498b2f681e
feat(frontends/lean/placeholder_elaborator): better error message for ambiguous class-instance resolution
2014-10-30 14:44:58 -07:00
Leonardo de Moura
dcd7e53fa7
feat(frontends/lean/builtin_cmds): remove workaround for getting nice metavariable names in the check command
...
We don't need it anymore after previous commit 2a16050
2014-10-30 13:12:45 -07:00
Leonardo de Moura
2a160508c3
feat(frontends/lean): lean --server should display meta-variables using the approach used in check command, closes #280
2014-10-30 12:45:41 -07:00
Leonardo de Moura
a98b12f067
fix(frontends/lean/elaborator): incorrect error position in begin-end block, fixes #276
2014-10-29 16:51:06 -07:00
Leonardo de Moura
1c9992800f
fix(frontends/lean/info_manager): suppress useless tactic type information, closes #277
2014-10-29 16:51:06 -07:00
Leonardo de Moura
0c185fc4ab
fix(library/tactic): add relax_main_opaque flag to proof_state objects, closes #274
2014-10-29 08:57:34 -07:00
Leonardo de Moura
83e4c0fcec
feat(frontends/lean): hide tactic "types"
...
it is not very useful to display the type of tactics (e.g., apply,
intros, ...)
2014-10-28 22:38:10 -07:00
Leonardo de Moura
eeb6c72508
feat(frontends/lean): modify begin-end semantics, closes #258
2014-10-28 22:15:38 -07:00
Leonardo de Moura
7516fcad97
feat(kernel/type_checker): add is_stuck method, and improve ensure_pi method, closes #261
2014-10-27 13:16:50 -07:00
Leonardo de Moura
2e5ad274a5
fix(frontends/lean/elaborator): remove invalid assertions
...
These assertions became invalid when we changed the behavior of undef
indentifiers at
8e6de93394
2014-10-27 10:31:09 -07:00
Leonardo de Moura
81dc201bab
fix(frontends/lean/elaborator): nested begin-end bug
2014-10-26 18:23:30 -07:00
Leonardo de Moura
a544d32fcf
fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders
2014-10-26 16:11:58 -07:00
Leonardo de Moura
f027acb5cb
fix(frontends/lean): missing type info in expressions nested in tactics
2014-10-23 18:31:05 -07:00
Leonardo de Moura
e750c9b67a
feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode
2014-10-23 13:18:30 -07:00
Leonardo de Moura
2c330e704e
fix(frontends/lean/elaborator): error localization for 'expr_to_tactic' failures
2014-10-23 10:26:19 -07:00
Leonardo de Moura
7c62446023
refactor(frontends/lean): remove dead code
2014-10-22 17:39:06 -07:00
Leonardo de Moura
5e15ac0c92
feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics
2014-10-22 17:29:50 -07:00
Leonardo de Moura
f0cc17af87
fix(frontends/lean/elaborator): missing type information when ! operator (aka consume_args) is used
2014-10-20 08:31:36 -07:00
Leonardo de Moura
b94d121580
refactor(library): move flycheck "helper" classes to separate module
2014-10-15 09:08:04 -07:00
Leonardo de Moura
fc01edee4d
fix(frontends/lean/elaborator): perform translation using "user-level" names
2014-10-14 17:53:24 -07:00
Leonardo de Moura
58c9421bab
refactor(library/tactic): elaborate expressions nested in tactics with respect to current goal, save postponed constraints (e.g., flex-flex constraints) closes #44 , fixes #70
2014-10-14 17:18:40 -07:00
Leonardo de Moura
a26618e0f2
feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied
2014-10-12 13:06:00 -07:00
Leonardo de Moura
5e6ff3eef3
fix(frontends/lean/elaborator): bug when reporting error position
2014-10-10 17:31:12 -07:00
Leonardo de Moura
3d65b1c25c
fix(frontends/lean/elaborator): incorrect type information being reports in lean-mode, fixes #241
2014-10-10 15:41:55 -07:00
Leonardo de Moura
052bc6ff20
fix(frontends/lean/elaborator): better specific universe detection
2014-10-09 14:43:07 -07:00
Leonardo de Moura
8947bf4347
feat(frontends/lean): display type of binders, closes #238
2014-10-08 22:54:10 -07:00
Leonardo de Moura
d445857f56
fix(frontends/lean): change how "as-is" expressions are handled
...
Implicit arguments are consumed.
2014-10-08 22:23:20 -07:00
Leonardo de Moura
8fa171cb92
refactor(library/unifier): allow general 'unify' procedure to take an initial substitution as argument
2014-10-07 17:30:57 -07:00
Leonardo de Moura
16041e4948
fix(frontends/lean/elaborator): 'as-is' expressions
...
The elaborator should not introduce implicit arguments on terms marked
as 'as-is'.
2014-10-07 16:38:31 -07:00
Leonardo de Moura
531de7990d
refactor(frontends/lean/tactic_hint): simplify tactic_hints
2014-10-07 11:34:58 -07:00
Leonardo de Moura
64f6601fe3
fix(frontends/lean/proof_qed_elaborator): information about synthesized variables in a proof-qed block was being lost
2014-10-04 09:15:42 -07:00
Leonardo de Moura
a1bb6d6017
refactor(frontends/lean/elaborator): expose elaborator class
2014-10-03 16:10:36 -07:00
Leonardo de Moura
dccf8a3a75
chore(frontends/lean/elaborator): fix field name
2014-10-03 15:34:23 -07:00
Leonardo de Moura
4cb54ac825
feat(frontends/lean/elaborator): more strict test for bad universe solution
2014-10-02 14:29:51 -07:00
Leonardo de Moura
98e66586e9
feat(frontends/lean/elaborator): elaborator rejects 'Type' if the universe is explicit
2014-10-02 14:29:51 -07:00
Leonardo de Moura
153e3927ac
feat(frontends/lean/elaborator): modify '!' semantics: it stops consuming arguments as soon it finds an argument that does not occur in the rest of the type.
2014-10-01 18:50:17 -07:00
Leonardo de Moura
ead827d6b7
feat(frontends/lean): add ! operator the "dual" of @, closes #220
2014-10-01 17:13:41 -07:00
Leonardo de Moura
2730e5163e
feat(frontends/lean): allow 'sorry' implicit argument to access the whole context, and avoid cryptic error message
...
See new test for explanation.
2014-09-30 18:04:04 -07:00
Leonardo de Moura
9c55bbb871
feat(frontends/lean/elaborator): report an error when Type becomes a Prop after elaboration, closes #208
2014-09-29 08:18:10 -07:00
Leonardo de Moura
c775da16ec
feat(frontends/lean/elaborator): discard partial solution during
...
class-instance resolution, use only tactic_hints associated with
classes, enforce is_strict
2014-09-25 19:46:08 -07:00
Leonardo de Moura
318fec43a4
feat(frontends/lean/elaborator): use tactic_hints for unsolved placeholders
2014-09-25 17:54:10 -07:00
Leonardo de Moura
bb1c6d44ac
fix(frontends/lean/elaborator): missing register_meta
2014-09-25 17:52:36 -07:00
Leonardo de Moura
8747f12118
refactor(frontends/lean/elaborator): remove unnecessary
...
set_local_context_for method
2014-09-25 10:21:31 -07:00
Leonardo de Moura
b8eb65aac2
perf(frontends/lean/placeholder_elaborator): reuse local_context, this
...
is possible now because local_context is a mainly "functional object"
2014-09-25 10:11:41 -07:00
Leonardo de Moura
2e2d2d21f1
refactor(local_context): local_context::scope auxiliary object is not
...
needed anymore
2014-09-25 09:59:27 -07:00
Leonardo de Moura
09162e5fea
refactor(frontends/lean/local_context): remove name_generator from local_context
2014-09-25 09:44:34 -07:00
Leonardo de Moura
354c456639
refactor(frontends/lean/local_context): move mvar2meta mapping to elaborator
2014-09-25 09:31:03 -07:00
Leonardo de Moura
fce1113b80
refactor(frontends/lean/coercion_elaborator): simplify
...
coercion_elaborator interface
2014-09-25 08:48:31 -07:00
Leonardo de Moura
a61b95a87e
refactor(frontends/lean/proof_qed_elaborator): simplify
...
proof_qed_elaborator interface
2014-09-25 08:38:02 -07:00
Leonardo de Moura
29d6bff785
refactor(frontends/lean): explicit initialization/finalization
2014-09-23 10:00:36 -07:00
Leonardo de Moura
b1ee888aae
refactor(*): start move to explicit initialization/finalization,
...
explicitly initialize/finalize options
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-22 10:41:07 -07:00
Leonardo de Moura
fd5daa8fda
feat(frontends/lean): use coercions to function-class and sort-class in
...
function arguments, closes #203
2014-09-20 09:00:10 -07:00
Leonardo de Moura
08ccd58eb6
feat(frontends/lean): add 'reducible' modifier for controlling which
...
definitions are unfolded during elaboration
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-19 15:54:32 -07:00
