1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139 | -- Abstract :
--
-- See spec.
--
-- Copyright (C) 2017 - 2021 Free Software Foundation, Inc.
--
-- This library is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. This library is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHAN-
-- TABILITY 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.
pragma License (Modified_GPL);
package body SAL.Gen_Bounded_Definite_Vectors
with Spark_Mode
is
pragma Suppress (All_Checks);
function Length (Container : in Vector) return Ada.Containers.Count_Type
is (Ada.Containers.Count_Type (To_Peek_Index (Container.Last)));
function Is_Full (Container : in Vector) return Boolean
is begin
return Length (Container) = Capacity;
end Is_Full;
procedure Clear (Container : in out Vector)
is begin
Container.Last := No_Index;
end Clear;
function Element (Container : Vector; Index : Index_Type) return Element_Type
is (Container.Elements (Peek_Type (Index - Index_Type'First + 1)));
procedure Replace_Element
(Container : in out Vector;
Index : in Index_Type;
New_Item : in Element_Type)
is begin
Container.Elements (To_Peek_Index (Index)) := New_Item;
end Replace_Element;
function Last_Index (Container : Vector) return Extended_Index
is (Container.Last);
function To_Vector (Element : in Element_Type) return Vector
is begin
return Result : Vector do
Append (Result, Element);
end return;
end To_Vector;
procedure Append (Container : in out Vector; New_Item : in Element_Type)
is
J : constant Peek_Type := To_Peek_Index (Container.Last + 1);
begin
Container.Elements (J) := New_Item;
Container.Last := Container.Last + 1;
end Append;
procedure Prepend (Container : in out Vector; New_Item : in Element_Type)
is
J : constant Peek_Type := Peek_Type (Container.Last + 1 - Index_Type'First + 1);
begin
Container.Elements (2 .. J) := Container.Elements (1 .. J - 1);
Container.Elements (1) := New_Item;
Container.Last := Container.Last + 1;
end Prepend;
procedure Insert
(Container : in out Vector;
New_Item : in Element_Type;
Before : in Extended_Index)
is
J : constant Peek_Type := To_Peek_Index ((if Before = No_Index then Container.Last + 1 else Before));
K : constant Base_Peek_Type := To_Peek_Index (Container.Last);
begin
Container.Elements (J + 1 .. K + 1) := Container.Elements (J .. K);
Container.Elements (J) := New_Item;
Container.Last := Container.Last + 1;
end Insert;
function "+" (Item : in Element_Type) return Vector
is begin
return Result : Vector do
Append (Result, Item);
end return;
end "+";
function "&" (Left : in Vector; Right : in Element_Type) return Vector
is begin
-- WORKAROUND: If init Result with ":= Left", GNAT Community 2019
-- checks Default_Initial_Condition (which fails when Left is not
-- empty)! That is only supposed to be checked when initialized by
-- default. Reported to AdaCore as ticket S724-042. Fixed in GNAT
-- Community 2021; keeping workaround until we drop support for 2020.
return Result : Vector do
Result := Left;
Append (Result, Right);
end return;
end "&";
procedure Delete_First (Container : in out Vector; Count : in Ada.Containers.Count_Type := 1)
is
use Ada.Containers;
begin
if Count = 0 then
return;
end if;
declare
New_Last : constant Extended_Index := Extended_Index (Integer (Container.Last) - Integer (Count));
J : constant Base_Peek_Type := Base_Peek_Type (Count);
K : constant Peek_Type := To_Peek_Index (Container.Last);
begin
-- Delete items 1 .. J, shift remaining down.
Container.Elements (1 .. K - J) := Container.Elements (J + 1 .. K);
Container.Last := New_Last;
end;
end Delete_First;
procedure Delete_Last (Container : in out Vector; Count : in Ada.Containers.Count_Type := 1)
is
use Ada.Containers;
begin
if Count = 0 then
return;
end if;
Container.Last := Extended_Index (Integer (Container.Last) - Integer (Count));
end Delete_Last;
end SAL.Gen_Bounded_Definite_Vectors;
|