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

5622 commits

Author SHA1 Message Date
Sebastian Ullrich
26ed304071 fix: pretty print simplified macro scopes 2020-09-17 17:13:50 +02:00
Sebastian Ullrich
3834a89cdc feat: activate new pretty printer 2020-09-17 08:12:28 -07:00
Sebastian Ullrich
0b9e46eee5 chore: universe-+ spacing 2020-09-17 08:12:28 -07:00
Sebastian Ullrich
fad4660135 feat: pretty print space between binders 2020-09-17 08:12:28 -07:00
Sebastian Ullrich
986bb17e34 test: remove broken test case 2020-09-17 08:12:28 -07:00
Sebastian Ullrich
131f30f7a9 feat: pretty print tuples 2020-09-17 08:12:28 -07:00
Sebastian Ullrich
27d936ffa5 feat: pretty print structure instances 2020-09-17 08:12:28 -07:00
Sebastian Ullrich
bacc77efa1 feat: delaborate builtin operators 2020-09-17 08:12:28 -07:00
Sebastian Ullrich
4f5b59ad02 feat: pretty print shortened names (export/open/namespace/private) 2020-09-17 08:12:28 -07:00
Leonardo de Moura
b37158f4f8 fix: apply 2020-09-16 16:18:30 -07:00
Leonardo de Moura
9f5e63cd3c feat: add option pp.macroStack 
@Kha I set it to `false` by default.
 2020-09-16 15:29:28 -07:00
Leonardo de Moura
965a989dc2 fix: must log at evalCommand 
Some macros expand a command into multiple commands. We should not
interrupt the elaboration of the command sequence when one fails.
 2020-09-16 14:55:58 -07:00
Leonardo de Moura
751db760d5 fix: sanitizeNames 
A macro scoped name cannot shadow a name without macro scopes.
 2020-09-16 13:54:30 -07:00
Leonardo de Moura
e10cd085f4 feat: use sanitizeNames at ppGoal 2020-09-16 13:39:06 -07:00
Leonardo de Moura
16ec9db1fc chore: fix test 2020-09-16 13:12:00 -07:00
Leonardo de Moura
e88e398642 fix: multiple occurrences of named holes 
@Kha I added a new test with the scenarios we discussed this morning.
 2020-09-16 10:27:30 -07:00
Leonardo de Moura
544d2f4ce5 fix: kind for type metavariable 
For example, `mkFreshExprMVar none MetavarKind.synthetic` should
create a fresh synthetic metavariable `?m` with type `?t` where `?t`
is a fresh natural metavariable. If users want a synthetic
metavariable `?t`, then it must create it themselves.
 2020-09-16 08:24:15 -07:00
Leonardo de Moura
0abca5475f refactor: move ppExpr to IO 
@Kha I am also tracking `currNamespace` and `openDecls`.

BTW, I also tried an experiment where I added `currNamespace` and
`openDecls` to `Meta.Context`, but it looked weird. This information
is only needed in the elaborator and pretty printer.
The `PPContext` object should contain everything you need. You
can put `currNamespace` and `openDecls` in the `Delaborator.Context`.
 2020-09-15 18:48:21 -07:00
Leonardo de Moura
1ce80d5ba7 feat: hide auxiliary declarations 2020-09-15 16:50:16 -07:00
Leonardo de Moura
19a7927f10 feat: sanitizeNames 
@Kha I am using `_shadowed.<idx>` suffix for marking variables that
have been shadowed. It is a bit verbose, but at least it is easy to
understand understand error messages such as
```
shadow.lean:4:0: error: type mismatch
  h
has type
  x._shadowed.1 = x._shadowed.1
but it is expected to have type
  x = x
```
It is better than the old cryptic version
```
shadow.lean:4:0: error: type mismatch
  h
has type
  x = x
but it is expected to have type
  x = x
```
 2020-09-15 16:28:50 -07:00
Leonardo de Moura
4e99b19a96 fix: expandMatchDiscr cannot be a macro 
The `matchType` created by the macro is bad for dependent pattern
matching. The `tst8` and `tst9` at `matchTac` failed to be elaborated
when using the macro.
 2020-09-15 13:29:28 -07:00
Leonardo de Moura
75814c2d21 chore: fix tests 2020-09-15 11:11:05 -07:00
Leonardo de Moura
3ebecc8caa test: open and export 2020-09-15 10:46:40 -07:00
Sebastian Ullrich
1e6faf3f28 test: ignore \r when diffing 2020-09-15 09:32:00 -07:00
Sebastian Ullrich
897f277a3e test: strip mvar suffixes 2020-09-15 09:32:00 -07:00
Leonardo de Moura
b8d90d77db feat: macro scope as the single mechanism for creating fresh names 
cc @Kha
 2020-09-14 20:09:07 -07:00
Leonardo de Moura
fde43e071d feat: improve matchType inference 2020-09-14 19:44:45 -07:00
Leonardo de Moura
cc3b48ce16 fix: check inductive datatype parameters in constructor resulting type 2020-09-14 16:56:13 -07:00
Leonardo de Moura
634f063631 feat: finish commit "using indentation" 2020-09-14 16:40:52 -07:00
Leonardo de Moura
ca90ff8b59 test: have-by in tactic mode 
@Kha By adding `have-by` macro (in term mode), we got `have-by` in
tactic mode without writing a single line of code :)
 2020-09-14 15:17:25 -07:00
Leonardo de Moura
a6b19cd4af feat: expand show-by and have-by macros 2020-09-14 15:08:28 -07:00
Leonardo de Moura
fc4ab139b5 feat: indented by 
@Kha This one is not as useful as the indented `do`. When writing
interactive proofs I like the error message at the `}` showing the
resulting tactic state. We can simulate it using a `skip` in the end of the sequence :)
We remove the `skip` when the proof is done. Note that, the last `;`
is usually not part of the `by`. Example:
```lean
theorem ex (x y z : Nat) : y = z → y = x → x = z :=
fun _ _ =>
  have x = y by apply Eq.symm; assumption; -- <<< the last `;` is part of the `have`
  Eq.trans this (by assumption)
```
 2020-09-14 14:20:02 -07:00
Leonardo de Moura
4c6a589e6c feat: indented do blocks 
@Kha it is soooooo much nicer :)
 2020-09-14 13:44:51 -07:00
Leonardo de Moura
163b0a7a3f fix: protected 
- `protected` outside of a namespace is an error.
- Fix `protected` in recursive definitions.

cc @Kha
 2020-09-14 13:09:04 -07:00
Leonardo de Moura
7c0216595e fix: remove duplicate error messages due to variable(s) 
In Lean4, we re-elaborate `variable`(s) for each command, but we don't
want the error messages due to `variable` to appear in the log
multiple times.
 2020-09-14 12:44:25 -07:00
Sebastian Ullrich
a93a53b4b5 feat: more IO Task functions 2020-09-14 17:57:33 +02:00
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
c672bd657f feat: IO.asTask 2020-09-14 17:57:33 +02:00
Leonardo de Moura
c58252ad74 chore: move more tests to new frontend 2020-09-13 16:13:20 -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
21c8366645 chore: fix test output 2020-09-13 13:50:00 -07:00
Leonardo de Moura
2ee1821f13 fix: ensure expectedType at fun body 2020-09-13 13:44:05 -07:00
Leonardo de Moura
32e26799ed chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
Leonardo de Moura
498d7886eb chore: fix test output 2020-09-13 13:21:58 -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
d936b9461f fix: always ensure expectedType when processing overloaded symbols and/or notation 2020-09-13 11:59:13 -07:00
Leonardo de Moura
c080d42692 chore: move tests to new frontend 2020-09-13 10:16:15 -07:00
Leonardo de Moura
897289599a fix: ignore auxiliary declarations at subst and assumption 2020-09-13 09:59:37 -07:00