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
|
-------------------------------------------------------------------------------
-- (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.
--
--=============================================================================
separate (SPARKProgram)
package body Iteration is
procedure FindNextAlphabetic (TheHeap : in Heap.HeapRecord;
TheIterator : in out Iterator)
--# global in LexTokenManager.State;
--# derives TheIterator from *,
--# LexTokenManager.State,
--# TheHeap;
is
FirstMember : LexTokenManager.Seq_Algebra.Member_Of_Seq;
Placeholder : LexTokenManager.Lex_String;
SeqComplete : Boolean;
NextItem : LexTokenManager.Seq_Algebra.Member_Of_Seq;
ThisMember : LexTokenManager.Seq_Algebra.Member_Of_Seq;
ThisLexString : LexTokenManager.Lex_String;
NextItemLex : LexTokenManager.Lex_String;
begin
---------------------------------------------------------------------------------------
-- We have a sequence of (lex) strings in no particular order. To return them
-- in alphabetical order we go through the whole sequence looking for the first
-- item in alphabetical order, return it, then start again looking for the next
-- item and so on. To do this we need to use a placeholder to tell us what the last
-- thing we returned was so that the state of the search is preserved between calls.
--
-- Each time this routine is called it loops over the whole sequence, comparing each
-- item with the placeholder to try and find the next best match.
-- (Note that it may be possible, and more efficient, to do this by deleting items
-- from the sequence once they have been returned, but need to be sure that sequences
-- are never re-used, eg when several exports have the same set of imports.)
-- Consider doing this later if performance is an issue.
--
-- We know we have finished when we have traversed the whole sequence without finding
-- a better match.
--
-- Note:
-- The sequence is very likely to be in alphabetical order already. If it is then
-- we can just write it straight out. If SPARKFormat needs to be made faster then
-- this subprogram could check whether the sequence is already sorted on the first
-- pass through (easy to check). If it is then it could just be written out in the
-- order in which items occur in the sequence.
---------------------------------------------------------------------------------------
FirstMember := TheIterator.First_Member;
Placeholder := TheIterator.Placeholder;
ThisMember := FirstMember;
SeqComplete := True;
-- If this is the first call then initialize NextItemLex to first item in sequence.
-- Otherwise, the best match so far is the last thing that was written.
if LexTokenManager.Lex_String_Case_Insensitive_Compare (Lex_Str1 => Placeholder,
Lex_Str2 => LexTokenManager.Null_String) =
LexTokenManager.Str_Eq then
NextItemLex := LexTokenManager.Seq_Algebra.Value_Of_Member (The_Heap => TheHeap,
M => ThisMember);
NextItem := ThisMember;
else
NextItemLex := Placeholder;
NextItem := ThisMember;
end if;
loop
exit when LexTokenManager.Seq_Algebra.Is_Null_Member (M => ThisMember);
ThisLexString := LexTokenManager.Seq_Algebra.Value_Of_Member (The_Heap => TheHeap,
M => ThisMember);
-- For this to be the next item to write it has to come strictly after the last item that was written
-- (Note that this test will fail in the case of MultiplyToken so we don't need a separate test to avoid
-- writing it out in the middle of a list.)
if LexTokenManager.Lex_String_Case_Insensitive_Compare (Lex_Str1 => ThisLexString,
Lex_Str2 => Placeholder) =
LexTokenManager.Str_Second then
-- If NextItemLex = Placeholder it indicates that we haven't updated NextItemLex on this
-- pass, so NextItemLex becomes the current item (provided current item is after Placeholder).
-- Or, if this item is before (or equal to) the current best match then it becomes the new best match.
if (LexTokenManager.Lex_String_Case_Insensitive_Compare (Lex_Str1 => NextItemLex,
Lex_Str2 => Placeholder) =
LexTokenManager.Str_Eq)
or else (LexTokenManager.Lex_String_Case_Insensitive_Compare (Lex_Str1 => NextItemLex,
Lex_Str2 => ThisLexString) /=
LexTokenManager.Str_First) then
NextItemLex := ThisLexString;
NextItem := ThisMember;
SeqComplete := False;
end if;
end if;
ThisMember := LexTokenManager.Seq_Algebra.Next_Member (The_Heap => TheHeap,
M => ThisMember);
end loop;
TheIterator.Placeholder := LexTokenManager.Seq_Algebra.Value_Of_Member (The_Heap => TheHeap,
M => NextItem);
TheIterator.Current_Member := NextItem;
TheIterator.Complete := SeqComplete;
end FindNextAlphabetic;
procedure Initialise
(The_Heap : in Heap.HeapRecord;
The_Seq : in LexTokenManager.Seq_Algebra.Seq;
The_Iterator : out Iterator)
is
begin
The_Iterator :=
Iterator'
(First_Member => LexTokenManager.Seq_Algebra.First_Member (The_Heap => The_Heap,
S => The_Seq),
Current_Member => LexTokenManager.Seq_Algebra.First_Member (The_Heap => The_Heap,
S => The_Seq),
Placeholder => LexTokenManager.Null_String,
Complete => LexTokenManager.Seq_Algebra.Is_Empty_Seq (The_Heap => The_Heap,
S => The_Seq));
FindNextAlphabetic (TheHeap => The_Heap,
TheIterator => The_Iterator);
end Initialise;
procedure Next (The_Heap : in Heap.HeapRecord;
The_Iterator : in out Iterator) is
begin
if not LexTokenManager.Seq_Algebra.Is_Null_Member (M => The_Iterator.Current_Member) then
FindNextAlphabetic (TheHeap => The_Heap,
TheIterator => The_Iterator);
else
-- This indicates that CurrentMember has not changed.
The_Iterator.Complete := True;
end if;
end Next;
function Complete (The_Iterator : Iterator) return Boolean is
begin
return The_Iterator.Complete;
end Complete;
function Current_String (The_Iterator : Iterator) return LexTokenManager.Lex_String is
begin
return The_Iterator.Placeholder;
end Current_String;
function Current_Member (The_Iterator : Iterator) return LexTokenManager.Seq_Algebra.Member_Of_Seq is
begin
return The_Iterator.Current_Member;
end Current_Member;
end Iteration;
|
