• 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
    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.
    7932c071
types.ml 114 KB