Add case expressions to language reference

Ref. #907
AdaCore · Jul 12, 2022 · c307ebf · c307ebf
1 parent 726d87e
commit c307ebf
Show file tree

Hide file tree

Showing 3 changed files with 48 additions and 6 deletions.
diff --git a/doc/Language-Reference.adoc b/doc/Language-Reference.adoc
@@ -1070,7 +1070,8 @@ Data_Channel'Write (Message)
 
 [subs="+macros,quotes"]
 ----
-[[syntax-expression]]expression ::= xref:syntax-literal[literal] | xref:syntax-variable[variable] | xref:syntax-mathematical_expression[mathematical_expression] | xref:syntax-boolean_expression[boolean_expression] | xref:syntax-message_aggregate[message_aggregate] | xref:syntax-aggregate[aggregate] | xref:syntax-attribute_reference[attribute_reference] | xref:syntax-selected[selected] | xref:syntax-comprehension[comprehension] | xref:syntax-binding[binding] | xref:syntax-quantified_expression[quantified_expression] | xref:syntax-call[call] | xref:syntax-conversion[conversion]
+[[syntax-expression]]expression ::= xref:syntax-literal[literal] | xref:syntax-variable[variable] | xref:syntax-mathematical_expression[mathematical_expression] | xref:syntax-boolean_expression[boolean_expression] | xref:syntax-message_aggregate[message_aggregate] | xref:syntax-aggregate[aggregate] | xref:syntax-attribute_reference[attribute_reference] | xref:syntax-selected[selected] | xref:syntax-comprehension[comprehension] | xref:syntax-binding[binding] | xref:syntax-quantified_expression[quantified_expression] | xref:syntax-call[call] | xref:syntax-conversion[conversion] | xref:syntax-case_expression[case_expression]
+
 ----
 
 ==== Literals
@@ -1592,6 +1593,45 @@ An invalid condition of a refinement leads to an exception transition. This beha
 Key_Update_Message (Handshake_Control_Message.Data)
 ----
 
+==== Case Expressions
+
+// Case Expressions [§S-E-CE]
+
+A xref:syntax-case_expression[case expression] selects one of several alternative dependent xref:syntax-expression[expressions] for evaluation based on the value of a selecting xref:syntax-expression[expression].
+
+*Syntax*
+
+[subs="+macros,quotes"]
+----
+[[syntax-case_expression]]case_expression ::=
+   *(* *case* selecting_xref:syntax-expression[expression] *is*
+       xref:syntax-case_expression_alternative[case_expression_alternative] { *,*
+       xref:syntax-case_expression_alternative[case_expression_alternative] } *)*
+
+[[syntax-case_expression_alternative]]case_expression_alternative ::=
+   *when* xref:syntax-discrete_choice_list[discrete_choice_list] *=>* dependent_xref:syntax-expression[expression]
+
+[[syntax-discrete_choice_list]]discrete_choice_list := xref:syntax-discrete_choice[discrete_choice] { *|* xref:syntax-discrete_choice[discrete_choice] }
+
+[[syntax-discrete_choice]]discrete_choice := xref:syntax-number[number] | xref:syntax-qualified_name[qualified_name]
+----
+
+*Static Semantics*
+
+The type of all the dependent_xref:syntax-expression[expression]s shall be compatible to the type of the xref:syntax-case_expression[case_expression].
+Each value of the type of the selecting_xref:syntax-expression[expression] shall be covered by a xref:syntax-discrete_choice[discrete_choice].
+Two distinct xref:syntax-discrete_choice[discrete_choices] of a xref:syntax-case_expression[case_expression] shall not cover the same value.
+
+*Example*
+
+[source,ada,rflx,extended_primary]
+----
+(case Value is
+    when T::V1 | T::V2 => 2,
+    when T::V3         => 4)
+----
+
+
 == Packages
 
 A package is used to structure a specification.

diff --git a/tests/integration/session_case_expression/generated/rflx-test-session.adb b/tests/integration/session_case_expression/generated/rflx-test-session.adb
@@ -57,7 +57,7 @@ is
          pragma Assert (Prepare_Invariant);
          goto Finalize_Prepare;
       end if;
-      --  tests/integration/session_case_expression/test.rflx:26:10
+      --  tests/integration/session_case_expression/test.rflx:27:10
       Universal.Message.Reset (Ctx.P.Message_Ctx);
       if Universal.Message.Valid_Next (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then
          if Universal.Message.Available_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) >= Universal.Message.Field_Size (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then
@@ -131,7 +131,7 @@ is
         Ghost;
    begin
       pragma Assert (Reply_Invariant);
-      --  tests/integration/session_case_expression/test.rflx:44:10
+      --  tests/integration/session_case_expression/test.rflx:46:10
       Ctx.P.Next_State := S_Terminated;
       pragma Assert (Reply_Invariant);
    end Reply;

diff --git a/tests/integration/session_case_expression/test.rflx b/tests/integration/session_case_expression/test.rflx
@@ -20,12 +20,14 @@ package Test is
       end Start;
 
       state Prepare is
-         Recv_Type : Universal::Message_Type;
+         Recv_Type : Universal::Message_Type; -- §S-D-V-T-SC
       begin
-         Recv_Type := Message.Message_Type;
+         Recv_Type := Message.Message_Type; -- §S-S-A-A-V
+         -- §S-S-A-A-MA
          Message := Universal::Message'(Message_Type => Universal::MT_Value,
                                         Length       => 1,
-                                        Value        => (case Recv_Type is
+                                        Value        => -- §S-E-CE
+                                                        (case Recv_Type is
                                                          when Universal::MT_Null | Universal::MT_Data =>   2,
                                                          when Universal::MT_Value                     =>   8,
                                                          when Universal::MT_Values                    =>  16,