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
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
ca2eab3a2f
fix(frontends/lean/structure_cmd): instantiate universe levels in projections to parents
2017-04-29 15:00:17 +02: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
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
Leonardo de Moura
9a4e04b8ca
feat(frontends/lean/structure_cmd): add equational lemma for auxiliary default values
2017-03-27 21:37:31 -07:00
Sebastian Ullrich
55425e7b1f
fix(frontends/lean/structure_cmd): unfold untrusted macros in intro rules
2017-03-27 13:42:08 -07:00
Sebastian Ullrich
bf8292cb17
feat(frontends/lean/structure_cmd): allow local notations
2017-03-27 13:42:08 -07:00
Leonardo de Moura
36770119b6
feat(library): do not generate C.destruct (for structures), and C.induction_on (for structures and inductive datatypes)
2017-03-15 14:45:13 -07:00
Daniel Selsam
7f56f23e70
chore(frontends/lean/inductive_cmds): allow sorrys
2017-03-15 14:06:56 -07:00
Daniel Selsam
538ac8d187
feat(inductive_compiler): generate injectivity lemmas
2017-03-10 22:27:18 -08: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
970e11bf5e
feat(frontends/lean/{elaborator,structure_cmd}): allow overriding field defaults
2017-03-08 10:41:20 -08:00
Daniel Selsam
5f0ebf90de
fix(frontends/lean/structure_cmd): call inductive compiler without params in type
2017-03-06 14:01:46 -08:00
Sebastian Ullrich
c4ebfab14c
fix(frontends/lean/structure_cmd): inheriting defaulted field depending on field starting with implicit parameter
2017-03-06 11:02:51 -08:00
Sebastian Ullrich
87b98d5aa2
fix(frontends/lean/structure_cmd): fix assertion violation when field depends on defaulted field
2017-03-06 11:02:50 -08:00
Leonardo de Moura
045fe4ad25
fix(frontends/lean/structure_cmd): allow default values for function fields
2017-03-06 07:41:42 -08:00
Leonardo de Moura
61254847fb
fix(frontends/lean/structure_cmd): when error recovery is enabled, we must not assume the expression in the fixed line is a binding expression (it may be a sorry expression)
2017-02-20 14:51:59 -08:00
Leonardo de Moura
add5266df7
fix(frontends/lean, library/tactic): error position in auto quoted terms
...
This commit also gets rid of the redundant "elaborator failed" error
message.
2017-02-09 18:03:04 -08:00
Leonardo de Moura
c09f60de6e
fix(frontends/lean/structure_cmd): fixes #1347
2017-01-30 14:49:14 -08:00
Gabriel Ebner
5fdc737dfc
feat(library/tactic): store name of current declaration in tactic_state
2017-01-28 08:27:19 +01:00
Sebastian Ullrich
2c3f6d0e1c
fix(frontends/lean/structure_cmd): default field values of Pi type
...
There were two separate issues:
* An explicit Pi as the type of a field with a default value would be considered a field reference
* An implicit Pi would be instantiated by the elaborator during `visit_structure_instance`
2017-01-26 18:53:55 +01:00
Sebastian Ullrich
5c5c998813
fix(frontends/lean/structure_cmd): fix default field values referencing universe variables
2017-01-26 18:52:20 +01:00
Leonardo de Moura
71a7a7f466
feat(frontends/lean): add default field values
2017-01-22 21:25:49 -08:00
Leonardo de Moura
9119554835
feat(frontends/lean/structure_cmd): avoid unnecessary local_ref
2016-12-15 16:22:22 -08:00
Leonardo de Moura
6978906a78
chore(frontends/lean): remove namespace documentation
...
We will add module level doc strings /-! -/
2016-11-27 11:57:03 -08:00
Leonardo de Moura
338a46c225
fix(library/documentation): do not store doc strings for namespaces and declarations in the same name_map
2016-11-26 09:41:07 -08:00
Leonardo de Moura
97dd2f34d5
feat(library,frontends/lean): add basic doc string support
2016-11-25 18:52:56 -08:00
Gabriel Ebner
a3aced1b30
feat(frontends/lean/structure_cmd): record position of structure declaration
2016-11-08 19:22:42 -08:00
Leonardo de Moura
9b84db083d
fix(frontends/lean): error localization bugs
2016-10-15 13:40:57 -07:00
Leonardo de Moura
f21f1219d9
fix(frontends/lean/structure_cmd): handle is_one_placeholder
2016-10-02 08:07:19 -07:00
Leonardo de Moura
4f69fe943a
fix(frontends/lean/structure_cmd): make sure structure_cmd takes the option default_priority into account
2016-10-01 13:47:19 -07:00
Leonardo de Moura
572751c56e
feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class
...
Before this commit, we were inferring whether an
inductive/structure/class were meta or not. This was bad since the user
had no clue whether the type was trusted (non meta) or not.
Moreover, users could get confused by this behavior and assume the
kernel was allowing trusted code to rely on untrusted one.
2016-09-29 17:56:35 -07:00
Leonardo de Moura
d0d75c0923
refactor(kernel): reduce number of configurations supported in the kernel
...
Now, eta and impredicativity are assumed to be always true.
Motivation: the rest of the system assumes eta.
Regarding impredicativity, we decided to support only the standard library.
2016-09-27 17:07:01 -07:00
Leonardo de Moura
5957022adb
feat(frontends/lean): add 'class' keyword
2016-09-24 14:32:01 -07:00
Leonardo de Moura
b2e1e920a9
chore(frontends/lean,library,linja): remove .ilean files
2016-09-20 08:43:45 -07:00
Leonardo de Moura
ac87de33e7
fix(frontends/lean/structure_cmd): universe level validation in the structure command
2016-09-18 10:00:31 -07:00
Leonardo de Moura
6c84a0a7b1
feat(frontends/lean): use new notation for declaring universes in constant and structure decls
2016-09-13 21:45:16 -07:00
Leonardo de Moura
932d14241b
chore(kernel): remove support for mutually inductive datatypes from the kernel
2016-09-10 17:39:17 -07:00
Daniel Selsam
b0c5744eea
feat(inductive_compiler): support for mutually inductive types
2016-09-10 14:22:27 -07:00
Leonardo de Moura
8d9e508a11
fix(frontends/lean/structure_cmd): leftover
2016-09-10 12:57:24 -07:00
Leonardo de Moura
d8caecff49
refactor(library/exception): avoid throw_generic_exception functions
2016-09-06 12:37:56 -07:00
Leonardo de Moura
81a30a69d2
refactor(library/normalize): remove unfold and unfold_full attributes
2016-09-05 08:40:58 -07:00
Leonardo de Moura
f7df7dc9a7
refactor(kernel): add reducibility_hints
2016-09-04 16:30:02 -07:00
Leonardo de Moura
a93eada058
feat(library/type_context): improved (and simplified) cache management for type_context
2016-08-23 17:56:58 -07:00
Leonardo de Moura
423319398d
fix(frontends/lean/structure_cmd): compilation warning
2016-08-17 15:42:20 -07:00
Daniel Selsam
a9b01991c2
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
...
Conflicts:
src/frontends/lean/CMakeLists.txt
src/frontends/lean/structure_cmd.h
2016-08-17 07:34:03 -07:00
