A subtype indication whose type mark is a predicated subtype inherits the predicates of its parent type. A loop whose specification has the form:
for S1 in T range Lo .. Hi loop ... and in which T has a static predicate, is executed over the values of T in the specified range that satisfy the predicate. Previous to this patch the inherited predicate was ignored and the loop executed for all values in the range. Executing: gnatmake -q main main must yield: TRUE TRUE Forward 3 4 10 11 12 Backwards 12 11 10 4 3 --- with Bar; use Bar; procedure Main is begin P; end; --- package Bar with SPARK_Mode is subtype B is Boolean with Static_Predicate => B = True; subtype C is integer with Static_Predicate => C in 1..4 | 10..20; function Ident (X : B) return B is (X); function Bizarre (X : Boolean) return B is (Ident (X)); procedure P; end Bar; --- With TExt_IO; use Text_IO; package body Bar with SPARK_Mode is procedure P is Thing : B; Thing2 : B := True; begin for X in B range False .. True loop THing := X; Thing := THing2; Put_Line (Thing'Img); end loop; put_line ("Forward"); for Y in C range 3 .. 12 loop Put_Line (Integer'Image (Y)); end loop; put_line ("Backwards"); for Y in reverse C range 3 .. 12 loop Put_Line (Integer'Image (Y)); end loop; end P; end Bar; Tested on x86_64-pc-linux-gnu, committed on trunk 2017-09-08 Ed Schonberg <schonb...@adacore.com> * exp_ch5.adb (Expand_Predicated_Loop): Handle properly a loop over a subtype of a type with a static predicate, taking into account the predicate function of the parent type and the bounds given in the loop specification. * sem_ch3.adb (Inherit_Predicate_Flags): For qn Itype created for a loop specification that is a subtype indication whose type mark is a type with a static predicate, inherit predicate function, used to build case statement for rewritten loop.
Index: exp_ch5.adb =================================================================== --- exp_ch5.adb (revision 251863) +++ exp_ch5.adb (working copy) @@ -4698,6 +4698,10 @@ -- end loop; -- end; + -- In addition, if the loop specification is given by a subtype + -- indication that constrains a predicated type, the bounds of + -- iteration are given by those of the subtype indication. + else Static_Predicate : declare S : Node_Id; @@ -4706,6 +4710,11 @@ Alts : List_Id; Cstm : Node_Id; + -- If the domain is an itype, note the bounds of its range. + + L_Hi : Node_Id; + L_Lo : Node_Id; + function Lo_Val (N : Node_Id) return Node_Id; -- Given static expression or static range, returns an identifier -- whose value is the low bound of the expression value or range. @@ -4760,6 +4769,11 @@ Set_Warnings_Off (Loop_Id); + if Is_Itype (Ltype) then + L_Hi := High_Bound (Scalar_Range (Ltype)); + L_Lo := Low_Bound (Scalar_Range (Ltype)); + end if; + -- Loop to create branches of case statement Alts := New_List; @@ -4768,12 +4782,21 @@ -- Initial value is largest value in predicate. - D := - Make_Object_Declaration (Loc, - Defining_Identifier => Loop_Id, - Object_Definition => New_Occurrence_Of (Ltype, Loc), - Expression => Hi_Val (Last (Stat))); + if Is_Itype (Ltype) then + D := + Make_Object_Declaration (Loc, + Defining_Identifier => Loop_Id, + Object_Definition => New_Occurrence_Of (Ltype, Loc), + Expression => L_Hi); + else + D := + Make_Object_Declaration (Loc, + Defining_Identifier => Loop_Id, + Object_Definition => New_Occurrence_Of (Ltype, Loc), + Expression => Hi_Val (Last (Stat))); + end if; + P := Last (Stat); while Present (P) loop if No (Prev (P)) then @@ -4794,15 +4817,34 @@ Prev (P); end loop; + if Is_Itype (Ltype) + and then Is_OK_Static_Expression (L_Lo) + and then + Expr_Value (L_Lo) /= Expr_Value (Lo_Val (First (Stat))) + then + Append_To (Alts, + Make_Case_Statement_Alternative (Loc, + Statements => New_List (Make_Exit_Statement (Loc)), + Discrete_Choices => New_List (L_Lo))); + end if; + else -- Initial value is smallest value in predicate. - D := - Make_Object_Declaration (Loc, - Defining_Identifier => Loop_Id, - Object_Definition => New_Occurrence_Of (Ltype, Loc), - Expression => Lo_Val (First (Stat))); + if Is_Itype (Ltype) then + D := + Make_Object_Declaration (Loc, + Defining_Identifier => Loop_Id, + Object_Definition => New_Occurrence_Of (Ltype, Loc), + Expression => L_Lo); + else + D := + Make_Object_Declaration (Loc, + Defining_Identifier => Loop_Id, + Object_Definition => New_Occurrence_Of (Ltype, Loc), + Expression => Lo_Val (First (Stat))); + end if; P := First (Stat); while Present (P) loop @@ -4823,6 +4865,17 @@ Next (P); end loop; + + if Is_Itype (Ltype) + and then Is_OK_Static_Expression (L_Hi) + and then + Expr_Value (L_Hi) /= Expr_Value (Lo_Val (Last (Stat))) + then + Append_To (Alts, + Make_Case_Statement_Alternative (Loc, + Statements => New_List (Make_Exit_Statement (Loc)), + Discrete_Choices => New_List (L_Hi))); + end if; end if; -- Add others choice Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 251871) +++ sem_ch3.adb (working copy) @@ -18449,6 +18449,19 @@ (Subt, Has_Static_Predicate_Aspect (Par)); Set_Has_Dynamic_Predicate_Aspect (Subt, Has_Dynamic_Predicate_Aspect (Par)); + + -- A named subtype does not inherit the predicate function of its + -- parent but an itype declared for a loop index needs the discrete + -- predicate information of its parent to execute the loop properly. + + if Is_Itype (Subt) and then Present (Predicate_Function (Par)) then + Set_Subprograms_For_Type (Subt, Subprograms_For_Type (Par)); + + if Has_Static_Predicate (Par) then + Set_Static_Discrete_Predicate + (Subt, Static_Discrete_Predicate (Par)); + end if; + end if; end Inherit_Predicate_Flags; ----------------------