sdks only

smithy-lang · Aug 9, 2024 · ed14e47 · ed14e47
1 parent 75f1ddb
commit ed14e47
Show file tree

Hide file tree

Showing 7 changed files with 8 additions and 24 deletions.
diff --git a/TestModels/SimpleTypes/SimpleTimestamp/test/SimpleTimestampImplTest.dfy b/TestModels/SimpleTypes/SimpleTimestamp/test/SimpleTimestampImplTest.dfy
@@ -19,7 +19,7 @@ module SimpleTimestampImplTest {
       modifies client.Modifies
       ensures client.ValidState()
     {
-        var dafnyTimestamp := "2024-06-11T12:34:56";
+        var dafnyTimestamp := "2024-06-11T12:34:56.000Z";
         var ret :- expect client.GetTimestamp(SimpleTimestamp.Types.GetTimestampInput(value:= Some(dafnyTimestamp)));
         expect ret.value == Some(dafnyTimestamp);
         print ret;

diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenConstants.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenConstants.java
diff --git a/...n/src/main/java/software/amazon/polymorph/smithypython/awssdk/AwsSdkCodegenConstants.java b/...n/src/main/java/software/amazon/polymorph/smithypython/awssdk/AwsSdkCodegenConstants.java
@@ -2,4 +2,5 @@
 
 public class AwsSdkCodegenConstants {
     public static String AWS_SDK_CODEGEN_SYMBOLWRITER_DUMP_FILE_FILENAME = "awssdk_codegen_todelete.tmp";
+    public static String BOTO3_TIMESTAMP_STRING_FORMAT = "%Y-%m-%dT%H:%M:%S.%fZ";
 }
diff --git a/...software/amazon/polymorph/smithypython/awssdk/shapevisitor/AwsSdkToDafnyShapeVisitor.java b/...software/amazon/polymorph/smithypython/awssdk/shapevisitor/AwsSdkToDafnyShapeVisitor.java
@@ -32,7 +32,7 @@
 import software.amazon.smithy.python.codegen.GenerationContext;
 import software.amazon.smithy.python.codegen.PythonWriter;
 
-import static software.amazon.polymorph.CodegenConstants.DAFNY_DATETIME_STRING_FORMAT;
+import static software.amazon.polymorph.smithypython.awssdk.AwsSdkCodegenConstants.BOTO3_TIMESTAMP_STRING_FORMAT;
 
 /**
  * ShapeVisitor that should be dispatched from a shape to generate code that maps a AWS SDK
@@ -249,7 +249,7 @@ public String timestampShape(TimestampShape shape) {
     writer.addStdlibImport("datetime", "timezone");
     return "_dafny.Seq(%1$s.astimezone(timezone.utc).strftime(\"%2$s\"))".formatted(
             dataSource,
-            DAFNY_DATETIME_STRING_FORMAT
+            BOTO3_TIMESTAMP_STRING_FORMAT
     );
   }
 

diff --git a/...software/amazon/polymorph/smithypython/awssdk/shapevisitor/DafnyToAwsSdkShapeVisitor.java b/...software/amazon/polymorph/smithypython/awssdk/shapevisitor/DafnyToAwsSdkShapeVisitor.java
@@ -32,7 +32,7 @@
 import software.amazon.smithy.python.codegen.GenerationContext;
 import software.amazon.smithy.python.codegen.PythonWriter;
 
-import static software.amazon.polymorph.CodegenConstants.DAFNY_DATETIME_STRING_FORMAT;
+import static software.amazon.polymorph.smithypython.awssdk.AwsSdkCodegenConstants.BOTO3_TIMESTAMP_STRING_FORMAT;
 
 /**
  * ShapeVisitor that should be dispatched from a shape to generate code that maps a Dafny shape's
@@ -235,7 +235,7 @@ public String timestampShape(TimestampShape shape) {
     writer.addStdlibImport("datetime", "datetime");
     return "datetime.strptime(%1$s.VerbatimString(False), \"%2$s\")".formatted(
             dataSource,
-            DAFNY_DATETIME_STRING_FORMAT
+            BOTO3_TIMESTAMP_STRING_FORMAT
     );
   }
 

diff --git a/...zon/polymorph/smithypython/localservice/shapevisitor/DafnyToLocalServiceShapeVisitor.java b/...zon/polymorph/smithypython/localservice/shapevisitor/DafnyToLocalServiceShapeVisitor.java
@@ -32,8 +32,6 @@
 import software.amazon.smithy.python.codegen.GenerationContext;
 import software.amazon.smithy.python.codegen.PythonWriter;
 
-import static software.amazon.polymorph.CodegenConstants.DAFNY_DATETIME_STRING_FORMAT;
-
 /**
  * ShapeVisitor that should be dispatched from a shape to generate code that maps a Dafny shape's
  * internal attributes to the corresponding Smithy shape's internal attributes.
@@ -272,11 +270,7 @@ public String enumShape(EnumShape shape) {
 
   @Override
   public String timestampShape(TimestampShape shape) {
-    writer.addStdlibImport("datetime", "datetime");
-    return "datetime.strptime(%1$s.VerbatimString(False), \"%2$s\")".formatted(
-            dataSource,
-            DAFNY_DATETIME_STRING_FORMAT
-    );
+    throw new UnsupportedOperationException("TimestampShape from within a LocalService not supported");
   }
 
   @Override

diff --git a/...zon/polymorph/smithypython/localservice/shapevisitor/LocalServiceToDafnyShapeVisitor.java b/...zon/polymorph/smithypython/localservice/shapevisitor/LocalServiceToDafnyShapeVisitor.java
@@ -32,8 +32,6 @@
 import software.amazon.smithy.python.codegen.GenerationContext;
 import software.amazon.smithy.python.codegen.PythonWriter;
 
-import static software.amazon.polymorph.CodegenConstants.DAFNY_DATETIME_STRING_FORMAT;
-
 /**
  * ShapeVisitor that should be dispatched from a shape
  * to generate code that maps a Smithy-modelled shape's internal attributes
@@ -275,11 +273,7 @@ public String enumShape(EnumShape shape) {
 
     @Override
     public String timestampShape(TimestampShape shape) {
-      writer.addStdlibImport("_dafny");
-      return "_dafny.Seq(%1$s.strftime(\"%2$s\"))".formatted(
-              dataSource,
-              DAFNY_DATETIME_STRING_FORMAT
-      );
+      throw new UnsupportedOperationException("TimestampShape from within a LocalService not supported");
     }
 
     @Override