1. 14 Dec, 2014 1 commit
  2. 06 Dec, 2014 2 commits
  3. 01 Dec, 2014 2 commits
    • Kim Nguyễn's avatar
      Recursively check in the global normalisation hash table whether the · 86748961
      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's avatar
      Improve the complexity of constraint normalisation by using a hash · 7932c071
      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
       - 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.
  4. 16 Oct, 2014 2 commits
  5. 03 Oct, 2014 1 commit
  6. 16 Sep, 2014 1 commit
    • Pietro Abate's avatar
      Make fresh variables really fresh · c9ad3e5c
      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.
  7. 10 Sep, 2014 1 commit
  8. 08 Sep, 2014 3 commits
  9. 28 Aug, 2014 1 commit
  10. 26 Aug, 2014 2 commits
  11. 25 Aug, 2014 1 commit
  12. 21 Aug, 2014 2 commits
  13. 19 Aug, 2014 3 commits
  14. 15 Jul, 2014 2 commits
  15. 14 Jul, 2014 5 commits
  16. 13 Jul, 2014 2 commits
    • Kim Nguyễn's avatar
      - Introduce an abstract type for precedences used during pretty-printing. · 148cae0c
      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
           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's avatar
      More work on pretty-printing: · 83ef66d7
      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).
  17. 12 Jul, 2014 1 commit
  18. 11 Jul, 2014 2 commits
  19. 10 Jul, 2014 4 commits
  20. 08 Jul, 2014 2 commits
    • Kim Nguyễn's avatar
      Preliminary work-around to only substitute by any/empty variables that were... · 4772f683
      Kim Nguyễn authored
      Preliminary work-around to only substitute by any/empty variables that were introduced by the tallying.
    • Kim Nguyễn's avatar
      Improve the type pretty printer, as follows : · 40740c72
      Kim Nguyễn authored
      for each component (int, atoms, pairs...) we optimize the case where the component is like
        T1&'a | T2 | T3&'a
      we split it into
      - T2
      - T1 &'a | T3 &'a
      we retrieve { 'a } as the set of top level vars in the second type
      we compute T2 &'a | T1 &'a | T3 &'a
      then remove 'a from that type and return finally :
      T2 | ('a & (T1 | T2 | T3))
      We special case if (T1 | T2 | T3) is top, then we just display
      T2 | 'a