-
Notifications
You must be signed in to change notification settings - Fork 0
/
UseRandomGenerator.hint
60 lines (48 loc) · 2.04 KB
/
UseRandomGenerator.hint
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
<?
import javax.lang.model.element.ElementKind;
?>
<!description="Introduce java.util.random.* API.">
// declarations
$modifiers$ java.util.Random $rng; :: sourceVersionGE(17) =>
$modifiers$ java.util.random.RandomGenerator $rng;
;;
$modifiers$ java.util.Random $rng = $initializer; :: sourceVersionGE(17) =>
$modifiers$ java.util.random.RandomGenerator $rng = $initializer;
;;
// assignments
// should be '$rng super java.util.random.RandomGenerator'
$rng = new java.util.Random($seed$) :: !$rng instanceof java.util.Random && sourceVersionGE(17)
=> $rng = java.util.random.RandomGeneratorFactory.of("Random").create($seed$)
=> $rng = java.util.random.RandomGeneratorFactory.getDefault().create($seed$)
=> $rng = RandomGenerator.getDefault()
;;
// this is redundant but required because the above hack does not catch
// RandomGenerator old2 = new Random() for some reason
java.util.random.RandomGenerator $rng = new java.util.Random($seed$) && sourceVersionGE(17)
=> java.util.random.RandomGenerator $rng = java.util.random.RandomGeneratorFactory.of("Random").create($seed$)
=> java.util.random.RandomGenerator $rng = java.util.random.RandomGeneratorFactory.getDefault().create($seed$)
=> java.util.random.RandomGenerator $rng = RandomGenerator.getDefault()
;;
// passed as value to methods or constructors
new java.util.Random($seed$) :: isPassedToMethod() && sourceVersionGE(17)
=> java.util.random.RandomGeneratorFactory.of("Random").create($seed$)
=> java.util.random.RandomGeneratorFactory.getDefault().create($seed$)
=> RandomGenerator.getDefault()
;;
<?
public boolean isPassedToMethod() throws Throwable {
Variable parent = context.parent(context.variableForName("$_"));
if (parent == null) {
return false;
}
ElementKind kind = context.elementKind(parent);
return kind == ElementKind.METHOD || kind == ElementKind.CONSTRUCTOR;
}
?>
/*
new java.util.Random($seed$)
=>java.util.random.RandomGeneratorFactory.of("Random").create($seed$)
=>java.util.random.RandomGeneratorFactory.getDefault().create($seed$)
=>RandomGenerator.getDefault()
;;
*/