summaryrefslogtreecommitdiff
path: root/testsuite/tests/pmcheck/should_compile/genS.py
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/tests/pmcheck/should_compile/genS.py')
-rwxr-xr-xtestsuite/tests/pmcheck/should_compile/genS.py72
1 files changed, 72 insertions, 0 deletions
diff --git a/testsuite/tests/pmcheck/should_compile/genS.py b/testsuite/tests/pmcheck/should_compile/genS.py
new file mode 100755
index 0000000000..529401cbfc
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/genS.py
@@ -0,0 +1,72 @@
+#! /usr/bin/env python3
+
+# See #17264.
+#
+# Generates a module of Luc Maranget's S series
+#
+# module S where
+#
+# data T = A | B
+#
+# s :: T -> T -> T -> T -> T -> T -> T -> T -> ()
+# s A A _ _ _ _ _ _ = ()
+# s _ _ A A _ _ _ _ = ()
+# s _ _ _ _ A A _ _ = ()
+# s _ _ _ _ _ _ A A = ()
+# s A B A B A B A B = ()
+#
+# Note how each clause splits into 2 uncovered Deltas
+# The last clause isn't strictly necessary to exhibit
+# exponential behavior in our algorithm, but the number
+# of missing matches is 2^n-1, easily demonstrated by
+# looking at the missing matches for S_2:
+#
+# B _ B _
+# A B B _
+# B _ A B
+
+import sys
+
+size = int(sys.argv[1]) if len(sys.argv) > 1 else 5
+
+a = 'A'
+b = 'B'
+wc = '_'
+
+def horiz_join(M, N):
+ return [ row_M + row_N for (row_M, row_N) in zip(M, N) ]
+
+def vert_join(M, N):
+ return M + N
+
+def n_cols(M):
+ return len(M[0])
+
+def s_rec(n):
+ if n == 1:
+ return [ [ a, a ] ]
+ s_sub = s_rec(n-1)
+ top_row = [ [ a, a ] + [ wc ]*n_cols(s_sub) ]
+ left_col = [ [ wc, wc ] ]*len(s_sub)
+ return vert_join(top_row, horiz_join(left_col, s_sub))
+
+def s(n):
+ return vert_join(s_rec(n), [ [ a, b ]*n ])
+
+def debug_print(M):
+ for row in M:
+ print("".join(row))
+
+def format_hs(M):
+ hdr = """module S where
+
+data T = A | B
+
+"""
+
+ fun = "s :: " + "T -> "*n_cols(M) + "()\n"
+ for row in M:
+ fun += "s " + " ".join(row) + "= ()\n"
+ return hdr + fun
+
+open("S.hs", "w").write(format_hs(s(size)))