Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion liquidjava-verifier/pom.xml
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@

<groupId>io.github.liquid-java</groupId>
<artifactId>liquidjava-verifier</artifactId>
<version>0.0.8</version>
<version>0.0.10</version>
<name>liquidjava-verifier</name>
<description>LiquidJava Verifier</description>
<url>https://github.com/liquid-java/liquidjava</url>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode;
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
import liquidjava.rj_language.opt.derivation_node.VarDerivationNode;
import liquidjava.utils.Utils;

import java.util.HashMap;
import java.util.Map;
Expand Down Expand Up @@ -47,8 +48,7 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map<String,
DerivationNode previousOrigin = varOrigins.get(name);

// preserve origin if value came from previous derivation
DerivationNode origin = previousOrigin != null ? new VarDerivationNode(name, previousOrigin)
: new VarDerivationNode(name);
DerivationNode origin = flattenVarOrigin(name, previousOrigin);
return new ValDerivationNode(value.clone(), origin);
}

Expand Down Expand Up @@ -138,4 +138,14 @@ private static void extractVarOrigins(ValDerivationNode node, Map<String, Deriva
extractVarOrigins(valOrigin, varOrigins);
}
}

/**
* Flattens same instance variable derivations to avoid redundancy by collapsing var -> var chains
*/
private static VarDerivationNode flattenVarOrigin(String varName, DerivationNode origin) {
if (origin instanceof VarDerivationNode varOrigin && Utils.isSameVariable(varOrigin.getVar(), varName)) {
return flattenVarOrigin(varOrigin.getVar(), varOrigin.getOrigin()); // recursively flatten
}
return origin != null ? new VarDerivationNode(varName, origin) : new VarDerivationNode(varName);
}
}
13 changes: 13 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java
Original file line number Diff line number Diff line change
Expand Up @@ -42,4 +42,17 @@ public static SourcePosition getRefinementAnnotationPosition(CtElement element,
return unquoted.equals(refinement);
}).findFirst().map(CtElement::getPosition).orElse(element.getPosition());
}

public static boolean isSameVariable(String var1, String var2) {
int index1 = var1.lastIndexOf('_');
int index2 = var2.lastIndexOf('_');
// no format
if (index1 < 0 || index2 < 0) {
return var1.equals(var2);
}
// #(.*)_n format
String name1 = var1.substring(0, index1);
String name2 = var2.substring(0, index2);
return name1.equals(name2);
}
}