edwinb/Idris-dev — pull request #492 by ahmadsalim (2013-09-22 09:24:29+00:00)
Title: New Parser in Trifecta

Refactoring of old parser to Trifecta, documenting and updating some items/fixing some issues.
New features:
* Using Trifecta now for better built-in diagnostics, and support for better custom diagnostics in the future
* Grammar extracted and added to parser comments
* Every function has type declaration and every top-level function is documented with haddock
* Adding of to most choices to get better error messages when expecting something
* Fixed some line number error with regard to parsing references to functions
* Should support the following now (will write the tests later):
1. proof and tactics as blocks similar to do e.g.

```Idris
proof intros
compute
trivial
```
2. Documentation comments in comments e.g.
```Idris
{-
Commented method:
{-| Converts a boolean to integer -}
toInt :: Bool -> Int

toInt False = 0

toInt True = 1
-}
```
3. Where is optional on empty instances e.g.
```Idris
instance Eq MyTree
```
instead of requiring
```Idris
instance Eq MyTree where
```

4. A tactic sequence can hold more than two tactics
e.g.
```Idris
{ compute; { intros; trivial } }
```
can now be written as
```Idris
{ compute; intros; trivial }
```

5. using/params blocks can be empty e.g.
```Idris
using (x : List a)
{-
dup : x -> x
dup l = l ++ l
-}
```

6. should check for paranthesis closure before eof i.e.
```Idris
main : IO ()
main = do { return 2;
```
should now fail

7. Other small fixes

Test 002 commented because of temporary disabling of TT quotation
support (as we discussed on mailing list).

Regression Test 003 and Test 020 have updated expected values (which
fixes previously erranous line number report from old parser).