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

14117 commits

Author SHA1 Message Date
Sebastian Ullrich
77cbaa752c fix: Task: make reference and -j0 semantics eager, simplify 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
5b83ceb1b5 feat: IO.mapTask, IO.bindTask 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
307a833798 feat: implement IO.asTask as primitive using always-run tasks 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
1782352af1 feat: optionally run tasks even when already cancelled 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
c672bd657f feat: IO.asTask 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
e14e76775f fix: ensure *println functions are atomic 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
bdea7c7b14 feat: lean: initialize task manager from -j flag 2020-09-14 17:57:33 +02:00
Leonardo de Moura
c3623e9a0a chore: reduce default max steps 2020-09-13 16:18:53 -07:00
Leonardo de Moura
5da7f0b50b fix: set constApprox := false at SynthInstance 
We don't want contraints such as
```
?m a =?= Nat
```
to be solved as
```
?m := fun a => Nat
```
durint type class resolution.
 2020-09-13 16:11:27 -07:00
Leonardo de Moura
2ee1821f13 fix: ensure expectedType at fun body 2020-09-13 13:44:05 -07:00
Leonardo de Moura
7b90f7d956 fix: synthesize pending mvars before trying coercions to Fun 
`tests/lean/repr_issue.lean` cannot be elaborated with this modification.
 2020-09-13 13:19:05 -07:00
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