Break dependency, just define more ClassName constants instead (#213)

smithy-lang · Mar 31, 2023 · 50eaf17 · 50eaf17
1 parent 6bce46b
commit 50eaf17
Show file tree

Hide file tree

Showing 7 changed files with 31 additions and 36 deletions.
diff --git a/codegen/smithy-dafny-codegen-cli/build.gradle.kts b/codegen/smithy-dafny-codegen-cli/build.gradle.kts
@@ -49,7 +49,6 @@ dependencies {
     testImplementation("junit", "junit", "4.13.2")
     // For Smithy-Java
     implementation("software.amazon.awssdk:codegen:2.20.4")
-    implementation("dafny.lang:DafnyRuntime:3.10.0")
     implementation("com.squareup:javapoet:1.13.0")
 
     // Used for parsing-based tests

diff --git a/codegen/smithy-dafny-codegen/build.gradle.kts b/codegen/smithy-dafny-codegen/build.gradle.kts
@@ -34,7 +34,6 @@ dependencies {
 
     // For Smithy-Java
     implementation("software.amazon.awssdk:codegen:2.20.26")
-    implementation("dafny.lang:DafnyRuntime:3.10.0")
     implementation("com.squareup:javapoet:1.13.0")
 
     // Used for parsing-based tests

diff --git a/.../src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java b/.../src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java
@@ -20,8 +20,8 @@
 
 import javax.lang.model.element.Modifier;
 
-import dafny.DafnySequence;
 import software.amazon.polymorph.smithyjava.generator.ToDafny;
+import software.amazon.polymorph.smithyjava.nameresolver.Constants;
 import software.amazon.polymorph.utils.AwsSdkNameResolverHelpers;
 import software.amazon.polymorph.utils.DafnyNameResolverHelpers;
 import software.amazon.polymorph.utils.ModelUtils;
@@ -337,7 +337,7 @@ MethodSpec generateConvertOpaqueError() {
                 ParameterizedTypeName.get(
                         ClassName.get("Wrappers_Compile", "Option"),
                         ParameterizedTypeName.get(
-                                ClassName.get(DafnySequence.class),
+                                software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_SEQUENCE_CLASS_NAME,
                                 WildcardTypeName.subtypeOf(Character.class))
                 ),
                 "message"

diff --git a/.../src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java b/.../src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java
@@ -24,7 +24,6 @@
 
 import javax.lang.model.element.Modifier;
 
-import dafny.DafnySequence;
 import software.amazon.polymorph.smithyjava.generator.ToDafny;
 import software.amazon.polymorph.utils.AwsSdkNameResolverHelpers;
 import software.amazon.polymorph.utils.DafnyNameResolverHelpers;
@@ -512,7 +511,7 @@ MethodSpec generateConvertOpaqueError() {
                 ParameterizedTypeName.get(
                         ClassName.get("Wrappers_Compile", "Option"),
                         ParameterizedTypeName.get(
-                                ClassName.get(DafnySequence.class),
+                                software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_SEQUENCE_CLASS_NAME,
                                 WildcardTypeName.subtypeOf(Character.class))
                 ),
                 "message"

diff --git a/.../src/main/java/software/amazon/polymorph/smithyjava/generator/library/ToDafnyLibrary.java b/.../src/main/java/software/amazon/polymorph/smithyjava/generator/library/ToDafnyLibrary.java
@@ -17,9 +17,9 @@
 
 import javax.lang.model.element.Modifier;
 
-import dafny.DafnySequence;
 import software.amazon.polymorph.smithyjava.MethodReference;
 import software.amazon.polymorph.smithyjava.generator.ToDafny;
+import software.amazon.polymorph.smithyjava.nameresolver.Constants;
 import software.amazon.polymorph.traits.DafnyUtf8BytesTrait;
 import software.amazon.polymorph.traits.PositionalTrait;
 import software.amazon.polymorph.utils.ModelUtils;
@@ -152,7 +152,7 @@ MethodSpec collectionError() {
         ClassName dafnyError = subject.dafnyNameResolver.abstractClassForError();
         ClassName collectionError = CollectionOfErrors.nativeClassName(subject.nativeNameResolver.modelPackage);
         ParameterizedTypeName listArg = ParameterizedTypeName.get(
-                ClassName.get(DafnySequence.class),
+                software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_SEQUENCE_CLASS_NAME,
                 WildcardTypeName.subtypeOf(dafnyError)
         );
         CodeBlock genericCall = AGGREGATE_CONVERSION_METHOD_FROM_SHAPE_TYPE.get(ShapeType.LIST).asNormalReference();

diff --git a/...ny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java b/...ny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java
@@ -8,9 +8,13 @@
 import software.amazon.smithy.model.shapes.ShapeType;
 
 public class Constants {
-    public static ShapeId SMITHY_API_UNIT = ShapeId.fromParts("smithy.api", "Unit");
-    public static ClassName DAFNY_RESULT_CLASS_NAME = ClassName.get("Wrappers_Compile", "Result");
-    public static ClassName DAFNY_TUPLE0_CLASS_NAME = ClassName.get("dafny", "Tuple0");
-    public static Set<ShapeType> SHAPE_TYPES_LIST_SET = Set.of(ShapeType.LIST, ShapeType.SET);
-    public static Set<ShapeType> SHAPE_TYPES_LIST_SET_MAP = Set.of(ShapeType.LIST, ShapeType.SET, ShapeType.MAP);
+    public static final ShapeId SMITHY_API_UNIT = ShapeId.fromParts("smithy.api", "Unit");
+    public static final ClassName DAFNY_RESULT_CLASS_NAME = ClassName.get("Wrappers_Compile", "Result");
+    public static final ClassName DAFNY_TUPLE0_CLASS_NAME = ClassName.get("dafny", "Tuple0");
+    public static final ClassName DAFNY_TYPE_DESCRIPTOR_CLASS_NAME = ClassName.get("dafny", "TypeDescriptor");
+    public static final ClassName DAFNY_SEQUENCE_CLASS_NAME = ClassName.get("dafny", "DafnySequence");
+    public static final ClassName DAFNY_SET_CLASS_NAME = ClassName.get("dafny", "DafnySet");
+    public static final ClassName DAFNY_MAP_CLASS_NAME = ClassName.get("dafny", "DafnyMap");
+    public static final Set<ShapeType> SHAPE_TYPES_LIST_SET = Set.of(ShapeType.LIST, ShapeType.SET);
+    public static final Set<ShapeType> SHAPE_TYPES_LIST_SET_MAP = Set.of(ShapeType.LIST, ShapeType.SET, ShapeType.MAP);
 }
diff --git a/...-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java b/...-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java
@@ -16,12 +16,6 @@
 
 import javax.annotation.Nullable;
 
-import dafny.DafnyMap;
-import dafny.DafnySequence;
-import dafny.DafnySet;
-import dafny.Tuple0;
-import dafny.TypeDescriptor;
-
 import software.amazon.polymorph.smithydafny.DafnyNameResolver;
 import software.amazon.polymorph.smithyjava.MethodReference;
 import software.amazon.polymorph.smithyjava.generator.CodegenSubject;
@@ -56,16 +50,16 @@ public class Dafny extends NameResolver {
     protected static final Map<ShapeType, CodeBlock> TYPE_DESCRIPTOR_BY_SHAPE_TYPE;
     static {
         TYPE_DESCRIPTOR_BY_SHAPE_TYPE = Map.ofEntries(
-                Map.entry(ShapeType.STRING, CodeBlock.of("$T._typeDescriptor($T.CHAR)", DafnySequence.class, TypeDescriptor.class)),
+                Map.entry(ShapeType.STRING, CodeBlock.of("$T._typeDescriptor($T.CHAR)", Constants.DAFNY_SEQUENCE_CLASS_NAME, Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME)),
                 // Tony is not sure BLOB is correct...
-                Map.entry(ShapeType.BLOB, CodeBlock.of("$T._typeDescriptor($T.BYTE)", DafnySequence.class, TypeDescriptor.class)),
-                Map.entry(ShapeType.BOOLEAN, CodeBlock.of("$T.BOOLEAN", TypeDescriptor.class)),
-                Map.entry(ShapeType.BYTE, CodeBlock.of("$T.BYTE", TypeDescriptor.class)),
-                Map.entry(ShapeType.SHORT, CodeBlock.of("$T.SHORT", TypeDescriptor.class)),
-                Map.entry(ShapeType.INTEGER, CodeBlock.of("$T.INT", TypeDescriptor.class)),
-                Map.entry(ShapeType.LONG, CodeBlock.of("$T.LONG", TypeDescriptor.class)),
-                Map.entry(ShapeType.TIMESTAMP, CodeBlock.of("$T._typeDescriptor($T.CHAR)", DafnySequence.class, TypeDescriptor.class)),
-                Map.entry(ShapeType.BIG_INTEGER, CodeBlock.of("$T.BIG_INTEGER", TypeDescriptor.class))
+                Map.entry(ShapeType.BLOB, CodeBlock.of("$T._typeDescriptor($T.BYTE)", Constants.DAFNY_SEQUENCE_CLASS_NAME, Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME)),
+                Map.entry(ShapeType.BOOLEAN, CodeBlock.of("$T.BOOLEAN", Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME)),
+                Map.entry(ShapeType.BYTE, CodeBlock.of("$T.BYTE", Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME)),
+                Map.entry(ShapeType.SHORT, CodeBlock.of("$T.SHORT", Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME)),
+                Map.entry(ShapeType.INTEGER, CodeBlock.of("$T.INT", Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME)),
+                Map.entry(ShapeType.LONG, CodeBlock.of("$T.LONG", Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME)),
+                Map.entry(ShapeType.TIMESTAMP, CodeBlock.of("$T._typeDescriptor($T.CHAR)", Constants.DAFNY_SEQUENCE_CLASS_NAME, Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME)),
+                Map.entry(ShapeType.BIG_INTEGER, CodeBlock.of("$T.BIG_INTEGER", Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME))
         );
     }
 
@@ -182,7 +176,7 @@ public TypeName typeForShape(final ShapeId shapeId) {
 
     private static TypeName typeForBlob() {
         return ParameterizedTypeName.get(
-                ClassName.get(DafnySequence.class),
+                Constants.DAFNY_SEQUENCE_CLASS_NAME,
                 WildcardTypeName.subtypeOf(TypeName.BYTE.box()));
     }
 
@@ -202,15 +196,15 @@ public TypeName typeForAggregateWithWildcard(final ShapeId shapeId) {
         }
         return switch (shape.getType()) {
             case LIST -> ParameterizedTypeName.get(
-                    ClassName.get(DafnySequence.class),
+                    Constants.DAFNY_SEQUENCE_CLASS_NAME,
                     WildcardTypeName.subtypeOf(typeForShape(shape.asListShape().get().getMember().getTarget()))
             );
             case SET -> ParameterizedTypeName.get(
-                    ClassName.get(DafnySet.class),
+                    Constants.DAFNY_SET_CLASS_NAME,
                     WildcardTypeName.subtypeOf(typeForShape(shape.asSetShape().get().getMember().getTarget()))
             );
             case MAP -> ParameterizedTypeName.get(
-                    ClassName.get(DafnyMap.class),
+                    Constants.DAFNY_MAP_CLASS_NAME,
                     WildcardTypeName.subtypeOf(typeForShape(shape.asMapShape().get().getKey().getTarget())),
                     WildcardTypeName.subtypeOf(typeForShape(shape.asMapShape().get().getValue().getTarget()))
             );
@@ -241,11 +235,11 @@ public CodeBlock typeDescriptor(ShapeId shapeId) {
         if (shape.hasTrait(ReferenceTrait.class)) {
             // It is safe to use typeForShape here, as ReferenceTrait will always turn into a Resource or Service
             TypeName interfaceClassName = typeForShape(shapeId);
-            return  CodeBlock.of("$T.reference($T.class)", TypeDescriptor.class, interfaceClassName);
+            return  CodeBlock.of("$T.reference($T.class)", Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME, interfaceClassName);
         }
         if (shape.getId().equals(Constants.SMITHY_API_UNIT)) {
             return CodeBlock.of("$L()",
-                    new MethodReference(ClassName.get(Tuple0.class), "_typeDescriptor").asNormalReference());
+                    new MethodReference(Constants.DAFNY_TUPLE0_CLASS_NAME, "_typeDescriptor").asNormalReference());
         }
         if (shape.getType().getCategory().equals(ShapeType.Category.SIMPLE) && !shape.hasTrait(EnumTrait.class)) {
             @Nullable CodeBlock typeDescriptor =
@@ -305,7 +299,7 @@ TypeName typeForString(StringShape shape) {
 
     TypeName typeForCharacterSequence() {
         return ParameterizedTypeName.get(
-                ClassName.get(DafnySequence.class),
+                Constants.DAFNY_SEQUENCE_CLASS_NAME,
                 WildcardTypeName.subtypeOf(Character.class)
         );
     }
@@ -318,7 +312,7 @@ public TypeName classForStructure(StructureShape shape) {
             return typeForShape(shape.expectTrait(ReferenceTrait.class).getReferentId());
         }
         if (shape.getId().equals(Constants.SMITHY_API_UNIT)) {
-            return ClassName.get(Tuple0.class);
+            return Constants.DAFNY_TUPLE0_CLASS_NAME;
         }
         return classForNotErrorNotUnitShape(shape);
     }