diff mbox series

[Ada] Dimensional checking and generic subprograms

Message ID 20170906115649.GA140817@adacore.com
State New
Headers show
Series [Ada] Dimensional checking and generic subprograms | expand

Commit Message

Arnaud Charlet Sept. 6, 2017, 11:56 a.m. UTC
This patch enahnces dimensionality checking to cover generic subprograms that
are intended to apply to types of different dimensions, such as an integration
function. Dimensionality checking is performed in each instance. and rely on
a special handling of conversion operations to prevent spurious dimensional
errors in the generic unit itself.

The following must compile quietly:

   gcc -c -gnatws integrate.adb

--- 
package Dims with SPARK_Mode is

    -----------------------------------------
    -- Setup Dimension System
    -----------------------------------------
    type Unit_Type is new Float with Dimension_System =>
        ((Unit_Name => Meter, Unit_Symbol => 'm', Dim_Symbol => 'L'),
         (Unit_Name => Kilogram, Unit_Symbol => "kg", Dim_Symbol => 'M'),
         (Unit_Name => Second, Unit_Symbol => 's', Dim_Symbol => 'T'),
         (Unit_Name => Ampere, Unit_Symbol => 'A', Dim_Symbol => 'I'),
         (Unit_Name => Kelvin, Unit_Symbol => 'K', Dim_Symbol => "Theta"),
         (Unit_Name => Radian, Unit_Symbol => "Rad", Dim_Symbol => "A")),
   Default_Value => 0.0; 

   -- Base Dimensions
   subtype Length_Type is Unit_Type with
        Dimension => (Symbol => 'm', Meter => 1, others => 0);  
 
   subtype Time_Type is Unit_Type with
        Dimension => (Symbol => 's', Second => 1, others => 0);   

   subtype Linear_Velocity_Type is Unit_Type with
        Dimension => (Meter => 1, Second => -1, others => 0);   

   -- Base Units
   Meter    : constant Length_Type := Length_Type (1.0);
   Second   : constant Time_Type   := Time_Type (1.0);
end dims;
---
with Dims; use Dims;
procedure Integrate is
   generic
      type Op1 is new Unit_Type;
      type Op2 is new Unit_Type;
      type Res is new Unit_Type;
   function I (X : op1; Y : Op2) return Res;
   function I (X : op1; Y : Op2) return Res is
   begin
      return Res (Unit_Type (X) *  Unit_type (Y));
   end I;

   function Distance is new I (Time_Type, Linear_Velocity_Type, Length_Type);
   Secs : Time_Type := 5.0;
   Speed : Linear_Velocity_Type := 10.0;
   Covered : Length_Type;
begin
   Covered  := Distance (Secs, Speed);

   declare
      subtype Area is Unit_Type with dimension =>
         (Meter => 2, others => 0);
      My_Little_Acre : Area;
      function Acres is new I (Length_Type, Length_Type, Area);
    begin
       My_Little_Acre := Covered * Covered;
       My_Little_Acre := Acres (Covered, Covered);
    end;
end Integrate;

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

2017-09-06  Ed Schonberg  <schonberg@adacore.com>

	* sem_dim.adb (Analyze_Dimension): In an instance, a type
	conversion takes its dimensions from the expression, not from
	the context type.
	(Dimensions_Of_Operand): Ditto.
diff mbox series

Patch

Index: sem_dim.adb
===================================================================
--- sem_dim.adb	(revision 251753)
+++ sem_dim.adb	(working copy)
@@ -1161,7 +1161,6 @@ 
             | N_Qualified_Expression
             | N_Selected_Component
             | N_Slice
-            | N_Type_Conversion
             | N_Unchecked_Type_Conversion
          =>
             Analyze_Dimension_Has_Etype (N);
@@ -1191,7 +1190,17 @@ 
          when N_Subtype_Declaration =>
             Analyze_Dimension_Subtype_Declaration (N);
 
+         when  N_Type_Conversion =>
+            if In_Instance
+              and then Exists (Dimensions_Of (Expression (N)))
+            then
+               Set_Dimensions (N, Dimensions_Of (Expression (N)));
+            else
+               Analyze_Dimension_Has_Etype (N);
+            end if;
+
          when N_Unary_Op =>
+
             Analyze_Dimension_Unary_Op (N);
 
          when others =>
@@ -1378,11 +1387,24 @@ 
 
          --  A type conversion may have been inserted to rewrite other
          --  expressions, e.g. function returns. Dimensions are those of
-         --  the target type.
+         --  the target type, unless this is a conversion in an instance,
+         --  in which case the proper dimensions are those of the operand,
 
          elsif Nkind (N) = N_Type_Conversion then
-            return Dimensions_Of (Etype (N));
+            if In_Instance
+              and then Is_Generic_Actual_Type (Etype (Expression (N)))
+            then
+               return Dimensions_Of (Etype (Expression (N)));
 
+            elsif In_Instance
+              and then Exists (Dimensions_Of (Expression (N)))
+            then
+               return Dimensions_Of (Expression (N));
+
+            else
+               return Dimensions_Of (Etype (N));
+            end if;
+
          --  Otherwise return the default dimensions
 
          else