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

209 commits

Author SHA1 Message Date
Leonardo de Moura
27e07d1b25 fix: remove auxiliary discriminants before elaborating patterns 2022-04-05 19:37:56 -07:00
Leonardo de Moura
46ce3013d0 feat: cleanup local context before elaborating match alternatives RHS 2022-03-29 18:52:07 -07:00
Leonardo de Moura
6d926c7989 feat: macro expand match alternatives 
see #371

This commit does not implement all features discussed in this issue.
It has implemented it as a macro expansion. Thus, the following is
accepted
```lean
inductive StrOrNum where
  | S (s : String)
  | I (i : Int)

def StrOrNum.asString (x : StrOrNum) :=
  match x with
  | I a | S a => toString a
```
It may confuse the Lean LSP server. The `a` on `toString` shows the
information for the first alternative after expansion (i.e., `a` is an `Int`).
After expansion, we have
```
def StrOrNum.asString (x : StrOrNum) :=
  match x with
  | I a => toString a
  | S a => toString a
```
 2022-03-20 14:20:13 -07:00
Leonardo de Moura
8f4d58893f feat: update match parser 
Support for
```
def fib (x : Nat) : Nat :=
  match x with
  | 0 | 1 => 1
  | x+2   => fib (x+1) + fib x
```

TODO: expand `matchAlts`
 2022-03-20 13:22:39 -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
eddcedb58c fix: pattern normalization code 2022-03-12 06:07:04 -08:00
Leonardo de Moura
a4f47adf9e fix: normalize method at Match.lean 2022-03-11 18:19:37 -08:00
Leonardo de Moura
272dd5533f chore: style use · instead of . for lambda dot notation 
We are considering removing `.` as an alternative for `·` in the
lambda dot notation (e.g., `(·+·)`).
Reasons:
- `.` is not a perfect replacement for `·` (e.g., `(·.insert ·)`)
- `.` is too overloaded: `(f.x)` and `(f .x)` and `(f . x)`. We want to keep the first two.
 2022-03-11 07:49:03 -08:00
Leonardo de Moura
3214a20d33 feat: allow overloaded notation in patterns 2022-03-10 12:51:34 -08:00
Leonardo de Moura
38668308ef fix: do not rename metavariables that are already in the patternVars array 
It fixes a regression introduced yesterday.
 2022-03-10 05:53:54 -08:00
Leonardo de Moura
9c5f6361a3 doc: document the new pattern elaboration procedure 2022-03-09 18:58:23 -08:00
Leonardo de Moura
ca253c43e1 refactor: pattern elaboration 
We don't use the following hack anymore:
-  /- HACK: `fvarId` is not in the scope of `mvarId`
-     If this generates problems in the future, we should update the metavariable declarations. -/
-  assignExprMVar mvarId (mkFVar fvarId)

This hack was corrupting the `InfoTree`.
 2022-03-09 18:19:14 -08:00
Leonardo de Moura
b0246172fa chore: add comment and remove dbg trace message 2022-03-09 14:02:30 -08:00
Leonardo de Moura
caa1366b62 fea: erase nested inaccessible annotations 2022-03-09 14:01:59 -08:00
Leonardo de Moura
1609f96128 refactor: simplify PatternVar.lean and Match.lean 2022-03-09 14:01:40 -08:00
Leonardo de Moura
a4d6cbfedd feat: improve match elaborator 2022-02-19 06:12:21 -08:00
Leonardo de Moura
3f4d8f370a fix: backtrack InfoTree when backtracking at the discriminant refinement method 
This commit addresses issue described at https://github.com/leanprover/lean4/issues/1018#issuecomment-1040597212

closes #1018
 2022-02-15 16:01:09 -08:00
Leonardo de Moura
fd9165415e feat: try to preserve variable names during discriminant refinement 
This fixes second issue at #1018
 2022-02-15 15:54:03 -08:00
Leonardo de Moura
56cdacfc28 feat: allow synthetic holes to be used as patterns 
They are useful for getting meaningful pattern variable names when the hole
is not an inaccessible pattern. See new test.

We are going to use this feature to address issue 2 at #1018.
 2022-02-15 15:34:14 -08:00
Leonardo de Moura
da1a327d13 chore: remove old comment 2022-02-15 15:01:26 -08:00
Leonardo de Moura
993ec54db6 chore: avoid hack that may introduce unnecessary dependencies 2022-02-15 12:17:40 -08:00
Leonardo de Moura
df584567f5 feat: (generalizing := true) is the default behavior for match-expressions 
closes #1018
 2022-02-15 11:12:04 -08:00
Leonardo de Moura
ffca6975f2 chore: remove bootstrapping workarounds 2022-02-14 15:39:21 -08:00
Leonardo de Moura
93b5b74b36 feat: modify notation for providing motive in "match" expressions 2022-02-14 15:36:14 -08:00
Leonardo de Moura
82bce7ebec fix: declare local instaces occurring in patterns 2022-02-12 12:01:08 -08:00
Leonardo de Moura
12e2a79170 chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
Leonardo de Moura
1c1e6d79a7 feat: add equality proof for named patterns 
The user can optionally name the equality proof.
The new test demostrates how to name the equality proof.

closes #501
 2022-01-18 12:43:01 -08:00
Leonardo de Moura
6631f1d5b3 chore: use namedPatternOld 2022-01-17 17:18:03 -08:00
Leonardo de Moura
2c690926cf feat: update namedPattern parser 2022-01-17 16:49:20 -08:00
Leonardo de Moura
bac91b9b5b chore: remove arbitrary 2022-01-15 12:14:27 -08:00
Sebastian Ullrich
6f9c6e4556 doc: match: mention (generalizing := true) 2021-12-19 11:14:27 +01:00
Leonardo de Moura
5b14caf329 fix: missing addTermInfo at elabAtomicDiscr 
closes #820
 2021-12-14 17:20:46 -08:00
Sebastian Ullrich
4063729b6c doc: document some built-in term notations 2021-11-26 17:13:19 +01:00
Gabriel Ebner
bfc74decde feat: add info field to Syntax.node 2021-10-26 20:19:27 +02:00
Leonardo de Moura
58430704e5 refactor: move inaccessible? to Expr.lean 2021-10-20 15:54:18 -07:00
Leonardo de Moura
a5b27952b5 fix: panic messages on invalid input 
fixes #689
 2021-09-25 09:01:01 -07:00
Leonardo de Moura
5fe40fbccf refactor: add sortFVarIds to Meta/Basic.lean 2021-09-20 11:32:53 -07:00
Leonardo de Moura
445cc3085f refactor: avoid Name, MVarId, and FVarId confusion 2021-09-07 19:06:50 -07:00
Leonardo de Moura
a8044eb252 feat: improve Match module for patterns containing Fin and UInt literals 2021-09-05 20:43:40 -07:00
Leonardo de Moura
c3bb948009 feat: ignore nested proofs in patterns 2021-09-05 15:46:03 -07:00
Leonardo de Moura
4abbb3d74c chore: cleanup 2021-08-11 16:05:07 -07:00
Leonardo de Moura
7e1bb3e65b refactor: add MatchAltView.lean and PatternVar.lean 2021-06-28 08:29:47 -07:00
Leonardo de Moura
7f986c62ba refactor: add Arg.lean 2021-06-28 08:10:16 -07:00
Sebastian Ullrich
eb1e285e26 chore: style 2021-06-21 10:17:26 -07:00
Leonardo de Moura
af4485f40e fix: fixes #482 2021-05-21 19:20:24 -07:00
Leonardo de Moura
8eceb07caf feat: new discriminant refinement procedure 2021-05-21 18:08:11 -07:00
Leonardo de Moura
73797841ba feat: add findDiscrRefinementPath 
The new method is going to be used to improve the discriminant
refinement procedure.
 2021-05-20 21:54:48 -07:00
Daniel Fabian
42bd44ab82 refactor: Capture environment modification in mkMatcher. 
Doing this allows us to add the declaration in the backtracking case of structural recursion.
 2021-05-20 15:20:16 -07:00
Daniel Fabian
cf030a1634 refactor: Add MkMatcherInput. 
Since we are going to make `mkMatcher` reversible, it's quite useful to have the input be a `structure`. This way we make sure, that the inverse function always returns the same type as `mkMatcher` needs as input.
 2021-05-19 07:28:14 -07:00
Leonardo de Moura
b0f0a59729 refactor: elabDiscrs 
Elaborate discriminants forward and infer match-type backwards.
 2021-05-18 19:59:11 -07:00