1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
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)))
|
