fix: Golang/union naming fix (#705)

* fix: Generate Wrappers for each resource * fix: Extendable extern * fix: ToDafnyNaming --------- Co-authored-by: Shubham Chaturvedi <scchatur@amazon.com>
smithy-lang · Nov 8, 2024 · aef7b27 · aef7b27
1 parent 3d2e47e
commit aef7b27
Show file tree

Hide file tree

Showing 6 changed files with 48 additions and 45 deletions.
diff --git a/TestModels/Union/runtimes/go/ImplementationFromDafny-go/go.mod b/TestModels/Union/runtimes/go/ImplementationFromDafny-go/go.mod
@@ -4,7 +4,7 @@ go 1.23.0
 
 require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
 
-require github.com/dafny-lang/DafnyRuntimeGo v0.0.0
+require github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
 
 //TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381
 replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/

diff --git a/TestModels/aws-sdks/ddbv2/runtimes/go/ImplementationFromDafny-go/go.mod b/TestModels/aws-sdks/ddbv2/runtimes/go/ImplementationFromDafny-go/go.mod
@@ -5,17 +5,25 @@ go 1.23.0
 replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/
 
 require (
+	github.com/aws/aws-sdk-go-v2/config v1.28.3
 	github.com/aws/aws-sdk-go-v2/service/dynamodb v1.34.9
 	github.com/aws/smithy-go v1.22.0
 	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
 	github.com/dafny-lang/DafnyStandardLibGo v0.0.0-00010101000000-000000000000
 )
 
 require (
-	github.com/aws/aws-sdk-go-v2 v1.30.5 // indirect
-	github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.17 // indirect
-	github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.17 // indirect
-	github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.4 // indirect
+	github.com/aws/aws-sdk-go-v2 v1.32.4 // indirect
+	github.com/aws/aws-sdk-go-v2/credentials v1.17.44 // indirect
+	github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.19 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.23 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.23 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.12.0 // indirect
 	github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.18 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.4 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sso v1.24.5 // indirect
+	github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.4 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sts v1.32.4 // indirect
 	github.com/jmespath/go-jmespath v0.4.0 // indirect
 )
diff --git a/TestModels/aws-sdks/ddbv2/runtimes/go/TestsFromDafny-go/go.mod b/TestModels/aws-sdks/ddbv2/runtimes/go/TestsFromDafny-go/go.mod
@@ -15,18 +15,18 @@ require (
 )
 
 require (
-	github.com/aws/aws-sdk-go-v2 v1.32.2 // indirect
-	github.com/aws/aws-sdk-go-v2/config v1.28.0 // indirect
-	github.com/aws/aws-sdk-go-v2/credentials v1.17.41 // indirect
-	github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.17 // indirect
-	github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.21 // indirect
-	github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.21 // indirect
+	github.com/aws/aws-sdk-go-v2 v1.32.4 // indirect
+	github.com/aws/aws-sdk-go-v2/config v1.28.3 // indirect
+	github.com/aws/aws-sdk-go-v2/credentials v1.17.44 // indirect
+	github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.19 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.23 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.23 // indirect
 	github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect
 	github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.12.0 // indirect
 	github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.18 // indirect
-	github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.2 // indirect
-	github.com/aws/aws-sdk-go-v2/service/sso v1.24.2 // indirect
-	github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.2 // indirect
-	github.com/aws/aws-sdk-go-v2/service/sts v1.32.2 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.4 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sso v1.24.5 // indirect
+	github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.4 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sts v1.32.4 // indirect
 	github.com/jmespath/go-jmespath v0.4.0 // indirect
 )
diff --git a/...ava/software/amazon/polymorph/smithygo/awssdk/shapevisitor/AwsSdkToDafnyShapeVisitor.java b/...ava/software/amazon/polymorph/smithygo/awssdk/shapevisitor/AwsSdkToDafnyShapeVisitor.java
@@ -561,11 +561,6 @@ public String unionShape(final UnionShape shape) {
       .asServiceShape()
       .get();
 
-    final var internalDafnyType = DafnyNameResolver.getDafnyType(
-      shape,
-      context.symbolProvider().toSymbol(shape)
-    );
-
     var returnType = DafnyNameResolver.getDafnyType(
       shape,
       context.symbolProvider().toSymbol(shape)
@@ -583,7 +578,6 @@ public String unionShape(final UnionShape shape) {
 
     final var eachMemberInUnion = new StringBuilder();
     for (final var member : shape.getAllMembers().values()) {
-      final var memberName = context.symbolProvider().toMemberName(member);
       final var targetShape = context.model().expectShape(member.getTarget());
       final var baseType = DafnyNameResolver.getDafnyType(
         targetShape,
@@ -603,7 +597,6 @@ public String unionShape(final UnionShape shape) {
       eachMemberInUnion.append(
         """
         case *%s.%s:
-            var companion = %s
             var inputToConversion = %s
             return %s
         """.formatted(
@@ -612,10 +605,6 @@ public String unionShape(final UnionShape shape) {
               true
             ),
             context.symbolProvider().toMemberName(member),
-            internalDafnyType.replace(
-              shape.getId().getName(),
-              "CompanionStruct_".concat(shape.getId().getName()).concat("_{}")
-            ),
             ShapeVisitorHelper.toDafnyShapeVisitorWriter(
               member,
               context,
@@ -628,7 +617,7 @@ public String unionShape(final UnionShape shape) {
             someWrapIfRequired.formatted(
               DafnyNameResolver.getDafnyCreateFuncForUnionMemberShape(
                 shape,
-                memberName
+                member.getMemberName()
               ),
               "inputToConversion.UnwrapOr(nil)%s".formatted(
                   !baseType.isEmpty() ? ".(".concat(baseType).concat(")") : ""

diff --git a/.../java/software/amazon/polymorph/smithygo/localservice/nameresolver/DafnyNameResolver.java b/.../java/software/amazon/polymorph/smithygo/localservice/nameresolver/DafnyNameResolver.java
@@ -1,7 +1,5 @@
 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;
@@ -129,6 +127,16 @@ public static String getDafnyCompanionStructType(
       );
   }
 
+  public static String getDafnyCompanionStructType(
+    final Shape shape,
+    final String memberName
+  ) {
+    return DafnyNameResolver
+      .dafnyTypesNamespace(shape)
+      .concat(DOT)
+      .concat("CompanionStruct_%s_".formatted(dafnyCompilesExtra_(memberName)));
+  }
+
   public static String getDafnyCompanionTypeCreate(
     final Shape shape,
     final Symbol symbol
@@ -149,11 +157,10 @@ public static String getDafnyCreateFuncForUnionMemberShape(
     final UnionShape unionShape,
     final String memberName
   ) {
-    return "companion".concat(DOT)
-      .concat(
-        memberName.replace(unionShape.getId().getName() + "Member", "Create_")
-      )
-      .concat("_");
+    return DafnyNameResolver
+      .getDafnyUnionBaseStructType(unionShape, unionShape.getId().getName())
+      .concat(DOT)
+      .concat("Create_%s_".formatted(dafnyCompilesExtra_(memberName)));
   }
 
   public static String getDafnyClient(final String sdkId) {
@@ -203,6 +210,15 @@ public static String getDafnyDependentErrorType(
       .concat(sdkId);
   }
 
+  public static String getDafnyUnionBaseStructType(
+    final Shape shape,
+    final String memberName
+  ) {
+    return DafnyNameResolver
+      .getDafnyCompanionStructType(shape, memberName)
+      .concat("{}");
+  }
+
   private static String dafnyCompilesExtra_(final String name) {
     return name.replace("_", "__");
   }

diff --git a/...ftware/amazon/polymorph/smithygo/localservice/shapevisitor/SmithyToDafnyShapeVisitor.java b/...ftware/amazon/polymorph/smithygo/localservice/shapevisitor/SmithyToDafnyShapeVisitor.java
@@ -660,10 +660,6 @@ public String doubleShape(final DoubleShape shape) {
 
   @Override
   public String unionShape(final UnionShape shape) {
-    final String internalDafnyType = DafnyNameResolver.getDafnyType(
-      shape,
-      context.symbolProvider().toSymbol(shape)
-    );
     String someWrapIfRequired = "%s(%s)";
     String returnType = DafnyNameResolver.getDafnyType(
       shape,
@@ -680,7 +676,6 @@ public String unionShape(final UnionShape shape) {
           switch %s.(type) {""".formatted(returnType, dataSource);
     final StringBuilder eachMemberInUnion = new StringBuilder();
     for (final var member : shape.getAllMembers().values()) {
-      final String memberName = context.symbolProvider().toMemberName(member);
       final Shape targetShape = context.model().expectShape(member.getTarget());
       final var refShape = targetShape.hasTrait(ReferenceTrait.class)
         ? targetShape.expectTrait(ReferenceTrait.class).getReferentId()
@@ -701,16 +696,11 @@ public String unionShape(final UnionShape shape) {
       eachMemberInUnion.append(
         """
         case *%s.%s:
-            var companion = %s
             var inputToConversion = %s
             return %s
             """.formatted(
             SmithyNameResolver.smithyTypesNamespace(shape),
             context.symbolProvider().toMemberName(member),
-            internalDafnyType.replace(
-              shape.getId().getName(),
-              "CompanionStruct_".concat(shape.getId().getName()).concat("_{}")
-            ),
             ShapeVisitorHelper.toDafnyShapeVisitorWriter(
               member,
               context,
@@ -728,7 +718,7 @@ public String unionShape(final UnionShape shape) {
             someWrapIfRequired.formatted(
               DafnyNameResolver.getDafnyCreateFuncForUnionMemberShape(
                 shape,
-                memberName
+                member.getMemberName()
               ),
               "inputToConversion.UnwrapOr(nil).(%s)".formatted(baseType)
             )