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

Explicit stride #1227

Merged
merged 17 commits into from
Jul 20, 2021
Merged

Explicit stride #1227

merged 17 commits into from
Jul 20, 2021

Commits on Jun 29, 2021

  1. Add new syntactic forms for enumerations with explicit stride values. 

    This doesn't yet pipe the new constructs through the typechecker.
    @robdockins
    robdockins committed Jun 29, 2021
    Configuration menu
    Copy the full SHA
    7024500 View commit details
    Browse the repository at this point in the history

  2. Add new primtives for the explicit stride enumerations. 

    Hook them up through the typechecker.  However, we still
need implementations.
    @robdockins
    robdockins committed Jun 29, 2021
    Configuration menu
    Copy the full SHA
    6fe2970 View commit details
    Browse the repository at this point in the history

  3. Add implementations for the new enumeration primitives.

    @robdockins
    robdockins committed Jun 29, 2021
    Configuration menu
    Copy the full SHA
    14a6601 View commit details
    Browse the repository at this point in the history

Commits on Jun 30, 2021

  1. Relax the finiteness restriction on the first argument of /^ and %^. 

    We define `inf /^ n = inf` and `inf %^ n` for finite, positive `n`.
    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    94a4c77 View commit details
    Browse the repository at this point in the history

  2. Fix incorrect "unused name" warnings from primitive type declarations.

    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    33afacc View commit details
    Browse the repository at this point in the history

  3. Add regression test for enumerations with explicit strides

    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    d1f945b View commit details
    Browse the repository at this point in the history

  4. Update "ProgrammingCryptol" 

    Minor output changes in the exercises are required.
    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    0778fd8 View commit details
    Browse the repository at this point in the history

  5. Add a check-docs command to the cry script

    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    3debc2b View commit details
    Browse the repository at this point in the history

  6. Minor test suite updates

    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    5a8a00f View commit details
    Browse the repository at this point in the history

  7. rename some identifiers in the test for issue138 

    We need to avoid the new `down` keyword.
    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    5258771 View commit details
    Browse the repository at this point in the history

  8. Update the fin prover with changes to the division operators.

    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    acb3ca9 View commit details
    Browse the repository at this point in the history

  9. Update solver definitions related to /^ and %^.

    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    b3c4317 View commit details
    Browse the repository at this point in the history

  10. Fix windows test output

    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    3ea59c7 View commit details
    Browse the repository at this point in the history

  11. Documentation tweaks and spellcheck in the prelude

    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    362649b View commit details
    Browse the repository at this point in the history

  12. Update tests again

    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    a3534f9 View commit details
    Browse the repository at this point in the history

  13. update docs again

    @robdockins
    robdockins committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    4d5d66f View commit details
    Browse the repository at this point in the history

Commits on Jul 14, 2021

  1. Merge remote-tracking branch 'origin/master' into explicit-stride

    @robdockins
    robdockins committed Jul 14, 2021
    Configuration menu
    Copy the full SHA
    af4d0d9 View commit details
    Browse the repository at this point in the history