1/*
2
3    This file is part of the Maude 2 interpreter.
4
5    Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
6
7    This program is free software; you can redistribute it and/or modify
8    it under the terms of the GNU General Public License as published by
9    the Free Software Foundation; either version 2 of the License, or
10    (at your option) any later version.
11
12    This program is distributed in the hope that it will be useful,
13    but WITHOUT ANY WARRANTY; without even the implied warranty of
14    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15    GNU General Public License for more details.
16
17    You should have received a copy of the GNU General Public License
18    along with this program; if not, write to the Free Software
19    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
20
21*/
22
23//
24//	Parser for Maude surface syntax.
25//
26
27%{
28#include <string>
29#include <stack>
30
31//      utility stuff
32#include "macros.hh"
33#include "vector.hh"
34
35//	forward declarations
36#include "interface.hh"
37#include "core.hh"
38#include "higher.hh"
39#include "strategyLanguage.hh"
40#include "mixfix.hh"
41
42//	core class definitions
43#include "lineNumber.hh"
44
45//	front end class definitions
46#include "token.hh"
47#include "renaming.hh"
48#include "view.hh"
49#include "moduleExpression.hh"
50#include "fileTable.hh"
51#include "directoryManager.hh"
52#include "syntacticPreModule.hh"
53#include "visibleModule.hh"  // HACK
54#include "userLevelRewritingContext.hh"
55#include "interpreter.hh"
56
57#include "global.hh"
58#define clear()			tokenSequence.clear();
59#define store(token)		tokenSequence.append(token)
60#define fragClear()		fragments.contractTo(0);
61#define fragStore(token)	fragments.append(token)
62//#define YYPARSE_PARAM	parseResult
63//#define PARSE_RESULT	(*((UserLevelRewritingContext::ParseResult*) parseResult))
64#define PARSE_RESULT	(*parseResult)
65
66#define CM		interpreter.getCurrentModule()
67#define CV		interpreter.getCurrentView()
68
69#include "lexerAux.hh"
70/*
71void lexerInitialMode();
72void lexerIdMode();
73void lexerCmdMode();
74void lexerFileNameMode();
75void lexerStringMode();
76void lexerLatexMode();
77bool handleEof();
78bool includeFile(const string& directory, const string& fileName, bool silent, int lineNr);
79//void eatComment(bool firstNonWhite);
80*/
81Vector<Token> singleton(1);
82Vector<Token> tokenSequence;
83Vector<Token> lexerBubble;
84Vector<Token> fragments;
85Vector<Token> moduleExpr;
86Vector<Token> opDescription;
87stack<ModuleExpression*> moduleExpressions;
88Renaming* currentRenaming = 0;
89SyntaxContainer* currentSyntaxContainer = 0;
90SyntaxContainer* oldSyntaxContainer = 0;
91
92Int64 number;
93Int64 number2;
94
95static void yyerror(UserLevelRewritingContext::ParseResult* parseResult, char *s);
96
97void cleanUpModuleExpression();
98void cleanUpParser();
99void missingSpace(const Token& token);
100%}
101%pure-parser
102%parse-param {UserLevelRewritingContext::ParseResult* parseResult}
103
104%union
105{
106  bool yyBool;
107  Int64 yyInt64;
108  const char* yyString;
109  Token yyToken;
110  ImportModule::ImportMode yyImportMode;
111  Interpreter::Flags yyFlags;
112  Interpreter::PrintFlags yyPrintFlags;
113  Interpreter::SearchKind yySearchKind;
114}
115
116%{
117int yylex(YYSTYPE* lvalp);
118%}
119
120%token <yyString> FILE_NAME_STRING UNINTERPRETED_STRING LATEX_STRING
121/*
122 *	Inert keywords: these are only recognized by lexer when in initial mode.
123 */
124%token <yyToken> KW_MOD KW_OMOD KW_VIEW
125%token KW_PARSE KW_NORMALIZE KW_REDUCE KW_REWRITE
126%token KW_LOOP KW_NARROW KW_XG_NARROW KW_MATCH KW_XMATCH KW_UNIFY KW_CHECK
127%token KW_GET KW_VARIANTS KW_VARIANT
128%token KW_EREWRITE KW_FREWRITE KW_SREWRITE
129%token KW_CONTINUE KW_SEARCH
130%token KW_SET KW_SHOW KW_ON KW_OFF
131%token KW_TRACE KW_BODY KW_BUILTIN KW_WHOLE KW_SELECT KW_DESELECT KW_CONDITION KW_SUBSTITUTION
132%token KW_PRINT KW_GRAPH KW_MIXFIX KW_FLAT KW_ATTRIBUTE KW_NEWLINE
133%token KW_WITH KW_PARENS KW_ALIASES KW_GC KW_TIME KW_STATS KW_TIMING
134%token KW_CMD KW_BREAKDOWN KW_BREAK KW_PATH
135%token KW_MODULE KW_MODULES KW_VIEWS KW_ALL KW_SORTS KW_OPS2 KW_VARS
136%token KW_MBS KW_EQS KW_RLS KW_SUMMARY KW_KINDS KW_ADVISE KW_VERBOSE
137%token KW_DO KW_CLEAR
138%token KW_PROTECT KW_EXTEND KW_INCLUDE KW_EXCLUDE
139%token KW_CONCEAL KW_REVEAL KW_COMPILE KW_COUNT
140%token KW_DEBUG KW_IRREDUNDANT KW_RESUME KW_ABORT KW_STEP KW_WHERE KW_CREDUCE KW_SREDUCE KW_DUMP KW_PROFILE
141%token KW_NUMBER KW_RAT KW_COLOR
142%token <yyInt64> SIMPLE_NUMBER
143%token KW_PWD KW_CD KW_PUSHD KW_POPD KW_LS KW_LOAD KW_QUIT KW_EOF KW_TEST KW_SMT_SEARCH
144
145/*
146 *	Start keywords: signal end of mixfix statement if following '.'.
147 */
148%token <yyToken> KW_ENDM KW_IMPORT KW_ENDV
149%token <yyToken> KW_SORT KW_SUBSORT KW_OP KW_OPS KW_MSGS KW_VAR KW_CLASS KW_SUBCLASS
150%token <yyToken> KW_MB KW_CMB KW_EQ KW_CEQ KW_RL KW_CRL
151
152/*
153 *	Mid keywords: need to be recognized in the middle of mixfix syntax.
154 */
155%token <yyToken> KW_IS KW_FROM
156%token <yyToken> KW_ARROW KW_ARROW2 KW_PARTIAL KW_IF
157%type <yyToken> ':' '=' '(' ')' '.' '<' '[' ']' ',' '|'
158
159/*
160 *	Module expression keywords.
161 */
162%token <yyToken> KW_LABEL KW_TO KW_COLON2
163%left <yyToken> '+'
164%left <yyToken> '*'
165%type <yyToken> '{' '}'
166
167/*
168 *	Attribute keywords need to be recognized when parsing attributes.
169 */
170%token <yyToken> KW_ASSOC KW_COMM KW_ID KW_IDEM KW_ITER
171%token <yyToken> KW_LEFT KW_RIGHT KW_PREC KW_GATHER KW_METADATA KW_STRAT KW_POLY
172%token <yyToken> KW_MEMO KW_FROZEN KW_CTOR KW_LATEX KW_SPECIAL KW_CONFIG KW_OBJ KW_MSG
173%token <yyToken> KW_DITTO KW_FORMAT
174%token <yyToken> KW_ID_HOOK KW_OP_HOOK KW_TERM_HOOK
175
176/*
177 *	Command keywords need to be recognized when parsing commands.
178 */
179%token <yyToken> KW_IN
180
181/*
182 *	Special tokens.
183 */
184%token <yyToken> IDENTIFIER NUMERIC_ID ENDS_IN_DOT
185
186/*
187 *	This is a dummy token that is never passed by the lexer but by
188 *	giving this as an alternative we force the parser to lookahead
189 *	one token and allow the lexer to grab a bubble.
190 */
191%token FORCE_LOOKAHEAD
192
193/*
194 *	Nonterminals that return tokens.
195 */
196%type <yyToken> identifier inert startKeyword startKeyword2 midKeyword attrKeyword attrKeyword2
197%type <yyToken> token endsInDot badType
198%type <yyToken> tokenBarColon
199%type <yyToken> tokenBarDot
200%type <yyToken> cTokenBarIn
201%type <yyToken> cTokenBarLeftIn cTokenBarDotNumber cTokenBarDotRight
202%type <yyToken> cSimpleTokenBarDot
203%type <yyToken> cTokenBarDotCommaRight cTokenBarDotCommaNumber
204%type <yyToken> sortName sortToken startModule sortDot
205
206/*
207 *	Nonterminals that return Interpreter::SearchKind.
208 */
209%type <yySearchKind> search
210/*
211 *	Nonterminals that return bool.
212 */
213%type <yyBool> polarity select match optDebug optIrredundant conceal exclude arrow
214/*
215 *	Nonterminals that return int.
216 */
217%type <yyInt64> optNumber
218/*
219 *	Nonterminals that return ImportMode.
220 */
221%type <yyImportMode> importMode
222/*
223 *	Nonterminals that return Flags.
224 */
225%type <yyFlags> traceOption
226/*
227 *	Nonterminals that return PrintFlags.
228 */
229%type <yyPrintFlags> printOption
230
231%start top
232
233%%
234
235top		:	item { YYACCEPT; }
236		|
237			{
238			  PARSE_RESULT = UserLevelRewritingContext::QUIT;
239			}
240		;
241
242item		:	module
243		|	view
244		|	directive
245		|	command
246		;
247
248/*
249 *	Directives.
250 */
251directive	:	KW_IN		{ lexerFileNameMode(); }
252			FILE_NAME_STRING
253			{
254			  int lineNr = lineNumber;
255			  //eatComment(false); // eat \n so that line number is correct
256			  string directory;
257			  string fileName;
258			  if (findFile($3, directory, fileName, lineNr))
259			    includeFile(directory, fileName, false, lineNr);
260			}
261		|	KW_LOAD		{ lexerFileNameMode(); }
262			FILE_NAME_STRING
263			{
264			  int lineNr = lineNumber;
265			  //eatComment(false); // eat \n so that line number is correct
266			  string directory;
267			  string fileName;
268			  if (findFile($3, directory, fileName, lineNr))
269			    includeFile(directory, fileName, true, lineNr);
270			}
271		|	KW_PWD
272			{
273			  cout << directoryManager.getCwd() << '\n';
274			}
275		|	KW_CD		{ lexerFileNameMode(); }
276			FILE_NAME_STRING
277			{
278			  string directory;
279			  directoryManager.realPath($3, directory);
280			  if (!directoryManager.cd(directory))
281			    {
282			      IssueWarning(LineNumber(lineNumber) <<
283					   ": cd failed");
284			    }
285			}
286		|	KW_PUSHD	{ lexerFileNameMode(); }
287			FILE_NAME_STRING
288			{
289			  string directory;
290			  directoryManager.realPath($3, directory);
291			  if (directoryManager.pushd(directory) == UNDEFINED)
292			    {
293			      IssueWarning(LineNumber(lineNumber) <<
294					   ": pushd failed");
295			    }
296			}
297		|	KW_POPD
298			{
299			  const char* path = directoryManager.popd();
300			  if (path != 0)
301			    cout << path << '\n';
302			  else
303			    {
304			      IssueWarning(LineNumber(lineNumber) <<
305					   ": popd failed");
306			    }
307			}
308		|	KW_LS		{ lexerStringMode(); }
309			UNINTERPRETED_STRING
310			{
311			  system((string("ls") + $3).c_str());
312			}
313		|	KW_QUIT
314			{
315			  PARSE_RESULT = UserLevelRewritingContext::QUIT;
316			  YYACCEPT;
317			}
318		|	KW_EOF
319			{
320			  if(!handleEof())
321			    {
322			      PARSE_RESULT = UserLevelRewritingContext::QUIT;
323			    }
324			}
325		;
326