Introduce shorthand for common if-then-else for Ada expressions

Ref. None
AdaCore · Apr 9, 2024 · f00be0f · f00be0f
1 parent e1f923d
commit f00be0f
Show file tree

Hide file tree

Showing 6 changed files with 290 additions and 380 deletions.
diff --git a/rflx/ada.py b/rflx/ada.py
@@ -767,6 +767,14 @@ def If(  # noqa: N802
     return IfExpr(condition_expressions, else_expression)
 
 
+def IfThenElse(  # noqa: N802
+    condition: Expr,
+    then_expr: Expr,
+    else_expr: Optional[Expr] = None,
+) -> Expr:
+    return If([(condition, then_expr)], else_expr)
+
+
 class IfExpr(Expr):
     def __init__(
         self,

diff --git a/rflx/generator/common.py b/rflx/generator/common.py
@@ -25,6 +25,7 @@
     GreaterEqual,
     If,
     IfExpr,
+    IfThenElse,
     Indexed,
     Last,
     Less,
@@ -384,46 +385,42 @@ def link_property(link: model.Link, unique: bool) -> Expr:
             else TRUE
         )
 
-        return If(
-            [
-                (
-                    precond,
-                    AndThen(
-                        Equal(
-                            Add(
-                                Sub(
-                                    Selected(
-                                        Indexed(
-                                            prefixed("Cursors").ada_expr(),
-                                            Variable(link.target.affixed_name),
-                                        ),
-                                        "Last",
-                                    ),
-                                    Selected(
-                                        Indexed(
-                                            prefixed("Cursors").ada_expr(),
-                                            Variable(link.target.affixed_name),
-                                        ),
-                                        "First",
-                                    ),
+        return IfThenElse(
+            precond,
+            AndThen(
+                Equal(
+                    Add(
+                        Sub(
+                            Selected(
+                                Indexed(
+                                    prefixed("Cursors").ada_expr(),
+                                    Variable(link.target.affixed_name),
                                 ),
-                                Number(1),
+                                "Last",
                             ),
-                            size.ada_expr(),
-                        ),
-                        Equal(
                             Selected(
                                 Indexed(
                                     prefixed("Cursors").ada_expr(),
                                     Variable(link.target.affixed_name),
                                 ),
                                 "First",
                             ),
-                            first.ada_expr(),
                         ),
+                        Number(1),
                     ),
+                    size.ada_expr(),
                 ),
-            ],
+                Equal(
+                    Selected(
+                        Indexed(
+                            prefixed("Cursors").ada_expr(),
+                            Variable(link.target.affixed_name),
+                        ),
+                        "First",
+                    ),
+                    first.ada_expr(),
+                ),
+            ),
         )
 
     def field_property(fld: model.Field) -> Expr:
@@ -432,16 +429,12 @@ def field_property(fld: model.Field) -> Expr:
         return AndThen(*[link_property(link, unique) for link in incoming])
 
     def map_invariant(fld: model.Field) -> Expr:
-        return If(
-            [
-                (
-                    Call(
-                        "Well_Formed",
-                        [Indexed(prefixed("Cursors").ada_expr(), Variable(fld.affixed_name))],
-                    ),
-                    field_property(fld),
-                ),
-            ],
+        return IfThenElse(
+            Call(
+                "Well_Formed",
+                [Indexed(prefixed("Cursors").ada_expr(), Variable(fld.affixed_name))],
+            ),
+            field_property(fld),
         )
 
     return AndThen(*[map_invariant(f) for f in message.fields])
@@ -460,51 +453,38 @@ def invalid_successors_invariant() -> Expr:
         """
         return AndThen(
             *[
-                If(
-                    [
-                        (
-                            AndThen(
-                                *[
-                                    Call(
-                                        "Invalid",
-                                        [
-                                            Indexed(
-                                                Variable("Cursors"),
-                                                Variable(p.affixed_name),
-                                            ),
-                                        ],
-                                    )
-                                    for p in message.direct_predecessors(f)
-                                ],
-                            ),
+                IfThenElse(
+                    AndThen(
+                        *[
                             Call(
                                 "Invalid",
-                                [
-                                    Indexed(
-                                        Variable("Cursors"),
-                                        Variable(f.affixed_name),
-                                    ),
-                                ],
+                                [Indexed(Variable("Cursors"), Variable(p.affixed_name))],
+                            )
+                            for p in message.direct_predecessors(f)
+                        ],
+                    ),
+                    Call(
+                        "Invalid",
+                        [
+                            Indexed(
+                                Variable("Cursors"),
+                                Variable(f.affixed_name),
                             ),
-                        ),
-                    ],
+                        ],
+                    ),
                 )
                 for f in message.fields
                 if f not in message.direct_successors(model.INITIAL)
             ],
         )
 
     return AndThen(
-        If(
-            [
-                (
-                    NotEqual(Variable("Buffer"), Variable("null")),
-                    And(
-                        Equal(First("Buffer"), Variable("Buffer_First")),
-                        Equal(Last("Buffer"), Variable("Buffer_Last")),
-                    ),
-                ),
-            ],
+        IfThenElse(
+            NotEqual(Variable("Buffer"), Variable("null")),
+            And(
+                Equal(First("Buffer"), Variable("Buffer_First")),
+                Equal(Last("Buffer"), Variable("Buffer_Last")),
+            ),
         ),
         public_context_predicate(),
         LessEqual(Sub(Variable("First"), Number(1)), Variable("Verified_Last")),
@@ -577,22 +557,15 @@ def valid_path_to_next_field_condition(
     prefix: str,
 ) -> list[Expr]:
     return [
-        If(
-            [
-                (
-                    l.condition.substituted(substitution(message, public=True, prefix=prefix))
-                    .simplified()
-                    .ada_expr(),
-                    (
-                        Call(
-                            "Valid_Next",
-                            [Variable("Ctx"), Variable(l.target.affixed_name)],
-                        )
-                        if l.target != model.FINAL
-                        else TRUE
-                    ),
-                ),
-            ],
+        IfThenElse(
+            l.condition.substituted(substitution(message, public=True, prefix=prefix))
+            .simplified()
+            .ada_expr(),
+            (
+                Call("Valid_Next", [Variable("Ctx"), Variable(l.target.affixed_name)])
+                if l.target != model.FINAL
+                else TRUE
+            ),
         )
         for l in message.outgoing(field)
         if l.target != model.FINAL