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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
|
-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset 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. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================
with E_Strings.Not_SPARK;
with SPARK_IO;
with SparkMakeErrors;
package body StringList is
------------------------------------------------------------------------
-- This package body is NOT SPARK
------------------------------------------------------------------------
function "<=" (Left, Right : in E_Strings.T) return Boolean is
begin
-- uses Standard."<=" for type String
return E_Strings.Not_SPARK.Get_String (E_Str => Left) <= E_Strings.Not_SPARK.Get_String (E_Str => Right);
end "<=";
------------------------------------------------------------------------
-- Constructors
------------------------------------------------------------------------
procedure Add_To_Front (To_List : in out Object;
The_Item : in E_Strings.T) is
begin
To_List := new Node'(The_Item => The_Item,
Next => To_List);
exception
when others =>
SparkMakeErrors.Fatal ("Exception raised in StringList.Add_To_Front");
end Add_To_Front;
procedure Add_To_Back (To_List : in out Object;
The_Item : in E_Strings.T) is
Current_Node : Object;
New_Node : Object;
begin
-- Create new node
New_Node := new Node'(The_Item => The_Item,
Next => Null_Object);
if To_List = Null_Object then
To_List := New_Node;
else
Current_Node := To_List;
-- Find the final node in the list
while Current_Node.Next /= Null_Object loop
Current_Node := Current_Node.Next;
end loop;
-- Link in the new node
Current_Node.Next := New_Node;
end if;
exception
when others =>
SparkMakeErrors.Fatal ("Exception raised in StringList.Add_To_Back");
end Add_To_Back;
procedure Add_In_Lex_Order (To_List : in out Object;
The_Item : in E_Strings.T) is
Current_Node : Object;
Prev_Node : Object;
New_Node : Object;
begin
-- Create new node
New_Node := new Node'(The_Item => The_Item,
Next => Null_Object);
if To_List = Null_Object then
-- To_List is empty, so
To_List := New_Node;
else
Current_Node := To_List;
Prev_Node := Null_Object;
-- Find spot between Prev_Node and Current_Node where New_Node
-- needs to be inserted. Note uses "<=" operator for
-- EString.T defined above.
while Current_Node.The_Item <= The_Item loop
Prev_Node := Current_Node;
Current_Node := Current_Node.Next;
exit when Current_Node = Null_Object;
end loop;
-- Link New_Node in before Current_Node
New_Node.Next := Current_Node;
if Prev_Node = Null_Object then
-- No previous node - New_Node must be the new head of To_List
To_List := New_Node;
else
-- Link previous node to New_Node
Prev_Node.Next := New_Node;
end if;
end if;
exception
when others =>
SparkMakeErrors.Fatal ("Exception raised in StringList.Add_In_Lex_Order");
end Add_In_Lex_Order;
function Get_First (In_List : Object) return Iterator is
begin
return Iterator (In_List);
exception
when others =>
SparkMakeErrors.Fatal ("Exception raised in StringList.Get_First");
return Null_Iterator;
end Get_First;
function Next (It : Iterator) return Iterator is
begin
return Iterator (It.all.Next);
exception
when others =>
SparkMakeErrors.Fatal ("Exception raised in StringList.Next");
return Null_Iterator;
end Next;
------------------------------------------------------------------------
-- Accessors
------------------------------------------------------------------------
function Is_Null (It : Iterator) return Boolean is
begin
return It = Null_Iterator;
exception
when others =>
SparkMakeErrors.Fatal ("Exception raised in StringList.Is_Null");
return False;
end Is_Null;
function Value (It : Iterator) return E_Strings.T is
begin
return It.all.The_Item;
exception
when others =>
SparkMakeErrors.Fatal ("Exception raised in StringList.Value");
return E_Strings.Empty_String;
end Value;
------------------------------------------------------------------------
-- Debug support
------------------------------------------------------------------------
procedure Output (The_List : in Object;
How : in Orientation) is
It : Iterator;
begin
It := Get_First (In_List => The_List);
if Is_Null (It => It) then
SPARK_IO.Put_String (SPARK_IO.Standard_Output, "<<Empty List>>", 0);
else
loop
if How = Vertical then -- expect stable expression
E_Strings.Put_Line (File => SPARK_IO.Standard_Output,
E_Str => Value (It));
else
E_Strings.Put_String (File => SPARK_IO.Standard_Output,
E_Str => Value (It));
end if;
It := Next (It);
exit when Is_Null (It => It);
if How = Horizontal then
SPARK_IO.Put_String (SPARK_IO.Standard_Output, ", ", 0);
end if;
end loop;
end if;
if How = Horizontal then
SPARK_IO.New_Line (File => SPARK_IO.Standard_Output,
Spacing => 1);
end if;
exception
when others =>
SparkMakeErrors.Fatal ("Exception raised in StringList.Output");
end Output;
end StringList;
|
