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

67 commits

Author SHA1 Message Date
Leonardo de Moura
ef449e816f chore: improve trace messages 2022-01-19 14:29:04 -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
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
6b235b05d2 feat: avoid code generation after stage1 for match auxiliary functions 2021-09-11 13:41:38 -07:00
Leonardo de Moura
ca747e9b27 feat: use contradiction at leaves 
closes #644
 2021-08-22 18:41:02 -07:00
Leonardo de Moura
bba9353619 fix: make sure isDefEqOffset does not expose kernel nat literals 
This issue is similar to a bug where `isDefEqOffset` was exposing
`Nat.add` when processing `HAdd.hAdd`.

Fixes #561
The example at issue #561 is now working, but we may have other places
where raw literals are being accidentally exposed.
 2021-08-02 11:27:00 -07:00
Gabriel Ebner
3cff5ceb99 perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
Daniel Fabian
9200de01ef refactor: fix code review comments. 2021-06-06 06:40:09 -07:00
Daniel Fabian
4e88fdc99a feat: add getMkMatcherInputInContext. 2021-06-06 06:40:09 -07:00
Leonardo de Moura
28b055463f fix: fixes #471 2021-05-22 15:42:52 -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
91ecbb5b5c feat: Add withMkMatcherInput. 
This is the inverse function to `mkMatcher`, i.e. a way to turn a matcher into an input.
 2021-05-19 07:28:14 -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
9d45ea6721 feat: try to improve dependent pattern matching failure error message 2021-03-30 23:40:11 -07:00
Leonardo de Moura
f20fc6328c fix: better error message when cases fails and there are no alternatives 2021-03-26 16:28:21 -07:00
Leonardo de Moura
650c6df380 feat: try other variables after failure 2021-03-22 21:02:26 -07:00
Leonardo de Moura
3749213e08 fix: missing whnf at Unify.unify 2021-03-21 22:38:46 -07:00
Leonardo de Moura
be841a7cad chore: throwError! => throwError, throwErrorAt! => throwErrorAt 
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
 2021-03-11 11:59:45 -08: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
e1f6965266 feat: allow user to define rewrite lemmas with (local) match expressions 2021-02-19 15:18:19 -08:00
Leonardo de Moura
6c119a1921 chore: use register_builtin_option 2021-01-26 18:24:56 -08:00
Leonardo de Moura
ea0fda39bc chore: Declaration.lean naming convention 
`Declaration.lean` was one of the first Lean 4 files, and was still
using an old naming convention.

cc @Kha
 2021-01-20 17:07:02 -08:00
Leonardo de Moura
6a39c65bd2 feat: improve match error message 2021-01-14 14:58:34 -08:00
Leonardo de Moura
11c7ca40c3 fix: missing case at Match.lean 2021-01-07 17:38:22 -08:00
Leonardo de Moura
39e374e7cd fix: improve error message at invalid match-expr 
The location is not perfect because we only have a `ref` for the whole alternative.
 2020-12-29 14:21:02 -08:00
Leonardo de Moura
ae5aa51712 chore: add explicit discard 2020-12-08 06:18:18 -08:00
Leonardo de Moura
9d304df757 feat: heterogeneous Append experiment 
@Kha This one required a bunch of manual fixes. The main issue is that
before we added the string interpolation feature, we created
`MessageData`s using `++` and coercions. For example, given
`(e : Expr)`, we would write
```
let msg : MessageData := "type: " ++ e
```
and rely on the coercions `String -> MessageData` and
`Expr -> MessageData`, and the instance `Append MessageData`.
However, heterogeneous operators "block" the expected type propagation downwards.
This kind of code is obsolete now since we can write a more compact
version using string interpolation
```
let msg := m!"type: {e}"
```
 2020-12-01 16:32:41 -08:00
Leonardo de Moura
b6f242434d fix: fixes #229 2020-11-30 11:51:13 -08:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Leonardo de Moura
8f1ad0411d fix: fixes #220 and #223 2020-11-24 10:18:02 -08:00
Leonardo de Moura
5c39cd5120 chore: cleanup 2020-11-24 10:18:02 -08:00
Leonardo de Moura
ecfe590268 refactor: split Match.lean 2020-11-24 10:18:02 -08:00
Leonardo de Moura
f67c93191f feat: use |>. 2020-11-19 08:38:47 -08:00
Leonardo de Moura
c305c2691f chore: use := 2020-11-19 07:22:31 -08:00
Leonardo de Moura
49e9064202 refactor: add MatcherInfo.lean 2020-11-15 14:22:05 -08:00
Leonardo de Moura
db5fe843de chore: add expandInterpolatedStr helper function, rename msg! => m! 2020-11-14 13:52:52 -08:00
Sebastian Ullrich
3665e3b7b5 feat: pretty print match 
Fixes #177
 2020-11-10 10:11:24 -08:00
Leonardo de Moura
defa45ae2f feat: improve error message 
when match-expression LHSs still contain metavariables after elaboration
 2020-11-09 18:26:14 -08:00
Leonardo de Moura
2d2d39c78e chore: use mut 2020-11-07 17:32:13 -08:00
Leonardo de Moura
81d6e065e7 chore: adjust files and tests 2020-11-07 17:32:12 -08:00
Leonardo de Moura
6858cb5fb6 chore: cleanup 2020-10-29 10:24:16 -07:00
Leonardo de Moura
4ba21ea10c chore: cleanup src/Array/Basic.lean 2020-10-28 19:35:42 -07:00
Leonardo de Moura
13c2a8ff51 chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Leonardo de Moura
21757b2be9 feat: add helper option for fixing bootstrapping issue at src/Init/Data/Int/Basic 2020-10-23 11:13:04 -07:00
Leonardo de Moura
bebd5075fd chore: cleanup 2020-10-23 10:00:23 -07:00
Leonardo de Moura
af968c60e6 chore: cleanup 2020-10-22 07:32:23 -07:00
Leonardo de Moura
1495f403a1 chore: use builtin_initialize instead of initialize at src/Lean 2020-10-19 15:17:02 -07:00
Leonardo de Moura
ef18b0ab49 chore: use [builtinInit] 2020-10-19 14:58:38 -07:00
Leonardo de Moura
aeac85dadb chore: cleanup 2020-10-17 09:09:30 -07:00