From ec5a50436adf5fa210fb3eb4ea4223c827462012 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Sun, 1 Nov 2020 16:19:50 -0800
Subject: [PATCH 1/2] Fix bug in `dumpableType` function. Fixes #946.

The function now works as documented, and succeeds on function
types that do not have `Bit` as a return type.
---
 src/Cryptol/Testing/Random.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs
index ae585ee85..8f063b537 100644
--- a/src/Cryptol/Testing/Random.hs
+++ b/src/Cryptol/Testing/Random.hs
@@ -111,7 +111,7 @@ dumpableType ty =
   case tIsFun ty of
     Just (t1, t2) ->
       do g  <- randomValue Concrete t1
-         as <- testableTypeGenerators t2
+         as <- dumpableType t2
          return (g : as)
     Nothing ->
       do (_ :: Gen g Concrete) <- randomValue Concrete ty

From fdd7aab01aaebcb68d88f5f4d2bde0c0f2c2bb75 Mon Sep 17 00:00:00 2001
From: Ben Selfridge <benselfridge@galois.com>
Date: Mon, 2 Nov 2020 13:59:22 -0800
Subject: [PATCH 2/2] Adds regression test for dumptests.

This only checks that a function with signature [32] -> [32] -> [32] will
succeed with the :dumptests command. More tests could/should be added.

Since this test creates a file called add32.out, I added tests/regression/*.out
to the .gitignore. I'm not sure if this is the right approach or if we should
make an attempt to clean up this subdirectory after the tests finish.
---
 .gitignore                             | 1 +
 tests/regression/dumptests.cry         | 2 ++
 tests/regression/dumptests.icry        | 3 +++
 tests/regression/dumptests.icry.stdout | 3 +++
 4 files changed, 9 insertions(+)
 create mode 100644 tests/regression/dumptests.cry
 create mode 100644 tests/regression/dumptests.icry
 create mode 100644 tests/regression/dumptests.icry.stdout

diff --git a/.gitignore b/.gitignore
index a73fa7685..8827bc1db 100644
--- a/.gitignore
+++ b/.gitignore
@@ -30,3 +30,4 @@ cryptol-2.*
 # ignore test suite output
 /bin
 /output
+/tests/regression/*.out
diff --git a/tests/regression/dumptests.cry b/tests/regression/dumptests.cry
new file mode 100644
index 000000000..0427fb343
--- /dev/null
+++ b/tests/regression/dumptests.cry
@@ -0,0 +1,2 @@
+add32 : [32] -> [32] -> [32]
+add32 x y = x + y
\ No newline at end of file
diff --git a/tests/regression/dumptests.icry b/tests/regression/dumptests.icry
new file mode 100644
index 000000000..369d882eb
--- /dev/null
+++ b/tests/regression/dumptests.icry
@@ -0,0 +1,3 @@
+:set tests=100
+:l dumptests.cry
+:dumptests add32.out add32
\ No newline at end of file
diff --git a/tests/regression/dumptests.icry.stdout b/tests/regression/dumptests.icry.stdout
new file mode 100644
index 000000000..57a1d7a1c
--- /dev/null
+++ b/tests/regression/dumptests.icry.stdout
@@ -0,0 +1,3 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main