Remove modular integer types

Ref. #727

CHANGELOG.md

@@ -5,6 +5,12 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [Unreleased]
+
+### Removed
+
+- Modular integer types (#727)
+
 ## [0.7.1] - 2022-11-04
 
 ### Fixed

doc/language_reference/index.rst

@@ -43,36 +43,23 @@ Integer Types
 
 ..
     Integers [§T-I]
-    Modular Integers [§T-I-M]
-    Range Integers [§T-I-R]
 
 An integer type is used to represent numbers.
-Two types of integers are supported: modular type and range type.
 
 **Syntax**
 
 .. productionlist::
-   modular_type: type `name` is mod `modulus`
-   range_type: type `name` is range `first` .. `last` with Size => `number`
-   modulus: `mathematical_expression`
+   integer_type: type `name` is range `first` .. `last` with Size => `number`
    first: `mathematical_expression`
    last: `mathematical_expression`
 
 **Static Semantics**
 
-A modular type represents the values from 0 to one less than the :token:`modulus`.
-The bit size of a modular type is determined by calculating the binary logarithm of :token:`modulus`.
-
-The set of values of a range type consists of all numbers from the lower bound to the upper bound.
-For a range type the bit size has to be specified explicitly.
+The set of values of a integer type consists of all numbers from the lower bound to the upper bound.
+The bit size has to be specified explicitly.
 
 **Example**
 
-.. doc-check: rflx,basic_declaration,3
-.. code:: ada
-
-   type Address is mod 2 ** 48
-
 .. doc-check: rflx,basic_declaration,3
 .. code:: ada
 
@@ -1641,7 +1628,7 @@ A package is used to structure a specification.
    package: package `name` is
           :    { `basic_declaration` }
           : end `name` ;
-   basic_declaration: ( `modular_type` | `range_type` | `enumeration_type` | `message_type` | `type_refinement` | `session` ) ;
+   basic_declaration: ( `integer_type` | `enumeration_type` | `message_type` | `type_refinement` | `session` ) ;
 
 **Static Semantics**
 
@@ -1655,10 +1642,10 @@ By convention one protocol is specified in one package.
 
    package Ethernet is
 
-      type Address is mod 2 ** 48;
+      type Address is range 0 .. 2 ** 48 - 1 with Size => 48;
       type Type_Length is range 46 .. 2 ** 16 - 1 with Size => 16;
       type TPID is range 16#8100# .. 16#8100# with Size => 16;
-      type TCI is mod 2 ** 16;
+      type TCI is range 0 .. 2 ** 16 - 1 with Size => 16;
       type Ether_Type is
          (ET_IPv4            => 16#0800#,
           ET_ARP             => 16#0806#,

doc/user_guide/index.rst

@@ -115,7 +115,7 @@ A more detailed description can be found in the :ref:`Language Reference`.
    package TLV is
 
       type Tag is (Msg_Data => 1, Msg_Error => 3) with Size => 8;
-      type Length is mod 2 ** 16;
+      type Length is range 0 .. 2 ** 16 - 1 with Size => 16;
 
       type Message is
          message
@@ -177,7 +177,7 @@ For ``TLV`` the following types are defined in the package ``RFLX.TLV``:
 
 - ``type Tag is (Msg_Data, Msg_Error) with Size => 8``
 - ``for Tag use (Msg_Data => 1, Msg_Error => 3);``
-- ``type Length is mod 2**16``
+- ``type Length is range 0 .. 2**16 with Size => 16``
 
 All types and subprograms related to ``Message`` can be found in the package ``RFLX.TLV.Message``:
 

examples/apps/dhcp_client/specs/dhcp.rflx

@@ -35,7 +35,7 @@ package DHCP is
    with Size => 8;
 
    type Len is range 1 .. 255 with Size => 8;
-   type Subnet_Mask is mod 2 ** 32;
+   type Subnet_Mask is range 0 .. 2 ** 32 - 1 with Size => 32;
    type Routers is sequence of IPv4::Address;
    type Time_Servers is sequence of IPv4::Address;
    type Name_Servers is sequence of IPv4::Address;
@@ -66,7 +66,7 @@ package DHCP is
 
    type X_Window_System_Font_Servers is sequence of IPv4::Address;
    type X_Window_System_Display_Managers is sequence of IPv4::Address;
-   type Lease_Time is mod 2 ** 32;
+   type Lease_Time is range 0 .. 2 ** 32 - 1 with Size => 32;
 
    type Option_Overload is
       (File_Overload           => 1,
@@ -89,7 +89,7 @@ package DHCP is
 
    type Option_Codes is sequence of Code;
    type Maximum_DHCP_Message_Size is range 576 .. 2 ** 16 - 1 with Size => 16;
-   type Time_Interval is mod 2 ** 32;
+   type Time_Interval is range 0 .. 2 ** 32 - 1 with Size => 32;
 
    type Option is
       message
@@ -184,9 +184,9 @@ package DHCP is
    -- https://www.iana.org/assignments/arp-parameters/arp-parameters.xml#arp-parameters-2.
    type Hardware_Address_Type is (HT_Reserved => 0, HT_Ethernet_10 => 1) with Size => 8, Always_Valid;
    type Hardware_Address_Length is (HL_Ethernet => 6) with Size => 8;
-   type Hops is mod 2 ** 8;
-   type Transaction_ID is mod 2 ** 32;
-   type Secs is mod 2 ** 16;
+   type Hops is range 0 .. 2 ** 8 - 1 with Size => 8;
+   type Transaction_ID is range 0 .. 2 ** 32 - 1 with Size => 32;
+   type Secs is range 0 .. 2 ** 16 - 1 with Size => 16;
    type Reserved_Flags is range 0 .. 0 with Size => 15;
    type Magic_Cookie is range 16#63825363# .. 16#63825363# with Size => 32;
    type Options is sequence of Option;

examples/apps/dhcp_client/specs/ipv4.rflx

@@ -2,18 +2,18 @@ package IPv4 is
 
    type Version is range 4 .. 4 with Size => 4;
    type IHL is range 5 .. 15 with Size => 4;
-   type DCSP is mod 2 ** 6;
-   type ECN is mod 2 ** 2;
-   type Total_Length is mod 2 ** 16;
-   type Identification is mod 2 ** 16;
-   type Fragment_Offset is mod 2 ** 13;
-   type TTL is mod 2 ** 8;
+   type DCSP is range 0 .. 2 ** 6 - 1 with Size => 6;
+   type ECN is range 0 .. 2 ** 2 - 1 with Size => 2;
+   type Total_Length is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Identification is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Fragment_Offset is range 0 .. 2 ** 13 - 1 with Size => 13;
+   type TTL is range 0 .. 2 ** 8 - 1 with Size => 8;
    type Protocol is (PROTOCOL_ICMP => 1, PROTOCOL_UDP => 17) with Size => 8, Always_Valid;
-   type Header_Checksum is mod 2 ** 16;
-   type Address is mod 2 ** 32;
+   type Header_Checksum is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Address is range 0 .. 2 ** 32 - 1 with Size => 32;
 
    type Option_Class is (CONTROL => 0, DEBUGGING_AND_MEASUREMENT => 2) with Size => 2;
-   type Option_Number is mod 2 ** 5;
+   type Option_Number is range 0 .. 2 ** 5 - 1 with Size => 5;
    type Option_Length is range 2 .. 2 ** 8 - 1 with Size => 8;
 
    type Option is

examples/apps/ping/specs/icmp.rflx

@@ -36,12 +36,12 @@ package ICMP is
    with Size => 8;
 
    type Code_Zero is range 0 .. 0 with Size => 8;
-   type Checksum is mod 2 ** 16;
-   type Identifier is mod 2 ** 16;
-   type Sequence_Number is mod 2 ** 16;
-   type Pointer is mod 2 ** 8;
-   type Timestamp is mod 2 ** 32;
-   type Gateway_Internet_Address is mod 2 ** 32;
+   type Checksum is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Identifier is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Sequence_Number is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Pointer is range 0 .. 2 ** 8 - 1 with Size => 8;
+   type Timestamp is range 0 .. 2 ** 32 - 1 with Size => 32;
+   type Gateway_Internet_Address is range 0 .. 2 ** 32 - 1 with Size => 32;
    type Unused_32 is range 0 .. 0 with Size => 32;
    type Unused_24 is range 0 .. 0 with Size => 24;
 

examples/apps/ping/specs/ipv4.rflx

@@ -5,15 +5,15 @@ package IPv4 is
 
    type Version is range 4 .. 4 with Size => 4;
    type IHL is range 5 .. 15 with Size => 4;
-   type DCSP is mod 2 ** 6;
-   type ECN is mod 2 ** 2;
-   type Total_Length is mod 2 ** 16;
-   type Identification is mod 2 ** 16;
-   type Fragment_Offset is mod 2 ** 13;
-   type TTL is mod 2 ** 8;
+   type DCSP is range 0 .. 2 ** 6 - 1 with Size => 6;
+   type ECN is range 0 .. 2 ** 2 - 1 with Size => 2;
+   type Total_Length is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Identification is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Fragment_Offset is range 0 .. 2 ** 13 - 1 with Size => 13;
+   type TTL is range 0 .. 2 ** 8 - 1 with Size => 8;
    type Protocol is (P_ICMP => 1, P_UDP => 17) with Size => 8, Always_Valid;
-   type Header_Checksum is mod 2 ** 16;
-   type Address is mod 2 ** 32;
+   type Header_Checksum is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Address is range 0 .. 2 ** 32 - 1 with Size => 32;
    type Options is sequence of IPv4_Option::Option;
 
    type Packet is

examples/apps/ping/specs/ipv4_option.rflx

@@ -1,7 +1,7 @@
 package IPv4_Option is
 
    type Option_Class is (Control => 0, Debugging_And_Measurement => 2) with Size => 2;
-   type Option_Number is mod 2 ** 5;
+   type Option_Number is range 0 .. 2 ** 5 - 1 with Size => 5;
    type Option_Length is range 2 .. 2 ** 8 - 1 with Size => 8;
 
    type Option is

examples/apps/ping/src/generic_checksum.adb

@@ -18,6 +18,7 @@ is
                                          Sequence_Number : ICMP.Sequence_Number;
                                          Data            : Types.Bytes) return ICMP.Checksum
    is
+      use type Interfaces.Unsigned_16;
       use type ICMP.Checksum;
       use type Types.Index;
       Checksum : ICMP.Checksum := Shift_Left (ICMP.Checksum (ICMP.To_Base_Integer (Tag)))
@@ -37,7 +38,7 @@ is
             Checksum := Add (Checksum, Shift_Left (To_Checksum (Data (Index))));
          end if;
       end if;
-      return not Checksum;
+      return ICMP.Checksum (not Interfaces.Unsigned_16 (Checksum));
    end Echo_Request_Reply_Checksum;
 
    function Add (C1 : ICMP.Checksum;

examples/apps/ping/src/generic_socket.ads

@@ -2,7 +2,7 @@ generic
    type Element_Type is (<>);
    type Index_Type is (<>);
    type Buffer_Type is array (Index_Type range <>) of Element_Type;
-   type IP4_Address is mod <>;
+   type IP4_Address is range <>;
 package Generic_Socket with
    SPARK_Mode,
    Abstract_State => Network,

examples/apps/ping/src/icmpv4.adb

@@ -1,5 +1,5 @@
-with Basalt.Strings_Generic;
 with Interfaces;
+with Basalt.Strings_Generic;
 with RFLX.IPv4.Packet;
 with RFLX.IPv4.Contains;
 with RFLX.ICMP;
@@ -14,7 +14,7 @@ package body ICMPv4 with
 is
 
    package Checksum is new Generic_Checksum (RFLX.RFLX_Types);
-   function Image is new Basalt.Strings_Generic.Image_Modular (RFLX.ICMP.Sequence_Number);
+   function Image is new Basalt.Strings_Generic.Image_Ranged (RFLX.ICMP.Sequence_Number);
    function Image is new Basalt.Strings_Generic.Image_Ranged (RFLX.RFLX_Builtin_Types.Length);
 
    function Image (Addr : RFLX.IPv4.Address) return String with
@@ -26,15 +26,15 @@ is
 
    function Image (Addr : RFLX.IPv4.Address) return String
    is
-      use type RFLX.IPv4.Address;
+      use type Interfaces.Unsigned_32;
       subtype Octet is RFLX.IPv4.Address range 0 .. 255;
-      function Img is new Basalt.Strings_Generic.Image_Modular (Octet);
+      function Img is new Basalt.Strings_Generic.Image_Ranged (Octet);
       type Octet_Address is array (1 .. 4) of Octet;
-      Addr_Var : RFLX.IPv4.Address := Addr;
+      Addr_Var : Interfaces.Unsigned_32 := Interfaces.Unsigned_32 (Addr);
       Address  : Octet_Address;
    begin
       for O of Address loop
-         O        := Addr_Var and 16#ff#;
+         O        := Octet (Addr_Var and 16#ff#);
          Addr_Var := Addr_Var / 256;
       end loop;
       return Img (Address (4)) & "."
@@ -107,7 +107,7 @@ is
       package Int renames Interfaces;
       subtype Octet is RFLX.IPv4.Address range 0 .. 255;
       type Octet_Address is array (1 .. 4) of Octet;
-      package Val is new Basalt.Strings_Generic.Value_Option_Modular (Octet);
+      package Val is new Basalt.Strings_Generic.Value_Option_Ranged (Octet);
       Address   : Octet_Address := (others => 0);
       Oct_First : Natural;
       Oct_Last  : Natural;

examples/specs/arp.rflx

@@ -13,7 +13,7 @@ package ARP is
 
    type Opcode is (OP_REQUEST => 1, OP_REPLY => 2) with Size => 16;
 
-   type Address_Length is mod 2 ** 8;
+   type Address_Length is range 0 .. 2 ** 8 - 1 with Size => 8;
 
    type Packet_IPv4 is
       message

examples/specs/ethernet.rflx

@@ -1,9 +1,9 @@
 package Ethernet is
 
-   type Address is mod 2 ** 48;
+   type Address is range 0 .. 2 ** 48 - 1 with Size => 48;
    type Type_Length is range 46 .. 2 ** 16 - 1 with Size => 16;
    type TPID is range 16#8100# .. 16#8100# with Size => 16;
-   type TCI is mod 2 ** 16;
+   type TCI is range 0 .. 2 ** 16 - 1 with Size => 16;
    type Ether_Type is
       (ET_IPV4               => 16#0800#,
        ET_ARP                => 16#0806#,

examples/specs/http_2.rflx

@@ -1,6 +1,6 @@
 package HTTP_2 is
 
-   type Payload_Length is mod 2 ** 24;
+   type Payload_Length is range 0 .. 2 ** 24 - 1 with Size => 24;
 
    type Frame_Type is
       (DATA          => 0,
@@ -24,14 +24,14 @@ package HTTP_2 is
        MAX_HEADER_LIST_SIZE   => 16#06#)
    with Size => 16;
 
-   type Settings_Value_Generic is mod 2 ** 32;
+   type Settings_Value_Generic is range 0 .. 2 ** 32 - 1 with Size => 32;
    type Settings_Value_Enable_Push is range 0 .. 1 with Size => 32;
    type Settings_Value_Initial_Window_Size is range 0 .. 2 ** 31 - 1 with Size => 32;
    type Settings_Value_Max_Frame_Size is range 2 ** 14 .. 2 ** 24 - 1 with Size => 32;
 
    type Zero_Bit is range 0 .. 0 with Size => 1;
-   type Stream_ID is mod 2 ** 31;
-   type Weight is mod 2 ** 8;
+   type Stream_ID is range 0 .. 2 ** 31 - 1 with Size => 31;
+   type Weight is range 0 .. 2 ** 8 - 1 with Size => 8;
    type Error_Code is
       (NO_ERROR            => 16#00#,
        PROTOCOL_ERROR      => 16#01#,
@@ -50,7 +50,7 @@ package HTTP_2 is
    with Size => 32;
 
    type Window_Size_Increment is range 1 .. 2 ** 31 - 1 with Size => 31;
-   type Pad_Length is mod 2 ** 8;
+   type Pad_Length is range 0 .. 2 ** 8 - 1 with Size => 8;
 
    type Settings_Parameter is
       message

examples/specs/icmp.rflx

@@ -36,12 +36,12 @@ package ICMP is
    with Size => 8;
 
    type Code_Zero is range 0 .. 0 with Size => 8;
-   type Checksum is mod 2 ** 16;
-   type Identifier is mod 2 ** 16;
-   type Sequence_Number is mod 2 ** 16;
-   type Pointer is mod 2 ** 8;
-   type Timestamp is mod 2 ** 32;
-   type Gateway_Internet_Address is mod 2 ** 32;
+   type Checksum is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Identifier is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Sequence_Number is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Pointer is range 0 .. 2 ** 8 - 1 with Size => 8;
+   type Timestamp is range 0 .. 2 ** 32 - 1 with Size => 32;
+   type Gateway_Internet_Address is range 0 .. 2 ** 32 - 1 with Size => 32;
    type Unused_32 is range 0 .. 0 with Size => 32;
    type Unused_24 is range 0 .. 0 with Size => 24;
 

examples/specs/icmpv6.rflx

@@ -4,7 +4,7 @@ package ICMPv6 is
 
    type Reserved_8 is range 0 .. 0 with Size => 8;
    type Reserved_32 is range 0 .. 0 with Size => 32;
-   type Checksum is mod 2 ** 16;
+   type Checksum is range 0 .. 2 ** 16 - 1 with Size => 16;
 
    type Tag is
       (Destination_Unreachable     =>   1,
@@ -44,8 +44,8 @@ package ICMPv6 is
 
    type MTU is range 1280 .. 2 ** 32 - 1 with Size => 32;
    type Pointer is range 0 .. 2 ** 32 - 1 with Size => 32;
-   type Identifier is mod 2 ** 16;
-   type Sequence_Number is mod 2 ** 16;
+   type Identifier is range 0 .. 2 ** 16 - 1 with Size => 16;
+   type Sequence_Number is range 0 .. 2 ** 16 - 1 with Size => 16;
 
    type Message is
       message