Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Remove the Record theory #1095

Open
wants to merge 14 commits into
base: next
Choose a base branch
from
Open

Remove the Record theory #1095

wants to merge 14 commits into from

Commits on Nov 12, 2024

  1. Merge Records into ADT

    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    7b4049a View commit details
    Browse the repository at this point in the history

  2. Remove useless flag in adt type

    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    8cac7a8 View commit details
    Browse the repository at this point in the history

  3. Remove more dead code

    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    6ff0e41 View commit details
    Browse the repository at this point in the history

  4. Promote tests

    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    d8508cb View commit details
    Browse the repository at this point in the history

  5. Do not display 0 candidates messages 

    As we load by default prelude with plenty of axioms, we got a lot of
messages about these axioms in the debugging printers of `Matching`.
This commit changes this behavior. We only print messages if there is at
least one candidate.
    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    aabc2bc View commit details
    Browse the repository at this point in the history

  6. Add a variant of the issue 1008 test 

    Currently, the test `record.smt2` of the issue 1008 only succeeds with
the Tableaux SAT solver
    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    62021dc View commit details
    Browse the repository at this point in the history

  7. Better printer + remove dead code 

    The function `xs_modulo_records` is not useful anymore. Indeed, all the
ADT variables are sent to the ADT relation thanks to the `init` function
of `Uf`. As record type has only one constructor by definition, this
will always replace a record variable by a record definition in the
union find and we can match patterns of the form `{ lbl1 = ..; ...; lblk =
..}`.
    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    6529b17 View commit details
    Browse the repository at this point in the history

  8. Add new tests

    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    caaf87b View commit details
    Browse the repository at this point in the history

  9. Use context of X.make

    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    7f2006f View commit details
    Browse the repository at this point in the history

  10. Revert "Use context of X.make" 

    This reverts commit 31c4c66.
    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    a89abf7 View commit details
    Browse the repository at this point in the history

  11. Remove test.smt2

    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    f2cbfc2 View commit details
    Browse the repository at this point in the history

  12. clean up

    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    6d20e79 View commit details
    Browse the repository at this point in the history

  13. Reapply "Use context of X.make" 

    This reverts commit 874ea98.
    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    1bf9e0f View commit details
    Browse the repository at this point in the history

  14. restore printer

    @Halbaroth
    Halbaroth committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    20d966c View commit details
    Browse the repository at this point in the history