The HOL parser Library

J. P. Van Tassel

University of Cambridge, Computer Laboratory

New Museums Site, Pembroke Street Cambridge, CB2 3QG, England.

July 1991 \begin{matrix}c \\ ◯ \end{matrix} J. P. Van Tassel 1991

Contents

1 The parser Library 1 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.3 Generating Parsers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

1.3.1 Auxiliary Files . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3.2 Running the Generated Parser . . . . . . . . . . . . . . . . . . . . . 5

1.4 Error Messages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.5 Internals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.6 Reserved Words . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.7 Action Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.8 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

1.8.1 Terminal Input and Errors . . . . . . . . . . . . . . . . . . . . . . . 10 1.8.2 HOL Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.8.3 Blocks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 1.8.4 Other Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

1.9 The Parser-Generating Language . . . . . . . . . . . . . . . . . . . . . . . 18

2 ML Functions in the parser Library 19

3 Pre-proved Theorems 21

References 23

Index 24 iv Contents

Chapter 1

The parser Library

That which can be conceived can be created. – Enzo Ferrari

1.1 Introduction

We describe a generic parser-generator to aid in the embedding of languages in HOL. The need for such a tool is becoming readily apparent as support for various languages in HOL has either been implemented or is in progress. The parser-generator described in this document was written to fulfill the needs of various projects underway in the Computer Laboratory dealing with either hardware description or programming languages.

The input to the generator is a form of modified BNF notation consisting of terminals, non-terminals, and action symbols. Users familiar with the definite clause grammar (DCG) notation of Prolog will see similarities here. This input is not, however, a full attribute grammar, and may originate either from the user’s terminal or a file. The output of the generator is an ML program that builds an object of user-defined type from input that meets the syntax specified by the grammar.

The discussion of the generator that follows will first cover the syntax of the input language. An overview of the translation process will then be delivered. It will be followed by a presentation of the generator’s reserved words, and an exposition of the construction of action symbols. We will conclude with some extended examples to demonstrate the use of the parser-generator.

1.2 Syntax

The generator is meant to deal with non left-recursive context free grammars. There is no checking for left-recursion, and any input employing it will necessarily cause an infinite loop to be generated. Action symbols are then embedded in the grammar to construct the user’s semantics for the syntax. If these symbols are not present, a simple recogniser for the language in question will be created.

As an example, if we wished to specify a grammar for a prefix representation of a subset of Boolean logic, the following BNF description might be used:

bool ::= term EOF
term ::= neg | imp | conj | disj | var
neg ::= NEG term
imp ::= IMP term term
conj ::= CONJ term term
disj ::= DISJ term term

where terminal symbols appear in boldface, var represents a Boolean variable, and EOF shows where the end of the input stream should occur.

The above grammar may be represented as input to the parser-generator as follows:

 FIRST_CHARS  `a b`.
 CHARS `a b c d`.
 MAIN_LOOP --> term [EOF].
 term --> neg | imp | conj | disj | {mk_var(TOKEN,":bool")}.
 conj --> [CONJ] {mk_conj(term,term)}.
 disj --> [DISJ] {mk_disj(term,term)}.
 neg --> [NEG] {mk_neg(term)}.
 imp --> [IMP] {mk_imp(term,term)}.

FIRST_CHARS and CHARS are declarations which define the legal first and other characters of the language’s identifiers. Within the grammar itself, action symbols are enclosed by braces ({}) whilst terminal symbols are delimited with square brackets ([]), and conditional branches are separated by vertical bars (|). The non-terminal MAIN_LOOP is a reserved symbol defining the start of the parser. The terminal symbol EOF is also reserved, and marks where the end of file should occur. The BNF syntax for the parsergenerator’s input language is provided in Section 1.9, and the system’s reserved words (including MAIN_LOOP and EOF) are described in Section 1.6.

1.3 Generating Parsers

The parser-generator may be incorporated into the HOL system by loading in the library parser. Once loaded, the generator is invoked by the function parse . Continuing with the Boolean logic example, the following session shows how a parser is generated from the grammar just specified.

1

 #parse();;
 Input file:  bool.grm
 Output file: bool
 Opening the file bool.ml (MAIN OUTPUT)
 Opening the file bool_decls.ml (DECLARATIONS)
 Load the declarations file before the main output.
 See the file bool_load.ml for a sample.
 See the file ./Makefile.bool for a sample Makefile.
 Output type: term
   Generating PARSE_file and PARSE_text (MAIN_LOOP used).
 () : void
 #quit();;

The generator prompts for an input file containing the grammar. It is assumed that the Boolean logic grammar is found in the file bool.grm. The second file is the beginning of the file name for the output of the generator. Since we want to create a HOL term using the generated parser, the appropritate type is supplied when prompted. The generator keys on the use of the non-terminal MAIN_LOOP to construct two functions to invoke the generated parser. PARSE_text allows target language constructs to be parsed from a ML string. PARSE_file provides the same functionality for input files containing these same objects.

1.3.1 Auxiliary Files

The first file created by the generator (bool_load.ml) is one that will load the parts of the newly-constructed parser into the HOL system in the proper order. In the current example, there are no user-specified actions. We therefore have no need to include any files other than the ones output by the parser-generator. The inital file loaded (general.ml) contains functions used by all generated parsers to provide basic operations. Once these functions have been loaded, declarations for each production are incorporated via the file bool decls.ml. They are in turn followed by a file holding the functions describing each production (bool.ml). The rationale behind the creation of these last two files is discussed in Section 1.5.

4 Chapter 1. The parser Library

% Generated parser load file
  First load some basic definitions: %
loadf `/usr/groups/hol/hol2/Library/parser/general`;;
% Insert any other files you want loaded here: %
% Now load the declarations: %
loadf `bool_decls`;;
% Finally load in the function definitions: %
loadf `bool`;;

No editing of the generated Makefile (./Makefile.bool) is required either. It simply compiles the generated files in the same order that they should be loaded. While compilation is not essential to use the generated parser, it is recommended. The system will run much faster. In order to make a compiled version of the parser, we need only execute the command make -f Makefile.bool all at the Unix prompt.

# Generated parser Makefile
# Version of HOL to be used:
HOL=/usr/groups/hol/hol2/hol
# General definitions for all generated parsers:
GENERAL=/usr/groups/hol/hol2/Library/parser/general
# Insert entries for user-defined stuff here:
# Remember to insert the appropriate dependencies and "load"'s below.
# Now compile the declarations:
bool_decls_ml.o: bool_decls.ml
        echo 'set_flag(`abort_when_fail`,true);;'\
             'loadf `$(GENERAL)`;;'\
             'compilet `bool_decls`;;'\
             'quit();;' | $(HOL)
# Finally do the actual functions
bool_ml.o: bool.ml bool_decls_ml.o
        echo 'set_flag(`abort_when_fail`,true);;'\
             'loadf `$(GENERAL)`;;'\
             'loadf `bool_decls`;;'\
             'compilet `bool`;;'\
             'quit();;' | $(HOL)
all: bool_ml.o
        @echo '===> Parser "bool" built.

NB: Both the load and make files are created every time the generator is run. It is therefore advisable to save a copy of each once their contents has been fixed.

1.3. Generating Parsers 5

1.3.2 Running the Generated Parser

We use the generated load file to install the parser in the HOL system. Note that the parser-generator is no longer needed. Invoking the function PARSE_text will then run the parser on the desired input. We have supplied a null list as both the second and third arguments to PARSE_text . The result is that only the default whitespace list (space, tab, and newline) is used to separate tokens. We will fully describe the nature of these arguments in Section 1.6, and an example their use appears in Section 1.8.2.3.

1

#loadf `bool_load`;;
................................................() : void
#PARSE_text(`IMP CONJ a b CONJ b a`,[],[]);;
"a /\ b ==> b /\ a" : term

We now introduce an error in the input to demonstrate the use of the debugging features of the system. The function debug_on puts the parser into debugging mode, and returns the previous debug state. Its converse is debug_off .

2

#PARSE_text(`IMP CON a b CONJ b a`,[],[]);;
evaluation failed     fail
#debug_on();;
false : bool
#PARSE_text (`IMP CON a b CONJ b a`,[],[]);;
ENTERING prdn "MAIN_LOOP": Curr. Token = "IMP"; Expected = "nil".
ENTERING prdn "term": Curr. Token = "IMP"; Expected = "nil".
ENTERING prdn "neg": Curr. Token = "IMP"; Expected = "nil".
ENTERING prdn "imp": Curr. Token = "IMP"; Expected = "nil".
ENTERING prdn "term": Curr. Token = "CON"; Expected = "nil".
ENTERING prdn "neg": Curr. Token = "CON"; Expected = "nil".
ENTERING prdn "imp": Curr. Token = "CON"; Expected = "nil".
ENTERING prdn "conj": Curr. Token = "CON"; Expected = "nil".
ENTERING prdn "disj": Curr. Token = "CON"; Expected = "nil".
ENTERING prdn "conj": Curr. Token = "IMP"; Expected = "nil".
ENTERING prdn "disj": Curr. Token = "IMP"; Expected = "nil".
evaluation failed     fail
#debug_off();;
true : bool
#PARSE_text(`IMP CONJ a b CONJ b a`,[],[]);;
"a /\ b ==> b /\ a" : term

The only mysterious part of the debugger is the Expected statement. It shows the character or language construct that should immediately follow the string currently being parsed. nil represents a “don’t care” case.

1.4 Error Messages

The parser-generator is quite sensitive to the context in which an error within the input grammar appears. Should an error be present, a message of the following form will occur.

 ERROR: symbol "symbol " encountered in the wrong place.
    -- Production: production
    -- Diagnostic: reason

symbol is the token that caused the error, production is the production in which it occurred, and reason is the reason that the parser-generator thinks might have caused the error.

1.5 Internals

We now present a short discussion of the internals of the parser-generator, as well as the design decisions that were made. The following were the main goals during the development of the generator.

• The order in which productions are specified should not be important

• Mutual recursion of productions should be allowed.

• Non-determinism within a given production should be possible (i.e. not just regular grammars).

• The output of any generated parser should be an object of user-defined type.

• The generator ought to operate in one pass.

Obstacles were presented to the first two of these goals by the way in which ML functions are declared and used. The difficulty is based on the fact that functions may not be used before they are defined, otherwise typechecking becomes problematic. As an illustration, if production A was to reference production B, then the function describing B must be defined in the ML system before the one specifying A. The result, therefore, is that production B would have to appear in the input grammar before production A. Even if the restriction of confining the user to a particular ordering of productions was adopted, it would still be insufficient to deal with the case where A and B are mutually recursive. The use of a gigantic let–and in ML would take care of the mutual recursion problem, but does not allow for the operation to be spread accross multiple files should one decide to structure one’s grammar in that manner.

To overcome these problems, the following translation scheme was developed:

• Each production specified by the user generates two objects, each in a separate file.

• Objects in the first file are ML letref declarations specifying the input and output types of the function that will be generated.

• Objects in the second file are λ-expressions representing the functions that describe the productions.

• Objects from the second file are bound to objects in the first file via assignment.

• When a generated parser is compiled, the file containing the declarations is loaded first. The one containing the λ-expressions and their assignments to an object from the first file is loaded afterwards.

The result of the above process is that all functions are declared before they are used. The productions that the user specifies may therefore reference each other in any order. Furthermore, should the user wish to describe a parser in many files, the productions may reference each other across those files. The proviso is, of course, that all generated declarations are loaded into the system first when the generated parser is run.

Each generated parser maintains an internal stack of intermediate results. It is simply a list of ML objects of a user-defined type that have been built up during the course of the parser’s execution. This results stack is the only method of building the final object that is returned to the user, and is accessed via the POP reserved symbol mentioned in Section 1.6 and described in Section 1.7. It is modified through action symbols that the user imbeds in the grammar.

The parser-generator will handle non-determinism in productions. In order to implement this feature, it was necessary to build a backtracking mechanism into all generated parsers. It is based on ML failure-trapping, and simply creates a fail trap for each branch of a production. These traps are guaranteed to be hierarchical in nature by the way in which an input grammar is specified. A one character look-ahead is used to determine if the syntactic object currently being parsed is followed by useful input. If it is not, a failure results, and the backtracking mechanism is invoked.

1.6 Reserved Words

The generator makes use of several reserved words. They are all in upper case, and since the parser-generator is case-sensitive, will not conflict with user-defined functions of the same name expressed in either mixed or lower case.

• NON-TERMINAL:

– MAIN_LOOP — a production that the user specifies to describe the top-level parse loop. The generator senses its presence and outputs two wrappers to call the generated parser in a properly initialised state. It may not be called from within the grammar at any time.

• TERMINAL:

– EOF — specifies when the end of file may occur.

• ARGUMENTS: The following can only appear as arguments to action symbols. Their presence anywhere else in the input grammar will cause a fatal error. Their types are given parenthetically.

– POP (:user-defined) — returns the most recent previously constructed result from the results list.

– TOKEN (:string) — returns a legal token identifier as specified using the constructs below. Successive calls to TOKEN will cause new identifiers to be obtained from the input source.

– WORD (:string) — returns the current string in the input stream. No checking of any kind is performed. The construct is particularly useful for dealing with arbitrary objects in the language that the user wants to treat specially.

• DECLARATIONS: Both FIRST_CHARS and CHARS below must appear for the parsergenerator to construct a tokeniser. If one is present without the other, a fatal error results. They may not be multiply defined within the same grammar.

– FIRST_CHARS — Used to specify a whitespace-separated string of characters representing the legal first characters of identifiers. It may not be empty.

– CHARS — Used to specify a whitespace-separated string of characters representing the other legal characters of identifiers. It may not be empty.

– USEFUL — Used to tell the generated parser those characters delineating a useful block of text which should be concatenated into a single string. It takes the form of an association list, where each member of the list has the type (string#string). The first element of the pair is the character which begins the block, and the second is the one that terminates it. The generator does not check the syntax or type of the list, and it is incumbent upon the user to make sure that it is well-formed.

– IGNORE – The converse of USEFUL. It is an association list of the same form as USEFUL, but is used to specify the beginning and ending of blocks of text which may be thrown away by generated parser as it is reading in input. The declaration is particularly useful in removing comments from an input stream before it is passed to the parser.

• FUNCTIONS:

– PARSE_file — The first function derived from the production MAIN_LOOP . Its name therefore cannot be used as the name of a non-terminal, or as an argument to an action symbol. The function takes three arguments. The first is the name of the input file, and is a standard ML string. If terminal I/O is desired, `nil` should be supplied. The second argument is of type string list, and represents the whitespace used by the language. Supplying a null list ([]) will trigger the use of the default list of blank, tab and newline. The final argument is used to describe special delimiting characters and those that may follow them to make a valid token. It is an association list of type (string # string list) list where the first element of each pair is the delimiting character, and the second is the list of following characters. A null following list means that the special character is a token by itself. If a null list is provided as the argument, the only separators used will be those contained in the whitespace list.

– PARSE_text — Another function created by the production MAIN_LOOP . Its arguments are the same as for PARSE_file with the exception of the first one. Here the language constructs to be parsed are directly stated as a ML string. It is important to remember to include the standard escape character in these strings when required. Failure to do so, can cause much frustration.

– TOKEN — The name of the generated tokeniser function.

– TOKEN_1 — The name of a helping function for TOKEN.

– chop_off, close_file, complete_separator, debug_enter, debug_off,
debug_on, debug_return, determine_lst, do_return, do_return_1,
eat_terminal, e_w_s, e_w_s_ok, get_word, get_word1, get_word2, gnt,
open_file, pop, push, read_char, read_input, write_string — These are

functions that are used by all generated parsers, and cannot be used as names for the user’s action symbols or productions.

1.7 Action Symbols

These are specified by the user outside the context of the grammar (i.e. in a separate file). Their arguments may be any of the reserved arguments just mentioned, non-terminals, or actual ML expressions. The parser-generator assumes that these functions exist, and simply creates a call to them. It is up to the user to make sure that the actual functions are well-typed with respect to the generated call.

EXAMPLES:

• {action} — Generates a call to the user-defined function action. It is assumed that action has () as its argument.

• {action(prdn)} — Generates a call to the user-defined function action, with the result of the elaboration of the non-terminal prdn as its argument. Since the execution of a non-terminal results in an object of user-defined type, the function action should reflect this in its specification.

• {action(prdn1,prdn2)} — Same as above. The non-terminals prdn1 and prdn2 are evaluated in sequence before the results are passed to action.

• {action(TOKEN)} — Evalutates the current input string as an identifier as specified by FIRST_CHARS and CHARS and passes the result to action. If there is no current string, one is fetched from the input source.

• {action(TOKEN,TOKEN)} — Same as above. The current string and the next one read from the input source are evaluated as identifiers, and passed to action in left-to-right order as arguments.

• {action(POP)} — The most recent previous result is removed from the result list, and passed as an argument to action.

• {action(POP,POP)} — Same as above. The most recent previous result is passed as the second argument to action, while the one before it is sent as the first argument.

       • {action(POP,TOKEN,prdn,POP)} — The calls to POP are first elaborated in

the manner just described (i.e. the most recent previous result will be passed as the last argument to action, while the one before that will be the first one). TOKEN is then executed before the non-terminal prdn is expanded. After prdn returns, the four results are passed to action.

1.8 Examples

In the examples that follow, we assume that the parser-generator has been loaded into the HOL system.

1.8.1 Terminal Input and Errors

The following session demonstrates the generator’s ability to understand input from the user’s console. Providing nil as the input file allows the user to specify a grammmar in an interactive manner. In the current example, there is an error in the grammar which causes an error message to be output .

1

 #parse();;
 Input file:  nil
 Output file: foo
 Opening the file foo.ml (MAIN OUTPUT)
 Opening the file foo_decls.ml (DECLARATIONS)
 Load the declarations file before the main output.
 See the file foo_load.ml for a sample.
 See the file ./Makefile.foo for a sample Makefile.
 Output type: term
 foo --> [A] get_word.
 evaluation failed
 ERROR: symbol "get_word" encountered in the wrong place.
    -- Production: foo
    -- Diagnostic: "get_word" is a system function.

Similar messages will be output for various classes of errors. An effort was made to trap all possible errors, and generate an appropriate message. The user should note, however, that there are probably unforeseen combinations of inputs not reflected in the trapping mechanism.

1.8. Examples 11

1.8.2 HOL Types

We now present a more complex example, the subject of which is a re-implementation of the HOL type parser. Points of interest include user-defined action symbols, operator precedences, and seamless integration of the parser with the HOL system. 1.8.2.1 The Grammar

FIRST_CHARS `a b c d e f g h i j k l m n o p q r s t u v w x y z
             A B C D E F G H I J K L M N O P Q R S T U V W X Y Z *`.
CHARS `a b c d e f g h i j k l m n o p q r s t u v w x y z
       A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
       1 2 3 4 5 6 7 8 9 0 *`.
tyname --> {mk_type_name(TOKEN)}.
tyvar --> {mk_type_var(TOKEN)}.
MAIN_LOOP --> typ [EOF].
typ --> type1 more_type.
more_type --> [#] {add_to_list(type1,POP)} more_prod_type sum_or_fun_type
            | [->] {MK_bin_type(`fun`,POP,typ)}
            | [+] type1 more_sum_type fun_type
            | [].
more_prod_type --> [#] {add_to_list(type1,POP)} more_prod_type
                 | {MK_defd_type(POP,`prod`)}.
sum_or_fun_type --> [+] {MK_bin_type(`sum`,POP,typ)}
                  | [->] {MK_bin_type(`fun`,POP,typ)}
                  | [].
more_sum_type --> [+] {add_to_list_rev(POP,POP)} type1 more_sum_type
                | [#] {add_to_list(type1,POP)} more_prod_type more_sum_type
                | {add_to_list_rev(POP,POP)} {MK_defd_type(POP,`sum`)}.
fun_type --> [->] {MK_bin_type(`fun`,POP,typ)} | [].
type1 --> [(] typ poss_cmpnd_type | tyname more_type1 | tyvar more_type1.
poss_cmpnd_type --> [)] more_type1 | [,] {add_to_list(POP,typ)} rest_of_cmpnd.
rest_of_cmpnd --> [,] {add_to_list(POP,typ)} rest_of_cmpnd
                | [)] {MK_type(POP,TOKEN)} more_type1.
more_type1 --> {MK_type(POP,TOKEN)} more_type1 | [].

The grammar used to specify the type parser is slightly more complex to specify than the Boolean logic example. The main difference is in the need to have a notion of operator precedence (-> > + > #). In order to preserve the ordering, it becomes necessary to make separate productions for each operator.

The action symbols used in the grammar all create an object of type type list. The reason for creating lists of types rather than types by themselves is based on the need to gather together arbitrarily many types to form a single one. This grouping into a list is a standard ploy when developing grammars for parsers where the final object to be created is dependent upon an unknown number of like objects.

1.8.2.2 Running the Generator

The parser-generator is run in exactly the same fashion as for the Boolean logic example. The only difference is in supplying type list as the output type of the generated parser.

1

 #parse();;
 Input file:  types.grm
 Output file: types
 Opening the file types.ml (MAIN OUTPUT)
 Opening the file types_decls.ml (DECLARATIONS)
 Load the declarations file before the main output.
 See the file types_load.ml for a sample.
 See the file ./Makefile.types for a sample Makefile.
 Output type: type list

  Generating PARSE_file and PARSE_text (MAIN_LOOP used).
 () : void
 #quit();;

1.8.2.3 Auxiliary Files

The first auxiliary file is not machine-generated. It contains all the functions used as action symbols within the grammar. mk_type_name and mk_type_var are the lowest-level functions, and create type lists from primitive types and type variables. add_to_list and add_to_list_rev group individual type lists into a single monolithic one. A reversed list of types is required to make sure that subcomponents of types associate properly. MK_type is the same as the standard ML function mk_type with the exception that it returns a type list. MK_bin_type is used to return a type list resulting from the creation of a type from a binary type operator. MK_defd_type uses fix_defd to create a properly associated type from a reversed list of types.

 let mk_type_name thing = [mk_type(thing,[])]
 and mk_type_var thing = [mk_vartype thing]
 and add_to_list (lst,thing) = append lst thing
 and add_to_list_rev (lst,thing) = append thing lst
 and MK_type(lst,op) = [mk_type(op,lst)]
 and MK_bin_type(op,type1,typ) = [mk_type(op,(append type1 typ))];;
 letrec fix_defd(lst,op,result) =
     if null lst then result
     else fix_defd(tl lst,op,mk_type(op,[hd lst;result]));;
 let MK_defd_type(lst,op) =
     [fix_defd(tl (tl lst),op,mk_type(op,[hd (tl lst);hd lst]))];;

Several additions have been made to the generated load file. The first is to load in the file of action function definitions just described (types_help.ml). Next, we have defined a list of separators to allow the lexical analyzer to break up the input stream into meaningful tokens in the possible absence of standard whitespace. The function parse is defined to call PARSE_text with the appropriate arguments, and to return the head of the result of its computation (a HOL type). new_syntax_block is a function provided as a part of HOL Version 1.12, and passes the string between its first and second arguments to the function named by its third. While not strictly necessary, the functionality provided by new_syntax_block makes input to the generated parser visually more appealing.

 % Generated parser load file
   First load some basic definitions: %
 loadf `/usr/groups/hol/hol2/Library/parser/general`;;
 % Insert any other files you want loaded here: %
 loadf `types_help`;;
 % Now load the declarations: %
 loadf `types_decls`;;
 % Finally load in the function definitions: %
 loadf `types`;;
 let SEPS = [(`(`,[]);(`)`,[]);(`#`,[]);(`-`,[`>`]);(`+`,[]);(`,`,[])];;
 let parse thing = hd (PARSE_text(thing,[],SEPS));;
 new_syntax_block(`<<`,`>>`,`parse`);;

The changes to the generated Makefile (Makefile.types) are less extensive. We have added a rule to deal with the compilation of the file of action functions. The new rule has then been linked into the dependencies of the parser’s compilation through its inclusion on the object list of types_decls_ml.o.

# Generated parser Makefile
# Version of HOL to be used:
HOL=/usr/groups/hol/hol2/hol
# General definitions for all generated parsers:
GENERAL=/usr/groups/hol/hol2/Library/parser/general
# Insert entries for user-defined stuff here:
# Remember to insert the appropriate dependencies and "load"'s below.
types_help_ml.o: types_help.ml
echo 'set_flag(`abort_when_fail`,true);;'\
     'loadf `$(GENERAL)`;;'\
     'compilet `types_help`;;'\
     'quit();;' | $(HOL)
# Now compile the declarations:
types_decls_ml.o: types_decls.ml types_help_ml.o
echo 'set_flag(`abort_when_fail`,true);;'\
     'loadf `$(GENERAL)`;;'\
     'loadf `types_help`;;'\
     'compilet `types_decls`;;'\
     'quit();;' | $(HOL)
# Finally do the actual functions
types_ml.o: types.ml types_decls_ml.o
echo 'set_flag(`abort_when_fail`,true);;'\
     'loadf `$(GENERAL)`;;'\
     'loadf `types_help`;;'\
     'loadf `types_decls`;;'\
     'compilet `types`;;'\
     'quit();;' | $(HOL)
all: types_ml.o
@echo '===> Parser "types" built.'

1.8.2.4 Running the Generated Parser

Running the parser is the much same as for the Boolean logic example. The only significant change is in the mode of input, which has been provided by new_syntax_block. The first part of the following session deals with loading in the generated parser into the HOL system, and presents an example input.

1.8. Examples 15

1

#loadf `loader`;;
...................................................................() : void
#":bool";;
":bool" : type
#<< bool >>;;
":bool" : type

Since we have re-implemented the HOL type parser, we have every reason to expect that our parser constructs types that are indistinguishable from those created by the system. We should also anticipate that our parser will not construct invalid types, while at the same time remaining sensitive to any additional ones created by the user. The continuation of the previous session demonstrates these properties. Also shown is the way in which the SEPS list (declared in the load file) permits a more natural style of input.

2

#":((* # (ind -> bool))list list + *list # * list -> *)list";;
":(((* # (ind -> bool))list)list + *list # (*)list -> *)list" : type
#<< ((* # (ind -> bool))list list + *list # * list -> *)list >>;;
":(((* # (ind -> bool))list)list + *list # (*)list -> *)list" : type
#":((bool,ind)fun,(*,*1)prod)sum";;
":(bool -> ind) + * # *1" : type
#<< ((bool,ind)fun,(*,*1)prod)sum >>;;
":(bool -> ind) + * # *1" : type
#":(bool,ind,*)tri";;
evaluation failed     mk_type in quotation
#<< (bool,ind,*)tri >>;;
evaluation failed     fail
#new_theory`tri`; new_type 3 `tri`;;
() : void
#":(bool,ind,*)tri";;
":(bool,ind,*)tri" : type
#<< (bool,ind,*)tri >>;;
":(bool,ind,*)tri" : type

1.8.3 Blocks

Here we demonstrate the use of the block declarations IGNORE and USEFUL . While the grammar will be trivial, the concept it shows is important. We will only present the grammar, and examples of the generated parser. The generation process is the same as for the previous examples.

1.8.3.1 The Grammar

The following grammar shows the pattern of input that is of interest. Note that no specification of legal characters is given, with the result that no token recogniser is generated. The USEFUL declaration states that all sequences of characters enclosed by single quotes should be concatenated into a single string. IGNORE describes the blocks that can be thrown away. The action symbol is a standard ML function that returns type void, which is also the type which should be provided to the generator.

 USEFUL [(`'`,`'`)].
 IGNORE [(`"`,`"`)].
 MAIN_LOOP --> foo [EOF].
 foo --> ['] {print_string(WORD)} ['] foo | [].

1.8.3.2 Running the Generated Parser

We provide below some sample input to the generated parser. It performs as expected.

1

 #loadf `blocks_load`;;
 ....................................() : void
 #PARSE_text(`'a;lsdkfj'`,[],[]);;
 a;lsdkfj() : void
 #PARSE_text(`'a;lsdkfj'"IIIIII'III"'MMMMM"""'`,[],[]);;
 a;lsdkfjMMMMM"""() : void

1.8.4 Other Examples

More examples are provided in the Examples directory distributed with the current version of the generator. See the READ-ME file associated with each for a brief description of the features. These additional examples are:

• Examples/HOL — A subset of the HOL term parser.

• Examples/ella — A parser for the the ELLA hardware description language.

• Examples/tiny — A for the programming language from the prog_logic88 library.

• Examples/user_guide — Examples used in this document:

       – blocks — The use of USEFUL and IGNORE .

1.8. Examples 17 – bool — Boolean logic.

– types — The HOL type parser.

1.9 The Parser-Generating Language

The BNF syntax for the parser-generator’s input grammar is described by the following productions. Items in typewriter font are the terminal symbols. A comment beginning and ending with the character % may appear anywhere in the grammar input to the generator.

grammar ::= declarations productions | productions declarations | productions declarations ::= first chars chars blocks | chars blocks first chars | blocks first chars chars first chars ::= FIRST_CHARS hol string . chars ::= CHARS hol string . hol string ::= (a standard ML string of whitespace-separated characters) blocks ::= useful ignore | ignore useful | useful | ignore | ϵ useful ::= USEFUL assoc list . ignore ::= IGNORE assoc list . assoc list ::= (a standard ML list of type (string#string))

productions ::= production name --> production productions
| ϵ
production ::= terminal prdn with choice
| one liner

terminal ::= [ terminal symbol ]

terminal symbol ::= (any alphanumeric character) terminal symbol
| \ special symbol terminal symbol
| ϵ

special symbol ::= { | } | \ | [ | ] production name ::= lead char (any sequence of alphanumeric characters) lead char ::= (any alphabetic character) action symbol ::= { action name optional args } optional args ::= ( args ) | ϵ action name ::= lead char (any sequence of alphanumeric characters) args ::= arg , args | arg

arg ::= TOKEN

       | WORD
       | POP

| production name
| ( HOL string or term)
prdn with choice ::= terminal prdn with choice
| action symbol prdn with choice
| production name prdn with choice
| | prdn with choice

                  | .

one liner ::= action symbol one liner
| production name one liner

           | .

Chapter 2

ML Functions in the parser Library

This chapter provides documentation on the single ML function that is made available in HOL when the parser library is loaded. This documentation is also available online via the help facility.

 parse

parse : (* -> void)

Synopsis

Top-level function to invoke the parser-generator.

Description

The function invokes the parser-generator. The generator prompts for various input files and types.

Failure

Fails if there is an error in the input grammar that specifies the operation of the parser to be generated. A descriptive message is produced to help pinpoint the cause of the failure.

Example

#parse();;
Input file:  foo.grm
Output file: foo
Opening the file foo.ml (MAIN OUTPUT)
Opening the file foo_decls.ml (DECLARATIONS)
Load the declarations file before the main output.
See the file foo_load.ml for a sample.
See the file ./Makefile.foo for a sample Makefile.
Output type: *

20 Chapter 2. ML Functions in the parser Library

Chapter 3

Pre-proved Theorems

22 Chapter 3. Pre-proved Theorems

References

[1] L. Sterling and E. Shapiro, The Art of Prolog: Advanced Programming Techniques, MIT Press, 1986.

[2] C.N. Fischer and R.J. LeBlanc, Jr., Crafting a Compiler, Benjamin/Cummings, 1988.

Index

action symbols, 9

CHARS, 2, 8, 9

chop_off, 9
close_file, 9
complete_separator, 9
debug_enter, 9
debug_off, 5, 9
debug_on, 5, 9
debug_return, 9

debugging, 5

deterimine_lst, 9
do_return, 9
do_return_1, 9
e_w_s_ok, 9
e_w_s, 9
eat_terminal, 9

EOF, 2, 7 error messages, 5, 6, 10

FIRST_CHARS, 2, 8, 9
FIRST_CHARS , 8
get_word, 9
get_word1, 9
get_word2, 9
gnt, 9

IGNORE, 8, 15, 16

MAIN_LOOP, 2, 3, 7–9
open_file, 9

parse, 2, 13, 19

PARSE_file, 3, 8, 9
PARSE_text, 3, 5, 9, 13

POP, 7, 8, 10

                                       pop, 9
                                       push, 9
                                       read_char, 9
                                       read_input, 9
                                       TOKEN, 8–10
                                       TOKEN_1, 9

USEFUL, 8, 15, 16

                                       WORD, 8
                                       write_string, 9