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

14106 commits

Author SHA1 Message Date
Leonardo de Moura
2de7f1f4d9 doc: possible improvement 2020-09-13 13:16:03 -07:00
Leonardo de Moura
d6a3e22992 chore: add auxiliary function 2020-09-13 13:13:34 -07:00
Leonardo de Moura
fd7dca9bc1 fix: do not cache if term contains Expr-metavariables 2020-09-13 13:13:05 -07:00
Leonardo de Moura
98a8867d90 chore: add coercions for new frontend 2020-09-13 12:00:32 -07:00
Leonardo de Moura
d936b9461f fix: always ensure expectedType when processing overloaded symbols and/or notation 2020-09-13 11:59:13 -07:00
Leonardo de Moura
3493d1871d feat: improve "ambiguous" error message 2020-09-13 11:39:59 -07:00
Leonardo de Moura
3c2044f06b chore: add coercion for new frontend 2020-09-13 10:12:25 -07:00
Leonardo de Moura
897289599a fix: ignore auxiliary declarations at subst and assumption 2020-09-13 09:59:37 -07:00
Leonardo de Moura
ac6fd1382d fix: collectDeps issue 2020-09-13 09:47:00 -07:00
Leonardo de Moura
e181c1adee refactor: add DefEqM 
The idea is to make clear that the field `posponed` is transient
state. It is only used during `isDefEq`.
The refactoring was motivated by a bug I found where the `posponed`
constraints were not being handled correctly. For example,
the `check (e : Expr)` method was returning `true`, but leaving pending
universe constraints at `postponed`.

cc @Kha
 2020-09-12 16:42:16 -07:00
Leonardo de Moura
0967ad7e91 feat: extend/cleanup isLevelDefEqAux 
`tests/lean/run/toExpr.lean` could not be processed by the new
frontend without these extensions.
 2020-09-12 15:38:48 -07:00
Leonardo de Moura
e1e65e83da fix: try to synthesize instance for substructures 2020-09-12 08:58:13 -07:00
Leonardo de Moura
b0f0536018 fix: improve error message for overloaded notation 2020-09-12 08:05:37 -07:00
Leonardo de Moura
09244c73f4 fix: lval resolution 2020-09-12 07:45:36 -07:00
Leonardo de Moura
cc520d422c fix: ensure no unassigned mvars at #eval 2020-09-12 07:18:43 -07:00
Leonardo de Moura
a8de3c5115 fix: isDefEq configuration in the elaborator 2020-09-11 17:36:28 -07:00
Leonardo de Moura
c93f48cc9f fix: missing field params 2020-09-11 16:26:52 -07:00
Leonardo de Moura
bf703c9cab fix: bug at inductive datatype resulting universe inference 2020-09-11 16:07:22 -07:00
Leonardo de Moura
9cd88807dd feat: add support for quoted literals in patterns 2020-09-11 15:16:54 -07:00
Leonardo de Moura
151012cb39 feat: remove emptyc elaboration hack 
@Kha I removed the hack. We know get a nice error message.
 2020-09-11 14:41:44 -07:00
Leonardo de Moura
b85d3d60b8 fix: bug at ambiguous error message 
We were saving the incorrect metavariable context (and environment)/
 2020-09-11 14:40:34 -07:00
Leonardo de Moura
b025c1c623 chore: remove HasEmptyc workarounds 2020-09-11 14:28:42 -07:00
Leonardo de Moura
cc6104b369 fix: bug in the old frontend 
It had to be fixed because we have code that needs to be compiled with
the old frontend, and the hacks we used to workaround this issue are
incompatible with the new frontend.
 2020-09-11 14:12:03 -07:00
Leonardo de Moura
e9f7fb45af chore: add coercion for new frontend 2020-09-11 14:00:16 -07:00
Leonardo de Moura
7950413526 feat: improve choice nodes + postpone 2020-09-11 12:45:38 -07:00
Leonardo de Moura
457e48cfe4 chore: add private 2020-09-11 11:23:07 -07:00
Leonardo de Moura
81987e59e7 fix: expected type propagation issue 2020-09-11 11:03:59 -07:00
Leonardo de Moura
1731962ea9 feat: elaborate emptyC notation 
@Kha this is a little bit ugly. As in Lean3, the notation `{ }` is
overloaded. It can be `HasEmptyc.emptyc` or the empty structure.
Moreover, if we have an instance `HasEmptyc A` for a structure `A`,
then `{ }` is notation for `HasEmptyc.emptyc`. I am not very happy
about this, but it seems users use this feature. It is even used in
our own Lean4 code base :)

BTW, I will try a different alternative later.
First, move the notation `{ }` as a proper parser for `emptyc`.
Then, make sure the elaborator throws an error when
`{ }` is ambiguous. That is, `{}` can be elaborated as the empty
structure `A` and there is an `HasEmptyc A` instance.
Example:
```
structure A :=
(x : Nat := 0)

instance : HasEmptyc A :=
⟨{ x := 10 }⟩
```

The main issue here is that the support for choice+postpone is
currently broken.
 2020-09-11 10:42:39 -07:00
Leonardo de Moura
32eabf2ef1 chore: remove old elaborator that is not needed anymore 2020-09-11 10:28:00 -07:00
Leonardo de Moura
5db5cf7734 fix: do not lift (<- action) nested in quotations 2020-09-11 08:06:20 -07:00
Leonardo de Moura
2978d7af32 fix: error message 2020-09-11 07:32:30 -07:00
Leonardo de Moura
a8df621683 fix: bug at elabEvalUnsafe 
It was forgetting the the updates performed by `MetaHasEval`.
Wow, I wasted a lot of time on this bug.
 2020-09-10 19:33:52 -07:00
Leonardo de Moura
13d067d619 fix: forallTelescopeReducing => forallTelescope 
It impacts `mkInhabitantFor`
 2020-09-10 18:06:29 -07:00
Leonardo de Moura
a5c99b7601 fix: bug at getInstances 2020-09-10 17:49:17 -07:00
Leonardo de Moura
f28def6c5e feat: add Meta.ppExpr 2020-09-10 17:27:14 -07:00
Leonardo de Moura
f871c7b552 feat: trace! macro in the new frontend 2020-09-10 15:18:20 -07:00
Leonardo de Moura
264ce93bc8 chore: simplify elabEval 
`TermElab` is now on top of `IO`
 2020-09-10 15:03:45 -07:00
Leonardo de Moura
40777c203b feat: add MonadEnv helper methods 2020-09-10 14:58:22 -07:00
Leonardo de Moura
22bdab67ff feat: expand sorry 2020-09-10 14:58:14 -07:00
Leonardo de Moura
ba4fdce508 feat: expand helper macros 2020-09-10 14:25:07 -07:00
Leonardo de Moura
d77dc5efb8 feat: add helper syntax 2020-09-10 13:31:45 -07:00
Leonardo de Moura
61bd10997a feat: add coercions for the new frontend 2020-09-10 13:24:13 -07:00
Leonardo de Moura
6b7088e71a fix: too restrictive condition 2020-09-10 11:20:09 -07:00
Leonardo de Moura
232fe8cadd doc: document parser trick 2020-09-10 11:20:09 -07:00
Leonardo de Moura
20152c1192 chore: change by precedence 
@Kha it now uses the same precedence of `fun`.
The main motivation is to allow us to write `@by { ... }` instead of
`@(by { ... })`.

BTW, I am considering disabling implicit lambdas for `by ...` expressions.
It is automatically "intro"ducing the implicit variables without
giving an opportunity for users to pick their names.
 2020-09-10 11:17:42 -07:00
Leonardo de Moura
b136c519e2 fix: scope and improve error message 2020-09-09 16:44:43 -07:00
Leonardo de Moura
02fc447b04 fix: error message 2020-09-09 16:42:41 -07:00
Leonardo de Moura
20bc004c70 feat: improve subst tactic 2020-09-09 16:20:15 -07:00
Leonardo de Moura
83410083a8 fix: do not generate code for noncomputable definitions 2020-09-09 15:28:41 -07:00
Leonardo de Moura
c78d0cf1f8 feat: use | position for reporting dependent-match elimination errors 2020-09-09 14:07:23 -07:00