2 Author: Thomas C. Hales
4 As a new user of HOL-light, I have had a difficult time distinguishing
5 between the different uses of overloaded operators such as
6 (+), ( * ), (abs) (&), and so forth.
8 Their interpretation is context dependent, according to which of
9 prioritize_num, prioritize_int, and prioritize_real was most
12 This file removes all ambiguities in notation.
13 Following the usage of CAML, we append a dot to operations on real
14 numbers so that addition is (+.), etc.
16 In the same way, we remove ambiguities between natural numbers and
17 integers by appending a character. We have chosen to use
18 the character `|` for natural number operations
19 and the character `:` for integer operations.
21 The character `&` continues to denote the embedding of
22 natural numbers into the integers or reals.
24 HOL-light parsing does not permit an operator mixing alphanumeric
25 characters with symbols. Thus, we were not able to use (abs.)
26 and (abs:) for the absolute value. Instead we adapt the usual notation
27 |x| for absolute value and write it in prefix notation ||: and
28 ||. for the integer and real absolute value functions respectively.
30 In deference to HOL-light notation, we use ** for the exponential
31 function. There are three versions: ( **| ), ( **: ), and ( **. ).
35 (* natural number operations *)
39 let unambiguous_interface() =
40 parse_as_infix("+|",(16,"right"));
41 parse_as_infix("-|",(18,"left"));
42 parse_as_infix("*|",(20,"right"));
43 parse_as_infix("**|",(24,"left")); (* EXP *)
44 parse_as_infix("/|",(22,"right")); (* DIV *)
45 parse_as_infix("%|",(22,"left")); (* MOD *)
46 parse_as_infix("<|",(12,"right"));
47 parse_as_infix("<=|",(12,"right"));
48 parse_as_infix(">|",(12,"right"));
49 parse_as_infix(">=|",(12,"right"));
50 override_interface("+|",`(+):num->(num->num)`);
51 override_interface("-|",`(-):num->(num->num)`);
52 override_interface("*|",`( * ):num->(num->num)`);
53 override_interface("**|",`(EXP):num->(num->num)`);
54 override_interface("/|",`(DIV):num->(num->num)`);
55 override_interface("%|",`(MOD):num->(num->num)`);
56 override_interface("<|",`(<):num->(num->bool)`);
57 override_interface("<=|",`(<=):num->(num->bool)`);
58 override_interface(">|",`(>):num->(num->bool)`);
59 override_interface(">=|",`(>=):num->(num->bool)`);
60 (* integer operations *)
61 parse_as_infix("+:",(16,"right"));
62 parse_as_infix("-:",(18,"left"));
63 parse_as_infix("*:",(20,"right"));
64 parse_as_infix("**:",(24,"left"));
65 parse_as_infix("<:",(12,"right"));
66 parse_as_infix("<=:",(12,"right"));
67 parse_as_infix(">:",(12,"right"));
68 parse_as_infix(">=:",(12,"right"));
69 override_interface("+:",`int_add:int->int->int`);
70 override_interface("-:",`int_sub:int->int->int`);
71 override_interface("*:",`int_mul:int->int->int`);
72 override_interface("**:",`int_pow:int->num->int`);
74 override_interface("<:",`int_lt:int->int->bool`);
75 override_interface("<=:",`int_le:int->int->bool`);
76 override_interface(">:",`int_gt:int->int->bool`);
77 override_interface(">=:",`int_ge:int->int->bool`);
79 override_interface("--:",`int_neg:int->int`);
80 override_interface("&:",`int_of_num:num->int`);
81 override_interface("||:",`int_abs:int->int`);
82 (* real number operations *)
83 parse_as_infix("+.",(16,"right"));
84 parse_as_infix("-.",(18,"left"));
85 parse_as_infix("*.",(20,"right"));
86 parse_as_infix("**.",(24,"left"));
87 parse_as_infix("<.",(12,"right"));
88 parse_as_infix("<=.",(12,"right"));
89 parse_as_infix(">.",(12,"right"));
90 parse_as_infix(">=.",(12,"right"));
91 override_interface("+.",`real_add:real->real->real`);
92 override_interface("-.",`real_sub:real->real->real`);
93 override_interface("*.",`real_mul:real->real->real`);
94 override_interface("**.",`real_pow:real->num->real`);
96 override_interface("<.",`real_lt:real->real->bool`);
97 override_interface("<=.",`real_le:real->real->bool`);
98 override_interface(">.",`real_gt:real->real->bool`);
99 override_interface(">=.",`real_ge:real->real->bool`);
101 override_interface("--.",`real_neg:real->real`);
102 override_interface("&.",`real_of_num:num->real`);
103 override_interface("||.",`real_abs:real->real`);;
105 let ambiguous_interface() =
106 reduce_interface("+|",`(+):num->(num->num)`);
107 reduce_interface("-|",`(-):num->(num->num)`);
108 reduce_interface("*|",`( * ):num->(num->num)`);
109 reduce_interface("**|",`(EXP):num->(num->num)`);
110 reduce_interface("/|",`(DIV):num->(num->num)`);
111 reduce_interface("%|",`(MOD):num->(num->num)`);
112 reduce_interface("<|",`(<):num->(num->bool)`);
113 reduce_interface("<=|",`(<=):num->(num->bool)`);
114 reduce_interface(">|",`(>):num->(num->bool)`);
115 reduce_interface(">=|",`(>=):num->(num->bool)`);
116 (* integer operations *)
117 reduce_interface("+:",`int_add:int->int->int`);
118 reduce_interface("-:",`int_sub:int->int->int`);
119 reduce_interface("*:",`int_mul:int->int->int`);
120 reduce_interface("**:",`int_pow:int->num->int`);
122 reduce_interface("<:",`int_lt:int->int->bool`);
123 reduce_interface("<=:",`int_le:int->int->bool`);
124 reduce_interface(">:",`int_gt:int->int->bool`);
125 reduce_interface(">=:",`int_ge:int->int->bool`);
127 reduce_interface("--:",`int_neg:int->int`);
128 reduce_interface("&:",`int_of_num:num->int`);
129 reduce_interface("||:",`int_abs:int->int`);
131 reduce_interface("+.",`real_add:real->real->real`);
132 reduce_interface("-.",`real_sub:real->real->real`);
133 reduce_interface("*.",`real_mul:real->real->real`);
134 reduce_interface("**.",`real_pow:real->num->real`);
136 reduce_interface("<.",`real_lt:real->real->bool`);
137 reduce_interface("<=.",`real_le:real->real->bool`);
138 reduce_interface(">.",`real_gt:real->real->bool`);
139 reduce_interface(">=.",`real_ge:real->real->bool`);
141 reduce_interface("--.",`real_neg:real->real`);
142 reduce_interface("&.",`real_of_num:num->real`);
143 reduce_interface("||.",`real_abs:real->real`);;
145 (* add to Harrison's priorities the functions pop_priority and get_priority *)
146 let prioritize_int,prioritize_num,prioritize_real,pop_priority,get_priority =
147 let v = ref ([]:string list) in
148 let prioritize_int() =
150 overload_interface ("+",`int_add:int->int->int`);
151 overload_interface ("-",`int_sub:int->int->int`);
152 overload_interface ("*",`int_mul:int->int->int`);
153 overload_interface ("<",`int_lt:int->int->bool`);
154 overload_interface ("<=",`int_le:int->int->bool`);
155 overload_interface (">",`int_gt:int->int->bool`);
156 overload_interface (">=",`int_ge:int->int->bool`);
157 overload_interface ("--",`int_neg:int->int`);
158 overload_interface ("pow",`int_pow:int->num->int`);
159 overload_interface ("abs",`int_abs:int->int`);
160 override_interface ("&",`int_of_num:num->int`) and
163 overload_interface ("+",`(+):num->num->num`);
164 overload_interface ("-",`(-):num->num->num`);
165 overload_interface ("*",`(*):num->num->num`);
166 overload_interface ("<",`(<):num->num->bool`);
167 overload_interface ("<=",`(<=):num->num->bool`);
168 overload_interface (">",`(>):num->num->bool`);
169 overload_interface (">=",`(>=):num->num->bool`) and
172 overload_interface ("+",`real_add:real->real->real`);
173 overload_interface ("-",`real_sub:real->real->real`);
174 overload_interface ("*",`real_mul:real->real->real`);
175 overload_interface ("/",`real_div:real->real->real`);
176 overload_interface ("<",`real_lt:real->real->bool`);
177 overload_interface ("<=",`real_le:real->real->bool`);
178 overload_interface (">",`real_gt:real->real->bool`);
179 overload_interface (">=",`real_ge:real->real->bool`);
180 overload_interface ("--",`real_neg:real->real`);
181 overload_interface ("pow",`real_pow:real->num->real`);
182 overload_interface ("inv",`real_inv:real->real`);
183 overload_interface ("abs",`real_abs:real->real`);
184 override_interface ("&",`real_of_num:num->real`) and
186 if (length !v <= 1) then (print_string "priority unchanged\n") else
187 let (a::b::c) = !v in
189 print_string ("priority is now "^b^"\n");
191 "num" -> prioritize_num() |
192 "int" -> prioritize_int() |
193 "real"-> prioritize_real()|
196 if (!v=[]) then "unknown" else
199 prioritize_int,prioritize_num,prioritize_real,pop_priority,get_priority;;