feat: add type descriptors for data constructors in Java, when necessary

.github/workflows/pull.yml

@@ -5,36 +5,39 @@ on:
   pull_request:
 
 jobs:
+  pr-populate-dafny-versions:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Populate Dafny versions list
+      id: populate-dafny-versions-list
+      run: echo "dafny-versions-list=['4.1.0', '4.3.0']" >> $GITHUB_OUTPUT
+    outputs:
+      dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }}
+
   pr-ci-verification:
+    needs: pr-populate-dafny-versions
     strategy:
       fail-fast: false
       matrix:
-        dafny-version: [
-          4.1.0,
-          4.3.0
-        ]
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
     uses: ./.github/workflows/test_models_dafny_verification.yml
     with:
       dafny: ${{ matrix.dafny-version }}
   pr-ci-java:
+    needs: pr-populate-dafny-versions
     strategy:
       fail-fast: false
       matrix:
-        dafny-version: [
-          4.1.0,
-          4.3.0
-        ]
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
     uses: ./.github/workflows/test_models_java_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}
   pr-ci-net:
+    needs: pr-populate-dafny-versions
     strategy:
       fail-fast: false
       matrix:
-        dafny-version: [
-          4.1.0,
-          4.3.0
-        ]
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
     uses: ./.github/workflows/test_models_net_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}

.github/workflows/push.yml

@@ -7,36 +7,39 @@ on:
       - main-1.x    
 
 jobs:
+  pr-populate-dafny-versions:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Populate Dafny versions list
+      id: populate-dafny-versions-list
+      run: echo "dafny-versions-list=['4.1.0', '4.3.0']" >> $GITHUB_OUTPUT
+    outputs:
+      dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }}
+
   push-ci-verification:
+    needs: pr-populate-dafny-versions
     strategy:
       fail-fast: false
       matrix:
-        dafny-version: [
-          4.1.0,
-          4.3.0
-        ]
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
     uses: ./.github/workflows/test_models_dafny_verification.yml
     with:
       dafny: ${{ matrix.dafny-version }}
   push-ci-java:
+    needs: pr-populate-dafny-versions
     strategy:
       fail-fast: false
       matrix:
-        dafny-version: [
-          4.1.0,
-          4.3.0
-        ]
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
     uses: ./.github/workflows/test_models_java_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}
   push-ci-net:
+    needs: pr-populate-dafny-versions
     strategy:
       fail-fast: false
       matrix:
-        dafny-version: [
-          4.1.0,
-          4.3.0
-        ]
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
     uses: ./.github/workflows/test_models_net_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/TestServiceShim.java

@@ -3,7 +3,6 @@
 package software.amazon.polymorph.smithyjava.generator.library.shims;
 
 import com.squareup.javapoet.ClassName;
-import com.squareup.javapoet.CodeBlock;
 import com.squareup.javapoet.FieldSpec;
 import com.squareup.javapoet.JavaFile;
 import com.squareup.javapoet.MethodSpec;
@@ -19,12 +18,10 @@
 import software.amazon.polymorph.smithyjava.BuilderSpecs;
 import software.amazon.polymorph.smithyjava.generator.library.JavaLibrary;
 import software.amazon.polymorph.smithyjava.modeled.Operation;
-import software.amazon.polymorph.smithyjava.nameresolver.Dafny;
 import software.amazon.smithy.model.shapes.ServiceShape;
 
 import static javax.lang.model.element.Modifier.PROTECTED;
 import static javax.lang.model.element.Modifier.PUBLIC;
-import static javax.lang.model.element.Modifier.STATIC;
 
 public class TestServiceShim extends ServiceShim {
     /** The Service Shape this Shim Tests. */

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java

@@ -100,6 +100,9 @@ public static String datatypeConstructorCreate(String name, boolean isRecordType
     //  Dafnys greater than or equal to this will need Type Descriptors for constructing datatypes  
     private static final DafnyVersion NEEDS_TYPE_DESCRIPTORS_WHEN_CONSTRUCTING_DATATYPES = new DafnyVersion(4, 2, 0);
 
+    /**
+     * @return Whether the given Dafny version requires type descriptor values when instantiating datatype constructors.
+     */
     public static boolean datatypeConstructorsNeedTypeDescriptors(DafnyVersion dafnyVersion) {
         return dafnyVersion.compareTo(NEEDS_TYPE_DESCRIPTORS_WHEN_CONSTRUCTING_DATATYPES) >= 0;
     }
@@ -108,6 +111,11 @@ private boolean datatypeConstructorsNeedTypeDescriptors() {
         return datatypeConstructorsNeedTypeDescriptors(dafnyVersion);
     }
 
+    /**
+     * Code to create an instance of the None constructor of Wrappers.Option<T>.
+     * @param typeDescriptor the code to create a TypeDescriptor for the type T,
+     *                       which is needed if datatypeConstructorsNeedTypeDescriptors()
+     */
     public CodeBlock createNone(CodeBlock typeDescriptor) {
         if (datatypeConstructorsNeedTypeDescriptors()) {
             return CodeBlock.of(
@@ -121,6 +129,11 @@ public CodeBlock createNone(CodeBlock typeDescriptor) {
         }
     }
 
+    /**
+     * Code to create an instance of the Some(value: T) constructor of Wrappers.Option<T>.
+     * @param typeDescriptor the code to create a TypeDescriptor for the type T,
+     *                       which is needed if datatypeConstructorsNeedTypeDescriptors()
+     */
     public CodeBlock createSome(CodeBlock typeDescriptor, CodeBlock value) {
         if (datatypeConstructorsNeedTypeDescriptors()) {
             return CodeBlock.of(
@@ -136,6 +149,11 @@ public CodeBlock createSome(CodeBlock typeDescriptor, CodeBlock value) {
         }
     }
 
+    /**
+     * Code to create an instance of the Success(value: T) constructor of Wrappers.Result<T, Error>.
+     * @param valueTypeDescriptor the code to create a TypeDescriptor for the type T,
+     *                       which is needed if datatypeConstructorsNeedTypeDescriptors()
+     */
     public CodeBlock createSuccess(CodeBlock valueTypeDescriptor, CodeBlock value) {
         if (datatypeConstructorsNeedTypeDescriptors()) {
             return CodeBlock.of(
@@ -151,12 +169,17 @@ public CodeBlock createSuccess(CodeBlock valueTypeDescriptor, CodeBlock value) {
         }
     }
 
-    public CodeBlock createFailure(CodeBlock typeDescriptor, CodeBlock error) {
+    /**
+     * Code to create an instance of the Failure(error: Error) constructor of Wrappers.Result<T, Error>.
+     * @param valueTypeDescriptor the code to create a TypeDescriptor for the type T,
+     *                            which is needed if datatypeConstructorsNeedTypeDescriptors()
+     */
+    public CodeBlock createFailure(CodeBlock valueTypeDescriptor, CodeBlock error) {
         if (datatypeConstructorsNeedTypeDescriptors()) {
             return CodeBlock.of(
                     "$T.create_Failure($L, Error._typeDescriptor(), $L)",
                     Constants.DAFNY_RESULT_CLASS_NAME,
-                    typeDescriptor,
+                    valueTypeDescriptor,
                     error);
         } else {
             return CodeBlock.of(