Util: Refactor DenseRank implementation

This commit is contained in:
Tom Hvitved
2024-11-20 13:09:59 +01:00
parent 6a3e34cc4c
commit 42e0d7ce10
2 changed files with 21 additions and 23 deletions

View File

@@ -378,7 +378,7 @@ module Impl {
} }
} }
private module DenseRankInput implements DenseRankInputSig3 { private module DenseRankInput implements DenseRankInputSig2 {
class C1 = VariableScope; class C1 = VariableScope;
class C2 = string; class C2 = string;
@@ -401,7 +401,7 @@ module Impl {
* to a variable named `name` in the variable scope `scope`. * to a variable named `name` in the variable scope `scope`.
*/ */
private int rankVariableOrAccess(VariableScope scope, string name, VariableOrAccessCand v) { private int rankVariableOrAccess(VariableScope scope, string name, VariableOrAccessCand v) {
result = DenseRank3<DenseRankInput>::denseRank(scope, name, v) - 1 v = DenseRank2<DenseRankInput>::denseRank(scope, name, result + 1)
} }
/** /**

View File

@@ -58,12 +58,12 @@ module DenseRank<DenseRankInputSig Input> {
rnk = rank[result](int rnk0 | rnk0 = getRank(_) | rnk0) rnk = rank[result](int rnk0 | rnk0 = getRank(_) | rnk0)
} }
/** Gets the dense rank of `r`. */ /** Gets the `Ranked` value for which the dense rank is `rnk`. */
int denseRank(Ranked r) { result = rankRank(r, getRank(r)) } Ranked denseRank(int rnk) { rnk = rankRank(result, getRank(result)) }
} }
/** Provides the input to `DenseRank2`. */ /** Provides the input to `DenseRank1`. */
signature module DenseRankInputSig2 { signature module DenseRankInputSig1 {
/** A ranking context. */ /** A ranking context. */
bindingset[this] bindingset[this]
class C; class C;
@@ -77,7 +77,7 @@ signature module DenseRankInputSig2 {
} }
/** Same as `DenseRank`, but allows for a context consisting of one element. */ /** Same as `DenseRank`, but allows for a context consisting of one element. */
module DenseRank2<DenseRankInputSig2 Input> { module DenseRank1<DenseRankInputSig1 Input> {
private import Input private import Input
private int rankRank(C c, Ranked r, int rnk) { private int rankRank(C c, Ranked r, int rnk) {
@@ -85,17 +85,15 @@ module DenseRank2<DenseRankInputSig2 Input> {
rnk = rank[result](int rnk0 | rnk0 = getRank(c, _) | rnk0) rnk = rank[result](int rnk0 | rnk0 = getRank(c, _) | rnk0)
} }
/** Gets the dense rank of `r` in the context provided by `c`. */ /**
int denseRank(C c, Ranked r) { * Gets the `Ranked` value for which the dense rank in the context provided by
exists(int rnk | * `c` is `rnk`.
result = rankRank(c, r, rnk) and */
rnk = getRank(c, r) Ranked denseRank(C c, int rnk) { rnk = rankRank(c, result, getRank(c, result)) }
)
}
} }
/** Provides the input to `DenseRank3`. */ /** Provides the input to `DenseRank2`. */
signature module DenseRankInputSig3 { signature module DenseRankInputSig2 {
/** A ranking context. */ /** A ranking context. */
bindingset[this] bindingset[this]
class C1; class C1;
@@ -113,7 +111,7 @@ signature module DenseRankInputSig3 {
} }
/** Same as `DenseRank`, but allows for a context consisting of two elements. */ /** Same as `DenseRank`, but allows for a context consisting of two elements. */
module DenseRank3<DenseRankInputSig3 Input> { module DenseRank2<DenseRankInputSig2 Input> {
private import Input private import Input
private int rankRank(C1 c1, C2 c2, Ranked r, int rnk) { private int rankRank(C1 c1, C2 c2, Ranked r, int rnk) {
@@ -121,11 +119,11 @@ module DenseRank3<DenseRankInputSig3 Input> {
rnk = rank[result](int rnk0 | rnk0 = getRank(c1, c2, _) | rnk0) rnk = rank[result](int rnk0 | rnk0 = getRank(c1, c2, _) | rnk0)
} }
/** Gets the dense rank of `r` in the context provided by `c1` and `c2`. */ /**
int denseRank(C1 c1, C2 c2, Ranked r) { * Gets the `Ranked` value for which the dense rank in the context provided by
exists(int rnk | * `c1` and `c2` is `rnk`.
result = rankRank(c1, c2, r, rnk) and */
rnk = getRank(c1, c2, r) Ranked denseRank(C1 c1, C2 c2, int rnk) {
) rnk = rankRank(c1, c2, result, getRank(c1, c2, result))
} }
} }