Fix bug in dumpableType function. Fixes #946.

[brianhuffman]

The function now works as documented, and succeeds on function
types that do not have Bit as a return type.

[brianhuffman]

We should also add a regression test before merging this PR.

[robdockins]

Looks right, pending a regression test.

[benjaminselfridge]

Added a regression test. A couple potential issues that I could resolve with a subsequent commit, if deemed necessary:

• Add more example functions as input to :dumptests. For this commit, I did the minimal example I could come up with that would have been broken before this bug fix. I can also add more examples in an attempt to exhaust all the cases one could think of that might break, but I figured I'd be conservative until I knew whether it was worth doing.

• The new test (tests/regression/dumptests) creates a turd file, add32.out, which I have added to the top level .gitignore. I'm not sure if this is the right approach; perhaps the cry script could instead recursively remove all .out files.

[brianhuffman]

Thanks @benjaminselfridge for adding the regression test! I was also unsure about how to handle a regression test that generates a file. I just added @yav as a reviewer; we can see what he thinks about it.

[yav]

I don't have a strong opinion but it would be nice to not have left over files. After all, if generating the file fails, we don't want the test to succeed because there is an old left-over file.

Cryptol supports shell commands (e.g., :!ls), so I guess we could generate the file, then cat it and then remove it all from the test script. This ought to work on Linux and Mac but I guess it would fail on Windows. Perhaps it it is good enough for now?

Alternatively, we could modify the test-runner to not just check for stdout but also other generated files, but we'd have to figure out a design.

[robdockins]

Maybe we could make it produce output on stdout instead if you pass - as a file name, or something like that? Or maybe the generated file isn't predictable enough for that?

[brianhuffman]

Well, in this case the regression test doesn't need to verify the contents of the file, only that the command ran successfully. The contents of the file are randomly-generated test vectors which are non-deterministic. I thought of having a stdout option, but the nondeterminism makes that tricky; what would the expected output be?

[brianhuffman]

I suppose we could specify something like /dev/null as the destination file, except that isn't exactly portable across different operating systems.

[robdockins]

Well, maybe it's overkill, but you could add an optional argument to seed the RNG. It would at least be deterministic then.

[benjaminselfridge]

Instead of an optional argument to :dumptests, what about a separate REPL command for seeding the RNG? I could see that being useful more generally, and it would be easy to integrate into a regression test. It might be worth testing the output itself as well, to ensure that the command not only was executed without failing, but also that what it spits out is consistent.

[robdockins]

@brianhuffman, #951 overlaps this PR, and I'd like to get it merged soon. Do we have a plan here?

[brianhuffman]

I'm fine with merging this PR as-is. In this case, the presence a leftover file will never make any difference to the success or failure of later runs of the regression test, so I don't think it's necessary to implement those other ideas we talked about just yet.