1\DOC add_infix 2 3\TYPE {add_infix : string * int * HOLgrammars.associativity -> unit} 4 5\SYNOPSIS 6Adds a string as an infix with the given precedence and associativity 7to the term grammar. 8 9\KEYWORDS 10parsing, prettyprinting 11 12\LIBRARY 13Parse 14 15\DESCRIBE 16This function adds the given string to the global term grammar such 17that the string 18{ 19 <str1> s <str2> 20} 21will be parsed as 22{ 23 s <t1> <t2> 24} 25where {<str1>} and {<str2>} have been parsed to two terms 26{<t1>} and {<t2>}. The parsing process does not pay any attention to 27whether or not {s} corresponds to a constant or not. This resolution 28happens later in the parse, and will result in either a constant or a 29variable with name {s}. In fact, if this name is overloaded, the 30eventual term generated may have a constant of quite a different name 31again; the resolution of overloading comes as a separate phase (see 32the entry for {overload_on}). 33 34\FAILURE 35{add_infix} fails if the precedence level chosen for the new infix is 36the same as a different type of grammar rule (e.g., suffix or binder), 37or if the specified precedence level has infixes already but of a 38different associativity. 39 40It is also possible that the choice of string {s} will result in an 41ambiguous grammar. This will be marked with a warning. The parser 42may behave in strange ways if it encounters ambiguous phrases, but 43will work normally otherwise. 44 45\EXAMPLE 46Though we may not have {+} defined as a constant, we can still define 47it as an infix for the purposes of printing and parsing: 48{ 49 - add_infix ("+", 500, HOLgrammars.LEFT); 50 > val it = () : unit 51 52 - val t = Term`x + y`; 53 <<HOL message: inventing new type variable names: 'a, 'b, 'c.>> 54 > val t = `x + y` : term 55} 56We can confirm that this new infix has indeed been parsed 57that way by taking the resulting term apart: 58{ 59 - dest_comb t; 60 > val it = (`$+ x`, `y`) : term * term 61} 62With its new status, {+} has to be ``quoted'' with a 63dollar-sign if we wish to use it in a position where it is not an 64infix, as in the binding list of an abstraction: 65{ 66 - Term`\$+. x + y`; 67 <<HOL message: inventing new type variable names: 'a, 'b, 'c.>> 68 > val it = `\$+. x + y` : term 69 - dest_abs it; 70 > val it = (`$+`,`x + y`) : term * term 71} 72The generation of three new type variables in the examples 73above emphasises the fact that the terms in the first example and the 74body of the second are really no different from {f x y} (where {f} is 75a variable), and don't have anything to do with the constant for 76addition from {arithmeticTheory}. The new {+} infix is left 77associative: 78{ 79 - Term`x + y + z`; 80 <<HOL message: inventing new type variable names: 'a, 'b.>> 81 > val it = `x + y + z` : term 82 83 - dest_comb it; 84 > val it = (`$+ (x + y)`, `z`) : term * term 85} 86It is also more tightly binding than {/\} (which has 87precedence 400 by default): 88{ 89 - Term`p /\ q + r`; 90 <<HOL message: inventing new type variable names: 'a, 'b.>> 91 > val it = `p /\ q + r` : term 92 93 - dest_comb it; 94 > val it = (`$/\ p`, `q + r`) : term * term 95} 96An attempt to define a right associative operator at the 97same level fails: 98{ 99 Lib.try add_infix("-", 500, HOLgrammars.RIGHT); 100 101 Exception raised at Parse.add_infix: 102 Grammar Error: Attempt to have differently associated infixes 103 (RIGHT and LEFT) at same level 104} 105Similarly we can't define an infix at level 900, because 106this is where the (true prefix) rule for logical negation ({~}) is. 107{ 108 - Lib.try add_infix("-", 900, HOLgrammars.RIGHT); 109 110 Exception raised at Parse.add_infix: 111 Grammar Error: Attempt to have different forms at same level 112} 113Finally, an attempt to have a second {+} infix at a different 114precedence level causes grief when we later attempt to use the parser: 115{ 116 - add_infix("+", 400, HOLgrammars.RIGHT); 117 > val it = () : unit 118 119 - Term`p + q`; 120 <<HOL warning: Parse.Term: Grammar ambiguous on token pair + and +, 121 and probably others too>> 122 <<HOL message: inventing new type variable names: 'a, 'b, 'c>> 123 > val it = ``p + q`` : term 124} 125In this situation, the behaviour of the parser will become quite 126unpredictable whenever the {+} token is encountered. In particular, 127{+} may parse with either fixity. 128 129 130\USES 131Most use of infixes will want to have them associated with a 132particular constant in which case the definitional principles 133({new_infixl_definition} etc) are more likely to be appropriate. 134However, a development of a theory of abstract algebra may well want 135to have infix variables such as {+} above. 136 137\COMMENTS 138As with other functions in the {Parse} structure, there is a companion 139{temp_add_infix} function, which has the same effect on the global 140grammar, but which does not cause this effect to persist when the 141current theory is exported. 142 143\SEEALSO 144Parse.add_rule, Parse.add_listform, Parse.Term. 145 146\ENDDOC 147