Golang/nameresolvers

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithygo/codegen/AddOperationShapes.java

@@ -100,7 +100,6 @@ public static Model execute(Model model, ShapeId serviceShapeId) {
     return modelBuilder.build();
   }
 
-
   private static StructureShape cloneOperationShape(
     ServiceShape service,
     ShapeId operationShapeId,

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithygo/localservice/nameresolver/Constants.java

@@ -0,0 +1,8 @@
+package software.amazon.polymorph.smithygo.localservice.nameresolver;
+
+public class Constants {
+
+  public static final String DOT = ".";
+  public static final String BLANK = "";
+  public static final String DAFNY_TYPES = "Types";
+}

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithygo/localservice/nameresolver/DafnyNameResolver.java

@@ -0,0 +1,199 @@
+package software.amazon.polymorph.smithygo.localservice.nameresolver;
+
+import static software.amazon.polymorph.smithygo.localservice.nameresolver.Constants.BLANK;
+import static software.amazon.polymorph.smithygo.localservice.nameresolver.Constants.DAFNY_TYPES;
+import static software.amazon.polymorph.smithygo.localservice.nameresolver.Constants.DOT;
+
+import software.amazon.polymorph.traits.LocalServiceTrait;
+import software.amazon.smithy.aws.traits.ServiceTrait;
+import software.amazon.smithy.codegen.core.Symbol;
+import software.amazon.smithy.model.shapes.ServiceShape;
+import software.amazon.smithy.model.shapes.Shape;
+import software.amazon.smithy.model.shapes.ShapeType;
+import software.amazon.smithy.model.shapes.UnionShape;
+import software.amazon.smithy.model.traits.EnumTrait;
+
+public class DafnyNameResolver {
+
+  public static String dafnyTypesNamespace(final Shape shape) {
+    // Delegate to the smithy-dafny-dafny logic. Ideally, this should be independent, but it is not today.
+    return software.amazon.polymorph.smithydafny.DafnyNameResolver.dafnyTypesModuleName(
+      shape.toShapeId().getNamespace()
+    );
+  }
+
+  public static String dafnyNamespace(final Shape shape) {
+    return software.amazon.polymorph.smithydafny.DafnyNameResolver.dafnyBaseModuleName(
+      shape.toShapeId().getNamespace()
+    );
+  }
+
+  public static String dafnyNamespace(final ServiceTrait serviceTrait) {
+    return software.amazon.polymorph.smithydafny.DafnyNameResolver.dafnyBaseModuleName(
+      serviceTrait.getSdkId()
+    );
+  }
+
+  public static String dafnyNamespace(
+    final LocalServiceTrait localServiceTrait
+  ) {
+    return software.amazon.polymorph.smithydafny.DafnyNameResolver.dafnyBaseModuleName(
+      localServiceTrait.getSdkId()
+    );
+  }
+
+  /**
+   * Returns the Dafny type for a given Shape.
+   *
+   * @param shape The Shape for which the Dafny type needs to be determined.
+   * @param symbol The Symbol representing the Shape.
+   * @return The Dafny type as a String.
+   */
+  public static String getDafnyType(final Shape shape, final Symbol symbol) {
+    ShapeType type = shape.getType();
+    if (shape.hasTrait(EnumTrait.class)) {
+      type = ShapeType.ENUM;
+    }
+    switch (type) {
+      case INTEGER, LONG, BOOLEAN:
+        return symbol.getName();
+      case MAP:
+        return "dafny.Map";
+      // TODO: Figure out the dafny type for TIMESTAMP
+      case DOUBLE, STRING, BLOB, LIST, TIMESTAMP:
+        return "dafny.Sequence";
+      // default catches a case where users may author their own classes that implement and extend resource (ExtendableTrait)
+      // ENUM, STRUCTURE, UNION can be removed but for posterity it looks great to see all the shapes being covered.
+      case ENUM, STRUCTURE, UNION:
+      default:
+        return DafnyNameResolver
+          .dafnyTypesNamespace(shape)
+          .concat(DOT)
+          .concat(symbol.getName());
+    }
+  }
+
+  public static String getDafnySubErrorType(
+    final Shape shape,
+    final Symbol symbol
+  ) {
+    return DafnyNameResolver
+      .getDafnyBaseErrorType(shape)
+      .concat("_")
+      .concat(symbol.getName());
+  }
+
+  public static String getDafnyBaseErrorType(final Shape shape) {
+    return DafnyNameResolver
+      .dafnyTypesNamespace(shape)
+      .concat(DOT)
+      .concat("Error");
+  }
+
+  public static String getDafnyCompanionType(
+    final Shape shape,
+    final Symbol symbol
+  ) {
+    return DafnyNameResolver
+      .dafnyTypesNamespace(shape)
+      .concat(DOT)
+      .concat("Companion_%s_".formatted(symbol.getName()));
+  }
+
+  public static String getDafnyErrorCompanion(final Shape shape) {
+    return DafnyNameResolver
+      .dafnyTypesNamespace(shape)
+      .concat(DOT)
+      .concat("Companion_Error_");
+  }
+
+  public static String getDafnyErrorCompanionCreate(
+    final Shape shape,
+    final Symbol symbol
+  ) {
+    return DafnyNameResolver
+      .getDafnyErrorCompanion(shape)
+      .concat(DOT)
+      .concat("Create_%s_".formatted(symbol.getName()));
+  }
+
+  public static String getDafnyCompanionStructType(
+    final Shape shape,
+    final Symbol symbol
+  ) {
+    return DafnyNameResolver
+      .dafnyTypesNamespace(shape)
+      .concat(DOT)
+      .concat("CompanionStruct_%s_".formatted(symbol.getName()));
+  }
+
+  public static String getDafnyCompanionTypeCreate(
+    final Shape shape,
+    final Symbol symbol
+  ) {
+    return DafnyNameResolver
+      .getDafnyCompanionType(shape, symbol)
+      .concat(DOT)
+      .concat("Create_%s_".formatted(symbol.getName()));
+  }
+
+  /**
+   * Returns the path to Create_ function for creating member shape within a union shape.
+   *
+   * @param unionShape The union shape containing the member shape.
+   * @param memberName The name of the member shape within the union shape.
+   */
+  public static String getDafnyCreateFuncForUnionMemberShape(
+    final UnionShape unionShape,
+    final String memberName
+  ) {
+    return "companion".concat(DOT)
+      .concat(
+        memberName.replace(unionShape.getId().getName() + "Member", "Create_")
+      )
+      .concat("_");
+  }
+
+  public static String getDafnyClient(final String sdkId) {
+    return sdkId.concat(DOT).concat(sdkId).concat("Client");
+  }
+
+  public static String getDafnyInterfaceClient(final Shape shape) {
+    return DafnyNameResolver
+      .dafnyTypesNamespace(shape)
+      .concat(DOT)
+      .concat("I")
+      .concat(shape.toShapeId().getName())
+      .concat("Client");
+  }
+
+  public static String getDafnyInterfaceClient(
+    final ServiceShape serviceShape,
+    final ServiceTrait awsSdkServiceTrait
+  ) {
+    return DafnyNameResolver
+      .dafnyTypesNamespace(serviceShape)
+      .concat(DOT)
+      .concat("I")
+      .concat(awsSdkServiceTrait.getSdkId())
+      .concat("Client");
+  }
+
+  public static String createDafnyClient(
+    final Shape shape,
+    final String sdkId
+  ) {
+    return sdkId.concat(".Companion_Default___").concat(DOT).concat(sdkId);
+  }
+
+  public static String getDafnyDependentErrorType(
+    final Shape shape,
+    final String sdkId
+  ) {
+    return DafnyNameResolver
+      .dafnyNamespace(shape)
+      .concat(".Companion_Default___")
+      .concat(DOT)
+      .concat(sdkId);
+  }
+}