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

4460 commits

Author SHA1 Message Date
Leonardo de Moura
2b58ecea60 chore: fix test 2020-06-08 16:13:52 -07:00
Leonardo de Moura
f46dcd7a13 chore: fix some tests 2020-06-08 16:12:06 -07:00
Leonardo de Moura
dd1aa2f271 chore: improve error message 
cc @Kha
 2020-06-08 16:12:05 -07:00
Leonardo de Moura
c6ea675cae chore: fix test 
@Kha The error message changed. Not sure the new one is expected. It
is due to the change in `trailingLoop`. We can discuss it in the next
meeting.
 2020-06-08 16:12:05 -07:00
Leonardo de Moura
aa66fc376b chore: fix test 2020-06-08 16:12:05 -07:00
Leonardo de Moura
b3a8d417b2 chore: fix test 2020-06-08 16:12:05 -07:00
Leonardo de Moura
62cf913d6a fix: interaction between errToSorry and observing. 
@Kha I implemented the solution 1 I described at Zulip.
I also tried to document the issue, and made sure test
`choiceMacroRules` fail if the bug is reintroduced.
 2020-06-08 12:37:43 -07:00
Leonardo de Moura
947369b4ce chore: Parenthesizer issues after removing sortApp 
@Kha Could you please double check these modifications.

I added a no-op for `checkRbpLt`. It is used at the `Sort` and `Type`
parsers.
As I described in previous commits, the `checkRBPGreater` comment and
implementation were misleading. It was actually succeeding when the
rbp was less than or equal to the given parameter. So, it was renamed
to `checkRbpLe`. So, is the depArrow parenthesizer ok? I did not check.

I updated the PPRoundtrip.lean.expected.out to make sure the tests
succeed, but we should revise it if there is a problem with the
modifications at Parenthesizer.lean
 2020-06-03 15:46:33 -07:00
Sebastian Ullrich
6614b4d6e3 fix: use exact instead of prefix token match when inheriting precedence 
/cc @leodemoura :)
 2020-05-28 14:14:52 +02:00
Leonardo de Moura
5dffa0093a feat: retrieve implicit lbp from Environment at syntax command 
@Kha It is not clear to me why I had to change the following line
```
-syntax term ">>>" term : foo
+syntax term:1 ">>>":1 term : foo
```
The test breaks without it.
 2020-05-27 17:11:57 -07:00
Leonardo de Moura
17b6957f6c chore: fix tests 2020-05-26 15:05:01 -07:00
Leonardo de Moura
9c0bd9dd41 chore: fix tests 2020-05-26 15:05:00 -07:00
Sebastian Ullrich
c11e88c768 test: Reparen: don't remove parentheses in syntax quotations 2020-05-26 14:32:42 +02:00
Sebastian Ullrich
674fea4876 fix: parenthesizer: adjust lbp after parenthesization 2020-05-26 14:32:42 +02:00
Sebastian Ullrich
b519997b58 feat: parenthesizer: handle choice 2020-05-26 14:32:42 +02:00
Sebastian Ullrich
60ac03916e feat: introduce anonymous antiquotations for all categories 2020-05-26 14:32:42 +02:00
Sebastian Ullrich
9247911e09 fix: basic parenthesizer approach, document 2020-05-26 11:26:57 +02:00
Sebastian Ullrich
52b9bb35ea test: reparenthesize files 2020-05-26 11:26:57 +02:00
Leonardo de Moura
a01552d361 chore: fix some tests 
Two of them are still broken due to a bug in the new elaborator.
 2020-05-21 09:50:20 -07:00
Leonardo de Moura
3ea9edbd13 chore: test for simulating old { Prod . ... } syntax 2020-05-20 16:06:57 -07:00
Leonardo de Moura
22ae065d16 feat: add { ... : <expected-type> } syntax 
It replaces the `{ <struct-name> . ... }` syntax.
 2020-05-20 15:24:27 -07:00
Leonardo de Moura
bd58048449 chore: { <source> with ... } syntax 2020-05-20 15:08:43 -07:00
Sebastian Ullrich
3d891be49e feat: delaborator: do not set whitespace information 2020-05-20 11:54:53 -07:00
Sebastian Ullrich
10253e89ea chore: move bin/ and .oleans into build directory 2020-05-14 14:47:54 +02:00
Sebastian Ullrich
053d4bab1c chore: factor out and unify common test behavior; retrieve lean from PATH 
`./test_single.sh foo.lean yes` is now `./test_single.sh -i foo.lean`
 2020-05-14 14:38:52 +02:00
Sebastian Ullrich
2325f5d358 chore: ignore more test output files 2020-05-14 14:38:52 +02:00
Sebastian Ullrich
bc40796729 chore: remove fail/ tests 
Checking for *any* failure is never a good idea. Use `$f.expected.ret` instead.
 2020-05-14 14:38:52 +02:00
Leonardo de Moura
ebc0663b3f chore: fix tests 2020-05-12 15:02:03 -07:00
Sebastian Ullrich
386c706f3e feat: basic parenthesizer 2020-05-04 14:28:36 -07:00
Sebastian Ullrich
e7920bcdb5 chore: remove test special case 2020-05-04 11:11:11 +02:00
Sebastian Ullrich
8f67db0101 refactor: never implicitly ignore monadic results 
Also change `do e; f` to desugar to `e *> f` so that it is affected as well
 2020-04-23 11:09:59 -07:00
Marc Huisinga
aa4fc12dff feat: translate and refactor Gabriel Ebner's JSON parser 
implement the JSON parser from https://github.com/gebner/lean4/tree/server by @gebner using new Lean 4 syntax and fix some minor bugs.
 2020-04-15 11:29:18 -07:00
Leonardo de Moura
7322345768 fix: private names 
@Kha I tried to fix a few issues with private names. The new test
tries to cover them. If you have more, please create an issue.

1- Scoping. A private declaration should shadow one in a previous scope.
2- We should not be able to define the same `private` in the same
module more than once.
   ```
   private def x := 10
   private def x := "hello" -- should produce error here
   ```
3- Dot-notation should work with private declarations in the module
where they were defined.
4- The following should work
   ```
   namespace N
   private def x := 10
   end N
   #check N.x
   ```
5- The following should **not** work
   ```
   def y := 10
   private def y := "hello" -- produce error

   private def z := 10
   def z := "hello" -- produce error
   ```
   BTW, I am happy to change this behavior. I just mimicked C's
   behavior for `static`.

It is not clear whether the following should work or not.
```
    namespace N
      private def b := 10
    end N
    open N
    #check b
```
 2020-04-09 16:28:21 -07:00
Leonardo de Moura
360cebf680 fix: induction tactic must check expected major premise type 
`whnfUntil` now returns `Option Expr`.
 2020-04-09 11:18:02 -07:00
Leonardo de Moura
9a5bed0f94 fix: missing ! at whnfUntil 2020-04-09 10:49:20 -07:00
Leonardo de Moura
7a5fcfae8b feat: add [recursor] attribute to Iff.elim 2020-04-09 10:45:27 -07:00
Leonardo de Moura
40336131bb feat: do not switch to term mode in the RHS of induction and cases tactics 2020-04-08 17:45:06 -07:00
Daniel Selsam
7c1c0dc01e test: example that requires the instance arg reordering 2020-04-08 16:56:14 -07:00
Leonardo de Moura
e22af8d1ef feat: add FloatArray 
cc @dselsam
 2020-04-07 18:05:54 -07:00
Leonardo de Moura
b8ea55c989 feat: expose some transcendental functions from the C library 
cc @dselsam
 2020-04-06 15:22:25 -07:00
Leonardo de Moura
8e84a8c9ec feat: Float from big numbers 2020-04-06 14:05:17 -07:00
Leonardo de Moura
746615d81d chore: remove ⇒ as alternative for => 2020-04-06 13:45:22 -07:00
Leonardo de Moura
22fc56f5c8 chore: fix test 2020-03-31 10:10:57 -07:00
Leonardo de Moura
af8bc28be0 fix: typo at IR.Expr.alphaEqv 2020-03-31 10:04:59 -07:00
Daniel Selsam
722ea2b694 failing test for suspicious behavior 2020-03-31 10:03:22 -07:00
Sebastian Ullrich
b6fc9428f1 fix: support Windows newlines and '\r' escape 2020-03-27 13:21:21 -07:00
Leonardo de Moura
0595e8a78a feat: add tryPureCoe 
@Kha It seems to work reasonably well. It didn't break any test.
 2020-03-27 11:20:43 -07:00
Sebastian Ullrich
fcdbdeecaf feat: delaborator: use implicit lambdas where possible 
/cc @leodemoura it's not bullet-proof (unless `pp.explicit` is set), but let's
see if it is good enough in practice
 2020-03-27 14:55:46 +01:00
Sebastian Ullrich
db93638a96 feat: delab forallE 2020-03-27 11:59:58 +01:00
Leonardo de Moura
02acdee9ce feat: disable implicit lambda insertion for fun containing {} or [] 
cc @Kha
 2020-03-26 14:32:12 -07:00