Dafny: module datatypes generics weirdness

Nov 19, 2012 at 2:51 PM
Edited Nov 19, 2012 at 2:53 PM

Not entirely sure how to explain what's going on here, but the problem code is here.

I mention "generics" in my title as removing the type argument fixes the problem.

Also, putting everything in the same module fixes the problem.

Just in case you're wondering why this came up, my real world code is about representing lists as pairs of lists to form a simple Deque (I forget the name for this, Binary Deque?).

Nov 19, 2012 at 3:35 PM

Thanks for the bug report.  Curiously, here are two workarounds.

One is to name the destructor of the Wrap2 constructor's first parameter:

datatype wrap2 = Wrap2(get: A.wrap);

and change the body of the function unwrap to just w.get.

The other is to import A as "opened":

import opened A;


Nov 19, 2012 at 3:56 PM

Cheers, actually didn't know destructors existed, this makes things easier.

Nov 19, 2012 at 4:20 PM

In that case, the Dafny Quick Reference (http://research.microsoft.com/en-us/projects/dafny/reference.aspx) may also explain other things you may or may not know about.  Cheers.

Nov 21, 2012 at 2:15 AM

Fixed. http://dafny.codeplex.com/SourceControl/changeset/289d05cf7c0c  (Note the new location of the sources:  DAFNY.codeplex.com)