fix dafny client

smithy-lang · Sep 25, 2024 · c23a6cf · c23a6cf
1 parent aaa0ddd
commit c23a6cf
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 10 deletions.
diff --git a/...tware/amazon/polymorph/smithygo/localservice/DafnyLocalServiceTypeConversionProtocol.java b/...tware/amazon/polymorph/smithygo/localservice/DafnyLocalServiceTypeConversionProtocol.java
@@ -21,6 +21,7 @@
 import software.amazon.smithy.model.shapes.StructureShape;
 import software.amazon.smithy.model.traits.ErrorTrait;
 import software.amazon.smithy.model.traits.UnitTypeTrait;
+import software.amazon.smithy.utils.CaseUtils;
 
 public class DafnyLocalServiceTypeConversionProtocol
   implements ProtocolGenerator {
@@ -968,9 +969,29 @@ func Error_ToDafny(err error)($L.Error) {
                   .getDependencies()
                 : new LinkedList<ShapeId>();
               if (dependencies != null) {
-                for (var dep : dependencies) {
+                Boolean wroteDepShape = false;
+                for (var dep : dependencies) {                 
                   var depShape = context.model().expectShape(dep);
-                  w.write(
+                  if (dep.getName().equals("TrentService") || dep.getName().equals("DynamoDB_20120810")) {
+                    // Generate Error Serialization only once
+                    if (wroteDepShape) {
+                      continue;
+                    }
+                    String depName = SmithyNameResolver.shapeNamespaceDafnyTranspiled(depShape);
+                    w.write(
+                      """
+                      case smithy.APIError:
+                        e := $L.Error_ToDafny(err)
+                        return $L.Create_$L_(e)
+                      """,
+                      SmithyNameResolver.shapeNamespace(depShape),
+                      DafnyNameResolver.getDafnyErrorCompanion(serviceShape),
+                      depName
+                    );
+                    wroteDepShape = true;
+                  }
+                  else {
+                    w.write(
                     """
                     case $L.$LBaseException:
                         return $L.Create_$L_($L.Error_ToDafny(err))
@@ -981,6 +1002,7 @@ func Error_ToDafny(err error)($L.Error) {
                     dep.getName(),
                     SmithyNameResolver.shapeNamespace(depShape)
                   );
+                  }
                 }
               }
             }),
@@ -1230,18 +1252,22 @@ func Error_FromDafny(err $L.Error)(error) {
                 var depService = context
                   .model()
                   .expectShape(dep, ServiceShape.class);
-                if (!depService.hasTrait(LocalServiceTrait.class)) {
-                  continue;
+                String shapeNamespace;
+                if (depService.hasTrait(LocalServiceTrait.class)) {
+                  shapeNamespace = depService.expectTrait(LocalServiceTrait.class).getSdkId();
+                }
+                else {
+                  shapeNamespace = SmithyNameResolver.shapeNamespaceDafnyTranspiled(depService);
                 }
                 w.write(
                   """
                   if err.Is_$L() {
                       return $L.Error_FromDafny(err.Dtor_$L())
                   }
                   """,
-                  depService.expectTrait(LocalServiceTrait.class).getSdkId(),
+                  shapeNamespace,
                   SmithyNameResolver.shapeNamespace(depService),
-                  depService.expectTrait(LocalServiceTrait.class).getSdkId()
+                  shapeNamespace
                 );
               }
             })

diff --git a/.../java/software/amazon/polymorph/smithygo/localservice/nameresolver/DafnyNameResolver.java b/.../java/software/amazon/polymorph/smithygo/localservice/nameresolver/DafnyNameResolver.java
@@ -145,8 +145,7 @@ public static String getDafnyCreateFuncForUnionMemberShape(
   }
 
   public static String getDafnyClient(final Shape shape, final String sdkId) {
-    return DafnyNameResolver
-      .dafnyNamespace(shape)
+    return shape.getId().getName()
       .concat(DOT)
       .concat(sdkId)
       .concat("Client");
@@ -177,8 +176,7 @@ public static String createDafnyClient(
     final Shape shape,
     final String sdkId
   ) {
-    return DafnyNameResolver
-      .dafnyNamespace(shape)
+    return shape.getId().getName()
       .concat(".Companion_Default___")
       .concat(DOT)
       .concat(sdkId);