Skip to content

Commit 6df5c9e

Browse files
authored
Refactor type inference in functions (#523)
So far, we were unsure what the best abstraction for type inference would be. After a couple of code generators, the structure for the type inference crystalized out: we refactor it into two functions, one for the class invariants and one for the transpilable verification functions. The type inference for pattern verification functions is explicitly left out as we can not infer the type of the matching result in any meaningful way with the simple types we have so far, and we also do not need to. Namely, we ensure that pattern verification functions follow a very strict structure where each variable can only be a string in the parsing stage.
1 parent ba0ca24 commit 6df5c9e

File tree

9 files changed

+342
-420
lines changed

9 files changed

+342
-420
lines changed

aas_core_codegen/cpp/verification/_generate.py

+37-62
Original file line numberDiff line numberDiff line change
@@ -1081,26 +1081,22 @@ def _transpile_class_invariant(
10811081
environment: intermediate_type_inference.Environment,
10821082
) -> Tuple[Optional[Stripped], Optional[Error]]:
10831083
"""Translate the invariant from the meta-model into a C++ condition."""
1084-
canonicalizer = intermediate_type_inference.Canonicalizer()
1085-
_ = canonicalizer.transform(invariant.body)
1086-
1087-
type_inferrer = intermediate_type_inference.Inferrer(
1088-
symbol_table=symbol_table,
1089-
environment=environment,
1090-
representation_map=canonicalizer.representation_map,
1084+
# fmt: off
1085+
type_map, inference_error = (
1086+
intermediate_type_inference.infer_for_invariant(
1087+
invariant=invariant,
1088+
environment=environment
1089+
)
10911090
)
1091+
# fmt: on
10921092

1093-
_ = type_inferrer.transform(invariant.body)
1093+
if inference_error is not None:
1094+
return None, inference_error
10941095

1095-
if len(type_inferrer.errors):
1096-
return None, Error(
1097-
invariant.parsed.node,
1098-
"Failed to infer the types in the invariant",
1099-
type_inferrer.errors,
1100-
)
1096+
assert type_map is not None
11011097

11021098
optional_inferrer = cpp_optionaling.Inferrer(
1103-
environment=environment, type_map=type_inferrer.type_map
1099+
environment=environment, type_map=type_map
11041100
)
11051101

11061102
_ = optional_inferrer.transform(invariant.body)
@@ -1114,7 +1110,7 @@ def _transpile_class_invariant(
11141110
)
11151111

11161112
transpiler = _ClassInvariantTranspiler(
1117-
type_map=type_inferrer.type_map,
1113+
type_map=type_map,
11181114
is_optional_map=optional_inferrer.is_optional_map,
11191115
environment=environment,
11201116
symbol_table=symbol_table,
@@ -2111,40 +2107,23 @@ def _generate_implementation_of_transpilable_verification(
21112107
base_environment: intermediate_type_inference.Environment,
21122108
) -> Tuple[Optional[Stripped], Optional[Error]]:
21132109
"""Transpile the verification to a function implementation."""
2114-
canonicalizer = intermediate_type_inference.Canonicalizer()
2115-
for node in verification.parsed.body:
2116-
_ = canonicalizer.transform(node)
2117-
2118-
environment = intermediate_type_inference.MutableEnvironment(
2119-
parent=base_environment
2120-
)
2121-
for arg in verification.arguments:
2122-
environment.set(
2123-
identifier=arg.name,
2124-
type_annotation=intermediate_type_inference.convert_type_annotation(
2125-
arg.type_annotation
2126-
),
2110+
# fmt: off
2111+
type_inference, inference_error = (
2112+
intermediate_type_inference.infer_for_verification(
2113+
verification=verification,
2114+
base_environment=base_environment
21272115
)
2128-
2129-
type_inferrer = intermediate_type_inference.Inferrer(
2130-
symbol_table=symbol_table,
2131-
environment=environment,
2132-
representation_map=canonicalizer.representation_map,
21332116
)
2117+
# fmt: on
21342118

2135-
for node in verification.parsed.body:
2136-
_ = type_inferrer.transform(node)
2119+
if inference_error is not None:
2120+
return None, inference_error
21372121

2138-
if len(type_inferrer.errors):
2139-
return None, Error(
2140-
verification.parsed.node,
2141-
f"Failed to infer the types "
2142-
f"in the verification function {verification.name!r}",
2143-
type_inferrer.errors,
2144-
)
2122+
assert type_inference is not None
21452123

21462124
optional_inferrer = cpp_optionaling.Inferrer(
2147-
environment=environment, type_map=type_inferrer.type_map
2125+
environment=type_inference.environment_with_args,
2126+
type_map=type_inference.type_map,
21482127
)
21492128
for node in verification.parsed.body:
21502129
_ = optional_inferrer.transform(node)
@@ -2158,9 +2137,9 @@ def _generate_implementation_of_transpilable_verification(
21582137
)
21592138

21602139
transpiler = _TranspilableVerificationTranspiler(
2161-
type_map=type_inferrer.type_map,
2140+
type_map=type_inference.type_map,
21622141
is_optional_map=optional_inferrer.is_optional_map,
2163-
environment=environment,
2142+
environment=type_inference.environment_with_args,
21642143
symbol_table=symbol_table,
21652144
verification=verification,
21662145
)
@@ -2398,26 +2377,22 @@ def _transpile_constrained_primitive_invariant(
23982377
constrained_primitive: intermediate.ConstrainedPrimitive,
23992378
) -> Tuple[Optional[Stripped], Optional[Error]]:
24002379
"""Translate the invariant from the meta-model into a C++ condition."""
2401-
canonicalizer = intermediate_type_inference.Canonicalizer()
2402-
_ = canonicalizer.transform(invariant.body)
2403-
2404-
type_inferrer = intermediate_type_inference.Inferrer(
2405-
symbol_table=symbol_table,
2406-
environment=environment,
2407-
representation_map=canonicalizer.representation_map,
2380+
# fmt: off
2381+
type_map, inference_error = (
2382+
intermediate_type_inference.infer_for_invariant(
2383+
invariant=invariant,
2384+
environment=environment
2385+
)
24082386
)
2387+
# fmt: on
24092388

2410-
_ = type_inferrer.transform(invariant.body)
2389+
if inference_error is not None:
2390+
return None, inference_error
24112391

2412-
if len(type_inferrer.errors):
2413-
return None, Error(
2414-
invariant.parsed.node,
2415-
"Failed to infer the types in the invariant",
2416-
type_inferrer.errors,
2417-
)
2392+
assert type_map is not None
24182393

24192394
optional_inferrer = cpp_optionaling.Inferrer(
2420-
environment=environment, type_map=type_inferrer.type_map
2395+
environment=environment, type_map=type_map
24212396
)
24222397

24232398
_ = optional_inferrer.transform(invariant.body)
@@ -2431,7 +2406,7 @@ def _transpile_constrained_primitive_invariant(
24312406
)
24322407

24332408
transpiler = _ConstrainedPrimitiveInvariantTranspiler(
2434-
type_map=type_inferrer.type_map,
2409+
type_map=type_map,
24352410
is_optional_map=optional_inferrer.is_optional_map,
24362411
environment=environment,
24372412
symbol_table=symbol_table,

aas_core_codegen/csharp/verification/_generate.py

+23-54
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ def __init__(self, defined_variables: Set[Identifier]) -> None:
8282
"""
8383
Initialize with the given values.
8484
85-
The ``initialized_variables`` are shared between different statement
85+
The ``defined_variables`` are shared between different statement
8686
transpilations. It is also mutated when assignments are transpiled. We need to
8787
keep track of variables so that we know when we have to define them, and when
8888
we can simply assign them a value, if they have been already defined.
@@ -427,41 +427,23 @@ def _transpile_transpilable_verification(
427427
environment: intermediate_type_inference.Environment,
428428
) -> Tuple[Optional[Stripped], Optional[Error]]:
429429
"""Transpile a verification function."""
430-
canonicalizer = intermediate_type_inference.Canonicalizer()
431-
for node in verification.parsed.body:
432-
_ = canonicalizer.transform(node)
433-
434-
environment_with_args = intermediate_type_inference.MutableEnvironment(
435-
parent=environment
436-
)
437-
for arg in verification.arguments:
438-
environment_with_args.set(
439-
identifier=arg.name,
440-
type_annotation=intermediate_type_inference.convert_type_annotation(
441-
arg.type_annotation
442-
),
430+
# fmt: off
431+
type_inference, error = (
432+
intermediate_type_inference.infer_for_verification(
433+
verification=verification,
434+
base_environment=environment
443435
)
444-
445-
type_inferrer = intermediate_type_inference.Inferrer(
446-
symbol_table=symbol_table,
447-
environment=environment_with_args,
448-
representation_map=canonicalizer.representation_map,
449436
)
437+
# fmt: on
450438

451-
for node in verification.parsed.body:
452-
_ = type_inferrer.transform(node)
439+
if error is not None:
440+
return None, error
453441

454-
if len(type_inferrer.errors):
455-
return None, Error(
456-
verification.parsed.node,
457-
f"Failed to infer the types "
458-
f"in the verification function {verification.name!r}",
459-
type_inferrer.errors,
460-
)
442+
assert type_inference is not None
461443

462444
transpiler = _TranspilableVerificationTranspiler(
463-
type_map=type_inferrer.type_map,
464-
environment=environment_with_args,
445+
type_map=type_inference.type_map,
446+
environment=type_inference.environment_with_args,
465447
symbol_table=symbol_table,
466448
verification=verification,
467449
)
@@ -598,35 +580,22 @@ def _transpile_invariant(
598580
environment: intermediate_type_inference.Environment,
599581
) -> Tuple[Optional[Stripped], Optional[Error]]:
600582
"""Translate the invariant from the meta-model into C# code."""
601-
# NOTE (mristin, 2021-10-24):
602-
# We manually transpile the invariant from our custom syntax without additional
603-
# semantic analysis in the :py:mod:`aas_core_codegen.intermediate` layer.
604-
#
605-
# While this might seem repetitive ("unDRY"), we are still not sure about
606-
# the appropriate abstraction. After we implement the code generation for a couple
607-
# of languages, we hope to have a much better understanding about the necessary
608-
# abstractions.
609-
610-
canonicalizer = intermediate_type_inference.Canonicalizer()
611-
_ = canonicalizer.transform(invariant.body)
612-
613-
type_inferrer = intermediate_type_inference.Inferrer(
614-
symbol_table=symbol_table,
615-
environment=environment,
616-
representation_map=canonicalizer.representation_map,
583+
# fmt: off
584+
type_map, inference_error = (
585+
intermediate_type_inference.infer_for_invariant(
586+
invariant=invariant,
587+
environment=environment
588+
)
617589
)
590+
# fmt: on
618591

619-
_ = type_inferrer.transform(invariant.body)
592+
if inference_error is not None:
593+
return None, inference_error
620594

621-
if len(type_inferrer.errors):
622-
return None, Error(
623-
invariant.parsed.node,
624-
"Failed to infer the types in the invariant",
625-
type_inferrer.errors,
626-
)
595+
assert type_map is not None
627596

628597
transpiler = _InvariantTranspiler(
629-
type_map=type_inferrer.type_map,
598+
type_map=type_map,
630599
environment=environment,
631600
symbol_table=symbol_table,
632601
)

aas_core_codegen/golang/verification/_generate.py

+25-46
Original file line numberDiff line numberDiff line change
@@ -485,40 +485,23 @@ def _transpile_transpilable_verification(
485485
environment: intermediate_type_inference.Environment,
486486
) -> Tuple[Optional[Stripped], Optional[Error]]:
487487
"""Transpile a verification function."""
488-
canonicalizer = intermediate_type_inference.Canonicalizer()
489-
for node in verification.parsed.body:
490-
_ = canonicalizer.transform(node)
491-
492-
environment_with_args = intermediate_type_inference.MutableEnvironment(
493-
parent=environment
494-
)
495-
for arg in verification.arguments:
496-
environment_with_args.set(
497-
identifier=arg.name,
498-
type_annotation=intermediate_type_inference.convert_type_annotation(
499-
arg.type_annotation
500-
),
488+
# fmt: off
489+
type_inference, error = (
490+
intermediate_type_inference.infer_for_verification(
491+
verification=verification,
492+
base_environment=environment
501493
)
502-
503-
type_inferrer = intermediate_type_inference.Inferrer(
504-
symbol_table=symbol_table,
505-
environment=environment_with_args,
506-
representation_map=canonicalizer.representation_map,
507494
)
495+
# fmt: on
508496

509-
for node in verification.parsed.body:
510-
_ = type_inferrer.transform(node)
497+
if error is not None:
498+
return None, error
511499

512-
if len(type_inferrer.errors):
513-
return None, Error(
514-
verification.parsed.node,
515-
f"Failed to infer the types "
516-
f"in the verification function {verification.name!r}",
517-
type_inferrer.errors,
518-
)
500+
assert type_inference is not None
519501

520502
pointer_inferrer = golang_pointering.Inferrer(
521-
environment=environment_with_args, type_map=type_inferrer.type_map
503+
environment=type_inference.environment_with_args,
504+
type_map=type_inference.type_map,
522505
)
523506

524507
for node in verification.parsed.body:
@@ -533,9 +516,9 @@ def _transpile_transpilable_verification(
533516
)
534517

535518
transpiler = _TranspilableVerificationTranspiler(
536-
type_map=type_inferrer.type_map,
519+
type_map=type_inference.type_map,
537520
is_pointer_map=pointer_inferrer.is_pointer_map,
538-
environment=environment_with_args,
521+
environment=type_inference.environment_with_args,
539522
symbol_table=symbol_table,
540523
verification=verification,
541524
)
@@ -693,26 +676,22 @@ def _transpile_invariant(
693676
environment: intermediate_type_inference.Environment,
694677
) -> Tuple[Optional[Stripped], Optional[Error]]:
695678
"""Translate the invariant from the meta-model into Golang code."""
696-
canonicalizer = intermediate_type_inference.Canonicalizer()
697-
_ = canonicalizer.transform(invariant.body)
698-
699-
type_inferrer = intermediate_type_inference.Inferrer(
700-
symbol_table=symbol_table,
701-
environment=environment,
702-
representation_map=canonicalizer.representation_map,
679+
# fmt: off
680+
type_map, inference_error = (
681+
intermediate_type_inference.infer_for_invariant(
682+
invariant=invariant,
683+
environment=environment
684+
)
703685
)
686+
# fmt: on
704687

705-
_ = type_inferrer.transform(invariant.body)
688+
if inference_error is not None:
689+
return None, inference_error
706690

707-
if len(type_inferrer.errors):
708-
return None, Error(
709-
invariant.parsed.node,
710-
"Failed to infer the types in the invariant",
711-
type_inferrer.errors,
712-
)
691+
assert type_map is not None
713692

714693
pointer_inferrer = golang_pointering.Inferrer(
715-
environment=environment, type_map=type_inferrer.type_map
694+
environment=environment, type_map=type_map
716695
)
717696

718697
_ = pointer_inferrer.transform(invariant.body)
@@ -725,7 +704,7 @@ def _transpile_invariant(
725704
)
726705

727706
transpiler = _InvariantTranspiler(
728-
type_map=type_inferrer.type_map,
707+
type_map=type_map,
729708
is_pointer_map=pointer_inferrer.is_pointer_map,
730709
environment=environment,
731710
symbol_table=symbol_table,

0 commit comments

Comments
 (0)