max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
26902 commits 1 branch 0 tags 5.3 GiB
Commit graph

94 commits

Author SHA1 Message Date
Leonardo de Moura
9d05023325 chore: remove some [specialize] annotations 2022-01-18 09:24:06 -08:00
Leonardo de Moura
68bd55af32 chore: fix codebase 2021-12-10 13:12:09 -08:00
Leonardo de Moura
41040a81de fix: auxiliary matcher definitions should be treated as abbreviations 
The motivation is to prevent performance problems such as the one
described at issue #854.

Fixes #854 after a update stage0
 2021-12-07 16:43:20 -08:00
Leonardo de Moura
7b6732a137 refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files 
We use the export/extern idiom to define `isLevelDefEqAux`, and then
define the `isDefEq` user facing functions at `Meta/Basic.lean`.
 2021-12-06 09:57:00 -08:00
Leonardo de Moura
0aa32d643e fix: eta struct and proof irrelevance issue 
see #777
 2021-11-27 07:15:57 -08:00
Leonardo de Moura
2d113e83f9 feat: eta struct support for unit-like datatypes 
For example, given `a b : Unit`, we have that `a` and `b` are
definitionally equal by `etaStruct`.

See #777
 2021-11-26 08:36:25 -08:00
Leonardo de Moura
43217884c0 feat: add Meta.Config.etaStruct 
It is useful to disable eta for structures for meta programs.
 2021-11-25 11:31:00 -08:00
Leonardo de Moura
ccc3f99507 chore: use isStructureLike 2021-11-25 11:31:00 -08:00
Leonardo de Moura
0de700fe45 chore: naming convetion 2021-11-25 11:31:00 -08:00
Leonardo de Moura
a8f4146070 feat: support eta struct recursively 
Addresses issues raised by @gebner at #777
 2021-11-23 17:38:48 -08:00
Leonardo de Moura
d685c545b4 feat: eta for structures 2021-11-23 06:21:25 -08:00
Leonardo de Moura
3367501511 fix: inaccessible annotations at isDefEq issue 
Issue was reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Change.20in.20pattern.20matching.3B.20expected.20behaviour.3F/near/259059096

fixes #742
 2021-10-27 09:26:12 -07:00
Leonardo de Moura
b4a6b4f882 fix: do not consume pretty print hints at isDefEq 
TODO: improve the solution. It is too hackish.

The issue was reported here https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20MData.20and.20unification/near/258352713
 2021-10-20 15:58:56 -07:00
Leonardo de Moura
445cc3085f refactor: avoid Name, MVarId, and FVarId confusion 2021-09-07 19:06:50 -07:00
Leonardo de Moura
bcfc927799 fix: fixes #602 2021-08-05 16:14:04 -07:00
Leonardo de Moura
789c7073dc fix: avoid eager TC synthesis at isDefEq 2021-08-05 12:09:22 -07:00
Leonardo de Moura
d1d7ce1839 feat: start support for strict implicit binder annotation 2021-08-03 18:42:15 -07:00
Leonardo de Moura
6e1620ca8d refactor: replace IO.Ref with the extern/export hack at MetaM 2021-08-03 11:50:57 -07:00
Leonardo de Moura
49a87ceb4d feat: add basic isDefEq cache 2021-07-28 16:29:44 -07:00
Leonardo de Moura
8a98987e26 chore: use isDefEq heuristic on regular definitions only 2021-07-26 07:11:55 -07:00
Leonardo de Moura
cce6165d4e perf: refine tryHeuristic 2021-07-23 12:04:11 -07:00
Leonardo de Moura
a435f3d641 feat: reduce s.1 =?= v to s =?= ⟨v⟩ if structure has a single field 
This feature was suggested by @dselsam at PR #521.
It closes #509
 2021-06-11 11:23:19 -07:00
Leonardo de Moura
a247249880 feat: add configuration option for disabling proof irrelevance at MetaM 2021-05-27 13:37:26 -07:00
Leonardo de Moura
663a5124f4 chore: naming convention 2021-05-01 21:29:06 -07:00
Leonardo de Moura
2694e7798a refactor: add MonadBacktrack 
The new class specifies an interface for saving and restoring the
backtrackable part of the state.
This commit also fixes a few issues.

- `commitWhen` at `LevelDefEq` was defining a checkpoint for
  the `isDefEq` methods, and it affects how postponed universe
  constraints are handled. However, the name suggests it is
  similar to `commitWhenSome?`, and consequently it was used
  in other places that had nothing to do with `isDefEq`.
  So, I renamed it, and provided the generic `commitWhen` at the new
  `MonadBacktrack.lean` file.

- We were restoring more state then needed in a few places.
  For example, we were discarding all caches.

- At `SyntheticMVars.lean`, we were using the `Meta.commitWhenSome?`
  method which does not restore the `Term.State`.
 2021-04-11 19:10:41 -07:00
Leonardo de Moura
68143ca8ba chore: trace[...]! ==> trace[...] 
@Kha I think this one is a good change, there is no real reason for
using the `!` suffix here.
 2021-03-10 18:44:43 -08:00
Leonardo de Moura
a4abdbf277 refactor: add checkApp 
Add comment describing possible extension.
 2021-03-08 15:26:07 -08:00
Leonardo de Moura
08fc25217d chore: cleanup, fix docs 2021-03-07 09:01:54 -08:00
Leonardo de Moura
6d236fbf2e chore: fix docstring 2021-03-07 09:01:54 -08:00
Jan Hrcek
2753822fe7
doc: fix typos 2021-03-07 15:06:02 +01:00
Leonardo de Moura
8b3c61dbb0 fix: checkAssignment 2021-02-11 16:56:32 -08:00
Leonardo de Moura
cab3c72374 fix: isDefEq for applications in WHNF 
The issue fixed by this commit was exposed by c17a1c382f
We also document the TC workaround used at `tryHeuristic`.
 2021-02-05 12:42:34 -08:00
Leonardo de Moura
c17a1c382f fix: isDeltaCandidate? 
It should return `some ...` only if `ConstantInfo` has a value.
 2021-02-05 09:19:37 -08:00
Leonardo de Moura
e63111b39a fix: fixes #302 
TODO: investigage error message duplication
 2021-02-03 15:04:18 -08:00
Leonardo de Moura
bf77f0707e refactor: remove no-mutual workaround 
This is still leftover from the old frontend.
 2021-01-29 17:13:04 -08:00
Leonardo de Moura
920ae5f1b9 chore: cleanup 2021-01-29 17:13:04 -08:00
Leonardo de Moura
e102cd4f42 fix: checkAssignment must be at assignConst 
Example of issue fixed by this commit: the variables `xs` may have references to `mvar`.
 2021-01-29 17:13:03 -08:00
Leonardo de Moura
8699f439da chore: avoid big match-expr 2021-01-29 17:13:03 -08:00
Leonardo de Moura
4fc2aead45 fix: missing checkAssignment at assignToConstFun 
Fixes #297
 2021-01-26 17:33:33 -08:00
Leonardo de Moura
4ed43bd925 chore: cleanup 2021-01-26 17:16:10 -08:00
Leonardo de Moura
2c05e78728 fix: bug at CheckAssignment 2021-01-26 16:20:41 -08:00
Leonardo de Moura
75466a7cf3 chore: cleanup 2021-01-26 16:01:46 -08:00
Leonardo de Moura
f53e83b182 feat: add options maxHeartbeats and synthInstance.maxHeartbeats 2021-01-24 17:45:50 -08:00
Sebastian Ullrich
dc77c45787 fix: mvar check trace message 2021-01-15 14:34:06 +01:00
Leonardo de Moura
74a9331571 feat: use left-to-right resolution 2021-01-13 16:33:30 -08:00
Leonardo de Moura
ec7be1d801 feat: add processAssignment' 2021-01-11 15:22:10 -08:00
Leonardo de Moura
0ca1c13a5d fix: bugs at ExprDefEq 2020-12-23 17:58:54 -08:00
Leonardo de Moura
9a422ddc23 fix: Array.back on empty array 2020-12-08 12:21:01 -08:00
Leonardo de Moura
ae5aa51712 chore: add explicit discard 2020-12-08 06:18:18 -08:00
Leonardo de Moura
265b7571b4 chore: change checkCache type 2020-12-06 16:24:51 -08:00