From 0d4266eb58d652c8d452768d6876308c39bd9b18 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 22 Aug 2024 08:29:33 -0700 Subject: [PATCH] chore: Optionally remove extern names when compiling to certain languages (#512) --- SmithyDafnyMakefile.mk | 20 +++-- SmithyDafnySedMakefile.mk | 83 +++++++++++++++++++ TestModels/Aggregate/Makefile | 14 ++++ TestModels/CodegenPatches/Makefile | 16 ++++ TestModels/Constraints/Makefile | 16 ++++ .../Extern/WrappedSimpleConstraintsService.cs | 9 +- TestModels/Constructor/Makefile | 15 ++++ TestModels/Dependencies/Makefile | 14 ++++ .../WrappedSimpleDependenciesService.cs | 8 +- TestModels/Documentation/Makefile | 16 ++++ TestModels/Errors/Makefile | 16 ++++ .../net/Extern/WrappedSimpleErrorsService.cs | 9 +- TestModels/Extendable/Makefile | 16 ++++ TestModels/Extendable/src/Index.dfy | 4 +- TestModels/Extendable/src/WrappedIndex.dfy | 4 +- TestModels/Extern/Makefile | 15 ++++ TestModels/LanguageSpecificLogic/Makefile | 2 +- TestModels/LocalService/Makefile | 19 ++++- TestModels/LocalService/src/Index.dfy | 4 +- TestModels/LocalService/src/WrappedIndex.dfy | 4 +- TestModels/MultipleModels/Makefile | 51 ++++++++++++ .../WrappedSimpleDependencyProjectService.cs | 9 +- .../WrappedSimplePrimaryProjectService.cs | 8 +- TestModels/Positional/Makefile | 15 ++++ TestModels/Refinement/Makefile | 14 ++++ TestModels/Resource/Makefile | 15 ++++ TestModels/Resource/src/Index.dfy | 4 +- TestModels/Resource/src/WrappedIndex.dfy | 4 +- TestModels/SimpleTypes/SimpleBlob/Makefile | 17 +++- .../net/Extern/WrappedSimpleBlobService.cs | 8 +- TestModels/SimpleTypes/SimpleBoolean/Makefile | 15 ++++ .../net/Extern/WrappedSimpleBooleanService.cs | 8 +- TestModels/SimpleTypes/SimpleDouble/Makefile | 15 ++++ .../SimpleDouble/src/WrappedIndex.dfy | 4 +- TestModels/SimpleTypes/SimpleEnum/Makefile | 14 ++++ TestModels/SimpleTypes/SimpleEnumV2/Makefile | 15 ++++ TestModels/SimpleTypes/SimpleInteger/Makefile | 14 ++++ TestModels/SimpleTypes/SimpleLong/Makefile | 14 ++++ TestModels/SimpleTypes/SimpleString/Makefile | 15 ++++ .../SimpleTypes/SimpleTimestamp/Makefile | 18 +++- TestModels/Union/Makefile | 15 ++++ TestModels/aws-sdks/ddb/Makefile | 12 +++ TestModels/aws-sdks/kms/Makefile | 12 +++ .../kms/runtimes/net/Extern/KMSClient.cs | 40 ++++----- scripts/sed_replace.sh | 63 ++++++++++++++ 45 files changed, 650 insertions(+), 73 deletions(-) create mode 100644 SmithyDafnySedMakefile.mk create mode 100755 scripts/sed_replace.sh diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index 056d1c8e8..7d9b292c2 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -56,14 +56,16 @@ SMITHY_MODEL_ROOT := $(LIBRARY_ROOT)/Model CODEGEN_CLI_ROOT := $(SMITHY_DAFNY_ROOT)/codegen/smithy-dafny-codegen-cli GRADLEW := $(SMITHY_DAFNY_ROOT)/codegen/gradlew -########################## Dafny targets +include $(SMITHY_DAFNY_ROOT)/SmithyDafnySedMakefile.mk + +# This flag enables pre-processing on extern module names. +# This pre-processing is required to compile to Python and Go. +# This is disabled by default. +# This should be enabled in each individual project's Makefile if that project compiles to Python or Go. +# This can be enabled by setting this variable to any nonempty value (ex. true, 1) +ENABLE_EXTERN_PROCESSING?= -# TODO: This target will not work for projects that use `replaceable` -# module syntax with multiple language targets. -# It will fail with error: -# Error: modules 'A' and 'B' both have CompileName 'same.extern.name' -# We need to come up with some way to verify files per-language. -# Rewrite this as part of Java implementation of LanguageSpecificLogic TestModel. +########################## Dafny targets # Proof of correctness for the math below # function Z3_PROCESSES(cpus:nat): nat @@ -426,7 +428,9 @@ _polymorph_rust: $(if $(RUST_BENERATED), , _polymorph) ########################## .NET targets +transpile_net: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_pre_transpile, ) transpile_net: | transpile_implementation_net transpile_test_net transpile_dependencies_net +transpile_net: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_post_transpile, ) transpile_implementation_net: TARGET=cs transpile_implementation_net: OUT=runtimes/net/ImplementationFromDafny @@ -474,7 +478,9 @@ format_net-check: build_java: transpile_java mvn_local_deploy_dependencies $(GRADLEW) -p runtimes/java build +transpile_java: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_pre_transpile, ) transpile_java: | transpile_implementation_java transpile_test_java transpile_dependencies_java +transpile_java: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_post_transpile, ) transpile_implementation_java: TARGET=java transpile_implementation_java: OUT=runtimes/java/ImplementationFromDafny diff --git a/SmithyDafnySedMakefile.mk b/SmithyDafnySedMakefile.mk new file mode 100644 index 000000000..db6f933d6 --- /dev/null +++ b/SmithyDafnySedMakefile.mk @@ -0,0 +1,83 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +# These are make targets that use sed to replace extern names. +# Some Smithy-Dafny modules declare extern attributes with names that do not work in all languages. +# These targets can remove or add those extern names based on the target language. +# A target language SHOULD declare use of these targets. + +# These should eventually be replaced by replaceable modules that declare per-langauge extern names. +# See https://github.com/smithy-lang/smithy-dafny/issues/528. +# Eventually, the replaceable modules should be removed (or, their extern names should be removed), +# and should be replaced by per-language package/namespace prefixes. + +# On macOS, sed requires an extra parameter of "" +OS := $(shell uname) +ifeq ($(OS), Darwin) + SED_PARAMETER := "" +else + SED_PARAMETER := +endif + +# Before transpiling to a target language that does not expect externs, +# remove any extern attributes. +_no_extern_pre_transpile: _no_extern_pre_transpile_dependencies _sed_types_file_remove_extern _sed_index_file_remove_extern _sed_wrapped_types_file_remove_extern +# After transpiling to a target language that does not expect externs, +# then add back any extern attributes, +# because the expected committed state has extern attributes. +_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 +# Before transpiling to a target language that does expect externs, +# add back any extern attributes if they are not present. +_with_extern_pre_transpile: _with_extern_pre_transpile_dependencies _sed_types_file_add_extern _sed_index_file_add_extern _sed_wrapped_types_file_add_extern +# After transpiling to a target language that does expect externs, +# add back any extern attributes if they are not present for any reason. +_with_extern_post_transpile: _with_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)) + +_with_extern_pre_transpile_dependencies: + $(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% _with_extern_pre_transpile;, $(PROJECT_DEPENDENCIES)) + +_with_extern_post_transpile_dependencies: + $(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% _with_extern_post_transpile;, $(PROJECT_DEPENDENCIES)) + +_sed_types_file_remove_extern: + @if [ -z $(TYPES_FILE_PATH) ] || [ -z $(TYPES_FILE_WITH_EXTERN_STRING) ] || [ -z $(TYPES_FILE_WITHOUT_EXTERN_STRING) ]; then \ + echo "Error: All variables TYPES_FILE_PATH, TYPES_FILE_WITH_EXTERN_STRING, and TYPES_FILE_WITHOUT_EXTERN_STRING must be set and non-empty."; \ + exit 1; \ + fi + $(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: + @if [ -z $(INDEX_FILE_PATH) ] || [ -z $(INDEX_FILE_WITH_EXTERN_STRING) ] || [ -z $(INDEX_FILE_WITHOUT_EXTERN_STRING) ]; then \ + echo "Error: All variables INDEX_FILE_PATH, INDEX_FILE_WITH_EXTERN_STRING, and INDEX_FILE_WITHOUT_EXTERN_STRING must be set and non-empty."; \ + exit 1; \ + fi + $(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: + @if [ -z $(TYPES_FILE_PATH) ] || [ -z $(TYPES_FILE_WITH_EXTERN_STRING) ] || [ -z $(TYPES_FILE_WITHOUT_EXTERN_STRING) ]; then \ + echo "Error: All variables TYPES_FILE_PATH, TYPES_FILE_WITH_EXTERN_STRING, and TYPES_FILE_WITHOUT_EXTERN_STRING must be set and non-empty."; \ + exit 1; \ + fi + $(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: + @if [ -z $(INDEX_FILE_PATH) ] || [ -z $(INDEX_FILE_WITH_EXTERN_STRING) ] || [ -z $(INDEX_FILE_WITHOUT_EXTERN_STRING) ]; then \ + echo "Error: All variables INDEX_FILE_PATH, INDEX_FILE_WITH_EXTERN_STRING, and INDEX_FILE_WITHOUT_EXTERN_STRING must be set and non-empty."; \ + exit 1; \ + fi + $(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: + $(SMITHY_DAFNY_ROOT)/scripts/sed_replace.sh diff --git a/TestModels/Aggregate/Makefile b/TestModels/Aggregate/Makefile index 01472b7c1..4da000f63 100644 --- a/TestModels/Aggregate/Makefile +++ b/TestModels/Aggregate/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../SharedMakefile.mk @@ -19,3 +20,16 @@ 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/SimpleAggregateTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.aggregate.internaldafny.types\" } SimpleAggregateTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleAggregateTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.aggregate.internaldafny\"} SimpleAggregate refines AbstractSimpleAggregateService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleAggregate refines AbstractSimpleAggregateService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleAggregateImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.aggregate.internaldafny.wrapped\"} WrappedSimpleAggregateService refines WrappedAbstractSimpleAggregateService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleAggregateService refines WrappedAbstractSimpleAggregateService {" diff --git a/TestModels/CodegenPatches/Makefile b/TestModels/CodegenPatches/Makefile index 012170614..ec15a823e 100644 --- a/TestModels/CodegenPatches/Makefile +++ b/TestModels/CodegenPatches/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../SharedMakefile.mk PROJECT_SERVICES := \ @@ -22,3 +24,17 @@ clean: _clean rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleCodegenpatchesTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.codegenpatches.internaldafny.types\" } SimpleCodegenpatchesTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleCodegenpatchesTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.codegenpatches.internaldafny\" } CodegenPatches refines AbstractSimpleCodegenpatchesService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleCodegenpatches refines AbstractSimpleCodegenpatchesService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedCodegenPatchesImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.codegenpatches.internaldafny.wrapped\"} WrappedSimpleCodegenPatchesService refines WrappedAbstractSimpleCodegenpatchesService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleCodegenpatchesService refines WrappedAbstractSimpleCodegenpatchesService {" diff --git a/TestModels/Constraints/Makefile b/TestModels/Constraints/Makefile index fa31cc541..77099fdad 100644 --- a/TestModels/Constraints/Makefile +++ b/TestModels/Constraints/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../SharedMakefile.mk PROJECT_SERVICES := \ @@ -24,3 +26,17 @@ polymorph: make polymorph_dafny make polymorph_java make polymorph_dotnet + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleConstraintsTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constraints.internaldafny.types\" } SimpleConstraintsTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleConstraintsTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constraints.internaldafny\" } SimpleConstraints refines AbstractSimpleConstraintsService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleConstraints refines AbstractSimpleConstraintsService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleConstraintsImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constraints.internaldafny.wrapped\"} WrappedSimpleConstraintsService refines WrappedAbstractSimpleConstraintsService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleConstraintsService refines WrappedAbstractSimpleConstraintsService {" diff --git a/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs b/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs index ef1e400b0..9dec57066 100644 --- a/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs +++ b/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs @@ -3,11 +3,14 @@ using Wrappers_Compile; using Simple.Constraints; using Simple.Constraints.Wrapped; -using TypeConversion = Simple.Constraints.TypeConversion ; +using TypeConversion = Simple.Constraints.TypeConversion; namespace simple.constraints.internaldafny.wrapped { - public partial class __default { - public static _IResult WrappedSimpleConstraints(types._ISimpleConstraintsConfig config) { + public partial class __default + { + [System.Obsolete] + public static _IResult WrappedSimpleConstraints(types._ISimpleConstraintsConfig config) + { var wrappedConfig = TypeConversion.FromDafny_N6_simple__N11_constraints__S23_SimpleConstraintsConfig(config); var impl = new SimpleConstraints(wrappedConfig); var wrappedClient = new SimpleConstraintsShim(impl); diff --git a/TestModels/Constructor/Makefile b/TestModels/Constructor/Makefile index 3191fcef7..5c067085f 100644 --- a/TestModels/Constructor/Makefile +++ b/TestModels/Constructor/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../SharedMakefile.mk @@ -20,3 +21,17 @@ 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/SimpleConstructorTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constructor.internaldafny.types\" } SimpleConstructorTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleConstructorTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constructor.internaldafny\" } SimpleConstructor refines AbstractSimpleConstructorService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleConstructor refines AbstractSimpleConstructorService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleConstructorImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constructor.internaldafny.wrapped\"} WrappedSimpleConstructorService refines WrappedAbstractSimpleConstructorService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleConstructorService refines WrappedAbstractSimpleConstructorService {" diff --git a/TestModels/Dependencies/Makefile b/TestModels/Dependencies/Makefile index 5186198bc..36a0e0f7a 100644 --- a/TestModels/Dependencies/Makefile +++ b/TestModels/Dependencies/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../SharedMakefile.mk PROJECT_SERVICES := \ @@ -39,3 +41,15 @@ clean: _clean rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated + +TYPES_FILE_PATH=Model/SimpleDependenciesTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.dependencies.internaldafny.types\" } SimpleDependenciesTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleDependenciesTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.dependencies.internaldafny\" } SimpleDependencies refines AbstractSimpleDependenciesService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleDependencies refines AbstractSimpleDependenciesService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleDependenciesImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.dependencies.internaldafny.wrapped\"} WrappedSimpleDependenciesService refines WrappedAbstractSimpleDependenciesService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleDependenciesService refines WrappedAbstractSimpleDependenciesService {" diff --git a/TestModels/Dependencies/runtimes/net/Extern/WrappedSimpleDependenciesService.cs b/TestModels/Dependencies/runtimes/net/Extern/WrappedSimpleDependenciesService.cs index f2ecb9d6d..84e45ac5d 100644 --- a/TestModels/Dependencies/runtimes/net/Extern/WrappedSimpleDependenciesService.cs +++ b/TestModels/Dependencies/runtimes/net/Extern/WrappedSimpleDependenciesService.cs @@ -3,11 +3,13 @@ using Wrappers_Compile; using Simple.Dependencies; using Simple.Dependencies.Wrapped; -using TypeConversion = Simple.Dependencies.TypeConversion ; +using TypeConversion = Simple.Dependencies.TypeConversion; namespace simple.dependencies.internaldafny.wrapped { - public partial class __default { - public static _IResult WrappedSimpleDependencies(types._ISimpleDependenciesConfig config) { + public partial class __default + { + public static _IResult WrappedSimpleDependencies(types._ISimpleDependenciesConfig config) + { var wrappedConfig = TypeConversion.FromDafny_N6_simple__N12_dependencies__S24_SimpleDependenciesConfig(config); var impl = new SimpleDependencies(wrappedConfig); var wrappedClient = new SimpleDependenciesShim(impl); diff --git a/TestModels/Documentation/Makefile b/TestModels/Documentation/Makefile index 80a43422e..1e8402bfb 100644 --- a/TestModels/Documentation/Makefile +++ b/TestModels/Documentation/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../SharedMakefile.mk PROJECT_SERVICES := \ @@ -18,3 +20,17 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy # DEPENDENT-MODELS:= POLYMORPH_OPTIONS=--generate client-constructors,project-files + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleDocumentationTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.documentation.internaldafny.types\" } SimpleDocumentationTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleDocumentationTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.documentation.internaldafny\" } SimpleDocumentation refines AbstractSimpleDocumentationService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleDocumentation refines AbstractSimpleDocumentationService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleDocumentationImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:options \"--function-syntax:4\"} {:extern \"simple.documentation.internaldafny.wrapped\"} WrappedSimpleDocumentationService refines WrappedAbstractSimpleDocumentationService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module {:options \"--function-syntax:4\"} WrappedSimpleDocumentationService refines WrappedAbstractSimpleDocumentationService {" diff --git a/TestModels/Errors/Makefile b/TestModels/Errors/Makefile index 21cda8f8d..62606a1fb 100644 --- a/TestModels/Errors/Makefile +++ b/TestModels/Errors/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../SharedMakefile.mk PROJECT_SERVICES := \ @@ -21,3 +23,17 @@ clean: _clean rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleErrorsTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.errors.internaldafny.types\" } SimpleErrorsTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleErrorsTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.errors.internaldafny\" } SimpleErrors refines AbstractSimpleErrorsService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleErrors refines AbstractSimpleErrorsService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleErrorsImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.errors.internaldafny.wrapped\"} WrappedSimpleErrorsService refines WrappedAbstractSimpleErrorsService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleErrorsService refines WrappedAbstractSimpleErrorsService {" diff --git a/TestModels/Errors/runtimes/net/Extern/WrappedSimpleErrorsService.cs b/TestModels/Errors/runtimes/net/Extern/WrappedSimpleErrorsService.cs index f489fa1e3..08a5a425e 100644 --- a/TestModels/Errors/runtimes/net/Extern/WrappedSimpleErrorsService.cs +++ b/TestModels/Errors/runtimes/net/Extern/WrappedSimpleErrorsService.cs @@ -3,11 +3,14 @@ using Wrappers_Compile; using Simple.Errors; using Simple.Errors.Wrapped; -using TypeConversion = Simple.Errors.TypeConversion ; +using TypeConversion = Simple.Errors.TypeConversion; namespace simple.errors.internaldafny.wrapped { - public partial class __default { - public static _IResult WrappedSimpleErrors(types._ISimpleErrorsConfig config) { + public partial class __default + { + [System.Obsolete] + public static _IResult WrappedSimpleErrors(types._ISimpleErrorsConfig config) + { var wrappedConfig = TypeConversion.FromDafny_N6_simple__N6_errors__S18_SimpleErrorsConfig(config); var impl = new SimpleErrors(wrappedConfig); var wrappedClient = new SimpleErrorsShim(impl); diff --git a/TestModels/Extendable/Makefile b/TestModels/Extendable/Makefile index 00777e807..87cf99536 100644 --- a/TestModels/Extendable/Makefile +++ b/TestModels/Extendable/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../SharedMakefile.mk NAMESPACE=simple.extendable.resources @@ -27,3 +29,17 @@ clean: _clean rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleExtendableResourcesTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.extendable.resources.internaldafny.types\" } SimpleExtendableResourcesTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleExtendableResourcesTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.extendable.resources.internaldafny\"} SimpleExtendableResources refines AbstractSimpleExtendableResourcesService" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleExtendableResources refines AbstractSimpleExtendableResourcesService" + +WRAPPED_INDEX_FILE_PATH=src/WrappedIndex.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.extendable.resources.internaldafny.wrapped\"} WrappedSimpleExtendableResources refines WrappedAbstractSimpleExtendableResourcesService" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleExtendableResources refines WrappedAbstractSimpleExtendableResourcesService" diff --git a/TestModels/Extendable/src/Index.dfy b/TestModels/Extendable/src/Index.dfy index d3ccc91d8..6eba446de 100644 --- a/TestModels/Extendable/src/Index.dfy +++ b/TestModels/Extendable/src/Index.dfy @@ -4,9 +4,7 @@ include "../Model/SimpleExtendableResourcesTypes.dfy" include "./SimpleExtendableResourcesOperations.dfy" -module - {:extern "simple.extendable.resources.internaldafny"} - SimpleExtendableResources refines AbstractSimpleExtendableResourcesService +module {:extern "simple.extendable.resources.internaldafny"} SimpleExtendableResources refines AbstractSimpleExtendableResourcesService { import Operations = SimpleExtendableResourcesOperations diff --git a/TestModels/Extendable/src/WrappedIndex.dfy b/TestModels/Extendable/src/WrappedIndex.dfy index cba052b7a..6b25c6c57 100644 --- a/TestModels/Extendable/src/WrappedIndex.dfy +++ b/TestModels/Extendable/src/WrappedIndex.dfy @@ -3,9 +3,7 @@ include "../Model/SimpleExtendableResourcesTypesWrapped.dfy" -module - {:extern "simple.extendable.resources.internaldafny.wrapped"} - WrappedSimpleExtendableResources refines WrappedAbstractSimpleExtendableResourcesService +module {:extern "simple.extendable.resources.internaldafny.wrapped"} WrappedSimpleExtendableResources refines WrappedAbstractSimpleExtendableResourcesService { import WrappedService = SimpleExtendableResources diff --git a/TestModels/Extern/Makefile b/TestModels/Extern/Makefile index a8a0c1fcc..91761e1e3 100644 --- a/TestModels/Extern/Makefile +++ b/TestModels/Extern/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../SharedMakefile.mk PROJECT_SERVICES := \ @@ -17,3 +19,16 @@ 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/SimpleDafnyExternTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.dafnyextern.internaldafny.types\" } SimpleDafnyExternTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleDafnyExternTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.dafnyextern.internaldafny\" } SimpleExtern refines AbstractSimpleDafnyExternService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleExtern refines AbstractSimpleDafnyExternService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleExternImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.dafnyextern.internaldafny.wrapped\"} WrappedSimpleExternService refines WrappedAbstractSimpleDafnyExternService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleExternService refines WrappedAbstractSimpleDafnyExternService {" diff --git a/TestModels/LanguageSpecificLogic/Makefile b/TestModels/LanguageSpecificLogic/Makefile index 3eabbac60..354a8f1a7 100644 --- a/TestModels/LanguageSpecificLogic/Makefile +++ b/TestModels/LanguageSpecificLogic/Makefile @@ -25,5 +25,5 @@ RUST_TEST_INDEX=test/replaces/rust RUST_OTHER_FILES=runtimes/rust/src/externs.rs # This project has no dependencies -# DEPENDENT-MODELS:= +# DEPENDENT-MODELS:= diff --git a/TestModels/LocalService/Makefile b/TestModels/LocalService/Makefile index c08fad231..343ddfaa4 100644 --- a/TestModels/LocalService/Makefile +++ b/TestModels/LocalService/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../SharedMakefile.mk NAMESPACE=simple.localService @@ -17,7 +19,22 @@ SERVICE_DEPS_SimpleLocalService := SMITHY_DEPS=dafny-dependencies/Model/traits.smithy # This project has no dependencies -# DEPENDENT-MODELS:= +# DEPENDENT-MODELS:= + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleLocalServiceTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.localservice.internaldafny.types\" } SimpleLocalServiceTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleLocalServiceTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.localservice.internaldafny\"} SimpleLocalService refines AbstractSimpleLocalServiceService" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleLocalService refines AbstractSimpleLocalServiceService" + +WRAPPED_INDEX_FILE_PATH=src/WrappedIndex.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.localservice.internaldafny.wrapped\"} WrappedSimpleLocalService refines WrappedAbstractSimpleLocalServiceService" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleLocalService refines WrappedAbstractSimpleLocalServiceService" + clean: diff --git a/TestModels/LocalService/src/Index.dfy b/TestModels/LocalService/src/Index.dfy index 9a566b871..8963c0b68 100644 --- a/TestModels/LocalService/src/Index.dfy +++ b/TestModels/LocalService/src/Index.dfy @@ -4,9 +4,7 @@ include "../Model/SimpleLocalServiceTypes.dfy" include "./SimpleLocalServiceOperations.dfy" -module - {:extern "simple.localservice.internaldafny"} - SimpleLocalService refines AbstractSimpleLocalServiceService +module {:extern "simple.localservice.internaldafny"} SimpleLocalService refines AbstractSimpleLocalServiceService { import Operations = SimpleLocalServiceOperations diff --git a/TestModels/LocalService/src/WrappedIndex.dfy b/TestModels/LocalService/src/WrappedIndex.dfy index 91a30ac91..617316458 100644 --- a/TestModels/LocalService/src/WrappedIndex.dfy +++ b/TestModels/LocalService/src/WrappedIndex.dfy @@ -3,9 +3,7 @@ include "../Model/SimpleLocalServiceTypesWrapped.dfy" -module - {:extern "simple.localservice.internaldafny.wrapped"} - WrappedSimpleLocalService refines WrappedAbstractSimpleLocalServiceService +module {:extern "simple.localservice.internaldafny.wrapped"} WrappedSimpleLocalService refines WrappedAbstractSimpleLocalServiceService { import WrappedService = SimpleLocalService diff --git a/TestModels/MultipleModels/Makefile b/TestModels/MultipleModels/Makefile index 4a22f49ea..279d1425c 100644 --- a/TestModels/MultipleModels/Makefile +++ b/TestModels/MultipleModels/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../SharedMakefile.mk # DIR_STRUCTURE_V2 is used to signal multiple subprojects/models in one project @@ -27,3 +29,52 @@ SERVICE_DEPS_PrimaryProject := \ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy # DEPENDENT-MODELS:= + +PRIMARY_PROJECT_TYPES_FILE_PATH=dafny/PrimaryProject/Model/SimpleMultiplemodelsPrimaryprojectTypes.dfy +PRIMARY_PROJECT_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.multiplemodels.primaryproject.internaldafny.types\" } SimpleMultiplemodelsPrimaryprojectTypes" +PRIMARY_PROJECT_TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleMultiplemodelsPrimaryprojectTypes" + +PRIMARY_PROJECT_INDEX_FILE_PATH=dafny/PrimaryProject/src/Index.dfy +PRIMARY_PROJECT_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.multiplemodels.primaryproject.internaldafny\" } SimpleMultiplemodelsPrimaryprojectService refines AbstractSimpleMultiplemodelsPrimaryprojectService {" +PRIMARY_PROJECT_INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleMultiplemodelsPrimaryprojectService refines AbstractSimpleMultiplemodelsPrimaryprojectService {" + +PRIMARY_PROJECT_WRAPPED_INDEX_FILE_PATH=dafny/PrimaryProject/src/WrappedSimpleMultiplemodelsPrimaryprojectImpl.dfy +PRIMARY_PROJECT_WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.multiplemodels.primaryproject.internaldafny.wrapped\"} WrappedSimpleMultiplemodelsPrimaryprojectService refines WrappedAbstractSimpleMultiplemodelsPrimaryprojectService {" +PRIMARY_PROJECT_WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleMultiplemodelsPrimaryprojectService refines WrappedAbstractSimpleMultiplemodelsPrimaryprojectService {" + +DEPENDENCY_PROJECT_TYPES_FILE_PATH=dafny/DependencyProject/Model/SimpleMultiplemodelsDependencyprojectTypes.dfy +DEPENDENCY_PROJECT_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.multiplemodels.dependencyproject.internaldafny.types\" } SimpleMultiplemodelsDependencyprojectTypes" +DEPENDENCY_PROJECT_TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleMultiplemodelsDependencyprojectTypes" + +DEPENDENCY_PROJECT_INDEX_FILE_PATH=dafny/DependencyProject/src/Index.dfy +DEPENDENCY_PROJECT_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.multiplemodels.dependencyproject.internaldafny\" } SimpleMultiplemodelsDependencyprojectService refines AbstractSimpleMultiplemodelsDependencyprojectService {" +DEPENDENCY_PROJECT_INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleMultiplemodelsDependencyprojectService refines AbstractSimpleMultiplemodelsDependencyprojectService {" + +DEPENDENCY_PROJECT_WRAPPED_INDEX_FILE_PATH=dafny/DependencyProject/src/WrappedSimpleMultiplemodelsDependencyprojectImpl.dfy +DEPENDENCY_PROJECT_WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.multiplemodels.dependencyproject.internaldafny.wrapped\"} WrappedSimpleMultiplemodelsDependencyprojectService refines WrappedAbstractSimpleMultiplemodelsDependencyprojectService {" +DEPENDENCY_PROJECT_WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleMultiplemodelsDependencyprojectService refines WrappedAbstractSimpleMultiplemodelsDependencyprojectService {" + +_sed_types_file_remove_extern: + $(MAKE) _sed_file SED_FILE_PATH=$(PRIMARY_PROJECT_TYPES_FILE_PATH) SED_BEFORE_STRING=$(PRIMARY_PROJECT_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(PRIMARY_PROJECT_TYPES_FILE_WITHOUT_EXTERN_STRING) + $(MAKE) _sed_file SED_FILE_PATH=$(DEPENDENCY_PROJECT_TYPES_FILE_PATH) SED_BEFORE_STRING=$(DEPENDENCY_PROJECT_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(DEPENDENCY_PROJECT_TYPES_FILE_WITHOUT_EXTERN_STRING) + +_sed_index_file_remove_extern: + $(MAKE) _sed_file SED_FILE_PATH=$(PRIMARY_PROJECT_INDEX_FILE_PATH) SED_BEFORE_STRING=$(PRIMARY_PROJECT_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(PRIMARY_PROJECT_INDEX_FILE_WITHOUT_EXTERN_STRING) + $(MAKE) _sed_file SED_FILE_PATH=$(DEPENDENCY_PROJECT_INDEX_FILE_PATH) SED_BEFORE_STRING=$(DEPENDENCY_PROJECT_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(DEPENDENCY_PROJECT_INDEX_FILE_WITHOUT_EXTERN_STRING) + +_sed_wrapped_types_file_remove_extern: + $(MAKE) _sed_file SED_FILE_PATH=$(PRIMARY_PROJECT_WRAPPED_INDEX_FILE_PATH) SED_BEFORE_STRING=$(PRIMARY_PROJECT_WRAPPED_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(PRIMARY_PROJECT_WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING) + $(MAKE) _sed_file SED_FILE_PATH=$(DEPENDENCY_PROJECT_WRAPPED_INDEX_FILE_PATH) SED_BEFORE_STRING=$(DEPENDENCY_PROJECT_WRAPPED_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(DEPENDENCY_PROJECT_WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING) + +_sed_types_file_add_extern: + $(MAKE) _sed_file SED_FILE_PATH=$(PRIMARY_PROJECT_TYPES_FILE_PATH) SED_BEFORE_STRING=$(PRIMARY_PROJECT_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(PRIMARY_PROJECT_TYPES_FILE_WITH_EXTERN_STRING) + $(MAKE) _sed_file SED_FILE_PATH=$(DEPENDENCY_PROJECT_TYPES_FILE_PATH) SED_BEFORE_STRING=$(DEPENDENCY_PROJECT_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(DEPENDENCY_PROJECT_TYPES_FILE_WITH_EXTERN_STRING) + +_sed_index_file_add_extern: + $(MAKE) _sed_file SED_FILE_PATH=$(PRIMARY_PROJECT_INDEX_FILE_PATH) SED_BEFORE_STRING=$(PRIMARY_PROJECT_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(PRIMARY_PROJECT_INDEX_FILE_WITH_EXTERN_STRING) + $(MAKE) _sed_file SED_FILE_PATH=$(DEPENDENCY_PROJECT_INDEX_FILE_PATH) SED_BEFORE_STRING=$(DEPENDENCY_PROJECT_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(DEPENDENCY_PROJECT_INDEX_FILE_WITH_EXTERN_STRING) + +_sed_wrapped_types_file_add_extern: + $(MAKE) _sed_file SED_FILE_PATH=$(PRIMARY_PROJECT_WRAPPED_INDEX_FILE_PATH) SED_BEFORE_STRING=$(PRIMARY_PROJECT_WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(PRIMARY_PROJECT_WRAPPED_INDEX_FILE_WITH_EXTERN_STRING) + $(MAKE) _sed_file SED_FILE_PATH=$(DEPENDENCY_PROJECT_WRAPPED_INDEX_FILE_PATH) SED_BEFORE_STRING=$(DEPENDENCY_PROJECT_WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(DEPENDENCY_PROJECT_WRAPPED_INDEX_FILE_WITH_EXTERN_STRING) + diff --git a/TestModels/MultipleModels/runtimes/net/Extern/WrappedSimpleDependencyProjectService.cs b/TestModels/MultipleModels/runtimes/net/Extern/WrappedSimpleDependencyProjectService.cs index da5aa6b4d..3f225fa80 100644 --- a/TestModels/MultipleModels/runtimes/net/Extern/WrappedSimpleDependencyProjectService.cs +++ b/TestModels/MultipleModels/runtimes/net/Extern/WrappedSimpleDependencyProjectService.cs @@ -3,11 +3,14 @@ using Wrappers_Compile; using Simple.Multiplemodels.Dependencyproject; using Simple.Multiplemodels.Dependencyproject.Wrapped; -using TypeConversion = Simple.Multiplemodels.Dependencyproject.TypeConversion ; +using TypeConversion = Simple.Multiplemodels.Dependencyproject.TypeConversion; namespace simple.multiplemodels.dependencyproject.internaldafny.wrapped { - public partial class __default { - public static _IResult WrappedDependencyProject(types._IDependencyProjectConfig config) { + public partial class __default + { + [System.Obsolete] + public static _IResult WrappedDependencyProject(types._IDependencyProjectConfig config) + { var wrappedConfig = TypeConversion.FromDafny_N6_simple__N14_multiplemodels__N17_dependencyproject__S23_DependencyProjectConfig(config); var impl = new DependencyProject(wrappedConfig); var wrappedClient = new DependencyProjectShim(impl); diff --git a/TestModels/MultipleModels/runtimes/net/Extern/WrappedSimplePrimaryProjectService.cs b/TestModels/MultipleModels/runtimes/net/Extern/WrappedSimplePrimaryProjectService.cs index 098ec7139..3d5e35d95 100644 --- a/TestModels/MultipleModels/runtimes/net/Extern/WrappedSimplePrimaryProjectService.cs +++ b/TestModels/MultipleModels/runtimes/net/Extern/WrappedSimplePrimaryProjectService.cs @@ -3,11 +3,13 @@ using Wrappers_Compile; using Simple.Multiplemodels.Primaryproject; using Simple.Multiplemodels.Primaryproject.Wrapped; -using TypeConversion = Simple.Multiplemodels.Primaryproject.TypeConversion ; +using TypeConversion = Simple.Multiplemodels.Primaryproject.TypeConversion; namespace simple.multiplemodels.primaryproject.internaldafny.wrapped { - public partial class __default { - public static _IResult WrappedPrimaryProject(types._IPrimaryProjectConfig config) { + public partial class __default + { + public static _IResult WrappedPrimaryProject(types._IPrimaryProjectConfig config) + { var wrappedConfig = TypeConversion.FromDafny_N6_simple__N14_multiplemodels__N14_primaryproject__S20_PrimaryProjectConfig(config); var impl = new PrimaryProject(wrappedConfig); var wrappedClient = new PrimaryProjectShim(impl); diff --git a/TestModels/Positional/Makefile b/TestModels/Positional/Makefile index 388b20559..7ea99b9fe 100644 --- a/TestModels/Positional/Makefile +++ b/TestModels/Positional/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../SharedMakefile.mk NAMESPACE=simple.positional @@ -21,3 +23,16 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy POLYMORPH_OPTIONS=--generate project-files,client-constructors +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimplePositionalTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.positional.internaldafny.types\" } SimplePositionalTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimplePositionalTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.positional.internaldafny\" } SimplePositional refines AbstractSimplePositionalService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimplePositional refines AbstractSimplePositionalService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimplePositionalImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:options \"--function-syntax:4\"} {:extern \"simple.positional.internaldafny.wrapped\"} WrappedSimplePositionalService refines WrappedAbstractSimplePositionalService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module {:options \"--function-syntax:4\" WrappedSimplePositionalService refines WrappedAbstractSimplePositionalService {" diff --git a/TestModels/Refinement/Makefile b/TestModels/Refinement/Makefile index 0009f4e89..1c51c37cf 100644 --- a/TestModels/Refinement/Makefile +++ b/TestModels/Refinement/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../SharedMakefile.mk @@ -21,3 +22,16 @@ 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/SimpleRefinementTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.refinement.internaldafny.types\" } SimpleRefinementTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleRefinementTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.refinement.internaldafny\"} SimpleRefinement refines AbstractSimpleRefinementService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleRefinement refines AbstractSimpleRefinementService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleRefinementImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.refinement.internaldafny.wrapped\"} WrappedSimpleRefinementService refines WrappedAbstractSimpleRefinementService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleRefinementService refines WrappedAbstractSimpleRefinementService {" diff --git a/TestModels/Resource/Makefile b/TestModels/Resource/Makefile index 3b260434e..e41789c2a 100644 --- a/TestModels/Resource/Makefile +++ b/TestModels/Resource/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../SharedMakefile.mk @@ -24,3 +25,17 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy format_net: pushd runtimes/net && dotnet format && popd + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleResourcesTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.resources.internaldafny.types\" } SimpleResourcesTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleResourcesTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.resources.internaldafny\"} SimpleResources refines AbstractSimpleResourcesService" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleResources refines AbstractSimpleResourcesService" + +WRAPPED_INDEX_FILE_PATH=src/WrappedIndex.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.resources.internaldafny.wrapped\"} WrappedSimpleResources refines WrappedAbstractSimpleResourcesService" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleResources refines WrappedAbstractSimpleResourcesService" diff --git a/TestModels/Resource/src/Index.dfy b/TestModels/Resource/src/Index.dfy index 6df0f8d08..a945e105d 100644 --- a/TestModels/Resource/src/Index.dfy +++ b/TestModels/Resource/src/Index.dfy @@ -4,9 +4,7 @@ include "../Model/SimpleResourcesTypes.dfy" include "./SimpleResourcesOperations.dfy" -module - {:extern "simple.resources.internaldafny"} - SimpleResources refines AbstractSimpleResourcesService +module {:extern "simple.resources.internaldafny"} SimpleResources refines AbstractSimpleResourcesService { import Operations = SimpleResourcesOperations diff --git a/TestModels/Resource/src/WrappedIndex.dfy b/TestModels/Resource/src/WrappedIndex.dfy index 1df003572..36915c588 100644 --- a/TestModels/Resource/src/WrappedIndex.dfy +++ b/TestModels/Resource/src/WrappedIndex.dfy @@ -3,9 +3,7 @@ include "../Model/SimpleResourcesTypesWrapped.dfy" -module - {:extern "simple.resources.internaldafny.wrapped"} - WrappedSimpleResources refines WrappedAbstractSimpleResourcesService +module {:extern "simple.resources.internaldafny.wrapped"} WrappedSimpleResources refines WrappedAbstractSimpleResourcesService { import WrappedService = SimpleResources diff --git a/TestModels/SimpleTypes/SimpleBlob/Makefile b/TestModels/SimpleTypes/SimpleBlob/Makefile index 0bc8fadca..7e9f840c2 100644 --- a/TestModels/SimpleTypes/SimpleBlob/Makefile +++ b/TestModels/SimpleTypes/SimpleBlob/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../../SharedMakefile.mk @@ -19,4 +20,18 @@ SERVICE_DEPS_SimpleBlob := SMITHY_DEPS=dafny-dependencies/Model/traits.smithy # This project has no dependencies -# DEPENDENT-MODELS:= +# DEPENDENT-MODELS:= + +# 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 {" diff --git a/TestModels/SimpleTypes/SimpleBlob/runtimes/net/Extern/WrappedSimpleBlobService.cs b/TestModels/SimpleTypes/SimpleBlob/runtimes/net/Extern/WrappedSimpleBlobService.cs index 059c7563d..62f5e1ae0 100644 --- a/TestModels/SimpleTypes/SimpleBlob/runtimes/net/Extern/WrappedSimpleBlobService.cs +++ b/TestModels/SimpleTypes/SimpleBlob/runtimes/net/Extern/WrappedSimpleBlobService.cs @@ -3,11 +3,13 @@ using Wrappers_Compile; using Simple.Types.Blob; using Simple.Types.Blob.Wrapped; -using TypeConversion = Simple.Types.Blob.TypeConversion ; +using TypeConversion = Simple.Types.Blob.TypeConversion; namespace simple.types.blob.internaldafny.wrapped { - public partial class __default { - public static _IResult WrappedSimpleBlob(types._ISimpleBlobConfig config) { + public partial class __default + { + public static _IResult WrappedSimpleBlob(types._ISimpleBlobConfig config) + { var wrappedConfig = TypeConversion.FromDafny_N6_simple__N5_types__N4_blob__S16_SimpleBlobConfig(config); var impl = new SimpleBlob(wrappedConfig); var wrappedClient = new SimpleTypesBlobShim(impl); diff --git a/TestModels/SimpleTypes/SimpleBoolean/Makefile b/TestModels/SimpleTypes/SimpleBoolean/Makefile index c0fbc380c..ecab9f6c5 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/Makefile +++ b/TestModels/SimpleTypes/SimpleBoolean/Makefile @@ -8,6 +8,7 @@ CORES=2 TRANSPILE_TESTS_IN_RUST=1 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../../SharedMakefile.mk @@ -25,3 +26,17 @@ 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 {" diff --git a/TestModels/SimpleTypes/SimpleBoolean/runtimes/net/Extern/WrappedSimpleBooleanService.cs b/TestModels/SimpleTypes/SimpleBoolean/runtimes/net/Extern/WrappedSimpleBooleanService.cs index 4975c00e9..6f81a4574 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/runtimes/net/Extern/WrappedSimpleBooleanService.cs +++ b/TestModels/SimpleTypes/SimpleBoolean/runtimes/net/Extern/WrappedSimpleBooleanService.cs @@ -3,11 +3,13 @@ using Wrappers_Compile; using Simple.Types.Boolean; using Simple.Types.Boolean.Wrapped; -using TypeConversion = Simple.Types.Boolean.TypeConversion ; +using TypeConversion = Simple.Types.Boolean.TypeConversion; namespace simple.types.boolean.internaldafny.wrapped { - public partial class __default { - public static _IResult WrappedSimpleBoolean(types._ISimpleBooleanConfig config) { + public partial class __default + { + public static _IResult WrappedSimpleBoolean(types._ISimpleBooleanConfig config) + { var wrappedConfig = TypeConversion.FromDafny_N6_simple__N5_types__N7_boolean__S19_SimpleBooleanConfig(config); var impl = new SimpleBoolean(wrappedConfig); var wrappedClient = new SimpleTypesBooleanShim(impl); diff --git a/TestModels/SimpleTypes/SimpleDouble/Makefile b/TestModels/SimpleTypes/SimpleDouble/Makefile index 407ff8747..3845e9400 100644 --- a/TestModels/SimpleTypes/SimpleDouble/Makefile +++ b/TestModels/SimpleTypes/SimpleDouble/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../../SharedMakefile.mk @@ -25,3 +26,17 @@ 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" diff --git a/TestModels/SimpleTypes/SimpleDouble/src/WrappedIndex.dfy b/TestModels/SimpleTypes/SimpleDouble/src/WrappedIndex.dfy index a040a4ef2..c94b00039 100644 --- a/TestModels/SimpleTypes/SimpleDouble/src/WrappedIndex.dfy +++ b/TestModels/SimpleTypes/SimpleDouble/src/WrappedIndex.dfy @@ -3,9 +3,7 @@ include "../Model/SimpleTypesSmithyDoubleTypesWrapped.dfy" -module - {:extern "simple.types.smithydouble.internaldafny.wrapped"} - WrappedSimpleTypesDouble refines WrappedAbstractSimpleTypesSmithyDoubleService +module {:extern "simple.types.smithydouble.internaldafny.wrapped"} WrappedSimpleTypesDouble refines WrappedAbstractSimpleTypesSmithyDoubleService { import WrappedService = SimpleDouble diff --git a/TestModels/SimpleTypes/SimpleEnum/Makefile b/TestModels/SimpleTypes/SimpleEnum/Makefile index dbc0a9220..7b89eda25 100644 --- a/TestModels/SimpleTypes/SimpleEnum/Makefile +++ b/TestModels/SimpleTypes/SimpleEnum/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../../SharedMakefile.mk @@ -21,3 +22,16 @@ 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/SimpleTypesSmithyEnumTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithyenum.internaldafny.types\" } SimpleTypesSmithyEnumTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesSmithyEnumTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithyenum.internaldafny\" } SimpleEnum refines AbstractSimpleTypesSmithyEnumService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleEnum refines AbstractSimpleTypesSmithyEnumService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleEnumImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithyenum.internaldafny.wrapped\"} WrappedSimpleTypesEnumService refines WrappedAbstractSimpleTypesSmithyEnumService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesEnumService refines WrappedAbstractSimpleTypesSmithyEnumService {" diff --git a/TestModels/SimpleTypes/SimpleEnumV2/Makefile b/TestModels/SimpleTypes/SimpleEnumV2/Makefile index 01a9a8612..d3e01bacb 100644 --- a/TestModels/SimpleTypes/SimpleEnumV2/Makefile +++ b/TestModels/SimpleTypes/SimpleEnumV2/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../../SharedMakefile.mk @@ -20,3 +21,17 @@ 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/SimpleTypesEnumV2Types.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.enumv2.internaldafny.types\" } SimpleTypesEnumV2Types" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesEnumV2Types" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.enumv2.internaldafny\" } SimpleEnumV2 refines AbstractSimpleTypesEnumV2Service {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleEnumV2 refines AbstractSimpleTypesEnumV2Service {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleEnumImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.enumv2.internaldafny.wrapped\"} WrappedSimpleTypesEnumV2Service refines WrappedAbstractSimpleTypesEnumV2Service {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesEnumV2Service refines WrappedAbstractSimpleTypesEnumV2Service {" diff --git a/TestModels/SimpleTypes/SimpleInteger/Makefile b/TestModels/SimpleTypes/SimpleInteger/Makefile index ad9561103..a4a1b60f5 100644 --- a/TestModels/SimpleTypes/SimpleInteger/Makefile +++ b/TestModels/SimpleTypes/SimpleInteger/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../../SharedMakefile.mk @@ -21,3 +22,16 @@ 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/SimpleTypesIntegerTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.integer.internaldafny.types\" } SimpleTypesIntegerTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesIntegerTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.integer.internaldafny\" } SimpleInteger refines AbstractSimpleTypesIntegerService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleInteger refines AbstractSimpleTypesIntegerService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleIntegerImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.integer.internaldafny.wrapped\"} WrappedSimpleTypesIntegerService refines WrappedAbstractSimpleTypesIntegerService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesIntegerService refines WrappedAbstractSimpleTypesIntegerService {" diff --git a/TestModels/SimpleTypes/SimpleLong/Makefile b/TestModels/SimpleTypes/SimpleLong/Makefile index a897cbded..814a95d6f 100644 --- a/TestModels/SimpleTypes/SimpleLong/Makefile +++ b/TestModels/SimpleTypes/SimpleLong/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../../SharedMakefile.mk @@ -21,3 +22,16 @@ 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/SimpleTypesSmithyLongTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithylong.internaldafny.types\" } SimpleTypesSmithyLongTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesSmithyLongTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithylong.internaldafny\" } SimpleLong refines AbstractSimpleTypesSmithyLongService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleLong refines AbstractSimpleTypesSmithyLongService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleLongImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithylong.internaldafny.wrapped\"} WrappedSimpleTypesLongService refines WrappedAbstractSimpleTypesSmithyLongService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesLongService refines WrappedAbstractSimpleTypesSmithyLongService {" diff --git a/TestModels/SimpleTypes/SimpleString/Makefile b/TestModels/SimpleTypes/SimpleString/Makefile index 9e7245723..2584b67bd 100644 --- a/TestModels/SimpleTypes/SimpleString/Makefile +++ b/TestModels/SimpleTypes/SimpleString/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../../SharedMakefile.mk @@ -20,3 +21,17 @@ 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/SimpleTypesSmithyStringTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithystring.internaldafny.types\" } SimpleTypesSmithyStringTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesSmithyStringTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithystring.internaldafny\" } SimpleString refines AbstractSimpleTypesSmithyStringService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleString refines AbstractSimpleTypesSmithyStringService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleStringImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithystring.internaldafny.wrapped\"} WrappedSimpleTypesStringService refines WrappedAbstractSimpleTypesSmithyStringService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesStringService refines WrappedAbstractSimpleTypesSmithyStringService {" diff --git a/TestModels/SimpleTypes/SimpleTimestamp/Makefile b/TestModels/SimpleTypes/SimpleTimestamp/Makefile index b49b5ab80..6575072c5 100644 --- a/TestModels/SimpleTypes/SimpleTimestamp/Makefile +++ b/TestModels/SimpleTypes/SimpleTimestamp/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../../SharedMakefile.mk @@ -22,4 +23,19 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy # DEPENDENT-MODELS:= -POLYMORPH_OPTIONS=--generate client-constructors,project-files \ No newline at end of file +POLYMORPH_OPTIONS=--generate client-constructors,project-files + + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleTypesTimestampTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.timestamp.internaldafny.types\" } SimpleTypesTimestampTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesTimestampTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.timestamp.internaldafny\" } SimpleTimestamp refines AbstractSimpleTypesTimestampService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleTimestamp refines AbstractSimpleTypesTimestampService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleTypesTimestampImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:options \"--function-syntax:4\"} {:extern \"simple.types.timestamp.internaldafny.wrapped\"} WrappedSimpleTypesTimestampService refines WrappedAbstractSimpleTypesTimestampService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module {:options \"--function-syntax:4\"} WrappedSimpleTypesTimestampService refines WrappedAbstractSimpleTypesTimestampService {" diff --git a/TestModels/Union/Makefile b/TestModels/Union/Makefile index ab1422214..49201a96d 100644 --- a/TestModels/Union/Makefile +++ b/TestModels/Union/Makefile @@ -3,6 +3,7 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 RUST_BENERATED=1 include ../SharedMakefile.mk @@ -22,3 +23,17 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy # DEPENDENT-MODELS:= transpile_net_dependencies: + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleUnionTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.union.internaldafny.types\" } SimpleUnionTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleUnionTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.union.internaldafny\" } SimpleUnion refines AbstractSimpleUnionService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleUnion refines AbstractSimpleUnionService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleUnionImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.union.internaldafny.wrapped\"} WrappedSimpleUnionService refines WrappedAbstractSimpleUnionService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleUnionService refines WrappedAbstractSimpleUnionService {" diff --git a/TestModels/aws-sdks/ddb/Makefile b/TestModels/aws-sdks/ddb/Makefile index 6f39f3795..7759e3a9f 100644 --- a/TestModels/aws-sdks/ddb/Makefile +++ b/TestModels/aws-sdks/ddb/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../../SharedMakefile.mk PROJECT_SERVICES := \ @@ -33,3 +35,13 @@ clean: _clean rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/ComAmazonawsDynamodbTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.services.dynamodb.internaldafny.types\" } ComAmazonawsDynamodbTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module ComAmazonawsDynamodbTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.services.dynamodb.internaldafny\"} Com.Amazonaws.Dynamodb refines AbstractComAmazonawsDynamodbService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module Com.Amazonaws.Dynamodb refines AbstractComAmazonawsDynamodbService {" diff --git a/TestModels/aws-sdks/kms/Makefile b/TestModels/aws-sdks/kms/Makefile index 9f58da919..c7b138d33 100644 --- a/TestModels/aws-sdks/kms/Makefile +++ b/TestModels/aws-sdks/kms/Makefile @@ -3,6 +3,8 @@ CORES=2 +ENABLE_EXTERN_PROCESSING=1 + include ../../SharedMakefile.mk NAMESPACE=com.amazonaws.kms @@ -32,3 +34,13 @@ clean: _clean rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/ComAmazonawsKmsTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.services.kms.internaldafny.types\" } ComAmazonawsKmsTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module ComAmazonawsKmsTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.services.kms.internaldafny\"} Com.Amazonaws.Kms refines AbstractComAmazonawsKmsService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module Com.Amazonaws.Kms refines AbstractComAmazonawsKmsService {" diff --git a/TestModels/aws-sdks/kms/runtimes/net/Extern/KMSClient.cs b/TestModels/aws-sdks/kms/runtimes/net/Extern/KMSClient.cs index d139ce4c3..50166c99e 100644 --- a/TestModels/aws-sdks/kms/runtimes/net/Extern/KMSClient.cs +++ b/TestModels/aws-sdks/kms/runtimes/net/Extern/KMSClient.cs @@ -10,26 +10,26 @@ // that refines the AWS SDK KMS Model namespace software.amazon.cryptography.services.kms.internaldafny { - public partial class __default - { - - public static - _IResult< - types.IKMSClient, - types._IError - > - KMSClient() + public partial class __default { - // var region = RegionEndpoint.GetBySystemName("us-west-2"); - // TODO add user agent, endpoint, and region - var client = new AmazonKeyManagementServiceClient(); - return Result< - types.IKMSClient, - types._IError - > - .create_Success(new KeyManagementServiceShim(client)); - } + public static + _IResult< + types.IKMSClient, + types._IError + > + KMSClient() + { + // var region = RegionEndpoint.GetBySystemName("us-west-2"); + // TODO add user agent, endpoint, and region + var client = new AmazonKeyManagementServiceClient(); + + return Result< + types.IKMSClient, + types._IError + > + .create_Success(new KeyManagementServiceShim(client)); + } public static _IOption RegionMatch( software.amazon.cryptography.services.kms.internaldafny.types.IKMSClient client, @@ -41,6 +41,6 @@ public static _IOption RegionMatch( // our code generation. IAmazonKeyManagementService nativeClient = ((KeyManagementServiceShim)client)._impl; return new Option_Some(nativeClient.Config.RegionEndpoint.SystemName.Equals(regionStr)); - } - } + } + } } diff --git a/scripts/sed_replace.sh b/scripts/sed_replace.sh new file mode 100755 index 000000000..46fb8d86d --- /dev/null +++ b/scripts/sed_replace.sh @@ -0,0 +1,63 @@ +#!/bin/bash + +# On macOS, sed requires an extra parameter of "" +OS=$(uname) +if [ "$OS" = "Darwin" ]; then + SED_PARAMETER='\"\"' +else + SED_PARAMETER='' +fi + +# Ensure all required variables are set +# (This SHOULD have already been checked) +if [ -z "$SED_FILE_PATH" ] || [ -z "$SED_BEFORE_STRING" ] || [ -z "$SED_AFTER_STRING" ]; then + echo "Error: SED_FILE_PATH, SED_BEFORE_STRING, and SED_AFTER_STRING must all be set and non-empty." + exit 1 +fi + +# Check if the file exists +if [ ! -f "$SED_FILE_PATH" ]; then + echo "Error: File $SED_FILE_PATH does not exist." + exit 1 +fi + +# 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: Both BEFORE and AFTER strings are present 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 + +# Verify the replacement was successful + +# 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" + exit 0 +fi