Additional units for unit checker; fixes #4116

typetools · May 5, 2021 · b542f2d · b542f2d
1 parent 2ab8484
commit b542f2d
Show file tree

Hide file tree

Showing 18 changed files with 602 additions and 4 deletions.
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/units/qual/Force.java b/checker-qual/src/main/java/org/checkerframework/checker/units/qual/Force.java
@@ -0,0 +1,19 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Units of force.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(UnknownUnits.class)
+public @interface Force {}
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/units/qual/N.java b/checker-qual/src/main/java/org/checkerframework/checker/units/qual/N.java
@@ -0,0 +1,22 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Newton.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(Force.class)
+@SuppressWarnings("checkstyle:typename")
+public @interface N {
+  Prefix value() default Prefix.one;
+}
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/units/qual/Volume.java b/checker-qual/src/main/java/org/checkerframework/checker/units/qual/Volume.java
@@ -0,0 +1,19 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Units of volume.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(UnknownUnits.class)
+public @interface Volume {}
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/units/qual/kN.java b/checker-qual/src/main/java/org/checkerframework/checker/units/qual/kN.java
@@ -0,0 +1,21 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Kilonewton.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(Force.class)
+@UnitsMultiple(quantity = N.class, prefix = Prefix.kilo)
+@SuppressWarnings("checkstyle:typename")
+public @interface kN {}
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/units/qual/km3.java b/checker-qual/src/main/java/org/checkerframework/checker/units/qual/km3.java
@@ -0,0 +1,20 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Cubic kilometer.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(Volume.class)
+@SuppressWarnings("checkstyle:typename")
+public @interface km3 {}
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/units/qual/m3.java b/checker-qual/src/main/java/org/checkerframework/checker/units/qual/m3.java
@@ -0,0 +1,20 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Cubic meter.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(Volume.class)
+@SuppressWarnings("checkstyle:typename")
+public @interface m3 {}
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/units/qual/mm3.java b/checker-qual/src/main/java/org/checkerframework/checker/units/qual/mm3.java
@@ -0,0 +1,20 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Cubic millimeter.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(Volume.class)
+@SuppressWarnings("checkstyle:typename")
+public @interface mm3 {}
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/units/qual/t.java b/checker-qual/src/main/java/org/checkerframework/checker/units/qual/t.java
@@ -0,0 +1,22 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Metric ton.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(Mass.class)
+// TODO: support arbitrary factors?
+// @UnitsMultiple(quantity=kg.class, factor=1000)
+@SuppressWarnings("checkstyle:typename")
+public @interface t {}
diff --git a/checker-util/src/main/java/org/checkerframework/checker/units/util/UnitsTools.java b/checker-util/src/main/java/org/checkerframework/checker/units/util/UnitsTools.java
@@ -3,24 +3,30 @@
 import org.checkerframework.checker.units.qual.A;
 import org.checkerframework.checker.units.qual.C;
 import org.checkerframework.checker.units.qual.K;
+import org.checkerframework.checker.units.qual.N;
 import org.checkerframework.checker.units.qual.cd;
 import org.checkerframework.checker.units.qual.degrees;
 import org.checkerframework.checker.units.qual.g;
 import org.checkerframework.checker.units.qual.h;
+import org.checkerframework.checker.units.qual.kN;
 import org.checkerframework.checker.units.qual.kg;
 import org.checkerframework.checker.units.qual.km;
 import org.checkerframework.checker.units.qual.km2;
+import org.checkerframework.checker.units.qual.km3;
 import org.checkerframework.checker.units.qual.kmPERh;
 import org.checkerframework.checker.units.qual.m;
 import org.checkerframework.checker.units.qual.m2;
+import org.checkerframework.checker.units.qual.m3;
 import org.checkerframework.checker.units.qual.mPERs;
 import org.checkerframework.checker.units.qual.mPERs2;
 import org.checkerframework.checker.units.qual.min;
 import org.checkerframework.checker.units.qual.mm;
 import org.checkerframework.checker.units.qual.mm2;
+import org.checkerframework.checker.units.qual.mm3;
 import org.checkerframework.checker.units.qual.mol;
 import org.checkerframework.checker.units.qual.radians;
 import org.checkerframework.checker.units.qual.s;
+import org.checkerframework.checker.units.qual.t;
 import org.checkerframework.framework.qual.AnnotatedFor;
 
 // TODO: add fromTo methods for all useful unit combinations.
@@ -49,6 +55,11 @@ public class UnitsTools {
   public static final @m2 int m2 = 1;
   public static final @km2 int km2 = 1;
 
+  // Volume
+  public static final @mm3 int mm3 = 1;
+  public static final @m3 int m3 = 1;
+  public static final @km3 int km3 = 1;
+
   // Current
   public static final @A int A = 1;
 
@@ -79,6 +90,7 @@ public class UnitsTools {
   // Mass
   public static final @g int g = 1;
   public static final @kg int kg = 1;
+  public static final @t int t = 1;
 
   public static @kg int fromGramToKiloGram(@g int g) {
     return g / 1000;
@@ -88,6 +100,26 @@ public class UnitsTools {
     return kg * 1000;
   }
 
+  public static @t int fromKiloGramToMetricTon(@kg int kg) {
+    return kg / 1000;
+  }
+
+  public static @kg int fromMetricTonToKiloGram(@t int t) {
+    return t * 1000;
+  }
+
+  // Force
+  public static final @N int N = 1;
+  public static final @kN int kN = 1;
+
+  public static @kN int fromNewtonToKiloNewton(@N int N) {
+    return N / 1000;
+  }
+
+  public static @N int fromKiloNewtonToNewton(@kN int kN) {
+    return kN * 1000;
+  }
+
   // Speed
   public static final @mPERs int mPERs = 1;
   public static final @kmPERh int kmPERh = 1;

diff --git a/checker/src/main/java/org/checkerframework/checker/units/UnitsRelationsDefault.java b/checker/src/main/java/org/checkerframework/checker/units/UnitsRelationsDefault.java
@@ -4,22 +4,39 @@
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.util.Elements;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.units.qual.N;
 import org.checkerframework.checker.units.qual.Prefix;
+import org.checkerframework.checker.units.qual.g;
 import org.checkerframework.checker.units.qual.h;
+import org.checkerframework.checker.units.qual.kg;
 import org.checkerframework.checker.units.qual.km2;
+import org.checkerframework.checker.units.qual.km3;
 import org.checkerframework.checker.units.qual.kmPERh;
 import org.checkerframework.checker.units.qual.m;
 import org.checkerframework.checker.units.qual.m2;
+import org.checkerframework.checker.units.qual.m3;
 import org.checkerframework.checker.units.qual.mPERs;
 import org.checkerframework.checker.units.qual.mPERs2;
 import org.checkerframework.checker.units.qual.mm2;
+import org.checkerframework.checker.units.qual.mm3;
 import org.checkerframework.checker.units.qual.s;
+import org.checkerframework.checker.units.qual.t;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 
 /** Default relations between SI units. */
 public class UnitsRelationsDefault implements UnitsRelations {
-  /** SI units. */
-  protected AnnotationMirror m, km, mm, m2, km2, mm2, s, h, mPERs, kmPERh, mPERs2;
+  /** SI base units. */
+  protected AnnotationMirror m, km, mm, s, g, kg;
+
+  /** Derived SI units without special names */
+  protected AnnotationMirror m2, km2, mm2, m3, km3, mm3, mPERs, mPERs2;
+
+  /** Derived SI units with special names */
+  protected AnnotationMirror N, kN;
+
+  /** Non-SI units */
+  protected AnnotationMirror h, kmPERh, t;
+
   /** The Element Utilities from the Units Checker's processing environment. */
   protected Elements elements;
 
@@ -39,6 +56,10 @@ public UnitsRelations init(ProcessingEnvironment env) {
     km2 = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, km2.class);
     mm2 = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, mm2.class);
 
+    m3 = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, m3.class);
+    km3 = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, km3.class);
+    mm3 = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, mm3.class);
+
     s = UnitsRelationsTools.buildAnnoMirrorWithDefaultPrefix(env, s.class);
     h = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, h.class);
 
@@ -47,6 +68,12 @@ public UnitsRelations init(ProcessingEnvironment env) {
 
     mPERs2 = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, mPERs2.class);
 
+    g = UnitsRelationsTools.buildAnnoMirrorWithDefaultPrefix(env, g.class);
+    kg = UnitsRelationsTools.buildAnnoMirrorWithSpecificPrefix(env, g.class, Prefix.kilo);
+    t = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, t.class);
+    N = UnitsRelationsTools.buildAnnoMirrorWithDefaultPrefix(env, N.class);
+    kN = UnitsRelationsTools.buildAnnoMirrorWithSpecificPrefix(env, N.class, Prefix.kilo);
+
     return this;
   }
 
@@ -83,6 +110,12 @@ public UnitsRelations init(ProcessingEnvironment env) {
       } else {
         return null;
       }
+    } else if (havePairOfUnitsIgnoringOrder(lht, m, rht, m2)) {
+      return m3;
+    } else if (havePairOfUnitsIgnoringOrder(lht, km, rht, km2)) {
+      return km3;
+    } else if (havePairOfUnitsIgnoringOrder(lht, mm, rht, mm2)) {
+      return mm3;
     } else if (havePairOfUnitsIgnoringOrder(lht, s, rht, mPERs)) {
       // s * mPERs or mPERs * s => m
       return m;
@@ -92,6 +125,12 @@ public UnitsRelations init(ProcessingEnvironment env) {
     } else if (havePairOfUnitsIgnoringOrder(lht, h, rht, kmPERh)) {
       // h * kmPERh or kmPERh * h => km
       return km;
+    } else if (havePairOfUnitsIgnoringOrder(lht, kg, rht, mPERs2)) {
+      // kg * mPERs2 or mPERs2 * kg = N
+      return N;
+    } else if (havePairOfUnitsIgnoringOrder(lht, t, rht, mPERs2)) {
+      // t * mPERs2 or mPERs2 * t = kN
+      return kN;
     } else {
       return null;
     }
@@ -118,6 +157,24 @@ public UnitsRelations init(ProcessingEnvironment env) {
     } else if (havePairOfUnits(lht, mm2, rht, mm)) {
       // mm2 / mm => mm
       return mm;
+    } else if (havePairOfUnits(lht, m3, rht, m)) {
+      // m3 / m => m2
+      return m2;
+    } else if (havePairOfUnits(lht, km3, rht, km)) {
+      // km3 / km => km2
+      return km2;
+    } else if (havePairOfUnits(lht, mm3, rht, mm)) {
+      // mm3 / mm => mm2
+      return mm2;
+    } else if (havePairOfUnits(lht, m3, rht, m2)) {
+      // m3 / m2 => m
+      return m;
+    } else if (havePairOfUnits(lht, km3, rht, km2)) {
+      // km3 / km2 => km
+      return km;
+    } else if (havePairOfUnits(lht, mm3, rht, mm2)) {
+      // mm3 / mm2 => mm
+      return mm;
     } else if (havePairOfUnits(lht, m, rht, mPERs)) {
       // m / mPERs => s
       return s;
@@ -130,6 +187,24 @@ public UnitsRelations init(ProcessingEnvironment env) {
     } else if (havePairOfUnits(lht, mPERs, rht, mPERs2)) {
       // mPERs / mPERs2 => s  (velocity / acceleration == time)
       return s;
+    } else if (UnitsRelationsTools.hasSpecificUnit(lht, N)) {
+      if (UnitsRelationsTools.hasSpecificUnit(rht, kg)) {
+        // N / kg => mPERs2
+        return mPERs2;
+      } else if (UnitsRelationsTools.hasSpecificUnit(rht, mPERs2)) {
+        // N / mPERs2 => kg
+        return kg;
+      }
+      return null;
+    } else if (UnitsRelationsTools.hasSpecificUnit(lht, kN)) {
+      if (UnitsRelationsTools.hasSpecificUnit(rht, t)) {
+        // kN / t => mPERs2
+        return mPERs2;
+      } else if (UnitsRelationsTools.hasSpecificUnit(rht, mPERs2)) {
+        // kN / mPERs2 => t
+        return t;
+      }
+      return null;
     } else {
       return null;
     }