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