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