Skip to content

Rewrite maps, tuples, lists as BDDs. Performance improvements. #14693

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 9 commits into
base: main
Choose a base branch
from

Conversation

gldubc
Copy link
Member

@gldubc gldubc commented Aug 4, 2025

Changing the representation of maps, tuples to instead use trees (binary decision diagrams).

As we use more and more the difference operator in the type system (e.g. to compute fun_from_inferred_clauses(args_clauses) for inferred function types from patterns), the "DNF" representation started running into pathological cases and hog out time during emptiness checks, and printing.

The BDD is now used for set operations and subtyping, and translated (using previous logic and simplications) to DNF for printing and type operations like map fetch.

The BDD representation is common to maps, tuples, lists and functions. Some functions are generic (called bdd_difference, bdd_intersection, ...).

We also changes some algorithms:

  • tuple_eliminate_negation was not generating disjoint tuples. It now does, which greatly improves performance and printing quality.
    -tuple_empty? now uses the same logic, this improves performances.
  • pivot_overlapping_clauses algorithm was not generating disjoint tuples. It now does.
  • The computation of subtyping for functions and function application is too slow for large arrow intersections (>30). This adds a special case apply_disjoint, when the functions are disjoint and non-empty (as produced by fun_from_inferred_clauses, for instance), which is much faster.

gldubc added 9 commits July 24, 2025 16:56
- Updated the representation of non-empty lists and empty intersections/differences to use BDD structures.
- Introduced new functions for BDD operations including list_get, list_get_pos, and list_all? for better handling of BDD paths.
- Modified list normalization and difference functions to work with BDDs
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

1 participant