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

Sum types #1602

Merged
merged 61 commits into from
Feb 2, 2024
Merged

Sum types #1602

merged 61 commits into from
Feb 2, 2024

Commits on Jan 12, 2024

  1. Checkpoint: sum types

    @yav
    yav committed Jan 12, 2024
    Configuration menu
    Copy the full SHA
    c978b91 View commit details
    Browse the repository at this point in the history

Commits on Jan 15, 2024

  1. Make constructors work

    @yav
    yav committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    5e0594f View commit details
    Browse the repository at this point in the history

Commits on Jan 16, 2024

  1. Fix docstrings on constructors, and show proper help for constructors

    @yav
    yav committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    1db3dbc View commit details
    Browse the repository at this point in the history

  2. Make simple patterns, we disallow nested constructir patterns.

    @yav
    yav committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    04d0e79 View commit details
    Browse the repository at this point in the history

  3. Fix renaming of CaseAlt

    @yav
    yav committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    ad34745 View commit details
    Browse the repository at this point in the history

  4. Get started on type checking case

    @yav
    yav committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    81c5d12 View commit details
    Browse the repository at this point in the history

  5. Make it build

    @yav
    yav committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    6a2b1c3 View commit details
    Browse the repository at this point in the history

  6. Keep constructors in a separate namespace. 

    This is similar to what happens in Haskell, and is useful when we validate
patterns---we need to make sure that only constructors can appear in
patterns, and not some random top-level name.

NSConstructor is a sub-namespace of NSValue, so whenever we look for name
uses of NSValue, we also check in NSConstructor
    @yav
    yav committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    e19a4de View commit details
    Browse the repository at this point in the history

Commits on Jan 17, 2024

  1. Typechecking for case expressions

    @yav
    yav committed Jan 17, 2024
    Configuration menu
    Copy the full SHA
    659030a View commit details
    Browse the repository at this point in the history

  2. Concrete evaluation for case

    @yav
    yav committed Jan 17, 2024
    Configuration menu
    Copy the full SHA
    a5404e6 View commit details
    Browse the repository at this point in the history

Commits on Jan 18, 2024

  1. Fix exports to account for constructors

    @yav
    yav committed Jan 18, 2024
    Configuration menu
    Copy the full SHA
    221bf4a View commit details
    Browse the repository at this point in the history

Commits on Jan 22, 2024

  1. Add missing signature

    @yav
    yav committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    5004a3d View commit details
    Browse the repository at this point in the history

  2. Comments

    @yav
    yav committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    385c328 View commit details
    Browse the repository at this point in the history

  3. Add missing cases for types that exist after NoPat

    @yav
    yav committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    a0179c0 View commit details
    Browse the repository at this point in the history

  4. Show help about constructors

    @yav
    yav committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    c7f12ad View commit details
    Browse the repository at this point in the history

  5. Improve error message for bad self recursive things

    @yav
    yav committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    c5b896c View commit details
    Browse the repository at this point in the history

  6. Add some tests

    @yav
    yav committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    cb6228e View commit details
    Browse the repository at this point in the history

  7. Handle missing cases for nested patterns, with test

    @yav
    yav committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    40a37c8 View commit details
    Browse the repository at this point in the history

  8. Document enum declarations

    @yav
    yav committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    e975355 View commit details
    Browse the repository at this point in the history

Commits on Jan 23, 2024

  1. Fix test

    @yav
    yav committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    5236aff View commit details
    Browse the repository at this point in the history

  2. Fill in some of the random code for enum. 

    We still need to figure out a reasonable way to sample an enum.
    @yav
    yav committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    4c1b857 View commit details
    Browse the repository at this point in the history

  3. Update issue1040 golden output

    @RyanGlScott
    RyanGlScott committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    e6291ce View commit details
    Browse the repository at this point in the history

  4. Implement random generation of enum values

    @RyanGlScott
    RyanGlScott committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    9438d83 View commit details
    Browse the repository at this point in the history

  5. Test case for :check'ing enum values

    @RyanGlScott
    RyanGlScott committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    f0706f9 View commit details
    Browse the repository at this point in the history

  6. Throw exception when symbolically evaluating enum values

    @RyanGlScott
    RyanGlScott committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    0a3a2e1 View commit details
    Browse the repository at this point in the history

  7. Implement toExpr for enums

    @RyanGlScott
    RyanGlScott committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    c00c9e5 View commit details
    Browse the repository at this point in the history

  8. Fix precedence when pretty-printing counterexamples

    @RyanGlScott
    RyanGlScott committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    77a8406 View commit details
    Browse the repository at this point in the history

  9. s/ppValue/ppValuePrec/

    @RyanGlScott
    RyanGlScott committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    a9c7751 View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2024

  1. Remove private annotations on constructors. 

    Keep things simple for now, we could introduce this on demand.
    @yav
    yav committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    8abf33f View commit details
    Browse the repository at this point in the history

Commits on Jan 25, 2024

  1. Implement symbolic evaluation for enum types.

    @yav
    yav committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    dd6313c View commit details
    Browse the repository at this point in the history

  2. Generalize CheckEnum test case to include :prove commands

    @RyanGlScott
    RyanGlScott committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    8252656 View commit details
    Browse the repository at this point in the history

  3. Use Vector and IntMap instead of Map, and a common ConInfo type

    @yav
    yav committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    3e072f7 View commit details
    Browse the repository at this point in the history

Commits on Jan 26, 2024

  1. Document no-overlapping-patterns restriction

    @RyanGlScott
    RyanGlScott committed Jan 26, 2024
    Configuration menu
    Copy the full SHA
    eb4a4ce View commit details
    Browse the repository at this point in the history

  2. Error when default case overlaps with subsequent cases

    @RyanGlScott
    RyanGlScott committed Jan 26, 2024
    Configuration menu
    Copy the full SHA
    ca85fac View commit details
    Browse the repository at this point in the history

  3. RefMan: Say "enums", not "enumerations", to avoid ambiguous terminology

    @RyanGlScott
    RyanGlScott committed Jan 26, 2024
    Configuration menu
    Copy the full SHA
    17b1e25 View commit details
    Browse the repository at this point in the history

  4. Rename "newtype" to "nominal type" after type checker 

    Fixes #1607
    @yav
    yav committed Jan 26, 2024
    Configuration menu
    Copy the full SHA
    1e07d0d View commit details
    Browse the repository at this point in the history

  5. Move constructors to the value namespace before checking for ambiguit… 

    …ies.

Fixes #1606
    @yav
    yav committed Jan 26, 2024
    Configuration menu
    Copy the full SHA
    99b9a3c View commit details
    Browse the repository at this point in the history

Commits on Jan 28, 2024

  1. Emit an error for non-exhaustive case expressions 

    Fixes #1608.
    @RyanGlScott
    RyanGlScott committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    d965cb4 View commit details
    Browse the repository at this point in the history

  2. Add regression test for #1606

    @RyanGlScott
    RyanGlScott committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    0c88cc3 View commit details
    Browse the repository at this point in the history

Commits on Jan 31, 2024

  1. Improvements to ":help" for nominal types/constructors 

    Fixes #1605
    @yav
    yav committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    e47ebcb View commit details
    Browse the repository at this point in the history

  2. Tweak error messages

    @yav
    yav committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    684a85e View commit details
    Browse the repository at this point in the history

  3. Make the cryptol-remote-api build again. 

    It looks like the code previously just a had a placeholder for
`newtypes`.  Now it sends a bit more info for nominal types, but
I am not sure that the rest of the code would handle these correctly.
    @yav
    yav committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    c68ecfc View commit details
    Browse the repository at this point in the history

  4. Rename some more things newtype -> nominal

    @yav
    yav committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    c06fc89 View commit details
    Browse the repository at this point in the history

  5. Add nominal type constructors in scope. 

    Fixes #1617
    @yav
    yav committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    e5251ee View commit details
    Browse the repository at this point in the history

  6. Implement sanity checking for case 

    Fixes #1615
    @yav
    yav committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    3e7d786 View commit details
    Browse the repository at this point in the history

Commits on Feb 1, 2024

  1. Make abstract type a special kind of nomainal type. 

    Fixes #1604
    @yav
    yav committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    a980328 View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review

    @RyanGlScott
    RyanGlScott authored Feb 1, 2024
    Configuration menu
    Copy the full SHA
    c8e4615 View commit details
    Browse the repository at this point in the history

  3. Clarify "Known Enum Type" restriction in RefMan

    @RyanGlScott
    RyanGlScott committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    2f5bbd9 View commit details
    Browse the repository at this point in the history

  4. Clarify two comments

    @RyanGlScott
    RyanGlScott committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    8aaad22 View commit details
    Browse the repository at this point in the history

  5. Add freeVars case for Abstract

    @RyanGlScott
    RyanGlScott committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    69327ba View commit details
    Browse the repository at this point in the history

  6. Fix a -Wunused-matches warning

    @RyanGlScott
    RyanGlScott committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    642d192 View commit details
    Browse the repository at this point in the history

  7. Add Option and Result types to the Cryptol prelude 

    These are useful enough that it is worth defining them in the standard library.
    @RyanGlScott
    RyanGlScott committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    8732b32 View commit details
    Browse the repository at this point in the history

  8. RefMan: Fix formatting error

    @RyanGlScott
    RyanGlScott committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    75958c1 View commit details
    Browse the repository at this point in the history

  9. RefMan: Regenerate HTML

    @RyanGlScott
    RyanGlScott committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    76f9c3e View commit details
    Browse the repository at this point in the history

  10. Mention enums in CHANGES.md

    @RyanGlScott
    RyanGlScott committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    4e6e5d8 View commit details
    Browse the repository at this point in the history

  11. Repair ProgrammingCryptol test

    @RyanGlScott
    RyanGlScott committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    56cf1a3 View commit details
    Browse the repository at this point in the history

  12. Repair ProgrammingCryptol test

    @RyanGlScott
    RyanGlScott committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    01d8c1d View commit details
    Browse the repository at this point in the history

Commits on Feb 2, 2024

  1. Update expected stdout for test cases

    @RyanGlScott
    RyanGlScott committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    f825abd View commit details
    Browse the repository at this point in the history

  2. Update .stdout.mingw32 and .stdout.darwin files

    @RyanGlScott
    RyanGlScott committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    a9e35fe View commit details
    Browse the repository at this point in the history

  3. Fix handling of abstract types 

    We must treat built-in abstract types slightly differently from user-defined
abstract types.

Also fix a bug in the way that the return kind of primitive types are computed:
we previously said that they all return `*`, but this is not necessarily the
case.
    @RyanGlScott
    RyanGlScott committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    ca0eb7e View commit details
    Browse the repository at this point in the history

  4. Fix typo (parameterss) in error message

    @RyanGlScott
    RyanGlScott committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    9be52cc View commit details
    Browse the repository at this point in the history