Code

WIP: Enumerator<T> trait#37

Code

Draft

robin-aws wants to merge 72 commits intodafny-lang:masterdafny-lang/libraries:masterfrom robin-aws:enumeration-experimentsrobin-aws/libraries:enumeration-experimentsCopy head branch name to clipboard

+3,757-7

Commits

Commits on Feb 2, 2022

• Partial work, almost verifying

  robin-aws

  committed
  6a32b86

  Copy full SHA for 6a32b86

Commits on Feb 5, 2022

• Got an iterator -> enumerator adaptor to verify

  robin-aws

  committed
  0be0251

  Copy full SHA for 0be0251

Commits on Feb 8, 2022

• Add Enumerator.Done()

  robin-aws

  committed
  6c2088a

  Copy full SHA for 6c2088a

Commits on Feb 9, 2022

• More partial work

  robin-aws

  committed
  2545eae

  Copy full SHA for 2545eae

Commits on Feb 12, 2022

• Stepper approach seems to work better!

  robin-aws

  committed
  6baa11f

  Copy full SHA for 6baa11f

Commits on Feb 13, 2022

• More partially-implemented enumerators

  robin-aws

  committed
  73cc542

  Copy full SHA for 73cc542

• Restricted Step post-condition and got Filter to verify!

  robin-aws

  committed
  768df4e

  Copy full SHA for 768df4e

Commits on Feb 14, 2022

• Defined Rust-style Iterator

  robin-aws

  committed
  c7aaacc

  Copy full SHA for c7aaacc

Commits on Feb 15, 2022

• Improve while loop idiom, start cleaning up

  robin-aws

  committed
  dc59bea

  Copy full SHA for dc59bea

• CLEANUP

  robin-aws

  committed
  4b8307e

  Copy full SHA for 4b8307e

• Add some todos

  robin-aws

  committed
  eee7d1d

  Copy full SHA for eee7d1d

Commits on Feb 16, 2022

• (Mostly) converted Step() to Next()

  robin-aws

  committed
  37015dd

  Copy full SHA for 37015dd

• Progress on fixing Filter

  robin-aws

  committed
  924d685

  Copy full SHA for 924d685

• Replace Done() with HasNext()

  robin-aws

  committed
  323abfd

  Copy full SHA for 323abfd

Commits on Feb 18, 2022

• Partial progress on proving enumerator semantics

  robin-aws

  committed
  aae5518

  Copy full SHA for aae5518

Commits on Feb 19, 2022

• Progress on fixing FilterEnumerator

  robin-aws

  committed
  2ebc186

  Copy full SHA for 2ebc186

• Proved semantics of FilteredEnumerator

  robin-aws

  committed
  5e63373

  Copy full SHA for 5e63373

• Fixed termination guarantee on FilteredEnumerator

  robin-aws

  committed
  a0e370f

  Copy full SHA for a0e370f

• Progress on iterator example

  robin-aws

  committed
  bcfbdb1

  Copy full SHA for bcfbdb1

Commits on Feb 21, 2022

• Fixed iterator adaptor example

  robin-aws

  committed
  9d52831

  Copy full SHA for 9d52831

Commits on Feb 22, 2022

• Relocating example code

  robin-aws

  committed
  5b3b315

  Copy full SHA for 5b3b315

Commits on Feb 23, 2022

• Add Fold

  robin-aws

  committed
  23395ac

  Copy full SHA for 23395ac

• Tons of documentation

  robin-aws

  committed
  16142fb

  Copy full SHA for 16142fb

• Bit more cleanup

  robin-aws

  committed
  2b4b2f6

  Copy full SHA for 2b4b2f6

• Add lit commands

  robin-aws

  committed
  a090841

  Copy full SHA for a090841

• Remove execution-created files

  robin-aws

  committed
  07132ad

  Copy full SHA for 07132ad

Commits on Feb 24, 2022

• Pr feedback, fix build

  robin-aws

  committed
  ee50ca5

  Copy full SHA for ee50ca5

• Fix another lit test failure

  robin-aws

  committed
  ef77a1c

  Copy full SHA for ef77a1c

• Trim redundant post-conditions

  robin-aws

  committed
  f172ef5

  Copy full SHA for f172ef5

• ACTUALLY fix lit test failure

  robin-aws

  committed
  08876c0

  Copy full SHA for 08876c0

• Add trait specializations

  Show description for 89984b4
  robin-aws

  committed
  89984b4

  Copy full SHA for 89984b4

• Sigh

  robin-aws

  committed
  64f257f

  Copy full SHA for 64f257f

Commits on Feb 25, 2022

• Switching to Option<T> flavour

  Show description for a5c7863
  robin-aws

  committed
  a5c7863

  Copy full SHA for a5c7863

Commits on Feb 26, 2022

• More verification progress and useful examples

  robin-aws

  committed
  e449f61

  Copy full SHA for e449f61

Commits on Mar 1, 2022

• Fixed iterator adaptor, progress on other parts

  robin-aws

  committed
  6a0c220

  Copy full SHA for 6a0c220

• Added WithEnumeratedEnumerator

  robin-aws

  committed
  a811a1f

  Copy full SHA for a811a1f

• Extra comment

  robin-aws

  committed
  a208cd4

  Copy full SHA for a208cd4

Commits on Mar 2, 2022

• Quick note

  robin-aws

  committed
  e68755c

  Copy full SHA for e68755c

Commits on May 3, 2023

• Merge branch 'master' of github.com:dafny-lang/libraries into enumeration-experiments

  robin-aws

  committed
  4aca2f3

  Copy full SHA for 4aca2f3

• Update for Dafny 4, couple of notes

  robin-aws

  committed
  256aabe

  Copy full SHA for 256aabe

Commits on May 8, 2023

• Trying out a pure-functional version

  robin-aws

  committed
  2f2aa05

  Copy full SHA for 2f2aa05

Commits on May 10, 2023

• Promising success with constant Next invariant

  robin-aws

  committed
  5986181

  Copy full SHA for 5986181

Commits on May 11, 2023

• Partial attempt to use function instead of constant function value

  robin-aws

  committed
  47dcc9d

  Copy full SHA for 47dcc9d

Commits on May 14, 2023

• Generalizing to Actions

  robin-aws

  committed
  49de185

  Copy full SHA for 49de185

Commits on May 15, 2023

• Temporary Repr restriction

  robin-aws

  committed
  a32f73b

  Copy full SHA for a32f73b

Commits on May 16, 2023

• Sweet solution for enumerator termination measure

  robin-aws

  committed
  377de50

  Copy full SHA for 377de50

Commits on May 17, 2023

• SeqEnumerator

  robin-aws

  committed
  e38755c

  Copy full SHA for e38755c

Commits on May 22, 2023

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

  robin-aws

  committed
  5f6e167

  Copy full SHA for 5f6e167

Commits on May 23, 2023

• Progress

  robin-aws

  committed
  006a553

  Copy full SHA for 006a553

• Remove unnecessary nested exists

  robin-aws

  committed
  f339ada

  Copy full SHA for f339ada

• More progress

  robin-aws

  committed
  8c88b21

  Copy full SHA for 8c88b21

Commits on May 27, 2023

• EnumeratedDistributesOverConcat!

  robin-aws

  committed
  4cae439

  Copy full SHA for 4cae439

Commits on May 29, 2023

• Partial work to fix definition of IsEnumerator()

  robin-aws

  committed
  f321710

  Copy full SHA for f321710

• Enumerators.dfy verifying again

  robin-aws

  committed
  bd81878

  Copy full SHA for bd81878

• NoOp verifies!

  robin-aws

  committed
  e066a2d

  Copy full SHA for e066a2d

• Mapping enumerator verifies (avoiding Enumerated lemmas for now)

  robin-aws

  committed
  cf6ac72

  Copy full SHA for cf6ac72

Commits on May 30, 2023

• Progress on composed action

  robin-aws

  committed
  300c012

  Copy full SHA for 300c012

Commits on Jun 7, 2023

• Experimenting with no CanConsume

  robin-aws

  committed
  bad3054

  Copy full SHA for bad3054

Commits on Jan 12, 2024

• Revert "Experimenting with no CanConsume"

  Show description for bcb450d
  robin-aws

  committed
  bcb450d

  Copy full SHA for bcb450d

• Complete EnumeratedDistributesOverConcat2

  robin-aws

  committed
  8139631

  Copy full SHA for 8139631

Commits on Jan 15, 2024

• More progress

  robin-aws

  committed
  8607ee7

  Copy full SHA for 8607ee7

• Got ComposedAction to verify!

  robin-aws

  committed
  2efc280

  Copy full SHA for 2efc280

Commits on Feb 17, 2024

• Lots more Actions, partial refactoring for “history”

  robin-aws

  committed
  259f899

  Copy full SHA for 259f899

Commits on Feb 21, 2024

• Got GenericAction to work as a base type

  robin-aws

  committed
  b036c66

  Copy full SHA for b036c66

Commits on Feb 22, 2024

• Updated most cases to deal with history change

  robin-aws

  committed
  627ec2a

  Copy full SHA for 627ec2a

• Improving combinator specs

  robin-aws

  committed
  abe9233

  Copy full SHA for abe9233

• Replace IsSmallerThan with DecreasesTo, motivating example

  robin-aws

  committed
  18a2ef4

  Copy full SHA for 18a2ef4

• Tweaks

  robin-aws

  committed
  fd231a1

  Copy full SHA for fd231a1

Commits on Mar 6, 2024

• added new type characteristic to get things to check

  ssomayyajula

  committed
  be37f10

  Copy full SHA for be37f10

Commits on Oct 25, 2024

• Snapshot

  robin-aws

  committed
  f43d0cc

  Copy full SHA for f43d0cc

• More

  robin-aws

  committed
  278a650

  Copy full SHA for 278a650

• Merge branch 'enumeration-experiments' of github.com:robin-aws/libraries into enumeration-experiments

  robin-aws

  committed
  636f139

  Copy full SHA for 636f139