|
16 | 16 | import java.text.ParsePosition; |
17 | 17 | import java.util.ArrayList; |
18 | 18 | import java.util.Comparator; |
| 19 | +import java.util.HashMap; |
19 | 20 | import java.util.LinkedHashSet; |
20 | 21 | import java.util.List; |
21 | 22 | import java.util.Map; |
@@ -239,6 +240,8 @@ public static int testInvariants(String inputFile, boolean doRange) throws IOExc |
239 | 240 | showMapLine(line, pp); |
240 | 241 | } else if (line.startsWith("Show")) { |
241 | 242 | showLine(line, pp); |
| 243 | + } else if (line.startsWith("EquivalencesOf")) { |
| 244 | + equivalencesLine(line, pp); |
242 | 245 | } else { |
243 | 246 | testLine(line, pp); |
244 | 247 | } |
@@ -272,6 +275,187 @@ static class PropertyComparison { |
272 | 275 | UnicodeProperty property2; |
273 | 276 | } |
274 | 277 |
|
| 278 | + private static void equivalencesLine(String line, ParsePosition pp) throws ParseException { |
| 279 | + pp.setIndex("EquivalencesOf".length()); |
| 280 | + final UnicodeSet domain = new UnicodeSet(line, pp, symbolTable); |
| 281 | + final var leftProperty = CompoundProperty.of(LATEST_PROPS, line, pp); |
| 282 | + scan(PATTERN_WHITE_SPACE, line, pp, true); |
| 283 | + char relationOperator = line.charAt(pp.getIndex()); |
| 284 | + pp.setIndex(pp.getIndex() + 1); |
| 285 | + final var rightProperty = CompoundProperty.of(LATEST_PROPS, line, pp); |
| 286 | + |
| 287 | + boolean leftShouldImplyRight = false; |
| 288 | + boolean rightShouldImplyLeft = false; |
| 289 | + |
| 290 | + boolean negated = true; |
| 291 | + switch (relationOperator) { |
| 292 | + case '⇍': |
| 293 | + relationOperator = '⇐'; |
| 294 | + break; |
| 295 | + case '⇎': |
| 296 | + relationOperator = '⇔'; |
| 297 | + break; |
| 298 | + case '⇏': |
| 299 | + relationOperator = '⇒'; |
| 300 | + break; |
| 301 | + default: |
| 302 | + negated = false; |
| 303 | + } |
| 304 | + |
| 305 | + switch (relationOperator) { |
| 306 | + case '⇐': |
| 307 | + rightShouldImplyLeft = true; |
| 308 | + break; |
| 309 | + case '⇔': |
| 310 | + leftShouldImplyRight = true; |
| 311 | + rightShouldImplyLeft = true; |
| 312 | + break; |
| 313 | + case '⇒': |
| 314 | + leftShouldImplyRight = true; |
| 315 | + break; |
| 316 | + default: |
| 317 | + throw new ParseException(line, pp.getIndex()); |
| 318 | + } |
| 319 | + final var leftValues = new HashMap<String, String>(); |
| 320 | + final var rightValues = new HashMap<String, String>(); |
| 321 | + final var leftClasses = new HashMap<String, UnicodeSet>(); |
| 322 | + final var rightClasses = new HashMap<String, UnicodeSet>(); |
| 323 | + for (String element : domain) { |
| 324 | + final var leftValue = new StringBuilder(); |
| 325 | + final var rightValue = new StringBuilder(); |
| 326 | + for (int codepoint : element.codePoints().toArray()) { |
| 327 | + leftValue.append(leftProperty.getValue(codepoint)); |
| 328 | + rightValue.append(rightProperty.getValue(codepoint)); |
| 329 | + } |
| 330 | + leftValues.put(element, leftValue.toString()); |
| 331 | + rightValues.put(element, rightValue.toString()); |
| 332 | + leftClasses.computeIfAbsent(leftValue.toString(), (k) -> new UnicodeSet()).add(element); |
| 333 | + rightClasses |
| 334 | + .computeIfAbsent(rightValue.toString(), (k) -> new UnicodeSet()) |
| 335 | + .add(element); |
| 336 | + } |
| 337 | + UnicodeSet remainingDomain = domain.cloneAsThawed(); |
| 338 | + final var leftImpliesRightCounterexamples = new ArrayList<String>(); |
| 339 | + final var rightImpliesLeftCounterexamples = new ArrayList<String>(); |
| 340 | + |
| 341 | + // For the implication ⇒, produce at most one counterexample per equivalence class of the |
| 342 | + // left-hand-side equivalence relation: we do not want an example per pair of Unicode code |
| 343 | + // points! |
| 344 | + if (leftShouldImplyRight) { |
| 345 | + while (!remainingDomain.isEmpty()) { |
| 346 | + String representative = remainingDomain.iterator().next(); |
| 347 | + UnicodeSet leftEquivalenceClass = leftClasses.get(leftValues.get(representative)); |
| 348 | + UnicodeSet rightEquivalenceClass = |
| 349 | + rightClasses.get(rightValues.get(representative)); |
| 350 | + if (leftShouldImplyRight |
| 351 | + && !rightEquivalenceClass.containsAll(leftEquivalenceClass)) { |
| 352 | + final String counterexampleRhs = |
| 353 | + leftEquivalenceClass |
| 354 | + .cloneAsThawed() |
| 355 | + .removeAll(rightEquivalenceClass) |
| 356 | + .iterator() |
| 357 | + .next(); |
| 358 | + leftImpliesRightCounterexamples.add( |
| 359 | + "\t\t" |
| 360 | + + leftProperty.getNameAliases() |
| 361 | + + "(" |
| 362 | + + representative |
| 363 | + + ") \t=\t " |
| 364 | + + leftProperty.getNameAliases() |
| 365 | + + "(" |
| 366 | + + counterexampleRhs |
| 367 | + + ") \t=\t " |
| 368 | + + leftValues.get(representative) |
| 369 | + + " \tbut\t " |
| 370 | + + rightValues.get(representative) |
| 371 | + + " \t=\t " |
| 372 | + + rightProperty.getNameAliases() |
| 373 | + + "(" |
| 374 | + + representative |
| 375 | + + ") \t≠\t " |
| 376 | + + rightProperty.getNameAliases() |
| 377 | + + "(" |
| 378 | + + counterexampleRhs |
| 379 | + + ") \t=\t " |
| 380 | + + rightValues.get(counterexampleRhs)); |
| 381 | + } |
| 382 | + remainingDomain.removeAll(leftEquivalenceClass); |
| 383 | + } |
| 384 | + } |
| 385 | + |
| 386 | + // Likewise, for the implication ⇐, produce at most one counterexample per equivalence class |
| 387 | + // of the |
| 388 | + // right-hand-side equivalence relation. |
| 389 | + remainingDomain = domain.cloneAsThawed(); |
| 390 | + if (rightShouldImplyLeft) { |
| 391 | + while (!remainingDomain.isEmpty()) { |
| 392 | + String representative = remainingDomain.iterator().next(); |
| 393 | + UnicodeSet leftEquivalenceClass = leftClasses.get(leftValues.get(representative)); |
| 394 | + UnicodeSet rightEquivalenceClass = |
| 395 | + rightClasses.get(rightValues.get(representative)); |
| 396 | + if (!leftEquivalenceClass.containsAll(rightEquivalenceClass)) { |
| 397 | + final String counterexampleRhs = |
| 398 | + rightEquivalenceClass |
| 399 | + .cloneAsThawed() |
| 400 | + .removeAll(leftEquivalenceClass) |
| 401 | + .iterator() |
| 402 | + .next(); |
| 403 | + rightImpliesLeftCounterexamples.add( |
| 404 | + leftValues.get(representative) |
| 405 | + + " \t=\t " |
| 406 | + + leftProperty.getNameAliases() |
| 407 | + + "(" |
| 408 | + + representative |
| 409 | + + ") \t≠\t " |
| 410 | + + leftProperty.getNameAliases() |
| 411 | + + "(" |
| 412 | + + counterexampleRhs |
| 413 | + + ") \t=\t " |
| 414 | + + rightValues.get(counterexampleRhs) |
| 415 | + + " \teven though\t " |
| 416 | + + rightValues.get(representative) |
| 417 | + + " \t=\t " |
| 418 | + + rightProperty.getNameAliases() |
| 419 | + + "(" |
| 420 | + + representative |
| 421 | + + ") \t=\t " |
| 422 | + + rightProperty.getNameAliases() |
| 423 | + + "(" |
| 424 | + + counterexampleRhs |
| 425 | + + ")\t\t"); |
| 426 | + } |
| 427 | + remainingDomain.removeAll(rightEquivalenceClass); |
| 428 | + } |
| 429 | + } |
| 430 | + final var counterexamples = new ArrayList<>(leftImpliesRightCounterexamples); |
| 431 | + counterexamples.addAll(rightImpliesLeftCounterexamples); |
| 432 | + boolean failure = counterexamples.isEmpty() == negated; |
| 433 | + if (failure) { |
| 434 | + ++testFailureCount; |
| 435 | + printErrorLine("Test Failure", Side.START, testFailureCount); |
| 436 | + } |
| 437 | + if (counterexamples.isEmpty()) { |
| 438 | + println("There are no counterexamples to " + relationOperator + "."); |
| 439 | + } else { |
| 440 | + if (leftShouldImplyRight) { |
| 441 | + println("The implication ⇒ is " + leftImpliesRightCounterexamples.isEmpty() + "."); |
| 442 | + } |
| 443 | + if (rightShouldImplyLeft) { |
| 444 | + println("The implication ⇐ is " + rightImpliesLeftCounterexamples.isEmpty() + "."); |
| 445 | + } |
| 446 | + } |
| 447 | + out.println(failure ? "<table class='f'>" : "<table>"); |
| 448 | + for (String counterexample : counterexamples) { |
| 449 | + out.println("<tr><td>"); |
| 450 | + out.println(toHTML.transform(counterexample).replace("\t", "</td><td>")); |
| 451 | + out.println("</tr></td>"); |
| 452 | + } |
| 453 | + out.println("</table>"); |
| 454 | + if (failure) { |
| 455 | + printErrorLine("Test Failure", Side.END, testFailureCount); |
| 456 | + } |
| 457 | + } |
| 458 | + |
275 | 459 | private static void inLine(ParsePosition pp, String line) throws ParseException { |
276 | 460 | pp.setIndex(2); |
277 | 461 | final PropertyComparison propertyComparison = getPropertyComparison(pp, line); |
@@ -800,6 +984,9 @@ private static void showSet(ParsePosition pp, final String value) { |
800 | 984 | for (final UnicodeSetIterator it = new UnicodeSetIterator(valueSet); |
801 | 985 | it.nextRange() && rangeLimit > 0; |
802 | 986 | --rangeLimit) { |
| 987 | + if (it.codepoint == it.IS_STRING) { |
| 988 | + continue; // TODO(egg): Show strings too. |
| 989 | + } |
803 | 990 | shorter.add(it.codepoint, it.codepointEnd); |
804 | 991 | } |
805 | 992 | abbreviated = totalSize - shorter.size(); |
|
0 commit comments