1\DOC add_listform
2
3\BLTYPE
4add_listform :
5  {separator : pp_element list, leftdelim : pp_element list,
6   rightdelim : pp_element list, cons : string, nilstr : string,
7   block_info : term_grammar.block_info } ->
8  unit
9\ELTYPE
10
11\SYNOPSIS
12Adds a ``list-form'' to the built-in grammar, allowing the parsing of
13strings such as {[a; b; c]} and {{}}.
14
15\KEYWORDS
16parsing, prettyprinting
17
18\LIBRARY
19Parse
20
21\DESCRIBE
22The {add_listform} function allows the user to augment the HOL parser
23with rules so that it can turn a string of the form
24{
25   <ld> str1 <sep> str2 <sep> ... strn <rd>
26}
27into the term
28{
29   <cons> t1 (<cons> t2 ... (<cons> tn <nilstr>))
30}
31where {<ld>} is the left delimiter string, {<rd>} the right
32delimiter, and {<sep>} is the separator string from the fields of the
33record argument to the function.  The various {stri} are strings
34representing the {ti} terms.  Further, the grammar will also parse
35{<ld> <rd>} into {<nilstr>}.
36
37The {pp_element} lists passed to this function for the {separator},
38{leftdelim} and {rightdelim} fields are interpreted as by the
39{add_rule} function.  These lists must have exactly one {TOK} element
40(this provides the string that will be printed), and other formatting
41elements such as {BreakSpace}.
42
43The {block_info} field is a pair consisting of a ``consistency''
44({PP.CONSISTENT}, or {PP.INCONSISTENT}), and an indentation depth (an
45integer).  The standard value for this field is {(PP.INCONSISTENT,0)},
46which will cause lists too long to fit in a single line to print with
47as many elements on the first line as will fit, and for subsequent
48elements to appear unindented on subsequent lines.  Changing the
49``consistency'' to {PP.CONSISTENT} would cause lists too long for a
50single line to print with one element per line.  The indentation level
51number specifies the number of extra spaces to be inserted when a
52line-break occurs.
53
54In common with the {add_rule} function, there is no requirement that
55the {cons} and {nilstr} fields be the names of constants; the
56parser/grammar combination will generate variables with these names if
57there are no corresponding constants.
58
59The HOL pretty-printer is simultaneously aware of the new rule, and
60terms of the forms above will print appropriately.
61
62\FAILURE
63Fails if any of the {pp_element} lists are ill-formed: if they include
64{TM}, {BeginFinalBlock}, or {EndInitialBlock} elements, or if do not
65include exactly one {TOK} element.  Subsequent calls to the term
66parser may also fail or behave unpredictably if the strings chosen for
67the various fields above introduce precedence conflicts.  For example,
68it will almost always be impossible to use left and right delimiters
69that are already present in the grammar, unless they are there as the
70left and right parts of a closefix.
71
72\EXAMPLE
73The definition of the ``list-form'' for lists in the HOL distribution
74is:
75{
76   add_listform {separator = [TOK ";", BreakSpace(1,0)],
77                 leftdelim = [TOK "["], rightdelim = [TOK "]"],
78                 cons = "CONS", nilstr = "NIL",
79                 block_info = (PP.INCONSISTENT, 0)};
80}
81while the set syntax is defined similarly:
82{
83   add_listform {leftdelim = [TOK "{"], rightdelim = TOK ["}"],
84                 separator = [";", BreakSpace(1,0)],
85                 cons = "INSERT", nilstr = "EMPTY",
86                 block_info = (PP.INCONSISTENT, 0)};
87}
88
89
90\USES
91Used to make sequential term structures print and parse more
92pleasingly.
93
94\COMMENTS
95As with other parsing functions, there is a {temp_add_listform}
96version of this function, which has the same effect on the global
97grammar, but which does not cause this effect to persist when the
98current theory is exported.
99
100\SEEALSO
101Parse.add_rule.
102\ENDDOC
103