Sebastian Ullrich
07b1cfb268
fix(frontends/lean/structure_cmd): do not combine field default overrides and parent field short-hands
...
Fixes #1557
2017-05-02 13:42:15 +02:00
Leonardo de Moura
55fee26b36
feat(library/class): add attribute for tracking symbols occurring in instances of type classes
...
For more information see:
https://github.com/leanprover/lean/wiki/Refactoring-structures
The new attribute [algebra] implements the [algebraic_class] described
in the page above.
2017-05-01 18:02:30 -07:00
Daniel Selsam
8b8814cfbe
fix(frontends/lean/inductive_cmd.cpp): fixes #1525
2017-05-01 14:57:25 -07:00
Gabriel Ebner
3810e8950d
refactor(util/lean_path,util/path): separate search path functions
2017-05-01 14:11:38 -07:00
Gabriel Ebner
d79909a1b8
refactor(util/lean_path): support leanpkg.path files
2017-05-01 14:11:38 -07:00
Gabriel Ebner
baa4c48f1f
refactor(util/lean_path): explicitly pass around search path
2017-05-01 14:11:38 -07:00
Leonardo de Moura
ba5eccdca8
refactor(library/init/core): rename out_param => inout_param
...
It is really input/output.
2017-05-01 14:01:41 -07:00
Leonardo de Moura
66a1fec94e
feat(library/init/category): add has_orelse type class
2017-05-01 09:58:27 -07:00
Leonardo de Moura
5cef84709f
refactor(library): avoid auxiliary definitions such as add/mul/le/etc
...
See Section "Other goodies" at
https://github.com/leanprover/lean/wiki/Refactoring-structures
This commit also improves the support for projections in the
unifier/matcher.
Now, we consider the extra case-split for projections.
Given a projection `proj`, and the constraint `proj s =?= proj t`, we need to try first `s =?= t` and if it fails, then try to reduce.
This is needed in the standard library because we now have constraints such as:
```
@has_le.le ?A ?s ?a ?b =?= @has_le.le nat nat.has_add x y
```
If we reduce the right hand side, we get the unsolvable constraint
```
@has_le.le ?A ?s ?a ?b =?= nat.le x y
```
Before this change, the constraint was `@le ?A ?s ?a ?b =?= @le nat nat.has_add x y`, and we already perform a case-split in this case.
Moreover, projections were eagerly reduced whenever possible.
The extra case-split generates a performance problem in several tests. For example `fib 8 = 34` was timing out.
I worked around this issue by performing the case-split only when the constraint contains meta-variables.
There are also minor issues. Example. `<` is notation for `has_lt.lt`, but `>` is for `gt`.
2017-05-01 08:52:19 -07:00
Gabriel Ebner
3e2e9ed98a
fix(frontends/lean/module_parser): make the #exit command end at the end of the file
...
Fixes #1553 .
2017-05-01 13:22:26 +02:00
Gabriel Ebner
8554b8eac1
fix(frontends/lean/pp): insert line breaks in notations
2017-05-01 13:13:07 +02:00
Gabriel Ebner
ca2eab3a2f
fix(frontends/lean/structure_cmd): instantiate universe levels in projections to parents
2017-04-29 15:00:17 +02:00
Johannes Hölzl
9535a14e94
fix(frontent/lean/elaborator): check if field is found in structure update
...
Fixes #1549
2017-04-28 17:42:07 +02:00
Sebastian Ullrich
0ca6e2c96f
refactor(library/{type_context,compiler/preprocess},frontends/lean/elaborator): use opaque, general type class instead of special app elaboration for eval_expr
2017-04-27 16:04:59 -07:00
Gabriel Ebner
271d8ca47a
fix(frontends/lean/definition_cmds): make sure auxiliary definitions introduced by abstract do not clash
2017-04-27 16:04:18 -07:00
Gabriel Ebner
5324f8c3d3
fix(frontends/lean/definition_cmds): use real name as prefix for abstracted proofs
2017-04-27 16:04:18 -07:00
Gabriel Ebner
a7d58008ac
fix(frontends/lean/parser): show exception message in import errors
2017-04-27 16:04:18 -07:00
Leonardo de Moura
f4ebd38ce3
feat(frontends/lean/builtin_exprs): improve infix paren notation
...
After this commit, `(+)` is notation for (add) instead of `(fun x y, add x y)`.
This change is relevant when defining type class instances such as
```lean
instance semigroup_to_is_associative [semigroup α] : is_associative α (*) :=
⟨mul_assoc⟩
```
2017-04-27 12:33:33 -07:00
Sebastian Ullrich
cfbc449769
refactor(frontends/lean/structure_cmd): some more cleanup
2017-04-26 14:22:46 -07:00
Sebastian Ullrich
d968b9a1c8
fix(frontends/lean/structure_cmd): remove evil Pi overload that accidentally abstracted constants in structure decls
2017-04-26 14:22:36 -07:00
Sebastian Ullrich
0d02136a09
fix(frontends/lean/inductive_cmds): do not whnf pre-exprs
...
Fixes #1507
2017-04-25 17:47:29 -07:00
Sebastian Ullrich
dd1f3e5f8c
fix(frontends/lean/structure_cmd): reject internal field names
...
Fixes #1539
2017-04-25 17:47:08 -07:00
Sebastian Ullrich
e9a6c544af
refactor(frontends/lean/{elaborator,structure_cmd}): compile structure inheritance to nested fields
2017-04-24 19:35:15 +02:00
Sebastian Ullrich
b26d15b9e9
fix(frontends/lean/elaborator): error message
2017-04-24 19:31:15 +02:00
Sebastian Ullrich
6ab0a008f9
feat(frontends/lean/{builtin_cmds,interactive}): complete namespace/section after end
2017-04-23 11:26:31 -07:00
Sebastian Ullrich
a54514fead
feat(frontends/lean/print_cmd): complete identifiers after #print
2017-04-23 11:26:31 -07:00
Sebastian Ullrich
5b17c3cbd9
fix(frontends/lean/interactive): fall back to elaborator info when not an interactive tactic
...
Fixes #1530
2017-04-23 11:26:31 -07:00
Gabriel Ebner
c2068dae46
fix(frontends/lean/tactic_notation): show error for unsolved focused goals at the end
...
Fixes #1531 .
2017-04-23 11:23:08 -07:00
Gabriel Ebner
489b3304bd
fix(frontends/lean/parser): allow enabling profiler via set_option
2017-04-23 11:22:50 -07:00
Gabriel Ebner
9424e6fa24
refactor(frontends/lean/definition_cmds): make profiling threshold configurable
2017-04-23 11:22:41 -07:00
Sebastian Ullrich
b3884d5f42
refactor(init/meta/interactive,frontends/lean/token_table): introduce generalizing keyword in Lean
2017-04-16 15:11:49 -07:00
Sebastian Ullrich
8ea2bc08cb
feat(init/meta/interactive): add generalizing parameter to induction
2017-04-11 17:07:28 -07:00
Gabriel Ebner
e2fa363423
feat(library/system/io,shell/lean): add --run switch
2017-04-11 16:41:30 -07:00
Gabriel Ebner
01a7efc007
fix(library/module_mgr): do not crash on missing imports
...
Fixes #1506 .
2017-04-04 19:56:33 +02:00
Gabriel Ebner
98fb21eab4
chore(frontends/lean/{parser_state,parser_pos_provider}): compiler warnings
2017-04-01 20:23:33 +02:00
Gabriel Ebner
cde946f293
fix(frontends/lean/scanner): fix assertion
2017-04-01 16:38:02 +02:00
Leonardo de Moura
b7c3d5a9f5
fix(frontends/lean/scanner): assertion
2017-03-31 19:39:13 -07:00
Sebastian Ullrich
3f87755a2a
fix(frontends/lean/pp): qualify constant shadowed by local
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
669c4130b1
fix(frontends/lean/builtin_expr): no field notation after @/@@
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
cd013f22c0
chore(*): replace "'^.' notation" with "field notation", pretty print using "."
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
93fdfdc4b6
feat(frontends/lean/elaborator): better error message on field notation that was probably supposed to be a single ident
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
3c8e176fb0
fix(frontends/lean/interactive): fix info on new field notation
2017-03-31 09:40:49 -07:00
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
Gabriel Ebner
f9c1ceb717
fix(frontends/lean/scanner): correctly handle positions in empty files
2017-03-31 09:40:15 -07:00
Leonardo de Moura
84bfd3e298
chore(frontends/lean): update keywords
...
Remark: "as" doesn't need to be a keyword.
So, we can now write patterns such as (a::as).
2017-03-30 16:51:08 -07:00
Sebastian Ullrich
7a147eab12
fix(frontends/lean/decl_util): truly fix top-level do pattern names race
2017-03-30 06:04:00 +02:00
Sebastian Ullrich
e7f01b7490
fix(frontends/lean/decl_util): bad reset in scope destructor
2017-03-30 06:04:00 +02: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
cb049f42b7
fix(frontends/lean/elaborator): resolve_local_name
2017-03-28 17:57:13 -07:00
