Update from HH
[hl193./.git] / Jordan / parse_ext_override_interface.ml
1 (*
2         Author: Thomas C. Hales
3
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.
7
8         Their interpretation is context dependent, according to which of
9         prioritize_num, prioritize_int, and prioritize_real was most
10         recently called.
11
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.
15
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.
20
21         The character `&` continues to denote the embedding of 
22         natural numbers into the integers or reals.
23
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.
29
30         In deference to HOL-light notation, we use ** for the exponential
31         function.  There are three versions: ( **| ), ( **: ), and ( **. ).
32
33 *)
34
35 (* natural number operations *)
36
37
38
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`);
73 (* boolean *)
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`);
78 (* unary *)
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`);
95 (* boolean *)
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`);
100 (* unary *)
101 override_interface("--.",`real_neg:real->real`);
102 override_interface("&.",`real_of_num:num->real`);
103 override_interface("||.",`real_abs:real->real`);;
104
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`);
121 (* boolean *)
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`);
126 (* unary *)
127 reduce_interface("--:",`int_neg:int->int`);
128 reduce_interface("&:",`int_of_num:num->int`);
129 reduce_interface("||:",`int_abs:int->int`);
130 (* real *)
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`);
135 (* boolean *)
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`);
140 (* unary *)
141 reduce_interface("--.",`real_neg:real->real`);
142 reduce_interface("&.",`real_of_num:num->real`);
143 reduce_interface("||.",`real_abs:real->real`);;
144
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() = 
149   v:= "int"::!v;
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
161   prioritize_num() = 
162   v:= "num"::!v;
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
170   prioritize_real() =
171   v:= "real"::!v;
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
185   pop_priority() = 
186   if (length !v <= 1) then (print_string "priority unchanged\n") else
187   let (a::b::c) = !v in
188   v:= (b::c);
189   print_string ("priority is now "^b^"\n");
190   match a with
191     "num" -> prioritize_num() |
192     "int" -> prioritize_int() |
193     "real"-> prioritize_real()|
194     _ -> () and
195   get_priority() = 
196   if (!v=[]) then "unknown" else
197   let (a::b) = !v in a
198   in
199   prioritize_int,prioritize_num,prioritize_real,pop_priority,get_priority;;
200
201
202
203
204