GitLab

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

Check all unit tests results against the version of cduce in master.
Many signature are syntactically different because of more liberal
use of parenthesis.

All problems related to the introduction of the new syntax for
constructed types