docs(dafny-java-conversion): JavaDocs for ToNative Blob & Double #252

texastony · 2023-05-08T23:22:06Z

Issue #, if available: [Polymorph][Java] Clean up Dafny-Java-Conversion Javadocs

Description of changes:

Java Docs for ToNative's Blob & Double methods.

State

@robin-aws wants to glance at the methods before I write the rest of the docs.
Tony has taken feedback from ^ and applied it, and written all the java docs.
@robin-aws may get around to editing the README
Anyone can update Smithy-Dafny to use the new package name
software.amazon.dafny.conversion -> software.amazon.smithy.dafny.conversion
Deploy the CFN changes
Merge this PR
Push to Code Artifact
Update Smithy-Dafny's consumers build.gradle.kts
Regenerate Smithy-Dafny's consumers Java
(or sed software.amazon.dafny.conversion -> software.amazon.smithy.dafny.conversion)

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

robin-aws · 2023-05-09T18:26:38Z

Here are my top-level suggestions on this:

Rather than using "idiomatic" too much in the documentation, I'd continue focusing on this conversion concept being driven from Smithy concepts. On the one hand you have how a Smithy shape is naturally represented in Java, and on the other you have how Dafny's natural representation is materialized for the Java runtime. So rather than saying "the Dafny-Java type" perhaps we could say "the Dafny runtime type" (where the fact that we're talking about the Java runtime is implicit most of the time).
I'd name this library such that it is clearly under the Smithy umbrella, making it even clearly this is a Smithy code generation runtime library, rather than a generic Dafny-Java conversion library (for now). Perhaps software.amazon.smithy.dafny:smithy-dafny-conversion?
I'm not going to nitpick about the class and method names, given they are all only intended to be referenced by Smithy-generated code, and I don't think it's worth the trouble to change them.

ToNative.Simple

robin-aws

Very nice work on the javadoc - I don't expect anyone to reference the methods directly, but you're adding a lot of useful design/implementation detail that future us will thank you for. :)

The nitpicking to the actual docstrings are stronger than the code suggestions I made because I happened to see them - I know the latter are not intended to be in scope for this PR so happy to address those later.

.github/workflows/smithy-dafny-conversion.yml

cfn/CA.yaml

smithy-dafny-conversion/src/main/java/software/amazon/smithy/dafny/conversion/ToDafny.java

robin-aws · 2023-05-15T20:30:41Z

smithy-dafny-conversion/src/main/java/software/amazon/smithy/dafny/conversion/ToDafny.java

+
+        /**
+         * @param aString The Java type for a String is {@link String}.
+         * @return The Dafny Runtime type for a String is A {@link DafnySequence} of {@link Character}s.


I'd mention "when --unicode-char is false".

I did not know this.
Can this be a more generic comment?
i.e:

Suggested change

* @return The Dafny Runtime type for a String is A {@link DafnySequence} of {@link Character}s.

* @return The Dafny Runtime type for a String can be a {@link DafnySequence} of {@link Character}s,

* if Dafny is configured to NOT use Unicode characters.

I think "IS A" is more accurate, since it will always be a DafnySequence<Character> if --unicode-char is false (and I would avoid "Unicode characters" as that's highly overloaded and misused :) )

FYI we'll probably add more overloads in the future with statements like The Dafny Runtime type for a String is A {@link DafnySequence} of {@link dafny.CodePoint}s if Dafny is configured with --unicode-char set to true

smithy-dafny-conversion/src/main/java/software/amazon/smithy/dafny/conversion/ToDafny.java

robin-aws · 2023-05-15T20:37:46Z

smithy-dafny-conversion/src/main/java/software/amazon/smithy/dafny/conversion/ToDafny.java

+        // SET("set", SetShape.class, Category.AGGREGATE),
+        // TODO: Frankly, we should avoid Dafny Sets since they do not preserve order;
+        //  Smithy 2.0 deprecates Sets for Unique Lists to ensure order is preserved.
+        // But, we would need to implement our own Dafny Ordered Set...


dafny-lang/libraries#107 :)

robin-aws · 2023-05-15T20:50:30Z

Also note I'll cut a separate PR to update the README

robin-aws · 2023-05-15T20:55:22Z

#255

texastony

Responding to comments.
Will pull down and address outstanding requests.

smithy-dafny-conversion/src/main/java/software/amazon/smithy/dafny/conversion/ToDafny.java

Co-authored-by: Robin Salkeld <[email protected]>

…afny/conversion/ToDafny.java Co-authored-by: Robin Salkeld <[email protected]>

Review: #252 (review)

…-dafny into tony/docs-java-conversion

…s-java-conversion # Conflicts: # smithy-dafny-conversion/build.gradle.kts

texastony

Ship it

docs(dafny-java-conversion): JavaDocs for ToNative Blob & Double

a4dedb8

robin-aws self-assigned this May 9, 2023

texastony added 7 commits May 9, 2023 13:19

Merge branch 'main-1.x' into tony/docs-java-conversion

a497daf

refactor!(conversion): rename to Smithy Dafny Conversion

c478dd7

refactor!(conversion): rename to Smithy Dafny Conversion

f8d1fa0

docs(conversion): Docs for ToDafny

619c349

docs(conversion): ToNative.Simple

b9b283c

docs(conversion): link ToDafny.Simple to

2ed632d

ToNative.Simple

docs(conversion): ToNative.Aggregate

90c6dda

texastony marked this pull request as ready for review May 10, 2023 02:41

texastony requested a review from a team as a code owner May 10, 2023 02:41

ci(conversion): run javadoc & publish in CI

30a7bc4

robin-aws requested changes May 15, 2023

View reviewed changes

robin-aws mentioned this pull request May 15, 2023

chore: Update README #255

Closed

texastony commented May 15, 2023

View reviewed changes

texastony and others added 9 commits May 15, 2023 14:07

Apply suggestions from code review

3999021

Co-authored-by: Robin Salkeld <[email protected]>

Update smithy-dafny-conversion/src/main/java/software/amazon/smithy/d…

ac42763

…afny/conversion/ToDafny.java Co-authored-by: Robin Salkeld <[email protected]>

refactor: address review comments

1bc7f3b

Review: #252 (review)

Merge branch 'tony/docs-java-conversion' of github.com:awslabs/smithy…

e541745

…-dafny into tony/docs-java-conversion

Renaming, detail on use, DafnyRuntime a normal dependency now

5507a72

Merge branch 'main-1.x' of github.com:awslabs/polymorph into tony/doc…

6792dca

…s-java-conversion # Conflicts: # smithy-dafny-conversion/build.gradle.kts

Fix invalid javadoc tag

fe70d14

Find-and-replace for renaming library and package

da17c7f

Dependency renamings

c919fb2

robin-aws approved these changes May 15, 2023

View reviewed changes

texastony commented May 15, 2023

View reviewed changes

robin-aws merged commit 66226da into main-1.x May 15, 2023

robin-aws deleted the tony/docs-java-conversion branch May 15, 2023 23:11

This was referenced May 16, 2023

chore: Account for smithy dafny conversion library renaming aws/aws-cryptographic-material-providers-library-java#5

Merged

chore: Account for smithy dafny conversion library renaming aws/aws-database-encryption-sdk-dynamodb#194

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

docs(dafny-java-conversion): JavaDocs for ToNative Blob & Double #252

docs(dafny-java-conversion): JavaDocs for ToNative Blob & Double #252

texastony commented May 8, 2023 •

edited by robin-aws

Loading

robin-aws commented May 9, 2023

robin-aws left a comment

robin-aws May 15, 2023

texastony May 15, 2023

robin-aws May 15, 2023

robin-aws May 15, 2023

robin-aws commented May 15, 2023

robin-aws commented May 15, 2023

texastony left a comment

texastony left a comment

	* @return The Dafny Runtime type for a String is A {@link DafnySequence} of {@link Character}s.
	* @return The Dafny Runtime type for a String can be a {@link DafnySequence} of {@link Character}s,
	* if Dafny is configured to NOT use Unicode characters.

docs(dafny-java-conversion): JavaDocs for ToNative Blob & Double #252

docs(dafny-java-conversion): JavaDocs for ToNative Blob & Double #252

Conversation

texastony commented May 8, 2023 • edited by robin-aws Loading

State

robin-aws commented May 9, 2023

robin-aws left a comment

Choose a reason for hiding this comment

robin-aws May 15, 2023

Choose a reason for hiding this comment

texastony May 15, 2023

Choose a reason for hiding this comment

robin-aws May 15, 2023

Choose a reason for hiding this comment

robin-aws May 15, 2023

Choose a reason for hiding this comment

robin-aws commented May 15, 2023

robin-aws commented May 15, 2023

texastony left a comment

Choose a reason for hiding this comment

texastony left a comment

Choose a reason for hiding this comment

texastony commented May 8, 2023 •

edited by robin-aws

Loading