chore: Change service constructor result type back (from trait to con…

…crete class) (#331) *Description of changes:* Reverts the part of #301 that changed the result type of constructing services from the concrete class type to the trait type, which turned out to be breaking in .NET as well as Dafny and was manually reverted in aws/aws-cryptographic-material-providers-library#257. See aws/aws-cryptographic-material-providers-library#267 for the upcoming proper fix to the MPL using this change. As it turns out this change wasn't necessary in the first place, and the `CreateSuccessOfClient/CreateFailureOfError` helpers are unchanged and still use the trait type, because these helpers are only needed for services that are created by target language code, i.e. SDK-style services and `--local-service-test` wrapped services. Regular local services are constructed in Dafny code so they never need the helper methods.
smithy-lang · Apr 9, 2024 · 66d3dbe · 66d3dbe
1 parent c2bff83
commit 66d3dbe
Show file tree

Hide file tree

Showing 26 changed files with 34 additions and 37 deletions.
diff --git a/TestModels/Aggregate/src/Index.dfy b/TestModels/Aggregate/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.aggregate.internaldafny"} SimpleAggregate refines Abstra
     }
 
     method SimpleAggregate(config: SimpleAggregateConfig)
-    returns (res: Result<ISimpleAggregateClient, Error>) {
+    returns (res: Result<SimpleAggregateClient, Error>) {
         var client := new SimpleAggregateClient(Operations.Config);
         return Success(client);
     }

diff --git a/TestModels/CodegenPatches/Model/SimpleCodegenpatchesTypes.dfy b/TestModels/CodegenPatches/Model/SimpleCodegenpatchesTypes.dfy
@@ -114,17 +114,17 @@ abstract module AbstractSimpleCodegenpatchesService
   import Operations : AbstractSimpleCodegenpatchesOperations
   function method DefaultCodegenPatchesConfig(): CodegenPatchesConfig
   method CodegenPatches(config: CodegenPatchesConfig := DefaultCodegenPatchesConfig())
-    returns (res: Result<ICodegenPatchesClient, Error>)
+    returns (res: Result<CodegenPatchesClient, Error>)
     ensures res.Success? ==>
               && fresh(res.value)
               && fresh(res.value.Modifies)
               && fresh(res.value.History)
               && res.value.ValidState()
 
-  // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals
+  // Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
   function method CreateSuccessOfClient(client: ICodegenPatchesClient): Result<ICodegenPatchesClient, Error> {
     Success(client)
-  } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals
+  }
   function method CreateFailureOfError(error: Error): Result<ICodegenPatchesClient, Error> {
     Failure(error)
   }
@@ -179,7 +179,7 @@ abstract module AbstractSimpleCodegenpatchesOperations {
   predicate ValidInternalConfig?(config: InternalConfig)
   function ModifiesInternalConfig(config: InternalConfig): set<object>
   predicate GetStringEnsuresPublicly(input: GetStringInput , output: Result<GetStringOutput, Error>)
-  // BEGIN MANUAL EDIT
+    // BEGIN MANUAL EDIT
   {
     true
   }

diff --git a/TestModels/CodegenPatches/src/Index.dfy b/TestModels/CodegenPatches/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.codegenpatches.internaldafny" } CodegenPatches refines A
   }
 
   method CodegenPatches(config: CodegenPatchesConfig)
-    returns (res: Result<ICodegenPatchesClient, Error>)
+    returns (res: Result<CodegenPatchesClient, Error>)
   {
     var client := new CodegenPatchesClient(Operations.Config);
     return Success(client);

diff --git a/TestModels/Constraints/src/Index.dfy b/TestModels/Constraints/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.constraints.internaldafny" } SimpleConstraints refines A
   }
 
   method SimpleConstraints(config: SimpleConstraintsConfig)
-    returns (res: Result<ISimpleConstraintsClient, Error>)
+    returns (res: Result<SimpleConstraintsClient, Error>)
   {
     var client := new SimpleConstraintsClient(Operations.Config);
     return Success(client);

diff --git a/TestModels/Constructor/src/Index.dfy b/TestModels/Constructor/src/Index.dfy
@@ -16,7 +16,7 @@ module {:extern "simple.constructor.internaldafny" } SimpleConstructor refines A
     }
 
     method SimpleConstructor(config: SimpleConstructorConfig)
-        returns (res: Result<ISimpleConstructorClient, Error>)
+        returns (res: Result<SimpleConstructorClient, Error>)
     {
         var configToAssign := Operations.Config(
             blobValue := config.blobValue.UnwrapOr([0]),

diff --git a/TestModels/Dependencies/src/Index.dfy b/TestModels/Dependencies/src/Index.dfy
@@ -25,7 +25,7 @@ module {:extern "simple.dependencies.internaldafny" } SimpleDependencies refines
   }
 
   method SimpleDependencies(config: SimpleDependenciesConfig)
-    returns (res: Result<ISimpleDependenciesClient, Error>)
+    returns (res: Result<SimpleDependenciesClient, Error>)
   {
     expect config.simpleResourcesConfig.Some?;
     expect config.specialString.Some?;

diff --git a/TestModels/Dependencies/src/SimpleDependenciesImpl.dfy b/TestModels/Dependencies/src/SimpleDependenciesImpl.dfy
@@ -85,7 +85,7 @@ module SimpleDependenciesImpl refines AbstractSimpleDependenciesOperations {
 
     var simpleResourcesConfig := config.simpleResourcesConfig;
 
-    var client: SimpleResourcesTypes.ISimpleResourcesClient :- expect SimpleResources.SimpleResources(
+    var client: SimpleResources.SimpleResourcesClient :- expect SimpleResources.SimpleResources(
       simpleResourcesConfig
     );
 

diff --git a/TestModels/Errors/src/Index.dfy b/TestModels/Errors/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.errors.internaldafny" } SimpleErrors refines AbstractSim
   }
 
   method SimpleErrors(config: SimpleErrorsConfig)
-    returns (res: Result<ISimpleErrorsClient, Error>)
+    returns (res: Result<SimpleErrorsClient, Error>)
   {
     var client := new SimpleErrorsClient(Operations.Config);
     return Success(client);

diff --git a/TestModels/Extendable/src/Index.dfy b/TestModels/Extendable/src/Index.dfy
@@ -20,7 +20,7 @@ module
     // so the implementation MUST have it.
     config: SimpleExtendableResourcesConfig
   ) returns (
-    res: Result<ISimpleExtendableResourcesClient, Error>
+    res: Result<SimpleExtendableResourcesClient, Error>
   )
   {
     var internalConfig := Operations.Config();

diff --git a/TestModels/Extern/src/Index.dfy b/TestModels/Extern/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.dafnyextern.internaldafny" } SimpleExtern refines Abstra
     }
 
     method SimpleExtern(config: SimpleExternConfig)
-        returns (res: Result<ISimpleExternClient, Error>)
+        returns (res: Result<SimpleExternClient, Error>)
     {
         var client := new SimpleExternClient(Operations.Config);
         return Success(client);

diff --git a/TestModels/LanguageSpecificLogic/src/Index.dfy b/TestModels/LanguageSpecificLogic/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "language.specific.logic.internaldafny"} LanguageSpecificLogic r
     }
 
     method LanguageSpecificLogic(config: LanguageSpecificLogicConfig)
-        returns (res: Result<ILanguageSpecificLogicClient, Error>)
+        returns (res: Result<LanguageSpecificLogicClient, Error>)
     {
         var client := new LanguageSpecificLogicClient(Operations.Config);
         return Success(client);

diff --git a/TestModels/LocalService/src/Index.dfy b/TestModels/LocalService/src/Index.dfy
@@ -18,7 +18,7 @@ module
   method SimpleLocalService(
     config: SimpleLocalServiceConfig
   ) returns (
-    res: Result<ISimpleLocalServiceClient, Error>
+    res: Result<SimpleLocalServiceClient, Error>
   )
   {
     var client := new SimpleLocalServiceClient(Operations.Config);

diff --git a/TestModels/MultipleModels/dafny/DependencyProject/src/Index.dfy b/TestModels/MultipleModels/dafny/DependencyProject/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.multiplemodels.dependencyproject.internaldafny" } Simple
     }
 
     method DependencyProject(config: DependencyProjectConfig)
-    returns (res: Result<IDependencyProjectClient, Error>) {
+    returns (res: Result<DependencyProjectClient, Error>) {
         var client := new DependencyProjectClient(Operations.Config);
         return Success(client);
     }

diff --git a/TestModels/MultipleModels/dafny/PrimaryProject/src/Index.dfy b/TestModels/MultipleModels/dafny/PrimaryProject/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.multiplemodels.primaryproject.internaldafny" } SimpleMul
     }
 
     method PrimaryProject(config: PrimaryProjectConfig)
-    returns (res: Result<IPrimaryProjectClient, Error>) {
+    returns (res: Result<PrimaryProjectClient, Error>) {
         var client := new PrimaryProjectClient(Operations.Config);
         return Success(client);
     }

diff --git a/TestModels/Refinement/src/Index.dfy b/TestModels/Refinement/src/Index.dfy
@@ -12,7 +12,7 @@ module {:extern "simple.refinement.internaldafny"} SimpleRefinement refines Abst
     method SimpleRefinement(
         config: SimpleRefinementConfig
     ) returns (
-        res: Result<ISimpleRefinementClient, Error>
+        res: Result<SimpleRefinementClient, Error>
     ) {
         var client := new SimpleRefinementClient(Operations.Config);
         return Success(client);

diff --git a/TestModels/Resource/src/Index.dfy b/TestModels/Resource/src/Index.dfy
@@ -20,7 +20,7 @@ module
   method SimpleResources(
     config: SimpleResourcesConfig
   ) returns (
-    res: Result<ISimpleResourcesClient, Error>
+    res: Result<SimpleResourcesClient, Error>
   )
   {
     var internalConfig: Operations.InternalConfig := Operations.Config(

diff --git a/TestModels/SimpleTypes/SimpleBlob/src/Index.dfy b/TestModels/SimpleTypes/SimpleBlob/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.types.blob.internaldafny" } SimpleBlob refines AbstractS
  }
 
  method SimpleBlob(config: SimpleBlobConfig)
- returns (res: Result<ISimpleTypesBlobClient, Error>) {
+ returns (res: Result<SimpleBlobClient, Error>) {
     var client := new SimpleBlobClient(Operations.Config);
     return Success(client);
  }

diff --git a/TestModels/SimpleTypes/SimpleBoolean/src/Index.dfy b/TestModels/SimpleTypes/SimpleBoolean/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.types.boolean.internaldafny" } SimpleBoolean refines Abs
  }
 
  method SimpleBoolean(config: SimpleBooleanConfig)
- returns (res: Result<ISimpleTypesBooleanClient, Error>) {
+ returns (res: Result<SimpleBooleanClient, Error>) {
     var client := new SimpleBooleanClient(Operations.Config);
     return Success(client);
  }

diff --git a/TestModels/SimpleTypes/SimpleDouble/src/Index.dfy b/TestModels/SimpleTypes/SimpleDouble/src/Index.dfy
@@ -12,7 +12,7 @@ module {:extern "simple.types.smithydouble.internaldafny" } SimpleDouble refines
  }
 
  method SimpleDouble(config: SimpleDoubleConfig)
- returns (res: Result<ISimpleTypesDoubleClient, Error>) {
+ returns (res: Result<SimpleDoubleClient, Error>) {
     var client := new SimpleDoubleClient(Operations.Config);
     return Success(client);
  }

diff --git a/TestModels/SimpleTypes/SimpleEnum/src/Index.dfy b/TestModels/SimpleTypes/SimpleEnum/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.types.smithyenum.internaldafny" } SimpleEnum refines Abs
  }
 
  method SimpleEnum(config: SimpleEnumConfig)
- returns (res: Result<ISimpleTypesEnumClient, Error>) {
+ returns (res: Result<SimpleEnumClient, Error>) {
     var client := new SimpleEnumClient(Operations.Config);
     return Success(client);
  }

diff --git a/TestModels/SimpleTypes/SimpleInteger/src/Index.dfy b/TestModels/SimpleTypes/SimpleInteger/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.types.integer.internaldafny" } SimpleInteger refines Abs
     }
 
     method SimpleInteger(config: SimpleIntegerConfig)
-    returns (res: Result<ISimpleTypesIntegerClient, Error>) {
+    returns (res: Result<SimpleIntegerClient, Error>) {
         var client := new SimpleIntegerClient(Operations.Config);
         return Success(client);
     }

diff --git a/TestModels/SimpleTypes/SimpleLong/src/Index.dfy b/TestModels/SimpleTypes/SimpleLong/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.types.smithylong.internaldafny" } SimpleLong refines Abs
  }
 
  method SimpleLong(config: SimpleLongConfig)
- returns (res: Result<ISimpleTypesLongClient, Error>) {
+ returns (res: Result<SimpleLongClient, Error>) {
     var client := new SimpleLongClient(Operations.Config);
     return Success(client);
  }

diff --git a/TestModels/SimpleTypes/SimpleString/src/Index.dfy b/TestModels/SimpleTypes/SimpleString/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.types.smithystring.internaldafny" } SimpleString refines
     }
 
     method SimpleString(config: SimpleStringConfig)
-    returns (res: Result<ISimpleTypesStringClient, Error>) {
+    returns (res: Result<SimpleStringClient, Error>) {
         var client := new SimpleStringClient(Operations.Config);
         return Success(client);
     }

diff --git a/TestModels/Union/src/Index.dfy b/TestModels/Union/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.union.internaldafny" } SimpleUnion refines AbstractSimpl
     }
 
     method SimpleUnion(config: SimpleUnionConfig)
-      returns (res: Result<ISimpleUnionClient, Error>)
+      returns (res: Result<SimpleUnionClient, Error>)
     {
         var client := new SimpleUnionClient(Operations.Config);
         return Success(client);

diff --git a/...hy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java b/...hy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java
@@ -1863,6 +1863,7 @@ private TokenTree modifiesClauseForPathToReference(
     public TokenTree generateAbstractLocalService(ServiceShape serviceShape)  {
         if (!serviceShape.hasTrait(LocalServiceTrait.class)) throw new IllegalStateException("MUST be an LocalService");
         final LocalServiceTrait localServiceTrait = serviceShape.expectTrait(LocalServiceTrait.class);
+        final String dafnyClientClass = "%sClient".formatted(localServiceTrait.getSdkId());
         final String dafnyClientTrait = nameResolver.traitForServiceClient(serviceShape);
 
         final String configTypeName = nameResolver.baseTypeForShape(localServiceTrait.getConfigId());
@@ -1888,7 +1889,8 @@ public TokenTree generateAbstractLocalService(ServiceShape serviceShape)  {
                 ),
             // Yes, Error is hard coded
             // this can work because we need to be able Errors from other modules...
-            "returns (res: Result<%s, Error>)\n".formatted(dafnyClientTrait)
+                "returns (res: Result<%s, Error>)\n"
+                        .formatted(dafnyClientClass)
         ).lineSeparated();
 
         // Add `requires` clauses
@@ -2057,21 +2059,16 @@ public TokenTree generateAbstractAwsServiceClass(ServiceShape serviceShape) {
      * See also TestModels/dafny-dependencies/StandardLibrary/src/WrappersInterop.dfy.
      */
     private static TokenTree generateResultOfClientHelperFunctions(String dafnyClientTrait) {
-        final TokenTree createSuccessOfClient = TokenTree
+        return TokenTree
           .of(
-            "// Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals",
+            "// Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals",
             "function method CreateSuccessOfClient(client: %s): Result<%s, Error> {".formatted(dafnyClientTrait, dafnyClientTrait),
             "  Success(client)",
-            "}"
-          ).lineSeparated();
-        final TokenTree createFailureOfError = TokenTree
-          .of(
-            "// Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals",
+            "}",
             "function method CreateFailureOfError(error: Error): Result<%s, Error> {".formatted(dafnyClientTrait),
             "  Failure(error)",
             "}"
           ).lineSeparated();
-        return TokenTree.of(createSuccessOfClient, createFailureOfError);
     }
 
     private static TokenTree generateLengthConstraint(final LengthTrait lengthTrait) {

diff --git a/...c/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java b/...c/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java
@@ -125,7 +125,7 @@ private MethodSpec serviceConstructor(BuilderSpecs builderSpecs) {
         method.addStatement(dafnyDeclareAndConvert(trait.getConfigId()));
         // Invoke client creation
         // i.e.: Result<AtomicPrimitivesClient, Error> result = software.amazon.cryptography.primitives.internaldafny.__default.AtomicPrimitives(dafnyValue);
-        TypeName success = subject.dafnyNameResolver.classNameForInterface(subject.serviceShape);
+        TypeName success = subject.dafnyNameResolver.classNameForConcreteServiceClient(subject.serviceShape);
         TypeName failure = subject.dafnyNameResolver.abstractClassForError();
         TypeName result = Dafny.asDafnyResult(success, failure);
         method.addStatement("$T $L = $T.$L($L)",