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
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
|
-------------------------------------------------------------------------------
-- (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.
--
--=============================================================================
--------------------------------------------------------------------------------
--Synopsis: --
-- --
-- Package containing subprograms to facilitate incremental parsing of a --
-- simplifier log file. --
-- The basic mode of operation is: --
-- Initialize the log file for parsing - Init(Logfile, ParserInfo, Status) --
-- Provided Status = Success finde the section of interest, e.g. --
-- Find_Rule_Summary(ParserInfo, Status).
-- Provided Status = Success obtain next subsection, e.g,
-- Get_Next_Rulefile(ParserInfo, Rulefile, Status)
-- Further subsections may be parsed similarly, e.g.,
-- Get_Next_Rule and Get_Next_VC.
-- When a subsection has been exhuasted a status of Not_Found is
-- returned and the previous higher level subsection parser should
-- be invoked again, e.g., when Get_Next_VC returns a Status of
-- Not_Found this means the next rule should be obtained via a call
-- to Get_Next_Rule.
--------------------------------------------------------------------------------
with E_Strings;
with SPARK_IO;
use type SPARK_IO.File_Status;
--# inherit Ada.Characters.Latin_1,
--# E_Strings,
--# SPARK_IO;
package SLG_Parser is
type Log_Info_T is private;
type Log_Status_T is (Success, Failure, Not_Found, Unexpected_Text, End_Of_File);
-- Given the file name of a simplifier log file opens the file for
-- incremental parsing.
-- Status = Success if the file is opened without errors
-- Status = Failure otherwise.
procedure Init (Logfile_Name : in E_Strings.T;
Info : out Log_Info_T;
Status : out Log_Status_T);
--# global in out SPARK_IO.File_Sys;
--# derives Info,
--# SPARK_IO.File_Sys,
--# Status from Logfile_Name,
--# SPARK_IO.File_Sys;
-- Locates the start of the log file section which contains the list of
-- of user rule files read in (but not necessarily used).
-- Status = Success if the section is found
-- Status = End_Of_File if the end of file is encountered during the find
-- operation
-- Status = Not_Found otherwise.
procedure Find_Rulefiles_Read (Info : in out Log_Info_T;
Status : out Log_Status_T);
--# global in out SPARK_IO.File_Sys;
--# derives Info,
--# SPARK_IO.File_Sys,
--# Status from Info,
--# SPARK_IO.File_Sys;
-- Locates the start of the log file section which contains the reporting
-- of user rule file syntax errors ready for parsing this section.
-- Status = Success if the section is found
-- Status = End_Of_File if the end of file is encountered during the find
-- operation
-- Status = Not_Found otherwise.
procedure Find_Rule_Syntax_Errors (Info : in out Log_Info_T;
Status : out Log_Status_T);
--# global in out SPARK_IO.File_Sys;
--# derives Info,
--# SPARK_IO.File_Sys,
--# Status from Info,
--# SPARK_IO.File_Sys;
-- Successively obtain the next rule file name which contains a syntax error.
-- Status = Success if a rule file name is returned in RuleFile,
-- Status = End_Of_File if this is encountered,
-- Status = Unexpected_Text if a syntax error is encountered,
-- Status = Not_Found otherwise.
procedure Get_Next_Rulefile_Syntax_Error (Info : in out Log_Info_T;
Rulefile : out E_Strings.T;
Status : out Log_Status_T);
--# global in out SPARK_IO.File_Sys;
--# derives Info,
--# Rulefile,
--# SPARK_IO.File_Sys,
--# Status from Info,
--# SPARK_IO.File_Sys;
-- Locates the start of the log file section which contains the use
-- of user rule file summary ready for parsing this section.
-- Status = Success if the section is found
-- Status = End_Of_File if the end of file is encountered during the find
-- operation
-- Status = Not_Found otherwise.
procedure Find_Rule_Summary (Info : in out Log_Info_T;
Status : out Log_Status_T);
--# global in out SPARK_IO.File_Sys;
--# derives Info,
--# SPARK_IO.File_Sys,
--# Status from Info,
--# SPARK_IO.File_Sys;
-- Successively obtain the next rule file name from the rule file summary.
-- Status = Success if a rule file name is returned in RuleFile,
-- Status = End_Of_File if this is encountered,
-- Status = Unexpected_Text if a syntax error is encountered,
-- Status = Not_Found otherwise.
procedure Get_Next_Rulefile (Info : in out Log_Info_T;
Rulefile : out E_Strings.T;
Status : out Log_Status_T);
--# global in out SPARK_IO.File_Sys;
--# derives Info,
--# Rulefile,
--# SPARK_IO.File_Sys,
--# Status from Info,
--# SPARK_IO.File_Sys;
-- If Get_Next_Rulefile succeeds, returning a rule file name in
-- RuleFile, then without any intervening calls to other
-- subprograms of Logfile_Incremental_Parser
-- successive calls toGet_Next_Rule retrieve the next rule name
-- of RuleFile from the summary.
-- Status = Success if a rule name is returned in Rule,
-- Status = End_Of_File if this is encountered,
-- Status = Unexpected_Text if a syntax error is encountered,
-- Status = Not_Found otherwise.
procedure Get_Next_Rule (Info : in out Log_Info_T;
Rule : out E_Strings.T;
Status : out Log_Status_T);
--# global in out SPARK_IO.File_Sys;
--# derives Info,
--# Rule,
--# SPARK_IO.File_Sys,
--# Status from Info,
--# SPARK_IO.File_Sys;
-- If Get_Next_Rule succeeds, returning a rule name in Rule,
-- then without any intervening calls to other subprograms
-- of Logfile_Incremental_Parser successive calls to Get_Next_Rule
-- retrieve the next VC in which Rule is used from the summary.
-- Status = Success if a VC number is returned in VC_Number,
-- Status = End_Of_File if this is encountered,
-- Status = Unexpected_Text if a syntax error is encountered,
-- Status = Not_Found otherwise.
procedure Get_Next_VC (Info : in out Log_Info_T;
VC_Number : out E_Strings.T;
Status : out Log_Status_T);
--# global in out SPARK_IO.File_Sys;
--# derives Info,
--# SPARK_IO.File_Sys,
--# Status,
--# VC_Number from Info,
--# SPARK_IO.File_Sys;
-- Closes the Logfile and completes the incremental parse.
procedure Finalise (Info : in out Log_Info_T);
--# global in out SPARK_IO.File_Sys;
--# derives Info,
--# SPARK_IO.File_Sys from *,
--# Info;
private
-- The Simplifier logfile has a number of three digit keys
-- (see the simplifier user guide). This enumeration type
-- represents the set of three digit codes used in the log.
type Log_Key is (
-- The following literals represent the keys which denote
-- headers for the various sections of the simplifier log.
---------------------------------------------------------
Read_Rulefiles_Header,
Syntax_Error_Header,
No_Semantic_Checks_Header,
VC_Header,
VC_Summary_Header,
Overall_Summary_Header,
----------------------------------------------------------
-- The remainder of the simplifier logfile keys.
Load_Rulefile,
Syntax_Error_In_Rulefile,
Simplified,
Proved,
Restructured,
Contradiction,
Hyp_Eliminated,
Hyp_Added,
Substitution,
New_Hyp_From_Subs,
Rulefile_Use,
Rule_Use,
Conclusions,
Hypotheses,
VCs_Using_Rule,
----------------------------------------------------------
-- Not keys. To support processing only.
Been_Initialised,
Not_A_Recognised_Key,
No_Room_For_Key,
Reached_EOF);
-- Subtype for all legal log keys.
subtype Legal_Log_Keys is Log_Key range Read_Rulefiles_Header .. VCs_Using_Rule;
-- Subtype just including the section headers.
subtype Log_Headers is Legal_Log_Keys range Read_Rulefiles_Header .. Overall_Summary_Header;
subtype Three_T is Positive range 1 .. 3;
subtype Key_String is String (Three_T);
type Log_Info_T is record
File_Handle : SPARK_IO.File_Type;
Key : Log_Key;
Key_Found : Boolean;
Posn : E_Strings.Lengths;
Curr_Line : E_Strings.T;
end record;
end SLG_Parser;
|
