Sebastian Ullrich
d5b3430e53
chore: ignore stage0/ (for rg etc.)
2022-03-18 15:28:20 +01: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
3193acecfa
fix: flush the CoreM and MetaM caches at modifyEnv
...
This fix may impact performance. Note that we don't need to flush the
cache if we are "adding" stuff to the environment. We only need to
flush the caches if the change is not monotonic. BTW, most of the
changes are monotonic. I think this is why we did not hit this bug before.
We may also move all these caches to an environment extension. It is
an easy way to make sure we preserve the cache when extending the
environment.
I tried a few benchmarks and did not notice a significant difference.
cc @kha @gebner
fixes #1051
2022-03-17 16:02:30 -07:00
Leonardo de Moura
719db55a9c
chore: fix trace class
2022-03-17 13:22:16 -07:00
Leonardo de Moura
184b0b8e8d
feat: improve "result types must be in the same universe level" error message
...
The new error message makes it clear why the definition is not accepted.
See issue #1050
2022-03-17 07:41:37 -07:00
zygi
ac793ce196
fix: forward start and stop in Array.allM
2022-03-17 10:08:40 +01:00
Sebastian Ullrich
0d03c6e319
chore: revise non-GMP interface
2022-03-16 17:32:51 -07:00
Daniel Fabian
969eea19f0
refactor: do not use mkAppM so much
2022-03-16 17:21:20 -07:00
Daniel Fabian
cf4e873974
feat: support Sort u in ac_refl.
2022-03-16 17:21:20 -07:00
Daniel Fabian
8e0763f502
fix: binder case.
2022-03-16 17:21:20 -07:00
Daniel Fabian
d667d5ab5d
feat: rewrite the tactic using simp as the basis.
2022-03-16 17:21:20 -07:00
Daniel Fabian
ed63274874
refactor: move ac_refl syntaxt to Init/Notation
2022-03-16 17:21:20 -07:00
Daniel Fabian
73a59e5bc4
feat: use simp instead of rewrite inside of ac_refl
2022-03-16 17:21:20 -07:00
Daniel Fabian
fda1c5b192
refactor: simplify proof using <;>
2022-03-16 17:21:20 -07:00
Daniel Fabian
84f72b9389
test: add further ac_refl tests.
2022-03-16 17:21:20 -07:00
Daniel Fabian
a60220b036
feat: add tactic for ac_refl.
2022-03-16 17:21:20 -07:00
Daniel Fabian
eaa48f0d8d
refactor: move ac proofs to Init.
2022-03-16 17:21:20 -07:00
Daniel Fabian
1114dfac6c
feat: add theory for ac normalization.
...
This lets us implement an AC reflexivity tactic.
2022-03-16 17:21:20 -07:00
Leonardo de Moura
4320a61f4d
chore: use Prod notation in test
2022-03-16 17:14:16 -07:00
Leonardo de Moura
50813429b8
fix: add expected type hint
...
Other tactics (e.g., `simp_all`) may try to infer the type of the
proof, and `Nat.Linear.eq_of_toNormPoly_eq` has a messy resulting type.
2022-03-16 17:07:22 -07:00
Leonardo de Moura
cb925a3a3c
fix: return some at simpCnstrPos? if arith expr was normalized, but not simplified
...
Example: converted `<`, `>`, or `>=` into `<=`.
2022-03-16 16:36:39 -07:00
Leonardo de Moura
9b9ed6db68
feat: add simp_all_arith macro
2022-03-16 16:17:45 -07:00
Leonardo de Moura
4ba5a9b041
fix: bug at KExprMap
2022-03-16 16:07:14 -07:00
Leonardo de Moura
09648521d1
chore: add Repr instances
2022-03-16 16:07:14 -07:00
Sebastian Ullrich
4fd520e902
feat: generalize inferred namespace notation to functions
2022-03-16 23:40:05 +01:00
Leonardo de Moura
68154a6c69
test: add Pos view
2022-03-16 10:08:43 -07:00
Leonardo de Moura
05a2778b0d
fix: ensure explicit pattern variables provided by the uses are indeed pattern variables
2022-03-16 07:50:29 -07:00
Leonardo de Moura
90c442da76
feat: add internal option for communicating to the delaborator that input term is a pattern
2022-03-16 07:50:29 -07:00
Sebastian Ullrich
a3c73f5df8
chore: remove orphan file
2022-03-16 10:25:18 +01:00
Leonardo de Moura
0a2d0bc3fd
chore: update stage0
2022-03-15 17:43:52 -07:00
Leonardo de Moura
0bd9de1cb9
perf: add InstantiateLevelCaches for types and values at CoreM
2022-03-15 17:42:38 -07:00
Leonardo de Moura
d6de53a7aa
perf: custom splitAnd
2022-03-15 16:59:11 -07:00
Leonardo de Moura
b8a4f3a7a3
perf: quick filter for simpMatch when proving equation theorems
2022-03-15 15:53:29 -07:00
Leonardo de Moura
e44b36cab0
chore: cleanup optimization using Lean bitwise operators
2022-03-15 12:06:08 -07:00
Leonardo de Moura
49e33fdb23
chore: fix tests
2022-03-15 11:35:47 -07:00
Leonardo de Moura
e1ba83d902
chore: update stage0
2022-03-15 11:31:39 -07:00
Leonardo de Moura
d3e2dfb079
perf: optimize mkApp
2022-03-15 11:31:15 -07:00
Leonardo de Moura
9d73317d76
perf: faster Expr.data
2022-03-15 11:30:41 -07:00
Leonardo de Moura
d2dc38fdb6
perf: use HasConstCache to minimize the number of visited terms at Structural and WF
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2022-03-15 08:40:47 -07:00
Leonardo de Moura
5283007aa4
feat: add HasConstCache
2022-03-15 08:39:48 -07:00
Leonardo de Moura
3278d7bc2a
chore: update stage0
2022-03-15 07:16:17 -07:00
Leonardo de Moura
ca6453a0ab
perf: efficient unsigned hash(expr const & e)
2022-03-15 07:15:00 -07:00
Leonardo de Moura
eccd5c11c9
perf: removeUnusedEqnHypotheses
2022-03-15 06:53:43 -07:00
Leonardo de Moura
2b71bc84f3
perf: try injection before contradiction at mkSplitterProof
2022-03-15 05:37:10 -07:00
Leonardo de Moura
c3c0b8b8a2
chore: remove unnecessary code
2022-03-15 05:26:33 -07:00
Leonardo de Moura
aa68057c85
chore: more general type universes in example
2022-03-15 05:19:02 -07:00
Leonardo de Moura
7ee7ca30b8
fix: index out of bounds
2022-03-15 05:16:19 -07:00
Leonardo de Moura
4e261b15e5
fix: smart unfolding bug in over applications
2022-03-14 19:17:21 -07:00
Leonardo de Moura
eb7539ef77
fix: mkEqnTypes overapplied lhs in equational theorems
...
This issue was exposed by the "Dependent de Bruijn indices" from CPDT.
2022-03-14 17:42:21 -07:00
Leonardo de Moura
c6dae18787
chore: add helper theorems
2022-03-14 16:24:05 -07:00
