- public void collectRefs(TObjectIntHashMap<Object> allRefs, TIntHashSet refs) {
- head.collectRefs(allRefs, refs);
- body.collectRefs(allRefs, refs);
+ private static final Object NEVER_USED = new Object();
+
+ private void warnForExistentialsUsedOnlyOnce(TranslationContext context) {
+ // Initialize the hash map
+ HashMap<Variable, Object> usageCount = new HashMap<>(existentialVariables.length);
+ for(Variable var : existentialVariables)
+ if(!var.getName().equals("_"))
+ usageCount.put(var, NEVER_USED);
+
+ // Collect variable uses
+ ExpressionVisitor visitor = new StandardExpressionVisitor() {
+ private void handle(Expression expression, Variable variable) {
+ Object object = usageCount.remove(variable);
+ if(object == NEVER_USED)
+ usageCount.put(variable, expression);
+ }
+ @Override
+ public void visit(EVariable expression) {
+ if(expression.variable != null)
+ handle(expression, expression.variable);
+ }
+ @Override
+ public void visit(EAsPattern expression) {
+ expression.pattern.accept(this);
+ handle(expression, expression.var);
+ }
+ };
+ head.accept(visitor);
+ body.accept(visitor);
+
+ // Report as warnings
+ usageCount.forEach((variable, expression_) -> {
+ if(!(expression_ instanceof Expression))
+ return; // Should never happen
+ Expression expression = (Expression)expression_;
+ if(context.isExpandedFromWildcard(expression))
+ return;
+
+ context.getErrorLog().logWarning(expression.location,
+ "Existential variable " + variable.getName() + " is referred only once. Replace by _ if this is a wildcard.");
+ });
+