text_formalization/jordan/parse_ext_override_interface.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Jordan                                                               *)
   5 (* Copied from HOL Light jordan directory *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-07-08                                                           *)
   8 (* ========================================================================== *)
   9
  10 module Parse_ext_override_interface = struct
  11
  12 (*
  13
  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.
  17
  18         Their interpretation is context dependent, according to which of
  19         prioritize_num, prioritize_int, and prioritize_real was most
  20         recently called.
  21
  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.
  25
  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.
  30
  31         The character `&` continues to denote the embedding of
  32         natural numbers into the integers or reals.
  33
  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.
  39
  40         In deference to HOL-light notation, we use ** for the exponential
  41         function.  There are three versions: ( **| ), ( **: ), and ( **. ).
  42
  43 *)
  44
  45 (* natural number operations *)
  46
  47
  48
  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`);
  83 (* boolean *)
  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`);
  88 (* unary *)
  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`);
 105 (* boolean *)
 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`);
 110 (* unary *)
 111 override_interface("--.",`real_neg:real->real`);
 112 override_interface("&.",`real_of_num:num->real`);
 113 override_interface("||.",`real_abs:real->real`);;
 114
 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`);
 131 (* boolean *)
 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`);
 136 (* unary *)
 137 reduce_interface("--:",`int_neg:int->int`);
 138 reduce_interface("&:",`int_of_num:num->int`);
 139 reduce_interface("||:",`int_abs:int->int`);
 140 (* real *)
 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`);
 145 (* boolean *)
 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`);
 150 (* unary *)
 151 reduce_interface("--.",`real_neg:real->real`);
 152 reduce_interface("&.",`real_of_num:num->real`);
 153 reduce_interface("||.",`real_abs:real->real`);;
 154
 155 (* add to Harrison's priorities the functions pop_priority and get_priority *)
 156
 157 let prioritize_int,prioritize_num,prioritize_real,pop_priority,get_priority =
 158   let v = ref ([]:string list) in
 159   let prioritize_int() =
 160   v:= "int"::!v;
 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
 172   prioritize_num() =
 173   v:= "num"::!v;
 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
 181   prioritize_real() =
 182   v:= "real"::!v;
 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
 196   pop_priority() =
 197   if (length !v <= 1) then (print_string "priority unchanged\n") else
 198   let (a::b::c) = !v in
 199   v:= (b::c);
 200   print_string ("priority is now "^b^"\n");
 201   match a with
 202     "num" -> prioritize_num() |
 203     "int" -> prioritize_int() |
 204     "real"-> prioritize_real()|
 205     _ -> () and
 206   get_priority() =
 207   if (!v=[]) then "unknown" else
 208   let (a::b) = !v in a
 209   in
 210   prioritize_int,prioritize_num,prioritize_real,pop_priority,get_priority;;
 211
 212
 213 end;;