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

5307 commits

Author SHA1 Message Date
Sebastian Ullrich
4a22854b1e chore: make server tests fixable 2020-12-27 15:05:29 +01:00
Sebastian Ullrich
bbafd80322 chore: token antiquotations: return/take full Syntax (but only use head info of it) 
/cc @leodemoura
 2020-12-26 23:54:46 +01:00
Sebastian Ullrich
837d6a1529 chore: fix test 2020-12-26 21:12:51 +01:00
Leonardo de Moura
4450b8567d fix: sigma notation precedence 2020-12-26 09:35:40 -08:00
Leonardo de Moura
01f8127c16 fix: position information at expandDoIf? 2020-12-26 08:26:54 -08:00
Wojciech Nawrocki
a2760d0144 test: multi-process server 2020-12-26 13:22:47 +01:00
Leonardo de Moura
48b92a4486 fix: error message and test 2020-12-25 10:03:42 -08:00
Leonardo de Moura
f05cbd1365 test: add test for "broken for" 2020-12-25 10:03:42 -08:00
Leonardo de Moura
b855d79718 feat: filter "failed to synthesize ..." errors when there are other errors 2020-12-25 10:03:42 -08:00
Sebastian Ullrich
b2fda9b9ae chore: disable randomly failing test 
/cc @mhuisi @Vtech234
 2020-12-25 18:48:58 +01:00
Sebastian Ullrich
c3c27f8dd3 feat: lift restriction on number of antiquotations in splice 
/cc @leodemoura
 2020-12-25 18:41:03 +01:00
Sebastian Ullrich
4878f0d13e fix: delaborator: correctly toggle individual when setting pp.all 2020-12-25 16:12:04 +01:00
Leonardo de Moura
480462fa24 feat: improve {...} error message 2020-12-24 09:35:55 -08:00
Leonardo de Moura
207b8a8c37 chore: fix test 2020-12-24 09:23:05 -08:00
Leonardo de Moura
87207030ce test: pretty printing if-then-else 
@Kha We will probably have to write a handwritten formatter in the
future. The new test shows some limitations with `do`, `else if`, ...
where we want the output
```
      if x == 0 then do
        IO.println "foo"
        IO.println "zero"
      else if x % 2 == 0 then do
        IO.println x
        IO.println "even"
      else do
        IO.println x
        IO.println "odd"
```
 2020-12-24 08:40:30 -08:00
Sebastian Ullrich
f42bd8f693 chore: deactivate server tests for now 2020-12-23 20:00:36 +01:00
Wojciech Nawrocki
1b9ae69729 feat: port basic server tests 2020-12-23 20:00:36 +01:00
Leonardo de Moura
ef51087138 feat: do not log error messages with synthetic sorry's 
Before this commit, only error messages caught at `elabTerm` were
filtered.

cc @Kha
 2020-12-23 10:52:27 -08:00
Leonardo de Moura
edb51b8977 test: implicit lambdas in action 2020-12-23 10:24:00 -08:00
Leonardo de Moura
74686a149a test: add structure field default value test 2020-12-23 08:35:27 -08:00
Leonardo de Moura
e74ba14f4c feat: modify structSimpleBinder parser 
@Kha It felt odd that we can write
```
   map f x := ...
```
in instances, but we had to write
```
   map (f x) := ...
```
when setting the field default value in a class.
 2020-12-23 08:23:14 -08:00
Leonardo de Moura
7720b843bb feat: allow users to use binders when setting default value for parent fields 2020-12-23 08:12:29 -08:00
Leonardo de Moura
df03130927 feat: improve error message 2020-12-22 17:50:26 -08:00
Leonardo de Moura
800b4af15d test: indentation 2020-12-22 14:53:03 -08:00
Leonardo de Moura
839017fdae feat: add macro tactical solve 2020-12-22 14:36:20 -08:00
Leonardo de Moura
832c7412d6 feat: add first tactical 
@Kha It has a few advantages over `<or>` (`<|>`).
- It is not an infix operator.
- It takes tactic sequences instead of tactics as arguments

For example, we can write
```
  first
    | apply h1; assumption
    | exact y; exact h3; assumption
```
or
```
first apply h1; assumption | exact y; exact h3; assumption
```
instead of
```
(apply h1; assumption) <|> (exact y; exact h3; assumption)
```
 2020-12-22 14:10:07 -08:00
Leonardo de Moura
69d83ecb86 chore: make sure term and tactic parsers have disjoint infix operators 2020-12-22 14:10:07 -08:00
Leonardo de Moura
18aee9de30 fix: precedence issues at tactic DSL 2020-12-22 14:10:06 -08:00
Leonardo de Moura
289ed6485d feat: eval allGoals 2020-12-22 09:52:54 -08:00
Leonardo de Moura
f638269a71 fix: name resolution at syntax command 
This commit also cleans up `toParserDescr`+`toParserDescrAux`.
 2020-12-22 08:40:00 -08:00
Sebastian Ullrich
1c31240ebb feat: token antiquotations in macro 2020-12-22 13:11:04 +01:00
Sebastian Ullrich
07c7638fd7 feat: token source info antiquotations tk%$id 
/cc @leodemoura
 2020-12-22 13:11:04 +01:00
Leonardo de Moura
43255a4af3 feat: local and scoped macros 2020-12-21 17:08:25 -08:00
Leonardo de Moura
1d5df4f28b test: matrix notation example 
- Heterogeneous `*` for matrix and scalar multiplication
- Homogeneous `+` for matrix addition
- Whitespace sensitive `x[i, j]` notation
 2020-12-21 16:40:52 -08:00
Leonardo de Moura
0083e1996a fix: scoped tokens 
Tokens introduced by scoped (local) parsers should be scoped (local).
 2020-12-21 13:11:09 -08:00
Leonardo de Moura
4fc06bfcca feat: add optional (priority := <prio>) to instance command 2020-12-21 10:02:12 -08:00
Leonardo de Moura
43284cc5fa feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
Leonardo de Moura
856559a983 chore: fix test output 2020-12-21 07:38:59 -08:00
Leonardo de Moura
c524bcf2d3 feat: improve universe level pretty printer 2020-12-21 07:34:48 -08:00
Sebastian Ullrich
3e77c7cdef fix: error position 2020-12-21 16:25:01 +01:00
Sebastian Ullrich
756d7643f0 chore: rename syntaxMaxDepth option for consistency and discoverability 
/cc @leodemoura
 2020-12-21 16:25:01 +01:00
Sebastian Ullrich
c54f9dd8c8 feat: "slice" patterns [$x, $y, $zs,*, $w] in syntax match 
/cc @leodemoura
 2020-12-21 15:29:46 +01:00
Leonardo de Moura
340cade575 fix: bug at specialize.cpp 2020-12-20 17:48:46 -08:00
Sebastian Ullrich
bc3e9ce961 feat: if let pat ← ... 2020-12-20 23:58:29 +01:00
Sebastian Ullrich
90f747e346 fix: don't change antiquotations semantics in do if 2020-12-20 17:51:37 +01:00
Sebastian Ullrich
eeb0cad29e feat: if let 
/cc @leodemoura
 2020-12-20 16:46:03 +01:00
Sebastian Ullrich
fdbec9101f fix: pattern reordering in syntax match 2020-12-20 13:52:25 +01:00
Leonardo de Moura
91f0e29285 feat: parallel for 2020-12-19 20:01:04 -08:00
Leonardo de Moura
074259201e feat: add helper classes for implementing parallel for 
It is based on an approach suggested by Andrew Kent, and refined by
Sebastian Ullrich.

TODO: expand the the parallel `for`s at `Do.lean`.
 2020-12-19 14:15:47 -08:00
Sebastian Ullrich
efc2b79aba feat: as patterns in syntax match 
@leodemoura no problem using the new architecture :)
 2020-12-19 22:03:37 +01:00