• Kim Nguyễn's avatar
    Fix typing of application and optimize the code: · 3f63d285
    Kim Nguyễn authored
    - fix a bug in Positive.decompose that was introducing components that were not
    in the original type
    - rewrite Positive.decompose to flatten long chains of `Cup [`Cup[`Cup ...]]
    - rewrite apply_raw to perform the correct dove-tail exploration of the branches
    - rewrite Positive.clean_type to perform substitution of {co,contra}-variant only
    variables and internal variable beautification at the same time
    - For the moment, only call Positive.clean_type at the very end, before returning the result type. Need to investigate if intermediate results would benefit from having less variables.
types.mli 10.3 KB