Leonardo de Moura
75549bafd7
refactor(frontends/lean/elaborator): rename elaborator to old_elaborator
2016-03-30 14:59:18 -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
9d0dfb8404
refactor(frontends/lean): remove calc_proof_elaborator
2016-03-03 17:22:45 -08:00
Leonardo de Moura
22f3efc5be
remove(frontends/lean): begin_end pre-tactics
...
This was never used
2016-03-03 10:02:09 -08:00
Leonardo de Moura
3c878ecd01
feat(kernel): add let-expressions to the kernel
...
The frontend is still using the old "let-expression macros".
We will use the new let-expressions to implement the new tactic framework.
2016-02-29 16:40:17 -08:00
Leonardo de Moura
f54963bc3e
refactor(library/tactic/expr_to_tactic): remove 'by_plus' support
2016-02-29 13:50:05 -08:00
Leonardo de Moura
15c4bc92b9
refactor(frontends/lean/elaborator): we only need to track one context
2016-02-29 12:49:17 -08:00
Leonardo de Moura
2b1d734544
feat(kernel/expr): remove 'contextual' flag from binder_info
2016-02-29 12:41:43 -08:00
Leonardo de Moura
7d61f640f6
refactor(*): add abstract_type_context class
2016-02-26 14:17:34 -08:00
Leonardo de Moura
2a294bcc17
fix(frontends/lean/elaborator): fixes #996
2016-02-22 17:03:14 -08:00
Leonardo de Moura
632d4fae36
chore(library): rename local_context to old_local_context
2016-02-11 18:15:16 -08:00
Leonardo de Moura
c9e9fee76a
refactor(*): remove name_generator and use simpler mk_fresh_name
2016-02-11 18:05:57 -08:00
Leonardo de Moura
04eaf184a9
feat(frontends/lean,library/unifier): checkpoints at have-expressions
...
@avigad, @fpvandoorn, @rlewis1988, @dselsam
This commit modifies how have-expressions are elaborated.
Now, to process
have H : <type>, from <proof>,
<rest>
we first process the constraints in <type> and <proof> simultaneously.
After all these constraints are solved, the elaborator performs
a Prolog-like cut, and process the constraints in <rest>.
So, all overloads, type classes and coercions in <type> and <proof> are solved
before we start processing <rest>. Moreover, while processing <rest>, we
cannot backtrack to <type> and <proof> anymore.
I fixed all affected proofs in the standard and HoTT libraries in
previous commits pushed today and yesterday. I think most affected proofs were not using a good
style and/or were easy to fix. Here is a common pattern that does not
work anymore.
structure has_scalar [class] (F V : Type) :=
(smul : F → V → V)
infixl ` • `:73 := has_scalar.smul
proposition smul_zero (a : R) : a • (0 : M) = 0 :=
have a • 0 + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
!add.left_cancel this
The `have` doesn't work because Lean can't figure out the type of 0 before
it starts processing `!add.left_cancel this`. This is easy to fix, we just have to
annotate one of the `0`s in the `have`:
proposition smul_zero (a : R) : a • (0 : M) = 0 :=
have a • (0:M) + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
!add.left_cancel this
BTW, all tactics are still being executed after all constraints are solved.
We may change that in the future. I didn't want to execute
the tactics at <proof> before <rest> because of universe
meta-variables. In Lean, unassigned universe meta-variables become
parameters. Moreover, we perform this conversion *before*
we start processing tactics. Reason: universe meta-variables
create many problems for tactics such as `rewrite`, `blast` and `simp`.
Finally, we can recover the previous behavior using the option
set_option parser.checkpoint_have false
2016-02-04 19:01:19 -08:00
Leonardo de Moura
496c84dac6
fix(frontends/lean/elaborator): fixes #982
2016-02-04 15:14:30 -08:00
Leonardo de Moura
0268f92eb4
fix(frontends/lean/elaborator): fixes #965
2016-02-04 13:41:21 -08:00
Leonardo de Moura
8c87f90a29
feat(frontends/lean/elaborator): avoid redudant "don't know how to synthesize placeholder" when using flycheck
2015-12-29 18:00:19 -08:00
Leonardo de Moura
b92416d66c
refactor(library/error_handling): move error_handling to library main dir
2015-12-29 15:31:40 -08:00
Leonardo de Moura
61ecf018e9
feat(frontends/lean,library/tactic): add easy tactic parsing support for at ... and with ...
2015-12-17 12:18:32 -08:00
Leonardo de Moura
7f1800962a
feat(frontends/lean/pp): allow user to override pp.all setting
...
see #922
2015-12-11 10:40:48 -08:00
Leonardo de Moura
725101c777
chore(frontends/lean): cleaup
2015-12-09 12:43:44 -08:00
Floris van Doorn
46739c8b70
feat(hott/algebra): port abstract structures
2015-12-09 12:34:06 -08:00
Leonardo de Moura
5ceac83b6a
feat(frontends/lean/elaborator): restrict the number of places where coercions are considered
...
We do not consider coercions around meta-variables anymore.
2015-11-11 12:37:19 -08:00
Leonardo de Moura
fa3baed701
feat(frontends/lean): add new option (elaborator.coercions) for disabling coercions
2015-11-11 11:57:44 -08:00
Daniel Selsam
ffc168d63a
fix(frontends/lean/elaborator): visit_app partial
2015-11-08 14:05:00 -08:00
Leonardo de Moura
ab940a2001
feat(frontends/lean/elaborator): add support for partial explicit in the elaborator
2015-11-08 14:05:00 -08:00
Leonardo de Moura
b71a68c606
fix(frontends/lean/elaborator): visit_prenum was creating unnecessary universe metavariable
...
This was creating problems for the new type class resolution procedure
since visit_prenum was also not creating any constraint that enforced
the universe level of A to be equal to the superfluous universe level.
2015-11-08 14:04:57 -08:00
Leonardo de Moura
6a36bffe4b
fix(library/class_instance_resolution): bugs in new type class resolution procedure
2015-11-08 14:04:57 -08:00
Leonardo de Moura
d1e111fd6c
fix(hott,frontends/lean,library,library/tactic): make sure we can still compile the HoTT library
2015-11-08 14:04:55 -08:00
Leonardo de Moura
8ee214f133
checkpoint: new numeral encoding
2015-11-08 14:04:55 -08:00
Leonardo de Moura
634c0b5e9d
feat(library/tactic,frontends/lean): propagate new options back to elaborator
2015-09-02 20:34:14 -07:00
Leonardo de Moura
3747ba095a
fix(frontends/lean/elaborator): incorrect assertion
...
It is supposed to be "!first implies is_local(from)"
fixes #807
2015-08-20 17:56:20 -07:00
Leonardo de Moura
21c41f50ea
fix(frontends/lean/elaborator): fixes #803
2015-08-17 14:56:41 -07:00
Daniel Selsam
40471ca8e3
doc(frontends/lean/elaborator): assert invariant in visit_app
2015-08-11 17:02:38 -07:00
Leonardo de Moura
5568085ab9
fix(frontends/lean/elaborator): closes #771
...
Produce nicer error message when type/goal is a metavariable and
universe metavariables have already been instantiated with universe
parameters.
2015-08-07 13:29:22 -07:00
Leonardo de Moura
8f5a760b89
feat(frontends/lean/elaborator): display the whole proof state in option "--goal"
...
see issue #755
2015-07-31 08:56:17 -07:00
Leonardo de Moura
cc4f18c062
feat(frontends/lean): add "--info" command line option for extracting identifier/keyword information
...
see issue #756
2015-07-30 10:18:03 -07:00
Leonardo de Moura
384ccf2b6c
feat(frontends/lean/elaborator): change behavior of "show goal" for incomplete "by tactic"
...
If "by tactic" did not completely solved the goal, then we show the
final state when the user presses "C-c C-g"
2015-07-29 17:34:42 -07:00
Leonardo de Moura
ed41a01a51
fix(frontends/lean/elaborator): fixes #755
2015-07-29 16:41:30 -07:00
Leonardo de Moura
cfa9412f96
fix(frontends/lean): "show goal" localization, add "position", support "by tactic"
2015-07-28 12:48:12 -07:00
Leonardo de Moura
91f83835bb
fix(frontends/lean/elaborator): "show goal" command line option for nested "begin...end" blocks
2015-07-27 20:11:27 -07:00
Leonardo de Moura
0786841c71
feat(frontends/lean): use uniform delimiter
2015-07-27 18:45:33 -07:00
Leonardo de Moura
3fb16d6287
feat(frontends/lean): add "show hole" command line option
2015-07-27 18:42:57 -07:00
Leonardo de Moura
68370d5c8e
feat(frontends/lean): process "show goal" command line option
2015-07-27 17:44:43 -07:00
Leonardo de Moura
b0c56273e2
fix(frontends/lean/elaborator): fixes #724
2015-07-06 15:19:19 -07:00
Leonardo de Moura
c843690d27
fix(frontends/lean/elaborator): fixes #719
2015-07-03 12:37:28 -07:00
Leonardo de Moura
95720b1670
fix(frontends/lean/elaborator): fixes #687
2015-06-28 19:58:57 -07:00
Leonardo de Moura
869ad261c5
fix(frontends/lean/elaborator): fixes #689
2015-06-27 16:19:38 -07:00
Leonardo de Moura
d8620ef4c9
fix(kernel,library,frontends/lean): improve error messages
...
see #669
2015-06-14 19:44:00 -07:00
Leonardo de Moura
3d9b557cfd
feat(frontends/lean): allow the user to mark subterms that should be automatically abstracted into new definitions
...
closes #484
2015-06-12 17:49:26 -07:00
Leonardo de Moura
d547698a56
refactor(library,library/tactic): move class_instance_synth to library
...
This module will be needed by the simplifier
2015-06-01 16:30:40 -07:00
