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