Skip to content

Conversation

@rcosta358
Copy link
Collaborator

Cleaned up some code by:

  • Moving scattered constants into dedicated classes: Formats, Keys, Ops, Patterns and Types
  • Refactoring some if else statements to switch cases instead
  • Updating some switch cases to use arrow syntax instead
  • Commenting out some unused methods (to be potentially removed in the future)

@rcosta358 rcosta358 self-assigned this Nov 9, 2025
Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

looks good, check the comments


public StateConflictError(CtElement element, Predicate predicate, String className) {
super("State Conflict Error", "Found multiple disjoint states from a StateSet in refinement", element);
super("State Conflict Error", "Found multiple disjoint states in state transition", element);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could even improve this message to something like "Found multiple disjoint states in state transition - State transition can only go to one state of each state set"

String name = String.format(freshFormat, context.getCounter());
if (c.getVariableNames().contains(WILD_VAR)) {
c = c.substituteVariable(WILD_VAR, name);
String name = String.format(Formats.RET, context.getCounter());
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why are we changing from fresh to return?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good eye! 😅

System.out.println("\nSMT subtyping:" + stringSMT + " <: " + expectedType.toString());
System.out.println("--------------------------------------------------------------");
}
// private void printVCs(String string, String stringSMT, Predicate expectedType) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

eliminate this code already, we can always go a previous version in git to get them

Predicate cSMTMessageReady = premises; // substituteByMap(premises, map);
ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter);
}
// private void printError(Predicate premises, Predicate expectedType, CtElement element,
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

same here

// TODO COMPLETE WITH MORE OPERANDS
}
return switch (kind) {
case PLUS -> Ops.PLUS;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

niceee

}
return noOld;
}
// private static Predicate changeVarsFields(Predicate pred, TypeChecker tc) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

delete

case Types.BOOLEAN -> new LiteralBoolean(value);
case Types.INT, Types.SHORT -> new LiteralInt(value);
case Types.DOUBLE, Types.LONG -> new LiteralReal(value);
default -> new LiteralReal(value);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

in the future if we want to add strings this default can be a problem, maybe we can emit an error or smt

Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In a followup for cleanup feel free to remove all code in comments, its just polluting the codebase

@rcosta358 rcosta358 merged commit 11a9263 into main Nov 10, 2025
1 check passed
@rcosta358 rcosta358 deleted the code-refactoring branch November 11, 2025 20:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants