dumptests undocumented

[kiniry]

The dumptests REPL command was added by @david-christiansen, but it is undocumented in Programming Cryptol. There are also no examples of its use shipped with Cryptol.

[weaversa]

Cryptol> :dumptests "test" \(x : [32]) -> x + 1

The expression is not of a testable type.
Type: [32] -> [32]

:dumptests only seems to support functions that return type Bit. I'm feeling like supporting expressions in general (not just theorems) would be helpful. Here I just want to generate some input/output pairs for a function so that when I modify/optimize/etc it I can test to see if I've messed it up.

[brianhuffman]

We do have in-REPL documentation for :dumptests. So if we implement #612 to give us an auto-generated markdown file containing all the REPL command help text, we can just include that as an appendix to the book and that should take care of this issue as well.

[kiniry]

Ensuring that dumpTests is in the Cryptol book and reference manual ASAP is now of high priority. CC @andrew-bivin @mccleeary-galois

[mccleeary-galois]

Cryptol> :dumptests "test" \(x : [32]) -> x + 1

The expression is not of a testable type.
Type: [32] -> [32]

:dumptests only seems to support functions that return type Bit. I'm feeling like supporting expressions in general (not just theorems) would be helpful. Here I just want to generate some input/output pairs for a function so that when I modify/optimize/etc it I can test to see if I've messed it up.

Just an FYI this appears to be the functionality now in which it can work on any function and generate test vectors for you. See example in #1760