------------------------------------------------------------------------------
-- --
-- GNAT RUN-TIME COMPONENTS --
-- --
-- A D A . S T R I N G S . M A P S --
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2023, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
-- --
-- GNAT was originally developed by the GNAT team at New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
-- Note: parts of this code are derived from the ADAR.CSH public domain
-- Ada 83 versions of the Appendix C string handling packages. The main
-- differences are that we avoid the use of the minimize function which
-- is bit-by-bit or character-by-character and therefore rather slow.
-- Generally for character sets we favor the full 32-byte representation.
-- Assertions, ghost code and loop invariants in this unit are meant for
-- analysis only, not for run-time checking, as it would be too costly
-- otherwise. This is enforced by setting the assertion policy to Ignore.
pragma Assertion_Policy (Assert => Ignore,
Ghost => Ignore,
Loop_Invariant => Ignore);
package body Ada.Strings.Maps
with SPARK_Mode
is
---------
-- "-" --
---------
function "-" (Left, Right : Character_Set) return Character_Set is
begin
return Left and not Right;
end "-";
---------
-- "=" --
---------
function "=" (Left, Right : Character_Set) return Boolean is
begin
return Character_Set_Internal (Left) = Character_Set_Internal (Right);
end "=";
-----------
-- "and" --
-----------
function "and" (Left, Right : Character_Set) return Character_Set is
begin
return Character_Set
(Character_Set_Internal (Left) and Character_Set_Internal (Right));
end "and";
-----------
-- "not" --
-----------
function "not" (Right : Character_Set) return Character_Set is
begin
return Character_Set (not Character_Set_Internal (Right));
end "not";
----------
-- "or" --
----------
function "or" (Left, Right : Character_Set) return Character_Set is
begin
return Character_Set
(Character_Set_Internal (Left) or Character_Set_Internal (Right));
end "or";
-----------
-- "xor" --
-----------
function "xor" (Left, Right : Character_Set) return Character_Set is
begin
return Character_Set
(Character_Set_Internal (Left) xor Character_Set_Internal (Right));
end "xor";
-----------
-- Is_In --
-----------
function Is_In
(Element : Character;
Set : Character_Set) return Boolean
is
(Set (Element));
---------------
-- Is_Subset --
---------------
function Is_Subset
(Elements : Character_Set;
Set : Character_Set) return Boolean
is
begin
return (Elements and Set) = Elements;
end Is_Subset;
---------------
-- To_Domain --
---------------
function To_Domain (Map : Character_Mapping) return Character_Sequence is
Result : String (1 .. Map'Length) with Relaxed_Initialization;
J : Natural;
type Character_Index is array (Character) of Natural with Ghost;
Indexes : Character_Index := [others => 0] with Ghost;
begin
J := 0;
for C in Map'Range loop
if Map (C) /= C then
J := J + 1;
Result (J) := C;
Indexes (C) := J;
end if;
pragma Loop_Invariant (if Map = Identity then J = 0);
pragma Loop_Invariant (J <= Character'Pos (C) + 1);
pragma Loop_Invariant (Result (1 .. J)'Initialized);
pragma Loop_Invariant (for all K in 1 .. J => Result (K) <= C);
pragma Loop_Invariant
(SPARK_Proof_Sorted_Character_Sequence (Result (1 .. J)));
pragma Loop_Invariant
(for all D in Map'First .. C =>
(if Map (D) = D then
Indexes (D) = 0
else
Indexes (D) in 1 .. J
and then Result (Indexes (D)) = D));
pragma Loop_Invariant
(for all Char of Result (1 .. J) => Map (Char) /= Char);
end loop;
return Result (1 .. J);
end To_Domain;
----------------
-- To_Mapping --
----------------
function To_Mapping
(From, To : Character_Sequence) return Character_Mapping
is
Result : Character_Mapping with Relaxed_Initialization;
Inserted : Character_Set := Null_Set;
From_Len : constant Natural := From'Length;
To_Len : constant Natural := To'Length;
begin
if From_Len /= To_Len then
raise Strings.Translation_Error;
end if;
for Char in Character loop
Result (Char) := Char;
pragma Loop_Invariant (Result (Result'First .. Char)'Initialized);
pragma Loop_Invariant
(for all C in Result'First .. Char => Result (C) = C);
end loop;
for J in From'Range loop
if Inserted (From (J)) then
raise Strings.Translation_Error;
end if;
Result (From (J)) := To (J - From'First + To'First);
Inserted (From (J)) := True;
pragma Loop_Invariant (Result'Initialized);
pragma Loop_Invariant
(for all K in From'First .. J =>
Result (From (K)) = To (K - From'First + To'First)
and then Inserted (From (K)));
pragma Loop_Invariant
(for all Char in Character =>
(Inserted (Char) =
(for some K in From'First .. J => Char = From (K))));
pragma Loop_Invariant
(for all Char in Character =>
(if not Inserted (Char) then Result (Char) = Char));
pragma Loop_Invariant
(if (for all K in From'First .. J =>
From (K) = To (J - From'First + To'First))
then Result = Identity);
end loop;
return Result;
end To_Mapping;
--------------
-- To_Range --
--------------
function To_Range (Map : Character_Mapping) return Character_Sequence is
-- Extract from the postcondition of To_Domain the essential properties
-- that define Seq as the domain of Map.
function Is_Domain
(Map : Character_Mapping;
Seq : Character_Sequence)
return Boolean
is
(Seq'First = 1
and then
SPARK_Proof_Sorted_Character_Sequence (Seq)
and then
(for all Char in Character =>
(if (for all X of Seq => X /= Char)
then Map (Char) = Char))
and then
(for all Char of Seq => Map (Char) /= Char))
with
Ghost;
-- Given Map, there is a unique sequence Seq for which
-- Is_Domain(Map,Seq) holds.
procedure Lemma_Domain_Unicity
(Map : Character_Mapping;
Seq1, Seq2 : Character_Sequence)
with
Ghost,
Pre => Is_Domain (Map, Seq1)
and then Is_Domain (Map, Seq2),
Post => Seq1 = Seq2;
-- Isolate the proof that To_Domain(Map) returns a sequence for which
-- Is_Domain holds.
procedure Lemma_Is_Domain (Map : Character_Mapping)
with
Ghost,
Post => Is_Domain (Map, To_Domain (Map));
-- Deduce the alternative expression of sortedness from the one in
-- SPARK_Proof_Sorted_Character_Sequence which compares consecutive
-- elements.
procedure Lemma_Is_Sorted (Seq : Character_Sequence)
with
Ghost,
Pre => SPARK_Proof_Sorted_Character_Sequence (Seq),
Post => (for all J in Seq'Range =>
(for all K in Seq'Range =>
(if J < K then Seq (J) < Seq (K))));
--------------------------
-- Lemma_Domain_Unicity --
--------------------------
procedure Lemma_Domain_Unicity
(Map : Character_Mapping;
Seq1, Seq2 : Character_Sequence)
is
J : Positive := 1;
begin
while J <= Seq1'Last
and then J <= Seq2'Last
and then Seq1 (J) = Seq2 (J)
loop
pragma Loop_Invariant
(Seq1 (Seq1'First .. J) = Seq2 (Seq2'First .. J));
pragma Loop_Variant (Increases => J);
if J = Positive'Last then
return;
end if;
J := J + 1;
end loop;
Lemma_Is_Sorted (Seq1);
Lemma_Is_Sorted (Seq2);
if J <= Seq1'Last
and then J <= Seq2'Last
then
if Seq1 (J) < Seq2 (J) then
pragma Assert (for all X of Seq2 => X /= Seq1 (J));
pragma Assert (Map (Seq1 (J)) = Seq1 (J));
pragma Assert (False);
else
pragma Assert (for all X of Seq1 => X /= Seq2 (J));
pragma Assert (Map (Seq2 (J)) = Seq2 (J));
pragma Assert (False);
end if;
elsif J <= Seq1'Last then
pragma Assert (for all X of Seq2 => X /= Seq1 (J));
pragma Assert (Map (Seq1 (J)) = Seq1 (J));
pragma Assert (False);
elsif J <= Seq2'Last then
pragma Assert (for all X of Seq1 => X /= Seq2 (J));
pragma Assert (Map (Seq2 (J)) = Seq2 (J));
pragma Assert (False);
end if;
end Lemma_Domain_Unicity;
---------------------
-- Lemma_Is_Domain --
---------------------
procedure Lemma_Is_Domain (Map : Character_Mapping) is
Ignore : constant Character_Sequence := To_Domain (Map);
begin
null;
end Lemma_Is_Domain;
---------------------
-- Lemma_Is_Sorted --
---------------------
procedure Lemma_Is_Sorted (Seq : Character_Sequence) is
begin
for A in Seq'Range loop
exit when A = Positive'Last;
for B in A + 1 .. Seq'Last loop
pragma Loop_Invariant
(for all K in A + 1 .. B => Seq (A) < Seq (K));
end loop;
pragma Loop_Invariant
(for all J in Seq'First .. A =>
(for all K in Seq'Range =>
(if J < K then Seq (J) < Seq (K))));
end loop;
end Lemma_Is_Sorted;
-- Local variables
Result : String (1 .. Map'Length) with Relaxed_Initialization;
J : Natural;
-- Repeat the computation from To_Domain in ghost code, in order to
-- prove the relationship between Result and To_Domain(Map).
Domain : String (1 .. Map'Length) with Ghost, Relaxed_Initialization;
type Character_Index is array (Character) of Natural with Ghost;
Indexes : Character_Index := [others => 0] with Ghost;
-- Start of processing for To_Range
begin
J := 0;
for C in Map'Range loop
if Map (C) /= C then
J := J + 1;
Result (J) := Map (C);
Domain (J) := C;
Indexes (C) := J;
end if;
-- Repeat the loop invariants from To_Domain regarding Domain and
-- Indexes. Add similar loop invariants for Result and Indexes.
pragma Loop_Invariant (J <= Character'Pos (C) + 1);
pragma Loop_Invariant (Result (1 .. J)'Initialized);
pragma Loop_Invariant (Domain (1 .. J)'Initialized);
pragma Loop_Invariant (for all K in 1 .. J => Domain (K) <= C);
pragma Loop_Invariant
(SPARK_Proof_Sorted_Character_Sequence (Domain (1 .. J)));
pragma Loop_Invariant
(for all D in Map'First .. C =>
(if Map (D) = D then
Indexes (D) = 0
else
Indexes (D) in 1 .. J
and then Domain (Indexes (D)) = D
and then Result (Indexes (D)) = Map (D)));
pragma Loop_Invariant
(for all Char of Domain (1 .. J) => Map (Char) /= Char);
pragma Loop_Invariant
(for all K in 1 .. J => Result (K) = Map (Domain (K)));
end loop;
-- Show the equality of Domain and To_Domain(Map)
Lemma_Is_Domain (Map);
Lemma_Domain_Unicity (Map, Domain (1 .. J), To_Domain (Map));
pragma Assert
(for all K in 1 .. J => Domain (K) = To_Domain (Map) (K));
pragma Assert (To_Domain (Map)'Length = J);
return Result (1 .. J);
end To_Range;
---------------
-- To_Ranges --
---------------
function To_Ranges (Set : Character_Set) return Character_Ranges is
Max_Ranges : Character_Ranges (1 .. Set'Length / 2 + 1)
with Relaxed_Initialization;
Range_Num : Natural;
C : Character;
C_Iter : Character with Ghost;
begin
C := Character'First;
Range_Num := 0;
loop
C_Iter := C;
-- Skip gap between subsets
while not Set (C) loop
pragma Loop_Invariant
(Character'Pos (C) >= Character'Pos (C'Loop_Entry));
pragma Loop_Invariant
(for all Char in C'Loop_Entry .. C => not Set (Char));
pragma Loop_Variant (Increases => C);
exit when C = Character'Last;
C := Character'Succ (C);
end loop;
exit when not Set (C);
Range_Num := Range_Num + 1;
Max_Ranges (Range_Num).Low := C;
-- Span a subset
loop
pragma Loop_Invariant
(Character'Pos (C) >= Character'Pos (C'Loop_Entry));
pragma Loop_Invariant
(for all Char in C'Loop_Entry .. C =>
(if Char /= C then Set (Char)));
pragma Loop_Variant (Increases => C);
exit when not Set (C) or else C = Character'Last;
C := Character'Succ (C);
end loop;
if Set (C) then
Max_Ranges (Range_Num).High := C;
exit;
else
Max_Ranges (Range_Num).High := Character'Pred (C);
end if;
pragma Assert
(for all Char in C_Iter .. C =>
(Set (Char) =
(Char in Max_Ranges (Range_Num).Low ..
Max_Ranges (Range_Num).High)));
pragma Assert
(for all Char in Character'First .. C_Iter =>
(if Char /= C_Iter then
(Set (Char) =
(for some Span of Max_Ranges (1 .. Range_Num - 1) =>
Char in Span.Low .. Span.High))));
pragma Loop_Invariant (2 * Range_Num <= Character'Pos (C) + 1);
pragma Loop_Invariant (Max_Ranges (1 .. Range_Num)'Initialized);
pragma Loop_Invariant (not Set (C));
pragma Loop_Invariant
(for all Char in Character'First .. C =>
(Set (Char) =
(for some Span of Max_Ranges (1 .. Range_Num) =>
Char in Span.Low .. Span.High)));
pragma Loop_Invariant
(for all Span of Max_Ranges (1 .. Range_Num) =>
(for all Char in Span.Low .. Span.High => Set (Char)));
pragma Loop_Variant (Increases => Range_Num);
end loop;
return Max_Ranges (1 .. Range_Num);
end To_Ranges;
-----------------
-- To_Sequence --
-----------------
function To_Sequence (Set : Character_Set) return Character_Sequence is
Result : String (1 .. Character'Pos (Character'Last) + 1)
with Relaxed_Initialization;
Count : Natural := 0;
begin
for Char in Set'Range loop
if Set (Char) then
Count := Count + 1;
Result (Count) := Char;
end if;
pragma Loop_Invariant (Count <= Character'Pos (Char) + 1);
pragma Loop_Invariant (Result (1 .. Count)'Initialized);
pragma Loop_Invariant (for all K in 1 .. Count => Result (K) <= Char);
pragma Loop_Invariant
(SPARK_Proof_Sorted_Character_Sequence (Result (1 .. Count)));
pragma Loop_Invariant
(for all C in Set'First .. Char =>
(Set (C) = (for some X of Result (1 .. Count) => C = X)));
pragma Loop_Invariant
(for all Char of Result (1 .. Count) => Is_In (Char, Set));
end loop;
return Result (1 .. Count);
end To_Sequence;
------------
-- To_Set --
------------
function To_Set (Ranges : Character_Ranges) return Character_Set is
Result : Character_Set := Null_Set;
begin
for R in Ranges'Range loop
for C in Ranges (R).Low .. Ranges (R).High loop
Result (C) := True;
pragma Loop_Invariant
(for all Char in Character =>
Result (Char) =
((for some Prev in Ranges'First .. R - 1 =>
Char in Ranges (Prev).Low .. Ranges (Prev).High)
or else Char in Ranges (R).Low .. C));
end loop;
pragma Loop_Invariant
(for all Char in Character =>
Result (Char) =
(for some Prev in Ranges'First .. R =>
Char in Ranges (Prev).Low .. Ranges (Prev).High));
end loop;
return Result;
end To_Set;
function To_Set (Span : Character_Range) return Character_Set is
Result : Character_Set := Null_Set;
begin
for C in Span.Low .. Span.High loop
Result (C) := True;
pragma Loop_Invariant
(for all Char in Character =>
Result (Char) = (Char in Span.Low .. C));
end loop;
return Result;
end To_Set;
function To_Set (Sequence : Character_Sequence) return Character_Set is
Result : Character_Set := Null_Set;
begin
for J in Sequence'Range loop
Result (Sequence (J)) := True;
pragma Loop_Invariant
(for all Char in Character =>
Result (Char) =
(for some K in Sequence'First .. J => Char = Sequence (K)));
end loop;
return Result;
end To_Set;
function To_Set (Singleton : Character) return Character_Set is
Result : Character_Set := Null_Set;
begin
Result (Singleton) := True;
return Result;
end To_Set;
-----------
-- Value --
-----------
function Value
(Map : Character_Mapping;
Element : Character) return Character
is
(Map (Element));
end Ada.Strings.Maps;