Move type operations to separate child package

ref #1126

rflx/generator/const.py

@@ -8,9 +8,13 @@
 BUILTIN_TYPES_CONVERSIONS_PACKAGE = ID("RFLX_Builtin_Types.Conversions")
 BUILTIN_TYPES_PACKAGE = ID("RFLX_Builtin_Types")
 GENERIC_TYPES_PACKAGE = ID("RFLX_Generic_Types")
+GENERIC_TYPES_GENERIC_OPERATORS_PACKAGE = ID("RFLX_Generic_Types.Generic_Operators")
+GENERIC_TYPES_GENERIC_OPERATIONS_PACKAGE = ID("RFLX_Generic_Types.Generic_Operations")
 MESSAGE_SEQUENCE_PACKAGE = ID("RFLX_Message_Sequence")
 SCALAR_SEQUENCE_PACKAGE = ID("RFLX_Scalar_Sequence")
 TYPES_PACKAGE = ID("RFLX_Types")
+TYPES_OPERATORS_PACKAGE = ID("RFLX_Types.Operators")
+TYPES_OPERATIONS_PACKAGE = ID("RFLX_Types.Operations")
 
 LIBRARY_FILES = [
     file_name(str(p)) + ".ads"
@@ -19,15 +23,19 @@
         BUILTIN_TYPES_CONVERSIONS_PACKAGE,
         BUILTIN_TYPES_PACKAGE,
         GENERIC_TYPES_PACKAGE,
+        GENERIC_TYPES_GENERIC_OPERATORS_PACKAGE,
+        GENERIC_TYPES_GENERIC_OPERATIONS_PACKAGE,
         MESSAGE_SEQUENCE_PACKAGE,
         SCALAR_SEQUENCE_PACKAGE,
         TYPES_PACKAGE,
+        TYPES_OPERATORS_PACKAGE,
+        TYPES_OPERATIONS_PACKAGE,
     ]
 ] + [
     file_name(str(p)) + ".adb"
     for p in [
         ARITHMETIC_PACKAGE,
-        GENERIC_TYPES_PACKAGE,
+        GENERIC_TYPES_GENERIC_OPERATIONS_PACKAGE,
         MESSAGE_SEQUENCE_PACKAGE,
         SCALAR_SEQUENCE_PACKAGE,
     ]
@@ -54,6 +62,7 @@
 TYPES_BYTE_ORDER = TYPES * "Byte_Order"
 TYPES_HIGH_ORDER_FIRST = TYPES * "High_Order_First"
 TYPES_LOW_ORDER_FIRST = TYPES * "Low_Order_First"
+TYPES_OPERATIONS = TYPES_OPERATIONS_PACKAGE
 
 UNREACHABLE = ada.Call(TYPES * "Unreachable")
 

rflx/generator/generator.py

@@ -345,19 +345,21 @@ def _create_message(self, message: Message) -> dict[ID, Unit]:
         if not message.fields:
             return units
 
-        context: ty.List[ContextItem] = []
+        context: ty.List[ContextItem] = [WithClause(self._prefix * const.TYPES_PACKAGE)]
+        body_context: ty.List[ContextItem] = []
 
         if any(t.package == BUILTINS_PACKAGE for t in message.types.values()):
             context.extend(
                 [
-                    WithClause(self._prefix * const.TYPES_PACKAGE),
                     WithClause(self._prefix * const.BUILTIN_TYPES_PACKAGE),
                     WithClause(self._prefix * const.BUILTIN_TYPES_CONVERSIONS_PACKAGE),
                     UsePackageClause(self._prefix * const.BUILTIN_TYPES_CONVERSIONS_PACKAGE),
                 ]
             )
 
-        context.append(WithClause(self._prefix * const.TYPES_PACKAGE))
+        for field_type in message.field_types.values():
+            if isinstance(field_type, Scalar):
+                body_context.append(WithClause(self._prefix * const.TYPES_OPERATIONS_PACKAGE))
 
         for field_type in message.types.values():
             if field_type.package in [BUILTINS_PACKAGE, INTERNAL_PACKAGE]:
@@ -374,7 +376,7 @@ def _create_message(self, message: Message) -> dict[ID, Unit]:
             elif isinstance(field_type, Sequence):
                 context.append(WithClause(self._prefix * field_type.identifier))
 
-        unit = self._create_unit(message.identifier, context)
+        unit = self._create_unit(message.identifier, context, body_context=body_context)
         units[message.identifier] = unit
 
         scalar_fields = {}

rflx/generator/parser.py

@@ -181,7 +181,7 @@ def create_get_function(
                     [
                         ReturnStatement(
                             Call(
-                                const.TYPES * "Extract",
+                                const.TYPES_OPERATIONS * "Extract",
                                 [
                                     Variable("Ctx.Buffer"),
                                     Variable("Buffer_First"),

rflx/generator/serializer.py

@@ -747,7 +747,7 @@ def body(
                             ],
                         ),
                         CallStatement(
-                            const.TYPES * "Insert",
+                            const.TYPES_OPERATIONS * "Insert",
                             [
                                 Variable("Val"),
                                 Variable("Ctx.Buffer"),

rflx/templates/rflx_generic_types.adb → rflx/templates/rflx_generic_types-generic_operations.adb

@@ -1,6 +1,8 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 
-package body {prefix}RFLX_Generic_Types with
+with {prefix}RFLX_Arithmetic;
+
+package body {prefix}RFLX_Generic_Types.Generic_Operations with
   SPARK_Mode
 is
 
@@ -397,4 +399,4 @@ is
       Insert (U64 (Val), Buffer, First, Last, Off, Size, BO);
    end Insert;
 
-end {prefix}RFLX_Generic_Types;
+end {prefix}RFLX_Generic_Types.Generic_Operations;

rflx/templates/rflx_generic_types-generic_operations.ads

@@ -0,0 +1,100 @@
+pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+
+with {prefix}RFLX_Generic_Types.Generic_Operators;
+
+generic
+   with package Operators is new {prefix}RFLX_Generic_Types.Generic_Operators (<>);
+package {prefix}RFLX_Generic_Types.Generic_Operations with
+   SPARK_Mode,
+   Annotate =>
+     (GNATprove, Always_Return)
+is
+   use Operators;
+
+   use type U64;
+
+   function Extract
+      (Buffer : Bytes_Ptr;
+       First  : Index;
+       Last   : Index;
+       Off    : Offset;
+       Size   : Positive;
+       BO     : Byte_Order) return U64
+   with
+     Pre =>
+       (Buffer /= null
+        and then First >= Buffer'First
+        and then Last <= Buffer'Last
+        and then Size in 1 .. U64'Size
+        and then First <= Last
+        and then Last - First <= Index'Last - 1
+        and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1)
+        and then (Offset'Pos (Off) + Size - 1) / Byte'Size <= Natural'Size
+        and then (Byte'Size - Natural (Offset'Pos (Off) mod Byte'Size)) < Long_Integer'Size - 1),
+    Post =>
+       (if Size < U64'Size then Extract'Result < 2**Size);
+
+   function Extract
+      (Buffer : Bytes_Ptr;
+       First  : Index;
+       Last   : Index;
+       Off    : Offset;
+       Size   : Positive;
+       BO     : Byte_Order) return Base_Integer
+   with
+     Pre =>
+       (Buffer /= null
+        and then First >= Buffer'First
+        and then Last <= Buffer'Last
+        and then Size in 1 .. 63
+        and then First <= Last
+        and then Last - First <= Index'Last - 1
+        and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1)
+        and then (Offset'Pos (Off) + Size - 1) / Byte'Size <= Natural'Size
+        and then (Byte'Size - Natural (Offset'Pos (Off) mod Byte'Size)) < Long_Integer'Size - 1),
+    Post =>
+       (U64 (Extract'Result) < 2**Size);
+
+   procedure Insert
+      (Val    : U64;
+       Buffer : Bytes_Ptr;
+       First  : Index;
+       Last   : Index;
+       Off    : Offset;
+       Size   : Positive;
+       BO     : Byte_Order)
+   with
+     Pre =>
+       (Buffer /= null
+        and then First >= Buffer'First
+        and then Last <= Buffer'Last
+        and then Size in 1 .. U64'Size
+        and then Fits_Into (Val, Size)
+        and then First <= Last
+        and then Last - First <= Index'Last - 1
+        and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1)),
+     Post =>
+       (Buffer'First = Buffer.all'Old'First and Buffer'Last = Buffer.all'Old'Last);
+
+   procedure Insert
+      (Val    : Base_Integer;
+       Buffer : Bytes_Ptr;
+       First  : Index;
+       Last   : Index;
+       Off    : Offset;
+       Size   : Positive;
+       BO     : Byte_Order)
+   with
+     Pre =>
+       (Buffer /= null
+        and then First >= Buffer'First
+        and then Last <= Buffer'Last
+        and then Size in 1 .. 63
+        and then Fits_Into (Val, Size)
+        and then First <= Last
+        and then Last - First <= Index'Last - 1
+        and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1)),
+     Post =>
+       (Buffer'First = Buffer.all'Old'First and Buffer'Last = Buffer.all'Old'Last);
+
+end {prefix}RFLX_Generic_Types.Generic_Operations;

rflx/templates/rflx_generic_types-generic_operators.ads

@@ -0,0 +1,27 @@
+generic
+package {prefix}RFLX_Generic_Types.Generic_Operators with
+   SPARK_Mode,
+   Annotate =>
+     (GNATprove, Always_Return)
+is
+
+   function "+" (Left : Index; Right : Length) return Index is
+      (Index (Length (Left) + Right))
+   with
+     Pre =>
+       Length (Left) <= Length'Last - Right;
+
+   function "-" (Left : Index; Right : Index) return Length is
+      (Length (Left) - Length (Right))
+   with
+     Pre =>
+       Length (Left) >= Length'First + Length (Right);
+
+   function "-" (Left : Index; Right : Length) return Index is
+      (Index (Length (Left) - Right))
+   with
+     Pre =>
+       Right < Length'Last
+       and then Length (Left) >= Length (Index'First) + Right;
+
+end {prefix}RFLX_Generic_Types.Generic_Operators;

rflx/templates/rflx_generic_types.ads

@@ -28,29 +28,10 @@ is
 
    subtype Bit_Length is Custom_Bit_Length;
 
-   function "+" (Left : Index; Right : Length) return Index is
-      (Index (Length (Left) + Right))
-   with
-     Pre =>
-       Length (Left) <= Length'Last - Right;
-
    function "+" (Left : Index; Right : Index) return Index is abstract;
 
-   function "-" (Left : Index; Right : Index) return Length is
-      (Length (Left) - Length (Right))
-   with
-     Pre =>
-       Length (Left) >= Length'First + Length (Right);
-
    function "-" (Left : Index; Right : Index) return Index is abstract;
 
-   function "-" (Left : Index; Right : Length) return Index is
-      (Index (Length (Left) - Right))
-   with
-     Pre =>
-       Right < Length'Last
-       and then Length (Left) >= Length (Index'First) + Right;
-
    pragma Compile_Time_Error (Index'First /= 1, "Index'First must be 1");
 
    pragma Compile_Time_Error (Byte'Size /= 8, "Byte must be of size 8");
@@ -70,8 +51,6 @@ is
 
    subtype U64 is {prefix}RFLX_Arithmetic.U64;
 
-   use type U64;
-
    subtype Base_Integer is {prefix}RFLX_Arithmetic.Base_Integer;
 
    subtype Bit_Index is Bit_Length range 1 .. Bit_Length'Last;
@@ -101,92 +80,6 @@ is
 
    type Byte_Order is (High_Order_First, Low_Order_First);
 
-   function Extract
-      (Buffer : Bytes_Ptr;
-       First  : Index;
-       Last   : Index;
-       Off    : Offset;
-       Size   : Positive;
-       BO     : Byte_Order) return U64
-   with
-     Pre =>
-       (Buffer /= null
-        and then First >= Buffer'First
-        and then Last <= Buffer'Last
-        and then Size in 1 .. U64'Size
-        and then First <= Last
-        and then Last - First <= Index'Last - 1
-        and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1)
-        and then (Offset'Pos (Off) + Size - 1) / Byte'Size <= Natural'Size
-        and then (Byte'Size - Natural (Offset'Pos (Off) mod Byte'Size)) < Long_Integer'Size - 1),
-    Post =>
-       (if Size < U64'Size then Extract'Result < 2**Size);
-
-   function Extract
-      (Buffer : Bytes_Ptr;
-       First  : Index;
-       Last   : Index;
-       Off    : Offset;
-       Size   : Positive;
-       BO     : Byte_Order) return Base_Integer
-   with
-     Pre =>
-       (Buffer /= null
-        and then First >= Buffer'First
-        and then Last <= Buffer'Last
-        and then Size in 1 .. 63
-        and then First <= Last
-        and then Last - First <= Index'Last - 1
-        and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1)
-        and then (Offset'Pos (Off) + Size - 1) / Byte'Size <= Natural'Size
-        and then (Byte'Size - Natural (Offset'Pos (Off) mod Byte'Size)) < Long_Integer'Size - 1),
-    Post =>
-       (U64 (Extract'Result) < 2**Size);
-
-   procedure Insert
-      (Val    : U64;
-       Buffer : Bytes_Ptr;
-       First  : Index;
-       Last   : Index;
-       Off    : Offset;
-       Size   : Positive;
-       BO     : Byte_Order)
-   with
-     Pre =>
-       (Buffer /= null
-        and then First >= Buffer'First
-        and then Last <= Buffer'Last
-        and then Size in 1 .. U64'Size
-        and then Fits_Into (Val, Size)
-        and then First <= Last
-        and then Last - First <= Index'Last - 1
-        and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1)),
-     Post =>
-       (Buffer'First = Buffer.all'Old'First and Buffer'Last = Buffer.all'Old'Last);
-
-   procedure Insert
-      (Val    : Base_Integer;
-       Buffer : Bytes_Ptr;
-       First  : Index;
-       Last   : Index;
-       Off    : Offset;
-       Size   : Positive;
-       BO     : Byte_Order)
-   with
-     Pre =>
-       (Buffer /= null
-        and then First >= Buffer'First
-        and then Last <= Buffer'Last
-        and then Size in 1 .. 63
-        and then Fits_Into (Val, Size)
-        and then First <= Last
-        and then Last - First <= Index'Last - 1
-        and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1)),
-     Post =>
-       (Buffer'First = Buffer.all'Old'First and Buffer'Last = Buffer.all'Old'Last);
-
-   procedure Free is new Ada.Unchecked_Deallocation (Object => Bytes, Name => Bytes_Ptr);
-
    pragma Warnings (Off, "precondition is always False");
 
    function Unreachable return Boolean is (False) with Pre => False;
@@ -199,4 +92,6 @@ is
 
    procedure Lemma_Size (Val : Base_Integer; Size : Positive) renames {prefix}RFLX_Arithmetic.Lemma_Size;
 
+   procedure Free is new Ada.Unchecked_Deallocation (Object => Bytes, Name => Bytes_Ptr);
+
 end {prefix}RFLX_Generic_Types;