Integer Sequences #15
Conversation
There was a problem hiding this comment.
Oh look, Robin is nit-picking about naming once again. :)
This is really cool stuff, thanks for contributing it! I didn't look too hard at the lemmas just yet as I want to see how my suggestion of using FoldLeft and FoldRight plays out first.
Out of curiosity, do you also have an implementation of Base64 built on this waiting in the wings too?
src/Collections/Sequences/NatSeq.dfy
Outdated
| } | ||
|
|
||
| /* Converts a sequence to a nat beginning from the most significant word. */ | ||
| function method {:opaque} ToNatRev(xs: seq<uint>): nat |
There was a problem hiding this comment.
I wouldn't use the "Rev" suffix as I incorrectly assumed it meant this function would behave like ToNat(Seq.Reverse(xs)). Perhaps these two functions could be ToNatLeft and ToNatRight?
In fact, now I'm curious whether these could use Seq.FoldLeft and Seq.FoldRight instead. If they can't, that feels like an indication we need more lemmas on those Fold functions for them to be actually useful. :)
src/Collections/Sequences/NatSeq.dfy
Outdated
| function method BOUND(): nat | ||
| ensures BOUND() > 1 |
There was a problem hiding this comment.
An alternative is to declare this nullary function as a const. To get the > 1 property, you can then either give a body-less lemma
lemma BoundAtLeastTwo()
ensures 2 <= BOUNDor declare (here or, better, elsewhere) a type
type Plural = x | 2 <= xand declare BOUND to be of this type.
There was a problem hiding this comment.
This does seem cleaner, but we'd like to initialize BOUND in the refining modules
There was a problem hiding this comment.
I'm getting an error from this small example:
module Test {
type LessThan10 = x | 0 <= x < 10
const C: LessThan10
}
module Test' refines Test {
const C: LessThan10 := 5
}
Process terminated. Assertion failed.
at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in /private/tmp/dafny-20210205-34509-rqus4y/dafny-3.0.0/Source/Dafny/Resolver.cs:line 2644
at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in /private/tmp/dafny-20210205-34509-rqus4y/dafny-3.0.0/Source/Dafny/Resolver.cs:line 1002
...
Am I missing something?
There was a problem hiding this comment.
@RustanLeino Did you have thoughts on this issue? I think this may be the last item holding up this PR. If function vs. const is a minor concern, perhaps we can merge this PR and then address the bug above and consider converting to a const in a future PR.
There was a problem hiding this comment.
I think that is the right path forward. It's unfortunate since fixing this later will be a breaking change for any refining users, but worth doing while we're still reserving the right to make such changes in these libraries.
I cut dafny-lang/dafny#1481 for the underlying issue and #21 to track the improvement once that is addressed.
|
@robin-aws Just to check in, where are we on merging this in? |
|
Apologies @parno, I misremembered Rustan's comment as the blocker and forgot I had requested changes. |
|
No problem -- thanks for merging it in! |
|
Thank you @robin-aws and @RustanLeino for reviewing! I appreciate all the feedback on our PRs. |
Hi everyone! Thanks for all of your valuable feedback on the
CollectionsandNonlinearArithmeticsections of the library. We have since addedNatSeq. Any comments are appreciated :)Here is the original standard library discussion.