diff --git a/aas_core_codegen/cpp/verification/_generate.py b/aas_core_codegen/cpp/verification/_generate.py index ff68d92ea..0cdc50161 100644 --- a/aas_core_codegen/cpp/verification/_generate.py +++ b/aas_core_codegen/cpp/verification/_generate.py @@ -1081,26 +1081,22 @@ def _transpile_class_invariant( environment: intermediate_type_inference.Environment, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Translate the invariant from the meta-model into a C++ condition.""" - canonicalizer = intermediate_type_inference.Canonicalizer() - _ = canonicalizer.transform(invariant.body) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment, - representation_map=canonicalizer.representation_map, + # fmt: off + type_map, inference_error = ( + intermediate_type_inference.infer_for_invariant( + invariant=invariant, + environment=environment + ) ) + # fmt: on - _ = type_inferrer.transform(invariant.body) + if inference_error is not None: + return None, inference_error - if len(type_inferrer.errors): - return None, Error( - invariant.parsed.node, - "Failed to infer the types in the invariant", - type_inferrer.errors, - ) + assert type_map is not None optional_inferrer = cpp_optionaling.Inferrer( - environment=environment, type_map=type_inferrer.type_map + environment=environment, type_map=type_map ) _ = optional_inferrer.transform(invariant.body) @@ -1114,7 +1110,7 @@ def _transpile_class_invariant( ) transpiler = _ClassInvariantTranspiler( - type_map=type_inferrer.type_map, + type_map=type_map, is_optional_map=optional_inferrer.is_optional_map, environment=environment, symbol_table=symbol_table, @@ -2111,40 +2107,23 @@ def _generate_implementation_of_transpilable_verification( base_environment: intermediate_type_inference.Environment, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Transpile the verification to a function implementation.""" - canonicalizer = intermediate_type_inference.Canonicalizer() - for node in verification.parsed.body: - _ = canonicalizer.transform(node) - - environment = intermediate_type_inference.MutableEnvironment( - parent=base_environment - ) - for arg in verification.arguments: - environment.set( - identifier=arg.name, - type_annotation=intermediate_type_inference.convert_type_annotation( - arg.type_annotation - ), + # fmt: off + type_inference, inference_error = ( + intermediate_type_inference.infer_for_verification( + verification=verification, + base_environment=base_environment ) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment, - representation_map=canonicalizer.representation_map, ) + # fmt: on - for node in verification.parsed.body: - _ = type_inferrer.transform(node) + if inference_error is not None: + return None, inference_error - if len(type_inferrer.errors): - return None, Error( - verification.parsed.node, - f"Failed to infer the types " - f"in the verification function {verification.name!r}", - type_inferrer.errors, - ) + assert type_inference is not None optional_inferrer = cpp_optionaling.Inferrer( - environment=environment, type_map=type_inferrer.type_map + environment=type_inference.environment_with_args, + type_map=type_inference.type_map, ) for node in verification.parsed.body: _ = optional_inferrer.transform(node) @@ -2158,9 +2137,9 @@ def _generate_implementation_of_transpilable_verification( ) transpiler = _TranspilableVerificationTranspiler( - type_map=type_inferrer.type_map, + type_map=type_inference.type_map, is_optional_map=optional_inferrer.is_optional_map, - environment=environment, + environment=type_inference.environment_with_args, symbol_table=symbol_table, verification=verification, ) @@ -2398,26 +2377,22 @@ def _transpile_constrained_primitive_invariant( constrained_primitive: intermediate.ConstrainedPrimitive, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Translate the invariant from the meta-model into a C++ condition.""" - canonicalizer = intermediate_type_inference.Canonicalizer() - _ = canonicalizer.transform(invariant.body) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment, - representation_map=canonicalizer.representation_map, + # fmt: off + type_map, inference_error = ( + intermediate_type_inference.infer_for_invariant( + invariant=invariant, + environment=environment + ) ) + # fmt: on - _ = type_inferrer.transform(invariant.body) + if inference_error is not None: + return None, inference_error - if len(type_inferrer.errors): - return None, Error( - invariant.parsed.node, - "Failed to infer the types in the invariant", - type_inferrer.errors, - ) + assert type_map is not None optional_inferrer = cpp_optionaling.Inferrer( - environment=environment, type_map=type_inferrer.type_map + environment=environment, type_map=type_map ) _ = optional_inferrer.transform(invariant.body) @@ -2431,7 +2406,7 @@ def _transpile_constrained_primitive_invariant( ) transpiler = _ConstrainedPrimitiveInvariantTranspiler( - type_map=type_inferrer.type_map, + type_map=type_map, is_optional_map=optional_inferrer.is_optional_map, environment=environment, symbol_table=symbol_table, diff --git a/aas_core_codegen/csharp/verification/_generate.py b/aas_core_codegen/csharp/verification/_generate.py index 5a3c3f46f..ba123ecfc 100644 --- a/aas_core_codegen/csharp/verification/_generate.py +++ b/aas_core_codegen/csharp/verification/_generate.py @@ -82,7 +82,7 @@ def __init__(self, defined_variables: Set[Identifier]) -> None: """ Initialize with the given values. - The ``initialized_variables`` are shared between different statement + The ``defined_variables`` are shared between different statement transpilations. It is also mutated when assignments are transpiled. We need to keep track of variables so that we know when we have to define them, and when we can simply assign them a value, if they have been already defined. @@ -427,41 +427,23 @@ def _transpile_transpilable_verification( environment: intermediate_type_inference.Environment, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Transpile a verification function.""" - canonicalizer = intermediate_type_inference.Canonicalizer() - for node in verification.parsed.body: - _ = canonicalizer.transform(node) - - environment_with_args = intermediate_type_inference.MutableEnvironment( - parent=environment - ) - for arg in verification.arguments: - environment_with_args.set( - identifier=arg.name, - type_annotation=intermediate_type_inference.convert_type_annotation( - arg.type_annotation - ), + # fmt: off + type_inference, error = ( + intermediate_type_inference.infer_for_verification( + verification=verification, + base_environment=environment ) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment_with_args, - representation_map=canonicalizer.representation_map, ) + # fmt: on - for node in verification.parsed.body: - _ = type_inferrer.transform(node) + if error is not None: + return None, error - if len(type_inferrer.errors): - return None, Error( - verification.parsed.node, - f"Failed to infer the types " - f"in the verification function {verification.name!r}", - type_inferrer.errors, - ) + assert type_inference is not None transpiler = _TranspilableVerificationTranspiler( - type_map=type_inferrer.type_map, - environment=environment_with_args, + type_map=type_inference.type_map, + environment=type_inference.environment_with_args, symbol_table=symbol_table, verification=verification, ) @@ -598,35 +580,22 @@ def _transpile_invariant( environment: intermediate_type_inference.Environment, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Translate the invariant from the meta-model into C# code.""" - # NOTE (mristin, 2021-10-24): - # We manually transpile the invariant from our custom syntax without additional - # semantic analysis in the :py:mod:`aas_core_codegen.intermediate` layer. - # - # While this might seem repetitive ("unDRY"), we are still not sure about - # the appropriate abstraction. After we implement the code generation for a couple - # of languages, we hope to have a much better understanding about the necessary - # abstractions. - - canonicalizer = intermediate_type_inference.Canonicalizer() - _ = canonicalizer.transform(invariant.body) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment, - representation_map=canonicalizer.representation_map, + # fmt: off + type_map, inference_error = ( + intermediate_type_inference.infer_for_invariant( + invariant=invariant, + environment=environment + ) ) + # fmt: on - _ = type_inferrer.transform(invariant.body) + if inference_error is not None: + return None, inference_error - if len(type_inferrer.errors): - return None, Error( - invariant.parsed.node, - "Failed to infer the types in the invariant", - type_inferrer.errors, - ) + assert type_map is not None transpiler = _InvariantTranspiler( - type_map=type_inferrer.type_map, + type_map=type_map, environment=environment, symbol_table=symbol_table, ) diff --git a/aas_core_codegen/golang/verification/_generate.py b/aas_core_codegen/golang/verification/_generate.py index 5511ed829..dd2b098e7 100644 --- a/aas_core_codegen/golang/verification/_generate.py +++ b/aas_core_codegen/golang/verification/_generate.py @@ -485,40 +485,23 @@ def _transpile_transpilable_verification( environment: intermediate_type_inference.Environment, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Transpile a verification function.""" - canonicalizer = intermediate_type_inference.Canonicalizer() - for node in verification.parsed.body: - _ = canonicalizer.transform(node) - - environment_with_args = intermediate_type_inference.MutableEnvironment( - parent=environment - ) - for arg in verification.arguments: - environment_with_args.set( - identifier=arg.name, - type_annotation=intermediate_type_inference.convert_type_annotation( - arg.type_annotation - ), + # fmt: off + type_inference, error = ( + intermediate_type_inference.infer_for_verification( + verification=verification, + base_environment=environment ) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment_with_args, - representation_map=canonicalizer.representation_map, ) + # fmt: on - for node in verification.parsed.body: - _ = type_inferrer.transform(node) + if error is not None: + return None, error - if len(type_inferrer.errors): - return None, Error( - verification.parsed.node, - f"Failed to infer the types " - f"in the verification function {verification.name!r}", - type_inferrer.errors, - ) + assert type_inference is not None pointer_inferrer = golang_pointering.Inferrer( - environment=environment_with_args, type_map=type_inferrer.type_map + environment=type_inference.environment_with_args, + type_map=type_inference.type_map, ) for node in verification.parsed.body: @@ -533,9 +516,9 @@ def _transpile_transpilable_verification( ) transpiler = _TranspilableVerificationTranspiler( - type_map=type_inferrer.type_map, + type_map=type_inference.type_map, is_pointer_map=pointer_inferrer.is_pointer_map, - environment=environment_with_args, + environment=type_inference.environment_with_args, symbol_table=symbol_table, verification=verification, ) @@ -693,26 +676,22 @@ def _transpile_invariant( environment: intermediate_type_inference.Environment, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Translate the invariant from the meta-model into Golang code.""" - canonicalizer = intermediate_type_inference.Canonicalizer() - _ = canonicalizer.transform(invariant.body) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment, - representation_map=canonicalizer.representation_map, + # fmt: off + type_map, inference_error = ( + intermediate_type_inference.infer_for_invariant( + invariant=invariant, + environment=environment + ) ) + # fmt: on - _ = type_inferrer.transform(invariant.body) + if inference_error is not None: + return None, inference_error - if len(type_inferrer.errors): - return None, Error( - invariant.parsed.node, - "Failed to infer the types in the invariant", - type_inferrer.errors, - ) + assert type_map is not None pointer_inferrer = golang_pointering.Inferrer( - environment=environment, type_map=type_inferrer.type_map + environment=environment, type_map=type_map ) _ = pointer_inferrer.transform(invariant.body) @@ -725,7 +704,7 @@ def _transpile_invariant( ) transpiler = _InvariantTranspiler( - type_map=type_inferrer.type_map, + type_map=type_map, is_pointer_map=pointer_inferrer.is_pointer_map, environment=environment, symbol_table=symbol_table, diff --git a/aas_core_codegen/intermediate/type_inference.py b/aas_core_codegen/intermediate/type_inference.py index fdcc3997a..85a39f0c3 100644 --- a/aas_core_codegen/intermediate/type_inference.py +++ b/aas_core_codegen/intermediate/type_inference.py @@ -11,7 +11,16 @@ import abc import contextlib import enum -from typing import Mapping, MutableMapping, Optional, List, Final, Union, get_args +from typing import ( + Mapping, + MutableMapping, + Optional, + List, + Final, + Union, + get_args, + Tuple, +) from icontract import DBC, ensure, require @@ -557,7 +566,7 @@ def remove(self, identifier: Identifier) -> None: del self._mapping[identifier] -class Canonicalizer(parse_tree.RestrictedTransformer[str]): +class _Canonicalizer(parse_tree.RestrictedTransformer[str]): """Represent the nodes as canonical strings so that they can be used in look-ups.""" #: Track of the canonical representations @@ -596,7 +605,7 @@ def _needs_no_brackets(node: parse_tree.Node) -> bool: def transform_member(self, node: parse_tree.Member) -> str: instance_repr = self.transform(node.instance) - if Canonicalizer._needs_no_brackets(node.instance): + if _Canonicalizer._needs_no_brackets(node.instance): result = f"{instance_repr}.{node.name}" else: result = f"({instance_repr}).{node.name}" @@ -608,7 +617,7 @@ def transform_index(self, node: parse_tree.Index) -> str: collection_repr = self.transform(node.collection) index_repr = self.transform(node.index) - if Canonicalizer._needs_no_brackets(node.collection): + if _Canonicalizer._needs_no_brackets(node.collection): result = f"{collection_repr}[{index_repr}]" else: result = f"({collection_repr})[{index_repr}]" @@ -618,11 +627,11 @@ def transform_index(self, node: parse_tree.Index) -> str: def transform_comparison(self, node: parse_tree.Comparison) -> str: left = self.transform(node.left) - if not Canonicalizer._needs_no_brackets(node.left): + if not _Canonicalizer._needs_no_brackets(node.left): left = f"({left})" right = self.transform(node.right) - if not Canonicalizer._needs_no_brackets(node.right): + if not _Canonicalizer._needs_no_brackets(node.right): right = f"({right})" result = f"{left} {node.op.value} {right}" @@ -631,11 +640,11 @@ def transform_comparison(self, node: parse_tree.Comparison) -> str: def transform_is_in(self, node: parse_tree.IsIn) -> str: member = self.transform(node.member) - if not Canonicalizer._needs_no_brackets(node.member): + if not _Canonicalizer._needs_no_brackets(node.member): member = f"({member})" container = self.transform(node.container) - if not Canonicalizer._needs_no_brackets(node.container): + if not _Canonicalizer._needs_no_brackets(node.container): container = f"({container})" result = f"{member} in {container}" @@ -644,11 +653,11 @@ def transform_is_in(self, node: parse_tree.IsIn) -> str: def transform_implication(self, node: parse_tree.Implication) -> str: antecedent = self.transform(node.antecedent) - if not Canonicalizer._needs_no_brackets(node.antecedent): + if not _Canonicalizer._needs_no_brackets(node.antecedent): antecedent = f"({antecedent})" consequent = self.transform(node.consequent) - if not Canonicalizer._needs_no_brackets(node.consequent): + if not _Canonicalizer._needs_no_brackets(node.consequent): consequent = f"({consequent})" result = f"{antecedent} ⇒ {consequent}" @@ -682,7 +691,7 @@ def transform_constant(self, node: parse_tree.Constant) -> str: def transform_is_none(self, node: parse_tree.IsNone) -> str: value = self.transform(node.value) - if not Canonicalizer._needs_no_brackets(node.value): + if not _Canonicalizer._needs_no_brackets(node.value): value = f"({value})" result = f"{value} is None" @@ -691,7 +700,7 @@ def transform_is_none(self, node: parse_tree.IsNone) -> str: def transform_is_not_none(self, node: parse_tree.IsNotNone) -> str: value = self.transform(node.value) - if not Canonicalizer._needs_no_brackets(node.value): + if not _Canonicalizer._needs_no_brackets(node.value): value = f"({value})" result = f"{value} is not None" @@ -706,7 +715,7 @@ def transform_name(self, node: parse_tree.Name) -> str: def transform_not(self, node: parse_tree.Not) -> str: operand_repr = self.transform(node.operand) - if not Canonicalizer._needs_no_brackets(node): + if not _Canonicalizer._needs_no_brackets(node): operand_repr = f"({operand_repr})" result = f"not {operand_repr}" @@ -717,7 +726,7 @@ def transform_and(self, node: parse_tree.And) -> str: values = [] # type: List[str] for value_node in node.values: value = self.transform(value_node) - if not Canonicalizer._needs_no_brackets(value_node): + if not _Canonicalizer._needs_no_brackets(value_node): value = f"({value})" values.append(value) @@ -730,7 +739,7 @@ def transform_or(self, node: parse_tree.Or) -> str: values = [] # type: List[str] for value_node in node.values: value = self.transform(value_node) - if not Canonicalizer._needs_no_brackets(value_node): + if not _Canonicalizer._needs_no_brackets(value_node): value = f"({value})" values.append(value) @@ -741,11 +750,11 @@ def transform_or(self, node: parse_tree.Or) -> str: def _transform_add_or_sub(self, node: Union[parse_tree.Add, parse_tree.Sub]) -> str: left_repr = self.transform(node.left) - if not Canonicalizer._needs_no_brackets(node.left): + if not _Canonicalizer._needs_no_brackets(node.left): left_repr = f"({left_repr})" right_repr = self.transform(node.right) - if not Canonicalizer._needs_no_brackets(node.right): + if not _Canonicalizer._needs_no_brackets(node.right): right_repr = f"({right_repr})" result: str @@ -788,7 +797,7 @@ def transform_joined_str(self, node: parse_tree.JoinedStr) -> str: def transform_for_each(self, node: parse_tree.ForEach) -> str: variable = self.transform(node.variable) iteration = self.transform(node.iteration) - if not Canonicalizer._needs_no_brackets(node.iteration): + if not _Canonicalizer._needs_no_brackets(node.iteration): iteration = f"({iteration})" result = f"for {variable} in {iteration}" @@ -808,7 +817,7 @@ def _transform_any_or_all(self, node: Union[parse_tree.Any, parse_tree.All]) -> generator = self.transform(node.generator) condition = self.transform(node.condition) - if not Canonicalizer._needs_no_brackets(node.condition): + if not _Canonicalizer._needs_no_brackets(node.condition): condition = f"({condition})" result: str @@ -831,7 +840,7 @@ def transform_all(self, node: parse_tree.All) -> str: def transform_assignment(self, node: parse_tree.Assignment) -> str: target = self.transform(node.target) - if not Canonicalizer._needs_no_brackets(node.target): + if not _Canonicalizer._needs_no_brackets(node.target): target = f"({target})" # NOTE (mristin, 2022-06-17): @@ -927,7 +936,7 @@ def decrement(self, key: str) -> None: ] -class Inferrer(parse_tree.RestrictedTransformer[Optional["TypeAnnotationUnion"]]): +class _Inferrer(parse_tree.RestrictedTransformer[Optional["TypeAnnotationUnion"]]): """ Infer the types of the given parse tree. @@ -944,13 +953,10 @@ class Inferrer(parse_tree.RestrictedTransformer[Optional["TypeAnnotationUnion"]] def __init__( self, - symbol_table: _types.SymbolTable, environment: "Environment", representation_map: Mapping[parse_tree.Node, str], ) -> None: """Initialize with the given values.""" - self._symbol_table = symbol_table - # We need to create our own child environment so that we can introduce new # entries without affecting the variables from the outer scopes. self._environment = MutableEnvironment(parent=environment) @@ -1688,7 +1694,7 @@ def _transform_add_or_sub( self.errors.append( Error( node.left.original_node, - f"{Inferrer._binary_operation_name_with_capital_the(node)} is " + f"{_Inferrer._binary_operation_name_with_capital_the(node)} is " f"only defined on integer and floating-point numbers, " f"but got as a left operand: {left_type}", ) @@ -1707,7 +1713,7 @@ def _transform_add_or_sub( self.errors.append( Error( node.right.original_node, - f"{Inferrer._binary_operation_name_with_capital_the(node)} is " + f"{_Inferrer._binary_operation_name_with_capital_the(node)} is " f"only defined on integer and floating-point numbers, " f"but got as a right operand: {right_type}", ) @@ -2122,6 +2128,92 @@ def populate_base_environment(symbol_table: _types.SymbolTable) -> Environment: return ImmutableEnvironment(mapping=mapping, parent=None) +class InferenceOfFunction: + """Represent the result of type inference on a function body and arguments.""" + + #: Environment inferred after processing a body of statements including + #: the function arguments + environment_with_args: Final[Environment] + + #: Map of body nodes to types + type_map: Final[Mapping[parse_tree.Node, "TypeAnnotationUnion"]] + + def __init__( + self, + environment_with_args: Environment, + type_map: Mapping[parse_tree.Node, "TypeAnnotationUnion"], + ) -> None: + """Initialize with the given values.""" + self.environment_with_args = environment_with_args + self.type_map = type_map + + +@ensure(lambda result: (result[0] is not None) ^ (result[1] is not None)) +def infer_for_verification( + verification: _types.TranspilableVerification, base_environment: Environment +) -> Tuple[Optional[InferenceOfFunction], Optional[Error]]: + """Infer the types for the given function and map the body nodes to the types.""" + canonicalizer = _Canonicalizer() + for node in verification.parsed.body: + _ = canonicalizer.transform(node) + + environment = MutableEnvironment(parent=base_environment) + + for arg in verification.arguments: + environment.set( + identifier=arg.name, + type_annotation=convert_type_annotation(arg.type_annotation), + ) + + type_inferrer = _Inferrer( + environment=environment, + representation_map=canonicalizer.representation_map, + ) + + for node in verification.parsed.body: + _ = type_inferrer.transform(node) + + if len(type_inferrer.errors): + return None, Error( + verification.parsed.node, + f"Failed to infer the types " + f"in the verification function {verification.name!r}", + type_inferrer.errors, + ) + + return ( + InferenceOfFunction( + environment_with_args=environment, type_map=type_inferrer.type_map + ), + None, + ) + + +@ensure(lambda result: (result[0] is not None) ^ (result[1] is not None)) +def infer_for_invariant( + invariant: _types.Invariant, environment: Environment +) -> Tuple[Optional[Mapping[parse_tree.Node, "TypeAnnotationUnion"]], Optional[Error]]: + """Infer the types of the nodes corresponding to the body of an invariant.""" + canonicalizer = _Canonicalizer() + _ = canonicalizer.transform(invariant.body) + + type_inferrer = _Inferrer( + environment=environment, + representation_map=canonicalizer.representation_map, + ) + + _ = type_inferrer.transform(invariant.body) + + if len(type_inferrer.errors): + return None, Error( + invariant.parsed.node, + "Failed to infer the types in the invariant", + type_inferrer.errors, + ) + + return type_inferrer.type_map, None + + assert_union_of_descendants_exhaustive( union=TypeAnnotationUnion, base_class=TypeAnnotation ) diff --git a/aas_core_codegen/java/optional.py b/aas_core_codegen/java/optional.py index 1b97ede49..e9a98bc46 100644 --- a/aas_core_codegen/java/optional.py +++ b/aas_core_codegen/java/optional.py @@ -1,6 +1,6 @@ """This module provides an inferrer to resolve optional type information.""" -from typing import Final, List, MutableMapping, Optional, Union +from typing import Final, List, MutableMapping, Optional, Union, Mapping from aas_core_codegen import intermediate from aas_core_codegen.common import ( @@ -38,7 +38,7 @@ class OptionalInferrer(parse_tree.Transformer[Optional[Error]]): def __init__( self, environment: intermediate_type_inference.Environment, - type_map: MutableMapping[ + type_map: Mapping[ parse_tree.Node, intermediate_type_inference.TypeAnnotationUnion ], ) -> None: diff --git a/aas_core_codegen/java/verification/_generate.py b/aas_core_codegen/java/verification/_generate.py index 67970d84b..44af4239b 100644 --- a/aas_core_codegen/java/verification/_generate.py +++ b/aas_core_codegen/java/verification/_generate.py @@ -4,7 +4,6 @@ from typing import ( List, Mapping, - MutableMapping, Optional, Sequence, Set, @@ -27,6 +26,9 @@ Stripped, wrap_text_into_lines, ) +from aas_core_codegen.intermediate import ( + type_inference as intermediate_type_inference, +) from aas_core_codegen.java import ( common as java_common, description as java_description, @@ -42,11 +44,9 @@ INDENT5 as IIIII, INDENT6 as IIIIII, ) -from aas_core_codegen.intermediate import ( - type_inference as intermediate_type_inference, -) from aas_core_codegen.parse import tree as parse_tree, retree as parse_retree + # region Verify @@ -113,13 +113,7 @@ class _PatternVerificationTranspiler( ): """Transpile a statement of a pattern verification into Java.""" - def __init__( - self, - defined_variables: Set[Identifier], - type_map: MutableMapping[ - parse_tree.Node, "intermediate_type_inference.TypeAnnotationUnion" - ], - ) -> None: + def __init__(self, defined_variables: Set[Identifier]) -> None: """ Initialize with the given values. @@ -129,7 +123,6 @@ def __init__( we can simply assign them a value, if they have been already defined. """ self.defined_variables = defined_variables - self.type_map = type_map @ensure(lambda result: (result[0] is not None) ^ (result[1] is not None)) def _transform_joined_str_values( @@ -246,59 +239,20 @@ def transform_assignment( else: self.defined_variables.add(node.target.identifier) - stmt_type = self.type_map.get(node.value) - - assert stmt_type is not None + # NOTE (mristin): + # We assume here that we checked in the parse stage that all the variables + # used in a pattern verification function are actually typed as strings. - type_anno, error = java_transpilation.generate_type(stmt_type) - if error is not None: - return None, error - assert type_anno is not None - - return Stripped(f"{type_anno} {variable} = {code};"), None + return Stripped(f"String {variable} = {code};"), None @ensure(lambda result: (result[0] is not None) ^ (result[1] is not None)) def _transpile_pattern_verification( verification: intermediate.PatternVerification, - symbol_table: intermediate.SymbolTable, - environment: intermediate_type_inference.Environment, package: java_common.PackageIdentifier, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Generate the verification function that checks the regular expressions.""" # We assume that we performed all the checks at the intermediate stage. - canonicalizer = intermediate_type_inference.Canonicalizer() - for node in verification.parsed.body: - _ = canonicalizer.transform(node) - - environment_with_args = intermediate_type_inference.MutableEnvironment( - parent=environment - ) - for arg in verification.arguments: - environment_with_args.set( - identifier=arg.name, - type_annotation=intermediate_type_inference.convert_type_annotation( - arg.type_annotation - ), - ) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment_with_args, - representation_map=canonicalizer.representation_map, - ) - - for node in verification.parsed.body: - if isinstance(node, parse_tree.Assignment): - _ = type_inferrer.transform(node) - - if len(type_inferrer.errors): - return None, Error( - verification.parsed.node, - f"Failed to infer the types " - f"in the verification function {verification.name!r}", - type_inferrer.errors, - ) construct_name = java_naming.private_method_name( Identifier(f"construct_{verification.name}") @@ -316,10 +270,7 @@ def _transpile_pattern_verification( ) defined_variables = set() # type: Set[Identifier] - transpiler = _PatternVerificationTranspiler( - defined_variables=defined_variables, - type_map=type_inferrer.type_map, - ) + transpiler = _PatternVerificationTranspiler(defined_variables=defined_variables) for i, stmt in enumerate(verification.parsed.body): if i == len(verification.parsed.body) - 1: @@ -495,41 +446,23 @@ def _transpile_transpilable_verification( The ``package`` defines the root Java package. """ - canonicalizer = intermediate_type_inference.Canonicalizer() - for node in verification.parsed.body: - _ = canonicalizer.transform(node) - - environment_with_args = intermediate_type_inference.MutableEnvironment( - parent=environment - ) - for arg in verification.arguments: - environment_with_args.set( - identifier=arg.name, - type_annotation=intermediate_type_inference.convert_type_annotation( - arg.type_annotation - ), + # fmt: off + type_inference, error = ( + intermediate_type_inference.infer_for_verification( + verification=verification, + base_environment=environment ) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment_with_args, - representation_map=canonicalizer.representation_map, ) + # fmt: on - for node in verification.parsed.body: - _ = type_inferrer.transform(node) + if error is not None: + return None, error - if len(type_inferrer.errors): - return None, Error( - verification.parsed.node, - f"Failed to infer the types " - f"in the verification function {verification.name!r}", - type_inferrer.errors, - ) + assert type_inference is not None optional_inferrer = java_optional.OptionalInferrer( - environment=environment_with_args, - type_map=type_inferrer.type_map, + environment=type_inference.environment_with_args, + type_map=type_inference.type_map, ) for node in verification.parsed.body: @@ -544,9 +477,9 @@ def _transpile_transpilable_verification( ) transpiler = _TranspilableVerificationTranspiler( - type_map=type_inferrer.type_map, + type_map=type_inference.type_map, is_optional_map=optional_inferrer.is_optional_map, - environment=environment_with_args, + environment=type_inference.environment_with_args, symbol_table=symbol_table, verification=verification, ) @@ -751,36 +684,23 @@ def _transpile_invariant( environment: intermediate_type_inference.Environment, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Translate the invariant from the meta-model into C# code.""" - # NOTE (empwilli, 2024-01-22): - # We manually transpile the invariant from our custom syntax without additional - # semantic analysis in the :py:mod:`aas_core_codegen.intermediate` layer. - # - # While this might seem repetitive ("unDRY"), we are still not sure about - # the appropriate abstraction. After we implement the code generation for a couple - # of languages, we hope to have a much better understanding about the necessary - # abstractions. - - canonicalizer = intermediate_type_inference.Canonicalizer() - _ = canonicalizer.transform(invariant.body) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment, - representation_map=canonicalizer.representation_map, + # fmt: off + type_map, inference_error = ( + intermediate_type_inference.infer_for_invariant( + invariant=invariant, + environment=environment + ) ) + # fmt: on - _ = type_inferrer.transform(invariant.body) + if inference_error is not None: + return None, inference_error - if len(type_inferrer.errors): - return None, Error( - invariant.parsed.node, - "Failed to infer the types in the invariant", - type_inferrer.errors, - ) + assert type_map is not None optional_inferrer = java_optional.OptionalInferrer( environment=environment, - type_map=type_inferrer.type_map, + type_map=type_map, ) _ = optional_inferrer.transform(invariant.body) @@ -793,7 +713,7 @@ def _transpile_invariant( ) transpiler = _InvariantTranspiler( - type_map=type_inferrer.type_map, + type_map=type_map, is_optional_map=optional_inferrer.is_optional_map, environment=environment, symbol_table=symbol_table, @@ -1352,8 +1272,6 @@ def generate( elif isinstance(verification, intermediate.PatternVerification): implementation, error = _transpile_pattern_verification( verification=verification, - symbol_table=symbol_table, - environment=base_environment, package=package, ) diff --git a/aas_core_codegen/python/verification/_generate.py b/aas_core_codegen/python/verification/_generate.py index 8696866c3..522e1ac21 100644 --- a/aas_core_codegen/python/verification/_generate.py +++ b/aas_core_codegen/python/verification/_generate.py @@ -444,41 +444,23 @@ def _transpile_transpilable_verification( aas_module: python_common.QualifiedModuleName, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Transpile a verification function.""" - canonicalizer = intermediate_type_inference.Canonicalizer() - for node in verification.parsed.body: - _ = canonicalizer.transform(node) - - environment_with_args = intermediate_type_inference.MutableEnvironment( - parent=environment - ) - for arg in verification.arguments: - environment_with_args.set( - identifier=arg.name, - type_annotation=intermediate_type_inference.convert_type_annotation( - arg.type_annotation - ), + # fmt: off + type_inference, error = ( + intermediate_type_inference.infer_for_verification( + verification=verification, + base_environment=environment ) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment_with_args, - representation_map=canonicalizer.representation_map, ) + # fmt: on - for node in verification.parsed.body: - _ = type_inferrer.transform(node) + if error is not None: + return None, error - if len(type_inferrer.errors): - return None, Error( - verification.parsed.node, - f"Failed to infer the types " - f"in the verification function {verification.name!r}", - type_inferrer.errors, - ) + assert type_inference is not None transpiler = _TranspilableVerificationTranspiler( - type_map=type_inferrer.type_map, - environment=environment_with_args, + type_map=type_inference.type_map, + environment=type_inference.environment_with_args, symbol_table=symbol_table, verification=verification, ) @@ -632,26 +614,22 @@ def _transpile_invariant( environment: intermediate_type_inference.Environment, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Translate the invariant from the meta-model into Python code.""" - canonicalizer = intermediate_type_inference.Canonicalizer() - _ = canonicalizer.transform(invariant.body) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment, - representation_map=canonicalizer.representation_map, + # fmt: off + type_map, inference_error = ( + intermediate_type_inference.infer_for_invariant( + invariant=invariant, + environment=environment + ) ) + # fmt: on - _ = type_inferrer.transform(invariant.body) + if inference_error is not None: + return None, inference_error - if len(type_inferrer.errors): - return None, Error( - invariant.parsed.node, - "Failed to infer the types in the invariant", - type_inferrer.errors, - ) + assert type_map is not None transpiler = _InvariantTranspiler( - type_map=type_inferrer.type_map, + type_map=type_map, environment=environment, symbol_table=symbol_table, ) diff --git a/aas_core_codegen/typescript/verification/_generate.py b/aas_core_codegen/typescript/verification/_generate.py index 25889295d..c55442e41 100644 --- a/aas_core_codegen/typescript/verification/_generate.py +++ b/aas_core_codegen/typescript/verification/_generate.py @@ -456,41 +456,23 @@ def _transpile_transpilable_verification( environment: intermediate_type_inference.Environment, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Transpile a verification function.""" - canonicalizer = intermediate_type_inference.Canonicalizer() - for node in verification.parsed.body: - _ = canonicalizer.transform(node) - - environment_with_args = intermediate_type_inference.MutableEnvironment( - parent=environment - ) - for arg in verification.arguments: - environment_with_args.set( - identifier=arg.name, - type_annotation=intermediate_type_inference.convert_type_annotation( - arg.type_annotation - ), + # fmt: off + type_inference, error = ( + intermediate_type_inference.infer_for_verification( + verification=verification, + base_environment=environment ) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment_with_args, - representation_map=canonicalizer.representation_map, ) + # fmt: on - for node in verification.parsed.body: - _ = type_inferrer.transform(node) + if error is not None: + return None, error - if len(type_inferrer.errors): - return None, Error( - verification.parsed.node, - f"Failed to infer the types " - f"in the verification function {verification.name!r}", - type_inferrer.errors, - ) + assert type_inference is not None transpiler = _TranspilableVerificationTranspiler( - type_map=type_inferrer.type_map, - environment=environment_with_args, + type_map=type_inference.type_map, + environment=type_inference.environment_with_args, symbol_table=symbol_table, verification=verification, ) @@ -642,26 +624,22 @@ def _transpile_invariant( environment: intermediate_type_inference.Environment, ) -> Tuple[Optional[Stripped], Optional[Error]]: """Translate the invariant from the meta-model into TypeScript code.""" - canonicalizer = intermediate_type_inference.Canonicalizer() - _ = canonicalizer.transform(invariant.body) - - type_inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment, - representation_map=canonicalizer.representation_map, + # fmt: off + type_map, inference_error = ( + intermediate_type_inference.infer_for_invariant( + invariant=invariant, + environment=environment + ) ) + # fmt: on - _ = type_inferrer.transform(invariant.body) + if inference_error is not None: + return None, inference_error - if len(type_inferrer.errors): - return None, Error( - invariant.parsed.node, - "Failed to infer the types in the invariant", - type_inferrer.errors, - ) + assert type_map is not None transpiler = _InvariantTranspiler( - type_map=type_inferrer.type_map, + type_map=type_map, environment=environment, symbol_table=symbol_table, ) diff --git a/tests/intermediate/test_type_inference.py b/tests/intermediate/test_type_inference.py index e946bb0d5..e491d3f33 100644 --- a/tests/intermediate/test_type_inference.py +++ b/tests/intermediate/test_type_inference.py @@ -38,19 +38,35 @@ def execute(source: str) -> None: ) for invariant in our_type.invariants: - canonicalizer = intermediate_type_inference.Canonicalizer() - canonicalizer.transform(invariant.body) - - inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment, - representation_map=canonicalizer.representation_map, + # fmt: off + _, inference_error = ( + intermediate_type_inference.infer_for_invariant( + invariant=invariant, + environment=environment + ) ) + # fmt: on - inferrer.transform(invariant.body) assert ( - len(inferrer.errors) == 0 - ), tests.common.most_underlying_messages(inferrer.errors) + inference_error is None + ), tests.common.most_underlying_messages([inference_error]) + + for verification in symbol_table.verification_functions: + if not isinstance(verification, intermediate.TranspilableVerification): + continue + + # fmt: off + _, inference_error = ( + intermediate_type_inference.infer_for_verification( + verification=verification, + base_environment=base_environment + ) + ) + # fmt: on + + assert inference_error is None, tests.common.most_underlying_messages( + [inference_error] + ) def expect_type_inference_to_fail( self, source: str, expected_joined_message: str @@ -82,28 +98,45 @@ def expect_type_inference_to_fail( ) for invariant in our_type.invariants: - canonicalizer = intermediate_type_inference.Canonicalizer() - canonicalizer.transform(invariant.body) - - inferrer = intermediate_type_inference.Inferrer( - symbol_table=symbol_table, - environment=environment, - representation_map=canonicalizer.representation_map, + # fmt: off + _, inference_error = ( + intermediate_type_inference.infer_for_invariant( + invariant=invariant, + environment=environment + ) ) + # fmt: on - inferrer.transform(invariant.body) - if len(inferrer.errors) > 0: + if inference_error is not None: type_inference_errors.append( - tests.common.most_underlying_messages(inferrer.errors) + tests.common.most_underlying_messages([inference_error]) ) - assert len(type_inference_errors) > 0, ( - f"Expected one or more type inference errors, " - f"but got none on the source code:\n{source}" + for verification in symbol_table.verification_functions: + if not isinstance(verification, intermediate.TranspilableVerification): + continue + + # fmt: off + _, inference_error = ( + intermediate_type_inference.infer_for_verification( + verification=verification, + base_environment=base_environment + ) ) + # fmt: on + + if inference_error is not None: + type_inference_errors.append( + tests.common.most_underlying_messages([inference_error]) + ) + + assert len(type_inference_errors) > 0, ( + f"Expected one or more type inference errors, " + f"but got none on the source code:\n{source}" + ) - joined_message = "\n".join(type_inference_errors) - self.assertEqual(expected_joined_message, joined_message, source) + joined_message = "\n".join(type_inference_errors) + self.assertEqual(expected_joined_message, joined_message, source) def test_enumeration_literal_as_member(self) -> None: source = textwrap.dedent(