Introduce sequence construction expressions #297
Conversation
|
There is a massive whitespace diff in the parser due to removing end-of-line space. Could you please remove that stuff from this logically complex PR? |
|
The github diff viewer has a "Hide whitespace changes" option when you click on the cog wheel, isn't that good enough to review this PR? |
RustanLeino
force-pushed
the
seq-construction-expr
branch
from
9008048
to
2569d2e
Compare
| @@ -939,6 +943,16 @@ axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Index(Seq#Build(s,v), i) } | |||
| axiom (forall s: Seq Box, bx: Box, t: Ty :: { $Is(Seq#Build(s,bx),TSeq(t)) } | |||
| $Is(s,TSeq(t)) && $IsBox(bx,t) ==> $Is(Seq#Build(s,bx),TSeq(t))); | |||
|
|
|||
| function Seq#Create(ty: Ty, heap: Heap, len: int, init: HandleType): Seq Box; | |||
There was a problem hiding this comment.
HandleType appears only once in DafnyPrelude. Could you describe what is going on here?
Also, why are we boxing, and why doesn't Box take a type parameter? I didn't think we support heterogeneous sequences.
There was a problem hiding this comment.
Generally, the types at the Boogie level are much more coarse-grained than in Dafny. For example, the single Boogie type Ref includes references to objects of all Dafny types (and also includes the null value and references to unallocated objects).
HandleType is part of the translation of functions as first-class values in Dafny. This is necessary, because Boogie is first-order and does not allow functions as values. HandleType is more coarse-grained than the various arrow types in Dafny, and so it includes total, partial, and read-effectful functions as well as functions of all arities and parameter types. The Dafny translation into Boogie generates axioms about different arities on demand, so there will be more uses of HandleType in the Boogie program generated from a Dafny program that uses functions.
The Boogie type Box is used to collect all possible values in a Dafny program. Every type has an injection (and sometimes a bijection) into Box. This lets Dafny encode polymorphism in Boogie.
Like any compiler or translation into a more primitive language, the primitive language allows a lot of things that are not possible in the source language. For example, assembly code gives you arbitrary goto's. The translation is responsible for making appropriate use of the constructs and values in the target language.
| ResolveExpression(e.N, opts); | ||
| ConstrainToIntegerType(e.N, "sequence construction must use an integer-based expression for the sequence size (got {0})"); | ||
| ResolveExpression(e.Initializer, opts); // TODO: check type (KRML) | ||
| var arrowType = new ArrowType(e.tok, builtIns.ArrowTypeDecls[1], new List<Type>() { Type.Int }, elementType); |
There was a problem hiding this comment.
I'm still a C# beginner, but is there a nicer way to create arrow types? Maybe we could have static methods for Function1/2/3 or something. This is fine, but rather chatty.
There was a problem hiding this comment.
The C# code that generates Boogie code is very chatty. What you can easily write in a line or two of Boogie, if only you could write Boogie in text, can sometimes take a dozen of lines of C#. I've often wished this were simpler, because it leads to a lot of complexity in the code. There are helper routines for many things, but they are not organized in any disciplined way, so they are typically hard to find. (Maybe sometime we can do a Refactor Fest to improve these things.)
I had missed the TODO comment on line 11741. :O
There was a problem hiding this comment.
Maybe a pedantic question, but why are we sure ArrowTypeDecls[1] is non-null? I only see [0] being created in all cases.
Nevermind. I see it in Resolver now.
| var tr = new Bpl.Trigger(tok, true, new List<Bpl.Expr> { ai }); | ||
| q = new Bpl.ForallExpr(tok, bvs, tr, Bpl.Expr.Imp(ante, Bpl.Expr.Eq(ai_prime, apply))); // TODO: use a more general Equality translation | ||
| builder.Add(new Bpl.AssumeCmd(tok, q)); | ||
| CheckElementInit(tok, true, tRhs.ArrayDimensions, tRhs.EType, tRhs.ElementInit, nw, builder, etran, new WFOptions()); |
There was a problem hiding this comment.
Nice to move this bunch of code to a method. Is the code changed at all? It's hard to review code movement changes.
There was a problem hiding this comment.
I think the movement did not change the previous code, only parameterized it.
Is there some way you'd prefer that such refactorings be marked or pointed out in the pull requests / code reviews? I commonly rearrange code to make it better or more usable.
There was a problem hiding this comment.
Yeah, I don't know a good way. On other teams we've enforced a policy that code movement goes in separate PRs so we don't need to use brain cycles diffing the two versions in our heads. That adds some overhead. Alternatively, you can comment on your own PR saying something like "this code is just moved, no logical changes". The danger of course is that when moving code you also change it in a way that introduced a bug, and the diff makes the change very difficult to find.
RustanLeino
force-pushed
the
seq-construction-expr
branch
from
2569d2e
to
c96cda8
Compare
|
I think my first force-push rebased from the separate white-space commit. Or at least that's what I intended it to do. |
You can now write
seq(N, i => E(i))to create a sequence of lengthNwhere elementihas the valueE(i). The pull request includes parsing, type checking, verification, and compilation to C#, JavaScript, and Go.