Skip to content

Instantly share code, notes, and snippets.

@gafter

gafter/Generator.jl

Last active May 17, 2023 22:50
Show Gist options
  • Save gafter/145db4a2282296bdaa08e0a0dcce9217 to your computer and use it in GitHub Desktop.
Save gafter/145db4a2282296bdaa08e0a0dcce9217 to your computer and use it in GitHub Desktop.
Download ZIP
Hard pattern-matching examples for Julia
Raw
Generator.jl
# Generate a pattern-match that is likely to blow up the state machine.
# Intended for use in diagnosing ways to reduce the size of the state machine.
#
# The Julia macro @match in Rematch2 attempts to avoid repeating tests in the code
# generated to determine which is the first matching case. It does this by encoding
# in the state of the generated decision automaton (i.e. the program counter during
# execution) which tests have succeeded and which have failed. As a side-effect,
# this construction permits us to diagnose pattern-matching cases that are
# impossible (because previous cases would match), and matches that are incomplete
# (because some input values would not match any case).
#
# The following constructs a Julia program that uses pattern-matching, but is hard
# to produce those diagnostics. The technique used to generate the target program
# is based on the fact that diagnosing pattern-matching is NP-hard.
#
# See https://niedzejkob.p4.team/rust-np/ for a proof of that fact and a
# reduction from an instance of 3SAT to a program involving pattern-matching.
#
# See https://www.sciencedirect.com/science/article/pii/0004370295000453 for
# a simple construction of a random hard 3SAT instance.
#
# We combine the two, and take advantage of the pattern-matching syntax in Rematch2,
# to simplify the reduction to a linear one.
#
# Since we don't care about definitely diagnosing all matches with impossible cases
# or non-exhaustive matches, we aim to compile these programs quickly into a
# moderate-sized state machine by sometimes not keeping track of which tests have
# been done.
module Generator
using Random
using StatsBase
function main(N::Int)
random = RandomDevice()
println("@match input begin")
for i in 1:(N * 43 ÷ 10)
three_random = sample(random, 1:N, 3; replace = false, ordered = true)
c = join(map(k -> rand(Bool) ? "v$k" : "!v$k", three_random), " && ")
println(" x where ($c) => $i")
end
println("end")
end
main(60)
end # module
Raw
TypicalOutput.jl
@match input begin
x where (v25 && !v51 && !v58) => 1
x where (v5 && !v16 && v36) => 2
x where (!v5 && !v18 && v41) => 3
x where (v5 && !v26 && !v58) => 4
x where (!v23 && !v26 && v39) => 5
x where (!v13 && !v36 && v52) => 6
x where (!v7 && v10 && v29) => 7
x where (!v35 && !v39 && !v46) => 8
x where (v19 && v26 && v54) => 9
x where (!v14 && v33 && !v40) => 10
x where (!v19 && v23 && !v24) => 11
x where (v13 && v30 && !v47) => 12
x where (!v8 && !v48 && v53) => 13
x where (!v6 && v23 && !v32) => 14
x where (v21 && v35 && v45) => 15
x where (v28 && !v57 && !v59) => 16
x where (v3 && !v23 && !v27) => 17
x where (!v29 && v36 && !v39) => 18
x where (!v30 && !v34 && !v53) => 19
x where (v2 && !v11 && v53) => 20
x where (!v9 && !v23 && v24) => 21
x where (v4 && v24 && !v38) => 22
x where (v4 && !v39 && !v59) => 23
x where (v5 && !v21 && !v45) => 24
x where (v34 && !v53 && v60) => 25
x where (!v10 && !v26 && !v44) => 26
x where (v6 && !v35 && !v53) => 27
x where (v1 && v39 && v40) => 28
x where (!v11 && v19 && !v55) => 29
x where (v3 && v7 && !v55) => 30
x where (v24 && v30 && !v57) => 31
x where (!v7 && v58 && !v60) => 32
x where (v14 && !v43 && v52) => 33
x where (v8 && !v43 && v56) => 34
x where (v31 && !v37 && v53) => 35
x where (!v8 && !v15 && v26) => 36
x where (!v1 && !v25 && !v43) => 37
x where (v24 && !v34 && v43) => 38
x where (v4 && v36 && v43) => 39
x where (!v22 && v39 && !v56) => 40
x where (v8 && v12 && v47) => 41
x where (!v32 && !v42 && !v45) => 42
x where (!v18 && v53 && !v56) => 43
x where (!v22 && !v25 && v59) => 44
x where (!v13 && v21 && v24) => 45
x where (!v17 && !v59 && v60) => 46
x where (!v8 && v30 && !v53) => 47
x where (!v8 && !v37 && !v54) => 48
x where (!v8 && !v51 && !v55) => 49
x where (v10 && v13 && v40) => 50
x where (v14 && v22 && !v36) => 51
x where (!v6 && !v17 && !v36) => 52
x where (v17 && v37 && !v44) => 53
x where (v5 && !v8 && v25) => 54
x where (!v5 && v11 && v33) => 55
x where (v13 && v26 && !v52) => 56
x where (v16 && !v31 && v35) => 57
x where (!v4 && v11 && !v58) => 58
x where (!v9 && v36 && v59) => 59
x where (v41 && v58 && !v60) => 60
x where (v5 && !v39 && !v57) => 61
x where (v18 && !v52 && v59) => 62
x where (!v3 && v34 && !v49) => 63
x where (v11 && !v34 && !v58) => 64
x where (v1 && !v2 && !v14) => 65
x where (v9 && !v23 && !v29) => 66
x where (!v45 && !v50 && !v51) => 67
x where (v31 && !v50 && v53) => 68
x where (!v6 && v53 && !v60) => 69
x where (!v5 && v6 && v41) => 70
x where (v8 && !v43 && v50) => 71
x where (!v4 && !v48 && !v60) => 72
x where (!v24 && !v27 && v50) => 73
x where (v12 && !v44 && v58) => 74
x where (!v10 && v18 && v44) => 75
x where (!v3 && !v38 && !v43) => 76
x where (v45 && v48 && !v57) => 77
x where (!v2 && !v31 && !v50) => 78
x where (v27 && !v47 && !v55) => 79
x where (v7 && v15 && !v42) => 80
x where (!v13 && v37 && v56) => 81
x where (!v18 && v45 && v55) => 82
x where (v3 && !v44 && v52) => 83
x where (v1 && !v42 && !v53) => 84
x where (v5 && !v7 && v40) => 85
x where (!v14 && v20 && v32) => 86
x where (!v16 && v34 && !v43) => 87
x where (!v9 && !v46 && v55) => 88
x where (!v34 && v35 && v50) => 89
x where (v3 && v34 && v52) => 90
x where (v11 && v44 && v60) => 91
x where (v14 && v21 && v48) => 92
x where (v5 && !v19 && v51) => 93
x where (!v24 && v31 && v48) => 94
x where (!v6 && v13 && v49) => 95
x where (!v28 && !v39 && v53) => 96
x where (v7 && v47 && !v50) => 97
x where (v25 && !v39 && !v57) => 98
x where (!v13 && v42 && v48) => 99
x where (!v16 && v25 && v44) => 100
x where (v10 && !v11 && !v23) => 101
x where (v14 && v34 && !v50) => 102
x where (v2 && v53 && !v59) => 103
x where (v39 && v54 && !v56) => 104
x where (v4 && v20 && v45) => 105
x where (!v6 && !v26 && !v46) => 106
x where (!v1 && !v40 && v59) => 107
x where (!v23 && !v40 && v57) => 108
x where (v12 && v56 && !v58) => 109
x where (v3 && !v20 && v60) => 110
x where (v37 && v48 && v52) => 111
x where (!v17 && !v22 && !v46) => 112
x where (v21 && !v36 && v45) => 113
x where (v29 && v37 && !v41) => 114
x where (!v18 && !v21 && v46) => 115
x where (v8 && v24 && v40) => 116
x where (v20 && !v27 && !v29) => 117
x where (!v20 && !v36 && v52) => 118
x where (!v19 && !v46 && !v54) => 119
x where (v11 && !v21 && v30) => 120
x where (v8 && !v21 && !v55) => 121
x where (!v9 && !v40 && v46) => 122
x where (!v7 && !v20 && v43) => 123
x where (v4 && !v12 && v35) => 124
x where (v33 && !v53 && !v58) => 125
x where (!v15 && v42 && !v43) => 126
x where (v36 && v44 && !v58) => 127
x where (!v30 && !v53 && !v54) => 128
x where (v31 && v39 && v52) => 129
x where (!v41 && v50 && v55) => 130
x where (v11 && !v14 && !v39) => 131
x where (v22 && v55 && !v58) => 132
x where (!v31 && !v49 && !v59) => 133
x where (!v6 && v21 && v41) => 134
x where (v18 && v46 && v53) => 135
x where (v13 && !v30 && v48) => 136
x where (!v3 && !v31 && !v57) => 137
x where (!v23 && v24 && !v38) => 138
x where (v15 && v26 && !v34) => 139
x where (v1 && v2 && !v30) => 140
x where (v15 && !v17 && !v22) => 141
x where (!v21 && v40 && v59) => 142
x where (v29 && !v33 && v38) => 143
x where (v13 && !v15 && v36) => 144
x where (!v1 && v29 && !v33) => 145
x where (v10 && v44 && !v57) => 146
x where (!v5 && v22 && v55) => 147
x where (!v11 && v25 && !v28) => 148
x where (v13 && !v15 && !v35) => 149
x where (v3 && !v33 && !v55) => 150
x where (v16 && v29 && !v35) => 151
x where (v27 && v33 && !v36) => 152
x where (v8 && !v31 && v48) => 153
x where (v15 && v18 && v25) => 154
x where (v7 && !v23 && !v43) => 155
x where (v12 && v33 && !v51) => 156
x where (!v5 && !v56 && v59) => 157
x where (!v18 && !v19 && !v36) => 158
x where (v12 && v14 && !v54) => 159
x where (v25 && v37 && v45) => 160
x where (v3 && v27 && !v35) => 161
x where (v25 && !v29 && v52) => 162
x where (v6 && !v13 && !v50) => 163
x where (v6 && !v9 && v23) => 164
x where (!v17 && !v23 && v42) => 165
x where (!v18 && !v33 && !v38) => 166
x where (!v6 && v12 && !v37) => 167
x where (!v1 && !v9 && !v17) => 168
x where (v3 && !v30 && v45) => 169
x where (v1 && v37 && !v45) => 170
x where (v14 && v18 && !v53) => 171
x where (v3 && !v13 && v32) => 172
x where (!v8 && v41 && !v47) => 173
x where (!v11 && v34 && v49) => 174
x where (!v18 && v28 && !v57) => 175
x where (!v5 && !v34 && v54) => 176
x where (v14 && v36 && v52) => 177
x where (v35 && !v54 && v55) => 178
x where (!v7 && !v26 && v47) => 179
x where (v11 && v26 && !v28) => 180
x where (v33 && !v43 && !v56) => 181
x where (v25 && v27 && !v56) => 182
x where (!v36 && !v42 && v54) => 183
x where (v12 && !v25 && v32) => 184
x where (!v5 && !v21 && !v24) => 185
x where (!v2 && v3 && v10) => 186
x where (v6 && v10 && !v16) => 187
x where (!v16 && !v46 && v54) => 188
x where (!v15 && v23 && v47) => 189
x where (v17 && v43 && !v60) => 190
x where (v15 && v28 && v34) => 191
x where (v39 && !v44 && v58) => 192
x where (v5 && v16 && v32) => 193
x where (!v4 && !v19 && !v41) => 194
x where (!v19 && v27 && !v28) => 195
x where (!v26 && !v35 && !v54) => 196
x where (v25 && !v47 && v55) => 197
x where (v30 && v32 && v59) => 198
x where (v34 && !v47 && v52) => 199
x where (!v19 && v23 && !v31) => 200
x where (v25 && v31 && v46) => 201
x where (v4 && !v14 && v34) => 202
x where (v7 && v12 && v34) => 203
x where (v31 && v50 && !v52) => 204
x where (!v15 && !v30 && v44) => 205
x where (!v21 && !v35 && v60) => 206
x where (v22 && v33 && v45) => 207
x where (v17 && !v18 && !v52) => 208
x where (v30 && v42 && !v59) => 209
x where (v1 && !v2 && v16) => 210
x where (!v18 && !v46 && v48) => 211
x where (v11 && !v31 && !v47) => 212
x where (!v3 && !v4 && !v16) => 213
x where (!v12 && !v27 && v39) => 214
x where (v13 && v46 && !v60) => 215
x where (!v6 && v51 && v55) => 216
x where (!v30 && v35 && v42) => 217
x where (v5 && v12 && v45) => 218
x where (v5 && v14 && !v29) => 219
x where (v5 && !v28 && v33) => 220
x where (v12 && !v25 && v34) => 221
x where (!v3 && v11 && !v37) => 222
x where (v26 && !v27 && v58) => 223
x where (v26 && v33 && v34) => 224
x where (!v16 && !v36 && v54) => 225
x where (v24 && !v32 && !v58) => 226
x where (v3 && v6 && v54) => 227
x where (v9 && !v16 && !v18) => 228
x where (v34 && v47 && v52) => 229
x where (v3 && !v36 && v38) => 230
x where (v4 && v25 && !v57) => 231
x where (v13 && v57 && v59) => 232
x where (v35 && v37 && v48) => 233
x where (v32 && !v43 && !v59) => 234
x where (!v23 && !v25 && v53) => 235
x where (v6 && v27 && v46) => 236
x where (!v22 && !v26 && !v50) => 237
x where (v2 && !v37 && !v50) => 238
x where (v17 && !v46 && v47) => 239
x where (v15 && v31 && v37) => 240
x where (!v4 && v43 && !v56) => 241
x where (!v19 && v27 && !v51) => 242
x where (!v32 && v33 && v41) => 243
x where (v1 && v50 && !v51) => 244
x where (!v11 && !v30 && v46) => 245
x where (v2 && v9 && !v45) => 246
x where (v14 && !v29 && v41) => 247
x where (v21 && !v46 && !v60) => 248
x where (v7 && !v16 && v38) => 249
x where (!v26 && !v29 && v36) => 250
x where (v8 && !v57 && !v59) => 251
x where (!v16 && v17 && !v32) => 252
x where (!v4 && v12 && !v39) => 253
x where (v4 && !v26 && !v49) => 254
x where (v3 && !v36 && !v44) => 255
x where (v28 && v47 && v60) => 256
x where (!v27 && !v48 && !v53) => 257
x where (!v37 && !v40 && v43) => 258
_ => 259
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment