[Ada] Conformance for quantified expressions

[Ada] Conformance for quantified expressions

[Arnaud Charlet]

[-- Attachment #1: Type: text/plain, Size: 1978 bytes --]

Ada2012 Quantified expressions can appear in default expressions, and must be
checked for conformance.
The following compilation:

     gcc -c -gnat12 -gnata conf.adb

must yield:

   conf.adb:16:14: not fully conformant with declaration at line 4
   conf.adb:16:14: default expression for "X" does not match
   conf.adb:22:14: not fully conformant with declaration at line 6
   conf.adb:22:14: default expression for "X" does not match
   conf.adb:29:14: not fully conformant with declaration at line 9
   conf.adb:29:14: default expression for "X" does not match
   conf.adb:37:14: not fully conformant with declaration at line 12
   conf.adb:37:14: default expression for "X" does not match

---
procedure Conf is
   table : array (1..10) of integer := (others => 1);

   procedure Maybe (X : Boolean := (for all E of table => E = 1));

   procedure Peut_Etre
    (X : Boolean := (for all I in table'range => Table (I) = 1));

   procedure Quizas
    (X : Boolean := (for all I in table'range => Table (I) = 1));

   procedure Qui_Sait
    (X : Boolean := (for all I of table => Table (I) = 1));

  -- Expression doesn't match
   procedure Maybe (X : Boolean := (for all E of table => E = 2)) is
   begin
      null;
   end;

   --  loop parameter doesn't match
   procedure Peut_Etre
     (X : Boolean := (for all J in table'range => Table (J) = 1)) is
   begin
      null;
   end;

  --  discrete range doesn't match
   procedure Quizas
     (X : Boolean := 
       (for all I in table'first  .. table'last => Table (I) = 1)) is
   begin
      null;
   end;

   --  discrete range doesn't match
   procedure Qui_Sait
       (X : Boolean := (for all I in reverse table'range => Table (I) = 1)) is
   begin
      null;
   end;

begin
   Table (5) := 0;
   Maybe;
   Qui_Sait;
   Quizas;
end;

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-08-01  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Fully_Conformant_Expressions): handle quantified
	expressions.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 2252 bytes --]

Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 177048)
+++ sem_ch6.adb	(working copy)
@@ -6685,6 +6685,50 @@
                    and then
                  FCE (Expression (E1), Expression (E2));
 
+            when N_Quantified_Expression =>
+               if not FCE (Condition (E1), Condition (E2)) then
+                  return False;
+               end if;
+
+               if Present (Loop_Parameter_Specification (E1))
+                 and then Present (Loop_Parameter_Specification (E2))
+               then
+                  declare
+                     L1 : constant Node_Id :=
+                       Loop_Parameter_Specification (E1);
+                     L2 : constant Node_Id :=
+                       Loop_Parameter_Specification (E2);
+
+                  begin
+                     return
+                       Reverse_Present (L1) = Reverse_Present (L2)
+                         and then
+                           FCE (Defining_Identifier (L1),
+                                Defining_Identifier (L2))
+                         and then
+                           FCE (Discrete_Subtype_Definition (L1),
+                                Discrete_Subtype_Definition (L2));
+                  end;
+
+               else   --  quantified expression with an iterator
+                  declare
+                     I1 : constant Node_Id := Iterator_Specification (E1);
+                     I2 : constant Node_Id := Iterator_Specification (E2);
+
+                  begin
+                     return
+                       FCE (Defining_Identifier (I1),
+                            Defining_Identifier (I2))
+                       and then
+                         Of_Present (I1) = Of_Present (I2)
+                       and then
+                         Reverse_Present (I1) = Reverse_Present (I2)
+                       and then FCE (Name (I1), Name (I2))
+                       and then FCE (Subtype_Indication (I1),
+                                      Subtype_Indication (I2));
+                  end;
+               end if;
+
             when N_Range =>
                return
                  FCE (Low_Bound (E1), Low_Bound (E2))