[Ada] Conformance of quantified expressions

[Arnaud Charlet]

This patch implements AI12-050, which extends the conformance rules to Ada2012
quantified expressions. Previously the conformance of corresponding identifiers
in the two expressions required that they denote the same entity. The loop
parameters of two quantified expressions are conformant if the identifiers are
the same, even though they denote different entities.

The following must compile quietly:

   gcc -c quantified_expressions.adb
   gcc -c -gnatc quantified_expressions.adb

---
with Support; use Support;
package Quantified_Expressions is

   procedure Matrix_Processing
 (M : in out Matrix;
  B :Boolean := (for all I in Ind =>
   (for some J in Ind =>
   Sample_Matrix (I, J) = 0)));
end Quantified_Expressions;
---
package body Quantified_Expressions is


   procedure Matrix_Processing
 (M : in out Matrix;
  B :Boolean := (for all I in Ind =>
   (for some J in Ind =>
   Sample_Matrix (I, J) = 0)))
   is
   begin
  null;
   end Matrix_Processing;

end Quantified_Expressions;

---
with Ada.Containers.Vectors;

package Support is

   subtype Ind is Integer range 1 .. 10;

   type Matrix is array (Ind, Ind) of Integer;

   Sample_Matrix : Matrix;
end Support;

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

2017-01-12  Ed Schonberg  

* sem_ch6.adb (Fully_Conformant_Expressions): Handle properly
quantified expressions, following AI12-050: the loop parameters
of two quantified expressions are conformant if they have the
same identifier.

Index: sem_ch6.adb
===
--- sem_ch6.adb (revision 244352)
+++ sem_ch6.adb (working copy)
@@ -8476,10 +8476,22 @@
   elsif Is_Entity_Name (E1) and then Is_Entity_Name (E2) then
  if Present (Entity (E1)) then
 return Entity (E1) = Entity (E2)
+
+  --  One may be a discriminant that has been replaced by
+  --  the correspondding discriminal
+
   or else (Chars (Entity (E1)) = Chars (Entity (E2))
 and then Ekind (Entity (E1)) = E_Discriminant
-and then Ekind (Entity (E2)) = E_In_Parameter);
+and then Ekind (Entity (E2)) = E_In_Parameter)
 
+ --  AI12-050 : the loop variables of quantified expressions
+ --  match if the have the same identifier, even though they
+ --  are different entities.
+
+  or else (Chars (Entity (E1)) = Chars (Entity (E2))
+   and then Ekind (Entity (E1)) = E_Loop_Parameter
+   and then Ekind (Entity (E2)) = E_Loop_Parameter);
+
  elsif Nkind (E1) = N_Expanded_Name
and then Nkind (E2) = N_Expanded_Name
and then Nkind (Selector_Name (E1)) = N_Character_Literal

[Ada] Conformance for quantified expressions

[Arnaud Charlet]

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  schonb...@adacore.com

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

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))