1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Fri May 25 21:08:45 2007 +0200
1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Fri May 25 21:08:46 2007 +0200
1.3 @@ -6,21 +6,21 @@
1.4
1.5 datatype nat = Zero_nat | Suc of nat;
1.6
1.7 +fun eq_nat Zero_nat (Suc m) = false
1.8 + | eq_nat (Suc n) Zero_nat = false
1.9 + | eq_nat (Suc n) (Suc m) = eq_nat n m
1.10 + | eq_nat Zero_nat Zero_nat = true;
1.11 +
1.12 fun plus_nat (Suc m) n = plus_nat m (Suc n)
1.13 | plus_nat Zero_nat n = n;
1.14
1.15 -fun op_eq_nat Zero_nat (Suc m) = false
1.16 - | op_eq_nat (Suc n) Zero_nat = false
1.17 - | op_eq_nat (Suc n) (Suc m) = op_eq_nat n m
1.18 - | op_eq_nat Zero_nat Zero_nat = true;
1.19 -
1.20 end; (*struct Nat*)
1.21
1.22 structure Code_Generator =
1.23 struct
1.24
1.25 -type 'a eq = {op_eq : 'a -> 'a -> bool};
1.26 -fun op_eq (A_:'a eq) = #op_eq A_;
1.27 +type 'a eq = {eq : 'a -> 'a -> bool};
1.28 +fun eq (A_:'a eq) = #eq A_;
1.29
1.30 end; (*struct Code_Generator*)
1.31
1.32 @@ -40,267 +40,273 @@
1.33 fun null (x :: xs) = false
1.34 | null [] = true;
1.35
1.36 -fun op_eq_nibble Nibble0 Nibble0 = true
1.37 - | op_eq_nibble Nibble1 Nibble1 = true
1.38 - | op_eq_nibble Nibble2 Nibble2 = true
1.39 - | op_eq_nibble Nibble3 Nibble3 = true
1.40 - | op_eq_nibble Nibble4 Nibble4 = true
1.41 - | op_eq_nibble Nibble5 Nibble5 = true
1.42 - | op_eq_nibble Nibble6 Nibble6 = true
1.43 - | op_eq_nibble Nibble7 Nibble7 = true
1.44 - | op_eq_nibble Nibble8 Nibble8 = true
1.45 - | op_eq_nibble Nibble9 Nibble9 = true
1.46 - | op_eq_nibble NibbleA NibbleA = true
1.47 - | op_eq_nibble NibbleB NibbleB = true
1.48 - | op_eq_nibble NibbleC NibbleC = true
1.49 - | op_eq_nibble NibbleD NibbleD = true
1.50 - | op_eq_nibble NibbleE NibbleE = true
1.51 - | op_eq_nibble NibbleF NibbleF = true
1.52 - | op_eq_nibble Nibble0 Nibble1 = false
1.53 - | op_eq_nibble Nibble0 Nibble2 = false
1.54 - | op_eq_nibble Nibble0 Nibble3 = false
1.55 - | op_eq_nibble Nibble0 Nibble4 = false
1.56 - | op_eq_nibble Nibble0 Nibble5 = false
1.57 - | op_eq_nibble Nibble0 Nibble6 = false
1.58 - | op_eq_nibble Nibble0 Nibble7 = false
1.59 - | op_eq_nibble Nibble0 Nibble8 = false
1.60 - | op_eq_nibble Nibble0 Nibble9 = false
1.61 - | op_eq_nibble Nibble0 NibbleA = false
1.62 - | op_eq_nibble Nibble0 NibbleB = false
1.63 - | op_eq_nibble Nibble0 NibbleC = false
1.64 - | op_eq_nibble Nibble0 NibbleD = false
1.65 - | op_eq_nibble Nibble0 NibbleE = false
1.66 - | op_eq_nibble Nibble0 NibbleF = false
1.67 - | op_eq_nibble Nibble1 Nibble2 = false
1.68 - | op_eq_nibble Nibble1 Nibble3 = false
1.69 - | op_eq_nibble Nibble1 Nibble4 = false
1.70 - | op_eq_nibble Nibble1 Nibble5 = false
1.71 - | op_eq_nibble Nibble1 Nibble6 = false
1.72 - | op_eq_nibble Nibble1 Nibble7 = false
1.73 - | op_eq_nibble Nibble1 Nibble8 = false
1.74 - | op_eq_nibble Nibble1 Nibble9 = false
1.75 - | op_eq_nibble Nibble1 NibbleA = false
1.76 - | op_eq_nibble Nibble1 NibbleB = false
1.77 - | op_eq_nibble Nibble1 NibbleC = false
1.78 - | op_eq_nibble Nibble1 NibbleD = false
1.79 - | op_eq_nibble Nibble1 NibbleE = false
1.80 - | op_eq_nibble Nibble1 NibbleF = false
1.81 - | op_eq_nibble Nibble2 Nibble3 = false
1.82 - | op_eq_nibble Nibble2 Nibble4 = false
1.83 - | op_eq_nibble Nibble2 Nibble5 = false
1.84 - | op_eq_nibble Nibble2 Nibble6 = false
1.85 - | op_eq_nibble Nibble2 Nibble7 = false
1.86 - | op_eq_nibble Nibble2 Nibble8 = false
1.87 - | op_eq_nibble Nibble2 Nibble9 = false
1.88 - | op_eq_nibble Nibble2 NibbleA = false
1.89 - | op_eq_nibble Nibble2 NibbleB = false
1.90 - | op_eq_nibble Nibble2 NibbleC = false
1.91 - | op_eq_nibble Nibble2 NibbleD = false
1.92 - | op_eq_nibble Nibble2 NibbleE = false
1.93 - | op_eq_nibble Nibble2 NibbleF = false
1.94 - | op_eq_nibble Nibble3 Nibble4 = false
1.95 - | op_eq_nibble Nibble3 Nibble5 = false
1.96 - | op_eq_nibble Nibble3 Nibble6 = false
1.97 - | op_eq_nibble Nibble3 Nibble7 = false
1.98 - | op_eq_nibble Nibble3 Nibble8 = false
1.99 - | op_eq_nibble Nibble3 Nibble9 = false
1.100 - | op_eq_nibble Nibble3 NibbleA = false
1.101 - | op_eq_nibble Nibble3 NibbleB = false
1.102 - | op_eq_nibble Nibble3 NibbleC = false
1.103 - | op_eq_nibble Nibble3 NibbleD = false
1.104 - | op_eq_nibble Nibble3 NibbleE = false
1.105 - | op_eq_nibble Nibble3 NibbleF = false
1.106 - | op_eq_nibble Nibble4 Nibble5 = false
1.107 - | op_eq_nibble Nibble4 Nibble6 = false
1.108 - | op_eq_nibble Nibble4 Nibble7 = false
1.109 - | op_eq_nibble Nibble4 Nibble8 = false
1.110 - | op_eq_nibble Nibble4 Nibble9 = false
1.111 - | op_eq_nibble Nibble4 NibbleA = false
1.112 - | op_eq_nibble Nibble4 NibbleB = false
1.113 - | op_eq_nibble Nibble4 NibbleC = false
1.114 - | op_eq_nibble Nibble4 NibbleD = false
1.115 - | op_eq_nibble Nibble4 NibbleE = false
1.116 - | op_eq_nibble Nibble4 NibbleF = false
1.117 - | op_eq_nibble Nibble5 Nibble6 = false
1.118 - | op_eq_nibble Nibble5 Nibble7 = false
1.119 - | op_eq_nibble Nibble5 Nibble8 = false
1.120 - | op_eq_nibble Nibble5 Nibble9 = false
1.121 - | op_eq_nibble Nibble5 NibbleA = false
1.122 - | op_eq_nibble Nibble5 NibbleB = false
1.123 - | op_eq_nibble Nibble5 NibbleC = false
1.124 - | op_eq_nibble Nibble5 NibbleD = false
1.125 - | op_eq_nibble Nibble5 NibbleE = false
1.126 - | op_eq_nibble Nibble5 NibbleF = false
1.127 - | op_eq_nibble Nibble6 Nibble7 = false
1.128 - | op_eq_nibble Nibble6 Nibble8 = false
1.129 - | op_eq_nibble Nibble6 Nibble9 = false
1.130 - | op_eq_nibble Nibble6 NibbleA = false
1.131 - | op_eq_nibble Nibble6 NibbleB = false
1.132 - | op_eq_nibble Nibble6 NibbleC = false
1.133 - | op_eq_nibble Nibble6 NibbleD = false
1.134 - | op_eq_nibble Nibble6 NibbleE = false
1.135 - | op_eq_nibble Nibble6 NibbleF = false
1.136 - | op_eq_nibble Nibble7 Nibble8 = false
1.137 - | op_eq_nibble Nibble7 Nibble9 = false
1.138 - | op_eq_nibble Nibble7 NibbleA = false
1.139 - | op_eq_nibble Nibble7 NibbleB = false
1.140 - | op_eq_nibble Nibble7 NibbleC = false
1.141 - | op_eq_nibble Nibble7 NibbleD = false
1.142 - | op_eq_nibble Nibble7 NibbleE = false
1.143 - | op_eq_nibble Nibble7 NibbleF = false
1.144 - | op_eq_nibble Nibble8 Nibble9 = false
1.145 - | op_eq_nibble Nibble8 NibbleA = false
1.146 - | op_eq_nibble Nibble8 NibbleB = false
1.147 - | op_eq_nibble Nibble8 NibbleC = false
1.148 - | op_eq_nibble Nibble8 NibbleD = false
1.149 - | op_eq_nibble Nibble8 NibbleE = false
1.150 - | op_eq_nibble Nibble8 NibbleF = false
1.151 - | op_eq_nibble Nibble9 NibbleA = false
1.152 - | op_eq_nibble Nibble9 NibbleB = false
1.153 - | op_eq_nibble Nibble9 NibbleC = false
1.154 - | op_eq_nibble Nibble9 NibbleD = false
1.155 - | op_eq_nibble Nibble9 NibbleE = false
1.156 - | op_eq_nibble Nibble9 NibbleF = false
1.157 - | op_eq_nibble NibbleA NibbleB = false
1.158 - | op_eq_nibble NibbleA NibbleC = false
1.159 - | op_eq_nibble NibbleA NibbleD = false
1.160 - | op_eq_nibble NibbleA NibbleE = false
1.161 - | op_eq_nibble NibbleA NibbleF = false
1.162 - | op_eq_nibble NibbleB NibbleC = false
1.163 - | op_eq_nibble NibbleB NibbleD = false
1.164 - | op_eq_nibble NibbleB NibbleE = false
1.165 - | op_eq_nibble NibbleB NibbleF = false
1.166 - | op_eq_nibble NibbleC NibbleD = false
1.167 - | op_eq_nibble NibbleC NibbleE = false
1.168 - | op_eq_nibble NibbleC NibbleF = false
1.169 - | op_eq_nibble NibbleD NibbleE = false
1.170 - | op_eq_nibble NibbleD NibbleF = false
1.171 - | op_eq_nibble NibbleE NibbleF = false
1.172 - | op_eq_nibble Nibble1 Nibble0 = false
1.173 - | op_eq_nibble Nibble2 Nibble0 = false
1.174 - | op_eq_nibble Nibble3 Nibble0 = false
1.175 - | op_eq_nibble Nibble4 Nibble0 = false
1.176 - | op_eq_nibble Nibble5 Nibble0 = false
1.177 - | op_eq_nibble Nibble6 Nibble0 = false
1.178 - | op_eq_nibble Nibble7 Nibble0 = false
1.179 - | op_eq_nibble Nibble8 Nibble0 = false
1.180 - | op_eq_nibble Nibble9 Nibble0 = false
1.181 - | op_eq_nibble NibbleA Nibble0 = false
1.182 - | op_eq_nibble NibbleB Nibble0 = false
1.183 - | op_eq_nibble NibbleC Nibble0 = false
1.184 - | op_eq_nibble NibbleD Nibble0 = false
1.185 - | op_eq_nibble NibbleE Nibble0 = false
1.186 - | op_eq_nibble NibbleF Nibble0 = false
1.187 - | op_eq_nibble Nibble2 Nibble1 = false
1.188 - | op_eq_nibble Nibble3 Nibble1 = false
1.189 - | op_eq_nibble Nibble4 Nibble1 = false
1.190 - | op_eq_nibble Nibble5 Nibble1 = false
1.191 - | op_eq_nibble Nibble6 Nibble1 = false
1.192 - | op_eq_nibble Nibble7 Nibble1 = false
1.193 - | op_eq_nibble Nibble8 Nibble1 = false
1.194 - | op_eq_nibble Nibble9 Nibble1 = false
1.195 - | op_eq_nibble NibbleA Nibble1 = false
1.196 - | op_eq_nibble NibbleB Nibble1 = false
1.197 - | op_eq_nibble NibbleC Nibble1 = false
1.198 - | op_eq_nibble NibbleD Nibble1 = false
1.199 - | op_eq_nibble NibbleE Nibble1 = false
1.200 - | op_eq_nibble NibbleF Nibble1 = false
1.201 - | op_eq_nibble Nibble3 Nibble2 = false
1.202 - | op_eq_nibble Nibble4 Nibble2 = false
1.203 - | op_eq_nibble Nibble5 Nibble2 = false
1.204 - | op_eq_nibble Nibble6 Nibble2 = false
1.205 - | op_eq_nibble Nibble7 Nibble2 = false
1.206 - | op_eq_nibble Nibble8 Nibble2 = false
1.207 - | op_eq_nibble Nibble9 Nibble2 = false
1.208 - | op_eq_nibble NibbleA Nibble2 = false
1.209 - | op_eq_nibble NibbleB Nibble2 = false
1.210 - | op_eq_nibble NibbleC Nibble2 = false
1.211 - | op_eq_nibble NibbleD Nibble2 = false
1.212 - | op_eq_nibble NibbleE Nibble2 = false
1.213 - | op_eq_nibble NibbleF Nibble2 = false
1.214 - | op_eq_nibble Nibble4 Nibble3 = false
1.215 - | op_eq_nibble Nibble5 Nibble3 = false
1.216 - | op_eq_nibble Nibble6 Nibble3 = false
1.217 - | op_eq_nibble Nibble7 Nibble3 = false
1.218 - | op_eq_nibble Nibble8 Nibble3 = false
1.219 - | op_eq_nibble Nibble9 Nibble3 = false
1.220 - | op_eq_nibble NibbleA Nibble3 = false
1.221 - | op_eq_nibble NibbleB Nibble3 = false
1.222 - | op_eq_nibble NibbleC Nibble3 = false
1.223 - | op_eq_nibble NibbleD Nibble3 = false
1.224 - | op_eq_nibble NibbleE Nibble3 = false
1.225 - | op_eq_nibble NibbleF Nibble3 = false
1.226 - | op_eq_nibble Nibble5 Nibble4 = false
1.227 - | op_eq_nibble Nibble6 Nibble4 = false
1.228 - | op_eq_nibble Nibble7 Nibble4 = false
1.229 - | op_eq_nibble Nibble8 Nibble4 = false
1.230 - | op_eq_nibble Nibble9 Nibble4 = false
1.231 - | op_eq_nibble NibbleA Nibble4 = false
1.232 - | op_eq_nibble NibbleB Nibble4 = false
1.233 - | op_eq_nibble NibbleC Nibble4 = false
1.234 - | op_eq_nibble NibbleD Nibble4 = false
1.235 - | op_eq_nibble NibbleE Nibble4 = false
1.236 - | op_eq_nibble NibbleF Nibble4 = false
1.237 - | op_eq_nibble Nibble6 Nibble5 = false
1.238 - | op_eq_nibble Nibble7 Nibble5 = false
1.239 - | op_eq_nibble Nibble8 Nibble5 = false
1.240 - | op_eq_nibble Nibble9 Nibble5 = false
1.241 - | op_eq_nibble NibbleA Nibble5 = false
1.242 - | op_eq_nibble NibbleB Nibble5 = false
1.243 - | op_eq_nibble NibbleC Nibble5 = false
1.244 - | op_eq_nibble NibbleD Nibble5 = false
1.245 - | op_eq_nibble NibbleE Nibble5 = false
1.246 - | op_eq_nibble NibbleF Nibble5 = false
1.247 - | op_eq_nibble Nibble7 Nibble6 = false
1.248 - | op_eq_nibble Nibble8 Nibble6 = false
1.249 - | op_eq_nibble Nibble9 Nibble6 = false
1.250 - | op_eq_nibble NibbleA Nibble6 = false
1.251 - | op_eq_nibble NibbleB Nibble6 = false
1.252 - | op_eq_nibble NibbleC Nibble6 = false
1.253 - | op_eq_nibble NibbleD Nibble6 = false
1.254 - | op_eq_nibble NibbleE Nibble6 = false
1.255 - | op_eq_nibble NibbleF Nibble6 = false
1.256 - | op_eq_nibble Nibble8 Nibble7 = false
1.257 - | op_eq_nibble Nibble9 Nibble7 = false
1.258 - | op_eq_nibble NibbleA Nibble7 = false
1.259 - | op_eq_nibble NibbleB Nibble7 = false
1.260 - | op_eq_nibble NibbleC Nibble7 = false
1.261 - | op_eq_nibble NibbleD Nibble7 = false
1.262 - | op_eq_nibble NibbleE Nibble7 = false
1.263 - | op_eq_nibble NibbleF Nibble7 = false
1.264 - | op_eq_nibble Nibble9 Nibble8 = false
1.265 - | op_eq_nibble NibbleA Nibble8 = false
1.266 - | op_eq_nibble NibbleB Nibble8 = false
1.267 - | op_eq_nibble NibbleC Nibble8 = false
1.268 - | op_eq_nibble NibbleD Nibble8 = false
1.269 - | op_eq_nibble NibbleE Nibble8 = false
1.270 - | op_eq_nibble NibbleF Nibble8 = false
1.271 - | op_eq_nibble NibbleA Nibble9 = false
1.272 - | op_eq_nibble NibbleB Nibble9 = false
1.273 - | op_eq_nibble NibbleC Nibble9 = false
1.274 - | op_eq_nibble NibbleD Nibble9 = false
1.275 - | op_eq_nibble NibbleE Nibble9 = false
1.276 - | op_eq_nibble NibbleF Nibble9 = false
1.277 - | op_eq_nibble NibbleB NibbleA = false
1.278 - | op_eq_nibble NibbleC NibbleA = false
1.279 - | op_eq_nibble NibbleD NibbleA = false
1.280 - | op_eq_nibble NibbleE NibbleA = false
1.281 - | op_eq_nibble NibbleF NibbleA = false
1.282 - | op_eq_nibble NibbleC NibbleB = false
1.283 - | op_eq_nibble NibbleD NibbleB = false
1.284 - | op_eq_nibble NibbleE NibbleB = false
1.285 - | op_eq_nibble NibbleF NibbleB = false
1.286 - | op_eq_nibble NibbleD NibbleC = false
1.287 - | op_eq_nibble NibbleE NibbleC = false
1.288 - | op_eq_nibble NibbleF NibbleC = false
1.289 - | op_eq_nibble NibbleE NibbleD = false
1.290 - | op_eq_nibble NibbleF NibbleD = false
1.291 - | op_eq_nibble NibbleF NibbleE = false;
1.292 +fun eq_nibble Nibble0 Nibble0 = true
1.293 + | eq_nibble Nibble1 Nibble1 = true
1.294 + | eq_nibble Nibble2 Nibble2 = true
1.295 + | eq_nibble Nibble3 Nibble3 = true
1.296 + | eq_nibble Nibble4 Nibble4 = true
1.297 + | eq_nibble Nibble5 Nibble5 = true
1.298 + | eq_nibble Nibble6 Nibble6 = true
1.299 + | eq_nibble Nibble7 Nibble7 = true
1.300 + | eq_nibble Nibble8 Nibble8 = true
1.301 + | eq_nibble Nibble9 Nibble9 = true
1.302 + | eq_nibble NibbleA NibbleA = true
1.303 + | eq_nibble NibbleB NibbleB = true
1.304 + | eq_nibble NibbleC NibbleC = true
1.305 + | eq_nibble NibbleD NibbleD = true
1.306 + | eq_nibble NibbleE NibbleE = true
1.307 + | eq_nibble NibbleF NibbleF = true
1.308 + | eq_nibble Nibble0 Nibble1 = false
1.309 + | eq_nibble Nibble0 Nibble2 = false
1.310 + | eq_nibble Nibble0 Nibble3 = false
1.311 + | eq_nibble Nibble0 Nibble4 = false
1.312 + | eq_nibble Nibble0 Nibble5 = false
1.313 + | eq_nibble Nibble0 Nibble6 = false
1.314 + | eq_nibble Nibble0 Nibble7 = false
1.315 + | eq_nibble Nibble0 Nibble8 = false
1.316 + | eq_nibble Nibble0 Nibble9 = false
1.317 + | eq_nibble Nibble0 NibbleA = false
1.318 + | eq_nibble Nibble0 NibbleB = false
1.319 + | eq_nibble Nibble0 NibbleC = false
1.320 + | eq_nibble Nibble0 NibbleD = false
1.321 + | eq_nibble Nibble0 NibbleE = false
1.322 + | eq_nibble Nibble0 NibbleF = false
1.323 + | eq_nibble Nibble1 Nibble2 = false
1.324 + | eq_nibble Nibble1 Nibble3 = false
1.325 + | eq_nibble Nibble1 Nibble4 = false
1.326 + | eq_nibble Nibble1 Nibble5 = false
1.327 + | eq_nibble Nibble1 Nibble6 = false
1.328 + | eq_nibble Nibble1 Nibble7 = false
1.329 + | eq_nibble Nibble1 Nibble8 = false
1.330 + | eq_nibble Nibble1 Nibble9 = false
1.331 + | eq_nibble Nibble1 NibbleA = false
1.332 + | eq_nibble Nibble1 NibbleB = false
1.333 + | eq_nibble Nibble1 NibbleC = false
1.334 + | eq_nibble Nibble1 NibbleD = false
1.335 + | eq_nibble Nibble1 NibbleE = false
1.336 + | eq_nibble Nibble1 NibbleF = false
1.337 + | eq_nibble Nibble2 Nibble3 = false
1.338 + | eq_nibble Nibble2 Nibble4 = false
1.339 + | eq_nibble Nibble2 Nibble5 = false
1.340 + | eq_nibble Nibble2 Nibble6 = false
1.341 + | eq_nibble Nibble2 Nibble7 = false
1.342 + | eq_nibble Nibble2 Nibble8 = false
1.343 + | eq_nibble Nibble2 Nibble9 = false
1.344 + | eq_nibble Nibble2 NibbleA = false
1.345 + | eq_nibble Nibble2 NibbleB = false
1.346 + | eq_nibble Nibble2 NibbleC = false
1.347 + | eq_nibble Nibble2 NibbleD = false
1.348 + | eq_nibble Nibble2 NibbleE = false
1.349 + | eq_nibble Nibble2 NibbleF = false
1.350 + | eq_nibble Nibble3 Nibble4 = false
1.351 + | eq_nibble Nibble3 Nibble5 = false
1.352 + | eq_nibble Nibble3 Nibble6 = false
1.353 + | eq_nibble Nibble3 Nibble7 = false
1.354 + | eq_nibble Nibble3 Nibble8 = false
1.355 + | eq_nibble Nibble3 Nibble9 = false
1.356 + | eq_nibble Nibble3 NibbleA = false
1.357 + | eq_nibble Nibble3 NibbleB = false
1.358 + | eq_nibble Nibble3 NibbleC = false
1.359 + | eq_nibble Nibble3 NibbleD = false
1.360 + | eq_nibble Nibble3 NibbleE = false
1.361 + | eq_nibble Nibble3 NibbleF = false
1.362 + | eq_nibble Nibble4 Nibble5 = false
1.363 + | eq_nibble Nibble4 Nibble6 = false
1.364 + | eq_nibble Nibble4 Nibble7 = false
1.365 + | eq_nibble Nibble4 Nibble8 = false
1.366 + | eq_nibble Nibble4 Nibble9 = false
1.367 + | eq_nibble Nibble4 NibbleA = false
1.368 + | eq_nibble Nibble4 NibbleB = false
1.369 + | eq_nibble Nibble4 NibbleC = false
1.370 + | eq_nibble Nibble4 NibbleD = false
1.371 + | eq_nibble Nibble4 NibbleE = false
1.372 + | eq_nibble Nibble4 NibbleF = false
1.373 + | eq_nibble Nibble5 Nibble6 = false
1.374 + | eq_nibble Nibble5 Nibble7 = false
1.375 + | eq_nibble Nibble5 Nibble8 = false
1.376 + | eq_nibble Nibble5 Nibble9 = false
1.377 + | eq_nibble Nibble5 NibbleA = false
1.378 + | eq_nibble Nibble5 NibbleB = false
1.379 + | eq_nibble Nibble5 NibbleC = false
1.380 + | eq_nibble Nibble5 NibbleD = false
1.381 + | eq_nibble Nibble5 NibbleE = false
1.382 + | eq_nibble Nibble5 NibbleF = false
1.383 + | eq_nibble Nibble6 Nibble7 = false
1.384 + | eq_nibble Nibble6 Nibble8 = false
1.385 + | eq_nibble Nibble6 Nibble9 = false
1.386 + | eq_nibble Nibble6 NibbleA = false
1.387 + | eq_nibble Nibble6 NibbleB = false
1.388 + | eq_nibble Nibble6 NibbleC = false
1.389 + | eq_nibble Nibble6 NibbleD = false
1.390 + | eq_nibble Nibble6 NibbleE = false
1.391 + | eq_nibble Nibble6 NibbleF = false
1.392 + | eq_nibble Nibble7 Nibble8 = false
1.393 + | eq_nibble Nibble7 Nibble9 = false
1.394 + | eq_nibble Nibble7 NibbleA = false
1.395 + | eq_nibble Nibble7 NibbleB = false
1.396 + | eq_nibble Nibble7 NibbleC = false
1.397 + | eq_nibble Nibble7 NibbleD = false
1.398 + | eq_nibble Nibble7 NibbleE = false
1.399 + | eq_nibble Nibble7 NibbleF = false
1.400 + | eq_nibble Nibble8 Nibble9 = false
1.401 + | eq_nibble Nibble8 NibbleA = false
1.402 + | eq_nibble Nibble8 NibbleB = false
1.403 + | eq_nibble Nibble8 NibbleC = false
1.404 + | eq_nibble Nibble8 NibbleD = false
1.405 + | eq_nibble Nibble8 NibbleE = false
1.406 + | eq_nibble Nibble8 NibbleF = false
1.407 + | eq_nibble Nibble9 NibbleA = false
1.408 + | eq_nibble Nibble9 NibbleB = false
1.409 + | eq_nibble Nibble9 NibbleC = false
1.410 + | eq_nibble Nibble9 NibbleD = false
1.411 + | eq_nibble Nibble9 NibbleE = false
1.412 + | eq_nibble Nibble9 NibbleF = false
1.413 + | eq_nibble NibbleA NibbleB = false
1.414 + | eq_nibble NibbleA NibbleC = false
1.415 + | eq_nibble NibbleA NibbleD = false
1.416 + | eq_nibble NibbleA NibbleE = false
1.417 + | eq_nibble NibbleA NibbleF = false
1.418 + | eq_nibble NibbleB NibbleC = false
1.419 + | eq_nibble NibbleB NibbleD = false
1.420 + | eq_nibble NibbleB NibbleE = false
1.421 + | eq_nibble NibbleB NibbleF = false
1.422 + | eq_nibble NibbleC NibbleD = false
1.423 + | eq_nibble NibbleC NibbleE = false
1.424 + | eq_nibble NibbleC NibbleF = false
1.425 + | eq_nibble NibbleD NibbleE = false
1.426 + | eq_nibble NibbleD NibbleF = false
1.427 + | eq_nibble NibbleE NibbleF = false
1.428 + | eq_nibble Nibble1 Nibble0 = false
1.429 + | eq_nibble Nibble2 Nibble0 = false
1.430 + | eq_nibble Nibble3 Nibble0 = false
1.431 + | eq_nibble Nibble4 Nibble0 = false
1.432 + | eq_nibble Nibble5 Nibble0 = false
1.433 + | eq_nibble Nibble6 Nibble0 = false
1.434 + | eq_nibble Nibble7 Nibble0 = false
1.435 + | eq_nibble Nibble8 Nibble0 = false
1.436 + | eq_nibble Nibble9 Nibble0 = false
1.437 + | eq_nibble NibbleA Nibble0 = false
1.438 + | eq_nibble NibbleB Nibble0 = false
1.439 + | eq_nibble NibbleC Nibble0 = false
1.440 + | eq_nibble NibbleD Nibble0 = false
1.441 + | eq_nibble NibbleE Nibble0 = false
1.442 + | eq_nibble NibbleF Nibble0 = false
1.443 + | eq_nibble Nibble2 Nibble1 = false
1.444 + | eq_nibble Nibble3 Nibble1 = false
1.445 + | eq_nibble Nibble4 Nibble1 = false
1.446 + | eq_nibble Nibble5 Nibble1 = false
1.447 + | eq_nibble Nibble6 Nibble1 = false
1.448 + | eq_nibble Nibble7 Nibble1 = false
1.449 + | eq_nibble Nibble8 Nibble1 = false
1.450 + | eq_nibble Nibble9 Nibble1 = false
1.451 + | eq_nibble NibbleA Nibble1 = false
1.452 + | eq_nibble NibbleB Nibble1 = false
1.453 + | eq_nibble NibbleC Nibble1 = false
1.454 + | eq_nibble NibbleD Nibble1 = false
1.455 + | eq_nibble NibbleE Nibble1 = false
1.456 + | eq_nibble NibbleF Nibble1 = false
1.457 + | eq_nibble Nibble3 Nibble2 = false
1.458 + | eq_nibble Nibble4 Nibble2 = false
1.459 + | eq_nibble Nibble5 Nibble2 = false
1.460 + | eq_nibble Nibble6 Nibble2 = false
1.461 + | eq_nibble Nibble7 Nibble2 = false
1.462 + | eq_nibble Nibble8 Nibble2 = false
1.463 + | eq_nibble Nibble9 Nibble2 = false
1.464 + | eq_nibble NibbleA Nibble2 = false
1.465 + | eq_nibble NibbleB Nibble2 = false
1.466 + | eq_nibble NibbleC Nibble2 = false
1.467 + | eq_nibble NibbleD Nibble2 = false
1.468 + | eq_nibble NibbleE Nibble2 = false
1.469 + | eq_nibble NibbleF Nibble2 = false
1.470 + | eq_nibble Nibble4 Nibble3 = false
1.471 + | eq_nibble Nibble5 Nibble3 = false
1.472 + | eq_nibble Nibble6 Nibble3 = false
1.473 + | eq_nibble Nibble7 Nibble3 = false
1.474 + | eq_nibble Nibble8 Nibble3 = false
1.475 + | eq_nibble Nibble9 Nibble3 = false
1.476 + | eq_nibble NibbleA Nibble3 = false
1.477 + | eq_nibble NibbleB Nibble3 = false
1.478 + | eq_nibble NibbleC Nibble3 = false
1.479 + | eq_nibble NibbleD Nibble3 = false
1.480 + | eq_nibble NibbleE Nibble3 = false
1.481 + | eq_nibble NibbleF Nibble3 = false
1.482 + | eq_nibble Nibble5 Nibble4 = false
1.483 + | eq_nibble Nibble6 Nibble4 = false
1.484 + | eq_nibble Nibble7 Nibble4 = false
1.485 + | eq_nibble Nibble8 Nibble4 = false
1.486 + | eq_nibble Nibble9 Nibble4 = false
1.487 + | eq_nibble NibbleA Nibble4 = false
1.488 + | eq_nibble NibbleB Nibble4 = false
1.489 + | eq_nibble NibbleC Nibble4 = false
1.490 + | eq_nibble NibbleD Nibble4 = false
1.491 + | eq_nibble NibbleE Nibble4 = false
1.492 + | eq_nibble NibbleF Nibble4 = false
1.493 + | eq_nibble Nibble6 Nibble5 = false
1.494 + | eq_nibble Nibble7 Nibble5 = false
1.495 + | eq_nibble Nibble8 Nibble5 = false
1.496 + | eq_nibble Nibble9 Nibble5 = false
1.497 + | eq_nibble NibbleA Nibble5 = false
1.498 + | eq_nibble NibbleB Nibble5 = false
1.499 + | eq_nibble NibbleC Nibble5 = false
1.500 + | eq_nibble NibbleD Nibble5 = false
1.501 + | eq_nibble NibbleE Nibble5 = false
1.502 + | eq_nibble NibbleF Nibble5 = false
1.503 + | eq_nibble Nibble7 Nibble6 = false
1.504 + | eq_nibble Nibble8 Nibble6 = false
1.505 + | eq_nibble Nibble9 Nibble6 = false
1.506 + | eq_nibble NibbleA Nibble6 = false
1.507 + | eq_nibble NibbleB Nibble6 = false
1.508 + | eq_nibble NibbleC Nibble6 = false
1.509 + | eq_nibble NibbleD Nibble6 = false
1.510 + | eq_nibble NibbleE Nibble6 = false
1.511 + | eq_nibble NibbleF Nibble6 = false
1.512 + | eq_nibble Nibble8 Nibble7 = false
1.513 + | eq_nibble Nibble9 Nibble7 = false
1.514 + | eq_nibble NibbleA Nibble7 = false
1.515 + | eq_nibble NibbleB Nibble7 = false
1.516 + | eq_nibble NibbleC Nibble7 = false
1.517 + | eq_nibble NibbleD Nibble7 = false
1.518 + | eq_nibble NibbleE Nibble7 = false
1.519 + | eq_nibble NibbleF Nibble7 = false
1.520 + | eq_nibble Nibble9 Nibble8 = false
1.521 + | eq_nibble NibbleA Nibble8 = false
1.522 + | eq_nibble NibbleB Nibble8 = false
1.523 + | eq_nibble NibbleC Nibble8 = false
1.524 + | eq_nibble NibbleD Nibble8 = false
1.525 + | eq_nibble NibbleE Nibble8 = false
1.526 + | eq_nibble NibbleF Nibble8 = false
1.527 + | eq_nibble NibbleA Nibble9 = false
1.528 + | eq_nibble NibbleB Nibble9 = false
1.529 + | eq_nibble NibbleC Nibble9 = false
1.530 + | eq_nibble NibbleD Nibble9 = false
1.531 + | eq_nibble NibbleE Nibble9 = false
1.532 + | eq_nibble NibbleF Nibble9 = false
1.533 + | eq_nibble NibbleB NibbleA = false
1.534 + | eq_nibble NibbleC NibbleA = false
1.535 + | eq_nibble NibbleD NibbleA = false
1.536 + | eq_nibble NibbleE NibbleA = false
1.537 + | eq_nibble NibbleF NibbleA = false
1.538 + | eq_nibble NibbleC NibbleB = false
1.539 + | eq_nibble NibbleD NibbleB = false
1.540 + | eq_nibble NibbleE NibbleB = false
1.541 + | eq_nibble NibbleF NibbleB = false
1.542 + | eq_nibble NibbleD NibbleC = false
1.543 + | eq_nibble NibbleE NibbleC = false
1.544 + | eq_nibble NibbleF NibbleC = false
1.545 + | eq_nibble NibbleE NibbleD = false
1.546 + | eq_nibble NibbleF NibbleD = false
1.547 + | eq_nibble NibbleF NibbleE = false;
1.548
1.549 -fun op_eq_char (Char (nibble1, nibble2)) (Char (nibble1', nibble2')) =
1.550 - op_eq_nibble nibble1 nibble1' andalso op_eq_nibble nibble2 nibble2';
1.551 +fun eq_char (Char (nibble1, nibble2)) (Char (nibble1', nibble2')) =
1.552 + eq_nibble nibble1 nibble1' andalso eq_nibble nibble2 nibble2';
1.553
1.554 -val eq_char = {op_eq = op_eq_char} : char Code_Generator.eq;
1.555 +val eq_chara = {eq = eq_char} : char Code_Generator.eq;
1.556 +
1.557 +fun eq_list A_ [] [] = true
1.558 + | eq_list A_ (a :: lista) (a' :: list') =
1.559 + Code_Generator.eq A_ a a' andalso eq_list A_ lista list'
1.560 + | eq_list A_ [] (a :: b) = false
1.561 + | eq_list A_ (a :: b) [] = false;
1.562
1.563 fun list_all p (x :: xs) = p x andalso list_all p xs
1.564 | list_all p [] = true;
1.565 @@ -313,15 +319,9 @@
1.566 | list_all2 p xs [] = null xs
1.567 | list_all2 p [] ys = null ys
1.568 | list_all2 p xs ys =
1.569 - Nat.op_eq_nat (size_list xs) (size_list ys) andalso
1.570 + Nat.eq_nat (size_list xs) (size_list ys) andalso
1.571 list_all (fn a as (aa, b) => p aa b) (zip xs ys);
1.572
1.573 -fun op_eq_list A_ [] [] = true
1.574 - | op_eq_list A_ (a :: lista) (a' :: list') =
1.575 - Code_Generator.op_eq A_ a a' andalso op_eq_list A_ lista list'
1.576 - | op_eq_list A_ [] (a :: b) = false
1.577 - | op_eq_list A_ (a :: b) [] = false;
1.578 -
1.579 end; (*struct List*)
1.580
1.581 structure Codegen =
1.582 @@ -329,9 +329,9 @@
1.583
1.584 datatype monotype = Mono of List.char list * monotype list;
1.585
1.586 -fun op_eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
1.587 - List.op_eq_list List.eq_char tyco1 tyco2 andalso
1.588 - List.list_all2 op_eq_monotype typargs1 typargs2;
1.589 +fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
1.590 + List.eq_list List.eq_chara tyco1 tyco2 andalso
1.591 + List.list_all2 eq_monotype typargs1 typargs2;
1.592
1.593 end; (*struct Codegen*)
1.594