GitLab

to use two lexers (depending on whether we are between square brackets
or not) is too brittle (it crudely tries to parse
 ``( [whitespace] 'a  [whitespace] )'' as a variable, to force the user
to write the variable beetween parenthesis. However this does not scale
to types with two arguments (says [ t ('a, 'b) ]).

We use a simpler heuristic (with look ahead)

(1) try to see if the regular expression

' (anything but ', \n)* '(anything but the first letter of an identifier)

can be found. If so, we put back the lexeme in the buffer and parse it as as
a string.

(2) if (1) failed, try to parse it as a variable

(3) if (3) failed, try to parse it again as a string. We are
guaranteed to fail here but it means we have a malformed string, so we
parse as a string to get a proper error message.

The only thing this does not cover are cases like
type t = [ 'abcd'Int ]
which was tokenized before as [, 'abcd', Int, ]
and is now tokenized as [, 'abcd, 'Int, ]
It does not seem to be a problem in practice though (since in the code
I have seen thus far, people were at least putting a space).
it is easy to emmit a warning in this case, suggesting the user to add
a whitespace to get the old behaviour back.

requiring an abscence of whitespace between ``t'' and ``(''.  Outside
of regular expression contexts, ``t (t1, …, tn)'' is parsed with a
higher precedence than & and \, to allow one to write
``t (Int) & Bool'' without extra parentheses (i.e.
``(t (Int)) & Bool'').  Inside a regular expression, type
instantiation and sequencing become ambiguous, and there is no way to
distinguish syntactically: ``[ Int (Int, Int) ]'' from
``[ t (Int, Int) ]''. The former should resolve to a sequence while
the latter only makes sense as an instantiation (if ``t'' is a
parametric type). Both are treated as element sequencing and
disambiguated during identifier resolution (more precisely during the
"derecurse" phase, before typechecking).

Note that due to the lower precedence of sequencing w.r.t to other
regular expression constructs, a type ``[ t (Int)* ]'' will be parsed
correctly, but yield an error message saying that t is not fully
intantiated. One has to write ``[ (t (Int))* ]'' which is similar to
function applications for expressions.

Finally, we also re-order sequencing after typing to always group a
potential type instantiation with its argument, i.e. we transform
sequences such as
``[ t1 t2 t3 ... tn ]'' (which are parsed as
``[ (((t1 t2) t3) ... tn) ]'' because sequence concatenation is
left-associative) into ``[ ... (ti tj) ... ]'' if ``ti'' is an
identifier and ``tj'' is of the form ``(s1,...,sk)''. This is sound
because concatenation of regular expression is associative (and the
original sequence would fail, anyway).

containing variables but no toplevel variables would not be printed as
regular expressions but nested pairs.

Now functions such as
let fun f (x:Int):Int = ...
are parsed correctly (that is, its parameter is 'x' with type Int).

sequence type would not show up (e.g. 'a & [ Any *] would be displayed
as [ Any * ], while the 'a would still be present internally).

compiles with the patched camlp4 bundled with fedora 21)

Positive.solve(Positive.decompose t) was not the identity but added spurious types at toplevel.

Added more test cases in poly-ok.cd to cover such regressions

type has already been normalized. Without this patch, in the following usage:

norm(T1, delta)
norm(<a>[ T1 ], delta)

the fact that T1 has already been normalized against some delta is not taken into
account while normalizin <a>[T1].

table instead of a 'recursion set' like in the paper.  The hash table
is tricky:

 - its keys should be both the type we are normalizing and
delta

 - we should store a flag together with the constraint set, indicating
whether the computation of the normalization for the corresponding
type has finished. If it has, we can use the associated constraint set
instead of CS.sat and stop recursion. If it has not, we can return
CS.sat (like the previous base case).

We also update the test case files to check that everything is in order:

- part2.cd has been rewritten to make use of the new syntax and remove
  the red-black trees examples that are now in a separate file

- red-black.cd is a fully typechecking file
- rb-fail.cd has the type definition and the wrong balance function.

when a type such as

type t('a) = (Int,'a)

is introduced, the variables occuring in the definitions are replaced by fresh occurences.
The variables in the left-hand-side were note renamed accordingly, yielding a type definition:

type t('a_0) = (Int, 'a_1)

when performing type substitutions, none of the occurences of 'a_1 were replaced.

Simplify (and fix) the code adding variables of a function interface to delta during the typing of its body.

Delay the check that detects types variables occurring in patterns until type-checking time (this allows us to have access to delta and thus know the monomorphic variables, which are allowed)

Revert "Partially revert commit 46a5262a (only file typing/typer.ml) to make balance type (in toplevel). This should be investigated more thoroughly."

This partial revert allows us to typecheck the wrong version of balance.

This reverts commit b98abca3.

Partially revert commit 46a5262a (only file typing/typer.ml) to make balance type (in toplevel). This should be investigated more thoroughly.

Fix variable ordering problem by adding a 'kind' field inside variables so that variables of the function type are processed before arguments types and after Gamma.

This reverts commit c9ad3e5c.

Conflicts:
	types/var.ml
	typing/typer.ml