diff --git a/aas_core_codegen/golang/transpilation.py b/aas_core_codegen/golang/transpilation.py index 99614f58a..6e00541a2 100644 --- a/aas_core_codegen/golang/transpilation.py +++ b/aas_core_codegen/golang/transpilation.py @@ -1133,6 +1133,56 @@ def transform_function_call( for arg_node, arg in zip(node.args, args) ] + for i, (arg_node, argument) in enumerate( + zip(node.args, func_type.func.arguments) + ): + source_type = intermediate_type_inference.beneath_optional( + self.type_map[arg_node] + ) + target_type = intermediate.beneath_optional(argument.type_annotation) + if not ( + isinstance(func_type.func, intermediate.TranspilableVerification) + and not argument.mutable + and isinstance( + source_type, intermediate_type_inference.ListTypeAnnotation + ) + and isinstance(target_type, intermediate.ListTypeAnnotation) + and isinstance( + source_type.items, intermediate_type_inference.OurTypeAnnotation + ) + and isinstance(target_type.items, intermediate.OurTypeAnnotation) + and isinstance(source_type.items.our_type, intermediate.Class) + and isinstance(target_type.items.our_type, intermediate.Class) + and source_type.items.our_type is not target_type.items.our_type + and source_type.items.our_type.is_subclass_of( + target_type.items.our_type + ) + ): + continue + + # NOTE (chris-koo): + # Go slices are invariant even when their item interfaces inherit. + # We convert only mismatching read-only arguments, preserving nil. + source_slice = self._our_type_name( + golang_naming.interface_name(source_type.items.our_type.name) + ) + target_slice = self._our_type_name( + golang_naming.interface_name(target_type.items.our_type.name) + ) + args[i] = Stripped( + f"""\ +func(items []{source_slice}) []{target_slice} {{ +{I}if items == nil {{ +{II}return nil +{I}}} +{I}result := make([]{target_slice}, len(items)) +{I}for i, item := range items {{ +{II}result[i] = item +{I}}} +{I}return result +}}({args[i]})""" + ) + args_joined = ", ".join(args) # Apply heuristic for breaking the lines diff --git a/dev/test_data/common_meta_models/list_of_classes.py b/dev/test_data/common_meta_models/list_of_classes.py index e43fb6404..a78e6db8c 100644 --- a/dev/test_data/common_meta_models/list_of_classes.py +++ b/dev/test_data/common_meta_models/list_of_classes.py @@ -1,5 +1,5 @@ from enum import Enum -from typing import List +from typing import List, Optional, Sequence from icontract import invariant @@ -17,6 +17,30 @@ def __init__(self, name: str) -> None: self.name = name +@verification +def items_are_some(items: Sequence[Abstract_item]) -> bool: + """Check a read-only list of base-class instances.""" + return all(isinstance(item, Some_item) for item in items) + + +@verification +def some_items_are_some(items: Sequence[Some_item]) -> bool: + """Pass a list of descendants to a base-class list parameter.""" + return items_are_some(items) + + +@verification +def optional_some_items_are_some(items: Optional[Sequence[Some_item]]) -> bool: + """Preserve an optional descendant list passed to an optional parameter.""" + return optional_items_are_some(items) + + +@verification +def optional_items_are_some(items: Optional[Sequence[Abstract_item]]) -> bool: + """Check a possibly missing read-only list of base-class instances.""" + return items is None or items_are_some(items) + + class Another_item(Abstract_item): serial_number: int diff --git a/dev/test_data/intermediate/common_meta_models/list_of_classes/expected_symbol_table.txt b/dev/test_data/intermediate/common_meta_models/list_of_classes/expected_symbol_table.txt index f7d0e0dcf..c61089224 100644 --- a/dev/test_data/intermediate/common_meta_models/list_of_classes/expected_symbol_table.txt +++ b/dev/test_data/intermediate/common_meta_models/list_of_classes/expected_symbol_table.txt @@ -398,7 +398,127 @@ SymbolTable( named_unions=[], constants=[], constants_by_name=..., - verification_functions=[], + verification_functions=[ + TranspilableVerification( + name='items_are_some', + visibility='PUBLIC', + arguments=[ + Argument( + name='items', + type_annotation=ListTypeAnnotation( + items=OurTypeAnnotation( + our_type='Reference to our type Abstract_item', + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check a read-only list of base-class instances.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='some_items_are_some', + visibility='PUBLIC', + arguments=[ + Argument( + name='items', + type_annotation=ListTypeAnnotation( + items=OurTypeAnnotation( + our_type='Reference to our type Some_item', + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Pass a list of descendants to a base-class list parameter.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='optional_some_items_are_some', + visibility='PUBLIC', + arguments=[ + Argument( + name='items', + type_annotation=OptionalTypeAnnotation( + value=ListTypeAnnotation( + items=OurTypeAnnotation( + our_type='Reference to our type Some_item', + parsed=...), + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Preserve an optional descendant list passed to an optional parameter.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='optional_items_are_some', + visibility='PUBLIC', + arguments=[ + Argument( + name='items', + type_annotation=OptionalTypeAnnotation( + value=ListTypeAnnotation( + items=OurTypeAnnotation( + our_type='Reference to our type Abstract_item', + parsed=...), + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check a possibly missing read-only list of base-class instances.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., + arguments_by_name=...)], verification_functions_by_name=..., meta_model=MetaModel( description=None, diff --git a/dev/test_data/main/cpp/expected/list_of_classes/expected_output/include/dummy/verification.hpp b/dev/test_data/main/cpp/expected/list_of_classes/expected_output/include/dummy/verification.hpp index 0dfe6262e..228ced3dc 100644 --- a/dev/test_data/main/cpp/expected/list_of_classes/expected_output/include/dummy/verification.hpp +++ b/dev/test_data/main/cpp/expected/list_of_classes/expected_output/include/dummy/verification.hpp @@ -212,6 +212,42 @@ class RecursiveVerification : public IVerification { const std::shared_ptr& instance_; }; // class RecursiveVerification +// region Verification functions + +/// \brief Check a read-only list of base-class instances. +bool ItemsAreSome( + const std::vector< + std::shared_ptr + >& items +); + +/// \brief Pass a list of descendants to a base-class list parameter. +bool SomeItemsAreSome( + const std::vector< + std::shared_ptr + >& items +); + +/// \brief Preserve an optional descendant list passed to an optional parameter. +bool OptionalSomeItemsAreSome( + const common::optional< + std::vector< + std::shared_ptr + > + >& items +); + +/// \brief Check a possibly missing read-only list of base-class instances. +bool OptionalItemsAreSome( + const common::optional< + std::vector< + std::shared_ptr + > + >& items +); + +// endregion Verification functions + } // namespace verification /**@}*/ diff --git a/dev/test_data/main/cpp/expected/list_of_classes/expected_output/src/verification.cpp b/dev/test_data/main/cpp/expected/list_of_classes/expected_output/src/verification.cpp index 40ac2d582..7a2e0161f 100644 --- a/dev/test_data/main/cpp/expected/list_of_classes/expected_output/src/verification.cpp +++ b/dev/test_data/main/cpp/expected/list_of_classes/expected_output/src/verification.cpp @@ -37,6 +37,68 @@ Error::Error( // endregion struct Error +// region Verification functions + +bool ItemsAreSome( + const std::vector< + std::shared_ptr + >& items +) { + return ( + common::All( + [&](const std::shared_ptr& item) -> bool { + return types::IsSomeItem(*item); + }, + items + ) + ); +} + +bool SomeItemsAreSome( + const std::vector< + std::shared_ptr + >& items +) { + return ( + ItemsAreSome( + items + ) + ); +} + +bool OptionalSomeItemsAreSome( + const common::optional< + std::vector< + std::shared_ptr + > + >& items +) { + return ( + OptionalItemsAreSome( + items + ) + ); +} + +bool OptionalItemsAreSome( + const common::optional< + std::vector< + std::shared_ptr + > + >& items +) { + return ( + ( + (!(items.has_value())) + || ItemsAreSome( + (*items) + ) + ) + ); +} + +// endregion Verification functions + namespace { /** diff --git a/dev/test_data/main/csharp/expected/list_of_classes/expected_output/dummy/verification.cs b/dev/test_data/main/csharp/expected/list_of_classes/expected_output/dummy/verification.cs index 014b3b7be..4b02182fc 100644 --- a/dev/test_data/main/csharp/expected/list_of_classes/expected_output/dummy/verification.cs +++ b/dev/test_data/main/csharp/expected/list_of_classes/expected_output/dummy/verification.cs @@ -31,6 +31,48 @@ namespace dummy /// public static class Verification { + /// + /// Check a read-only list of base-class instances. + /// + public static bool ItemsAreSome( + List items + ) + { + return items.All( + item => item is Our.ISomeItem); + } // public static bool ItemsAreSome + + /// + /// Pass a list of descendants to a base-class list parameter. + /// + public static bool SomeItemsAreSome( + List items + ) + { + return Verification.ItemsAreSome(items); + } // public static bool SomeItemsAreSome + + /// + /// Preserve an optional descendant list passed to an optional parameter. + /// + public static bool OptionalSomeItemsAreSome( + List? items + ) + { + return Verification.OptionalItemsAreSome(items); + } // public static bool OptionalSomeItemsAreSome + + /// + /// Check a possibly missing read-only list of base-class instances. + /// + public static bool OptionalItemsAreSome( + List? items + ) + { + return (items == null) + || Verification.ItemsAreSome(items); + } // public static bool OptionalItemsAreSome + /// /// Hash allowed enum values for efficient validation of enums. /// diff --git a/dev/test_data/main/golang/expected/list_of_classes/expected_output/verification/verification.go b/dev/test_data/main/golang/expected/list_of_classes/expected_output/verification/verification.go index 26a54b221..90f60efc8 100644 --- a/dev/test_data/main/golang/expected/list_of_classes/expected_output/verification/verification.go +++ b/dev/test_data/main/golang/expected/list_of_classes/expected_output/verification/verification.go @@ -12,6 +12,7 @@ package verification import ( "fmt" + ourcommon "github.com/dummy-works/dummy/common" ourreporting "github.com/dummy-works/dummy/reporting" ourtypes "github.com/dummy-works/dummy/types" ) @@ -44,6 +45,62 @@ func (ve *VerificationError) PathString() string { return ourreporting.ToGolangPath(ve.Path) } +// Check a read-only list of base-class instances. +func ItemsAreSome( + items []ourtypes.IAbstractItem, +) bool { + return ourcommon.All( + func(item ourtypes.IAbstractItem) bool { + return ourtypes.IsSomeItem(item) + }, + items, + ) +} + +// Pass a list of descendants to a base-class list parameter. +func SomeItemsAreSome( + items []ourtypes.ISomeItem, +) bool { + return ItemsAreSome( + func(items []ourtypes.ISomeItem) []ourtypes.IAbstractItem { + if items == nil { + return nil + } + result := make([]ourtypes.IAbstractItem, len(items)) + for i, item := range items { + result[i] = item + } + return result + }(items), + ) +} + +// Preserve an optional descendant list passed to an optional parameter. +func OptionalSomeItemsAreSome( + items []ourtypes.ISomeItem, +) bool { + return OptionalItemsAreSome( + func(items []ourtypes.ISomeItem) []ourtypes.IAbstractItem { + if items == nil { + return nil + } + result := make([]ourtypes.IAbstractItem, len(items)) + for i, item := range items { + result[i] = item + } + return result + }(items), + ) +} + +// Check a possibly missing read-only list of base-class instances. +func OptionalItemsAreSome( + items []ourtypes.IAbstractItem, +) bool { + return (items == nil) || + ItemsAreSome(items) +} + // Verify `that` instance of [ourtypes.ISomeItem]. // // You have to supply the callback `onError` to iterate over the errors. diff --git a/dev/test_data/main/java/expected/list_of_classes/expected_output/src/main/java/dummy/verification/Verification.java b/dev/test_data/main/java/expected/list_of_classes/expected_output/src/main/java/dummy/verification/Verification.java index 7beb43f66..5e27769f0 100644 --- a/dev/test_data/main/java/expected/list_of_classes/expected_output/src/main/java/dummy/verification/Verification.java +++ b/dev/test_data/main/java/expected/list_of_classes/expected_output/src/main/java/dummy/verification/Verification.java @@ -28,8 +28,43 @@ import dummy.types.model.*; import dummy.visitation.AbstractTransformer; import java.util.List; +import java.util.Optional; public class Verification { + /** + * Check a read-only list of base-class instances. + */ + public static Boolean itemsAreSome( + List items) { + return items.stream().allMatch( + item -> item instanceof ISomeItem); + } + + /** + * Pass a list of descendants to a base-class list parameter. + */ + public static Boolean someItemsAreSome( + List items) { + return itemsAreSome(items); + } + + /** + * Preserve an optional descendant list passed to an optional parameter. + */ + public static Boolean optionalSomeItemsAreSome( + Optional> items) { + return optionalItemsAreSome(items); + } + + /** + * Check a possibly missing read-only list of base-class instances. + */ + public static Boolean optionalItemsAreSome( + Optional> items) { + return (!items.isPresent()) + || itemsAreSome(items.orElse(null)); + } + /** * Hash allowed enum values for efficient validation of enums. */ diff --git a/dev/test_data/main/python/expected/list_of_classes/expected_output/dummy/verification.py b/dev/test_data/main/python/expected/list_of_classes/expected_output/dummy/verification.py index a68d63f87..5b328630e 100644 --- a/dev/test_data/main/python/expected/list_of_classes/expected_output/dummy/verification.py +++ b/dev/test_data/main/python/expected/list_of_classes/expected_output/dummy/verification.py @@ -62,6 +62,50 @@ Error = our_reporting.Error +def items_are_some( + items: Sequence[our_types.AbstractItem] +) -> bool: + """Check a read-only list of base-class instances.""" + # pylint: disable=all + return ( + all( + isinstance(item, our_types.SomeItem) + for item in items + )) + + +def some_items_are_some( + items: Sequence[our_types.SomeItem] +) -> bool: + """Pass a list of descendants to a base-class list parameter.""" + # pylint: disable=all + return items_are_some(items) + + +def optional_some_items_are_some( + items: Optional[Sequence[our_types.SomeItem]] +) -> bool: + """ + Preserve an optional descendant list passed to an optional parameter. + """ + # pylint: disable=all + return optional_items_are_some(items) + + +def optional_items_are_some( + items: Optional[Sequence[our_types.AbstractItem]] +) -> bool: + """ + Check a possibly missing read-only list of base-class instances. + """ + # pylint: disable=all + return ( + ( + (items is None) + or items_are_some(items) + )) + + class _Transformer( our_types.AbstractTransformer[ Iterator[Error] diff --git a/dev/test_data/main/typescript/expected/list_of_classes/expected_output/src/verification.ts b/dev/test_data/main/typescript/expected/list_of_classes/expected_output/src/verification.ts index 2538f6bcf..20a87e801 100644 --- a/dev/test_data/main/typescript/expected/list_of_classes/expected_output/src/verification.ts +++ b/dev/test_data/main/typescript/expected/list_of_classes/expected_output/src/verification.ts @@ -189,6 +189,51 @@ export class VerificationError { } } +/** + * Check a read-only list of base-class instances. + */ +export function itemsAreSome( + items: Array +): boolean { + return OurCommon.every( + OurCommon.map( + items, + item => + OurTypes.isSomeItem(item) + ) + ); +} + +/** + * Pass a list of descendants to a base-class list parameter. + */ +export function someItemsAreSome( + items: Array +): boolean { + return itemsAreSome(items); +} + +/** + * Preserve an optional descendant list passed to an optional parameter. + */ +export function optionalSomeItemsAreSome( + items: Array | null +): boolean { + return optionalItemsAreSome(items); +} + +/** + * Check a possibly missing read-only list of base-class instances. + */ +export function optionalItemsAreSome( + items: Array | null +): boolean { + return ( + (items === null) + || itemsAreSome(items) + ); +} + /** * Verify the items of `that` recursively. */ diff --git a/dev/test_data/parse/common_meta_models/list_of_classes/expected_symbol_table.txt b/dev/test_data/parse/common_meta_models/list_of_classes/expected_symbol_table.txt index 891d433fe..e8a7516ae 100644 --- a/dev/test_data/parse/common_meta_models/list_of_classes/expected_symbol_table.txt +++ b/dev/test_data/parse/common_meta_models/list_of_classes/expected_symbol_table.txt @@ -252,7 +252,195 @@ UnverifiedSymbolTable( methods_by_name=...)], named_unions=[], constants=[], - verification_functions=[], + verification_functions=[ + UnderstoodMethod( + name='items_are_some', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='items', + type_annotation=SubscriptedTypeAnnotation( + identifier='Sequence', + subscripts=[ + AtomicTypeAnnotation( + identifier='Abstract_item', + node=...)], + node=...), + default=None, + node=...)], + returns=AtomicTypeAnnotation( + identifier='bool', + node=...), + description=Description( + document=..., + node=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + non_mutating=False, + body=[ + textwrap.dedent("""\ + Return( + value=All( + generator=ForEach( + variable=Name( + identifier='item', + original_node=...), + iteration=Name( + identifier='items', + original_node=...), + original_node=...), + condition=IsInstance( + value=Name( + identifier='item', + original_node=...), + classes=[ + Name( + identifier='Some_item', + original_node=...)], + original_node=...), + original_node=...), + original_node=...)""")], + node=..., + arguments_by_name=...), + UnderstoodMethod( + name='some_items_are_some', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='items', + type_annotation=SubscriptedTypeAnnotation( + identifier='Sequence', + subscripts=[ + AtomicTypeAnnotation( + identifier='Some_item', + node=...)], + node=...), + default=None, + node=...)], + returns=AtomicTypeAnnotation( + identifier='bool', + node=...), + description=Description( + document=..., + node=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + non_mutating=False, + body=[ + textwrap.dedent("""\ + Return( + value=FunctionCall( + name='items_are_some', + args=[ + Name( + identifier='items', + original_node=...)], + original_node=...), + original_node=...)""")], + node=..., + arguments_by_name=...), + UnderstoodMethod( + name='optional_some_items_are_some', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='items', + type_annotation=SubscriptedTypeAnnotation( + identifier='Optional', + subscripts=[ + SubscriptedTypeAnnotation( + identifier='Sequence', + subscripts=[ + AtomicTypeAnnotation( + identifier='Some_item', + node=...)], + node=...)], + node=...), + default=None, + node=...)], + returns=AtomicTypeAnnotation( + identifier='bool', + node=...), + description=Description( + document=..., + node=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + non_mutating=False, + body=[ + textwrap.dedent("""\ + Return( + value=FunctionCall( + name='optional_items_are_some', + args=[ + Name( + identifier='items', + original_node=...)], + original_node=...), + original_node=...)""")], + node=..., + arguments_by_name=...), + UnderstoodMethod( + name='optional_items_are_some', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='items', + type_annotation=SubscriptedTypeAnnotation( + identifier='Optional', + subscripts=[ + SubscriptedTypeAnnotation( + identifier='Sequence', + subscripts=[ + AtomicTypeAnnotation( + identifier='Abstract_item', + node=...)], + node=...)], + node=...), + default=None, + node=...)], + returns=AtomicTypeAnnotation( + identifier='bool', + node=...), + description=Description( + document=..., + node=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + non_mutating=False, + body=[ + textwrap.dedent("""\ + Return( + value=Or( + values=[ + IsNone( + value=Name( + identifier='items', + original_node=...), + original_node=...), + FunctionCall( + name='items_are_some', + args=[ + Name( + identifier='items', + original_node=...)], + original_node=...)], + original_node=...), + original_node=...)""")], + node=..., + arguments_by_name=...)], meta_model=MetaModel( description=None, version='dummy',