wip

SmithyDafnyMakefile.mk

@@ -56,6 +56,14 @@ SMITHY_MODEL_ROOT := $(LIBRARY_ROOT)/Model
 CODEGEN_CLI_ROOT := $(SMITHY_DAFNY_ROOT)/codegen/smithy-dafny-codegen-cli
 GRADLEW := $(SMITHY_DAFNY_ROOT)/codegen/gradlew
 
+# On macOS, sed requires an extra parameter of ""
+OS := $(shell uname)
+ifeq ($(OS), Darwin)
+  SED_PARAMETER := ""
+else
+  SED_PARAMETER :=
+endif
+
 ########################## Dafny targets
 
 # TODO: This target will not work for projects that use `replaceable` 
@@ -151,6 +159,74 @@ clean-dafny-report:
 
 # Dafny helper targets
 
+_no_extern_pre_transpile: _no_extern_pre_transpile_dependencies _sed_index_file_remove_extern _sed_types_file_remove_extern _sed_wrapped_types_file_remove_extern
+_no_extern_post_transpile: _no_extern_post_transpile_dependencies _sed_types_file_add_extern _sed_index_file_add_extern _sed_wrapped_types_file_add_extern
+
+_no_extern_pre_transpile_dependencies:
+	$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% _no_extern_pre_transpile;, $(PROJECT_DEPENDENCIES))
+
+_no_extern_post_transpile_dependencies:
+	$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% _no_extern_post_transpile;, $(PROJECT_DEPENDENCIES))
+
+_sed_types_file_remove_extern:
+	$(MAKE) _sed_file SED_FILE_PATH=$(TYPES_FILE_PATH) SED_BEFORE_STRING=$(TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(TYPES_FILE_WITHOUT_EXTERN_STRING)
+
+_sed_index_file_remove_extern:
+	$(MAKE) _sed_file SED_FILE_PATH=$(INDEX_FILE_PATH) SED_BEFORE_STRING=$(INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(INDEX_FILE_WITHOUT_EXTERN_STRING)
+
+_sed_wrapped_types_file_remove_extern:
+	$(if $(strip $(WRAPPED_INDEX_FILE_PATH)), $(MAKE) _sed_file SED_FILE_PATH=$(WRAPPED_INDEX_FILE_PATH) SED_BEFORE_STRING=$(WRAPPED_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING), )
+
+_sed_types_file_add_extern:
+	$(MAKE) _sed_file SED_FILE_PATH=$(TYPES_FILE_PATH) SED_BEFORE_STRING=$(TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(TYPES_FILE_WITH_EXTERN_STRING)
+
+_sed_index_file_add_extern:
+	$(MAKE) _sed_file SED_FILE_PATH=$(INDEX_FILE_PATH) SED_BEFORE_STRING=$(INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(INDEX_FILE_WITH_EXTERN_STRING)
+
+_sed_wrapped_types_file_add_extern:
+	$(if $(strip $(WRAPPED_INDEX_FILE_PATH)), $(MAKE) _sed_file SED_FILE_PATH=$(WRAPPED_INDEX_FILE_PATH) SED_BEFORE_STRING=$(WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(WRAPPED_INDEX_FILE_WITH_EXTERN_STRING), )
+
+_sed_file:
+	@{ \
+	: "If the AFTER string is already present and the BEFORE string is not," ; \
+	: "then exit success," ; \
+	: "because the expected result is already present." ; \
+	if grep -q '$(SED_AFTER_STRING)' $(SED_FILE_PATH) && ! grep -q '$(SED_BEFORE_STRING)' $(SED_FILE_PATH); then \
+		echo "String has already been replaced in $(SED_FILE_PATH)"; \
+		exit 0; \
+	fi; \
+	\
+	: "If neither the AFTER nor BEFORE strings are present," ; \
+	: "then exit failure," ; \
+	: "because the sed will fail as the BEFORE string is not present." ; \
+	if ! grep -q '$(SED_BEFORE_STRING)' $(SED_FILE_PATH); then \
+		echo "Error: Could not find string to replace in $(SED_FILE_PATH)"; \
+		exit 1; \
+	fi; \
+	\
+	: "If both the AFTER and BEFORE strings are present," ; \
+	: "then exit failure," ; \
+	: "because the sed will produce unintended results (2 after strings)." ; \
+	if grep -q '$(SED_AFTER_STRING)' $(SED_FILE_PATH) && grep -q '$(SED_BEFORE_STRING)' $(SED_FILE_PATH); then \
+		echo "Error: Could not find string to replace in $(SED_FILE_PATH)"; \
+		exit 1; \
+	fi; \
+	\
+	: "Perform sed" ; \
+	echo "Replacing in $(SED_FILE_PATH)"; \
+	sed -i $(SED_PARAMETER) 's/$(SED_BEFORE_STRING)/$(SED_AFTER_STRING)/g' $(SED_FILE_PATH); \
+	\
+	: "If the BEFORE string is still present or the AFTER string is not present," ; \
+	: "then exit failure," ; \
+	: "because the sed did not succeed." ; \
+	if grep -q '$(SED_BEFORE_STRING)' $(SED_FILE_PATH) || ! grep -q '$(SED_AFTER_STRING)' $(SED_FILE_PATH); then \
+		echo "Error: No replacements made in $(SED_FILE_PATH)"; \
+		exit 1; \
+	else \
+		echo "Replacement successful in $(SED_FILE_PATH)"; \
+	fi; \
+	}
+
 # Transpile the entire project's impl
 # For each index file listed in the project Makefile's PROJECT_INDEX variable,
 #   append a `-library:TestModels/$(PROJECT_INDEX) to the transpiliation target
@@ -605,7 +681,7 @@ clean: _clean
 ########################## Python targets
 
 # Python MUST transpile dependencies first to generate .dtr files
-transpile_python: | transpile_dependencies_python transpile_implementation_python transpile_test_python
+transpile_python: | _no_extern_pre_transpile transpile_dependencies_python transpile_implementation_python transpile_test_python _no_extern_post_transpile
 
 transpile_implementation_python: TARGET=py
 transpile_implementation_python: OUT=runtimes/python/dafny_src

TestModels/Aggregate/Makefile

@@ -20,6 +20,20 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
 # This project has no dependencies 
 # DEPENDENT-MODELS:= 
 
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleTypesBooleanTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny.types\" } SimpleTypesBooleanTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesBooleanTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny\" } SimpleBoolean refines AbstractSimpleTypesBooleanService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleBoolean refines AbstractSimpleTypesBooleanService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleBooleanImpl.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny.wrapped\"} WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService {"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService {"
+
 # Python
 
 PYTHON_MODULE_NAME=simple_aggregate

TestModels/SimpleTypes/SimpleBlob/Makefile

@@ -16,6 +16,20 @@ SERVICE_DEPS_SimpleBlob :=
 
 SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
 
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleTypesBlobTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.blob.internaldafny.types\" } SimpleTypesBlobTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesBlobTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.blob.internaldafny\" } SimpleBlob refines AbstractSimpleTypesBlobService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleBlob refines AbstractSimpleTypesBlobService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleBlobImpl.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.blob.internaldafny.wrapped\"} WrappedSimpleTypesBlobService refines WrappedAbstractSimpleTypesBlobService {"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesBlobService refines WrappedAbstractSimpleTypesBlobService {"
+
 # Python
 
 PYTHON_MODULE_NAME=simple_types_blob

TestModels/SimpleTypes/SimpleBlob/src/Index.dfy

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 include "SimpleBlobImpl.dfy"
 
-module SimpleBlob refines AbstractSimpleTypesBlobService {
+module {:extern "simple.types.blob.internaldafny" } SimpleBlob refines AbstractSimpleTypesBlobService {
     import Operations = SimpleBlobImpl
 
  function method DefaultSimpleBlobConfig(): SimpleBlobConfig {

TestModels/SimpleTypes/SimpleBlob/src/WrappedSimpleBlobImpl.dfy

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 include "../Model/SimpleTypesBlobTypesWrapped.dfy"
 
-module WrappedSimpleTypesBlobService refines WrappedAbstractSimpleTypesBlobService {
+module {:extern "simple.types.blob.internaldafny.wrapped"} WrappedSimpleTypesBlobService refines WrappedAbstractSimpleTypesBlobService {
     import WrappedService = SimpleBlob
     function method WrappedDefaultSimpleBlobConfig(): SimpleBlobConfig {
         SimpleBlobConfig

TestModels/SimpleTypes/SimpleBoolean/Makefile

@@ -16,6 +16,20 @@ SERVICE_DEPS_SimpleBoolean :=
 
 SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
 
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleTypesBooleanTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny.types\" } SimpleTypesBooleanTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesBooleanTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny\" } SimpleBoolean refines AbstractSimpleTypesBooleanService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleBoolean refines AbstractSimpleTypesBooleanService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleBooleanImpl.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny.wrapped\"} WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService {"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService {"
+
 # Python
 
 PYTHON_MODULE_NAME=simple_types_boolean

TestModels/SimpleTypes/SimpleBoolean/src/Index.dfy

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 include "SimpleBooleanImpl.dfy"
 
-module SimpleBoolean refines AbstractSimpleTypesBooleanService {
+module {:extern "simple.types.boolean.internaldafny" } SimpleBoolean refines AbstractSimpleTypesBooleanService {
     import Operations = SimpleBooleanImpl
 
  function method DefaultSimpleBooleanConfig(): SimpleBooleanConfig {

TestModels/SimpleTypes/SimpleBoolean/src/WrappedSimpleBooleanImpl.dfy

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 include "../Model/SimpleTypesBooleanTypesWrapped.dfy"
 
-module WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService {
+module {:extern "simple.types.boolean.internaldafny.wrapped"} WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService {
     import WrappedService = SimpleBoolean
     function method WrappedDefaultSimpleBooleanConfig(): SimpleBooleanConfig {
         SimpleBooleanConfig

TestModels/SimpleTypes/SimpleDouble/Makefile

@@ -24,6 +24,20 @@ transpile_net_dependencies:
 format_net:
 	pushd runtimes/net && dotnet format && popd
 
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleTypesSmithyDoubleTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithydouble.internaldafny.types\" } SimpleTypesSmithyDoubleTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesSmithyDoubleTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithydouble.internaldafny\" } SimpleDouble refines AbstractSimpleTypesSmithyDoubleService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleDouble refines AbstractSimpleTypesSmithyDoubleService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedIndex.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithydouble.internaldafny.wrapped\"} WrappedSimpleTypesDouble refines WrappedAbstractSimpleTypesSmithyDoubleService"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesDouble refines WrappedAbstractSimpleTypesSmithyDoubleService"
+
 # Python
 
 PYTHON_MODULE_NAME=simple_types_smithydouble

TestModels/SimpleTypes/SimpleDouble/src/Index.dfy

@@ -4,7 +4,7 @@
 include "../Model/SimpleTypesSmithyDoubleTypes.dfy"
 include "./SimpleSmithyDoubleOperations.dfy"
 
-module SimpleDouble refines AbstractSimpleTypesSmithyDoubleService {
+module {:extern "simple.types.smithydouble.internaldafny" } SimpleDouble refines AbstractSimpleTypesSmithyDoubleService {
  import Operations = SimpleSmithyDoubleOperations
 
  function method DefaultSimpleDoubleConfig(): SimpleDoubleConfig {

TestModels/SimpleTypes/SimpleDouble/src/WrappedIndex.dfy

@@ -3,8 +3,7 @@
 
 include "../Model/SimpleTypesSmithyDoubleTypesWrapped.dfy"
 
-module
-  WrappedSimpleTypesDouble refines WrappedAbstractSimpleTypesSmithyDoubleService
+module {:extern "simple.types.smithydouble.internaldafny.wrapped"} WrappedSimpleTypesDouble refines WrappedAbstractSimpleTypesSmithyDoubleService
 {
   import WrappedService = SimpleDouble
 

TestModels/SimpleTypes/SimpleEnum/Makefile

@@ -19,6 +19,20 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
 # This project has no dependencies 
 # DEPENDENT-MODELS:= 
 
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleTypesEnumTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.enum.internaldafny.types\" } SimpleTypesEnumTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesEnumTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.enum.internaldafny\" } SimpleEnum refines AbstractSimpleTypesEnumService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleEnum refines AbstractSimpleTypesEnumService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleEnumImpl.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.enum.internaldafny.wrapped\"} WrappedSimpleTypesEnumService refines WrappedAbstractSimpleTypesEnumService {"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesEnumService refines WrappedAbstractSimpleTypesEnumService {"
+
 # Python
 
 PYTHON_MODULE_NAME=simple_types_smithyenum

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java

@@ -129,7 +129,10 @@ public Map<Path, TokenTree> generate() {
       namespace
     );
     final TokenTree typesModuleHeader = Token.of(
-      "module %s".formatted(
+      "module {:extern \"%s\" } %s".formatted(
+          DafnyNameResolverHelpers.dafnyExternNamespaceForShapeId(
+            serviceShape.getId()
+          ),
           typesModuleName
         )
     );