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

WIP: Enumerator<T> trait #37

Draft
wants to merge 72 commits into
base: master
Choose a base branch
from
Draft

WIP: Enumerator<T> trait #37

wants to merge 72 commits into from

Commits on Feb 2, 2022

  1. Partial work, almost verifying

    @robin-aws
    robin-aws committed Feb 2, 2022
    Configuration menu
    Copy the full SHA
    6a32b86 View commit details
    Browse the repository at this point in the history

Commits on Feb 5, 2022

  1. Got an iterator -> enumerator adaptor to verify

    @robin-aws
    robin-aws committed Feb 5, 2022
    Configuration menu
    Copy the full SHA
    0be0251 View commit details
    Browse the repository at this point in the history

Commits on Feb 8, 2022

  1. Add Enumerator.Done()

    @robin-aws
    robin-aws committed Feb 8, 2022
    Configuration menu
    Copy the full SHA
    6c2088a View commit details
    Browse the repository at this point in the history

Commits on Feb 9, 2022

  1. More partial work

    @robin-aws
    robin-aws committed Feb 9, 2022
    Configuration menu
    Copy the full SHA
    2545eae View commit details
    Browse the repository at this point in the history

Commits on Feb 12, 2022

  1. Stepper approach seems to work better!

    @robin-aws
    robin-aws committed Feb 12, 2022
    Configuration menu
    Copy the full SHA
    6baa11f View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2022

  1. More partially-implemented enumerators

    @robin-aws
    robin-aws committed Feb 13, 2022
    Configuration menu
    Copy the full SHA
    73cc542 View commit details
    Browse the repository at this point in the history

  2. Restricted Step post-condition and got Filter to verify!

    @robin-aws
    robin-aws committed Feb 13, 2022
    Configuration menu
    Copy the full SHA
    768df4e View commit details
    Browse the repository at this point in the history

Commits on Feb 14, 2022

  1. Defined Rust-style Iterator

    @robin-aws
    robin-aws committed Feb 14, 2022
    Configuration menu
    Copy the full SHA
    c7aaacc View commit details
    Browse the repository at this point in the history

Commits on Feb 15, 2022

  1. Improve while loop idiom, start cleaning up

    @robin-aws
    robin-aws committed Feb 15, 2022
    Configuration menu
    Copy the full SHA
    dc59bea View commit details
    Browse the repository at this point in the history

  2. CLEANUP

    @robin-aws
    robin-aws committed Feb 15, 2022
    Configuration menu
    Copy the full SHA
    4b8307e View commit details
    Browse the repository at this point in the history

  3. Add some todos

    @robin-aws
    robin-aws committed Feb 15, 2022
    Configuration menu
    Copy the full SHA
    eee7d1d View commit details
    Browse the repository at this point in the history

Commits on Feb 16, 2022

  1. (Mostly) converted Step() to Next()

    @robin-aws
    robin-aws committed Feb 16, 2022
    Configuration menu
    Copy the full SHA
    37015dd View commit details
    Browse the repository at this point in the history

  2. Progress on fixing Filter

    @robin-aws
    robin-aws committed Feb 16, 2022
    Configuration menu
    Copy the full SHA
    924d685 View commit details
    Browse the repository at this point in the history

  3. Replace Done() with HasNext()

    @robin-aws
    robin-aws committed Feb 16, 2022
    Configuration menu
    Copy the full SHA
    323abfd View commit details
    Browse the repository at this point in the history

Commits on Feb 18, 2022

  1. Partial progress on proving enumerator semantics

    @robin-aws
    robin-aws committed Feb 18, 2022
    Configuration menu
    Copy the full SHA
    aae5518 View commit details
    Browse the repository at this point in the history

Commits on Feb 19, 2022

  1. Progress on fixing FilterEnumerator

    @robin-aws
    robin-aws committed Feb 19, 2022
    Configuration menu
    Copy the full SHA
    2ebc186 View commit details
    Browse the repository at this point in the history

  2. Proved semantics of FilteredEnumerator

    @robin-aws
    robin-aws committed Feb 19, 2022
    Configuration menu
    Copy the full SHA
    5e63373 View commit details
    Browse the repository at this point in the history

  3. Fixed termination guarantee on FilteredEnumerator

    @robin-aws
    robin-aws committed Feb 19, 2022
    Configuration menu
    Copy the full SHA
    a0e370f View commit details
    Browse the repository at this point in the history

  4. Progress on iterator example

    @robin-aws
    robin-aws committed Feb 19, 2022
    Configuration menu
    Copy the full SHA
    bcfbdb1 View commit details
    Browse the repository at this point in the history

Commits on Feb 21, 2022

  1. Fixed iterator adaptor example

    @robin-aws
    robin-aws committed Feb 21, 2022
    Configuration menu
    Copy the full SHA
    9d52831 View commit details
    Browse the repository at this point in the history

Commits on Feb 22, 2022

  1. Relocating example code

    @robin-aws
    robin-aws committed Feb 22, 2022
    Configuration menu
    Copy the full SHA
    5b3b315 View commit details
    Browse the repository at this point in the history

Commits on Feb 23, 2022

  1. Add Fold

    @robin-aws
    robin-aws committed Feb 23, 2022
    Configuration menu
    Copy the full SHA
    23395ac View commit details
    Browse the repository at this point in the history

  2. Tons of documentation

    @robin-aws
    robin-aws committed Feb 23, 2022
    Configuration menu
    Copy the full SHA
    16142fb View commit details
    Browse the repository at this point in the history

  3. Bit more cleanup

    @robin-aws
    robin-aws committed Feb 23, 2022
    Configuration menu
    Copy the full SHA
    2b4b2f6 View commit details
    Browse the repository at this point in the history

  4. Add lit commands

    @robin-aws
    robin-aws committed Feb 23, 2022
    Configuration menu
    Copy the full SHA
    a090841 View commit details
    Browse the repository at this point in the history

  5. Remove execution-created files

    @robin-aws
    robin-aws committed Feb 23, 2022
    Configuration menu
    Copy the full SHA
    07132ad View commit details
    Browse the repository at this point in the history

Commits on Feb 24, 2022

  1. Pr feedback, fix build

    @robin-aws
    robin-aws committed Feb 24, 2022
    Configuration menu
    Copy the full SHA
    ee50ca5 View commit details
    Browse the repository at this point in the history

  2. Fix another lit test failure

    @robin-aws
    robin-aws committed Feb 24, 2022
    Configuration menu
    Copy the full SHA
    ef77a1c View commit details
    Browse the repository at this point in the history

  3. Trim redundant post-conditions

    @robin-aws
    robin-aws committed Feb 24, 2022
    Configuration menu
    Copy the full SHA
    f172ef5 View commit details
    Browse the repository at this point in the history

  4. ACTUALLY fix lit test failure

    @robin-aws
    robin-aws committed Feb 24, 2022
    Configuration menu
    Copy the full SHA
    08876c0 View commit details
    Browse the repository at this point in the history

  5. Add trait specializations 

    Addresses my concern about needing to know the concrete types of Enumerators to prove behaviors
    @robin-aws
    robin-aws committed Feb 24, 2022
    Configuration menu
    Copy the full SHA
    89984b4 View commit details
    Browse the repository at this point in the history

  6. Sigh

    @robin-aws
    robin-aws committed Feb 24, 2022
    Configuration menu
    Copy the full SHA
    64f257f View commit details
    Browse the repository at this point in the history

Commits on Feb 25, 2022

  1. Switching to Option<T> flavour 

    A few verification failures left but looks like it will work out!
    @robin-aws
    robin-aws committed Feb 25, 2022
    Configuration menu
    Copy the full SHA
    a5c7863 View commit details
    Browse the repository at this point in the history

Commits on Feb 26, 2022

  1. More verification progress and useful examples

    @robin-aws
    robin-aws committed Feb 26, 2022
    Configuration menu
    Copy the full SHA
    e449f61 View commit details
    Browse the repository at this point in the history

Commits on Mar 1, 2022

  1. Fixed iterator adaptor, progress on other parts

    @robin-aws
    robin-aws committed Mar 1, 2022
    Configuration menu
    Copy the full SHA
    6a0c220 View commit details
    Browse the repository at this point in the history

  2. Added WithEnumeratedEnumerator

    @robin-aws
    robin-aws committed Mar 1, 2022
    Configuration menu
    Copy the full SHA
    a811a1f View commit details
    Browse the repository at this point in the history

  3. Extra comment

    @robin-aws
    robin-aws committed Mar 1, 2022
    Configuration menu
    Copy the full SHA
    a208cd4 View commit details
    Browse the repository at this point in the history

Commits on Mar 2, 2022

  1. Quick note

    @robin-aws
    robin-aws committed Mar 2, 2022
    Configuration menu
    Copy the full SHA
    e68755c View commit details
    Browse the repository at this point in the history

Commits on May 3, 2023

  1. Merge branch 'master' of github.com:dafny-lang/libraries into enumera… 

    …tion-experiments
    @robin-aws
    robin-aws committed May 3, 2023
    Configuration menu
    Copy the full SHA
    4aca2f3 View commit details
    Browse the repository at this point in the history

  2. Update for Dafny 4, couple of notes

    @robin-aws
    robin-aws committed May 3, 2023
    Configuration menu
    Copy the full SHA
    256aabe View commit details
    Browse the repository at this point in the history

Commits on May 8, 2023

  1. Trying out a pure-functional version

    @robin-aws
    robin-aws committed May 8, 2023
    Configuration menu
    Copy the full SHA
    2f2aa05 View commit details
    Browse the repository at this point in the history

Commits on May 10, 2023

  1. Promising success with constant Next invariant

    @robin-aws
    robin-aws committed May 10, 2023
    Configuration menu
    Copy the full SHA
    5986181 View commit details
    Browse the repository at this point in the history

Commits on May 11, 2023

  1. Partial attempt to use function instead of constant function value

    @robin-aws
    robin-aws committed May 11, 2023
    Configuration menu
    Copy the full SHA
    47dcc9d View commit details
    Browse the repository at this point in the history

Commits on May 14, 2023

  1. Generalizing to Actions

    @robin-aws
    robin-aws committed May 14, 2023
    Configuration menu
    Copy the full SHA
    49de185 View commit details
    Browse the repository at this point in the history

Commits on May 15, 2023

  1. Temporary Repr restriction

    @robin-aws
    robin-aws committed May 15, 2023
    Configuration menu
    Copy the full SHA
    a32f73b View commit details
    Browse the repository at this point in the history

Commits on May 16, 2023

  1. Sweet solution for enumerator termination measure

    @robin-aws
    robin-aws committed May 16, 2023
    Configuration menu
    Copy the full SHA
    377de50 View commit details
    Browse the repository at this point in the history

Commits on May 17, 2023

  1. SeqEnumerator

    @robin-aws
    robin-aws committed May 17, 2023
    Configuration menu
    Copy the full SHA
    e38755c View commit details
    Browse the repository at this point in the history

Commits on May 22, 2023

  1. Use height instead of Repr for termination, split up more files

    @robin-aws
    robin-aws committed May 22, 2023
    Configuration menu
    Copy the full SHA
    5f6e167 View commit details
    Browse the repository at this point in the history

Commits on May 23, 2023

  1. Progress

    @robin-aws
    robin-aws committed May 23, 2023
    Configuration menu
    Copy the full SHA
    006a553 View commit details
    Browse the repository at this point in the history

  2. Remove unnecessary nested exists

    @robin-aws
    robin-aws committed May 23, 2023
    Configuration menu
    Copy the full SHA
    f339ada View commit details
    Browse the repository at this point in the history

  3. More progress

    @robin-aws
    robin-aws committed May 23, 2023
    Configuration menu
    Copy the full SHA
    8c88b21 View commit details
    Browse the repository at this point in the history

Commits on May 27, 2023

  1. EnumeratedDistributesOverConcat!

    @robin-aws
    robin-aws committed May 27, 2023
    Configuration menu
    Copy the full SHA
    4cae439 View commit details
    Browse the repository at this point in the history

Commits on May 29, 2023

  1. Partial work to fix definition of IsEnumerator()

    @robin-aws
    robin-aws committed May 29, 2023
    Configuration menu
    Copy the full SHA
    f321710 View commit details
    Browse the repository at this point in the history

  2. Enumerators.dfy verifying again

    @robin-aws
    robin-aws committed May 29, 2023
    Configuration menu
    Copy the full SHA
    bd81878 View commit details
    Browse the repository at this point in the history

  3. NoOp verifies!

    @robin-aws
    robin-aws committed May 29, 2023
    Configuration menu
    Copy the full SHA
    e066a2d View commit details
    Browse the repository at this point in the history

  4. Mapping enumerator verifies (avoiding Enumerated lemmas for now)

    @robin-aws
    robin-aws committed May 29, 2023
    Configuration menu
    Copy the full SHA
    cf6ac72 View commit details
    Browse the repository at this point in the history

Commits on May 30, 2023

  1. Progress on composed action

    @robin-aws
    robin-aws committed May 30, 2023
    Configuration menu
    Copy the full SHA
    300c012 View commit details
    Browse the repository at this point in the history

Commits on Jun 7, 2023

  1. Experimenting with no CanConsume

    @robin-aws
    robin-aws committed Jun 7, 2023
    Configuration menu
    Copy the full SHA
    bad3054 View commit details
    Browse the repository at this point in the history

Commits on Jan 12, 2024

  1. Revert "Experimenting with no CanConsume" 

    This reverts commit bad3054.
    @robin-aws
    robin-aws committed Jan 12, 2024
    Configuration menu
    Copy the full SHA
    bcb450d View commit details
    Browse the repository at this point in the history

  2. Complete EnumeratedDistributesOverConcat2

    @robin-aws
    robin-aws committed Jan 12, 2024
    Configuration menu
    Copy the full SHA
    8139631 View commit details
    Browse the repository at this point in the history

Commits on Jan 15, 2024

  1. More progress

    @robin-aws
    robin-aws committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    8607ee7 View commit details
    Browse the repository at this point in the history

  2. Got ComposedAction to verify!

    @robin-aws
    robin-aws committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    2efc280 View commit details
    Browse the repository at this point in the history

Commits on Feb 17, 2024

  1. Lots more Actions, partial refactoring for “history”

    @robin-aws
    robin-aws committed Feb 17, 2024
    Configuration menu
    Copy the full SHA
    259f899 View commit details
    Browse the repository at this point in the history

Commits on Feb 21, 2024

  1. Got GenericAction to work as a base type

    @robin-aws
    robin-aws committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    b036c66 View commit details
    Browse the repository at this point in the history

Commits on Feb 22, 2024

  1. Updated most cases to deal with history change

    @robin-aws
    robin-aws committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    627ec2a View commit details
    Browse the repository at this point in the history

  2. Improving combinator specs

    @robin-aws
    robin-aws committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    abe9233 View commit details
    Browse the repository at this point in the history

  3. Replace IsSmallerThan with DecreasesTo, motivating example

    @robin-aws
    robin-aws committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    18a2ef4 View commit details
    Browse the repository at this point in the history

  4. Tweaks

    @robin-aws
    robin-aws committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    fd231a1 View commit details
    Browse the repository at this point in the history

Commits on Mar 6, 2024

  1. added new type characteristic to get things to check

    Siva Somayyajula committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    be37f10 View commit details
    Browse the repository at this point in the history

Commits on Oct 25, 2024

  1. Snapshot

    @robin-aws
    robin-aws committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    f43d0cc View commit details
    Browse the repository at this point in the history

  2. More

    @robin-aws
    robin-aws committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    278a650 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'enumeration-experiments' of github.com:robin-aws/librar… 

    …ies into enumeration-experiments
    @robin-aws
    robin-aws committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    636f139 View commit details
    Browse the repository at this point in the history