Merge branch 'main' into refactor-refinement-predicate

liquid-java · rcosta358 · Apr 11, 2026 · Apr 7, 2026 · Apr 7, 2026 · Apr 11, 2026
commit cd78b7aef34ae036b1970a3e6143465aa41d8cd5
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java b/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java
@@ -26,7 +26,7 @@
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
-@Repeatable(GhostMultiple.class)
+@Repeatable(Ghost.Multiple.class)
 public @interface Ghost {
 
     /**
@@ -40,4 +40,13 @@
      * </pre>
      */
     String value();
+
+    /**
+     * Container annotation used by {@link Repeatable} to support multiple ghost declarations.
+     */
+    @Retention(RetentionPolicy.RUNTIME)
+    @Target({ElementType.TYPE})
+    @interface Multiple {
+        Ghost[] value();
+    }
 }
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java
@@ -28,7 +28,7 @@
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
-@Repeatable(RefinementAliasMultiple.class)
+@Repeatable(RefinementAlias.Multiple.class)
 public @interface RefinementAlias {
 
     /**
@@ -42,4 +42,13 @@
      * </pre>
      */
     String value();
+
+    /**
+     * Container annotation used by {@link Repeatable} to support multiple refinement aliases.
+     */
+    @Retention(RetentionPolicy.RUNTIME)
+    @Target({ElementType.TYPE})
+    @interface Multiple {
+        RefinementAlias[] value();
+    }
 }
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java
@@ -29,7 +29,7 @@
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
-@Repeatable(RefinementPredicateMultiple.class)
+@Repeatable(RefinementPredicate.Multiple.class)
 public @interface RefinementPredicate {
 
     /**
@@ -43,4 +43,13 @@
      * </pre>
      */
     String value();
+
+    /**
+     * Container annotation used by {@link Repeatable} to support multiple refinement predicates.
+     */
+    @Retention(RetentionPolicy.RUNTIME)
+    @Target({ElementType.TYPE})
+    @interface Multiple {
+        RefinementPredicate[] value();
+    }
 }
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java
@@ -28,7 +28,7 @@
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
-@Repeatable(StateRefinementMultiple.class)
+@Repeatable(StateRefinement.Multiple.class)
 public @interface StateRefinement {
 
     /**
@@ -66,4 +66,13 @@
      * </pre>
      */
     String msg() default "";
+
+    /**
+     * Container annotation used by {@link Repeatable} to support multiple state transitions.
+     */
+    @Retention(RetentionPolicy.RUNTIME)
+    @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+    @interface Multiple {
+        StateRefinement[] value();
+    }
 }
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java
@@ -28,7 +28,7 @@
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
-@Repeatable(StateSets.class)
+@Repeatable(StateSet.Multiple.class)
 public @interface StateSet {
 
     /**
@@ -42,4 +42,13 @@
      * </pre>
      */
     String[] value();
+
+    /**
+     * Container annotation used by {@link Repeatable} to support multiple state sets.
+     */
+    @Retention(RetentionPolicy.RUNTIME)
+    @Target({ElementType.TYPE})
+    @interface Multiple {
+        StateSet[] value();
+    }
 }
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumField.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumField.java
@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class CorrectEnumField {
+    enum Color {
+        Red, Green, Blue
+    }
+
+    @Refinement("color != Color.Blue")
+    Color color;
+
+    void setColor(@Refinement("c != Color.Blue") Color c) {
+        color = c;
+    }
+
+    public static void main(String[] args) {
+        CorrectEnumField cef = new CorrectEnumField();
+        cef.setColor(Color.Red);   // correct
+        cef.setColor(Color.Green); // correct
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumParam.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumParam.java
@@ -0,0 +1,19 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class CorrectEnumParam {
+    enum Status {
+        Active, Inactive, Pending
+    }
+
+    Status process(@Refinement("status == Status.Inactive") Status status) {
+        return Status.Active;
+    }
+
+    public static void main(String[] args) {
+        CorrectEnumParam cep = new CorrectEnumParam();
+        cep.process(Status.Inactive); // correct
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumRefinement.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumRefinement.java
@@ -0,0 +1,15 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+class CorrectEnumRefinement {
+    enum Lever {
+        Up, Down, Middle
+    }
+
+    public static void main(String[] args) {
+        @Refinement("_==Lever.Up || _==Lever.Down")
+        Lever lever = Lever.Up;
+        System.out.println(lever);
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java
@@ -0,0 +1,45 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@SuppressWarnings("unused")
+@StateSet({"photoMode", "videoMode", "noMode"})
+class CorrectEnumUsage {
+	enum Mode {
+		Photo, Video, Unknown
+	}
+
+	Mode mode;
+	@StateRefinement(to="noMode(this)")
+	public CorrectEnumUsage() {}
+
+	@StateRefinement(from="noMode(this) && mode == Mode.Photo", to="photoMode(this)")
+	@StateRefinement(from="noMode(this) && mode == Mode.Video", to="videoMode(this)")
+	public void setMode(Mode mode) {
+		this.mode = mode;
+	}
+
+	@StateRefinement(from="photoMode(this)", to="noMode(this)")
+	@StateRefinement(from="videoMode(this)", to="noMode(this)")
+	public void resetMode() {
+		this.mode = null;
+	}
+
+	@StateRefinement(from="photoMode(this)")
+	public void takePhoto() {}
+
+	@StateRefinement(from="videoMode(this)")
+	public void takeVideo() {}
+
+
+	public static void main(String[] args) {
+		// Correct
+		CorrectEnumUsage st = new CorrectEnumUsage();
+		st.setMode(Mode.Photo);  // noMode -> photoMode
+		st.takePhoto();
+		st.resetMode();          // photoMode -> noMode
+		st.setMode(Mode.Video);  // noMode -> videoMode
+		st.takeVideo();
+	}
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumFunctionRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumFunctionRefinement.java
@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class ErrorEnumFunctionRefinement {
+	enum Color {
+		Red, Green, Blue
+	}
+
+	Color c;
+
+	Color changeColor(@Refinement("newColor == Color.Red || newColor == Color.Green") Color newColor) {
+		c = newColor;
+		return c;
+	}
+
+	public static void main(String[] args) {
+		ErrorEnumFunctionRefinement e = new ErrorEnumFunctionRefinement();
+		e.changeColor(Color.Red);
+		e.changeColor(Color.Blue); // Refinement Error
+	}
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java
@@ -0,0 +1,18 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class ErrorEnumNegation {
+    enum Status {
+        Active, Inactive, Pending
+    }
+
+    void process(@Refinement("status != Status.Inactive") Status status) {}
+
+    public static void main(String[] args) {
+        ErrorEnumNegation e = new ErrorEnumNegation();
+        e.process(Status.Active);
+        e.process(Status.Inactive); // Refinement Error
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java
@@ -0,0 +1,15 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class ErrorEnumNull {
+	enum Color {
+		Red, Green, Blue
+	}
+
+	public static void main(String[] args) {
+		@Refinement("c == Color.Red || c == Color.Green")
+		Color c = null; // Refinement Error
+	}
+}