GitLab

This reverts commit a8ba6ab6.

This commit introduces a regression where suprious type variables are introduced in the final type.

Seal the representation of SortedList.Make(X).t (by making the type private). Expose Var.Set as a SortedList.S

Perform a more aggressive memoization of substituted types and register the name if the original type was named.
Make the pretty-printer re-entrant.

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

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

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.

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

Add a global variable table, so when we call "Var.mk id" twice, the
same variable is returned and when we call "Var.fresh v" we always
return a truly globally fresh variable.

- type t 'a = ('a,'a)
- type t ('a,'b) = ('a,'b)

Fix Typer.pp_env printer for types
Minor code refactring

Conflicts:
	Makefile.distrib
	depend

Change $$ in >> in types.ml for the substitution operator

Do not generate equations for monomorphic variables, during the generation of type equation from constraints.

- New fresh variables now share the same str, but different freshness index
- Remove the function is_internal from var module

Fix a pretty printing error for ground types (the negative part was not shown due to "worth_complement" being called twice).

Fix a pretty printing error for ground types (the negative part was not shown due to "worth_complement" being called twice).

Rework the type variable infrastructure. Remove it from the type structure and have the auxiliary function cache the results as needed.

when a constraint 'a < t or t < 'a with 'a being monomorphic occurs during constraint generation, we check whether
it holds for all 'a, that is we use plain subtyping.
(It generalizes the fact that 'a < Any or Empty < 'a hold for monomorphic variables, but also accounts for constraints such as 'a < 'a | t and so on).

- Change the precedence of the XML constructor to be stronger than the set-theoretic operations (compatibility with previous CDuce)
- Pretty-printing of regular expressions. When the input type contains a sequence type, print the sequence as a regular expression. Do not print empty sequences unless the rest of the atom components is finite:
     `a |`b | `nil
will be printed as
     [] | `a | `b
but
     Atom \ 'a
will be printed as
     Atom \'a
and not
     Atom \ ('a | `nil) | []
- Remove Arrow from positive arrow part (unless it is the only component)
- Fix a bug where records would be printed instead of attributes