- 06 Dec, 2014 1 commit
-
-
Kim Nguyễn authored
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
-
- 01 Dec, 2014 2 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 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.
-
- 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.
-
- 03 Oct, 2014 1 commit
-
-
Pietro Abate authored
This reverts commit c9ad3e5c. Conflicts: types/var.ml typing/typer.ml
-
- 19 Sep, 2014 1 commit
-
-
Pietro Abate authored
All problems related to the introduction of the new syntax for constructed types
-
- 16 Sep, 2014 1 commit
-
-
Pietro Abate authored
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.
-
- 10 Sep, 2014 1 commit
-
-
Pietro Abate authored
-
- 08 Sep, 2014 3 commits
-
-
Pietro Abate authored
-
Pietro Abate authored
- type t 'a = ('a,'a) - type t ('a,'b) = ('a,'b) Fix Typer.pp_env printer for types Minor code refactring
-
Kim Nguyễn authored
Conflicts: Makefile.distrib depend Change $$ in >> in types.ml for the substitution operator
-
- 28 Aug, 2014 2 commits
-
-
Kim Nguyễn authored
Do not generate equations for monomorphic variables, during the generation of type equation from constraints.
-
Pietro Abate authored
- Var identifiers are now of type U.t instead of string - Remove TVar from ast. Polymorphic variables are just types
-
- 26 Aug, 2014 2 commits
-
-
Pietro Abate authored
-
Pietro Abate authored
- New fresh variables now share the same str, but different freshness index - Remove the function is_internal from var module
-
- 25 Aug, 2014 1 commit
-
-
Pietro Abate authored
-
- 21 Aug, 2014 3 commits
-
-
Kim Nguyễn authored
-
Pietro Abate authored
Now gamma is correctly propagated in the compilation Enviroment and substitions are correctly applied to abstractions
-
Pietro Abate authored
-
- 20 Aug, 2014 1 commit
-
-
Pietro Abate authored
-
- 19 Aug, 2014 4 commits
-
-
Pietro Abate authored
-
Pietro Abate authored
-
Pietro Abate authored
-
Pietro Abate authored
-
- 15 Jul, 2014 2 commits
-
-
Kim Nguyễn authored
-
Kim Nguyễn authored
-
- 14 Jul, 2014 5 commits
-
-
Kim Nguyễn authored
Fix a pretty printing error for ground types (the negative part was not shown due to "worth_complement" being called twice).
-
Kim Nguyễn authored
Fix a pretty printing error for ground types (the negative part was not shown due to "worth_complement" being called twice).
-
Kim Nguyễn authored
Rework the type variable infrastructure. Remove it from the type structure and have the auxiliary function cache the results as needed.
-
Kim Nguyễn authored
-
Kim Nguyễn authored
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).
-
- 13 Jul, 2014 2 commits
-
-
Kim Nguyễn authored
- 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
-
Kim Nguyễn authored
- Simplify the pretty-printing descriptor type - Fix a bug where some unions were shown as intersections - Correctly display parentheses where needed (issue: #17) - Prevent sharing for "small" subtrees (AST less than 6 nodes), so: (Int -> Int) -> Int -> Int is not shown as: X1 -> X1 where X1 = Int -> Int (but bigger types are).
-
- 12 Jul, 2014 1 commit
-
-
Kim Nguyễn authored
-
- 11 Jul, 2014 2 commits
-
-
Kim Nguyễn authored
distribute it (redudantly) under all variables to simplify their pretty-printing. Hence, instead of having e.g. : ('a \ (Int)) | Char | Int | Atom) we have ('a | Char | Int | Atom)
-
Kim Nguyễn authored
-
- 10 Jul, 2014 3 commits
-
-
Kim Nguyễn authored
-
Kim Nguyễn authored
Remove commented code in clean_type. Restore cleaning of variables that are in covariant position in the result type, to avoid having strange types such as: [] -> [ ('b) * ]
-
Kim Nguyễn authored
Given a type for which each kind is i DNF : ints: \/ /\a /\v /\~b /\~w chars: \/ /\a /\v /\~b /\~w ... where a, b are atoms and v w toplevel variables, index the type by pairs of variables, for each kind, which gives a matrix of 8 lines. ... (v, w) ... (x,y) ... ints: t1 t1 chars: ... ... atoms: times: xml: arrow: record: abstract: t8 t8 let T = t1 | ... | t8, we can write ((v & w) | (x & y)) & T we now try to factor according to variables (intersection of v x and w y) to have a type of the form: ('a | ... | 'd) & 'e ... & (Any \ 'f) & T
-