 16 Feb, 2015 1 commit


Kim Nguyễn authored
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 reorder 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 leftassociative) 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).

 15 Feb, 2015 2 commits


Kim Nguyễn authored
containing variables but no toplevel variables would not be printed as regular expressions but nested pairs.

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

 13 Feb, 2015 2 commits


Kim Nguyễn authored

Kim Nguyễn authored

 10 Feb, 2015 3 commits


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

Kim Nguyễn authored

Kim Nguyễn authored

 19 Dec, 2014 2 commits


Giuseppe Castagna authored

Giuseppe Castagna authored

 18 Dec, 2014 1 commit


Giuseppe Castagna authored

 16 Dec, 2014 4 commits


Giuseppe Castagna authored

Giuseppe Castagna authored

Giuseppe Castagna authored

Giuseppe Castagna authored

 14 Dec, 2014 2 commits


Kim Nguyễn authored

Kim Nguyễn authored
compiles with the patched camlp4 bundled with fedora 21)

 06 Dec, 2014 3 commits


Kim Nguyễn authored

Kim Nguyễn authored
Positive.solve(Positive.decompose t) was not the identity but added spurious types at toplevel. Added more test cases in polyok.cd to cover such regressions

Kim Nguyễn authored

 04 Dec, 2014 1 commit


Kim Nguyễn authored

 01 Dec, 2014 9 commits


Kim Nguyễn authored
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].

Kim Nguyễn authored
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 redblack trees examples that are now in a separate file  redblack.cd is a fully typechecking file  rbfail.cd has the type definition and the wrong balance function.

Kim Nguyễn authored
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 lefthandside 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.

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

Kim Nguyễn authored

Kim Nguyễn authored
Delay the check that detects types variables occurring in patterns until typechecking time (this allows us to have access to delta and thus know the monomorphic variables, which are allowed)

Kim Nguyễn authored

Kim Nguyễn authored
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.

Kim Nguyễn authored

 27 Oct, 2014 3 commits


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

Giuseppe Castagna authored

Pietro Abate authored

 16 Oct, 2014 2 commits


Pietro Abate authored

Kim Nguyễn authored
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.

 06 Oct, 2014 1 commit


https://git.cduce.org/cducePietro Abate authored

 05 Oct, 2014 1 commit


Julien Lopez authored

 03 Oct, 2014 1 commit


Pietro Abate authored
This reverts commit c9ad3e5c. Conflicts: types/var.ml typing/typer.ml

 19 Sep, 2014 2 commits


Pietro Abate authored

https://git.cduce.org/cducePietro Abate authored
