Leonardo de Moura
dd682bf1d5
feat: add support for HO projections at DiscrTree
...
closes #1937
Requires update stage0
2023-01-05 13:33:43 -08:00
Leonardo de Moura
71b7562c2f
fix: class projection at DiscrTree
2022-11-24 11:56:36 -08:00
Leonardo de Moura
8225be2f0e
feat: ensure projections are not reducing at DiscrTree V (simpleReduce := true)
...
Now, the `simp` discrimination tree does not perform `iota` nor reduce
projections.
2022-11-15 16:47:12 -08:00
Leonardo de Moura
1b0c2f7157
feat: parameterize DiscrTree indicating whether non trivial reductions are allowed or not when indexing/retrieving terms
2022-11-15 16:47:12 -08:00
Leonardo de Moura
81c84bf045
feat: do not perform iota reduction at the discrimination tree module
2022-11-15 16:47:12 -08:00
Leonardo de Moura
7874c03c27
chore: style
2022-10-08 07:49:27 -07:00
Leonardo de Moura
6bc4144409
fix: fixes #1549
2022-10-08 07:41:49 -07:00
Mario Carneiro
6392c5b456
chore: import reductions
2022-09-15 14:02:38 -07:00
Leonardo de Moura
3896244c55
chore: cleanup
2022-07-25 22:39:56 -07:00
Leonardo de Moura
8335a82aed
refactor: improve MVarId method discoverability
...
See issue #1346
2022-07-24 21:36:33 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Gabriel Ebner
a8cab84735
refactor: use computed fields for Expr
2022-07-11 14:19:41 -07:00
Leonardo de Moura
2ebcf29cde
chore: use a[i]! for array accesses that may panic
2022-07-02 15:12:05 -07:00
Leonardo de Moura
c498285d94
chore: add missing double backtick
2022-06-27 09:56:47 -07:00
Sebastian Ullrich
ae7b895f7a
refactor: unname some unused variables
2022-06-07 16:37:45 -07:00
Leonardo de Moura
42b707e250
perf: improve getMatchWithExtra
2022-03-18 17:10:46 -07:00
Leonardo de Moura
38a1675c72
fix: dicrimination tree getMatchWithExtra
...
It was buggy when the input argument could be reduced `e`.
fixes #1048
2022-03-17 16:44:38 -07:00
Leonardo de Moura
b664a93d8e
fix: a match application is stuck if one of the discriminants contain metavariables
2022-03-06 07:51:09 -08:00
Leonardo de Moura
8bcaafb28b
fix: universe metavariables should not be taken into account at getKeyArgs
2022-03-06 07:50:19 -08:00
Leonardo de Moura
613cf19509
fix: discrimination trees and "stuck" terms
...
See comments and new test.
2022-03-05 15:12:20 -08:00
Leonardo de Moura
9c2942c36d
chore: "simp lemma" => "simp theorem"
2022-02-06 09:15:39 -08:00
Leonardo de Moura
12e2a79170
chore: fix codebase after removing auto pure
2022-02-03 18:08:14 -08:00
Leonardo de Moura
8db923e010
feat: generate error message for simp theorems that are equivalent to x = x
...
see #973
see https://github.com/leanprover-community/mathport/issues/70
2022-01-26 11:16:31 -08:00
Leonardo de Moura
cf3b8d4eb4
chore: cleanup
...
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
2022-01-26 09:18:17 -08:00
Leonardo de Moura
bac91b9b5b
chore: remove arbitrary
2022-01-15 12:14:27 -08:00
Gabriel Ebner
7537fa7795
fix: unfold x<y in discrimination tree module
2021-11-23 07:34:51 -08:00
Leonardo de Moura
1282fb2d97
fix: getMatchWithExtra
...
`getMatchKeyArgs` returns arguments in reverse order.
2021-09-25 08:36:12 -07:00
Leonardo de Moura
19a710ffc9
feat: add getMatchWithExtra and improve tryLemma at simp
2021-09-09 19:28:09 -07:00
Leonardo de Moura
09eecc5c08
fix: simp was not applying rewrites to the function application prefixes
2021-09-09 17:07:14 -07:00
Leonardo de Moura
445cc3085f
refactor: avoid Name, MVarId, and FVarId confusion
2021-09-07 19:06:50 -07:00
Leonardo de Moura
d1d7ce1839
feat: start support for strict implicit binder annotation
2021-08-03 18:42:15 -07:00
Wojciech Nawrocki
f51b80060d
feat: generic tagged Format
2021-08-01 09:58:44 +02:00
Leonardo de Moura
c6308a0f1f
feat: add support for kernel projections to DiscrTree
2021-07-29 16:59:47 -07:00
Leonardo de Moura
b25bb78e2a
feat: improve DiscrTree
...
Try to improve the performance issue described at #587 .
The issue is that Mathlib contains thousands of theorems where the
associated key for the discrimination tree is just
`Key.other`. The indexing is not effective for them. This happens because
1- Lambda expressions are indexed using `Key.other`. The
discrimination tree mainly focus on the first-order structure.
2- It unfolds reducible constants when inserting and retrieving
entries. The motivation is that users expect simp theorems to fire
modulo reducible constants.
Then, we have many theorems such as
```lean
map ?g ∘ map ?f = map (?g ∘ ?f)
```
when we expand the function composition on the left-hand side, we get
```lean
fun (x : List ?α) => map ?g (map ?f x)
```
Which is indexed as `Key.other`.
We should not avoid the `Array`s in the discrimination tree nodes
If the index is working effectively, these arrays are all very small.
In this commit, we try to address the problem by using a different
approach. When processing the root of a pattern, we interrupt
reduction as soon as the we hit something that would be indexed
as `Key.other`. Note that, in Lean 3, the root of a pattern also
receives special treatment.
2021-07-29 16:08:26 -07:00
Leonardo de Moura
3a80e87793
chore: #405 step 1
2021-04-22 20:03:48 -07:00
Leonardo de Moura
083301e286
fix: non-dependent arrow vs dependent arrow issue at DiscrTree
2021-03-25 13:04:24 -07:00
Leonardo de Moura
b7acc38810
feat: add support for "arrow" at DiscrTree
2021-03-25 12:21:10 -07:00
Leonardo de Moura
cc0712fc82
feat: add support for offset terms at DiscrTree
2021-03-14 08:23:44 -07:00
Leonardo de Moura
8392b09db2
feat: shouldAddAsStar only for nested terms
2021-02-18 11:33:56 -08:00
Leonardo de Moura
479da7b914
feat: elaborate noindex! annotation
2020-12-28 17:49:54 -08:00
Leonardo de Moura
944cc567d0
chore: cleanup
...
Document why we have `shouldAddAsStar`.
2020-12-28 16:41:00 -08:00
Leonardo de Moura
469c9b7bbf
chore: remove TODO
2020-12-14 11:50:22 -08:00
Leonardo de Moura
04a07c15b9
chore: use deriving Inhabited
2020-12-13 11:57:59 -08:00
Leonardo de Moura
d629c76f9e
chore: more heterogeneous operators support
2020-12-01 12:39:45 -08:00
Leonardo de Moura
d6f778bec4
refactor: arbitrary without explicit arguments
...
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
2020-11-25 09:07:38 -08:00
Leonardo de Moura
2daeb195b5
chore: use new names
2020-11-10 10:15:19 -08:00
Leonardo de Moura
898a08a0c1
chore: avoid Has prefix in type classes
...
closes #203
2020-10-27 18:29:19 -07:00
Leonardo de Moura
97c93ec557
chore: prepare to rename
2020-10-27 18:09:03 -07:00
Leonardo de Moura
ff493751b5
chore: HasFormat ==> ToFormat
2020-10-27 16:19:14 -07:00
Leonardo de Moura
5481999560
chore: cleanup
2020-10-26 14:25:38 -07:00
