Improve the surface language syntax

[florentc]

This introduces a new syntax to declare functions and fixes #131. It replaces the previous syntax. All the examples and tests have been rewritten accordingly. The dedicated test suite includes generic cases and regression tests for issues encountered during development.

Features

• Haskell-like function declaration syntax
• Basic line-folding for top-level declarations (functions and datatypes) relying on a Reader (Maybe Pos) where Pos is the column where the current line-folding section (if any) began
• Type @x and term x parameters (no need for lambdas and LAMBDAS anymore although they are still supported)
• Case statements (syntaxic support only, translation to system F to be implemented) on patterns made of constructors, variables, and catch-all patterns _)
• Explicit or implicit kind for type variables in both function and datatype declarations (e.g. forall (m : * -> *) a is the same as forall (m : * -> *) (a : *), and data Maybe a the same as data Maybe (a : *))

isJust : forall a . Maybe a -> Bool
isJust @x mx =
  case @Bool @(Maybe x) mx of {
    Nothing -> False ;
    Just _ -> True
  }

Other changes

• Migration of all example code and test suites to the new syntax
• Removal of the old syntax
• Extensive test suite for the new syntax
• Improved documentation in the parser module

Future work

More detailed issues will be open after this PR is merged.

• Translation of case statements to system F. Once this is done, replace calls to match_XXX functions by case statements in examples (especially in IsUnity) and tests throughout Pirouette

• Nested line-folding: support for nested line-folded sections is not trivial but would make it possible to get rid of the { ; ; ; } syntax in case statements and introduce let and where local function declarations (name clashes and name shadowing should be kept in mind when implementing this)

• Implicitly quantified type variables: isJust : Maybe a -> Bool would be equivalent to isJust : forall a . Maybe a -> Bool

• Implicit naming of type variables in function body: for isJust : forall a . Maybe a -> Bool, the body declaration isJust mx = would be equivalent to isJust @a mx (name clashes and name shadowing should be kept in mind when implementing this)

• Pattern matching directly in multiple function bodies: the Param type should rely on Pattern lang instead of String. The main question remains how to represent this when there are several pattern-matched function parameters: either as desugared nested case expressions ExprCase or in an adapted FunDecl type. The parser is ready for such a change and multi-bodies function declarations thanks to line folding, Pattern lang, and Param

• Adapt the pretty printer to provide output in the new syntax than can be parsed back