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

Fix issue 1099 #1102

Merged
merged 6 commits into from
Jun 11, 2024
Merged

Fix issue 1099 #1102

merged 6 commits into from
Jun 11, 2024

Commits on Jun 11, 2024

  1. Fix issue 1099 

    The `D_cnf` module didn't use the flag `toplevel` as it was done in `Cnf`.
This flag is important because the `Expr` AST doesn't store quantified
type variables with binders as it does for the term variable. Instead, we
use a `prenex polymorphism` approach, which means the quantified type
variables are at the top level only.

I believe this PR fixes the issue OCamlPro#1099.
    @Halbaroth
    Halbaroth committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    af77783 View commit details
    Browse the repository at this point in the history

  2. Attempt to fix regressions

    @Halbaroth
    Halbaroth committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    90d0ff8 View commit details
    Browse the repository at this point in the history

  3. Enforce prenex polymorphism 

    Alt-Ergo only supports prenex polymorphism. This commit
adds a failwith clause in `D_cnf` to enforce this property.
    @Halbaroth
    Halbaroth committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    de37c06 View commit details
    Browse the repository at this point in the history

  4. Clarify the meaning of top level in quantified type

    @Halbaroth
    Halbaroth committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    2d823b5 View commit details
    Browse the repository at this point in the history

  5. Clarify the documentation

    @Halbaroth
    Halbaroth committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    45174bf View commit details
    Browse the repository at this point in the history

  6. Poetry

    @Halbaroth
    Halbaroth committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    ca3d3d1 View commit details
    Browse the repository at this point in the history