Leonardo de Moura
a8d672f237
test: add Kevin and Yakov's examples
2021-03-25 17:22:14 -07:00
Leonardo de Moura
c79712becb
chore: fix test
2021-03-25 17:20:58 -07:00
Leonardo de Moura
05022cc80b
fix: disable implicit lambda insertion at _, ?h, and by ...
...
@Kha This commit addresses an issue reported by Kevin. Holes and tactic
blocks represent a discontinuity in the elaboration process.
By introducing inaccessible variables (or "things" as Kevin calls
them), we create error message that are harder to understand (see
affected test), and goals where we didn't allow the user to select the
variable name and/or eagerly unfolded a definition.
BTW, I first considered using "reducible" setting when deciding
whether to insert implicit lambdas or not. This is a bad idea.
See `monotone.lean` test. The decision should not depend on
reducibility status, but whether there is "discontinuity" on the
elaboration process or not. As Kevin pointed out,
"introducing implicits work great if you finish the job".
2021-03-25 16:13:15 -07:00
Sebastian Ullrich
96c8cdfb14
chore: revert test changes
2021-03-25 10:35:22 +01:00
Leonardo de Moura
3176be136c
feat: improve "discriminant refinement"
2021-03-24 21:05:08 -07:00
Leonardo de Moura
f11a003526
test: add "discriminant refinement" tests
2021-03-24 19:10:50 -07:00
Leonardo de Moura
ec5afce45b
feat: contextual := true at simp_all
...
cc @Kha
2021-03-24 15:49:31 -07:00
Leonardo de Moura
e31c02522b
feat: closes #327
2021-03-24 12:29:33 -07:00
Leonardo de Moura
d86164cf54
fix: simple match case
2021-03-24 11:46:55 -07:00
Leonardo de Moura
d03f5fe318
feat: add trivial extensible (macro) tactic
2021-03-24 09:50:56 -07:00
Leonardo de Moura
1b7f7e9d39
chore: remove unnecessary annotations
2021-03-23 20:42:59 -07:00
Leonardo de Moura
5742b078af
feat: "discriminant refinement" for match-expressions
2021-03-23 20:40:07 -07:00
Leonardo de Moura
5ac7b1232a
chore: add workarounds
...
@Kha It seems the recent parser modifications created some unexpected
problems. I didn't investigate them. I am "lost" in the elaborator and
dependent pattern matching land.
1) We can't write anymore
```
f [1, 2, 3] |>.run' 0 = Except.ok ()
```
We have to use parentheses and the error message is weird :(
```
(f [1, 2, 3] |>.run' 0) = Except.ok ()
```
2) I had to add comments to `macro.lean`, I didn't find a workaround
for one of the rules. BTW, I had to add a bunch of `:term` for fixing
the other rules, and the error messages were counterintuitive.
2021-03-23 18:35:27 -07:00
Leonardo de Moura
1b963862c6
test: add test for former weird error message
2021-03-23 18:16:06 -07:00
Leonardo de Moura
99cd4fa720
feat: refine auto bound implicit locals
2021-03-23 17:33:15 -07:00
Leonardo de Moura
ec409a9bfc
fix: fixes #366
2021-03-23 16:02:45 -07:00
Sebastian Ullrich
62ae39e62b
fix: pp.all should not turn off pp.binder_types
2021-03-23 19:45:41 +01:00
Leonardo de Moura
81e6181488
test: add another test
2021-03-22 21:21:14 -07:00
Leonardo de Moura
650c6df380
feat: try other variables after failure
2021-03-22 21:02:26 -07:00
Sebastian Ullrich
cd4cd581be
feat: make infix non-associative
2021-03-22 16:33:37 +01:00
Sebastian Ullrich
bbf6c717fc
feat: introduce arg precedence
2021-03-22 16:33:37 +01:00
Leonardo de Moura
3749213e08
fix: missing whnf at Unify.unify
2021-03-21 22:38:46 -07:00
Leonardo de Moura
2fd0b8c663
feat: contradiction catches empty inductive types
2021-03-21 21:48:43 -07:00
Leonardo de Moura
d9273786c7
chore: remove when and «unless»
...
They are obsolete.
cc @Kha
2021-03-20 18:52:18 -07:00
Leonardo de Moura
9a5f239513
refactor: remove Monad Option and Alternative Option
...
We should use `OptionM` instead.
`Option` still implements `Functor` and `OrElse`.
cc @Kha
2021-03-20 18:25:25 -07:00
Sebastian Ullrich
83ecff44c6
test: make infoTree an output test
2021-03-20 08:28:18 -07:00
Sebastian Ullrich
c0af90022e
feat: term info at #print
2021-03-20 08:28:18 -07:00
Sebastian Ullrich
62891a1b0c
feat: trace.Elab.info
2021-03-20 08:28:18 -07:00
Leonardo de Moura
86a204d8a1
feat: add simp_all tactic
...
cc @Kha
2021-03-19 22:34:35 -07:00
Leonardo de Moura
d70740fef2
fix: location notation and simp
2021-03-19 19:54:22 -07:00
Leonardo de Moura
03e3a1cc6b
chore: remove hack
...
It produces weird error messages in some examples, and it will be
obsolete after the new precedence feature.
2021-03-19 11:09:18 -07:00
Sebastian Ullrich
54405c4543
fix: automatically wrap many/sepBy items in null nodes where necessary
2021-03-19 15:15:55 +01:00
Leonardo de Moura
f73615c3d2
fix: nontermination
2021-03-18 14:23:03 -07:00
Leonardo de Moura
1af02dcaca
feat: allow users to mark definitions with [simp]
...
cc @JasonGross @Kha
2021-03-17 19:11:55 -07:00
Leonardo de Moura
205b42a397
feat: proper syntax for configuring simp
2021-03-17 16:37:04 -07:00
Leonardo de Moura
5eda786f6e
feat: use False.elim when simplifying local declarations that rewrite to False
2021-03-17 15:30:54 -07:00
Sebastian Ullrich
f4c3d068ae
feat: uniform "unsolved case" positions with fullRange
...
/cc @leodemoura
2021-03-17 12:45:15 +01:00
Sebastian Ullrich
0d86ebe5eb
chore: remove volatile cases from test
2021-03-17 12:32:25 +01:00
pcpthm
419a6190e8
fix: bitwise shift overflow of UInt types
...
It is an undefined behavior in C when the right operand of a shift operation exceeds the bit-width of the left operand.
We define the shift operation to be `x << (y % B)` where `B` is the bit-width of the left operand.
2021-03-17 10:08:02 +01:00
Leonardo de Moura
dd4fb3b71b
chore: improve error message
...
see #346
2021-03-16 20:42:38 -07:00
Leonardo de Moura
08f87752ee
fix: closes #346
2021-03-16 18:55:46 -07:00
Leonardo de Moura
60a1b828ad
fix: fixes #348
2021-03-16 17:50:40 -07:00
Leonardo de Moura
1fd8089d19
fix: register new metavariables created when applying default instance
...
closes #353
2021-03-16 17:31:51 -07:00
Leonardo de Moura
c37d961fc3
chore: make sure both alternatives use throwError
2021-03-16 17:20:00 -07:00
Leonardo de Moura
7dc6721fea
fix: missing pushScope and popScope
2021-03-16 16:42:45 -07:00
Leonardo de Moura
89797c4485
chore: improve congrDefault
...
We don't need `congrMatch` anymore.
2021-03-16 15:59:11 -07:00
Leonardo de Moura
8227d3afcd
feat: support for simplifying match discriminants
2021-03-16 15:51:36 -07:00
Leonardo de Moura
ea91317f1a
fix: avoid nontermination due to respecialization
2021-03-15 19:12:57 -07:00
Leonardo de Moura
cc0712fc82
feat: add support for offset terms at DiscrTree
2021-03-14 08:23:44 -07:00
Sebastian Ullrich
75a97fad94
feat: nicer token parse errors
2021-03-14 08:23:32 -07:00
